Commit 690ccd6d authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Do not assume all gfunctor are map from gname

parent a692605f
......@@ -4,12 +4,12 @@ Import uPred.
(* The CMRA we need. *)
Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
auth_inG :> inG Λ Σ (authR A);
auth_inG :> inG Λ Σ (mapR gname (authR A));
auth_identity :> CMRAUnit A;
auth_timeless :> CMRADiscrete A;
}.
(* The Functor we need. *)
Definition authGF (A : cmraT) : gFunctor := GFunctor (constRF (authR A)).
Definition authGF (A : cmraT) : gFunctor := GFunctor (mapRF gname (constRF (authR A))).
(* Show and register that they match. *)
Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
`{CMRAUnit A, CMRADiscrete A} : authG Λ Σ A.
......
......@@ -4,30 +4,39 @@ From iris.program_logic Require Export pviewshifts global_functor.
From iris.program_logic Require Import ownership.
Import uPred.
Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
Definition own `{inG Λ Σ (mapR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
ownG (to_globalF γ a).
Definition ownl `{inG Λ Σ A} (γ : gname) (a : A) : ilPropG Λ Σ :=
Definition ownl `{inG Λ Σ (mapR gname A)} (γ : gname) (a : A) : ilPropG Λ Σ :=
ownGl (to_globalF γ a).
Instance: Params (@to_globalF) 5.
Instance: Params (@own) 5.
Typeclasses Opaque to_globalF own.
(** Properties about ghost ownership *)
Section global.
Context `{i : inG Λ Σ A}.
Implicit Types a : A.
Section empty.
Context `{i : inG Λ Σ A} `{CMRAUnit A}.
(** * Transport empty *)
Instance inG_empty `{Empty A} :
Empty (projT2 Σ inG_id (iPreProp Λ (globalF Σ))) := cmra_transport inG_prf .
Instance inG_empty_spec `{Empty A} :
CMRAUnit A CMRAUnit (projT2 Σ inG_id (iPreProp Λ (globalF Σ))).
Lemma cmra_unit_unique {M: cmraT} (a b: M):
( x', a x' x')
( x', b x' x')
a b.
Proof.
intros Hu1 Hu2. specialize (Hu1 b). specialize (Hu2 a).
rewrite -Hu1. rewrite -{1}Hu2. by rewrite comm.
Qed.
Lemma inG_empty_back:
cmra_transport inG_prf (: A).
Proof.
split.
- apply cmra_transport_valid, cmra_unit_valid.
- intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
- apply _.
eapply cmra_unit_unique.
- intros; by rewrite left_id.
- intros. destruct inG_prf. by rewrite left_id.
Qed.
End empty.
(** Properties about ghost ownership *)
Section global.
Context `{i : inG Λ Σ (mapR gname A)}.
Implicit Types a : A.
(** * Properties of own *)
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
......@@ -42,9 +51,8 @@ Lemma own_valid γ a : own γ a ⊢ ✓ a.
Proof.
rewrite /own ownG_valid /to_globalF.
rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
(* implicit arguments differ a bit *)
by trans ( cmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf.
trans ( cmra_transport inG_prf {[γ := a]} : iPropG Λ Σ)%I; last destruct inG_prf; auto.
by rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
Qed.
Lemma own_valid_r γ a : own γ a (own γ a a).
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
......@@ -57,14 +65,20 @@ Proof. rewrite /own; apply _. Qed.
(* 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 own_alloc_strong a E (G : gset gname) :
a True (|={E}=> γ, (γ G) own γ a).
Proof.
intros Ha.
rewrite -(pvs_mono _ _ ( m, ( γ, γ G m = to_globalF γ a) ownG m)%I).
- rewrite ownG_empty. eapply pvs_ownG_updateP, (iprod_singleton_updateP_empty inG_id);
first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha);
naive_solver.
- rewrite ownG_empty. eapply pvs_ownG_updateP.
eapply (iprod_singleton_updateP_empty inG_id
(λ y, γ, γ G iprod_singleton inG_id y = to_globalF γ a)).
* rewrite inG_empty_back.
eapply cmra_transport_updateP. eapply map_updateP_alloc_strong'; eauto.
intros ? (γ&?&?&?); subst.
exists γ. split_and!; eauto.
* naive_solver.
- apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
by rewrite -(exist_intro γ) const_equiv // left_id.
Qed.
......@@ -80,7 +94,7 @@ Proof.
intros Ha.
rewrite -(pvs_mono _ _ ( m, ( a', m = to_globalF γ a' P a') ownG m)%I).
- eapply pvs_ownG_updateP, iprod_singleton_updateP;
first by (eapply map_singleton_updateP', cmra_transport_updateP', Ha).
first by (apply cmra_transport_updateP', map_singleton_updateP', Ha).
naive_solver.
- apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
......@@ -96,9 +110,12 @@ Lemma own_empty `{Empty A, !CMRAUnit A} γ E :
True (|={E}=> own γ ).
Proof.
rewrite ownG_empty /own. apply pvs_ownG_update, cmra_update_updateP.
eapply iprod_singleton_updateP_empty;
first by eapply map_singleton_updateP_empty', cmra_transport_updateP',
cmra_update_updateP, cmra_update_unit.
naive_solver.
eapply (iprod_singleton_updateP_empty inG_id
(λ y, iprod_singleton inG_id y = to_globalF γ )).
- rewrite inG_empty_back.
eapply cmra_transport_updateP;
first eapply map_singleton_updateP_empty', cmra_update_updateP, cmra_update_unit.
naive_solver.
- naive_solver.
Qed.
End global.
......@@ -6,9 +6,11 @@ From iris.program_logic Require Export model.
Structure gFunctor := GFunctor {
gFunctor_F :> rFunctor;
gFunctor_contractive : rFunctorContractive gFunctor_F;
gFunctor_empty : A : cofeT, Empty (gFunctor_F A);
gFunctor_identity : A : cofeT, CMRAUnit (gFunctor_F A)
}.
Arguments GFunctor _ {_}.
Existing Instance gFunctor_contractive.
Arguments GFunctor _ {_ _ _}.
Existing Instances gFunctor_contractive gFunctor_empty gFunctor_identity.
(** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *)
Definition gFunctors := { n : nat & fin n gFunctor }.
......@@ -18,7 +20,7 @@ Definition gid (Σ : gFunctors) := fin (projT1 Σ).
Definition gname := positive.
Definition globalF (Σ : gFunctors) : iFunctor :=
IFunctor (iprodRF (λ i, mapRF gname (projT2 Σ i))).
IFunctor (iprodRF (projT2 Σ)).
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Notation ilPropG Λ Σ := (ilProp Λ (globalF Σ)).
......@@ -27,12 +29,12 @@ Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
inG_prf : A = projT2 Σ inG_id (iPreProp Λ (globalF Σ))
}.
Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton inG_id {[ γ := cmra_transport inG_prf a ]}.
Definition to_globalF `{inG Λ Σ (mapR gname A)} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton inG_id (cmra_transport inG_prf ({[ γ := a ]})).
(** * Properties of to_globalC *)
Section to_globalF.
Context `{i : inG Λ Σ A}.
Context `{i : inG Λ Σ (mapR gname A)}.
Implicit Types a : A.
Global Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF γ).
......@@ -40,7 +42,7 @@ Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma to_globalF_op γ a1 a2 :
to_globalF γ (a1 a2) to_globalF γ a1 to_globalF γ a2.
Proof.
by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
by rewrite /to_globalF iprod_op_singleton -cmra_transport_op map_op_singleton.
Qed.
Global Instance to_globalF_timeless γ m: Timeless m Timeless (to_globalF γ m).
Proof. rewrite /to_globalF; apply _. Qed.
......
......@@ -3,9 +3,9 @@ From iris.program_logic Require Export ghost_ownership.
Import uPred.
Class oneShotG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
one_shot_inG :> inG Λ Σ (one_shotR $ agreeR $ laterC $ F (iPreProp Λ (globalF Σ))).
one_shot_inG :> inG Λ Σ (mapR gname $ one_shotR $ agreeR $ laterC $ F (iPreProp Λ (globalF Σ))).
Definition oneShotGF (F : cFunctor) : gFunctor :=
GFunctor (one_shotRF (agreeRF ( F))).
GFunctor (mapRF gname (one_shotRF (agreeRF ( F)))).
Instance inGF_oneShotG `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
Proof. apply: inGF_inG. Qed.
......
......@@ -3,9 +3,9 @@ From iris.program_logic Require Export ghost_ownership.
Import uPred.
Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPreProp Λ (globalF Σ))))).
saved_prop_inG :> inG Λ Σ (mapR gname (agreeR (laterC (F (iPreProp Λ (globalF Σ)))))).
Definition savedPropGF (F : cFunctor) : gFunctor :=
GFunctor (agreeRF ( F)).
GFunctor (mapRF gname (agreeRF ( F))).
Instance inGF_savedPropG `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F.
Proof. apply: inGF_inG. Qed.
......
......@@ -4,12 +4,12 @@ Import uPred.
(** The CMRA we need. *)
Class stsG Λ Σ (sts : stsT) := StsG {
sts_inG :> inG Λ Σ (stsR sts);
sts_inG :> inG Λ Σ (mapR gname (stsR sts));
sts_inhabited :> Inhabited (sts.state sts);
}.
Coercion sts_inG : stsG >-> inG.
(** The Functor we need. *)
Definition stsGF (sts : stsT) : gFunctor := GFunctor (constRF (stsR sts)).
Definition stsGF (sts : stsT) : gFunctor := GFunctor (mapRF gname (constRF (stsR sts))).
(* Show and register that they match. *)
Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
`{Inhabited (sts.state sts)} : stsG Λ Σ sts.
......
......@@ -105,7 +105,7 @@ Proof. by intros; apply vs_alt, inv_alloc. Qed.
End vs.
Section vs_ghost.
Context `{inG Λ Σ A}.
Context `{inG Λ Σ (mapR gname A)}.
Implicit Types a : A.
Implicit Types P Q R : iPropG Λ Σ.
......
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