boxes.v 11.9 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
6
7
Import uPred.

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

Section box_defs.
14
  Context `{invG Σ, boxG Σ} (N : namespace).
15

16
  Definition slice_name := gname.
17

18
  Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool)))
19
    := own γ (a, (:option (agree (later (iPreProp Σ))))).
20

21
  Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
22
    own γ (:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))).
23

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

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

30
31
  Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
    ( Φ : slice_name  iProp Σ,
32
33
       (P  [ map] γ  b  f, Φ γ) 
      [ map] γ  b  f, box_own_auth γ ( Excl' b)  box_own_prop γ (Φ γ) 
34
                         inv N (slice_inv γ (Φ γ)))%I.
35
36
End box_defs.

37
38
39
40
Instance: Params (@box_own_prop) 3.
Instance: Params (@slice_inv) 3.
Instance: Params (@slice) 5.
Instance: Params (@box) 5.
41

42
Section box.
43
Context `{invG Σ, boxG Σ} (N : namespace).
44
Implicit Types P Q : iProp Σ.
45

46
Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
47
Proof. solve_proper. Qed.
48
Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
49
Proof. solve_proper. Qed.
50
Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ).
51
Proof. solve_proper. Qed.
52
53
54
55
56
57
Global Instance box_contractive f : Contractive (box N f).
Proof.
  intros n P1 P2 HP1P2. apply exist_ne. intros Φ. f_equiv; last done.
  apply contractive. intros n' ?. by rewrite HP1P2.
Qed.

58
Global Instance slice_persistent γ P : PersistentP (slice N γ P).
59
60
Proof. apply _. Qed.

61
Lemma box_own_auth_agree γ b1 b2 :
Ralf Jung's avatar
Ralf Jung committed
62
  box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2)  b1 = b2.
63
Proof.
64
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
65
  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
66
67
Qed.

68
Lemma box_own_auth_update γ b1 b2 b3 :
69
70
  box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2)
  == box_own_auth γ ( Excl' b3)  box_own_auth γ ( Excl' b3).
71
Proof.
72
73
  rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
  by apply auth_update, option_local_update, exclusive_local_update.
74
75
76
Qed.

Lemma box_own_agree γ Q1 Q2 :
77
  box_own_prop γ Q1  box_own_prop γ Q2   (Q1  Q2).
78
Proof.
79
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
80
  rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
81
  iIntros "#HQ". iNext. rewrite -{2}(iProp_fold_unfold Q1).
82
83
84
  iRewrite "HQ". by rewrite iProp_fold_unfold.
Qed.

85
Lemma box_alloc : box N  True%I.
86
87
88
89
90
91
Proof.
  iIntros; iExists (λ _, True)%I; iSplit.
  - iNext. by rewrite big_sepM_empty.
  - by rewrite big_sepM_empty.
Qed.

92
Lemma box_insert_empty Q E f P :
Ralf Jung's avatar
Ralf Jung committed
93
   box N f P ={E}=  γ, f !! γ = None 
94
    slice N γ Q   box N (<[γ:=false]> f) (Q  P).
95
Proof.
96
  iDestruct 1 as (Φ) "[#HeqP Hf]".
