derived.tex 21.3 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 208 209 210 211 \paragraph{Lifting of operational semantics.} We can derive some specialized forms of the lifting axioms for the operational semantics, as well as some forms that involve view shifts and Hoare triples. \ralf{Add these.}  Ralf Jung committed Mar 10, 2016 212 \subsection{Global functor and ghost ownership}  Ralf Jung committed Mar 11, 2016 213 214  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 215 216 $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 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 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} \inferH{NewGhostStrong}{\text{$G$ infinite}} { \TRUE \vs \Exists\gname\in G. \ownGhost\gname{\melt : M_i} } \and \axiomH{NewGhost}{ \TRUE \vs \Exists\gname. \ownGhost\gname{\melt : M_i} } \and \inferH{GhostUpd} {\melt \mupd_{M_i} B} {\ownGhost\gname{\melt : M_i} \vs \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}} \and \axiomH{GhostEq} {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \Lra \ownGhost\gname{\melt\mtimes\meltB : M_i}} \axiomH{GhostVal} {\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)} \inferH{GhostTimeless} {\text{$\melt$ is a discrete COFE element}} {\timeless{\ownGhost\gname{\melt : M_i}}} \end{mathparpagebreakable}  Ralf Jung committed Mar 07, 2016 244   Ralf Jung committed Mar 08, 2016 245 \subsection{Invariant identifier namespaces}  Ralf Jung committed Mar 11, 2016 246 247 248 249 250 251 252  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 253 We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$.  Ralf Jung committed Mar 11, 2016 254 255  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 256 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 257   Ralf Jung committed Mar 11, 2016 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 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 284   Ralf Jung committed Mar 07, 2016 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 % \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 314   Ralf Jung committed Mar 07, 2016 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 % 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 331   Ralf Jung committed Mar 07, 2016 332 333 % 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 334   Ralf Jung committed Mar 07, 2016 335 336 337 % 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 338   Ralf Jung committed Mar 07, 2016 339 340 % 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 341   Ralf Jung committed Mar 07, 2016 342 % This holds by our premise.  Ralf Jung committed Jan 31, 2016 343 % \end{proof}  Ralf Jung committed Jan 31, 2016 344   Ralf Jung committed Mar 07, 2016 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 370 371 372 373 374 375 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 % % \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} % {\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}}} % \and % \axiomH{AuthClose} % {\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}} } % \end{mathpar} % These view shifts in turn can be used to prove variants of the invariant rules: % \begin{mathpar} % \inferH{Auth} % {\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] % \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} % {\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)} % {\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 408 % FIXME use the finmap provided by the global ghost ownership, instead of adding our own  Ralf Jung committed Mar 07, 2016 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 % 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 436   Ralf Jung committed Jan 31, 2016 437 438 439 440 441  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: