ghost_ownership.v 5.11 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
Require Export algebra.iprod program_logic.pviewshifts.
Require Import program_logic.ownership.
3
4
Import uPred.

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

13
Class InG (Λ : language) (Σ : gid  iFunctor) (i : gid) (A : cmraT) :=
14
  inG : A = Σ i (laterC (iPreProp Λ (globalF Σ))).
15

16
17
Definition to_globalF {Λ Σ A}
    (i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
  iprod_singleton i {[ γ  cmra_transport inG a ]}.
Definition own {Λ Σ A}
20
21
22
    (i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iProp Λ (globalF Σ) :=
  ownG (to_globalF i γ a).
Instance: Params (@to_globalF) 6.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Instance: Params (@own) 6.
24
25
26
27
Typeclasses Opaque to_globalF own.

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

29
Section global.
30
Context {Λ : language} {Σ : iFunctorG} (i : gid) `{!InG Λ Σ i A}.
31
32
Implicit Types a : A.

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

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

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

Lemma own_op γ a1 a2 : own i γ (a1  a2)  (own i γ a1  own i γ a2)%I.
72
Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Lemma always_own_unit γ a : ( own i γ (unit a))%I  own i γ (unit a).
74
Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Lemma own_valid γ a : own i γ a   a.
76
Proof.
77
  rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalF_validN.
78
Qed.
Ralf Jung's avatar
Ralf Jung committed
79
Lemma own_valid_r γ a : own i γ a  (own i γ a   a).
80
Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82
Global Instance own_timeless γ a : Timeless a  TimelessP (own i γ a).
Proof. unfold own; apply _. Qed.
83

Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
(* 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. *)
Ralf Jung's avatar
Ralf Jung committed
86
Lemma own_alloc a E :  a  True  pvs E E ( γ, own i γ a).
87
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
  intros Ha.
89
  rewrite -(pvs_mono _ _ ( m,  ( γ, m = to_globalF i γ a)  ownG m)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
92
93
  * eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i);
      first (eapply map_updateP_alloc', cmra_transport_valid, Ha); naive_solver.
  * apply exist_elim=>m; apply const_elim_l=>-[γ ->].
    by rewrite -(exist_intro γ).
94
Qed.
95

Ralf Jung's avatar
Ralf Jung committed
96
Lemma own_updateP γ a P E :
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  a ~~>: P  own i γ a  pvs E E ( a',  P a'  own i γ a').
98
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  intros Ha.
100
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalF i γ a'  P a')  ownG m)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  * eapply pvs_ownG_updateP, iprod_singleton_updateP;
102
      first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
    naive_solver.
  * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
106
107
Qed.

Ralf Jung's avatar
Ralf Jung committed
108
Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} γ a P E :
109
   ~~>: P  True  pvs E E ( a,  P a  own i γ a).
110
Proof.
111
  intros Hemp.
112
  rewrite -(pvs_mono _ _ ( m,  ( a', m = to_globalF i γ a'  P a')  ownG m)%I).
113
114
  * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty;
      first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp.
115
116
117
118
119
    naive_solver.
  * apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Qed.

Ralf Jung's avatar
Ralf Jung committed
120
Lemma own_update γ a a' E : a ~~> a'  own i γ a  pvs E E (own i γ a').
121
Proof.
Ralf Jung's avatar
Ralf Jung committed
122
  intros; rewrite (own_updateP _ _ (a' =)); last by apply cmra_update_updateP.
123
124
  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
Qed.
125
End global.