docs: global ghost functor

algebra/one_shot.v

@@ -249,6 +249,20 @@ Proof.
   intros Ha n [|b| |] ?; simpl; auto.
   apply cmra_validN_op_l with (core a1), Ha. by rewrite cmra_core_r.
 Qed.
+Lemma one_shot_updateP (P : A → Prop) (Q : one_shot A → Prop) a :
+  a ~~>: P → (∀ b, P b → Q (Shot b)) → Shot a ~~>: Q.
+Proof.
+  intros Hx HP n mf Hm. destruct mf as [|b| |]; try by destruct Hm.
+  - destruct (Hx n b) as (c&?&?); try done.
+    exists (Shot c). auto.
+  - destruct (Hx n (core a)) as (c&?&?); try done.
+    { rewrite cmra_core_r. done. }
+    exists (Shot c). split; first by auto.
+    simpl. by eapply cmra_validN_op_l.
+Qed.
+Lemma one_shot_updateP' (P : A → Prop) a :
+  a ~~>: P → Shot a ~~>: λ m', ∃ b, m' = Shot b ∧ P b.
+Proof. eauto using one_shot_updateP. Qed.
 
 End cmra.
 

docs/algebra.tex

@@ -43,7 +43,7 @@ Note that $\COFEs$ is cartesian closed.
 
 \subsection{RA}
 
-\ralf{Define this, including frame-preserving updates.}
+\ralf{Copy this from the paper, when that one is more polished.}
 
 \subsection{CMRA}
 
@@ -67,6 +67,8 @@ Note that $\COFEs$ is cartesian closed.
 
 This is a natural generalization of RAs over COFEs.
 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 \mathbb{N}} \mval_n \]
 
 \paragraph{The extension axiom (\ruleref{cmra-extend}).}
 Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq.

docs/constructions.tex

@@ -2,6 +2,38 @@
 
 \section{CMRA 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$.
+
+Frame-preserving updates on the $M_i$ lift to the product:
+\begin{mathpar}
+  \inferH{prod-update}
+  {\melt \mupd_{M_i} \meltsB}
+  {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
+\end{mathpar}
+
+\subsection{Finite partial function}
+\label{sec:fpfnm}
+
+Given some countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a COFE and CMRA structure by lifting everything pointwise.
+
+We obtain the following frame-preserving updates:
+\begin{mathpar}
+  \inferH{fpfn-alloc-strong}
+  {\text{$G$ infinite} \and \melt \in \mval}
+  {\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in G}}
+
+  \inferH{fpfn-alloc}
+  {\melt \in \mval}
+  {\emptyset \mupd \set{[\gname \mapsto \melt]}}
+
+  \inferH{fpfn-update}
+  {\melt \mupd \meltsB}
+  {f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
+\end{mathpar}
+
 \subsection{Agreement}
 
 Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
@@ -62,6 +94,16 @@ The step-indexed equivalence is inductively defined as follows:
 \end{mathpar}
 $\oneshotm(-)$ is a locally non-expansive bifunctor 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 monoid}
 
@@ -89,26 +131,6 @@ $\oneshotm(-)$ is a locally non-expansive bifunctor from $\CMRAs$ to $\CMRAs$.
 % If $\melt_f \neq \munit$, then we must have $\melt = \meltB = \munit$, as otherwise one of the two products would be $\mzero$.
 % \end{proof}
 
-% \subsection{Agreement monoid}
-
-% Given a set $X$, we define a monoid such that everybody agrees on which $x \in X$ has been chosen.
-% Let $\agm{X}$ be the monoid with carrier $X \uplus \{ \munit \}$ and multiplication
-% \[
-% \melt \cdot \meltB \;\eqdef\;
-% \begin{cases}
-% \melt & \mbox{if } \meltB = \munit \lor \melt = \meltB \\
-% \meltB & \mbox{if } \melt = \munit
-% \end{cases}
-% \]
-
-% Agreement monoids are cancellative.
-% \begin{proof}[Proof of cancellativity]
-% 	If $\melt_f = \munit$, then the statement is trivial.
-% 	If $\melt_f \neq \munit$, then if $\melt = \munit$, we must have $\meltB = \munit$ and we are done.
-% 	Similar so for $\meltB = \munit$.
-% 	So let $\melt \neq \munit \neq \meltB$ and $\melt_f \mtimes \melt = \melt_f \mtimes \meltB \neq \mzero$.
-% 	It follows immediately that $\melt = \melt_f = \meltB$.
-% \end{proof}
 
 % \subsection{Finite Powerset Monoid}
 
@@ -137,35 +159,6 @@ $\oneshotm(-)$ is a locally non-expansive bifunctor from $\CMRAs$ to $\CMRAs$.
 % 	The other direction works the same way.
 % \end{proof}
 
-% \subsection{Product monoid}
-% \label{sec:prodm}
-
-% Given a family $(M_i)_{i \in I}$ of monoids ($I$ countable), we construct a product monoid.
-% Let $\prod_{i \in I} M_i$ be the monoid with carrier $\prod_{i \in I} \mcarp{M_i}$ and point-wise multiplication, non-zero when \emph{all} individual multiplications are non-zero.
-% For $f \in \prod_{i \in I} \mcarp{M_i}$, we write $f[i \mapsto a]$ for the disjoint union $f \uplus [i \mapsto a]$.
-
-% Frame-preserving updates on the $M_i$ lift to the product:
-% \begin{mathpar}
-%   \inferH{ProdUpd}
-%   {a \mupd_{M_i} B}
-%   {f[i \mapsto a] \mupd \{ f[i \mapsto b] \mid b \in B\}}
-% \end{mathpar}
-% \begin{proof}[Proof of \ruleref{ProdUpd}]
-% Assume some frame $g$ and let $c \eqdef g(i)$.
-% Since $f[i \mapsto a] \sep g$, we get $f \sep g$ and $a \sep_{M_i} c$.
-% Thus there exists $b \in B$ such that $b \sep_{M_i} c$.
-% It suffices to show $f[i \mapsto b] \sep g$.
-% Since multiplication is defined pointwise, this is the case if all components are compatible.
-% For $i$, we know this from $b \sep_{M_i} c$.
-% For all the other components, from $f \sep g$.
-% \end{proof}
-
-% If every $M_i$ is cancellative, then so is $\prod_{i \in I} M_i$.
-% \begin{proof}[Proof of cancellativity]
-% Let $\melt, \meltB, \melt_f \in \prod_{i \in I} \mcarp{M_i}$, and assume $\melt_f \mtimes \melt = \melt_f \mtimes \meltB \neq \mzero$.
-% By the definition of multiplication, this means that for all $i \in I$ we have $\melt_f(i) \mtimes \melt(i) = \melt_f(i) \mtimes \meltB(i) \neq \mzero_{M_i}$.
-% As all base monoids are cancellative, we obtain $\forall i \in I.\; \melt(i) = \meltB(i)$ from which we immediately get $\melt = \meltB$.
-% \end{proof}
 
 % \subsection{Fractional monoid}
 % \label{sec:fracm}
@@ -214,32 +207,6 @@ $\oneshotm(-)$ is a locally non-expansive bifunctor from $\CMRAs$ to $\CMRAs$.
 % The first is trivial, the second follows from cancellativitiy of $M$.
 % \end{proof}
 
-% \subsection{Finite partial function monoid}
-% \label{sec:fpfunm}
-
-% Given a countable set $X$ and a monoid $M$, we construct a monoid representing finite partial functions from $X$ to (non-unit, non-zero elements of) $M$.
-% \ralf{all outdated}
-% Let ${X} \fpfn {M}$ be the product monoid $\prod_{x \in X} M$, as defined in \secref{sec:prodm} but restricting the carrier to functions $f$ where the set $\dom(f) \eqdef \{ x \mid f(x) \neq \munit_M \}$ is finite.
-% This is well-defined as the set of these $f$ contains the unit and is closed under multiplication.
-% (We identify finite partial functions from $X$ to $\mcarp{M}\setminus\{\munit_M\}$ and total functions from $X$ to $\mcarp{M}$ with finite $\munit_M$-support.)
-
-% We use two frame-preserving updates:
-% \begin{mathpar}
-%   \inferH{FpFunAlloc}
-%   {a \in \mcarp{M}}
-%   {f \mupd \{ f[x \mapsto a] \mid x \notin \dom(f) \}}
-%   \and
-%   \inferH{FpFunUpd}
-%   {a \mupd_M B}
-%   {f[i \mapsto a] \mupd \{ f[i \mapsto b] \mid b \in B\}}
-% \end{mathpar}
-% Rule \ruleref{FpFunUpd} simply restates \ruleref{ProdUpd}.
-
-% \begin{proof}[Proof of \ruleref{FpFunAlloc}]
-%   Assume some $g \sep f$. Since $\dom(f \mtimes g)$ is finite, there will be some undefined element $x \notin \dom(f \mtimes g)$. Let $f' \eqdef f[x \mapsto a]$. This is compatible with $g$, so we are done.
-% \end{proof}
-
-% We write $[x \mapsto a]$ for the function mapping $x$ to $a$ and everything else in $X$ to $\munit$.
 
 % %\subsection{Disposable monoid}
 % %

docs/derived.tex

@@ -205,38 +205,37 @@ We can derive some specialized forms of the lifting axioms for the operational s
 \ralf{Add these.}
 
 \subsection{Global functor and ghost ownership}
-\ralf{Describe this.}
 
-% \subsection{Global monoid}
+Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(F_i)_{i \in I}$ for some finite $I$ by picking
+\[ F(\cofe) \eqdef \prod_{i \in I} \textdom{GhName} \fpfn F_i(\cofe) \]
+We don't care so much about what concretely $\textdom{GhName}$ is, as long as it is countable and infinite.
+With $M_i \eqdef F_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto [\gname \mapsto \melt]]}$.
+In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the ``ghost location'' $\gname$ is allocated and we own piece $\melt$.
 
-% Hereinafter we assume the global monoid (served up as a parameter to Iris) is obtained from a family of monoids $(M_i)_{i \in I}$ by first applying the construction for finite partial functions to each~(\Sref{sec:fpfunm}), and then applying the product construction~(\Sref{sec:prodm}):
-% \[ M \eqdef \prod_{i \in I} \textdom{GhName} \fpfn M_i \]
-% We don't care so much about what concretely $\textdom{GhName}$ is, as long as it is countable and infinite.
-% We write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto [\gname \mapsto \melt]]}$ when $\melt \in \mcarp {M_i}$, and for $\FALSE$ when $\melt = \mzero_{M_i}$.
-% In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the name $\gname$ is allocated and has at least value $\melt$.
-
-% From~\ruleref{FpUpd} and the multiplications and frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfunm}, we have the following derived rules.
-% \begin{mathpar}
-% 	\axiomH{NewGhost}{
-% 		\TRUE \vs \Exists\gname. \ownGhost\gname{\melt : M_i}
-% 	}
-% 	\and
-% 	\inferH{GhostUpd}
-%     {\melt \mupd_{M_i} B}
-%     {\ownGhost\gname{\melt : M_i} \vs \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}}
-%   \and
-%   \axiomH{GhostEq}
-%     {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \Lra \ownGhost\gname{\melt\mtimes\meltB : M_i}}
-
-%   \axiomH{GhostUnit}
-%     {\TRUE \Ra \ownGhost{\gname}{\munit : M_i}}
-
-%   \axiomH{GhostZero}
-%     {\ownGhost\gname{\mzero : M_i} \Ra \FALSE}
-
-%   \axiomH{GhostTimeless}
-%     {\timeless{\ownGhost\gname{\melt : M_i}}}
-% \end{mathpar}
+From~\ruleref{pvs-update}, \ruleref{vs-update} and the frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfnm}, we have the following derived rules.
+\begin{mathparpagebreakable}
+  \inferH{NewGhostStrong}{\text{$G$ infinite}}
+  {  \TRUE \vs \Exists\gname\in G. \ownGhost\gname{\melt : M_i}
+  }
+  \and
+  \axiomH{NewGhost}{
+    \TRUE \vs \Exists\gname. \ownGhost\gname{\melt : M_i}
+  }
+  \and
+  \inferH{GhostUpd}
+    {\melt \mupd_{M_i} B}
+    {\ownGhost\gname{\melt : M_i} \vs \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}}
+  \and
+  \axiomH{GhostEq}
+    {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \Lra \ownGhost\gname{\melt\mtimes\meltB : M_i}}
+
+  \axiomH{GhostVal}
+    {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}
+
+  \inferH{GhostTimeless}
+    {\text{$\melt$ is a discrete COFE element}}
+    {\timeless{\ownGhost\gname{\melt : M_i}}}
+\end{mathparpagebreakable}
 
 \subsection{Invariant identifier namespaces}
 

docs/logic.tex

@@ -129,7 +129,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
     \All \var:\type. \prop \mid
 \\&
     \knowInv{\term}{\prop} \mid
-    \ownGGhost{\term} \mid
+    \ownGGhost{\term} \mid \mval(\term) \mid
     \ownPhys{\term} \mid
     \always\prop \mid
     {\later\prop} \mid
@@ -276,6 +276,9 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 \and
 	\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
 		{\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
+\and
+	\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
+		{\vctx \proves \wtt{\mval(\melt)}{\Prop}}
 \and
 	\infer{\vctx \proves \wtt{\state}{\textlog{State}}}
 		{\vctx \proves \wtt{\ownPhys{\state}}{\Prop}}
@@ -418,7 +421,7 @@ This is entirely standard.
 \begin{mathpar}
 \begin{array}{rMcMl}
 \ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff&  \ownGGhost{\melt \mtimes \meltB} \\
-\ownGGhost{\melt} &\provesIff& \melt \in \mval \\
+\ownGGhost{\melt} &\provesIff& \mval(\melt) \\
 \TRUE &\proves&  \ownGGhost{\munit}
 \end{array}
 \and
@@ -463,6 +466,10 @@ This is entirely standard.
 {\text{$\melt$ is a discrete COFE element}}
 {\timeless{\ownGGhost\melt}}
 
+\infer
+{\text{$\melt$ is a discrete COFE element}}
+{\timeless{\mval(\melt)}}
+
 \infer{}
 {\timeless{\ownPhys\state}}
 
@@ -536,17 +543,17 @@ This is entirely standard.
 \infer[pvs-frame]
 {}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop}
 
-\infer[pvs-allocI]
+\inferH{pvs-allocI}
 {\text{$\mask$ is infinite}}
 {\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
 
-\infer[pvs-openI]
+\inferH{pvs-openI}
 {}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
 
-\infer[pvs-closeI]
+\inferH{pvs-closeI}
 {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
 
-\infer[pvs-update]
+\inferH{pvs-update}
 {\melt \mupd \meltsB}
 {\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB}
 \end{mathpar}