\section{Derived proof rules} \subsection{Base logic} \ralf{Give the most important derived rules.} \subsection{Program logic} \ralf{Sync this with Coq.} Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively: \[ \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \dynA{\expr}{\lambda\Ret\val.\propB}{\mask})} \qquad\qquad \begin{aligned} \prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvsA{\propB}{\mask_1}{\mask_2})} \\ \prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop \end{aligned} \] We write just one mask for a view shift when $\mask_1 = \mask_2$. The convention for omitted masks is generous: An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts. We write $\provesalways$ to denote judgments that can only be extended with a boxed proof context, in contrast to our usual convention of allowing the context to be extended with any assertions. \paragraph{Hoare triples.} \begin{mathpar} \inferH{Ret} {} {\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]} \and \inferH{Bind} {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\ \All \val. \hoare{\propB}{K[\val]}{\Ret\valB.\propC}[\mask]} {\hoare{\prop}{K[\expr]}{\Ret\valB.\propC}[\mask]} \and \inferH{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{Frame} {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]} {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask \uplus \mask']} \and \inferH{AFrame} {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \text{$\expr$ not a value} } {\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask \uplus \mask']} % \and % \inferH{Fork} % {\hoare{\prop}{\expr}{\Ret\any. \TRUE}[\top]} % {\hoare{\later\prop * \later\propB}{\fork{\expr}}{\Ret\val. \val = \textsf{fRet} \land \propB}[\mask]} \and \inferH{ACsq} {\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} } {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']} \end{mathpar} \paragraph{View shifts.} \begin{mathpar} \inferH{NewInv} {\infinite(\mask)} {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}} \and \inferH{FpUpd} {\melt \mupd \meltsB} {\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}} \and \inferH{VSTrans} {\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 \inferH{VSImp} {\always{(\prop \Ra \propB)}} {\prop \vs[\emptyset] \propB} \and \inferH{VSFrame} {\prop \vs[\mask_1][\mask_2] \propB} {\prop * \propC \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB * \propC} \and \inferH{VSTimeless} {\timeless{\prop}} {\later \prop \vs \prop} \and \axiomH{InvOpen} {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop} \and \axiomH{InvClose} {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE } \end{mathpar} \vspace{5pt} \subsection{Derived rules} \ralf{Move all these to the two paragraphs above.} \paragraph{Derived structural rules.} The following are easily derived by unfolding the sugar for Hoare triples and view shifts. \begin{mathpar} \inferHB{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{VSDisj} {\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 \inferHB{Exist} {\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]} {\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]} \and \inferHB{VSExist} {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)} {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB} \and \inferHB{BoxOut} {\always\propB \provesalways \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]} {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]} \and \inferHB{VSBoxOut} {\always\propB \provesalways \prop \vs[\mask_1][\mask_2] \propC} {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC} \and \inferH{False} {} {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]} \and \inferH{VSFalse} {} {\FALSE \vs[\mask_1][\mask_2] \prop } \end{mathpar} \paragraph{Derived rules for invariants.} Invariants can be opened around atomic expressions and view shifts. \begin{mathpar} \inferH{Inv} {\hoare{\later{\propC} * \prop } {\expr} {\Ret\val. \later{\propC} * \propB }[\mask] \and \physatomic{\expr} } {\knowInv{\iname}{\propC} \proves \hoare{\prop} {\expr} {\Ret\val. \propB}[\mask \uplus \{ \iname \}] } \and \inferH{VSInv} {\later{\prop} * \propB \vs[\mask_1][\mask_2] \later{\prop} * \propC} {\knowInv{\iname}{\prop} \proves \propB \vs[\mask_1 \uplus \{ \iname \}][\mask_2 \uplus \{ \iname \}] \propC} \end{mathpar} \clearpage \section{Derived constructions} 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} % 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$. % 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]\] % 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]\] % 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]\] % This holds by our premise. % \end{proof} % % \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]$. %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: