counter.v 7.21 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
From iris.heap_lang Require Export lang.
3
From iris.proofmode Require Import tactics.
4
From iris.algebra Require Import frac auth.
5 6 7 8 9
From iris.heap_lang Require Import proofmode notation.

Definition newcounter : val := λ: <>, ref #0.
Definition inc : val :=
  rec: "inc" "l" :=
10 11 12
    let: "n" := !"l" in
    if: CAS "l" "n" (#1 + "n") then #() else "inc" "l".
Definition read : val := λ: "l", !"l".
13 14
Global Opaque newcounter inc get.

15 16 17
(** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
Definition mcounterΣ : gFunctors := #[GFunctor (constRF (authR mnatUR))].
18

19
Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ  mcounterG Σ.
20
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
21

22 23 24 25 26 27 28 29 30 31 32 33 34 35
Section mono_proof.
  Context `{!heapG Σ, !mcounterG Σ} (N : namespace).

  Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
    ( n, own γ ( (n : mnat))  l  #n)%I.

  Definition mcounter (l : loc) (n : nat) : iProp Σ :=
    ( γ, heapN  N  heap_ctx 
          inv N (mcounter_inv γ l)  own γ ( (n : mnat)))%I.

  (** The main proofs. *)
  Global Instance mcounter_persistent l n : PersistentP (mcounter l n).
  Proof. apply _. Qed.

36
  Lemma newcounter_mono_spec (R : iProp Σ) :
37
    heapN  N 
38
    {{{ heap_ctx }}} newcounter #() {{{ l; #l, mcounter l 0 }}}.
39
  Proof.
40
    iIntros (? Φ) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
41 42
    iMod (own_alloc ( (O:mnat)   (O:mnat))) as (γ) "[Hγ Hγ']"; first done.
    iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
43
    { iNext. iExists 0%nat. by iFrame. }
44
    iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
45 46
  Qed.

47 48
  Lemma inc_mono_spec l n :
    {{{ mcounter l n }}} inc #l {{{; #(), mcounter l (S n) }}}.
49
  Proof.
50
    iIntros (Φ) "[Hl HΦ]". iLöb as "IH". wp_rec.
51 52
    iDestruct "Hl" as (γ) "(% & #? & #Hinv & Hγf)".
    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
53 54
    wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
    iModIntro. wp_let. wp_op.
55 56 57 58
    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
    destruct (decide (c' = c)) as [->|].
    - iDestruct (own_valid_2 with "[$Hγ $Hγf]")
        as %[?%mnat_included _]%auth_valid_discrete_2.
59
      iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
60
      { apply auth_update, (mnat_local_update _ _ (S c)); auto. } 
61
      wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
62
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
63
      iModIntro. wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
64 65 66
      iApply (own_mono with "Hγf"). apply: auth_frag_mono.
      by apply mnat_included, le_n_S.
    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
67 68
      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
      iModIntro. wp_if. iApply ("IH" with "[Hγf] HΦ").
69 70 71
      rewrite {3}/mcounter; eauto 10.
  Qed.

72 73
  Lemma read_mono_spec l j :
    {{{ mcounter l j }}} read #l {{{ i; #i,  (j  i)%nat  mcounter l i }}}.
74
  Proof.
75
    iIntros (ϕ) "[Hc HΦ]". iDestruct "Hc" as (γ) "(% & #? & #Hinv & Hγf)".
76 77
    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
    iDestruct (own_valid_2 with "[$Hγ $Hγf]")
78
      as %[?%mnat_included _]%auth_valid_discrete_2.
79
    iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
80
    { apply auth_update, (mnat_local_update _ _ c); auto. }
81
    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
82
    iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
  Qed.
End mono_proof.

(** Counter with contributions *)
Class ccounterG Σ :=
  CCounterG { ccounter_inG :> inG Σ (authR (optionUR (prodR fracR natR))) }.
Definition ccounterΣ : gFunctors :=
  #[GFunctor (constRF (authR (optionUR (prodR fracR natR))))].

Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ  ccounterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.

Section contrib_spec.
  Context `{!heapG Σ, !ccounterG Σ} (N : namespace).

  Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
    ( n, own γ ( Some (1%Qp, n))  l  #n)%I.

  Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
    (heapN  N  heap_ctx  inv N (ccounter_inv γ l))%I.

  Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
    own γ ( Some (q, n)).

  (** The main proofs. *)
  Lemma ccounter_op γ q1 q2 n1 n2 :
    ccounter γ (q1 + q2) (n1 + n2)  ccounter γ q1 n1 ccounter γ q2 n2.
  Proof. by rewrite /ccounter -own_op -auth_frag_op. Qed.

112
  Lemma newcounter_contrib_spec (R : iProp Σ) :
113
    heapN  N 
114 115
    {{{ heap_ctx }}} newcounter #()
    {{{ γ l; #l, ccounter_ctx γ l  ccounter γ 1 0 }}}.
116
  Proof.
117
    iIntros (? Φ) "[#Hh HΦ]". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
118
    iMod (own_alloc ( (Some (1%Qp, O%nat))   (Some (1%Qp, 0%nat))))
119
      as (γ) "[Hγ Hγ']"; first done.
120
    iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
121
    { iNext. iExists 0%nat. by iFrame. }
122
    iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
123 124
  Qed.

125 126 127
  Lemma inc_contrib_spec γ l q n :
    {{{ ccounter_ctx γ l  ccounter γ q n }}} inc #l
    {{{; #(), ccounter γ q (S n) }}}.
128
  Proof.
129
    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)". iLöb as "IH". wp_rec.
130
    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]" "Hclose".
131 132
    wp_load. iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
    iModIntro. wp_let. wp_op.
133 134
    wp_bind (CAS _ _ _). iInv N as (c') ">[Hγ Hl]" "Hclose".
    destruct (decide (c' = c)) as [->|].
135
    - iMod (own_update_2 with "[$Hγ $Hγf]") as "[Hγ Hγf]".
136 137
      { apply auth_update, option_local_update, prod_local_update_2.
        apply (nat_local_update _ _ (S c) (S n)); omega. }
138
      wp_cas_suc. iMod ("Hclose" with "[Hl Hγ]") as "_".
139
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
140
      iModIntro. wp_if. by iApply "HΦ".
141
    - wp_cas_fail; first (by intros [= ?%Nat2Z.inj]).
142 143
      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
      iModIntro. wp_if. by iApply ("IH" with "[Hγf] HΦ").
144 145
  Qed.

146 147 148
  Lemma read_contrib_spec γ l q n :
    {{{ ccounter_ctx γ l  ccounter γ q n }}} read #l
    {{{ c; #c,  (n  c)%nat  ccounter γ q n }}}.
149
  Proof.
150
    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)".
151 152 153
    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
    iDestruct (own_valid_2 with "[$Hγ $Hγf]")
      as %[[? ?%nat_included]%Some_pair_included_total_2 _]%auth_valid_discrete_2.
154
    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
155
    iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
156 157
  Qed.

158 159 160
  Lemma read_contrib_spec_1 γ l n :
    {{{ ccounter_ctx γ l  ccounter γ 1 n }}} read #l
    {{{ n; #n, ccounter γ 1 n }}}.
161
  Proof.
162
    iIntros (Φ) "((#(%&?&?) & Hγf) & HΦ)".
163 164 165
    rewrite /read /=. wp_let. iInv N as (c) ">[Hγ Hl]" "Hclose". wp_load.
    iDestruct (own_valid_2 with "[$Hγ $Hγf]") as %[Hn _]%auth_valid_discrete_2.
    apply (Some_included_exclusive _) in Hn as [= ->]%leibniz_equiv; last done.
166
    iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c; by iFrame|].
167 168 169
    by iApply "HΦ".
  Qed.
End contrib_spec.