ghost_ownership.v 12.9 KB
Newer Older
1
From stdpp Require Export functions.
2
From fri.algebra Require Export iprod upred.
3
4
From fri.program_logic Require Export pviewshifts pstepshifts global_functor.
From fri.program_logic Require Import ownership.
5
From iris.proofmode Require Import tactics classes.
6
Import uPred.
7
Definition own_def `{inG Λ Σ (gmapUR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
8
  ownG (to_globalF γ a).
9
10
11
Definition own_aux : { x | x = @own_def }. by eexists. Qed.
Definition own {Λ Σ A i} := proj1_sig own_aux Λ Σ A i.
Definition own_eq : @own = @own_def := proj2_sig own_aux.
12
Instance: Params (@own) 5.
13
Typeclasses Opaque own.
14

15
16
17
18
19
Definition ownl_def `{inG Λ Σ (gmapUR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
  ownGl (to_globalF γ a).
Definition ownl_aux : { x | x = @ownl_def }. by eexists. Qed.
Definition ownl {Λ Σ A i} := proj1_sig ownl_aux Λ Σ A i.
Definition ownl_eq : @ownl = @ownl_def := proj2_sig ownl_aux.
20
Instance: Params (@ownl) 5.
21
Typeclasses Opaque ownl.
22

23
Definition owne_def `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
24
  ownG (to_globalFe a).
25
26
27
28
29
30
31
Definition owne_aux : { x | x = @owne_def }. by eexists. Qed.
Definition owne {Λ Σ A i} := proj1_sig owne_aux Λ Σ A i.
Definition owne_eq : @owne = @owne_def := proj2_sig owne_aux.
Instance: Params (@owne) 4.
Typeclasses Opaque owne.

Definition ownle_def `{inG Λ Σ A} (a : A) : iPropG Λ Σ :=
32
  ownGl (to_globalFe a).
33
34
35
Definition ownle_aux : { x | x = @ownle_def }. by eexists. Qed.
Definition ownle {Λ Σ A i} := proj1_sig ownle_aux Λ Σ A i.
Definition ownle_eq : @ownle = @ownle_def := proj2_sig ownle_aux.
36
Instance: Params (@ownle) 4.
37
Typeclasses Opaque ownle.
38

39
40
41

(** Properties about ghost ownership *)
Section global.
42
Context `{i : inG Λ Σ (gmapUR gname A)}.
43
Implicit Types a : A.
44
45

(** * Properties of own *)
46
Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Λ Σ A _ γ).
47
Proof. rewrite !own_eq. solve_proper. Qed.
48
49
Global Instance own_proper γ :
  Proper (() ==> (⊣⊢)) (@own Λ Σ A _ γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
50

51
Lemma own_op γ a1 a2 : own γ (a1  a2) ⊣⊢ own γ a1  own γ a2.
52
Proof. by rewrite !own_eq /own_def -ownG_op to_globalF_op. Qed.
53

54
Global Instance own_mono γ : Proper (flip () ==> ()) (@own Λ Σ A _ γ).
55
Proof. 
56
  move=>a b [c ->]. rewrite own_op own_eq /own. apply sep_elim_l. apply _.
57
Qed.
58
59
60
Global Instance into_sep_own γ a1 a2:
  IntoSep (own γ (a1  a2)) (own γ a1) (own γ a2).
Proof. rewrite /IntoSep own_op //=. Qed.
61
62
63
Global Instance from_sep_own γ a1 a2:
  FromSep (own γ (a1  a2)) (own γ a1) (own γ a2).
Proof. rewrite /FromSep own_op //=. Qed.
64

65
Lemma own_valid γ a : own γ a  ⧆✓ a.
66
Proof.
67
  rewrite !own_eq /own_def ownG_valid /to_globalF.
68
  rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
69
  apply affinely_mono.
70
71
  trans ( ucmra_transport (@inG_prf _ _ _ i) {[γ := a]} : iPropG Λ Σ)%I;
    last destruct inG_prf; auto.
72
  by rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
73
Qed.
74
Lemma own_valid_r γ a : own γ a  (own γ a  ⧆✓ a).
75
76
77
78
79
Proof.
  iIntros "H". iAssert (bi_affinely ( a))%I with "[#]" as "$"; last done.
  rewrite /bi_absorbingly; iSplitR "H"; auto.
  by iApply own_valid.
Qed.
80
Lemma own_valid_l γ a : own γ a  (⧆✓ a  own γ a).
81
Proof. by rewrite comm -own_valid_r. Qed.
82
83
Global Instance own_atimeless γ a : Discrete a  ATimeless (own γ a).
Proof. rewrite !own_eq /own_def. apply _. Qed.
84
Global Instance own_affine γ a : Affine (own γ a).
85
Proof. rewrite !own_eq /own_def; apply _. Qed.
86
Global Instance own_core_persistent γ a : cmra.Persistent a  Persistent (own γ a).
87
Proof. rewrite !own_eq /own_def; apply _. Qed.
88

Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
(* TODO: This also holds if we just have  a at the current step-idx, as Iris
   assertion. However, the map_updateP_alloc does not suffice to show this. *)
91

92
Lemma own_alloc_strong a E (G : gset gname) :
93
   a  emp  |={E}=>  γ, (γ  G)  own γ a.
94
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  intros Ha.
96
  rewrite -(pvs_mono _ _ ( m,  ( γ, γ  G  m = to_globalF γ a)  ownG m)%I).
97
  - rewrite ownG_empty. eapply pvs_ownG_updateP. 
98
99
    eapply (iprod_singleton_updateP_empty (inG_id i)
              (λ y,  γ, γ  G  iprod_singleton (inG_id i) y = to_globalF γ a)).
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
    * rewrite -(ucmra_transport_unit inG_prf).
      eapply ucmra_transport_updateP; first by eapply alloc_updateP_strong'; eauto.
102
103
104
      intros ? (γ&?&?&?); subst.
      exists γ. split_and!; eauto.
    * naive_solver.
105
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
106
    by rewrite !own_eq -(exist_intro γ) pure_True // left_id.
107
Qed.
108
Lemma own_alloc_strong' a E (G : gset gname) :
109
   a  emp  |={E}=>  γ, ⧆■(γ  G)  own γ a.
110
111
112
Proof. 
  intros Ha. rewrite (own_alloc_strong a E G); auto.
  apply pvs_mono, exist_mono=>?.
113
114
  rewrite -(affine_affinely (own _ _)) affinely_and_r affinely_and.
  by iIntros "(H1&H2)"; iFrame.
115
Qed.
116
117

Lemma own_alloc a E :  a  emp  (|={E}=>  γ, own γ a).
118
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
120
  intros Ha. rewrite (own_alloc_strong a E ) //; [].
  apply pvs_mono, exist_mono=>?. eauto with I.
121
Qed.
122

123
Lemma own_updateP P γ a E : a ~~>: P  own γ a ={E}=>  a',  P a'  own γ a'.
124
Proof.
125
  intros Ha. rewrite !own_eq.
126
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalF γ a'  P a')  ownG m)%I).
127
  - eapply pvs_ownG_updateP, iprod_singleton_updateP;
128
    first by (apply ucmra_transport_updateP', singleton_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
129
    naive_solver.
130
131
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
132
133
Qed.

134
Lemma own_update γ a a' E : a ~~> a'  own γ a ={E}=> own γ a'.
135
Proof.
136
  intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
137
  by apply pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
138
Qed.
139
End global.
140

141
142
143
144
145
146
Arguments own_valid {_ _ _} [_] _ _.
Arguments own_valid_l {_ _ _} [_] _ _.
Arguments own_valid_r {_ _ _} [_] _ _.
Arguments own_updateP {_ _ _} [_] _ _ _ _ _.
Arguments own_update {_ _ _} [_] _ _ _ _ _.

147
Section global_empty.
148
Context `{i : inG Λ Σ (gmapUR gname (A:ucmraT))}.
149
150
Implicit Types a : A.

151
Lemma own_empty γ E : emp ={E}=> own γ (:A).
152
Proof.
153
  rewrite ownG_empty !own_eq /own_def.
154
155
156
157
158
159
160
161
162
163
164
  apply pvs_ownG_update, cmra_update_updateP.
  eapply (iprod_singleton_updateP_empty (inG_id i)
              (λ y, iprod_singleton (inG_id i) y = to_globalF γ )).
  - rewrite -(ucmra_transport_unit inG_prf).
    eapply ucmra_transport_updateP;
      first eapply (alloc_unit_singleton_updateP' _ ). 
      * apply ucmra_unit_valid.
      * apply _.
      * apply cmra_update_updateP, ucmra_update_unit.
      * naive_solver.
  - naive_solver. 
165
Qed.
166
End global_empty.
167
168
169
170
171
172
173
174

(* There is obviously some redundancy *)
(** Properties about ghost ownership in the nameless case *)
Section globale.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.

(** * Properties of own *)
175
Global Instance owne_ne n : Proper (dist n ==> dist n) (@owne Λ Σ A _).
176
Proof. rewrite !owne_eq. solve_proper. Qed.
177
Global Instance owne_proper : Proper (() ==> (⊣⊢)) (@owne Λ Σ A _) := ne_proper _.
178
179

Lemma owne_op a1 a2 : owne (a1  a2) ⊣⊢ (owne a1  owne a2).
180
Proof. by rewrite !owne_eq /owne_def -ownG_op to_globalFe_op. Qed.
181
Global Instance owne_mono : Proper (flip () ==> ()) (@owne Λ Σ A _).
182
Proof. move=>a b [c ->]. rewrite !owne_eq /owne_def //= /to_globalFe.
183
       eapply ownG_mono. simpl.
184
       rewrite ucmra_transport_op -iprod_op_singleton.
185
186
187
188
       eexists; eauto.
Qed.

Lemma owne_valid a : owne a  ⧆✓ a.
189
Proof.
190
191
  rewrite !owne_eq /owne_def ownG_valid /to_globalFe.
  rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
192
  apply affinely_mono.
193
  trans ( ucmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
194
Qed.
195
Lemma owne_valid_r a : owne a  (owne a  ⧆✓ a).
196
197
198
199
200
Proof.
  iIntros "H". iAssert (bi_affinely ( a))%I with "[#]" as "$"; last done.
  rewrite /bi_absorbingly; iSplitR "H"; auto.
  by iApply owne_valid.
Qed.
201
Lemma owne_valid_l a : owne a  (⧆✓ a  owne a).
202
Proof. by rewrite comm -owne_valid_r. Qed.
203
Global Instance owne_atimeless a : Discrete a  ATimeless (owne a).
204
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
205
Global Instance owne_affine a : Affine (owne a).
206
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
207
Global Instance owne_core_persistent a : cmra.Persistent a  Persistent (owne a).
208
Proof. rewrite !owne_eq /owne_def; apply _. Qed.
209
210
211
212
213
214
215

(* TODO: This also holds if we just have  a at the current step-idx, as Iris
   assertion. However, the map_updateP_alloc does not suffice to show this. *)

Lemma owne_updateP P a E :
  a ~~>: P  owne a  (|={E}=>  a',  P a'  owne a').
Proof.
216
  intros Ha. rewrite !owne_eq.
217
218
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalFe a'  P a')  ownG m)%I).
  - eapply pvs_ownG_updateP, iprod_singleton_updateP;
219
    first by (apply ucmra_transport_updateP',  Ha).
220
    naive_solver.
221
222
  - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
223
224
225
226
Qed.

Lemma owne_update a a' E : a ~~> a'  owne a  (|={E}=> owne a').
Proof.
227
  intros; rewrite (owne_updateP (a' =)); last by apply cmra_update_updateP.
228
  by apply pvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
229
230
Qed.

231
Lemma owne_empty E :
232
  emp ={E}=> owne (:A).
233
Proof.
234
235
236
237
238
239
240
241
  rewrite ownG_empty !owne_eq /owne_def. apply pvs_ownG_update, cmra_update_updateP.
  eapply (iprod_singleton_updateP_empty (inG_id i)
              (λ y, iprod_singleton (inG_id i) y = to_globalFe )).
  - rewrite -(ucmra_transport_unit inG_prf).
    eapply ucmra_transport_updateP;
      first eapply cmra_update_updateP, ucmra_update_unit.
      naive_solver.
  - naive_solver. 
242
Qed.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
243
244
245
246
247
248

Section globale_step.
  
  Definition trivial_step (A: cmraT) :=
     (a a': A) n, a _(n) a'.

249
  Context (AltTriv:  (gid': gid Σ) A, gid'  (inG_id i) 
Robbert Krebbers's avatar
Robbert Krebbers committed
250
                                        A = projT2 Σ gid' (iPreProp Λ (globalF Σ)) _  
Joseph Tassarotti's avatar
Joseph Tassarotti committed
251
252
253
254
255
256
                                        trivial_step A).
  
  Lemma owne_stepP P (a al: A) E :
    a # al ~~>>: P  (owne a   ownle al) 
                        (|={E}=>>  a' al', ⧆■ P a' al'  owne a'  ownle al').
  Proof.
257
  rewrite owne_eq /owne_def ownle_eq /ownle_def cmra_total_step_updateP=>Ha.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
258
259
  rewrite -(psvs_mono _ _ ( m ml, ⧆■ ( a' al', m = to_globalFe a'  ml = to_globalFe al' 
                                                 P a' al')  ownG m  ownGl ml)%I).
260
261
262
  - eapply psvs_stepP, cmra_total_step_updateP. intros n zf Hval.
    specialize (Ha n (ucmra_transport (Coq.Init.Logic.eq_sym inG_prf) (zf (inG_id i)))).
    generalize (Hval (inG_id i)).
Joseph Tassarotti's avatar
Joseph Tassarotti committed
263
264
    unfold to_globalFe.
    rewrite ?iprod_lookup_op ?iprod_lookup_singleton.
265
266
    rewrite -(ucmra_transport_validN (Init.Logic.eq_sym inG_prf)).
    rewrite !ucmra_transport_op !ucmra_transport_sym_inv.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
267
268
269
270
271
272
    intros Hval_inG. edestruct (Ha Hval_inG) as (y&yl&?&Hval'&Hstep).
    exists (to_globalFe y), (to_globalFe yl); split_and!.
    * do 2 eexists; eauto.
    * unfold to_globalFe.
      intro X. 
      rewrite ?iprod_lookup_op.
273
      case (decide (X = (inG_id i))).
Joseph Tassarotti's avatar
Joseph Tassarotti committed
274
      ** intros ->. rewrite ?iprod_lookup_singleton.
275
276
         rewrite -(ucmra_transport_validN (Init.Logic.eq_sym inG_prf)).
         rewrite !ucmra_transport_op !ucmra_transport_sym_inv.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
277
278
279
         auto.
      ** specialize (Hval X). unfold to_globalFe in Hval.
         intros; rewrite ?iprod_lookup_op ?iprod_lookup_singleton_ne in Hval *; eauto. 
280
    * intro X. case (decide (X = (inG_id i))).
Joseph Tassarotti's avatar
Joseph Tassarotti committed
281
      ** intros ->. unfold to_globalFe. rewrite ?iprod_lookup_singleton. 
282
         apply ucmra_transport_stepN. eauto.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
283
      ** intros. eapply (AltTriv X); eauto.
284
285
286
  - iIntros "H". iDestruct "H" as (m ml) "(H&?&?)". 
    iDestruct "H" as %(a'&al'&Heq_m&Heq_ml&HP).
    subst. iExists a', al'. iFrame. iAlways; done.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
287
288
289
290
291
Qed.
  

End globale_step.

292
End globale.
293
294
295
296
297
298

Section globalle.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.

(** * Properties of own *)
299
Global Instance ownle_ne n : Proper (dist n ==> dist n) (@ownle Λ Σ A _).
300
Proof. intros x y Heq. rewrite !ownle_eq /ownle_def. solve_proper. Qed.
301
Global Instance ownle_proper : Proper (() ==> (⊣⊢)) (@ownle Λ Σ A _) := ne_proper _.
302
303

Lemma ownle_op a1 a2 : ownle (a1  a2) ⊣⊢ (ownle a1  ownle a2).
304
Proof. by rewrite !ownle_eq /ownle_def -ownGl_op to_globalFe_op. Qed.
305
306
307

Lemma ownle_valid a : ownle a ⊣⊢ (ownle a  ⧆✓ a).
Proof.
308
309
310
311
312
313
  apply (anti_symm ()).
  - rewrite !ownle_eq /ownle_def {1}ownGl_valid_r /to_globalFe.
    rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
    apply sep_mono; auto.
    trans (⧆✓ ucmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
  - iIntros "(?&_)"; done.
314
315
316
317
318
Qed.
Lemma ownle_valid_r a : ownle a  (ownle a  ⧆✓ a).
Proof. rewrite {1}ownle_valid //=. Qed.
Lemma ownle_valid_l a : ownle a  (⧆✓ a  ownle a).
Proof. by rewrite comm -ownle_valid_r. Qed.
319
320
Global Instance ownle_core_persistent a : cmra.Persistent a  Persistent ( ownle a).
Proof. rewrite !ownle_eq /ownle_def. apply _. Qed.
321

322
End globalle.