From 0816b3de1b6a724897447df833d158e8c384e292 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 12 Mar 2016 15:19:13 +0100 Subject: [PATCH] docs: typos, nits --- docs/algebra.tex | 4 ++-- docs/constructions.tex | 32 +++++++++++++++--------------- docs/derived.tex | 44 +++++++++++++++++++++--------------------- docs/logic.tex | 26 ++++++++++++------------- docs/model.tex | 10 +++++----- 5 files changed, 58 insertions(+), 58 deletions(-) diff --git a/docs/algebra.tex b/docs/algebra.tex index 6d738187..7d18bfab 100644 --- a/docs/algebra.tex +++ b/docs/algebra.tex @@ -74,7 +74,7 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th \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 - $\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$. \end{defn} @@ -146,7 +146,7 @@ This operation is needed to prove that $\later$ commutes with existential quanti \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 - $\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$. \end{defn} diff --git a/docs/constructions.tex b/docs/constructions.tex index d5849d53..dc3b643b 100644 --- a/docs/constructions.tex +++ b/docs/constructions.tex @@ -195,16 +195,16 @@ We obtain the following frame-preserving update: % \end{mathpar} % \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. % \end{proof} % The powerset monoids is cancellative. % \begin{proof}[Proof of cancellativity] -% 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$. -% 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$. +% 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$. +% 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$. % The other direction works the same way. % \end{proof} @@ -238,20 +238,20 @@ We obtain the following frame-preserving update: % \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$. -% In the interesting case, we have $f = (q_f, a_f)$. -% Obtain $b$ such that $b \in B \land b \sep 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$. % Then $(q, b) \sep f$, and we are done. % \end{proof} % $\fracm{M}$ is cancellative if $M$ is cancellative. % \begin{proof}[Proof of cancellativitiy] -% If $\melt_f = \munit$, we are trivially done. -% So let $\melt_f = (q_f, \melt_f')$. +% If $\melt_\f = \munit$, we are trivially done. +% So let $\melt_\f = (q_\f, \melt_\f')$. % If $\melt = \munit$, then $\meltB = \munit$ as otherwise the fractions could not match up. % Again, we are trivially done. % Similar so for $\meltB = \munit$. % 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'$. % The first is trivial, the second follows from cancellativitiy of $M$. % \end{proof} @@ -312,7 +312,7 @@ We obtain the following frame-preserving update: % The frame-preserving update involves a rather unwieldy side-condition: % \begin{mathpar} % \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 % }{ % \authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt' @@ -392,11 +392,11 @@ We obtain the following frame-preserving update: % We have % \begin{quote} % If $(s, T) \ra (s', T')$\\ -% and $T_f \sep (T \uplus \STSL(s))$,\\ -% then $\textsf{frame}(s, T_f) \ra \textsf{frame}(s', T_f)$. +% and $T_\f \sep (T \uplus \STSL(s))$,\\ +% then $\textsf{frame}(s, T_\f) \ra \textsf{frame}(s', T_\f)$. % \end{quote} % \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'$. % \end{proof} @@ -418,8 +418,8 @@ We obtain the following frame-preserving update: % {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')} % \end{mathpar} % \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'$. -% By upward-closedness, it suffices to show $\textsf{frame}(s, T_f) \ststrans \textsf{frame}(s', T_f)$. +% 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)$. % This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step. % \end{proof} diff --git a/docs/derived.tex b/docs/derived.tex index 34b94a53..55a0c06f 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -210,20 +210,20 @@ We can derive some specialized forms of the lifting axioms for the operational s \infer[wp-lift-atomic-step] {\atomic(\expr_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)} - {\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_f. \pred(\ofval(\val), \state_2, \expr_f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \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)} + {\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. \pred(\ofval(\val), \state_2, \expr_\f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} \infer[wp-lift-atomic-det-step] {\atomic(\expr_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 \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_f = \expr_f'} - {\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \All \expr'_2, \state'_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \expr_\f = \expr_\f'} + {\later\ownPhys{\state_1} * \later(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} \infer[wp-lift-pure-det-step] {\toval(\expr_1) = \bot \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 \expr_2 = \expr_2' \land \expr_f = \expr_f'} - {\later ( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}} + \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 \expr_2 = \expr_2' \land \expr_\f = \expr_\f'} + {\later ( \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{mathparpagebreakable} Furthermore, we derive some forms that directly involve view shifts and Hoare triples. @@ -232,35 +232,35 @@ Furthermore, we derive some forms that directly involve view shifts and Hoare tr {\mask_2 \subseteq \mask_1 \and \toval(\expr_1) = \bot \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) \\\\ \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and - \All \expr_2, \state_2, \expr_f. \pred(\expr_2, \state_2, \expr_f) * \ownPhys{\state_2} * \prop' \vs[\mask_2][\mask_1] \propB_1 * \propB_2 \\\\ - \All \expr_2, \state_2, \expr_f. \hoare{\propB_1}{\expr_2}{\Ret\val.\propC}[\mask_1] \and - \All \expr_2, \state_2, \expr_f. \hoare{\propB_2}{\expr_f}{\Ret\any. \TRUE}[\top]} + \All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) * \ownPhys{\state_2} * \prop' \vs[\mask_2][\mask_1] \propB_1 * \propB_2 \\\\ + \All \expr_2, \state_2, \expr_\f. \hoare{\propB_1}{\expr_2}{\Ret\val.\propC}[\mask_1] \and + \All \expr_2, \state_2, \expr_\f. \hoare{\propB_2}{\expr_\f}{\Ret\any. \TRUE}[\top]} { \hoare\prop{\expr_1}{\Ret\val.\propC}[\mask_1] } \infer[ht-lift-atomic-step] {\atomic(\expr_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) \\\\ \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and - \All \expr_2, \state_2, \expr_f. \hoare{\pred(\expr_2,\state_2,\expr_f) * \prop}{\expr_f}{\Ret\any. \TRUE}[\top]} - { \hoare{\later\ownPhys{\state_1} * \later\prop}{\expr_1}{\Ret\val.\Exists \state_2, \expr_f. \ownPhys{\state_2} * \pred(\ofval(\expr_2),\state_2,\expr_f)}[\mask_1] } + \All \expr_2, \state_2, \expr_\f. \hoare{\pred(\expr_2,\state_2,\expr_\f) * \prop}{\expr_\f}{\Ret\any. \TRUE}[\top]} + { \hoare{\later\ownPhys{\state_1} * \later\prop}{\expr_1}{\Ret\val.\Exists \state_2, \expr_\f. \ownPhys{\state_2} * \pred(\ofval(\expr_2),\state_2,\expr_\f)}[\mask_1] } \infer[ht-lift-pure-step] {\toval(\expr_1) = \bot \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 \expr_2, \expr_f. \hoare{\pred(\expr_2,\expr_f) * \prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and - \All \expr_2, \expr_f. \hoare{\pred(\expr_2,\expr_f) * \prop'}{\expr_f}{\Ret\any. \TRUE}[\top]} + \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 \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and + \All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]} { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] } \infer[ht-lift-pure-det-step] {\toval(\expr_1) = \bot \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 \expr_2 = \expr_2' \land \expr_f = \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 \expr_2 = \expr_2' \land \expr_\f = \expr_\f' \\\\ \hoare{\prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and - \hoare{\prop'}{\expr_f}{\Ret\any. \TRUE}[\top]} + \hoare{\prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]} { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] } \end{mathparpagebreakable} @@ -438,21 +438,21 @@ We can now derive the following rules for this derived form of the invariant ass % {\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}}} +% {\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}} } +% {\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] +% {\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)} +% {\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)} diff --git a/docs/logic.tex b/docs/logic.tex index 2c8a49da..53ba97a9 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -7,7 +7,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} \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})$ 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: $\expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot$ \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} {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and {{ \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{mathpar} @@ -26,7 +26,7 @@ It does not matter whether they fork off an arbitrary expression. \begin{defn} 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} \begin{defn}[Context] @@ -35,9 +35,9 @@ It does not matter whether they fork off an arbitrary expression. \item $\lctx$ does not turn non-values into values:\\ $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot$ \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:\\ - $\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{defn} @@ -54,9 +54,9 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. \cfg{\tpool'}{\state'}} \begin{mathpar} \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_2] \dplus \tpool' \dplus [\expr_f]}{\state'}} + \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_\f]}{\state'}} \and\infer {\expr_1, \state_1 \step \expr_2, \state_2} {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step @@ -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} \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] {}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop} @@ -594,19 +594,19 @@ This is entirely standard. {\mask_2 \subseteq \mask_1 \and \toval(\expr_1) = \bot \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... - ~~\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}} } \infer[wp-lift-pure-step] {\toval(\expr_1) = \bot \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)} - {\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}} + \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}} \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} diff --git a/docs/model.tex b/docs/model.tex index d1af61a1..ea2a89bd 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -76,7 +76,7 @@ We then pick $\iProp$ as the interpretation of $\Prop$: \paragraph{Interpretation of assertions.} $\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{-}{-}{-} : \Delta\textdom{State} \times @@ -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))} \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*} \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} \end{aligned}} \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. \begin{align*} \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 {}\\ &(\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 {}&\\ -- GitLab