diff --git a/docs/algebra.tex b/docs/algebra.tex
index dc8bdead2a4ecf03b35cda890b1889420fca2241..528f307f6774a84a638e65aea0c433ac4a3522d3 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -126,7 +126,7 @@ RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two k
\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}.
@@ -154,22 +154,22 @@ Notice that $\maybe{\melt_\f}$ could be $\mnocore$, so the frame-preserving upda
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 : \monoid \nfn \SProp, \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 \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\
- \All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\
- \All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
- \All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-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{cmra-core-mono} \\
- \All \melt, \meltB.& \mval(\melt \mtimes \meltB) \subseteq \mval(\melt) \tagH{cmra-valid-op} \\
+ \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{cmra-extend} \\
+ &\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{cmra-incl} \\
- \melt \mincl[n] \meltB \eqdef{}& \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclN}
+ \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}
@@ -178,7 +178,7 @@ All operations have to be non-expansive, and the validity predicate $\mval$ can
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{cmra-extend}).}
+\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:
@@ -203,7 +203,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\end{mathpar}
\begin{defn}
- An element $\munit$ of a CMRA $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:
+ 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)$
\item $\munit$ is a left-identity of the operation: \\
@@ -212,7 +212,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\end{enumerate}
\end{defn}
-\begin{lem}\label{lem:cmra-unit-total-core}
+\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}
@@ -225,18 +225,18 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
Note that for RAs, this and the RA-based definition of a frame-preserving update coincide.
\begin{defn}
- A CMRA $\monoid$ is \emph{discrete} if it satisfies the following conditions:
+ A camera $\monoid$ is \emph{discrete} if it satisfies the following conditions:
\begin{enumerate}[itemsep=0pt]
\item $\monoid$ is a discrete COFE
\item $\mval$ ignores the step-index: \\
$\All \melt \in \monoid. 0 \in \mval(\melt) \Ra \All n. n \in \mval(\melt)$
\end{enumerate}
\end{defn}
-Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation.
-Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$.
+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}[CMRA homomorphism]
- A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{a CMRA homomorphism} if it satisfies the following conditions:
+\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$ is non-expansive
\item $f$ commutes with composition:\\
@@ -249,7 +249,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\end{defn}
\begin{defn}
- The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows.
+ The category $\CMRAs$ consists of cameras as objects, and monotone functions as arrows.
\end{defn}
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.
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 5907de36b49d31e65dfd38b5599f27a0b0fc4978..72cda315e722d7a311d884dba8e8eff44471c9c8 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -1,8 +1,8 @@
\section{Base Logic}
\label{sec:base-logic}
-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}}
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 60315f69d038f7f5db84c823626ee4c583b2e97f..bfa2c1ffa6c3a175ac4a47e848d7e5b6c9275cd1 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -19,7 +19,7 @@ $\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:
\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)} \\
@@ -27,7 +27,7 @@ Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform pr
\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 CMRA that ``ignore'' invalid elements (as defined by the quotient).
+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$.
@@ -51,12 +51,12 @@ connective.
\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}
@@ -68,7 +68,7 @@ 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):
\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 \\
@@ -82,7 +82,7 @@ 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 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}
@@ -104,12 +104,12 @@ We obtain the following frame-preserving updates, as well as their symmetric cou
{\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 CMRA is on if $\mval$ has \emph{no possible frame}.
+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 (CM)RA axioms already lifted the composition operation on $\monoid$ to one on $\maybe\monoid$.
-We can easily extend this to a full CMRA by defining a suitable core, namely
+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$}
@@ -119,7 +119,7 @@ Notice that this core is total, as the result always lies in $\maybe\monoid$ (ra
\subsection{Finite Partial Functions}
\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 CMRA structure by lifting everything pointwise.
+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}
@@ -141,7 +141,7 @@ $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
-Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
+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) \\
@@ -168,9 +168,9 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
\end{mathpar}
-\subsection{Exclusive CMRA}
+\subsection{Exclusive Camera}
-Given an OFE $\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 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 \neq \mundef}
@@ -276,9 +276,9 @@ We obtain the following frame-preserving update:
\subsection{Authoritative}
-\label{sec:auth-cmra}
+\label{sec:auth-camera}
-Given a CMRA $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$.
+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*}
@@ -309,7 +309,7 @@ We then obtain
\end{mathpar}
\subsection{STS with Tokens}
-\label{sec:sts-cmra}
+\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.
diff --git a/docs/derived.tex b/docs/derived.tex
index aca9dbc2cfca81383db90d0e36dc5e9c7e6002f7..cbbdd51d5669d9170a27ed5cad403782972cdaae 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -109,7 +109,7 @@ This is essentially an \emph{optional later}, indicating that the lemmas can be
\newcommand\SliceInv{\textlog{SliceInv}}
The above rules are validated by the following model.
-We need a CMRA as follows:
+We need a camera as follows:
\begin{align*}
\BoxState \eqdef{}& \BoxFull + \BoxEmp \\
\BoxM \eqdef{}& \authm(\maybe{\exm(\BoxState)}) \times \maybe{\agm(\latert \iProp)}
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 103dcfb3d7ce4575ed1630aac902c227bbe2aa16..b4edcf9c843cbe0ae9283870a574019c4d5cab76 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -135,7 +135,7 @@ The following rules identify the class of timeless assertions:
{\timeless{\ownM\melt}}
\infer
-{\text{$\melt$ is an element of a discrete CMRA}}
+{\text{$\melt$ is an element of a discrete camera}}
{\timeless{\mval(\melt)}}
\end{mathparpagebreakable}
diff --git a/docs/iris.sty b/docs/iris.sty
index 16c893eaaa742dbd3442e0314d944f59827b0a9b..c00061382801b8e3c9167d295e2d59af4bd5ba43 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -155,8 +155,8 @@
\newcommand{\ofeB}{U}
\newcommand{\cofe}{\ofe}
\newcommand{\cofeB}{\ofeB}
-\newcommand{\OFEs}{\mathcal{OFE}} % category of OFEs
-\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs
+\newcommand{\OFEs}{\mathbf{OFE}} % category of OFEs
+\newcommand{\COFEs}{\mathbf{COFE}} % category of COFEs
\newcommand{\iFunc}{\Sigma}
\newcommand{\fix}{\textdom{fix}}
@@ -195,7 +195,7 @@
$\preccurlyeq$\cr
}}}}}
-\newcommand{\CMRAs}{\mathcal{CMRA}} % category of CMRAs
+\newcommand{\CMRAs}{\mathbf{Camera}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
diff --git a/docs/model.tex b/docs/model.tex
index e855482dc9d1dfd4def067f03ebf961a3c220fcb..d14d392b437b67814a2dcf279821b4b0aa9a00eb 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -29,7 +29,7 @@ For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \
\judgment[Interpretation of assertions.]{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \UPred(\monoid)}
Remember that $\UPred(\monoid)$ is isomorphic to $\monoid \monra \SProp$.
-We are thus going to define the assertions as mapping CMRA elements to sets of step-indices.
+We are thus going to define the assertions as mapping camera elements to sets of step-indices.
\begin{align*}
\Sem{\vctx \proves t =_\type u : \Prop}_\venv &\eqdef
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 06a9f74959f9bad0bc14ead5414f9418e9a1c152..84cc7dd678af1544322461c87398182431762341 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -8,13 +8,13 @@ So in the following, we assume that some language $\Lang$ was fixed.
\subsection{Dynamic Composeable Higher-Order Resources}
\label{sec:composeable-resources}
-The base logic described in \Sref{sec:base-logic} works over an arbitrary CMRA $\monoid$ defining the structure of the resources.
-It turns out that we can generalize this further and permit picking CMRAs ``$\iFunc(\Prop)$'' that depend on the structure of assertions themselves.
+The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources.
+It turns out that we can generalize this further and permit picking cameras ``$\iFunc(\Prop)$'' that depend on the structure of assertions themselves.
Of course, $\Prop$ is just the syntactic type of assertions; for this to make sense we have to look at the semantics.
-Furthermore, there is a composability problem with the given logic: if we have one proof performed with CMRA $\monoid_1$, and another proof carried out with a \emph{different} CMRA $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.
+Furthermore, there is a composability problem with the given logic: if we have one proof performed with camera $\monoid_1$, and another proof carried out with a \emph{different} camera $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.
-Finally, in many cases just having a single ``instance'' of a CMRA available for reasoning is not enough.
+Finally, in many cases just having a single ``instance'' of a camera available for reasoning is not enough.
For example, when reasoning about a dynamically allocated data structure, every time a new instance of that data structure is created, we will want a fresh resource governing the state of this particular instance.
While it would be possible to handle this problem whenever it comes up, it turns out to be useful to provide a general solution.
@@ -23,7 +23,7 @@ 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 : \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.)
+(This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.)
From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
@@ -31,7 +31,7 @@ From this, we construct the bifunctor defining the overall resources as follows:
\textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \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}(\ofe^\op, \ofe)$ 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 camera by lifting the individual cameras 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:
@@ -47,13 +47,13 @@ We do not need to consider how the object $\iPreProp$ is constructed, we only ne
Notice that $\iProp$ is the semantic model of assertions for the base logic described in \Sref{sec:base-logic} with $\Res$:
\[ \Sem{\Prop} \eqdef \iProp = \UPred(\Res) \]
-Effectively, we just defined a way to instantiate the base logic with $\Res$ as the CMRA of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.
+Effectively, we just defined a way to instantiate the base logic with $\Res$ as the camera of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.
We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical assertions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.
\paragraph{Proof composability.}
To make our proofs composeable, we \emph{generalize} our proofs over the family of functors.
-This is possible because we made $\Res$ a \emph{product} of all the CMRAs picked by the user, and because we can actually work with that product ``pointwise''.
+This is possible because we made $\Res$ a \emph{product} of all the cameras picked by the user, and because we can actually work with that product ``pointwise''.
So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}.
Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors.
Since the logic is entirely parametric in the choice of functors, there is no trouble reasoning without full knowledge of the family of functors.
@@ -61,7 +61,7 @@ Since the logic is entirely parametric in the choice of functors, there is no tr
Only when the top-level proof is completed we will ``close'' the proof by picking a concrete family that contains exactly those functors the proof needs.
\paragraph{Dynamic resources.}
-Finally, the use of finite partial functions lets us have as many instances of any CMRA as we could wish for:
+Finally, the use of finite partial functions lets us have as many instances of any camera as we could wish for:
Because there can only ever be finitely many instances already allocated, it is always possible to create a fresh instance with any desired (valid) starting state.
This is best demonstrated by giving some proof rules.
@@ -96,7 +96,7 @@ We can show the following properties for this form of ownership:
\end{mathparpagebreakable}
Below, we will always work within (an instance of) the logic as described here.
-Whenever a CMRA is used in a proof, we implicitly assume it to be available in the global family of functors.
+Whenever a camera is used in a proof, we implicitly assume it to be available in the global family of functors.
We will typically leave the $M_i$ implicit when asserting ghost ownership, as the type of $\melt$ will be clear from the context.
@@ -108,7 +108,7 @@ To introduce invariants into our logic, we will define weakest precondition to e
However, in order to be able to access invariants, we will also have to provide a way to \emph{temporarily disable} (or ``open'') them.
To this end, we use tokens that manage which invariants are currently enabled.
-We assume to have the following four CMRAs available:
+We assume to have the following four cameras available:
\begin{align*}
\InvName \eqdef{}& \nat \\
\textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
@@ -117,7 +117,7 @@ We assume to have the following four CMRAs available:
\end{align*}
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
-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.
+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 cameras 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: