Commit 865b1f14 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.science.ru.nl:lgg/iris-c-monad

parents f612cffc af8c5367
......@@ -44,16 +44,16 @@ 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 Σ}.
Lemma a_seq_spec R Φ :
Lemma a_seq_spec R Φ :
U (Φ #()) -
awp (a_seq #()) R Φ.
Proof.
......@@ -98,17 +98,17 @@ Section proofs.
iModIntro. 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 "H HΦ". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iApply awp_bind.
iApply awp_value.
awp_let.
iApply (awp_wand with "H"). 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.
......@@ -130,17 +130,15 @@ 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 "H HΦ". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iApply awp_bind.
iApply (awp_wand with "H"). clear v.
iIntros (v) "HΨ". awp_lam.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
......@@ -155,11 +153,28 @@ 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 bi.big_sepM_insert; eauto. iFrame. eauto.
+ iPureIntro. by rewrite locked_locs_alloc_unlocked.
- by iApply "HΦ".
- iApply ("HΦ" with "HΨ Hl'").
Qed.
Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
awp e1 R Ψ1 - awp e2 R Ψ2 -
( v1 v2, Ψ1 v1 - Ψ2 v2 -
w, bin_op_eval op v1 v2 = Some w Φ w)-
awp (a_bin_op op e1 e2) R Φ.
Proof.
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam.
iApply awp_bind.
iApply ((awp_par Ψ1 Ψ2) with "HΨ1 HΨ2").
iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
iSpecialize ("HΦ" with "HΨ1 HΨ2").
iDestruct "HΦ" as (w0) "[% H]". by wp_pure _.
Qed.
Lemma a_store_spec R Φ Ψ1 Ψ2 e1 e2 :
......@@ -212,34 +227,44 @@ Section proofs.
- 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 "H HΦ". awp_apply (a_wp_awp with "H"); iIntros (v) "H". do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). 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.
......@@ -7,32 +7,44 @@ From iris_c.c_translation Require Import monad lifting proofmode translation.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Definition factorial_body : val := λ: "n" "c" "r",
a_while
(λ:<>, a_bin_op LeOp (a_load (a_ret "c")) (a_ret "n"))
(λ:<>, a_store (a_ret "c")
( a_bin_op PlusOp (a_load (a_ret "c")) (a_ret #1)) ;;;;
a_store (a_ret "r")
(a_bin_op MultOp (a_load (a_ret "r")) (a_load (a_ret "c"))) ;;;
a_seq #()).
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.
iModIntro.
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 := λ: <>,
......@@ -45,35 +57,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_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 :
......@@ -83,30 +94,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". iModIntro.
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". iModIntro.
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. iModIntro. 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 :
......@@ -130,7 +154,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.
......@@ -159,7 +183,7 @@ Section test.
iMod (locking_heap_change_lock _ _ ULvl LLvl with "Hσ Hl") as "[Hσ Hl]".
do 2 wp_proj. rewrite mapsto_eq /mapsto_def.
iDestruct "Hl" as "[Hv Hl]".
rewrite (big_sepM_lookup_acc _ _ l ULvl); last done.
rewrite (bi.big_sepM_lookup_acc _ _ l ULvl); last done.
iDestruct "Hls" as "[Hl' Hls]".
iDestruct "Hl'" as (?) "Hl'".
iDestruct (mapsto_agree l (1/2) (1/2) with "Hl' Hv") as %->.
......@@ -169,7 +193,7 @@ Section test.
iSpecialize ("Hls" with "[Hl']"); eauto.
wp_proj. iFrame "HR". iSplitR "Hl Hv".
- iExists ({[#l]} X),(<[l:=LLvl]> σ). iFrame. iSplitL.
+ rewrite -big_sepM_insert_override; eauto.
+ rewrite -bi.big_sepM_insert_override; eauto.
+ (* TODO: a separate lemma somewhere *)
iPureIntro. rewrite locked_locs_lock.
revert Hlocks. rewrite /correct_locks /set_Forall. set_solver.
......
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