From 856d8b43b25576c2ddf1728556b22234758815ea Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 27 Apr 2016 18:04:39 -0400 Subject: [PATCH] ConcurrentSeparationLogic: for soundness proof, only cases left are for unlock and parallel composition --- ConcurrentSeparationLogic.v | 1118 ++++++++++++++--------------------- 1 file changed, 429 insertions(+), 689 deletions(-) diff --git a/ConcurrentSeparationLogic.v b/ConcurrentSeparationLogic.v index 820ba26..79bb52e 100644 --- a/ConcurrentSeparationLogic.v +++ b/ConcurrentSeparationLogic.v @@ -86,6 +86,13 @@ Inductive step : forall A, heap * locks * cmd A -> heap * locks * cmd A -> Prop | StepFree : forall h l a numWords, step (h, l, Free a numWords) (deallocate h a numWords, l, Return tt) +| StepLock : forall h l a, + ~a \in l + -> step (h, l, Lock a) (h, l \cup {a}, Return tt) +| StepUnlock : forall h l a, + a \in l + -> step (h, l, Unlock a) (h, l \setminus {a}, Return tt) + | StepPar1 : forall h l c1 c2 h' l' c1', step (h, l, c1) (h', l', c1') -> step (h, l, Par c1 c2) (h', l', Par c1' c2) @@ -293,7 +300,7 @@ Inductive hoare_triple (linvs : list hprop) : forall {result}, hprop -> cmd resu (forall acc, hoare_triple linvs (I (Again acc)) (body acc) I) -> hoare_triple linvs (I (Again init)) (Loop init body) (fun r => I (Done r)) | HtFail : forall {result}, - hoare_triple linvs (fun _ => False) (Fail (result := result)) (fun _ _ => False) + hoare_triple linvs [| False |]%sep (Fail (result := result)) (fun _ => [| False |])%sep | HtRead : forall a R, hoare_triple linvs (exists v, a |-> v * R v)%sep (Read a) (fun r => a |-> r * R r)%sep | HtWrite : forall a v', @@ -318,8 +325,8 @@ Inductive hoare_triple (linvs : list hprop) : forall {result}, hprop -> cmd resu (* When forking into two threads, divide the (local) heap among them. *) | HtPar : forall P1 c1 Q1 P2 c2 Q2, hoare_triple linvs P1 c1 Q1 - -> hoare_triple linvs P2 c1 Q2 - -> hoare_triple linvs (P1 * P1)%sep (Par c1 c2) (fun _ => Q1 tt * Q2 tt)%sep + -> hoare_triple linvs P2 c2 Q2 + -> hoare_triple linvs (P1 * P2)%sep (Par c1 c2) (fun _ => Q1 tt * Q2 tt)%sep (* Now we repeat these two structural rules from before. *) | HtConsequence : forall {result} (c : cmd result) P Q (P' : hprop) (Q' : _ -> hprop), @@ -332,50 +339,50 @@ Inductive hoare_triple (linvs : list hprop) : forall {result}, hprop -> cmd resu -> hoare_triple linvs (P * R)%sep c (fun r => Q r * R)%sep. -(* -Notation "{{ P }} c {{ r ~> Q }}" := - (hoare_triple P%sep c (fun r => Q%sep)) (at level 90, c at next level). +Notation "linvs ||- {{ P }} c {{ r ~> Q }}" := + (hoare_triple linvs 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 +Lemma HtStrengthen : forall linvs {result} (c : cmd result) P Q (Q' : _ -> hprop), + hoare_triple linvs P c Q -> (forall r, Q r ===> Q' r) - -> hoare_triple P c Q'. + -> hoare_triple linvs P c Q'. Proof. simplify. eapply HtConsequence; eauto. reflexivity. Qed. -Lemma HtWeaken : forall {result} (c : cmd result) P Q (P' : hprop), - hoare_triple P c Q +Lemma HtWeaken : forall linvs {result} (c : cmd result) P Q (P' : hprop), + hoare_triple linvs P c Q -> P' ===> P - -> hoare_triple P' c Q. + -> hoare_triple linvs P' c Q. Proof. simplify. eapply HtConsequence; eauto. reflexivity. Qed. -Lemma invert_Return : forall {result : Set} (r : result) P Q, - hoare_triple P (Return r) Q - -> forall h, P h -> Q r h. +Hint Resolve himp_refl. + +Lemma invert_Return : forall linvs {result : Set} (r : result) P Q, + hoare_triple linvs P (Return r) Q + -> P ===> Q r. Proof. induct 1; propositional; eauto. - exists h, $0; propositional; eauto. - unfold lift; propositional. + cancel. - unfold himp in *; eauto. + eauto using himp_trans. - unfold star, himp in *; simp; eauto 7. + rewrite IHhoare_triple; eauto. Qed. 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. +Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, + hoare_triple linvs P (Bind c1 c2) Q + -> exists R, hoare_triple linvs P c1 R + /\ forall r, hoare_triple linvs (R r) (c2 r) Q. Proof. induct 1; propositional; eauto. @@ -395,11 +402,11 @@ Proof. eapply HtFrame; eauto. 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). +Lemma invert_Loop : forall linvs {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) P Q, + hoare_triple linvs P (Loop init body) Q + -> exists I, (forall acc, hoare_triple linvs (I (Again acc)) (body acc) I) + /\ P ===> I (Again init) + /\ (forall r, I (Done r) ===> Q r). Proof. induct 1; propositional; eauto. @@ -407,19 +414,12 @@ Proof. exists x; propositional; eauto. unfold himp in *; eauto. + eauto using himp_trans. + 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. + rewrite H0; eauto. + rewrite H3; eauto. Qed. (* Now that we proved enough basic facts, let's hide the definitions of all @@ -438,16 +438,18 @@ Proof. linear_arithmetic. Qed. -Lemma invert_Read : forall a P Q, - hoare_triple P (Read a) Q +Lemma invert_Read : forall linvs a P Q, + hoare_triple linvs 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_nat in x0; simp. + + apply unit_not_nat in x0; simp. + + apply unit_not_nat in x0; simp. apply unit_not_nat in x0; simp. @@ -463,8 +465,8 @@ Proof. cancel. Qed. -Lemma invert_Write : forall a v' P Q, - hoare_triple P (Write a v') Q +Lemma invert_Write : forall linvs a v' P Q, + hoare_triple linvs P (Write a v') Q -> exists R, (P ===> (exists v, a |-> v) * R)%sep /\ a |-> v' * R ===> Q tt. Proof. @@ -491,8 +493,8 @@ Proof. cancel. Qed. -Lemma invert_Alloc : forall numWords P Q, - hoare_triple P (Alloc numWords) Q +Lemma invert_Alloc : forall linvs numWords P Q, + hoare_triple linvs P (Alloc numWords) Q -> forall r, P * r |--> zeroes numWords ===> Q r. Proof. induct 1; simp; eauto. @@ -503,8 +505,14 @@ Proof. apply unit_not_nat in x0; simp. - rewrite H0. - eauto using himp_trans. + apply unit_not_nat in x0; simp. + + apply unit_not_nat in x0; simp. + + apply unit_not_nat in x0; simp. + + rewrite H0; eauto. + eauto 7 using himp_trans. rewrite <- IHhoare_triple. cancel. @@ -568,7 +576,7 @@ Lemma initialize_fresh : forall a' h a numWords, Proof. induct numWords; simp; auto. Qed. - + Lemma zeroes_initialize : forall numWords a h, (forall i, i < numWords -> h $? (a + i) = None) -> (fun h' => h' = initialize h a numWords) ===> (fun h' => h' = h) * a |--> zeroes numWords. @@ -586,8 +594,8 @@ Proof. rewrite initialize_fresh; auto. Qed. -Lemma invert_Free : forall a numWords P Q, - hoare_triple P (Free a numWords) Q +Lemma invert_Free : forall linvs a numWords P Q, + hoare_triple linvs P (Free a numWords) Q -> P ===> a |->? numWords * Q tt. Proof. induct 1; simp; eauto. @@ -651,9 +659,9 @@ Proof. Opaque himp. Qed. -Lemma HtReturn' : forall P {result : Set} (v : result) Q, +Lemma HtReturn' : forall linvs P {result : Set} (v : result) Q, P ===> Q v - -> hoare_triple P (Return v) Q. + -> hoare_triple linvs P (Return v) Q. Proof. simp. eapply HtStrengthen. @@ -662,699 +670,431 @@ Proof. cancel. Qed. +Opaque heq himp lift star exis ptsto. + +Lemma invert_Lock : forall linvs a P Q, + hoare_triple linvs P (Lock a) Q + -> exists I, nth_error linvs a = Some I + /\ P * I ===> Q tt. +Proof. + induct 1; simp; eauto 10. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + eexists; simp. + eauto. + cancel. + + eexists; simp. + eauto. + rewrite H0; eauto using himp_trans. + + eexists; simp. + eauto. + rewrite <- H2. + cancel. +Qed. + +Lemma invert_Unlock : forall linvs a P Q, + hoare_triple linvs P (Unlock a) Q + -> exists I, nth_error linvs a = Some I + /\ P ===> Q tt * I. +Proof. + induct 1; simp; eauto 10. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + eexists; simp. + eauto. + cancel. + + eexists; simp. + eauto. + rewrite <- H1; eauto using himp_trans. + + eexists; simp. + eauto. + rewrite H2. + cancel. +Qed. + +Lemma invert_Par : forall linvs c1 c2 P Q, + hoare_triple linvs P (Par c1 c2) Q + -> exists P1 P2 Q1 Q2, + hoare_triple linvs P1 c1 Q1 + /\ hoare_triple linvs P2 c2 Q2 + /\ P ===> P1 * P2 + /\ Q1 tt * Q2 tt ===> Q tt. +Proof. + induct 1; simp; eauto 10. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + eauto 10 using himp_trans. + + exists (x * R)%sep, x0, (fun r => x1 r * R)%sep, x2; simp; eauto. + rewrite H2; cancel. + rewrite <- H4; cancel. +Qed. + (* Temporarily transparent again! *) Transparent heq himp lift star exis ptsto. -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. +(* Guarded predicates *) +Definition guarded (P : Prop) (p : hprop) : hprop := + fun h => IF P then p h else emp%sep h. + +Infix "===>" := guarded : sep_scope. + +Theorem guarded_true : forall (P : Prop) p, P + -> (P ===> p) === p. +Proof. + unfold heq, guarded, IF_then_else; simp. +Qed. + +Theorem guarded_false : forall (P : Prop) p, ~P + -> (P ===> p) === emp. +Proof. + unfold heq, guarded, IF_then_else; simp. +Qed. + +(* Iterated separating conjunction *) +Fixpoint bigstar A (P : nat -> A -> hprop) (ls : list A) : hprop := + match ls with + | nil => emp + | x :: ls' => P 0 x * bigstar (fun n => P (S n)) ls' + end%sep. + +Definition lockChunks (l : locks) (ls : list hprop) := + bigstar (fun i I => (~i \in l) ===> I)%sep ls. + +Lemma use_himp : forall P Q, P ===> Q + -> forall h, P h -> Q h. +Proof. + auto. +Qed. + +Lemma ptsto_out : forall h a v p, + h $? a = Some v + -> (exists v', a |-> v' * p v')%sep h + -> (a |-> v * p v)%sep h + /\ forall v', (a |-> v' * p v)%sep (h $+ (a, v')). +Proof. + invert 2. + invert H1. + simp. + + invert H2. + unfold split in H0; subst. + rewrite lookup_join1 in H. + unfold heap1 in H. + simplify. + invert H. + exists (heap1 a v), x1; simp. + eauto. + unfold ptsto. + eauto. + unfold heap1; simplify. + sets. + + invert H2. + unfold split in H0; subst. + rewrite lookup_join1 in H. + unfold heap1 in H. + simplify. + invert H. + exists (heap1 a v'), x1; simp. + unfold split. + maps_equal. + rewrite lookup_join1. + unfold heap1; simplify; auto. + unfold heap1; simplify; sets. + repeat rewrite lookup_join2; auto. + unfold heap1; simplify; sets. + unfold heap1; simplify; sets. + unfold disjoint in *; simp. + apply (H1 a0); eauto. + cases (a ==n a0); simp. + unfold heap1 in *; simplify; equality. + unfold heap1 in *; simplify; equality. + unfold ptsto. + eauto. + unfold heap1; simplify; sets. +Qed. + +Lemma specialize_hprop : forall (p : hprop) h, + p h + -> (fun h' => h' = h) ===> p. +Proof. + unfold himp; equality. +Qed. + +Opaque heq himp lift star exis ptsto. + +Lemma bigstar_impl : forall A ls (p q : nat -> A -> hprop), + (forall i x, p i x ===> q i x) + -> bigstar p ls ===> bigstar q ls. +Proof. + induct ls; simplify; auto. + rewrite H. + rewrite IHls. + cancel. + simp. + eauto. +Qed. + +Lemma guarded_impl : forall P Q p, + P <-> Q + -> (P ===> p) ===> (Q ===> p). +Proof. + simp. + excluded_middle P. + repeat rewrite guarded_true by propositional. + auto. + repeat rewrite guarded_false by propositional. + auto. +Qed. + +Lemma lockChunks_lock' : forall l I linvs (f : nat -> nat) a, + ~f a \in l + -> nth_error linvs a = Some I + -> (forall x y, f x = f y -> x = y) + -> bigstar (fun i I => (~f i \in l) ===> I)%sep linvs ===> I * bigstar (fun i I => (~(f i \in l \cup {f a})) ===> I)%sep linvs. +Proof. + induct linvs; simplify. + + cases a; simplify; equality. + + cases a0; simplify. + invert H0. + rewrite guarded_true by sets. + rewrite guarded_false by sets. + cancel. + apply bigstar_impl. + simp. + apply guarded_impl. + sets. + apply H1 in H2. + equality. + + apply (IHlinvs (fun n => f (S n))) in H0; auto. + rewrite H0. + cancel. + apply guarded_impl. + sets. + apply H1 in H3. + equality. + simp. + apply H1 in H2. + equality. +Qed. + +Lemma lockChunks_lock : forall a l I linvs, + ~a \in l + -> nth_error linvs a = Some I + -> lockChunks l linvs ===> I * lockChunks (l \cup {a}) linvs. +Proof. + simp. + apply lockChunks_lock' with (f := fun n => n); auto. +Qed. + +Lemma preservation : forall linvs {result} (c : cmd result) h l c' h' l', + step (h, l, c) (h', l', c') + -> forall P Q, hoare_triple linvs P c Q + -> (P * lockChunks l linvs)%sep h + -> exists P', hoare_triple linvs P' c' Q + /\ (P' * lockChunks l' linvs)%sep h'. Proof. induct 1; simplify. apply invert_Bind in H0; simp. + apply IHstep in H0; eauto. + simp. eauto. - + apply invert_Bind in H; simp. specialize (invert_Return H); eauto using HtWeaken. apply invert_Loop in H; simp. + eexists; simp. econstructor. - eapply HtWeaken. eauto. - assumption. simp. cases r. apply HtReturn'. - unfold himp; simp; eauto. + auto. eapply HtStrengthen. eauto. - unfold himp; simp; eauto. + eauto. + eapply use_himp; try eassumption. + rewrite H1. + eauto. apply invert_Read in H0; simp. + assert ((exists v, a |-> v * (x v * lockChunks l' linvs))%sep h'). + eapply use_himp; try eassumption. + rewrite H0. + cancel. + eapply ptsto_out in H2; eauto. + eexists; 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. + eauto. + eapply use_himp; try eassumption. + cancel. apply invert_Write in H0; simp. + assert ((exists v, a |-> v * (x * lockChunks l' linvs))%sep h). + eapply use_himp; try eassumption. + rewrite H0. + cancel. + eapply ptsto_out in H2; eauto. + propositional. + eexists; simp. apply HtReturn'. - simp. - assert (((exists v : nat, 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 (a0 ==n a); simp. - apply H1 with (a0 := a). - unfold heap1; simp. - equality. - assumption. - unfold ptsto; reflexivity. + eauto. + eapply use_himp; try apply H5. + cancel. apply invert_Alloc with (r := a) in H0. + eexists; propositional. apply HtReturn'. - unfold himp; simp. - eapply himp_trans in H0; try apply zeroes_initialize. - auto. - assumption. + eassumption. + apply use_himp with ((P * lockChunks l' linvs) * a |--> zeroes numWords)%sep. + cancel. + apply use_himp with ((fun h' => h' = h) * a |--> zeroes numWords)%sep. + cancel. + eauto using specialize_hprop. + eapply use_himp. + apply zeroes_initialize; auto. + simp. apply invert_Free in H. - assert ((a |->? numWords * Q tt)%sep h) by auto. + eexists; propositional. + instantiate (1 := Q tt). apply HtReturn'. - unfold himp; simp. - eapply do_deallocate. - eauto. -Qed. - -Lemma deallocate_None : forall a' numWords h a, - h $? a' = None - -> deallocate h a numWords $? a' = None. -Proof. - induct numWords; simp. - rewrite IHnumWords; simp. - cases (a ==n a'); simp. -Qed. - -Lemma preservation_finite : forall {result} (c : cmd result) h c' h' bound, - step (h, c) (h', c') - -> (forall a, a >= bound -> h $? a = None) - -> exists bound', forall a, a >= bound' -> h' $? a = None. -Proof. - induct 1; simplify; eauto. - - exists bound; simp. - cases (a ==n a0); simp. - rewrite H0 in H; equality. auto. + apply do_deallocate; simplify. + change (fun f => (Q tt * lockChunks l' linvs) f)%sep with (Q tt * lockChunks l' linvs)%sep. + eapply use_himp; try eassumption. + rewrite H. + cancel. - exists (max bound (a + numWords)); simp. - rewrite initialize_fresh; auto. + apply invert_Lock in H0. + simp. + eexists; propositional. + apply HtReturn'; auto. + eapply use_himp; try eassumption. + rewrite <- H3. + cancel. + apply lockChunks_lock; auto. +Admitted. - exists bound; simp. - eauto using deallocate_None. -Qed. +Definition allLockChunks (linvs : list hprop) := bigstar (fun _ I => I) linvs. -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 bound, forall a, a >= bound -> h $? a = None) - -> (exists r, c = Return r) - \/ (exists h' c', step (h, c) (h', c')). +Lemma allLockChunks_lockChunks' : forall linvs (f : nat -> nat), + bigstar (fun _ I => I) linvs ===> bigstar (fun i I => (~f i \in {}) ===> I) linvs. 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. + induct linvs; simp; auto. - invert H1. - right; exists h, (Return x0). - 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 lift in H1; simp. - apply split_empty_fwd' in H; simp. - right; exists (initialize h2 x numWords), (Return x). - constructor. - simp; auto. - - unfold star in H2; simp. - apply IHhoare_triple with (h := h) (h1 := x0) (h2 := h2 $++ x1); eauto. - unfold split in *; simp. - rewrite (@join_comm _ _ h2 x1). - apply join_assoc. - sets. - cases (h2 $? x2). - cases (x1 $? x2). - specialize (H2 x2). - specialize (H1 x2). - rewrite lookup_join2 in H1. - apply H1; equality. - unfold not. - simplify. - cases (x0 $? x2). - 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 H8. - apply H1 with (a := a); auto. - rewrite lookup_join1; auto. - cases (x0 $? a); try equality. - eauto using lookup_Some_dom. - eauto using lookup_Some_dom. - rewrite lookup_join2 in H8; eauto. - eauto using lookup_None_dom. + rewrite guarded_true by sets. + rewrite IHlinvs. + cancel. Qed. -Lemma hoare_triple_sound' : forall P {result} (c : cmd result) Q, - hoare_triple P c Q - -> P $0 - -> invariantFor (trsys_of $0 c) +Lemma allLockChunks_lockChunks : forall linvs, + allLockChunks linvs ===> lockChunks {} linvs. +Proof. + simp. + apply allLockChunks_lockChunks' with (f := fun n => n). +Qed. + +Lemma hoare_triple_sound' : forall linvs P {result} (c : cmd result) Q, + hoare_triple linvs P c Q + -> forall h, (P * allLockChunks linvs)%sep h + -> invariantFor (trsys_of h {} c) (fun p => - (exists bound, forall a, a >= bound -> fst p $? a = None) - /\ hoare_triple (fun h' => h' = fst p) - (snd p) - Q). + let '(h, l, c) := p in + exists P', hoare_triple linvs P' c Q + /\ (P' * lockChunks l linvs)%sep h). Proof. simplify. apply invariant_induction; simplify. propositional; subst; simplify. - exists 0; simp. - eapply HtWeaken; eauto. - unfold himp; simplify; equality. + eexists; propositional. + eauto. + eapply use_himp; try eassumption. + rewrite allLockChunks_lockChunks. + auto. cases s. + cases p. cases s'. + cases p. simp. - eauto using preservation_finite. eauto using preservation. Qed. -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')). +Fixpoint notAboutToFail {result} (c : cmd result) := + match c with + | Fail _ => false + | Bind _ _ c1 _ => notAboutToFail c1 + | Par c1 c2 => notAboutToFail c1 && notAboutToFail c2 + | _ => true + end. + +Lemma hoare_triple_notAboutToFail : forall linvs P result (c : cmd result) Q, + hoare_triple linvs P c Q + -> notAboutToFail c = false + -> P ===> [| False |]. +Proof. + induct 1; simp; try equality; eauto using himp_trans. + + apply andb_false_iff in H1; propositional. + rewrite H1; cancel. + rewrite H1; cancel. + + rewrite H1; cancel. +Qed. + +Lemma False_star : forall p, + [| False |] * p ===> [| False |]. +Proof. + cancel. +Qed. + +Theorem hoare_triple_sound : forall linvs P {result} (c : cmd result) Q, + hoare_triple linvs P c Q + -> forall h, (P * allLockChunks linvs)%sep h + -> invariantFor (trsys_of h {} c) + (fun p => let '(_, _, c) := p in + notAboutToFail c = true). Proof. simplify. eapply invariant_weaken. eapply hoare_triple_sound'; eauto. simp. - specialize (progress H3); simplify. - specialize (H2 (fst s) (fst s) $0). - assert (split (fst s) (fst s) $0) by auto. - assert (disjoint (fst s) $0) by auto. - assert (exists bound, forall a, a >= bound -> fst s $? a = None) by eauto. - 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 *) - -Opaque heq himp lift star exis ptsto. - -(* Here comes some automation that we won't explain in detail, instead opting to - * use examples. *) - -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. + cases s. + cases p. 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 || eapply HtAlloc || eapply HtFree. - -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. - -(* That's the end of the largely unexplained automation. Let's prove some - * programs! *) - - -(** ** Swapping with two pointers *) - -Definition swap p q := - tmpp <- Read p; - tmpq <- Read q; - _ <- Write p tmpq; - Write q tmpp. - -(* Looking at the precondition here, note how we no longer work with explicit - * functions over heaps. All that is hidden within the assertion language. - * Also note that the definition of [*] gives us nonaliasing of [p] and [q] for - * free! *) -Theorem swap_ok : forall p q a b, - {{p |-> a * q |-> b}} - swap p q - {{_ ~> p |-> b * q |-> a}}. -Proof. - unfold swap. - (* [simp] is our generic simplifier for this file. *) - simp. - (* We generally just keep calling [step] to advance forward by one atomic - * statement. *) - step. - step. - (* We do often want to use [simp] to clean up the goal after [step] infers an - * intermediate assertion. *) - simp. - step. - step. - simp. - step. - step. - simp. - step. - (* The [cancel] procedure repeatedly finds matching subformulas on the two - * sides of [===>], removing them and recurring, possibly learning the values - * of some unification variables each time. *) - cancel. - subst. + cases (notAboutToFail c0); auto. + eapply hoare_triple_notAboutToFail in Heq; eauto. + apply use_himp with (Q := [| False |]%sep) in H3. + invert H3; propositional. + rewrite Heq. cancel. Qed. - -Opaque swap. -(* This command prevents later proofs from peeking inside the implementation of - * [swap]. Instead, we only reason about it through [swap_ok]. *) - -(* Two swaps in a row provide a kind of rotation across three addresses. *) -Definition rotate p q r := - _ <- swap p q; - swap q r. - -Theorem rotate_ok : forall p q r a b c, - {{p |-> a * q |-> b * r |-> c}} - rotate p q r - {{_ ~> p |-> b * q |-> c * r |-> a}}. -Proof. - unfold rotate. - simp. - step. - (* Now we invoke our earlier theorem by name. Note that its precondition only - * matches a subset of our current precondition. The rest of state is left - * alone, which we can prove "for free" by the frame rule. *) - use swap_ok. - simp. - use swap_ok. - simp. - cancel. -Qed. - -Opaque rotate. - -(** ** Initializing a fresh object *) - -Definition init := - p <- Alloc 2; - _ <- Write p 7; - _ <- Write (p+1) 8; - Return p. - -Theorem init_ok : - {{emp}} - init - {{p ~> p |--> [7; 8]}}. -Proof. - unfold init. - simp. - step. - step. - simp. - step. - step. - simp. - step. - step. - simp. - step. - cancel. -Qed. - -Opaque init. - -Theorem the_circle_of_life_ok : - {{emp}} - p <- init; - Free p 2 - {{_ ~> emp}}. -Proof. - step. - use init_ok. - simp. - step. - cancel. -Qed. - -Theorem ultra_combo_ok : - {{emp}} - p <- init; - _ <- swap p (p+1); - Return p - {{p ~> p |--> [8; 7]}}. -Proof. - step. - use init_ok. - simp. - step. - use swap_ok. - simp. - step. - cancel. -Qed. - -(** ** In-place reversal of a singly linked list *) - -(* Let's give a recursive definition of how a linked list should be laid out in - * memory. *) -Fixpoint linkedList (p : nat) (ls : list nat) := - match ls with - | nil => [| p = 0 |] - (* An empty list is associated with a null pointer and no memory - * contents. *) - | x :: ls' => [| p <> 0 |] - * exists p', p |--> [x; p'] * linkedList p' ls' - (* A nonempty list is associated with a nonnull pointer and a two-cell - * struct, which points to a further list. *) - end%sep. - -(* The definition of [linkedList] is recursive in the list. Let's also prove - * lemmas for simplifying [linkedList] invocations based on values of [p]. *) - -Theorem linkedList_null : forall ls, - linkedList 0 ls === [| ls = nil |]. -Proof. - (* Tactic [heq] breaks an equivalence into two implications. *) - 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. - -(* Let's hide the definition of [linkedList], so that we *only* reason about it - * via the two lemmas we just proved. *) -Opaque linkedList. - -(* In-place linked-list reverse, the "hello world" of separation logic! *) -Definition reverse p := - pr <- for pr := (p, 0) loop - let (p, r) := pr in - if p ==n 0 then - Return (Done pr) - else - tmp <- Read (p + 1); - _ <- Write (p+1) r; - Return (Again (tmp, p)) - done; - Return (snd pr). - -(* Helper function to peel away the [Done]/[Again] status of a [loop_outcome] *) -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. - (* When we reach a loop, we give the invariant with a special tactic. *) - 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 (a ==n 0); simp. - step. - cancel. - step. - (* We use [setoid_rewrite] for rewriting under binders ([exists], in this - * case). Note that we also specify hypothesis [n] explicitly, since - * [setoid_rewrite] isn't smart enough to infer parameters otherwise. *) - 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. - -(* ** Calling [reverse] twice, to illustrate the *frame rule* *) - -Theorem reverse_two_ok : forall p1 ls1 p2 ls2, - {{linkedList p1 ls1 * linkedList p2 ls2}} - p1 <- reverse p1; - p2 <- reverse p2; - Return (p1, p2) - {{ps ~> linkedList (fst ps) (rev ls1) * linkedList (snd ps) (rev ls2)}}. -Proof. - simp. - step. - use reverse_ok. - simp. - step. - use reverse_ok. - simp. - step. - cancel. -Qed. -(* Note that the intuitive correctness theorem would be *false* for lists - * sharing any cells in common! The inherent disjointness of [*] saves us from - * worrying about those cases. *) - - -(* ** Computing the length of a linked list *) - -(* To state a good loop invariant, it will be helpful to define - * *list segments* that end with some pointer beside null. *) -Fixpoint linkedListSegment (p : nat) (ls : list nat) (q : nat) := - match ls with - | nil => [| p = q |] - | x :: ls' => [| p <> 0 |] * exists p', p |-> x * (p+1) |-> p' * linkedListSegment p' ls' q - end%sep. - -(* Next, two [linkedListSegment] lemmas analogous to those for [linkedList] - * above *) - -Lemma linkedListSegment_empty : forall p ls, - linkedList p ls ===> linkedList p ls * linkedListSegment p nil p. -Proof. - cancel. -Qed. - -Lemma linkedListSegment_append : forall q r x ls p, - q <> 0 - -> linkedListSegment p ls q * q |-> x * (q+1) |-> r ===> linkedListSegment p (ls ++ x :: nil) r. -Proof. - induct ls; cancel; auto. - subst; cancel. - rewrite <- IHls; cancel; auto. -Qed. - -(* One more [linkedList] lemma will be helpful. We'll re-reveal the predicate's - * definition to prove the lemma. *) - -Transparent linkedList. - -Lemma linkedListSegment_null : forall ls p, - linkedListSegment p ls 0 ===> linkedList p ls. -Proof. - induct ls; cancel; auto. -Qed. - -Opaque linkedList linkedListSegment. - -(* A few algebraic properties of list operations: *) -Hint Rewrite <- app_assoc. -Hint Rewrite app_length app_nil_r. - -(* We tie a few of them together into this lemma. *) -Lemma move_along : forall A (ls : list A) x2 x1 x0 x, - ls = x2 ++ x1 - -> x1 = x0 :: x - -> ls = (x2 ++ [x0]) ++ x. -Proof. - simp. -Qed. - -Hint Resolve move_along. - -Theorem length_ok : forall p ls, - {{linkedList p ls}} - q_len <- for q_len := (p, 0) loop - let (q, len) := q_len in - if q ==n 0 then - Return (Done q_len) - else - tmp <- Read (q + 1); - Return (Again (tmp, len+1)) - done; - Return (snd q_len) - {{len ~> linkedList p ls * [| len = length ls |]}}. -Proof. - simp. - step. - loop_inv (fun o => exists ls1 ls2, [| ls = ls1 ++ ls2 |] - * linkedListSegment p ls1 (fst (valueOf o)) - * linkedList (fst (valueOf o)) ls2 - * [| snd (valueOf o) = length ls1 |] - * [| match o with - | Done (q, _) => q = 0 /\ ls2 = nil - | _ => True - end |])%sep. - cases (a ==n 0); simp. - step. - setoid_rewrite linkedList_null. - cancel. - step. - setoid_rewrite (linkedList_nonnull _ n). - step. - simp. - step. - cancel. - eauto. - simp. - setoid_rewrite <- linkedListSegment_append. - cancel. - auto. - rewrite linkedListSegment_empty. - cancel. - simp. - step. - cancel. - simp. - simp. - rewrite linkedListSegment_null. - rewrite linkedList_null. - cancel. -Qed. -*)