diff --git a/opam b/opam
index 59aa3a30142c89e093de12104a2998661096e3c1..3b763e328b585b85a82c2d4183d1543466780151 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
- "coq-iris" { (= "dev.2018-10-22.3.4842a060") | (= "dev") }
+ "coq-iris" { (= "dev.2018-10-31.0.6356ef03") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/barrier/example_client.v b/theories/barrier/example_client.v
index 1b119dc5faf4716c9dc12b56639fe35d1477946a..66117e3457cd05f8ab58b6c0594df420700cf76b 100644
--- a/theories/barrier/example_client.v
+++ b/theories/barrier/example_client.v
@@ -46,7 +46,7 @@ Section client.
- (* The original thread, the sender. *)
wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
iSplitR "Hy"; first by eauto.
- iExists _; iSplitL; [done|]. iIntros "!#" (n). wp_let. by wp_op.
+ iExists _; iSplitL; [done|]. iIntros "!#" (n). by wp_pures.
- (* The two spawned threads, the waiters. *)
iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). }
diff --git a/theories/barrier/example_joining_existentials.v b/theories/barrier/example_joining_existentials.v
index 91fda79b192264bb33b445574014abe3a4209b7b..c30d462abf87f5396f8c7e3e7c41bb185977b1cc 100644
--- a/theories/barrier/example_joining_existentials.v
+++ b/theories/barrier/example_joining_existentials.v
@@ -19,9 +19,10 @@ Definition oneShotΣ (F : cFunctor) : gFunctors :=
Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ → oneShotG Σ F.
Proof. solve_inG. Qed.
-Definition client eM eW1 eW2 : expr :=
+Definition client : val :=
+ λ: "fM" "fW1" "fW2",
let: "b" := newbarrier #() in
- (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
+ ("fM" #() ;; signal "b") ||| ((wait "b" ;; "fW1" #()) ||| (wait "b" ;; "fW2" #())).
Section proof.
Local Set Default Proof Using "Type*".
@@ -32,7 +33,7 @@ Local Notation X := (F (iProp Σ)).
Definition barrier_res γ (Φ : X → iProp Σ) : iProp Σ :=
(∃ x, own γ (Shot x) ∗ Φ x)%I.
-Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) `{!Closed [] e} :
+Lemma worker_spec e γ l (Φ Ψ : X → iProp Σ) :
recv N l (barrier_res γ Φ) -∗ (∀ x, {{ Φ x }} e {{ _, Ψ x }}) -∗
WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Proof.
@@ -68,31 +69,31 @@ Proof.
iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
Qed.
-Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2} :
+Lemma client_spec_new (fM fW1 fW2 : val) :
P -∗
- {{ P }} eM {{ _, ∃ x, Φ x }} -∗
- (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -∗
- (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -∗
- WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
+ {{ P }} fM #() {{ _, ∃ x, Φ x }} -∗
+ (∀ x, {{ Φ1 x }} fW1 #() {{ _, Ψ1 x }}) -∗
+ (∀ x, {{ Φ2 x }} fW2 #() {{ _, Ψ2 x }}) -∗
+ WP client fM fW1 fW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
Proof using All.
- iIntros "/= HP #He #He1 #He2"; rewrite /client.
+ iIntros "/= HP #Hf #Hf1 #Hf2"; rewrite /client.
iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
- wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
+ wp_lam. wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
iIntros (l) "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 ∗ barrier_res γ Ψ2)%I).
- wp_let. wp_apply (wp_par (λ _, True)%I workers_post with "[HP Hs Hγ] [Hr]").
- - wp_bind eM. iApply (wp_wand with "[HP]"); [by iApply "He"|].
- iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
+ wp_apply (par_spec (λ _, True)%I workers_post with "[HP Hs Hγ] [Hr]").
+ - wp_lam. wp_bind (fM #()). iApply (wp_wand with "[HP]"); [by iApply "Hf"|].
+ iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_seq.
iMod (own_update with "Hγ") as "Hx".
{ by apply (cmra_update_exclusive (Shot x)). }
iApply (signal_spec with "[- $Hs]"); last auto.
iExists x; auto.
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iMod (recv_split with "Hr") as "[H1 H2]"; first done.
- wp_apply (wp_par (λ _, barrier_res γ Ψ1)%I
- (λ _, barrier_res γ Ψ2)%I with "[H1] [H2]").
- + iApply (worker_spec with "H1"); auto.
- + iApply (worker_spec with "H2"); auto.
+ wp_apply (par_spec (λ _, barrier_res γ Ψ1)%I
+ (λ _, barrier_res γ Ψ2)%I with "[H1] [H2]").
+ + wp_apply (worker_spec with "H1"); auto.
+ + wp_apply (worker_spec with "H2"); auto.
+ auto.
- iIntros (_ v) "[_ [H1 H2]]". iDestruct (Q_res_join with "H1 H2") as "?". auto.
Qed.
diff --git a/theories/barrier/proof.v b/theories/barrier/proof.v
index 44482dca0ccdc7de70f856a47e151aa8c45b7088..d227b4854a8892d14569f50a2da8033610913220 100644
--- a/theories/barrier/proof.v
+++ b/theories/barrier/proof.v
@@ -92,7 +92,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
{{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
Proof.
iIntros (Φ) "_ HΦ".
- rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
+ rewrite -wp_fupd /newbarrier /=. wp_lam. wp_alloc l as "Hl".
iApply ("HΦ" with "[> -]").
iMod (saved_prop_alloc P) as (γ) "#?".
iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
@@ -117,7 +117,7 @@ Lemma signal_spec l P :
{{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}.
Proof.
rewrite /signal /=.
- iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "[#Hsts Hγ]". wp_let.
+ iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "[#Hsts Hγ]". wp_lam.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
destruct p; [|done]. wp_store.
diff --git a/theories/concurrent_stacks/concurrent_stack1.v b/theories/concurrent_stacks/concurrent_stack1.v
index ffe481c550f1f6d415db732b2b4335753ee12521..d923178cd18aec9e7f27e3651cef038a16579701 100644
--- a/theories/concurrent_stacks/concurrent_stack1.v
+++ b/theories/concurrent_stacks/concurrent_stack1.v
@@ -98,7 +98,7 @@ Section stacks.
iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hisstack".
{ iExists None; iFrame; auto.
iApply is_stack_unfold. auto. }
- wp_let.
+ wp_pures.
iModIntro.
iApply "HΦ".
- iIntros "!#".
@@ -111,13 +111,13 @@ Section stacks.
destruct v' as [l'|]; simpl; last first.
+ iMod ("Hclose" with "[Hl' Hstack]") as "_".
{ rewrite /stack_inv. eauto with iFrame. }
- iModIntro. wp_match. by iRight.
+ iModIntro. wp_match. wp_pures. by iRight.
+ iDestruct (is_stack_copy with "Hstack") as "[Hstack Hmy]".
iDestruct "Hmy" as (q h t) "Hl".
iMod ("Hclose" with "[Hl' Hstack]") as "_".
{ rewrite /stack_inv. eauto with iFrame. }
iModIntro. wp_match.
- wp_load. wp_proj.
+ wp_load. wp_pures.
wp_bind (CAS _ _ _).
iInv N as "Hstack" "Hclose".
iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
@@ -131,7 +131,7 @@ Section stacks.
iModIntro.
wp_if.
wp_load.
- wp_proj.
+ wp_pures.
eauto.
* simpl in Hne. wp_cas_fail.
iMod ("Hclose" with "[Hl'' Hstack]").
@@ -151,8 +151,7 @@ Section stacks.
iModIntro.
wp_let.
wp_alloc r'' as "Hr''".
- wp_let.
- wp_bind (CAS _ _ _).
+ wp_pures. wp_bind (CAS _ _ _).
iInv N as "Hstack" "Hclose".
iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
wp_cas as ->%oloc_to_val_inj|_.
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index 0876be16db26b06fff9445c9bf282b0643423d6f..f2dba8bb7c89b8fc73b070b454cd54a4a66406da 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -113,11 +113,11 @@ Section stack_works.
Proof.
iIntros "HΦ HP".
rename ι into N.
- wp_let.
+ wp_rec.
wp_alloc l as "Hl".
iMod (inv_alloc N _ (stack_inv P #l) with "[Hl HP]") as "#Istack".
{ iNext; iExists l, (InjLV #()), []; iSplit; iFrame; auto. }
- wp_let.
+ wp_pures.
iApply "HΦ".
- iIntros "!# Hcont".
iLöb as "IH".
@@ -137,7 +137,7 @@ Section stack_works.
iMod ("Hclose" with "[Hl' Hstack HP]").
{ iExists l', (InjLV #()), []; iSplit; iFrame; auto. }
iModIntro.
- wp_match.
+ wp_pures.
iRight; auto.
* iDestruct "H" as (q l h t) "[% Hl]".
subst.
@@ -148,10 +148,9 @@ Section stack_works.
assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val.
assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto).
wp_match.
- unfold subst; simpl; fold of_val.
wp_load.
- wp_proj.
+ wp_pures.
wp_bind (CAS _ _ _).
iInv N as "Hstack" "Hclose".
iDestruct "Hstack" as (l'' v' ys) "[>% [Hl'' [Hstack HP]]]".
@@ -171,7 +170,7 @@ Section stack_works.
iModIntro.
wp_if.
wp_load.
- wp_proj.
+ wp_pures.
iLeft; iExists _; auto.
+ wp_cas_fail.
iMod ("Hclose" with "[Hl'' Hstack HP]").
@@ -192,7 +191,7 @@ Section stack_works.
iModIntro.
wp_let.
wp_alloc lp as "Hlp".
- wp_let.
+ wp_pures.
wp_bind (CAS _ _ _).
iInv N as "Hstack" "Hclose".
iDestruct "Hstack" as (l'' v'' xs) "[>% [Hl'' [Hstack HP]]]".
diff --git a/theories/hocap/cg_bag.v b/theories/hocap/cg_bag.v
index 3e280452ae307dd1ea28240b251b5ffa94db532c..69aeeccf8e2766b626e85a9e8c1d28bd3588fc47 100644
--- a/theories/hocap/cg_bag.v
+++ b/theories/hocap/cg_bag.v
@@ -108,7 +108,7 @@ Section proof.
iMod (own_alloc (1%Qp, to_agree ∅)) as (γb) "[Ha Hf]"; first done.
wp_apply (newlock_spec N (bag_inv γb r) with "[Hr Ha]").
{ iExists []. iFrame. }
- iIntros (lk γ) "#Hlk". wp_let. iApply "HΦ".
+ iIntros (lk γ) "#Hlk". wp_pures. iApply "HΦ".
rewrite /is_bag /bag_contents. iFrame.
iExists _,_,_. by iFrame "Hlk".
Qed.
@@ -123,7 +123,7 @@ Section proof.
Proof.
iIntros "#Hvs".
iIntros (Φ). iAlways. iIntros "[#Hbag HP] HΦ".
- unfold pushBag. do 2 wp_rec.
+ unfold pushBag. wp_rec. wp_let.
rewrite /is_bag /bag_inv.
iDestruct "Hbag" as (lk b γl) "[% #Hlk]"; simplify_eq/=.
repeat wp_pure _.
@@ -133,7 +133,7 @@ Section proof.
wp_bind (_ <- _)%E.
iApply (wp_mask_mono _ (⊤∖↑N)); first done.
iMod ("Hvs" with "[$Ha $HP]") as "[Hbc HQ]".
- wp_store. wp_let.
+ wp_store. wp_seq.
wp_apply (release_spec with "[$Hlk $Htok Hbc Hb]").
{ iExists (v::ls); iFrame. }
iIntros "_". by iApply "HΦ".
@@ -184,4 +184,3 @@ Canonical Structure cg_bag `{!heapG Σ, !bagG Σ} : bag Σ :=
abstract_bag.newBag_spec := newBag_spec;
abstract_bag.pushBag_spec := pushBag_spec;
abstract_bag.popBag_spec := popBag_spec |}.
-
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index e2492a15400668496e081152086cf2ae0807adf5..fbbbacd001869100fbc7533369dd16c231cecd95 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -220,28 +220,27 @@ Section contents.
{{{ γ γ' t, RET t; isTask r γ γ' t P Q ∗ task γ γ' t a P Q }}}.
Proof.
iIntros (Φ) "[#Hrunner HP] HΦ".
- unfold newTask. do 2 wp_rec. iApply wp_fupd.
+ wp_rec. wp_pures. iApply wp_fupd.
wp_alloc res as "Hres".
wp_alloc status as "Hstatus".
iMod (new_pending) as (γ) "[Htoken Htask]".
iMod (new_INIT) as (γ') "[Hinit Hinit']".
iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
{ iNext. iLeft. iFrame. }
- iModIntro. iApply "HΦ".
+ wp_pures. iModIntro. iApply "HΦ".
iFrame. iSplitL; iExists _,_,_; iFrame "Hinv"; eauto.
Qed.
- Lemma task_Join_spec γb γ γ' (te : expr) (r t a : val) P Q :
- IntoVal te t →
+ Lemma task_Join_spec γb γ γ' (r t a : val) P Q :
{{{ runner γb P Q r ∗ task γ γ' t a P Q }}}
- task_Join te
+ task_Join t
{{{ res, RET res; Q a res }}}.
Proof.
- iIntros (<- Φ) "[#Hrunner Htask] HΦ".
+ iIntros (Φ) "[#Hrunner Htask] HΦ".
iLöb as "IH".
rewrite {2}/task_Join.
iDestruct "Htask" as (r' state res) "(% & Htoken & #Htask)". simplify_eq.
- repeat wp_pure _.
+ wp_rec. wp_pures.
wp_bind (! #state)%E. iInv (N.@"task") as "Hstatus" "Hcl".
rewrite {2}/task_inv.
iDestruct "Hstatus" as "[>(Hstate & Hres)|[Hstatus|Hstatus]]".
@@ -294,7 +293,7 @@ Section contents.
iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)".
iDestruct "Htask" as (arg state res) "(% & HP & HINIT & #Htask)".
simplify_eq. rewrite /task_Run.
- repeat wp_pure _.
+ wp_rec. wp_pures.
wp_bind (body _ arg).
iDestruct ("Hbody" $! (PairV body bag) arg) as "Hbody'".
iSpecialize ("Hbody'" with "[HP]").
@@ -302,7 +301,7 @@ Section contents.
iExists _,_; iSplitR; eauto. }
iApply (wp_wand with "Hbody'").
iIntros (v) "HQ". wp_let.
- wp_bind (#res <- SOME v)%E.
+ wp_bind (#res <- SOME v)%E. wp_inj.
iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT')|[Hstatus|Hstatus]]" "Hcl".
- wp_store.
iMod (INIT_SET_RES v γ' with "[HINIT HINIT']") as "[HSETRES HSETRES']".
@@ -311,7 +310,7 @@ Section contents.
apply _. }
iMod ("Hcl" with "[HSETRES Hstate Hres Hpending]") as "_".
{ iNext. iRight. iLeft. iExists _; iFrame. }
- iModIntro. wp_let.
+ iModIntro. wp_seq.
iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT')|[Hstatus|Hstatus]]" "Hcl".
{ iExFalso. iApply (INIT_not_SET_RES with "HINIT' HSETRES'"). }
+ iDestruct "Hstatus" as (v') "(Hstate & Hres & Hpending & HSETRES)".
@@ -340,7 +339,7 @@ Section contents.
iIntros (Φ) "#Hrunner HΦ".
rewrite runner_unfold /runner_runTask.
iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)"; simplify_eq.
- repeat wp_pure _.
+ wp_rec. wp_pures.
wp_bind (popBag b _).
iApply (popBag_spec with "Hbag").
iNext. iIntros (t') "[_ [%|Ht]]"; simplify_eq.
@@ -362,15 +361,15 @@ Section contents.
iLöb as "IH". rewrite /runner_runTasks.
wp_rec. wp_bind (runner_runTask r).
iApply runner_runTask_spec; eauto.
- iNext. iIntros "_". wp_rec. by iApply "IH".
+ iNext. iIntros "_". wp_seq. by iApply "IH".
Qed.
Lemma loop_spec (n i : nat) P Q γb r:
{{{ runner γb P Q r }}}
- (rec: "loop" "i" :=
+ (RecV "loop" "i" (
if: "i" < #n
then Fork (runner_runTasks r);; "loop" ("i" + #1)
- else r) #i
+ else r)) #i
{{{ r, RET r; runner γb P Q r }}}.
Proof.
iIntros (Φ) "#Hrunner HΦ".
@@ -379,50 +378,48 @@ Section contents.
{ by iApply "HΦ". }
wp_bind (Fork _). iApply (wp_fork with "[]").
- iNext. by iApply runner_runTasks_spec.
- - iNext. wp_rec. wp_op.
+ - iNext. wp_seq. wp_op.
(* Set Printing Coercions. *)
assert ((Z.of_nat i + 1) = Z.of_nat (i + 1)) as -> by lia.
iApply ("IH" with "HΦ").
Qed.
- Lemma newRunner_spec P Q (fe ne : expr) (f : val) (n : nat) :
- IntoVal fe f → IntoVal ne (#n) →
+ Lemma newRunner_spec P Q (f : val) (n : nat) :
{{{ ∀ (γ: name Σ b) (r: val),
□ ∀ a: val, (runner γ P Q r ∗ P a -∗ WP f r a {{ v, Q a v }}) }}}
- newRunner fe ne
+ newRunner f #n
{{{ γb r, RET r; runner γb P Q r }}}.
Proof.
- iIntros (<- <- Φ) "#Hf HΦ".
+ iIntros (Φ) "#Hf HΦ".
unfold newRunner. iApply wp_fupd.
- repeat wp_pure _.
+ wp_lam. wp_pures.
wp_bind (newBag b #()).
iApply (newBag_spec b (N.@"bag") (λ x y, ∃ γ γ', isTask (f,x) γ γ' y P Q)%I); auto.
iNext. iIntros (bag). iDestruct 1 as (γb) "#Hbag".
- do 3 wp_let.
+ wp_let. wp_pair. wp_let. wp_closure. wp_let.
iAssert (runner γb P Q (PairV f bag))%I with "[]" as "#Hrunner".
{ rewrite runner_unfold. iExists _,_. iSplit; eauto. }
iApply (loop_spec n 0 with "Hrunner [HΦ]"); eauto.
iNext. iIntros (r) "Hr". by iApply "HΦ".
Qed.
- Lemma runner_Fork_spec γb (re ae:expr) (r a:val) P Q :
- IntoVal re r → IntoVal ae a →
+ Lemma runner_Fork_spec γb (r a:val) P Q :
{{{ runner γb P Q r ∗ P a }}}
- runner_Fork re ae
+ runner_Fork r a
{{{ γ γ' t, RET t; task γ γ' t a P Q }}}.
Proof.
- iIntros (<- <- Φ) "[#Hrunner HP] HΦ".
+ iIntros (Φ) "[#Hrunner HP] HΦ".
rewrite /runner_Fork runner_unfold.
iDestruct "Hrunner" as (body bag) "(% & #Hbag & #Hbody)". simplify_eq.
Local Opaque newTask.
- repeat wp_pure _. wp_bind (newTask _ _).
+ wp_lam. wp_pures. wp_bind (newTask _ _).
iApply (newTask_spec γb (body,bag) a P Q with "[Hbag Hbody HP]").
{ iFrame "HP". rewrite runner_unfold.
iExists _,_; iSplit; eauto. }
iNext. iIntros (γ γ' t) "[Htask Htask']". wp_let.
wp_bind (pushBag _ _ _).
iApply (pushBag_spec with "[$Hbag Htask]"); eauto.
- iNext. iIntros "_". wp_rec. by iApply "HΦ".
+ iNext. iIntros "_". wp_seq. by iApply "HΦ".
Qed.
End contents.
diff --git a/theories/hocap/fg_bag.v b/theories/hocap/fg_bag.v
index 5c822a8dbf6ede41682806c055cce1c1ac245fac..dd5f1d1ccebbe5990198f10cb67b578c2b17e874 100644
--- a/theories/hocap/fg_bag.v
+++ b/theories/hocap/fg_bag.v
@@ -150,18 +150,17 @@ Section proof.
iIntros "#Hvs".
iIntros (Φ). iAlways. iIntros "[#Hbag HP] HΦ".
unfold pushBag.
- iLöb as "IH". do 2 wp_rec.
+ iLöb as "IH". wp_rec. wp_pures.
rewrite /is_bag.
iDestruct "Hbag" as (b) "[% #Hinv]"; simplify_eq/=.
- repeat wp_pure _.
wp_bind (! #b)%E.
iInv N as (o ls) "[Ho [Hls >Hb]]" "Hcl".
wp_load.
iMod ("Hcl" with "[Ho Hls Hb]") as "_".
{ iNext. iExists _,_. iFrame. } clear ls.
- iModIntro. repeat wp_pure _.
+ iModIntro.
wp_alloc n as "Hn".
- wp_bind (CAS _ _ _).
+ wp_pures. wp_bind (CAS _ _ _).
iInv N as (o' ls) "[Ho [Hls >Hb]]" "Hcl".
iPoseProof (is_list_unboxed with "Hls") as "#>%".
destruct (decide (o = o')) as [->|?].
@@ -227,7 +226,7 @@ Section proof.
iMod ("Hvs1" with "[$Hb $HP]") as "[Hb HQ]".
iMod ("Hcl" with "[Ho Htl Hb]") as "_".
{ iNext. iExists _,ls. by iFrame "Ho Hb". }
- iModIntro. wp_if_true. by iApply "HΦ".
+ iModIntro. wp_pures. by iApply "HΦ".
+ wp_cas_fail.
iMod ("Hcl" with "[Ho Hls Hb]") as "_".
{ iNext. iExists _,ls'. by iFrame "Ho Hb". }
diff --git a/theories/hocap/parfib.v b/theories/hocap/parfib.v
index dd04bf8f23cd7b1f31bf940c5349446dfa3e3a7c..6eea3f2baae5a24b4a99e75edddaa2c60554b81b 100644
--- a/theories/hocap/parfib.v
+++ b/theories/hocap/parfib.v
@@ -39,7 +39,7 @@ Section contents.
{{{ True }}} seqFib #n {{{ (m : nat), RET #m; ⌜fib n = m⌠}}}.
Proof.
iIntros (Φ) "_ HΦ".
- iLöb as "IH" forall (n Φ).
+ iLöb as "IH" forall (n Φ).
wp_rec. simpl. wp_op. case_bool_decide; simplify_eq; wp_if.
{ assert (n = O) as -> by lia.
by iApply ("HΦ" $! 1%nat). }
@@ -77,7 +77,7 @@ Section contents.
Proof.
iIntros (Φ) "[#Hrunner HP] HΦ".
iDestruct "HP" as (n) "%"; simplify_eq.
- do 2 wp_rec. simpl. wp_op. case_bool_decide; wp_if.
+ wp_lam. wp_let. wp_op. case_bool_decide; wp_if.
- iApply seqFib_spec; eauto.
iNext. iIntros (? <-). iApply "HΦ".
iExists n; done.
@@ -107,7 +107,7 @@ Section contents.
{{{ True }}} fibRunner #n #a {{{ (m : nat), RET #m; ⌜fib a = m⌠}}}.
Proof.
iIntros (Φ) "_ HΦ".
- unfold fibRunner. do 2 wp_rec. wp_bind (newRunner _ _ _).
+ unfold fibRunner. wp_lam. wp_let. wp_bind (newRunner _ _ _).
iApply (newRunner_spec b N P Q).
- iIntros (γb r). iAlways. iIntros (a') "[#Hrunner HP]".
iApply (parFib_spec with "[$HP]"); eauto.
diff --git a/theories/lecture_notes/ccounter.v b/theories/lecture_notes/ccounter.v
index 92c31c1289f094aeef4e0b1197bdd24e113ad9a3..e79736eae91bbc36291d8f3d15deeb1cf931cecf 100644
--- a/theories/lecture_notes/ccounter.v
+++ b/theories/lecture_notes/ccounter.v
@@ -26,7 +26,7 @@ Section ccounter.
Lemma ccounterRA_valid_full (m n : natR): ✓ (â—! m â‹… â—¯! n) → (n = m)%nat.
Proof.
by intros ?%frac_auth_agree.
- Qed.
+ Qed.
Lemma ccounterRA_update (m n : natR) (q : frac): (â—! m â‹… â—¯!{q} n) ~~> (â—! (S m) â‹… â—¯!{q} (S n)).
Proof.
@@ -51,7 +51,7 @@ Section ccounter.
Qed.
Lemma newcounter_contrib_spec (R : iProp Σ) m:
- {{{ True }}}
+ {{{ True }}}
newcounter #m
{{{ γ₠γ₂ ℓ, RET #ℓ; is_ccounter γ₠γ₂ ℓ 1 m%nat }}}.
Proof.
@@ -66,21 +66,21 @@ Section ccounter.
Lemma incr_contrib_spec γ₠γ₂ ℓ q n :
{{{ is_ccounter γ₠γ₂ ℓ q n }}}
- incr #â„“
+ incr #â„“
{{{ (y : Z), RET #y; is_ccounter γ₠γ₂ ℓ q (S n) }}}.
Proof.
- iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
+ iIntros (Φ) "[Hown #[Hinv HCnt]] HΦ".
iApply (incr_spec N γ₂ _ (own γ₠(◯!{q} n))%I (λ _, (own γ₠(◯!{q} (S n))))%I with "[] [Hown]"); first set_solver.
- - iIntros (m) "!# [HOwnElem HP]".
+ - iIntros (m) "!# [HOwnElem HP]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
- iDestruct (makeElem_eq with "HOwnElem H2") as %->.
+ iDestruct (makeElem_eq with "HOwnElem H2") as %->.
iMod (makeElem_update _ _ _ (k+1) with "HOwnElem H2") as "[HOwnElem H2]".
iMod (own_update_2 with "H1 HP") as "[H1 HP]".
- { apply ccounterRA_update. }
+ { apply ccounterRA_update. }
iMod ("HClose" with "[H1 H2]") as "_".
{ iNext; iExists (S k); iFrame.
rewrite Nat2Z.inj_succ Z.add_1_r //.
- }
+ }
by iFrame.
- by iFrame.
- iNext.
@@ -89,7 +89,7 @@ Section ccounter.
Qed.
Lemma read_contrib_spec γ₠γ₂ ℓ q n :
- {{{ is_ccounter γ₠γ₂ ℓ q n }}}
+ {{{ is_ccounter γ₠γ₂ ℓ q n }}}
read #â„“
{{{ (c : Z), RET #c; ⌜Z.of_nat n ≤ c⌠∧ is_ccounter γ₠γ₂ ℓ q n }}}.
Proof.
@@ -97,7 +97,7 @@ Section ccounter.
wp_apply (read_spec N γ₂ _ (own γ₠(◯!{q} n))%I (λ m, ⌜n ≤ m⌠∗ (own γ₠(◯!{q} n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
- iDestruct (makeElem_eq with "HownE H2") as %->.
+ iDestruct (makeElem_eq with "HownE H2") as %->.
iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid.
iMod ("HClose" with "[H1 H2]") as "_".
{ iExists _; by iFrame. }
@@ -118,7 +118,7 @@ Section ccounter.
wp_apply (read_spec N γ₂ _ (own γ₠(◯! n))%I (λ m, ⌜Z.of_nat n = m⌠∗ (own γ₠(◯! n)))%I with "[] [Hown]"); first set_solver.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
- iDestruct (makeElem_eq with "HownE H2") as %->.
+ iDestruct (makeElem_eq with "HownE H2") as %->.
iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid_full; simplify_eq.
iMod ("HClose" with "[H1 H2]") as "_".
{ iExists _; by iFrame. }
diff --git a/theories/lecture_notes/coq_intro_example_1.v b/theories/lecture_notes/coq_intro_example_1.v
index 234fa5099de83ef63f33b2d24eb82ec3116042fe..cf2e23d68881df7c67fddc5aa52bc05450f72018 100644
--- a/theories/lecture_notes/coq_intro_example_1.v
+++ b/theories/lecture_notes/coq_intro_example_1.v
@@ -139,10 +139,8 @@ Section proof.
proved in the par library we have imported above. The rule/lemma is
called wp_par. The two arguments are the conclusions of the two
parallel threads. Here they are simply True, as in the paper proof when
- we used the ht-par rule. The first two subgoals are bookkeeping
- subgoals about closedness (absence of free variables) of expression
- incr â„“ and incr â„“. They are easily dispatched by the done tactic. *)
- iApply (wp_par (λ _ , ⌜TrueâŒ)%I (λ _ , ⌜TrueâŒ)%I); [done | done | ..].
+ we used the ht-par rule. *)
+ iApply (wp_par (λ _ , ⌜TrueâŒ)%I (λ _ , ⌜TrueâŒ)%I).
(* We now have three subgoals. The first two are proofs that each thread
does the correct thing, and the final goal is to show that the combined
conclusion of the two threads implies the desired conclusion. This last
@@ -236,9 +234,9 @@ Section proof.
..., thus we first remove the later modality using the later
introduction rule, implemented by the iNext tactic. After that we
have to deal with the application of a function with a dummy argument,
- i.e., sequencing. The wp_lam tactic handles it. *)
+ i.e., sequencing. The wp_seq tactic handles it. *)
iNext.
- wp_lam.
+ wp_seq.
(* The last interesting part of the proof is before us. We do exactly as
we did on paper. We open the invariant, and read the value. And the
invariant will tell us that the value is at least n. We can then apply
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index 0daf96311b416ea798f6597fc08953df285a5ba9..3bc85d30a0a2cd9d21eb18199b4117fd4bf08185 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -315,7 +315,7 @@ Section monotone_counter.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists m; iFrame. }
iModIntro.
- wp_lam; wp_op; wp_lam.
+ wp_let; wp_op; wp_let.
wp_bind (CAS _ _ _)%E.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
@@ -332,7 +332,7 @@ Section monotone_counter.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists (1 + m)%nat.
rewrite Nat2Z.inj_succ Z.add_1_l; iFrame. }
- iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
+ iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
iExists γ; iFrame "#"; iFrame.
+ wp_cas_fail; first intros ?; simplify_eq.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
@@ -377,9 +377,9 @@ Section auth_update.
apply auth_update.
intros ? mz ? Heq.
split.
- - apply cmra_valid_validN; auto.
+ - apply cmra_valid_validN; auto.
- simpl in *.
- rewrite Heq.
+ rewrite Heq.
destruct mz; simpl; auto.
rewrite -assoc (comm _ _ z) assoc //.
Qed.
@@ -425,7 +425,7 @@ Section monotone_counter'.
The general definition also involves the use of step-indices, which is not needed in our case. *)
rewrite auth_valid_discrete_2.
split.
- - intros [? _]; by apply mnat_included.
+ - intros [? _]; by apply mnat_included.
- intros ?%mnat_included; done.
Qed.
@@ -468,7 +468,7 @@ Section monotone_counter'.
+ iApply ("HCont" with "[HFrac HInv]").
iExists γ; iFrame.
Qed.
-
+
(* The read method specification. *)
Lemma read_spec' â„“ n: {{{ isCounter' â„“ n }}} read #â„“ {{{ m, RET #m; ⌜n ≤ mâŒ%nat }}}.
Proof.
@@ -500,7 +500,7 @@ Section monotone_counter'.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists m; iFrame. }
iModIntro.
- wp_lam; wp_op; wp_lam.
+ wp_let; wp_op; wp_let.
wp_bind (CAS _ _ _)%E.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
@@ -511,7 +511,7 @@ Section monotone_counter'.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists (1 + m)%nat.
rewrite Nat2Z.inj_succ Z.add_1_l; iFrame. }
- iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
+ iModIntro; wp_if; iApply ("HCont" with "[HInv HOwnFrag]").
iExists γ; iFrame "#"; iFrame.
+ wp_cas_fail; first intros ?; simplify_eq.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
@@ -559,7 +559,7 @@ Section ccounter.
Lemma ccounterRA_valid_full (m n : natR): ✓ (â—! m â‹… â—¯! n) → (n = m)%nat.
Proof.
by intros ?%frac_auth_agree.
- Qed.
+ Qed.
Lemma ccounterRA_update (m n : natR) (q : frac): (â—! m â‹… â—¯!{q} n) ~~> (â—! (S m) â‹… â—¯!{q} (S n)).
Proof.
@@ -588,7 +588,7 @@ Section ccounter.
(** The main proofs. *)
(* As explained in the notes the is_ccounter predicate for this specificatin is not persistent.
- However it is still shareable in the following restricted way.
+ However it is still shareable in the following restricted way.
*)
Lemma is_ccounter_op γ ℓ q1 q2 (n1 n2 : nat) :
is_ccounter γ ℓ (q1 + q2) (n1 + n2)%nat ⊣⊢ is_ccounter γ ℓ q1 n1 ∗ is_ccounter γ ℓ q2 n2.
@@ -601,11 +601,11 @@ Section ccounter.
Qed.
Lemma newcounter_contrib_spec (R : iProp Σ) :
- {{{ True }}}
+ {{{ True }}}
newCounter #()
{{{ γ ℓ, RET #ℓ; is_ccounter γ ℓ 1 0%nat }}}.
Proof.
- iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_seq. wp_alloc ℓ as "Hpt".
+ iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc ℓ as "Hpt".
iMod (own_alloc (â—! O%nat â‹… â—¯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
iMod (inv_alloc N _ (ccounter_inv γ ℓ) with "[Hpt Hγ]").
{ iNext. iExists 0%nat. by iFrame. }
@@ -614,7 +614,7 @@ Section ccounter.
Lemma incr_contrib_spec γ ℓ q n :
{{{ is_ccounter γ ℓ q n }}}
- incr #â„“
+ incr #â„“
{{{ RET #(); is_ccounter γ ℓ q (S n) }}}.
Proof.
iIntros (Φ) "[Hown #Hinv] HΦ". iLöb as "IH". wp_rec.
@@ -634,12 +634,12 @@ Section ccounter.
Qed.
Lemma read_contrib_spec γ ℓ q n :
- {{{ is_ccounter γ ℓ q n }}}
+ {{{ is_ccounter γ ℓ q n }}}
read #â„“
{{{ c, RET #c; ⌜n ≤ câŒ%nat ∧ is_ccounter γ â„“ q n }}}.
Proof.
iIntros (Φ) "[Hown #Hinv] HΦ".
- rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
+ rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hown") as % ?%ccounterRA_valid. (* We use the validity property of our RA. *)
iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"); rewrite /is_ccounter; eauto.
@@ -650,7 +650,7 @@ Section ccounter.
{{{ m, RET #m; ⌜m = n⌠∗ is_ccounter γ ℓ 1 m }}}.
Proof.
iIntros (Φ) "[Hown #Hinv] HΦ".
- rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
+ rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
iDestruct (own_valid_2 with "Hγ Hown") as % <-%ccounterRA_valid_full. (* We use the validity property of our RA. *)
iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists n; by iFrame|].
iApply "HΦ"; iModIntro. iFrame "Hown #"; done.
diff --git a/theories/lecture_notes/lists.v b/theories/lecture_notes/lists.v
index b5ff25aa552863a2856c16a11e2a24e8fa3ca143..9d6f3f9536a0971bc627c929c4af53b63ac6c1b6 100644
--- a/theories/lecture_notes/lists.v
+++ b/theories/lecture_notes/lists.v
@@ -1,5 +1,3 @@
-
-
(* In this file we explain how to do the "list examples" from the
Chapter on Separation Logic for Sequential Programs in the
Iris Lecture Notes *)
@@ -13,30 +11,30 @@ From iris.program_logic Require Export weakestpre.
the lang file contains the actual language syntax. *)
From iris.heap_lang Require Export notation lang.
-(* Files related to the interactive proof mode. The first import includes the
- general tactics of the proof mode. The second provides some more specialized
- tactics particular to the instantiation of Iris to a particular programming
+(* Files related to the interactive proof mode. The first import includes the
+ general tactics of the proof mode. The second provides some more specialized
+ tactics particular to the instantiation of Iris to a particular programming
language. *)
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode.
-(* The following line makes Coq check that we do not use any admitted facts /
+(* The following line makes Coq check that we do not use any admitted facts /
additional assumptions not in the statement of the theorems being proved. *)
Set Default Proof Using "Type".
(* ---------------------------------------------------------------------- *)
Section list_model.
- (* This section contains the definition of our model of lists, i.e.,
+ (* This section contains the definition of our model of lists, i.e.,
definitions relating pointer data structures to our model, which is
simply mathematical sequences (Coq lists). *)
-
-
+
+
(* In order to do the proof we need to assume certain things about the
instantiation of Iris. The particular, even the heap is handled in an
analogous way as other ghost state. This line states that we assume the
Iris instantiation has sufficient structure to manipulate the heap, e.g.,
- it allows us to use the points-to predicate. *)
+ it allows us to use the points-to predicate. *)
Context `{!heapG Σ}.
Implicit Types l : loc.
@@ -45,9 +43,9 @@ Implicit Types l : loc.
But since Σ is the same throughout the development we shall define
shorthand notation which hides it. *)
Notation iProp := (iProp Σ).
-
+
(* Here is the basic is_list representation predicate:
- is_list hd xs holds if hd points to a linked list consisting of
+ is_list hd xs holds if hd points to a linked list consisting of
the elements in the mathematical sequence (Coq list) xs.
*)
Fixpoint is_list (hd : val) (xs : list val) : iProp :=
@@ -58,7 +56,7 @@ end%I.
(* The following predicate
is_listP P hd xs
- holds if hd points to a linked list consisting of the elements in xs and
+ holds if hd points to a linked list consisting of the elements in xs and
each of those elements satisfy P.
*)
Fixpoint is_listP P (hd : val) (xs : list val) : iProp :=
@@ -82,9 +80,9 @@ Proof.
- iDestruct 1 as "(H_isList & ? & H)". iDestruct "H_isList" as (l hd') "(? & ? & ?)".
iExists l, hd'. rewrite IHxs'. iFrame.
Qed.
-
+
(* The predicate
- is_list_nat hd xs
+ is_list_nat hd xs
holds if hd is a pointer to a linked list of numbers (integers).
*)
Fixpoint is_list_nat (hd : val) (xs : list Z) : iProp :=
@@ -119,9 +117,9 @@ End list_model.
(* ---------------------------------------------------------------------- *)
-Section list_code.
+Section list_code.
(* This section contains the code of the list functions we specify *)
-
+
(* Function inc hd assumes all values in the linked list pointed to by hd
are numbers and increments them by 1, in-place *)
Definition inc : val :=
@@ -147,7 +145,7 @@ Section list_code.
"l"
end.
- (* Function rev l acc reverses all the pointers in linked list l and stiches
+ (* Function rev l acc reverses all the pointers in linked list l and stiches
the accumulator argument acc at the end *)
Definition rev : val :=
rec: "rev" "l" "acc" :=
@@ -159,7 +157,7 @@ Section list_code.
"p" <- ("h", "acc");;
"rev" "t" "l"
end.
-
+
(* Function len l returns the lenght of linked list l *)
Definition len : val :=
rec: "len" "l" :=
@@ -181,7 +179,7 @@ Section list_code.
"f" ("hd", ("foldr" "f" "a" "t"))
end.
- (* sum_list l returns the sum of the list of numbers in linked list l,
+ (* sum_list l returns the sum of the list of numbers in linked list l,
implemented by call to foldr *)
Definition sum_list : val :=
rec: "sum_list" "l" :=
@@ -209,7 +207,7 @@ Section list_code.
else "xs")
in (foldr "f" empty_list "l").
- (* map_list f l is the usual map function on linked lists with f the function
+ (* map_list f l is the usual map function on linked lists with f the function
to be mapped over the list l. Implemented using foldr. *)
Definition map_list : val :=
rec: "map_list" "f" "l" :=
@@ -225,7 +223,7 @@ Section list_code.
rec: "incr" "l" :=
map_list (λ: "n", "n" + #1)%I "l".
-End list_code.
+End list_code.
(* ---------------------------------------------------------------------- *)
@@ -233,9 +231,9 @@ Section list_spec.
(* This section contains the specifications and proofs for the list functions.
The specifications and proofs are explained in the Iris Lecture Notes
*)
-
+
Context `{!heapG Σ}.
-
+
Lemma inc_spec hd xs :
{{{ is_list_nat hd xs }}}
inc hd
@@ -277,12 +275,12 @@ Proof.
iIntros (Ï•) "[H1 H2] HL".
iInduction vs as [| v vs'] "IH" forall (acc l us).
- iSimplifyEq. wp_rec. wp_let. wp_match. iApply "HL". done.
- - simpl. iDestruct "H1" as (l' t) "(% & H3 & H1)". wp_rec. wp_let.
+ - simpl. iDestruct "H1" as (l' t) "(% & H3 & H1)". wp_rec. wp_let.
rewrite -> H at 1. wp_match. do 2 (wp_load; wp_proj; wp_let).
wp_store. iSpecialize ("IH" $! l t ([v] ++ us)).
iApply ("IH" with "[H1] [H3 H2]").
+ done.
- + simpl. iExists l', acc. iFrame. done.
+ + simpl. iExists l', acc. iFrame. done.
+ iNext. rewrite -> app_assoc. done.
Qed.
@@ -300,27 +298,26 @@ Proof.
Qed.
(* The following specifications for foldr are non-trivial because the code is higher-order
- and hence the specifications involved nested triples.
+ and hence the specifications involved nested triples.
The specifications are explained in the Iris Lecture Notes. *)
-Lemma foldr_spec_PI P I (f a hd : val) (e_f e_a e_hd : expr) (xs : list val) :
- IntoVal e_f f → IntoVal e_a a → IntoVal e_hd hd →
+Lemma foldr_spec_PI P I (f a hd : val) (xs : list val) :
{{{ (∀ (x a' : val) (ys : list val),
{{{ P x ∗ I ys a'}}}
- e_f (x, a')
+ f (x, a')
{{{r, RET r; I (x::ys) r }}})
∗ is_list hd xs
∗ ([∗ list] x ∈ xs, P x)
∗ I [] a
}}}
- foldr e_f e_a e_hd
+ foldr f a hd
{{{
r, RET r; is_list hd xs
∗ I xs r
}}}.
Proof.
- iIntros (<- <- <- Ï•) "(#H_f & H_isList & H_Px & H_Iempty) H_inv".
+ iIntros (Ï•) "(#H_f & H_isList & H_Px & H_Iempty) H_inv".
iInduction xs as [|x xs'] "IH" forall (Ï• a hd); wp_rec; do 2 wp_let; iSimplifyEq.
- wp_match. iApply "H_inv". eauto.
- iDestruct "H_isList" as (l hd') "[% [H_l H_isList]]".
@@ -335,22 +332,21 @@ Proof.
iExists l, hd'. by iFrame.
Qed.
-Lemma foldr_spec_PPI P I (f a hd : val ) (e_f e_a e_hd : expr) (xs : list val) :
- IntoVal e_f f → IntoVal e_a a → IntoVal e_hd hd →
+Lemma foldr_spec_PPI P I (f a hd : val) (xs : list val) :
{{{ (∀ (x a' : val) (ys : list val),
{{{ P x ∗ I ys a'}}}
- e_f (x, a')
+ f (x, a')
{{{r, RET r; I (x::ys) r }}})
∗ is_listP P hd xs
∗ I [] a
}}}
- foldr e_f e_a e_hd
+ foldr f a hd
{{{
r, RET r; is_listP (fun x => True) hd xs
∗ I xs r
}}}.
Proof.
- iIntros (<- <- <- Ï•) "(#H_f & H_isList & H_Iempty) H_inv".
+ iIntros (Ï•) "(#H_f & H_isList & H_Iempty) H_inv".
rewrite about_isList. iDestruct "H_isList" as "(H_isList & H_Pxs)".
iApply (foldr_spec_PI with "[-H_inv]").
- iFrame. by iFrame "H_f".
@@ -364,7 +360,7 @@ Lemma sum_spec (hd: val) (xs: list Z) :
{{{ v, RET v; ⌜v = # (fold_right Z.add 0 xs)⌠}}}.
Proof.
iIntros (Ï•) "H_is_list H_later".
- wp_rec. wp_let.
+ wp_rec. wp_pures.
iApply (foldr_spec_PI
(fun x => (∃ (n : Z), ⌜x = #nâŒ)%I)
(fun xs' acc => ∃ ys,
@@ -376,7 +372,7 @@ Proof.
+ iIntros (x a' ys). iAlways. iIntros (Ï•') "(H1 & H2) H3".
do 5 (wp_pure _).
iDestruct "H2" as (zs) "(% & % & H_list)".
- iDestruct "H1" as (n2) "%". iSimplifyEq. wp_binop.
+ iDestruct "H1" as (n2) "%". iSimplifyEq. wp_pures.
iApply "H3". iExists (n2::zs). repeat (iSplit; try done).
by iExists _.
+ iSplit.
@@ -392,7 +388,7 @@ Qed.
Lemma filter_spec (hd p : val) (xs : list val) (P : val -> bool) :
{{{ is_list hd xs
- ∗ (∀ x : val ,
+ ∗ (∀ x : val ,
{{{ True }}}
p x
{{{r, RET r; ⌜r = #(P x)⌠}}})
@@ -402,17 +398,16 @@ Lemma filter_spec (hd p : val) (xs : list val) (P : val -> bool) :
∗ is_list v (List.filter P xs)
}}}.
Proof.
- iIntros (Ï•) "[H_isList #H_p] H_Ï•".
- do 3 (wp_pure _).
+ iIntros (Ï•) "[H_isList #H_p] H_Ï•". wp_rec. wp_pures.
iApply (foldr_spec_PI (fun x => True)%I
- (fun xs' acc => is_list acc (List.filter P xs'))%I
+ (fun xs' acc => is_list acc (List.filter P xs'))%I
with "[$H_isList] [H_Ï•]").
- iSplitL.
+ iIntros "** !#" (Ï•'). iIntros "[_ H_isList] H_Ï•'".
repeat (wp_pure _). wp_bind (p x). iApply "H_p"; first done.
iNext. iIntros (r) "H". iSimplifyEq. destruct (P x); wp_if.
- * unfold cons. repeat (wp_pure _). wp_alloc l. iApply "H_Ï•'".
- iExists l, a'. by iFrame.
+ * wp_rec. wp_pures. wp_alloc l. wp_pures. iApply "H_Ï•'".
+ iExists l, a'. by iFrame.
* by iApply "H_Ï•'".
+ iSplit; last done.
rewrite big_sepL_forall. eauto.
@@ -420,24 +415,23 @@ Proof.
Qed.
-Lemma map_spec P Q (e_f e_hd : expr) (f hd : val) (xs : list val) :
- IntoVal e_f f → IntoVal e_hd hd →
+Lemma map_spec P Q (f hd : val) (xs : list val) :
{{{
is_list hd xs
∗ (∀ (x : val), {{{ P x }}}
- e_f x
+ f x
{{{r, RET r; Q x r}}})
∗ [∗ list] x ∈ xs, P x
}}}
- map_list e_f e_hd
+ map_list f hd
{{{
r, RET r; ∃ (ys : list val), is_list r ys
∗ ([∗ list] p ∈ zip xs ys, Q (fst p) (snd p))
∗ ⌜List.length ys = List.length xsâŒ
}}}.
Proof.
- iIntros (<- <- Ï•) "[H_is_list [#H1 H_P_xs]] H_Ï•".
- do 3 (wp_pure _).
+ iIntros (Ï•) "[H_is_list [#H1 H_P_xs]] H_Ï•".
+ wp_rec. wp_pures.
iApply (foldr_spec_PI
P
(fun xs acc => ∃ ys, (is_list acc ys)
@@ -445,12 +439,12 @@ Proof.
∗ ⌜length xs = length ysâŒ)%I
with "[H_is_list H1 H_P_xs] [H_Ï•]").
- iSplitR "H_is_list H_P_xs".
- + iIntros (x a' ys). iAlways. iIntros (Ï•') "(H_Px & H_Q) H_Ï•'". repeat (wp_pure _).
+ + iIntros (x a' ys). iAlways. iIntros (Ï•') "(H_Px & H_Q) H_Ï•'". wp_pures.
wp_bind (f x). iApply ("H1" with "[H_Px][H_Q H_Ï•']"); try done.
- iNext. iIntros (r) "H_Qr". repeat (wp_pure _). wp_alloc l. iApply "H_Ï•'".
+ iNext. iIntros (r) "H_Qr". wp_rec. wp_alloc l. wp_pures. iApply "H_Ï•'".
iDestruct "H_Q" as (ys') "(H_is_list_ys' & H_Qys' & %)". iExists (r::ys').
iSplitR "H_Qr H_Qys'".
- * unfold is_list. iExists l, a'. fold is_list. by iFrame.
+ * unfold is_list. iExists l, a'. fold is_list. by iFrame.
* iSimplifyEq. iFrame. eauto.
+ iFrame. iExists []. iSplit; by simpl.
- iNext. iIntros (r) "H". iApply "H_Ï•". iDestruct "H" as "(_ & H_Q)".
@@ -459,7 +453,7 @@ Qed.
Lemma about_length {A : Type} (xs : list A) (n : nat) :
- length xs = S n -> exists x xs', xs = x::xs'.
+ length xs = S n -> exists x xs', xs = x::xs'.
Proof.
intro H. induction xs as [| x xs' ].
- inversion H.
@@ -472,27 +466,26 @@ Lemma inc_with_map hd (xs : list Z) :
{{{ v, RET v; is_list v (List.map (fun (n : Z) => #n) (List.map Z.succ xs)) }}}.
Proof.
iIntros (Ï•) "H_isList H_Ï•".
- wp_rec. iApply (map_spec
+ wp_rec. wp_apply (map_spec
(fun x => (∃ (n : Z), ⌜x = #nâŒ)%I)
(fun x r => (∃ (n' : Z),
⌜r = #(Z.succ n')âŒ
∗ ⌜x = #n'âŒ)%I)
with "[$H_isList] [H_Ï•]").
- - iSplit. iIntros (x) "!#". iIntros (Ï•') "H1 H2". wp_let. iDestruct "H1" as (n) "H_x".
+ - iSplit. iIntros (x) "!#". iIntros (Ï•') "H1 H2". wp_lam. iDestruct "H1" as (n) "H_x".
iSimplifyEq. wp_binop. iApply "H2". by iExists n.
rewrite big_sepL_fmap. rewrite big_sepL_forall. eauto.
- - iNext. iIntros (r) "H". iApply "H_Ï•". iDestruct "H" as (ys) "(H_isList & H_post & H_length)".
+ - iNext. iIntros (r) "H". iApply "H_Ï•". iDestruct "H" as (ys) "(H_isList & H_post & H_length)".
iAssert (⌜ys = (List.map (λ n : Z, #n) (List.map Z.succ xs))âŒ)%I with "[-H_isList]" as %->.
- { iInduction ys as [| y ys'] "IH" forall (xs); iDestruct "H_length" as %H.
+ { iInduction ys as [| y ys'] "IH" forall (xs); iDestruct "H_length" as %H.
- simpl. destruct xs. by simpl. inversion H.
- rewrite fmap_length in H. symmetry in H. simpl in H.
destruct (about_length _ _ H) as (x & xs' & ->). simpl.
iDestruct "H_post" as "(H_head & H_tail)".
iDestruct "H_head" as (n') "(% & %)". iSimplifyEq.
iDestruct ("IH" with "H_tail []") as %->. by rewrite fmap_length. done.
- }
+ }
iFrame.
Qed.
-End list_spec.
-
+End list_spec.
diff --git a/theories/lecture_notes/lock_unary_spec.v b/theories/lecture_notes/lock_unary_spec.v
index 892156a4711f96305edb9257aecfe93caaac171c..85eb9810f469fb0f7aa4f2b8b84f6081145f55ef 100644
--- a/theories/lecture_notes/lock_unary_spec.v
+++ b/theories/lecture_notes/lock_unary_spec.v
@@ -15,9 +15,9 @@ From iris.program_logic Require Export weakestpre.
the lang file contains the actual language syntax. *)
From iris.heap_lang Require Export notation lang.
-(* Files related to the interactive proof mode. The first import includes the
- general tactics of the proof mode. The second provides some more specialized
- tactics particular to the instantiation of Iris to a particular programming
+(* Files related to the interactive proof mode. The first import includes the
+ general tactics of the proof mode. The second provides some more specialized
+ tactics particular to the instantiation of Iris to a particular programming
language. *)
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode.
@@ -30,18 +30,18 @@ From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Import excl.
-Section lock_model.
+Section lock_model.
(* In order to do the proof we need to assume certain things about the
instantiation of Iris. The particular, even the heap is handled in an
analogous way as other ghost state. This line states that we assume the Iris
instantiation has sufficient structure to manipulate the heap, e.g., it
allows us to use the points-to predicate, and that the ghost state includes
the exclusive resource algebra over the singleton set (represented using the
- unitR type). *)
+ unitR type). *)
Context `{heapG Σ}.
Context `{inG Σ (exclR unitR)}.
-
+
(* We use a ghost name with a token to model whether the lock is locked or not.
The the token is just exclusive ownerwhip of unit value. *)
Definition locked γ := own γ (Excl ()).
@@ -57,13 +57,13 @@ Section lock_model.
(* The is_lock predicate is persistent *)
Global Instance is_lock_persistent γ l Φ : Persistent (is_lock γ l Φ).
Proof. apply _. Qed.
-
+
End lock_model.
Section lock_code.
(* Here is the standard spin lock code *)
-
+
Definition newlock : val := λ: <>, ref #false.
Definition acquire : val :=
rec: "acquire" "l" :=
@@ -75,11 +75,11 @@ End lock_code.
Section lock_spec.
Context `{heapG Σ}.
Context `{inG Σ (exclR unitR)}.
-
- (* Here is the interesting part of this example, namely the new specification
- for newlock, which allows one to get a post-condition which can be instantiated
- with the lock invariant at some point later, when it is known.
- See the discussion in Iris Lecture Notes.
+
+ (* Here is the interesting part of this example, namely the new specification
+ for newlock, which allows one to get a post-condition which can be instantiated
+ with the lock invariant at some point later, when it is known.
+ See the discussion in Iris Lecture Notes.
First we show the specs using triples, and afterwards using weakest preconditions.
*)
@@ -111,7 +111,7 @@ Section lock_spec.
wp_rec.
wp_bind (CAS _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- - wp_cas_suc.
+ - wp_cas_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_if.
@@ -132,7 +132,7 @@ Section lock_spec.
iIntros (HE φ) "(#Hi & Hld & HP) Hcont"; rewrite /release.
wp_lam.
iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
- - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
+ - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
- wp_store.
iMod ("Hcl" with "[-Hcont]") as "_"; first by iNext; iLeft; iFrame.
iApply "Hcont".
@@ -140,14 +140,14 @@ Section lock_spec.
Qed.
(* Here are the specifications again, just written using weakest preconditions *)
-
+
Lemma wp_newlock :
True ⊢ WP newlock #() {{v, ∃ (l: loc) γ, ⌜v = #l⌠∧ (∀ P E, P ={E}=∗ is_lock γ l P) }}.
Proof.
iIntros "_".
rewrite -wp_fupd /newlock.
wp_lam.
- wp_alloc l as "HPt".
+ wp_alloc l as "HPt".
iExists l.
iMod (own_alloc (Excl ())) as (γ) "Hld"; first done.
iExists γ.
@@ -159,7 +159,7 @@ Section lock_spec.
{ iNext; iLeft; iFrame. }
Qed.
-
+
Lemma wp_acquire E γ l P :
nclose (lockN l) ⊆ E →
is_lock γ l P ⊢ WP acquire (#l) @ E {{v, P ∗ locked γ}}.
@@ -169,7 +169,7 @@ Section lock_spec.
wp_rec.
wp_bind (CAS _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- - wp_cas_suc.
+ - wp_cas_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_if.
@@ -189,7 +189,7 @@ Section lock_spec.
iIntros (HE) "(#Hi & Hld & HP)"; rewrite /release.
wp_lam.
iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
- - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
+ - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
- wp_store.
iMod ("Hcl" with "[-]") as "_"; first by iNext; iLeft; iFrame.
done.
@@ -201,7 +201,7 @@ Section lock_spec.
(* We now present a simple client of the lock which cannot be verified with the
lock specification described in the Chapter on Invariants and Ghost State in the
Iris Lecture Notes, but which can be specifed and verified with the current
- specification.
+ specification.
*)
Definition test : expr :=
let: "l" := newlock #() in
@@ -216,11 +216,11 @@ Section lock_spec.
iApply (wp_newlock_t); auto.
iNext.
iIntros (v) "Hs".
- wp_lam.
+ wp_let.
wp_bind (ref #0)%E.
wp_alloc l as "Hl".
- wp_lam.
- wp_lam.
+ wp_let.
+ wp_seq.
wp_bind (acquire v)%E.
iDestruct "Hs" as (l' γ) "[% H2]".
subst.
@@ -229,7 +229,7 @@ Section lock_spec.
wp_apply (wp_acquire_t with "H3"); auto.
iIntros (v) "(Hpt & Hlocked)".
iDestruct "Hpt" as (u) "Hpt".
- wp_lam.
+ wp_seq.
wp_load.
wp_op.
wp_store.
@@ -242,4 +242,4 @@ End lock_spec.
Typeclasses Opaque locked.
Global Opaque locked.
Typeclasses Opaque is_lock.
-Global Opaque is_lock.
\ No newline at end of file
+Global Opaque is_lock.
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index 4b39bc1ea98ab01bef7963359d00db014183258a..9fd6b0ac4077242ea77e63b3f08da1b2c580d9c6 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -51,7 +51,7 @@ Section cnt_model.
by rewrite /= agree_idemp.
Qed.
- Global Instance makeElem_as_fractional γ m q:
+ Global Instance makeElem_as_fractional γ m q:
AsFractional (own γ (makeElem q m)) (λ q, γ ⤇[q] m)%I q.
Proof.
split. done. apply _.
@@ -59,13 +59,13 @@ Section cnt_model.
Global Instance makeElem_Exclusive m: Exclusive (makeElem 1 m).
Proof.
- intros [y ?] [H _]. apply (exclusive_l _ _ H).
+ intros [y ?] [H _]. apply (exclusive_l _ _ H).
Qed.
Lemma makeElem_op p q n:
makeElem p n ⋅ makeElem q n ≡ makeElem (p + q) n.
Proof.
- rewrite /makeElem; split; first done.
+ rewrite /makeElem; split; first done.
by rewrite /= agree_idemp.
Qed.
@@ -86,7 +86,7 @@ Section cnt_model.
iCombine "H1" "H2" as "H".
by rewrite makeElem_op.
Qed.
-
+
Lemma makeElem_update γ (n m k : Z):
γ ⤇½ n -∗ γ ⤇½ m ==∗ γ ⤇[1] k.
Proof.
@@ -95,7 +95,7 @@ Section cnt_model.
rewrite Qp_div_2.
iApply (own_update with "H"); by apply cmra_update_exclusive.
Qed.
-End cnt_model.
+End cnt_model.
Notation "γ ⤇[ q ] m" := (own γ (makeElem q m))
(at level 20, q at level 50, format "γ ⤇[ q ] m") : bi_scope.
@@ -104,7 +104,7 @@ Notation "γ ⤇½ m" := (own γ (makeElem (1/2) m))
Section cnt_spec.
Context `{!heapG Σ, !cntG Σ} (N : namespace).
-
+
Definition cnt_inv ℓ γ := (∃ (m : Z), ℓ ↦ #m ∗ γ ⤇½ m)%I.
Definition Cnt (ℓ : loc) (γ : gname) : iProp Σ :=
@@ -125,7 +125,7 @@ Section cnt_spec.
{{{ True }}} newcounter #m @ E {{{ (ℓ : loc), RET #ℓ; ∃ γ, Cnt ℓ γ ∗ γ ⤇½ m}}}.
Proof.
iIntros (Hsubset Φ) "#Ht HΦ".
- rewrite -wp_fupd.
+ rewrite -wp_fupd.
wp_lam.
wp_alloc â„“ as "Hl".
iApply "HΦ".
@@ -133,7 +133,7 @@ Section cnt_spec.
Qed.
Theorem read_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q : Z → iProp Σ) (ℓ : loc):
- ↑(N .@ "internal") ⊆ E →
+ ↑(N .@ "internal") ⊆ E →
(∀ m, (γ ⤇½ m ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ m ∗ Q m)) ⊢
{{{ Cnt ℓ γ ∗ P}}} read #ℓ @ E {{{ (m : Z), RET #m; Cnt ℓ γ ∗ Q m }}}.
Proof.
@@ -150,10 +150,10 @@ Section cnt_spec.
iModIntro.
iFrame.
done.
- Qed.
+ Qed.
Theorem incr_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q : Z → iProp Σ) (ℓ : loc):
- ↑(N .@ "internal") ⊆ E →
+ ↑(N .@ "internal") ⊆ E →
(∀ (n : Z), γ ⤇½ n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q n) ⊢
{{{ Cnt ℓ γ ∗ P }}} incr #ℓ @ E {{{ (m : Z), RET #m; Cnt ℓ γ ∗ Q m}}}.
Proof.
@@ -198,7 +198,7 @@ Section cnt_spec.
wp_bind (! _)%E.
iInv (N .@ "internal") as (m) "[>Hpt >Hown]" "HClose".
wp_load.
- iDestruct (makeElem_eq with "Hγ Hown") as %->.
+ iDestruct (makeElem_eq with "Hγ Hown") as %->.
iMod ("HClose" with "[Hpt Hown]") as "_".
{ iNext; iExists _; iFrame. }
iModIntro.
@@ -210,10 +210,10 @@ Section cnt_spec.
wp_store.
iMod ("HClose" with "[Hpt Hown]") as "_".
{ iNext; iExists _; iFrame. }
- iModIntro.
+ iModIntro.
iApply "HCont"; by iFrame.
Qed.
-
+
Theorem wk_incr_spec' (γ : gname) (E : coPset) (P Q : iProp Σ) (ℓ : loc) (n : Z) (q : Qp):
↑(N .@ "internal") ⊆ E →
(γ ⤇½ n ∗ γ ⤇[q] n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ γ ⤇[q] (n + 1) ∗ Q) -∗
@@ -221,7 +221,7 @@ Section cnt_spec.
Proof.
iIntros (Hsubset) "#HVS".
iApply wk_incr_spec; done.
-Qed.
+Qed.
End cnt_spec.
Global Opaque newcounter incr read wk_incr.
@@ -229,21 +229,21 @@ Global Opaque newcounter incr read wk_incr.
Section incr_twice.
Context `{!heapG Σ, !cntG Σ} (N : namespace).
Definition incr_twice : val := λ: "ℓ", incr "ℓ" ;; incr "ℓ".
-
+
Theorem incr_twice_spec (γ : gname) (E : coPset) (P : iProp Σ) (Q Q' : Z → iProp Σ) (ℓ : loc):
↑(N .@ "internal") ⊆ E →
(∀ (n : Z), (γ ⤇½ n ∗ P ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q n))
- -∗
+ -∗
(∀ (n : Z), γ ⤇½ n ∗ (∃ m, Q m) ={E ∖ ↑(N .@ "internal")}=> γ ⤇½ (n+1) ∗ Q' n)
-∗
{{{ Cnt N ℓ γ ∗ P }}} incr_twice #ℓ @ E {{{ (m : Z), RET #m; Cnt N ℓ γ ∗ Q' m}}}.
Proof.
iIntros (?) "#HVS1 #HVS2 !#".
iIntros (Φ) "HPre HΦ".
- wp_let. wp_bind (incr _)%E.
+ wp_lam. wp_bind (incr _)%E.
wp_apply (incr_spec with "HVS1 HPre"); auto.
iIntros (m) "[HCnt HPre]".
- wp_let.
+ wp_seq.
wp_apply (incr_spec with "HVS2 [$HCnt HPre]"); auto.
Qed.
End incr_twice.
@@ -279,10 +279,10 @@ Section example_1.
}
wp_let.
wp_bind (_ ||| _)%E.
- let tac := iApply ("HIncr" with "[$HInc]"); iNext; by iIntros (?) "_" in
+ let tac := iApply ("HIncr" with "[$HInc]"); iNext; by iIntros (?) "_" in
iApply (wp_par (λ _, True%I) (λ _, True%I)); [tac | tac | ].
{ iIntros (v1 v2) "_ !>".
- wp_let.
+ wp_seq.
wp_apply (read_spec _ _ _ True%I (λ _, True%I)); auto.
iIntros (n) "!# [Hown _] !>"; by iFrame.
}
diff --git a/theories/lecture_notes/recursion_through_the_store.v b/theories/lecture_notes/recursion_through_the_store.v
index 1c7def59de09d6c80503ccd6b94bf79d436d37c3..a69b7c1eb9e9358464f882fab8c9023b6fea7285 100644
--- a/theories/lecture_notes/recursion_through_the_store.v
+++ b/theories/lecture_notes/recursion_through_the_store.v
@@ -50,19 +50,18 @@ Definition myrec : val :=
(* Here is the specification for the recursion through the store function.
See the Iris Lecture Notes for an in-depth discussion of both the specification and
the proof. *)
-Lemma myrec_spec (P: val -> iProp Σ) (Q: val -> val -> iProp Σ) (F v1: val) (e_F e_v : expr) :
- IntoVal e_F F → IntoVal e_v v1 →
+Lemma myrec_spec (P: val -> iProp Σ) (Q: val -> val -> iProp Σ) (F v1: val) :
{{{
- ( ∀e_f:expr,∀f : val, ∀v2:val, ⌜IntoVal e_f f⌠-∗ {{{(∀ v3 :val, {{{P v3 }}} e_f v3 {{{u, RET u; Q u v3 }}})
+ ( ∀f : val, ∀v2:val, {{{(∀ v3 :val, {{{P v3 }}} f v3 {{{u, RET u; Q u v3 }}})
∗ P v2 }}}
- F e_f v2
+ F f v2
{{{u, RET u; Q u v2}}})
∗ P v1
}}}
-myrec e_F e_v
+myrec F v1
{{{u, RET u; Q u v1}}}.
Proof.
- iIntros (<- <- Ï•) "[#H P] Q".
+ iIntros (Ï•) "[#H P] Q".
wp_lam.
wp_alloc r as "r".
wp_let.
@@ -71,12 +70,12 @@ Proof.
iMod (inv_alloc (nroot.@"myrec") _ _ with "[r]") as "#inv"; first by iNext; iExact "r".
iAssert (▷ ∀ u : val, Q u v1 -∗ ϕ u)%I with "[Q]" as "Q"; first done.
iLöb as "IH" forall(v1 ϕ).
- wp_let.
+ wp_lam.
wp_bind (! _)%E.
iInv (nroot.@"myrec") as "r" "cl".
wp_load.
iMod ("cl" with "[r]") as "_"; first done. iModIntro.
- iApply ("H" with "[][P]"); first (iIntros "!%"; apply _); last done.
+ iApply ("H" with "[P]"); last done.
iFrame. iIntros (v3).
iAlways. iIntros (Φ) "P Q". iApply ("IH" with "[P][Q]"); done.
Qed.
@@ -138,7 +137,7 @@ Section factorial_client.
Proof.
iLöb as "IH".
iIntros (n Φ) "ret".
- wp_lam. wp_lam.
+ wp_lam. wp_let.
wp_binop.
case_bool_decide; simplify_eq/=.
- wp_if. iApply "ret".
@@ -175,17 +174,17 @@ Section factorial_client.
(* Finally, here is the specification that our implementation of factorial
really does implement the mathematical factorial function. *)
- Lemma myfac_spec (n: expr) (n': Z):
- IntoVal n #n' → (0 ≤ n') →
+ Lemma myfac_spec (n: Z):
+ (0 ≤ n) →
{{{ True}}}
- myfac n
- {{{v, RET v; ⌜v = #(fac_int n')âŒ}}}.
+ myfac #n
+ {{{v, RET v; ⌜v = #(fac_int n)âŒ}}}.
Proof.
- iIntros (<- Hleq Φ) "_ ret"; simplify_eq.
+ iIntros (Hleq Φ) "_ ret"; simplify_eq. unfold myfac. wp_pures.
iApply (myrec_spec (fun v => ⌜∃m' : Z, 0 ≤ m' ∧ to_val v = Some #m'âŒ%I)
(fun u => fun v => ⌜∃m' : Z, to_val v = Some #m' ∧ u = #(fac_int m')âŒ%I)).
- - iSplit; last eauto. iIntros (e_f f v <-). iAlways. iIntros (Φ') "spec_f ret".
- wp_lam. wp_lam. iDestruct "spec_f" as "[spec_f %]".
+ - iSplit; last eauto. iIntros (f v). iAlways. iIntros (Φ') "spec_f ret".
+ wp_lam. wp_let. iDestruct "spec_f" as "[spec_f %]".
destruct H as [m' [Hleqm' Heq%of_to_val]]; simplify_eq.
wp_binop.
case_bool_decide; simplify_eq/=; wp_if.
diff --git a/theories/lecture_notes/stack.v b/theories/lecture_notes/stack.v
index a2ee5d4712f86c29159da817913cbe2ae8246dcd..936f98b95bc6aa6cd54e43cc327f18fc1d8d21ae 100644
--- a/theories/lecture_notes/stack.v
+++ b/theories/lecture_notes/stack.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type".
(* ---------------------------------------------------------------------- *)
-Section stack_code.
+Section stack_code.
(* This section contains the code of the stack functions we specify *)
Definition new_stack : val := λ: <>, ref NONEV.
@@ -29,7 +29,7 @@ Section stack_code.
let: "x" := Fst "p" in
"s" <- Snd "p" ;; SOME "x"
end).
-End stack_code.
+End stack_code.
(* ---------------------------------------------------------------------- *)
@@ -59,14 +59,14 @@ Section stack_spec.
The specifications and proofs are explained in the Iris Lecture Notes
*)
Context `{!heapG Σ}.
-
+
Lemma new_stack_spec:
{{{ True }}}
new_stack #()
{{{ s, RET s; is_stack s [] }}}.
Proof.
iIntros (ϕ) "_ HΦ".
- wp_let.
+ wp_lam.
wp_alloc â„“ as "Hpt".
iApply "HΦ".
iExists â„“, NONEV.
@@ -80,9 +80,10 @@ Section stack_spec.
Proof.
iIntros (ϕ) "Hstack HΦ".
iDestruct "Hstack" as (â„“ hd ->) "[Hpt Hlist]".
- wp_lam; wp_lam.
+ wp_lam. wp_let.
wp_load.
- wp_let.
+ wp_let.
+ wp_pair.
wp_let.
wp_alloc â„“' as "Hptâ„“'".
wp_store.
@@ -90,7 +91,7 @@ Section stack_spec.
iExists â„“, (SOMEV #â„“'); iFrame.
iSplitR; first done.
iExists â„“', hd; by iFrame.
- Qed.
+ Qed.
Lemma pop_spec_nonempty s (x : val) xs:
{{{ is_stack s (x :: xs) }}}
@@ -102,7 +103,7 @@ Section stack_spec.
iDestruct "Hlist" as (â„“' hd' ->) "[Hptâ„“' Hlist]".
wp_lam.
wp_load.
- wp_let.
+ wp_let.
wp_match.
wp_load.
wp_let.
@@ -110,9 +111,10 @@ Section stack_spec.
wp_let.
wp_proj.
wp_store.
+ wp_pures.
iApply "HΦ".
iExists â„“, hd'; by iFrame.
- Qed.
+ Qed.
Lemma pop_spec_empty s:
{{{ is_stack s [] }}}
@@ -123,11 +125,10 @@ Section stack_spec.
iDestruct "Hstack" as (â„“ hd ->) "[Hpt %]"; subst.
wp_lam.
wp_load.
- wp_let.
- wp_match.
+ wp_pures.
iApply "HΦ".
iExists â„“, NONEV; by iFrame.
- Qed.
+ Qed.
End stack_spec.
@@ -155,14 +156,14 @@ Section stack_ownership_spec.
The specifications and proofs are explained in the Iris Lecture Notes
*)
Context `{!heapG Σ}.
-
+
Lemma newstack_ownership_spec:
{{{ True }}}
new_stack #()
{{{ s, RET s; is_stack s [] }}}.
Proof.
iIntros (ϕ) "_ HΦ".
- wp_let.
+ wp_lam.
wp_alloc â„“ as "Hpt".
iApply "HΦ".
iExists â„“, NONEV.
@@ -176,17 +177,15 @@ Lemma push_ownership_spec s Φ Φs (x : val):
Proof.
iIntros (Ψ) "[Hstack HΦx] HΨ".
iDestruct "Hstack" as (â„“ hd ->) "[Hpt Hlist]".
- wp_lam; wp_lam.
+ wp_lam; wp_let.
wp_load.
- wp_let.
- wp_let.
wp_alloc â„“' as "Hptâ„“'".
wp_store.
iApply "HΨ".
iExists â„“, (SOMEV #â„“'); iFrame.
iSplitR; first done.
iExists â„“', x, hd; by iFrame.
-Qed.
+Qed.
Lemma pop_ownership_spec_nonempty s Φ Φs:
{{{ is_stack_own s (Φ :: Φs) }}}
@@ -198,7 +197,7 @@ Proof.
iDestruct "Hlist" as (ℓ' x hd' ->) "[Hptℓ' [HΦ Hlist]]".
wp_lam.
wp_load.
- wp_let.
+ wp_let.
wp_match.
wp_load.
wp_let.
@@ -206,10 +205,11 @@ Proof.
wp_let.
wp_proj.
wp_store.
+ wp_inj.
iApply "HΨ".
iFrame "HΦ".
iExists â„“, hd'; by iFrame.
-Qed.
+Qed.
Lemma pop_ownership_spec_empty s:
{{{ is_stack s [] }}}
@@ -220,14 +220,13 @@ Proof.
iDestruct "Hstack" as (â„“ hd ->) "[Hpt %]"; subst.
wp_lam.
wp_load.
- wp_let.
- wp_match.
+ wp_pures.
iApply "HΦ".
iExists â„“, NONEV; by iFrame.
-Qed.
+Qed.
End stack_ownership_spec.
(* Exercise 1: Derive the other specifications from the lecture notes.
Exercise 2: Derive the first specification from the second. That is, from is_stack_own define is_stack, and reprove all the methods in section stack_spec from the specifications in stack_ownership_spec.
- *)
\ No newline at end of file
+ *)
diff --git a/theories/logatom_stack/hocap_spec.v b/theories/logatom_stack/hocap_spec.v
index 1ef0a8b39cddd4db58c548ed49b4f89e54e860c1..3d8001fde8987ef7d731f6661ecdbe15bc204194 100644
--- a/theories/logatom_stack/hocap_spec.v
+++ b/theories/logatom_stack/hocap_spec.v
@@ -48,11 +48,10 @@ Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
(* -- operation specs -- *)
new_stack_spec N :
{{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s ∗ stack_content_frag γs [] }}};
- push_spec N γs s e v (Φ : val → iProp Σ) :
- IntoVal e v →
+ push_spec N γs s (v : val) (Φ : val → iProp Σ) :
is_stack N γs s -∗
make_laterable (∀ l, stack_content_auth γs l ={⊤∖↑N}=∗ stack_content_auth γs (v::l) ∗ Φ #()) -∗
- WP push (s, e) {{ Φ }};
+ WP push s v {{ Φ }};
pop_spec N γs s (Φ : val → iProp Σ) :
is_stack N γs s -∗
make_laterable (∀ l, stack_content_auth γs l ={⊤∖↑N}=∗
@@ -92,14 +91,13 @@ interface. *)
Section hocap_logatom.
Context `{!heapG Σ} (stack: hocap_stack Σ).
- Lemma logatom_push N γs s e v :
- IntoVal e v →
+ Lemma logatom_push N γs s (v : val) :
stack.(is_stack) N γs s -∗
<<< ∀ l : list val, stack.(stack_content_frag) γs l >>>
- stack.(push) (s, e) @ ⊤∖↑N
+ stack.(push) s v @ ⊤∖↑N
<<< stack.(stack_content_frag) γs (v::l), RET #() >>>.
Proof.
- iIntros (?) "Hstack". iApply wp_atomic_intro. iIntros (Φ) "HΦ".
+ iIntros "Hstack". iApply wp_atomic_intro. iIntros (Φ) "HΦ".
iApply (push_spec with "Hstack").
iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
@@ -172,13 +170,12 @@ Section logatom_hocap.
iApply inv_alloc. eauto with iFrame.
Qed.
- Lemma hocap_push N γs s e v (Φ : val → iProp Σ) :
- IntoVal e v →
+ Lemma hocap_push N γs s (v : val) (Φ : val → iProp Σ) :
hocap_is_stack N γs s -∗
make_laterable (∀ l, hocap_stack_content_auth γs l ={⊤∖↑N}=∗ hocap_stack_content_auth γs (v::l) ∗ Φ #()) -∗
- WP stack.(logatom.push) (s, e) {{ Φ }}.
+ WP stack.(logatom.push) s v {{ Φ }}.
Proof using Type*.
- iIntros (?) "#[Hstack Hwrap] Hupd". iApply (logatom.push_spec with "Hstack"); first iAccu.
+ iIntros "#[Hstack Hwrap] Hupd". iApply (logatom.push_spec with "Hstack"); first iAccu.
iAuIntro. iInv "Hwrap" as (l) "[>Hcont >Hâ—]".
iAaccIntro with "Hcont"; first by eauto 10 with iFrame.
iIntros "Hcont".
diff --git a/theories/logatom_stack/spec.v b/theories/logatom_stack/spec.v
index b258c3b49f8f27e23f61944ce4e741fb4603f36b..7cd3c880d9bba034052b3ed7ab48922f8cfd3208 100644
--- a/theories/logatom_stack/spec.v
+++ b/theories/logatom_stack/spec.v
@@ -22,11 +22,10 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
(* -- operation specs -- *)
new_stack_spec N :
{{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s ∗ stack_content γs [] }}};
- push_spec N γs s e v :
- IntoVal e v →
+ push_spec N γs s (v : val) :
is_stack N γs s -∗
<<< ∀ l : list val, stack_content γs l >>>
- push (s, e) @ ⊤∖↑N
+ push s v @ ⊤∖↑N
<<< stack_content γs (v::l), RET #() >>>;
pop_spec N γs s :
is_stack N γs s -∗
diff --git a/theories/logatom_stack/stack.v b/theories/logatom_stack/stack.v
index 8630239e23156ec7b2e6b8bb7d513c6ca2fc83fc..3b6f78b8596a4337d3e9267dea567860bb743695 100644
--- a/theories/logatom_stack/stack.v
+++ b/theories/logatom_stack/stack.v
@@ -42,9 +42,7 @@ Section stack.
("head", "offer").
Definition push : val :=
- rec: "push" "args" :=
- let: "stack" := Fst "args" in
- let: "val" := Snd "args" in
+ rec: "push" "stack" "val" :=
let: "head_old" := !(Fst "stack") in
let: "head_new" := ref ("val", "head_old") in
if: CAS (Fst "stack") "head_old" (SOME "head_new") then #() else
@@ -57,7 +55,7 @@ Section stack.
(Snd "stack") <- NONE ;;
if: CAS "state" #0 #2 then
(* We retracted the offer. Just try the entire thing again. *)
- "push" "args"
+ "push" "stack" "val"
else
(* Someone took the offer. We are done. *)
#().
@@ -180,20 +178,19 @@ Section stack.
{ apply auth_valid_discrete_2. split; done. }
iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
{ iNext. iExists None, None, _. iFrame. done. }
- iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
+ wp_pures. iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
Qed.
- Lemma push_spec γs s e v :
- IntoVal e v →
+ Lemma push_spec γs s (v : val) :
is_stack γs s -∗
<<< ∀ l : list val, stack_content γs l >>>
- push (s, e) @ ⊤∖↑N
+ push s v @ ⊤∖↑N
<<< stack_content γs (v::l), RET #() >>>.
Proof.
- iIntros (<-) "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "AU".
+ iIntros "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "AU".
iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
iLöb as "IH".
- wp_let. wp_proj. wp_let. wp_proj. wp_let. wp_proj.
+ wp_lam.
(* Load the old head. *)
wp_apply (load_spec with "[AU]"); first by iAccu.
iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs◠& >H↦ & Hrem)".
@@ -202,7 +199,6 @@ Section stack.
iIntros "!> AU". clear offer_rep l.
(* Go on. *)
wp_let. wp_apply alloc_spec; first done. iIntros (head_new) "Hhead_new".
- wp_let. wp_proj.
(* CAS to change the head. *)
wp_apply cas_spec; [by destruct stack_rep|iAccu|].
iAuIntro. iInv stackN as (stack_rep' offer_rep l) "(>Hs◠& >H↦ & Hlist & Hoffer)".
@@ -225,7 +221,6 @@ Section stack.
clear stack_rep stack_rep' offer_rep l head_new.
iIntros "H". wp_if.
wp_apply alloc_spec; first done. iIntros (st_loc) "Hoffer_st".
- wp_let. wp_let. wp_proj.
(* Make the offer *)
wp_apply store_spec; first by iAccu.
iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs◠& >H↦ & Hlist & >Hoffer↦ & Hoffer)".
@@ -238,9 +233,9 @@ Section stack.
{ iClear "Hoffer". iExists _, (Some (v, st_loc)), _. iFrame.
rewrite /is_offer /=. iExists _, _, _. iFrame "AU_back Hoinv". done. }
clear stack_rep offer_rep l.
- iIntros "!> _". wp_let.
+ iIntros "!> _".
(* Retract the offer. *)
- wp_proj. wp_apply store_spec; first by iAccu.
+ wp_apply store_spec; first by iAccu.
iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs◠& >H↦ & Hlist & >Hoffer↦ & Hoffer)".
iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.
iIntros "?". iSplitR "Htok".
@@ -279,8 +274,7 @@ Section stack.
Proof.
iIntros "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "AU".
iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
- iLöb as "IH".
- wp_let. wp_proj.
+ iLöb as "IH". wp_lam. wp_pures.
(* Load the old head *)
wp_apply load_spec; first by iAccu.
iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs◠& >H↦ & Hlist & Hrem)".
@@ -294,14 +288,14 @@ Section stack.
%[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
iMod ("Hclose" with "Hl'") as "HΦ".
iSplitR "HΦ"; first by eauto 10 with iFrame.
- iIntros "!> _". wp_match. by iApply "HΦ".
+ iIntros "!> _". wp_pures. by iApply "HΦ".
- (* Non-empty list, let's try to pop. *)
iDestruct "Hlist" as (tail q rep) "[>% [[Htail Htail2] Hlist]]". subst stack_rep.
iSplitR "AU Htail"; first by eauto 15 with iFrame.
clear offer_rep l.
iIntros "!> _". wp_match.
wp_apply (atomic_wp_seq $! (load_spec _) with "Htail").
- iIntros "Htail". wp_let. wp_proj. wp_proj.
+ iIntros "Htail". wp_pures.
(* CAS to change the head *)
wp_apply cas_spec; [done|iAccu|].
iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs◠& >H↦ & Hlist & Hrem)".
@@ -324,7 +318,7 @@ Section stack.
iMod ("Hclose" with "Hl'") as "HΦ {Htail Htail'}".
iSplitR "HΦ"; first by eauto 10 with iFrame.
iIntros "!> _". clear q' q offer_rep l.
- wp_if. wp_proj. by iApply "HΦ".
+ wp_pures. by iApply "HΦ".
+ (* CAS failed. Go on looking for an offer. *)
iSplitR "AU"; first by eauto 10 with iFrame.
iIntros "!> _". wp_if. clear rep stack_rep offer_rep l q tail v.
@@ -365,7 +359,7 @@ Section stack.
iMod ("Hclose" with "Hl'") as "HΦ".
iSplitR "Hoff↦ HQoff HΦ"; first by eauto 10 with iFrame. iSplitR "HΦ".
{ iIntros "!> !> !>". iExists OfferAccepted. iFrame. }
- iIntros "!> !> _". wp_if. wp_proj. by iApply "HΦ".
+ iIntros "!> !> _". wp_pures. by iApply "HΦ".
Qed.
End stack.
diff --git a/theories/spanning_tree/mon.v b/theories/spanning_tree/mon.v
index df249ab3b5f19db6109d10bef7fb66ccfcfc437a..4dfce4ea9a0b02ed019b0e6968c613843d3b3abe 100644
--- a/theories/spanning_tree/mon.v
+++ b/theories/spanning_tree/mon.v
@@ -97,11 +97,6 @@ Definition child_to_val (c : option loc) : val :=
Definition children_to_val (ch : option loc * option loc) : val :=
(child_to_val (ch.1), child_to_val (ch.2)).
-Lemma children_to_val_is_val (c c' : option loc) :
- to_val (child_to_val c, child_to_val c') =
- Some (child_to_val c, child_to_val c')%V.
-Proof. by destruct c; destruct c'. Qed.
-
Definition marked_graph := gmap loc (bool * (option loc * option loc)).
Identity Coercion marked_graph_gmap: marked_graph >-> gmap.
diff --git a/theories/spanning_tree/proof.v b/theories/spanning_tree/proof.v
index 81098608287f6187f1a8869213a9181da0e099bc..363d5676427ee7fbfebba44c6af79c7ab7d3c2f4 100644
--- a/theories/spanning_tree/proof.v
+++ b/theories/spanning_tree/proof.v
@@ -30,7 +30,7 @@ Section wp_span.
iIntros (Hgl Hgmx Hgcn) "Hgr".
iMod (graph_ctx_alloc _ g markings with "[Hgr]") as (Ig κ) "(key & #Hgr & Hg)";
eauto.
- iApply wp_fupd.
+ iApply wp_fupd. wp_pures.
iApply wp_wand_l; iSplitR;
[|iApply ((rec_wp_span κ g markings 1 1 (SOMEV #l)) with "[Hg key]");
eauto; iFrame "#"; iFrame].
@@ -66,4 +66,4 @@ Section wp_span.
exfalso; revert Hmrk. rewrite dom_empty. inversion 1.
Qed.
-End wp_span.
\ No newline at end of file
+End wp_span.
diff --git a/theories/spanning_tree/spanning.v b/theories/spanning_tree/spanning.v
index a07adc622e67f41a2474b343c77175e2485033ff..f7a4ccadc097cf46bf6b8932caf39c1d1143aa39 100644
--- a/theories/spanning_tree/spanning.v
+++ b/theories/spanning_tree/spanning.v
@@ -46,7 +46,7 @@ Section Helpers.
}}.
Proof.
iIntros (Hgx) "(#Hgr & Hx & key)".
- wp_let; wp_bind (! _)%E. unfold graph_ctx.
+ wp_lam; wp_bind (! _)%E. unfold graph_ctx.
iMod (cinv_open with "Hgr key") as "(>Hinv & key & Hcl)"; first done.
unfold graph_inv at 2.
iDestruct "Hinv" as (G) "(Hi1 & Hi2 & Hi3 & Hi4)".
@@ -157,13 +157,13 @@ Section Helpers.
(g !! x) = Some v →
(graph_ctx κ g markings ∗ own_graph q (x [↦] w) ∗ cinv_own κ k)
⊢
- WP (#x <- (#m, children_to_val w'))
+ WP (#x <- (#m, children_to_val w')%V)
{{ v, own_graph q (x [↦] w') ∗ cinv_own κ k }}.
Proof.
iIntros (Hagree Hmrk Hgx) "(#Hgr & Hx & key)".
assert (Hgx' : x ∈ dom (gset _) g).
{ rewrite elem_of_dom Hgx; eauto. }
- unfold graph_ctx.
+ unfold graph_ctx. wp_pures.
iMod (cinv_open _ graphN with "Hgr key")
as "(>Hinv & key & Hclose)"; first done.
unfold graph_inv at 2.
@@ -204,13 +204,13 @@ Section Helpers.
{{ _, own_graph q (x [↦] (None, w2)) ∗ cinv_own κ k }}.
Proof.
iIntros (Hgx) "(#Hgr & Hx & key)".
- wp_let. wp_bind (! _)%E.
+ wp_lam. wp_bind (! _)%E.
iApply wp_wand_l; iSplitR;
[|iApply wp_load_graph; eauto; iFrame "Hgr"; by iFrame].
iIntros (u) "(H1 & Hagree & Hx & key)". iDestruct "H1" as (m) "[Hmrk Hu]".
iDestruct "Hagree" as %Hagree.
iDestruct "Hmrk" as %Hmrk; iDestruct "Hu" as %Hu; subst.
- wp_let. do 3 wp_proj.
+ wp_pures.
iApply (wp_store_graph _ (None, w2) with "[Hx key]"); eauto;
[|iFrame "Hgr"; by iFrame].
{ by destruct w1; destruct w2; destruct v; inversion Hagree; subst. }
@@ -224,13 +224,13 @@ Section Helpers.
{{ _, own_graph q (x [↦] (w1, None)) ∗ cinv_own κ k }}.
Proof.
iIntros (Hgx) "(#Hgr & Hx & key)".
- wp_let. wp_bind (! _)%E.
+ wp_lam. wp_bind (! _)%E.
iApply wp_wand_l; iSplitR;
[|iApply wp_load_graph; eauto; iFrame "Hgr"; by iFrame].
iIntros (u) "(H1 & Hagree & Hx & key)". iDestruct "H1" as (m) "[Hmrk Hu]".
iDestruct "Hagree" as %Hagree.
iDestruct "Hmrk" as %Hmrk; iDestruct "Hu" as %Hu; subst.
- wp_let. wp_bind (Fst _). do 3 wp_proj.
+ wp_pures.
iApply (wp_store_graph _ (w1, None) with "[Hx key]"); eauto;
[|iFrame "Hgr"; by iFrame].
{ by destruct w1; destruct w2; destruct v; inversion Hagree; subst. }
@@ -329,7 +329,7 @@ Section Helpers.
[|iApply wp_load_graph; eauto; iFrame "Hgr"; by iFrame].
iIntros (v) "(H1 & Hagree & Hx & key)". iDestruct "H1" as (m) "[Hmrk Hv]".
iDestruct "Hagree" as %Hagree. iDestruct "Hv" as %Hv; subst v.
- wp_let. wp_bind (par _).
+ wp_let. wp_pures. wp_bind (par _ _).
iDestruct "key" as "[K1 K2]".
iDestruct (empty_graph_divide with "Hx1") as "[Hx11 Hx12]".
destruct u as [u1 u2]. iApply (par_spec with "[Hx11 K1] [Hx12 K2]").
@@ -359,7 +359,7 @@ Section Helpers.
(* separating all four cases *)
iDestruct "Hvl" as "[[% Hvll]|[% Hvlr]]"; subst;
iDestruct "Hvr" as "[[% Hvrl]|[% Hvrr]]"; subst.
- - wp_proj. wp_op. wp_if; wp_seq. wp_proj. wp_op. wp_if. wp_seq.
+ - wp_pures.
iDestruct "Hvll" as (l1) "(Hl1eq & Hg1 & ml1)".
iDestruct "Hg1" as (G1 mr1 tr1) "(Hxl & Hl1im & Hmx1 & Hfr1 & Hfml)".
iDestruct "Hfr1" as %Hfr1. iDestruct "Hmx1" as %Hmx1.
@@ -383,7 +383,7 @@ Section Helpers.
{ rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
split; auto.
{ eapply maximally_marked_tree_both; eauto. }
- - wp_proj. wp_op. wp_if. wp_seq. wp_proj. wp_op. wp_if.
+ - wp_pures.
iDestruct "Hvll" as (l1) "(Hl1eq & Hg1 & ml1)".
iDestruct "Hg1" as (G1 mr1 tr1) "(Hxl & Hl1im & Hmx1 & Hfr1 & Hfml)".
iDestruct "Hfr1" as %Hfr1. iDestruct "Hmx1" as %Hmx1.
@@ -416,7 +416,7 @@ Section Helpers.
{ rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
split; auto.
{ eapply maximally_marked_tree_left; eauto. }
- - wp_proj. wp_op. wp_if.
+ - wp_pures.
iDestruct "Hvlr" as "(Hvl & Hxl)".
iDestruct "Hvrl" as (l2) "(Hl2eq & Hg2 & ml2)".
iDestruct "Hg2" as (G2 mr2 tr2) "(Hxr & Hl2im & Hmx2 & Hfr2 & Hfmr)".
@@ -490,4 +490,4 @@ Section Helpers.
{ eapply maximally_marked_tree_none; eauto. }
Qed.
-End Helpers.
\ No newline at end of file
+End Helpers.