Commit b5e8ab4e authored by Robbert Krebbers's avatar Robbert Krebbers

Remove gFunctorList and use gFunctors everywhere.

This makes stuff more uniform and also removes the need for the [inGFs]
type class. Instead, there is now a type class [subG Σ1 Σ2] which expresses
that a list of functors [Σ1] is contained in [Σ2].
parent 3f3d517d
Pipeline #2571 passed with stage
in 4 minutes and 14 seconds
...@@ -76,7 +76,6 @@ program_logic/ectx_language.v ...@@ -76,7 +76,6 @@ program_logic/ectx_language.v
program_logic/ectxi_language.v program_logic/ectxi_language.v
program_logic/ectx_lifting.v program_logic/ectx_lifting.v
program_logic/ghost_ownership.v program_logic/ghost_ownership.v
program_logic/global_functor.v
program_logic/saved_prop.v program_logic/saved_prop.v
program_logic/auth.v program_logic/auth.v
program_logic/sts.v program_logic/sts.v
......
...@@ -4,7 +4,7 @@ From iris.program_logic Require Import auth ownership. ...@@ -4,7 +4,7 @@ From iris.program_logic Require Import auth ownership.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics weakestpre. From iris.proofmode Require Import tactics weakestpre.
Definition heapGF : gFunctorList := [authGF heapUR; irisGF heap_lang]. Definition heapΣ : gFunctors := #[authΣ heapUR; irisΣ heap_lang].
Definition heap_adequacy Σ `{irisPreG heap_lang Σ, authG Σ heapUR} e σ φ : Definition heap_adequacy Σ `{irisPreG heap_lang Σ, authG Σ heapUR} e σ φ :
( `{heapG Σ}, heap_ctx WP e {{ v, φ v }}) ( `{heapG Σ}, heap_ctx WP e {{ v, φ v }})
......
...@@ -14,10 +14,10 @@ Class barrierG Σ := BarrierG { ...@@ -14,10 +14,10 @@ Class barrierG Σ := BarrierG {
barrier_savedPropG :> savedPropG Σ idCF; barrier_savedPropG :> savedPropG Σ idCF;
}. }.
(** The Functors we need. *) (** The Functors we need. *)
Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF idCF]. Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
(* Show and register that they match. *) (* Show and register that they match. *)
Instance inGF_barrierG `{H : inGFs Σ barrierGF} : barrierG Σ. Instance subG_barrierΣ {Σ} : subG barrierΣ Σ barrierG Σ.
Proof. destruct H as (?&?&?). split; apply _. Qed. Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
(** Now we come to the Iris part of the proof. *) (** Now we come to the Iris part of the proof. *)
Section proof. Section proof.
......
...@@ -14,9 +14,10 @@ Global Opaque newcounter inc get. ...@@ -14,9 +14,10 @@ Global Opaque newcounter inc get.
(** The CMRA we need. *) (** The CMRA we need. *)
Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }. Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }.
Definition counterGF : gFunctorList := [authGF mnatUR].
Instance inGF_counterG `{H : inGFs Σ counterGF} : counterG Σ. Definition counterΣ : gFunctors := #[authΣ mnatUR].
Proof. destruct H; split; apply _. Qed. Instance subG_counterΣ {Σ} : subG counterΣ Σ counterG Σ.
Proof. intros [? _]%subG_inv. split; apply _. Qed.
Section proof. Section proof.
Context `{!heapG Σ, !counterG Σ} (N : namespace). Context `{!heapG Σ, !counterG Σ} (N : namespace).
......
...@@ -14,9 +14,10 @@ Global Opaque newlock acquire release. ...@@ -14,9 +14,10 @@ Global Opaque newlock acquire release.
(** The CMRA we need. *) (** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }. Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
Instance inGF_lockG `{H : inGFs Σ lockGF} : lockG Σ. Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
Proof. destruct H. split. apply: inGF_inG. Qed. Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Section proof. Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace). Context `{!heapG Σ, !lockG Σ} (N : namespace).
......
...@@ -19,11 +19,11 @@ Global Opaque spawn join. ...@@ -19,11 +19,11 @@ Global Opaque spawn join.
(** The CMRA we need. *) (** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }. Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
(** The functor we need. *)
Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))]. (** The functor we need and register that they match. *)
(* Show and register that they match. *) Definition spawnΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
Instance inGF_spawnG `{H : inGFs Σ spawnGF} : spawnG Σ. Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ.
Proof. destruct H as (?&?). split. apply: inGF_inG. Qed. Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
(** Now we come to the Iris part of the proof. *) (** Now we come to the Iris part of the proof. *)
Section proof. Section proof.
......
...@@ -36,10 +36,10 @@ Class tlockG Σ := TlockG { ...@@ -36,10 +36,10 @@ Class tlockG Σ := TlockG {
tlock_exclG :> inG Σ (exclR unitC) tlock_exclG :> inG Σ (exclR unitC)
}. }.
Definition tlockGF : gFunctorList := Definition tlockΣ : gFunctors :=
[authGF (gset_disjUR nat); GFunctor (constRF (exclR unitC))]. #[authΣ (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
Instance inGF_tlockG `{H : inGFs Σ tlockGF} : tlockG Σ. Instance subG_tlockΣ {Σ} : subG tlockΣ Σ tlockG Σ.
Proof. destruct H as (? & ? & ?). split. apply _. apply: inGF_inG. Qed. Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
Section proof. Section proof.
Context `{!heapG Σ, !tlockG Σ} (N : namespace). Context `{!heapG Σ, !tlockG Σ} (N : namespace).
......
...@@ -7,13 +7,13 @@ Import uPred. ...@@ -7,13 +7,13 @@ Import uPred.
(* The CMRA we need. *) (* The CMRA we need. *)
Class authG Σ (A : ucmraT) := AuthG { Class authG Σ (A : ucmraT) := AuthG {
auth_inG :> inG Σ (authR A); auth_inG :> inG Σ (authR A);
auth_timeless :> CMRADiscrete A; auth_discrete :> CMRADiscrete A;
}. }.
(* The Functor we need. *)
Definition authGF (A : ucmraT) : gFunctor := GFunctor (constRF (authR A)). (* The global functor we need and register that they match. *)
(* Show and register that they match. *) Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
Instance authGF_inGF `{inGF Σ (authGF A), CMRADiscrete A} : authG Σ A. Instance subG_authΣ Σ A : subG (authΣ A) Σ CMRADiscrete A authG Σ A.
Proof. split; try apply _. apply: inGF_inG. Qed. Proof. intros ?%subG_inG ?. by split. Qed.
Section definitions. Section definitions.
Context `{irisG Λ Σ, authG Σ A} (γ : gname). Context `{irisG Λ Σ, authG Σ A} (γ : gname).
......
From iris.program_logic Require Export global_functor. From iris.program_logic Require Export model.
From iris.algebra Require Import iprod gmap. From iris.algebra Require Import iprod gmap.
Import uPred. Import uPred.
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
[Σ]. This class is similar to the [subG] class, but written down in terms of
individual CMRAs instead of lists of CMRA functors. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) :=
InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) }.
Arguments inG_id {_ _} _.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPreProp Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4.
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ := Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (to_iRes γ a). uPred_ownM (iRes_singleton γ a).
Definition own_aux : { x | x = @own_def }. by eexists. Qed. Definition own_aux : { x | x = @own_def }. by eexists. Qed.
Definition own {Σ A i} := proj1_sig own_aux Σ A i. Definition own {Σ A i} := proj1_sig own_aux Σ A i.
Definition own_eq : @own = @own_def := proj2_sig own_aux. Definition own_eq : @own = @own_def := proj2_sig own_aux.
Instance: Params (@own) 4. Instance: Params (@own) 4.
Typeclasses Opaque own. Typeclasses Opaque own.
(** Properties about ghost ownership *) (** * Properties about ghost ownership *)
Section global. Section global.
Context `{i : inG Σ A}. Context `{i : inG Σ A}.
Implicit Types a : A. Implicit Types a : A.
(** * Properties of own *) (** ** Properties of [iRes_singleton] *)
Global Instance iRes_singleton_ne γ n :
Proper (dist n ==> dist n) (@iRes_singleton Σ A _ γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma iRes_singleton_op γ a1 a2 :
iRes_singleton γ (a1 a2) iRes_singleton γ a1 iRes_singleton γ a2.
Proof.
by rewrite /iRes_singleton iprod_op_singleton op_singleton cmra_transport_op.
Qed.
(** ** Properties of [own] *)
Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Σ A _ γ). Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Σ A _ γ).
Proof. rewrite !own_eq. solve_proper. Qed. Proof. rewrite !own_eq. solve_proper. Qed.
Global Instance own_proper γ : Global Instance own_proper γ :
Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _. Proper (() ==> ()) (@own Σ A _ γ) := ne_proper _.
Lemma own_op γ a1 a2 : own γ (a1 a2) own γ a1 own γ a2. Lemma own_op γ a1 a2 : own γ (a1 a2) own γ a1 own γ a2.
Proof. by rewrite !own_eq /own_def -ownM_op to_iRes_op. Qed. Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
Global Instance own_mono γ : Proper (flip () ==> ()) (@own Σ A _ γ). Global Instance own_mono γ : Proper (flip () ==> ()) (@own Σ A _ γ).
Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed. Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
Lemma own_valid γ a : own γ a a. Lemma own_valid γ a : own γ a a.
Proof. Proof.
rewrite !own_eq /own_def ownM_valid /to_iRes. rewrite !own_eq /own_def ownM_valid /iRes_singleton.
rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton. rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI. rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
(* implicit arguments differ a bit *) (* implicit arguments differ a bit *)
...@@ -42,13 +69,14 @@ Proof. rewrite !own_eq /own_def; apply _. Qed. ...@@ -42,13 +69,14 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
Global Instance own_core_persistent γ a : Persistent a PersistentP (own γ a). Global Instance own_core_persistent γ a : Persistent a PersistentP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed. Proof. rewrite !own_eq /own_def; apply _. Qed.
(** ** Allocation *)
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris (* 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. *) assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong a (G : gset gname) : Lemma own_alloc_strong a (G : gset gname) :
a True =r=> γ, (γ G) own γ a. a True =r=> γ, (γ G) own γ a.
Proof. Proof.
intros Ha. intros Ha.
rewrite -(rvs_mono ( m, ( γ, γ G m = to_iRes γ a) uPred_ownM m)%I). rewrite -(rvs_mono ( m, ( γ, γ G m = iRes_singleton γ a) uPred_ownM m)%I).
- rewrite ownM_empty. - rewrite ownM_empty.
eapply rvs_ownM_updateP, (iprod_singleton_updateP_empty (inG_id i)); eapply rvs_ownM_updateP, (iprod_singleton_updateP_empty (inG_id i));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha); first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
...@@ -62,10 +90,11 @@ Proof. ...@@ -62,10 +90,11 @@ Proof.
apply rvs_mono, exist_mono=>?. eauto with I. apply rvs_mono, exist_mono=>?. eauto with I.
Qed. Qed.
(** ** Frame preserving updates *)
Lemma own_updateP P γ a : a ~~>: P own γ a =r=> a', P a' own γ a'. Lemma own_updateP P γ a : a ~~>: P own γ a =r=> a', P a' own γ a'.
Proof. Proof.
intros Ha. rewrite !own_eq. intros Ha. rewrite !own_eq.
rewrite -(rvs_mono ( m, ( a', m = to_iRes γ a' P a') uPred_ownM m)%I). rewrite -(rvs_mono ( m, ( a', m = iRes_singleton γ a' P a') uPred_ownM m)%I).
- eapply rvs_ownM_updateP, iprod_singleton_updateP; - eapply rvs_ownM_updateP, iprod_singleton_updateP;
first by (eapply singleton_updateP', cmra_transport_updateP', Ha). first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
naive_solver. naive_solver.
......
From iris.program_logic Require Export model.
From iris.algebra Require Import iprod gmap.
Class inG (Σ : gFunctors) (A : cmraT) := InG {
inG_id : gid Σ;
inG_prf : A = projT2 Σ inG_id (iPreProp Σ)
}.
Arguments inG_id {_ _} _.
Definition to_iRes `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@to_iRes) 4.
Typeclasses Opaque to_iRes.
(** * Properties of [to_iRes] *)
Section to_iRes.
Context `{inG Σ A}.
Implicit Types a : A.
Global Instance to_iRes_ne γ n :
Proper (dist n ==> dist n) (@to_iRes Σ A _ γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma to_iRes_op γ a1 a2 :
to_iRes γ (a1 a2) to_iRes γ a1 to_iRes γ a2.
Proof.
by rewrite /to_iRes iprod_op_singleton op_singleton cmra_transport_op.
Qed.
Global Instance to_iRes_timeless γ a : Timeless a Timeless (to_iRes γ a).
Proof. rewrite /to_iRes; apply _. Qed.
Global Instance to_iRes_persistent γ a :
Persistent a Persistent (to_iRes γ a).
Proof. rewrite /to_iRes; apply _. Qed.
End to_iRes.
(** When instantiating the logic, we want to just plug together the
requirements exported by the modules we use. To this end, we construct
the "gFunctors" from a "list gFunctor", and have some typeclass magic
to infer the inG. *)
Module gFunctorList.
Inductive T :=
| nil : T
| cons : gFunctor T T.
Coercion singleton (F : gFunctor) : T := cons F nil.
Fixpoint app (Fs1 Fs2 : T) : T :=
match Fs1 with nil => Fs2 | cons F Fs1 => cons F (app Fs1 Fs2) end.
Fixpoint fold_right {A} (f : gFunctor A A) (a : A) (Fs : T) : A :=
match Fs with
| nil => a
| cons F Fs => f F (fold_right f a Fs)
end.
End gFunctorList.
Notation gFunctorList := gFunctorList.T.
Delimit Scope gFunctor_scope with gFunctor.
Bind Scope gFunctor_scope with gFunctorList.
Arguments gFunctorList.cons _ _%gFunctor.
Notation "[ ]" := gFunctorList.nil (format "[ ]") : gFunctor_scope.
Notation "[ F ]" := (gFunctorList.app F gFunctorList.nil) : gFunctor_scope.
Notation "[ F1 ; F2 ; .. ; Fn ]" :=
(gFunctorList.app F1 (gFunctorList.app F2 ..
(gFunctorList.app Fn gFunctorList.nil) ..)) : gFunctor_scope.
Module gFunctors.
Definition nil : gFunctors := existT 0 (fin_0_inv _).
Definition cons (F : gFunctor) (Σ : gFunctors) : gFunctors :=
existT (S (projT1 Σ)) (fin_S_inv _ F (projT2 Σ)).
Fixpoint app (Fs : gFunctorList) (Σ : gFunctors) : gFunctors :=
match Fs with
| gFunctorList.nil => Σ
| gFunctorList.cons F Fs => cons F (app Fs Σ)
end.
End gFunctors.
(** Cannot bind this scope with the [gFunctorG] since [gFunctorG] is a
notation hiding a more complex type. *)
Notation "#[ ]" := gFunctors.nil (format "#[ ]").
Notation "#[ Fs ]" := (gFunctors.app Fs gFunctors.nil).
Notation "#[ Fs1 ; Fs2 ; .. ; Fsn ]" :=
(gFunctors.app Fs1 (gFunctors.app Fs2 ..
(gFunctors.app Fsn gFunctors.nil) ..)).
(** 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 (Σ : gFunctors) (F : gFunctor) := InGF {
inGF_id : gid Σ;
inGF_prf : F = projT2 Σ inGF_id;
}.
(* Avoid eager type class search: this line ensures that type class search
is only triggered if the first two arguments of inGF do not contain evars. Since
instance search for [inGF] is restrained, instances should always have [inGF] as
their first argument to avoid loops. For example, the instances [authGF_inGF]
and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode inGF + - : typeclass_instances.
Lemma inGF_inG {Σ F} : inGF Σ F inG Σ (F (iPreProp Σ)).
Proof. intros. exists inGF_id. by rewrite -inGF_prf. Qed.
Instance inGF_here {Σ} (F: gFunctor) : inGF (gFunctors.cons F Σ) F.
Proof. by exists 0%fin. Qed.
Instance inGF_further {Σ} (F F': gFunctor) :
inGF Σ F inGF (gFunctors.cons F' Σ) F.
Proof. intros [i ?]. by exists (FS i). Qed.
(** For modules that need more than one functor, we offer a typeclass
[inGFs] to demand a list of rFunctor to be available. We do
*not* register any instances that go from there to [inGF], to
avoid cycles. *)
Class inGFs (Σ : gFunctors) (Fs : gFunctorList) :=
InGFs : (gFunctorList.fold_right (λ F T, inGF Σ F * T) () Fs)%type.
Instance inGFs_nil {Σ} : inGFs Σ [].
Proof. exact tt. Qed.
Instance inGFs_cons {Σ} F Fs :
inGF Σ F inGFs Σ Fs inGFs Σ (gFunctorList.cons F Fs).
Proof. by split. Qed.
...@@ -17,13 +17,14 @@ Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG { ...@@ -17,13 +17,14 @@ Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
disabled_name : gname; disabled_name : gname;
}. }.
Definition irisGF (Λ : language) : gFunctorList := Definition irisΣ (Λ : language) : gFunctors :=
[GFunctor (constRF (authUR (optionUR (exclR (stateC Λ))))); #[GFunctor (constRF (authUR (optionUR (exclR (stateC Λ)))));
GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF)))); GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
GFunctor (constRF coPset_disjUR); GFunctor (constRF coPset_disjUR);
GFunctor (constRF (gset_disjUR positive))]. GFunctor (constRF (gset_disjUR positive))].
Instance inGF_barrierG `{H : inGFs Σ (irisGF Λ)} : irisPreG Λ Σ. Instance subG_irisΣ {Σ Λ} : subG (irisΣ Λ) Σ irisPreG Λ Σ.
Proof. Proof.
by destruct H as (?%inGF_inG & ?%inGF_inG & ?%inGF_inG & ?%inGF_inG & _). intros [?%subG_inG [?%subG_inG
Qed. [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv]%subG_inv; by constructor.
Qed.
\ No newline at end of file
...@@ -2,11 +2,27 @@ From iris.algebra Require Export upred. ...@@ -2,11 +2,27 @@ From iris.algebra Require Export upred.
From iris.algebra Require Import iprod gmap. From iris.algebra Require Import iprod gmap.
From iris.algebra Require cofe_solver. From iris.algebra Require cofe_solver.
(* The Iris program logic is parametrized by a dependent product of a bunch of (** In this file we construct the type [iProp] of propositions of the Iris
[gFunctor]s, which are locally contractive functor from the category of COFEs to logic. This is done by solving the following recursive domain equation:
the category of CMRAs. These functors are instantiated with [iProp], the type
of Iris propositions, which allows one to construct impredicate CMRAs, such as iProp ≈ uPred { i : gid & gname -fin-> (Σ i) iProp }
invariants and stored propositions using the agreement CMRA. *)
where:
Σ : gFunctors := lists of locally constractive functors
i : gid := indexes addressing individual functors in [Σ]
γ : gname := ghost variable names
The Iris logic is parametrized by a list of locally contractive functors [Σ]
from the category of COFEs to the category of CMRAs. These functors are
instantiated with [iProp], the type of Iris propositions, which allows one to
construct impredicate CMRAs, such as invariants and stored propositions using
the agreement CMRA. *)
(** * Locally contractive functors *)
(** The type [gFunctor] bundles a functor from the category of COFEs to the
category of CMRAs with a proof that it is locally contractive. *)
Structure gFunctor := GFunctor { Structure gFunctor := GFunctor {
gFunctor_F :> rFunctor; gFunctor_F :> rFunctor;
gFunctor_contractive : rFunctorContractive gFunctor_F; gFunctor_contractive : rFunctorContractive gFunctor_F;
...@@ -14,51 +30,125 @@ Structure gFunctor := GFunctor { ...@@ -14,51 +30,125 @@ Structure gFunctor := GFunctor {
Arguments GFunctor _ {_}. Arguments GFunctor _ {_}.
Existing Instance gFunctor_contractive. Existing Instance gFunctor_contractive.
(** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *) (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
of [gFunctor]s.
Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
alternative way to avoid universe inconsistencies with respect to the universe
monomorphic [list] type. *)
Definition gFunctors := { n : nat & fin n gFunctor }. Definition gFunctors := { n : nat & fin n gFunctor }.
Definition gid (Σ : gFunctors) := fin (projT1 Σ). Definition gid (Σ : gFunctors) := fin (projT1 Σ).
Definition gFunctors_lookup (Σ : gFunctors) : gid Σ gFunctor := projT2 Σ.
Coercion gFunctors_lookup : gFunctors >-> Funclass.
(** Name of one instance of a particular CMRA in the ghost state. *)
Definition gname := positive. Definition gname := positive.
(** Solution of the recursive domain equation *) (** The resources functor [iResF Σ A := { i : gid & gname -fin-> (Σ i) A }]. *)
Definition iResF (Σ : gFunctors) : urFunctor :=
iprodURF (λ i, gmapURF gname (Σ i)).
(** We define functions for the empty list of functors, the singleton list of
functors, and the append operator on lists of functors. These are used to
compose [gFunctors] out of smaller pieces. *)
Module gFunctors.
Definition nil : gFunctors := existT 0 (fin_0_inv _).
Definition singleton (F : gFunctor) : gFunctors :=
existT 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).
Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
existT (projT1 Σ1 + projT1 Σ2) (fin_plus_inv _ (projT2 Σ1) (projT2 Σ2)).
End gFunctors.
Coercion gFunctors.singleton : gFunctor >-> gFunctors.
Notation "#[ ]" := gFunctors.nil (format "#[ ]").
Notation "#[ Σ1 ; .. ; Σn ]" :=
(gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..).
(** * Subfunctors *)
(** In order to make proofs in the Iris logic modular, they are not done with
respect to some concrete list of functors [Σ], but are instead parametrized by
an arbitrary list of functors [Σ] that contains atleast certain functors. For
example, the lock library is parametrized by a functor [Σ] that should have:
the functors corresponding to: the heap and the exclusive monoid to manage to
lock invariant.
The contraints to can be expressed using the type class [subG Σ1 Σ2], which
expresses that the functors [Σ1] are contained in [Σ2]. *)
Class subG (Σ1 Σ2 : gFunctors) := in_subG i : { j | Σ1 i = Σ2 j }.
(** Avoid trigger happy type class search: this line ensures that type class
search is only triggered if the arguments of [subG] do not contain evars. Since
instance search for [subG] is restrained, instances should always have [subG] as
their first parameter to avoid loops. For example, the instances [subG_authΣ]
and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode subG + + : typeclass_instances.
Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ subG Σ1 Σ * subG Σ2 Σ.
Proof.
move=> H; split.
- move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_plus_inv_L; eauto.
- move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_plus_inv_R; eauto.
Qed.
Instance subG_refl Σ : subG Σ Σ.
Proof. move=> i; by exists i. Qed.
Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 subG Σ (gFunctors.app Σ1 Σ2).
Proof.
move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
Qed.
Instance inGF_app_r Σ Σ1 Σ2 : subG Σ Σ2 subG Σ (gFunctors.app Σ1 Σ2).
Proof.
move=> H i; move: H=> /(_ i) [j ?].
exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.
Qed.
(** * Solution of the recursive domain equation *)
(** We first declare a module type and then an instance of it so as to seall of
the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig. Module Type iProp_solution_sig.
Parameter iPreProp : gFunctors cofeT. Parameter iPreProp : gFunctors cofeT.
Definition iResUR (Σ : gFunctors) : ucmraT := Definition iResUR (Σ : gFunctors) : ucmraT :=
iprodUR (λ i, gmapUR gname (projT2 Σ i (iPreProp Σ))). iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Definition iProp (Σ : gFunctors) : cofeT := uPredC (iResUR Σ). Definition iProp (Σ : gFunctors) : cofeT := uPredC (iResUR Σ).
Parameter iProp_unfold: {Σ}, iProp Σ -n> iPreProp Σ. Parameter iProp_unfold: {Σ}, iProp Σ -n> iPreProp Σ.
Parameter iProp_fold: {Σ}, iPreProp Σ -n> iProp Σ. Parameter iProp_fold: {Σ}, iPreProp Σ -n> iProp Σ.
Parameter iProp_fold_unfold: {Σ} (P : iProp Σ), Parameter iProp_fold_unfold: {Σ} (P : iProp Σ),
iProp_fold (iProp_unfold P) P. iProp_fold (iProp_unfold P) P.
Parameter iProp_unfold_fold: {Σ} (P : iPreProp Σ), Parameter iProp_unfold_fold: {Σ} (P : iPreProp Σ),
iProp_unfold (iProp_fold P) P. iProp_unfold (iProp_fold P) P.
End iProp_solution_sig. End iProp_solution_sig.
Module Export iProp_solution : iProp_solution_sig. Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver. Import cofe_solver.
Definition iResF (Σ : gFunctors) : urFunctor := Definition iProp_result (Σ : gFunctors) :
iprodURF (λ i, gmapURF gname (projT2 Σ i)). solution (uPredCF (iResF Σ)) := solver.result _.
Definition iProp_result (Σ : gFunctors) :
solution (uPredCF (iResF Σ)) := solver.result _. Definition iPreProp (Σ : gFunctors) : cofeT := iProp_result Σ.