boxes.v 8.19 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
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)))).

22
  Definition box_slice_inv (γ : gname) (P : iProp) : iProp :=
23 24 25
    ( b, box_own_auth γ ( Excl' b)  box_own_prop γ P  if b then P else True)%I.

  Definition box_slice (γ : gname) (P : iProp) : iProp :=
26
    inv N (box_slice_inv γ P).
27 28 29 30 31

  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 γ (Φ γ) 
32
                         inv N (box_slice_inv γ (Φ γ)))%I.
33 34
End box_defs.

35 36
Instance: Params (@box_own_auth) 4.
Instance: Params (@box_own_prop) 4.
37
Instance: Params (@box_slice_inv) 4.
38 39 40
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
(* FIXME: solve_proper picks the eq ==> instance for Next. *)
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) (box_slice_inv γ).
50 51 52 53 54 55 56 57 58
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
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 :
64
  box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2)  b1 = b2.
65 66 67 68 69 70 71
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 :
72 73
  box_own_auth γ ( Excl' b1)  box_own_auth γ ( Excl' b2)
  ={E}=> box_own_auth γ ( Excl' b3)  box_own_auth γ ( Excl' b3).
74 75 76
Proof.
  rewrite /box_own_prop -!own_op.
  apply own_update, prod_update; simpl; last reflexivity.
77
  apply (auth_local_update (λ _, Excl' b3)). apply _. done.
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
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 :
97
   box N f P ={N}=>  γ, f !! γ = None 
98 99 100 101 102 103 104 105
    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.
106
  iPvs (inv_alloc N _ (box_slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done.
107
  { iNext. iExists false; eauto. }
108 109 110 111
  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 //.
112
    iFrame; eauto.
113 114 115 116
Qed.

Lemma box_delete f P Q γ :
  f !! γ = Some false 
117
  box_slice N γ Q   box N f P ={N}=>  P',
118 119 120 121 122 123 124
      (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.
125
  iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
126
  iDestruct (box_own_auth_agree γ b false with "[#]")
127
    as "%"; subst; first by iFrame.
128
  iSplitL "Hγ"; last iSplit.
129
  - iExists false; eauto.
130
  - iNext. iRewrite "HeqP". iRewrite "HeqQ". by rewrite -big_sepM_delete.
131
  - iExists Φ; eauto.
132 133
Qed.

134 135
Lemma box_fill f γ P Q :
  f !! γ = Some false 
136
  box_slice N γ Q   Q   box N f P ={N}=>  box N (<[γ:=true]> f) P.
137 138 139 140
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".
141
  iDestruct (big_sepM_delete _ f _ false with "Hf")
142
    as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
143
  iPvs (box_own_auth_update _ γ b' false true with "[Hγ Hγ']")
144
    as "[Hγ Hγ']"; first by iFrame.
145 146
  iPvsIntro; iNext; iSplitL "Hγ HQ"; first (iExists true; by iFrame "Hγ HQ").
  iExists Φ; iSplit.
147
  - by rewrite big_sepM_insert_override.
148
  - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
149
    iFrame; eauto.
150 151 152 153
Qed.

Lemma box_empty f P Q γ :
  f !! γ = Some true 
154
  box_slice N γ Q   box N f P ={N}=>  Q   box N (<[γ:=false]> f) P.
155 156 157 158
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".
Ralf Jung's avatar
Ralf Jung committed
159
  iDestruct (big_sepM_delete _ f with "Hf")
160 161
    as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
  iDestruct (box_own_auth_agree γ b true with "[#]")
162
    as "%"; subst; first by iFrame.
163
  iFrame "HQ".
Ralf Jung's avatar
Ralf Jung committed
164
  iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
165
    as "[Hγ Hγ']"; first by iFrame.
166 167
  iPvsIntro; iNext; iSplitL "Hγ"; first (iExists false; by repeat iSplit).
  iExists Φ; iSplit.
168
  - by rewrite big_sepM_insert_override.
169
  - rewrite -insert_delete big_sepM_insert ?lookup_delete //.
170
    iFrame; eauto.
171 172
Qed.

173
Lemma box_fill_all f P Q : box N f P   P ={N}=> box N (const true <$> f) P.
174 175 176 177 178 179 180 181 182
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γ".
Ralf Jung's avatar
Ralf Jung committed
183
  iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
184 185
    as "[Hγ $]"; first by iFrame.
  iPvsIntro; iNext; iExists true. by iFrame.
186 187 188 189
Qed.

Lemma box_empty_all f P Q :
  map_Forall (λ _, (true =)) f 
190
  box N f P ={N}=>  P  box N (const false <$> f) P.
191 192 193
Proof.
  iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
  iAssert ([ map] γ↦b  f,  Φ γ  box_own_auth γ ( Excl' false) 
194
    box_own_prop γ (Φ γ)  inv N (box_slice_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]".
195 196 197 198 199
  { 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 "[#]")
200
      as "%"; subst; first by iFrame.
201
    iPvs (box_own_auth_update _ γ true true false with "[Hγ Hγ']")
202 203
      as "[Hγ $]"; first by iFrame.
    iPvsIntro; iNext. iFrame "HΦ". iExists false. iFrame; eauto. }
204 205 206 207 208
  iPvsIntro; iSplitL "HΦ".
  - rewrite eq_iff later_iff big_sepM_later. by iApply "HeqP".
  - iExists Φ; iSplit; by rewrite big_sepM_fmap.
Qed.
End box.
209 210

Typeclasses Opaque box_slice box.