Commit ce20ffb1 authored by Ralf Jung's avatar Ralf Jung

make variable names a bit more consistent between Coq and LaTeX

parent 8f443ec0
Pipeline #17542 passed with stage
in 13 minutes and 48 seconds
......@@ -231,18 +231,18 @@ The purpose of the adequacy statement is to show that our notion of weakest prec
The most general form of the adequacy statement is about proving properties of an arbitrary program execution.
\begin{thm}[Adequacy]
Assume we are given some $\expr_0$, $\state_0$, $\vec\obs$, $\tpool_1$, $\state_1$ such that $([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1)$, and we are also given a \emph{meta-level} property $\metaprop$ that we want to show.
Assume we are given some $\expr_1$, $\state_1$, $\vec\obs$, $\tpool_2$, $\state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we are also given a \emph{meta-level} property $\metaprop$ that we want to show.
To verify that $\metaprop$ holds, it is sufficient to show the following Iris entailment:
\begin{align*}
&\TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{x.\; \pred(x)} * \left(\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1) \vs[\top][\emptyset] \hat{\metaprop}\right)
&\TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{x.\; \pred(x)} * \left(\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \hat{\metaprop}\right)
\end{align*}
where $\consstate$ describes states that are consistent with the state interpretation and postconditions:
\begin{align*}
\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1) \eqdef{}&\Exists \expr_1, \tpool_1'. \tpool_1 = [\expr_1] \dplus \tpool_1' * {}\\
&\quad (s = \NotStuck \Ra \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1) ) *{}\\
&\quad \stateinterp(\state_1, (), |\tpool_1'|) *{}\\
&\quad (\toval(\expr_1) \ne \bot \wand \pred(\toval(\expr_1))) *{}\\
&\quad \left(\Sep[\expr \in \tpool_1'] \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))\right)
\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \eqdef{}&\Exists \expr_2, \tpool_2'. \tpool_2 = [\expr_2] \dplus \tpool_2' * {}\\
&\quad (s = \NotStuck \Ra \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2) ) *{}\\
&\quad \stateinterp(\state_2, (), |\tpool_2'|) *{}\\
&\quad (\toval(\expr_2) \ne \bot \wand \pred(\toval(\expr_2))) *{}\\
&\quad \left(\Sep[\expr \in \tpool_2'] \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))\right)
\end{align*}
The $\hat\metaprop$ here arises because we need a way to talk about $\metaprop$ inside Iris.
To this end, we assume that the signature $\Sig$ contains some assertion $\hat{\metaprop}$:
......@@ -259,15 +259,15 @@ In other words, to show that $\metaprop$ holds, we have to prove an entailment i
\begin{itemize}
\item the initial state interpretation,
\item a weakest-precondition,
\item and a view shift showing the desired $\hat\metaprop$ under the extra assumption $\consstate(\tpool_1, \state_1)$.
\item and a view shift showing the desired $\hat\metaprop$ under the extra assumption $\consstate(\tpool_2, \state_2)$.
\end{itemize}
Notice that the state interpretation and the postconditions are chosen \emph{after} doing a fancy update, which allows them to depend on the names of ghost variables that are picked in that initial fancy update.
This gives us a chance to allocate some ``global'' ghost state that state interpretation and postcondition can refer to.
$\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1)$ says that:
$\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2)$ says that:
\begin{itemize}
\item The final thread-pool $\tpool_1$ contains the final state of the main thread $\expr_1$, and any number of additional forked threads in $\tpool_1'$.
\item If this is a stuck-free weakest precondition, then all threads in the final thread-pool are either values or are reducible in the final state $\state_1$.
\item The final thread-pool $\tpool_2$ contains the final state of the main thread $\expr_2$, and any number of additional forked threads in $\tpool_2'$.
\item If this is a stuck-free weakest precondition, then all threads in the final thread-pool are either values or are reducible in the final state $\state_2$.
\item The state interpretation $\stateinterp$ holds for the final state.
\item If the main thread reduced to a value, the post-condition $\pred$ of the weakest precondition holds for that value.
\item If any other thread reduced to a value, the forked-thread post-condition $\pred_F$ holds for that value.
......@@ -275,56 +275,56 @@ $\consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1)$ says
~\par
As an example for how to use this adequacy theorem, let us say we wanted to prove that a program $\expr_0$ for which we derived a $\NotStuck$ weakest-precondition cannot get stuck:
As an example for how to use this adequacy theorem, let us say we wanted to prove that a program $\expr_1$ for which we derived a $\NotStuck$ weakest-precondition cannot get stuck:
\begin{cor}[Stuck-freedom]
Assume we are given some $\expr_0$ such that the following holds:
Assume we are given some $\expr_1$ such that the following holds:
\[
\TRUE \proves \All\state_0, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\NotStuck;\top]{x.\; \pred(x)}
\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\NotStuck;\top]{x.\; \pred(x)}
\]
Then it is the case that:
\[
\All \state_0, \vec\obs, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1)
\All \state_1, \vec\obs, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2) \Ra \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2)
\]
\end{cor}
To prove the conclusion of this corollary, we assume some $\state_0, \vec\obs, \tpool_1, \state_1$ and $([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1)$, and we instantiate the main theorem with this execution and $\metaprop \eqdef \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1)$.
To prove the conclusion of this corollary, we assume some $\state_1, \vec\obs, \tpool_2, \state_2$ and $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we instantiate the main theorem with this execution and $\metaprop \eqdef \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2)$.
We can then show the premise of adequacy using the Iris entailment that we assumed in the corollary and:
\[ \TRUE \proves \consstate^{\stateinterp;\pred;\pred_F}_{\NotStuck}(\tpool_1, \state_1) \vs[\top][\emptyset] \metaprop \]
\[ \TRUE \proves \consstate^{\stateinterp;\pred;\pred_F}_{\NotStuck}(\tpool_2, \state_2) \vs[\top][\emptyset] \metaprop \]
This proof, just like the following, also exploits that we can freely swap between meta-level universal quantification ($\All x. \TRUE \proves \prop$) and quantification in Iris ($\TRUE \proves \All x. \prop$).
~\par
Similarly we could show that the postcondition makes adequate statements about the possible final value of the main thread:
\begin{cor}[Adequate postcondition]
Assume we are given some $\expr_0$ and a set $V \subseteq \Val$ such that the following holds (assuming we can talk about sets like $V$ inside the logic):
Assume we are given some $\expr_1$ and a set $V \subseteq \Val$ such that the following holds (assuming we can talk about sets like $V$ inside the logic):
\[
\TRUE \proves \All\state_0, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{x.\; x \in V}
\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{x.\; x \in V}
\]
Then it is the case that:
\[
\All \state_0, \vec\obs, \val_1, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] ([\ofval(\val_1)] \dplus \tpool_1, \state_1) \Ra \val_1 \in V
\All \state_1, \vec\obs, \val_2, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] ([\ofval(\val_2)] \dplus \tpool_2, \state_2) \Ra \val_2 \in V
\]
\end{cor}
To show this, we assume some $\state_0, \vec\obs, \val_1, \tpool_1, \state_1$ such that $([\expr_0], \state_0) \tpsteps[\vec\obs] ([\ofval(\val_1)] \dplus \tpool_1, \state_1)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \val_1 \in \Val$.
To show this, we assume some $\state_1, \vec\obs, \val_2, \tpool_2, \state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] ([\ofval(\val_2)] \dplus \tpool_2, \state_2)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \val_2 \in \Val$.
Then we only have to show:
$$\TRUE \proves \consstate^{\stateinterp;(\Lam \val. \val \in \Val);\pred_F}_{\stuckness}([\ofval(\val_1)] \dplus \tpool_1, \state_1) \vs[\top][\emptyset] \val_1 \in \Val $$
$$\TRUE \proves \consstate^{\stateinterp;(\Lam \val. \val \in \Val);\pred_F}_{\stuckness}([\ofval(\val_2)] \dplus \tpool_2, \state_2) \vs[\top][\emptyset] \val_2 \in \Val $$
~\par
As a final example, we could use adequacy to show that the state $\state$ of the program is always in some set $\Sigma \subseteq \State$:
\begin{cor}[Adequate state interpretation]
Assume we are given some $\expr_0$ and a set $\Sigma \subseteq \State$ such that the following holds (assuming we can talk about sets like $\Sigma$ inside the logic):
Assume we are given some $\expr_1$ and a set $\Sigma \subseteq \State$ such that the following holds (assuming we can talk about sets like $\Sigma$ inside the logic):
\[
\TRUE \proves \All\state_0, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{\pred} * (\All \state_1, m. \stateinterp(\state_1,(),m) \!\vs[\top][\emptyset] \state_1 \in \Sigma)
\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stuckness, \stateinterp, \pred, \pred_F. \stateinterp(\state_1,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{\pred} * (\All \state_2, m. \stateinterp(\state_2,(),m) \!\vs[\top][\emptyset] \state_2 \in \Sigma)
\]
Then it is the case that:
\[
\All \state_0, \vec\obs, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra \state_1 \in \Sigma
\All \state_1, \vec\obs, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2) \Ra \state_2 \in \Sigma
\]
\end{cor}
To show this, we assume some $\state_0, \vec\obs, \tpool_1, \state_1$ such that $([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \state_1 \in \Sigma$.
To show this, we assume some $\state_1, \vec\obs, \tpool_2, \state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \state_2 \in \Sigma$.
Then we have to show:
\[
(\All \state_1, m. \stateinterp(\state_1,(),m) \!\vs[\top][\emptyset] \state_1 \in \Sigma) \proves \consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_1, \state_1) \vs[\top][\emptyset] \state_1 \in \Sigma
(\All \state_2, m. \stateinterp(\state_2,(),m) \!\vs[\top][\emptyset] \state_2 \in \Sigma) \proves \consstate^{\stateinterp;\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \state_2 \in \Sigma
\]
\paragraph{Hoare triples.}
......
......@@ -114,7 +114,7 @@ Qed.
End adequacy.
(** Iris's generic adequacy result *)
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e σ1 n κs t2 σ2 φ :
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e1 σ1 n κs t2 σ2 φ :
( `{Hinv : !invG Σ},
(|={}=>
(s: stuckness)
......@@ -122,7 +122,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e σ1 n κs t2 σ2 φ :
(Φ fork_post : val Λ iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
stateI σ1 κs 0
WP e @ s; {{ Φ }}
WP e1 @ s; {{ Φ }}
( e2 t2',
(* e2 is the final state of the main thread, t2' the rest *)
t2 = e2 :: t2' -
......@@ -140,7 +140,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e σ1 n κs t2 σ2 φ :
one can use [fupd_intro_mask'] or [fupd_mask_weaken] to introduce the
fancy update. *)
|={,}=> φ ))%I)
nsteps n ([e], σ1) κs (t2, σ2)
nsteps n ([e1], σ1) κs (t2, σ2)
(* Then we can conclude [φ] at the meta-level. *)
φ.
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment