boxes.v 8.96 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 Σ :=
25
    ( b, box_own_auth γ ( Excl' b)  box_own_prop γ P  if b then P else True)%I.
26

27
  Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
28
    inv N (slice_inv γ P).
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 52 53
Proof. solve_proper. Qed.
Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f).
Proof. solve_proper. Qed.
54
Global Instance slice_persistent γ P : PersistentP (slice N γ P).
55 56
Proof. apply _. Qed.

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

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

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

81
Lemma box_alloc : box N  True%I.
82 83 84 85 86 87
Proof.
  iIntros; iExists (λ _, True)%I; iSplit.
  - iNext. by rewrite big_sepM_empty.
  - by rewrite big_sepM_empty.
Qed.

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

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

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

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
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
Lemma box_insert_full E f P Q :
  N  E 
   Q   box N f P ={E}=  γ, f !! γ = None 
    slice N γ Q   box N (<[γ:=true]> f) (Q  P).
Proof.
  iIntros (?) "[HQ Hbox]".
  iMod (box_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
  iExists γ. iFrame "%#".
  iMod (box_fill with "[$Hslice $HQ $Hbox]"). done.
  by apply lookup_insert. by rewrite insert_insert.
Qed.

Lemma box_delete_full E f P Q γ :
  N  E 
  f !! γ = Some true 
  slice N γ Q   box N f P ={E}=
   Q   P',   (P  (Q  P'))   box N (delete γ f) P'.
Proof.
  iIntros (??) "[#Hslice Hbox]".
  iMod (box_empty with "[$Hslice $Hbox]") as "[$ Hbox]"; try done.
  iMod (box_delete_empty with "[$Hslice $Hbox]") as (P') "[Heq Hbox]".
    done. by apply lookup_insert.
  iExists P'. rewrite delete_insert. iFrame.
  iMod (box_fill with "[$Hslice $HQ $Hbox]"). done.
   by rewrite insert_insert.
Qed.

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

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

233
Typeclasses Opaque slice box.