Commit 3ca48414 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents d71cbe0f 04d3ee68
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
\subsection{COFE} \subsection{COFE}
This definition varies slightly from the original one in~\cite{catlogic}.
\begin{defn}[Chain] \begin{defn}[Chain]
Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \mathbb{N}}$ of equivalence relations, a \emph{chain} is a function $c : \mathbb{N} \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$. Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \mathbb{N}}$ of equivalence relations, a \emph{chain} is a function $c : \mathbb{N} \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
\end{defn} \end{defn}
...@@ -22,6 +23,8 @@ ...@@ -22,6 +23,8 @@
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}
...@@ -30,6 +33,7 @@ ...@@ -30,6 +33,7 @@
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.
...@@ -52,7 +56,31 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th ...@@ -52,7 +56,31 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th
\subsection{RA} \subsection{RA}
\ralf{Copy this from the paper, when that one is more polished.} \begin{defn}
A \emph{resource algebra} (RA) is a tuple \\
$(\monoid, \mval \subseteq \monoid, \mcore{-}:
\monoid \to \monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying
\begin{align*}
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{ra-assoc} \\
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{ra-comm} \\
\All \melt.& \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\
\All \melt.& \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\
\All \melt, \meltB.& \melt \mincl \meltB \Ra \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\\
\melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
\end{align*}
\end{defn}
\begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
\[ \All \melt_\f. \melt \mtimes \melt_\f \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_\f \in \mval \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
\ralf{Copy the explanation from the paper, when that one is more polished.}
\subsection{CMRA} \subsection{CMRA}
...@@ -70,7 +98,8 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th ...@@ -70,7 +98,8 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th
\All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$\melt \in \mval_n \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\ \All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$\melt \in \mval_n \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{cmra-extend} \\
\text{where}\qquad\qquad\\ \text{where}\qquad\qquad\\
\melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \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}
\end{align*} \end{align*}
\end{defn} \end{defn}
...@@ -117,7 +146,7 @@ This operation is needed to prove that $\later$ commutes with existential quanti ...@@ -117,7 +146,7 @@ This operation is needed to prove that $\later$ commutes with existential quanti
\begin{defn} \begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
\[ \All n, \melt_f. \melt \mtimes \melt_f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_f \in \mval_n \] \[ \All n, \melt_\f. \melt \mtimes \melt_\f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_\f \in \mval_n \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn} \end{defn}
......
...@@ -25,7 +25,7 @@ where $\mProp$ is the set of meta-level propositions, \eg Coq's \texttt{Prop}. ...@@ -25,7 +25,7 @@ where $\mProp$ is the set of meta-level propositions, \eg Coq's \texttt{Prop}.
$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$. $\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
One way to understand this definition is to re-write it a little. One way to understand this definition is to re-write it a little.
We start by defining the COFE of \emph{step-indexed propositions}: We start by defining the COFE of \emph{step-indexed propositions}: For every step-index, we proposition either holds or does not hold.
\begin{align*} \begin{align*}
\SProp \eqdef{}& \psetdown{\mathbb{N}} \\ \SProp \eqdef{}& \psetdown{\mathbb{N}} \\
\eqdef{}& \setComp{\prop \in \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in \prop \Ra m \in \prop } \\ \eqdef{}& \setComp{\prop \in \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in \prop \Ra m \in \prop } \\
...@@ -33,7 +33,7 @@ We start by defining the COFE of \emph{step-indexed propositions}: ...@@ -33,7 +33,7 @@ We start by defining the COFE of \emph{step-indexed propositions}:
\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,33 +149,38 @@ We obtain the following frame-preserving updates: ...@@ -149,33 +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}
% \subsection{Exclusive monoid} \subsection{Exclusive CMRA}
% 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} \axiom{\bot \nequiv{n} \bot}
% {x \in X} \end{mathpar}
% {x \mupd \melt} $\exm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
% \end{mathpar}
% is easily shown, as the only possible frame for $x$ is $\munit$. We obtain the following frame-preserving update:
\begin{mathpar}
\inferH{ex-update}{}
{\exinj(x) \mupd \exinj(y)}
\end{mathpar}
% Exclusive monoids are cancellative.
% \begin{proof}[Proof of cancellativity]
% If $\melt_f = \munit$, then the statement is trivial.
% If $\melt_f \neq \munit$, then we must have $\melt = \meltB = \munit$, as otherwise one of the two products would be $\mzero$.
% \end{proof}
%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:
...@@ -190,16 +195,16 @@ We obtain the following frame-preserving updates: ...@@ -190,16 +195,16 @@ We obtain the following frame-preserving updates:
% \end{mathpar} % \end{mathpar}
% \begin{proof}[Proof of \ruleref{PowFinUpd}] % \begin{proof}[Proof of \ruleref{PowFinUpd}]
% Assume some frame $\melt_f \sep \emptyset$. Since $\melt_f$ is finite and $X$ is infinite, there exists an $x \notin \melt_f$. % Assume some frame $\melt_\f \sep \emptyset$. Since $\melt_\f$ is finite and $X$ is infinite, there exists an $x \notin \melt_\f$.
% Pick that for the result. % Pick that for the result.
% \end{proof} % \end{proof}
% The powerset monoids is cancellative. % The powerset monoids is cancellative.
% \begin{proof}[Proof of cancellativity] % \begin{proof}[Proof of cancellativity]
% Let $\melt_f \mtimes \melt = \melt_f \mtimes \meltB \neq \mzero$. % Let $\melt_\f \mtimes \melt = \melt_\f \mtimes \meltB \neq \mzero$.
% So we have $\melt_f \sep \melt$ and $\melt_f \sep \meltB$, and we have to show $\melt = \meltB$. % So we have $\melt_\f \sep \melt$ and $\melt_\f \sep \meltB$, and we have to show $\melt = \meltB$.
% Assume $x \in \melt$. Hence $x \in \melt_f \mtimes \melt$ and thus $x \in \melt_f \mtimes \meltB$. % Assume $x \in \melt$. Hence $x \in \melt_\f \mtimes \melt$ and thus $x \in \melt_\f \mtimes \meltB$.
% By disjointness, $x \notin \melt_f$ and hence $x \in meltB$. % By disjointness, $x \notin \melt_\f$ and hence $x \in meltB$.
% The other direction works the same way. % The other direction works the same way.
% \end{proof} % \end{proof}
...@@ -233,20 +238,20 @@ We obtain the following frame-preserving updates: ...@@ -233,20 +238,20 @@ We obtain the following frame-preserving updates:
% \begin{proof}[Proof of \ruleref{FracUpdLocal}] % \begin{proof}[Proof of \ruleref{FracUpdLocal}]
% Assume some $f \sep (q, a)$. If $f = \munit$, then $f \sep (q, b)$ is trivial for any $b \in B$. Just pick the one we obtain by choosing $\munit_M$ as the frame for $a$. % Assume some $f \sep (q, a)$. If $f = \munit$, then $f \sep (q, b)$ is trivial for any $b \in B$. Just pick the one we obtain by choosing $\munit_M$ as the frame for $a$.
% In the interesting case, we have $f = (q_f, a_f)$. % In the interesting case, we have $f = (q_\f, a_\f)$.
% Obtain $b$ such that $b \in B \land b \sep a_f$. % Obtain $b$ such that $b \in B \land b \sep a_\f$.
% Then $(q, b) \sep f$, and we are done. % Then $(q, b) \sep f$, and we are done.
% \end{proof} % \end{proof}
% $\fracm{M}$ is cancellative if $M$ is cancellative. % $\fracm{M}$ is cancellative if $M$ is cancellative.
% \begin{proof}[Proof of cancellativitiy] % \begin{proof}[Proof of cancellativitiy]
% If $\melt_f = \munit$, we are trivially done. % If $\melt_\f = \munit$, we are trivially done.
% So let $\melt_f = (q_f, \melt_f')$. % So let $\melt_\f = (q_\f, \melt_\f')$.
% If $\melt = \munit$, then $\meltB = \munit$ as otherwise the fractions could not match up. % If $\melt = \munit$, then $\meltB = \munit$ as otherwise the fractions could not match up.
% Again, we are trivially done. % Again, we are trivially done.
% Similar so for $\meltB = \munit$. % Similar so for $\meltB = \munit$.
% So let $\melt = (q_a, \melt')$ and $\meltB = (q_b, \meltB')$. % So let $\melt = (q_a, \melt')$ and $\meltB = (q_b, \meltB')$.
% We have $(q_f + q_a, \melt_f' \mtimes \melt') = (q_f + q_b, \melt_f' \mtimes \meltB')$. % We have $(q_\f + q_a, \melt_\f' \mtimes \melt') = (q_\f + q_b, \melt_\f' \mtimes \meltB')$.
% We have to show $q_a = q_b$ and $\melt' = \meltB'$. % We have to show $q_a = q_b$ and $\melt' = \meltB'$.
% The first is trivial, the second follows from cancellativitiy of $M$. % The first is trivial, the second follows from cancellativitiy of $M$.
% \end{proof} % \end{proof}
...@@ -307,7 +312,7 @@ We obtain the following frame-preserving updates: ...@@ -307,7 +312,7 @@ We obtain the following frame-preserving updates:
% The frame-preserving update involves a rather unwieldy side-condition: % The frame-preserving update involves a rather unwieldy side-condition:
% \begin{mathpar} % \begin{mathpar}
% \inferH{AuthUpd}{ % \inferH{AuthUpd}{
% \All\melt_f\in\mcar{\monoid}. \melt\sep\meltB \land \melt\mtimes\melt_f \le \meltB\mtimes\melt_f \Ra \melt'\mtimes\melt_f \le \melt'\mtimes\meltB \and % \All\melt_\f\in\mcar{\monoid}. \melt\sep\meltB \land \melt\mtimes\melt_\f \le \meltB\mtimes\melt_\f \Ra \melt'\mtimes\melt_\f \le \melt'\mtimes\meltB \and
% \melt' \sep \meltB % \melt' \sep \meltB
% }{ % }{
% \authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt' % \authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt'
...@@ -373,8 +378,6 @@ We obtain the following frame-preserving updates: ...@@ -373,8 +378,6 @@ We obtain the following frame-preserving updates:
% \subsection{STS with tokens monoid} % \subsection{STS with tokens monoid}
% \label{sec:stsmon} % \label{sec:stsmon}
% \ralf{This needs syncing with the Coq development.}
% Given a state-transition system~(STS) $(\STSS, \ra)$, a set of tokens $\STSS$, and a labeling $\STSL: \STSS \ra \mathcal{P}(\STST)$ of \emph{protocol-owned} tokens for each state, we construct a monoid modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens. % Given a state-transition system~(STS) $(\STSS, \ra)$, a set of tokens $\STSS$, and a labeling $\STSL: \STSS \ra \mathcal{P}(\STST)$ of \emph{protocol-owned} tokens for each state, we construct a monoid modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
% The construction follows the idea of STSs as described in CaReSL \cite{caresl}. % The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
...@@ -389,11 +392,11 @@ We obtain the following frame-preserving updates: ...@@ -389,11 +392,11 @@ We obtain the following frame-preserving updates:
% We have % We have
% \begin{quote} % \begin{quote}
% If $(s, T) \ra (s', T')$\\ % If $(s, T) \ra (s', T')$\\
% and $T_f \sep (T \uplus \STSL(s))$,\\ % and $T_\f \sep (T \uplus \STSL(s))$,\\
% then $\textsf{frame}(s, T_f) \ra \textsf{frame}(s', T_f)$. % then $\textsf{frame}(s, T_\f) \ra \textsf{frame}(s', T_\f)$.
% \end{quote} % \end{quote}
% \begin{proof} % \begin{proof}
% This follows directly by framing the tokens in $\STST \setminus (T_f \uplus T \uplus \STSL(s))$ around the given transition, which yields $(s, \STST \setminus (T_f \uplus \STSL{T}(s))) \ra (s', T' \uplus (\STST \setminus (T_f \uplus T \uplus \STSL{T}(s))))$. % This follows directly by framing the tokens in $\STST \setminus (T_\f \uplus T \uplus \STSL(s))$ around the given transition, which yields $(s, \STST \setminus (T_\f \uplus \STSL{T}(s))) \ra (s', T' \uplus (\STST \setminus (T_\f \uplus T \uplus \STSL{T}(s))))$.
% This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s') \uplus T'$. % This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s') \uplus T'$.
% \end{proof} % \end{proof}
...@@ -415,8 +418,8 @@ We obtain the following frame-preserving updates: ...@@ -415,8 +418,8 @@ We obtain the following frame-preserving updates:
% {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')} % {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')}
% \end{mathpar} % \end{mathpar}
% \begin{proof}[Proof of \ruleref{StsStep}] % \begin{proof}[Proof of \ruleref{StsStep}]
% Assume some upwards-closed $S_f, T_f$ (the frame cannot be authoritative) s.t.\ $s \in S_f$ and $T_f \sep (T \uplus \STSL(s))$. We have to show that this frame combines with our final monoid element, which is the case if $s' \in S_f$ and $T_f \sep T'$. % Assume some upwards-closed $S_\f, T_\f$ (the frame cannot be authoritative) s.t.\ $s \in S_\f$ and $T_\f \sep (T \uplus \STSL(s))$. We have to show that this frame combines with our final monoid element, which is the case if $s' \in S_\f$ and $T_\f \sep T'$.
% By upward-closedness, it suffices to show $\textsf{frame}(s, T_f) \ststrans \textsf{frame}(s', T_f)$. % By upward-closedness, it suffices to show $\textsf{frame}(s, T_\f) \ststrans \textsf{frame}(s', T_\f)$.
% This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step. % This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step.
% \end{proof} % \end{proof}
......
...@@ -205,9 +205,64 @@ The following rules can be derived for Hoare triples. ...@@ -205,9 +205,64 @@ The following rules can be derived for Hoare triples.
\end{mathparpagebreakable} \end{mathparpagebreakable}
\paragraph{Lifting of operational semantics.} \paragraph{Lifting of operational semantics.}
We can derive some specialized forms of the lifting axioms for the operational semantics, as well as some forms that involve view shifts and Hoare triples. We can derive some specialized forms of the lifting axioms for the operational semantics.
\begin{mathparpagebreakable}
\infer[wp-lift-atomic-step]
{\atomic(\expr_1) \and
\red(\expr_1, \state_1) \and
\All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f)}
{\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. \pred(\ofval(\val), \state_2, \expr_\f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
\infer[wp-lift-atomic-det-step]
{\atomic(\expr_1) \and
\red(\expr_1, \state_1) \and
\All \expr'_2, \state'_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_\f = \expr_\f'}
{\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
\infer[wp-lift-pure-det-step]
{\toval(\expr_1) = \bot \and
\All \state_1. \red(\expr_1, \state_1) \and
\All \state_1, \expr_2', \state_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_\f = \expr_\f'}
{\later ( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
\end{mathparpagebreakable}
\ralf{Add these.} Furthermore, we derive some forms that directly involve view shifts and Hoare triples.
\begin{mathparpagebreakable}
\infer[ht-lift-step]
{\mask_2 \subseteq \mask_1 \and
\toval(\expr_1) = \bot \and
\red(\expr_1, \state_1) \and
\All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f) \\\\
\prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and
\All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) * \ownPhys{\state_2} * \prop' \vs[\mask_2][\mask_1] \propB_1 * \propB_2 \\\\
\All \expr_2, \state_2, \expr_\f. \hoare{\propB_1}{\expr_2}{\Ret\val.\propC}[\mask_1] \and
\All \expr_2, \state_2, \expr_\f. \hoare{\propB_2}{\expr_\f}{\Ret\any. \TRUE}[\top]}
{ \hoare\prop{\expr_1}{\Ret\val.\propC}[\mask_1] }
\infer[ht-lift-atomic-step]
{\atomic(\expr_1) \and
\red(\expr_1, \state_1) \and
\All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f) \\\\
\prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and
\All \expr_2, \state_2, \expr_\f. \hoare{\pred(\expr_2,\state_2,\expr_\f) * \prop}{\expr_\f}{\Ret\any. \TRUE}[\top]}
{ \hoare{\later\ownPhys{\state_1} * \later\prop}{\expr_1}{\Ret\val.\Exists \state_2, \expr_\f. \ownPhys{\state_2} * \pred(\ofval(\expr_2),\state_2,\expr_\f)}[\mask_1] }
\infer[ht-lift-pure-step]
{\toval(\expr_1) = \bot \and
\All\state_1. \red(\expr_1, \state_1) \and
\All \state_1, \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_\f) \\\\
\All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and
\All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]}
{ \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] }
\infer[ht-lift-pure-det-step]
{\toval(\expr_1) = \bot \and
\All\state_1. \red(\expr_1, \state_1) \and
\All \state_1, \expr_2', \state_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_\f = \expr_\f' \\\\
\hoare{\prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and
\hoare{\prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]}
{ \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] }
\end{mathparpagebreakable}
\subsection{Global functor and ghost ownership} \subsection{Global functor and ghost ownership}
...@@ -282,6 +337,7 @@ We can now derive the following rules for this derived form of the invariant ass ...@@ -282,6 +337,7 @@ We can now derive the following rules for this derived form of the invariant ass
{\knowInv\namesp\prop \proves \propB \vs[\mask] \propC} {\knowInv\namesp\prop \proves \propB \vs[\mask] \propC}
\end{mathpar} \end{mathpar}
% TODO: These need syncing with Coq
% \subsection{STSs with interpretation}\label{sec:stsinterp} % \subsection{STSs with interpretation}\label{sec:stsinterp}
% Building on \Sref{sec:stsmon}, after constructing the monoid $\STSMon{\STSS}$ for a particular STS, we can use an invariant to tie an interpretation, $\pred : \STSS \to \Prop$, to the STS's current state, recovering CaReSL-style reasoning~\cite{caresl}. % Building on \Sref{sec:stsmon}, after constructing the monoid $\STSMon{\STSS}$ for a particular STS, we can use an invariant to tie an interpretation, $\pred : \STSS \to \Prop$, to the STS's current state, recovering CaReSL-style reasoning~\cite{caresl}.
...@@ -382,21 +438,21 @@ We can now derive the following rules for this derived form of the invariant ass ...@@ -382,21 +438,21 @@ We can now derive the following rules for this derived form of the invariant ass
% {\later\pred_\bot(a) \vs[\mask] \exists \iname \in \mask, \gname.\; \Auth(M, \pred, \gname, \iname) * \ownGhost{\gname}{\authfrag a : \auth{M}}} % {\later\pred_\bot(a) \vs[\mask] \exists \iname \in \mask, \gname.\; \Auth(M, \pred, \gname, \iname) * \ownGhost{\gname}{\authfrag a : \auth{M}}}
% \and % \and
% \axiomH{AuthOpen} % \axiomH{AuthOpen}
% {\Auth(M, \pred, \gname, \iname) \vdash \ownGhost{\gname}{\authfrag \melt : \auth{M}} \vsE[\{\iname\}][\emptyset] \exists \melt_f.\; \later\pred_\bot(\melt \mtimes \melt_f) * \ownGhost{\gname}{\authfull \melt \mtimes \melt_f, \authfrag a:\auth{M}}} % {\Auth(M, \pred, \gname, \iname) \vdash \ownGhost{\gname}{\authfrag \melt : \auth{M}} \vsE[\{\iname\}][\emptyset] \exists \melt_\f.\; \later\pred_\bot(\melt \mtimes \melt_\f) * \ownGhost{\gname}{\authfull \melt \mtimes \melt_\f, \authfrag a:\auth{M}}}
% \and % \and
% \axiomH{AuthClose} % \axiomH{AuthClose}
% {\Auth(M, \pred, \gname, \iname) \vdash \later\pred_\bot(\meltB \mtimes \melt_f) * \ownGhost{\gname}{\authfull a \mtimes \melt_f, \authfrag a:\auth{M}} \vs[\emptyset][\{\iname\}] \ownGhost{\gname}{\authfrag \meltB : \auth{M}} } % {\Auth(M, \pred, \gname, \iname) \vdash \later\pred_\bot(\meltB \mtimes \melt_\f) * \ownGhost{\gname}{\authfull a \mtimes \melt_\f, \authfrag a:\auth{M}} \vs[\emptyset][\{\iname\}] \ownGhost{\gname}{\authfrag \meltB : \auth{M}} }
% \end{mathpar} % \end{mathpar}
% These view shifts in turn can be used to prove variants of the invariant rules: % These view shifts in turn can be used to prove variants of the invariant rules:
% \begin{mathpar} % \begin{mathpar}
% \inferH{Auth} % \inferH{Auth}
% {\forall \melt_f.\; \hoare{\later\pred_\bot(a \mtimes \melt_f) * P}{\expr}{\Ret\val. \exists \meltB.\; \later\pred_\bot(\meltB\mtimes \melt_f) * Q}[\mask] % {\forall \melt_\f.\; \hoare{\later\pred_\bot(a \mtimes \melt_\f) * P}{\expr}{\Ret\val. \exists \meltB.\; \later\pred_\bot(\meltB\mtimes \melt_\f) * Q}[\mask]
% \and \physatomic{\expr}} % \and \physatomic{\expr}}
% {\Auth(M, \pred, \gname, \iname) \vdash \hoare{\ownGhost{\gname}{\authfrag a:\auth{M}} * P}{\expr}{\Ret\val. \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q}[\mask \uplus \{\iname\}]} % {\Auth(M, \pred, \gname, \iname) \vdash \hoare{\ownGhost{\gname}{\authfrag a:\auth{M}} * P}{\expr}{\Ret\val. \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q}[\mask \uplus \{\iname\}]}
% \and % \and
% \inferH{VSAuth} % \inferH{VSAuth}
% {\forall \melt_f.\; \later\pred_\bot(a \mtimes \melt_f) * P \vs[\mask_1][\mask_2] \exists \meltB.\; \later\pred_\bot(\meltB \mtimes \melt_f) * Q(\meltB)} % {\forall \melt_\f.\; \later\pred_\bot(a \mtimes \melt_\f) * P \vs[\mask_1][\mask_2] \exists \meltB.\; \later\pred_\bot(\meltB \mtimes \melt_\f) * Q(\meltB)}
% {\Auth(M, \pred, \gname, \iname) \vdash % {\Auth(M, \pred, \gname, \iname) \vdash
% \ownGhost{\gname}{\authfrag a:\auth{M}} * P \vs[\mask_1 \uplus \{\iname\}][\mask_2 \uplus \{\iname\}] % \ownGhost{\gname}{\authfrag a:\auth{M}} * P \vs[\mask_1 \uplus \{\iname\}][\mask_2 \uplus \{\iname\}]
% \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q(\meltB)} % \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q(\meltB)}
......
...@@ -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}
...@@ -221,7 +227,7 @@ ...@@ -221,7 +227,7 @@
\newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]} \newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]}
\newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]} \newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]}
\newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}} \newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}}
\newcommand{\ownM}[1]{\textlog{Own}(#1)}
\newcommand{\ownPhys}[1]{\textlog{Phy}(#1)} \newcommand{\ownPhys}[1]{\textlog{Phy}(#1)}