wsat.v 8.7 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Export coPset.
2
From iris.proofmode Require Import tactics.
3 4
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic.lib Require Export own.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7 8 9
(** All definitions in this file are internal to [fancy_updates] with the
exception of what's in the [invG] module. The module [invG] is thus exported in
[fancy_updates], which [wsat] is only imported. *)
10 11
Module invG.
  Class invG (Σ : gFunctors) : Set := WsatG {
12
    inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ)))));
13 14 15 16 17 18 19
    enabled_inG :> inG Σ coPset_disjR;
    disabled_inG :> inG Σ (gset_disjR positive);
    invariant_name : gname;
    enabled_name : gname;
    disabled_name : gname;
  }.

20
  Definition invΣ : gFunctors :=
21
    #[GFunctor (authRF (gmapURF positive (agreeRF (laterOF idOF))));
22 23
      GFunctor coPset_disjUR;
      GFunctor (gset_disjUR positive)].
24

25
  Class invPreG (Σ : gFunctors) : Set := WsatPreG {
26
    inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ)))));
27 28 29
    enabled_inPreG :> inG Σ coPset_disjR;
    disabled_inPreG :> inG Σ (gset_disjR positive);
  }.
30

Robbert Krebbers's avatar
Robbert Krebbers committed
31 32
  Instance subG_invΣ {Σ} : subG invΣ Σ  invPreG Σ.
  Proof. solve_inG. Qed.
33 34 35
End invG.
Import invG.

36 37
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
  to_agree (Next (iProp_unfold P)).
38
Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
39
  own invariant_name ( {[ i := invariant_unfold P ]}).
40
Arguments ownI {_ _} _ _%I.
41
Typeclasses Opaque ownI.
42 43
Instance: Params (@invariant_unfold) 1 := {}.
Instance: Params (@ownI) 3 := {}.
44

45
Definition ownE `{!invG Σ} (E : coPset) : iProp Σ :=
46 47
  own enabled_name (CoPset E).
Typeclasses Opaque ownE.
48
Instance: Params (@ownE) 3 := {}.
49

50
Definition ownD `{!invG Σ} (E : gset positive) : iProp Σ :=
51 52
  own disabled_name (GSet E).
Typeclasses Opaque ownD.
53
Instance: Params (@ownD) 3 := {}.
54

55
Definition wsat `{!invG Σ} : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  locked ( I : gmap positive (iProp Σ),
57 58
    own invariant_name ( (invariant_unfold <$> I : gmap _ _)) 
    [ map] i  Q  I,  Q  ownD {[i]}  ownE {[i]})%I.
59

60
Section wsat.
61
Context `{!invG Σ}.
62 63
Implicit Types P : iProp Σ.

Robbert Krebbers's avatar
Robbert Krebbers committed
64
(* Invariants *)
65 66
Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
Proof. solve_contractive. Qed.
67
Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
68
Proof. solve_contractive. Qed.
69
Global Instance ownI_persistent i P : Persistent (ownI i P).
70
Proof. rewrite /ownI. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71

72
Lemma ownE_empty : (|==> ownE )%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Proof.
Ralf Jung's avatar
Ralf Jung committed
74
  rewrite /uPred_valid /bi_emp_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
75 76
  by rewrite (own_unit (coPset_disjUR) enabled_name).
Qed.
77
Lemma ownE_op E1 E2 : E1 ## E2  ownE (E1  E2)  ownE E1  ownE E2.
78
Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
79
Lemma ownE_disjoint E1 E2 : ownE E1  ownE E2  E1 ## E2.
80
Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed.
81
Lemma ownE_op' E1 E2 : E1 ## E2  ownE (E1  E2)  ownE E1  ownE E2.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof.
83
  iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
84
  iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
85
  iSplit; first done. iApply ownE_op; by try iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Qed.
87
Lemma ownE_singleton_twice i : ownE {[i]}  ownE {[i]}  False.
88
Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
89

90
Lemma ownD_empty : (|==> ownD )%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Proof.
Ralf Jung's avatar
Ralf Jung committed
92
  rewrite /uPred_valid /bi_emp_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94
  by rewrite (own_unit (gset_disjUR positive) disabled_name).
Qed.
95
Lemma ownD_op E1 E2 : E1 ## E2  ownD (E1  E2)  ownD E1  ownD E2.
96
Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
97
Lemma ownD_disjoint E1 E2 : ownD E1  ownD E2  E1 ## E2.
98
Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
99
Lemma ownD_op' E1 E2 : E1 ## E2  ownD (E1  E2)  ownD E1  ownD E2.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Proof.
101
  iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
102
  iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
103
  iSplit; first done. iApply ownD_op; by try iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
Qed.
105
Lemma ownD_singleton_twice i : ownD {[i]}  ownD {[i]}  False.
106 107
Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.

108
Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
109
  own invariant_name ( (invariant_unfold <$> I : gmap _ _)) 
110
  own invariant_name ( {[i := invariant_unfold P]}) 
Ralf Jung's avatar
Ralf Jung committed
111
   Q, I !! i = Some Q   (Q  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Proof.
113
  rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
114 115
  iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
  iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
116
  rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.
117 118 119 120 121 122 123
  case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
  iExists Q; iSplit; first done.
  iAssert (invariant_unfold Q  invariant_unfold P)%I as "?".
  { case: (I' !! i)=> [Q'|] //=.
    iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI.
    iRewrite -"HvI" in "HI". by rewrite agree_idemp. }
  rewrite /invariant_unfold.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
  by rewrite agree_equivI bi.later_equivI iProp_unfold_equivI.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Qed.
126

127
Lemma ownI_open i P : wsat  ownI i P  ownE {[i]}  wsat   P  ownD {[i]}.
128
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  rewrite /ownI /wsat -!lock.
130
  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
131
  iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
132
  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
133
  - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
134
    iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
135
    iFrame "HI"; eauto.
136
  - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
137
Qed.
138
Lemma ownI_close i P : wsat  ownI i P   P  ownD {[i]}  wsat  ownE {[i]}.
139
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  rewrite /ownI /wsat -!lock.
141
  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
142
  iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
143
  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
144
  - iDestruct (ownD_singleton_twice with "[$]") as %[].
145
  - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
146 147 148 149 150
    iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
Qed.

Lemma ownI_alloc φ P :
  ( E : gset positive,  i, i  E  φ i) 
Ralf Jung's avatar
Ralf Jung committed
151
  wsat   P ==  i, ⌜φ i  wsat  ownI i P.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
  iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
154
  iDestruct "Hw" as (I) "[Hw HI]".
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
156
  iMod (own_updateP with "[$]") as "HE".
157
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None  φ i)).
158 159 160
    intros E. destruct (Hfresh (E  dom _ I))
      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
  iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
161
  iMod (own_update with "Hw") as "[Hw HiP]".
162 163
  { eapply auth_update_alloc,
     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
164
    by rewrite /= lookup_fmap HIi. }
165
  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
166 167
  iExists (<[i:=P]>I); iSplitL "Hw".
  { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
168
  iApply (big_sepM_insert _ I); first done.
169
  iFrame "HI". iLeft. by rewrite /ownD; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Qed.
171 172 173 174 175

Lemma ownI_alloc_open φ P :
  ( E : gset positive,  i, i  E  φ i) 
  wsat ==  i, ⌜φ i  (ownE {[i]} - wsat)  ownI i P  ownD {[i]}.
Proof.
176
  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
178
  iMod (own_updateP with "[$]") as "HD".
179 180 181 182 183 184 185 186 187 188 189 190
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None  φ i)).
    intros E. destruct (Hfresh (E  dom _ I))
      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
  iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
  iMod (own_update with "Hw") as "[Hw HiP]".
  { eapply auth_update_alloc,
     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
    by rewrite /= lookup_fmap HIi. }
  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
  rewrite -/(ownD _). iFrame "HD".
  iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
  { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
191
  iApply (big_sepM_insert _ I); first done.
192 193
  iFrame "HI". by iRight.
Qed.
194
End wsat.
195 196

(* Allocation of an initial world *)
197
Lemma wsat_alloc `{!invPreG Σ} : (|==>  _ : invG Σ, wsat  ownE )%I.
198 199
Proof.
  iIntros.
200
  iMod (own_alloc ( ( : gmap positive _))) as (γI) "HI";
201
    first by rewrite auth_auth_valid.
202 203 204 205 206 207
  iMod (own_alloc (CoPset )) as (γE) "HE"; first done.
  iMod (own_alloc (GSet )) as (γD) "HD"; first done.
  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
  rewrite /wsat /ownE -lock; iFrame.
  iExists . rewrite fmap_empty big_opM_empty. by iFrame.
Qed.