diff --git a/docs/algebra.tex b/docs/algebra.tex index a11f91ab16bbc0da21de589750ea7eba8527428f..7d18bfab11fffa712c8a9f00cba93acc84b6bd08 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -2,6 +2,7 @@ \subsection{COFE} +This definition varies slightly from the original one in~\cite{catlogic}. \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)$. \end{defn} @@ -22,6 +23,8 @@ An element $x \in \cofe$ of a COFE is called \emph{discrete} if $\All y \in \cofe. x \nequiv{0} y \Ra x = y$ 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} \begin{defn} @@ -30,6 +33,7 @@ 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)$ \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} 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 \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} @@ -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 {}$} \\ &\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\\ - \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{defn} @@ -117,7 +146,7 @@ This operation is needed to prove that $\later$ commutes with existential quanti \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 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$. \end{defn} diff --git a/docs/constructions.tex b/docs/constructions.tex index 834f29af760a7f156f148b11ed2feb9bff75bc43..dc3b643b3f7347ac7da9f3789e18ffd3080d27a5 100644 --- a/docs/constructions.tex +++ b/docs/constructions.tex @@ -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$. 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*} \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 } \\ @@ -33,7 +33,7 @@ We start by defining the COFE of \emph{step-indexed propositions}: \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. \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)} \end{align*} 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$. \subsection{Agreement} Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows: -\newcommand{\agc}{\mathrm{c}} % the "c" field of an agreement element -\newcommand{\agV}{\mathrm{V}} % the "V" field of an agreement element +\newcommand{\aginjc}{\mathrm{c}} % the "c" field of an agreement element +\newcommand{\aginjV}{\mathrm{V}} % the "V" field of an agreement element \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} \\ - \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 \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)) \\ - \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.\agV \land \All m \leq n. \melt.\agc(n) \nequiv{m} \melt.\agc(m) } \\ + \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.\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.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\ \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*} $\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)$. -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$? -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$. -We define an injection $\ag$ into $\agm(\cofe)$ as follows: -$\ag(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \mathbb{N}}$ +We define an injection $\aginj$ into $\agm(\cofe)$ as follows: +$\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: \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} \subsection{One-shot} @@ -115,17 +115,17 @@ 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*} - \mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\ - \mcore{\munit} \eqdef{}& \munit & \mcore{\bot} \eqdef{}& \bot -\end{align*} -\begin{align*} +\\%\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*} +\end{align*}% 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} @@ -149,33 +149,38 @@ We obtain the following frame-preserving updates: {\osshot(\melt) \mupd \setComp{\osshot(\meltB)}{\meltB \in \meltsB}} \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. -% Let $\exm{X}$ be the monoid with carrier $X \uplus \{ \munit \}$ and multiplication -% $-% \melt \cdot \meltB \;\eqdef\; -% \begin{cases} -% \melt & \mbox{if } \meltB = \munit \\ -% \meltB & \mbox{if } \melt = \munit -% \end{cases} -%$ +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) +\end{align*} +The remaining cases of composition go to $\bot$. +\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 -% \begin{mathpar} -% \inferH{ExUpd} -% {x \in X} -% {x \mupd \melt} -% \end{mathpar} -% is easily shown, as the only possible frame for $x$ is $\munit$. + \axiom{\munit \nequiv{n} \munit} + + \axiom{\bot \nequiv{n} \bot} +\end{mathpar} +$\exm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$. + +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} % 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: % \end{mathpar} % \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. % \end{proof} % The powerset monoids is cancellative. % \begin{proof}[Proof of cancellativity] -% 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$. -% 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$. +% 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$. +% 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$. % The other direction works the same way. % \end{proof} @@ -233,20 +238,20 @@ We obtain the following frame-preserving updates: % \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$. -% In the interesting case, we have $f = (q_f, a_f)$. -% Obtain $b$ such that $b \in B \land b \sep 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$. % Then $(q, b) \sep f$, and we are done. % \end{proof} % $\fracm{M}$ is cancellative if $M$ is cancellative. % \begin{proof}[Proof of cancellativitiy] -% If $\melt_f = \munit$, we are trivially done. -% So let $\melt_f = (q_f, \melt_f')$. +% If $\melt_\f = \munit$, we are trivially done. +% So let $\melt_\f = (q_\f, \melt_\f')$. % If $\melt = \munit$, then $\meltB = \munit$ as otherwise the fractions could not match up. % Again, we are trivially done. % Similar so for $\meltB = \munit$. % 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'$. % The first is trivial, the second follows from cancellativitiy of $M$. % \end{proof} @@ -307,7 +312,7 @@ We obtain the following frame-preserving updates: % The frame-preserving update involves a rather unwieldy side-condition: % \begin{mathpar} % \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 % }{ % \authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt' @@ -373,8 +378,6 @@ We obtain the following frame-preserving updates: % \subsection{STS with tokens monoid} % \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. % The construction follows the idea of STSs as described in CaReSL \cite{caresl}. @@ -389,11 +392,11 @@ We obtain the following frame-preserving updates: % We have % \begin{quote} % If $(s, T) \ra (s', T')$\\ -% and $T_f \sep (T \uplus \STSL(s))$,\\ -% then $\textsf{frame}(s, T_f) \ra \textsf{frame}(s', T_f)$. +% and $T_\f \sep (T \uplus \STSL(s))$,\\ +% then $\textsf{frame}(s, T_\f) \ra \textsf{frame}(s', T_\f)$. % \end{quote} % \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'$. % \end{proof} @@ -415,8 +418,8 @@ We obtain the following frame-preserving updates: % {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')} % \end{mathpar} % \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'$. -% By upward-closedness, it suffices to show $\textsf{frame}(s, T_f) \ststrans \textsf{frame}(s', T_f)$. +% 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)$. % This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step. % \end{proof} diff --git a/docs/derived.tex b/docs/derived.tex index aeb47ab448177b2dded70244a082c99247011ff4..55a0c06fef6b30fb87e521ffab457bf3aa5fbe73 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -205,9 +205,64 @@ The following rules can be derived for Hoare triples. \end{mathparpagebreakable} \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} @@ -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} \end{mathpar} +% TODO: These need syncing with Coq % \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}. @@ -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}}} % \and % \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 % \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} % These view shifts in turn can be used to prove variants of the invariant rules: % \begin{mathpar} % \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}} % {\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 % \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 % \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)} diff --git a/docs/iris.sty b/docs/iris.sty index 7f79af763272adc5cbf913fb5f135c28ae76deb2..8b0cb49dbdba6af5a63e593ca2d115031bb8dacf 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -86,13 +86,15 @@ \newcommand{\rs}{r} \newcommand{\rsB}{s} +\newcommand{\rss}{R} \newcommand{\pres}{\pi} \newcommand{\wld}{w} \newcommand{\ghostRes}{g} %% 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 @@ -114,6 +116,7 @@ \newcommand{\UPred}{\textdom{UPred}} \newcommand{\mProp}{\textdom{Prop}} % meta-level prop \newcommand{\iProp}{\textdom{iProp}} +\newcommand{\iPreProp}{\textdom{iPreProp}} \newcommand{\Wld}{\textdom{Wld}} \newcommand{\Res}{\textdom{Res}} @@ -121,6 +124,7 @@ \newcommand{\cofeB}{U} \newcommand{\COFEs}{\mathcal{U}} % category of COFEs \newcommand{\iFunc}{\Sigma} +\newcommand{\fix}{\textdom{fix}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS @@ -136,6 +140,8 @@ \newcommand{\melts}{A} \newcommand{\meltsB}{B} +\newcommand{\f}{\mathrm{f}} % for "frame" + \newcommand{\mcar}[1]{|#1|} \newcommand{\mcarp}[1]{\mcar{#1}^{+}} \newcommand{\munit}{\varepsilon} @@ -221,7 +227,7 @@ \newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]} \newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]} \newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}} - +\newcommand{\ownM}[1]{\textlog{Own}(#1)} \newcommand{\ownPhys}[1]{\textlog{Phy}(#1)} %% View Shifts @@ -286,7 +292,7 @@ %% Some commonly used identifiers \newcommand{\timeless}[1]{\textlog{timeless}(#1)} -\newcommand{\physatomic}[1]{\textlog{$#1$ phys.\ atomic}} +\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)} \newcommand{\infinite}{\textlog{infinite}} \newcommand{\Prop}{\textlog{Prop}} @@ -321,13 +327,14 @@ % Agreement \newcommand{\agm}{\ensuremath{\textmon{Ag}}} -\newcommand{\ag}{\textlog{ag}} +\newcommand{\aginj}{\textlog{ag}} % Fraction \newcommand{\fracm}{\ensuremath{\textmon{Frac}}} % Exclusive \newcommand{\exm}{\ensuremath{\textmon{Ex}}} +\newcommand{\exinj}{\textlog{ex}} % Auth \newcommand{\authm}{\textmon{Auth}} diff --git a/docs/iris.tex b/docs/iris.tex index eeb23de910e9e08f2700b8f4cbd40d5b47d5ab76..2b93d245aacf0d4d866797f74db895bd43eb5c4b 100644 --- a/docs/iris.tex +++ b/docs/iris.tex @@ -33,8 +33,8 @@ \endgroup\clearpage\begingroup \input{logic} \endgroup\clearpage\begingroup -%\input{model} -%\endgroup\clearpage\begingroup +\input{model} +\endgroup\clearpage\begingroup \input{derived} \endgroup\clearpage\begingroup \printbibliography diff --git a/docs/logic.tex b/docs/logic.tex index 9d89d639a1469635e9abc6b6b39b18b6112957a2..53ba97a9bab28ec15c0559d37efcb7828fa071ec 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -7,7 +7,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} \end{mathpar} \item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{\bot})$ We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\ - A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr'$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr'$ is forked off. + 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 @@ -16,7 +16,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and {{ \begin{inbox} -\All\expr_1, \state_1, \expr_2, \state_2, \expr'. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr' \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2 +\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} @@ -26,7 +26,7 @@ It does not matter whether they fork off an arbitrary expression. \begin{defn} An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if - $\Exists \expr_2, \state_2, \expr'. \expr,\state \step \expr_2,\state_2,\expr'$ + $\Exists \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f$ \end{defn} \begin{defn}[Context] @@ -35,9 +35,9 @@ It does not matter whether they fork off an arbitrary expression. \item $\lctx$ does not turn non-values into values:\\ $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ \item One can perform reductions below $\lctx$:\\ - $\All \expr_1, \state_1, \expr_2, \state_2, \expr'. \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr'$ + $\All \expr_1, \state_1, \expr_2, \state_2, \expr_\f. \expr_1, \state_1 \step \expr_2,\state_2,\expr_\f \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr_\f$ \item Reductions stay below $\lctx$ until there is a value in the hole:\\ - $\All \expr_1', \state_1, \expr_2, \state_2, \expr'. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr'$ + $\All \expr_1', \state_1, \expr_2, \state_2, \expr_\f. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr_\f \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr_\f$ \end{enumerate} \end{defn} @@ -54,9 +54,9 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. \cfg{\tpool'}{\state'}} \begin{mathpar} \infer - {\expr_1, \state_1 \step \expr_2, \state_2, \expr' \and \expr' \neq ()} + {\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \and \expr_\f \neq \bot} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step - \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr']}{\state'}} + \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_\f]}{\state'}} \and\infer {\expr_1, \state_1 \step \expr_2, \state_2} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step @@ -124,7 +124,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t \prop * \prop \mid \prop \wand \prop \mid \\& - \MU \var:\type. \pred \mid + \MU \var:\type. \term \mid \Exists \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 \pvs[\term][\term] \prop\mid \wpre{\term}[\term]{\Ret\var.\term} \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$. We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$. @@ -170,8 +170,6 @@ We introduce additional metavariables ranging over terms and generally let the c \] \paragraph{Variable conventions.} -We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}. -We omit type annotations in binders, when the type is clear from context. We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence. @@ -538,7 +536,7 @@ This is entirely standard. {\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop} \infer[pvs-mask-frame] -{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_f][\mask_2 \uplus \mask_f] \prop} +{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \prop} \infer[pvs-frame] {}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop} @@ -596,17 +594,19 @@ This is entirely standard. {\mask_2 \subseteq \mask_1 \and \toval(\expr_1) = \bot \and \red(\expr_1, \state_1) \and - \All \expr_2, \state_2, \expr'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \pred(\expr_2,\state_2,\expr')} - {\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr'. \pred(\expr_2, \state_2, \expr') \land \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \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)} + { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below... + ~~\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \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{inbox}} } \infer[wp-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'. \expr_1,\state_1 \step \expr_2,\state_2,\expr' \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr')} - {\later\All \expr_2, \expr'. \pred(\expr_2, \expr') \wand \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr'}[\top]{\Ret\var.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \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)} + {\later\All \expr_2, \expr_\f. \pred(\expr_2, \expr_\f) \Ra \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{mathpar} -Here we define $\wpre{\expr'}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr' = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression). +Here we define $\wpre{\expr_\f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_\f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression). \subsection{Adequacy} diff --git a/docs/model.tex b/docs/model.tex index 2a7fd7bc71354630fdc45237c9731c18a3fdf6fc..ea2a89bdc89af2ed6f544bbb4c4a4a10d29c5add 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -1,528 +1,208 @@ \section{Model and semantics} -\ralf{What also needs to be done here: Define uPred and its later function; define black later; define the resource CMRA} - The semantics closely follows the ideas laid out in~\cite{catlogic}. -We just repeat some of the most important definitions here. -An \emph{ordered family of equivalence relations} (o.f.e.\@) is a pair -$(X,(\nequiv{n})_{n\in\mathbb{N}})$, with $X$ a set, and each $\nequiv{n}$ -an equivalence relation over $X$ satisfying -\begin{itemize} - \item $\All x,x'. x \nequiv{0} x',$ - \item $\All x,x',n. x \nequiv{n+1} x' \implies x \nequiv{n} x',$ - \item $\All x,x'. (\All n. x\nequiv{n} x') \implies x = x'.$ -\end{itemize} -\a -Let $(X,(\nequivset{n}{X})_{n\in\mathbb{N}})$ and -$(Y,(\nequivset{n}{Y})_{n\in\mathbb{N}})$ be o.f.e.'s. A function $f: -X\to Y$ is \emph{non-expansive} if, for all $x$, $x'$ and $n$, -$-x \nequivset{n}{X} x' \implies -fx \nequivset{n}{Y} f x'. -$ -Let $(X,(\nequiv{n})_{n\in\mathbb{N}})$ be an o.f.e. -A sequence $(x_i)_{i\in\mathbb{N}}$ of elements in $X$ is a -\emph{chain} (aka \emph{Cauchy sequence}) if -$-\All k. \Exists n. \All i,j\geq n. x_i \nequiv{k} x_j. -$ -A \emph{limit} of a chain $(x_i)_{i\in\mathbb{N}}$ is an element -$x\in X$ such that -$-\All n. \Exists k. \All i\geq k. x_i \nequiv{n} x. -$ -An o.f.e.\ $(X,(\nequiv{n})_{n\in\mathbb{N}})$ is \emph{complete} -if all chains have a limit. -A complete o.f.e.\ is called a c.o.f.e.\ (pronounced coffee''). -When the family of equivalence relations is clear from context we -simply -write $X$ for a c.o.f.e.\ $(X,(\nequiv{n})_{n\in\mathbb{N}})$. +\subsection{Generic model of base logic} +\label{sec:upred-logic} +The base logic including equality, later, always, and a notion of ownership is defined on $\UPred(\monoid)$ for any CMRA $\monoid$. -Let $\cal U$ be the category of c.o.f.e.'s and nonexpansive maps. - -Products and function spaces are defined as follows. -For c.o.f.e.'s $(X,(\nequivset{n}{X})_{n\in\mathbb{N}})$ and -$(Y,(\nequivset{n}{Y})_{n\in\mathbb{N}})$, their product -is -$(X\times Y, (\nequiv{n})_{n\in\mathbb{N}}),$ -where -$-(x,y) \nequiv{n} (x',y') \iff -x \nequiv{n} x' \land -y \nequiv{n} y'. -$ -The function space is -$-(\{\, f : X\to Y \mid f \text{ is non-expansive}\,\}, (\nequiv{n})_{n\in\mathbb{N}}), -$ -where -$-f \nequiv{n} g \iff -\All x. f(x) \nequiv{n} g(x). -$ - -For a c.o.f.e.\ $(X,(\nequiv{n}_{n\in\mathbb{N}}))$, -$\latert (X,(\nequiv{n}_{n\in\mathbb{N}}))$ is the c.o.f.e.\@ -$(X,(\nequivB{n}_{n\in\mathbb{N}}))$, where -$-x \nequivB{n} x' \iff \begin{cases} -\top &\IF n=0 \\ -x \nequiv{n-1} x' &\IF n>0 -\end{cases} -$ - -(Sidenote: $\latert$ extends to a functor on $\cal U$ by the identity -action on morphisms). - - -\subsection{Semantic structures: propositions} -\ralf{This needs to be synced with the Coq development again.} - -$-\begin{array}[t]{rcl} -% \protStatus &::=& \enabled \ALT \disabled \\[0.4em] -\textdom{Res} &\eqdef& -\{\, \rs = (\pres, \ghostRes) \mid -\pres \in \textdom{State} \uplus \{\munit\} \land \ghostRes \in \mcarp{\monoid} \,\} \\[0.5em] -(\pres, \ghostRes) \rtimes -(\pres', \ghostRes') &\eqdef& -\begin{cases} -(\pres, \ghostRes \mtimes \ghostRes') & \mbox{if \pres' = \munit and \ghostRes \mtimes \ghostRes' \neq \mzero} \\ -(\pres', \ghostRes \mtimes \ghostRes') & \mbox{if \pres = \munit and \ghostRes \mtimes \ghostRes' \neq \mzero} -\end{cases} -\\[0.5em] -% -\rs \leq \rs' & \eqdef & -\Exists \rs''. \rs' = \rs \rtimes \rs''\\[1em] -% -\UPred(\textdom{Res}) &\eqdef& -\{\, p \subseteq \mathbb{N} \times \textdom{Res} \mid -\All (k,\rs) \in p. -\All j\leq k. -\All \rs' \geq \rs. -(j,\rs')\in p \,\}\\[0.5em] -\restr{p}{k} &\eqdef& -\{\, (j, \rs) \in p \mid j < k \,\}\\[0.5em] -p \nequiv{n} q & \eqdef & \restr{p}{n} = \restr{q}{n}\\[1em] -% -\textdom{PreProp} & \cong & -\latert\big( \textdom{World} \monra \UPred(\textdom{Res}) -\big)\\[0.5em] -% -\textdom{World} & \eqdef & -\mathbb{N} \fpfn \textdom{PreProp}\\[0.5em] -% -w \nequiv{n} w' & \eqdef & -n = 0 \lor -\bigl(\dom(w) = \dom(w') \land \All i\in\dom(w). w(i) \nequiv{n} w'(i)\bigr) -\\[0.5em] -% -w \leq w' & \eqdef & -\dom(w) \subseteq \dom(w') \land \All i \in \dom(w). w(i) = w'(i) -\\[0.5em] -% -\textdom{Prop} & \eqdef & \textdom{World} \monra \UPred(\textdom{Res}) -\end{array} -$ +\typedsection{Interpretation of base assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \UPred(\monoid)} +Remember that $\UPred(\monoid)$ is isomorphic to $\monoid \monra \SProp$. +We are thus going to define the assertions as mapping CMRA elements to sets of step-indices. -For $p,q\in\UPred(\textdom{Res})$ with $p \nequiv{n} q$ defined -as above, $\UPred(\textdom{Res})$ is a -c.o.f.e. +We introduce an additional logical connective $\ownM\melt$, which will later be used to encode all of $\knowInv\iname\prop$, $\ownGGhost\melt$ and $\ownPhys\state$. -$\textdom{Prop}$ is a c.o.f.e., which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89}. -We do not need to consider how the object is constructed. -We only need the isomorphism, given by maps \begin{align*} - \wIso &: \latert \bigl(World \monra \UPred(\textdom{Res})\bigr) \to \textdom{PreProp} \\ - \wIso^{-1} &: \textdom{PreProp} \to \latert \bigl(World \monra \UPred(\textdom{Res})\bigr) + \Sem{\vctx \proves t =_\type u : \Prop}_\gamma &\eqdef + \Lam \any. \setComp{n}{\Sem{\vctx \proves t : \type}_\gamma \nequiv{n} \Sem{\vctx \proves u : \type}_\gamma} \\ + \Sem{\vctx \proves \FALSE : \Prop}_\gamma &\eqdef \Lam \any. \emptyset \\ + \Sem{\vctx \proves \TRUE : \Prop}_\gamma &\eqdef \Lam \any. \mathbb{N} \\ + \Sem{\vctx \proves \prop \land \propB : \Prop}_\gamma &\eqdef + \Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cap \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\ + \Sem{\vctx \proves \prop \lor \propB : \Prop}_\gamma &\eqdef + \Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cup \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\ + \Sem{\vctx \proves \prop \Ra \propB : \Prop}_\gamma &\eqdef + \Lam \melt. \setComp{n}{\begin{aligned} + \All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\ + & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt)\end{aligned}}\\ + \Sem{\vctx \proves \All x : \type. \prop : \Prop}_\gamma &\eqdef + \Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\ + \Sem{\vctx \proves \Exists x : \type. \prop : \Prop}_\gamma &\eqdef + \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\ + ~\\ + \Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\ + \Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\ + \Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}\Exists \meltB_1, \meltB_2. &\melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \land {}\\& n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB_1) \land n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB_2)\end{aligned}} +\\ + \Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &\eqdef + \Lam \melt. \setComp{n}{\begin{aligned} + \All m, \meltB.& m \leq n \land \melt\mtimes\meltB \in \mval_m \Ra {} \\ + & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\ + \Sem{\vctx \proves \ownM{\melt} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\melt \mincl[n] \meltB} \\ + \Sem{\vctx \proves \mval(\melt) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\melt \in \mval_n} \\ \end{align*} -which are inverses to each other. -Note: this is an isomorphism in $\cal U$, i.e., $\wIso$ and -$\wIso^{-1}$ are both non-expansive. -$\textdom{World}$ is a c.o.f.e.\ with the family of equivalence -relations defined as shown above. +For every definition, we have to show all the side-conditions: The maps have to be non-expansive and monotone. -\subsection{Semantic structures: types and environments} -For a set $X$, write $\Delta X$ for the discrete c.o.f.e.\ with $x \nequiv{n} -x'$ iff $n = 0$ or $x = x'$ -$-\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -\Sem{\textsort{Unit}} &\eqdef& \Delta \{ \star \} \\ -\Sem{\textsort{InvName}} &\eqdef& \Delta \mathbb{N} \\ -\Sem{\textsort{InvMask}} &\eqdef& \Delta \pset{\mathbb{N}} \\ -\Sem{\textsort{Monoid}} &\eqdef& \Delta |\monoid| -\end{array} -\qquad\qquad -\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -\Sem{\textsort{Val}} &\eqdef& \Delta \textdom{Val} \\ -\Sem{\textsort{Exp}} &\eqdef& \Delta \textdom{Exp} \\ -\Sem{\textsort{Ectx}} &\eqdef& \Delta \textdom{Ectx} \\ -\Sem{\textsort{State}} &\eqdef& \Delta \textdom{State} \\ -\end{array} -\qquad\qquad -\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} -\Sem{\sort \times \sort'} &\eqdef& \Sem{\sort} \times \Sem{\sort} \\ -\Sem{\sort \to \sort'} &\eqdef& \Sem{\sort} \to \Sem{\sort} \\ -\Sem{\Prop} &\eqdef& \textdom{Prop} \\ -\end{array} -$ - -The balance of our signature $\Sig$ is interpreted as follows. -For each base type $\type$ not covered by the preceding table, we pick an object $X_\type$ in $\cal U$ and define -$-\Sem{\type} \eqdef X_\type -$ -For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$, we pick an arrow $\Sem{\sigfn} : \Sem{\type_1} \times \dots \times \Sem{\type_n} \to \Sem{\type_{n+1}}$ in $\cal U$. - -An environment $\vctx$ is interpreted as the set of -maps $\rho$, with $\dom(\rho) = \dom(\vctx)$ and -$\rho(x)\in\Sem{\vctx(x)}$, -and -$\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land -\All x\in\dom(\rho). \rho(x) \nequiv{n} \rho'(x)\bigr)$. - -\ralf{Re-check all the following definitions with the Coq development.} -%\typedsection{Validity}{valid : \pset{\textdom{Prop}} \in Sets} -% -%\begin{align*} -%valid(p) &\iff \All n \in \mathbb{N}. \All \rs \in \textdom{Res}. \All W \in \textdom{World}. (n, \rs) \in p(W) -%\end{align*} - -\typedsection{Later modality}{\later : \textdom{Prop} \to \textdom{Prop} \in {\cal U}} +\subsection{Iris model} +\paragraph{Semantic domain of assertions.} +The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$. +We start by defining the functor that assembles the CMRAs we need to the global resource CMRA: \begin{align*} - \later p &\eqdef \Lam W. \{\, (n + 1, r) \mid (n, r) \in p(W) \,\} \cup \{\, (0, r) \mid r \in \textdom{Res} \,\} + \textdom{ResF}(\cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: F(\cofe)} \end{align*} -\begin{lem} - $\later{}$ is well-defined: $\later {p}$ is a valid proposition (this amounts to showing non-expansiveness), and $\later{}$ itself is a \emph{contractive} map. -\end{lem} - -\typedsection{Always modality}{\always{} : \textdom{Prop} \to \textdom{Prop} \in {\cal U}} +where $F$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$. +$\textdom{ResF}(\cofe)$ is a CMRA by lifting the individual CMRAs pointwise. +Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$. +Now we can write down the recursive domain equation: +$\iPreProp \cong \UPred(\textdom{ResF}(\iPreProp))$ +$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89}. +We do not need to consider how the object is constructed. +We only need the isomorphism, given by \begin{align*} - \always{p} \eqdef \Lam W. \{\, (n, r) \mid (n, \munit) \in p(W) \,\} + \Res &\eqdef \textdom{ResF}(\iPreProp) \\ + \iProp &\eqdef \UPred(\Res) \\ + \wIso &: \iProp \nfn \iPreProp \\ + \wIso^{-1} &: \iPreProp \nfn \iProp \end{align*} -\begin{lem} - $\always{}$ is well-defined: $\always{p}$ is a valid proposition (this amounts to showing non-expansiveness), and $\always{}$ itself is a non-expansive map. -\end{lem} -% PDS: p \Rightarrow q not defined. -%\begin{lem}\label{lem:always-impl-valid} -%\begin{align*} -%&\forall p, q \in \textdom{Prop}.~\\ -%&\qquad -% (\forall n \in \mathbb{N}.~\forall \rs \in \textdom{Res}.~\forall W \in \textdom{World}.~(n, \rs) \in p(W) \Rightarrow (n, \rs) \in q(W)) \Leftrightarrow~valid(\always{(p \Rightarrow q)}) -%\end{align*} -%\end{lem} +We then pick $\iProp$ as the interpretation of $\Prop$: +$\Sem{\Prop} \eqdef \iProp$ + + +\paragraph{Interpretation of assertions.} +$\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply. +We only have to define the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions. -\typedsection{Invariant definition}{inv : \Delta(\mathbb{N}) \times \textdom{Prop} \to \textdom{Prop} \in {\cal U}} +\typedsection{World satisfaction}{\wsat{-}{-}{-} : + \Delta\textdom{State} \times + \Delta\pset{\mathbb{N}} \times + \textdom{Res} \nfn \SProp } \begin{align*} - \mathit{inv}(\iota, p) &\eqdef \Lam W. \{\, (n, r) \mid \iota\in\dom(W) \land W(\iota) \nequiv{n+1}_{\textdom{PreProp}} \wIso(p) \,\} + \wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t] + \rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land + \dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\ + \All\iname \in \mask, \prop. \rs.\wld(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname)) + \end{inbox}\\ + \wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))} \end{align*} -\begin{lem} - $\mathit{inv}$ is well-defined: $\mathit{inv}(\iota, p)$ is a valid proposition (this amounts to showing non-expansiveness), and $\mathit{inv}$ itself is a non-expansive map. -\end{lem} -\typedsection{World satisfaction}{\wsat{-}{-}{-}{-} : - \textdom{State} \times - \pset{\mathbb{N}} \times - \textdom{Res} \times - \textdom{World} \to \psetdown{\mathbb{N}} \in {\cal U}} -\ralf{Make this Dave-compatible: Explicitly compose all the things in $s$} +\typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp} \begin{align*} - \wsat{\state}{\mask}{\rs}{W} &= - \begin{aligned}[t] - \{\, n + 1 \in \mathbb{N} \mid &\Exists \rsB:\mathbb{N} \fpfn \textdom{Res}. (\rs \rtimes \rsB).\pres = \state \land{}\\ - &\quad \All \iota \in \dom(W). \iota \in \dom(W) \leftrightarrow \iota \in \dom(\rsB) \land {}\\ - &\quad\quad \iota \in \mask \ra (n, \rsB(\iota)) \in \wIso^{-1}(W(\iota))(W) \,\} \cup \{ 0 \} - \end{aligned} + \mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned} + \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \sep \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\& + \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f} + \end{aligned}} \end{align*} -\begin{lem}\label{lem:fullsat-nonexpansive} - $\wsat{-}{-}{-}{-}$ is well-defined: It maps into $\psetdown{\mathbb{N}}$. (There is no need for it to be a non-expansive map, it doesn't itself live in $\cal U$.) -\end{lem} -\begin{lem}\label{lem:fullsat-weaken-mask} - \begin{align*} - \MoveEqLeft - \All \state \in \Delta(\textdom{State}). - \All \mask_1, \mask_2 \in \Delta(\pset{\mathbb{N}}). - \All \rs, \rsB \in \Delta(\textdom{Res}). - \All W \in \textdom{World}. \\& - \mask_1 \subseteq \mask_2 \implies (\wsat{\state}{\mask_2}{\rs}{W}) \subseteq (\wsat{\state}{\mask_1}{\rs}{W}) - \end{align*} -\end{lem} - -\begin{lem}\label{lem:nequal_ext_world} - \begin{align*} - & - \All n \in \mathbb{N}. - \All W_1, W_1', W_2 \in \textdom{World}. - W_1 \nequiv{n} W_2 \land W_1 \leq W_1' \implies \Exists W_2' \in \textdom{World}. W_1' \nequiv{n} W_2' \land W_2 \leq W_2' - \end{align*} -\end{lem} - -\typedsection{Timeless}{\textit{timeless} : \textdom{Prop} \to \textdom{Prop}} +\typedsection{Weakest precondition}{\mathit{wp}_{-}(-, -) : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp} +$\textdom{wp}$ is defined as the fixed-point of a contractive function. \begin{align*} - \textit{timeless}(p) \eqdef - \begin{aligned}[t] - \Lam W. - \{\, (n, r) &\mid \All W' \geq W. \All k \leq n. \All r' \in \textdom{Res}. \\ - &\qquad - k > 0 \land (k - 1, r') \in p(W') \implies (k, r') \in p(W') \,\} - \end{aligned} + \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned} + \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \sep \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\ + &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\ + &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\ + &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\ + &\qquad\qquad (\expr_\f = \bot \lor m \in \textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2)) + \end{aligned}} \\ + \textdom{wp}_\mask(\expr, \pred) &\eqdef \mathit{fix}(\textdom{pre-wp})(\mask, \expr, \pred) \end{align*} -\begin{lem} - \textit{timeless} is well-defined: \textit{timeless}(p) is a valid proposition, and \textit{timeless} itself is a non-expansive map. -\end{lem} -% PDS: \Ra undefined. -%\begin{lem} -%\begin{align*} -%& -% \All p \in \textdom{Prop}. -% \All \mask \in \pset{\mathbb{N}}. -%valid(\textit{timeless}(p) \Ra (\later p \vs[\mask][\mask] p)) -%\end{align*} -%\end{lem} +\typedsection{Interpretation of program logic assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \iProp} -\typedsection{View-shift}{\mathit{vs} : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \textdom{Prop} \to \textdom{Prop} \in {\cal U}} \begin{align*} - \mathit{vs}_{\mask_1}^{\mask_2}(q) &= \Lam W. - \begin{aligned}[t] - \{\, (n, \rs) &\mid \All W_F \geq W. \All \rs_F, \mask_F, \state. \All k \leq n.\\ - &\qquad - k \in (\wsat{\state}{\mask_1 \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\ - &\qquad - \Exists W' \geq W_F. \Exists \rs'. k \in (\wsat{\state}{\mask_2 \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(W') - \,\} - \end{aligned} + \Sem{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &\eqdef \ownM{[\iname \mapsto \aginj(\latertinj(\wIso(\prop)))], \munit, \munit} \\ + \Sem{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &\eqdef \ownM{\munit, \munit, \melt} \\ + \Sem{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &\eqdef \ownM{\munit, \exinj(\state), \munit} \\ + \Sem{\vctx \proves \pvs[\mask_1][\mask_2] \prop : \Prop}_\gamma &\eqdef + \textdom{pvs}^{\Sem{\vctx \proves \mask_2 : \textlog{InvMask}}_\gamma}_{\Sem{\vctx \proves \mask_1 : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \\ + \Sem{\vctx \proves \wpre{\expr}[\mask]{\Ret\var.\prop} : \Prop}_\gamma &\eqdef + \textdom{wp}_{\Sem{\vctx \proves \mask : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \expr : \textlog{Expr}}_\gamma, \Lam\val. \Sem{\vctx \proves \prop : \Prop}_{\gamma[\var\mapsto\val]}) \end{align*} -\begin{lem} - $\mathit{vs}$ is well-defined: $\mathit{vs}_{\mask_1}^{\mask_2}(q)$ is a valid proposition, and $\mathit{vs}$ is a non-expansive map. -\end{lem} - - -%\begin{lem}\label{lem:prim_view_shift_trans} -%\begin{align*} -%\MoveEqLeft -% \All \mask_1, \mask_2, \mask_3 \in \Delta(\pset{\mathbb{N}}). -% \All p, q \in \textdom{Prop}. \All W \in \textdom{World}. -% \All n \in \mathbb{N}.\\ -%& -% \mask_2 \subseteq \mask_1 \cup \mask_3 \land -% \bigl(\All W' \geq W. \All r \in \textdom{Res}. \All k \leq n. (k, r) \in p(W') \implies (k, r) \in vs_{\mask_2}^{\mask_3}(q)(W')\bigr) \\ -%&\qquad -% {}\implies \All r \in \textdom{Res}. (n, r) \in vs_{\mask_1}^{\mask_2}(p)(W) \implies (n, r) \in vs_{\mask_1}^{\mask_3}(q)(W) -%\end{align*} -%\end{lem} - -% PDS: E_1 ==>> E_2 undefined. -%\begin{lem} -%\begin{align*} -%& -% \forall \mask_1, \mask_2, \mask_3 \in \Delta(\pset{\mathbb{N}}).~ -% \forall p_1, p_2, p_3 \in \textdom{Prop}.~\\ -%&\qquad -% \mask_2 \subseteq \mask_1 \cup \mask_3 \Rightarrow -% valid(((p_1 \vs[\mask_1][\mask_2] p_2) \land (p_2 \vs[\mask_2][\mask_3] p_3)) \Rightarrow (p_1 \vs[\mask_1][\mask_3] p_3)) -%\end{align*} -%\end{lem} - -%\begin{lem} -%\begin{align*} -%\MoveEqLeft -% \All \iota \in \mathbb{N}. -% \All p \in \textdom{Prop}. -% \All W \in \textdom{World}. -% \All \rs \in \textdom{Res}. -% \All n \in \mathbb{N}. \\ -%& -% (n, \rs) \in inv(\iota, p)(W) \implies (n, \rs) \in vs_{\{ \iota \}}^{\emptyset}(\later p)(W) -%\end{align*} -%\end{lem} -% PDS: * undefined. -%\begin{lem} -%\begin{align*} -%& -% \forall \iota \in \mathbb{N}.~ -% \forall p \in \textdom{Prop}.~ -% \forall W \in \textdom{World}.~ -% \forall \rs \in \textdom{Res}.~ -% \forall n \in \mathbb{N}.~\\ -%&\qquad -% (n, \rs) \in (inv(\iota, p) * \later p)(W) \Rightarrow (n, \rs) \in vs^{\{ \iota \}}_{\emptyset}(\top)(W) -%\end{align*} -%\end{lem} +\paragraph{Remaining semantic domains, and interpretation of non-assertion terms.} -% \begin{lem} -% \begin{align*} -% & -% \forall \mask_1, \mask_2 \in \Delta(\pset{\mathbb{N}}).~ -% valid(\bot \vs[\mask_1][\mask_2] \bot) -% \end{align*} -% \end{lem} - -% PDS: E_1 ==>> E_2 undefined. -%\begin{lem} -%\begin{align*} -%& -% \forall p, q \in \textdom{Prop}.~ -% \forall \mask \in \pset{\mathbb{N}}.~ -%valid(\always{(p \Rightarrow q)} \Rightarrow (p \vs[\mask][\mask] q)) -%\end{align*} -%\end{lem} - -% PDS: E # E' and E_1 ==>> E_2 undefined. -%\begin{lem} -%\begin{align*} -%& -% \forall p_1, p_2, p_3 \in \textdom{Prop}.~ -% \forall \mask_1, \mask_2, \mask \in \pset{\mathbb{N}}.~ -%valid(\mask \sep \mask_1 \Ra \mask \sep \mask_2 \Ra (p_1 \vs[\mask_1][\mask_2] p_2) \Rightarrow (p_1 * p_3 \vs[\mask_1 \cup \mask][\mask_2 \cup \mask] p_2 * p_3)) -%\end{align*} -%\end{lem} - -\typedsection{Weakest precondition}{\mathit{wp} : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \to \textdom{Prop}) \to \textdom{Prop} \in {\cal U}} - -% \begin{align*} -% \mathit{wp}_\mask(\expr, q) &\eqdef \Lam W. -% \begin{aligned}[t] -% \{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\wsat{\state}{\mask \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \implies{}\\ -% &\qquad -% (\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \rs'. \\ -% &\qquad\qquad -% k \in (\wsat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\ -% &\qquad -% (\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \rs'. \\ -% &\qquad\qquad -% k - 1 \in (\wsat{\state'}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\ -% &\qquad -% (\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \rs', \rs_1', \rs_2'. \\ -% &\qquad\qquad -% k - 1 \in (\wsat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land \rs' = \rs_1' \rtimes \rs_2'~\land \\ -% &\qquad\qquad -% (k-1, \rs_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land -% (k-1, \rs_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W')) -% \,\} -% \end{aligned} -% \end{align*} -\begin{lem} - $\mathit{wp}$ is well-defined: $\mathit{wp}_{\mask}(\expr, q)$ is a valid proposition, and $\mathit{wp}$ is a non-expansive map. Besides, the dependency on the recursive occurrence is contractive, so $\mathit{wp}$ has a fixed-point. -\end{lem} - -\begin{lem} - $\mathit{wp}$ on values and non-mask-changing $\mathit{vs}$ agree: - $\mathit{wp}_\mask(\val, q) = \mathit{vs}_{\mask}^{\mask}(q \: \val)$ -\end{lem} - -\typedsection{Interpretation of terms}{\Sem{\vctx \proves \term : \sort} : \Sem{\vctx} \to \Sem{\sort} \in {\cal U}} +The remaining domains are interpreted as follows: +$+\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} +\Sem{\textlog{InvName}} &\eqdef& \Delta \mathbb{N} \\ +\Sem{\textlog{InvMask}} &\eqdef& \Delta \pset{\mathbb{N}} \\ +\Sem{\textlog{M}} &\eqdef& F(\iProp) +\end{array} +\qquad\qquad +\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} +\Sem{\textlog{Val}} &\eqdef& \Delta \textdom{Val} \\ +\Sem{\textlog{Expr}} &\eqdef& \Delta \textdom{Expr} \\ +\Sem{\textlog{State}} &\eqdef& \Delta \textdom{State} \\ +\end{array} +\qquad\qquad +\begin{array}[t]{@{}l@{\ }c@{\ }l@{}} +\Sem{1} &\eqdef& \Delta \{ () \} \\ +\Sem{\type \times \type'} &\eqdef& \Sem{\type} \times \Sem{\type} \\ +\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\ +\end{array} +$ -%A term $\vctx \proves \term : \sort$ is interpreted as a non-expansive map from $\Sem{\vctx}$ to $\Sem{\sort}$. +The balance of our signature $\Sig$ is interpreted as follows. +For each base type $\type$ not covered by the preceding table, we pick an object $X_\type$ in $\cal U$ and define +$+\Sem{\type} \eqdef X_\type +$ +For each function symbol $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$, we pick a function $\Sem{\sigfn} : \Sem{\type_1} \times \dots \times \Sem{\type_n} \nfn \Sem{\type_{n+1}}$. +\typedsection{Interpretation of non-propositional terms}{\Sem{\vctx \proves \term : \type} : \Sem{\vctx} \nfn \Sem{\type}} \begin{align*} - \Sem{\vctx \proves x : \sort}_\gamma &= \gamma(x) \\ - \Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &= \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \ \WHEN \sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn \\ - \Sem{\vctx \proves \Lam x. \term : \sort \to \sort'}_\gamma &= - \Lam v : \Sem{\sort}. \Sem{\vctx, x : \sort \proves \term : \sort'}_{\gamma[x \mapsto v]} \\ - \Sem{\vctx \proves \term~\termB : \sort'}_\gamma &= - \Sem{\vctx \proves \term : \sort \to \sort'}_\gamma(\Sem{\vctx \proves \termB : \sort}_\gamma) \\ - \Sem{\vctx \proves \unitval : \unitsort}_\gamma &= \star \\ - \Sem{\vctx \proves (\term_1, \term_2) : \sort_1 \times \sort_2}_\gamma &= (\Sem{\vctx \proves \term_1 : \sort_1}_\gamma, \Sem{\vctx \proves \term_2 : \sort_2}_\gamma) \\ - \Sem{\vctx \proves \pi_i~\term : \sort_1}_\gamma &= \pi_i(\Sem{\vctx \proves \term : \sort_1 \times \sort_2}_\gamma) -\end{align*} -% -\begin{align*} - \Sem{\vctx \proves \mzero : \textsort{Monoid}}_\gamma &= \mzero \\ - \Sem{\vctx \proves \munit : \textsort{Monoid}}_\gamma &= \munit \\ - \Sem{\vctx \proves \melt \mtimes \meltB : \textsort{Monoid}}_\gamma &= - \Sem{\vctx \proves \melt : \textsort{Monoid}}_\gamma \mtimes \Sem{\vctx \proves \meltB : \textsort{Monoid}}_\gamma + \Sem{\vctx \proves x : \type}_\gamma &\eqdef \gamma(x) \\ + \Sem{\vctx \proves \sigfn(\term_1, \dots, \term_n) : \type_{n+1}}_\gamma &\eqdef \Sem{\sigfn}(\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \dots, \Sem{\vctx \proves \term_n : \type_n}_\gamma) \\ + \Sem{\vctx \proves \Lam \var:\type. \term : \type \to \type'}_\gamma &\eqdef + \Lam \termB : \Sem{\type}. \Sem{\vctx, \var : \type \proves \term : \type}_{\gamma[\var \mapsto \termB]} \\ + \Sem{\vctx \proves \term(\termB) : \type'}_\gamma &\eqdef + \Sem{\vctx \proves \term : \type \to \type'}_\gamma(\Sem{\vctx \proves \termB : \type}_\gamma) \\ + \Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef + \mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\gamma[x \mapsto \termB]}) \\ + ~\\ + \Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\ + \Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\ + \Sem{\vctx \proves \pi_i(\term) : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\ + ~\\ + \Sem{\vctx \proves \munit : \textlog{M}}_\gamma &\eqdef \munit \\ + \Sem{\vctx \proves \mcore\melt : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \melt : \textlog{M}}_\gamma} \\ + \Sem{\vctx \proves \melt \mtimes \meltB : \textlog{M}}_\gamma &\eqdef + \Sem{\vctx \proves \melt : \textlog{M}}_\gamma \mtimes \Sem{\vctx \proves \meltB : \textlog{M}}_\gamma \end{align*} % -\begin{align*} - \Sem{\vctx \proves t =_\sort u : \Prop}_\gamma &= - \Lam W. \{\, (n, r) \mid \Sem{\vctx \proves t : \sort}_\gamma \nequiv{n+1} \Sem{\vctx \proves u : \sort}_\gamma \,\} \\ - \Sem{\vctx \proves \FALSE : \Prop}_\gamma &= \Lam W. \emptyset \\ - \Sem{\vctx \proves \TRUE : \Prop}_\gamma &= \Lam W. \mathbb{N} \times \textdom{Res} \\ - \Sem{\vctx \proves P \land Q : \Prop}_\gamma &= - \Lam W. \Sem{\vctx \proves P : \Prop}_\gamma(W) \cap \Sem{\vctx \proves Q : \Prop}_\gamma(W) \\ - \Sem{\vctx \proves P \lor Q : \Prop}_\gamma &= - \Lam W. \Sem{\vctx \proves P : \Prop}_\gamma(W) \cup \Sem{\vctx \proves Q : \Prop}_\gamma(W) \\ - \Sem{\vctx \proves P \Ra Q : \Prop}_\gamma &= - \Lam W. \begin{aligned}[t] - \{\, (n, r) &\mid \All n' \leq n. \All W' \geq W. \All r' \geq r. \\ - &\qquad - (n', r') \in \Sem{\vctx \proves P : \Prop}_\gamma(W')~ \\ - &\qquad - \implies (n', r') \in \Sem{\vctx \proves Q : \Prop}_\gamma(W') \,\} - \end{aligned} \\ - \Sem{\vctx \proves \All x : \sort. P : \Prop}_\gamma &= - \Lam W. \{\, (n, r) \mid \All v \in \Sem{\sort}. (n, r) \in \Sem{\vctx, x : \sort \proves P : \Prop}_{\gamma[x \mapsto v]}(W) \,\} \\ - \Sem{\vctx \proves \Exists x : \sort. P : \Prop}_\gamma &= - \Lam W. \{\, (n, r) \mid \Exists v \in \Sem{\sort}. (n, r) \in \Sem{\vctx, x : \sort \proves P : \Prop}_{\gamma[x \mapsto v]}(W) \,\} -\end{align*} -% -\begin{align*} - \Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &= \always{\Sem{\vctx \proves \prop : \Prop}_\gamma} \\ - \Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &= \later \Sem{\vctx \proves \prop : \Prop}_\gamma\\ - \Sem{\vctx \proves \MU x. \pred : \sort \to \Prop}_\gamma &= - \mathit{fix}(\Lam v : \Sem{\sort \to \Prop}. \Sem{\vctx, x : \sort \to \Prop \proves \pred : \sort \to \Prop}_{\gamma[x \mapsto v]}) \\ - \Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &= - \begin{aligned}[t] - \Lam W. \{\, (n, r) &\mid \Exists r_1, r_2. r = r_1 \bullet r_2 \land{} \\ - &\qquad - (n, r_1) \in \Sem{\vctx \proves \prop : \Prop}_\gamma \land{} \\ - &\qquad - (n, r_2) \in \Sem{\vctx \proves \propB : \Prop}_\gamma \,\} - \end{aligned} \\ - \Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &= - \begin{aligned}[t] - \Lam W. \{\, (n, r) &\mid \All n' \leq n. \All W' \geq W. \All r'. \\ - &\qquad - (n', r') \in \Sem{\vctx \proves \prop : \Prop}_\gamma(W') \land r \sep r' \\ - &\qquad - \implies (n', r \bullet r') \in \Sem{\vctx \proves \propB : \Prop}_\gamma(W') - \} - \end{aligned} \\ - \Sem{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &= - inv(\Sem{\vctx \proves \iname : \textsort{InvName}}_\gamma, \Sem{\vctx \proves \prop : \Prop}_\gamma) \\ - \Sem{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &= - \Lam W. \{\, (n, \rs) \mid \rs.\ghostRes \geq \Sem{\vctx \proves \melt : \textsort{Monoid}}_\gamma \,\} \\ - \Sem{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &= - \Lam W. \{\, (n, \rs) \mid \rs.\pres = \Sem{\vctx \proves \state : \textsort{State}}_\gamma \,\} -\end{align*} -% -\begin{align*} - \Sem{\vctx \proves \pvsA{\prop}{\mask_1}{\mask_2} : \Prop}_\gamma &= - \textdom{vs}^{\Sem{\vctx \proves \mask_2 : \textsort{InvMask}}_\gamma}_{\Sem{\vctx \proves \mask_1 : \textsort{InvMask}}_\gamma}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \\ - \Sem{\vctx \proves \dynA{\expr}{\pred}{\mask} : \Prop}_\gamma &= - \textdom{wp}_{\Sem{\vctx \proves \mask : \textsort{InvMask}}_\gamma}(\Sem{\vctx \proves \expr : \textsort{Exp}}_\gamma, \Sem{\vctx \proves \pred : \textsort{Val} \to \Prop}_\gamma) \\ - \Sem{\vctx \proves \wtt{\timeless{\prop}}{\Prop}}_\gamma &= - \textdom{timeless}(\Sem{\vctx \proves \prop : \Prop}_\gamma) -\end{align*} -\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : 2 \in \mathit{Sets}} +An environment $\vctx$ is interpreted as the set of +finite partial functions $\rho$, with $\dom(\rho) = \dom(\vctx)$ and +$\rho(x)\in\Sem{\vctx(x)}$. + +\paragraph{Logical entailment.} +We can now define \emph{semantic} logical entailment. + +\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : 2} \Sem{\vctx \mid \pfctx \proves \propB} \eqdef \begin{aligned}[t] \MoveEqLeft \forall n \in \mathbb{N}.\; -\forall W \in \textdom{World}.\; \forall \rs \in \textdom{Res}.\; \forall \gamma \in \Sem{\vctx},\; \\& -\bigl(\All \propB \in \pfctx. (n, \rs) \in \Sem{\vctx \proves \propB : \Prop}_\gamma(W)\bigr) -\implies (n, \rs) \in \Sem{\vctx \proves \prop : \Prop}_\gamma(W) +\bigl(\All \propB \in \pfctx. n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\rs)\bigr) +\Ra n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs) \end{aligned} +The soundness statement of the logic reads +$\vctx \mid \pfctx \proves \prop \Ra \Sem{\vctx \mid \pfctx \proves \prop}$ + %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" diff --git a/heap_lang/lang.v b/heap_lang/lang.v index 3d63e057b9cf05a4e062651fcdda34db7bd06ebb..b8af355587e5e5f24b327cf5283d847f630e0a4d 100644 --- a/heap_lang/lang.v +++ b/heap_lang/lang.v @@ -447,7 +447,7 @@ Proof. end; auto with f_equal. Qed. -Instance: Inj (=) (=) of_val. +Instance of_val_inj : Inj (=) (=) of_val. Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki). diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v index 4cbc79cdaf7afb4d20a23b9489356e8e2089e59d..c95e71f2f312e8abd14d397474c1f9522a90b8f3 100644 --- a/heap_lang/lifting.v +++ b/heap_lang/lifting.v @@ -25,16 +25,18 @@ Lemma wp_alloc_pst E σ e v Φ : ⊢ WP Alloc e @ E {{ Φ }}. Proof. (* TODO RJ: This works around ssreflect bug #22. *) - intros. set (φ v' σ' ef := ∃ l, - ef = None ∧ v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None). + intros. set (φ (e' : expr []) σ' ef := ∃ l, + ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None). rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ; - last by intros; inv_step; eauto 8. + last (by intros; inv_step; eauto 8); last (by simpl; eauto). apply sep_mono, later_mono; first done. - apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef. + apply forall_intro=>v2; apply forall_intro=>σ2; apply forall_intro=>ef. apply wand_intro_l. rewrite always_and_sep_l -assoc -always_and_sep_l. - apply const_elim_l=>-[l [-> [-> [-> ?]]]]. - by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r. + apply const_elim_l=>-[l [-> [Hl [-> ?]]]]. + rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r. + rewrite -(of_to_val (Loc l) (LocV l)) // in Hl. apply of_val_inj in Hl. + by subst. Qed. Lemma wp_load_pst E σ l v Φ : @@ -42,7 +44,7 @@ Lemma wp_load_pst E σ l v Φ : (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊢ WP Load (Loc l) @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //; - last by intros; inv_step; eauto using to_of_val. + last (by intros; inv_step; eauto using to_of_val); simpl; by eauto. Qed. Lemma wp_store_pst E σ l e v v' Φ : @@ -51,7 +53,7 @@ Lemma wp_store_pst E σ l e v v' Φ : ⊢ WP Store (Loc l) e @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None) - ?right_id //; last by intros; inv_step; eauto. + ?right_id //; last (by intros; inv_step; eauto); simpl; by eauto. Qed. Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ : @@ -60,7 +62,8 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ : ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_det_step σ (LitV $LitBool false) σ None) - ?right_id //; last by intros; inv_step; eauto. + ?right_id //; last (by intros; inv_step; eauto); + simpl; split_and?; by eauto. Qed. Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ : @@ -69,7 +72,8 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ : ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}. Proof. intros. rewrite -(wp_lift_atomic_det_step σ (LitV$ LitBool true) - (<[l:=v2]>σ) None) ?right_id //; last by intros; inv_step; eauto. + (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_step; eauto); + simpl; split_and?; by eauto. Qed. (** Base axioms for core primitives of the language: Stateless reductions *) diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v index 7318ff8e960d159739fa33be49bfdd469ec1a64f..c9dfcfed8faba1eac5e09a44f67cfa9b97effee9 100644 --- a/program_logic/hoare_lifting.v +++ b/program_logic/hoare_lifting.v @@ -23,19 +23,19 @@ Lemma ht_lift_step E1 E2 E2 ⊆ E1 → to_val e1 = None → reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → - ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef, - (■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧ - {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }} ∧ - {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }}) + ((P ={E1,E2}=> ▷ ownP σ1 ★ ▷ P') ∧ + (∀ e2 σ2 ef, ■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧ + (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧ + (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }})) ⊢ {{ P }} e1 @ E1 {{ Ψ }}. Proof. intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l. rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r. rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono. rewrite always_and_sep_r -assoc; apply sep_mono_r. - rewrite (later_intro (∀ _, _)) -later_sep; apply later_mono. + rewrite [(_ ∧ _)%I]later_intro -later_sep; apply later_mono. apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef. - rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef). + do 3 rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef). apply wand_intro_l; rewrite !always_and_sep_l. (* Apply the view shift. *) rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc. @@ -62,13 +62,14 @@ Proof. (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I); try by (rewrite /φ'; eauto using atomic_not_val, atomic_step). apply and_intro; [by rewrite -vs_reflexive; apply const_intro|]. - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef. apply and_intro; [|apply and_intro; [|done]]. - - rewrite -vs_impl; apply: always_intro. apply impl_intro_l. + - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef. + rewrite -vs_impl; apply: always_intro. apply impl_intro_l. rewrite and_elim_l !assoc; apply sep_mono; last done. rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??]. by repeat apply and_intro; try apply const_intro. - - apply (always_intro _ _), impl_intro_l; rewrite and_elim_l. + - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef. + apply (always_intro _ _), impl_intro_l; rewrite and_elim_l. rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?]. rewrite -(of_to_val e2 v) // -wp_value'; []. rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //. @@ -79,16 +80,15 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e to_val e1 = None → (∀ σ1, reducible e1 σ1) → (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) → - (∀ e2 ef, - {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }} ∧ - {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }}) + ((∀ e2 ef, {{ ■ φ e2 ef ★ P }} e2 @ E {{ Ψ }}) ∧ + (∀ e2 ef, {{ ■ φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }})) ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}. Proof. intros ? Hsafe Hstep; apply: always_intro. apply impl_intro_l. rewrite -(wp_lift_pure_step E φ _ e1) //. - rewrite (later_intro (∀ _, _)) -later_and; apply later_mono. + rewrite [(_ ∧ ∀ _, _)%I]later_intro -later_and; apply later_mono. apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l. - rewrite (forall_elim e2) (forall_elim ef). + do 2 rewrite (forall_elim e2) (forall_elim ef). rewrite always_and_sep_l !always_and_sep_r {1}(always_sep_dup (■ _)). sep_split left: [■ φ _ _; P; {{ ■ φ _ _ ★ P }} e2 @ E {{ Ψ }}]%I. - rewrite assoc {1}/ht -always_wand_impl always_elim wand_elim_r //. @@ -106,11 +106,13 @@ Lemma ht_lift_pure_det_step Proof. intros ? Hsafe Hdet. rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto. - apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono. - - apply: always_intro. apply impl_intro_l. + apply and_mono. + - apply forall_intro=>e2'; apply forall_intro=>ef'. + apply: always_intro. apply impl_intro_l. rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst. by rewrite /ht always_elim impl_elim_r. - - destruct ef' as [e'|]; simpl; [|by apply const_intro]. + - apply forall_intro=>e2'; apply forall_intro=>ef'. + destruct ef' as [e'|]; simpl; [|by apply const_intro]. apply: always_intro. apply impl_intro_l. rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst. by rewrite /= /ht always_elim impl_elim_r. diff --git a/program_logic/lifting.v b/program_logic/lifting.v index e50e251368687daac2e76e2dafeefaed74d2be3d..edade4d96539fab7be61931e5a5ce3295c4435fb 100644 --- a/program_logic/lifting.v +++ b/program_logic/lifting.v @@ -61,40 +61,42 @@ Qed. Import uPred. Lemma wp_lift_atomic_step {E Φ} e1 - (φ : val Λ → state Λ → option (expr Λ) → Prop) σ1 : - to_val e1 = None → + (φ : expr Λ → state Λ → option (expr Λ) → Prop) σ1 : + atomic e1 → reducible e1 σ1 → (∀ e2 σ2 ef, - prim_step e1 σ1 e2 σ2 ef → ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) → - (▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ v2 σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef) + prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → + (▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}. Proof. - intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, ∃ v2, - to_val e2 = Some v2 ∧ φ v2 σ2 ef) _ e1 σ1) //; []. + intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, + is_Some (to_val e2) ∧ φ e2 σ2 ef) _ e1 σ1) //; + try by (eauto using atomic_not_val, atomic_step). rewrite -pvs_intro. apply sep_mono, later_mono; first done. apply forall_intro=>e2'; apply forall_intro=>σ2'. apply forall_intro=>ef; apply wand_intro_l. rewrite always_and_sep_l -assoc -always_and_sep_l. - apply const_elim_l=>-[v2' [Hv ?]] /=. + apply const_elim_l=>-[[v2 Hv] ?] /=. rewrite -pvs_intro. - rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //. - by rewrite left_id wand_elim_r -(wp_value _ _ e2' v2'). + rewrite (forall_elim v2) (forall_elim σ2') (forall_elim ef) const_equiv //. + rewrite left_id wand_elim_r -(wp_value _ _ e2' v2) //. + by erewrite of_to_val. Qed. Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef : - to_val e1 = None → + atomic e1 → reducible e1 σ1 → (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' → σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') → (▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊢ WP e1 @ E {{ Φ }}. Proof. - intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef', - σ2 = σ2' ∧ v2 = v2' ∧ ef = ef') σ1) //; last naive_solver. + intros. rewrite -(wp_lift_atomic_step _ (λ e2' σ2' ef', + σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') σ1) //. apply sep_mono, later_mono; first done. apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'. apply wand_intro_l. - rewrite always_and_sep_l -assoc -always_and_sep_l. - apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r. + rewrite always_and_sep_l -assoc -always_and_sep_l to_of_val. + apply const_elim_l=>-[-> [[->] ->]] /=. by rewrite wand_elim_r. Qed. Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :