boxes.v 8.39 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import auth saved_prop.
From iris.proofmode Require Import tactics invariants ghost_ownership.
Import uPred.

(** The CMRAs we need. *)
Class boxG Λ Σ :=
  boxG_inG :> inG Λ Σ (prodR
    (authR (optionUR (exclR boolC)))
    (optionR (agreeR (laterC (iPrePropG Λ Σ))))).

Section box_defs.
  Context `{boxG Λ Σ} (N : namespace).
  Notation iProp := (iPropG Λ Σ).

  Definition box_own_auth (γ : gname) (a : auth (option (excl bool))) : iProp :=
    own γ (a, ).

  Definition box_own_prop (γ : gname) (P : iProp) : iProp :=
    own γ (:auth _, Some (to_agree (Next (iProp_unfold P)))).

  Definition box_inv (γ : gname) (P : iProp) : iProp :=
    ( b, box_own_auth γ ( Excl' b)  box_own_prop γ P  if b then P else True)%I.

  Definition box_slice (γ : gname) (P : iProp) : iProp :=
    inv N (box_inv γ P).

  Definition box (f : gmap gname bool) (P : iProp) : iProp :=
    ( Φ : gname  iProp,
       (P  [ map] γ  b  f, Φ γ) 
      [ map] γ  b  f, box_own_auth γ ( Excl' b)  box_own_prop γ (Φ γ) 
                         inv N (box_inv γ (Φ γ)))%I.
End box_defs.

35
36
37
38
39
40
Instance: Params (@box_own_auth) 4.
Instance: Params (@box_own_prop) 4.
Instance: Params (@box_inv) 4.
Instance: Params (@box_slice) 5.
Instance: Params (@box) 5.

41
42
43
44
45
Section box.
Context `{boxG Λ Σ} (N : namespace).
Notation iProp := (iPropG Λ Σ).
Implicit Types P Q : iProp.

46
47
48
49
50
51
52
53
54
55
56
57
58
(* FIXME: solve_proper picks the eq ==> instance for Next. *)
Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
Proof. intros P P' HP. by rewrite /box_own_prop HP. Qed.
Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (box_inv γ).
Proof. solve_proper. Qed.
Global Instance box_slice_ne n γ : Proper (dist n ==> dist n) (box_slice N γ).
Proof. solve_proper. Qed.
Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f).
Proof. solve_proper. Qed.
Global Instance box_slice_persistent γ P : PersistentP (box_slice N γ P).
Proof. apply _. Qed.

(* This should go automatic *)
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
Instance box_own_auth_timeless γ
  (a : auth (option (excl bool))) : TimelessP (box_own_auth γ a).
Proof. apply own_timeless, pair_timeless; apply _. Qed.

Lemma box_own_auth_agree γ b1 b2 :
  (box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2))  (b1 = b2).
Proof.
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
  iIntros "Hb".
  by iDestruct "Hb" as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
Qed.

Lemma box_own_auth_update E γ b1 b2 b3 :
  (box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2))
   |={E}=> (box_own_auth γ ( Excl' b3)  box_own_auth γ ( Excl' b3)).
