derived.tex 19.5 KB
 Ralf Jung committed Dec 10, 2017 1 \section{Derived Constructions}  Ralf Jung committed Dec 06, 2016 2   Ralf Jung committed Dec 11, 2017 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 \subsection{Cancellable Invariants} Iris invariants as described in \Sref{sec:invariants} are persistent---once established, they hold forever. However, based on them, it is possible to \emph{encode} a form of invariants that can be cancelled'' again. First, we need some ghost state: \begin{align*} \textmon{CInvTok} \eqdef{}& \fracm \end{align*} Now we define: \begin{align*} \CInvTok{\gname}{q} \eqdef{}& \ownGhost\gname{q} \\ \CInv{\gname}{\namesp}{\prop} \eqdef{}& \knowInv\namesp{\prop \lor \ownGhost\gname{1}} \end{align*} It is then straight-forward to prove: \begin{mathpar} \inferH{CInv-new}{} {\later\prop \vs[\bot] \Exists \gname. \CInvTok\gname{1} * \always\CInv\gname\namesp\prop} \inferH{CInv-acc}{} {\CInv\gname\namesp\prop \proves \Acc[\namesp][\emptyset]{\CInvTok\gname{q}}{\later\prop}} \inferH{CInv-cancel}{} {\CInv\gname\namesp\prop \proves \CInvTok\gname{1} \vs[\namesp] \later\prop} \end{mathpar} Cancellable invariants are useful, for example, when reasoning about data structures that will be deallocated: Every reference to the data structure comes with a fraction of the token, and when all fractions have been gathered, \ruleref{CInv-cancel} is used to cancel the invariant, after which the data structure can be deallocated.  Ralf Jung committed Dec 10, 2017 33 \subsection{Non-atomic (Thread-Local'') Invariants}  Ralf Jung committed Dec 06, 2016 34 35  Sometimes it is necessary to maintain invariants that we need to open non-atomically.  Ralf Jung committed Dec 07, 2016 36 37 38 39 40 Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice, something like the masks that avoid reentrancy on the normal'', atomic invariants. The idea is to use tokens\footnote{Very much like the tokens that are used to encode normal'', atomic invariants} that guard access to non-atomic invariants. Having the token $\NaTokE\pid\mask$ indicates that we can open all invariants in $\mask$. The $\pid$ here is the name of the \emph{invariant pool}. This mechanism allows us to have multiple, independent pools of invariants that all have their own namespaces.  Ralf Jung committed Dec 06, 2016 41   Ralf Jung committed Dec 07, 2016 42 43 44 45 46 One way to think about non-atomic invariants is as thread-local invariants'', where every pool is a thread. Every thread thus has its own, independent set of invariants. Every thread threads through all the tokens for its own pool, so that each invariant can only be opened in the thread it belongs to. As a consequence, they can be kept open around any sequence of expressions (\ie there is no restriction to atomic expressions) -- after all, there cannot be any races with other threads.  Ralf Jung committed Dec 06, 2016 47 48 49  Concretely, this is the monoid structure we need: \begin{align*}  Ralf Jung committed Dec 07, 2016 50 51 \textdom{PId} \eqdef{}& \GName \\ \textmon{NaTok} \eqdef{}& \finpset{\InvName} \times \pset{\InvName}  Ralf Jung committed Dec 06, 2016 52 \end{align*}  Ralf Jung committed Dec 07, 2016 53 For every pool, there is a set of tokens designating which invariants are \emph{enabled} (closed).  Ralf Jung committed Dec 06, 2016 54 55 56 57 This corresponds to the mask of normal'' invariants. We re-use the structure given by namespaces for non-atomic invariants. Furthermore, there is a \emph{finite} set of invariants that is \emph{disabled} (open).  Ralf Jung committed Dec 07, 2016 58 Owning tokens is defined as follows:  Ralf Jung committed Dec 06, 2016 59 \begin{align*}  Ralf Jung committed Dec 07, 2016 60 61 \NaTokE\pid\mask \eqdef{}& \ownGhost{\pid}{ (\emptyset, \mask) } \\ \NaTok\pid \eqdef{}& \NaTokE\pid\top  Ralf Jung committed Dec 06, 2016 62 63 64 65 66 \end{align*} Next, we define non-atomic invariants. To simplify this construction,we piggy-back into normal'' invariants. \begin{align*}  Ralf Jung committed Dec 07, 2016 67  \NaInv\pid\namesp\prop \eqdef{}& \Exists \iname\in\namesp. \knowInv\namesp{\prop * \ownGhost\pid{(\set{\iname},\emptyset)} \lor \NaTokE\pid{\set{\iname}}}  Ralf Jung committed Dec 06, 2016 68 69 70 71 72 \end{align*} We easily obtain: \begin{mathpar}  Ralf Jung committed Dec 11, 2017 73  \axiomH{NAInv-new-pool}  Ralf Jung committed Dec 07, 2016 74  {\TRUE \vs[\bot] \Exists\pid. \NaTok\pid}  Ralf Jung committed Dec 06, 2016 75   Ralf Jung committed Dec 11, 2017 76  \axiomH{NAInv-tok-split}  Ralf Jung committed Dec 07, 2016 77  {\NaTokE\pid{\mask_1 \uplus \mask_2} \Lra \NaTokE\pid{\mask_1} * \NaTokE\pid{\mask_2}}  Ralf Jung committed Dec 06, 2016 78   Ralf Jung committed Dec 11, 2017 79  \axiomH{NAInv-new-inv}  Ralf Jung committed Dec 07, 2016 80  {\later\prop \vs[\namesp] \always\NaInv\pid\namesp\prop}  Ralf Jung committed Dec 06, 2016 81   Ralf Jung committed Dec 11, 2017 82  \axiomH{NAInv-acc}  Ralf Jung committed Dec 07, 2016 83  {\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\namesp}{\later\prop}}  Ralf Jung committed Dec 06, 2016 84 85 86 87 88 \end{mathpar} from which we can derive \begin{mathpar} \infer {\namesp \subseteq \mask}  Ralf Jung committed Dec 07, 2016 89  {\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\mask}{\later\prop * \NaTokE\pid{\mask \setminus \namesp}}}  Ralf Jung committed Dec 06, 2016 90 91 \end{mathpar}  Ralf Jung committed Dec 12, 2016 92 93 \subsection{Boxes}  Robbert Krebbers committed Dec 10, 2017 94 95 The idea behind the \emph{boxes} is to have an proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately. In some sense, this is a replacement for having an authoritative PCM of Iris propositions itself''.  Ralf Jung committed Dec 12, 2016 96 97 It is similar to the pattern involving saved propositions that was used for the barrier~\cite{iris2}, but more complicated because there are some operations that we want to perform without a later.  Robbert Krebbers committed Dec 10, 2017 98 99 Roughly, the idea is that a \emph{box} is a container for an proposition $\prop$. A box consists of a bunch of \emph{slices} which decompose $\prop$ into a separating conjunction of the propositions $\propB_\sname$ governed by the individual slices.  Ralf Jung committed Dec 12, 2016 100 Each slice is either \emph{full} (it right now contains $\propB_\sname$), or \emph{empty} (it does not contain anything currently).  Robbert Krebbers committed Dec 10, 2017 101 The proposition governing the box keeps track of the state of all the slices that make up the box.  Ralf Jung committed Dec 12, 2016 102 103 104 The crux is that opening and closing of a slice can be done even if we only have ownership of the boxes later'' ($\later$). The interface for boxes is as follows:  Robbert Krebbers committed Dec 10, 2017 105 The two core propositions are: $\BoxSlice\namesp\prop\sname$, saying that there is a slice in namespace $\namesp$ with name $\sname$ and content $\prop$; and $\ABox\namesp\prop{f}$, saying that $f$ describes the slices of a box in namespace $\namesp$, such that all the slices together contain $\prop$. Here, $f$ is of type $\nat \fpfn \BoxState$ mapping names to states, where $\BoxState \eqdef \set{\BoxFull, \BoxEmp}$.  Ralf Jung committed Dec 12, 2016 106 107 108 109 110 111 112 113 114 \begin{mathpar} \inferH{Box-create}{} {\TRUE \vs[\namesp] \ABox\namesp\TRUE\emptyset} \inferH{Slice-insert-empty}{} {\lateropt b\ABox\namesp\prop{f} \vs[\namesp] \Exists\sname \notin \dom(f). \always\BoxSlice\namesp\propB\sname * \lateropt b\ABox\namesp{\prop * \propB}{\mapinsert\sname\BoxEmp{f}}} \inferH{Slice-delete-empty} {f(\sname) = \BoxEmp}  Dan Frumin committed Nov 23, 2017 115  {\BoxSlice\namesp\propB\sname \proves \lateropt b\ABox\namesp\prop{f} \vs[\namesp] \Exists \prop'. \lateropt b(\later(\prop = \prop' * \propB) * \ABox\namesp{\prop'}{\mapinsert\sname\bot{f}})}  Ralf Jung committed Dec 12, 2016 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141  \inferH{Slice-fill} {f(\sname) = \BoxEmp} {\BoxSlice\namesp\propB\sname \proves \lateropt b\propB * \later\ABox\namesp\prop{f} \vs[\namesp] \lateropt b\ABox\namesp\prop{\mapinsert\sname\BoxFull{f}}} \inferH{Slice-empty} {f(\sname) = \BoxFull} {\BoxSlice\namesp\propB\sname \proves \lateropt b\ABox\namesp\prop{f} \vs[\namesp] \later\propB * \lateropt b\ABox\namesp\prop{\mapinsert\sname\BoxEmp{f}}} \inferH{Box-fill} {\All\sname\in\dom(f). f(\sname) = \BoxEmp} {\later\prop * \ABox\namesp\prop{f} \vs[\namesp] \ABox\namesp\prop{\mapinsertComp\sname\BoxFull{\sname\in\dom(f)}{f}}} \inferH{Box-empty} {\All\sname\in\dom(f). f(\sname) = \BoxFull} {\ABox\namesp\prop{f} \vs[\namesp] \later\prop * \ABox\namesp\prop{\mapinsertComp\sname\BoxEmp{\sname\in\dom(f)}{f}}} \end{mathpar} Above, $\lateropt b \prop$ is syntactic sugar for $\later\prop$ (if $b$ is $1$) or $\prop$ (if $b$ is $0$). This is essentially an \emph{optional later}, indicating that the lemmas can be applied with \textlog{Box} being owned now or later, and that ownership is returned the same way. \begingroup \paragraph{Model.} \newcommand\BoxM{\textmon{Box}} \newcommand\SliceInv{\textlog{SliceInv}} The above rules are validated by the following model.  Robbert Krebbers committed Dec 10, 2017 142 We need a camera as follows:  Ralf Jung committed Dec 12, 2016 143 144 145 146 147 \begin{align*} \BoxState \eqdef{}& \BoxFull + \BoxEmp \\ \BoxM \eqdef{}& \authm(\maybe{\exm(\BoxState)}) \times \maybe{\agm(\latert \iProp)} \end{align*}  Robbert Krebbers committed Dec 10, 2017 148 Now we can define the propositions:  Ralf Jung committed Dec 12, 2016 149 \begin{align*}  Dan Frumin committed Nov 23, 2017 150  \SliceInv(\sname, \prop) \eqdef{}& \Exists b. \ownGhost\sname{(\authfull b, \munit)} * ((b = \BoxFull) \Ra \prop) \\  Ralf Jung committed Dec 12, 2016 151 152  \BoxSlice\namesp\prop\sname \eqdef{}& \ownGhost\sname{(\munit, \prop)} * \knowInv\namesp{\SliceInv(\sname,\prop)} \\ \ABox\namesp\prop{f} \eqdef{}& \Exists \propB : \nat \to \Prop. \later\left( \prop = \Sep_{\sname \in \dom(f)} \propB(\sname) \right ) * {}\\  Dan Frumin committed Nov 23, 2017 153  & \Sep_{\sname \in \dom(f)} \ownGhost\sname{(\authfrag f(\sname), \propB(\sname))} * \knowInv\namesp{\SliceInv(\sname,\propB(\sname))}  Ralf Jung committed Dec 12, 2016 154 155 156 157 158 159 160 161 162 \end{align*} \endgroup % Model paragraph \paragraph{Derived rules.} Here are some derived rules: \begin{mathpar} \inferH{Slice-insert-full}{} {\later\propB * \lateropt b\ABox\namesp\prop{f} \vs[\namesp] \Exists\sname \notin \dom(f). \always\BoxSlice\namesp\propB\sname * \lateropt b\ABox\namesp{\prop * \propB}{\mapinsert\sname\BoxFull{f}}}  Ralf Jung committed Dec 12, 2016 163  \inferH{Slice-delete-full}  Ralf Jung committed Dec 12, 2016 164 165 166 167 168  {f(\sname) = \BoxFull} {\BoxSlice\namesp\propB\sname \proves \lateropt b \ABox\namesp\prop{f} \vs[\namesp] \later\propB * \Exists \prop'. \lateropt b (\later(\prop = \prop' * \propB) * \ABox\namesp{\prop'}{\mapinsert\sname\bot{f}})} \inferH{Slice-split} {f(\sname) = s}  Dan Frumin committed Nov 23, 2017 169  {\kern-4ex\BoxSlice\namesp{\propB_1 * \propB_2}\sname \proves \lateropt b \ABox\namesp\prop{f} \vs[\namesp] \Exists \sname_1 \notin \dom(f), \sname_2 \notin \dom(f). \sname_1 \neq \sname_2 \land {}\\\kern5ex \always\BoxSlice\namesp{\propB_1}{\sname_1} * \always\BoxSlice\namesp{\propB_2}{\sname_2} * \lateropt b \ABox\namesp\prop{\mapinsert{\sname_2}{s}{\mapinsert{\sname_1}{s}{\mapinsert\sname\bot{f}}}}}  Ralf Jung committed Dec 12, 2016 170 171 172 173 174 175 176 177  \inferH{Slice-merge} {\sname_1 \neq \sname_2 \and f(\sname_1) = f(\sname_2) = s} {\BoxSlice\namesp{\propB_1}{\sname_1}, \BoxSlice\namesp{\propB_2}{\sname_2} \proves \lateropt b \ABox\namesp\prop{f} \vs[\namesp] \Exists \sname \notin \dom(f) \setminus \set{\sname_1, \sname_2}. {}\\\kern5ex \always\BoxSlice\namesp{\propB_1 * \propB_2}\sname * \lateropt b \ABox\namesp\prop{\mapinsert\sname{s}{\mapinsert{\sname_2}{\bot}{\mapinsert{\sname_1}{\bot}{f}}}}} \end{mathpar}  Ralf Jung committed Mar 08, 2016 178   Ralf Jung committed Mar 12, 2016 179 % TODO: These need syncing with Coq  Ralf Jung committed Mar 07, 2016 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 % \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 209   Ralf Jung committed Mar 07, 2016 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 % 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 226   Ralf Jung committed Mar 07, 2016 227 228 % 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 229   Ralf Jung committed Mar 07, 2016 230 231 232 % 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 233   Ralf Jung committed Mar 07, 2016 234 235 % 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 236   Ralf Jung committed Mar 07, 2016 237 % This holds by our premise.  Ralf Jung committed Jan 31, 2016 238 % \end{proof}  Ralf Jung committed Jan 31, 2016 239   Ralf Jung committed Mar 07, 2016 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 % % \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 280 % {\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 281 282 % \and % \axiomH{AuthClose}  Ralf Jung committed Mar 12, 2016 283 % {\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 284 285 286 287 288 % \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 289 % {\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 290 291 292 293 % \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 294 % {\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 295 296 297 298 299 300 301 302 % {\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 303 % FIXME use the finmap provided by the global ghost ownership, instead of adding our own  Ralf Jung committed Mar 07, 2016 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 % 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$.  Robbert Krebbers committed Oct 17, 2016 320 % To implement this interface, allocate an instance $\gname_G$ of $\FHeap(\Val)$ and define  Ralf Jung committed Mar 07, 2016 321 322 323 324 325 326 327 328 329 330 % $% 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 331   Ralf Jung committed Jan 31, 2016 332 333 334 335 336  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: