1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
|
From iris.algebra Require Import lib.excl_auth gmap agree.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Export invariants.
From iris.prelude Require Import options.
Import uPred.
(** The CMRAs we need. *)
Class boxG Σ :=
#[local] boxG_inG :: inG Σ (prodR
(excl_authR boolO)
(optionR (agreeR (laterO (iPropO Σ))))).
Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
optionRF (agreeRF (▶ ∙)) ) ].
Global Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
Proof. solve_inG. Qed.
Section box_defs.
Context `{!invGS_gen hlc Σ, !boxG Σ} (N : namespace).
Definition slice_name := gname.
Definition box_own_auth (γ : slice_name) (a : excl_authR boolO) : iProp Σ :=
own γ (a, None).
Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
own γ (ε, Some (to_agree (Next P))).
Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
∃ b, box_own_auth γ (●E b) ∗ if b then P else True.
Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
box_own_prop γ P ∗ inv N (slice_inv γ P).
Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
tc_opaque (∃ Φ : slice_name → iProp Σ,
▷ (P ≡ [∗ map] γ ↦ _ ∈ f, Φ γ) ∗
[∗ map] γ ↦ b ∈ f, box_own_auth γ (◯E b) ∗ box_own_prop γ (Φ γ) ∗
inv N (slice_inv γ (Φ γ)))%I.
End box_defs.
Global Instance: Params (@box_own_prop) 3 := {}.
Global Instance: Params (@slice_inv) 3 := {}.
Global Instance: Params (@slice) 5 := {}.
Global Instance: Params (@box) 5 := {}.
Section box.
Context `{!invGS_gen hlc Σ, !boxG Σ} (N : namespace).
Implicit Types P Q : iProp Σ.
Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
Proof. solve_proper. Qed.
Global Instance box_own_prop_contractive γ : Contractive (box_own_prop γ).
Proof. solve_contractive. Qed.
Global Instance box_inv_ne γ : NonExpansive (slice_inv γ).
Proof. solve_proper. Qed.
Global Instance slice_ne γ : NonExpansive (slice N γ).
Proof. solve_proper. Qed.
Global Instance slice_contractive γ : Contractive (slice N γ).
Proof. solve_contractive. Qed.
Global Instance slice_proper γ : Proper ((≡) ==> (≡)) (slice N γ).
Proof. apply ne_proper, _. Qed.
Global Instance slice_persistent γ P : Persistent (slice N γ P).
Proof. apply _. Qed.
Global Instance box_contractive f : Contractive (box N f).
Proof. solve_contractive. Qed.
Global Instance box_ne f : NonExpansive (box N f).
Proof. apply (contractive_ne _). Qed.
Global Instance box_proper f : Proper ((≡) ==> (≡)) (box N f).
Proof. apply ne_proper, _. Qed.
Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2) ⊢ ⌜b1 = b2⌝.
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
by iDestruct 1 as %?%excl_auth_agree_L.
Qed.
Lemma box_own_auth_update γ b1 b2 b3 :
box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2)
==∗ box_own_auth γ (●E b3) ∗ box_own_auth γ (◯E b3).
Proof.
rewrite /box_own_auth -!own_op. iApply own_update. apply prod_update; last done.
apply excl_auth_update.
Qed.
Lemma box_own_agree γ Q1 Q2 :
box_own_prop γ Q1 ∗ box_own_prop γ Q2 ⊢ ▷ (Q1 ≡ Q2).
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
by rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
Qed.
Lemma box_alloc : ⊢ box N ∅ True.
Proof.
iIntros. iExists (λ _, True)%I. by rewrite !big_opM_empty.
Qed.
Lemma slice_insert_empty E q f Q P :
▷?q box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
slice N γ Q ∗ ▷?q box N (<[γ:=false]> f) (Q ∗ P).
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_cofinite (●E false ⋅ ◯E false,
Some (to_agree (Next Q))) (dom f))
as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid_discrete|]).
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
{ iNext. iExists false; eauto. }
iModIntro; iExists γ; repeat iSplit; auto.
iNext. iExists (<[γ:=Q]> Φ); iSplit.
- iNext. iRewrite "HeqP". by rewrite big_opM_fn_insert'.
- rewrite (big_opM_fn_insert (λ _ _ P', _ ∗ _ _ P' ∗ _ _ (_ _ P')))%I //.
iFrame; eauto.
Qed.
Lemma slice_delete_empty E q f P Q γ :
↑N ⊆ E →
f !! γ = Some false →
slice N γ Q -∗ ▷?q box N f P ={E}=∗ ∃ P',
▷?q (▷ (P ≡ (Q ∗ P')) ∗ box N (delete γ f) P').
Proof.
iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
iInv N as (b) "[>Hγ _]".
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
iModIntro. iSplitL "Hγ"; first iExists false; eauto.
iModIntro. iNext. iSplit.
- iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
- iExists Φ; eauto.
Qed.
Lemma slice_fill E q f γ P Q :
↑N ⊆ E →
f !! γ = Some false →
slice N γ Q -∗ ▷ Q -∗ ▷?q box N f P ={E}=∗ ▷?q box N (<[γ:=true]> f) P.
Proof.
iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b') "[>Hγ _]".
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_opM_insert_override.
- rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
iFrame; eauto.
Qed.
Lemma slice_empty E q f P Q γ :
↑N ⊆ E →
f !! γ = Some true →
slice N γ Q -∗ ▷?q box N f P ={E}=∗ ▷ Q ∗ ▷?q box N (<[γ:=false]> f) P.
Proof.
iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iInv N as (b) "[>Hγ HQ]".
iDestruct (big_sepM_delete _ f with "Hf")
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iFrame "HQ".
iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
iModIntro. iSplitL "Hγ"; first (iNext; iExists false; by repeat iSplit).
iModIntro; iNext; iExists Φ; iSplit.
- by rewrite big_opM_insert_override.
- rewrite -insert_delete_insert big_opM_insert ?lookup_delete //.
iFrame; eauto.
Qed.
Lemma slice_insert_full E q f P Q :
↑N ⊆ E →
▷ Q -∗ ▷?q box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
slice N γ Q ∗ ▷?q box N (<[γ:=true]> f) (Q ∗ P).
Proof.
iIntros (?) "HQ Hbox".
iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
- by apply lookup_insert.
- by rewrite insert_insert.
Qed.
Lemma slice_delete_full E q f P Q γ :
↑N ⊆ E →
f !! γ = Some true →
slice N γ Q -∗ ▷?q box N f P ={E}=∗
∃ P', ▷ Q ∗ ▷?q ▷ (P ≡ (Q ∗ P')) ∗ ▷?q box N (delete γ f) P'.
Proof.
iIntros (??) "#Hslice Hbox".
iMod (slice_empty with "Hslice Hbox") as "[$ Hbox]"; try done.
iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; first done.
{ by apply lookup_insert. }
iExists P'. iFrame. rewrite -insert_delete_insert delete_insert ?lookup_delete //.
Qed.
Lemma box_fill E f P :
↑N ⊆ E →
box N f P -∗ ▷ P ={E}=∗ box N (const true <$> f) P.
Proof.
iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists Φ; iSplitR; first by rewrite big_opM_fmap.
iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf".
rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
iApply (@big_sepM_impl with "Hf").
iIntros "!>" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]".
iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
Qed.
Lemma box_empty E f P :
↑N ⊆ E →
map_Forall (λ _, (true =.)) f →
box N f P ={E}=∗ ▷ P ∗ box N (const false <$> f) P.
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ) ∗
[∗ map] γ↦b ∈ f, box_own_auth γ (◯E false) ∗ box_own_prop γ (Φ γ) ∗
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
iIntros "!>" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]".
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]".
iModIntro. iSplitL "Hγ"; first (iNext; iExists false; iFrame; eauto).
iFrame "HγΦ Hinv". by iApply "HΦ". }
iModIntro; iSplitL "HΦ".
- rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
- iExists Φ; iSplit; by rewrite big_opM_fmap.
Qed.
Lemma slice_iff E q f P Q Q' γ b :
↑N ⊆ E → f !! γ = Some b →
▷ □ (Q ↔ Q') -∗ slice N γ Q -∗ ▷?q box N f P ={E}=∗ ∃ γ' P',
⌜delete γ f !! γ' = None⌝ ∗ ▷?q ▷ □ (P ↔ P') ∗
slice N γ' Q' ∗ ▷?q box N (<[γ' := b]>(delete γ f)) P'.
Proof.
iIntros (??) "#HQQ' #Hs Hb". destruct b.
- iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
iDestruct ("HQQ'" with "HQ") as "HQ'".
iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
- iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', (Q' ∗ P')%I. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed.
Lemma slice_split E q f P Q1 Q2 γ b :
↑N ⊆ E → f !! γ = Some b →
slice N γ (Q1 ∗ Q2) -∗ ▷?q box N f P ={E}=∗ ∃ γ1 γ2,
⌜delete γ f !! γ1 = None⌝ ∗ ⌜delete γ f !! γ2 = None⌝ ∗ ⌜γ1 ≠ γ2⌝ ∗
slice N γ1 Q1 ∗ slice N γ2 Q2 ∗ ▷?q box N (<[γ2 := b]>(<[γ1 := b]>(delete γ f))) P.
Proof.
iIntros (??) "#Hslice Hbox". destruct b.
- iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
iMod (slice_insert_full with "HQ1 Hbox") as (γ1 ?) "[#Hslice1 Hbox]"; first done.
iMod (slice_insert_full with "HQ2 Hbox") as (γ2 ?) "[#Hslice2 Hbox]"; first done.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
- iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
iMod (slice_insert_empty with "Hbox") as (γ2 ?) "[#Hslice2 Hbox]".
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
iNext. iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq] Hbox").
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
Qed.
Lemma slice_combine E q f P Q1 Q2 γ1 γ2 b :
↑N ⊆ E → γ1 ≠ γ2 → f !! γ1 = Some b → f !! γ2 = Some b →
slice N γ1 Q1 -∗ slice N γ2 Q2 -∗ ▷?q box N f P ={E}=∗ ∃ γ,
⌜delete γ2 (delete γ1 f) !! γ = None⌝ ∗ slice N γ (Q1 ∗ Q2) ∗
▷?q box N (<[γ := b]>(delete γ2 (delete γ1 f))) P.
Proof.
iIntros (????) "#Hslice1 #Hslice2 Hbox". destruct b.
- iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done.
iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done.
{ by simplify_map_eq. }
iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2) with "[$HQ1 $HQ2] Hbox")
as (γ ?) "[#Hslice Hbox]"; first done.
iExists γ. iIntros "{$% $#} !>". iNext.
iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
- iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
{ by simplify_map_eq. }
iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iIntros "{$% $#} !>". iNext.
iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Qed.
End box.
Global Typeclasses Opaque slice box.
|
