boxes.v 13.3 KB
Newer Older
1
From iris.base_logic.lib Require Export invariants.
2
3
From iris.algebra Require Import auth gmap agree.
From iris.base_logic Require Import big_op.
4
From iris.proofmode Require Import tactics.
5
Set Default Proof Using "Type".
6
7
8
Import uPred.

(** The CMRAs we need. *)
9
10
Class boxG Σ :=
  boxG_inG :> inG Σ (prodR
11
    (authR (optionUR (exclR boolC)))
12
    (optionR (agreeR (laterC (iPreProp Σ))))).
13

14
15
16
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
                                            optionRF (agreeRF ( )) ) ].

17
Instance subG_stsΣ Σ : subG boxΣ Σ  boxG Σ.
18
Proof. solve_inG. Qed.
19

20
Section box_defs.
21
  Context `{invG Σ, boxG Σ} (N : namespace).
22

23
  Definition slice_name := gname.
24

Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
  Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool))) : iProp Σ :=
    own γ (a, (:option (agree (later (iPreProp Σ))))).
27

28
  Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
29
    own γ (:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))).
30

31
  Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
32
    ( b, box_own_auth γ ( Excl' b)  if b then P else True)%I.
33

34
  Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    (box_own_prop γ P  inv N (slice_inv γ P))%I.
36

37
38
  Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
    ( Φ : slice_name  iProp Σ,
Robbert Krebbers's avatar
Robbert Krebbers committed
39
       (P  [ map] γ  _  f, Φ γ) 
40
      [ map] γ  b  f, box_own_auth γ ( Excl' b)  box_own_prop γ (Φ γ) 
41
                         inv N (slice_inv γ (Φ γ)))%I.
42
43
End box_defs.

44
45
46
47
Instance: Params (@box_own_prop) 3.
Instance: Params (@slice_inv) 3.
Instance: Params (@slice) 5.
Instance: Params (@box) 5.
48

49
Section box.
50
Context `{invG Σ, boxG Σ} (N : namespace).
51
Implicit Types P Q : iProp Σ.
52

53
Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
54
Proof. solve_proper. Qed.
55
56
57
Global Instance box_own_prop_contractive γ : Contractive (box_own_prop γ).
Proof. solve_contractive. Qed.

58
Global Instance box_inv_ne γ : NonExpansive (slice_inv γ).
59
Proof. solve_proper. Qed.
60

61
Global Instance slice_ne γ : NonExpansive (slice N γ).
62
Proof. solve_proper. Qed.
63
64
Global Instance slice_contractive γ : Contractive (slice N γ).
Proof. solve_contractive. Qed.
65
66
Global Instance slice_proper γ : Proper (() ==> ()) (slice N γ).
Proof. apply ne_proper, _. Qed.
67

68
Global Instance slice_persistent γ P : PersistentP (slice N γ P).
69
70
Proof. apply _. Qed.

71
72
Global Instance box_contractive f : Contractive (box N f).
Proof. solve_contractive. Qed.
73
Global Instance box_ne f : NonExpansive (box N f).
74
Proof. apply (contractive_ne _). Qed.
75
76
Global Instance box_proper f : Proper (() ==> ()) (box N f).
Proof. apply ne_proper, _. Qed.
77

78
Lemma box_own_auth_agree γ b1 b2 :
Ralf Jung's avatar
Ralf Jung committed
79
  box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2)  b1 = b2.
80
Proof.
81
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
82
  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
83
84
Qed.

85
Lemma box_own_auth_update γ b1 b2 b3 :
86
87
  box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2)
  == box_own_auth γ ( Excl' b3)  box_own_auth γ ( Excl' b3).
88
Proof.
89
90
  rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
  by apply auth_update, option_local_update, exclusive_local_update.
91
92
93
Qed.

Lemma box_own_agree γ Q1 Q2 :
94
  box_own_prop γ Q1  box_own_prop γ Q2   (Q1  Q2).
95
Proof.
96
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
97
  rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
98
  iIntros "#HQ". iNext. rewrite -{2}(iProp_fold_unfold Q1).
99
100
101
  iRewrite "HQ". by rewrite iProp_fold_unfold.
Qed.

102
Lemma box_alloc : box N  True%I.
103
Proof.
104
105
  iIntros; iExists (λ _, True)%I; iSplit; last done.
  iNext. by rewrite big_opM_empty.
106
107
Qed.

108
109
110
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).
111
Proof.
112
  iDestruct 1 as (Φ) "[#HeqP Hf]".
113
  iMod (own_alloc_strong ( Excl' false   Excl' false,
114
    Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
115
    as (γ) "[Hdom Hγ]"; first done.
116
117
  rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
  iDestruct "Hdom" as % ?%not_elem_of_dom.
118
  iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
119
  { iNext. iExists false; eauto. }
120
  iModIntro; iExists γ; repeat iSplit; auto.
121
  iNext. iExists (<[γ:=Q]> Φ); iSplit.
122
123
  - iNext. iRewrite "HeqP". by rewrite big_opM_fn_insert'.
  - rewrite (big_opM_fn_insert (λ _ _ P',  _  _ _ P'  _ _ (_ _ P')))%I //.
124
    iFrame; eauto.
125
126
Qed.

127
Lemma slice_delete_empty E q f P Q γ :
128
  N  E 
129
  f !! γ = Some false 
130
131
  slice N γ Q - ?q box N f P ={E}=  P',
    ?q  (P  (Q  P'))  ?q box N (delete γ f) P'.
132
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
134
  iExists ([ map] γ'_  delete γ f, Φ γ')%I.
135
  iInv N as (b) "[>Hγ _]" "Hclose".
136
  iDestruct (big_opM_delete _ f _ false with "Hf")
137
    as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
138
  iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
139
140
141
  iMod ("Hclose" with "[Hγ]"); first iExists false; eauto.
  iModIntro. iNext. iSplit.
  - iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
142
    iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_opM_delete.
143
  - iExists Φ; eauto.
144
145
Qed.

146
Lemma slice_fill E q f γ P Q :
147
  N  E 
148
  f !! γ = Some false 
149
  slice N γ Q -  Q - ?q box N f P ={E}= ?q box N (<[γ:=true]> f) P.
150
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
  iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
  iInv N as (b') "[>Hγ _]" "Hclose".
153
  iDestruct (big_opM_delete _ f _ false with "Hf")
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
155
  iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
156
157
  iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
  iModIntro; iNext; iExists Φ; iSplit.
158
159
  - by rewrite big_opM_insert_override.
  - rewrite -insert_delete big_opM_insert ?lookup_delete //.
160
    iFrame; eauto.
161
162
Qed.

163
Lemma slice_empty E q f P Q γ :
164
  N  E 
165
  f !! γ = Some true 
166
  slice N γ Q - ?q box N f P ={E}=  Q  ?q box N (<[γ:=false]> f) P.
167
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
  iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
  iInv N as (b) "[>Hγ HQ]" "Hclose".
170
  iDestruct (big_opM_delete _ f with "Hf")
Robbert Krebbers's avatar
Robbert Krebbers committed
171
    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
172
  iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
173
  iFrame "HQ".
174
  iMod (box_own_auth_update γ with "[$Hγ $Hγ']") as "[Hγ Hγ']".
175
176
  iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
  iModIntro; iNext; iExists Φ; iSplit.
177
178
  - by rewrite big_opM_insert_override.
  - rewrite -insert_delete big_opM_insert ?lookup_delete //.
179
    iFrame; eauto.
180
181
Qed.

182
Lemma slice_insert_full E q f P Q :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
183
  N  E 
184
185
   Q - ?q box N f P ={E}=  γ, f !! γ = None 
    slice N γ Q  ?q box N (<[γ:=true]> f) (Q  P).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
186
Proof.
187
  iIntros (?) "HQ Hbox".
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
  iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
  iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
190
191
192
  by apply lookup_insert. by rewrite insert_insert.
Qed.

193
Lemma slice_delete_full E q f P Q γ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
194
195
  N  E 
  f !! γ = Some true 
196
197
  slice N γ Q - ?q box N f P ={E}=
   P',  Q  ?q  (P  (Q  P'))  ?q box N (delete γ f) P'.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
198
Proof.
199
  iIntros (??) "#Hslice Hbox".
Robbert Krebbers's avatar
Robbert Krebbers committed
200
201
202
  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. }
203
  iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
204
205
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
206
Lemma box_fill E f P :
207
  N  E 
208
  box N f P -  P ={E}= box N (const true <$> f) P.
209
Proof.
210
  iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
211
212
  iExists Φ; iSplitR; first by rewrite big_opM_fmap.
  rewrite internal_eq_iff later_iff big_opM_commute.
213
  iDestruct ("HeqP" with "HP") as "HP".
214
  iCombine "Hf" "HP" as "Hf".
215
  rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
216
  iApply (@big_sepM_impl with "[$Hf]").
217
  iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
Robbert Krebbers's avatar
Robbert Krebbers committed
218
  iInv N as (b) "[>Hγ _]" "Hclose".
219
  iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
220
  iApply "Hclose". iNext; iExists true. by iFrame.
221
222
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
223
Lemma box_empty E f P :
224
  N  E 
225
  map_Forall (λ _, (true =)) f 
226
  box N f P ={E}=  P  box N (const false <$> f) P.
227
Proof.
228
  iDestruct 1 as (Φ) "[#HeqP Hf]".
229
230
231
  iAssert (([ map] γ↦b  f,  Φ γ) 
    [ map] γ↦b  f, box_own_auth γ ( Excl' false)   box_own_prop γ (Φ γ) 
      inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
232
  { rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
Robbert Krebbers's avatar
Robbert Krebbers committed
233
    iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
234
    assert (true = b) as <- by eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
    iInv N as (b) "[>Hγ HΦ]" "Hclose".
236
    iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
237
    iMod (box_own_auth_update γ true true false with "[$Hγ $Hγ']") as "[Hγ $]".
238
    iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
Robbert Krebbers's avatar
Robbert Krebbers committed
239
    iFrame "HγΦ Hinv". by iApply "HΦ". }
240
  iModIntro; iSplitL "HΦ".
241
242
  - rewrite internal_eq_iff later_iff big_opM_commute. by iApply "HeqP".
  - iExists Φ; iSplit; by rewrite big_opM_fmap.
243
Qed.
244

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
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 γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iRewrite "Heq".
    iAlways. 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 γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iRewrite "Heq".
    iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed.

263
Lemma slice_split E q f P Q1 Q2 γ b :
264
  N  E  f !! γ = Some b 
265
  slice N γ (Q1  Q2) - ?q box N f P ={E}=  γ1 γ2,
266
    delete γ f !! γ1 = None  delete γ f !! γ2 = None  ⌜γ1  γ2 
267
    slice N γ1 Q1  slice N γ2 Q2  ?q box N (<[γ2 := b]>(<[γ1 := b]>(delete γ f))) P.
268
269
Proof.
  iIntros (??) "#Hslice Hbox". destruct b.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
  - iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
271
272
    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.
273
274
275
    iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro.
    { by eapply lookup_insert_None. }
    { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
276
    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
Robbert Krebbers's avatar
Robbert Krebbers committed
277
278
    iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
  - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
279
280
    iMod (slice_insert_empty with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)".
    iMod (slice_insert_empty with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)".
281
282
283
    iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro.
    { by eapply lookup_insert_None. }
    { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
284
    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
Robbert Krebbers's avatar
Robbert Krebbers committed
285
    iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
286
287
Qed.

288
Lemma slice_combine E q f P Q1 Q2 γ1 γ2 b :
289
  N  E  γ1  γ2  f !! γ1 = Some b  f !! γ2 = Some b 
290
  slice N γ1 Q1 - slice N γ2 Q2 - ?q box N f P ={E}=  γ,
291
    delete γ2 (delete γ1 f) !! γ = None  slice N γ (Q1  Q2) 
292
    ?q box N (<[γ := b]>(delete γ2 (delete γ1 f))) P.
293
294
Proof.
  iIntros (????) "#Hslice1 #Hslice2 Hbox". destruct b.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
296
297
  - 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. }
298
    iMod (slice_insert_full _ _ _ _ (Q1  Q2)%I with "[$HQ1 $HQ2] Hbox")
Robbert Krebbers's avatar
Robbert Krebbers committed
299
      as (γ) "(% & #Hslice & Hbox)"; first done.
300
301
302
    iExists γ. iFrame "%#". iModIntro. iNext.
    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
    iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
304
305
  - 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. }
306
    iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
307
308
309
310
    iExists γ. iFrame "%#". iModIntro. iNext.
    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
    iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Qed.
311
End box.
312

313
Typeclasses Opaque slice box.