@@ -224,76 +224,108 @@ This basically just copies the second branch (the non-value case) of the definit
\paragraph{Adequacy of weakest precondition.}
\newcommand\traceprop{\Sigma}
\newcommand\metaprop{p}
\newcommand\consstate{C}
The purpose of the adequacy statement is to show that our notion of weakest preconditions is \emph{realistic} in the sense that it actually has anything to do with the actual behavior of the program.
The most general form of the adequacy statement is about proving properties of arbitrary program executions.
That is, the goal is to prove a statement of the form
Furthermore, we assume that the \emph{interpretation}$\Sem{\hat{\traceprop}}$ of $\hat{\traceprop}$ reflects $\traceprop$ (also see \Sref{sec:model}):
\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.
To verify that $\metaprop$ holds, it is sufficient to show the following Iris entailment:
In other words, to show that $\traceprop$ holds for all possible executions of the program, we have to prove an entailment in Iris that, starting from the empty context, proves that the initial state interpretation holds, proves a weakest precondition, \emph{and} proves that $\hat{\traceprop}$ holds under the following assumptions:
In other words, to show that $\metaprop$ holds, we have to prove an entailment in Iris that, starting from the empty context, chooses some state interpretation, postcondition, forked-thread postcondition and stuckness and then proves:
\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)$.
\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.
\item The final thread-pool $\tpool_1$ contains the final state of the main thread $\expr_1$, and any number of additional threads in $\tpool_1'$.
\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 state interpretation holds for the final state.
\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.
\end{itemize}
Notice also that the adequacy statement quantifies over the program trace only once, so it can be easily specialized to, say, some particular initial state $\state_0$.
This lets us show properties that only hold for some executions.
Furthermore, 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.
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_0$ 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:
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)$.
We can then show the premise of adequacy using the Iris entailment that we assumed in the corollary and:
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, if we wanted to show that the final value of the main thread is always in some set $V \subseteq\Val$, we could pick
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):
\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
\]
\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$.
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):
\[
\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)
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$.
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
\]
\paragraph{Hoare triples.}
It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq.
