From 6562c4be742a7044e7e7e105e6d171cc3e0c3a96 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 11 Mar 2016 17:20:34 +0100
Subject: [PATCH] docs: global ghost functor
---
algebra/one_shot.v | 14 +++++
docs/algebra.tex | 4 +-
docs/constructions.tex | 117 +++++++++++++++--------------------------
docs/derived.tex | 59 ++++++++++-----------
docs/logic.tex | 19 ++++---
5 files changed, 101 insertions(+), 112 deletions(-)
diff --git a/algebra/one_shot.v b/algebra/one_shot.v
index 2cefc59b7..9989f8a6c 100644
--- a/algebra/one_shot.v
+++ b/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.
diff --git a/docs/algebra.tex b/docs/algebra.tex
index a120b09f0..4b0058e62 100644
--- a/docs/algebra.tex
+++ b/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.
diff --git a/docs/constructions.tex b/docs/constructions.tex
index b780efec9..6579c6c71 100644
--- a/docs/constructions.tex
+++ b/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}
% %
diff --git a/docs/derived.tex b/docs/derived.tex
index 0560bc0eb..8e8767cbf 100644
--- a/docs/derived.tex
+++ b/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}
diff --git a/docs/logic.tex b/docs/logic.tex
index 150836bff..2f77240a2 100644
--- a/docs/logic.tex
+++ b/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}
--
GitLab