From 2467bf219798dbeef00c06496228558b1ecb35ca Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Mar 2016 14:55:59 +0100
Subject: [PATCH] Add both non-expansive and contractive functors, and bundle
 them for the general Iris instance as well as the global functor construction

This allows us to move the \later in the user-defined functor to any place we want.
In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.
---
 algebra/agree.v                 |  11 +--
 algebra/auth.v                  |   9 ++-
 algebra/cmra.v                  |  36 ++++++++--
 algebra/cofe.v                  |  83 +++++++++++++++++-----
 algebra/cofe_solver.v           |   3 +-
 algebra/excl.v                  |  17 +++--
 algebra/fin_maps.v              |  26 +++++--
 algebra/frac.v                  |   9 ++-
 algebra/iprod.v                 |  34 ++++++---
 algebra/option.v                |  26 +++++--
 algebra/upred.v                 |  11 +--
 barrier/client.v                |   6 +-
 barrier/proof.v                 |  12 ++--
 barrier/specification.v         |   2 +-
 heap_lang/derived.v             |   2 +-
 heap_lang/heap.v                |   4 +-
 heap_lang/lifting.v             |   2 +-
 heap_lang/par.v                 |   2 +-
 heap_lang/spawn.v               |   8 +--
 heap_lang/tests.v               |   2 +-
 program_logic/adequacy.v        |   6 +-
 program_logic/auth.v            |   8 +--
 program_logic/ghost_ownership.v |  65 ++++-------------
 program_logic/global_functor.v  | 121 +++++++++++++++++++++++---------
 program_logic/hoare.v           |   2 +-
 program_logic/hoare_lifting.v   |   2 +-
 program_logic/invariants.v      |   2 +-
 program_logic/lifting.v         |   2 +-
 program_logic/model.v           |  32 +++++----
 program_logic/ownership.v       |  10 +--
 program_logic/pviewshifts.v     |  17 +----
 program_logic/resources.v       |  34 ++++-----
 program_logic/saved_prop.v      |  17 +++--
 program_logic/sts.v             |   6 +-
 program_logic/tactics.v         |   2 +-
 program_logic/tests.v           |  11 +--
 program_logic/viewshifts.v      |  11 +--
 program_logic/weakestpre.v      |   2 +-
 program_logic/wsat.v            |  13 ++--
 39 files changed, 413 insertions(+), 255 deletions(-)

