Commit 7cb94e3e authored by Ralf Jung's avatar Ralf Jung

docs: complete model description

parent 82aee390
Pipeline #331 passed with stage
...@@ -23,6 +23,8 @@ This definition varies slightly from the original one in~\cite{catlogic}. ...@@ -23,6 +23,8 @@ This definition varies slightly from the original one in~\cite{catlogic}.
An element $x \in \cofe$ of a COFE is called \emph{discrete} if An element $x \in \cofe$ of a COFE is called \emph{discrete} if
\[ \All y \in \cofe. x \nequiv{0} y \Ra x = y\] \[ \All y \in \cofe. x \nequiv{0} y \Ra x = y\]
A COFE $A$ is called \emph{discrete} if all its elements are discrete. A COFE $A$ is called \emph{discrete} if all its elements are discrete.
For a set $X$, we write $\Delta X$ for the discrete COFE with $x \nequiv{n} x' \eqdef x = x'$
\end{defn} \end{defn}
\begin{defn} \begin{defn}
...@@ -31,6 +33,7 @@ This definition varies slightly from the original one in~\cite{catlogic}. ...@@ -31,6 +33,7 @@ This definition varies slightly from the original one in~\cite{catlogic}.
It is \emph{contractive} if It is \emph{contractive} if
\[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x) \] \[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x) \]
\end{defn} \end{defn}
The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
\begin{defn} \begin{defn}
The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows. The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
......
...@@ -33,7 +33,7 @@ We start by defining the COFE of \emph{step-indexed propositions}: For every ste ...@@ -33,7 +33,7 @@ We start by defining the COFE of \emph{step-indexed propositions}: For every ste
\end{align*} \end{align*}
Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny. Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny.
\begin{align*} \begin{align*}
\UPred(\monoid) \approx{}& \monoid \monra \SProp \\ \UPred(\monoid) \cong{}& \monoid \monra \SProp \\
\eqdef{}& \setComp{\pred: \monoid \nfn \SProp}{\All n, m, x, y. n \in \pred(x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra m \in \pred(y)} \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}{\All n, m, x, y. n \in \pred(x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra m \in \pred(y)}
\end{align*} \end{align*}
The reason we chose the first definition is that it is easier to work with in Coq. The reason we chose the first definition is that it is easier to work with in Coq.
...@@ -77,35 +77,35 @@ $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$. ...@@ -77,35 +77,35 @@ $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement} \subsection{Agreement}
Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows: Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\newcommand{\agc}{\mathrm{c}} % the "c" field of an agreement element \newcommand{\aginjc}{\mathrm{c}} % the "c" field of an agreement element
\newcommand{\agV}{\mathrm{V}} % the "V" field of an agreement element \newcommand{\aginjV}{\mathrm{V}} % the "V" field of an agreement element
\begin{align*} \begin{align*}
\agm(\cofe) \eqdef{}& \record{\agc : \mathbb{N} \to \cofe , \agV : \SProp} \\ \agm(\cofe) \eqdef{}& \record{\aginjc : \mathbb{N} \to \cofe , \aginjV : \SProp} \\
& \text{quotiented by} \\ & \text{quotiented by} \\
\melt \equiv \meltB \eqdef{}& \melt.\agV = \meltB.\agV \land \All n. n \in \melt.\agV \Ra \melt.\agc(n) \nequiv{n} \meltB.\agc(n) \\ \melt \equiv \meltB \eqdef{}& \melt.\aginjV = \meltB.\aginjV \land \All n. n \in \melt.\aginjV \Ra \melt.\aginjc(n) \nequiv{n} \meltB.\aginjc(n) \\
\melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\agV \Lra m \in \meltB.\agV) \land (\All m \leq n. m \in \melt.\agV \Ra \melt.\agc(m) \nequiv{m} \meltB.\agc(m)) \\ \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\aginjV \Lra m \in \meltB.\aginjV) \land (\All m \leq n. m \in \melt.\aginjV \Ra \melt.\aginjc(m) \nequiv{m} \meltB.\aginjc(m)) \\
\mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.\agV \land \All m \leq n. \melt.\agc(n) \nequiv{m} \melt.\agc(m) } \\ \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\
\mcore\melt \eqdef{}& \melt \\ \mcore\melt \eqdef{}& \melt \\
\melt \mtimes \meltB \eqdef{}& (\melt.\agc, \setComp{n}{n \in \melt.\agV \land n \in \meltB.\agV \land \melt \nequiv{n} \meltB }) \melt \mtimes \meltB \eqdef{}& (\melt.\aginjc, \setComp{n}{n \in \melt.\aginjV \land n \in \meltB.\aginjV \land \melt \nequiv{n} \meltB })
\end{align*} \end{align*}
$\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$. $\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
You can think of the $\agc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in \agV$ steps. You can think of the $\aginjc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in \aginjV$ steps.
The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$. The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
However, given such a chain, we cannot constructively define its limit: Clearly, the $\agV$ of the limit is the limit of the $\agV$ of the chain. However, given such a chain, we cannot constructively define its limit: Clearly, the $\aginjV$ of the limit is the limit of the $\aginjV$ of the chain.
But what to pick for the actual data, for the element of $\cofe$? But what to pick for the actual data, for the element of $\cofe$?
Only if $\agV = \mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $\agV$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin \agV$. Only if $\aginjV = \mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $\aginjV$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin \aginjV$.
To mitigate this, we apply the usual construction to close a set; we go from elements of $\cofe$ to chains of $\cofe$. To mitigate this, we apply the usual construction to close a set; we go from elements of $\cofe$ to chains of $\cofe$.
We define an injection $\ag$ into $\agm(\cofe)$ as follows: We define an injection $\aginj$ into $\agm(\cofe)$ as follows:
\[ \ag(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \mathbb{N}} \] \[ \aginj(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \mathbb{N}} \]
There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following: There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
\begin{mathpar} \begin{mathpar}
\axiomH{ag-val}{\ag(x) \in \mval_n} \axiomH{ag-val}{\aginj(x) \in \mval_n}
\axiomH{ag-dup}{\ag(x) = \ag(x)\mtimes\ag(x)} \axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)}
\axiomH{ag-agree}{\ag(x) \mtimes \ag(y) \in \mval_n \Ra x \nequiv{n} y} \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Ra x \nequiv{n} y}
\end{mathpar} \end{mathpar}
\subsection{One-shot} \subsection{One-shot}
...@@ -115,17 +115,17 @@ Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows: ...@@ -115,17 +115,17 @@ Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows:
\begin{align*} \begin{align*}
\oneshotm(\monoid) \eqdef{}& \ospending + \osshot(\monoid) + \munit + \bot \\ \oneshotm(\monoid) \eqdef{}& \ospending + \osshot(\monoid) + \munit + \bot \\
\mval_n \eqdef{}& \set{\ospending, \munit} \cup \setComp{\osshot(\melt)}{\melt \in \mval_n} \mval_n \eqdef{}& \set{\ospending, \munit} \cup \setComp{\osshot(\melt)}{\melt \in \mval_n}
\end{align*} \\%\end{align*}
\begin{align*} %\begin{align*}
\mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\
\mcore{\munit} \eqdef{}& \munit & \mcore{\bot} \eqdef{}& \bot
\end{align*}
\begin{align*}
\osshot(\melt) \mtimes \osshot(\meltB) \eqdef{}& \osshot(\melt \mtimes \meltB) \\ \osshot(\melt) \mtimes \osshot(\meltB) \eqdef{}& \osshot(\melt \mtimes \meltB) \\
\munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\ \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
\munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt)
\end{align*} \end{align*}%
The remaining cases of composition go to $\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: The step-indexed equivalence is inductively defined as follows:
\begin{mathpar} \begin{mathpar}
\axiom{\ospending \nequiv{n} \ospending} \axiom{\ospending \nequiv{n} \ospending}
...@@ -149,34 +149,38 @@ We obtain the following frame-preserving updates: ...@@ -149,34 +149,38 @@ We obtain the following frame-preserving updates:
{\osshot(\melt) \mupd \setComp{\osshot(\meltB)}{\meltB \in \meltsB}} {\osshot(\melt) \mupd \setComp{\osshot(\meltB)}{\meltB \in \meltsB}}
\end{mathpar} \end{mathpar}
%TODO: These need syncing with Coq \subsection{Exclusive CMRA}
% \subsection{Exclusive monoid}
% Given a set $X$, we define a monoid such that at most one $x \in X$ can be owned. Given a cofe $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
% Let $\exm{X}$ be the monoid with carrier $X \uplus \{ \munit \}$ and multiplication \begin{align*}
% \[ \exm(\cofe) \eqdef{}& \exinj(\cofe) + \munit + \bot \\
% \melt \cdot \meltB \;\eqdef\; \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot} \\
% \begin{cases} \munit \mtimes \exinj(x) \eqdef{}& \exinj(x) \mtimes \munit \eqdef \exinj(x)
% \melt & \mbox{if } \meltB = \munit \\ \end{align*}
% \meltB & \mbox{if } \melt = \munit The remaining cases of composition go to $\bot$.
% \end{cases} \begin{align*}
% \] \mcore{\exinj(x)} \eqdef{}& \munit & \mcore{\munit} \eqdef{}& \munit &
\mcore{\bot} \eqdef{}& \bot
\end{align*}
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
\infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
% The frame-preserving update \axiom{\munit \nequiv{n} \munit}
% \begin{mathpar}
% \inferH{ExUpd}
% {x \in X}
% {x \mupd \melt}
% \end{mathpar}
% is easily shown, as the only possible frame for $x$ is $\munit$.
% Exclusive monoids are cancellative. \axiom{\bot \nequiv{n} \bot}
% \begin{proof}[Proof of cancellativity] \end{mathpar}
% If $\melt_f = \munit$, then the statement is trivial. $\exm(-)$ is a locally non-expansive functor from $\COFEs$ 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} We obtain the following frame-preserving update:
\begin{mathpar}
\inferH{ex-update}{}
{\exinj(x) \mupd \exinj(y)}
\end{mathpar}
%TODO: These need syncing with Coq
% \subsection{Finite Powerset Monoid} % \subsection{Finite Powerset Monoid}
% Given an infinite set $X$, we define a monoid $\textmon{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows: % Given an infinite set $X$, we define a monoid $\textmon{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows:
......
...@@ -86,13 +86,15 @@ ...@@ -86,13 +86,15 @@
\newcommand{\rs}{r} \newcommand{\rs}{r}
\newcommand{\rsB}{s} \newcommand{\rsB}{s}
\newcommand{\rss}{R}
\newcommand{\pres}{\pi} \newcommand{\pres}{\pi}
\newcommand{\wld}{w} \newcommand{\wld}{w}
\newcommand{\ghostRes}{g} \newcommand{\ghostRes}{g}
%% Various pieces of syntax %% Various pieces of syntax
\newcommand{\wsat}[4]{#1 \models_{#2} #3; #4} \newcommand{\wsat}[3]{#1 \models_{#2} #3}
\newcommand{\wsatpre}{\textdom{pre-wsat}}
\newcommand{\wtt}[2]{#1 : #2} % well-typed term \newcommand{\wtt}[2]{#1 : #2} % well-typed term
...@@ -114,6 +116,7 @@ ...@@ -114,6 +116,7 @@
\newcommand{\UPred}{\textdom{UPred}} \newcommand{\UPred}{\textdom{UPred}}
\newcommand{\mProp}{\textdom{Prop}} % meta-level prop \newcommand{\mProp}{\textdom{Prop}} % meta-level prop
\newcommand{\iProp}{\textdom{iProp}} \newcommand{\iProp}{\textdom{iProp}}
\newcommand{\iPreProp}{\textdom{iPreProp}}
\newcommand{\Wld}{\textdom{Wld}} \newcommand{\Wld}{\textdom{Wld}}
\newcommand{\Res}{\textdom{Res}} \newcommand{\Res}{\textdom{Res}}
...@@ -121,6 +124,7 @@ ...@@ -121,6 +124,7 @@
\newcommand{\cofeB}{U} \newcommand{\cofeB}{U}
\newcommand{\COFEs}{\mathcal{U}} % category of COFEs \newcommand{\COFEs}{\mathcal{U}} % category of COFEs
\newcommand{\iFunc}{\Sigma} \newcommand{\iFunc}{\Sigma}
\newcommand{\fix}{\textdom{fix}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS % CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
...@@ -136,6 +140,8 @@ ...@@ -136,6 +140,8 @@
\newcommand{\melts}{A} \newcommand{\melts}{A}
\newcommand{\meltsB}{B} \newcommand{\meltsB}{B}
\newcommand{\f}{\mathrm{f}} % for "frame"
\newcommand{\mcar}[1]{|#1|} \newcommand{\mcar}[1]{|#1|}
\newcommand{\mcarp}[1]{\mcar{#1}^{+}} \newcommand{\mcarp}[1]{\mcar{#1}^{+}}
\newcommand{\munit}{\varepsilon} \newcommand{\munit}{\varepsilon}
...@@ -321,13 +327,14 @@ ...@@ -321,13 +327,14 @@
% Agreement % Agreement
\newcommand{\agm}{\ensuremath{\textmon{Ag}}} \newcommand{\agm}{\ensuremath{\textmon{Ag}}}
\newcommand{\ag}{\textlog{ag}} \newcommand{\aginj}{\textlog{ag}}
% Fraction % Fraction
\newcommand{\fracm}{\ensuremath{\textmon{Frac}}} \newcommand{\fracm}{\ensuremath{\textmon{Frac}}}
% Exclusive % Exclusive
\newcommand{\exm}{\ensuremath{\textmon{Ex}}} \newcommand{\exm}{\ensuremath{\textmon{Ex}}}
\newcommand{\exinj}{\textlog{ex}}
% Auth % Auth
\newcommand{\authm}{\textmon{Auth}} \newcommand{\authm}{\textmon{Auth}}
......
...@@ -124,7 +124,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t ...@@ -124,7 +124,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\prop * \prop \mid \prop * \prop \mid
\prop \wand \prop \mid \prop \wand \prop \mid
\\& \\&
\MU \var:\type. \pred \mid \MU \var:\type. \term \mid
\Exists \var:\type. \prop \mid \Exists \var:\type. \prop \mid
\All \var:\type. \prop \mid \All \var:\type. \prop \mid
\\& \\&
...@@ -136,7 +136,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t ...@@ -136,7 +136,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\pvs[\term][\term] \prop\mid \pvs[\term][\term] \prop\mid
\wpre{\term}[\term]{\Ret\var.\term} \wpre{\term}[\term]{\Ret\var.\term}
\end{align*} \end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality. Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$. 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$. We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
......
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment