diff --git a/docs/base-logic.tex b/docs/base-logic.tex index b18936b38013712a40030981a11a3b5f7f137d9e..e2e95048417f1c33512b3e52b718cf895e2d8462 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 744919b2c2c16248c8d20622323d9f34e47cbba8..c8db5b047ec2d34fbbfdf462c90d7681fbe08713 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 21769c81a77023511e1c44ca103b5076c234fe23..d5226a1ecf805fa487795e2ae31a3d77fe877cb4 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 3e0216bbf183b7eae73ce737234c94f2bb38aa6c..ae1f111d9dfcad2be969b944f305e7b170de31e9 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 e74f5a254a06fa8ffa07728061081eb62b099ea3..0976f763f5018066589fa1beb3eecb3448b5c1bb 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{$\maskis 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*}