Commit 0816b3de by Ralf Jung

### docs: typos, nits

parent 7cb94e3e
Pipeline #332 passed with stage
 ... @@ -74,7 +74,7 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th ... @@ -74,7 +74,7 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th \begin{defn} \begin{defn} It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if $\All \melt_f. \melt \mtimes \melt_f \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_f \in \mval$ $\All \melt_\f. \melt \mtimes \melt_\f \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_\f \in \mval$ We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn} \end{defn} ... @@ -146,7 +146,7 @@ This operation is needed to prove that $\later$ commutes with existential quanti ... @@ -146,7 +146,7 @@ This operation is needed to prove that $\later$ commutes with existential quanti \begin{defn} \begin{defn} It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if $\All n, \melt_f. \melt \mtimes \melt_f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_f \in \mval_n$ $\All n, \melt_\f. \melt \mtimes \melt_\f \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \melt_\f \in \mval_n$ We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$. \end{defn} \end{defn} ... ...
 ... @@ -195,16 +195,16 @@ We obtain the following frame-preserving update: ... @@ -195,16 +195,16 @@ We obtain the following frame-preserving update: % \end{mathpar} % \end{mathpar} % \begin{proof}[Proof of \ruleref{PowFinUpd}] % \begin{proof}[Proof of \ruleref{PowFinUpd}] % Assume some frame $\melt_f \sep \emptyset$. Since $\melt_f$ is finite and $X$ is infinite, there exists an $x \notin \melt_f$. % Assume some frame $\melt_\f \sep \emptyset$. Since $\melt_\f$ is finite and $X$ is infinite, there exists an $x \notin \melt_\f$. % Pick that for the result. % Pick that for the result. % \end{proof} % \end{proof} % The powerset monoids is cancellative. % The powerset monoids is cancellative. % \begin{proof}[Proof of cancellativity] % \begin{proof}[Proof of cancellativity] % Let $\melt_f \mtimes \melt = \melt_f \mtimes \meltB \neq \mzero$. % Let $\melt_\f \mtimes \melt = \melt_\f \mtimes \meltB \neq \mzero$. % So we have $\melt_f \sep \melt$ and $\melt_f \sep \meltB$, and we have to show $\melt = \meltB$. % So we have $\melt_\f \sep \melt$ and $\melt_\f \sep \meltB$, and we have to show $\melt = \meltB$. % Assume $x \in \melt$. Hence $x \in \melt_f \mtimes \melt$ and thus $x \in \melt_f \mtimes \meltB$. % Assume $x \in \melt$. Hence $x \in \melt_\f \mtimes \melt$ and thus $x \in \melt_\f \mtimes \meltB$. % By disjointness, $x \notin \melt_f$ and hence $x \in meltB$. % By disjointness, $x \notin \melt_\f$ and hence $x \in meltB$. % The other direction works the same way. % The other direction works the same way. % \end{proof} % \end{proof} ... @@ -238,20 +238,20 @@ We obtain the following frame-preserving update: ... @@ -238,20 +238,20 @@ We obtain the following frame-preserving update: % \begin{proof}[Proof of \ruleref{FracUpdLocal}] % \begin{proof}[Proof of \ruleref{FracUpdLocal}] % Assume some $f \sep (q, a)$. If $f = \munit$, then $f \sep (q, b)$ is trivial for any $b \in B$. Just pick the one we obtain by choosing $\munit_M$ as the frame for $a$. % Assume some $f \sep (q, a)$. If $f = \munit$, then $f \sep (q, b)$ is trivial for any $b \in B$. Just pick the one we obtain by choosing $\munit_M$ as the frame for $a$. % In the interesting case, we have $f = (q_f, a_f)$. % In the interesting case, we have $f = (q_\f, a_\f)$. % Obtain $b$ such that $b \in B \land b \sep a_f$. % Obtain $b$ such that $b \in B \land b \sep a_\f$. % Then $(q, b) \sep f$, and we are done. % Then $(q, b) \sep f$, and we are done. % \end{proof} % \end{proof} % $\fracm{M}$ is cancellative if $M$ is cancellative. % $\fracm{M}$ is cancellative if $M$ is cancellative. % \begin{proof}[Proof of cancellativitiy] % \begin{proof}[Proof of cancellativitiy] % If $\melt_f = \munit$, we are trivially done. % If $\melt_\f = \munit$, we are trivially done. % So let $\melt_f = (q_f, \melt_f')$. % So let $\melt_\f = (q_\f, \melt_\f')$. % If $\melt = \munit$, then $\meltB = \munit$ as otherwise the fractions could not match up. % If $\melt = \munit$, then $\meltB = \munit$ as otherwise the fractions could not match up. % Again, we are trivially done. % Again, we are trivially done. % Similar so for $\meltB = \munit$. % Similar so for $\meltB = \munit$. % So let $\melt = (q_a, \melt')$ and $\meltB = (q_b, \meltB')$. % So let $\melt = (q_a, \melt')$ and $\meltB = (q_b, \meltB')$. % We have $(q_f + q_a, \melt_f' \mtimes \melt') = (q_f + q_b, \melt_f' \mtimes \meltB')$. % We have $(q_\f + q_a, \melt_\f' \mtimes \melt') = (q_\f + q_b, \melt_\f' \mtimes \meltB')$. % We have to show $q_a = q_b$ and $\melt' = \meltB'$. % We have to show $q_a = q_b$ and $\melt' = \meltB'$. % The first is trivial, the second follows from cancellativitiy of $M$. % The first is trivial, the second follows from cancellativitiy of $M$. % \end{proof} % \end{proof} ... @@ -312,7 +312,7 @@ We obtain the following frame-preserving update: ... @@ -312,7 +312,7 @@ We obtain the following frame-preserving update: % The frame-preserving update involves a rather unwieldy side-condition: % The frame-preserving update involves a rather unwieldy side-condition: % \begin{mathpar} % \begin{mathpar} % \inferH{AuthUpd}{ % \inferH{AuthUpd}{ % \All\melt_f\in\mcar{\monoid}. \melt\sep\meltB \land \melt\mtimes\melt_f \le \meltB\mtimes\melt_f \Ra \melt'\mtimes\melt_f \le \melt'\mtimes\meltB \and % \All\melt_\f\in\mcar{\monoid}. \melt\sep\meltB \land \melt\mtimes\melt_\f \le \meltB\mtimes\melt_\f \Ra \melt'\mtimes\melt_\f \le \melt'\mtimes\meltB \and % \melt' \sep \meltB % \melt' \sep \meltB % }{ % }{ % \authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt' % \authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt' ... @@ -392,11 +392,11 @@ We obtain the following frame-preserving update: ... @@ -392,11 +392,11 @@ We obtain the following frame-preserving update: % We have % We have % \begin{quote} % \begin{quote} % If $(s, T) \ra (s', T')$\\ % If $(s, T) \ra (s', T')$\\ % and $T_f \sep (T \uplus \STSL(s))$,\\ % and $T_\f \sep (T \uplus \STSL(s))$,\\ % then $\textsf{frame}(s, T_f) \ra \textsf{frame}(s', T_f)$. % then $\textsf{frame}(s, T_\f) \ra \textsf{frame}(s', T_\f)$. % \end{quote} % \end{quote} % \begin{proof} % \begin{proof} % This follows directly by framing the tokens in $\STST \setminus (T_f \uplus T \uplus \STSL(s))$ around the given transition, which yields $(s, \STST \setminus (T_f \uplus \STSL{T}(s))) \ra (s', T' \uplus (\STST \setminus (T_f \uplus T \uplus \STSL{T}(s))))$. % This follows directly by framing the tokens in $\STST \setminus (T_\f \uplus T \uplus \STSL(s))$ around the given transition, which yields $(s, \STST \setminus (T_\f \uplus \STSL{T}(s))) \ra (s', T' \uplus (\STST \setminus (T_\f \uplus T \uplus \STSL{T}(s))))$. % This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s') \uplus T'$. % This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s') \uplus T'$. % \end{proof} % \end{proof} ... @@ -418,8 +418,8 @@ We obtain the following frame-preserving update: ... @@ -418,8 +418,8 @@ We obtain the following frame-preserving update: % {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')} % {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')} % \end{mathpar} % \end{mathpar} % \begin{proof}[Proof of \ruleref{StsStep}] % \begin{proof}[Proof of \ruleref{StsStep}] % Assume some upwards-closed $S_f, T_f$ (the frame cannot be authoritative) s.t.\ $s \in S_f$ and $T_f \sep (T \uplus \STSL(s))$. We have to show that this frame combines with our final monoid element, which is the case if $s' \in S_f$ and $T_f \sep T'$. % Assume some upwards-closed $S_\f, T_\f$ (the frame cannot be authoritative) s.t.\ $s \in S_\f$ and $T_\f \sep (T \uplus \STSL(s))$. We have to show that this frame combines with our final monoid element, which is the case if $s' \in S_\f$ and $T_\f \sep T'$. % By upward-closedness, it suffices to show $\textsf{frame}(s, T_f) \ststrans \textsf{frame}(s', T_f)$. % By upward-closedness, it suffices to show $\textsf{frame}(s, T_\f) \ststrans \textsf{frame}(s', T_\f)$. % This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step. % This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step. % \end{proof} % \end{proof} ... ...
 ... @@ -7,7 +7,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} ... @@ -7,7 +7,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} \end{mathpar} \end{mathpar} \item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{\bot})$ \item There exists a \emph{primitive reduction relation} $(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{\bot})$ We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\ We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\ A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_f$ is forked off. A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_\f$ is forked off. \item All values are stuck: \item All values are stuck: $\expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot$ $\expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot$ \item There is a predicate defining \emph{atomic} expressions satisfying \item There is a predicate defining \emph{atomic} expressions satisfying ... @@ -16,7 +16,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} ... @@ -16,7 +16,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and {{ {{ \begin{inbox} \begin{inbox} \All\expr_1, \state_1, \expr_2, \state_2, \expr_f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2 \All\expr_1, \state_1, \expr_2, \state_2, \expr_\f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2 \end{inbox} \end{inbox} }} }} \end{mathpar} \end{mathpar} ... @@ -26,7 +26,7 @@ It does not matter whether they fork off an arbitrary expression. ... @@ -26,7 +26,7 @@ It does not matter whether they fork off an arbitrary expression. \begin{defn} \begin{defn} An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if $\Exists \expr_2, \state_2, \expr_f. \expr,\state \step \expr_2,\state_2,\expr_f$ $\Exists \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f$ \end{defn} \end{defn} \begin{defn}[Context] \begin{defn}[Context] ... @@ -35,9 +35,9 @@ It does not matter whether they fork off an arbitrary expression. ... @@ -35,9 +35,9 @@ It does not matter whether they fork off an arbitrary expression. \item $\lctx$ does not turn non-values into values:\\ \item $\lctx$ does not turn non-values into values:\\ $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ \item One can perform reductions below $\lctx$:\\ \item One can perform reductions below $\lctx$:\\ $\All \expr_1, \state_1, \expr_2, \state_2, \expr_f. \expr_1, \state_1 \step \expr_2,\state_2,\expr_f \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr_f$ $\All \expr_1, \state_1, \expr_2, \state_2, \expr_\f. \expr_1, \state_1 \step \expr_2,\state_2,\expr_\f \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr_\f$ \item Reductions stay below $\lctx$ until there is a value in the hole:\\ \item Reductions stay below $\lctx$ until there is a value in the hole:\\ $\All \expr_1', \state_1, \expr_2, \state_2, \expr_f. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr_f \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr_f$ $\All \expr_1', \state_1, \expr_2, \state_2, \expr_\f. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr_\f \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr_\f$ \end{enumerate} \end{enumerate} \end{defn} \end{defn} ... @@ -54,9 +54,9 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. ... @@ -54,9 +54,9 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. \cfg{\tpool'}{\state'}} \cfg{\tpool'}{\state'}} \begin{mathpar} \begin{mathpar} \infer \infer {\expr_1, \state_1 \step \expr_2, \state_2, \expr_f \and \expr_f \neq \bot} {\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \and \expr_\f \neq \bot} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_f]}{\state'}} \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_\f]}{\state'}} \and\infer \and\infer {\expr_1, \state_1 \step \expr_2, \state_2} {\expr_1, \state_1 \step \expr_2, \state_2} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step ... @@ -536,7 +536,7 @@ This is entirely standard. ... @@ -536,7 +536,7 @@ This is entirely standard. {\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop} {\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop} \infer[pvs-mask-frame] \infer[pvs-mask-frame] {}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_f][\mask_2 \uplus \mask_f] \prop} {}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \prop} \infer[pvs-frame] \infer[pvs-frame] {}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop} {}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop} ... @@ -594,19 +594,19 @@ This is entirely standard. ... @@ -594,19 +594,19 @@ This is entirely standard. {\mask_2 \subseteq \mask_1 \and {\mask_2 \subseteq \mask_1 \and \toval(\expr_1) = \bot \and \toval(\expr_1) = \bot \and \red(\expr_1, \state_1) \and \red(\expr_1, \state_1) \and \All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f)} \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f)} { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below... { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below... ~~\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_f. \pred(\expr_2, \state_2, \expr_f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop} ~~\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop} \end{inbox}} } \end{inbox}} } \infer[wp-lift-pure-step] \infer[wp-lift-pure-step] {\toval(\expr_1) = \bot \and {\toval(\expr_1) = \bot \and \All \state_1. \red(\expr_1, \state_1) \and \All \state_1. \red(\expr_1, \state_1) \and \All \state_1, \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_f)} \All \state_1, \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_\f)} {\later\All \expr_2, \expr_f. \pred(\expr_2, \expr_f) \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} {\later\All \expr_2, \expr_\f. \pred(\expr_2, \expr_\f) \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} \end{mathpar} \end{mathpar} Here we define $\wpre{\expr_f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression). Here we define $\wpre{\expr_\f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_\f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression). \subsection{Adequacy} \subsection{Adequacy} ... ...
 ... @@ -76,7 +76,7 @@ We then pick $\iProp$ as the interpretation of $\Prop$: ... @@ -76,7 +76,7 @@ We then pick $\iProp$ as the interpretation of $\Prop$: \paragraph{Interpretation of assertions.} \paragraph{Interpretation of assertions.} $\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply. $\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply. We only have to define the missing connectives, the most interesting bits being are primitive view shifts and weakest preconditions. We only have to define the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions. \typedsection{World satisfaction}{\wsat{-}{-}{-} : \typedsection{World satisfaction}{\wsat{-}{-}{-} : \Delta\textdom{State} \times \Delta\textdom{State} \times ... @@ -91,20 +91,20 @@ We only have to define the missing connectives, the most interesting bits being ... @@ -91,20 +91,20 @@ We only have to define the missing connectives, the most interesting bits being \wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))} \wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))} \end{align*} \end{align*} \typedsection{Primitive view-shift}{\mathit{pvs} : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp} \typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp} \begin{align*} \begin{align*} \mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned} \mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned} \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \sep \mask_f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\& \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \sep \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\& \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f} \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f} \end{aligned}} \end{aligned}} \end{align*} \end{align*} \typedsection{Weakest precondition}{\mathit{wp} : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp} \typedsection{Weakest precondition}{\mathit{wp}_{-}(-, -) : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp} $\textdom{wp}$ is defined as the fixed-point of a contractive function. $\textdom{wp}$ is defined as the fixed-point of a contractive function. \begin{align*} \begin{align*} \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned} \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned} \All &\rs_\f, m, \mask_f, \state. 0 \leq m < n \land \mask \sep \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\ \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \sep \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\ &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\ &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\ &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\ &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\ &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\ &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\ ... ...