wsat.v 8.04 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Export coPset.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.algebra Require Import gmap_view gset coPset.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.proofmode Require Import proofmode.
4
From iris.base_logic.lib Require Export own.
Ralf Jung's avatar
Ralf Jung committed
5
From iris.prelude Require Import options.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7
(** All definitions in this file are internal to [fancy_updates] with the
8
exception of what's in the [invGS] module. The module [invGS] is thus exported in
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
9
[fancy_updates], where [wsat] is only imported. *)
10
11
Module invGS.
  Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
12
13
14
    invGpreS_inv : inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
    invGpreS_enabled : inG Σ coPset_disjR;
    invGpreS_disabled : inG Σ (gset_disjR positive);
15
16
  }.

17
  Class invGS (Σ : gFunctors) : Set := InvG {
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
18
    inv_inG : invGpreS Σ;
19
20
21
22
23
    invariant_name : gname;
    enabled_name : gname;
    disabled_name : gname;
  }.

24
  Definition invΣ : gFunctors :=
Ralf Jung's avatar
Ralf Jung committed
25
    #[GFunctor (gmap_viewRF positive (laterOF idOF));
26
27
      GFunctor coPset_disjR;
      GFunctor (gset_disjR positive)].
28

29
  Global Instance subG_invΣ {Σ} : subG invΣ Σ  invGpreS Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  Proof. solve_inG. Qed.
31
32
End invGS.
Import invGS.
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
33
Local Existing Instances inv_inG invGpreS_inv invGpreS_enabled invGpreS_disabled.
34

35
36
Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
  Next P.
37
Definition ownI `{!invGS Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
Ralf Jung's avatar
Ralf Jung committed
38
  own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
39
Typeclasses Opaque ownI.
40
41
Global Instance: Params (@invariant_unfold) 1 := {}.
Global Instance: Params (@ownI) 3 := {}.
42

43
Definition ownE `{!invGS Σ} (E : coPset) : iProp Σ :=
44
45
  own enabled_name (CoPset E).
Typeclasses Opaque ownE.
46
Global Instance: Params (@ownE) 3 := {}.
47

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

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

58
Section wsat.
59
Context `{!invGS Σ}.
60
61
Implicit Types P : iProp Σ.

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

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

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

106
Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
107
  own invariant_name (gmap_view_auth (DfracOwn 1) (invariant_unfold <$> I)) 
Ralf Jung's avatar
Ralf Jung committed
108
  own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)) 
Ralf Jung's avatar
Ralf Jung committed
109
   Q, I !! i = Some Q   (Q  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Proof.
Ralf Jung's avatar
Ralf Jung committed
111
  rewrite -own_op own_valid gmap_view_both_validI bi.and_elim_r.
112
113
114
115
  rewrite lookup_fmap option_equivI.
  case: (I !! i)=> [Q|] /=; last by eauto.
  iIntros "?". iExists Q; iSplit; first done.
  by rewrite later_equivI.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
Qed.
117

118
Lemma ownI_open i P : wsat  ownI i P  ownE {[i]}  wsat   P  ownD {[i]}.
119
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  rewrite /ownI /wsat -!lock.
121
  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
122
  iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
123
  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
124
  - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
125
    iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
126
    iFrame "HI"; eauto.
127
  - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
128
Qed.
129
Lemma ownI_close i P : wsat  ownI i P   P  ownD {[i]}  wsat  ownE {[i]}.
130
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
  rewrite /ownI /wsat -!lock.
132
  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
133
  iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
134
  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
135
  - iDestruct (ownD_singleton_twice with "[$]") as %[].
136
  - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
137
138
139
140
141
    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
142
  wsat   P ==  i, ⌜φ i  wsat  ownI i P.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
145
  iDestruct "Hw" as (I) "[Hw HI]".
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
147
  iMod (own_updateP with "[$]") as "HE".
148
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None  φ i)).
149
    intros E. destruct (Hfresh (E  dom I))
150
151
      as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
  iDestruct "HE" as (X) "[Hi HE]"; iDestruct "Hi" as %(i & -> & HIi & ?).
152
  iMod (own_update with "Hw") as "[Hw HiP]".
Ralf Jung's avatar
Ralf Jung committed
153
154
  { eapply (gmap_view_alloc _ i DfracDiscarded); last done.
    by rewrite /= lookup_fmap HIi. }
155
  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
156
  iExists (<[i:=P]>I); iSplitL "Hw".
157
  { by rewrite fmap_insert. }
158
  iApply (big_sepM_insert _ I); first done.
159
  iFrame "HI". iLeft. by rewrite /ownD; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
Qed.
161
162
163
164
165

Lemma ownI_alloc_open φ P :
  ( E : gset positive,  i, i  E  φ i) 
  wsat ==  i, ⌜φ i  (ownE {[i]} - wsat)  ownI i P  ownD {[i]}.
Proof.
166
  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
168
  iMod (own_updateP with "[$]") as "HD".
169
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None  φ i)).
170
    intros E. destruct (Hfresh (E  dom I))
171
172
173
      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]".
Ralf Jung's avatar
Ralf Jung committed
174
175
  { eapply (gmap_view_alloc _ i DfracDiscarded); last done.
    by rewrite /= lookup_fmap HIi. }
176
177
178
  iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
  rewrite -/(ownD _). iFrame "HD".
  iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
179
  { by rewrite fmap_insert. }
180
  iApply (big_sepM_insert _ I); first done.
181
182
  iFrame "HI". by iRight.
Qed.
183
End wsat.
184
185

(* Allocation of an initial world *)
186
Lemma wsat_alloc `{!invGpreS Σ} :  |==>  _ : invGS Σ, wsat  ownE .
187
188
Proof.
  iIntros.
189
  iMod (own_alloc (gmap_view_auth (DfracOwn 1) )) as (γI) "HI";
Ralf Jung's avatar
Ralf Jung committed
190
    first by apply gmap_view_auth_valid.
191
192
  iMod (own_alloc (CoPset )) as (γE) "HE"; first done.
  iMod (own_alloc (GSet )) as (γD) "HD"; first done.
Ralf Jung's avatar
Ralf Jung committed
193
  iModIntro; iExists (InvG _ _ γI γE γD).
194
195
196
  rewrite /wsat /ownE -lock; iFrame.
  iExists . rewrite fmap_empty big_opM_empty. by iFrame.
Qed.