wsat.v 7.41 KB
Newer Older
1
2
From iris.program_logic Require Export iris.
From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
3
From iris.proofmode Require Import tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

5
6
7
8
9
10
11
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
  to_agree (Next (iProp_unfold P)).
Definition ownI `{irisG Λ Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
  own invariant_name ( {[ i := invariant_unfold P ]}).
Arguments ownI {_ _ _} _ _%I.
Typeclasses Opaque ownI.
Instance: Params (@ownI) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
12

13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
Definition ownP `{irisG Λ Σ} (σ : state Λ) : iProp Σ :=
  own state_name ( (Excl' σ)).
Typeclasses Opaque ownP.
Instance: Params (@ownP) 4.

Definition ownP_auth `{irisG Λ Σ} (σ : state Λ) : iProp Σ :=
  own state_name ( (Excl' σ)).
Typeclasses Opaque ownP_auth.
Instance: Params (@ownP_auth) 4.

Definition ownE `{irisG Λ Σ} (E : coPset) : iProp Σ :=
  own enabled_name (CoPset E).
Typeclasses Opaque ownE.
Instance: Params (@ownE) 4.

Definition ownD `{irisG Λ Σ} (E : gset positive) : iProp Σ :=
  own disabled_name (GSet E).
Typeclasses Opaque ownD.
Instance: Params (@ownD) 4.

Definition wsat `{irisG Λ Σ} : iProp Σ :=
  ( I : gmap positive (iProp Σ),
    own invariant_name ( (invariant_unfold <$> I : gmap _ _)) 
    [ map] i  Q  I,  Q  ownD {[i]}  ownE {[i]})%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
37

Robbert Krebbers's avatar
Robbert Krebbers committed
38
Section ownership.
39
Context `{irisG Λ Σ}.
40
Implicit Types σ : state Λ.
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
Implicit Types P : iProp Σ.

(* Allocation *)
Lemma iris_alloc `{irisPreG Λ Σ} σ :
  True =r=>  _ : irisG Λ Σ, wsat  ownE   ownP_auth σ  ownP σ.
Proof.
  iIntros.
  iVs (own_alloc ( (Excl' σ)   (Excl' σ))) as (γσ) "[Hσ Hσ']"; first done.
  iVs (own_alloc ( ( : gmap _ _))) as (γI) "HI"; first done.
  iVs (own_alloc (CoPset )) as (γE) "HE"; first done.
  iVs (own_alloc (GSet )) as (γD) "HD"; first done.
  iVsIntro; iExists (IrisG _ _ _ γσ γI γE γD).
  rewrite /wsat /ownE /ownP_auth /ownP; iFrame.
  iExists . rewrite fmap_empty big_sepM_empty. by iFrame.
Qed.

(* Physical state *)
Lemma ownP_twice σ1 σ2 : ownP σ1  ownP σ2  False.
59
Proof. rewrite /ownP own_valid_2. by iIntros (?). Qed.
60
61
62
63
64
Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ _ σ).
Proof. rewrite /ownP; apply _. Qed.

Lemma ownP_agree σ1 σ2 : ownP_auth σ1  ownP σ2  σ1 = σ2.
Proof.
65
  rewrite /ownP /ownP_auth own_valid_2 -auth_both_op.
66
67
68
69
  by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
Qed.
Lemma ownP_update σ1 σ2 : ownP_auth σ1  ownP σ1 =r=> ownP_auth σ2  ownP σ2.
Proof.
70
71
  rewrite /ownP -!own_op.
  by apply own_update, auth_update, option_local_update, exclusive_local_update.
72
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74

(* Invariants *)
75
Global Instance ownI_contractive i : Contractive (@ownI Λ Σ _ i).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
77
78
  intros n P Q HPQ. rewrite /ownI /invariant_unfold. do 4 f_equiv.
  apply Next_contractive=> j ?; by rewrite (HPQ j).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
80
81
Global Instance ownI_persistent i P : PersistentP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82

83
84
85
86
87
Lemma ownE_empty : True =r=> ownE .
Proof. by rewrite (own_empty (A:=coPset_disjUR) enabled_name). Qed.
Lemma ownE_op E1 E2 : E1  E2  ownE (E1  E2)  ownE E1  ownE E2.
Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
Lemma ownE_disjoint E1 E2 : ownE E1  ownE E2  E1  E2.
88
Proof. rewrite /ownE own_valid_2. by iIntros (?%coPset_disj_valid_op). Qed.
89
Lemma ownE_op' E1 E2 : E1  E2  ownE (E1  E2)  ownE E1  ownE E2.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Proof.
91
  iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
92
  iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
93
  iSplit; first done. iApply ownE_op; by try iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
Qed.
95
96
Lemma ownE_singleton_twice i : ownE {[i]}  ownE {[i]}  False.
Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
97

98
99
100
101
102
Lemma ownD_empty : True =r=> ownD .
Proof. by rewrite (own_empty (A:=gset_disjUR _) disabled_name). Qed.
Lemma ownD_op E1 E2 : E1  E2  ownD (E1  E2)  ownD E1  ownD E2.
Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
Lemma ownD_disjoint E1 E2 : ownD E1  ownD E2  E1  E2.
103
Proof. rewrite /ownD own_valid_2. by iIntros (?%gset_disj_valid_op). Qed.
104
Lemma ownD_op' E1 E2 : E1  E2  ownD (E1  E2)  ownD E1  ownD E2.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
Proof.
106
  iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
107
  iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
108
  iSplit; first done. iApply ownD_op; by try iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Qed.
110
111
112
113
114
115
116
Lemma ownD_singleton_twice i : ownD {[i]}  ownD {[i]}  False.
Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.

Lemma invariant_lookup `{irisG Λ Σ} (I : gmap positive (iProp Σ)) i P :
  own invariant_name ( (invariant_unfold <$> I : gmap _ _)) 
  own invariant_name ( {[i := invariant_unfold P]}) 
   Q, I !! i = Some Q   (Q  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Proof.
118
  rewrite own_valid_2 auth_validI /=. iIntros "[#HI #HvI]".
119
120
121
122
123
124
125
126
127
128
  iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
  iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
  rewrite left_id_L lookup_fmap lookup_op lookup_singleton uPred.option_equivI.
  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.
129
  by rewrite agree_equivI uPred.later_equivI iProp_unfold_equivI.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Qed.
131
132
133
134

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

Lemma ownI_alloc φ P :
  ( E : gset positive,  i, i  E  φ i) 
  wsat   P =r=>  i,  (φ i)  wsat  ownI i P.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Proof.
156
157
158
  iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
  iVs (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
  iVs (own_updateP with "HE") as "HE".
159
  { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None  φ i)).
160
161
162
163
    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 & ?).
  iVs (own_update with "Hw") as "[Hw HiP]".
164
165
  { eapply auth_update_alloc,
     (alloc_singleton_local_update _ i (invariant_unfold P)); last done.
166
167
168
169
170
171
    by rewrite /= lookup_fmap HIi. }
  iVsIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
  iExists (<[i:=P]>I); iSplitL "Hw".
  { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
  iApply (big_sepM_insert _ I); first done.
  iFrame "HI". iLeft. by rewrite /ownD; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
Qed.
End ownership.