97
  iMod (own_alloc_strong ( Excl' false   Excl' false,
98
    Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
99
    as (γ) "[Hdom Hγ]"; first done.
100
101
  rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
  iDestruct "Hdom" as % ?%not_elem_of_dom.
102
  iMod (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv".
103
  { iNext. iExists false; eauto. }
104
  iModIntro; iExists γ; repeat iSplit; auto.
105
  iNext. iExists (<[γ:=Q]> Φ); iSplit.
106
  - iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
107
  - rewrite (big_sepM_fn_insert (λ _ _ P',  _  _ _ P'  _ _ (_ _ P')))%I //.
108
    iFrame; eauto.
109
110
Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
111
Lemma box_delete_empty E f P Q γ :
112
  N  E 
113
  f !! γ = Some false 
114
  slice N γ Q -  box N f P ={E}=  P',
115
      (P  (Q  P'))   box N (delete γ f) P'.
116
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
118
  iExists ([ map] γ'_  delete γ f, Φ γ')%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  iInv N as (b) "[Hγ _]" "Hclose".
120
  iApply fupd_trans_frame; iFrame "Hclose"; iModIntro; iNext.
121
122
  iDestruct (big_sepM_delete _ f _ false with "Hf")
    as "[[Hγ' #[HγΦ ?]] ?]"; first done.
123
  iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
124
  iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
125
  iSplitL "Hγ"; last iSplit.
126
  - iExists false; eauto.
127
  - iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
128
  - iExists Φ; eauto.
129
130
Qed.

131
Lemma box_fill E f γ P Q :
132
  N  E 
133
  f !! γ = Some false 
134
  slice N γ Q -  Q -  box N f P ={E}=  box N (<[γ:=true]> f) P.
135
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
  iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
  iInv N as (b') "[>Hγ _]" "Hclose".
138
  iDestruct (big_sepM_later _ f with "Hf") as "Hf".
139
  iDestruct (big_sepM_delete _ f _ false with "Hf")
Robbert Krebbers's avatar
Robbert Krebbers committed
140
    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
141
  iMod (box_own_auth_update γ b' false true with "[Hγ Hγ']")
142
    as "[Hγ Hγ']"; first by iFrame.
143
144
  iMod ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
  iModIntro; iNext; iExists Φ; iSplit.
145
  - by rewrite big_sepM_insert_override.
146
  - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
147
    iFrame; eauto.
148
149
Qed.

150
Lemma box_empty E f P Q γ :
151
  N  E 
152
  f !! γ = Some true 
153
  slice N γ Q -  box N f P ={E}=  Q   box N (<[γ:=false]> f) P.
154
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
  iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
  iInv N as (b) "[>Hγ HQ]" "Hclose".
157
  iDestruct (big_sepM_later _ f with "Hf") as "Hf".
Ralf Jung's avatar
Ralf Jung committed
158
  iDestruct (big_sepM_delete _ f with "Hf")
Robbert Krebbers's avatar
Robbert Krebbers committed
159
    as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
160
  iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
161
  iFrame "HQ".
162
163
164
  iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
  iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
  iModIntro; iNext; iExists Φ; iSplit.
165
  - by rewrite big_sepM_insert_override.
166
  - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
167
    iFrame; eauto.
168
169
Qed.

170
Lemma box_insert_full Q E f P :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
171
  N  E 
172
   Q -  box N f P ={E}=  γ, f !! γ = None 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
173
174
    slice N γ Q   box N (<[γ:=true]> f) (Q  P).
Proof.
175
  iIntros (?) "HQ Hbox".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
176
  iMod (box_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  iExists γ. iFrame "%#". iMod (box_fill with "Hslice HQ Hbox"); first done.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
178
179
180
181
182
183
  by apply lookup_insert. by rewrite insert_insert.
Qed.

Lemma box_delete_full E f P Q γ :
  N  E 
  f !! γ = Some true 
184
185
  slice N γ Q -  box N f P ={E}=
   P',  Q    (P  (Q  P'))   box N (delete γ f) P'.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
186
Proof.
187
188
189
  iIntros (??) "#Hslice Hbox".
  iMod (box_empty with "Hslice Hbox") as "[$ Hbox]"; try done.
  iMod (box_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
190
    done. by apply lookup_insert.
191
  iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
192
193
Qed.

194
Lemma box_fill_all E f P :
195
  N  E 
196
  box N f P -  P ={E}= box N (const true <$> f) P.
197
Proof.
198
  iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
199
  iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
200
201
  rewrite internal_eq_iff later_iff big_sepM_later.
  iDestruct ("HeqP" with "HP") as "HP".
202
  iCombine "Hf" "HP" as "Hf".
203
  rewrite big_sepM_fmap; iApply (fupd_big_sepM _ _ f).
204
  iApply (big_sepM_impl _ _ f); iFrame "Hf".
205
  iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  iInv N as (b) "[>Hγ _]" "Hclose".
207
  iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
208
  iApply "Hclose". iNext; iExists true. by iFrame.
209
210
Qed.

211
Lemma box_empty_all E f P :
212
  N  E 
213
  map_Forall (λ _, (true =)) f 
214
  box N f P ={E}=  P  box N (const false <$> f) P.
215
Proof.
216
  iDestruct 1 as (Φ) "[#HeqP Hf]".
217
218
  iAssert ([ map] γ↦b  f,  Φ γ  box_own_auth γ ( Excl' false) 
    box_own_prop γ (Φ γ)  inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]".
219
  { iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
Robbert Krebbers's avatar
Robbert Krebbers committed
220
    iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
221
    assert (true = b) as <- by eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
    iInv N as (b) "[>Hγ HΦ]" "Hclose".
223
    iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
224
    iMod (box_own_auth_update γ true true false with "[Hγ Hγ']")
225
      as "[Hγ $]"; first by iFrame.
226
    iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
Robbert Krebbers's avatar
Robbert Krebbers committed
227
    iFrame "HγΦ Hinv". by iApply "HΦ". }
228
  iModIntro; iSplitL "HΦ".
229
  - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
230
231
  - iExists Φ; iSplit; by rewrite big_sepM_fmap.
Qed.
232
233
234
235

Lemma box_split E f P Q1 Q2 γ b :
  N  E  f !! γ = Some b 
  slice N γ (Q1  Q2) -  box N f P ={E}=  γ1 γ2,
236
    delete γ f !! γ1 = None  delete γ f !! γ2 = None  ⌜γ1  γ2 
237
238
239
240
241
242
    slice N γ1 Q1  slice N γ2 Q2   box N (<[γ2 := b]>(<[γ1 := b]>(delete γ f))) P.
Proof.
  iIntros (??) "#Hslice Hbox". destruct b.
  - iMod (box_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
    iMod (box_insert_full Q1 with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)". done.
    iMod (box_insert_full Q2 with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)". done.
243
244
245
    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). }
246
247
248
249
250
    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
    iNext. iRewrite "Heq". iPureIntro. rewrite assoc. f_equiv. by rewrite comm. done.
  - iMod (box_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
    iMod (box_insert_empty Q1 with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)".
    iMod (box_insert_empty Q2 with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)".
251
252
253
    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). }
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
    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
    iNext. iRewrite "Heq". iPureIntro. rewrite assoc. f_equiv. by rewrite comm. done.
Qed.

Lemma box_combine E 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 -  box N f P ={E}=  γ,
    delete γ2 (delete γ1 f) !! γ = None  slice N γ (Q1  Q2) 
     box N (<[γ := b]>(delete γ2 (delete γ1 f))) P.
Proof.
  iIntros (????) "#Hslice1 #Hslice2 Hbox". destruct b.
  - iMod (box_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done.
    iMod (box_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)".
      done. by simplify_map_eq.
    iMod (box_insert_full (Q1  Q2)%I with "[$HQ1 $HQ2] Hbox")
        as (γ) "(% & #Hslice & Hbox)". done.
    iExists γ. iFrame "%#". iModIntro. iNext.
    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
    iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
  - iMod (box_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
    iMod (box_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)".
      done. by simplify_map_eq.
    iMod (box_insert_empty (Q1  Q2)%I with "Hbox") as (γ) "(% & #Hslice & Hbox)".
    iExists γ. iFrame "%#". iModIntro. iNext.
    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
    iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Qed.
281
End box.
282

283
Typeclasses Opaque slice box.