diff --git a/tex/iris.sty b/tex/iris.sty index e3937c08bec50e3573a3bbfc999026852c821aed..cce3a90a9bb42f5741125f4677777ba3576d5b41 100644 --- a/tex/iris.sty +++ b/tex/iris.sty @@ -295,6 +295,7 @@ }\IfNoValueF{#3}{^{\,#3}}% } \newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]} +\newcommand*{\invM}[2]{\textlog{Inv}^{#1}\left(#2\right)} \newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]} \newcommand*{\ownM}[1]{\textlog{Own}\left(#1\right)} \newcommand*{\ownPhys}[1]{\textlog{Phy}(#1)} diff --git a/tex/program-logic.tex b/tex/program-logic.tex index 754660ea099e914ee700c4c2e9446efa97e81ebb..f6ddeebd3d97ef737645dbfce5bf69234929cd38 100644 --- a/tex/program-logic.tex +++ b/tex/program-logic.tex @@ -40,7 +40,7 @@ We can now define the proposition $W$ (\emph{world satisfaction}) which ensures \paragraph{Invariants.} The following proposition states that an invariant with name $\iname$ exists and maintains proposition $\prop$: -$\knowInv\iname\prop \eqdef \ownGhost{\gname_{\textdom{Inv}}} +\[ \invM\iname\prop \eqdef \ownGhost{\gname_{\textdom{Inv}}} {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}}$ \paragraph{Fancy Updates and View Shifts.} @@ -80,16 +80,6 @@ Fancy updates satisfy the following basic proof rules: \infer[fup-timeless] {\timeless\prop} {\later\prop \proves \pvs[\mask] \prop} -% -% \inferH{fup-allocI} -% {\text{$\mask$ is infinite}} -% {\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop} -%gov -% \inferH{fup-openI} -% {}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop} -% -% \inferH{fup-closeI} -% {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE} \end{mathparpagebreakable} (There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.) @@ -125,17 +115,7 @@ Still, just to give an idea of what view shifts are'', here are some proof rul \inferH{vs-timeless} {\timeless{\prop}} {\later \prop \vs[\emptyset] \prop} - -% \inferH{vs-allocI} -% {\infinite(\mask)} -% {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}} -% \and -% \axiomH{vs-openI} -% {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop} -% \and -% \axiomH{vs-closeI} -% {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE } -% +\and \inferHB{vs-disj} {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC} {\prop \lor \propB \vs[\mask_1][\mask_2] \propC} @@ -390,24 +370,12 @@ We only give some of the proof rules for Hoare triples here, since we usually do \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-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 \set\iname]} -% \and -% \inferH{Ht-inv-timeless} -% {\hoare{\propC*\prop}{\expr}{\Ret\val.\propC*\propB}[\mask] \and -% \physatomic{\expr} \and \timeless\propC -% } -% {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]} \end{mathparpagebreakable} \subsection{Invariant Namespaces} \label{sec:namespaces} -In \Sref{sec:invariants}, we defined a proposition $\knowInv\iname\prop$ expressing knowledge (\ie the proposition is persistent) that $\prop$ is maintained as invariant with name $\iname$. +In \Sref{sec:invariants}, we defined a proposition $\invM\iname\prop$ expressing knowledge (\ie the proposition is persistent) that $\prop$ is maintained as invariant with name $\iname$. The concrete name $\iname$ is picked when the invariant is allocated, so it cannot possibly be statically known -- it will always be a variable that's threaded through everything. However, we hardly care about the actual, concrete name. All we need to know is that this name is \emph{different} from the names of other invariants that we want to open at the same time. @@ -434,20 +402,20 @@ Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: $\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}$ We will overload the notation for invariant propositions for using namespaces instead of names: -$\knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop}$ +$\invM\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \invM\iname{\prop}$ We can now derive the following rules (this involves unfolding the definition of fancy updates): \begin{mathpar} - \axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop} + \axiomH{inv-persist}{\invM\namesp\prop \proves \always\invM\namesp\prop} - \axiomH{inv-alloc}{\later\prop \proves \pvs[\emptyset] \knowInv\namesp\prop} + \axiomH{inv-alloc}{\later\prop \proves \pvs[\emptyset] \invM\namesp\prop} \inferH{inv-open} {\namesp \subseteq \mask} - {\knowInv\namesp\prop \vs[\mask][\mask\setminus\namesp] \later\prop * (\later\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)} + {\invM\namesp\prop \vs[\mask][\mask\setminus\namesp] \later\prop * (\later\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)} \inferH{inv-open-timeless} {\namesp \subseteq \mask \and \timeless\prop} - {\knowInv\namesp\prop \vs[\mask][\mask\setminus\namesp] \prop * (\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)} + {\invM\namesp\prop \vs[\mask][\mask\setminus\namesp] \prop * (\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)} \end{mathpar} \subsection{Accessors} @@ -488,6 +456,26 @@ For the symmetric case where $\prop = \propC$ and $\propB = \propB'$, we use the $\Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop)$ This accessor is idempotent'' in the sense that it does not actually change the state. After applying it, we get our $\prop$ back so we end up where we started. +\paragraph{Accessor-style invariants.} +In fact, the user-visible notion of invariants $\knowInv\namesp\prop$ is defined via \ruleref{inv-open}: +\begin{align*} + \knowInv\namesp\prop \eqdef \always\All\mask. \pvs[\mask][\mask\setminus\namesp] \later\prop * (\later\prop \vsW[\mask\setminus\namesp][\mask] \TRUE) +\end{align*} +All the invariant laws shown above for $\invM\namesp\prop$ also hold for $\knowInv\namesp\prop$, but we can also show some additional laws that would otherwise not hold: +\begin{mathpar} + \inferH{inv-combine} + {\namesp_1 \disj \namesp_2 \and \namesp_1 \cup \namesp_2 \subseteq \namesp} + {\knowInv{\namesp_1}{\prop_1} * \knowInv{\namesp_2}{\prop_2} \vdash \knowInv{\namesp}{\prop_1 * \prop_2}} + + \inferH{inv-split} + {} + {\knowInv{\namesp}{\prop_1 * \prop_2} \vdash \knowInv{\namesp}{\prop_1} * \knowInv{\namesp}{\prop_2}} + + \inferH{inv-alter} + {} + {\later\always(\prop \wand \propB * (\propB \wand \prop)) \vdash \knowInv\namesp\prop \wand \knowInv\namesp\propB} +\end{mathpar} + %%% Local Variables: %%% mode: latex %%% TeX-master: "iris"