counter.v 7.23 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
      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
Ralf Jung's avatar
Ralf Jung committed
68
      iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
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
      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
Ralf Jung's avatar
Ralf Jung committed
143
      iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
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.