diff --git a/docs/proof_guide.md b/docs/resource_algebras.md
index 3195c63d..eaee3948 100644
--- a/docs/proof_guide.md
+++ b/docs/resource_algebras.md
@@ -1,101 +1,17 @@
-# Iris Proof Guide
+## Global resource algebra management
-This work-in-progress document serves to explain how Iris proofs are typically
-carried out in Coq: what are the common patterns and conventions, what are the
-common pitfalls. This complements the tactic documentation for the
-[proof mode](./proof_mode.md) and [HeapLang](./heap_lang.md).
+The type of Iris propositions `iProp Σ` is parameterized by a *global* list `Σ:
+gFunctors` of resource algebras that the proof may use. (Actually this list
+contains functors instead of resource algebras, but you only need to worry about
+that when dealing with higher-order ghost state -- see "Camera functors" below.)
-## Order of `Requires`
+In our proofs, we always keep the `Σ` universally quantified to enable composition of proofs.
+Each proof just assumes that some particular resource algebras are contained in that global list.
+This is expressed via the `inG Σ R` typeclass, which roughly says that `R ∈ Σ`.
-In Coq, declarations in modules imported later may override the
-previous definition. Therefore, in order to make sure the most
-relevant declarations and notations always take priority, we recommend
-importing dependencies from the furthest to the closest.
-
-In particular, when importing Iris, Stdpp and Coq stdlib modules, we
-recommend importing in the following order:
-- Coq
-- stdpp
-- iris.bi
-- iris.proofmode
-- iris.algebra
-- iris.base_logic
-- iris.program_logic
-- iris.heap_lang
-
-## Combinators for functors
-
-In Iris, the type of propositions [iProp] is described by the solution to the
-recursive domain equation:
-
-```
-iProp ≅ uPred (F (iProp))
-```
-
-Here, `F` is a user-chosen locally contractive bifunctor from COFEs to unital
-Cameras (a step-indexed generalization of unital resource algebras). To make it
-convenient to construct such functors out of smaller pieces, we provide a number
-of abstractions:
-
-- [`cFunctor`](theories/algebra/ofe.v): bifunctors from COFEs to OFEs.
-- [`rFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to cameras.
-- [`urFunctor`](theories/algebra/cmra.v): bifunctors from COFEs to unital
- cameras.
-
-Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
-`urFunctorContractive` which describe the subset of the above functors that
-are contractive.
-
-To compose these functors, we provide a number of combinators, e.g.:
-
-- `constCF (A : ofeT) : cFunctor := λ (B,B⁻), A `
-- `idCF : cFunctor := λ (B,B⁻), B`
-- `prodCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
-- `ofe_morCF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
-- `laterCF (F : cFunctor) : cFunctor := λ (B,B⁻), later (F (B,B⁻))`
-- `agreeRF (F : cFunctor) : rFunctor := λ (B,B⁻), agree (F (B,B⁻))`
-- `gmapURF K (F : rFunctor) : urFunctor := λ (B,B⁻), gmap K (F (B,B⁻))`
-
-Using these combinators, one can easily construct bigger functors in point-free
-style, e.g:
-
-```
-F := gmapURF K (agreeRF (prodCF (constCF natC) (laterCF idCF)))
-```
-
-which effectively defines `F := λ (B,B⁻), gmap K (agree (nat * later B))`.
-
-Furthermore, for functors written using these combinators like the functor `F`
-above, Coq can automatically `urFunctorContractive F`.
-
-To make it a little bit more convenient to write down such functors, we make
-the constant functors (`constCF`, `constRF`, and `constURF`) a coercion, and
-provide the usual notation for products, etc. So the above functor can be
-written as follows (which is similar to the effective definition of `F` above):
-
-```
-F := gmapURF K (agreeRF (natC * ▶ ∙))
-```
-
-## Resource algebra management
-
-When using ghost state in Iris, you have to make sure that the resource algebras
-you need are actually available. Every Iris proof is carried out using a
-universally quantified list `Σ: gFunctors` defining which resource algebras are
-available. The `Σ` is the *global* list of resources that the entire proof can
-use. We keep the `Σ` universally quantified to enable composition of proofs.
-
-You can think of this as a list of resource algebras, though in reality it is a
-list of locally contractive functors from COFEs to Cameras. This list is used
-to define the parameter `F` of Iris mentioned in the previous section. The
-formal side of this is described in §7.4 of
-[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.1.pdf); here we
-describe the user-side Coq aspects of this approach.
-
-The assumptions that an Iris proof makes are collected in a type class called
-`somethingG`. The most common kind of assumptions is `inG`, which says that a
-particular resource algebra is available for ghost state. For example, in the
-[one-shot example](tests/one_shot.v):
+Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
+not have to expose to clients what exactly their resource algebras are. For
+example, in the [one-shot example](../tests/one_shot.v), we have:
```
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
```
@@ -107,10 +23,9 @@ add a field like `one_shot_other :> otherG Σ`.
Having defined the type class, we need to provide a way to instantiate it. This
is an important step, as not every resource algebra can actually be used: if
your resource algebra refers to `Σ`, the definition becomes recursive. That is
-actually legal under some conditions (which is why the global list `Σ` contains
-functors and not just resource algebras), but for the purpose of this guide we
-will ignore that case. We have to define a list that contains all the resource
-algebras we need:
+actually legal under some conditions (see "Camera functors" below), but for now
+we will ignore that case. We have to define a list that contains all the
+resource algebras we need:
```
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
```
@@ -152,7 +67,24 @@ assuming. This can easily lead to making more assumptions than you are aware
of, and often it leads to duplicate assumptions which breaks type class
resolutions.
-### Obtaining a closed proof
+## Resource algebra combinators
+
+Defining a new resource algebra `one_shotR` for each new proof and verifying all
+the algebra laws would be quite cumbersome, so instead Iris provides a rich set
+of resource algebra combinators that one can use to build up the desired
+resource algebras. For example, `one_shotR` is defined as follows:
+
+```
+Definition one_shotR := csumR (exclR unitO) (agreeR ZO).
+```
+
+The suffixes `R` and `O` indicate that we are not working on the level of Coq
+types here, but on the level of `R`esource algebras and `O`FEs,
+respectively. Unfortunately this means we cannot use Coq's usual type notation
+(such as `*` for products and `()` for the unit type); we have to spell out the
+underlying OFE or resource algebra names instead.
+
+## Obtaining a closed proof
To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
`inG`, you have to assemble a list of functors of all the involved modules,
@@ -175,7 +107,7 @@ Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
```
-### Advanced topic: Ghost state singletons
+## Advanced topic: Ghost state singletons
Some Iris modules involve a form of "global state". For example, defining the
`↦` for HeapLang involves a piece of ghost state that matches the current
@@ -224,171 +156,128 @@ assumed explicitly everywhere. Bundling `heapG` in a module type class like
`one_shotG` would lose track of the fact that there exists just one `heapG`
instance that is shared by everyone.
-### Advanced topic: Additional module assumptions
+## Advanced topic: Camera functors and higher-order ghost state
+
+As we already alluded to, `Σ` actually consists of functors, not resource
+algebras. This enables you to use *higher-order ghost state*: ghost state that
+recursively refers to `iProp`.
+
+**Background: Iris Model.** To understand how this works, we have to dig a bit
+into the model of Iris. In Iris, the type of propositions `iProp` is described
+by the solution to the recursive domain equation:
-Some modules need additional assumptions. For example, the STS module is
-parameterized by an STS and assumes that the STS state space is inhabited:
```
-Class stsG Σ (sts : stsT) := {
- sts_inG :> inG Σ (stsR sts);
- sts_inhabited :> Inhabited (sts.state sts);
-}.
+iProp ≅ uPred (F (iProp))
```
-In this rather exceptional case, the `Instance` for this class has more than
-just a `subG` assumption:
-```
-Instance subG_stsΣ Σ sts :
- subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
-```
-If users of this module follow the pattern described above, their own type class
-instance will check these additional assumption. But this is one more reason
-why it is important for every module to have an instance for its `somethingG`:
-to make sure that it does not accidentally make more assumptions than it intends
-to.
-
-Another subtle detail here is that the `subG` assumption comes first in
-`subG_stsΣ`, i.e., it appears before the `Inhabited`. This is important because
-otherwise, `sts_inhabited` and `subG_stsΣ` form an instance cycle that makes
-type class search diverge.
-
-## Canonical structures and type classes
-
-In Iris, we use both canonical structures and type classes, and some careful
-tweaking is necessary to make the two work together properly. The details of
-this still need to be written up properly, but here is some background material:
-
-* [Type Classes for Mathematics in Type Theory](http://www.eelis.net/research/math-classes/mscs.pdf)
-* [Canonical Structures for the working Coq user](https://hal.inria.fr/hal-00816703v1/document)
-
-## Implicit generalization
-
-We often use the implicit generalization feature of Coq, triggered by a backtick:
-`` `{!term A B}`` means that an implicit argument of type `term A B` is added,
-and if any of the identifiers that are used here is not yet bound, it gets added
-as well. Usually, `term` will be some existing type class or similar, and we
-use this syntax to also generalize over `A` and `B`; then the above is
-equivalent to `{A B} {Hterm: term A B}`. The `!` in front of the term disables
-an even stronger form of generalization, where if `term` is a type class then
-all missing arguments get implicitly generalized as well. This is sometimes
-useful, e.g. we can write `` `{Countable C}`` instead of `` `{!EqDecision C,
-!Countable C}``. However, generally it is more important to be aware of the
-assumptions you are making, so implicit generalization without `!` should be
-avoided.
-
-## Type class resolution control
-
-When you are writing a module that exports some Iris term for others to use
-(e.g., `join_handle` in the [spawn module](theories/heap_lang/lib/spawn.v)), be
-sure to mark these terms as opaque for type class search at the *end* of your
-module (and outside any section):
-```
-Typeclasses Opaque join_handle.
-```
-This makes sure that the proof mode does not "look into" your definition when it
-is used by clients.
-
-## Notations
-
-Notations starting with `(` or `{` should be left at their default level (`0`),
-and inner subexpressions that are bracketed by delimiters should be left at
-their default level (`200`).
-
-Moreover, correct parsing of notations sometimes relies on Coq's automatic
-left-factoring, which can require coordinating levels of certain "conflicting"
-notations and their subexpressions. For instance, to disambiguate `(⊢@{ PROP
-})` and `(⊢@{ PROP } P)`, Coq must factor out a nonterminal for `⊢@{ PROP }`,
-but it can only do so if all occurrences of `⊢@{ PROP }` agree on the
-precedences for all subexpressions. This also requires using the same
-tokenization in all cases, i.e., the notation has to consistently be declared as
-`(⊢@{` or `('⊢@{'`, but not a mixture of the two. The latter form of using
-explicit tokenization with `'` is preferred to avoid relying on Coq's default.
-
-For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules).
-
-## Naming conventions for variables/arguments/hypotheses
-
-### small letters
-
-* a : A = cmraT or ofeT
-* b : B = cmraT or ofeT
-* c
-* d
-* e : expr = expressions
-* f = some generic function
-* g = some generic function
-* h : heap
-* i
-* j
-* k
-* l
-* m : iGst = ghost state
-* m* = prefix for option
-* n
-* o
-* p
-* q
-* r : iRes = resources
-* s = state (STSs)
-* s = stuckness bits
-* t
-* u
-* v : val = values of language
-* w
-* x
-* y
-* z
-
-### capital letters
-
-* A : Type, cmraT or ofeT
-* B : Type, cmraT or ofeT
-* C
-* D
-* E : coPset = Viewshift masks
-* F = a functor
-* G
-* H = hypotheses
-* I = indexing sets
-* J
-* K : ectx = evaluation contexts
-* K = keys of a map
-* L
-* M = maps / global CMRA
-* N : namespace
-* O
-* P : uPred, iProp or Prop
-* Q : uPred, iProp or Prop
-* R : uPred, iProp or Prop
-* S : set state = state sets in STSs
-* T : set token = token sets in STSs
-* U
-* V : abstraction of value type in frame shift assertions
-* W
-* X : sets
-* Y : sets
-* Z : sets
-
-### small greek letters
-
-* γ : gname
-* σ : state = state of language
-* φ : interpretation of STS/Auth
-
-### capital greek letters
-
-* Φ : general predicate (over uPred, iProp or Prop)
-* Ψ : general predicate (over uPred, iProp or Prop)
-
-## Naming conventions for algebraic classes
-
-### Suffixes
-
-* O: OFEs
-* R: cameras
-* UR: unital cameras or resources algebras
-* F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
-* G: global camera functor management (typeclass; see [proof\_guide.md](./proof_guide.md))
-* I: bunched implication logic (of type `bi`)
-* SI: step-indexed bunched implication logic (of type `sbi`)
-* T: canonical structures for algebraic classes (for example ofeT for OFEs, cmraT for cameras)
-* Σ: global camera functor management (`gFunctors`; see [proof\_guide.md](./proof_guide.md))
+
+Here, `uPred M` describes "propositions with resources of type `M`". The
+peculiar aspect of this definition is that the notion of resources can itself
+refer to the set propositions that we are just defining; that dependency is
+expressed by `F`. `F` is a user-chosen locally contractive bifunctor from COFEs
+to unital Cameras (a step-indexed generalization of unital resource
+algebras). Having just a single fixed `F` would however be rather inconvenient,
+so instead we have a list `Σ`, and then we define the global functor `F_global`
+roughly as follows:
+
+```
+F_global X := Π_{F ∈ Σ} gmap nat (F X)
+```
+
+In other words, each functor in `Σ` is applied to the recursive argument `X`,
+wrapped in a finite partial function, and then we take a big product of all of
+that. The product ensures that all `F ∈ Σ` are available, and the `gmap` is
+needed to provide the proof rule `own_alloc`, which lets you create new
+instances of the given type of resource any time.
+
+However, this on its own would be too restrictive, as it requires all
+occurrences of `X` to be in positive positions (otherwise the functor laws
+would not hold for `F`). To mitigate this, we instead work with "bifunctors":
+functors that take two arguments, `X` and `X⁻`, where `X⁻` is used for
+negative positions. This leads us to the following domain equation:
+
+```
+iProp ≅ uPred (F_global (iProp,iProp))
+F_global (X,X⁻) := Π_{F ∈ Σ} gmap nat (F (X,X⁻))
+```
+
+To make this equation well-defined, the bifunctors `F ∈ Σ` need to be "contractive".
+For further details, see §7.4 of
+[The Iris Documentation](http://plv.mpi-sws.org/iris/appendix-3.3.pdf); here we
+describe the user-side Coq aspects of this approach.
+
+Below, when we say "functor", we implicitly mean "bifunctor".
+
+**Higher-order ghost state.** To use higher-order ghost state, you need to give
+a functor whose "hole" will later be filled with `iProp` itself. For example,
+let us say you would like to have ghost state of type `gmap K (agree (nat *
+later iProp))`, using the "type-level" `later` operator which ensures
+contractivity. Then you will have to define a functor such as:
+
+```
+F (X,X⁻) := gmap K (agree (nat * ▶ X))
+```
+
+To make it convenient to construct such functors and prove their contractivity,
+we provide a number of abstractions:
+
+- [`cFunctor`](theories/algebra/ofe.v): functors from COFEs to OFEs.
+- [`rFunctor`](theories/algebra/cmra.v): functors from COFEs to cameras.
+- [`urFunctor`](theories/algebra/cmra.v): functors from COFEs to unital
+ cameras.
+
+Besides, there are the classes `cFunctorContractive`, `rFunctorContractive`, and
+`urFunctorContractive` which describe the subset of the above functors that are
+contractive.
+
+To compose these functors, we provide a number of combinators, e.g.:
+
+- `constOF (A : ofeT) : cFunctor := λ (B,B⁻), A `
+- `idOF : cFunctor := λ (B,B⁻), B`
+- `prodOF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B,B⁻) * F2 (B,B⁻)`
+- `ofe_morOF (F1 F2 : cFunctor) : cFunctor := λ (B,B⁻), F1 (B⁻,B) -n> F2 (B,B⁻)`
+- `laterOF (F : cFunctor) : cFunctor := λ (B,B⁻), later (F (B,B⁻))`
+- `agreeRF (F : cFunctor) : rFunctor := λ (B,B⁻), agree (F (B,B⁻))`
+- `gmapURF K (F : rFunctor) : urFunctor := λ (B,B⁻), gmap K (F (B,B⁻))`
+
+Note in particular how the functor for the function space, `ofe_morOF`, swaps
+`B` and `B⁻` for the functor `F1` describing the domain. This reflects the fact
+that that functor is used in a negative position.
+
+Using these combinators, one can easily construct bigger functors in point-free
+style and automatically infer their contractivity, e.g:
+
+```
+F := gmaURF K (agreeRF (prodOF (constOF natO) (laterOF idOF)))
+```
+
+which effectively defines the desired example functor
+`F := λ (B,B⁻), gmap K (agree (nat * later B))`.
+
+To make it a little bit more convenient to write down such functors, we make
+the constant functors (`constOF`, `constRF`, and `constURF`) a coercion, and
+provide the usual notation for products, etc. So the above functor can be
+written as follows:
+
+```
+F := gmapRF K (agreeRF (natO * ▶ ∙))
+```
+
+Basically, the functor can be written "as if" you were writing a resource
+algebra, except that there need to be extra "F" suffixes to indicate that we are
+working with functors, and the desired recursive `iProp` is replaced by the
+"hole" `∙`.
+
+Putting it all together, the `libG` typeclass and `libΣ` list of functors for
+your example would look as follows:
+
+```
+Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
+Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
+Proof. solve_inG. Qed.
+```
+
+It is instructive to remove the `▶` and see what happens: the `libG` class still
+works just fine, but `libΣ` complains that the functor is not contractive. This
+demonstrates the importance of always defining a `libΣ` alongside the `libG` and
+proving their relation.