ghost_ownership.v 6.72 KB
Newer Older
1
From prelude Require Export functions.
2
3
4
From algebra Require Export iprod.
From program_logic Require Export pviewshifts.
From program_logic Require Import ownership.
5
6
Import uPred.

Ralf Jung's avatar
Ralf Jung committed
7
8
9
10
11
(** Index of a CMRA in the product of global CMRAs. *)
Definition gid := nat.
(** Name of one instance of a particular CMRA in the ghost state. *)
Definition gname := positive.
(** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *)
12
Definition globalF (Σ : gid  iFunctor) : iFunctor :=
Ralf Jung's avatar
Ralf Jung committed
13
  iprodF (λ i, mapF gname (Σ i)).
14

15
16
17
18
Class inG (Λ : language) (Σ : gid  iFunctor) (A : cmraT) := InG {
  inG_id : gid;
  inG_prf : A = Σ inG_id (laterC (iPreProp Λ (globalF Σ)))
}.
19

20
Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
21
  iprod_singleton inG_id {[ γ := cmra_transport inG_prf a ]}.
22
23
24
25
Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iProp Λ (globalF Σ) :=
  ownG (to_globalF γ a).
Instance: Params (@to_globalF) 5.
Instance: Params (@own) 5.
26
27
28
29
Typeclasses Opaque to_globalF own.

Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Notation iFunctorG := (gid  iFunctor).
Robbert Krebbers's avatar
Robbert Krebbers committed
30

31
Section global.
32
Context `{i : inG Λ Σ A}.
33
34
Implicit Types a : A.

35
(** * Properties of to_globalC *)
36
Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
37
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
38
Lemma to_globalF_op γ a1 a2 :
39
  to_globalF γ (a1  a2)  to_globalF γ a1  to_globalF γ a2.
40
Proof.
41
  by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
42
Qed.
43
Lemma to_globalF_unit γ a : unit (to_globalF γ a)  to_globalF γ (unit a).
44
Proof.
45
  by rewrite /to_globalF
Robbert Krebbers's avatar
Robbert Krebbers committed
46
    iprod_unit_singleton map_unit_singleton cmra_transport_unit.
47
Qed.
48
Instance to_globalF_timeless γ m : Timeless m  Timeless (to_globalF γ m).
49
Proof. rewrite /to_globalF; apply _. Qed.
50

51
(** * Transport empty *)
52
53
Instance inG_empty `{Empty A} :
  Empty (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))) := cmra_transport inG_prf .
54
Instance inG_empty_spec `{Empty A} :
55
  CMRAIdentity A  CMRAIdentity (Σ inG_id (laterC (iPreProp Λ (globalF Σ)))).
56
57
Proof.
  split.
58
59
60
  - apply cmra_transport_valid, cmra_empty_valid.
  - intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
  - apply _.
61
62
63
Qed.

(** * Properties of own *)
64
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof. by intros m m' Hm; rewrite /own Hm. Qed.
66
Global Instance own_proper γ : Proper (() ==> ()) (own γ) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
67

68
Lemma own_op γ a1 a2 : own γ (a1  a2)  (own γ a1  own γ a2)%I.
69
Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
70
Global Instance own_mono γ : Proper (flip () ==> ()) (own γ).
Ralf Jung's avatar
Ralf Jung committed
71
Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
72
Lemma always_own_unit γ a : ( own γ (unit a))%I  own γ (unit a).
73
Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
74
75
Lemma always_own γ a : unit a  a  ( own γ a)%I  own γ a.
Proof. by intros <-; rewrite always_own_unit. Qed.
76
Lemma own_valid γ a : own γ a   a.
77
Proof.
78
  rewrite /own ownG_valid /to_globalF.
79
  rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
80
  rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
81
  by destruct inG_prf.
82
Qed.
83
Lemma own_valid_r γ a : own γ a  (own γ a   a).
84
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
85
Lemma own_valid_l γ a : own γ a  ( a  own γ a).
86
Proof. by rewrite comm -own_valid_r. Qed.
87
Global Instance own_timeless γ a : Timeless a  TimelessP (own γ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
88
Proof. unfold own; apply _. Qed.
89
90
Global Instance own_unit_always_stable γ a : AlwaysStable (own γ (unit a)).
Proof. by rewrite /AlwaysStable always_own_unit. Qed.
91

Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
(* 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. *)
94
Lemma own_alloc_strong a E (G : gset gname) :
95
   a  True  (|={E}=>  γ, (γ  G)  own γ a).
96
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  intros Ha.
98
  rewrite -(pvs_mono _ _ ( m,  ( γ, γ  G  m = to_globalF γ a)  ownG m)%I).
99
  - eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty inG_id);
100
101
      first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha);
      naive_solver.
102
  - apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
103
104
    by rewrite -(exist_intro γ) const_equiv.
Qed.
105
Lemma own_alloc a E :  a  True  (|={E}=>  γ, own γ a).
106
107
108
Proof.
  intros Ha. rewrite (own_alloc_strong a E ) //; []. apply pvs_mono.
  apply exist_mono=>?. eauto with I.
109
Qed.
110

111
Lemma own_updateP P γ a E :
112
  a ~~>: P  own γ a  (|={E}=>  a',  P a'  own γ a').
113
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  intros Ha.
115
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalF γ a'  P a')  ownG m)%I).
116
  - eapply pvs_ownG_updateP, iprod_singleton_updateP;
117
      first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
118
    naive_solver.
119
  - apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
Robbert Krebbers's avatar
Robbert Krebbers committed
120
    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
121
122
Qed.

123
Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} P γ E :
124
   ~~>: P  True  (|={E}=>  a,  P a  own γ a).
125
Proof.
126
  intros Hemp.
127
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalF γ a'  P a')  ownG m)%I).
128
  - eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty;
129
      first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp.
130
    naive_solver.
131
  - apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
132
133
134
    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Qed.

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

Lemma own_update_empty `{Empty A, !CMRAIdentity A} γ E :
142
  True  (|={E}=> own γ ).
143
144
145
Proof.
  rewrite (own_updateP_empty ( =)); last by apply cmra_updateP_id.
  apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
146
Qed.
147
End global.
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166

(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
   the functor breaks badly because Coq is unable to infer the correct
   typeclasses, it does not unfold the functor. *)
Class inGF (Λ : language) (Σ : gid  iFunctor) (F : iFunctor) := InGF {
  inGF_id : gid;
  inGF_prf : F = Σ inGF_id;
}.

Instance inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
Proof. exists inGF_id. f_equal. apply inGF_prf. Qed.

Instance inGF_nil {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
Proof. exists 0. done. Qed.

Instance inGF_cons `{inGF Λ Σ F} (F': iFunctor) : inGF Λ (F' .:: Σ) F.
Proof. exists (S inGF_id). apply inGF_prf. Qed.

Definition endF : gid  iFunctor := const (constF unitRA).