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.
...
...
@@ -73,18 +83,28 @@ COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary
\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.
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))$.
This also holds if $f^k$ is contractive for an arbitrary $k$.
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.
\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$.
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$).
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 $\mval$ of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).
\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, CMRAs, in the next subsection.
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}.
...
...
@@ -122,42 +145,44 @@ Notice also that the core of an RA is a strict generalization of the unit that a
\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
We further define $\melt\mupd\meltB\eqdef\melt\mupd\set\meltB$.
\end{defn}
The assertion $\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$.
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{CMRA}
\subsection{Cameras}
\begin{defn}
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:
A \emph{camera} is a tuple $(\monoid : \OFEs, \mval : \monoid\nfn\SProp,\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}\\
This is a natural generalization of RAs over OFEs.
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 $\mval$ as the ``limit'' of the $\mval_n$:
\[\mval\eqdef\bigcap_{n \in\nat}\mval_n\]
We define the plain $\mvalFull$ as the ``limit'' of the step-indexed approximation:
\[\mvalFull(\melt)\eqdef\All n. n \in\mval(\melt)\]
The base logic is parameterized by an arbitrary CMRA$\monoid$ having a unit $\munit$.
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.
The base logic is parameterized by an arbitrary camera$\monoid$ having a unit $\munit$.
By \lemref{lem:camera-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.
...
...
@@ -193,7 +193,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\infer{\vctx\proves\wtt{\melt}{\textlog{M}}}
{\vctx\proves\wtt{\ownM{\melt}}{\Prop}}
\and
\infer{\vctx\proves\wtt{\melt}{\type}\and\text{$\type$ is a CMRA}}
\infer{\vctx\proves\wtt{\melt}{\type}\and\text{$\type$ is a camera}}
{\vctx\proves\wtt{\mval(\melt)}{\Prop}}
\and
\infer{\vctx\proves\wtt{\prop}{\Prop}}
...
...
@@ -212,13 +212,13 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
}
\end{mathparpagebreakable}
\subsection{Proof rules}
\subsection{Proof Rules}
\label{sec:proof-rules}
The judgment $\vctx\mid\prop\proves\propB$ says that with free variables $\vctx$, proposition $\propB$ holds whenever assumption $\prop$ holds.
Most of the rules will entirely omit the variable contexts $\vctx$.
In this case, we assume the same arbitrary context is used for every constituent of the rules.
%Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
%Furthermore, an arbitrary \emph{boxed} proposition context $\always\pfctx$ may be added to every constituent.
Axioms $\vctx\mid\prop\provesIff\propB$ indicate that both $\vctx\mid\prop\proves\propB$ and $\vctx\mid\propB\proves\prop$ are proof rules of the logic.
\judgment{\vctx\mid\prop\proves\propB}
...
...
@@ -448,7 +448,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlo
{\upd\plainly\prop\proves\prop}
\end{mathpar}
The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
%\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
%\ralf{Trouble is, we do not actually have $\in$ inside the logic...}
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)}
\subsection{Next (Type-Level Later)}
Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
\begin{align*}
...
...
@@ -19,42 +19,44 @@ $\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
\subsection{Uniform Predicates}
Given a CMRA$\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
Given a camera$\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
\pred\equiv\predB\eqdef{}&\All m, \melt. m \in\mval(\melt) \Ra (m \in\pred(\melt) \iff m \in\predB(\melt)) \\
\pred\nequiv{n}\predB\eqdef{}&\All m \le n, \melt. m \in\mval(\melt) \Ra (m \in\pred(\melt) \iff m \in\predB(\melt))
\end{align*}
where $\mProp$ is the set of meta-level propositions, \eg Coq's \texttt{Prop}.
You can think of uniform predicates as monotone, step-indexed predicates over a camera that ``ignore'' invalid elements (as defined by the quotient).
$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
One way to understand this definition is to re-write it a little.
We start by defining the COFE of \emph{step-indexed propositions}: For every step-index, the proposition either holds or does not hold.
It is worth noting that the above quotient admits canonical
representatives. More precisely, one can show that every
equivalence class contains exactly one element $P_0$ such that:
\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
\All n, \melt. (\mval(\melt) \nincl{n} P_0(\melt)) \Ra n \in P_0(\melt) \tagH{UPred-canonical}
\end{align*}
Notice that this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA:
We could equivalently require every CMRA to define $\mval_{-}(-) : \monoid\nfn\SProp$, replacing \ruleref{cmra-valid-ne} and \ruleref{cmra-valid-mono}.
Intuitively, this says that $P_0$ trivially holds whenever the resource is invalid.
Starting from any element $P$, one can find this canonical
representative by choosing $P_0(\melt) :=\setComp{n}{n \in\mval(\melt)\Ra n \in P(\melt)}$.
Hence, as an alternative definition of $\UPred$, we could use the set
of canonical representatives. This alternative definition would
save us from using a quotient. However, the definitions of the various
connectives would get more complicated, because we have to make sure
they all verify \ruleref{UPred-canonical}, which sometimes requires some adjustments. We
would moreover need to prove one more property for every logical
connective.
Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny.
\begin{align*}
\UPred(\monoid) \cong{}&\monoid\monra\SProp\\
\eqdef{}&\setComp{\pred: \monoid\nfn\SProp}{\All n, m, x, y. n \in\pred(x) \land x \mincl y \land m \leq n \land y \in\mval_m \Ra m \in\pred(y)}
\end{align*}
The reason we chose the first definition is that it is easier to work with in Coq.
\clearpage
\section{RA and CMRA constructions}
\section{RA and Camera Constructions}
\subsection{Product}
\label{sec:prodm}
Given a family $(M_i)_{i \in I}$ of CMRAs ($I$ finite), we construct a CMRA for the product $\prod_{i \in I} M_i$ by lifting everything pointwise.
Given a family $(M_i)_{i \in I}$ of cameras ($I$ finite), we construct a camera for the product $\prod_{i \in I} M_i$ by lifting everything pointwise.
Frame-preserving updates on the $M_i$ lift to the product:
\begin{mathpar}
...
...
@@ -66,21 +68,21 @@ Frame-preserving updates on the $M_i$ lift to the product:
\subsection{Sum}
\label{sec:summ}
The \emph{sum CMRA}$\monoid_1\csumm\monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
The \emph{sum camera}$\monoid_1\csumm\monoid_2$ for any cameras $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
The composition and core for $\cinr$ are defined symmetrically.
Above, $\mval_1$ refers to the validity of $\monoid_1$.
The validity, composition and core for $\cinr$ are defined symmetrically.
The remaining cases of the composition and core are all $\mundef$.
Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$.
Notice that we added the artificial ``invalid'' (or ``undefined'') element $\mundef$ to this CMRA just in order to make certain compositions of elements (in this case, $\cinl$ and $\cinr$) invalid.
Notice that we added the artificial ``invalid'' (or ``undefined'') element $\mundef$ to this camera just in order to make certain compositions of elements (in this case, $\cinl$ and $\cinr$) invalid.
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
...
...
@@ -99,54 +101,54 @@ We obtain the following frame-preserving updates, as well as their symmetric cou