diff --git a/algebra/agree.v b/algebra/agree.v
index 6cd85d7f2..4db475ddc 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -184,10 +184,6 @@ Program Definition agreeRF (F : cFunctor) : rFunctor := {|
   rFunctor_car A B := agreeR (cFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg := agreeC_map (cFunctor_map F fg)
 |}.
-Next Obligation.
-  intros F A1 A2 B1 B2 n ???; simpl.
-  by apply agreeC_map_ne, cFunctor_contractive.
-Qed.
 Next Obligation.
   intros F A B x; simpl. rewrite -{2}(agree_map_id x).
   apply agree_map_ext=>y. by rewrite cFunctor_id.
@@ -196,3 +192,10 @@ Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
   apply agree_map_ext=>y; apply cFunctor_compose.
 Qed.
+
+Instance agreeRF_contractive F :
+  cFunctorContractive F → rFunctorContractive (agreeRF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ???; simpl.
+  by apply agreeC_map_ne, cFunctor_contractive.
+Qed.
diff --git a/algebra/auth.v b/algebra/auth.v
index 23be7312c..faf993d3b 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -244,9 +244,6 @@ Program Definition authRF (F : rFunctor) : rFunctor := {|
   rFunctor_car A B := authR (rFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg := authC_map (rFunctor_map F fg)
 |}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_contractive.
-Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(auth_map_id x).
   apply auth_map_ext=>y; apply rFunctor_id.
@@ -255,3 +252,9 @@ Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
   apply auth_map_ext=>y; apply rFunctor_compose.
 Qed.
+
+Instance authRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (authRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, rFunctor_contractive.
+Qed.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index bc365697e..a940eff8b 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -623,7 +623,6 @@ Structure rFunctor := RFunctor {
   rFunctor_car : cofeT → cofeT -> cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_contractive {A1 A2 B1 B2} : Contractive (@rFunctor_map A1 A2 B1 B2);
   rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
   rFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
@@ -631,9 +630,21 @@ Structure rFunctor := RFunctor {
   rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CMRAMonotone (rFunctor_map fg) 
 }.
-Existing Instances rFunctor_contractive rFunctor_mono.
+Existing Instances rFunctor_mono.
 Instance: Params (@rFunctor_map) 5.
 
+Class rFunctorNe (F : rFunctor) :=
+  rFunctor_ne A1 A2 B1 B2 n :> Proper (dist n ==> dist n) (@rFunctor_map F A1 A2 B1 B2).
+Class rFunctorContractive (F : rFunctor) :=
+  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
+
+(* TODO: Check if this instance hurts us. We don't have such a large search space
+   overall, and because of the priority constCF and laterCF should be the only
+   users of this. *)
+Instance rFunctorContractive_Ne F :
+  rFunctorContractive F → rFunctorNe F.
+Proof. intros ?????. apply contractive_ne, _. Qed.
+
 Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
 Coercion rFunctor_diag : rFunctor >-> Funclass.
 
@@ -641,17 +652,30 @@ Program Definition constRF (B : cmraT) : rFunctor :=
   {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
 
+Instance constRF_contractive B : rFunctorContractive (constRF B).
+Proof. intros ????. apply _. Qed.
+
 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
   rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
   rFunctor_map A1 A2 B1 B2 fg :=
     prodC_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
-Next Obligation.
-  by intros F1 F2 A1 A2 B1 B2 n ???;
-    apply prodC_map_ne; apply rFunctor_contractive.
-Qed.
 Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
 Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !rFunctor_compose.
 Qed.
+
+Instance prodRF_ne F1 F2 :
+  rFunctorNe F1 → rFunctorNe F2 → rFunctorNe (prodRF F1 F2).
+Proof.
+  intros ?? A1 A2 B1 B2 n ???;
+    by apply prodC_map_ne; apply rFunctor_ne.
+Qed.
+Instance prodRF_contractive F1 F2 :
+  rFunctorContractive F1 → rFunctorContractive F2 →
+  rFunctorContractive (prodRF F1 F2).
+Proof.
+  intros ?? A1 A2 B1 B2 n ???;
+    by apply prodC_map_ne; apply rFunctor_contractive.
+Qed.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 53aeeb909..a1a87b890 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -336,16 +336,26 @@ Structure cFunctor := CFunctor {
   cFunctor_car : cofeT → cofeT -> cofeT;
   cFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
-  cFunctor_contractive {A1 A2 B1 B2} : Contractive (@cFunctor_map A1 A2 B1 B2);
   cFunctor_id {A B : cofeT} (x : cFunctor_car A B) :
     cFunctor_map (cid,cid) x ≡ x;
   cFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
 }.
-Existing Instances cFunctor_contractive.
 Instance: Params (@cFunctor_map) 5.
 
+Class cFunctorNe (F : cFunctor) :=
+  cFunctor_ne A1 A2 B1 B2 n :> Proper (dist n ==> dist n) (@cFunctor_map F A1 A2 B1 B2).
+Class cFunctorContractive (F : cFunctor) :=
+  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
+
+(* TODO: Check if this instance hurts us. We don't have such a large search space
+   overall, and because of the priority constCF and laterCF should be the only
+   users of this. *)
+Instance cFunctorContractive_Ne F :
+  cFunctorContractive F → cFunctorNe F.
+Proof. intros ?????. apply contractive_ne, _. Qed.
+
 Definition cFunctor_diag (F: cFunctor) (A: cofeT) : cofeT := cFunctor_car F A A.
 Coercion cFunctor_diag : cFunctor >-> Funclass.
 
@@ -353,30 +363,46 @@ Program Definition constCF (B : cofeT) : cFunctor :=
   {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
 Solve Obligations with done.
 
+Instance constCF_contractive B : cFunctorContractive (constCF B).
+Proof. intros ????. apply _. Qed.
+
+Program Definition idCF : cFunctor :=
+  {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
+Solve Obligations with done.
+
+Instance idCF_ne : cFunctorNe idCF.
+Proof. intros ????. solve_proper. Qed.
+
 Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
   cFunctor_map A1 A2 B1 B2 fg :=
     prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
 |}.
-Next Obligation.
-  by intros F1 F2 A1 A2 B1 B2 n ???;
-    apply prodC_map_ne; apply cFunctor_contractive.
-Qed.
 Next Obligation. by intros F1 F2 A B [??]; rewrite /= !cFunctor_id. Qed.
 Next Obligation.
   intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
   by rewrite !cFunctor_compose.
 Qed.
 
+Instance prodCF_ne F1 F2 :
+  cFunctorNe F1 → cFunctorNe F2 → cFunctorNe (prodCF F1 F2).
+Proof.
+  intros ?? A1 A2 B1 B2 n ???;
+    by apply prodC_map_ne; apply cFunctor_ne.
+Qed.
+Instance prodCF_contractive F1 F2 :
+  cFunctorContractive F1 → cFunctorContractive F2 →
+  cFunctorContractive (prodCF F1 F2).
+Proof.
+  intros ?? A1 A2 B1 B2 n ???;
+    by apply prodC_map_ne; apply cFunctor_contractive.
+Qed.
+
 Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := cofe_mor (cFunctor_car F1 B A) (cFunctor_car F2 A B);
   cFunctor_map A1 A2 B1 B2 fg :=
     cofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
 |}.
-Next Obligation.
-  intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
-  apply cofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
-Qed.
 Next Obligation.
   intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
   apply (ne_proper f). apply cFunctor_id.
@@ -386,6 +412,20 @@ Next Obligation.
   rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
 Qed.
 
+Instance cofe_morCF_ne F1 F2 :
+  cFunctorNe F1 → cFunctorNe F2 → cFunctorNe (cofe_morCF F1 F2).
+Proof.
+  intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
+  apply cofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
+Qed.
+Instance cofe_morCF_contractive F1 F2 :
+  cFunctorContractive F1 → cFunctorContractive F2 →
+  cFunctorContractive (cofe_morCF F1 F2).
+Proof.
+  intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
+  apply cofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
+Qed.
+
 (** Discrete cofe *)
 Section discrete_cofe.
   Context `{Equiv A, @Equivalence A (≡)}.
@@ -470,13 +510,22 @@ Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
 Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
 Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
 
-Program Definition laterCF : cFunctor := {|
-  cFunctor_car A B := laterC B;
-  cFunctor_map A1 A2 B1 B2 fg := laterC_map (fg.2)
+Program Definition laterCF (F : cFunctor) : cFunctor := {|
+  cFunctor_car A B := laterC (cFunctor_car F A B);
+  cFunctor_map A1 A2 B1 B2 fg := laterC_map (cFunctor_map F fg)
 |}.
 Next Obligation.
-  intros A1 A2 B1 B2 n fg fg' Hfg.
-  apply laterC_map_contractive=> i ?; by apply Hfg.
+  intros F A B x; simpl. rewrite -{2}(later_map_id x).
+  apply later_map_ext=>y. by rewrite cFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -later_map_compose.
+  apply later_map_ext=>y; apply cFunctor_compose.
+Qed.
+
+Instance laterCF_contractive F : 
+  cFunctorNe F → cFunctorContractive (laterCF F).
+Proof.
+  intros ? A1 A2 B1 B2 n fg fg' Hfg.
+  apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
 Qed.
-Next Obligation. by intros A B []. Qed.
-Next Obligation. by intros A1 A2 A3 B1 B2 B3 f g f' g' []. Qed.
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 4a6e702de..855db70a1 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -11,7 +11,8 @@ Arguments solution_unfold {_} _.
 Arguments solution_fold {_} _.
 
 Module solver. Section solver.
-Context (F : cFunctor) `{Finhab : Inhabited (F unitC)}.
+Context (F : cFunctor) `{Fcontr : cFunctorContractive F}
+        `{Finhab : Inhabited (F unitC)}.
 Notation map := (cFunctor_map F).
 
 Fixpoint A (k : nat) : cofeT :=
diff --git a/algebra/excl.v b/algebra/excl.v
index af31f267a..bc1fe57df 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -201,14 +201,10 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
 Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
 Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
 
-Program Definition exclF (F : cFunctor) : rFunctor := {|
+Program Definition exclRF (F : cFunctor) : rFunctor := {|
   rFunctor_car A B := exclR (cFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
 |}.
-Next Obligation.
-  intros A1 A2 B1 B2 n x1 x2 ??.
-  by apply exclC_map_ne, cFunctor_contractive.
-Qed.
 Next Obligation.
   intros F A B x; simpl. rewrite -{2}(excl_map_id x).
   apply excl_map_ext=>y. by rewrite cFunctor_id.
@@ -217,3 +213,14 @@ Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose.
   apply excl_map_ext=>y; apply cFunctor_compose.
 Qed.
+
+Instance exclRF_ne F : cFunctorNe F → rFunctorNe (exclRF F).
+Proof.
+  intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
+Qed.
+Instance exclRF_contractive F :
+  cFunctorContractive F → rFunctorContractive (exclRF F).
+Proof.
+  intros A1 A2 B1 B2 n x1 x2 ??.
+  by apply exclC_map_ne, cFunctor_contractive.
+Qed.
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 069cb792d..a428f34d3 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -356,9 +356,6 @@ Program Definition mapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := mapC K (cFunctor_car F A B);
   cFunctor_map A1 A2 B1 B2 fg := mapC_map (cFunctor_map F fg)
 |}.
-Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g ?; apply mapC_map_ne, cFunctor_contractive.
-Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
   apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
@@ -368,13 +365,20 @@ Next Obligation.
   apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
 Qed.
 
+Instance mapCF_ne K `{Countable K} F : cFunctorNe F → cFunctorNe (mapCF K F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, cFunctor_ne.
+Qed.
+Instance mapCF_contractive K `{Countable K} F :
+  cFunctorContractive F → cFunctorContractive (mapCF K F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, cFunctor_contractive.
+Qed.
+
 Program Definition mapRF K `{Countable K} (F : rFunctor) : rFunctor := {|
   rFunctor_car A B := mapR K (rFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg := mapC_map (rFunctor_map F fg)
 |}.
-Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g ?; apply mapC_map_ne, rFunctor_contractive.
-Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
   apply map_fmap_setoid_ext=>y ??; apply rFunctor_id.
@@ -383,3 +387,13 @@ Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
   apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
 Qed.
+
+Instance mapRF_ne K `{Countable K} F : rFunctorNe F → rFunctorNe (mapRF K F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, rFunctor_ne.
+Qed.
+Instance mapRF_contractive K `{Countable K} F :
+  rFunctorContractive F → rFunctorContractive (mapRF K F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply mapC_map_ne, rFunctor_contractive.
+Qed.
diff --git a/algebra/frac.v b/algebra/frac.v
index 7dade1f20..5035c76ca 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -248,9 +248,6 @@ Program Definition fracRF (F : rFunctor) : rFunctor := {|
   rFunctor_car A B := fracR (rFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg)
 |}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
-Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(frac_map_id x).
   apply frac_map_ext=>y; apply rFunctor_id.
@@ -259,3 +256,9 @@ Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -frac_map_compose.
   apply frac_map_ext=>y; apply rFunctor_compose.
 Qed.
+
+Instance fracRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (fracRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive.
+Qed.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 10dd8e63b..d23ffc86e 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -292,10 +292,6 @@ Program Definition iprodCF {C} (F : C → cFunctor) : cFunctor := {|
   cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
   cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
 |}.
-Next Obligation.
-  intros C F A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply cFunctor_contractive.
-Qed.
 Next Obligation.
   intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
   apply iprod_map_ext=> y; apply cFunctor_id.
@@ -305,14 +301,23 @@ Next Obligation.
   apply iprod_map_ext=>y; apply cFunctor_compose.
 Qed.
 
+Instance iprodCF_ne {C} (F : C → cFunctor) :
+  (∀ c, cFunctorNe (F c)) → cFunctorNe (iprodCF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>c; apply cFunctor_ne.
+Qed.
+Instance iprodCF_contractive {C} (F : C → cFunctor) :
+  (∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>c; apply cFunctor_contractive.
+Qed.
+
 Program Definition iprodRF {C} (F : C → rFunctor) : rFunctor := {|
   rFunctor_car A B := iprodR (λ c, rFunctor_car (F c) A B);
   rFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, rFunctor_map (F c) fg)
 |}.
-Next Obligation.
-  intros C F A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply rFunctor_contractive.
-Qed.
 Next Obligation.
   intros C F A B g; simpl. rewrite -{2}(iprod_map_id g).
   apply iprod_map_ext=> y; apply rFunctor_id.
@@ -321,3 +326,16 @@ Next Obligation.
   intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
   apply iprod_map_ext=>y; apply rFunctor_compose.
 Qed.
+
+Instance iprodRF_ne {C} (F : C → rFunctor) :
+  (∀ c, rFunctorNe (F c)) → rFunctorNe (iprodRF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>c; apply rFunctor_ne.
+Qed.
+Instance iprodRF_contractive {C} (F : C → rFunctor) :
+  (∀ c, rFunctorContractive (F c)) → rFunctorContractive (iprodRF F).
+Proof.
+  intros ? A1 A2 B1 B2 n ?? g.
+  by apply iprodC_map_ne=>c; apply rFunctor_contractive.
+Qed.
diff --git a/algebra/option.v b/algebra/option.v
index 3b9bbfa34..853578733 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -193,9 +193,6 @@ Program Definition optionCF (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := optionC (cFunctor_car F A B);
   cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
 |}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
-Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
   apply option_fmap_setoid_ext=>y; apply cFunctor_id.
@@ -205,13 +202,20 @@ Next Obligation.
   apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
 Qed.
 
+Instance optionCF_ne F : cFunctorNe F → cFunctorNe (optionCF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
+Qed.
+Instance optionCF_contractive F :
+  cFunctorContractive F → cFunctorContractive (optionCF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
+Qed.
+
 Program Definition optionRF (F : rFunctor) : rFunctor := {|
   rFunctor_car A B := optionR (rFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
 |}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
-Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
   apply option_fmap_setoid_ext=>y; apply rFunctor_id.
@@ -220,3 +224,13 @@ Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
   apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
 Qed.
+
+Instance optionRF_ne F : rFunctorNe F → rFunctorNe (optionRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+Qed.
+Instance optionRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (optionRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
+Qed.
diff --git a/algebra/upred.v b/algebra/upred.v
index 1e8ee934b..0ff7b62ad 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -101,10 +101,6 @@ Program Definition uPredCF (F : rFunctor) : cFunctor := {|
   cFunctor_car A B := uPredC (rFunctor_car F B A);
   cFunctor_map A1 A2 B1 B2 fg := uPredC_map (rFunctor_map F (fg.2, fg.1))
 |}.
-Next Obligation.
-  intros F A1 A2 B1 B2 n P Q HPQ.
-  apply uPredC_map_ne, rFunctor_contractive=> i ?; split; by apply HPQ.
-Qed.
 Next Obligation.
   intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
   apply uPred_map_ext=>y. by rewrite rFunctor_id.
@@ -114,6 +110,13 @@ Next Obligation.
   apply uPred_map_ext=>y; apply rFunctor_compose.
 Qed.
 
+Instance uPredCF_contractive F :
+  rFunctorContractive F → cFunctorContractive (uPredCF F).
+Proof.
+  intros ? A1 A2 B1 B2 n P Q HPQ.
+  apply uPredC_map_ne, rFunctor_contractive=> i ?; split; by apply HPQ.
+Qed.
+
 (** logical entailement *)
 Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
   { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
diff --git a/barrier/client.v b/barrier/client.v
index 54cae55da..57465a50d 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -12,7 +12,7 @@ Definition client : expr [] :=
     (^(worker 12) '"b" '"y" || ^(worker 17) '"b" '"y").
 
 Section client.
-  Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
+  Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ, !spawnG Σ} (heapN N : namespace).
   Local Notation iProp := (iPropG heap_lang Σ).
 
   Definition y_inv q y : iProp :=
@@ -33,7 +33,7 @@ Section client.
     rewrite /worker. wp_lam. wp_let. ewp apply wait_spec.
     rewrite comm. apply sep_mono_r. apply wand_intro_l.
     rewrite sep_exist_r. apply exist_elim=>f. wp_seq.
-    (* TODO these aprenthesis are rather surprising. *)
+    (* TODO these parenthesis are rather surprising. *)
     (ewp apply: (wp_load heapN _ _ q f)); eauto with I.
     strip_later. (* hu, shouldn't it do that? *)
     rewrite -assoc. apply sep_mono_r. apply wand_intro_l.
@@ -76,7 +76,7 @@ Qed.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : rFunctorG := #[ heapGF ; barrierGF ; spawnGF ].
+  Definition Σ : gFunctors := #[ heapGF ; barrierGF ; spawnGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
diff --git a/barrier/proof.v b/barrier/proof.v
index 8cdd1ad6c..c0392b89a 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -10,17 +10,17 @@ Import uPred.
 (* Not bundling heapG, as it may be shared with other users. *)
 Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG heap_lang Σ sts;
-  barrier_savedPropG :> savedPropG heap_lang Σ laterCF;
+  barrier_savedPropG :> savedPropG heap_lang Σ (laterCF idCF);
 }.
 (** The Functors we need. *)
-Definition barrierGF : rFunctors := [stsGF sts; agreeRF laterCF].
+Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF (laterCF idCF)].
 (* Show and register that they match. *)
 Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ.
 Proof. destruct H as (?&?&?). split; apply _. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ}.
+Context {Σ : gFunctors} `{!heapG Σ, !barrierG Σ}.
 Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
@@ -119,7 +119,7 @@ Proof.
   apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
   rewrite !assoc. apply pvs_wand_r.
   (* The core of this proof: Allocating the STS and the saved prop. *)
-  eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=laterCF) _ (Next P)).
+  eapply sep_elim_True_r; first by eapply (saved_prop_alloc (F:=laterCF idCF) _ (Next P)).
   rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
   apply exist_elim=>i.
   trans (pvs ⊤ ⊤ (heap_ctx heapN ★
@@ -182,7 +182,7 @@ Proof.
   rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
   apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
   rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
-  apply exist_elim=>i. rewrite -!assoc. apply const_elim_sep_l=>?.
+  apply exist_elim=>i. rewrite -!(assoc (★)%I). apply const_elim_sep_l=>?.
   wp_focus (! _)%E.
   (* I think some evars here are better than repeating *everything* *)
   eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
@@ -231,7 +231,7 @@ Proof.
   rename P1 into R1. rename P2 into R2. intros HN.
   rewrite {1}/recv /barrier_ctx. 
   apply exist_elim=>γ. rewrite sep_exist_r.  apply exist_elim=>P. 
-  apply exist_elim=>Q. apply exist_elim=>i. rewrite -!assoc.
+  apply exist_elim=>Q. apply exist_elim=>i. rewrite -!(assoc (★)%I).
   apply const_elim_sep_l=>?. rewrite -pvs_trans'.
   (* I think some evars here are better than repeating *everything* *)
   eapply pvs_mk_fsa, (sts_fsaS _ pvs_fsa) with (N0:=N) (γ0:=γ); simpl;
diff --git a/barrier/specification.v b/barrier/specification.v
index 01472466c..8de9c66e3 100644
--- a/barrier/specification.v
+++ b/barrier/specification.v
@@ -4,7 +4,7 @@ From barrier Require Import proof.
 Import uPred.
 
 Section spec.
-Context {Σ : rFunctorG} `{!heapG Σ} `{!barrierG Σ}. 
+Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}. 
 
 Local Notation iProp := (iPropG heap_lang Σ).
 
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index e3bc70046..4760925d5 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -12,7 +12,7 @@ Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
 Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
 
 Section derived.
-Context {Σ : rFunctor}.
+Context {Σ : iFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 8d877e716..4ca6c7dd3 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -15,7 +15,7 @@ Class heapG Σ := HeapG {
   heap_name : gname
 }.
 (** The Functor we need. *)
-Definition heapGF : rFunctor := authGF heapR.
+Definition heapGF : gFunctor := authGF heapR.
 
 Definition to_heap : state → heapR := fmap (λ v, Frac 1 (DecAgree v)).
 Definition of_heap : heapR → state :=
@@ -43,7 +43,7 @@ Notation "l ↦{ q } v" := (heap_mapsto l q v)
 Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
 
 Section heap.
-  Context {Σ : rFunctorG}.
+  Context {Σ : gFunctors}.
   Implicit Types N : namespace.
   Implicit Types P Q : iPropG heap_lang Σ.
   Implicit Types Φ : val → iPropG heap_lang Σ.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 2e8b8fc0e..0e0edce3f 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -7,7 +7,7 @@ Import uPred.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
 
 Section lifting.
-Context {Σ : rFunctor}.
+Context {Σ : iFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
 Implicit Types K : ectx.
diff --git a/heap_lang/par.v b/heap_lang/par.v
index 51ccb03e4..b3b9d1f9d 100644
--- a/heap_lang/par.v
+++ b/heap_lang/par.v
@@ -15,7 +15,7 @@ Infix "||" := ParV : expr_scope.
 Infix "||" := Par : expr_scope.
 
 Section proof.
-Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
+Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
 Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
diff --git a/heap_lang/spawn.v b/heap_lang/spawn.v
index 386354665..c26c69590 100644
--- a/heap_lang/spawn.v
+++ b/heap_lang/spawn.v
@@ -20,15 +20,15 @@ Class spawnG Σ := SpawnG {
   spawn_tokG :> inG heap_lang Σ (exclR unitC);
 }.
 (** The functor we need. *)
-Definition spawnGF : rFunctors := [constRF (exclR unitC)].
+Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
 (* Show and register that they match. *)
 Instance inGF_spawnG
-  `{inGF heap_lang Σ (constRF (exclR unitC))} : spawnG Σ.
-Proof. split. apply: inGF_inG. Qed.
+  `{H : inGFs heap_lang Σ spawnGF} : spawnG Σ.
+Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context {Σ : rFunctorG} `{!heapG Σ, !spawnG Σ}.
+Context {Σ : gFunctors} `{!heapG Σ, !spawnG Σ}.
 Context (heapN N : namespace).
 Local Notation iProp := (iPropG heap_lang Σ).
 
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 87e3f05e1..95ddc3f1b 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -70,7 +70,7 @@ Section LiftingTests.
 End LiftingTests.
 
 Section ClosedProofs.
-  Definition Σ : rFunctorG := #[ heapGF ].
+  Definition Σ : gFunctors := #[ heapGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index b824d58f4..ac2cf9a98 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -8,7 +8,7 @@ Local Hint Extern 10 (✓{_} _) =>
   end; solve_validN.
 
 Section adequacy.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types e : expr Λ.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
@@ -74,9 +74,9 @@ Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
   ∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
 Proof.
   intros Hv ? [k ?]%rtc_nsteps.
-  eapply wp_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
+  eapply wp_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
   { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
-  uPred.unseal; exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_and?.
+  uPred.unseal; exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m); split_and?.
   - by rewrite Res_op ?left_id ?right_id.
   - rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
   - by apply ownG_spec.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 09087055b..7fab97fbb 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,5 +1,5 @@
 From algebra Require Export auth upred_tactics.
-From program_logic Require Export invariants global_functor.
+From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
 (* The CMRA we need. *)
@@ -9,7 +9,7 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_timeless :> CMRADiscrete A;
 }.
 (* The Functor we need. *)
-Definition authGF (A : cmraT) : rFunctor := constRF (authR A).
+Definition authGF (A : cmraT) : gFunctor := GFunctor (constRF (authR A)).
 (* Show and register that they match. *)
 Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
   `{CMRAIdentity A, CMRADiscrete A} : authG Λ Σ A.
@@ -69,8 +69,8 @@ Section auth.
     by rewrite always_and_sep_l.
   Qed.
 
-  Lemma auth_empty γ E : True ⊑ (|={E}=> auth_own γ ∅).
-  Proof. by rewrite -own_update_empty. Qed.
+  Lemma auth_empty γ E : True ⊑ |={E}=> auth_own γ ∅.
+  Proof. by rewrite -own_empty. Qed.
 
   Lemma auth_opened E γ a :
     (▷ auth_inv γ φ ★ auth_own γ a)
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 057830231..eff242b15 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -1,28 +1,9 @@
 From prelude Require Export functions.
 From algebra Require Export iprod.
-From program_logic Require Export pviewshifts.
+From program_logic Require Export pviewshifts global_functor.
 From program_logic Require Import ownership.
 Import uPred.
 
-(** 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) *)
-Definition globalF (Σ : gid → rFunctor) : rFunctor :=
-  iprodRF (λ i, mapRF gname (Σ i)).
-Notation rFunctorG := (gid → rFunctor).
-Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
-
-Class inG (Λ : language) (Σ : rFunctorG) (A : cmraT) := InG {
-  inG_id : gid;
-  inG_prf : A = Σ inG_id (iPreProp Λ (globalF Σ))
-}.
-
-Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
-  iprod_singleton inG_id {[ γ := cmra_transport inG_prf a ]}.
 Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
   ownG (to_globalF γ a).
 Instance: Params (@to_globalF) 5.
@@ -34,22 +15,6 @@ Section global.
 Context `{i : inG Λ Σ A}.
 Implicit Types a : A.
 
-(** * Properties of to_globalC *)
-Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF γ).
-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.
-Qed.
-Lemma to_globalF_unit γ a : unit (to_globalF γ a) ≡ to_globalF γ (unit a).
-Proof.
-  by rewrite /to_globalF
-    iprod_unit_singleton map_unit_singleton cmra_transport_unit.
-Qed.
-Instance to_globalF_timeless γ m : Timeless m → Timeless (to_globalF γ m).
-Proof. rewrite /to_globalF; apply _. Qed.
-
 (** * Transport empty *)
 Instance inG_empty `{Empty A} :
   Empty (Σ inG_id (iPreProp Λ (globalF Σ))) := cmra_transport inG_prf ∅.
@@ -87,6 +52,11 @@ Lemma own_valid_r γ a : own γ a ⊑ (own γ a ★ ✓ a).
 Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊑ (✓ a ★ own γ a).
 Proof. by rewrite comm -own_valid_r. Qed.
+Lemma own_empty `{CMRAIdentity A} γ : True ⊑ own γ ∅.
+Proof.
+  rewrite ownG_empty /own. apply equiv_spec, ownG_proper.
+  (* FIXME: rewrite to_globalF_empty. *)
+Abort.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. unfold own; apply _. Qed.
 Global Instance own_unit_always_stable γ a : AlwaysStable (own γ (unit a)).
@@ -99,7 +69,7 @@ Lemma own_alloc_strong a E (G : gset gname) :
 Proof.
   intros Ha.
   rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
-  - eapply pvs_ownG_updateP_empty, (iprod_singleton_updateP_empty inG_id);
+  - 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.
   - apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
@@ -123,28 +93,19 @@ Proof.
     rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
 Qed.
 
-Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} P γ E :
-  ∅ ~~>: P → True ⊑ (|={E}=> ∃ a, ■ P a ∧ own γ a).
-Proof.
-  intros Hemp.
-  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
-  - eapply pvs_ownG_updateP_empty, iprod_singleton_updateP_empty;
-      first eapply map_singleton_updateP_empty', cmra_transport_updateP', Hemp.
-    naive_solver.
-  - apply exist_elim=>m; apply const_elim_l=>-[a' [-> HP]].
-    rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
-Qed.
-
 Lemma own_update γ a a' E : a ~~> a' → own γ a ⊑ (|={E}=> own γ a').
 Proof.
   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 :
+Lemma own_empty `{Empty A, !CMRAIdentity A} γ E :
   True ⊑ (|={E}=> own γ ∅).
 Proof.
-  rewrite (own_updateP_empty (∅ =)); last by apply cmra_updateP_id.
-  apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
+  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_empty.
+  naive_solver.
 Qed.
 End global.
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index 99cd636de..e7c68d057 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -1,52 +1,107 @@
-From program_logic Require Export ghost_ownership.
+From algebra Require Export iprod.
+From program_logic Require Export model.
 
-Module rFunctors.
-  Inductive rFunctors :=
-    | nil  : rFunctors
-    | cons : rFunctor → rFunctors → rFunctors.
-  Coercion singleton (F : rFunctor) : rFunctors := cons F nil.
+(** Index of a CMRA in the product of global CMRAs. *)
+Definition gid := nat.
 
-  Fixpoint fold_right {A} (f : rFunctor → A → A) (a : A) (Fs : rFunctors) : A :=
+(** Name of one instance of a particular CMRA in the ghost state. *)
+Definition gname := positive.
+
+(** The "default" iFunctor is constructed as the dependent product of
+    a bunch of gFunctor. *)
+Structure gFunctor := GFunctor {
+  gFunctor_F :> rFunctor;
+  gFunctor_contractive : rFunctorContractive gFunctor_F;
+}.
+Arguments GFunctor _ {_}.
+Existing Instance gFunctor_contractive.
+
+(** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *)
+Definition globalF (Σ : gid → gFunctor) : iFunctor :=
+  IFunctor (iprodRF (λ i, mapRF gname (Σ i))).
+Notation gFunctors := (gid → gFunctor).
+Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
+
+Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
+  inG_id : gid;
+  inG_prf : A = Σ inG_id (iPreProp Λ (globalF Σ))
+}.
+
+Definition to_globalF `{inG Λ Σ 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}.
+Implicit Types a : A.
+
+Global Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF γ).
+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.
+Qed.
+Lemma to_globalF_unit γ a : unit (to_globalF γ a) ≡ to_globalF γ (unit a).
+Proof.
+  by rewrite /to_globalF
+    iprod_unit_singleton map_unit_singleton cmra_transport_unit.
+Qed.
+Global Instance to_globalF_timeless γ m : Timeless m → Timeless (to_globalF γ m).
+Proof. rewrite /to_globalF; apply _. Qed.
+End to_globalF.
+
+(** 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 gFunctorList :=
+    | nil  : gFunctorList
+    | cons : gFunctor → gFunctorList → gFunctorList.
+  Coercion singleton (F : gFunctor) : gFunctorList := cons F nil.
+
+  Fixpoint fold_right {A} (f : gFunctor → A → A) (a : A) (Fs : gFunctorList) : A :=
     match Fs with
     | nil => a
     | cons F Fs => f F (fold_right f a Fs)
     end.
-End rFunctors.
-Notation rFunctors := rFunctors.rFunctors.
+End gFunctorList.
+Notation gFunctorList := gFunctorList.gFunctorList.
 
-Delimit Scope rFunctors_scope with rFunctors.
-Bind Scope rFunctors_scope with rFunctors.
-Arguments rFunctors.cons _ _%rFunctors.
+Delimit Scope gFunctor_scope with gFunctor.
+Bind Scope gFunctor_scope with gFunctorList.
+Arguments gFunctorList.cons _ _%gFunctor.
 
-Notation "[ ]" := rFunctors.nil (format "[ ]") : rFunctors_scope.
-Notation "[ F ]" := (rFunctors.cons F rFunctors.nil) : rFunctors_scope.
+Notation "[ ]" := gFunctorList.nil (format "[ ]") : gFunctor_scope.
+Notation "[ F ]" := (gFunctorList.cons F gFunctorList.nil) : gFunctor_scope.
 Notation "[ F ; .. ; F' ]" :=
-  (rFunctors.cons F .. (rFunctors.cons F' rFunctors.nil) ..) : rFunctors_scope.
+  (gFunctorList.cons F .. (gFunctorList.cons F' gFunctorList.nil) ..) : gFunctor_scope.
 
-Module rFunctorG.
-  Definition nil : rFunctorG := const (constRF unitR).
+Module gFunctors.
+  Definition nil : gFunctors := const (GFunctor (constRF unitR)).
 
-  Definition cons (F : rFunctor) (Σ : rFunctorG) : rFunctorG :=
+  Definition cons (F : gFunctor) (Σ : gFunctors) : gFunctors :=
     λ n, match n with O => F | S n => Σ n end.
 
-  Fixpoint app (Fs : rFunctors) (Σ : rFunctorG) : rFunctorG :=
+  Fixpoint app (Fs : gFunctorList) (Σ : gFunctors) : gFunctors :=
     match Fs with
-    | rFunctors.nil => Σ
-    | rFunctors.cons F Fs => cons F (app Fs Σ)
+    | gFunctorList.nil => Σ
+    | gFunctorList.cons F Fs => cons F (app Fs Σ)
     end.
-End rFunctorG.
+End gFunctors.
 
-(** Cannot bind this scope with the [rFunctorG] since [rFunctorG] is a
+(** Cannot bind this scope with the [gFunctorG] since [gFunctorG] is a
 notation hiding a more complex type. *)
-Notation "#[ ]" := rFunctorG.nil (format "#[ ]").
-Notation "#[ Fs ]" := (rFunctorG.app Fs rFunctorG.nil).
+Notation "#[ ]" := gFunctors.nil (format "#[ ]").
+Notation "#[ Fs ]" := (gFunctors.app Fs gFunctors.nil).
 Notation "#[ Fs ; .. ; Fs' ]" :=
-  (rFunctorG.app Fs .. (rFunctorG.app Fs' rFunctorG.nil) ..).
+  (gFunctors.app Fs .. (gFunctors.app Fs' 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 (Λ : language) (Σ : rFunctorG) (F : rFunctor) := InGF {
+Class inGF (Λ : language) (Σ : gFunctors) (F : gFunctor) := InGF {
   inGF_id : gid;
   inGF_prf : F = Σ inGF_id;
 }.
@@ -59,21 +114,21 @@ Hint Mode inGF + + - : typeclass_instances.
 
 Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (iPreProp Λ (globalF Σ))).
 Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
-Instance inGF_here {Λ Σ} (F: rFunctor) : inGF Λ (rFunctorG.cons F Σ) F.
+Instance inGF_here {Λ Σ} (F: gFunctor) : inGF Λ (gFunctors.cons F Σ) F.
 Proof. by exists 0. Qed.
-Instance inGF_further {Λ Σ} (F F': rFunctor) :
-  inGF Λ Σ F → inGF Λ (rFunctorG.cons F' Σ) F.
+Instance inGF_further {Λ Σ} (F F': gFunctor) :
+  inGF Λ Σ F → inGF Λ (gFunctors.cons F' Σ) F.
 Proof. intros [i ?]. by exists (S 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 (Λ : language) (Σ : rFunctorG) (Fs : rFunctors) :=
-  InGFs : (rFunctors.fold_right (λ F T, inGF Λ Σ F * T) () Fs)%type.
+Class inGFs (Λ : language) (Σ : 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 Λ Σ (rFunctors.cons F Fs).
+  inGF Λ Σ F → inGFs Λ Σ Fs → inGFs Λ Σ (gFunctorList.cons F Fs).
 Proof. by split. Qed.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 3d4e283e9..667a5960d 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -19,7 +19,7 @@ Notation "{{ P } } e {{ Φ } }" := (True ⊑ ht ⊤ P e Φ)
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
 
 Section hoare.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ Ψ : val Λ → iProp Λ Σ.
 Implicit Types v : val Λ.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index d3bea2519..ac4842d17 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -13,7 +13,7 @@ Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
    format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
 
 Section lifting.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types e : expr Λ.
 Implicit Types P Q R : iProp Λ Σ.
 Implicit Types Ψ : val Λ → iProp Λ Σ.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 324e00387..05388245b 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -14,7 +14,7 @@ Instance: Params (@inv) 3.
 Typeclasses Opaque inv.
 
 Section inv.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types i : positive.
 Implicit Types N : namespace.
 Implicit Types P Q R : iProp Λ Σ.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 32cfe5cc0..784f06dbf 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -8,7 +8,7 @@ Local Hint Extern 10 (✓{_} _) =>
   end; solve_validN.
 
 Section lifting.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
diff --git a/program_logic/model.v b/program_logic/model.v
index 420a6730b..d9ad12adb 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -2,19 +2,27 @@ From algebra Require Export upred.
 From program_logic Require Export resources.
 From algebra Require Import cofe_solver.
 
-(* The Iris program logic is parametrized by a functor from the category of
-COFEs to the category of CMRAs, which is instantiated with [laterC iProp]. The
-[laterC iProp] can be used to construct impredicate CMRAs, such as the stored
-propositions using the agreement CMRA. *)
+(* The Iris program logic is parametrized by a locally contractive functor
+from the category of COFEs to the category of CMRAs, which is instantiated
+with [iProp]. The [iProp] can be used to construct impredicate CMRAs, such as
+the stored propositions using the agreement CMRA. *)
+Structure iFunctor := IFunctor {
+  iFunctor_F :> rFunctor;
+  iFunctor_contractive : rFunctorContractive iFunctor_F;
+  iFunctor_empty (A : cofeT) : Empty (iFunctor_F A);
+  iFunctor_identity (A : cofeT) : CMRAIdentity (iFunctor_F A);
+}.
+Arguments IFunctor _ {_ _ _}.
+Existing Instances iFunctor_contractive iFunctor_empty iFunctor_identity.
 
 Module Type iProp_solution_sig.
-Parameter iPreProp : language → rFunctor → cofeT.
-Definition iGst (Λ : language) (Σ : rFunctor) : cmraT := Σ (iPreProp Λ Σ).
+Parameter iPreProp : language → iFunctor → cofeT.
+Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ).
 Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
 Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
 Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
 Definition iPst Λ := excl (state Λ).
-Definition iProp (Λ : language) (Σ : rFunctor) : cofeT := uPredC (iResR Λ Σ).
+Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ).
 
 Parameter iProp_unfold: ∀ {Λ Σ}, iProp Λ Σ -n> iPreProp Λ Σ.
 Parameter iProp_fold: ∀ {Λ Σ}, iPreProp Λ Σ -n> iProp Λ Σ.
@@ -25,17 +33,17 @@ Parameter iProp_unfold_fold: ∀ {Λ Σ} (P : iPreProp Λ Σ),
 End iProp_solution_sig.
 
 Module Export iProp_solution : iProp_solution_sig.
-Definition iProp_result (Λ : language) (Σ : rFunctor) :
-  solution (uPredCF (resRF Λ laterCF Σ)) := solver.result _.
+Definition iProp_result (Λ : language) (Σ : iFunctor) :
+  solution (uPredCF (resRF Λ (laterCF idCF) Σ)) := solver.result _.
 
-Definition iPreProp (Λ : language) (Σ : rFunctor) : cofeT := iProp_result Λ Σ.
-Definition iGst (Λ : language) (Σ : rFunctor) : cmraT := Σ (iPreProp Λ Σ).
+Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp_result Λ Σ.
+Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ).
 Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
 Definition iResR Λ Σ := resR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
 Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
 Definition iPst Λ := excl (state Λ).
 
-Definition iProp (Λ : language) (Σ : rFunctor) : cofeT := uPredC (iResR Λ Σ).
+Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResR Λ Σ).
 Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ :=
   solution_fold (iProp_result Λ Σ).
 Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index af0c10c03..495c985fb 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -4,7 +4,7 @@ Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
   uPred_ownM (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
 Arguments ownI {_ _} _ _%I.
 Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_ownM (Res ∅ (Excl σ) ∅).
-Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownM (Res ∅ ∅ (Some m)).
+Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownM (Res ∅ ∅ m).
 Instance: Params (@ownI) 3.
 Instance: Params (@ownP) 2.
 Instance: Params (@ownG) 2.
@@ -12,7 +12,7 @@ Instance: Params (@ownG) 2.
 Typeclasses Opaque ownI ownG ownP.
 
 Section ownership.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types r : iRes Λ Σ.
 Implicit Types σ : state Λ.
 Implicit Types P : iProp Λ Σ.
@@ -61,10 +61,12 @@ Lemma always_ownG m : unit m ≡ m → (□ ownG m)%I ≡ ownG m.
 Proof. by intros <-; rewrite always_ownG_unit. Qed.
 Lemma ownG_valid m : ownG m ⊑ ✓ m.
 Proof.
-  rewrite /ownG uPred.ownM_valid res_validI /= option_validI; auto with I.
+  rewrite /ownG uPred.ownM_valid res_validI /=; auto with I.
 Qed.
 Lemma ownG_valid_r m : ownG m ⊑ (ownG m ★ ✓ m).
 Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
+Lemma ownG_empty : True ⊑ (ownG ∅ : iProp Λ Σ).
+Proof. apply uPred.ownM_empty. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 Global Instance ownG_unit_always_stable m : AlwaysStable (ownG (unit m)).
@@ -88,7 +90,7 @@ Proof.
   rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
   rewrite (timeless_iff n). naive_solver (apply cmra_empty_leastN).
 Qed.
-Lemma ownG_spec n r m : (ownG m) n r ↔ Some m ≼{n} gst r.
+Lemma ownG_spec n r m : (ownG m) n r ↔ m ≼{n} gst r.
 Proof.
   rewrite /ownG; uPred.unseal.
   rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_leastN).
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 6d1312c3e..e98fa4095 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -40,7 +40,7 @@ Notation "|={ E }=> Q" := (pvs E E Q%I)
    format "|={ E }=>  Q") : uPred_scope.
 
 Section pvs.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types m : iGst Λ Σ.
 
@@ -115,23 +115,12 @@ Qed.
 Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
   m ~~>: P → ownG m ⊑ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
 Proof.
-  rewrite pvs_eq. intros Hup%option_updateP'.
+  rewrite pvs_eq. intros Hup.
   uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
-  destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
+  destruct (wsat_update_gst k (E ∪ Ef) σ r rf m P) as (m'&?&?); eauto.
   { apply cmra_includedN_le with (S n); auto. }
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
 Qed.
-Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
-    E (P : iGst Λ Σ → Prop) :
-  ∅ ~~>: P → True ⊑ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
-Proof.
-  rewrite pvs_eq. intros Hup; uPred.unseal; split=> -[|n] r ? _ rf [|k] Ef σ ???; try lia.
-  destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto.
-  { apply cmra_empty_leastN. }
-  { apply cmra_updateP_compose_l with (Some ∅), option_updateP with P;
-      auto using option_update_None. }
-  exists (update_gst m' r); by split; [exists m'; split; [|apply ownG_spec]|].
-Qed.
 Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ (|={E}=> ∃ i, ■ (i ∈ E) ∧ ownI i P).
 Proof.
   rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 32387d522..1d411a3bf 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -5,7 +5,7 @@ From program_logic Require Export language.
 Record res (Λ : language) (A : cofeT) (M : cmraT) := Res {
   wld : mapR positive (agreeR A);
   pst : exclR (stateC Λ);
-  gst : optionR M;
+  gst : M;
 }.
 Add Printing Constructor res.
 Arguments Res {_ _ _} _ _ _.
@@ -73,7 +73,7 @@ Proof. by destruct 3; constructor; try apply: timeless. Qed.
 
 Instance res_op : Op (res Λ A M) := λ r1 r2,
   Res (wld r1 â‹… wld r2) (pst r1 â‹… pst r2) (gst r1 â‹… gst r2).
-Global Instance res_empty : Empty (res Λ A M) := Res ∅ ∅ ∅.
+Global Instance res_empty `{Empty M} : Empty (res Λ A M) := Res ∅ ∅ ∅.
 Instance res_unit : Unit (res Λ A M) := λ r,
   Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
 Instance res_valid : Valid (res Λ A M) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
@@ -124,7 +124,7 @@ Proof.
     by exists (Res w σ m, Res w' σ' m').
 Qed.
 Canonical Structure resR : cmraT := CMRAT res_cofe_mixin res_cmra_mixin.
-Global Instance res_cmra_identity : CMRAIdentity resR.
+Global Instance res_cmra_identity `{CMRAIdentity M} : CMRAIdentity resR.
 Proof.
   split.
   - split_and!; apply cmra_empty_valid.
@@ -135,7 +135,7 @@ Qed.
 Definition update_pst (σ : state Λ) (r : res Λ A M) : res Λ A M :=
   Res (wld r) (Excl σ) (gst r).
 Definition update_gst (m : M) (r : res Λ A M) : res Λ A M :=
-  Res (wld r) (pst r) (Some m).
+  Res (wld r) (pst r) m.
 
 Lemma wld_validN n r : ✓{n} r → ✓{n} wld r.
 Proof. by intros (?&?&?). Qed.
@@ -176,7 +176,7 @@ Arguments resR : clear implicits.
 (* Functor *)
 Definition res_map {Λ} {A A' : cofeT} {M M' : cmraT}
     (f : A → A') (g : M → M') (r : res Λ A M) : res Λ A' M' :=
-  Res (agree_map f <$> wld r) (pst r) (g <$> gst r).
+  Res (agree_map f <$> wld r) (pst r) (g $ gst r).
 Instance res_map_ne {Λ} {A A': cofeT} {M M' : cmraT} (f : A → A') (g : M → M') :
   (∀ n, Proper (dist n ==> dist n) f) → (∀ n, Proper (dist n ==> dist n) g) →
   ∀ n, Proper (dist n ==> dist n) (@res_map Λ _ _ _ _ f g).
@@ -186,7 +186,6 @@ Proof.
   constructor; rewrite /res_map /=; f_equal.
   - rewrite -{2}(map_fmap_id (wld r)). apply map_fmap_setoid_ext=> i y ? /=.
     by rewrite -{2}(agree_map_id y).
-  - by rewrite option_fmap_id.
 Qed.
 Lemma res_map_compose {Λ} {A1 A2 A3 : cofeT} {M1 M2 M3 : cmraT}
    (f : A1 → A2) (f' : A2 → A3) (g : M1 → M2) (g' : M2 → M3) (r : res Λ A1 M1) :
@@ -195,7 +194,6 @@ Proof.
   constructor; rewrite /res_map /=; f_equal.
   - rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=.
     by rewrite -agree_map_compose.
-  - by rewrite option_fmap_compose.
 Qed.
 Lemma res_map_ext {Λ} {A A' : cofeT} {M M' : cmraT}
     (f f' : A → A') (g g' : M → M') (r : res Λ A M) :
@@ -203,7 +201,6 @@ Lemma res_map_ext {Λ} {A A' : cofeT} {M M' : cmraT}
 Proof.
   intros Hf Hg; split; simpl; auto.
   - by apply map_fmap_setoid_ext=>i x ?; apply agree_map_ext.
-  - by apply option_fmap_setoid_ext.
 Qed.
 Instance res_map_cmra_monotone {Λ}
     {A A' : cofeT} {M M': cmraT} (f: A → A') (g: M → M') :
@@ -223,19 +220,13 @@ Instance resC_map_ne {Λ A A' M M'} n :
 Proof.
   intros f g Hfg r; split; simpl; auto.
   - by apply (mapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
-  - by apply optionC_map_ne.
 Qed.
 
 Program Definition resRF (Λ : language)
-    (F : cFunctor) (Σ : rFunctor) : rFunctor := {|
-  rFunctor_car A B := resR Λ (cFunctor_car F A B) (rFunctor_car Σ A B);
-  rFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F fg) (rFunctor_map Σ fg)
+    (F1 : cFunctor) (F2 : rFunctor) : rFunctor := {|
+  rFunctor_car A B := resR Λ (cFunctor_car F1 A B) (rFunctor_car F2 A B);
+  rFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
-Next Obligation.
-  intros Λ F Σ A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
-  - by apply cFunctor_contractive.
-  - by apply rFunctor_contractive.
-Qed.
 Next Obligation.
   intros Λ F Σ A B x. rewrite /= -{2}(res_map_id x).
   apply res_map_ext=>y. apply cFunctor_id. apply rFunctor_id.
@@ -244,3 +235,12 @@ Next Obligation.
   intros Λ F Σ A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -res_map_compose.
   apply res_map_ext=>y. apply cFunctor_compose. apply rFunctor_compose.
 Qed.
+
+Instance resRF_contractive Λ F1 F2 :
+  cFunctorContractive F1 → rFunctorContractive F2 →
+  rFunctorContractive (resRF Λ F1 F2).
+Proof.
+  intros ?? A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
+  - by apply cFunctor_contractive.
+  - by apply rFunctor_contractive.
+Qed.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index ef129783f..e0543d70e 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -1,12 +1,17 @@
 From algebra Require Export agree.
-From program_logic Require Export global_functor.
+From program_logic Require Export ghost_ownership.
 Import uPred.
 
-Class savedPropG (Λ : language) (Σ : rFunctorG) (F : cFunctor) :=
-  saved_prop_inG :> inG Λ Σ (agreeR (F (iPreProp Λ (globalF Σ)))).
-
-Instance inGF_savedPropG `{inGF Λ Σ (agreeRF F)} : savedPropG Λ Σ F.
-Proof. apply: inGF_inG. Qed.
+Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
+  SavedPropG {
+    saved_prop_F_contractive :> cFunctorContractive F;
+    saved_prop_inG :> inG Λ Σ (agreeR (F (iPreProp Λ (globalF Σ))));
+  }.
+Definition savedPropGF (F : cFunctor) `{cFunctorContractive F} :
+  gFunctor := GFunctor (agreeRF F).
+Instance inGF_savedPropG `{cFunctorContractive F}
+         `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F.
+Proof. split; try apply _; apply: inGF_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Λ Σ F}
     (γ : gname) (x : F (iPropG Λ Σ)) : iPropG Λ Σ :=
diff --git a/program_logic/sts.v b/program_logic/sts.v
index a429981e1..e9034fb73 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,5 +1,5 @@
 From algebra Require Export sts upred_tactics.
-From program_logic Require Export invariants global_functor.
+From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
 (** The CMRA we need. *)
@@ -9,7 +9,7 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 }.
 Coercion sts_inG : stsG >-> inG.
 (** The Functor we need. *)
-Definition stsGF (sts : stsT) : rFunctor := constRF (stsR sts).
+Definition stsGF (sts : stsT) : gFunctor := GFunctor (constRF (stsR sts)).
 (* Show and register that they match. *)
 Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
   `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
@@ -59,8 +59,6 @@ Section sts.
   Implicit Types S : sts.states sts.
   Implicit Types T : sts.tokens sts.
 
-  (** Setoids *)
-
   (* The same rule as implication does *not* hold, as could be shown using
      sts_frag_included. *)
   Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
diff --git a/program_logic/tactics.v b/program_logic/tactics.v
index dbbc1ce90..f3e1b6e3d 100644
--- a/program_logic/tactics.v
+++ b/program_logic/tactics.v
@@ -6,7 +6,7 @@ Module uPred_reflection_pvs.
   Import uPred_reflection.
   Section uPred_reflection_pvs.
   
-  Context {Λ : language} {Σ : rFunctor}.
+  Context {Λ : language} {Σ : iFunctor}.
   Local Notation iProp := (iProp Λ Σ).
 
   Lemma cancel_entails_pvs Σ' E1 E2 e1 e2 e1' e2' ns :
diff --git a/program_logic/tests.v b/program_logic/tests.v
index 5fae5c570..4f39e8b27 100644
--- a/program_logic/tests.v
+++ b/program_logic/tests.v
@@ -2,20 +2,21 @@
 From program_logic Require Import model saved_prop.
 
 Module ModelTest. (* Make sure we got the notations right. *)
-  Definition iResTest {Λ : language} {Σ : rFunctor}
-    (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p (Some g).
+  Definition iResTest {Λ : language} {Σ : iFunctor}
+    (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p g.
 End ModelTest.
 
 Module SavedPropTest.
   (* Test if we can really go "crazy higher order" *)
   Section sec.
-    Definition Σ : rFunctorG := #[ agreeRF (cofe_morCF laterCF laterCF) ].
+    Definition F := laterCF (cofe_morCF idCF idCF).
+    Definition Σ : gFunctors := #[ savedPropGF F ].
     Context {Λ : language}.
     Notation iProp := (iPropG Λ Σ).
 
-    Local Instance : savedPropG Λ Σ (cofe_morCF laterCF laterCF) := _.
+    Local Instance : savedPropG Λ Σ F := _.
 
-    Definition own_pred γ (φ : laterC iProp -n> laterC iProp) : iProp :=
+    Definition own_pred γ (φ : laterC (iProp -n> iProp)) : iProp :=
       saved_prop_own γ φ.
   End sec.
 End SavedPropTest.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 28a3cb3d0..7737c2bfa 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -18,7 +18,7 @@ Notation "P ={ E }=> Q" := (True ⊑ vs E E P%I Q%I)
   (at level 199, E at level 50, format "P  ={ E }=>  Q") : C_scope.
 
 Section vs.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q R : iProp Λ Σ.
 Implicit Types N : namespace.
 
@@ -114,10 +114,11 @@ Lemma vs_own_updateP E γ a φ :
   a ~~>: φ → own γ a ={E}=> ∃ a', ■ φ a' ∧ own γ a'.
 Proof. by intros; apply vs_alt, own_updateP. Qed.
 
-Lemma vs_own_updateP_empty `{Empty A, !CMRAIdentity A} E γ φ :
-  ∅ ~~>: φ → True ={E}=> ∃ a', ■ φ a' ∧ own γ a'.
-Proof. by intros; eapply vs_alt, own_updateP_empty. Qed.
-
 Lemma vs_update E γ a a' : a ~~> a' → own γ a ={E}=> own γ a'.
 Proof. by intros; apply vs_alt, own_update. Qed.
+
+Lemma vs_own_empty `{Empty A, !CMRAIdentity A} E γ :
+  True ={E}=> own γ ∅.
+Proof. by intros; eapply vs_alt, own_empty. Qed.
+
 End vs_ghost.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 432764235..c87f8635f 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -65,7 +65,7 @@ Notation "#> e {{ Φ } }" := (wp ⊤ e Φ)
    format "#>  e   {{  Φ  } }") : uPred_scope.
 
 Section wp.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 Implicit Types v : val Λ.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 89f0160fd..5cbcab711 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -28,13 +28,12 @@ Instance: Params (@wsat) 5.
 Arguments wsat : simpl never.
 
 Section wsat.
-Context {Λ : language} {Σ : rFunctor}.
+Context {Λ : language} {Σ : iFunctor}.
 Implicit Types σ : state Λ.
 Implicit Types r : iRes Λ Σ.
 Implicit Types rs : gmap positive (iRes Λ Σ).
 Implicit Types P : iProp Λ Σ.
 Implicit Types m : iGst Λ Σ.
-Implicit Types mm : option (iGst Λ Σ).
 
 Instance wsat_ne' : Proper (dist n ==> impl) (@wsat Λ Σ n E σ).
 Proof.
@@ -68,7 +67,7 @@ Proof.
   destruct n; first done.
   intros _ [rs ?]; eapply cmra_validN_op_l, wsat_pre_valid; eauto.
 Qed.
-Lemma wsat_init k E σ mm : ✓{S k} mm → wsat (S k) E σ (Res ∅ (Excl σ) mm).
+Lemma wsat_init k E σ m : ✓{S k} m → wsat (S k) E σ (Res ∅ (Excl σ) m).
 Proof.
   intros Hv. exists ∅; constructor; auto.
   - rewrite big_opM_empty right_id.
@@ -125,13 +124,13 @@ Proof.
   split; [done|exists rs].
   by constructor; first split_and!; try rewrite /= -assoc Hpst'.
 Qed.
-Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
-  mm1 ≼{S n} gst r → mm1 ~~>: (λ mm2, default False mm2 P) →
+Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
+  m1 ≼{S n} gst r → m1 ~~>: P →
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.
   intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
-  destruct (Hup (S n) (mf â‹… gst (rf â‹… big_opM rs))) as ([m2|]&?&Hval'); try done.
-  { by rewrite /= (assoc _ mm1) -Hr assoc. }
+  destruct (Hup (S n) (mf â‹… gst (rf â‹… big_opM rs))) as (m2&?&Hval'); try done.
+  { by rewrite /= (assoc _ m1) -Hr assoc. }
   exists m2; split; [exists rs|done].
   by constructor; first split_and!; auto.
 Qed.
-- 
GitLab