Commit f0e60e9d authored by Ralf Jung's avatar Ralf Jung
Browse files

Change some names related to the global ghost CMRA around

globalC -> globalF
New notation: iPropG, iFunctorG
parent e2efc09c
...@@ -4,11 +4,10 @@ Import uPred. ...@@ -4,11 +4,10 @@ Import uPred.
Section auth. Section auth.
Context {A : cmraT} `{Empty A, !CMRAIdentity A} `{! a : A, Timeless a}. Context {A : cmraT} `{Empty A, !CMRAIdentity A} `{! a : A, Timeless a}.
Context {Λ : language} {Σ : gid iFunctor} (AuthI : gid) `{!InG Λ Σ AuthI (authRA A)}. Context {Λ : language} {Σ : iFunctorG} (AuthI : gid) `{!InG Λ Σ AuthI (authRA A)}.
(* TODO: Come up with notation for "iProp Λ (globalC Σ)". *) Context (N : namespace) (φ : A iPropG Λ Σ).
Context (N : namespace) (φ : A iProp Λ (globalC Σ)).
Implicit Types P Q R : iProp Λ (globalC Σ). Implicit Types P Q R : iPropG Λ Σ.
Implicit Types a b : A. Implicit Types a b : A.
Implicit Types γ : gname. Implicit Types γ : gname.
...@@ -23,12 +22,12 @@ Section auth. ...@@ -23,12 +22,12 @@ Section auth.
(* TODO: Need this to be proven somewhere. *) (* TODO: Need this to be proven somewhere. *)
(* FIXME ✓ binds too strong, I need parenthesis here. *) (* FIXME ✓ binds too strong, I need parenthesis here. *)
Hypothesis auth_valid : Hypothesis auth_valid :
forall a b, ( (Auth (Excl a) b) : iProp Λ (globalC Σ)) ( b', a b b'). forall a b, ( (Auth (Excl a) b) : iPropG Λ Σ) ( b', a b b').
Definition auth_inv (γ : gname) : iProp Λ (globalC Σ) := Definition auth_inv (γ : gname) : iPropG Λ Σ :=
( a, own AuthI γ ( a) φ a)%I. ( a, own AuthI γ ( a) φ a)%I.
Definition auth_own (γ : gname) (a : A) : iProp Λ (globalC Σ) := own AuthI γ ( a). Definition auth_own (γ : gname) (a : A) : iPropG Λ Σ := own AuthI γ ( a).
Definition auth_ctx (γ : gname) : iProp Λ (globalC Σ) := inv N (auth_inv γ). Definition auth_ctx (γ : gname) : iPropG Λ Σ := inv N (auth_inv γ).
Lemma auth_alloc a : Lemma auth_alloc a :
a φ a pvs N N ( γ, auth_ctx γ auth_own γ a). a φ a pvs N N ( γ, auth_ctx γ auth_own γ a).
...@@ -78,7 +77,7 @@ Section auth. ...@@ -78,7 +77,7 @@ Section auth.
step-indices. However, since A is timeless, that should not be step-indices. However, since A is timeless, that should not be
a restriction. *) a restriction. *)
Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA) Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
`{!LocalUpdate Lv L} E P (Q : X iProp Λ (globalC Σ)) γ a : `{!LocalUpdate Lv L} E P (Q : X iPropG Λ Σ) γ a :
nclose N E nclose N E
(auth_ctx γ auth_own γ a ( a', ▷φ (a a') - (auth_ctx γ auth_own γ a ( a', ▷φ (a a') -
FSA (E nclose N) (λ x, (Lv a (L aa')) ▷φ (L a a') (auth_own γ (L a) - Q x)))) FSA (E nclose N) (λ x, (Lv a (L aa')) ▷φ (L a a') (auth_own γ (L a) - Q x))))
......
...@@ -7,52 +7,55 @@ Definition gid := nat. ...@@ -7,52 +7,55 @@ Definition gid := nat.
(** Name of one instance of a particular CMRA in the ghost state. *) (** Name of one instance of a particular CMRA in the ghost state. *)
Definition gname := positive. Definition gname := positive.
(** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *) (** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *)
Definition globalC (Σ : gid iFunctor) : iFunctor := Definition globalF (Σ : gid iFunctor) : iFunctor :=
iprodF (λ i, mapF gname (Σ i)). iprodF (λ i, mapF gname (Σ i)).
Class InG (Λ : language) (Σ : gid iFunctor) (i : gid) (A : cmraT) := Class InG (Λ : language) (Σ : gid iFunctor) (i : gid) (A : cmraT) :=
inG : A = Σ i (laterC (iPreProp Λ (globalC Σ))). inG : A = Σ i (laterC (iPreProp Λ (globalF Σ))).
Definition to_globalC {Λ Σ A} Definition to_globalF {Λ Σ A}
(i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iGst Λ (globalC Σ) := (i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton i {[ γ cmra_transport inG a ]}. iprod_singleton i {[ γ cmra_transport inG a ]}.
Definition own {Λ Σ A} Definition own {Λ Σ A}
(i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iProp Λ (globalC Σ) := (i : gid) `{!InG Λ Σ i A} (γ : gname) (a : A) : iProp Λ (globalF Σ) :=
ownG (to_globalC i γ a). ownG (to_globalF i γ a).
Instance: Params (@to_globalC) 6. Instance: Params (@to_globalF) 6.
Instance: Params (@own) 6. Instance: Params (@own) 6.
Typeclasses Opaque to_globalC own. Typeclasses Opaque to_globalF own.
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Notation iFunctorG := (gid iFunctor).
Section global. Section global.
Context {Λ : language} {Σ : gid iFunctor} (i : gid) `{!InG Λ Σ i A}. Context {Λ : language} {Σ : iFunctorG} (i : gid) `{!InG Λ Σ i A}.
Implicit Types a : A. Implicit Types a : A.
(** * Properties of to_globalC *) (** * Properties of to_globalC *)
Instance to_globalC_ne γ n : Proper (dist n ==> dist n) (to_globalC i γ). Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF i γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed. Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma to_globalC_validN n γ a : {n} (to_globalC i γ a) {n} a. Lemma to_globalF_validN n γ a : {n} (to_globalF i γ a) {n} a.
Proof. Proof.
by rewrite /to_globalC by rewrite /to_globalF
iprod_singleton_validN map_singleton_validN cmra_transport_validN. iprod_singleton_validN map_singleton_validN cmra_transport_validN.
Qed. Qed.
Lemma to_globalC_op γ a1 a2 : Lemma to_globalF_op γ a1 a2 :
to_globalC i γ (a1 a2) to_globalC i γ a1 to_globalC i γ a2. to_globalF i γ (a1 a2) to_globalF i γ a1 to_globalF i γ a2.
Proof. Proof.
by rewrite /to_globalC iprod_op_singleton map_op_singleton cmra_transport_op. by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
Qed. Qed.
Lemma to_globalC_unit γ a : unit (to_globalC i γ a) to_globalC i γ (unit a). Lemma to_globalF_unit γ a : unit (to_globalF i γ a) to_globalF i γ (unit a).
Proof. Proof.
by rewrite /to_globalC by rewrite /to_globalF
iprod_unit_singleton map_unit_singleton cmra_transport_unit. iprod_unit_singleton map_unit_singleton cmra_transport_unit.
Qed. Qed.
Instance to_globalC_timeless γ m : Timeless m Timeless (to_globalC i γ m). Instance to_globalF_timeless γ m : Timeless m Timeless (to_globalF i γ m).
Proof. rewrite /to_globalC; apply _. Qed. Proof. rewrite /to_globalF; apply _. Qed.
(** * Transport empty *) (** * Transport empty *)
Instance inG_empty `{Empty A} : Empty (Σ i (laterC (iPreProp Λ (globalC Σ)))) := Instance inG_empty `{Empty A} : Empty (Σ i (laterC (iPreProp Λ (globalF Σ)))) :=
cmra_transport inG . cmra_transport inG .
Instance inG_empty_spec `{Empty A} : Instance inG_empty_spec `{Empty A} :
CMRAIdentity A CMRAIdentity (Σ i (laterC (iPreProp Λ (globalC Σ)))). CMRAIdentity A CMRAIdentity (Σ i (laterC (iPreProp Λ (globalF Σ)))).
Proof. Proof.
split. split.
* apply cmra_transport_valid, cmra_empty_valid. * apply cmra_transport_valid, cmra_empty_valid.
...@@ -66,12 +69,12 @@ Proof. by intros m m' Hm; rewrite /own Hm. Qed. ...@@ -66,12 +69,12 @@ Proof. by intros m m' Hm; rewrite /own Hm. Qed.
Global Instance own_proper γ : Proper (() ==> ()) (own i γ) := ne_proper _. 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. Lemma own_op γ a1 a2 : own i γ (a1 a2) (own i γ a1 own i γ a2)%I.
Proof. by rewrite /own -ownG_op to_globalC_op. Qed. Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
Lemma always_own_unit γ a : ( own i γ (unit a))%I own i γ (unit a). Lemma always_own_unit γ a : ( own i γ (unit a))%I own i γ (unit a).
Proof. by rewrite /own -to_globalC_unit always_ownG_unit. Qed. Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
Lemma own_valid γ a : own i γ a a. Lemma own_valid γ a : own i γ a a.
Proof. Proof.
rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalC_validN. rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalF_validN.
Qed. Qed.
Lemma own_valid_r γ a : own i γ a (own i γ a a). Lemma own_valid_r γ a : own i γ a (own i γ a a).
Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed. Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
...@@ -83,7 +86,7 @@ Proof. unfold own; apply _. Qed. ...@@ -83,7 +86,7 @@ Proof. unfold own; apply _. Qed.
Lemma own_alloc a E : a True pvs E E ( γ, own i γ a). Lemma own_alloc a E : a True pvs E E ( γ, own i γ a).
Proof. Proof.
intros Ha. intros Ha.
rewrite -(pvs_mono _ _ ( m, ( γ, m = to_globalC i γ a) ownG m)%I). rewrite -(pvs_mono _ _ ( m, ( γ, m = to_globalF i γ a) ownG m)%I).
* eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i); * eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty i);
first (eapply map_updateP_alloc', cmra_transport_valid, Ha); naive_solver. first (eapply map_updateP_alloc', cmra_transport_valid, Ha); naive_solver.
* apply exist_elim=>m; apply const_elim_l=>-[γ ->]. * apply exist_elim=>m; apply const_elim_l=>-[γ ->].
...@@ -94,7 +97,7 @@ Lemma own_updateP γ a P E : ...@@ -94,7 +97,7 @@ Lemma own_updateP γ a P E :
a ~~>: P own i γ a pvs E E ( a', P a' own i γ a'). a ~~>: P own i γ a pvs E E ( a', P a' own i γ a').
Proof. Proof.
intros Ha. intros Ha.
rewrite -(pvs_mono _ _ ( m, ( a', m = to_globalC i γ a' P a') ownG m)%I). rewrite -(pvs_mono _ _ ( m, ( a', m = to_globalF i γ a' P a') ownG m)%I).
* eapply pvs_ownG_updateP, iprod_singleton_updateP; * eapply pvs_ownG_updateP, iprod_singleton_updateP;
first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha). first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
naive_solver. naive_solver.
...@@ -106,7 +109,7 @@ Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} γ a P E : ...@@ -106,7 +109,7 @@ Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} γ a P E :
~~>: P True pvs E E ( a, P a own i γ a). ~~>: P True pvs E E ( a, P a own i γ a).
Proof. Proof.
intros Hemp. intros Hemp.
rewrite -(pvs_mono _ _ ( m, ( a', m = to_globalC i γ a' P a') ownG m)%I). rewrite -(pvs_mono _ _ ( m, ( a', m = to_globalF i γ a' P a') ownG m)%I).
* eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty; * eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty;
first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp. first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp.
naive_solver. naive_solver.
......
...@@ -105,9 +105,9 @@ Proof. by intros; apply vs_alt, inv_alloc. Qed. ...@@ -105,9 +105,9 @@ Proof. by intros; apply vs_alt, inv_alloc. Qed.
End vs. End vs.
Section vs_ghost. Section vs_ghost.
Context {Λ : language} {Σ : gid iFunctor} (i : gid) `{!InG Λ Σ i A}. Context {Λ : language} {Σ : iFunctorG} (i : gid) `{!InG Λ Σ i A}.
Implicit Types a : A. Implicit Types a : A.
Implicit Types P Q R : iProp Λ (globalC Σ). Implicit Types P Q R : iPropG Λ Σ.
Lemma vs_own_updateP E γ a φ : Lemma vs_own_updateP E γ a φ :
a ~~>: φ own i γ a ={E}=> a', φ a' own i γ a'. a ~~>: φ own i γ a ={E}=> a', φ a' own i γ a'.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment