diff --git a/docs/algebra.tex b/docs/algebra.tex
index e9d12d74c8375b3796592523a3d54326a33cf58e..b5050387cb9299a45f6fa1066d4e3a39e90402c3 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -1,65 +1,82 @@
\section{Algebraic Structures}
-\subsection{COFE}
+\subsection{OFE}
-The model of Iris lives in the category of \emph{Complete Ordered Families of Equivalences} (COFEs).
+The model of Iris lives in the category of \emph{Ordered Families of Equivalences} (OFEs).
This definition varies slightly from the original one in~\cite{catlogic}.
-\begin{defn}[Chain]
- Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
-\end{defn}
-
\begin{defn}
- A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe, ({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}, \lim : \chain(\cofe) \to \cofe)$ satisfying
+ An \emph{ordered family of equivalences} (OFE) is a tuple $(\ofe, ({\nequiv{n}} \subseteq \ofe \times \ofe)_{n \in \nat})$ satisfying
\begin{align*}
- \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\
- \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\
- \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\
- \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
+ \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{ofe-equiv} \\
+ \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{ofe-mono} \\
+ \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{ofe-limit}
\end{align*}
\end{defn}
-The key intuition behind COFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
-In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{cofe-mono})---and in the limit, it agrees with plain equality (\ruleref{cofe-limit}).
-In order to solve the recursive domain equation in \Sref{sec:model} it is also essential that COFEs are \emph{complete}, \ie that any chain has a limit (\ruleref{cofe-compl}).
+The key intuition behind OFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
+In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{ofe-mono})---and in the limit, it agrees with plain equality (\ruleref{ofe-limit}).
\begin{defn}
- An element $x \in \cofe$ of a COFE is called \emph{discrete} if
- \[ \All y \in \cofe. x \nequiv{0} y \Ra x = y\]
- A COFE $A$ is called \emph{discrete} if all its elements are discrete.
- For a set $X$, we write $\Delta X$ for the discrete COFE with $x \nequiv{n} x' \eqdef x = x'$
-
+ An element $x \in \ofe$ of an OFE is called \emph{discrete} if
+ \[ \All y \in \ofe. x \nequiv{0} y \Ra x = y\]
+ An OFE $A$ is called \emph{discrete} if all its elements are discrete.
+ For a set $X$, we write $\Delta X$ for the discrete OFE with $x \nequiv{n} x' \eqdef x = x'$
\end{defn}
\begin{defn}
- A function $f : \cofe \to \cofeB$ between two COFEs is \emph{non-expansive} (written $f : \cofe \nfn \cofeB$) if
- \[\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
+ A function $f : \ofe \to \ofeB$ between two OFEs is \emph{non-expansive} (written $f : \ofe \nfn \ofeB$) if
+ \[\All n, x \in \ofe, y \in \ofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
It is \emph{contractive} if
- \[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
+ \[ \All n, x \in \ofe, y \in \ofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
\end{defn}
Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data.
Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$.
-The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
\begin{defn}
- The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
+ The category $\OFEs$ consists of OFEs as objects, and non-expansive functions as arrows.
\end{defn}
-Note that $\COFEs$ is cartesian closed. In particular:
+Note that $\OFEs$ is cartesian closed. In particular:
\begin{defn}
- Given two COFEs $\cofe$ and $\cofeB$, the set of non-expansive functions $\set{f : \cofe \nfn \cofeB}$ is itself a COFE with
+ Given two OFEs $\ofe$ and $\ofeB$, the set of non-expansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with
\begin{align*}
- f \nequiv{n} g \eqdef{}& \All x \in \cofe. f(x) \nequiv{n} g(x)
+ f \nequiv{n} g \eqdef{}& \All x \in \ofe. f(x) \nequiv{n} g(x)
\end{align*}
\end{defn}
\begin{defn}
- A (bi)functor $F : \COFEs \to \COFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.
+ A (bi)functor $F : \OFEs \to \OFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.
Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
\end{defn}
The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.
Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.
-The reason contractive (bi)functors are interesting is that by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, they have a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
+
+\subsection{COFE}
+
+COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary chains.
+
+\begin{defn}[Chain]
+ Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
+\end{defn}
+
+\begin{defn}
+ A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe : \OFEs, \lim : \chain(\cofe) \to \cofe)$ satisfying
+ \begin{align*}
+ \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
+ \end{align*}
+\end{defn}
+
+\begin{defn}
+ The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
+\end{defn}
+
+The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the domain $\ofe$ can actually be just an OFE).
+
+Completeness is necessary to take fixed-points.
+For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$ is a COFE and inhabited has a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
+Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
+
\subsection{RA}
@@ -115,7 +132,7 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\subsection{CMRA}
\begin{defn}
- A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \nat},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
+ A \emph{CMRA} is a tuple $(\monoid : \OFEs, (\mval_n \subseteq \monoid)_{n \in \nat},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
\begin{align*}
\All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
\All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmra-valid-mono} \\
@@ -133,7 +150,7 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\end{align*}
\end{defn}
-This is a natural generalization of RAs over COFEs.
+This is a natural generalization of RAs over OFEs.
All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
We define the plain $\mval$ as the ``limit'' of the $\mval_n$:
\[ \mval \eqdef \bigcap_{n \in \nat} \mval_n \]
@@ -209,7 +226,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\begin{defn}
The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows.
\end{defn}
-Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
+Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\OFEs$.
The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
%TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 28205478fc37ac687206bcda2592aa6cc0922e02..eb72d0c87c0467463e528f9d9580d2ac79280a50 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -1,20 +1,20 @@
-\section{COFE constructions}
+\section{OFE and COFE constructions}
\subsection{Trivial pointwise lifting}
-The COFE structure on many types can be easily obtained by pointwise lifting of the structure of the components.
+The (C)OFE structure on many types can be easily obtained by pointwise lifting of the structure of the components.
This is what we do for option $\maybe\cofe$, product $(M_i)_{i \in I}$ (with $I$ some finite index set), sum $\cofe + \cofe'$ and finite partial functions $K \fpfn \monoid$ (with $K$ infinite countable).
\subsection{Next (type-level later)}
-Given a COFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
+Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
\begin{align*}
\latert\cofe \eqdef{}& \latertinj(x:\cofe) \\
\latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
\end{align*}
Note that in the definition of the carrier $\latert\cofe$, $\latertinj$ is a constructor (like the constructors in Coq), \ie this is short for $\setComp{\latertinj(x)}{x \in \cofe}$.
-$\latert(-)$ is a locally \emph{contractive} functor from $\COFEs$ to $\COFEs$.
+$\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
\subsection{Uniform Predicates}
@@ -117,7 +117,7 @@ Notice that this core is total, as the result always lies in $\maybe\monoid$ (ra
\subsection{Finite partial function}
\label{sec:fpfnm}
-Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a COFE and CMRA structure by lifting everything pointwise.
+Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a CMRA structure by lifting everything pointwise.
We obtain the following frame-preserving updates:
\begin{mathpar}
@@ -139,7 +139,7 @@ $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
-Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
+Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
\begin{align*}
\agm(\cofe) \eqdef{}& \set{(c, V) \in (\nat \to \cofe) \times \SProp}/\ {\sim} \\[-0.2em]
\textnormal{where }& \melt \sim \meltB \eqdef{} \melt.V = \meltB.V \land
@@ -152,7 +152,7 @@ Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\end{align*}
%Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
-$\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
+$\agm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in V$ steps.
The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
@@ -175,7 +175,7 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
\subsection{Exclusive CMRA}
-Given a COFE $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
+Given an OFE $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
\begin{align*}
\exm(\cofe) \eqdef{}& \exinj(\cofe) \mid \mundef \\
\mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \mundef}
@@ -193,7 +193,7 @@ The step-indexed equivalence is inductively defined as follows:
\axiom{\mundef \nequiv{n} \mundef}
\end{mathpar}
-$\exm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
+$\exm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
We obtain the following frame-preserving update:
\begin{mathpar}
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 95fa8e378dee01645b6518ea1cf922359dda7dec..19084064abdf675943c6751e3c6e11582cd07c2b 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -51,7 +51,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
-\[ \diamond \prop \eqdef \later\FALSE \lor \Prop \]
+\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]
This modality is useful because there is a class of assertions which we call \emph{timeless} assertions, for which we have
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
@@ -122,11 +122,11 @@ The following rules identify the class of timeless assertions:
\axiom{\timeless{\FALSE}}
\infer
-{\text{$\term$ or $\term'$ is a discrete COFE element}}
+{\text{$\term$ or $\term'$ is a discrete OFE element}}
{\timeless{\term =_\type \term'}}
\infer
-{\text{$\melt$ is a discrete COFE element}}
+{\text{$\melt$ is a discrete OFE element}}
{\timeless{\ownM\melt}}
\infer
diff --git a/docs/iris.sty b/docs/iris.sty
index 9c5becfcd1dc6689cea6fbef6ad2e94f82506d70..51d4ebae4e1a740268817d74a126f72cd2ed5211 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -146,8 +146,11 @@
% List
\newcommand{\List}{\ensuremath{\textdom{List}}}
-\newcommand{\cofe}{T}
-\newcommand{\cofeB}{U}
+\newcommand{\ofe}{T}
+\newcommand{\ofeB}{U}
+\newcommand{\cofe}{\ofe}
+\newcommand{\cofeB}{\ofeB}
+\newcommand{\OFEs}{\mathcal{OFE}} % category of OFEs
\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs
\newcommand{\iFunc}{\Sigma}
\newcommand{\fix}{\textdom{fix}}
diff --git a/docs/model.tex b/docs/model.tex
index fcb9d7272614f9f1981ca557a0f20394ca01f16a..f91d3d37e333c6ee9eb3cf303cc458c6cae20ae3 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -18,7 +18,7 @@ The semantic domains are interpreted as follows:
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]
-For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\COFEs$ and define
+For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\OFEs$ and define
\[
\Sem{\type} \eqdef X_\type
\]
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 0f3be2919805db98545ae6ff71eb6a6e07deb1fc..1d33f1f1a5e3877214fb224e7456f766c736cb63 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -22,16 +22,16 @@ The purpose of this section is to describe how we solve these issues.
\paragraph{Picking the resources.}
The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
-To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
+To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.
(This is in contrast to the base logic, where the user picks a single, fixed CMRA that has a unit.)
From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
\mathcal G \eqdef{}& \nat \\
- \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\cofe^\op, \cofe)
+ \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\ofe^\op, \ofe)
\end{align*}
We will motivate both the use of a product and the finite partial function below.
-$\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).
+$\textdom{ResF}(\ofe^\op, \ofe)$ 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:
@@ -93,7 +93,7 @@ We can show the following properties for this form of ownership:
{\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}
\inferH{res-timeless}
- {\text{$\melt$ is a discrete COFE element}}
+ {\text{$\melt$ is a discrete OFE element}}
{\timeless{\ownGhost\gname{\melt : M_i}}}
\end{mathparpagebreakable}
@@ -121,8 +121,7 @@ We assume to have the following four CMRAs available:
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine.
-Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created.
-(We will discuss later how this assumption is discharged.)
+We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created, such that these names are globally known.
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
@@ -187,7 +186,7 @@ Fancy updates satisfy the following basic proof rules:
% \inferH{fup-closeI}
% {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
\end{mathparpagebreakable}
-(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:invariants}.)
+(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.)
We can further define the notions of \emph{view shifts} and \emph{linear view shifts}:
\begin{align*}