Commit 5b588f83 authored by Robbert Krebbers's avatar Robbert Krebbers

WIP

parent 0337bba4
......@@ -38,23 +38,18 @@ Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
Definition a_seq : val := λ: <>,
a_atomic_env (λ: "env", mset_clear "env").
Definition a_sequence : val := λ: "e1" "e2",
("e1" #());;; a_seq #();;;("e2" #()).
Definition a_seq_bind : val := λ: "e1" "e2",
a_bind (λ: "x", a_seq #();;; "e2" "x") "e1".
Notation "a ;;;; b"
:= (a_sequence (λ: <>, a) (λ: <>, b))%E (at level 80, right associativity).
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".
Definition a_while: val := λ: "cond" "body",
let: "rwhile" :=
rec: "while" "cnd" "bdy" :=
λ: "env" "l",
(a_if "cnd"
(a_sequence "bdy" ("while" "cnd" "bdy"))
(a_ret #())) "env" "l"
in "rwhile" "cond" "body".
Definition a_while: val :=
rec: "while" "cnd" "bdy" :=
a_if "cnd" ("bdy" ;;;; "while" "cnd" "bdy") (a_ret #()).
Section proofs.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
......@@ -91,15 +86,26 @@ Section proofs.
{ rewrite -big_sepM_insert_override; eauto. }
Qed.
Lemma a_sequence_spec R (e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} Φ :
awp e1 R (λ _, U (awp e2 R Φ)) -
awp (e1 ;;;; e2) R Φ.
Lemma a_fill R Ψ Φ K e :
awp e R Ψ -
( v : val, awp v R Ψ - awp (fill K (of_val v)) R Φ) -
awp (fill K e) R Φ.
Proof.
iIntros "HΦ". do 2 awp_lam. iApply awp_bind.
awp_lam.
iApply (awp_wand with "[HΦ]"); first done.
iIntros (v) "H". awp_lam. iApply awp_bind. iApply a_seq_spec.
iUnlock. by do 2 awp_lam.
iIntros "Hwp H". iApply wp_bind. iApply (wp_wand with "Hwp").
iIntros (v) "Hwp". iApply "H". iApply wp_value'. done.
Qed.
Lemma a_sequence_spec R Φ (e1 e2 : expr) :
AsVal e2
awp e1 R (λ v, U (awp (e2 v) R Φ)) -
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").
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) Φ :
......@@ -166,21 +172,27 @@ Section proofs.
- by iApply "HΦ".
Qed.
Lemma a_store_spec R (l : loc) (v : val) (we : expr) (w : val) Φ :
IntoVal we w
l U v -
(l L w - Φ w) -
awp (a_store (a_ret (#l)%E) (a_ret we)) R Φ.
Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
awp e1 R (λ v, l : loc, v = #l Ψ1 l)-
awp e2 R Ψ2 -
( (l : loc) w,
Ψ1 l - Ψ2 w - ( v, l U v (l L w - Φ w))) -
awp (a_store e1 e2) R Φ.
Proof.
intros <-%of_to_val. unfold a_store.
iIntros "Hv HΦ".
rewrite /a_ret. do 4 awp_lam.
iApply awp_bind.
iApply (awp_par (fun v => v = #l) (fun v => v = w))%I.
{ by iApply awp_value. }
{ by iApply awp_value. }
iNext. iIntros (? ?) "% %"; simplify_eq/=. iNext.
awp_let.
iIntros "H1 H2 HΦ".
iApply (a_fill _ _ _ [AppRCtx a_store; AppLCtx e2] with "H1").
iIntros (v) "H1 /=".
rewrite /a_store. awp_lam.
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.
iApply awp_bind. iApply (awp_par with "H1 H2"). iNext.
iIntros (w1 w2) "H1 H2".
iDestruct "H1" as (l ->) "H1".
iNext. awp_lam. clear v.
iDestruct ("HΦ" with "H1 H2") as (v) "[Hv HΦ]".
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
......
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