From e8cc63fe91490a753654ab703bec11e6570796bf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 10 Oct 2016 13:49:46 +0200
Subject: [PATCH] docs: move more things to their right place: timeless,
persistent; also define and give rules for ghost ownership, view shift, WP
---
docs/base-logic.tex | 4 +-
docs/derived.tex | 119 ------------------
docs/ghost-state.tex | 147 +++++++++++++++++++++-
docs/iris.sty | 6 +-
docs/program-logic.tex | 269 +++++++++++++++++++++--------------------
5 files changed, 285 insertions(+), 260 deletions(-)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index b18936b38..e2e950484 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -309,9 +309,11 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\prop \proves \propB}
{\always{\prop} \proves \always{\propB}}
\and
+\infer[$\always$-E]{}
+{\always\prop \proves \prop}
+\and
\begin{array}[c]{rMcMl}
\TRUE &\proves& \always{\TRUE} \\
- \always{\prop} &\proves& \prop \\
\always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
\always{\prop} \land \propB &\proves& \always{\prop} * \propB
\end{array}
diff --git a/docs/derived.tex b/docs/derived.tex
index 744919b2c..c8db5b047 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -7,74 +7,6 @@ We assume that the signature $\Sig$ embeds all the meta-level concepts we use, a
\subsection{Base logic}
-We collect here some important and frequently used derived proof rules.
-\begin{mathparpagebreakable}
- \infer{}
- {\prop \Ra \propB \proves \prop \wand \propB}
-
- \infer{}
- {\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB}
-
- \infer{}
- {\prop * \All\var.\propB \proves \All\var. \prop * \propB}
-
- \infer{}
- {\always(\prop*\propB) \provesIff \always\prop * \always\propB}
-
- \infer{}
- {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB}
-
- \infer{}
- {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB}
-
- \infer{}
- {\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}
-
- \infer{}
- {\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB}
-
- \infer{}
- {\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}
-
- \infer
- {\pfctx, \later\prop \proves \prop}
- {\pfctx \proves \prop}
-\end{mathparpagebreakable}
-
-\paragraph{Persistent assertions.}
-\begin{defn}
- An assertion $\prop$ is \emph{persistent} if $\prop \proves \always\prop$.
-\end{defn}
-
-\ralf{Needs update.}
-Of course, $\always\prop$ is persistent for any $\prop$.
-Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$, $\mval(\melt)$ and $\knowInv\iname\prop$ are persistent.
-Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification.
-
-In our proofs, we will implicitly add and remove $\always$ from persistent assertions as necessary, and generally treat them like normal, non-linear assumptions.
-
-\paragraph{Timeless assertions.}
-
-We can show that the following additional closure properties hold for timeless assertions:
-
-\begin{mathparpagebreakable}
- \infer
- {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
- {\vctx \proves \timeless{\prop \land \propB}}
-
- \infer
- {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
- {\vctx \proves \timeless{\prop \lor \propB}}
-
- \infer
- {\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
- {\vctx \proves \timeless{\prop * \propB}}
-
- \infer
- {\vctx \proves \timeless{\prop}}
- {\vctx \proves \timeless{\always\prop}}
-\end{mathparpagebreakable}
-
\subsection{Program logic}
@@ -96,57 +28,6 @@ An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts.
\paragraph{View shifts.}
The following rules can be derived for view shifts.
-\begin{mathparpagebreakable}
-\inferH{vs-update}
- {\melt \mupd \meltsB}
- {\ownGhost\gname{\melt} \vs \exists \meltB \in \meltsB.\; \ownGhost\gname{\meltB}}
-\and
-\inferH{vs-trans}
- {\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC \and \mask_2 \subseteq \mask_1 \cup \mask_3}
- {\prop \vs[\mask_1][\mask_3] \propC}
-\and
-\inferH{vs-imp}
- {\always{(\prop \Ra \propB)}}
- {\prop \vs[\emptyset] \propB}
-\and
-\inferH{vs-mask-frame}
- {\prop \vs[\mask_1][\mask_2] \propB}
- {\prop \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB}
-\and
-\inferH{vs-frame}
- {\prop \vs[\mask_1][\mask_2] \propB}
- {\prop * \propC \vs[\mask_1][\mask_2] \propB * \propC}
-\and
-\inferH{vs-timeless}
- {\timeless{\prop}}
- {\later \prop \vs \prop}
-\and
-\inferH{vs-allocI}
- {\infinite(\mask)}
- {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}}
-\and
-\axiomH{vs-openI}
- {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop}
-\and
-\axiomH{vs-closeI}
- {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE }
-
-\inferHB{vs-disj}
- {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC}
- {\prop \lor \propB \vs[\mask_1][\mask_2] \propC}
-\and
-\inferHB{vs-exist}
- {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)}
- {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB}
-\and
-\inferHB{vs-box}
- {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC}
- {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC}
- \and
-\inferH{vs-false}
- {}
- {\FALSE \vs[\mask_1][\mask_2] \prop }
-\end{mathparpagebreakable}
\paragraph{Hoare triples.}
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 21769c81a..d5226a1ec 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -1,5 +1,141 @@
-\section{Composeable Dynamic Higher-Order Resources}
-\label{sec:hogs}
+\section{Extensions of the Base Logic}
+
+In this section we discuss some additional constructions that we will within and on top of the base logic.
+These are not ``extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.
+
+\subsection{Derived rules about base connectives}
+We collect here some important and frequently used derived proof rules.
+\begin{mathparpagebreakable}
+ \infer{}
+ {\prop \Ra \propB \proves \prop \wand \propB}
+
+ \infer{}
+ {\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB}
+
+ \infer{}
+ {\prop * \All\var.\propB \proves \All\var. \prop * \propB}
+
+ \infer{}
+ {\always(\prop*\propB) \provesIff \always\prop * \always\propB}
+
+ \infer{}
+ {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB}
+
+ \infer{}
+ {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB}
+
+ \infer{}
+ {\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}
+
+ \infer{}
+ {\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB}
+
+ \infer{}
+ {\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}
+
+ \infer{}
+ {\prop \proves \later\prop}
+\end{mathparpagebreakable}
+
+\subsection{Persistent assertions}
+We call an assertion $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
+These are assertions that ``don't own anything'', so we can (and will) treat them like ``normal'' intuitionistic assertions.
+
+Of course, $\always\prop$ is persistent for any $\prop$.
+Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $\TRUE$, $\FALSE$, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$ and $\mval(\melt)$ are persistent.
+Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification and $\later$.
+
+
+
+\subsection{Timeless assertions and except-0}
+
+One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
+It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
+\[ \diamond \prop \eqdef \later\FALSE \lor \Prop \]
+
+This modality is useful because there is a class of assertions which we call \emph{timeless} assertions, for which we have
+\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
+In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless assertions.
+
+The following ruels can be derived about except-0:
+\begin{mathpar}
+ \inferH{ex0-mono}
+ {\prop \proves \propB}
+ {\diamond\prop \proves \diamond\propB}
+
+ \axiomH{ex0-intro}
+ {\prop \proves \diamond\prop}
+
+ \axiomH{ex0-idem}
+ {\diamond\diamond\prop \proves \diamond\prop}
+
+\begin{array}[c]{rMcMl}
+ \diamond{(\prop * \propB)} &\provesIff& \diamond\prop * \diamond\propB \\
+ \diamond{(\prop \land \propB)} &\provesIff& \diamond\prop \land \diamond\propB \\
+ \diamond{(\prop \lor \propB)} &\provesIff& \diamond\prop \lor \diamond\propB
+\end{array}
+
+\begin{array}[c]{rMcMl}
+ \diamond{\All x. \prop} &\provesIff& \All x. \diamond{\prop} \\
+ \diamond{\Exists x. \prop} &\provesIff& \Exists x. \diamond{\prop} \\
+ \diamond\always{\prop} &\provesIff& \always\diamond{\prop} \\
+ \diamond\later\prop &\proves& \later{\prop}
+\end{array}
+\end{mathpar}
+
+The following rules identify the class of timeless assertions:
+\begin{mathparpagebreakable}
+\infer
+{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
+{\vctx \proves \timeless{\prop \land \propB}}
+
+\infer
+{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
+{\vctx \proves \timeless{\prop \lor \propB}}
+
+\infer
+{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
+{\vctx \proves \timeless{\prop * \propB}}
+
+\infer
+{\vctx \proves \timeless{\prop}}
+{\vctx \proves \timeless{\always\prop}}
+
+\infer
+{\vctx \proves \timeless{\propB}}
+{\vctx \proves \timeless{\prop \Ra \propB}}
+
+\infer
+{\vctx \proves \timeless{\propB}}
+{\vctx \proves \timeless{\prop \wand \propB}}
+
+\infer
+{\vctx,\var:\type \proves \timeless{\prop}}
+{\vctx \proves \timeless{\All\var:\type.\prop}}
+
+\infer
+{\vctx,\var:\type \proves \timeless{\prop}}
+{\vctx \proves \timeless{\Exists\var:\type.\prop}}
+
+\axiom{\timeless{\TRUE}}
+
+\axiom{\timeless{\FALSE}}
+
+\infer
+{\text{$\term$ or $\term'$ is a discrete COFE element}}
+{\timeless{\term =_\type \term'}}
+
+\infer
+{\text{$\melt$ is a discrete COFE element}}
+{\timeless{\ownM\melt}}
+
+\infer
+{\text{$\melt$ is an element of a discrete CMRA}}
+{\timeless{\mval(\melt)}}
+\end{mathparpagebreakable}
+
+\subsection{DC logic: Dynamic Composeable Resources}
+\label{sec:dc-logic}
The base logic described in \Sref{sec:base-logic} works over an arbitrary CMRA $\monoid$ defining the structure of the resources.
It turns out that we can generalize this further and permit picking CMRAs ``$\iFunc(\Prop)$'' that depend on the structure of assertions themselves.
@@ -15,7 +151,7 @@ The purpose of this section is to describe how we solve these issues.
\paragraph{Picking the resources.}
The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
-To instantiate the composeable, dynamic logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
+To instantiate the DC logic (base logic with dynamic composeable resources), the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
(This is in contrast to the base logic, where the user picks a single, fixed CMRA that has a unit.)
From this, we construct the bifunctor defining the overall resources as follows:
@@ -84,9 +220,12 @@ We can show the following properties for this form of ownership:
\axiomH{res-valid}
{\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}
+ \inferH{res-timeless}
+ {\text{$\melt$ is a discrete COFE element}}
+ {\timeless{\ownGhost\gname{\melt : M_i}}}
\end{mathparpagebreakable}
-Below, we will always work in the context of this dynamic, composeable logic.
+Below, we will always work within (an instance of) the DC logic.
Whenever a CMRA is used in a proof, we implicitly assume it to be available in the global family of functors.
We will typically leave the $M_i$ implicit when asserting ghost ownership, as the type of $\melt$ will be clear from the context.
diff --git a/docs/iris.sty b/docs/iris.sty
index 3e0216bbf..ae1f111d9 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -242,10 +242,10 @@
\tensor*[^{#1}]{#2}{^{#3}}
}%
}}%
-\NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
-\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
+\NewDocumentCommand \vs {O{} O{}} {\kern-0.5ex\vsGen[#1]{\Rrightarrow}[#2]}
+\NewDocumentCommand \vsL {O{} O{}} {\\kern-0.5exvsGen[#1]{\Lleftarrow}[#2]}
\NewDocumentCommand \vsE {O{} O{}} %
- {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
+ {\kern-0.5ex\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}}
\newcommand\vsWand{\kern0.1ex\tikz[baseline=(base),line width=0.375pt]{%
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index e74f5a254..0976f763f 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -59,7 +59,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\section{Program Logic}
\label{sec:program-logic}
-This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the logic described in \Sref{sec:hogs}.
+This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the logic described in \Sref{sec:dc-logic}.
So in the following, we assume that some language $\Lang$ was fixed.
\subsection{World Satisfaction, Invariants, View Shifts}
@@ -91,25 +91,120 @@ We can now define the assertion $W$ (\emph{world satisfaction}) which ensures th
The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$:
\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}{\set{\iname \mapsto \authfrag \aginj(\latertinj(\wIso(\prop)))}} \]
-\paragraph{View Shifts.}
+\paragraph{View Updates and View Shifts.}
Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
-\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop \]
+\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
-We will write $\top$ for the largest possible mask, $\mathbb N$.
+We use $\top$ as symbol for the largest possible mask, $\mathbb N$.
+We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
+%
+View updates satisfy the following basic proof rules:
+\begin{mathpar}
+\infer[vup-mono]
+{\prop \proves \propB}
+{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}
+
+\infer[vup-intro-mask]
+{\mask_2 \subseteq \mask_1}
+{(\pvs[\mask_2][\mask_1]\TRUE) \wand \prop \proves \pvs[\mask_1][\mask_2] \prop}
+
+\infer[vup-trans]
+{}
+{\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}
+
+\infer[vup-frame]
+{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop}
+
+\inferH{vup-update}
+{\melt \mupd \meltsB}
+{\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB}
+
+\infer[vup-upd]
+{}{\upd\prop \proves \pvs[\mask] \prop}
+
+\infer[vup-timeless]
+{\timeless\prop}
+{\later\prop \proves \pvs[\mask] \prop}
+
+\infer[vup-mask-frame]
+{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \prop}
+
+\inferH{vup-allocI}
+{\text{$\mask$ is infinite}}
+{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
+
+\inferH{vup-openI}
+{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
+
+\inferH{vup-closeI}
+{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
+
+\end{mathpar}
We further define the notions of \emph{view shifts} and \emph{linear view shifts}:
\begin{align*}
\prop \vs[\mask_1][\mask_2] \propB \eqdef{}& \always(\prop \Ra \pvs[\mask_1][\mask_2] \propB) \\
\prop \vsW[\mask_1][\mask_2] \propB \eqdef{}& \prop \wand \pvs[\mask_1][\mask_2] \propB
\end{align*}
-
-We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$, and similar for the view shifts.
-
-\ralf{Show some proof rules.}
-
-\subsection{Hoare Triples}
+These two are useful when writing down specifications, but for reasoning, it is typically easier to just work directly with view updates.
+Still, just to give an idea of what view shifts ``are'', here are some proof rules for them:
+\begin{mathparpagebreakable}
+\inferH{vs-update}
+ {\melt \mupd \meltsB}
+ {\ownGhost\gname{\melt} \vs \exists \meltB \in \meltsB.\; \ownGhost\gname{\meltB}}
+\and
+\inferH{vs-trans}
+ {\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC}
+ {\prop \vs[\mask_1][\mask_3] \propC}
+\and
+\inferH{vs-imp}
+ {\always{(\prop \Ra \propB)}}
+ {\prop \vs[\emptyset] \propB}
+\and
+\inferH{vs-mask-frame}
+ {\prop \vs[\mask_1][\mask_2] \propB}
+ {\prop \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB}
+\and
+\inferH{vs-frame}
+ {\prop \vs[\mask_1][\mask_2] \propB}
+ {\prop * \propC \vs[\mask_1][\mask_2] \propB * \propC}
+\and
+\inferH{vs-timeless}
+ {\timeless{\prop}}
+ {\later \prop \vs \prop}
+\and
+\inferH{vs-allocI}
+ {\infinite(\mask)}
+ {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}}
+\and
+\axiomH{vs-openI}
+ {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop}
+\and
+\axiomH{vs-closeI}
+ {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE }
+
+\inferHB{vs-disj}
+ {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC}
+ {\prop \lor \propB \vs[\mask_1][\mask_2] \propC}
+\and
+\inferHB{vs-exist}
+ {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)}
+ {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB}
+\and
+\inferHB{vs-always}
+ {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC}
+ {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC}
+ \and
+\inferH{vs-false}
+ {}
+ {\FALSE \vs[\mask_1][\mask_2] \prop }
+\end{mathparpagebreakable}
+
+\subsection{Weakest Precondition}
Finally, we can define the core piece of the program logic, the assertion that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived.
+
+\paragraph{Defining weakest precondition.}
We assume that everything making up the definition of the language, \ie values, expressions, states, the conversion functions, reduction relation and all their properties, are suitably reflected into the logic (\ie they are part of the signature $\Sig$).
\begin{align*}
@@ -127,124 +222,15 @@ This ties the authoritative part of \textmon{State} to the actual physical state
The fragment will then be available to the user of the logic, as their way of talking about the physical state:
\[ \ownPhys\state \eqdef \ownGhost{\gname_{\textmon{State}}}{\authfrag \state} \]
-It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs on paper.
-Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
-\[
-\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\Ret\val.\propB})}
-\]
-
-\subsection{Lost stuff}
-\ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}
-
-
-We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
-If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
-%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
-
-Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
-This is a \emph{meta-level} assertion about propositions, defined as follows:
-
-\[ \vctx \proves \timeless{\prop} \eqdef \vctx\mid\later\prop \proves \prop \lor \later\FALSE \]
-
-\paragraph{Metavariable conventions.}
-We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
-\[
-\begin{array}{r|l}
- \text{metavariable} & \text{type} \\\hline
- \term, \termB & \text{arbitrary} \\
- \val, \valB & \textlog{Val} \\
- \expr & \textlog{Expr} \\
- \state & \textlog{State} \\
-\end{array}
-\qquad\qquad
-\begin{array}{r|l}
- \text{metavariable} & \text{type} \\\hline
- \iname & \textlog{InvName} \\
- \mask & \textlog{InvMask} \\
- \melt, \meltB & \textlog{M} \\
- \prop, \propB, \propC & \Prop \\
- \pred, \predB, \predC & \type\to\Prop \text{ (when $\type$ is clear from context)} \\
-\end{array}
-\]
-
-\begin{mathpar}
-\infer
-{\text{$\term$ or $\term'$ is a discrete COFE element}}
-{\timeless{\term =_\type \term'}}
-
-\infer
-{\text{$\melt$ is a discrete COFE element}}
-{\timeless{\ownM\melt}}
-
-\infer
-{\text{$\melt$ is an element of a discrete CMRA}}
-{\timeless{\mval(\melt)}}
-
-\infer{}
-{\timeless{\ownPhys\state}}
-
-\infer
-{\vctx \proves \timeless{\propB}}
-{\vctx \proves \timeless{\prop \Ra \propB}}
-
-\infer
-{\vctx \proves \timeless{\propB}}
-{\vctx \proves \timeless{\prop \wand \propB}}
-
-\infer
-{\vctx,\var:\type \proves \timeless{\prop}}
-{\vctx \proves \timeless{\All\var:\type.\prop}}
-
-\infer
-{\vctx,\var:\type \proves \timeless{\prop}}
-{\vctx \proves \timeless{\Exists\var:\type.\prop}}
-\end{mathpar}
-
-\begin{mathpar}
-\infer[pvs-intro]
-{}{\prop \proves \pvs[\mask] \prop}
-
-\infer[pvs-mono]
-{\prop \proves \propB}
-{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}
-
-\infer[pvs-timeless]
-{\timeless\prop}
-{\later\prop \proves \pvs[\mask] \prop}
-
-\infer[pvs-trans]
-{\mask_2 \subseteq \mask_1 \cup \mask_3}
-{\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}
-
-\infer[pvs-frame]
-{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop}
-
-\inferH{pvs-allocI}
-{\text{$\mask$ is infinite}}
-{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
-
-\inferH{pvs-openI}
-{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
-
-\inferH{pvs-closeI}
-{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
-
-\inferH{pvs-update}
-{\melt \mupd \meltsB}
-{\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB}
-\end{mathpar}
-
-\paragraph{Laws of weakest preconditions.}
+\paragraph{Laws of weakest precondition.}
+The following rules can all be derived inside the DC logic:
\begin{mathpar}
\infer[wp-value]
{}{\prop[\val/\var] \proves \wpre{\val}[\mask]{\Ret\var.\prop}}
\infer[wp-mono]
-{\mask_1 \subseteq \mask_2 \and \var:\textlog{val}\mid\prop \proves \propB}
-{\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
+{\mask_1 \subseteq \mask_2 \and \vctx,\var:\textlog{val}\mid\prop \proves \propB}
+{\vctx\mid\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
\infer[pvs-wp]
{}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
@@ -253,7 +239,7 @@ We introduce additional metavariables ranging over terms and generally let the c
{}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
\infer[wp-atomic]
-{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
+{\physatomic{\expr}}
{\pvs[\mask_1][\mask_2] \wpre\expr[\mask_2]{\Ret\var. \pvs[\mask_2][\mask_1]\prop}
\proves \wpre\expr[\mask_1]{\Ret\var.\prop}}
@@ -262,31 +248,48 @@ We introduce additional metavariables ranging over terms and generally let the c
\infer[wp-frame-step]
{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
-{\wpre\expr[\mask]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask \uplus \mask_1]{\Ret\var.\propB*\prop}}
+{\wpre\expr[\mask_2]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask_1]{\Ret\var.\propB*\prop}}
\infer[wp-bind]
{\text{$\lctx$ is a context}}
{\wpre\expr[\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\mask]{\Ret\varB.\prop}}
\end{mathpar}
-\paragraph{Lifting of operational semantics.}~
+We will also want rules that connect weakest preconditions to the operational semantics of the language.
+In order to cover the most general case, those rules end up being more complicated:
\begin{mathpar}
\infer[wp-lift-step]
- {\mask_2 \subseteq \mask_1 \and
- \toval(\expr_1) = \bot}
+ {\toval(\expr_1) = \bot}
{ {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
- ~~\pvs[\mask_1][\mask_2] \Exists \state_1. \red(\expr_1,\state_1) \land \later\ownPhys{\state_1} * {}\\\qquad\qquad\qquad \later\All \expr_2, \state_2, \expr_\f. \left( (\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f) \land \ownPhys{\state_2} \right) \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}
+ ~~\pvs[\mask][\emptyset] \Exists \state_1. \red(\expr_1,\state_1) * \later\ownPhys{\state_1} * {}\\\qquad~~ \later\All \expr_2, \state_2, \bar\expr. \Bigl( (\expr_1, \state_1 \step \expr_2, \state_2, \bar\expr) * \ownPhys{\state_2} \Bigr) \wand \pvs[\emptyset][\mask] \Bigl(\wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr) {}\\\proves \wpre{\expr_1}[\mask]{\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_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 }
- {\later\All \state, \expr_2, \expr_\f. (\expr_1,\state \step \expr_2, \state,\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}}
+ \All \state_1, \expr_2, \state_2, \bar\expr. \expr_1,\state_1 \step \expr_2,\state_2,\bar\expr \Ra \state_1 = \state_2 }
+ {\later\All \state, \expr_2, \bar\expr. (\expr_1,\state \step \expr_2, \state,\bar\expr) \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \bar\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}}
\end{mathpar}
-Notice that primitive view shifts cover everything to their right, \ie $\pvs \prop * \propB \eqdef \pvs (\prop * \propB)$.
-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).
+
+\paragraph{Adequacy of weakest precondition.}
+~\ralf{TODO.}
+
+\paragraph{Hoare triples.}
+It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs in Coq.
+Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
+\[
+\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\Ret\val.\propB})}
+\]
+
+\subsection{Lost stuff}
+\ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}
+
+
+
+\paragraph{Laws of weakest preconditions.}
+
+\paragraph{Lifting of operational semantics.}~
The adequacy statement concerning functional correctness reads as follows:
\begin{align*}
--
GitLab