frac_token.v 9.35 KB
Newer Older
1
2
From iris.bi Require Import bi.
From iris.bi Require Export fractional.
3
4
5
From iris.algebra Require Import auth numbers.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import base_logic own.
6

7
8
From diaframe Require Import proofmode_base.
From diaframe.lib Require Import tokenizable own_hints.
9
10


11
12
13
14
15
16
17
(* This file defines the token ghost state used by, among others, ARC.
   The concrete definitions are abstracted away in this library too provide
   a cleaner presentation of the required ghost-state reasoning.
   Additionally, the proofs of the various updates sometimes require foresight, 
   and Diaframe cannot handle such proofs automatically. 
   Since this Diaframe comes with biabduction hints, Diaframe can reason about token automatically. *)

18
19
20
21
22
23
24
25
Section fractional_tokenizable.
  Definition fracTokenR := authUR $ optionUR $ prodR fracR positiveR.
  Class fracTokenG Σ := { fracPayloadTokenCounter_inG :> inG Σ fracTokenR }.
  Definition fracTokenΣ : gFunctors := #[GFunctor fracTokenR].
  Global Instance subG_fracTokenΣ {Σ} : subG fracTokenΣ Σ  fracTokenG Σ.
  Proof. solve_inG. Qed.

  Context `{!fracTokenG Σ}.
26
27
28
  Context (P : Qp  iProp Σ).
  Context {HP : Fractional P}.

29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
  Instance P_AsFractional q : AsFractional (P q) P q.
  Proof using HP. done. Qed.

  Program Definition fractional_payload_token_counter : tokenizable.Tokenizable $ iPropI Σ :=
    tokenizable.Build_Tokenizable
      (P 1)
      (λ γ,  q, own γ ( (Some (q, 1%positive)))  P q)%I
      (λ γ p,  q q', own γ ( (Some (q, p)))  (q + q' = 1)%Qp  P q')%I
      (λ γ q, own γ ({#q} None))
      _.
  Next Obligation.
    split.
    - iStepsS.
    - do 3 iStepS.
      iStepDebug.
      solveStep.
      solveStep.
      iExists (x1 + (x2 / 2))%Qp.
      unshelve solveSteps; [shelve | | split ].
      { apply frac_valid. rewrite -H. apply Qp_add_le_mono_l. by apply Qp_lt_le_incl, Qp_div_lt. }
      { rewrite -H -assoc.
        apply Qp_add_eq_mono_l, Qp_div_2. }
      iDestruct "H2" as "[H2 H2']".
      replace (Pos.succ x0 - x0)%positive with 1%positive by lia.
      iStepsS.
    - do 2 iStepS.
      iStepDebug.
      solveStep.
      solveStep.
      iExists (1/2)%Qp.
      solveSteps.
      split. { apply Qp_div_2. }
      iDestruct "H2" as "[H2 H2']".
      iStepsS.
63
    - do 4 iStepS.
64
      apply Qp_lt_sum in H2 as [q ->].
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
      iExists q.
      iStepS.
      iExists (x4 + x3)%Qp.
      iStepsS.
      * by rewrite assoc (Qp_add_comm q).
      * by iCombine "H4 H2" as "$".
    - iStepsS.
      rewrite -H.
      by iCombine "H4 H2" as "$".
    - do 3 iStepS.
    - do 4 iStepS.
    - iSolveTC.
    - do 3 iStepS. iDestruct (own_valid with "H1") as %[Hx0%dfrac_valid_own _]%auth_auth_dfrac_valid.
      revert Hx0 => /dfrac_valid_own Hx0; iStepsS.
    - intros γ p q. eapply (anti_symm _); iStepS.
      * by iDestruct "H1" as "[$ $]".
      * by rewrite Qp_add_comm.
  Qed.

  Let tc := fractional_payload_token_counter.
85

86
87
88
  Definition token := tokenizable.token tc.
  Definition token_counter := tokenizable.token_counter tc.
  Definition no_tokens := tokenizable.no_tokens tc.
89
End fractional_tokenizable.
90
91

Section automation.
92
  Context `{!fracTokenG Σ}.
93
94
95
96
97
  Context (P : Qp  iProp Σ).
  Context {HP : Fractional P}.

  Global Instance biabd_alloc_none q φ mq :
    CmraSubtract 1%Qp q φ mq 
98
    HINT empty_hyp_last  [⌜φ⌝]  [bupd] γ; no_tokens P γ q  [default emp (q'  mq; Some $ no_tokens P γ q')].
99
  Proof. apply: tokenizable.biabd_alloc_none. Qed.
100
101

  Global Instance biabd_alloc_some :
102
    HINT empty_hyp_last  [ - ; P 1]  [bupd] γ; token_counter P γ 1  [token P γ].
103
  Proof. apply: tokenizable.biabd_alloc_some. Qed.
104
105
106

  Global Instance biabd_create_token γ p1 p2 :
    SolveSepSideCondition (p2 = Pos.succ p1) 
Ike Mulder's avatar
Ike Mulder committed
107
    HINT token_counter P γ p1  [- ; emp]  [bupd]; token_counter P γ p2  [token P γ].
108
  Proof. apply: tokenizable.biabd_create_token. Qed.
109
110
111

  Global Instance biabd_create_first_token γ p :
    SolveSepSideCondition (p = 1%positive) 
112
    HINT no_tokens P γ 1  [- ; P 1]  [bupd]; token_counter P γ p  [token P γ].
113
  Proof. apply: tokenizable.biabd_create_first_token. Qed.
114
115
116
117

  Global Instance biabd_delete_token γ p1 p2 :
    SolveSepSideCondition (1 < p1)%positive 
    SolveSepSideCondition (p2 = Pos.pred p1) 
118
    HINT token_counter P γ p1  [- ; token P γ]  [bupd]; token_counter P γ p2  [emp].
119
  Proof. apply: tokenizable.biabd_delete_token. Qed.
120
121
122
123

  Global Instance biabd_delete_last_token γ q mq φ p :
    SolveSepSideCondition (p = 1)%positive 
    CmraSubtract 1%Qp q φ mq 
124
    HINT token_counter P γ p  [- ; token P γ  ⌜φ⌝]  [bupd]; no_tokens P γ q  [P 1  default emp (q'  mq; Some $ no_tokens P γ q')].
125
  Proof. apply: tokenizable.biabd_delete_last_token. Qed.
126
127
128

  Global Instance biabd_delete_last_token_to_req γ p :
    SolveSepSideCondition (p = 1%positive) 
129
    HINT token_counter P γ p  [- ; token P γ]  [bupd]; P 1  [no_tokens P γ 1].
130
  Proof. apply: tokenizable.biabd_delete_last_token_to_req. Qed.
131
132
133

  Global Instance no_tokens_split γ q1 q2 mq :
    FracSub q1 q2 mq 
Ike Mulder's avatar
Ike Mulder committed
134
    HINT no_tokens P γ q1  [- ; True]  [id]; no_tokens P γ q2  [match mq with | Some q => no_tokens P γ q | None => True end].
135
  Proof. apply: tokenizable.no_tokens_split. Qed.
136

137
138
139
140
141
142
143
144
145
146
147
  Fixpoint token_iter n γ : iProp Σ :=
    match n with
    | O => emp
    | S n => token P γ  token_iter n γ
    end.

  Lemma token_iter_eq γ n : token_iter n γ = tokenizable.tokenizable.token_iter (fractional_payload_token_counter P) n γ.
  Proof.
    induction n as [| n IH] => //=.
    by rewrite IH.
  Qed.
148
149

  Global Instance merge_token_no_tokens γ q :
150
    MergableConsume ( token P γ) (λ p Pin Pout,
151
      TCAnd (TCEq Pin (no_tokens P γ q))
152
            (TCEq Pout ( False)))%I | 11.
153
  Proof. apply: tokenizable.merge_token_no_tokens. Qed.
154

155
156
157
158
159
160
  Global Instance merge_token_no_tokens_now γ q :
    MergableConsume (token P γ) (λ p Pin Pout,
      TCAnd (TCEq Pin (no_tokens P γ q))
            (TCEq Pout ( False)))%I | 11.
  Proof. apply: tokenizable.merge_token_no_tokens_now. Qed.

161
  Global Instance merge_no_tokens_token_now γ q :
162
163
    MergableConsume (no_tokens P γ q) (λ p Pin Pout,
      TCAnd (TCEq Pin (token P γ))
164
            (TCEq Pout ( False)))%I | 10.
165
166
167
168
169
170
  Proof. apply: tokenizable.merge_no_tokens_token_now. Qed.

  Global Instance merge_no_tokens_token γ q :
    MergableConsume (no_tokens P γ q) (λ p Pin Pout,
      TCAnd (TCEq Pin ( token P γ))
            (TCEq Pout ( False)))%I | 10.
171
  Proof. apply: tokenizable.merge_no_tokens_token. Qed.
172
173

  Global Instance merge_no_tokens_token_later_counter γ q pos:
174
175
    MergableConsume (no_tokens P γ q) (λ p Pin Pout,
      TCAnd (TCEq Pin ( token_counter P γ pos))
176
            (TCEq Pout ( False)))%I | 11.
177
  Proof. apply: tokenizable.merge_no_tokens_token_later_counter. Qed.
178
179

  Global Instance merge_no_tokens_token_counter γ q pos:
180
181
    MergableConsume (no_tokens P γ q) (λ p Pin Pout,
      TCAnd (TCEq Pin (token_counter P γ pos))
182
            (TCEq Pout ( False)))%I | 12.
183
  Proof. apply: tokenizable.merge_no_tokens_token_counter. Qed.
184
185

  Global Instance merge_no_tokens γ q q1 q2 :
186
187
    MergableConsume (no_tokens P γ q1) (λ p Pin Pout,
      TCAnd (TCEq Pin (no_tokens P γ q2)) $
188
      TCAnd (IsOp q q1 q2) 
189
190
            (TCEq Pout (no_tokens P γ q  q  1%Qp)))%I | 20.
  Proof. apply: tokenizable.merge_no_tokens. Qed.
191
192

  Global Instance merge_token_counter_no_tokens γ q pos:
193
194
    MergableConsume (token_counter P γ pos) (λ p Pin Pout,
      TCAnd (TCEq Pin (no_tokens P γ q))
195
            (TCEq Pout ( False)))%I | 11.
196
  Proof. apply: tokenizable.merge_token_counter_no_tokens. Qed.
197
198

  Global Instance merge_token_counter_no_tokens_later γ q pos:
199
200
    MergableConsume ( token_counter P γ pos)%I (λ p Pin Pout,
      TCAnd (TCEq Pin (no_tokens P γ q))
201
            (TCEq Pout ( False)))%I | 11.
202
  Proof. apply: tokenizable.merge_token_counter_no_tokens_later. Qed.
203

204
205
206
207
208
209
  Global Instance no_tokens_fractional γ : Fractional (no_tokens P γ).
  Proof. iSolveTC. Qed.

  Global Instance no_tokens_timeless γ q : Timeless (no_tokens P γ q).
  Proof. iSolveTC. Qed.

210
  Global Instance token_into_exist γ : 
211
    (* this one should currently be manually enabled with Existing Instance token_into_exist *)
212
    AtomIntoExist (token P γ) (λ q : Qp, P q   (P q - token P γ))%I.
213
  Proof. 
214
    rewrite /AtomIntoExist /IntoExistCareful2 /IntoExistCareful. iStepsS.
215
216
217
    iApply bi.except_0_intro. iStepsS.
  Qed.

218
219
End automation.

220
221
222
Global Opaque token_counter.
Global Opaque no_tokens.
Global Opaque token.
223

224
225
226
227
(* this is missing and sometimes causes very slow TC resolution.
    TODO: merge into Iris? *)
Global Hint Mode Fractional + + : typeclass_instances.

228
229
230
231
232
233
Section token_counter_extra.
  Context `{!fracTokenG Σ}.
  Context (P : Qp  iProp Σ).
  Context {HP : Fractional P}.

  Global Instance biabd_alloc_multiple (p : positive) :
234
    HINT empty_hyp_last  [- ; P 1]  [bupd] γ; token_counter P γ p  [token_iter P (Pos.to_nat p) γ] | 500.
235
  Proof.
236
    rewrite /BiAbd /= empty_hyp_last_eq left_id.
237
238
239
240
241
242
243
244
245
246
247
248
    rewrite -{1}(Pos2Nat.id p).
    assert (0 < Pos.to_nat p) by lia. revert H.
    generalize (Pos.to_nat p) => n {p}.
    induction n as [|[|n] IHn]; first lia.
    - clear IHn => _. cbn. iStepsS.
    - intros Hn.
      rewrite IHn; last by lia.
      iStepsS.
  Qed.

End token_counter_extra.

249
250