counter.v 7 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
From iris.base_logic.lib Require Export invariants.
3
From iris.heap_lang Require Export lang.
4
From iris.proofmode Require Import tactics.
5
From iris.algebra Require Import frac_auth auth.
6
From iris.heap_lang Require Import proofmode notation lib.compare_and_set.
7
Set Default Proof Using "Type".
8

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

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

19
Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ  mcounterG Σ.
20
Proof. solve_inG. 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

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

  (** The main proofs. *)
32
  Global Instance mcounter_persistent l n : Persistent (mcounter l n).
33 34
  Proof. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
35
  Lemma newcounter_mono_spec :
36
    {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
37
  Proof.
38
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
39
    iMod (own_alloc ( (O:mnat)   (O:mnat))) as (γ) "[Hγ Hγ']";
40
      first by apply auth_both_valid.
41
    iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
42
    { iNext. iExists 0%nat. by iFrame. }
43
    iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
44 45
  Qed.

46 47
  Lemma incr_mono_spec l n :
    {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
48
  Proof.
Ralf Jung's avatar
Ralf Jung committed
49
    iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
50 51
    iDestruct "Hl" as (γ) "[#? Hγf]".
    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
52
    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
53 54
    wp_pures. wp_apply caset_spec; first done.
    iInv N as (c') ">[Hγ Hl]" "Hclose".
55
    destruct (decide (c' = c)) as [->|].
56
    - iDestruct (own_valid_2 with "Hγ Hγf")
57
        as %[?%mnat_included _]%auth_both_valid.
58
      iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
59
      { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
60 61 62 63
      iExists _; iFrame "Hl". iIntros "!> Hl".
      rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. iFrame. }
      iModIntro. wp_if.
64
      iApply "HΦ"; iExists γ; repeat iSplit; eauto.
65 66 67
      iApply (own_mono with "Hγf").
      (* FIXME: FIXME(Coq #6294): needs new unification *)
      apply: auth_frag_mono. by apply mnat_included, le_n_S.
68 69 70 71
    - iExists _; iFrame "Hl". iIntros "!> Hl".
      rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
      iMod ("Hclose" with "[Hl Hγ]") as "_"; [iNext; iExists c'; by iFrame|].
      iModIntro. wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
72 73 74
      rewrite {3}/mcounter; eauto 10.
  Qed.

75
  Lemma read_mono_spec l j :
Ralf Jung's avatar
Ralf Jung committed
76
    {{{ mcounter l j }}} read #l {{{ i, RET #i; j  i%nat  mcounter l i }}}.
77
  Proof.
78
    iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
79
    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]".
80
    wp_load.
81
    iDestruct (own_valid_2 with "Hγ Hγf")
82
      as %[?%mnat_included _]%auth_both_valid.
83
    iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
84
    { apply auth_update, (mnat_local_update _ _ c); auto. }
85
    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
86
    iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10.
87 88 89 90 91
  Qed.
End mono_proof.

(** Counter with contributions *)
Class ccounterG Σ :=
92
  CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
93
Definition ccounterΣ : gFunctors :=
94
  #[GFunctor (frac_authR natR)].
95 96

Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ  ccounterG Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Proof. solve_inG. Qed.
98 99 100 101 102

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

  Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
103
    ( n, own γ (F n)  l  #n)%I.
104 105

  Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
106
    inv N (ccounter_inv γ l).
107 108

  Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
109
    own γ (F{q} n).
110 111 112

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

116
  Lemma newcounter_contrib_spec (R : iProp Σ) :
117
    {{{ True }}} newcounter #()
118
    {{{ γ l, RET #l; ccounter_ctx γ l  ccounter γ 1 0 }}}.
119
  Proof.
120
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
Ralf Jung's avatar
Ralf Jung committed
121
    iMod (own_alloc (F O%nat  F 0%nat)) as (γ) "[Hγ Hγ']";
122
      first by apply auth_both_valid.
123
    iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
124
    { iNext. iExists 0%nat. by iFrame. }
125
    iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
126 127
  Qed.

128 129
  Lemma incr_contrib_spec γ l q n :
    {{{ ccounter_ctx γ l  ccounter γ q n }}} incr #l
130
    {{{ RET #(); ccounter γ q (S n) }}}.
131
  Proof.
132
    iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
133
    wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]".
134
    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
135 136
    wp_pures. wp_apply caset_spec; first done.
    iInv N as (c') ">[Hγ Hl]" "Hclose".
137
    destruct (decide (c' = c)) as [->|].
138
    - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
Ralf Jung's avatar
Ralf Jung committed
139
      { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
140 141
      iExists _; iFrame "Hl". iIntros "!> Hl".
      rewrite bool_decide_true //. iMod ("Hclose" with "[Hl Hγ]") as "_".
142
      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
143 144 145 146 147
      iModIntro. wp_if. by iApply "HΦ".
    - iExists _; iFrame "Hl". iIntros "!> Hl".
      rewrite bool_decide_false; last by intros [= ?%Nat2Z.inj].
      iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists c'; by iFrame|].
      iModIntro. wp_if. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
148 149
  Qed.

150
  Lemma read_contrib_spec γ l q n :
151
    {{{ ccounter_ctx γ l  ccounter γ q n }}} read #l
Ralf Jung's avatar
Ralf Jung committed
152
    {{{ c, RET #c; n  c%nat  ccounter γ q n }}}.
153
  Proof.
154
    iIntros (Φ) "[#? Hγf] HΦ".
155
    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
156
    iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
157
    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
158
    iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10.
159 160
  Qed.

161
  Lemma read_contrib_spec_1 γ l n :
162
    {{{ ccounter_ctx γ l  ccounter γ 1 n }}} read #l
163
    {{{ n, RET #n; ccounter γ 1 n }}}.
164
  Proof.
165
    iIntros (Φ) "[#? Hγf] HΦ".
166
    rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
167
    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
168
    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
169 170 171
    by iApply "HΦ".
  Qed.
End contrib_spec.