Proof.
  rewrite /box_own_prop -!own_op.
  apply own_update, prod_update; simpl; last reflexivity.
  by apply (auth_local_update (λ _, Excl' b3)).
Qed.

Lemma box_own_agree γ Q1 Q2 :
  (box_own_prop γ Q1  box_own_prop γ Q2)   (Q1  Q2).
Proof.
  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
  rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
  iIntros "#HQ >". rewrite -{2}(iProp_fold_unfold Q1).
  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 :
   box N f P  |={N}=>  γ, f !! γ = None 
    box_slice N γ Q   box N (<[γ:=false]> f) (Q  P).
Proof.
  iIntros "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
  iPvs (own_alloc_strong ( Excl' false   Excl' false,
    Some (to_agree (Next (iProp_unfold Q)))) _ (dom _ f))
    as {γ} "[Hdom Hγ]"; first done.
  rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
  iDestruct "Hdom" as % ?%not_elem_of_dom.
  iPvs (inv_alloc N _ (box_inv γ Q) with "[Hγ]") as "#Hinv"; first done.
  { iNext. iExists false. by repeat iSplit. }
  iPvsIntro; iExists γ; repeat iSplit; auto.
  iNext. iExists (<[γ:=Q]> Φ); iSplit.
  - iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
  - rewrite (big_sepM_fn_insert (λ _ _ P',  _  _ _ P'  _ _ (_ _ P')))%I //.
    iFrame "Hf Hγ'". by iSplit.
Qed.

Lemma box_delete f P Q γ :
  f !! γ = Some false 
  (box_slice N γ Q   box N f P)  |={N}=>  P',
      (P  (Q  P'))   box N (delete γ f) P'.
Proof.
  iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
  iExists ([ map] γ'↦_  delete γ f, Φ γ')%I.
  iInv N as {b} "(Hγ & #HγQ &_)"; iPvsIntro; iNext.
  iDestruct (big_sepM_delete _ f _ false with "Hf")
    as "[[Hγ' #[HγΦ ?]] ?]"; first done.
  iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by iSplit.
  iDestruct (box_own_auth_agree γ b false with "[#]")
    as "%"; subst; first by iFrame "Hγ".
  iSplitL "Hγ"; last iSplit.
  - iExists false; repeat iSplit; auto.
  - iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
  - iExists Φ; by iSplit; [iNext|].
Qed.

Lemma box_fill f γ b P Q :
  f !! γ = Some b 
  (box_slice N γ Q   Q   box N f P)  |={N}=>  box N (<[γ:=true]> f) P.
Proof.
  iIntros {?} "(#Hinv & HQ & H)"; iDestruct "H" as {Φ} "[#HeqP Hf]".
  iInv N as {b'} "(Hγ & #HγQ & _)"; iTimeless "Hγ".
  iDestruct (big_sepM_later _ f with "Hf") as "Hf".
  iDestruct (big_sepM_delete _ f _ b with "Hf")
    as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
  iPvs (box_own_auth_update _ γ b' b true with "[Hγ Hγ']")
    as "[Hγ Hγ']"; first by iFrame "Hγ".
  iPvsIntro; iNext; iSplitL "Hγ HQ"; first (iExists true; by iFrame "Hγ HQ").
  iExists Φ; iSplit.
147
  - by rewrite big_sepM_insert_override.
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
  - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    iFrame "Hγ'". by repeat iSplit.
Qed.

Lemma box_empty f P Q γ :
  f !! γ = Some true 
  (box_slice N γ Q   box N f P)  |={N}=>  Q   box N (<[γ:=false]> f) P.
Proof.
  iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
  iInv N as {b} "(Hγ & #HγQ & HQ)"; iTimeless "Hγ".
  iDestruct (big_sepM_later _ f with "Hf") as "Hf".
  iDestruct (big_sepM_delete _ f _ true with "Hf")
    as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
  iDestruct (box_own_auth_agree γ b true with "[#]")
    as "%"; subst; first by iFrame "Hγ".
  iFrame "HQ".
  iPvs (box_own_auth_update _ γ true true false with "[Hγ Hγ']")
    as "[Hγ Hγ']"; first by iFrame "Hγ".
  iPvsIntro; iNext; iSplitL "Hγ"; first (iExists false; by repeat iSplit).
  iExists Φ; iSplit.
168
  - by rewrite big_sepM_insert_override.
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
  - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    iFrame "Hγ'". by repeat iSplit.
Qed.

Lemma box_fill_all f P Q :
  (box N f P   P)  |={N}=> box N (const true <$> f) P.
Proof.
  iIntros "[H HP]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
  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".
  rewrite big_sepM_fmap; iApply (pvs_big_sepM _ _ f).
  iApply (big_sepM_impl _ _ f); iFrame "Hf".
  iAlways; iIntros {γ b' ?} "[(Hγ' & #$ & #$) HΦ]".
  iInv N as {b} "[Hγ _]"; iTimeless "Hγ".
  iPvs (box_own_auth_update _ γ b b' true with "[Hγ Hγ']")
    as "[Hγ $]"; first by iFrame "Hγ".
  iPvsIntro; iNext; iExists true. by iFrame "HΦ Hγ".
Qed.

Lemma box_empty_all f P Q :
  map_Forall (λ _, (true =)) f 
  box N f P  |={N}=>  P  box N (const false <$> f) P.
Proof.
  iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
  iAssert ([ map] γ↦b  f,  Φ γ  box_own_auth γ ( Excl' false) 
    box_own_prop γ (Φ γ)  inv N (box_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]".
  { iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
    iAlways; iIntros {γ b ?} "(Hγ' & #$ & #$)".
    assert (true = b) as <- by eauto.
    iInv N as {b} "(Hγ & _ & HΦ)"; iTimeless "Hγ".
    iDestruct (box_own_auth_agree γ b true with "[#]")
      as "%"; subst; first by iFrame "Hγ".
    iPvs (box_own_auth_update _ γ true true false with "[Hγ Hγ']")
      as "[Hγ $]"; first by iFrame "Hγ".
    iPvsIntro; iNext. iFrame "HΦ". iExists false. by iFrame "Hγ"; iSplit. }
  iPvsIntro; iSplitL "HΦ".
  - rewrite eq_iff later_iff big_sepM_later. by iApply "HeqP".
  - iExists Φ; iSplit; by rewrite big_sepM_fmap.
Qed.
End box.
210
211

Typeclasses Opaque box_slice box.