From iris_c.vcgen Require Import proofmode. From iris.algebra Require Import frac_auth. Definition inc : val := λᶜ "l", c_ret "l" +=ᶜ ♯ 1 ;ᶜ ♯ 1. Definition par_inc : val := λᶜ "l", callᶜ (c_ret inc) (c_ret "l") +ᶜ callᶜ (c_ret inc) (c_ret "l"). Section par_inc. Context `{cmonadG Σ, !inG Σ (frac_authR natR)}. Lemma inc_spec R cl (n : Z) Φ : cl ↦C #n -∗ (cl ↦C #(1 + n) -∗ Φ #1) -∗ CWP inc (cloc_to_val cl) @ R {{ Φ }}. Proof. iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H". Qed. Lemma par_inc_spec R cl (n : Z) : cl ↦C #n -∗ 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]]"; [by apply auth_both_valid|]. set (par_inc_inv := (∃ n' : nat, cl ↦C #(n' + n) ∗ own γ (●! n'))%I). iApply (cwp_insert_res _ _ par_inc_inv with "[Hγ Hl]"). { iExists 0%nat. iFrame. } iAssert (□ (own γ (◯!{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". { 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]"). - by iApply "H". - by iApply "H". - iIntros (v1 v2) "[-> Hγ1] [-> Hγ2]". iExists #2; iSplit; first done. iDestruct 1 as (n') ">[Hl Hγ]". iCombine "Hγ1 Hγ2" as "Hγ'". iDestruct (own_valid_2 with "Hγ Hγ'") as %->%frac_auth_agreeL. iFrame; auto. Qed. End par_inc.