From 9330f3714e8858758a33c2f945ec01a2463aabc8 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 10 Apr 2016 15:38:47 -0400 Subject: [PATCH] DeepAndShallowEmbeddings: adding failure --- .gitignore | 1 + DeepAndShallowEmbeddings.v | 336 +++++++++++++++++++++++++++++++++++++ DeeperWithFailInterp.ml | 29 ++++ 3 files changed, 366 insertions(+) create mode 100644 DeeperWithFailInterp.ml diff --git a/.gitignore b/.gitignore index 55213b2..d9ca9f4 100644 --- a/.gitignore +++ b/.gitignore @@ -17,3 +17,4 @@ frap.tgz .coq-native Deep.ml* Deeper.ml* +DeeperWithFail.ml* diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index dd5a09f..c190804 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -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. diff --git a/DeeperWithFailInterp.ml b/DeeperWithFailInterp.ml new file mode 100644 index 0000000..f44a5b8 --- /dev/null +++ b/DeeperWithFailInterp.ml @@ -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