Commit 76689257 authored by Ralf Jung's avatar Ralf Jung

bump Iris; fix for frac_auth notation changes

parent dfbfe1bd
Pipeline #17671 canceled with stage
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-06-02.0.2c926d86") | (= "dev") }
"coq-iris" { (= "dev.2019-06-11.8.a51fa3cf") | (= "dev") }
]
......@@ -22,22 +22,22 @@ Section par_inc.
CWP par_inc (cloc_to_val cl) @ R {{ v, v = #2 cl C #(2 + n) }}.
Proof.
iIntros "Hl". iApply cwp_fun; simpl.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]";
iMod (own_alloc (F 0%nat F 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]";
[by apply auth_both_valid|].
set (par_inc_inv := ( n' : nat, cl C #(n' + n) own γ (! n'))%I).
set (par_inc_inv := ( n' : nat, cl C #(n' + n) own γ (F n'))%I).
iApply (cwp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
{ iExists 0%nat. iFrame. }
iAssert ( (own γ (!{1 / 2} 0%nat) -
iAssert ( (own γ (F{1 / 2} 0%nat) -
CWP call (c_ret inc) (c_ret (cloc_to_val cl)) @ par_inc_inv R
{{ v, v = #1 own γ (!{1 / 2} 1%nat) }}))%I as "#H".
{{ v, v = #1 own γ (F{1 / 2} 1%nat) }}))%I as "#H".
{ iIntros "!> Hγ'". vcg; iIntros "[HR $] !> !>". iDestruct "HR" as (n') "[Hl Hγ]".
iApply cwp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl".
iMod (own_update_2 with "Hγ Hγ'") as "[Hγ Hγ']".
{ apply frac_auth_update, (nat_local_update _ _ (S n') 1); lia. }
iModIntro. iSplitL "Hl Hγ"; last vcg_continue; eauto.
iExists (S n'). rewrite Nat2Z.inj_succ -Z.add_1_l -Z.add_assoc. iFrame. }
iApply (cwp_bin_op _ _ (λ v, v = #1 own γ (!{1 / 2} 1%nat))%I
(λ v, v = #1 own γ (!{1 / 2} 1%nat))%I with "[Hγ1] [Hγ2]").
iApply (cwp_bin_op _ _ (λ v, v = #1 own γ (F{1 / 2} 1%nat))%I
(λ v, v = #1 own γ (F{1 / 2} 1%nat))%I with "[Hγ1] [Hγ2]").
- by iApply "H".
- by iApply "H".
- iIntros (v1 v2) "[-> Hγ1] [-> Hγ2]". iExists #2; iSplit; first done.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment