boxes.v 13 KB
Newer Older
1
From iris.algebra Require Import lib.excl_auth gmap agree.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.proofmode Require Import tactics.
3
From iris.base_logic.lib Require Export invariants.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.prelude Require Import options.
5
6
7
Import uPred.

(** The CMRAs we need. *)
8
9
Class boxG Σ :=
  boxG_inG :> inG Σ (prodR
10
    (excl_authR boolO)
11
    (optionR (agreeR (laterO (iPropO Σ))))).
12

13
Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
14
15
                                            optionRF (agreeRF ( )) ) ].

Robbert Krebbers's avatar
Robbert Krebbers committed
16
Instance subG_boxΣ Σ : subG boxΣ Σ  boxG Σ.
17
Proof. solve_inG. Qed.
18

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

22
  Definition slice_name := gname.
23

24
  Definition box_own_auth (γ : slice_name) (a : excl_authR boolO) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
25
    own γ (a, None).
26

27
  Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
28
    own γ (ε, Some (to_agree (Next P))).
29

30
  Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
31
     b, box_own_auth γ (E b)  if b then P else True.
32

33
  Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
34
    box_own_prop γ P  inv N (slice_inv γ P).
35

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

43
44
45
46
Instance: Params (@box_own_prop) 3 := {}.
Instance: Params (@slice_inv) 3 := {}.
Instance: Params (@slice) 5 := {}.
Instance: Params (@box) 5 := {}.
47

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

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

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

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

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

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

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

84
Lemma box_own_auth_update γ b1 b2 b3 :
85
86
  box_own_auth γ (E b1)  box_own_auth γ (E b2)
  == box_own_auth γ (E b3)  box_own_auth γ (E b3).
87
Proof.
88
  rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
89
  apply excl_auth_update.
90
91
92
Qed.

Lemma box_own_agree γ Q1 Q2 :
93
  box_own_prop γ Q1  box_own_prop γ Q2   (Q1  Q2).
94
Proof.
95
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
96
  by rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
97
98
Qed.

Gregory Malecha's avatar
Gregory Malecha committed
99
Lemma box_alloc :  box N  True.
100
Proof.
101
  iIntros. iExists (λ _, True)%I. by rewrite !big_opM_empty.
102
103
Qed.

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

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

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

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

178
Lemma slice_insert_full E q f P Q :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
179
  N  E 
180
181
   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
182
Proof.
183
  iIntros (?) "HQ Hbox".
184
  iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
Robbert Krebbers's avatar
Robbert Krebbers committed
185
  iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
Tej Chajed's avatar
Tej Chajed committed
186
187
  - by apply lookup_insert.
  - by rewrite insert_insert.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
188
189
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
203
Lemma box_fill E f P :
204
  N  E 
205
  box N f P -  P ={E}= box N (const true <$> f) P.
206
Proof.
207
  iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
208
  iExists Φ; iSplitR; first by rewrite big_opM_fmap.
209
  iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
210
  iDestruct ("HeqP" with "HP") as "HP".
211
  iCombine "Hf" "HP" as "Hf".
212
  rewrite -big_sepM_sep big_opM_fmap; iApply (big_sepM_fupd _ _ f).
Robbert Krebbers's avatar
Robbert Krebbers committed
213
  iApply (@big_sepM_impl with "Hf").
214
  iIntros "!>" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
Ralf Jung's avatar
Ralf Jung committed
215
  iInv N as (b) "[>Hγ _]".
216
  iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
Ralf Jung's avatar
Ralf Jung committed
217
  iModIntro. iSplitL; last done. iNext; iExists true. iFrame.
218
219
Qed.

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
242
243
244
245
246
247
248
249
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.
250
    iDestruct ("HQQ'" with "HQ") as "HQ'".
251
    iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
252
    iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
253
    iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
254
  - iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
255
    iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
256
    iExists γ', (Q'  P')%I. iIntros "{$∗ $# $%} !>".  do 2 iNext. iRewrite "Heq".
257
    iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
258
259
Qed.

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

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

310
Typeclasses Opaque slice box.