\section{OFE and COFE Constructions} \subsection{Trivial Pointwise Lifting} 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 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 $\OFEs$ to $\OFEs$. \subsection{Uniform Predicates} Given a camera $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows: \begin{align*} \monoid \monnra \SProp \eqdef{}& \setComp{\pred: \monoid \nfn \SProp} {\All n, \melt, \meltB. \melt \mincl[n] \meltB \Ra \pred(\melt) \nincl{n} \pred(\meltB)} \\ \UPred(\monoid) \eqdef{}& \faktor{\monoid \monnra \SProp}{\equiv} \\ \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*} 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$. 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*} \All n, \melt. (\mval(\melt) \nincl{n} P_0(\melt)) \Ra n \in P_0(\melt) \tagH{UPred-canonical} \end{align*} 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. \clearpage \section{RA and Camera Constructions} \subsection{Product} \label{sec:prodm} 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} \inferH{prod-update} {\melt \mupd_{M_i} \meltsB} {\mapinsert i \melt f \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}} \end{mathpar} \subsection{Sum} \label{sec:summ} 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): \begin{align*} \monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \mundef \\ \mval(\mundef) \eqdef{}& \emptyset \\ \mval(\cinl(\melt)) \eqdef{}& \mval_1(\melt) \\ \cinl(\melt_1) \mtimes \cinl(\meltB_1) \eqdef{}& \cinl(\melt_1 \mtimes \meltB_1) \\ % \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\ % \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) \\ \mcore{\cinl(\melt_1)} \eqdef{}& \begin{cases}\mnocore & \text{if $\mcore{\melt_1} = \mnocore$} \\ \cinl({\mcore{\melt_1}}) & \text{otherwise} \end{cases} \end{align*} 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$. 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} \infer{x \nequiv{n} y}{\cinl(x) \nequiv{n} \cinl(y)} \infer{x \nequiv{n} y}{\cinr(x) \nequiv{n} \cinr(y)} \axiom{\mundef \nequiv{n} \mundef} \end{mathpar} We obtain the following frame-preserving updates, as well as their symmetric counterparts: \begin{mathpar} \inferH{sum-update} {\melt \mupd_{M_1} \meltsB} {\cinl(\melt) \mupd \setComp{ \cinl(\meltB)}{\meltB \in \meltsB}} \inferH{sum-swap} {\All \melt_\f \in M, n. n \notin \mval(\melt \mtimes \melt_\f) \and \mvalFull(\meltB)} {\cinl(\melt) \mupd \cinr(\meltB)} \end{mathpar} Crucially, the second rule allows us to \emph{swap} the side'' of the sum that the camera is on if $\mval$ has \emph{no possible frame}. \subsection{Option} The definition of the camera/RA axioms already lifted the composition operation on $\monoid$ to one on $\maybe\monoid$. We can easily extend this to a full camera by defining a suitable core, namely \begin{align*} \mcore{\mnocore} \eqdef{}& \mnocore & \\ \mcore{\maybe\melt} \eqdef{}& \mcore\melt & \text{If $\maybe\melt \neq \mnocore$} \end{align*} Notice that this core is total, as the result always lies in $\maybe\monoid$ (rather than in $\maybe{\mathord{\maybe\monoid}}$). \subsection{Finite Partial Functions} \label{sec:fpfnm} Given some infinite countable $K$ and some camera $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a camera structure by lifting everything pointwise. We obtain the following frame-preserving updates: \begin{mathpar} \inferH{fpfn-alloc-strong} {\text{$G$ infinite} \and \mvalFull(\melt)} {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in G}} \inferH{fpfn-alloc} {\mvalFull(\melt)} {\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}} \inferH{fpfn-update} {\melt \mupd_\monoid \meltsB} {\mapinsert i \melt f] \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}} \end{mathpar} Above, $\mvalFull$ refers to the (full) validity of $\monoid$. $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$. \subsection{Agreement} Given some OFE $\cofe$, we define the camera $\agm(\cofe)$ as follows: \begin{align*} \agm(\cofe) \eqdef{}& \setComp{\melt \in \finpset\cofe}{\melt \neq \emptyset} /\ {\sim} \-0.2em] \melt \nequiv{n} \meltB \eqdef{}& (\All x \in \melt. \Exists y \in \meltB. x \nequiv{n} y) \land (\All y \in \meltB. \Exists x \in \melt. x \nequiv{n} y) \\ \textnormal{where }& \melt \sim \meltB \eqdef{} \All n. \melt \nequiv{n} \meltB \\ ~\\ % \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\ \mval(\melt) \eqdef{}& \setComp{n}{ \All x, y \in \melt. x \nequiv{n} y } \\ \mcore\melt \eqdef{}& \melt \\ \melt \mtimes \meltB \eqdef{}& \melt \cup \meltB \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 \OFEs to \CMRAs. We define a non-expansive injection \aginj into \agm(\cofe) as follows: \[ \aginj(x) \eqdef \set{x} There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following: \begin{mathpar} \axiomH{ag-val}{\mvalFull(\aginj(x))} \axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)} \axiomH{ag-agree}{n \in \mval(\aginj(x) \mtimes \aginj(y)) \Ra x \nequiv{n} y} \end{mathpar} \subsection{Exclusive Camera} Given an OFE $\cofe$, we define a camera $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned: \begin{align*} \exm(\cofe) \eqdef{}& \exinj(\cofe) \mid \mundef \\ \mval(\melt) \eqdef{}& \setComp{n}{\melt \notnequiv{n} \mundef} \end{align*} All cases of composition go to $\mundef$. \begin{align*} \mcore{\exinj(x)} \eqdef{}& \mnocore & \mcore{\mundef} \eqdef{}& \mundef \end{align*} Remember that $\mnocore$ is the dummy'' element in $\maybe\monoid$ indicating (in this case) that $\exinj(x)$ has no core. The step-indexed equivalence is inductively defined as follows: \begin{mathpar} \infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)} \axiom{\mundef \nequiv{n} \mundef} \end{mathpar} $\exm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$. We obtain the following frame-preserving update: \begin{mathpar} \inferH{ex-update}{} {\exinj(x) \mupd \exinj(y)} \end{mathpar} \subsection{Fractions} We define an RA structure on the rational numbers in $(0, 1]$ as follows: \begin{align*} \fracm \eqdef{}& \fracinj(\mathbb{Q} \cap (0, 1]) \mid \mundef \\ \mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\ \fracinj(q_1) \mtimes \fracinj(q_2) \eqdef{}& \fracinj(q_1 + q_2) \quad \text{if $q_1 + q_2 \leq 1$} \\ \mcore{\fracinj(x)} \eqdef{}& \bot \\ \mcore{\mundef} \eqdef{}& \mundef \end{align*} All remaining cases of composition go to $\mundef$. Frequently, we will write just $x$ instead of $\fracinj(x)$. The most important property of this RA is that $1$ has no frame. This is useful in combination with \ruleref{sum-swap}, and also when used with pairs: \begin{mathpar} \inferH{pair-frac-change}{} {(1, a) \mupd (1, b)} \end{mathpar} %TODO: These need syncing with Coq % \subsection{Finite Powerset Monoid} % Given an infinite set $X$, we define a monoid $\textmon{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows: % $% \melt \cdot \meltB \;\eqdef\; \melt \cup \meltB \quad \mbox{if } \melt \cap \meltB = \emptyset %$ % We obtain: % \begin{mathpar} % \inferH{PowFinUpd}{} % {\emptyset \mupd \{ \{x\} \mid x \in X \}} % \end{mathpar} % \begin{proof}[Proof of \ruleref{PowFinUpd}] % Assume some frame $\melt_\f \sep \emptyset$. Since $\melt_\f$ is finite and $X$ is infinite, there exists an $x \notin \melt_\f$. % Pick that for the result. % \end{proof} % The powerset monoids is cancellative. % \begin{proof}[Proof of cancellativity] % Let $\melt_\f \mtimes \melt = \melt_\f \mtimes \meltB \neq \mzero$. % So we have $\melt_\f \sep \melt$ and $\melt_\f \sep \meltB$, and we have to show $\melt = \meltB$. % Assume $x \in \melt$. Hence $x \in \melt_\f \mtimes \melt$ and thus $x \in \melt_\f \mtimes \meltB$. % By disjointness, $x \notin \melt_\f$ and hence $x \in meltB$. % The other direction works the same way. % \end{proof} \subsection{Authoritative} \label{sec:auth-camera} Given a camera $M$, we construct $\authm(M)$ modeling someone owning an \emph{authoritative} element $\melt$ of $M$, and others potentially owning fragments $\meltB \mincl \melt$ of $\melt$. We assume that $M$ has a unit $\munit$, and hence its core is total. (If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.) \begin{align*} \authm(M) \eqdef{}& \maybe{\exm(M)} \times M \\ \mval( (x, \meltB ) ) \eqdef{}& \setComp{ n }{ (x = \mnocore \land n \in \mval(\meltB)) \lor (\Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt \land n \in \mval(\melt)) } \\ (x_1, \meltB_1) \mtimes (x_2, \meltB_2) \eqdef{}& (x_1 \mtimes x_2, \meltB_2 \mtimes \meltB_2) \\ \mcore{(x, \meltB)} \eqdef{}& (\mnocore, \mcore\meltB) \\ (x_1, \meltB_1) \nequiv{n} (x_2, \meltB_2) \eqdef{}& x_1 \nequiv{n} x_2 \land \meltB_1 \nequiv{n} \meltB_2 \end{align*} Note that $(\mnocore, \munit)$ is the unit and asserts no ownership whatsoever, but $(\exinj(\munit), \munit)$ asserts that the authoritative element is $\munit$. Let $\melt, \meltB \in M$. We write $\authfull \melt$ for full ownership $(\exinj(\melt), \munit)$ and $\authfrag \meltB$ for fragmental ownership $(\mnocore, \meltB)$ and $\authfull \melt , \authfrag \meltB$ for combined ownership $(\exinj(\melt), \meltB)$. 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}. n \in \mval(\melt_1) \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra n \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$. We then obtain \begin{mathpar} \inferH{auth-update} {(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)} {\authfull \melt_1 , \authfrag \meltB_1 \mupd \authfull \melt_2 , \authfrag \meltB_2} \end{mathpar} \subsection{STS with Tokens} \label{sec:sts-camera} Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep} \subseteq \STSS \times \STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS \ra \wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens. The construction follows the idea of STSs as described in CaReSL \cite{caresl}. We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing a \emph{law of token conservation}) and define a stepping relation for the \emph{frame} of a given token set: \begin{align*} (s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\ s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \disj \STSL(s) \cup T \land (s, T_1) \stsstep (s', T_2) \end{align*} We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set: \begin{align*} \STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \disj T \land \left(\All s'. s \stsfstep{T} s' \Ra s' \in S\right) \\ \upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' } \end{align*} The STS RA is defined as follows \begin{align*} \monoid \eqdef{}& \STSauth(s:\STSS, T:\wp(\STST) \mid \STSL(s) \disj T) \mid{}\\& \STSfrag(S: \wp(\STSS), T: \wp(\STST) \mid \STSclsd(S, T) \land S \neq \emptyset) \mid \mundef \\ \mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\ \STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \disj T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\ \STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \disj T'$ and $s \in S$} \\ \mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\ \mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset) \end{align*} The remaining cases are all $\mundef$. We will need the following frame-preserving update: \begin{mathpar} \inferH{sts-step}{(s, T) \ststrans (s', T')} {\STSauth(s, T) \mupd \STSauth(s', T')} \inferH{sts-weaken} {\STSclsd(S_2, T_2) \and S_1 \subseteq S_2 \and T_2 \subseteq T_1} {\STSfrag(S_1, T_1) \mupd \STSfrag(S_2, T_2)} \end{mathpar} \paragraph{The core is not a homomorphism.} The core of the STS construction is only satisfying the RA axioms because we are \emph{not} demanding the core to be a homomorphism---all we demand is for the core to be monotone with respect the \ruleref{ra-incl}. In other words, the following does \emph{not} hold for the STS core as defined above: $\mcore\melt \mtimes \mcore\meltB = \mcore{\melt\mtimes\meltB}$ To see why, consider the following STS: \newcommand\st{\textlog{s}} \newcommand\tok{\textmon{t}} \begin{center} \begin{tikzpicture}[sts] \node at (0,0) (s1) {$\st_1$}; \node at (3,0) (s2) {$\st_2$}; \node at (9,0) (s3) {$\st_3$}; \node at (6,0) (s4) {$\st_4$\\$[\tok_1, \tok_2]$}; \path[sts_arrows] (s2) edge (s4); \path[sts_arrows] (s3) edge (s4); \end{tikzpicture} \end{center} Now consider the following two elements of the STS RA: $\melt \eqdef \STSfrag(\set{\st_1,\st_2}, \set{\tok_1}) \qquad\qquad \meltB \eqdef \STSfrag(\set{\st_1,\st_3}, \set{\tok_2})$ We have: \begin{mathpar} {\melt\mtimes\meltB = \STSfrag(\set{\st_1}, \set{\tok_1, \tok_2})} {\mcore\melt = \STSfrag(\set{\st_1, \st_2, \st_4}, \emptyset)} {\mcore\meltB = \STSfrag(\set{\st_1, \st_3, \st_4}, \emptyset)} {\mcore\melt \mtimes \mcore\meltB = \STSfrag(\set{\st_1, \st_4}, \emptyset) \neq \mcore{\melt \mtimes \meltB} = \STSfrag(\set{\st_1}, \emptyset)} \end{mathpar} %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: