Newer
Older
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}.
An \emph{ordered family of equivalences} (OFE) is a tuple $(\ofe, ({\nequiv{n}} \subseteq \ofe \times \ofe)_{n \in \nat})$ satisfying
\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 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}).
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'$
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) \]
\[ \All n, x \in \ofe, y \in \ofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
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 category $\OFEs$ consists of OFEs as objects, and non-expansive functions as arrows.
Note that $\OFEs$ is bicartesian closed, \ie it has all sums, products and exponentials as well as an initial and a terminal object.
In particular:
Given two OFEs $\ofe$ and $\ofeB$, the set of non-expansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with
f \nequiv{n} g \eqdef{}& \All x \in \ofe. f(x) \nequiv{n} g(x)
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.
One very important OFE is the OFE of \emph{step-indexed propositions}:
For every step-index, such a proposition either holds or does not hold.
Moreover, if a propositions holds for some $n$, it also has to hold for all smaller step-indices.
\begin{align*}
\SProp \eqdef{}& \psetdown{\nat} \\
\eqdef{}& \setComp{X \in \pset{\nat}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\
X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y \\
X \nincl{n} Y \eqdef{}& \All m \leq n. m \in X \Ra m \in Y
\end{align*}
\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).
$\SProp$ as defined above is complete, \ie it is a COFE.
Completeness is necessary to take fixed-points.
\begin{thm}[Banach's fixed-point]
\label{thm:banach}
Given an inhabited COFE $\ofe$ and a contractive function $f : \ofe \to \ofe$, there exists a unique fixed-point $\fixp_T f$ such that $f(\fixp_T f) = \fixp_T f$.
Ralf Jung
committed
Moreover, this theorem also holds if $f$ is just non-expansive, and $f^k$ is contractive for an arbitrary $k$.
\end{thm}
\begin{thm}[America and Rutten~\cite{America-Rutten:JCSS89,birkedal:metric-space}]
\label{thm:america_rutten}
Let $1$ be the discrete COFE on the unit type: $1 \eqdef \Delta \{ () \}$.
Given a locally contractive bifunctor $G : \COFEs^{\textrm{op}} \times \COFEs \to \COFEs$, and provided that \(G(1, 1)\) is inhabited,
then there exists a unique\footnote{Uniqueness is not proven in Coq.} COFE $\ofe$ such that $G(\ofe^{\textrm{op}}, \ofe) \cong \ofe$ (\ie the two are isomorphic in $\COFEs$).
\end{thm}
\subsection{RA}
\begin{defn}
A \emph{resource algebra} (RA) is a tuple \\
$(\monoid, \mvalFull : \monoid \to \mProp, \mcore{{-}}:
\monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:
\begin{align*}
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{ra-assoc} \\
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{ra-comm} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\
\All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\
\All \melt, \meltB.& \mvalFull(\melt \mtimes \meltB) \Ra \mvalFull(\melt) \tagH{ra-valid-op} \\
\maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\
\melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
Here, $\mProp$ is the set of (meta-level) propositions.
Think of \texttt{Prop} in Coq or $\mathbb{B}$ in classical mathematics.
RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences:
\begin{enumerate}
\item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).
These valid elements are identified by the \emph{validity predicate} $\mvalFull$.
This take on partiality is necessary when defining the structure of \emph{higher-order} ghost state, \emph{cameras}, in the next subsection.
\item Instead of a single unit that is an identity to every element, we allow
for an arbitrary number of units, via a function $\mcore{{-}}$ assigning to an element $\melt$ its \emph{(duplicable) core} $\mcore\melt$, as demanded by \ruleref{ra-core-id}.
We further demand that $\mcore{{-}}$ is idempotent (\ruleref{ra-core-idem}) and monotone (\ruleref{ra-core-mono}) with respect to the \emph{extension order}, defined similarly to that for PCMs (\ruleref{ra-incl}).
Notice that the domain of the core is $\maybe\monoid$, a set that adds a dummy element $\mnocore$ to $\monoid$.
% (This corresponds to the option type.)
Thus, the core can be \emph{partial}: not all elements need to have a unit.
We use the metavariable $\maybe\melt$ to indicate elements of $\maybe\monoid$.
We also lift the composition $(\mtimes)$ to $\maybe\monoid$.
Partial cores help us to build interesting composite RAs from smaller primitives.
Notice also that the core of an RA is a strict generalization of the unit that any PCM must provide, since $\mcore{{-}}$ can always be picked as a constant function.
\begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
\[ \All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \mvalFull(\maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \mvalFull(\maybe{\melt_\f}) \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
The proposition $\melt \mupd \meltsB$ says that every element $\maybe{\melt_\f}$ compatible with $\melt$ (we also call such elements \emph{frames}), must also be compatible with some $\meltB \in \meltsB$.
Notice that $\maybe{\melt_\f}$ could be $\mnocore$, so the frame-preserving update can also be applied to elements that have \emph{no} frame.
Intuitively, this means that whatever assumptions the rest of the program is making about the state of $\gname$, if these assumptions are compatible with $\melt$, then updating to $\meltB$ will not invalidate any of these assumptions.
Since Iris ensures that the global ghost state is valid, this means that we can soundly update the ghost state from $\melt$ to a non-deterministically picked $\meltB \in \meltsB$.
\subsection{Cameras}
A \emph{camera} is a tuple $(\monoid : \OFEs, \mval : \monoid \nfn \SProp, \mcore{{-}}: \monoid \nfn \maybe\monoid,\\ (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{camera-assoc} \\
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{camera-comm} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{camera-core-id} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{camera-core-idem} \\
\All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{camera-core-mono} \\
\All \melt, \meltB.& \mval(\melt \mtimes \meltB) \subseteq \mval(\melt) \tagH{camera-valid-op} \\
\All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$n \in \mval(\melt) \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\
&\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{camera-extend} \\
\text{where}\qquad\qquad\\
\melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{camera-incl} \\
\melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{camera-inclN}
\end{align*}
\end{defn}
This is a natural generalization of RAs over OFEs\footnote{The reader may wonder why on earth we call them ``cameras''.
The reason, which may not be entirely convincing, is that ``camera'' was originally just used as a comfortable pronunciation of ``CMRA'', the name used in earlier Iris papers.
CMRA was originally supposed to be an acronym for ``complete metric resource algebras'' (or something like that), but we were never very satisfied with it and thus ended up never spelling it out.
To make matters worse, the ``complete'' part of CMRA is now downright misleading, for whereas previously the carrier of a CMRA was required to be a COFE (complete OFE), we have relaxed that restriction and permit it to be an (incomplete) OFE.
For these reasons, we have decided to stick with the name ``camera'', for purposes of continuity, but to drop any pretense that it stands for something.}.
All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
We define the plain $\mvalFull$ as the ``limit'' of the step-indexed approximation:
\[ \mvalFull(\melt) \eqdef \All n. n \in \mval(\melt) \]
\paragraph{The extension axiom (\ruleref{camera-extend}).}
Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq.
The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the following square:
% RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so
\begin{center}
\begin{tikzpicture}[every edge/.style={draw=none}]
\node (a) at (0, 0) {$\melt$};
\node (b) at (1.7, 0) {$\meltB$};
\node (b12) at (1.7, -1) {$\meltB_1 \mtimes \meltB_2$};
\node (a12) at (0, -1) {$\melt_1 \mtimes \melt_2$};
\path (a) edge node {$\nequiv{n}$} (b);
\path (a12) edge node {$\nequiv{n}$} (b12);
\path (a) edge node [rotate=90] {$=$} (a12);
\path (b) edge node [rotate=90] {$=$} (b12);
\end{tikzpicture}\end{center}
where the $n$-equivalence at the bottom is meant to apply to the pairs of elements, \ie we demand $\melt_1 \nequiv{n} \meltB_1$ and $\melt_2 \nequiv{n} \meltB_2$.
In other words, extension carries the decomposition of $\meltB$ into $\meltB_1$ and $\meltB_2$ over the $n$-equivalence of $\melt$ and $\meltB$, and yields a corresponding decomposition of $\melt$ into $\melt_1$ and $\melt_2$.
This operation is needed to prove that $\later$ commutes with separating conjunction:
\axiom{\later (\prop * \propB) \Lra \later\prop * \later\propB}
\begin{defn}
An element $\munit$ of a camera $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:
\begin{enumerate}[itemsep=0pt]
\item $\munit$ is valid: \\ $\All n. n \in \mval(\munit)$
$\All \melt \in M. \munit \mtimes \melt = \melt$
\item $\munit$ is its own core: \\ $\mcore\munit = \munit$
\end{enumerate}
\end{defn}
\begin{lem}\label{lem:camera-unit-total-core}
If $\monoid$ has a unit $\munit$, then the core $\mcore{{-}}$ is total, \ie $\All\melt. \mcore\melt \in \monoid$.
\end{lem}
\begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
\[ \All n, \maybe{\melt_\f}. n \in \mval(\melt \mtimes \maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. n \in\mval(\meltB \mtimes \maybe{\melt_\f}) \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
Note that for RAs, this and the RA-based definition of a frame-preserving update coincide.
A camera $\monoid$ is \emph{discrete} if it satisfies the following conditions:
\begin{enumerate}[itemsep=0pt]
\item $\monoid$ is a discrete COFE
$\All \melt \in \monoid. 0 \in \mval(\melt) \Ra \All n. n \in \mval(\melt)$
Note that every RA is a discrete camera, by picking the discrete COFE for the equivalence relation.
Furthermore, discrete cameras can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$.
\begin{defn}[Camera homomorphism]
A function $f : \monoid_1 \to \monoid_2$ between two cameras is \emph{a camera homomorphism} if it satisfies the following conditions:
\begin{enumerate}[itemsep=0pt]
\item $f$ commutes with composition:\\
$\All \melt_1 \in \monoid_1, \melt_2 \in \monoid_1. f(\melt_1) \mtimes f(\melt_2) = f(\melt_1 \mtimes \melt_2)$
\item $f$ commutes with the core:\\
$\All \melt \in \monoid_1. \mcore{f(\melt)} = f(\mcore{\melt})$
$\All n, \melt \in \monoid_1. n \in \mval(\melt) \Ra n \in \mval(f(\melt))$
\end{enumerate}
\end{defn}
\begin{defn}
The category $\CMRAs$ consists of cameras as objects, and monotone functions as arrows.
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.