docs: update CMRA constructions for partial core

CHANGELOG.md

@@ -12,6 +12,8 @@ This version accompanies the final ICFP paper.
   carry a proof of closedness.  Substitution, closedness and value-ness proofs
   are performed by computation after reflecting into a term langauge that knows
   about values and closed expressions.
+* [program_logic/language] The language does not define its own "atomic"
+  predicate.  Instead, atomicity is defined as reducing in one step to a value.
 
 ## Iris 2.0-rc1
 

docs/algebra.tex

@@ -61,7 +61,6 @@ 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.
 
 \subsection{RA}
-\newcommand\dummymelt\bot
 
 \begin{defn}
   A \emph{resource algebra} (RA) is a tuple \\
@@ -75,7 +74,7 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th
     \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.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\
     \text{where}\qquad %\qquad\\
-    \maybe\monoid \eqdef{}& \monoid \uplus \set{\dummymelt} \qquad\qquad\qquad \melt^? \mtimes \dummymelt \eqdef \dummymelt \mtimes \melt^? \eqdef \melt^? \\
+    \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}
   \end{align*}
 \end{defn}
@@ -90,7 +89,7 @@ This take on partiality is necessary when defining the structure of \emph{higher
 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 $\dummymelt$ to $\monoid$.
+  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$.
@@ -108,7 +107,7 @@ Notice also that the core of an RA is a strict generalization of the unit that a
   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$.
-Notice that $\maybe{\melt_\f}$ could be $\dummymelt$, so the frame-preserving update can also be applied to elements that have \emph{no} frame.
+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$.
 
@@ -173,7 +172,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
   \end{enumerate}
 \end{defn}
 
-\begin{lem}
+\begin{lem}\label{lem:cmra-unit-total-core}
   If $\monoid$ has a unit $\munit$, then the core $\mcore{{-}}$ is total, \ie $\All\melt. \mcore\melt \in \monoid$.
 \end{lem}
 

docs/constructions.tex

@@ -59,6 +59,35 @@ Frame-preserving updates on the $M_i$ lift to the product:
   {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
 \end{mathpar}
 
+\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:
+\begin{align*}
+  \monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \bot \\
+  \mval_n \eqdef{}& \setComp{\cinl(\melt_1)\!}{\!\melt_1 \in \mval'_n}
+    \cup \setComp{\cinr(\melt_2)\!}{\!\melt_2 \in \mval''_n}  \\
+  \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*}
+The composition and core for $\cinr$ are defined symmetrically.
+The remaining cases of the composition and core are all $\bot$.
+Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$.
+
+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, n. \melt \mtimes \melt_\f \notin \mval'_n \and \meltB \in \mval''}
+  {\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}.
+
 \subsection{Finite partial function}
 \label{sec:fpfnm}
 
@@ -118,59 +147,17 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
   \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Ra x \nequiv{n} y}
 \end{mathpar}
 
-\subsection{One-shot}
-
-The purpose of the one-shot CMRA is to lazily initialize the state of a ghost location.
-Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows:
-\begin{align*}
-  \oneshotm(\monoid) \eqdef{}& \ospending + \osshot(\monoid) + \munit + \bot \\
-  \mval_n \eqdef{}& \set{\ospending, \munit} \cup \setComp{\osshot(\melt)}{\melt \in \mval_n}
-\\%\end{align*}
-%\begin{align*}
-  \osshot(\melt) \mtimes \osshot(\meltB) \eqdef{}& \osshot(\melt \mtimes \meltB) \\
-  \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
-  \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt)
-\end{align*}%
-Notice that $\oneshotm(\monoid)$ is a disjoint sum with the four constructors (injections) $\ospending$, $\osshot$, $\munit$ and $\bot$.
-The remaining cases of composition go to $\bot$.
-\begin{align*}
-  \mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\
-  \mcore{\munit} \eqdef{}& \munit &  \mcore{\bot} \eqdef{}& \bot
-\end{align*}
-The step-indexed equivalence is inductively defined as follows:
-\begin{mathpar}
-  \axiom{\ospending \nequiv{n} \ospending}
-
-  \infer{\melt \nequiv{n} \meltB}{\osshot(\melt) \nequiv{n} \osshot(\meltB)}
-
-  \axiom{\munit \nequiv{n} \munit}
-
-  \axiom{\bot \nequiv{n} \bot}
-\end{mathpar}
-$\oneshotm(-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
-
-We obtain the following frame-preserving updates:
-\begin{mathpar}
-  \inferH{oneshot-shoot}
-  {\melt \in \mval}
-  {\ospending \mupd \osshot(\melt)}
-
-  \inferH{oneshot-update}
-  {\melt \mupd \meltsB}
-  {\osshot(\melt) \mupd \setComp{\osshot(\meltB)}{\meltB \in \meltsB}}
-\end{mathpar}
 
 \subsection{Exclusive CMRA}
 
 Given a cofe $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
 \begin{align*}
-  \exm(\cofe) \eqdef{}& \exinj(\cofe) + \munit + \bot \\
-  \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot} \\
-  \munit \mtimes \exinj(x) \eqdef{}& \exinj(x) \mtimes \munit \eqdef \exinj(x)
+  \exm(\cofe) \eqdef{}& \exinj(\cofe) + \bot \\
+  \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot}
 \end{align*}
-The remaining cases of composition go to $\bot$.
+All cases of composition go to $\bot$.
 \begin{align*}
-  \mcore{\exinj(x)} \eqdef{}& \munit & \mcore{\munit} \eqdef{}& \munit &
+  \mcore{\exinj(x)} \eqdef{}& \mnocore &
   \mcore{\bot} \eqdef{}& \bot
 \end{align*}
 The step-indexed equivalence is inductively defined as follows:

docs/iris.sty

@@ -147,6 +147,7 @@
 
 \newcommand{\munit}{\varepsilon}
 \newcommand{\mcore}[1]{{\mid}#1{\mid}} % using "|" here makes LaTeX diverge. WTF.
+\newcommand{\mnocore}\top
 \newcommand{\mtimes}{\mathbin{\cdot}}
 
 \newcommand{\mupd}{\rightsquigarrow}

docs/logic.tex

@@ -10,18 +10,6 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
   A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_\f$ is forked off.
 \item All values are stuck:
 \[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
-\item There is a predicate defining \emph{atomic} expressions satisfying
-\let\oldcr\cr
-\begin{mathpar}
-  {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and
-  {{
-    \begin{inbox}
-\All\expr_1, \state_1, \expr_2, \state_2, \expr_\f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
-    \end{inbox}
-}}
-\end{mathpar}
-In other words, atomic expression \emph{reduce in one step to a value}.
-It does not matter whether they fork off an arbitrary expression.
 \end{itemize}
 
 \begin{defn}
@@ -29,6 +17,11 @@ It does not matter whether they fork off an arbitrary expression.
   \[ \Exists \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \]
 \end{defn}
 
+\begin{defn}
+  An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value:
+  \[ \All\state_1, \expr_2, \state_2, \expr_\f. \expr, \state_1 \step \expr_2, \state_2, \expr_\f \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
+\end{defn}
+
 \begin{defn}[Context]
   A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
   \begin{enumerate}[itemsep=0pt]
@@ -68,8 +61,8 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
 
 To instantiate Iris, you need to define the following parameters:
 \begin{itemize}
-\item A language $\Lang$
-\item A locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit
+\item A language $\Lang$, and
+\item a locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(A)$ is a total function.)
 \end{itemize}
 
 \noindent
@@ -141,7 +134,7 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
 Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
 We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
 If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
-\ralf{$\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.}
+%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
 
 Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
 This is a \emph{meta-level} assertion about propositions, defined as follows: