derived.tex 25 KB
 Ralf Jung committed Mar 08, 2016 1 \section{Derived proof rules and other constructions}  Ralf Jung committed Mar 07, 2016 2   Ralf Jung committed Mar 12, 2016 3 4 5 6 7 We will below abuse notation, using the \emph{term} meta-variables like $\val$ to range over (bound) \emph{variables} of the corresponding type.. We omit type annotations in binders and equality, when the type is clear from context. We assume that the signature $\Sig$ embeds all the meta-level concepts we use, and their properties, into the logic. (The Coq formalization is a \emph{shallow embedding} of the logic, so we have direct access to all meta-level notions within the logic anyways.)  Ralf Jung committed Mar 07, 2016 8 9 \subsection{Base logic}  Ralf Jung committed Mar 08, 2016 10 11 12 13 14 15 We collect here some important and frequently used derived proof rules. \begin{mathparpagebreakable} \infer{} {\prop \Ra \propB \proves \prop \wand \propB} \infer{}  Ralf Jung committed Mar 08, 2016 16  {\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB}  Ralf Jung committed Mar 08, 2016 17 18 19 20 21  \infer{} {\prop * \Exists\var.\propB \proves \Exists\var. \prop * \propB} \infer{}  Ralf Jung committed Mar 08, 2016 22  {\always(\prop*\propB) \provesIff \always\prop * \always\propB}  Ralf Jung committed Mar 08, 2016 23 24 25 26 27 28 29 30  \infer{} {\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB} \infer{} {\always(\prop \wand \propB) \proves \always\prop \wand \always\propB} \infer{}  Ralf Jung committed Mar 08, 2016 31  {\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}  Ralf Jung committed Mar 08, 2016 32 33 34 35 36 37 38 39 40 41 42  \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}  Ralf Jung committed Mar 07, 2016 43   Ralf Jung committed Mar 07, 2016 44 45 46 47 48 49 \paragraph{Persistent assertions.} \begin{defn} An assertion $\prop$ is \emph{persistent} if $\prop \proves \always\prop$. \end{defn} Of course, $\always\prop$ is persistent for any $\prop$.  Ralf Jung committed Mar 08, 2016 50 Furthermore, by the proof rules given above, $t = t'$ as well as $\ownGGhost{\mcore\melt}$ and $\knowInv\iname\prop$ are persistent.  Ralf Jung committed Mar 07, 2016 51 52 53 54 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.  Ralf Jung committed Mar 08, 2016 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 \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}  Ralf Jung committed Mar 07, 2016 78 79 \subsection{Program logic}  Ralf Jung committed Mar 06, 2016 80 Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively:  Ralf Jung committed Mar 07, 2016 81  Ralf Jung committed Mar 08, 2016 82 \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\lambda\Ret\val.\propB})}  Ralf Jung committed Mar 07, 2016 83 84 85 86 87 88 \qquad\qquad \begin{aligned} \prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvs[\mask_1][\mask_2] {\propB})} \\ \prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop \end{aligned}  Ralf Jung committed Mar 06, 2016 89 We write just one mask for a view shift when $\mask_1 = \mask_2$.  Ralf Jung committed Mar 07, 2016 90 91 Clearly, all of these assertions are persistent. The convention for omitted masks is similar to the base logic:  Ralf Jung committed Mar 06, 2016 92 93 94 An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts.  Ralf Jung committed Mar 08, 2016 95 \paragraph{View shifts.}  Ralf Jung committed Mar 07, 2016 96 The following rules can be derived for view shifts.  Ralf Jung committed Mar 06, 2016 97   Ralf Jung committed Mar 07, 2016 98 99 \begin{mathparpagebreakable} \inferH{vs-update}  Ralf Jung committed Mar 06, 2016 100 101 102  {\melt \mupd \meltsB} {\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}} \and  Ralf Jung committed Mar 07, 2016 103 \inferH{vs-trans}  Ralf Jung committed Mar 06, 2016 104 105 106  {\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  Ralf Jung committed Mar 07, 2016 107 \inferH{vs-imp}  Ralf Jung committed Mar 06, 2016 108 109 110  {\always{(\prop \Ra \propB)}} {\prop \vs[\emptyset] \propB} \and  Ralf Jung committed Mar 07, 2016 111 \inferH{vs-mask-frame}  Ralf Jung committed Mar 06, 2016 112  {\prop \vs[\mask_1][\mask_2] \propB}  Ralf Jung committed Mar 07, 2016 113  {\prop \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB}  Ralf Jung committed Mar 06, 2016 114 \and  Ralf Jung committed Mar 07, 2016 115 116 117 118 119 \inferH{vs-frame} {\prop \vs[\mask_1][\mask_2] \propB} {\prop * \propC \vs[\mask_1][\mask_2] \propB * \propC} \and \inferH{vs-timeless}  Ralf Jung committed Mar 06, 2016 120 121 122  {\timeless{\prop}} {\later \prop \vs \prop} \and  Ralf Jung committed Mar 07, 2016 123 124 125 126 127 \inferH{vs-allocI} {\infinite(\mask)} {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}} \and \axiomH{vs-openI}  Ralf Jung committed Mar 06, 2016 128 129  {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop} \and  Ralf Jung committed Mar 07, 2016 130 \axiomH{vs-closeI}  Ralf Jung committed Mar 06, 2016 131 132  {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE }  Ralf Jung committed Mar 07, 2016 133 \inferHB{vs-disj}  Ralf Jung committed Mar 06, 2016 134 135 136  {\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  Ralf Jung committed Mar 07, 2016 137 \inferHB{vs-exist}  Ralf Jung committed Mar 06, 2016 138 139 140  {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)} {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB} \and  Ralf Jung committed Mar 07, 2016 141 \inferHB{vs-box}  Ralf Jung committed Mar 07, 2016 142  {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC}  Ralf Jung committed Mar 06, 2016 143 144  {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC} \and  Ralf Jung committed Mar 07, 2016 145 \inferH{vs-false}  Ralf Jung committed Mar 06, 2016 146 147  {} {\FALSE \vs[\mask_1][\mask_2] \prop }  Ralf Jung committed Mar 07, 2016 148 \end{mathparpagebreakable}  Ralf Jung committed Mar 06, 2016 149 150   Ralf Jung committed Mar 07, 2016 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 177 178 179 180 181 182 183 184 185 186 \paragraph{Hoare triples.} The following rules can be derived for Hoare triples. \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} {\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask]} \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}  Ralf Jung committed Mar 06, 2016 187  }  Ralf Jung committed Mar 07, 2016 188  {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']}  Ralf Jung committed Mar 06, 2016 189 \and  Ralf Jung committed Mar 07, 2016 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 \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-false} {} {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]} \end{mathparpagebreakable}  Ralf Jung committed Mar 06, 2016 206   Ralf Jung committed Mar 08, 2016 207 \paragraph{Lifting of operational semantics.}  Ralf Jung committed Mar 12, 2016 208 209 210 We can derive some specialized forms of the lifting axioms for the operational semantics. \begin{mathparpagebreakable} \infer[wp-lift-atomic-step]  Ralf Jung committed Mar 12, 2016 211  {\atomic(\expr_1) \and  Ralf Jung committed Mar 12, 2016 212  \red(\expr_1, \state_1) \and  Ralf Jung committed Mar 12, 2016 213 214  \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f)} {\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. \pred(\ofval(\val), \state_2, \expr_\f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}  Ralf Jung committed Mar 12, 2016 215 216  \infer[wp-lift-atomic-det-step]  Ralf Jung committed Mar 12, 2016 217  {\atomic(\expr_1) \and  Ralf Jung committed Mar 12, 2016 218  \red(\expr_1, \state_1) \and  Ralf Jung committed Mar 12, 2016 219 220  \All \expr'_2, \state'_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_\f = \expr_\f'} {\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}  Ralf Jung committed Mar 12, 2016 221 222 223 224  \infer[wp-lift-pure-det-step] {\toval(\expr_1) = \bot \and \All \state_1. \red(\expr_1, \state_1) \and  Ralf Jung committed Mar 12, 2016 225 226  \All \state_1, \expr_2', \state_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_\f = \expr_\f'} {\later ( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}  Ralf Jung committed Mar 12, 2016 227 \end{mathparpagebreakable}  Ralf Jung committed Mar 08, 2016 228   Ralf Jung committed Mar 12, 2016 229 230 231 232 233 234 Furthermore, we derive some forms that directly involve view shifts and Hoare triples. \begin{mathparpagebreakable} \infer[ht-lift-step] {\mask_2 \subseteq \mask_1 \and \toval(\expr_1) = \bot \and \red(\expr_1, \state_1) \and  Ralf Jung committed Mar 12, 2016 235  \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f) \\\\  Ralf Jung committed Mar 12, 2016 236  \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and  Ralf Jung committed Mar 12, 2016 237 238 239  \All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) * \ownPhys{\state_2} * \prop' \vs[\mask_2][\mask_1] \propB_1 * \propB_2 \\\\ \All \expr_2, \state_2, \expr_\f. \hoare{\propB_1}{\expr_2}{\Ret\val.\propC}[\mask_1] \and \All \expr_2, \state_2, \expr_\f. \hoare{\propB_2}{\expr_\f}{\Ret\any. \TRUE}[\top]}  Ralf Jung committed Mar 12, 2016 240 241 242 243 244  { \hoare\prop{\expr_1}{\Ret\val.\propC}[\mask_1] } \infer[ht-lift-atomic-step] {\atomic(\expr_1) \and \red(\expr_1, \state_1) \and  Ralf Jung committed Mar 12, 2016 245  \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f) \\\\  Ralf Jung committed Mar 12, 2016 246  \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and  Ralf Jung committed Mar 12, 2016 247 248  \All \expr_2, \state_2, \expr_\f. \hoare{\pred(\expr_2,\state_2,\expr_\f) * \prop}{\expr_\f}{\Ret\any. \TRUE}[\top]} { \hoare{\later\ownPhys{\state_1} * \later\prop}{\expr_1}{\Ret\val.\Exists \state_2, \expr_\f. \ownPhys{\state_2} * \pred(\ofval(\expr_2),\state_2,\expr_\f)}[\mask_1] }  Ralf Jung committed Mar 12, 2016 249 250 251 252  \infer[ht-lift-pure-step] {\toval(\expr_1) = \bot \and \All\state_1. \red(\expr_1, \state_1) \and  Ralf Jung committed Mar 12, 2016 253 254 255  \All \state_1, \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_\f) \\\\ \All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and \All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]}  Ralf Jung committed Mar 12, 2016 256 257 258 259 260  { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] } \infer[ht-lift-pure-det-step] {\toval(\expr_1) = \bot \and \All\state_1. \red(\expr_1, \state_1) \and  Ralf Jung committed Mar 12, 2016 261  \All \state_1, \expr_2', \state_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_\f = \expr_\f' \\\\  Ralf Jung committed Mar 12, 2016 262  \hoare{\prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and  Ralf Jung committed Mar 12, 2016 263  \hoare{\prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]}  Ralf Jung committed Mar 12, 2016 264 265  { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] } \end{mathparpagebreakable}  Ralf Jung committed Mar 08, 2016 266   Ralf Jung committed Mar 10, 2016 267 \subsection{Global functor and ghost ownership}  Ralf Jung committed Mar 11, 2016 268 269  Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(F_i)_{i \in I}$ for some finite $I$ by picking  Ralf Jung committed Mar 11, 2016 270 271 $F(\cofe) \eqdef \prod_{i \in I} \textlog{GhName} \fpfn F_i(\cofe)$ We don't care so much about what concretely $\textlog{GhName}$ is, as long as it is countable and infinite.  Ralf Jung committed Mar 11, 2016 272 273 274 275 276 With $M_i \eqdef F_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto [\gname \mapsto \melt]]}$. In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the ghost location'' $\gname$ is allocated and we own piece $\melt$. From~\ruleref{pvs-update}, \ruleref{vs-update} and the frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfnm}, we have the following derived rules. \begin{mathparpagebreakable}  Ralf Jung committed Mar 15, 2016 277  \inferH{ghost-alloc-strong}{\text{$G$ infinite}}  Ralf Jung committed Mar 11, 2016 278 279 280  { \TRUE \vs \Exists\gname\in G. \ownGhost\gname{\melt : M_i} } \and  Ralf Jung committed Mar 15, 2016 281  \axiomH{ghost-alloc}{  Ralf Jung committed Mar 11, 2016 282 283 284  \TRUE \vs \Exists\gname. \ownGhost\gname{\melt : M_i} } \and  Ralf Jung committed Mar 15, 2016 285  \inferH{ghost-update}  Ralf Jung committed Mar 11, 2016 286 287 288  {\melt \mupd_{M_i} B} {\ownGhost\gname{\melt : M_i} \vs \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}} \and  Ralf Jung committed Mar 15, 2016 289  \axiomH{ghost-op}  Ralf Jung committed Mar 11, 2016 290 291  {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \Lra \ownGhost\gname{\melt\mtimes\meltB : M_i}}  Ralf Jung committed Mar 15, 2016 292  \axiomH{ghost-valid}  Ralf Jung committed Mar 11, 2016 293 294  {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}  Ralf Jung committed Mar 15, 2016 295  \inferH{ghost-timeless}  Ralf Jung committed Mar 11, 2016 296 297 298  {\text{$\melt$ is a discrete COFE element}} {\timeless{\ownGhost\gname{\melt : M_i}}} \end{mathparpagebreakable}  Ralf Jung committed Mar 07, 2016 299   Ralf Jung committed Mar 08, 2016 300 \subsection{Invariant identifier namespaces}  Ralf Jung committed Mar 11, 2016 301 302 303 304 305 306 307  Let $\namesp \ni \textlog{InvNamesp} \eqdef \textlog{list}(\textlog{InvName})$ be the type of \emph{namespaces} for invariant names. Notice that there is an injection $\textlog{namesp\_inj}: \textlog{InvNamesp} \ra \textlog{InvName}$. Whenever needed (in particular, for masks at view shifts and Hoare triples), we coerce $\namesp$ to its suffix-closure: $\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}$ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$. We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$.  Ralf Jung committed Mar 12, 2016 308 We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$.  Ralf Jung committed Mar 11, 2016 309 310  Similarly, we define $\namesp_1 \sep \namesp_2 \eqdef \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.  Ralf Jung committed Mar 12, 2016 311 We have that $\namesp_1 \sep \namesp_2 \Ra \namecl{\namesp_2} \sep \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$.  Ralf Jung committed Mar 11, 2016 312   Ralf Jung committed Mar 11, 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 We will overload the usual Iris notation for invariant assertions in the following: $\knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop}$ We can now derive the following rules for this derived form of the invariant assertion: \begin{mathpar} \axiom{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop} \axiom{\later\prop \proves \pvs[\namesp] \knowInv\namesp\prop} \infer{\physatomic{\expr} \and \namesp \subseteq \mask \and \pfctx \proves \knowInv\namesp\prop \and \pfctx \proves \later\prop \wand \wpre\expr[\mask \setminus \namesp]{\Ret\val.\later\prop * \propB}} {\pfctx \proves \wpre\expr[\mask]{\Ret\val.\propB}} \infer{\namesp \subseteq \mask \and \pfctx \proves \knowInv\namesp\prop \and \pfctx \proves \later\prop \wand \pvs[\mask \setminus \namesp]{\later\prop * \propB}} {\pfctx \proves \pvs[\mask]{\propB}} \infer{\physatomic{\expr} \and \namesp \subseteq \mask \and \hoare{\later\prop*\propB}\expr{\Ret\val.\later\prop*\propC}[\mask \setminus \namesp]} {\knowInv\namesp\prop \proves \hoare\propB\expr{\Ret\val.\propC}[\mask]} \infer{\namesp \subseteq \mask \and \later\prop*\propB \vs[\mask \setminus \namesp] \later\prop*\propC} {\knowInv\namesp\prop \proves \propB \vs[\mask] \propC} \end{mathpar}  Ralf Jung committed Mar 08, 2016 339   Ralf Jung committed Mar 12, 2016 340 % TODO: These need syncing with Coq  Ralf Jung committed Mar 07, 2016 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 % \subsection{STSs with interpretation}\label{sec:stsinterp} % Building on \Sref{sec:stsmon}, after constructing the monoid $\STSMon{\STSS}$ for a particular STS, we can use an invariant to tie an interpretation, $\pred : \STSS \to \Prop$, to the STS's current state, recovering CaReSL-style reasoning~\cite{caresl}. % An STS invariant asserts authoritative ownership of an STS's current state and that state's interpretation: % \begin{align*} % \STSInv(\STSS, \pred, \gname) \eqdef{}& \Exists s \in \STSS. \ownGhost{\gname}{(s, \STSS, \emptyset):\STSMon{\STSS}} * \pred(s) \\ % \STS(\STSS, \pred, \gname, \iname) \eqdef{}& \knowInv{\iname}{\STSInv(\STSS, \pred, \gname)} % \end{align*} % We can specialize \ruleref{NewInv}, \ruleref{InvOpen}, and \ruleref{InvClose} to STS invariants: % \begin{mathpar} % \inferH{NewSts} % {\infinite(\mask)} % {\later\pred(s) \vs[\mask] \Exists \iname \in \mask, \gname. \STS(\STSS, \pred, \gname, \iname) * \ownGhost{\gname}{(s, \STST \setminus \STSL(s)) : \STSMon{\STSS}}} % \and % \axiomH{StsOpen} % { \STS(\STSS, \pred, \gname, \iname) \vdash \ownGhost{\gname}{(s_0, T) : \STSMon{\STSS}} \vsE[\{\iname\}][\emptyset] \Exists s\in \upclose(\{s_0\}, T). \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T):\STSMon{\STSS}}} % \and % \axiomH{StsClose} % { \STS(\STSS, \pred, \gname, \iname), (s, T) \ststrans (s', T') \proves \later\pred(s') * \ownGhost{\gname}{(s, S, T):\STSMon{\STSS}} \vs[\emptyset][\{\iname\}] \ownGhost{\gname}{(s', T') : \STSMon{\STSS}} } % \end{mathpar} % \begin{proof} % \ruleref{NewSts} uses \ruleref{NewGhost} to allocate $\ownGhost{\gname}{(s, \upclose(s, T), T) : \STSMon{\STSS}}$ where $T \eqdef \STST \setminus \STSL(s)$, and \ruleref{NewInv}. % \ruleref{StsOpen} just uses \ruleref{InvOpen} and \ruleref{InvClose} on $\iname$, and the monoid equality $(s, \upclose(\{s_0\}, T), T) = (s, \STSS, \emptyset) \mtimes (\munit, \upclose(\{s_0\}, T), T)$. % \ruleref{StsClose} applies \ruleref{StsStep} and \ruleref{InvClose}. % \end{proof}  Ralf Jung committed Jan 31, 2016 370   Ralf Jung committed Mar 07, 2016 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 % Using these view shifts, we can prove STS variants of the invariant rules \ruleref{Inv} and \ruleref{VSInv}~(compare the former to CaReSL's island update rule~\cite{caresl}): % \begin{mathpar} % \inferH{Sts} % {\All s \in \upclose(\{s_0\}, T). \hoare{\later\pred(s) * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * Q}[\mask] % \and \physatomic{\expr}} % { \STS(\STSS, \pred, \gname, \iname) \vdash \hoare{\ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P}{\expr}{\Ret \val. \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q}[\mask \uplus \{\iname\}]} % \and % \inferH{VSSts} % {\forall s \in \upclose(\{s_0\}, T).\; \later\pred(s) * P \vs[\mask_1][\mask_2] \exists s', T'.\; (s, T) \ststrans (s', T') * \later\pred(s') * Q} % { \STS(\STSS, \pred, \gname, \iname) \vdash \ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P \vs[\mask_1 \uplus \{\iname\}][\mask_2 \uplus \{\iname\}] \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q} % \end{mathpar} % \begin{proof}[Proof of \ruleref{Sts}]\label{pf:sts} % We have to show % $\hoare{\ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P}{\expr}{\Ret \val. \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q}[\mask \uplus \{\iname\}]$ % where $\val$, $s'$, $T'$ are free in $Q$.  Ralf Jung committed Jan 31, 2016 387   Ralf Jung committed Mar 07, 2016 388 389 % First, by \ruleref{ACsq} with \ruleref{StsOpen} and \ruleref{StsClose} (after moving $(s, T) \ststrans (s', T')$ into the view shift using \ruleref{VSBoxOut}), it suffices to show % $\hoareV{\Exists s\in \upclose(\{s_0\}, T). \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * P}{\expr}{\Ret \val. \Exists s, T, S, s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * \ownGhost{\gname}{(s, S, T):\STSMon{\STSS}} * Q(\val, s', T')}[\mask]$  Ralf Jung committed Jan 31, 2016 390   Ralf Jung committed Mar 07, 2016 391 392 393 % Now, use \ruleref{Exist} to move the $s$ from the precondition into the context and use \ruleref{Csq} to (i)~fix the $s$ and $T$ in the postcondition to be the same as in the precondition, and (ii)~fix $S \eqdef \upclose(\{s_0\}, T)$. % It remains to show: % $\hoareV{s\in \upclose(\{s_0\}, T) * \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * Q(\val, s', T')}[\mask]$  Ralf Jung committed Jan 31, 2016 394   Ralf Jung committed Mar 07, 2016 395 396 % Finally, use \ruleref{BoxOut} to move $s\in \upclose(\{s_0\}, T)$ into the context, and \ruleref{Frame} on $\ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)}$: % $s\in \upclose(\{s_0\}, T) \vdash \hoare{\later\pred(s) * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * Q(\val, s', T')}[\mask]$  Ralf Jung committed Jan 31, 2016 397   Ralf Jung committed Mar 07, 2016 398 % This holds by our premise.  Ralf Jung committed Jan 31, 2016 399 % \end{proof}  Ralf Jung committed Jan 31, 2016 400   Ralf Jung committed Mar 07, 2016 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 % % \begin{proof}[Proof of \ruleref{VSSts}] % % This is similar to above, so we only give the proof in short notation: % % \hproof{% % % Context: $\knowInv\iname{\STSInv(\STSS, \pred, \gname)}$ \\ % % \pline[\mask_1 \uplus \{\iname\}]{ % % \ownGhost\gname{(s_0, T)} * P % % } \\ % % \pline[\mask_1]{% % % \Exists s. \later\pred(s) * \ownGhost\gname{(s, S, T)} * P % % } \qquad by \ruleref{StsOpen} \\ % % Context: $s \in S \eqdef \upclose(\{s_0\}, T)$ \\ % % \pline[\mask_2]{% % % \Exists s', T'. \later\pred(s') * Q(s', T') * \ownGhost\gname{(s, S, T)} % % } \qquad by premiss \\ % % Context: $(s, T) \ststrans (s', T')$ \\ % % \pline[\mask_2 \uplus \{\iname\}]{ % % \ownGhost\gname{(s', T')} * Q(s', T') % % } \qquad by \ruleref{StsClose} % % } % % \end{proof} % \subsection{Authoritative monoids with interpretation}\label{sec:authinterp} % Building on \Sref{sec:auth}, after constructing the monoid $\auth{M}$ for a cancellative monoid $M$, we can tie an interpretation, $\pred : \mcarp{M} \to \Prop$, to the authoritative element of $M$, recovering reasoning that is close to the sharing rule in~\cite{krishnaswami+:icfp12}. % Let $\pred_\bot$ be the extension of $\pred$ to $\mcar{M}$ with $\pred_\bot(\mzero) = \FALSE$. % Now define % \begin{align*} % \AuthInv(M, \pred, \gname) \eqdef{}& \exists \melt \in \mcar{M}.\; \ownGhost{\gname}{\authfull \melt:\auth{M}} * \pred_\bot(\melt) \\ % \Auth(M, \pred, \gname, \iname) \eqdef{}& M~\textlog{cancellative} \land \knowInv{\iname}{\AuthInv(M, \pred, \gname)} % \end{align*} % The frame-preserving updates for $\auth{M}$ gives rise to the following view shifts: % \begin{mathpar} % \inferH{NewAuth} % {\infinite(\mask) \and M~\textlog{cancellative}} % {\later\pred_\bot(a) \vs[\mask] \exists \iname \in \mask, \gname.\; \Auth(M, \pred, \gname, \iname) * \ownGhost{\gname}{\authfrag a : \auth{M}}} % \and % \axiomH{AuthOpen}  Ralf Jung committed Mar 12, 2016 441 % {\Auth(M, \pred, \gname, \iname) \vdash \ownGhost{\gname}{\authfrag \melt : \auth{M}} \vsE[\{\iname\}][\emptyset] \exists \melt_\f.\; \later\pred_\bot(\melt \mtimes \melt_\f) * \ownGhost{\gname}{\authfull \melt \mtimes \melt_\f, \authfrag a:\auth{M}}}  Ralf Jung committed Mar 07, 2016 442 443 % \and % \axiomH{AuthClose}  Ralf Jung committed Mar 12, 2016 444 % {\Auth(M, \pred, \gname, \iname) \vdash \later\pred_\bot(\meltB \mtimes \melt_\f) * \ownGhost{\gname}{\authfull a \mtimes \melt_\f, \authfrag a:\auth{M}} \vs[\emptyset][\{\iname\}] \ownGhost{\gname}{\authfrag \meltB : \auth{M}} }  Ralf Jung committed Mar 07, 2016 445 446 447 448 449 % \end{mathpar} % These view shifts in turn can be used to prove variants of the invariant rules: % \begin{mathpar} % \inferH{Auth}  Ralf Jung committed Mar 12, 2016 450 % {\forall \melt_\f.\; \hoare{\later\pred_\bot(a \mtimes \melt_\f) * P}{\expr}{\Ret\val. \exists \meltB.\; \later\pred_\bot(\meltB\mtimes \melt_\f) * Q}[\mask]  Ralf Jung committed Mar 07, 2016 451 452 453 454 % \and \physatomic{\expr}} % {\Auth(M, \pred, \gname, \iname) \vdash \hoare{\ownGhost{\gname}{\authfrag a:\auth{M}} * P}{\expr}{\Ret\val. \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q}[\mask \uplus \{\iname\}]} % \and % \inferH{VSAuth}  Ralf Jung committed Mar 12, 2016 455 % {\forall \melt_\f.\; \later\pred_\bot(a \mtimes \melt_\f) * P \vs[\mask_1][\mask_2] \exists \meltB.\; \later\pred_\bot(\meltB \mtimes \melt_\f) * Q(\meltB)}  Ralf Jung committed Mar 07, 2016 456 457 458 459 460 461 462 463 % {\Auth(M, \pred, \gname, \iname) \vdash % \ownGhost{\gname}{\authfrag a:\auth{M}} * P \vs[\mask_1 \uplus \{\iname\}][\mask_2 \uplus \{\iname\}] % \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q(\meltB)} % \end{mathpar} % \subsection{Ghost heap} % \label{sec:ghostheap}%  Ralf Jung committed Mar 10, 2016 464 % FIXME use the finmap provided by the global ghost ownership, instead of adding our own  Ralf Jung committed Mar 07, 2016 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 % We define a simple ghost heap with fractional permissions. % Some modules require a few ghost names per module instance to properly manage ghost state, but would like to expose to clients a single logical name (avoiding clutter). % In such cases we use these ghost heaps. % We seek to implement the following interface: % \newcommand{\GRefspecmaps}{\textsf{GMapsTo}}% % \begin{align*} % \exists& {\fgmapsto[]} : \textsort{Val} \times \mathbb{Q}_{>} \times \textsort{Val} \ra \textsort{Prop}.\;\\ % & \All x, q, v. x \fgmapsto[q] v \Ra x \fgmapsto[q] v \land q \in (0, 1] \\ % &\forall x, q_1, q_2, v, w.\; x \fgmapsto[q_1] v * x \fgmapsto[q_2] w \Leftrightarrow x \fgmapsto[q_1 + q_2] v * v = w\\ % & \forall v.\; \TRUE \vs[\emptyset] \exists x.\; x \fgmapsto[1] v \\ % & \forall x, v, w.\; x \fgmapsto[1] v \vs[\emptyset] x \fgmapsto[1] w % \end{align*} % We write $x \fgmapsto v$ for $\exists q.\; x \fgmapsto[q] v$ and $x \gmapsto v$ for $x \fgmapsto[1] v$. % Note that $x \fgmapsto v$ is duplicable but cannot be boxed (as it depends on resources); \ie we have $x \fgmapsto v \Lra x \fgmapsto v * x \fgmapsto v$ but not $x \fgmapsto v \Ra \always x \fgmapsto v$. % To implement this interface, allocate an instance $\gname_G$ of $\FHeap(\textdom{Val})$ and define % $% x \fgmapsto[q] v \eqdef % \begin{cases} % \ownGhost{\gname_G}{x \mapsto (q, v)} & \text{if q \in (0, 1]} \\ % \FALSE & \text{otherwise} % \end{cases} %$ % The view shifts in the specification follow immediately from \ruleref{GhostUpd} and the frame-preserving updates in~\Sref{sec:fheapm}. % The first implication is immediate from the definition. % The second implication follows by case distinction on $q_1 + q_2 \in (0, 1]$.  Ralf Jung committed Jan 31, 2016 492   Ralf Jung committed Jan 31, 2016 493 494 495 496 497  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: