mirror of
https://github.com/achlipala/frap.git
synced 2024-11-28 07:16:20 +00:00
DeepAndShallowEmbeddings: adding failure
This commit is contained in:
Adam Chlipala
parent
290fec1e5b
commit
9330f3714e
3 changed files with 366 additions and 0 deletions
1
.gitignore
vendored
1
.gitignore
vendored
|
|
@ -17,3 +17,4 @@ frap.tgz
|
|||
.coq-native
|
||||
Deep.ml*
|
||||
Deeper.ml*
|
||||
DeeperWithFail.ml*
|
||||
|
|
|
|||
|
|
@ -655,3 +655,339 @@ Module Deeper.
|
|||
|
||||
Extraction "Deeper.ml" index_of.
|
||||
End Deeper.
|
||||
|
||||
|
||||
(** * Adding the possibility of program failure *)
|
||||
|
||||
Module DeeperWithFail.
|
||||
Inductive loop_outcome acc :=
|
||||
| Done (a : acc)
|
||||
| Again (a : acc).
|
||||
|
||||
Inductive cmd : Set -> Type :=
|
||||
| Return {result : Set} (r : result) : cmd result
|
||||
| Bind {result result'} (c1 : cmd result') (c2 : result' -> cmd result) : cmd result
|
||||
| Read (a : nat) : cmd nat
|
||||
| Write (a v : nat) : cmd unit
|
||||
| Loop {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) : cmd acc
|
||||
| Fail {result} : cmd result.
|
||||
|
||||
Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80).
|
||||
Notation "'for' x := i 'loop' c1 'done'" := (Loop i (fun x => c1)) (right associativity, at level 80).
|
||||
|
||||
Definition forever : cmd nat :=
|
||||
_ <- Write 0 1;
|
||||
for i := 1 loop
|
||||
h_i <- Read i;
|
||||
acc <- Read 0;
|
||||
match acc with
|
||||
| 0 => Fail
|
||||
| _ =>
|
||||
_ <- Write 0 (acc + h_i);
|
||||
Return (Again (i + 1))
|
||||
end
|
||||
done.
|
||||
|
||||
Inductive stepResult (result : Set) :=
|
||||
| Answer (r : result)
|
||||
| Stepped (h : heap) (c : cmd result)
|
||||
| Failed.
|
||||
|
||||
Implicit Arguments Failed [result].
|
||||
|
||||
Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
|
||||
match c with
|
||||
| Return r => Answer r
|
||||
| Bind c1 c2 =>
|
||||
match step c1 h with
|
||||
| Answer r => Stepped h (c2 r)
|
||||
| Stepped h' c1' => Stepped h' (Bind c1' c2)
|
||||
| Failed => Failed
|
||||
end
|
||||
| Read a => Answer (h $! a)
|
||||
| Write a v => Stepped (h $+ (a, v)) (Return tt)
|
||||
| Loop init body =>
|
||||
Stepped h (r <- body init;
|
||||
match r with
|
||||
| Done r' => Return r'
|
||||
| Again r' => Loop r' body
|
||||
end)
|
||||
| Fail => Failed
|
||||
end.
|
||||
|
||||
Fixpoint multiStep {result} (c : cmd result) (h : heap) (n : nat) : stepResult result :=
|
||||
match n with
|
||||
| O => Stepped h c
|
||||
| S n' => match step c h with
|
||||
| Answer r => Answer r
|
||||
| Stepped h' c' => multiStep c' h' n'
|
||||
| Failed => Failed
|
||||
end
|
||||
end.
|
||||
|
||||
Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop :=
|
||||
| HtReturn : forall P {result : Set} (v : result),
|
||||
hoare_triple P (Return v) (fun r h => P h /\ r = v)
|
||||
| HtBind : forall P {result' result} (c1 : cmd result') (c2 : result' -> cmd result) Q R,
|
||||
hoare_triple P c1 Q
|
||||
-> (forall r, hoare_triple (Q r) (c2 r) R)
|
||||
-> hoare_triple P (Bind c1 c2) R
|
||||
| HtRead : forall P a,
|
||||
hoare_triple P (Read a) (fun r h => P h /\ r = h $! a)
|
||||
| HtWrite : forall P a v,
|
||||
hoare_triple P (Write a v) (fun _ h => exists h', P h' /\ h = h' $+ (a, v))
|
||||
| HtConsequence : forall {result} (c : cmd result) P Q (P' : assertion) (Q' : _ -> assertion),
|
||||
hoare_triple P c Q
|
||||
-> (forall h, P' h -> P h)
|
||||
-> (forall r h, Q r h -> Q' r h)
|
||||
-> hoare_triple P' c Q'
|
||||
|
||||
| HtLoop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) I,
|
||||
(forall acc, hoare_triple (I (Again acc)) (body acc) I)
|
||||
-> hoare_triple (I (Again init)) (Loop init body) (fun r h => I (Done r) h)
|
||||
|
||||
| HtFail : forall {result},
|
||||
hoare_triple (fun _ => False) (Fail (result := result)) (fun _ _ => False).
|
||||
|
||||
Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" :=
|
||||
(hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level).
|
||||
|
||||
Lemma HtStrengthen : forall {result} (c : cmd result) P Q (Q' : _ -> assertion),
|
||||
hoare_triple P c Q
|
||||
-> (forall r h, Q r h -> Q' r h)
|
||||
-> hoare_triple P c Q'.
|
||||
Proof.
|
||||
simplify.
|
||||
eapply HtConsequence; eauto.
|
||||
Qed.
|
||||
|
||||
Lemma HtWeaken : forall {result} (c : cmd result) P Q (P' : assertion),
|
||||
hoare_triple P c Q
|
||||
-> (forall h, P' h -> P h)
|
||||
-> hoare_triple P' c Q.
|
||||
Proof.
|
||||
simplify.
|
||||
eapply HtConsequence; eauto.
|
||||
Qed.
|
||||
|
||||
Theorem forever_ok :
|
||||
{{ _ ~> True }}
|
||||
forever
|
||||
{{ _&_ ~> False }}.
|
||||
Proof.
|
||||
unfold forever.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
eapply HtConsequence.
|
||||
apply HtLoop with (I := fun r h => h $! 0 > 0 /\ match r with
|
||||
| Done _ => False
|
||||
| _ => True
|
||||
end); simplify.
|
||||
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
cases r1.
|
||||
eapply HtConsequence.
|
||||
apply HtFail.
|
||||
simplify.
|
||||
linear_arithmetic.
|
||||
simplify.
|
||||
linear_arithmetic.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
eapply HtStrengthen.
|
||||
econstructor.
|
||||
simplify.
|
||||
propositional; subst.
|
||||
invert H0; propositional; subst.
|
||||
simplify.
|
||||
linear_arithmetic.
|
||||
invert H0; propositional; subst.
|
||||
simplify.
|
||||
invert H; propositional; subst.
|
||||
simplify.
|
||||
linear_arithmetic.
|
||||
simplify.
|
||||
propositional.
|
||||
Qed.
|
||||
|
||||
Definition trsys_of {result} (c : cmd result) (h : heap) := {|
|
||||
Initial := {(c, h)};
|
||||
Step := fun p1 p2 => step (fst p1) (snd p1) = Stepped (snd p2) (fst p2)
|
||||
|}.
|
||||
|
||||
Lemma invert_Return : forall {result : Set} (r : result) P Q,
|
||||
hoare_triple P (Return r) Q
|
||||
-> forall h, P h -> Q r h.
|
||||
Proof.
|
||||
induct 1; propositional; eauto.
|
||||
Qed.
|
||||
|
||||
Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
|
||||
hoare_triple P (Bind c1 c2) Q
|
||||
-> exists R, hoare_triple P c1 R
|
||||
/\ forall r, hoare_triple (R r) (c2 r) Q.
|
||||
Proof.
|
||||
induct 1; propositional; eauto.
|
||||
|
||||
invert IHhoare_triple; propositional.
|
||||
eexists; propositional.
|
||||
eapply HtWeaken.
|
||||
eassumption.
|
||||
auto.
|
||||
eapply HtStrengthen.
|
||||
apply H4.
|
||||
auto.
|
||||
Qed.
|
||||
|
||||
Lemma unit_not_nat : unit = nat -> False.
|
||||
Proof.
|
||||
simplify.
|
||||
assert (exists x : unit, forall y : unit, x = y).
|
||||
exists tt; simplify.
|
||||
cases y; reflexivity.
|
||||
rewrite H in H0.
|
||||
invert H0.
|
||||
specialize (H1 (S x)).
|
||||
linear_arithmetic.
|
||||
Qed.
|
||||
|
||||
Lemma invert_Read : forall a P Q,
|
||||
hoare_triple P (Read a) Q
|
||||
-> forall h, P h -> Q (h $! a) h.
|
||||
Proof.
|
||||
induct 1; propositional; eauto.
|
||||
apply unit_not_nat in x0.
|
||||
propositional.
|
||||
Qed.
|
||||
|
||||
Lemma invert_Write : forall a v P Q,
|
||||
hoare_triple P (Write a v) Q
|
||||
-> forall h, P h -> Q tt (h $+ (a, v)).
|
||||
Proof.
|
||||
induct 1; propositional; eauto.
|
||||
symmetry in x0.
|
||||
apply unit_not_nat in x0.
|
||||
propositional.
|
||||
Qed.
|
||||
|
||||
Lemma invert_Loop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) P Q,
|
||||
hoare_triple P (Loop init body) Q
|
||||
-> exists I, (forall acc, hoare_triple (I (Again acc)) (body acc) I)
|
||||
/\ (forall h, P h -> I (Again init) h)
|
||||
/\ (forall r h, I (Done r) h -> Q r h).
|
||||
Proof.
|
||||
induct 1; propositional; eauto.
|
||||
|
||||
invert IHhoare_triple; propositional.
|
||||
exists x; propositional; eauto.
|
||||
Qed.
|
||||
|
||||
Lemma invert_Fail : forall result P Q,
|
||||
hoare_triple P (Fail (result := result)) Q
|
||||
-> forall h, P h -> False.
|
||||
Proof.
|
||||
induct 1; propositional; eauto.
|
||||
Qed.
|
||||
|
||||
Lemma step_sound : forall {result} (c : cmd result) h Q,
|
||||
hoare_triple (fun h' => h' = h) c Q
|
||||
-> match step c h with
|
||||
| Answer r => Q r h
|
||||
| Stepped h' c' => hoare_triple (fun h'' => h'' = h') c' Q
|
||||
| Failed => False
|
||||
end.
|
||||
Proof.
|
||||
induct c; simplify; propositional.
|
||||
|
||||
eapply invert_Return.
|
||||
eauto.
|
||||
simplify; auto.
|
||||
|
||||
apply invert_Bind in H0.
|
||||
invert H0; propositional.
|
||||
apply IHc in H0.
|
||||
cases (step c h); auto.
|
||||
econstructor.
|
||||
apply H2.
|
||||
equality.
|
||||
auto.
|
||||
econstructor; eauto.
|
||||
|
||||
eapply invert_Read; eauto.
|
||||
simplify; auto.
|
||||
|
||||
eapply HtStrengthen.
|
||||
econstructor.
|
||||
simplify; propositional; subst.
|
||||
eapply invert_Write; eauto.
|
||||
simplify; auto.
|
||||
|
||||
apply invert_Loop in H0.
|
||||
invert H0; propositional.
|
||||
econstructor.
|
||||
eapply HtWeaken.
|
||||
apply H0.
|
||||
equality.
|
||||
simplify.
|
||||
cases r.
|
||||
eapply HtStrengthen.
|
||||
econstructor.
|
||||
simplify.
|
||||
propositional; subst; eauto.
|
||||
eapply HtStrengthen.
|
||||
eapply HtLoop.
|
||||
auto.
|
||||
simplify.
|
||||
eauto.
|
||||
|
||||
eapply invert_Fail; eauto.
|
||||
simplify; eauto.
|
||||
Qed.
|
||||
|
||||
Lemma hoare_triple_sound' : forall P {result} (c : cmd result) Q,
|
||||
hoare_triple P c Q
|
||||
-> forall h, P h
|
||||
-> invariantFor (trsys_of c h)
|
||||
(fun p => hoare_triple (fun h => h = snd p)
|
||||
(fst p)
|
||||
Q).
|
||||
Proof.
|
||||
simplify.
|
||||
|
||||
apply invariant_induction; simplify.
|
||||
|
||||
propositional; subst; simplify.
|
||||
eapply HtConsequence.
|
||||
eassumption.
|
||||
equality.
|
||||
auto.
|
||||
|
||||
eapply step_sound in H1.
|
||||
rewrite H2 in H1.
|
||||
auto.
|
||||
Qed.
|
||||
|
||||
Theorem hoare_triple_sound : forall P {result} (c : cmd result) Q,
|
||||
hoare_triple P c Q
|
||||
-> forall h, P h
|
||||
-> invariantFor (trsys_of c h)
|
||||
(fun p => step (fst p) (snd p) <> Failed).
|
||||
Proof.
|
||||
simplify.
|
||||
|
||||
eapply invariant_weaken.
|
||||
eapply hoare_triple_sound'; eauto.
|
||||
simplify.
|
||||
eapply step_sound in H1.
|
||||
cases (step (fst s) (snd s)); equality.
|
||||
Qed.
|
||||
|
||||
Extraction "DeeperWithFail.ml" forever.
|
||||
End DeeperWithFail.
|
||||
|
|
|
|||
29
DeeperWithFailInterp.ml
Normal file
29
DeeperWithFailInterp.ml
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
let rec i2n n =
|
||||
match n with
|
||||
| 0 -> O
|
||||
| _ -> S (i2n (n - 1))
|
||||
|
||||
let interp c =
|
||||
let h : (nat, nat) Hashtbl.t = Hashtbl.create 0 in
|
||||
Hashtbl.add h (i2n 0) (i2n 2);
|
||||
Hashtbl.add h (i2n 1) (i2n 1);
|
||||
Hashtbl.add h (i2n 2) (i2n 8);
|
||||
Hashtbl.add h (i2n 3) (i2n 6);
|
||||
|
||||
let rec interp' (c : 'a cmd) : 'a =
|
||||
match c with
|
||||
| Return v -> v
|
||||
| Bind (c1, c2) -> interp' (c2 (interp' c1))
|
||||
| Read a ->
|
||||
Obj.magic (try
|
||||
Hashtbl.find h a
|
||||
with Not_found -> O)
|
||||
| Write (a, v) -> Obj.magic (Hashtbl.replace h a v)
|
||||
| Loop (i, b) ->
|
||||
begin match Obj.magic (interp' (Obj.magic (b i))) with
|
||||
| Done r -> r
|
||||
| Again r -> interp' (Loop (r, b))
|
||||
end
|
||||
| Fail -> failwith "Fail"
|
||||
|
||||
in h, interp' c
|
||||
Loading…
Reference in a new issue