par_inc.v 2.09 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
From iris_c.vcgen Require Import proofmode.
From iris.algebra Require Import frac_auth.

4
Definition inc : val := λᶜ "l",
5
  c_ret "l" +=  1 ;  1.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7
Definition par_inc : val := λᶜ "l",
8
  call (c_ret inc) (c_ret "l") + call (c_ret inc) (c_ret "l").
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10

Section par_inc.
11
  Context `{cmonadG Σ, !inG Σ (frac_authR natR)}.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14

  Lemma inc_spec R cl (n : Z) Φ :
    cl C #n - (cl C #(1 + n) - Φ #1) -
15
    CWP inc (cloc_to_val cl) @ R {{ Φ }}.
16
  Proof.
17
    iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H".
18
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
19 20 21

  Lemma par_inc_spec R cl (n : Z) :
    cl C #n -
22
    CWP par_inc (cloc_to_val cl) @ R {{ v,  v = #2   cl C #(2 + n) }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
    iIntros "Hl". iApply cwp_fun; simpl.
Hai Dang's avatar
Hai Dang committed
25 26
    iMod (own_alloc (! 0%nat  ! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]";
      [by apply auth_both_valid|].
Robbert Krebbers's avatar
Robbert Krebbers committed
27
    set (par_inc_inv := ( n' : nat, cl C #(n' + n)  own γ (! n'))%I).
28
    iApply (cwp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30
    { iExists 0%nat. iFrame. }
    iAssert ( (own γ (!{1 / 2} 0%nat) -
31
      CWP call (c_ret inc) (c_ret (cloc_to_val cl)) @ par_inc_inv  R
Robbert Krebbers's avatar
Robbert Krebbers committed
32
      {{ v, v = #1  own γ (!{1 / 2} 1%nat) }}))%I as "#H".
Dan Frumin's avatar
Dan Frumin committed
33
    { iIntros "!> Hγ'". vcg; iIntros "[HR $] !> !>". iDestruct "HR" as (n') "[Hl Hγ]".
34
      iApply cwp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl".
Robbert Krebbers's avatar
Robbert Krebbers committed
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. }
39
    iApply (cwp_bin_op _ _ (λ v,  v = #1   own γ (!{1 / 2} 1%nat))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
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γ'".
45
      iDestruct (own_valid_2 with "Hγ Hγ'") as %->%frac_auth_agreeL. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  Qed.
Dan Frumin's avatar
Dan Frumin committed
47
End par_inc.