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

Ralf Jung's avatar
Ralf Jung committed
6
7
8
9
10
(** 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) *)
11
Definition globalF (Σ : gid  iFunctor) : iFunctor :=
Ralf Jung's avatar
Ralf Jung committed
12
  iprodF (λ i, mapF gname (Σ i)).
13

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

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

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

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

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

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

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

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

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

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

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

130
Lemma own_update γ a a' E : a ~~> a'  own γ a  pvs E E (own γ a').
131
Proof.
132
133
134
135
136
  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 :
137
  True  pvs E E (own γ ).
138
139
140
Proof.
  rewrite (own_updateP_empty ( =)); last by apply cmra_updateP_id.
  apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
141
Qed.
142
End global.