par_inc.v 2.09 KB
 Robbert Krebbers committed Nov 14, 2018 1 2 3 ``````From iris_c.vcgen Require Import proofmode. From iris.algebra Require Import frac_auth. `````` Robbert Krebbers committed Nov 15, 2018 4 ``````Definition inc : val := λᶜ "l", `````` Robbert Krebbers committed Nov 16, 2018 5 `````` c_ret "l" +=ᶜ ♯ 1 ;ᶜ ♯ 1. `````` Robbert Krebbers committed Nov 14, 2018 6 `````` `````` Robbert Krebbers committed Nov 15, 2018 7 ``````Definition par_inc : val := λᶜ "l", `````` Robbert Krebbers committed Nov 16, 2018 8 `````` callᶜ (c_ret inc) (c_ret "l") +ᶜ callᶜ (c_ret inc) (c_ret "l"). `````` Robbert Krebbers committed Nov 14, 2018 9 10 `````` Section par_inc. `````` Robbert Krebbers committed Nov 16, 2018 11 `````` Context `{cmonadG Σ, !inG Σ (frac_authR natR)}. `````` Robbert Krebbers committed Nov 14, 2018 12 13 14 `````` Lemma inc_spec R cl (n : Z) Φ : cl ↦C #n -∗ (cl ↦C #(1 + n) -∗ Φ #1) -∗ `````` Robbert Krebbers committed Nov 16, 2018 15 `````` CWP inc (cloc_to_val cl) @ R {{ Φ }}. `````` Robbert Krebbers committed Nov 15, 2018 16 `````` Proof. `````` Robbert Krebbers committed Nov 16, 2018 17 `````` iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H". `````` Robbert Krebbers committed Nov 15, 2018 18 `````` Qed. `````` Robbert Krebbers committed Nov 14, 2018 19 20 21 `````` Lemma par_inc_spec R cl (n : Z) : cl ↦C #n -∗ `````` Robbert Krebbers committed Nov 16, 2018 22 `````` CWP par_inc (cloc_to_val cl) @ R {{ v, ⌜ v = #2 ⌝ ∧ cl ↦C #(2 + n) }}. `````` Robbert Krebbers committed Nov 14, 2018 23 `````` Proof. `````` Robbert Krebbers committed Mar 16, 2019 24 `````` iIntros "Hl". iApply cwp_fun; simpl. `````` Hai Dang committed May 25, 2019 25 26 `````` iMod (own_alloc (●! 0%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [by apply auth_both_valid|]. `````` Robbert Krebbers committed Nov 14, 2018 27 `````` set (par_inc_inv := (∃ n' : nat, cl ↦C #(n' + n) ∗ own γ (●! n'))%I). `````` Robbert Krebbers committed Nov 16, 2018 28 `````` iApply (cwp_insert_res _ _ par_inc_inv with "[Hγ Hl]"). `````` Robbert Krebbers committed Nov 14, 2018 29 30 `````` { iExists 0%nat. iFrame. } iAssert (□ (own γ (◯!{1 / 2} 0%nat) -∗ `````` Robbert Krebbers committed Nov 16, 2018 31 `````` CWP callᶜ (c_ret inc) (c_ret (cloc_to_val cl)) @ par_inc_inv ∗ R `````` Robbert Krebbers committed Nov 14, 2018 32 `````` {{ v, ⌜v = #1⌝ ∧ own γ (◯!{1 / 2} 1%nat) }}))%I as "#H". `````` Dan Frumin committed Feb 01, 2019 33 `````` { iIntros "!> Hγ'". vcg; iIntros "[HR \$] !> !>". iDestruct "HR" as (n') "[Hl Hγ]". `````` Robbert Krebbers committed Nov 16, 2018 34 `````` iApply cwp_fupd. iApply (inc_spec with "[\$]"); iIntros "Hl". `````` Robbert Krebbers committed Nov 14, 2018 35 36 37 38 `````` 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. } `````` Robbert Krebbers committed Nov 16, 2018 39 `````` iApply (cwp_bin_op _ _ (λ v, ⌜ v = #1 ⌝ ∧ own γ (◯!{1 / 2} 1%nat))%I `````` Robbert Krebbers committed Nov 14, 2018 40 41 42 43 44 `````` (λ 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γ'". `````` Robbert Krebbers committed Nov 15, 2018 45 `````` iDestruct (own_valid_2 with "Hγ Hγ'") as %->%frac_auth_agreeL. iFrame; auto. `````` Robbert Krebbers committed Nov 14, 2018 46 `````` Qed. `````` Dan Frumin committed Feb 01, 2019 47 ``End par_inc.``