program-logic.tex 18.2 KB
 Ralf Jung committed Oct 06, 2016 1 2 \let\bar\overline  Ralf Jung committed Oct 04, 2016 3 \section{Language}  Ralf Jung committed Oct 06, 2016 4 \label{sec:language}  Ralf Jung committed Oct 04, 2016 5 6 7 8 9 10  A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that \begin{itemize} \item There exist functions $\ofval : \textdom{Val} \to \textdom{Expr}$ and $\toval : \textdom{Expr} \pfn \textdom{val}$ (notice the latter is partial), such that \begin{mathpar} {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All\val. \toval(\ofval(\val)) = \val} \end{mathpar}  Ralf Jung committed Oct 06, 2016 11 12 13 \item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\cup_n \textdom{Expr}^n)$ A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off. We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$, \ie when no threads are forked off. \\  Ralf Jung committed Oct 04, 2016 14 15 16 17 18 19 \item All values are stuck: $\expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot$ \end{itemize} \begin{defn} An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if  Ralf Jung committed Oct 06, 2016 20  $\Exists \expr_2, \state_2, \bar\expr. \expr,\state \step \expr_2,\state_2,\bar\expr$  Ralf Jung committed Oct 04, 2016 21 22 23 24 \end{defn} \begin{defn} An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value:  Ralf Jung committed Oct 06, 2016 25  $\All\state_1, \expr_2, \state_2, \bar\expr. \expr, \state_1 \step \expr_2, \state_2, \bar\expr \Ra \Exists \val_2. \toval(\expr_2) = \val_2$  Ralf Jung committed Oct 04, 2016 26 27 28 29 30 31 32 33 \end{defn} \begin{defn}[Context] A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied: \begin{enumerate}[itemsep=0pt] \item $\lctx$ does not turn non-values into values:\\ $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ \item One can perform reductions below $\lctx$:\\  Ralf Jung committed Oct 06, 2016 34  $\All \expr_1, \state_1, \expr_2, \state_2, \bar\expr. \expr_1, \state_1 \step \expr_2,\state_2,\bar\expr \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\bar\expr$  Ralf Jung committed Oct 04, 2016 35  \item Reductions stay below $\lctx$ until there is a value in the hole:\\  Ralf Jung committed Oct 06, 2016 36  $\All \expr_1', \state_1, \expr_2, \state_2, \bar\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\bar\expr \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\bar\expr$  Ralf Jung committed Oct 04, 2016 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52  \end{enumerate} \end{defn} \subsection{Concurrent language} For any language $\Lang$, we define the corresponding thread-pool semantics. \paragraph{Machine syntax} $\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Expr}^n$ \judgment[Machine reduction]{\cfg{\tpool}{\state} \step \cfg{\tpool'}{\state'}} \begin{mathpar} \infer  Ralf Jung committed Oct 06, 2016 53  {\expr_1, \state_1 \step \expr_2, \state_2, \bar\expr}  Ralf Jung committed Oct 04, 2016 54  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step  Ralf Jung committed Oct 06, 2016 55  \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \bar\expr}{\state_2}}  Ralf Jung committed Oct 04, 2016 56 57 58 59 \end{mathpar} \clearpage \section{Program Logic}  Ralf Jung committed Oct 06, 2016 60 \label{sec:program-logic}  Ralf Jung committed Oct 04, 2016 61   Ralf Jung committed Oct 06, 2016 62 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}.  Ralf Jung committed Oct 06, 2016 63 So in the following, we assume that some language $\Lang$ was fixed.  Ralf Jung committed Oct 06, 2016 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83  \subsection{World Satisfaction, Invariants, View Shifts} 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. We assume to have the following four CMRAs available: \begin{align*} \textmon{State} \eqdef{}& \authm(\exm(\textdom{State})) \\ \textmon{Inv} \eqdef{}& \authm(\mathbb N \fpfn \agm(\latert \iPreProp)) \\ \textmon{En} \eqdef{}& \pset{\mathbb N} \\ \textmon{Dis} \eqdef{}& \finpset{\mathbb N} \end{align*} The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves. Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine. Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created. (We will discuss later how this assumption is discharged.)  Ralf Jung committed Oct 06, 2016 84 \paragraph{World Satisfaction.}  Ralf Jung committed Oct 06, 2016 85 86 We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained: \begin{align*}  Ralf Jung committed Oct 06, 2016 87 88 89 90 91 92 93 94 95 96  W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull \aginj(\latertinj(\wIso(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{align*} \paragraph{Invariants.} The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$: $\knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}{\authfrag \aginj(\latertinj(\wIso(\prop)))}$ \paragraph{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$  Ralf Jung committed Oct 06, 2016 97 98 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$.  Ralf Jung committed Oct 06, 2016 99 100 101 102 103 104 105  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*}  Ralf Jung committed Oct 06, 2016 106 107 We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$, and similar for the view shifts.  Ralf Jung committed Oct 06, 2016 108 109 110 111 112 113 114 115 \ralf{Show some proof rules.} \subsection{Hoare Triples} 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. 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*}  Ralf Jung committed Oct 06, 2016 116 117 118  \textdom{wp} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\ & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \prop) \lor {}\\ & \Bigl(\toval(\expr) = \bot \land \All \state. \ownGhost{\gname_{\textmon{State}}}{\authfull \state} \vsW[\mask][\emptyset] {}\\  Ralf Jung committed Oct 06, 2016 119  &\qquad \red(\expr, \state) * \later\All \expr', \state', \bar\expr. (\expr, \state \step \expr', \state', \bar\expr) \vsW[\emptyset][\mask] {}\\  Ralf Jung committed Oct 06, 2016 120  &\qquad\qquad \ownGhost{\gname_{\textmon{State}}}{\authfull \state'} * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \bar\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\  Ralf Jung committed Oct 06, 2016 121 % (* value case *)  Ralf Jung committed Oct 06, 2016 122  \wpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\mask, \expr, \Lam\val.\prop)  Ralf Jung committed Oct 06, 2016 123 \end{align*}  Ralf Jung committed Oct 06, 2016 124 If we leave away the mask, we assume it to default to $\top$.  Ralf Jung committed Oct 06, 2016 125   Ralf Jung committed Oct 06, 2016 126 127 128 129 130 131 132 This ties the authoritative part of \textmon{State} to the actual physical state of the reduction witnessed by the weakest precondition. 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: $ Derek Dreyer committed Oct 07, 2016 133 \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\Ret\val.\propB})}  Ralf Jung committed Oct 06, 2016 134 $  Ralf Jung committed Oct 06, 2016 135 136  \subsection{Lost stuff}  Ralf Jung committed Oct 04, 2016 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 \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}}  Ralf Jung committed Oct 06, 2016 177 {\timeless{\ownM\melt}}  Ralf Jung committed Oct 04, 2016 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236  \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}  Ralf Jung committed Oct 06, 2016 237 {\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB}  Ralf Jung committed Oct 04, 2016 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 \end{mathpar} \paragraph{Laws of weakest preconditions.} \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}} \infer[pvs-wp] {}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}} \infer[wp-pvs] {}{\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}} {\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} {\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}} \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.}~ \begin{mathpar} \infer[wp-lift-step] {\mask_2 \subseteq \mask_1 \and \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} \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}} \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). The adequacy statement concerning functional correctness reads as follows: \begin{align*} &\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'. \\&(\All n. \melt \in \mval_n) \Ra  Ralf Jung committed Oct 06, 2016 295  \\&( \ownPhys\state * \ownM\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra  Ralf Jung committed Oct 04, 2016 296 297 298 299 300 301 302 303 304 305  \\&\cfg{\state}{[\expr]} \step^\ast \cfg{\state'}{[\val] \dplus \tpool'} \Ra \\&\pred(\val) \end{align*} where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants. Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets \emph{stuck}: Every expression in the thread pool either is a value, or can reduce further. \begin{align*} &\All \mask, \expr, \state, \melt, \state', \tpool'. \\&(\All n. \melt \in \mval_n) \Ra  Ralf Jung committed Oct 06, 2016 306  \\&( \ownPhys\state * \ownM\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra  Ralf Jung committed Oct 04, 2016 307 308 309 310 311 312  \\&\cfg{\state}{[\expr]} \step^\ast \cfg{\state'}{\tpool'} \Ra \\&\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state') \end{align*} 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.  Ralf Jung committed Oct 04, 2016 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 \subsection{Iris model} \paragraph{Semantic domain of assertions.} \paragraph{Interpretation of assertions.} $\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply. We only have to define the interpretation of the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions. \typedsection{World satisfaction}{\wsat{-}{-}{-} : \Delta\textdom{State} \times \Delta\pset{\mathbb{N}} \times \textdom{Res} \nfn \SProp } \begin{align*} \wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t] \rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land \dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\ \All\iname \in \mask, \prop \in \iProp. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname)) \end{inbox}\\ \wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))} \end{align*} \typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp} \begin{align*} \mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned} \All \rs_\f, k, \mask_\f, \state.& 0 < k \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\& \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f} \end{aligned}} \end{align*} \typedsection{Weakest precondition}{\mathit{wp}_{-}(-, -) : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp} $\textdom{wp}$ is defined as the fixed-point of a contractive function. \begin{align*} \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned} \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \disj \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\ &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \pred(\val)(\rsB) \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f}) \land {}\\ &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\ &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rsB_1 \mtimes \rsB_2 \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\ &\qquad\qquad (\expr_\f = \bot \lor m \in \textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2)) \end{aligned}} \\ \textdom{wp}_\mask(\expr, \pred) &\eqdef \mathit{fix}(\textdom{pre-wp})(\mask, \expr, \pred) \end{align*}  Ralf Jung committed Oct 04, 2016 359 360 361 362 363  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: