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.
...
...
@@ -84,7 +94,7 @@ Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkeda
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.
...
...
@@ -122,7 +135,7 @@ 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}
...
...
@@ -134,17 +147,15 @@ 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 : \OFEs, (\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 : \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}\\
\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}.
$\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.
\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
\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}.
You can think of uniform predicates as monotone, step-indexed predicates over a CMRA that ``ignore'' invalid elements (as defined by the quotient).
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.
$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
\clearpage
\section{RA and CMRA constructions}
...
...
@@ -69,16 +52,16 @@ Frame-preserving updates on the $M_i$ lift to the product:
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 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.
...
...
@@ -99,7 +82,7 @@ We obtain the following frame-preserving updates, as well as their symmetric cou
@@ -295,7 +278,7 @@ The frame-preserving update involves the notion of a \emph{local update}:
\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
\begin{defn}
It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1)\lupd(\melt_2, \meltB_2)$, if
\[\All n, \maybe{\melt_\f}. \melt_1\in\mval_n\land\melt_1\nequiv{n}\meltB_1\mtimes\maybe{\melt_\f}\Ra\melt_2\in\mval_n\land\melt_2\nequiv{n}\meltB_2\mtimes\maybe{\melt_\f}\]
\[\All n, \maybe{\melt_\f}. n\in\mval(\melt_1)\land\melt_1\nequiv{n}\meltB_1\mtimes\maybe{\melt_\f}\Ran\in\mval(\melt_2)\land\melt_2\nequiv{n}\meltB_2\mtimes\maybe{\melt_\f}\]
\end{defn}
In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.
...
...
@@ -327,7 +310,7 @@ We further define \emph{closed} sets of states (given a particular set of tokens
\All m, \melt'. & m \leq n \land (\melt\mtimes\melt') \in\mval_m \Ra{}\\&\Exists\meltB. (\meltB\mtimes\melt') \in\mval_m \land m \in\Sem{\vctx\proves\prop :\Prop}_\gamma(\meltB)
\All m, \melt'. & m \leq n \landm \in\mval(\melt\mtimes\melt') \Ra{}\\&\Exists\meltB. m \in\mval(\meltB\mtimes\melt') \land m \in\Sem{\vctx\proves\prop :\Prop}_\gamma(\meltB)
