derived.tex 16.7 KB
 Ralf Jung committed Mar 07, 2016 1 2 3 4 5 6 \section{Derived proof rules} \subsection{Base logic} \ralf{Give the most important derived rules.} Ralf Jung committed Mar 07, 2016 7 8 9 10 11 12 \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 13 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 14 15 16 17 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 07, 2016 18 19 20 \subsection{Program logic} \ralf{Sync this with Coq.} Ralf Jung committed Mar 06, 2016 21 22 Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively: Ralf Jung committed Mar 07, 2016 23 24 25 26 27 28 29 30 \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}{\lambda\Ret\val.\propB}[\mask])} \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 31 We write just one mask for a view shift when $\mask_1 = \mask_2$. Ralf Jung committed Mar 07, 2016 32 33 Clearly, all of these assertions are persistent. The convention for omitted masks is similar to the base logic: Ralf Jung committed Mar 06, 2016 34 35 36 An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts. Ralf Jung committed Mar 07, 2016 37 38 \paragraph{View shifts.}~ The following rules can be derived for view shifts. Ralf Jung committed Mar 06, 2016 39 Ralf Jung committed Mar 07, 2016 40 41 \begin{mathparpagebreakable} \inferH{vs-update} Ralf Jung committed Mar 06, 2016 42 43 44 {\melt \mupd \meltsB} {\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}} \and Ralf Jung committed Mar 07, 2016 45 \inferH{vs-trans} Ralf Jung committed Mar 06, 2016 46 47 48 {\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 49 \inferH{vs-imp} Ralf Jung committed Mar 06, 2016 50 51 52 {\always{(\prop \Ra \propB)}} {\prop \vs[\emptyset] \propB} \and Ralf Jung committed Mar 07, 2016 53 \inferH{vs-mask-frame} Ralf Jung committed Mar 06, 2016 54 {\prop \vs[\mask_1][\mask_2] \propB} Ralf Jung committed Mar 07, 2016 55 {\prop \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB} Ralf Jung committed Mar 06, 2016 56 \and Ralf Jung committed Mar 07, 2016 57 58 59 60 61 \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 62 63 64 {\timeless{\prop}} {\later \prop \vs \prop} \and Ralf Jung committed Mar 07, 2016 65 66 67 68 69 \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 70 71 {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop} \and Ralf Jung committed Mar 07, 2016 72 \axiomH{vs-closeI} Ralf Jung committed Mar 06, 2016 73 74 {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE } Ralf Jung committed Mar 07, 2016 75 \inferHB{vs-disj} Ralf Jung committed Mar 06, 2016 76 77 78 {\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 79 \inferHB{vs-exist} Ralf Jung committed Mar 06, 2016 80 81 82 {\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 83 \inferHB{vs-box} Ralf Jung committed Mar 07, 2016 84 {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC} Ralf Jung committed Mar 06, 2016 85 86 {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC} \and Ralf Jung committed Mar 07, 2016 87 \inferH{vs-false} Ralf Jung committed Mar 06, 2016 88 89 {} {\FALSE \vs[\mask_1][\mask_2] \prop } Ralf Jung committed Mar 07, 2016 90 \end{mathparpagebreakable} Ralf Jung committed Mar 06, 2016 91 92 Ralf Jung committed Mar 07, 2016 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 \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 129 } Ralf Jung committed Mar 07, 2016 130 {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']} Ralf Jung committed Mar 06, 2016 131 \and Ralf Jung committed Mar 07, 2016 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 \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 148 Ralf Jung committed Mar 07, 2016 149 \clearpage Ralf Jung committed Jan 31, 2016 150 151 \section{Derived constructions} Ralf Jung committed Mar 07, 2016 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 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 In this section we describe some derived constructions that are generally useful and language-independent. \ralf{Describe at least global monoid and invariant namespaces.} % \subsection{Global monoid} % Hereinafter we assume the global monoid (served up as a parameter to Iris) is obtained from a family of monoids $(M_i)_{i \in I}$ by first applying the construction for finite partial functions to each~(\Sref{sec:fpfunm}), and then applying the product construction~(\Sref{sec:prodm}): % $M \eqdef \prod_{i \in I} \textdom{GhName} \fpfn M_i$ % We don't care so much about what concretely $\textdom{GhName}$ is, as long as it is countable and infinite. % 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]]}$ when $\melt \in \mcarp {M_i}$, and for $\FALSE$ when $\melt = \mzero_{M_i}$. % In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the name $\gname$ is allocated and has at least value $\melt$. % From~\ruleref{FpUpd} and the multiplications and frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfunm}, we have the following derived rules. % \begin{mathpar} % \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{GhostUnit} % {\TRUE \Ra \ownGhost{\gname}{\munit : M_i}} % \axiomH{GhostZero} % {\ownGhost\gname{\mzero : M_i} \Ra \FALSE} % \axiomH{GhostTimeless} % {\timeless{\ownGhost\gname{\melt : M_i}}} % \end{mathpar} % \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 215 Ralf Jung committed Mar 07, 2016 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 % 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 232 Ralf Jung committed Mar 07, 2016 233 234 % 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 235 Ralf Jung committed Mar 07, 2016 236 237 238 % 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 239 Ralf Jung committed Mar 07, 2016 240 241 % 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 242 Ralf Jung committed Mar 07, 2016 243 % This holds by our premise. Ralf Jung committed Jan 31, 2016 244 % \end{proof} Ralf Jung committed Jan 31, 2016 245 Ralf Jung committed Mar 07, 2016 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 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 % % \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}% % 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 337 Ralf Jung committed Jan 31, 2016 338 339 340 341 342 %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: