boxes.v 7.92 KB
Newer Older
1
From iris.program_logic 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 `{irisG Λ Σ, 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 26
    ( b, box_own_auth γ ( Excl' b)  box_own_prop γ P  if b then P else True)%I.

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 41
Instance: Params (@box_own_auth) 5.
Instance: Params (@box_own_prop) 5.
Instance: Params (@slice_inv) 5.
Instance: Params (@slice) 6.
Instance: Params (@box) 6.
42

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

47
Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
48
Proof. solve_proper. Qed.
49
Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
50
Proof. solve_proper. Qed.
51
Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ).
52 53 54
Proof. solve_proper. Qed.
Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f).
Proof. solve_proper. Qed.
55
Global Instance slice_persistent γ P : PersistentP (slice N γ P).
56 57
Proof. apply _. Qed.

58
Lemma box_own_auth_agree γ b1 b2 :
59
  box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2)  b1 = b2.
60
Proof.
61
  rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_l.
62
  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
63 64
Qed.

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

Lemma box_own_agree γ Q1 Q2 :
  (box_own_prop γ Q1  box_own_prop γ Q2)   (Q1  Q2).
Proof.
76
  rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_r.
77
  rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  iIntros "#HQ !>". rewrite -{2}(iProp_fold_unfold Q1).
79 80 81 82 83 84 85 86 87 88 89
  iRewrite "HQ". by rewrite iProp_fold_unfold.
Qed.

Lemma box_alloc : True  box N  True.
Proof.
  iIntros; iExists (λ _, True)%I; iSplit.
  - iNext. by rewrite big_sepM_empty.
  - by rewrite big_sepM_empty.
Qed.

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

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

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

164
Lemma box_fill_all f P Q : box N f P   P ={N}= box N (const true <$> f) P.
165
Proof.
166
  iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
167 168 169
  iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
  rewrite eq_iff later_iff big_sepM_later; iDestruct ("HeqP" with "HP") as "HP".
  iCombine "Hf" "HP" as "Hf".
170
  rewrite big_sepM_fmap; iApply (fupd_big_sepM _ _ f).
171
  iApply (big_sepM_impl _ _ f); iFrame "Hf".
172
  iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  iInv N as (b) "[>Hγ _]" "Hclose".
174
  iUpd (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
175
  iApply "Hclose". iNext; iExists true. by iFrame.
176 177 178 179
Qed.

Lemma box_empty_all f P Q :
  map_Forall (λ _, (true =)) f 
180
  box N f P ={N}=  P  box N (const false <$> f) P.
181
Proof.
182
  iDestruct 1 as (Φ) "[#HeqP Hf]".
183
  iAssert ([ map] γ↦b  f,  Φ γ  box_own_auth γ ( Excl' false) 
Robbert Krebbers's avatar
Robbert Krebbers committed
184
    box_own_prop γ (Φ γ)  inv N (slice_inv γ (Φ γ)))%I with "==>[Hf]" as "[HΦ ?]".
185
  { iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
186
    iAlways; iIntros (γ b ?) "(Hγ' & #$ & #$)".
187
    assert (true = b) as <- by eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
    iInv N as (b) "(>Hγ & _ & HΦ)" "Hclose".
189
    iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
190
    iUpd (box_own_auth_update γ true true false with "[Hγ Hγ']")
191
      as "[Hγ $]"; first by iFrame.
192
    iUpd ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
193
    by iApply "HΦ". }
194
  iUpdIntro; iSplitL "HΦ".
195 196 197 198
  - rewrite eq_iff later_iff big_sepM_later. by iApply "HeqP".
  - iExists Φ; iSplit; by rewrite big_sepM_fmap.
Qed.
End box.
199

200
Typeclasses Opaque slice_name slice box.