Commit c18dc76f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Update coq-iris : R2L evaluation, curry functions, Val constructor.

parent 288dbd0c
Pipeline #12588 failed with stage
in 13 minutes and 26 seconds
......@@ -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" }
]
......@@ -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"). }
......
......@@ -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.
......
......@@ -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.
......
......@@ -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|_.
......
......@@ -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]]]".
......
......@@ -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 |}.
......@@ -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.
......
......@@ -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". }
......
......@@ -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.
......
......@@ -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. }
......
......@@ -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
......
......@@ -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|].