program-logic.tex 30.8 KB
 Ralf Jung committed Oct 06, 2016 1   Ralf Jung committed Oct 04, 2016 2 \section{Program Logic}  Ralf Jung committed Oct 06, 2016 3 \label{sec:program-logic}  Ralf Jung committed Oct 04, 2016 4   Ralf Jung committed Oct 22, 2016 5 This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the base logic.  Ralf Jung committed Oct 06, 2016 6 So in the following, we assume that some language $\Lang$ was fixed.  Ralf Jung committed Oct 06, 2016 7   Ralf Jung committed Dec 10, 2017 8 \subsection{Dynamic Composeable Higher-Order Resources}  Ralf Jung committed Oct 22, 2016 9 10 \label{sec:composeable-resources}  Robbert Krebbers committed Dec 10, 2017 11 The base logic described in \Sref{sec:base-logic} works over an arbitrary camera $\monoid$ defining the structure of the resources.  Robbert Krebbers committed Dec 10, 2017 12 13 It turns out that we can generalize this further and permit picking cameras $\iFunc(\Prop)$'' that depend on the structure of propositions themselves. Of course, $\Prop$ is just the syntactic type of propositions; for this to make sense we have to look at the semantics.  Ralf Jung committed Oct 22, 2016 14   Robbert Krebbers committed Dec 10, 2017 15 Furthermore, there is a composability problem with the given logic: if we have one proof performed with camera $\monoid_1$, and another proof carried out with a \emph{different} camera $\monoid_2$, then the two proofs are actually carried out in two \emph{entirely separate logics} and hence cannot be combined.  Ralf Jung committed Oct 22, 2016 16   Robbert Krebbers committed Dec 10, 2017 17 Finally, in many cases just having a single instance'' of a camera available for reasoning is not enough.  Ralf Jung committed Oct 22, 2016 18 19 20 21 22 23 24 For example, when reasoning about a dynamically allocated data structure, every time a new instance of that data structure is created, we will want a fresh resource governing the state of this particular instance. While it would be possible to handle this problem whenever it comes up, it turns out to be useful to provide a general solution. 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.  Ralf Jung committed Dec 05, 2016 25 To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.  Robbert Krebbers committed Dec 10, 2017 26 (This is in contrast to the base logic, where the user picks a single, fixed camera that has a unit.)  Ralf Jung committed Oct 22, 2016 27 28 29  From this, we construct the bifunctor defining the overall resources as follows: \begin{align*}  Ralf Jung committed Dec 07, 2016 30 31  \GName \eqdef{}& \nat \\ \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe)  Ralf Jung committed Oct 22, 2016 32 33 \end{align*} We will motivate both the use of a product and the finite partial function below.  Robbert Krebbers committed Dec 10, 2017 34 $\textdom{ResF}(\ofe^\op, \ofe)$ is a camera by lifting the individual cameras pointwise, and it has a unit (using the empty finite partial functions).  Ralf Jung committed Oct 22, 2016 35 36 37 38 Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$. Now we can write down the recursive domain equation: $\iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp))$  39 Here, $\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor, which exists and is unique up to isomorphism by \thmref{thm:america_rutten}.  Robbert Krebbers committed Dec 10, 2017 40 We do not need to consider how the object $\iPreProp$ is constructed, we only need the isomorphism, given by:  Ralf Jung committed Oct 22, 2016 41 42 43 44 45 46 47 \begin{align*} \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\ \iProp &\eqdef \UPred(\Res) \\ \wIso &: \iProp \nfn \iPreProp \\ \wIso^{-1} &: \iPreProp \nfn \iProp \end{align*}  Robbert Krebbers committed Dec 10, 2017 48 Notice that $\iProp$ is the semantic model of propositions for the base logic described in \Sref{sec:base-logic} with $\Res$:  Ralf Jung committed Oct 22, 2016 49 $\Sem{\Prop} \eqdef \iProp = \UPred(\Res)$  Robbert Krebbers committed Dec 10, 2017 50 Effectively, we just defined a way to instantiate the base logic with $\Res$ as the camera of resources, while providing a way for $\Res$ to depend on $\iPreProp$, which is isomorphic to $\Sem\Prop$.  Ralf Jung committed Oct 22, 2016 51   Robbert Krebbers committed Dec 10, 2017 52 We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical propositions $\Sem\Prop$ and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.  Ralf Jung committed Oct 22, 2016 53   Ralf Jung committed Feb 07, 2017 54 \paragraph{Proof composability.}  Ralf Jung committed Oct 22, 2016 55 To make our proofs composeable, we \emph{generalize} our proofs over the family of functors.  Robbert Krebbers committed Dec 10, 2017 56 This is possible because we made $\Res$ a \emph{product} of all the cameras picked by the user, and because we can actually work with that product pointwise''.  Ralf Jung committed Oct 22, 2016 57 58 59 60 61 62 63 So instead of picking a \emph{concrete} family, proofs will assume to be given an \emph{arbitrary} family of functors, plus a proof that this family \emph{contains the functors they need}. Composing two proofs is then merely a matter of conjoining the assumptions they make about the functors. Since the logic is entirely parametric in the choice of functors, there is no trouble reasoning without full knowledge of the family of functors. Only when the top-level proof is completed we will close'' the proof by picking a concrete family that contains exactly those functors the proof needs. \paragraph{Dynamic resources.}  Robbert Krebbers committed Dec 10, 2017 64 Finally, the use of finite partial functions lets us have as many instances of any camera as we could wish for:  Ralf Jung committed Oct 22, 2016 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 Because there can only ever be finitely many instances already allocated, it is always possible to create a fresh instance with any desired (valid) starting state. This is best demonstrated by giving some proof rules. So let us first define the notion of ghost ownership that we use in this logic. Assuming that the family of functors contains the functor $\Sigma_i$ at index $i$, and furthermore assuming that $\monoid_i = \Sigma_i(\iPreProp, \iPreProp)$, given some $\melt \in \monoid_i$ we define: $\ownGhost\gname{\melt:\monoid_i} \eqdef \ownM{(\ldots, \emptyset, i:\mapsingleton \gname \melt, \emptyset, \ldots)}$ This is ownership of the pair (element of the product over all the functors) that has the empty finite partial function in all components \emph{except for} the component corresponding to index $i$, where we own the element $\melt$ at index $\gname$ in the finite partial function. We can show the following properties for this form of ownership: \begin{mathparpagebreakable} \inferH{res-alloc}{\text{$G$ infinite} \and \melt \in \mval_{M_i}} { \TRUE \proves \upd \Exists\gname\in G. \ownGhost\gname{\melt : M_i} } \and \inferH{res-update} {\melt \mupd_{M_i} B} {\ownGhost\gname{\melt : M_i} \proves \upd \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}} \inferH{res-empty} {\text{$\munit$ is a unit of $M_i$}} {\TRUE \proves \upd \ownGhost\gname\munit} \axiomH{res-op} {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \provesIff \ownGhost\gname{\melt\mtimes\meltB : M_i}} \axiomH{res-valid} {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)} \inferH{res-timeless}  Ralf Jung committed Dec 05, 2016 94  {\text{$\melt$ is a discrete OFE element}}  Ralf Jung committed Oct 22, 2016 95 96 97 98  {\timeless{\ownGhost\gname{\melt : M_i}}} \end{mathparpagebreakable} Below, we will always work within (an instance of) the logic as described here.  Robbert Krebbers committed Dec 10, 2017 99 Whenever a camera is used in a proof, we implicitly assume it to be available in the global family of functors.  Ralf Jung committed Oct 22, 2016 100 101 102 103 We will typically leave the $M_i$ implicit when asserting ghost ownership, as the type of $\melt$ will be clear from the context.  Ralf Jung committed Dec 10, 2017 104 \subsection{World Satisfaction, Invariants, Fancy Updates}  Ralf Jung committed Oct 10, 2016 105 \label{sec:invariants}  Ralf Jung committed Oct 06, 2016 106 107 108 109 110  To introduce invariants into our logic, we will define weakest precondition to explicitly thread through the proof that all the invariants are maintained throughout program execution. However, in order to be able to access invariants, we will also have to provide a way to \emph{temporarily disable} (or open'') them. To this end, we use tokens that manage which invariants are currently enabled.  Robbert Krebbers committed Dec 10, 2017 111 We assume to have the following four cameras available:  Ralf Jung committed Oct 06, 2016 112 \begin{align*}  Ralf Jung committed Dec 07, 2016 113 114 115  \InvName \eqdef{}& \nat \\ \textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\ \textmon{En} \eqdef{}& \pset{\InvName} \\  Ralf Jung committed Dec 12, 2016 116  \textmon{Dis} \eqdef{}& \finpset{\InvName}  Ralf Jung committed Oct 06, 2016 117 118 119 \end{align*} The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.  Robbert Krebbers committed Dec 10, 2017 120 We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these cameras have been created, such that these names are globally known.  Ralf Jung committed Oct 06, 2016 121   Ralf Jung committed Oct 06, 2016 122 \paragraph{World Satisfaction.}  Robbert Krebbers committed Dec 10, 2017 123 We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:  Ralf Jung committed Oct 06, 2016 124 \begin{align*}  Ralf Jung committed Dec 07, 2016 125  W \eqdef{}& \Exists I : \InvName \fpfn \Prop.  Ralf Jung committed Oct 31, 2016 126  \begin{array}[t]{@{} l}  Robbert Krebbers committed Oct 17, 2016 127  \ownGhost{\gname_{\textmon{Inv}}}{\authfull  Ralf Jung committed Oct 31, 2016 128  \mapComp {\iname}  Robbert Krebbers committed Oct 17, 2016 129 130 131 132  {\aginj(\latertinj(\wIso(I(\iname))))} {\iname \in \dom(I)}} * \\ \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right) \end{array}  Ralf Jung committed Oct 06, 2016 133 134 135 \end{align*} \paragraph{Invariants.}  Robbert Krebbers committed Dec 10, 2017 136 The following proposition states that an invariant with name $\iname$ exists and maintains proposition $\prop$:  Robbert Krebbers committed Oct 17, 2016 137 138 $\knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}} {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}}$  Ralf Jung committed Oct 06, 2016 139   Ralf Jung committed Dec 10, 2017 140 \paragraph{Fancy Updates and View Shifts.}  Ralf Jung committed Oct 21, 2016 141 Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:  Ralf Jung committed Oct 10, 2016 142 $\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)$  Ralf Jung committed Oct 06, 2016 143 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.  Robbert Krebbers committed Oct 17, 2016 144 We use $\top$ as symbol for the largest possible mask, $\nat$, and $\bot$ for the smallest possible mask $\emptyset$.  Ralf Jung committed Oct 10, 2016 145 146 We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$. %  Ralf Jung committed Oct 21, 2016 147 Fancy updates satisfy the following basic proof rules:  Ralf Jung committed Oct 31, 2016 148 \begin{mathparpagebreakable}  Ralf Jung committed Oct 21, 2016 149 \infer[fup-mono]  Ralf Jung committed Oct 10, 2016 150 151 152 {\prop \proves \propB} {\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}  Ralf Jung committed Oct 21, 2016 153 \infer[fup-intro-mask]  Ralf Jung committed Oct 10, 2016 154 {\mask_2 \subseteq \mask_1}  Ralf Jung committed Oct 10, 2016 155 {\prop \proves \pvs[\mask_1][\mask_2]\pvs[\mask_2][\mask_1] \prop}  Ralf Jung committed Oct 10, 2016 156   Ralf Jung committed Oct 21, 2016 157 \infer[fup-trans]  Ralf Jung committed Oct 10, 2016 158 159 160 {} {\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}  Ralf Jung committed Oct 21, 2016 161 \infer[fup-upd]  Ralf Jung committed Oct 10, 2016 162 163 {}{\upd\prop \proves \pvs[\mask] \prop}  Ralf Jung committed Oct 21, 2016 164 \infer[fup-frame]  Ralf Jung committed Oct 10, 2016 165 {}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \propB * \prop}  Ralf Jung committed Oct 10, 2016 166   Ralf Jung committed Oct 21, 2016 167 \inferH{fup-update}  Ralf Jung committed Oct 10, 2016 168 169 170 {\melt \mupd \meltsB} {\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB}  Ralf Jung committed Oct 21, 2016 171 \infer[fup-timeless]  Ralf Jung committed Oct 10, 2016 172 173 {\timeless\prop} {\later\prop \proves \pvs[\mask] \prop}  Ralf Jung committed Oct 10, 2016 174 %  Ralf Jung committed Oct 21, 2016 175 % \inferH{fup-allocI}  Ralf Jung committed Oct 10, 2016 176 177 178 % {\text{$\mask$ is infinite}} % {\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop} %gov  Ralf Jung committed Oct 21, 2016 179 % \inferH{fup-openI}  Ralf Jung committed Oct 10, 2016 180 181 % {}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop} %  Ralf Jung committed Oct 21, 2016 182 % \inferH{fup-closeI}  Ralf Jung committed Oct 10, 2016 183 % {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}  Ralf Jung committed Oct 31, 2016 184 \end{mathparpagebreakable}  Ralf Jung committed Dec 05, 2016 185 (There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.)  Ralf Jung committed Oct 06, 2016 186   Ralf Jung committed Oct 21, 2016 187 We can further define the notions of \emph{view shifts} and \emph{linear view shifts}:  Ralf Jung committed Oct 06, 2016 188 \begin{align*}  Ralf Jung committed Oct 21, 2016 189  \prop \vsW[\mask_1][\mask_2] \propB \eqdef{}& \prop \wand \pvs[\mask_1][\mask_2] \propB \\  Ralf Jung committed Feb 02, 2017 190 191  \prop \vs[\mask_1][\mask_2] \propB \eqdef{}& \always(\prop \wand \pvs[\mask_1][\mask_2] \propB) \\ \prop \vs[\mask] \propB \eqdef{}& \prop \vs[\mask][\mask] \propB  Ralf Jung committed Oct 06, 2016 192 \end{align*}  Ralf Jung committed Oct 21, 2016 193 These two are useful when writing down specifications and for comparing with previous versions of Iris, but for reasoning, it is typically easier to just work directly with fancy updates.  Ralf Jung committed Oct 10, 2016 194 195 196 197 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}  Ralf Jung committed Feb 02, 2017 198  {\ownGhost\gname{\melt} \vs[\emptyset] \exists \meltB \in \meltsB.\; \ownGhost\gname{\meltB}}  Ralf Jung committed Oct 10, 2016 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 \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}}  Ralf Jung committed Feb 02, 2017 218  {\later \prop \vs[\emptyset] \prop}  Ralf Jung committed Oct 10, 2016 219   Ralf Jung committed Oct 10, 2016 220 221 222 223 224 225 226 227 228 229 % \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 } %  Ralf Jung committed Oct 10, 2016 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 \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}  Ralf Jung committed Dec 10, 2017 247 \subsection{Weakest Precondition}  Ralf Jung committed Oct 06, 2016 248   Robbert Krebbers committed Dec 10, 2017 249 Finally, we can define the core piece of the program logic, the proposition that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived.  Ralf Jung committed Oct 10, 2016 250 251  \paragraph{Defining weakest precondition.}  Ralf Jung committed Oct 06, 2016 252 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$).  Robbert Krebbers committed Dec 10, 2017 253 We further assume (as a parameter) a predicate $\stateinterp : \State \to \iProp$ that interprets the physical state as an Iris proposition.  Ralf Jung committed Dec 12, 2016 254 This can be instantiated, for example, with ownership of an authoritative RA to tie the physical state to fragments that are used for user-level proofs.  Ralf Jung committed Oct 06, 2016 255 256  \begin{align*}  Ralf Jung committed Oct 06, 2016 257  \textdom{wp} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\  Joseph Tassarotti committed Nov 14, 2017 258  & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\  Robbert Krebbers committed Dec 10, 2017 259  & \Bigl(\toval(\expr) = \bot \land \All \state. \stateinterp(\state) \vsW[\mask][\emptyset] {}\\  Robbert Krebbers committed Oct 17, 2016 260  &\qquad \red(\expr, \state) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\  Robbert Krebbers committed Dec 10, 2017 261  &\qquad\qquad \stateinterp(\state') * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\  Ralf Jung committed Oct 06, 2016 262 % (* value case *)  Ralf Jung committed Oct 06, 2016 263  \wpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\mask, \expr, \Lam\val.\prop)  Ralf Jung committed Oct 06, 2016 264 \end{align*}  Ralf Jung committed Oct 06, 2016 265 If we leave away the mask, we assume it to default to $\top$.  Ralf Jung committed Oct 06, 2016 266   Ralf Jung committed Oct 10, 2016 267 \paragraph{Laws of weakest precondition.}  Ralf Jung committed Oct 22, 2016 268 The following rules can all be derived:  Ralf Jung committed Oct 04, 2016 269 270 271 272 273 \begin{mathpar} \infer[wp-value] {}{\prop[\val/\var] \proves \wpre{\val}[\mask]{\Ret\var.\prop}} \infer[wp-mono]  Ralf Jung committed Oct 10, 2016 274 275 {\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}}  Ralf Jung committed Oct 04, 2016 276   Ralf Jung committed Oct 21, 2016 277 \infer[fup-wp]  Ralf Jung committed Oct 04, 2016 278 279 {}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}  Ralf Jung committed Oct 21, 2016 280 \infer[wp-fup]  Ralf Jung committed Oct 04, 2016 281 282 283 {}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}} \infer[wp-atomic]  Ralf Jung committed Oct 10, 2016 284 {\physatomic{\expr}}  Ralf Jung committed Oct 04, 2016 285 286 287 288 289 290 291 292 {\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}} \infer[wp-frame] {}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}} \infer[wp-frame-step] {\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}  Ralf Jung committed Oct 10, 2016 293 {\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}}  Ralf Jung committed Oct 04, 2016 294 295 296 297 298 299  \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}  Ralf Jung committed Dec 12, 2016 300 We will also want a rule that connect weakest preconditions to the operational semantics of the language.  Ralf Jung committed Oct 04, 2016 301 302 \begin{mathpar} \infer[wp-lift-step]  Ralf Jung committed Dec 12, 2016 303  {\toval(\expr_1) = \bot}  Ralf Jung committed Oct 04, 2016 304  { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...  Robbert Krebbers committed Dec 10, 2017 305  ~~\All \state_1. \stateinterp(\state_1) \vsW[\mask][\emptyset] \red(\expr_1,\state_1) * {}\\\qquad~~ \later\All \expr_2, \state_2, \vec\expr. (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr) \vsW[\emptyset][\mask] \Bigl(\stateinterp(\state_2) * \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr) {}\\\proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}  Ralf Jung committed Oct 04, 2016 306 307 308  \end{inbox}} } \end{mathpar}  Ralf Jung committed Dec 12, 2016 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 % We can further derive some slightly simpler rules for special cases. % \begin{mathparpagebreakable} % \infer[wp-lift-pure-step] % {\All \state_1. \red(\expr_1, \state_1) \and % \All \state_1, \expr_2, \state_2, \vec\expr. \expr_1,\state_1 \step \expr_2,\state_2,\vec\expr \Ra \state_1 = \state_2 } % {\later\All \state, \expr_2, \vec\expr. (\expr_1,\state \step \expr_2, \state,\vec\expr) \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}} % \infer[wp-lift-atomic-step] % {\atomic(\expr_1) \and % \red(\expr_1, \state_1)} % { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \vec\expr. (\expr_1,\state_1 \step \ofval(\val),\state_2,\vec\expr) * \ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\ \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop} % \end{inbox}} } % \infer[wp-lift-atomic-det-step] % {\atomic(\expr_1) \and % \red(\expr_1, \state_1) \and % \All \expr'_2, \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \vec\expr = \vec\expr'} % {\later\ownPhys{\state_1} * \later \Bigl(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} % \infer[wp-lift-pure-det-step] % {\All \state_1. \red(\expr_1, \state_1) \\ % \All \state_1, \expr_2', \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_1 = \state'_2 \land \expr_2 = \expr_2' \land \vec\expr = \vec\expr'} % {\later \Bigl( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} % \end{mathparpagebreakable}  Ralf Jung committed Oct 10, 2016 333 334   Ralf Jung committed Oct 10, 2016 335 \paragraph{Adequacy of weakest precondition.}  Ralf Jung committed Oct 04, 2016 336   Ralf Jung committed Oct 10, 2016 337 338 339 340 The purpose of the adequacy statement is to show that our notion of weakest preconditions is \emph{realistic} in the sense that it actually has anything to do with the actual behavior of the program. There are two properties we are looking for: First of all, the postcondition should reflect actual properties of the values the program can terminate with. Second, a proof of a weakest precondition with any postcondition should imply that the program is \emph{safe}, \ie that it does not get stuck.  Ralf Jung committed Jan 11, 2017 341 342 343 344 345 346 347 348 \begin{defn}[Adequacy] A program $\expr$ in some initial state $\state$ is \emph{adequate} for a set $V \subseteq \Val$ of legal return values ($\expr, \state \vDash V$) if for all $\tpool', \state'$ such that $([\expr], \state) \tpstep^\ast (\tpool', \state')$ we have \begin{enumerate} \item Safety: For any $\expr' \in \tpool'$ we have that either $\expr'$ is a value, or $$\red(\expr'_i,\state')$$: $\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')$ Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step. \item Legal return value: If $\tpool'_1$ (the main thread) is a value $\val'$, then $\val' \in V$:  Ralf Jung committed Feb 02, 2017 349  $\All \val',\tpool''. \tpool' = [\val'] \dplus \tpool'' \Ra \val' \in V$  Ralf Jung committed Jan 11, 2017 350 351 352 \end{enumerate} \end{defn}  Ralf Jung committed Jan 12, 2017 353 354 355 To express the adequacy statement for functional correctness, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic: $\pred : \Val \to \Prop \in \SigFn$ Furthermore, we assume that the \emph{interpretation} $\Sem\pred$ of $\pred$ reflects some set $V$ of legal return values into the logic (also see \Sref{sec:model}):  Ralf Jung committed Oct 10, 2016 356 $\begin{array}{rMcMl}  Robbert Krebbers committed Oct 17, 2016 357  \Sem\pred &:& \Sem{\Val\,} \nfn \Sem\Prop \\  Ralf Jung committed Oct 10, 2016 358 359 360 361  \Sem\pred &\eqdef& \Lam \val. \Lam \any. \setComp{n}{v \in V} \end{array}$ The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound. The adequacy statement now reads as follows:  Ralf Jung committed Oct 04, 2016 362 \begin{align*}  Ralf Jung committed Jan 12, 2017 363  &\All \mask, \expr, \val, \state.  Robbert Krebbers committed Dec 10, 2017 364  \\&( \TRUE \proves {\upd}_\mask \Exists \stateinterp. \stateinterp(\state) * \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra  Ralf Jung committed Jan 11, 2017 365  \\&\expr, \state \vDash V  Ralf Jung committed Oct 04, 2016 366 \end{align*}  Ralf Jung committed Jan 11, 2017 367 Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.  Ralf Jung committed Oct 04, 2016 368   Ralf Jung committed Oct 10, 2016 369 \paragraph{Hoare triples.}  Robbert Krebbers committed Dec 10, 2017 370 It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq.  Ralf Jung committed Oct 10, 2016 371 372 Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple: $ Ralf Jung committed Oct 21, 2016 373 \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \wand \wpre{\expr}[\mask]{\Ret\val.\propB})}  Ralf Jung committed Oct 10, 2016 374 $  Ralf Jung committed Oct 04, 2016 375   Ralf Jung committed Oct 10, 2016 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 We only give some of the proof rules for Hoare triples here, since we usually do all our reasoning directly with weakest preconditions and use Hoare triples only to write specifications. \begin{mathparpagebreakable} \inferH{Ht-ret} {} {\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]} \and \inferH{Ht-bind} {\text{$\lctx$ is a context} \and \hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\ \All \val. \hoare{\propB}{\lctx(\val)}{\Ret\valB.\propC}[\mask]} {\hoare{\prop}{\lctx(\expr)}{\Ret\valB.\propC}[\mask]} \and \inferH{Ht-csq} {\prop \vs \prop' \\ \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\ \All \val. \propB' \vs \propB} {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} \and % \inferH{Ht-mask-weaken} % {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]} % {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask \uplus \mask']} % \\\\ \inferH{Ht-frame} {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]} {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]} \and % \inferH{Ht-frame-step} % {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot \and \mask_2 \subseteq \mask_2 \\\\ \propC_1 \vs[\mask_1][\mask_2] \later\propC_2 \and \propC_2 \vs[\mask_2][\mask_1] \propC_3} % {\hoare{\prop * \propC_1}{\expr}{\Ret\val. \propB * \propC_3}[\mask \uplus \mask_1]} % \and \inferH{Ht-atomic} {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\ \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\ \All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\ \physatomic{\expr} } {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']} \and \inferH{Ht-false} {} {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]} \and \inferHB{Ht-disj} {\hoare{\prop}{\expr}{\Ret\val.\propC}[\mask] \and \hoare{\propB}{\expr}{\Ret\val.\propC}[\mask]} {\hoare{\prop \lor \propB}{\expr}{\Ret\val.\propC}[\mask]} \and \inferHB{Ht-exist} {\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} {\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]} \and \inferHB{Ht-box} {\always\propB \proves \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]} {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]} % \and % \inferH{Ht-inv} % {\hoare{\later\propC*\prop}{\expr}{\Ret\val.\later\propC*\propB}[\mask] \and % \physatomic{\expr} % } % {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]} % \and % \inferH{Ht-inv-timeless} % {\hoare{\propC*\prop}{\expr}{\Ret\val.\propC*\propB}[\mask] \and % \physatomic{\expr} \and \timeless\propC % } % {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]} \end{mathparpagebreakable}  Ralf Jung committed Oct 04, 2016 441   Ralf Jung committed Dec 10, 2017 442 \subsection{Invariant Namespaces}  Ralf Jung committed Oct 10, 2016 443 444 \label{sec:namespaces}  Robbert Krebbers committed Dec 10, 2017 445 In \Sref{sec:invariants}, we defined a proposition $\knowInv\iname\prop$ expressing knowledge (\ie the proposition is persistent) that $\prop$ is maintained as invariant with name $\iname$.  Ralf Jung committed Oct 10, 2016 446 447 448 449 450 451 The concrete name $\iname$ is picked when the invariant is allocated, so it cannot possibly be statically known -- it will always be a variable that's threaded through everything. However, we hardly care about the actual, concrete name. All we need to know is that this name is \emph{different} from the names of other invariants that we want to open at the same time. Keeping track of the $n^2$ mutual inequalities that arise with $n$ invariants quickly gets in the way of the actual proof. To solve this issue, instead of remembering the exact name picked for an invariant, we will keep track of the \emph{namespace} the invariant was allocated in.  Jacques-Henri Jourdan committed Oct 13, 2016 452 Namespaces are sets of invariants, following a tree-like structure:  Ralf Jung committed Oct 10, 2016 453 454 455 456 457 458 459 460 Think of the name of an invariant as a sequence of identifiers, much like a fully qualified Java class name. A \emph{namespace} $\namesp$ then is like a Java package: it is a sequence of identifiers that we think of as \emph{containing} all invariant names that begin with this sequence. For example, \texttt{org.mpi-sws.iris} is a namespace containing the invariant name \texttt{org.mpi-sws.iris.heap}. The crux is that all namespaces contain infinitely many invariants, and hence we can \emph{freely pick} the namespace an invariant is allocated in -- no further, unpredictable choice has to be made. Furthermore, we will often know that namespaces are \emph{disjoint} just by looking at them. The namespaces $\namesp.\texttt{iris}$ and $\namesp.\texttt{gps}$ are disjoint no matter the choice of $\namesp$. As a result, there is often no need to track disjointness of namespaces, we just have to pick the namespaces that we allocate our invariants in accordingly.  Robbert Krebbers committed Oct 17, 2016 461 Formally speaking, let $\namesp \in \textlog{InvNamesp} \eqdef \List(\nat)$ be the type of \emph{invariant namespaces}.  Ralf Jung committed Oct 10, 2016 462 463 464 465 We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$. (In other words, the list is backwards''. This is because cons-ing to the list, like the dot does above, is easier to deal with in Coq than appending at the end.) The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name).  Robbert Krebbers committed Oct 17, 2016 466 They, too, are lists of $\nat$, the same type as namespaces.  Ralf Jung committed Dec 07, 2016 467 468 In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\InvName$, the type of plain'' invariant names. Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\InvName$ is infinite.  Ralf Jung committed Oct 10, 2016 469 470 Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: $\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}$  Robbert Krebbers committed Dec 10, 2017 471 We will overload the notation for invariant propositions for using namespaces instead of names:  Ralf Jung committed Oct 10, 2016 472 $\knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop}$  Ralf Jung committed Oct 21, 2016 473 We can now derive the following rules (this involves unfolding the definition of fancy updates):  Ralf Jung committed Oct 10, 2016 474 475 \begin{mathpar} \axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}  Ralf Jung committed Oct 04, 2016 476   Jacques-Henri Jourdan committed Oct 13, 2016 477  \axiomH{inv-alloc}{\later\prop \proves \pvs[\emptyset] \knowInv\namesp\prop}  Ralf Jung committed Oct 04, 2016 478   Ralf Jung committed Oct 10, 2016 479 480 481  \inferH{inv-open} {\namesp \subseteq \mask} {\knowInv\namesp\prop \vs[\mask][\mask\setminus\namesp] \later\prop * (\later\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)}  Ralf Jung committed Oct 04, 2016 482   Ralf Jung committed Oct 10, 2016 483 484 485 486  \inferH{inv-open-timeless} {\namesp \subseteq \mask \and \timeless\prop} {\knowInv\namesp\prop \vs[\mask][\mask\setminus\namesp] \prop * (\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)} \end{mathpar}  Ralf Jung committed Oct 04, 2016 487   Ralf Jung committed Oct 10, 2016 488 489 490 491 \subsection{Accessors} The two rules \ruleref{inv-open} and \ruleref{inv-open-timeless} above may look a little surprising, in the sense that it is not clear on first sight how they would be applied. The rules are the first \emph{accessors} that show up in this document.  Robbert Krebbers committed Dec 10, 2017 492 Accessors are propositions of the form  Ralf Jung committed Oct 10, 2016 493 494 $\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC)$  Robbert Krebbers committed Dec 10, 2017 495 496 One way to think about such propositions is as follows: Given some accessor, if during our verification we have the proposition $\prop$ and the mask $\mask_1$ available, we can use the accessor to \emph{access} $\propB$ and obtain the witness $\var$.  Ralf Jung committed Oct 10, 2016 497 498 499 500 501 We call this \emph{opening} the accessor, and it changes the mask to $\mask_2$. Additionally, opening the accessor provides us with $\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC$, a \emph{linear view shift} (\ie a view shift that can only be used once). This linear view shift tells us that in order to \emph{close} the accessor again and go back to mask $\mask_1$, we have to pick some $\varB$ and establish the corresponding $\propB'$. After closing, we will obtain $\propC$.  Ralf Jung committed Feb 02, 2017 502 503 504 505 506 507 508 509 510 511 512 513 514 515 Using \ruleref{vs-trans} and \ruleref{Ht-atomic} (or the corresponding proof rules for fancy updates and weakest preconditions), we can show that it is possible to open an accessor around any view shift and any \emph{atomic} expression: \begin{mathpar} \inferH{Acc-vs} {\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC) \and \All\var. \propB * \prop_F \vs[\mask_2] \Exists\varB. \propB' * \prop_F} {\prop * \prop_F \vs[\mask_1] \propC * \prop_F} \inferH{Acc-Ht} {\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC) \and \All\var. \hoare{\propB * \prop_F}\expr{\Exists\varB. \propB' * \prop_F}[\mask_2] \and \physatomic\expr} {\hoare{\prop * \prop_F}\expr{\propC * \prop_F}[\mask_1]} \end{mathpar}  Ralf Jung committed Oct 10, 2016 516 517 518 519 520 Furthermore, in the special case that $\mask_1 = \mask_2$, the accessor can be opened around \emph{any} expression. For this reason, we also call such accessors \emph{non-atomic}. The reasons accessors are useful is that they let us talk about opening X'' (\eg opening invariants'') without having to care what X is opened around. Furthermore, as we construct more sophisticated and more interesting things that can be opened (\eg invariants that can be cancelled'', or STSs), accessors become a useful interface that allows us to mix and match different abstractions in arbitrary ways.  Ralf Jung committed Oct 04, 2016 521   Ralf Jung committed Dec 06, 2016 522 523 For the special case that $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition: $\Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop)$  Robbert Krebbers committed Dec 10, 2017 524 This accessor is idempotent'' in the sense that it does not actually change the state. After applying it, we get our $\prop$ back so we end up where we started.  Ralf Jung committed Dec 06, 2016 525   Ralf Jung committed Oct 04, 2016 526 527 528 529 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: