From ef310e2b1e62df27cc0d92e5095168ad86a409d6 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 17 Apr 2016 16:55:52 -0400 Subject: [PATCH] SeparationLogic: soundness proof --- Map.v | 257 +++++++++++ SeparationLogic.v | 1079 ++++++++++++++++++++++++++++++++++++++++++++- _CoqProject | 1 + 3 files changed, 1335 insertions(+), 2 deletions(-) diff --git a/Map.v b/Map.v index f883391..149af30 100644 --- a/Map.v +++ b/Map.v @@ -175,6 +175,101 @@ Module Type S. Axiom lookup_None_dom : forall K V (m : fmap K V) k, m $? k = None -> ~ k \in dom m. + + (* Bits meant for separation logic *) + Section splitting. + Variables K V : Type. + + Definition disjoint (h1 h2 : fmap K V) : Prop := + forall a, h1 $? a <> None + -> h2 $? a <> None + -> False. + + Definition split (h h1 h2 : fmap K V) : Prop := + h = h1 $++ h2. + + Axiom split_empty_fwd : forall h h1, + split h h1 $0 + -> h = h1. + + Axiom split_empty_fwd' : forall h h1, + split h $0 h1 + -> h = h1. + + Axiom split_empty_bwd : forall h, + split h h $0. + + Axiom split_empty_bwd' : forall h, + split h $0 h. + + Axiom disjoint_hemp : forall h, + disjoint h $0. + + Axiom disjoint_hemp' : forall h, + disjoint $0 h. + + Axiom disjoint_comm : forall h1 h2, + disjoint h1 h2 + -> disjoint h2 h1. + + Axiom split_comm : forall h h1 h2, + disjoint h1 h2 + -> split h h1 h2 + -> split h h2 h1. + + Axiom split_assoc1 : forall h h1 h' h2 h3, + split h h1 h' + -> split h' h2 h3 + -> split h (join h1 h2) h3. + + Axiom split_assoc2' : forall h h1 h' h2 h3, + split h h1 h' + -> split h' h2 h3 + -> disjoint h1 h' + -> disjoint h2 h3 + -> split h h2 (join h3 h1). + + Axiom split_assoc2 : forall h h1 h' h2 h3, + split h h' h1 + -> split h' h2 h3 + -> disjoint h' h1 + -> disjoint h2 h3 + -> split h h2 (join h3 h1). + + Axiom disjoint_assoc1 : forall h h1 h' h2 h3, + split h h1 h' + -> split h' h2 h3 + -> disjoint h1 h' + -> disjoint h2 h3 + -> disjoint (join h1 h2) h3. + + Axiom disjoint_assoc2 : forall h h1 h' h2 h3, + split h h' h1 + -> split h' h2 h3 + -> disjoint h' h1 + -> disjoint h2 h3 + -> disjoint h2 (join h3 h1). + + Axiom split_join : forall h1 h2, + split (join h1 h2) h1 h2. + + Axiom split_disjoint : forall h h1 h2 h' h3, + split h h1 h' + -> split h' h2 h3 + -> disjoint h1 h' + -> disjoint h2 h3 + -> disjoint h1 h2. + + Axiom disjoint_assoc3 : forall h h1 h2 h3, + disjoint h h2 + -> split h h1 h3 + -> disjoint h1 h3 + -> disjoint h3 h2. + End splitting. + + Hint Immediate disjoint_comm split_comm. + Hint Immediate split_empty_bwd disjoint_hemp disjoint_hemp' split_assoc1 split_assoc2. + Hint Immediate disjoint_assoc1 disjoint_assoc2 split_join split_disjoint disjoint_assoc3. End S. Module M : S. @@ -479,6 +574,168 @@ Module M : S. Proof. unfold lookup, dom, In; congruence. Qed. + + Section splitting. + Variables K V : Type. + + Notation "$0" := (@empty K V). + Notation "m $+ ( k , v )" := (add m k v) (at level 50, left associativity). + Infix "$-" := remove (at level 50, left associativity). + Infix "$++" := join (at level 50, left associativity). + Infix "$?" := lookup (at level 50, no associativity). + Infix "$<=" := includes (at level 90). + + Definition disjoint (h1 h2 : fmap K V) : Prop := + forall a, h1 $? a <> None + -> h2 $? a <> None + -> False. + + Definition split (h h1 h2 : fmap K V) : Prop := + h = h1 $++ h2. + + Hint Extern 2 (_ <> _) => congruence. + + Ltac splt := unfold disjoint, split, join, lookup in *; intros; subst; + try match goal with + | [ |- @eq (fmap K V) _ _ ] => let a := fresh "a" in extensionality a; simpl + end; + repeat match goal with + | [ a : K, H : forall a : K, _ |- _ ] => specialize (H a) + end; + repeat match goal with + | [ H : _ |- _ ] => rewrite H + | [ |- context[match ?E with Some _ => _ | None => _ end] ] => destruct E + | [ _ : context[match ?E with Some _ => _ | None => _ end] |- _ ] => destruct E + end; eauto; try solve [ exfalso; eauto ]. + + Lemma split_empty_fwd : forall h h1, + split h h1 $0 + -> h = h1. + Proof. + splt. + Qed. + + Lemma split_empty_fwd' : forall h h1, + split h $0 h1 + -> h = h1. + Proof. + splt. + Qed. + + Lemma split_empty_bwd : forall h, + split h h $0. + Proof. + splt. + Qed. + + Lemma split_empty_bwd' : forall h, + split h $0 h. + Proof. + splt. + Qed. + + Lemma disjoint_hemp : forall h, + disjoint h $0. + Proof. + splt. + Qed. + + Lemma disjoint_hemp' : forall h, + disjoint $0 h. + Proof. + splt. + Qed. + + Lemma disjoint_comm : forall h1 h2, + disjoint h1 h2 + -> disjoint h2 h1. + Proof. + splt. + Qed. + + Lemma split_comm : forall h h1 h2, + disjoint h1 h2 + -> split h h1 h2 + -> split h h2 h1. + Proof. + splt. + Qed. + + Hint Immediate disjoint_comm split_comm. + + Lemma split_assoc1 : forall h h1 h' h2 h3, + split h h1 h' + -> split h' h2 h3 + -> split h (join h1 h2) h3. + Proof. + splt. + Qed. + + Lemma split_assoc2' : forall h h1 h' h2 h3, + split h h1 h' + -> split h' h2 h3 + -> disjoint h1 h' + -> disjoint h2 h3 + -> split h h2 (join h3 h1). + Proof. + splt. + Qed. + + Lemma split_assoc2 : forall h h1 h' h2 h3, + split h h' h1 + -> split h' h2 h3 + -> disjoint h' h1 + -> disjoint h2 h3 + -> split h h2 (join h3 h1). + Proof. + intros; eapply split_assoc2'; eauto. + Qed. + + Lemma disjoint_assoc1 : forall h h1 h' h2 h3, + split h h1 h' + -> split h' h2 h3 + -> disjoint h1 h' + -> disjoint h2 h3 + -> disjoint (join h1 h2) h3. + Proof. + splt. + Qed. + + Lemma disjoint_assoc2 : forall h h1 h' h2 h3, + split h h' h1 + -> split h' h2 h3 + -> disjoint h' h1 + -> disjoint h2 h3 + -> disjoint h2 (join h3 h1). + Proof. + splt. + Qed. + + Lemma split_join : forall h1 h2, + split (join h1 h2) h1 h2. + Proof. + splt. + Qed. + + Lemma split_disjoint : forall h h1 h2 h' h3, + split h h1 h' + -> split h' h2 h3 + -> disjoint h1 h' + -> disjoint h2 h3 + -> disjoint h1 h2. + Proof. + splt. + Qed. + + Lemma disjoint_assoc3 : forall h h1 h2 h3, + disjoint h h2 + -> split h h1 h3 + -> disjoint h1 h3 + -> disjoint h3 h2. + Proof. + splt. + Qed. + End splitting. End M. Export M. diff --git a/SeparationLogic.v b/SeparationLogic.v index 5e9acee..674d245 100644 --- a/SeparationLogic.v +++ b/SeparationLogic.v @@ -3,7 +3,7 @@ * Author: Adam Chlipala * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) -Require Import Frap. +Require Import Frap Setoid Classes.Morphisms. Set Implicit Arguments. Set Asymmetric Patterns. @@ -56,7 +56,7 @@ Fixpoint initialize (h : heap) (base numWords : nat) : heap := Fixpoint deallocate (h : heap) (base numWords : nat) : heap := match numWords with | O => h - | S numWords' => deallocate h base numWords' $- (base + numWords') + | S numWords' => deallocate (h $- (base + numWords')) base numWords' end. (* Let's do the semantics a bit differently this time, falling back on classic @@ -91,3 +91,1078 @@ Definition trsys_of (h : heap) {result} (c : cmd result) := {| Initial := {(h, c)}; Step := step (A := result) |}. + + +(* CODE TO BE MOVED TO A LIBRARY MODULE SOON *) +Module Type SEP. + Parameter hprop : Type. + Parameter lift : Prop -> hprop. + Parameter star : hprop -> hprop -> hprop. + Parameter exis : forall A, (A -> hprop) -> hprop. + + Notation "[| P |]" := (lift P). + Infix "*" := star. + Notation "'exists' x .. y , p" := (exis (fun x => .. (exis (fun y => p)) ..)). + + Parameters himp heq : hprop -> hprop -> Prop. + + Infix "===" := heq (no associativity, at level 70). + Infix "===>" := himp (no associativity, at level 70). + + Axiom himp_heq : forall p q, p === q + <-> (p ===> q /\ q ===> p). + Axiom himp_refl : forall p, p ===> p. + Axiom himp_trans : forall p q r, p ===> q -> q ===> r -> p ===> r. + + Axiom lift_left : forall p (Q : Prop) r, + (Q -> p ===> r) + -> p * [| Q |] ===> r. + Axiom lift_right : forall p q (R : Prop), + R + -> p ===> q + -> p ===> q * [| R |]. + Axiom extra_lift : forall (P : Prop) p, + P + -> p === [| P |] * p. + + Axiom star_comm : forall p q, p * q === q * p. + Axiom star_assoc : forall p q r, p * (q * r) === (p * q) * r. + Axiom star_cancel : forall p1 p2 q1 q2, p1 ===> p2 + -> q1 ===> q2 + -> p1 * q1 ===> p2 * q2. + + Axiom exis_gulp : forall A p (q : A -> _), + p * exis q === exis (fun x => p * q x). + Axiom exis_left : forall A (p : A -> _) q, + (forall x, p x ===> q) + -> exis p ===> q. + Axiom exis_right : forall A p (q : A -> _) x, + p ===> q x + -> p ===> exis q. +End SEP. + +Module Sep(Import S : SEP). + Add Parametric Relation : hprop himp + reflexivity proved by himp_refl + transitivity proved by himp_trans + as himp_rel. + + Lemma heq_refl : forall p, p === p. + Proof. + intros; apply himp_heq; intuition (apply himp_refl). + Qed. + + Lemma heq_sym : forall p q, p === q -> q === p. + Proof. + intros; apply himp_heq; apply himp_heq in H; intuition. + Qed. + + Lemma heq_trans : forall p q r, p === q -> q === r -> p === r. + Proof. + intros; apply himp_heq; apply himp_heq in H; apply himp_heq in H0; + intuition (eauto using himp_trans). + Qed. + + Add Parametric Relation : hprop heq + reflexivity proved by heq_refl + symmetry proved by heq_sym + transitivity proved by heq_trans + as heq_rel. + + Instance himp_heq_mor : Proper (heq ==> heq ==> iff) himp. + Proof. + hnf; intros; hnf; intros. + apply himp_heq in H; apply himp_heq in H0. + intuition eauto using himp_trans. + Qed. + + Add Parametric Morphism : star + with signature heq ==> heq ==> heq + as star_mor. + Proof. + intros; apply himp_heq; apply himp_heq in H; apply himp_heq in H0; + intuition (auto using star_cancel). + Qed. + + Add Parametric Morphism : star + with signature himp ==> himp ==> himp + as star_mor'. + Proof. + auto using star_cancel. + Qed. + + Instance exis_iff_morphism (A : Type) : + Proper (pointwise_relation A heq ==> heq) (@exis A). + Proof. + hnf; intros; apply himp_heq; intuition. + hnf in H. + apply exis_left; intro. + eapply exis_right. + assert (x x0 === y x0) by eauto. + apply himp_heq in H0; intuition eauto. + hnf in H. + apply exis_left; intro. + eapply exis_right. + assert (x x0 === y x0) by eauto. + apply himp_heq in H0; intuition eauto. + Qed. + + Lemma star_comm_lift : forall P q, [| P |] * q === q * [| P |]. + Proof. + intros; apply star_comm. + Qed. + + Lemma star_assoc_lift : forall p Q r, + (p * [| Q |]) * r === p * r * [| Q |]. + Proof. + intros. + rewrite <- star_assoc. + rewrite (star_comm [| Q |]). + apply star_assoc. + Qed. + + Lemma star_comm_exis : forall A (p : A -> _) q, exis p * q === q * exis p. + Proof. + intros; apply star_comm. + Qed. + + Ltac lift := + intros; apply himp_heq; split; + repeat (apply lift_left; intro); + repeat (apply lift_right; intuition). + + Lemma lift_combine : forall p Q R, + p * [| Q |] * [| R |] === p * [| Q /\ R |]. + Proof. + intros; apply himp_heq; split; + repeat (apply lift_left; intro); + repeat (apply lift_right; intuition). + Qed. + + Lemma lift1_left : forall (P : Prop) q, + (P -> [| True |] ===> q) + -> [| P |] ===> q. + Proof. + intros. + rewrite (@extra_lift True [| P |]); auto. + apply lift_left; auto. + Qed. + + Lemma lift1_right : forall p (Q : Prop), + Q + -> p ===> [| True |] + -> p ===> [| Q |]. + Proof. + intros. + rewrite (@extra_lift True [| Q |]); auto. + apply lift_right; auto. + Qed. + + Ltac normalize0 := + setoid_rewrite exis_gulp + || setoid_rewrite lift_combine + || setoid_rewrite star_assoc + || setoid_rewrite star_comm_lift + || setoid_rewrite star_assoc_lift + || setoid_rewrite star_comm_exis. + + Ltac normalizeL := + (apply exis_left || apply lift_left; intro; try congruence) + || match goal with + | [ |- [?P] ===> _ ] => + match P with + | True => fail 1 + | _ => apply lift1_left; intro; try congruence + end + end. + + Ltac normalizeR := + eapply exis_right || apply lift_right + || match goal with + | [ |- _ ===> [?Q] ] => + match Q with + | True => fail 1 + | _ => apply lift1_right + end + end. + + Ltac normalize1 := normalize0 || normalizeL || normalizeR. + + Lemma lift_uncombine : forall p P Q, + p * [| P /\ Q |] === p * [| P |] * [| Q |]. + Proof. + lift. + Qed. + + Ltac normalize2 := setoid_rewrite lift_uncombine + || setoid_rewrite star_assoc. + + Ltac normalizeLeft := + let s := fresh "s" in intro s; + let rhs := fresh "rhs" in + match goal with + | [ |- _ ===> ?Q ] => set (rhs := Q) + end; + simpl; intros; repeat (normalize0 || normalizeL); + repeat match goal with + | [ H : ex _ |- _ ===> _ ] => destruct H + | [ H : _ /\ _ |- _ ] => destruct H + | [ H : _ = _ |- _ ] => rewrite H + end; subst; subst rhs. + + Ltac normalize := + simpl; intros; repeat normalize1; repeat normalize2; + repeat (match goal with + | [ H : ex _ |- _ ===> _ ] => destruct H + end; intuition subst); subst. + + Ltac forAllAtoms p k := + match p with + | ?q * ?r => (forAllAtoms q k || forAllAtoms r k) || fail 2 + | _ => k p + end. + + Lemma stb1 : forall p q r, + (q * p) * r === q * r * p. + Proof. + intros; rewrite <- star_assoc; rewrite (star_comm p r); apply star_assoc. + Qed. + + Ltac sendToBack part := + repeat match goal with + | [ |- context[(?p * part) * ?q] ] => setoid_rewrite (stb1 part p q) + | [ |- context[part * ?p] ] => setoid_rewrite (star_comm part p) + end. + + Theorem star_cancel' : forall p1 p2 q, p1 ===> p2 + -> p1 * q ===> p2 * q. + Proof. + intros; apply star_cancel; auto using himp_refl. + Qed. + + Ltac cancel1 := + match goal with + | _ => apply himp_refl + | _ => apply star_cancel' + | [ |- ?p ===> ?q ] => + forAllAtoms p ltac:(fun p0 => + sendToBack p0; + forAllAtoms q ltac:(fun q0 => + sendToBack q0; + apply star_cancel')) + | _ => progress autorewrite with core + end. + + Ltac cancel := normalize; repeat cancel1; + try match goal with + | [ |- _ ===> _ ] => intuition (try congruence) + end. +End Sep. + + +(* Now we instantiate the generic signature of separation-logic assertions and + * connectives. *) +Module Import S <: SEP. + Definition hprop := heap -> Prop. + + (* 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 *) + Definition lift (P : Prop) : hprop := + fun h => P /\ h = $0. + + (* Separating conjunction, one of the two big ideas of separation logic *) + 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. + Delimit Scope sep_scope with sep. + Notation "p === q" := (heq p%sep q%sep) (no associativity, at level 70). + Notation "p ===> q" := (himp p%sep q%sep) (no associativity, at level 70). + + Local Open Scope sep_scope. + + (* And now we prove some key algebraic properties. I'll skip explaining the + * details. *) + + 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). + Proof. + firstorder. + Qed. + + Local Ltac t := (unfold himp, heq, lift, star, exis; propositional; subst); + repeat (match goal with + | [ H : forall x, _ <-> _ |- _ ] => + apply iff_two in H + | [ H : ex _ |- _ ] => destruct H + | [ H : split _ _ $0 |- _ ] => apply split_empty_fwd in H + end; propositional; subst); eauto 15. + + Theorem himp_heq : forall p q, p === q + <-> (p ===> q /\ q ===> p). + Proof. + t. + Qed. + + Theorem himp_refl : forall p, p ===> p. + Proof. + t. + Qed. + + Theorem himp_trans : forall p q r, p ===> q -> q ===> r -> p ===> r. + Proof. + t. + Qed. + + Theorem lift_left : forall p (Q : Prop) r, + (Q -> p ===> r) + -> p * [| Q |] ===> r. + Proof. + t. + Qed. + + Theorem lift_right : forall p q (R : Prop), + R + -> p ===> q + -> p ===> q * [| R |]. + Proof. + t. + Qed. + + Hint Resolve split_empty_bwd'. + + Theorem extra_lift : forall (P : Prop) p, + P + -> p === [| P |] * p. + Proof. + t. + apply split_empty_fwd' in H1; subst; auto. + Qed. + + Theorem star_comm : forall p q, p * q === q * p. + Proof. + t. + Qed. + + Theorem star_assoc : forall p q r, p * (q * r) === (p * q) * r. + Proof. + t. + Qed. + + Theorem star_cancel : forall p1 p2 q1 q2, p1 ===> p2 + -> q1 ===> q2 + -> p1 * q1 ===> p2 * q2. + Proof. + t. + Qed. + + Theorem exis_gulp : forall A p (q : A -> _), + p * exis q === exis (fun x => p * q x). + Proof. + t. + Qed. + + Theorem exis_left : forall A (p : A -> _) q, + (forall x, p x ===> q) + -> exis p ===> q. + Proof. + t. + Qed. + + Theorem exis_right : forall A p (q : A -> _) x, + p ===> q x + -> p ===> exis q. + Proof. + t. + Qed. + + Theorem emp_heap : forall h, lift True h -> h = $0. + Proof. + t. + Qed. +End S. + +Export S. +(* Instantiate our big automation engine to these definitions. *) +Module Import Se := Sep(S). +Export Se. + + +(* ** Some extra predicates outside the set that the engine knows about *) + +(* Capturing single-mapping heaps *) +Definition heap1 (a v : nat) : heap := $0 $+ (a, v). +Definition ptsto (a v : nat) : hprop := + fun h => h = heap1 a v. + +(* Helpful notations, some the same as above *) +Notation "[| P |]" := (lift P) : sep_scope. +Notation emp := (lift True). +Infix "*" := star : sep_scope. +Notation "'exists' x .. y , p" := (exis (fun x => .. (exis (fun y => p)) ..)) : sep_scope. +Delimit Scope sep_scope with sep. +Notation "p === q" := (heq p%sep q%sep) (no associativity, at level 70). +Notation "p ===> q" := (himp p%sep q%sep) (no associativity, at level 70). +Infix "|->" := ptsto (at level 30) : sep_scope. + +Fixpoint multi_ptsto (a : nat) (vs : list nat) : 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. + +Fixpoint zeroes (n : nat) : list nat := + match n with + | O => nil + | S n' => zeroes n' ++ 0 :: nil + end. + + +(** * Finally, the Hoare logic *) + +Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop := +(* First, four basic rules that look exactly the same as before *) +| HtReturn : forall P {result : Set} (v : result), + hoare_triple P (Return v) (fun r h => P h /\ r = v) +| HtBind : forall P {result' result} (c1 : cmd result') (c2 : result' -> cmd result) Q R, + hoare_triple P c1 Q + -> (forall r, hoare_triple (Q r) (c2 r) R) + -> hoare_triple P (Bind c1 c2) R +| HtLoop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) I, + (forall acc, hoare_triple (I (Again acc)) (body acc) I) + -> hoare_triple (I (Again init)) (Loop init body) (fun r h => I (Done r) h) +| HtFail : forall {result}, + hoare_triple (fun _ => False) (Fail (result := result)) (fun _ _ => False) + +| HtRead : forall a v, + hoare_triple (a |-> v)%sep (Read a) (fun r => a |-> v * [| r = v |])%sep +| HtWrite : forall a v', + hoare_triple (exists v, a |-> v)%sep (Write a v') (fun _ => a |-> v')%sep +| HtAlloc : forall numWords, + hoare_triple emp%sep (Alloc numWords) (fun r => r |--> zeroes numWords)%sep +| HtFree : forall a numWords, + hoare_triple (exists vs, a |--> vs * [| length vs = numWords |])%sep (Free a numWords) (fun _ => emp)%sep + +| HtConsequence : forall {result} (c : cmd result) P Q (P' : assertion) (Q' : _ -> assertion), + hoare_triple P c Q + -> P' ===> P + -> (forall r, Q r ===> Q' r) + -> hoare_triple P' c Q' +| 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 "{{ 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' : _ -> assertion), + hoare_triple P c Q + -> (forall r h, Q r h -> Q' r h) + -> hoare_triple P c Q'. +Proof. + simplify. + eapply HtConsequence; eauto. + reflexivity. +Qed. + +Lemma HtWeaken : forall {result} (c : cmd result) P Q (P' : assertion), + hoare_triple P c Q + -> (forall h, P' h -> P h) + -> hoare_triple P' c Q. +Proof. + simplify. + eapply HtConsequence; eauto. + 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. +Proof. + induct 1; propositional; eauto. + + unfold himp in *; eauto. + + unfold star, himp in *; simp; eauto 7. +Qed. + +Lemma invert_Bind : forall {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, + hoare_triple P (Bind c1 c2) Q + -> exists R, hoare_triple P c1 R + /\ forall r, hoare_triple (R r) (c2 r) Q. +Proof. + induct 1; propositional; eauto. + + invert IHhoare_triple; propositional. + eexists; propositional. + eapply HtWeaken. + eassumption. + auto. + eapply HtStrengthen. + apply H4. + auto. + + simp. + exists (fun r => x r * R)%sep. + propositional. + eapply HtFrame; eauto. + eapply HtFrame; eauto. +Qed. + +Hint Constructors hoare_triple. + +Lemma invert_Loop : forall {acc : Set} (init : acc) (body : acc -> cmd (loop_outcome acc)) P Q, + hoare_triple P (Loop init body) Q + -> exists I, (forall acc, hoare_triple (I (Again acc)) (body acc) I) + /\ (forall h, P h -> I (Again init) h) + /\ (forall r h, I (Done r) h -> Q r h). +Proof. + induct 1; propositional; eauto. + + invert IHhoare_triple; propositional. + exists x; propositional; eauto. + unfold himp in *; eauto. + + 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_nat : unit = nat -> False. +Proof. + simplify. + assert (exists x : unit, forall y : unit, x = y). + exists tt; simplify. + cases y; reflexivity. + rewrite H in H0. + invert H0. + specialize (H1 (S x)). + linear_arithmetic. +Qed. + +Lemma invert_Read : forall a P Q, + hoare_triple P (Read a) Q + -> exists v R, (P ===> a |-> v * R)%sep + /\ a |-> v * R ===> Q v. +Proof. + induct 1; simp; eauto. + + exists v, emp; simp. + cancel; auto. + cancel; auto. + + apply unit_not_nat in x0; simp. + + apply unit_not_nat in x0; simp. + + eauto 7 using himp_trans. + + exists x, (x0 * R)%sep; simp. + cancel. + + 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_nat in x0; simp. + + exists emp; simp. + cancel; auto. + cancel; auto. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + eauto 7 using himp_trans. + + exists (x * R)%sep; simp. + rewrite H1. + cancel. + + cancel. +Qed. + +Lemma invert_Alloc : forall numWords P Q, + hoare_triple P (Alloc numWords) Q + -> forall r, P * r |--> zeroes numWords ===> Q r. +Proof. + induct 1; simp; eauto. + + apply unit_not_nat in x0; simp. + + cancel. + + apply unit_not_nat in x0; simp. + + rewrite H0. + eauto using himp_trans. + + rewrite <- IHhoare_triple. + cancel. +Qed. + +(* Temporarily transparent again! *) +Transparent heq himp lift star exis ptsto. + +Lemma zeroes_initialize' : forall h a v, + h $? a = None + -> (fun h' : heap => h' = h $+ (a, v)) ===> (fun h' => h' = h) * a |-> v. +Proof. + unfold himp, star, split, ptsto, disjoint; simp. + exists h, (heap1 a v). + propositional. + maps_equal. + unfold heap1. + rewrite lookup_join2. + simp. + simp. + apply lookup_None_dom in H. + propositional. + cases (h $? k). + rewrite lookup_join1; auto. + eauto using lookup_Some_dom. + rewrite lookup_join2; auto. + unfold heap1; simp. + eauto using lookup_None_dom. + unfold heap1 in *. + cases (a ==n a0); simp. +Qed. + +(* Opaque again! *) +Opaque heq himp lift star exis ptsto. + +Lemma multi_ptsto_app : forall ls2 ls1 a, + a |--> ls1 * (a + length ls1) |--> ls2 ===> a |--> (ls1 ++ ls2). +Proof. + induct ls1; simp; cancel; auto. + + replace (a + 0) with a by linear_arithmetic. + cancel. + + rewrite <- IHls1. + cancel. + replace (a0 + 1 + length ls1) with (a0 + S (length ls1)) by linear_arithmetic. + cancel. +Qed. + +Lemma length_zeroes : forall n, + length (zeroes n) = n. +Proof. + induct n; simplify; auto. + rewrite app_length; simplify. + linear_arithmetic. +Qed. + +Lemma initialize_fresh : forall a' h a numWords, + a' >= a + numWords + -> initialize h a numWords $? a' = h $? a'. +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. +Proof. + induct numWords; simp. + + cancel; auto. + rewrite <- multi_ptsto_app. + rewrite zeroes_initialize'. + erewrite IHnumWords. + simp. + rewrite length_zeroes. + cancel; auto. + auto. + rewrite initialize_fresh; auto. +Qed. + +Lemma invert_Free : forall a numWords P Q, + hoare_triple P (Free a numWords) Q + -> P ===> (exists vs, a |--> vs * [| length vs = numWords |]) * Q tt. +Proof. + induct 1; simp; eauto. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + symmetry in x0. + apply unit_not_nat in x0; simp. + + cancel; auto. + + rewrite H0. + rewrite IHhoare_triple. + cancel; auto. + + rewrite IHhoare_triple. + cancel; auto. +Qed. + +Lemma grab_last' : forall n2 n1 a, + (exists vs, a |--> vs * [|length vs = n1 + n2|]) + ===> (exists vs, a |--> vs * [| length vs = n1 |]) + * (exists vs, (a + n1) |--> vs * [| length vs = n2 |]). +Proof. + induct n1; simp. + + cancel. + instantiate (1 := nil); simp. + replace (a + 0) with a by linear_arithmetic. + cancel; auto. + + apply himp_trans with ((exists v, a |-> v) + * (exists vs : list nat, + (a+1) |--> vs * [|length vs = n1 + n2|]))%sep. + cancel. + instantiate (1 := tl x). + cases x; simp. + instantiate (1 := hd 0 x). + cases x; simp. + cancel. + + rewrite IHn1. + clear IHn1. + replace (a + S n1) with (a + 1 + n1) by linear_arithmetic. + cancel. + instantiate (1 := x1 :: x0); simp. + cancel. +Qed. + +Lemma grab_last : forall n a, + (exists vs, a |--> vs * [|length vs = S n|]) + ===> (exists vs, a |--> vs * [|length vs = n|]) + * (exists v, (a + n) |-> v). +Proof. + simplify. + replace (S n) with (n + 1) by linear_arithmetic. + rewrite grab_last'. + cancel; auto. + instantiate (1 := hd 0 x). + cases x; simp. + cases x; simp. + cancel. +Qed. + +(* Temporarily transparent again! *) +Transparent heq himp lift star exis ptsto. + +Lemma do_deallocate' : forall a Q h, + ((exists v, a |-> v) * Q)%sep h + -> Q (h $- a). +Proof. + unfold ptsto, star, split, heap1; simp. + invert H1. + replace ($0 $+ (a, x1) $++ x0 $- a) with x0; auto. + maps_equal. + cases (k ==n a); simp. + specialize (H a). + simp. + cases (x0 $? a); auto. + exfalso; apply H; equality. + rewrite lookup_join2; auto. + apply lookup_None_dom. + simp. +Qed. + +Lemma do_deallocate : forall Q a numWords h, + ((exists vs, a |--> vs * [|length vs = numWords|]) * Q)%sep h + -> Q (deallocate h a numWords). +Proof. + induct numWords; simp. + + unfold star, exis, lift in H; simp. + cases x1; simp. + unfold emp in *; simp. + replace h with x0. + equality. + apply split_empty_fwd in H1; simp. + apply split_empty_fwd' in H0; equality. + + apply IHnumWords. + clear IHnumWords. + Opaque heq himp lift star exis ptsto. + assert ((exists vs : list nat, + a |--> vs * [|Datatypes.length vs = S numWords|]) * Q + ===> (exists vs, a |--> vs * [|length vs = numWords|]) + * (exists v, (a + numWords) |-> v) * Q) by (rewrite grab_last; cancel; auto). + apply H0 in H; clear H0. + assert ((exists vs, a |--> vs * [|length vs = numWords|]) + * (exists v : nat, (a + numWords) |-> v) * Q + ===> (exists v : nat, (a + numWords) |-> v) * + ((exists vs, a |--> vs * [|length vs = numWords|]) * Q)) by (cancel; auto). + apply H0 in H; clear H0. + apply do_deallocate'. + assumption. +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. +Proof. + induct 1; simplify. + + apply invert_Bind in H0; simp. + eauto. + + apply invert_Bind in H; simp. + specialize (invert_Return H); eauto using HtWeaken. + + apply invert_Loop in H; simp. + econstructor. + eapply HtWeaken. + eauto. + assumption. + simp. + cases r. + eapply HtStrengthen. + eauto. + simp; eauto. + eapply HtStrengthen. + eauto. + simp; eauto. + + apply invert_Read in H0; simp. + eapply HtStrengthen. + econstructor. + simp. + assert ((a |-> x * x0)%sep h') by auto. + unfold star in H0; simp. + unfold ptsto in H4; subst. + unfold split in H3; subst. + unfold heap1 in H. + rewrite lookup_join1 in H by (simp; sets). + 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. + eapply HtStrengthen. + econstructor. + 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). + 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. + + apply invert_Alloc with (r := a) in H0. + eapply HtStrengthen. + econstructor. + simp. + eapply himp_trans in H0; try apply zeroes_initialize. + auto. + assumption. + + apply invert_Free in H. + assert (((exists vs : list nat, a |--> vs * [|Datatypes.length vs = numWords|]) * Q tt)%sep h) by auto. + eapply HtStrengthen. + econstructor. + 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 + numWords ==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. + + exists (max bound (a + numWords)); simp. + rewrite initialize_fresh; auto. + + exists bound; simp. + eauto using deallocate_None. +Qed. + +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')). +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. + + right; exists h, (Return v). + constructor. + unfold split, ptsto, heap1 in *; simp. + 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 emp 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. +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 => + (exists bound, forall a, a >= bound -> fst p $? a = None) + /\ hoare_triple (fun h' => h' = fst p) + (snd p) + Q). +Proof. + simplify. + + apply invariant_induction; simplify. + + propositional; subst; simplify. + exists 0; simp. + eapply HtWeaken; eauto. + unfold himp; simplify; equality. + + cases s. + cases s'. + 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')). +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. diff --git a/_CoqProject b/_CoqProject index 53b5c7a..8424197 100644 --- a/_CoqProject +++ b/_CoqProject @@ -24,3 +24,4 @@ LambdaCalculusAndTypeSoundness.v TypesAndMutation.v DeepAndShallowEmbeddings_template.v DeepAndShallowEmbeddings.v +SeparationLogic.v