diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 9850a424a89e3a64492210abb662133a07013f7d..55c7baf02f8fd36e2bc7035750ee823e9cb8472e 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -2,6 +2,7 @@
 \label{sec:base-logic}
 
 The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit.
+By \lemref{lem:cmra-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following.
 This defines the structure of resources that can be owned.
 
 As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language.
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
new file mode 100644
index 0000000000000000000000000000000000000000..1c9c76d867495704cacf2ed5412ebda209f1805e
--- /dev/null
+++ b/docs/ghost-state.tex
@@ -0,0 +1,43 @@
+\section{Modular Dynamic Higher-Order Resources}
+\label{sec:hogs}
+
+The logic described in \Sref{sec:base-logic} works over an arbitrary CMRA $\monoid$ defining the structure of the resources.
+It turns out that we can generalize this further and permit picking CMRAs ``$\iFunc(\Prop)$'' that depend on the structure of assertions themselves.
+Of course, $\Prop$ is just the syntactic type of assertions; for this to make sense we have to look at the semantics.
+
+To instantiate the logic, you pick a family of locally contractive bifunctors $(\iFunc_i : \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
+
+From this, we construct the bifunctor defining the overall resources as follows:
+\begin{align*}
+  \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \prod_{i \in \mathcal I} \mathbb{N} \fpfn \iFunc_i(\cofe^\op, \cofe)
+\end{align*}
+$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
+Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$.
+
+Now we can write down the recursive domain equation:
+\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
+$\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor.
+This fixed-point exists and is unique by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
+We do not need to consider how the object is constructed. 
+We only need the isomorphism, given by
+\begin{align*}
+  \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
+  \iProp &\eqdef \UPred(\Res) \\
+	\wIso &: \iProp \nfn \iPreProp \\
+	\wIso^{-1} &: \iPreProp \nfn \iProp
+\end{align*}
+
+Notice that $\iProp$ is the semantic model of assertions for  the logic described in \Sref{sec:base-logic} with $\Res$:
+\[ \Sem{\Prop} \eqdef \iProp = \UPred(\Res) \]
+We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical assertions and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.
+
+\ralf{TODO: Describe the pattern of only assuming some elements of the index family to indicate a particular functor.}
+\ralf{TODO: Show the rules for ownership in this world.}
+
+
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End:
diff --git a/docs/iris.tex b/docs/iris.tex
index ff135e11fbfe60fbc43fc90a79f2619e538913bc..05674383cb82d661a7c118ccb1a827614740392d 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -35,6 +35,8 @@
 \endgroup\clearpage\begingroup
 \input{model}
 \endgroup\clearpage\begingroup
+\input{ghost-state}
+\endgroup\clearpage\begingroup
 \input{program-logic}
 \endgroup\clearpage\begingroup
 \input{derived}
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index ce1af0d58f55921efae2469ef104539e1d7be432..733eb31452efc074854a917eaa9ed0f1b8ef47b7 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -1,4 +1,5 @@
 \section{Language}
+\label{sec:language}
 
 A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that
 \begin{itemize}
@@ -58,6 +59,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
 
 \clearpage
 \section{Program Logic}
+\label{sec:program-logic}
 
 \ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}
 
@@ -243,32 +245,7 @@ Notice that this is stronger than saying that the thread pool can reduce; we act
 \subsection{Iris model}
 
 \paragraph{Semantic domain of assertions.}
-The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$.
-We start by defining the functor that assembles the CMRAs we need to the global resource CMRA:
-\begin{align*}
-  \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \mathbb{N} \fpfn \agm(\latert \cofe), \pres: \maybe{\exm(\textdom{State})}, \ghostRes: \iFunc(\cofe^\op, \cofe)}
-\end{align*}
-Above, $\maybe\monoid$ is the monoid obtained by adding a unit to $\monoid$.
-(It's not a coincidence that we used the same notation for the range of the core; it's the same type either way: $\monoid + 1$.)
-Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$ (see~\Sref{sec:logic}).
-$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
-Furthermore, since $\Sigma$ is locally contractive, so is $\textdom{ResF}$.
-
-Now we can write down the recursive domain equation:
-\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
-$\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor.
-This fixed-point exists and is unique by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
-We do not need to consider how the object is constructed. 
-We only need the isomorphism, given by
-\begin{align*}
-  \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
-  \iProp &\eqdef \UPred(\Res) \\
-	\wIso &: \iProp \nfn \iPreProp \\
-	\wIso^{-1} &: \iPreProp \nfn \iProp
-\end{align*}
 
-We then pick $\iProp$ as the interpretation of $\Prop$:
-\[ \Sem{\Prop} \eqdef \iProp \]
 
 
 \paragraph{Interpretation of assertions.}