diff --git a/Connecting.v b/Connecting.v index 05495ca..a8088f2 100644 --- a/Connecting.v +++ b/Connecting.v @@ -3,14 +3,12 @@ * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) -Require Import FrapWithoutSets SepCancel. -Require Import Arith.Div2. +Require Import Frap SepCancel ModelCheck Classes.Morphisms. +Require Import Arith.Div2 Eqdep. (** * Some odds and ends from past chapters *) -Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 30). - Ltac simp := repeat (simplify; subst; propositional; try match goal with | [ H : ex _ |- _ ] => invert H @@ -94,9 +92,9 @@ Hint Resolve shatter_word_0. Require Import Coq.Logic.Eqdep_dec. -Definition weq : forall {sz} (x y : word sz), {x = y} + {x <> y}. - refine (fix weq sz (x : word sz) : forall y : word sz, {x = y} + {x <> y} := - match x in word sz return forall y : word sz, {x = y} + {x <> y} with +Definition weq : forall {sz} (x y : word sz), sumbool (x = y) (x <> y). + refine (fix weq sz (x : word sz) : forall y : word sz, sumbool (x = y) (x <> y) := + match x in word sz return forall y : word sz, sumbool (x = y) (x <> y) with | WO => fun _ => left _ _ | WS b x' => fun y => if bool_dec b (whd y) then if weq _ x' (wtl y) then left _ _ else right _ _ @@ -113,199 +111,144 @@ Definition weq : forall {sz} (x y : word sz), {x = y} + {x <> y}. abstract (rewrite (shatter_word y); simpl; intro; apply n0; injection H; auto). Defined. +Lemma mod2_2times : forall n, + mod2 (2 * n) = false. +Proof. + induct n; simplify; auto. + replace (n + S (n + 0)) with (S (2 * n)) by linear_arithmetic. + assumption. +Qed. -(** * A simple C-like language with just two data types *) +Lemma mod2_plus1_2times : forall n, + mod2 (1 + 2 * n) = true. +Proof. + induct n; simplify; auto. + replace (n + S (n + 0)) with (S (2 * n)) by linear_arithmetic. + assumption. +Qed. + +Theorem adding_one_changes : forall sz (w : word sz), + sz > 0 + -> w ^+ ^1 <> w. +Proof. + propositional. + cases sz; try linear_arithmetic. + pose proof (shatter_word_S w); first_order; subst. + unfold wplus in H0. + simplify. + invert H0. + clear H3. + cases x. + replace (S (wordToNat x0 + (wordToNat x0 + 0)) + S (wordToNat (^ 0) + (wordToNat (^ 0) + 0))) + with (2 * (1 + wordToNat x0 + @wordToNat sz (^0))) in H2 by linear_arithmetic. + rewrite mod2_2times in H2; equality. + replace (wordToNat x0 + (wordToNat x0 + 0) + S (wordToNat (^ 0) + (wordToNat (^ 0) + 0))) + with (1 + 2 * (wordToNat x0 + @wordToNat sz (^0))) in H2 by linear_arithmetic. + rewrite mod2_plus1_2times in H2. + equality. +Qed. Module Type BIT_WIDTH. Parameter bit_width : nat. + Axiom bit_width_nonzero : bit_width > 0. End BIT_WIDTH. -Module DeeplyEmbedded(Import BW : BIT_WIDTH). + +(** * A modification of last chapter's language, to use words instead of naturals *) + + +Module MixedEmbedded(Import BW : BIT_WIDTH). Definition wrd := word bit_width. + Definition heap := fmap wrd wrd. - Inductive exp := - | Var (x : var) - - | Const (n : wrd) - | Add (x : var) (n : wrd) - - | Head (x : var) - | Tail (x : var) - - | NotNull (x : var). - - Inductive stmt := - | Skip - | Assign (x : var) (e : exp) - | WriteHead (x : var) (e : exp) - | WriteTail (x : var) (e : exp) - | Seq (s1 s2 : stmt) - | IfThenElse (e : exp) (s1 s2 : stmt) - | WhileLoop (e : exp) (s1 : stmt). - - Inductive type := - | Scalar - | ListPointer (t : type). - - Definition type_eq : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}. - decide equality. - Defined. - - Record function := { - Params : list (var * type); - Locals : list (var * type); - Return : type; - Body : stmt - }. - - Section fn. - Variable fn : function. - - Definition vars := Params fn ++ Locals fn ++ [("result", Return fn)]. - - Fixpoint varType (x : var) (vs : list (var * type)) : option type := - match vs with - | nil => None - | (y, t) :: vs' => if y ==v x then Some t else varType x vs' - end. - - Fixpoint expType (e : exp) : option type := - match e with - | Var x => varType x vars - | Const _ => Some Scalar - | Add x _ => match varType x vars with - | Some Scalar => Some Scalar - | _ => None - end - | Head x => match varType x vars with - | Some (ListPointer t) => Some t - | _ => None - end - | Tail x => match varType x vars with - | Some (ListPointer t) => Some (ListPointer t) - | _ => None - end - | NotNull x => match varType x vars with - | Some (ListPointer _) => Some Scalar - | _ => None - end - end. - - Fixpoint stmtWf (s : stmt) : bool := - match s with - | Skip => true - | Assign x e => match varType x vars, expType e with - | Some t1, Some t2 => - if type_eq t1 t2 then true else false - | _, _ => false - end - | WriteHead x e => match varType x vars, expType e with - | Some (ListPointer t1), Some t2 => - if type_eq t1 t2 then true else false - | _, _ => false - end - | WriteTail x e => match varType x vars, expType e with - | Some (ListPointer t1), Some (ListPointer t2) => - if type_eq t1 t2 then true else false - | _, _ => false - end - | Seq s1 s2 => stmtWf s1 && stmtWf s2 - | IfThenElse e s1 s2 => match expType e with - | Some Scalar => stmtWf s1 && stmtWf s2 - | _ => false - end - | WhileLoop e s1 => match expType e with - | Some Scalar => stmtWf s1 - | _ => false - end - end. - - Record functionWf : Prop := { - VarsOk : NoDup (map fst (Params fn ++ Locals fn)); - BodyOk : stmtWf (Body fn) = true - }. - End fn. - - Inductive value := - | VScalar (n : wrd) - | VList (p : wrd). - - Definition heap := fmap (wrd) (value * value). - Definition valuation := fmap var value. - - Inductive eval : heap -> valuation -> exp -> value -> Prop := - | VVar : forall H V x v, - V $? x = Some v - -> eval H V (Var x) v - | VConst : forall H V n, - eval H V (Const n) (VScalar n) - | VAdd : forall H V x n xn, - V $? x = Some (VScalar xn) - -> eval H V (Add x n) (VScalar (xn ^+ n)) - | VHead : forall H V x p ph pt, - V $? x = Some (VList p) - -> H $? p = Some (ph, pt) - -> eval H V (Head x) ph - | VTail : forall H V x p ph pt, - V $? x = Some (VList p) - -> H $? p = Some (ph, pt) - -> eval H V (Tail x) pt - | VNotNull : forall H V x p, - V $? x = Some (VList p) - -> eval H V (NotNull x) (VScalar (if weq p (^0) then ^1 else ^0)). - - Inductive step : heap * valuation * stmt -> heap * valuation * stmt -> Prop := - | StAssign : forall H V x e v, - eval H V e v - -> step (H, V, Assign x e) (H, V $+ (x, v), Skip) - | StWriteHead : forall H V x e a v hv tv, - V $? x = Some (VList a) - -> eval H V e v - -> H $? a = Some (hv, tv) - -> step (H, V, WriteHead x e) (H $+ (a, (v, tv)), V, Skip) - | StWriteTail : forall H V x e a v hv tv, - V $? x = Some (VList a) - -> eval H V e v - -> H $? a = Some (hv, tv) - -> step (H, V, WriteTail x e) (H $+ (a, (hv, v)), V, Skip) - | StSeq1 : forall H V s2, - step (H, V, Seq Skip s2) (H, V, s2) - | StSeq2 : forall H V s1 s2 H' V' s1', - step (H, V, s1) (H', V', s1') - -> step (H, V, Seq s1 s2) (H', V', Seq s1' s2) - | StIfThen : forall H V e s1 s2 n, - eval H V e (VScalar n) - -> n <> ^0 - -> step (H, V, IfThenElse e s1 s2) (H, V, s1) - | StIfElse : forall H V e s1 s2, - eval H V e (VScalar (^0)) - -> step (H, V, IfThenElse e s1 s2) (H, V, s2) - | StWhileTrue : forall H V e s1 n, - eval H V e (VScalar n) - -> n <> ^0 - -> step (H, V, WhileLoop e s1) (H, V, Seq s1 (WhileLoop e s1)) - | StWhileFalse : forall H V e s1, - eval H V e (VScalar (^0)) - -> step (H, V, WhileLoop e s1) (H, V, Skip). + Ltac simp := repeat (simplify; subst; propositional; + try match goal with + | [ H : ex _ |- _ ] => invert H + end). - (** * Separation logic for our language *) + Inductive loop_outcome {acc} := + | Done (a : acc) + | Again (a : acc). + Arguments loop_outcome : clear implicits. + + 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 : wrd) : cmd wrd + | Write (a v : wrd) : cmd unit + | Loop {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) : cmd acc + | Fail {result} : cmd result. + + (* We're leaving out allocation and deallocation, to avoid distraction from + * the main point of the examples to follow. *) + + 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). + + Inductive step : forall {A}, heap * cmd A -> heap * cmd A -> Prop := + | StepBindRecur : forall result result' (c1 c1' : cmd result') (c2 : result' -> cmd result) h h', + step (h, c1) (h', c1') + -> step (h, Bind c1 c2) (h', Bind c1' c2) + | StepBindProceed : forall (result result' : Set) (v : result') (c2 : result' -> cmd result) h, + step (h, Bind (Return v) c2) (h, c2 v) + + | StepLoop : forall (acc : Set) (init : acc) (body : acc -> cmd (loop_outcome acc)) h, + step (h, Loop init body) (h, o <- body init; match o with + | Done a => Return a + | Again a => Loop a body + end) + + | StepRead : forall h a v, + h $? a = Some v + -> step (h, Read a) (h, Return v) + | StepWrite : forall h a v v', + h $? a = Some v + -> step (h, Write a v') (h $+ (a, v'), Return tt). + + + Definition trsys_of (h : heap) {result} (c : cmd result) := {| + Initial := {(h, c)}; + Step := step (A := result) + |}. + + Definition multistep_trsys_of (h : heap) {result} (c : cmd result) := {| + Initial := {(h, c)}; + Step := (step (A := result))^* + |}. + + (* Now let's get into the first distinctive feature of separation logic: an + * assertion language that takes advantage of *partiality* of heaps. We give our + * definitions inside a module, which will shortly be used as a parameter to + * another module (from the book library), to get some free automation for + * implications between these assertions. *) Module Import S <: SEP. Definition hprop := heap -> Prop. + (* A [hprop] is a regular old assertion over heaps. *) + (* Implication *) Definition himp (p q : hprop) := forall h, p h -> q h. + + (* Equivalence *) Definition heq (p q : hprop) := forall h, p h <-> q h. + (* Lifting a pure proposition: it must hold, and the heap must be empty. *) Definition lift (P : Prop) : hprop := fun h => P /\ h = $0. + (* Separating conjunction, one of the two big ideas of separation logic. + * When does [star p q] apply to [h]? When [h] can be partitioned into two + * subheaps [h1] and [h2], respectively compatible with [p] and [q]. See book + * module [Map] for definitions of [split] and [disjoint]. *) Definition star (p q : hprop) : hprop := fun h => exists h1 h2, split h h1 h2 /\ disjoint h1 h2 /\ p h1 /\ q h2. + (* Existential quantification *) Definition exis {A} (p : A -> hprop) : hprop := fun h => exists x, p x h. + (* Convenient notations *) Notation "[| P |]" := (lift P) : sep_scope. Infix "*" := star : sep_scope. Notation "'exists' x .. y , p" := (exis (fun x => .. (exis (fun y => p)) ..)) : sep_scope. @@ -315,6 +258,9 @@ Module DeeplyEmbedded(Import BW : BIT_WIDTH). Local Open Scope sep_scope. + (* And now we prove some key algebraic properties, whose details aren't so + * important. The library automation uses these properties. *) + Lemma iff_two : forall A (P Q : A -> Prop), (forall x, P x <-> Q x) -> (forall x, P x -> Q x) /\ (forall x, Q x -> P x). @@ -326,7 +272,7 @@ Module DeeplyEmbedded(Import BW : BIT_WIDTH). repeat (match goal with | [ H : forall x, _ <-> _ |- _ ] => apply iff_two in H - | [ H : ex _ |- _ ] => cases H + | [ H : ex _ |- _ ] => destruct H | [ H : split _ _ $0 |- _ ] => apply split_empty_fwd in H end; propositional; subst); eauto 15. @@ -410,13 +356,17 @@ Module DeeplyEmbedded(Import BW : BIT_WIDTH). End S. Export S. + (* Instantiate our big automation engine to these definitions. *) Module Import Se := SepCancel.Make(S). + Export Se. - Definition heap1 (a : wrd) (p : value * value) : heap := $0 $+ (a, p). - Definition ptsto (a : wrd) (p : value * value) : hprop := - fun h => h = heap1 a p. - (* Helpful notations, some the same as above *) + (* ** Predicates *) + + Definition heap1 (a v : wrd) : heap := $0 $+ (a, v). + Definition ptsto (a v : wrd) : hprop := + fun h => h = heap1 a v. + Notation "[| P |]" := (lift P) : sep_scope. Notation emp := (lift True). Infix "*" := star : sep_scope. @@ -426,952 +376,1044 @@ Module DeeplyEmbedded(Import BW : BIT_WIDTH). Notation "p ===> q" := (himp p%sep q%sep) (no associativity, at level 70). Infix "|->" := ptsto (at level 30) : sep_scope. + Fixpoint multi_ptsto (a : wrd) (vs : list wrd) : hprop := + match vs with + | nil => emp + | v :: vs' => a |-> v * multi_ptsto (a ^+ ^1) vs' + end%sep. + + Infix "|-->" := multi_ptsto (at level 30) : sep_scope. + (** * Finally, the Hoare logic *) - Definition hassert := valuation -> hprop. + Inductive hoare_triple : forall {result}, hprop -> cmd result -> (result -> hprop) -> Prop := + | HtReturn : forall P {result : Set} (v : result), + hoare_triple P (Return v) (fun r => P * [| r = v |])%sep + | 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 + | 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 => I (Done r)) + | HtFail : forall {result}, + hoare_triple (fun _ => False) (Fail (result := result)) (fun _ _ => False) - Inductive hoare_triple_exp : hassert -> exp -> (value -> hassert) -> Prop := - | HtVar : forall x, - hoare_triple_exp (fun V => exists v, [| V $? x = Some v |])%sep - (Var x) - (fun r V => [| V $? x = Some r |])%sep - | HtConst : forall n, - hoare_triple_exp (fun _ => emp)%sep - (Const n) - (fun r _ => [| r = VScalar n |])%sep - | HtAdd : forall x n, - hoare_triple_exp (fun V => exists xn, [| V $? x = Some (VScalar xn) |])%sep - (Add x n) - (fun r V => exists xn, [| V $? x = Some (VScalar xn) |] - * [| r = VScalar (xn ^+ n) |])%sep - | HtHead : forall R x, - hoare_triple_exp (fun V => exists a, [| V $? x = Some (VList a) |] - * exists p, a |-> p * R p)%sep - (Head x) - (fun r V => exists a, [| V $? x = Some (VList a) |] - * exists vt, a |-> (r, vt) * R (r, vt))%sep - | HtTail : forall R x, - hoare_triple_exp (fun V => exists a, [| V $? x = Some (VList a) |] - * exists p, a |-> p * R p)%sep - (Tail x) - (fun r V => exists a, [| V $? x = Some (VList a) |] - * exists vh, a |-> (vh, r) * R (vh, r))%sep - | HtNotNull : forall x, - hoare_triple_exp (fun V => exists a, [| V $? x = Some (VList a) |])%sep - (NotNull x) - (fun r V => exists a, [| V $? x = Some (VList a) |] - * [| r = VScalar (if weq a (^0) then ^1 else ^0) |])%sep - | HtExpConsequence : forall P e Q P' Q', - hoare_triple_exp P e Q - -> (forall V, P' V ===> P V) - -> (forall r V, Q r V ===> Q' r V) - -> hoare_triple_exp P' e Q' - | HtExpFrame : forall P e Q R, - hoare_triple_exp P e Q - -> hoare_triple_exp (fun V => P V * R V)%sep e (fun r V => Q r V * R V)%sep. + | HtRead : forall a R, + hoare_triple (exists v, a |-> v * R v)%sep (Read a) (fun r => a |-> r * R r)%sep + | HtWrite : forall a v', + hoare_triple (exists v, a |-> v)%sep (Write a v') (fun _ => a |-> v')%sep - Fixpoint couldChange (s : stmt) (x : var) : bool := - match s with - | Skip => false - | Assign y _ => if y ==v x then true else false - | WriteHead _ _ - | WriteTail _ _ => false - | Seq s1 s2 => couldChange s1 x || couldChange s2 x - | IfThenElse _ s1 s2 => couldChange s1 x || couldChange s2 x - | WhileLoop _ s1 => couldChange s1 x - end. + | HtConsequence : forall {result} (c : cmd result) P Q (P' : hprop) (Q' : _ -> hprop), + hoare_triple P c Q + -> P' ===> P + -> (forall r, Q r ===> Q' r) + -> hoare_triple P' c Q' - Inductive hoare_triple : hassert -> stmt -> hassert -> Prop := - | HtSkip : forall P, - hoare_triple P Skip P - | HtAssign : forall P x e Q, - hoare_triple_exp P e Q - -> hoare_triple P (Assign x e) (fun V => exists V' r, Q r V' * [| V = V' $+ (x, r) |])%sep - | HtWriteHead : forall P x e R, - hoare_triple_exp P e (fun r V => exists a, [| V $? x = Some (VList a) |] * exists vhd vtl, a |-> (vhd, vtl) * R r vhd vtl V)%sep - -> hoare_triple P - (WriteHead x e) - (fun V => exists a, [| V $? x = Some (VList a) |] * exists r vhd vtl, a |-> (r, vtl) * R r vhd vtl V)%sep - | HtWriteTail : forall P x e R, - hoare_triple_exp P e (fun r V => exists a, [| V $? x = Some (VList a) |] * exists vhd vtl, a |-> (vhd, vtl) * R r vhd vtl V)%sep - -> hoare_triple P - (WriteTail x e) - (fun V => exists a, [| V $? x = Some (VList a) |] * exists r vhd vtl, a |-> (vhd, r) * R r vhd vtl V)%sep - | HtSeq : forall P s1 Q s2 R, - hoare_triple P s1 Q - -> hoare_triple Q s2 R - -> hoare_triple P (Seq s1 s2) R - | HtIfThenElse : forall P e s1 s2 Q R, - hoare_triple_exp P e (fun r V => Q r V * exists n, [| r = VScalar n |])%sep - -> hoare_triple (fun V => exists n, Q (VScalar n) V * [| n <> ^0 |])%sep s1 R - -> hoare_triple (fun V => Q (VScalar (^0)) V)%sep s2 R - -> hoare_triple P (IfThenElse e s1 s2) R - | HtWhileLoop : forall I e s1 Q, - hoare_triple_exp I e (fun r V => Q r V * exists n, [| r = VScalar n |])%sep - -> hoare_triple (fun V => exists n, Q (VScalar n) V * [| n <> ^0 |])%sep s1 I - -> hoare_triple I (WhileLoop e s1) (Q (VScalar (^0))) - | HtConsequence : forall P s Q P' Q', - hoare_triple P s Q - -> (forall V, P' V ===> P V) - -> (forall V, Q V ===> Q' V) - -> hoare_triple P' s Q' - | HtFrame : forall P s Q R, - hoare_triple P s Q - -> (forall V1 V2, (forall x, couldChange s x = false - -> V1 $? x = V2 $? x) - -> R V1 = R V2) - -> hoare_triple (fun V => P V * R V)%sep s (fun V => Q V * R V)%sep. + | HtFrame : forall {result} (c : cmd result) P Q R, + hoare_triple P c Q + -> hoare_triple (P * R)%sep c (fun r => Q r * R)%sep. - Notation "{{ V1 ~> P }} c {{ V2 ~> Q }}" := - (hoare_triple (fun V1 => P%sep) c (fun V2 => Q%sep)) (at level 90, c at next level). - Lemma HtStrengthen : forall P s Q Q', - hoare_triple P s Q - -> (forall V, Q V ===> Q' V) - -> hoare_triple P s Q'. + Notation "{{ P }} c {{ r ~> Q }}" := + (hoare_triple P%sep c (fun r => Q%sep)) (at level 90, c at next level). + + Lemma HtStrengthen : forall {result} (c : cmd result) P Q (Q' : _ -> hprop), + hoare_triple P c Q + -> (forall r, Q r ===> Q' r) + -> hoare_triple P c Q'. Proof. simplify. eapply HtConsequence; eauto. reflexivity. Qed. - Lemma HtWeaken : forall P s Q P', - hoare_triple P s Q - -> (forall V, P' V ===> P V) - -> hoare_triple P' s Q. + Lemma HtWeaken : forall {result} (c : cmd result) P Q (P' : hprop), + hoare_triple P c Q + -> P' ===> P + -> hoare_triple P' c Q. Proof. simplify. eapply HtConsequence; eauto. reflexivity. Qed. - Definition trsys_of (H : heap) (V : valuation) (s : stmt) := {| - Initial := constant [(H, V, s)]; - Step := step - |}. + (* Now, we carry out a moderately laborious soundness proof! It's safe to skip + * ahead to the text "Examples", but a few representative lemma highlights + * include [invert_Read], [preservation], [progress], and the main theorem + * [hoare_triple_sound]. *) - Hint Constructors hoare_triple_exp hoare_triple eval step. - - Lemma eval_subheap : forall H V e r, - eval H V e r - -> forall H', (forall a v, H $? a = Some v -> H' $? a = Some v) - -> eval H' V e r. - Proof. - invert 1; simplify; eauto. - Qed. - - Lemma drop_cells : forall P e Q, - hoare_triple_exp P e Q - -> forall V H r, eval H V e r - -> forall H', P V H' - -> (forall a v, H' $? a = Some v -> H $? a = Some v) - -> eval H' V e r. - Proof. - induct 1; simplify. - - invert H0; auto. - - invert H0; auto. - - invert H0; auto. - - invert H0. - invert H1. - invert H0; simp. - invert H3. - apply split_empty_fwd' in H1; subst. - invert H6. - invert H1; simp. - econstructor. - eassumption. - cases (x2 $? x0). - apply H2 in Heq. - replace p0 with (r, pt) by equality. - eauto. - unfold split in H3; subst. - unfold ptsto in H6; subst. - unfold heap1 in Heq. - rewrite lookup_join1 in Heq by (simplify; sets). - simplify; equality. - - invert H0. - invert H1. - invert H0; simp. - invert H3. - apply split_empty_fwd' in H1; subst. - invert H6. - invert H1; simp. - econstructor. - eassumption. - cases (x2 $? x0). - apply H2 in Heq. - replace p0 with (ph, r) by equality. - eauto. - unfold split in H3; subst. - unfold ptsto in H6; subst. - unfold heap1 in Heq. - rewrite lookup_join1 in Heq by (simplify; sets). - simplify; equality. - - invert H0; auto. - - eapply IHhoare_triple_exp; eauto. - apply H0; auto. - - invert H2; simp. - eapply IHhoare_triple_exp in H1. - 2: eauto. - eapply eval_subheap; eauto. - simplify. - unfold split in H4; subst. - rewrite lookup_join1 by eauto using lookup_Some_dom. - auto. - simplify. - unfold split in H4; subst. - apply H3. - rewrite lookup_join1 by eauto using lookup_Some_dom. - auto. - Qed. - - Lemma preservation_exp : forall P e Q, - hoare_triple_exp P e Q - -> forall V H r, P V H -> eval H V e r -> Q r V H. - Proof. - induct 1; simplify. - - invert H1. - cases H0. - cases H0. - constructor; assumption. - - invert H1. - invert H0. - constructor; reflexivity. - - invert H1. - invert H0. - invert H1. - eexists. - exists $0, $0; propositional; eauto. - constructor; eauto. - constructor; equality. - - invert H1. - invert H0. - invert H1. - simp. - invert H2. - invert H5. - cases x1. - replace r with v. - exists x0. - exists $0, H; propositional; eauto. - constructor; auto. - exists v0. - apply split_empty_fwd' in H0; equality. - invert H2; simp. - unfold split in H5; subst. - unfold ptsto in H6; subst. - apply split_empty_fwd' in H0; subst. - replace x0 with p in * by equality. - unfold heap1 in H7. - simplify. - rewrite lookup_join1 in H7. - simplify; equality. - simplify; sets. - - invert H1. - invert H0. - invert H1. - simp. - invert H2. - invert H5. - cases x1. - replace r with v0. - exists x0. - exists $0, H; propositional; eauto. - constructor; auto. - exists v. - apply split_empty_fwd' in H0; equality. - invert H2; simp. - unfold split in H5; subst. - unfold ptsto in H6; subst. - apply split_empty_fwd' in H0; subst. - replace x0 with p in * by equality. - unfold heap1 in H7. - simplify. - rewrite lookup_join1 in H7. - simplify; equality. - simplify; sets. - - invert H1. - invert H0. - invert H1. - exists p, $0, $0; propositional; eauto. - constructor; auto. - constructor; auto. - - unfold himp in *; eauto. - - invert H1; simp. - exists x, x0; propositional; eauto. - eapply IHhoare_triple_exp; eauto. - eapply drop_cells; eauto. - simplify. - unfold split in H3; subst. - rewrite lookup_join1 by eauto using lookup_Some_dom. - auto. - Qed. - - Opaque heq himp lift star exis ptsto. - - Lemma invert_Assign : forall P x e Q, - hoare_triple P (Assign x e) Q - -> exists Q', hoare_triple_exp P e Q' - /\ forall V r, Q' r V ===> Q (V $+ (x, r)). + 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. - do 2 eexists. - eassumption. - simplify. - do 2 eapply exis_right. - cancel. + exists h, $0; propositional; eauto. + unfold lift; propositional. - first_order. - do 2 eexists. - eapply HtExpConsequence. - eassumption. - assumption. - reflexivity. - etransitivity; eauto. + unfold himp in *; eauto. - first_order. - do 2 eexists. - eapply HtExpFrame. - eassumption. - simplify. - rewrite H0 with (V1 := V) (V2 := V $+ (x, r)). - rewrite H2. - reflexivity. - simplify. - cases (x ==v x1); simplify; equality. + unfold star, himp in *; simp; eauto 7. Qed. - Lemma invert_WriteHead : forall P x e Q, - hoare_triple P (WriteHead x e) Q - -> exists R, hoare_triple_exp P e (fun r V => exists a, [| V $? x = Some (VList a) |] * exists vhd vtl, a |-> (vhd, vtl) * R r vhd vtl V)%sep - /\ (forall V, (exists a, [| V $? x = Some (VList a) |] * exists r vhd vtl, a |-> (r, vtl) * R r vhd vtl V) ===> Q V). + Hint Constructors hoare_triple. + + 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; first_order; eauto. - - do 2 eexists. - eassumption. - reflexivity. - - do 2 eexists. - eapply HtExpConsequence. - eassumption. - assumption. - simplify. - reflexivity. - etransitivity; eauto. - - exists (fun r vhd vtl V => x0 r vhd vtl V * R V)%sep. - propositional. - eapply HtExpConsequence with (Q := fun r V => - ((exists a, [|V $? x = Some (VList a)|] - * exists vhd vtl, a |-> (vhd, vtl) * x0 r vhd vtl V) * R V)%sep). - eapply HtExpFrame. - eassumption. - reflexivity. - cancel. - rewrite <- H2. - cancel. - Qed. - - Lemma invert_WriteTail : forall P x e Q, - hoare_triple P (WriteTail x e) Q - -> exists R, hoare_triple_exp P e (fun r V => exists a, [| V $? x = Some (VList a) |] * exists vhd vtl, a |-> (vhd, vtl) * R r vhd vtl V)%sep - /\ (forall V, (exists a, [| V $? x = Some (VList a) |] * exists r vhd vtl, a |-> (vhd, r) * R r vhd vtl V) ===> Q V). - Proof. - induct 1; first_order; eauto. - - do 2 eexists. - eassumption. - reflexivity. - - do 2 eexists. - eapply HtExpConsequence. - eassumption. - assumption. - simplify. - reflexivity. - etransitivity; eauto. - - exists (fun r vhd vtl V => x0 r vhd vtl V * R V)%sep. - propositional. - eapply HtExpConsequence with (Q := fun r V => - ((exists a, [|V $? x = Some (VList a)|] - * exists vhd vtl, a |-> (vhd, vtl) * x0 r vhd vtl V) * R V)%sep). - eapply HtExpFrame. - eassumption. - reflexivity. - cancel. - rewrite <- H2. - cancel. - Qed. - - Lemma invert_Skip : forall P Q, - hoare_triple P Skip Q - -> forall V, P V ===> Q V. - Proof. - induct 1; simplify. - - reflexivity. - - do 2 (etransitivity; eauto). - - rewrite IHhoare_triple. - reflexivity. - Qed. - - Lemma invert_Seq : forall P s1 s2 Q, - hoare_triple P (Seq s1 s2) Q - -> exists R, hoare_triple P s1 R - /\ hoare_triple R s2 Q. - Proof. - induct 1; simplify; first_order. - - do 2 eexists. - eapply HtConsequence; eauto; reflexivity. - eapply HtConsequence; eauto; reflexivity. - - do 2 eexists. - eapply HtFrame; eauto. - simplify. - apply H0. - simplify. - apply orb_false_elim in H4; propositional; eauto. - eapply HtFrame; eauto. - simplify. - apply H0. - simplify. - apply orb_false_elim in H4; propositional; eauto. - Qed. - - Lemma invert_IfThenElse : forall P e s1 s2 Q, - hoare_triple P (IfThenElse e s1 s2) Q - -> exists R, hoare_triple_exp P e (fun r V => R r V * exists n, [| r = VScalar n |])%sep - /\ hoare_triple (fun V => exists n, R (VScalar n) V * [| n <> ^0 |])%sep s1 Q - /\ hoare_triple (fun V => R (VScalar (^0)) V)%sep s2 Q. - Proof. - induct 1; simplify; first_order. + induct 1; propositional; eauto. + invert IHhoare_triple; propositional. eexists; propositional. - eapply HtExpConsequence. - eassumption. - assumption. - simplify. - reflexivity. - eapply HtStrengthen. - eassumption. - assumption. - eapply HtStrengthen. - eassumption. - assumption. - - exists (fun r V => x r V * R V)%sep; propositional. - eapply HtExpConsequence. - eapply HtExpFrame. - eauto. - simplify. - reflexivity. - simplify. - cancel. - eauto. eapply HtWeaken. - eapply HtFrame. eassumption. - simplify. - apply H0. - simplify. - apply orb_false_elim in H5; propositional; eauto. - simplify. - cancel. - eapply HtFrame. - assumption. - simplify. - apply H0. - simplify. - apply orb_false_elim in H5; propositional; eauto. + auto. + eapply HtStrengthen. + apply H4. + auto. + + simp. + exists (fun r => x r * R)%sep. + propositional. + eapply HtFrame; eauto. + eapply HtFrame; eauto. Qed. - Lemma invert_WhileLoop : forall P e s1 Q, - hoare_triple P (WhileLoop e s1) Q - -> exists I R, (forall V, P V ===> I V) - /\ hoare_triple_exp I e (fun r V => R r V * exists n, [| r = VScalar n |])%sep - /\ hoare_triple (fun V => exists n, R (VScalar n) V * [| n <> ^0 |])%sep s1 I - /\ (forall V, R (VScalar (^0)) V ===> Q V). + 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; simplify; first_order. + induct 1; propositional; eauto. - do 2 eexists; propositional; eauto; reflexivity. + invert IHhoare_triple; propositional. + exists x; propositional; eauto. + unfold himp in *; eauto. - exists x, x0; propositional. - etransitivity; eauto. - etransitivity; eauto. - - exists (fun V => x V * R V)%sep, (fun r V => x0 r V * R V)%sep; propositional. - rewrite H1; reflexivity. - eapply HtExpConsequence. - eapply HtExpFrame. - eauto. - simplify. - reflexivity. - simplify. - cancel. - eauto. - eapply HtWeaken. - eauto. - simplify. - cancel. - rewrite H4. - reflexivity. + simp. + exists (fun o => x o * R)%sep; propositional; eauto. + unfold star in *; simp; eauto 7. + unfold star in *; simp; eauto 7. 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. + + unfold star in *; simp; eauto. + Qed. + + (* Now that we proved enough basic facts, let's hide the definitions of all + * these predicates, so that we reason about them only through automation. *) + Opaque heq himp lift star exis ptsto. + + Lemma unit_not_wrd : unit = wrd -> 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 (x ^+ ^1)). + eapply adding_one_changes. + apply bit_width_nonzero. + symmetry; eassumption. + Qed. + + Lemma invert_Read : forall a P Q, + hoare_triple P (Read a) Q + -> exists R, (P ===> exists v, a |-> v * R v)%sep + /\ forall r, a |-> r * R r ===> Q r. + Proof. + induct 1; simp; eauto. + + exists R; simp. + cancel; auto. + cancel; auto. + + apply unit_not_wrd in x0; simp. + + specialize (IHhoare_triple _ _ eq_refl JMeq.JMeq_refl JMeq.JMeq_refl); first_order. + exists x. + propositional. + etransitivity; eauto. + etransitivity; eauto. + + specialize (IHhoare_triple _ _ eq_refl JMeq.JMeq_refl JMeq.JMeq_refl); first_order. + exists (fun n => x n * R)%sep; simp. + rewrite H0. + cancel. + + rewrite <- H1. + cancel. + Qed. + + Lemma invert_Write : forall a v' P Q, + hoare_triple P (Write a v') Q + -> exists R, (P ===> (exists v, a |-> v) * R)%sep + /\ a |-> v' * R ===> Q tt. + Proof. + induct 1; simp; eauto. + + symmetry in x0. + apply unit_not_wrd in x0; simp. + + exists emp; simp. + cancel; auto. + cancel; auto. + + eexists; split. + etransitivity; eauto. + etransitivity; eauto. + + exists (x * R)%sep; simp. + rewrite H1. + cancel. + + cancel. + rewrite <- H2. + cancel. + Qed. + + Lemma HtReturn' : forall P {result : Set} (v : result) Q, + P ===> Q v + -> hoare_triple P (Return v) Q. + Proof. + simp. + eapply HtStrengthen. + constructor. + simp. + cancel. + Qed. + + (* Temporarily transparent again! *) Transparent heq himp lift star exis ptsto. - Lemma preservation : forall s H V s' V' H', - step (H, V, s) (H', V', s') - -> forall Q, hoare_triple (fun V' H' => H' = H /\ V' = V) s Q - -> hoare_triple (fun V'' H'' => H'' = H' /\ V'' = V') s' Q. + Lemma preservation : forall {result} (c : cmd result) h c' h', + step (h, c) (h', c') + -> forall Q, hoare_triple (fun h' => h' = h) c Q + -> hoare_triple (fun h'' => h'' = h') c' Q. Proof. induct 1; simplify. - apply invert_Assign in H; simp. - eapply preservation_exp in H0; eauto. - eapply HtWeaken. - auto. - unfold himp; simplify. - propositional; subst. - apply H2; assumption. - simplify; auto. - - apply invert_WriteHead in H3; simp. - eapply preservation_exp in H1; eauto. - simplify. - eapply HtWeaken. - auto. - unfold himp; simplify. - propositional; subst. - apply H5. - invert H1. - invert H4; simp. - invert H6. - invert H8. - invert H6. - invert H8; simp. - invert H9. - exists x1. - apply split_empty_fwd' in H1; subst. - exists $0, (x3 $+ (a, (v, tv))); propositional; eauto. - constructor; auto. - exists v, x2, tv. - exists (heap1 x1 (v, tv)), x6; propositional; eauto. - unfold split, heap1. - unfold split, heap1 in H6. - subst. - apply fmap_ext; simplify. - cases (weq k x1); subst. - replace x1 with a by equality. - repeat (rewrite lookup_join1 by (simplify; sets); simplify). - auto. - simplify. - repeat (rewrite lookup_join2 by (simplify; sets); simplify). - auto. - unfold disjoint, heap1 in *. - intros. - apply H8 with a0. - cases (weq x1 a0); subst; simplify. - equality. - assumption. - assumption. - constructor. - unfold split in H6; subst. - replace x1 with a in * by equality. - unfold heap1 in H2. - rewrite lookup_join1 in H2 by (simplify; sets). - simplify. - equality. - simplify; auto. - - apply invert_WriteTail in H3; simp. - eapply preservation_exp in H1; eauto. - simplify. - eapply HtWeaken. - auto. - unfold himp; simplify. - propositional; subst. - apply H5. - invert H1. - invert H4; simp. - invert H6. - invert H8. - invert H6. - invert H8; simp. - invert H9. - exists x1. - apply split_empty_fwd' in H1; subst. - exists $0, (x3 $+ (a, (hv, v))); propositional; eauto. - constructor; auto. - exists v, hv, x4. - exists (heap1 x1 (hv, v)), x6; propositional; eauto. - unfold split, heap1. - unfold split, heap1 in H6. - subst. - apply fmap_ext; simplify. - cases (weq k x1); subst. - replace x1 with a by equality. - repeat (rewrite lookup_join1 by (simplify; sets); simplify). - auto. - simplify. - repeat (rewrite lookup_join2 by (simplify; sets); simplify). - auto. - unfold disjoint, heap1 in *. - intros. - apply H8 with a0. - cases (weq x1 a0); subst; simplify. - equality. - assumption. - assumption. - constructor. - unfold split in H6; subst. - replace x1 with a in * by equality. - unfold heap1 in H2. - rewrite lookup_join1 in H2 by (simplify; sets). - simplify. - equality. - simplify; auto. - - apply invert_Seq in H; first_order. - eapply HtWeaken. - eauto. - simplify. - eapply invert_Skip in H; eassumption. - - apply invert_Seq in H1; first_order. + apply invert_Bind in H0; simp. eauto. - apply invert_IfThenElse in H; first_order. - eapply HtWeaken; eauto. - simplify. - unfold himp; propositional; subst. - eapply preservation_exp in H0; eauto. - exists n, H', $0; propositional; eauto. - invert H0; simp. - invert H7. - invert H6. - apply split_empty_fwd in H4; subst. - auto. - constructor; auto. - simplify; auto. + apply invert_Bind in H; simp. + specialize (invert_Return _ _ _ H); eauto using HtWeaken. - apply invert_IfThenElse in H; first_order. - eapply HtWeaken; eauto. - simplify. - unfold himp; propositional; subst. - eapply preservation_exp in H0; eauto. - eapply HtExpConsequence. + apply invert_Loop in H; simp. + econstructor. + eapply HtWeaken. eauto. - simplify. - instantiate (1 := fun V H'0 => H'0 = H' /\ V = V'). - simplify. - reflexivity. - simplify. - unfold himp; simplify. - invert H3; simp. - invert H7. - invert H6. - apply split_empty_fwd in H4; subst. - auto. - simplify; auto. - - apply invert_WhileLoop in H; first_order. - eapply HtSeq. - eapply HtWeaken; eauto. - simplify. - unfold himp; propositional; subst. - eapply preservation_exp in H0; eauto. - exists n, H', $0; propositional; eauto. - invert H0; simp. - invert H8. - invert H7. - apply split_empty_fwd in H5; subst. - auto. - constructor; auto. - apply H; simplify; auto. + assumption. + simp. + cases r. + apply HtReturn'. + unfold himp; simp; eauto. eapply HtStrengthen. eauto. - eauto. + unfold himp; simp; eauto. - apply invert_WhileLoop in H; first_order. - eapply HtWeaken; eauto. - simplify. - unfold himp; propositional; subst. - eapply preservation_exp in H0; eauto. - apply H3; auto. - simplify. - invert H0; simp. - invert H7. - invert H6. - apply split_empty_fwd in H4; subst. - auto. - apply H; simplify; auto. + apply invert_Read in H0; simp. + apply HtReturn'. + assert ((exists v, a |-> v * x v)%sep h') by auto. + unfold exis, star in H1; simp. + unfold ptsto in H4; subst. + unfold split in H1; subst. + unfold heap1 in H. + rewrite lookup_join1 in H by (simp; sets). + unfold himp; simp. + invert H. + apply H2. + unfold star. + exists (heap1 a v), x2; propositional. + unfold split; reflexivity. + unfold ptsto; reflexivity. + + apply invert_Write in H0; simp. + apply HtReturn'. + simp. + assert (((exists v : wrd, a |-> v) * x)%sep h) by auto. + unfold star in H1; simp. + invert H4. + unfold ptsto in H5; subst. + unfold split in H3; subst. + unfold heap1 in H. + rewrite lookup_join1 in H by (simp; sets). + unfold himp; simp. + invert H. + apply H2. + unfold star. + exists ($0 $+ (a, v')), x1; propositional. + unfold split. + unfold heap1. + maps_equal. + rewrite lookup_join1 by (simp; sets). + simp. + repeat rewrite lookup_join2 by (simp; sets); reflexivity. + unfold disjoint in *; simp. + cases (weq a0 a); simp. + apply H1 with (a0 := a). + unfold heap1; simp. + equality. + assumption. + unfold ptsto; reflexivity. Qed. - Lemma hoare_triple_sound' : forall P s Q, - hoare_triple P s Q - -> forall H V, P V H - -> invariantFor (trsys_of H V s) - (fun p => hoare_triple (fun V' H' => H' = fst (fst p) /\ V' = snd (fst p)) - (snd p) - Q). + Hint Constructors step. + + Lemma progress : forall {result} (c : cmd result) P Q, + hoare_triple P c Q + -> forall h h1 h2, split h h1 h2 + -> disjoint h1 h2 + -> P h1 + -> (exists r, c = Return r) + \/ (exists h' c', step (h, c) (h', c')). + Proof. + induct 1; simp; + repeat match goal with + | [ H : forall _ h1 _, _ -> _ -> ?P h1 -> _, H' : ?P _ |- _ ] => eapply H in H'; clear H; try eassumption; simp + end; eauto. + + invert H1. + right; exists h, (Return x). + constructor. + unfold split, ptsto, heap1 in *; simp. + unfold star in H2; simp. + unfold split in H; simp. + rewrite lookup_join1; simp. + rewrite lookup_join1; simp. + sets. + eapply lookup_Some_dom. + rewrite lookup_join1; simp. + sets. + + right; exists (h $+ (a, v')), (Return tt). + unfold split, exis, ptsto, heap1 in *; simp. + econstructor. + rewrite lookup_join1; simp. + sets. + + unfold star in H2; simp. + apply IHhoare_triple with (h := h) (h1 := x) (h2 := h2 $++ x0); eauto. + unfold split in *; simp. + rewrite (@join_comm _ _ h2 x0). + apply join_assoc. + sets. + cases (h2 $? x1). + cases (x0 $? x1). + specialize (H2 x1). + specialize (H1 x1). + rewrite lookup_join2 in H1. + apply H1; equality. + unfold not. + simplify. + cases (x $? x1). + exfalso; apply H2; equality. + apply lookup_None_dom in Heq1; propositional. + apply lookup_None_dom in Heq0; propositional. + apply lookup_None_dom in Heq; propositional. + + unfold split, disjoint in *; simp. + cases (h2 $? a). + rewrite lookup_join1 in H7. + apply H1 with (a := a); auto. + rewrite lookup_join1; auto. + cases (x $? a); try equality. + eauto using lookup_Some_dom. + eauto using lookup_Some_dom. + rewrite lookup_join2 in H7. + eapply H2; eassumption. + eauto using lookup_None_dom. + Qed. + + Lemma hoare_triple_sound' : forall P {result} (c : cmd result) Q, + hoare_triple P c Q + -> P $0 + -> invariantFor (trsys_of $0 c) + (fun p => + hoare_triple (fun h' => h' = fst p) + (snd p) + Q). Proof. simplify. apply invariant_induction; simplify. propositional; subst; simplify. - eapply HtWeaken. - eauto. + eapply HtWeaken; eauto. unfold himp; simplify; equality. - cases s0. - cases p. + cases s. cases s'. - cases p. - simplify. - eapply preservation; eauto. - Qed. - - Lemma progress_exp : forall P e Q, - hoare_triple_exp P e Q - -> forall V H H1 H2, split H H1 H2 - -> disjoint H1 H2 - -> P V H1 - -> exists v, eval H V e v. - Proof. - induct 1; simplify; eauto. - - invert H4. - invert H5. - eauto. - - invert H4. - invert H5. - eexists. - econstructor. - eauto. - - invert H4. - invert H5; simp. - invert H6. - apply split_empty_fwd' in H4; subst. - invert H8. - invert H1; simp. - invert H6. - cases x1. - eexists. - econstructor. - eauto. - unfold heap1, split in *; subst. - rewrite lookup_join1. - rewrite lookup_join1. - simplify. - eauto. - eapply lookup_Some_dom; simplify; sets. - eapply lookup_Some_dom; simplify. - rewrite lookup_join1. - simplify; eauto. - eapply lookup_Some_dom; simplify; sets. - - invert H4. - invert H5; simp. - invert H6. - apply split_empty_fwd' in H4; subst. - invert H8. - invert H1; simp. - invert H6. - cases x1. - eexists. - econstructor. - eauto. - unfold heap1, split in *; subst. - rewrite lookup_join1. - rewrite lookup_join1. - simplify. - eauto. - eapply lookup_Some_dom; simplify; sets. - eapply lookup_Some_dom; simplify. - rewrite lookup_join1. - simplify; eauto. - eapply lookup_Some_dom; simplify; sets. - - invert H4. - invert H5. - eauto. - - eapply IHhoare_triple_exp; eauto. - apply H0; auto. - - invert H5; simp. - eapply IHhoare_triple_exp in H7; eauto. - Qed. - - Lemma progress : forall P s Q, - hoare_triple P s Q - -> forall V H H1 H2, split H H1 H2 - -> disjoint H1 H2 - -> P V H1 - -> s = Skip \/ (exists H' V' s', step (H, V, s) (H', V', s')). - Proof. - induct 1; simplify; eauto. - - eapply (progress_exp _ _ _ H) in H5; eauto. simp. - right; do 3 eexists. - econstructor. - eauto. - - pose proof (progress_exp _ _ _ H _ _ _ _ H3 H4 H5) as Hprog. - invert Hprog. - assert (Hdropped : eval H1 V e x0). - eapply drop_cells; eauto. - unfold split in H3; subst. - simplify. - rewrite lookup_join1; auto. - eapply lookup_Some_dom; eauto. - pose proof (preservation_exp _ _ _ H _ _ _ H5 Hdropped) as Hpres. - simplify. - invert Hpres. - invert H7; simp. - invert H9. - apply split_empty_fwd' in H8; subst. - invert H11. - invert H1. - invert H8; simp. - invert H9. - right; do 3 eexists. - econstructor. - eauto. - eauto. - unfold heap1, split in *; subst. - rewrite lookup_join1. - rewrite lookup_join1. - simplify. - eauto. - eapply lookup_Some_dom; simplify; sets. - eapply lookup_Some_dom; simplify. - rewrite lookup_join1. - simplify; eauto. - eapply lookup_Some_dom; simplify; sets. - - pose proof (progress_exp _ _ _ H _ _ _ _ H3 H4 H5) as Hprog. - invert Hprog. - assert (Hdropped : eval H1 V e x0). - eapply drop_cells; eauto. - unfold split in H3; subst. - simplify. - rewrite lookup_join1; auto. - eapply lookup_Some_dom; eauto. - pose proof (preservation_exp _ _ _ H _ _ _ H5 Hdropped) as Hpres. - simplify. - invert Hpres. - invert H7; simp. - invert H9. - apply split_empty_fwd' in H8; subst. - invert H11. - invert H1. - invert H8; simp. - invert H9. - right; do 3 eexists. - econstructor. - eauto. - eauto. - unfold heap1, split in *; subst. - rewrite lookup_join1. - rewrite lookup_join1. - simplify. - eauto. - eapply lookup_Some_dom; simplify; sets. - eapply lookup_Some_dom; simplify. - rewrite lookup_join1. - simplify; eauto. - eapply lookup_Some_dom; simplify; sets. - - specialize (IHhoare_triple1 _ _ _ _ H4 H5 H6); simp; eauto 6. - - pose proof (progress_exp _ _ _ H _ _ _ _ H5 H6 H7) as Hprog. - invert Hprog. - assert (Hdropped : eval H3 V e x). - eapply drop_cells; eauto. - unfold split in H5; subst. - simplify. - rewrite lookup_join1; auto. - eapply lookup_Some_dom; eauto. - pose proof (preservation_exp _ _ _ H _ _ _ H7 Hdropped) as Hpres. - simplify. - invert Hpres; simp. - invert H13. - invert H12. - cases (weq x2 (^0)); subst; eauto 10. - - pose proof (progress_exp _ _ _ H _ _ _ _ H4 H5 H6) as Hprog. - invert Hprog. - assert (Hdropped : eval H2 V e x). - eapply drop_cells; eauto. - unfold split in H4; subst. - simplify. - rewrite lookup_join1; auto. - eapply lookup_Some_dom; eauto. - pose proof (preservation_exp _ _ _ H _ _ _ H6 Hdropped) as Hpres. - simplify. - invert Hpres; simp. - invert H12. - invert H11. - cases (weq x2 (^0)); subst; eauto 10. - - apply H0 in H7. - eapply IHhoare_triple in H7; eauto. - - invert H6; simp. - eapply IHhoare_triple in H8; eauto. + eauto using preservation. Qed. - Theorem hoare_triple_sound : forall P s Q, - hoare_triple P s Q - -> forall H V, P V H - -> invariantFor (trsys_of H V s) - (fun p => (snd p = Skip /\ Q (snd (fst p)) (fst (fst p))) - \/ exists p', step p p'). + Theorem hoare_triple_sound : forall P {result} (c : cmd result) Q, + hoare_triple P c Q + -> P $0 + -> invariantFor (trsys_of $0 c) + (fun p => (exists r, snd p = Return r) + \/ (exists p', step p p')). + Proof. + simplify. + + eapply invariant_weaken. + eapply hoare_triple_sound'; eauto. + simp. + specialize (progress _ _ _ H1); simplify. + specialize (H2 (fst s) (fst s) $0). + assert (split (fst s) (fst s) $0) by auto. + assert (disjoint (fst s) $0) by auto. + cases s; simp; eauto. + Qed. + + (* Fancy theorem to help us rewrite within preconditions and postconditions *) + Instance hoare_triple_morphism : forall A, + Proper (heq ==> eq ==> (eq ==> heq) ==> iff) (@hoare_triple A). + Proof. + Transparent himp. + repeat (hnf; intros). + unfold pointwise_relation in *; intuition subst. + + eapply HtConsequence; eauto. + rewrite H; reflexivity. + intros. + hnf in H1. + specialize (H1 r _ eq_refl). + rewrite H1; reflexivity. + + eapply HtConsequence; eauto. + rewrite H; reflexivity. + intros. + hnf in H1. + specialize (H1 r _ eq_refl). + rewrite H1; reflexivity. + Opaque himp. + Qed. + + + (** * Examples *) + + Global Opaque heq himp lift star exis ptsto. + + Theorem use_lemma : forall result P' (c : cmd result) (Q : result -> hprop) P R, + hoare_triple P' c Q + -> P ===> P' * R + -> hoare_triple P c (fun r => Q r * R)%sep. + Proof. + simp. + eapply HtWeaken. + eapply HtFrame. + eassumption. + eauto. + Qed. + + Theorem HtRead' : forall a v, + hoare_triple (a |-> v)%sep (Read a) (fun r => a |-> v * [| r = v |])%sep. + Proof. + simp. + apply HtWeaken with (exists r, a |-> r * [| r = v |])%sep. + eapply HtStrengthen. + apply HtRead. + simp. + cancel; auto. + subst; cancel. + cancel; auto. + Qed. + + Theorem HtRead'' : forall p P R, + P ===> (exists v, p |-> v * R v) + -> hoare_triple P (Read p) (fun r => p |-> r * R r)%sep. + Proof. + simp. + eapply HtWeaken. + apply HtRead. + assumption. + Qed. + + Ltac basic := apply HtReturn' || eapply HtWrite. + + Ltac step0 := basic || eapply HtBind || (eapply use_lemma; [ basic | cancel; auto ]) + || (eapply use_lemma; [ eapply HtRead' | solve [ cancel; auto ] ]) + || (eapply HtRead''; solve [ cancel ]) + || (eapply HtStrengthen; [ eapply use_lemma; [ basic | cancel; auto ] | ]) + || (eapply HtConsequence; [ apply HtFail | .. ]). + Ltac step := step0; simp. + Ltac ht := simp; repeat step. + Ltac conseq := simplify; eapply HtConsequence. + Ltac use_IH H := conseq; [ apply H | .. ]; ht. + Ltac loop_inv0 Inv := (eapply HtWeaken; [ apply HtLoop with (I := Inv) | .. ]) + || (eapply HtConsequence; [ apply HtLoop with (I := Inv) | .. ]). + Ltac loop_inv Inv := loop_inv0 Inv; ht. + Ltac use H := (eapply use_lemma; [ eapply H | cancel; auto ]) + || (eapply HtStrengthen; [ eapply use_lemma; [ eapply H | cancel; auto ] | ]). + + Ltac heq := intros; apply himp_heq; split. + + + (** * List-reverse example *) + + Fixpoint linkedList (p : wrd) (ls : list wrd) := + match ls with + | nil => [| p = ^0 |] + | x :: ls' => [| p <> ^0 |] + * exists p', p |--> [x; p'] * linkedList p' ls' + end%sep. + + Theorem linkedList_null : forall ls, + linkedList (^0) ls === [| ls = nil |]. + Proof. + heq; cases ls; cancel. + Qed. + + Theorem linkedList_nonnull : forall p ls, + p <> ^0 + -> linkedList p ls === exists x ls' p', [| ls = x :: ls' |] * p |--> [x; p'] * linkedList p' ls'. + Proof. + heq; cases ls; cancel; match goal with + | [ H : _ = _ :: _ |- _ ] => invert H + end; cancel. + Qed. + + Hint Rewrite <- rev_alt. + Hint Rewrite rev_involutive. + + Opaque linkedList. + + Definition reverse p := + pr <- for pr := (p, ^0) loop + let (p, r) := pr in + if weq p (^0) then + Return (Done pr) + else + tmp <- Read (p ^+ ^1); + _ <- Write (p ^+ ^1) r; + Return (Again (tmp, p)) + done; + Return (snd pr). + + Definition valueOf {A} (o : loop_outcome A) := + match o with + | Done v => v + | Again v => v + end. + + Theorem reverse_ok : forall p ls, + {{linkedList p ls}} + reverse p + {{r ~> linkedList r (rev ls)}}. + Proof. + unfold reverse. + simp. + step. + loop_inv (fun o => exists ls1 ls2, [| ls = rev_append ls1 ls2 |] + * linkedList (fst (valueOf o)) ls2 + * linkedList (snd (valueOf o)) ls1 + * [| match o with + | Done (p, _) => p = ^0 + | _ => True + end |])%sep. + cases (weq a (^0)); simp. + step. + cancel. + step. + setoid_rewrite (linkedList_nonnull _ _ n). + step. + simp. + step. + step. + simp. + step. + setoid_rewrite (linkedList_nonnull _ _ n). + cancel. + simp. + setoid_rewrite linkedList_null. + cancel. + equality. + simp. + step. + cancel. + simp. + setoid_rewrite linkedList_null. + cancel. + simp. + cancel. + Qed. + + Opaque reverse. +End MixedEmbedded. + + +(** * A simple C-like language with just two data types *) + +Module DeeplyEmbedded(Import BW : BIT_WIDTH). + Definition wrd := word bit_width. + + Inductive exp := + | Var (x : var) + | Const (n : wrd) + | Add (e1 e2 : exp) + | Head (e : exp) + | Tail (e : exp) + | NotNull (e : exp). + + Inductive stmt := + | Skip + | Assign (x : var) (e : exp) + | WriteHead (x : var) (e : exp) + | WriteTail (x : var) (e : exp) + | Seq (s1 s2 : stmt) + | IfThenElse (e : exp) (s1 s2 : stmt) + | WhileLoop (e : exp) (s1 : stmt). + + Inductive type := + | Scalar + | ListPointer (t : type). + + Definition type_eq : forall t1 t2 : type, sumbool (t1 = t2) (t1 <> t2). + decide equality. + Defined. + + Record function := { + Params : list (var * type); + Locals : list (var * type); + Return : type; + Body : stmt + }. + + Section fn. + Variable fn : function. + + Definition vars := Params fn ++ Locals fn ++ [("result", Return fn)]. + + Fixpoint varType (x : var) (vs : list (var * type)) : option type := + match vs with + | nil => None + | (y, t) :: vs' => if y ==v x then Some t else varType x vs' + end. + + Fixpoint expType (e : exp) : option type := + match e with + | Var x => varType x vars + | Const _ => Some Scalar + | Add e1 e2 => match expType e1, expType e2 with + | Some Scalar, Some Scalar => Some Scalar + | _, _ => None + end + | Head x => match expType x with + | Some (ListPointer t) => Some t + | _ => None + end + | Tail x => match expType x with + | Some (ListPointer t) => Some (ListPointer t) + | _ => None + end + | NotNull e1 => match expType e1 with + | Some (ListPointer _) => Some Scalar + | _ => None + end + end. + + Fixpoint stmtWf (s : stmt) : bool := + match s with + | Skip => true + | Assign x e => match varType x vars, expType e with + | Some t1, Some t2 => + if type_eq t1 t2 then true else false + | _, _ => false + end + | WriteHead x e => match varType x vars, expType e with + | Some (ListPointer t1), Some t2 => + if type_eq t1 t2 then true else false + | _, _ => false + end + | WriteTail x e => match varType x vars, expType e with + | Some (ListPointer t1), Some (ListPointer t2) => + if type_eq t1 t2 then true else false + | _, _ => false + end + | Seq s1 s2 => stmtWf s1 && stmtWf s2 + | IfThenElse e s1 s2 => match expType e with + | Some Scalar => stmtWf s1 && stmtWf s2 + | _ => false + end + | WhileLoop e s1 => match expType e with + | Some Scalar => stmtWf s1 + | _ => false + end + end. + + Record functionWf : Prop := { + VarsOk : NoDup (map fst (Params fn ++ Locals fn)); + BodyOk : stmtWf (Body fn) = true + }. + End fn. + + Definition heap := fmap (wrd) (wrd * wrd). + Definition valuation := fmap var wrd. + + Inductive eval : heap -> valuation -> exp -> wrd -> Prop := + | VVar : forall H V x v, + V $? x = Some v + -> eval H V (Var x) v + | VConst : forall H V n, + eval H V (Const n) n + | VAdd : forall H V e1 e2 n1 n2, + eval H V e1 n1 + -> eval H V e2 n2 + -> eval H V (Add e1 e2) (n1 ^+ n2) + | VHead : forall H V e1 p ph pt, + eval H V e1 p + -> H $? p = Some (ph, pt) + -> eval H V (Head e1) ph + | VTail : forall H V e1 p ph pt, + eval H V e1 p + -> H $? p = Some (ph, pt) + -> eval H V (Tail e1) pt + | VNotNull : forall H V e1 p, + eval H V e1 p + -> eval H V (NotNull e1) (if weq p (^0) then ^1 else ^0). + + Inductive step : heap * valuation * stmt -> heap * valuation * stmt -> Prop := + | StAssign : forall H V x e v, + eval H V e v + -> step (H, V, Assign x e) (H, V $+ (x, v), Skip) + | StWriteHead : forall H V x e a v hv tv, + V $? x = Some a + -> eval H V e v + -> H $? a = Some (hv, tv) + -> step (H, V, WriteHead x e) (H $+ (a, (v, tv)), V, Skip) + | StWriteTail : forall H V x e a v hv tv, + V $? x = Some a + -> eval H V e v + -> H $? a = Some (hv, tv) + -> step (H, V, WriteTail x e) (H $+ (a, (hv, v)), V, Skip) + | StSeq1 : forall H V s2, + step (H, V, Seq Skip s2) (H, V, s2) + | StSeq2 : forall H V s1 s2 H' V' s1', + step (H, V, s1) (H', V', s1') + -> step (H, V, Seq s1 s2) (H', V', Seq s1' s2) + | StIfThen : forall H V e s1 s2 n, + eval H V e n + -> n <> ^0 + -> step (H, V, IfThenElse e s1 s2) (H, V, s1) + | StIfElse : forall H V e s1 s2, + eval H V e (^0) + -> step (H, V, IfThenElse e s1 s2) (H, V, s2) + | StWhileTrue : forall H V e s1 n, + eval H V e n + -> n <> ^0 + -> step (H, V, WhileLoop e s1) (H, V, Seq s1 (WhileLoop e s1)) + | StWhileFalse : forall H V e s1, + eval H V e (^0) + -> step (H, V, WhileLoop e s1) (H, V, Skip). + + Definition trsys_of (H : heap) (V : valuation) (s : stmt) := {| + Initial := {(H, V, s)}; + Step := step + |}. +End DeeplyEmbedded. + + +(** * Connecting the two *) + +Module MixedToDeep(Import BW : BIT_WIDTH). + Module Import DE := DeeplyEmbedded(BW). + Module Import ME := MixedEmbedded(BW). + + Inductive translate_exp (V : valuation) : forall {A}, A -> exp -> Prop := + | TrAdd : forall (v1 v2 : wrd) e1 e2, + translate_exp V v1 e1 + -> translate_exp V v2 e2 + -> translate_exp V (v1 ^+ v2) (Add e1 e2) + | TrVar : forall x v, + V $? x = Some v + -> translate_exp V v (Var x) + | TrConst : forall v, + translate_exp V v (Const v). + + Fixpoint couldWrite (x : var) (s : stmt) : bool := + match s with + | Assign y _ => if x ==v y then true else false + | Skip + | WriteHead _ _ + | WriteTail _ _ => false + | Seq s1 s2 + | IfThenElse _ s1 s2 => couldWrite x s1 || couldWrite x s2 + | WhileLoop _ s1 => couldWrite x s1 + end. + + Inductive translate (out : var) : valuation -> forall {A}, cmd A -> stmt -> Prop := + | TrReturn : forall V (A : Set) (v : A) e, + translate_exp V v e + -> translate out V (Return v) (Assign out e) + | TrReturned : forall V v, + V $? out = Some v + -> translate out V (Return v) Skip + | TrAssign : forall V (B : Set) (v : wrd) (c : wrd -> cmd B) e x s1, + translate_exp V v e + -> (forall w, translate out (V $+ (x, w)) (c w) s1) + -> translate out V (Bind (Return v) c) (Seq (Assign x e) s1) + | TrAssigned : forall V (B : Set) (v : wrd) (c : wrd -> cmd B) x s1, + V $? x = Some v + -> translate out (V $+ (x, v)) (c v) s1 + -> translate out V (Bind (Return v) c) (Seq Skip s1). + + Example adder (a b c : wrd) := + Bind (Return (a ^+ b)) (fun ab => Return (ab ^+ c)). + + Ltac freshFor vm k := + let rec keepTrying x := + let H := fresh in + (assert (H : vm $? x = None) by (simplify; equality); + clear H; k x) + || let x' := eval simpl in (x ++ "'")%string in keepTrying x' in + keepTrying "tmp". + + Ltac translate := + match goal with + | [ |- translate_exp _ (_ ^+ _) _ ] => eapply TrAdd + | [ |- translate_exp ?V ?v _ ] => + match V with + | context[add _ ?y v] => apply TrVar with (x := y); simplify; equality + end + + | [ |- translate _ _ (Return _) _ ] => apply TrReturn + | [ |- translate _ ?V (Bind (Return _) _) _ ] => + freshFor V ltac:(fun y => + eapply TrAssign with (x := y); [ | intro ]) + end. + + Lemma translate_adder : sig (fun s => + forall a b c, translate "result" ($0 $+ ("a", a) $+ ("b", b) $+ ("c", c)) (adder a b c) s). + Proof. + eexists; simplify. + unfold adder. + repeat translate. + Defined. + + Definition adder_compiled := Eval simpl in proj1_sig translate_adder. + + Inductive translated : forall {A}, DE.heap * valuation * stmt -> ME.heap * cmd A -> Prop := + | Translated : forall A H h V s (c : cmd A), + translate "result" V c s + -> translated (H, V, s) (h, c). + + Lemma eval_translate : forall H V e v, + eval H V e v + -> forall (v' : wrd), translate_exp V v' e + -> v = v'. + Proof. + induct 1; invert 1; simplify. + + apply inj_pair2 in H2; subst. + equality. + + apply inj_pair2 in H1; subst. + equality. + + apply inj_pair2 in H1; subst. + erewrite IHeval1 by eauto. + erewrite IHeval2 by eauto. + equality. + Qed. + + Lemma multistep_bind : forall A h (c1 : cmd A) h' c1', + step^* (h, c1) (h', c1') + -> forall B (c2 : A -> cmd B), step^* (h, Bind c1 c2) (h', Bind c1' c2). + Proof. + induct 1; eauto. + cases y; simplify. + specialize (IHtrc _ _ _ _ _ eq_refl JMeq.JMeq_refl JMeq.JMeq_refl JMeq.JMeq_refl _ c2). + eauto. + Qed. + + Lemma step_translate : forall H V s H' V' s', + DE.step (H, V, s) (H', V', s') + -> forall h (c : cmd wrd) out, + translate out V c s + -> exists c', ME.step^* (h, c) (h, c') + /\ translate out V' c' s'. + Proof. + induct 1; invert 1; simplify. + + apply inj_pair2 in H1; subst. + eapply eval_translate in H5; eauto; subst. + eexists; propositional. + eauto. + apply TrReturned; simplify; auto. + + apply inj_pair2 in H0; subst. + eexists; propositional. + eapply TrcFront. + eauto. + eauto. + replace V' with (V' $+ (x, v)). + assumption. + maps_equal. + symmetry; assumption. + + apply inj_pair2 in H2; subst. + invert H0. + eexists; propositional. + eauto. + eapply TrAssigned with (x := x). + eapply eval_translate in H7; eauto. + simplify. + subst. + reflexivity. + match goal with + | [ |- translate _ ?V' _ _ ] => replace V' with (V $+ (x, v)) by (maps_equal; equality) + end. + eauto. + + invert H0. + Qed. + + Theorem translated_simulates : forall H V c h s, + translate "result" V c s + -> simulates (translated (A := wrd)) (DE.trsys_of H V s) (ME.multistep_trsys_of h c). + Proof. + constructor; simplify. + + propositional; subst. + eexists; split. + econstructor. + eassumption. + eauto. + + invert H1. + apply inj_pair2 in H4; subst. + cases st1'. + cases p. + eapply step_translate in H2; eauto. + first_order. + eexists; split; [ | eassumption ]. + econstructor. + assumption. + Qed. + + Hint Constructors eval DE.step. + + Lemma translate_exp_sound : forall V v e, + translate_exp V v e + -> forall H, eval H V e v. + Proof. + induct 1; simplify; eauto. + Qed. + + Hint Resolve translate_exp_sound. + + Lemma not_stuck : forall A h (c : cmd A) h' c', + step (h, c) (h', c') + -> forall out V s, translate out V c s + -> forall H, exists p', DE.step (H, V, s) p'. + Proof. + induct 1; invert 1; simplify. + + eexists. + econstructor. + econstructor. + eauto. + + eexists. + econstructor. + + eexists. + econstructor. + econstructor. + eauto. + + eexists. + econstructor. + Qed. + + Theorem hoare_triple_sound : forall P (c : cmd wrd) Q V s, + hoare_triple P c Q + -> P $0 + -> translate "result" V c s + -> V $? "result" = None + -> invariantFor (DE.trsys_of $0 V s) + (fun p => snd p = Skip + \/ exists p', DE.step p p'). Proof. simplify. eapply invariant_weaken. - eapply hoare_triple_sound'; eauto. - simplify. + eapply invariant_simulates. + apply translated_simulates. + eassumption. + apply invariant_multistepify with (sys := trsys_of $0 c). + eauto using hoare_triple_sound. + invert 1; first_order. - cases s0. - cases p. - simplify. - pose proof (progress _ _ _ H2 v h h $0) as Hprog; simplify. - cases Hprog; eauto. - subst. - eapply invert_Skip in H2. - left; propositional. - apply H2; auto. - first_order. + cases st2; simplify; subst. + invert H4; simplify. + apply inj_pair2 in H9; subst. + invert H8. + apply inj_pair2 in H4; subst. + right; eexists. + econstructor; eauto. + auto. + + invert H4. + apply inj_pair2 in H6; subst; simplify. + cases x. + eapply not_stuck in H3; eauto. Qed. -End DeeplyEmbedded. + Theorem adder_ok : forall a b c, + {{emp}} + adder a b c + {{r ~> [| r = a ^+ b ^+ c |]}}. + Proof. + unfold adder. + simplify. + step. + step. + instantiate (1 := (fun r => [| r = a ^+ b |])%sep). + cancel. + simp. + step. + cancel. + equality. + Qed. + + Theorem adder_compiled_ok : forall a b c, + invariantFor (DE.trsys_of $0 ($0 $+ ("a", a) $+ ("b", b) $+ ("c", c)) adder_compiled) + (fun p => snd p = Skip + \/ exists p', DE.step p p'). + Proof. + simplify. + eapply hoare_triple_sound. + apply adder_ok. + constructor; auto. + apply (proj2_sig translate_adder). + simplify; equality. + Qed. +End MixedToDeep. + + +(** * Getting concrete *) + +Module Bw64. + Definition bit_width := 64. + Theorem bit_width_nonzero : bit_width > 0. + Proof. + unfold bit_width; linear_arithmetic. + Qed. +End Bw64. + +Module MixedEmbedded64. + Module Import ME := MixedEmbedded(Bw64). +End MixedEmbedded64. diff --git a/Invariant.v b/Invariant.v index 2dbffe8..a0c11d7 100644 --- a/Invariant.v +++ b/Invariant.v @@ -80,3 +80,21 @@ Definition parallel shared private1 private2 Initial := parallel1 sys1.(Initial) sys2.(Initial); Step := parallel2 sys1.(Step) sys2.(Step) |}. + + +(** * Switching to multistep versions of systems *) + +Lemma trc_idem : forall A (R : A -> A -> Prop) x1 x2, + R^*^* x1 x2 + -> R^* x1 x2. +Proof. + induction 1; eauto using trc_trans. +Qed. + +Theorem invariant_multistepify : forall {state} (sys : trsys state) + (invariant : state -> Prop), + invariantFor sys invariant + -> invariantFor {| Initial := Initial sys; Step := (Step sys)^* |} invariant. +Proof. + unfold invariantFor; simpl; intuition eauto using trc_idem. +Qed.