Commit 06c3dc56 authored by Dan Frumin's avatar Dan Frumin

Adapt the specs according to a_fill

parent 4e5128c0
......@@ -45,11 +45,11 @@ Notation "e1 ;;;; e2" :=
(a_seq_bind e1 (λ: <>, e2))%E (at level 80, right associativity).
Definition a_if : val := λ: "cnd" "e1" "e2",
a_bind (λ: "c", if: "c" then "e1" else "e2") "cnd".
a_bind (λ: "c", if: "c" then "e1" #() else "e2" #()) "cnd".
Definition a_while: val :=
rec: "while" "cnd" "bdy" :=
a_if "cnd" ("bdy" ;;;; "while" "cnd" "bdy") (a_ret #()).
a_if ("cnd" #()) ("bdy" ;;;; "while" "cnd" "bdy").
Section proofs.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
......@@ -86,7 +86,7 @@ Section proofs.
{ rewrite -big_sepM_insert_override; eauto. }
Qed.
Lemma a_fill R Ψ Φ K e :
Lemma a_fill K R Ψ Φ e :
awp e R Ψ -
( v : val, awp v R Ψ - awp (fill K (of_val v)) R Φ) -
awp (fill K e) R Φ.
......@@ -101,24 +101,26 @@ Section proofs.
awp (a_seq_bind e1 e2) R Φ.
Proof.
iIntros ([v2 <-%of_to_val]) "H".
iApply (a_fill _ _ _ [AppRCtx a_seq_bind; AppLCtx v2] with "H").
iApply (a_fill [AppRCtx a_seq_bind; AppLCtx v2] with "H").
iIntros (v) "H /=". rewrite /a_seq_bind. awp_lam. awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
awp_lam. iApply awp_bind. iApply a_seq_spec.
iUnlock. by awp_lam.
Qed.
Lemma a_load_spec R (l : loc) (v : val) Φ :
l U v -
(l U v - Φ v) -
awp (a_load (a_ret #l)) R Φ.
Lemma a_load_spec R Φ Ψ e :
awp e R (λ v, l : loc, v = #l Ψ l) -
( (l : loc), Ψ l - ( v, l U v (l U v - Φ v))) -
awp (a_load e) R Φ.
Proof.
unfold a_load. iIntros "Hv HΦ".
rewrite /a_ret.
do 2 awp_lam.
iIntros "He HΦ".
iApply (a_fill [AppRCtx a_load] with "He").
iIntros (v) "Hv /=". awp_lam.
iApply awp_bind.
iApply awp_value.
awp_let.
iApply (awp_wand with "Hv"). clear v.
iIntros (v). iDestruct 1 as (l ->) "HΨ".
awp_lam.
iDestruct ("HΦ" with "HΨ") as (v) "[Hv HΦ]".
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
......@@ -140,17 +142,18 @@ Section proofs.
- by iApply "HΦ".
Qed.
Lemma a_alloc_spec R (ev : expr) (v : val) Φ :
IntoVal ev v
( l, l U v - Φ #l) -
awp (a_alloc (a_ret ev)) R Φ.
Lemma a_alloc_spec R Φ Ψ e :
awp e R Ψ -
( v l, Ψ v - l U v - Φ #l) -
awp (a_alloc e) R Φ.
Proof.
intros <-%of_to_val.
unfold a_alloc. iIntros "HΦ".
rewrite /a_ret.
do 2 awp_lam.
iApply awp_bind. iApply awp_value.
awp_let.
iIntros "He HΦ".
iApply (a_fill [AppRCtx a_alloc] with "He").
iIntros (v) "Hv /=".
awp_lam.
iApply awp_bind.
iApply (awp_wand with "Hv"). clear v.
iIntros (v) "HΨ". awp_lam.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
......@@ -165,11 +168,11 @@ Section proofs.
by iDestruct (mapsto_valid_2 l with "Hl Hl'") as %[]. }
iDestruct "Hl" as "[Hl Hl']".
iMod (locking_heap_alloc σ l ULvl v with "Hl' Hσ") as "[Hσ Hl']"; eauto.
iModIntro. iFrame "HR". iSplitR "HΦ Hl'".
iModIntro. iFrame "HR". iSplitR "HΦ HΨ Hl'".
- iExists X,(<[l:=ULvl]>σ). iFrame. iSplit.
+ rewrite big_sepM_insert; eauto. iFrame. eauto.
+ iPureIntro. by rewrite locked_locs_alloc_unlocked.
- by iApply "HΦ".
- iApply ("HΦ" with "HΨ Hl'").
Qed.
Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
......@@ -180,10 +183,10 @@ Section proofs.
awp (a_store e1 e2) R Φ.
Proof.
iIntros "H1 H2 HΦ".
iApply (a_fill _ _ _ [AppRCtx a_store; AppLCtx e2] with "H1").
iApply (a_fill [AppRCtx a_store; AppLCtx e2] with "H1").
iIntros (v) "H1 /=".
rewrite /a_store. awp_lam.
iApply (a_fill _ _ _ [AppRCtx (LamV "x2" (
iApply (a_fill [AppRCtx (LamV "x2" (
(a_bind (λ: "vv", a_atomic_env (λ: "env", (mset_add (Fst "vv")) "env";; Fst "vv" <- Snd "vv";; Snd "vv")))
((a_par v) "x2")
)%E)] with "H2"). simpl. iIntros (v2) "H2". awp_lam.
......@@ -229,35 +232,49 @@ iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]".
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
- iApply "HΦ". iFrame.
Qed.
Lemma a_if_true_spec R (e1 e2 : val) Φ :
awp e1 R Φ - awp (a_if (a_ret #true) e1 e2) R Φ.
Lemma a_if_spec R Φ Ψ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
awp e R Ψ -
( v, Ψ v - (v = #true awp e1 R Φ) (v = #false awp e2 R Φ)) -
awp (a_if e (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ".
do 4 awp_lam.
iApply awp_bind.
iApply awp_value.
awp_lam. by awp_if_true.
iIntros "He HΦ".
iApply (a_fill [AppRCtx a_if; AppLCtx (λ: <>, e1); AppLCtx (λ: <>, e2)] with "He").
iIntros (v) "Hv /=".
do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "Hv"). clear v.
iIntros (v) "HΨ". awp_lam.
iDestruct ("HΦ" with "HΨ") as "[[% H] | [% H]]"; simplify_eq/=;
by do 2 (awp_pure _).
Qed.
Lemma a_if_false_spec R (e1 e2 : val) Φ :
awp e2 R Φ - awp (a_if (a_ret #false) e1 e2) R Φ.
Lemma a_if_true_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
awp e1 R Φ - awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ".
do 4 awp_lam.
iApply awp_bind.
iApply awp_value.
awp_lam. by awp_if_false.
iApply (a_if_spec _ _ (λ v, v = #true)%I).
{ iApply awp_ret. iApply wp_value. eauto. }
iIntros (? ->). iLeft. eauto.
Qed.
Lemma a_if_spec R (e e1 e2 : val) Φ:
awp e R (λ cnd, (cnd = #true awp e1 R Φ) (cnd = #false awp e2 R Φ)) -
awp (a_if e e1 e2) R Φ.
Lemma a_if_false_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
awp e2 R Φ - awp (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ". do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "HΦ").
iIntros (v) "[[% H] | [% H]]"; subst; by repeat awp_pure _.
iIntros "HΦ".
iApply (a_if_spec _ _ (λ v, v = #false)%I).
{ iApply awp_ret. iApply wp_value. eauto. }
iIntros (? ->). iRight. eauto.
Qed.
Lemma a_while_spec (cnd bdy : val) R Φ :
awp (a_if (cnd #()) (bdy ;;;; (a_while cnd bdy))) R Φ -
awp (a_while cnd bdy) R Φ.
Proof.
iIntros "HAWP".
rewrite {2}/a_while.
awp_lam. awp_lam.
rewrite /a_while.
iApply "HAWP".
Qed.
End proofs.
......@@ -11,30 +11,32 @@ Section test.
Lemma test1 (l : loc) :
l L #1 -
awp (a_seq #();;; a_load (a_ret #l))%E True (fun v => v = #1).
awp (a_seq #();;; a_load (a_ret #l))%E True (fun v => v = #1 l U #1).
Proof.
iIntros "Hl".
iApply awp_bind.
iApply a_seq_spec.
iUnlock.
awp_lam.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
iApply (a_load_spec _ _ (λ v, v = l)%I).
{ iApply awp_ret. iApply wp_value; eauto. }
iIntros (? ->). iExists #1. iFrame. eauto.
Qed.
Lemma test2 (l r : loc) R :
l U #3 - r L #0 -
awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l)) R (fun v => v = #1).
Proof.
iIntros "Hl Hr".
iApply awp_bind.
iApply (a_store_spec with "Hl"). iIntros "Hl".
awp_lam.
iApply awp_bind.
iApply a_seq_spec.
iUnlock.
awp_lam.
iApply (a_load_spec with "Hl"). iIntros "Hl". eauto.
Qed.
(* Lemma test2 (l r : loc) R : *)
(* l ↦U #3 -∗ r ↦L #0 -∗ *)
(* awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l)) R (fun v => ⌜v = #1⌝). *)
(* Proof. *)
(* iIntros "Hl Hr". *)
(* iApply awp_bind. *)
(* iApply (a_store_spec with "Hl"). iIntros "Hl". *)
(* awp_lam. *)
(* iApply awp_bind. *)
(* iApply a_seq_spec. *)
(* iUnlock. *)
(* awp_lam. *)
(* iApply (a_load_spec with "Hl"). iIntros "Hl". eauto. *)
(* Qed. *)
Definition swap_aform (l1 l2 : loc) : val := λ: <>,
......@@ -47,35 +49,34 @@ Section test.
a_seq #()))
(a_alloc (a_ret #0)).
Lemma swap_spec_aform (l1 l2 : loc) (v1 v2: val) R :
l1 U v1 - l2 U v2 -
awp (swap_aform l1 l2 #()) R (λ _, l1 U v2 l2 U v1).
Proof.
iIntros "Hl1 Hl2".
(* let r = ref 0 in *)
awp_lam; iApply awp_bind; iApply (a_alloc_spec R #0); iIntros (r) "Hr".
(* r <- !l1 ; *)
awp_lam; do 2 iApply awp_bind; iApply (a_load_spec with "[$Hl1]"); iIntros "Hl1".
awp_lam; iApply (a_store_spec with "Hr"); iIntros "Hr"; awp_seq.
iApply awp_bind. iApply a_seq_spec; iUnlock.
(* l1 <- !l2 ; *)
awp_lam; do 2 iApply awp_bind; iApply (a_load_spec with "[$Hl2]"); iIntros "Hl2".
awp_lam; iApply (a_store_spec with "Hl1"); iIntros "Hl1"; awp_seq.
iApply awp_bind. iApply a_seq_spec. iUnlock.
(* l2 <- !r ; *)
awp_lam. do 2 iApply awp_bind. iApply (a_load_spec with "[$Hr]"); iIntros "Hr".
awp_lam; iApply (a_store_spec with "Hl2"); iIntros "Hl2"; awp_seq.
iApply a_seq_spec; iUnlock.
(* Post-condition*)
by iFrame.
Qed.
(* Lemma swap_spec_aform (l1 l2 : loc) (v1 v2: val) R : *)
(* l1 ↦U v1 -∗ l2 ↦U v2 -∗ *)
(* awp (swap_aform l1 l2 #()) R (λ _, l1 ↦U v2 ∗ l2 ↦U v1). *)
(* Proof. *)
(* iIntros "Hl1 Hl2". *)
(* (* let r = ref 0 in *) *)
(* awp_lam; iApply awp_bind; iApply (a_alloc_spec R #0); iIntros (r) "Hr". *)
(* (* r <- !l1 ; *) *)
(* awp_lam; do 2 iApply awp_bind; iApply (a_load_spec with "[$Hl1]"); iIntros "Hl1". *)
(* awp_lam; iApply (a_store_spec with "Hr"); iIntros "Hr"; awp_seq. *)
(* iApply awp_bind. iApply a_seq_spec; iUnlock. *)
(* (* l1 <- !l2 ; *) *)
(* awp_lam; do 2 iApply awp_bind; iApply (a_load_spec with "[$Hl2]"); iIntros "Hl2". *)
(* awp_lam; iApply (a_store_spec with "Hl1"); iIntros "Hl1"; awp_seq. *)
(* iApply awp_bind. iApply a_seq_spec. iUnlock. *)
(* (* l2 <- !r ; *) *)
(* awp_lam. do 2 iApply awp_bind. iApply (a_load_spec with "[$Hr]"); iIntros "Hr". *)
(* awp_lam; iApply (a_store_spec with "Hl2"); iIntros "Hl2"; awp_seq. *)
(* iApply a_seq_spec; iUnlock. *)
(* (* Post-condition*) *)
(* by iFrame. *)
(* Qed. *)
Definition swap : val := λ: "l1" "l2",
a_bind (λ: "r",
((a_bind (λ: "v", (a_store (a_ret "r")) (a_ret "v"))) (a_load (a_ret "l1")));;;;
((a_bind (λ: "v", (a_store (a_ret "l1")) (a_ret "v"))) (a_load (a_ret "l2")));;;;
((a_bind (λ: "v", (a_store (a_ret "l2")) (a_ret "v"))) (a_load (a_ret "r")));;;
a_seq #())
a_bind (λ: "r",
(a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
(a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
((a_store (a_ret "l2") (a_load (a_ret "r")))) ;;; a_seq #())
(a_alloc (a_ret #0%V)).
Lemma swap_spec (l1 l2 : loc) (v1 v2: val) R :
......@@ -85,30 +86,43 @@ Section test.
iIntros "Hl1 Hl2".
do 2 awp_lam.
iApply awp_bind.
iApply a_alloc_spec.
iIntros (r) "Hr".
awp_lam.
iApply a_sequence_spec.
iApply awp_bind.
iApply (a_load_spec with "Hl1"). iIntros "Hl1".
awp_lam.
iApply (a_store_spec with "Hr"). iIntros "Hr".
iUnlock.
iApply (a_alloc_spec _ _ (λ v, v = #0)%I).
{ iApply awp_ret. by iApply wp_value. }
iIntros (? r ->) "Hr". awp_lam.
iApply a_sequence_spec.
iApply (a_store_spec _ _ (λ l, l = r)%I (λ v, v = v1 l1 U v1)%I with "[] [Hl1]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = l1)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
iIntros (? ? ->) "[% Hl1]"; subst.
iExists _; iFrame. iIntros "Hr". iUnlock.
awp_seq.
iApply a_sequence_spec.
iApply (a_store_spec _ _ (λ l, l = l1)%I (λ v, v = v2 l2 U v2)%I with "[] [Hl2]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = l2)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
iIntros (? ? ->) "[% Hl2]"; subst.
iExists _; iFrame. iIntros "Hl1". iUnlock.
awp_seq.
iApply awp_bind.
iApply (a_load_spec with "Hl2"). iIntros "Hl2".
awp_lam.
iApply (a_store_spec with "Hl1"). iIntros "Hl1".
iUnlock.
iApply awp_bind.
iApply awp_bind.
iApply (a_load_spec with "Hr"). iIntros "Hr".
awp_lam.
iApply (a_store_spec with "Hl2"). iIntros "Hl2".
awp_lam.
iApply a_seq_spec. iUnlock; iFrame.
iApply (a_store_spec _ _ (λ l, l = l2)%I (λ v, v = v1 r U v1)%I with "[] [Hr]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = r)%I).
- iApply awp_ret. iApply wp_value; eauto.
- iIntros (? ->). iExists _; iFrame. eauto. }
iIntros (? ? ->) "[% Hr]"; subst.
Opaque awp.
iExists _; iFrame. iIntros "Hl2".
awp_seq. iApply a_seq_spec. iUnlock. by iFrame.
Qed.
Definition incr1 : val := λ: "l",
a_store (a_ret "l") (a_bin_op PlusOp (a_load "l") (a_ret #1)).
Lemma incr1_spec (l : loc) (n : Z) R :
......@@ -132,7 +146,7 @@ Section test.
iApply awp_bind.
iApply (awp_par (λ v, v = #l) (λ v, v = #(n+1) l U #n) with "[] [Hl]")%I.
- by iApply awp_value.
- rewrite /awp.
- Transparent awp. rewrite /awp.
iApply wp_value.
iIntros (γ π env lk) "#Hlock1 Hunfl1". do 2 wp_let.
Opaque par.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment