counter.v 7.26 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
From iris.heap_lang Require Import proofmode notation.

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

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
Section mono_proof.
  Context `{!heapG Σ, !mcounterG Σ} (N : namespace).

  Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
26
    ( n, own γ ( (n : mnat))  l  #n)%I.
27
28
29
30
31
32
33
34
35

  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, RET #l; mcounter l 0 }}}.
39
  Proof.
Ralf Jung's avatar
Ralf Jung committed
40
    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /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 incr_mono_spec l n :
    {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
49
  Proof.
Ralf Jung's avatar
Ralf Jung committed
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
  Lemma read_mono_spec l j :
73
    {{{ mcounter l j }}} read #l {{{ i, RET #i;  (j  i)%nat  mcounter l i }}}.
74
  Proof.
Ralf Jung's avatar
Ralf Jung committed
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
  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 Σ :=
99
    ( n, own γ ( Some (1%Qp, n))  l  #n)%I.
100
101
102
103
104
105
106
107
108

  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 :
109
    ccounter γ (q1 + q2) (n1 + n2)  ccounter γ q1 n1 ccounter γ q2 n2.
110
111
  Proof. by rewrite /ccounter -own_op -auth_frag_op. Qed.

112
  Lemma newcounter_contrib_spec (R : iProp Σ) :
113
    heapN  N 
114
    {{{ heap_ctx }}} newcounter #()
115
    {{{ γ l, RET #l; ccounter_ctx γ l  ccounter γ 1 0 }}}.
116
  Proof.
Ralf Jung's avatar
Ralf Jung committed
117
    iIntros (? Φ) "#Hh HΦ". rewrite -wp_fupd /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
  Lemma incr_contrib_spec γ l q n :
    {{{ ccounter_ctx γ l  ccounter γ q n }}} incr #l
127
    {{{ RET #(); ccounter γ q (S n) }}}.
128
  Proof.
Ralf Jung's avatar
Ralf Jung committed
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
  Lemma read_contrib_spec γ l q n :
147
    {{{ ccounter_ctx γ l  ccounter γ q n }}} read #l
148
    {{{ c, RET #c;  (n  c)%nat  ccounter γ q n }}}.
149
  Proof.
Ralf Jung's avatar
Ralf Jung committed
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
  Lemma read_contrib_spec_1 γ l n :
159
    {{{ ccounter_ctx γ l  ccounter γ 1 n }}} read #l
160
    {{{ n, RET #n; ccounter γ 1 n }}}.
161
  Proof.
Ralf Jung's avatar
Ralf Jung committed
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.