From b9c5f9b654e5cd0b02d5c14dbda505f6c4fdca8a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 Dec 2017 14:18:08 +0100
Subject: [PATCH] Docs: use \stateinterp macro.
---
docs/program-logic.tex | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 7e7f2e000..a009324a9 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -250,15 +250,15 @@ Finally, we can define the core piece of the program logic, the assertion that r
\paragraph{Defining weakest precondition.}
We assume that everything making up the definition of the language, \ie values, expressions, states, the conversion functions, reduction relation and all their properties, are suitably reflected into the logic (\ie they are part of the signature $\Sig$).
-We further assume (as a parameter) a predicate $I : \State \to \iProp$ that interprets the physical state as an Iris assertion.
+We further assume (as a parameter) a predicate $\stateinterp : \State \to \iProp$ that interprets the physical state as an Iris assertion.
This can be instantiated, for example, with ownership of an authoritative RA to tie the physical state to fragments that are used for user-level proofs.
\begin{align*}
\textdom{wp} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\
& (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
- & \Bigl(\toval(\expr) = \bot \land \All \state. I(\state) \vsW[\mask][\emptyset] {}\\
+ & \Bigl(\toval(\expr) = \bot \land \All \state. \stateinterp(\state) \vsW[\mask][\emptyset] {}\\
&\qquad \red(\expr, \state) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\
- &\qquad\qquad I(\state') * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\
+ &\qquad\qquad \stateinterp(\state') * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\
% (* value case *)
\wpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\mask, \expr, \Lam\val.\prop)
\end{align*}
@@ -302,7 +302,7 @@ We will also want a rule that connect weakest preconditions to the operational s
\infer[wp-lift-step]
{\toval(\expr_1) = \bot}
{ {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
- ~~\All \state_1. I(\state_1) \vsW[\mask][\emptyset] \red(\expr_1,\state_1) * {}\\\qquad~~ \later\All \expr_2, \state_2, \vec\expr. (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr) \vsW[\emptyset][\mask] \Bigl(I(\state_2) * \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr) {}\\\proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}
+ ~~\All \state_1. \stateinterp(\state_1) \vsW[\mask][\emptyset] \red(\expr_1,\state_1) * {}\\\qquad~~ \later\All \expr_2, \state_2, \vec\expr. (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr) \vsW[\emptyset][\mask] \Bigl(\stateinterp(\state_2) * \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}\Bigr) {}\\\proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}
\end{inbox}} }
\end{mathpar}
@@ -361,7 +361,7 @@ The signature can of course state arbitrary additional properties of $\pred$, as
The adequacy statement now reads as follows:
\begin{align*}
&\All \mask, \expr, \val, \state.
- \\&( \TRUE \proves {\upd}_\mask \Exists I. I(\state) * \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
+ \\&( \TRUE \proves {\upd}_\mask \Exists \stateinterp. \stateinterp(\state) * \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
\\&\expr, \state \vDash V
\end{align*}
Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.
--
GitLab