diff --git a/CHANGELOG.md b/CHANGELOG.md index bfa50834cea8066800bb39ef9c8dfd3121c7e31c..c4153ca2215e1ae640a043b8fe1dc48074f5c6fc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -27,9 +27,9 @@ Changes in the theory of Iris itself: the number of forked-off threads, and have a global fixed proposition that describes the postcondition of each forked-off thread (instead of it being True). -* [#] A stronger adequacy statement for weakest preconditions that involves - the final state, involves the post-condition of forked-off threads, and also - applies if the main-thread has not terminated. +* A stronger adequacy statement for weakest preconditions that involves + the final state, the post-condition of forked-off threads, and also applies if + the main-thread has not terminated. * The user-chosen functor used to instantiate the Iris logic now goes from COFEs to Cameras (it was OFEs to Cameras). diff --git a/docs/program-logic.tex b/docs/program-logic.tex index 7f1c6a59fe8cb1505b1704506b801938d9cb15b0..354dda8b2e66d410ce2f0848efd3e5e0cebc4f9c 100644 --- a/docs/program-logic.tex +++ b/docs/program-logic.tex @@ -250,48 +250,77 @@ This basically just copies the second branch (the non-value case) of the definit \paragraph{Adequacy of weakest precondition.} +\newcommand\traceprop{\Sigma} + 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. -There are two properties we are looking for: First of all, the postcondition should reflect actual properties of the values the program can terminate with. -Second, a proof of a weakest precondition with any postcondition should imply that the program is \emph{safe}, \ie that it does not get stuck. - -\begin{defn}[Adequacy] - A program $\expr$ in some initial state $\state$ is \emph{adequate} for stuckness $\stuckness$ and a set $V \subseteq \Val \times \State$ of legal return-value-final-state combinations (written $\expr, \state \vDash_\stuckness V$) if for all $\tpool', \state'$ such that $([\expr], \state) \tpsteps[\vec\obs] (\tpool', \state')$ we have -\begin{enumerate} -\item Safety: If $\stuckness = \NotStuck$, then for any $\expr' \in \tpool'$ we have that either $\expr'$ is a - value, or $$\red(\expr'_i,\state')$$: - $\stuckness = \NotStuck \Ra \All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')$ - Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step. -\item Legal return value: If $\tpool'_1$ (the main thread) is a value $\val'$, then $\val' \in V$: - $\All \val',\tpool''. \tpool' = [\val'] \dplus \tpool'' \Ra (\val',\state') \in V$ -\end{enumerate} -\end{defn} - -To express the adequacy statement for functional correctness, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic: -$\pred : \Val \times \State \to \Prop \in \SigFn$ -Furthermore, we assume that the \emph{interpretation} $\Sem\pred$ of $\pred$ reflects some set $V$ of legal return values and final states into the logic (also see \Sref{sec:model}): +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 +$+\All \expr_0, \state_0, \vec\obs, \tpool_1, \state_1. ([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra (\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \in \traceprop +$ +for some \emph{meta-level} relation $\traceprop$ characterizing the trace property'' we are interested in. + +To state the adequacy theorem, we need a way to talk about $\traceprop$ inside Iris. +To this end, we assume that the signature $\Sig$ contains some predicate $\hat{\traceprop}$: +$\hat{\traceprop} : \Expr \times \State \times \List(\Obs) \times \List(\Expr) \times \State \to \Prop \in \SigFn$ +Furthermore, we assume that the \emph{interpretation} $\Sem{\hat{\traceprop}}$ of $\hat{\traceprop}$ reflects $\traceprop$ (also see \Sref{sec:model}): $\begin{array}{rMcMl} - \Sem\pred &:& \Sem{\Val\times\State\,} \nfn \Sem\Prop \\ - \Sem\pred &\eqdef& \Lam (\val,\state). \Lam \any. \setComp{n}{(v,\state) \in V} + \Sem{\hat{\traceprop}} &:& \Sem{\Expr \times \State \times \List(\Obs) \times \List(\Expr) \times \State\,} \nfn \Sem\Prop \\ + \Sem{\hat{\traceprop}} &\eqdef& \Lam (\expr_0, \state_0, \vec\obs, \tpool_1, \state_1). \Lam \any. \setComp{n}{(\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \in \traceprop} \end{array}$ -The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound. +The signature can of course state arbitrary additional properties of $\hat{\traceprop}$, as long as they are proven sound. + The adequacy statement now reads as follows: \begin{align*} - &\All \mask, \expr, \state. - \\&( \TRUE \proves \All\vec\obs. \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]{x.\; \All \state, m. \stateinterp(\state', (), m) \vsW[\top][\emptyset] \pred(x,\state')}) \Ra - \\&\expr, \state \vDash_\stuckness V + &\All \expr_0, \state_0, \vec\obs, \tpool_1, \state_1.\\ + &( \TRUE \proves \pvs[\top] \Exists \stuckness, \stateinterp, \pred_F, \pred. {}\\ + &\quad\stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\stuckness;\top]{x.\; \pred(x)} * {}\\ + &\quad(\All \expr_1, \tpool_1'. \tpool_1 = [\expr_1] \dplus \tpool_1' \wand {}\\ + &\quad\quad (s = \NotStuck \Ra \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1) ) \wand {}\\ + &\quad\quad \stateinterp(\state_1, (), |\tpool_1'|) \wand{}\\ + &\quad\quad (\toval(\expr_1) \ne \bot \wand \pred(\toval(\expr_1))) \wand{}\\ + &\quad\quad (\Sep[\expr \in \tpool_1'] \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))) \wand{}\\ + &\quad\quad \pvs[\top,\emptyset] \hat{\traceprop}(\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \\ + &\quad ) \Ra{}\\ + &([\expr_0], \state_0) \tpsteps[\vec\obs] (\tpool_1, \state_1) \Ra (\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \in \traceprop \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. -Also, notice that the proof of $\expr$ must be performed with a universally quantified list of observations $\vec\obs$, but the \emph{entire} list is known to the proof from the beginning. +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: +\begin{itemize} +\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 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 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. +We would pick +$+\traceprop(\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \eqdef \All \expr \in \tpool_1. \toval(\expr) \neq \bot \lor \red(\expr, \state_1) +$ +and we would show the following in Iris: +$+\TRUE \proves \All \state_0, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred_F, \pred. \stateinterp(\state_0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_0}[\NotStuck;\top]{x.\; \pred(x)} +$ +The adequacy theorem would then give us: +$+\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) +$ -The following variant of adequacy also allows exploiting the second parameter of $\stateinterp$, the number of threads, but only applies when \emph{all} threads have reduced to a value: +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 +$+\traceprop(\expr_0, \state_0, \vec\obs, \tpool_1, \state_1) \eqdef \All\val_1, \tpool_1'. \tpool_1 = [\ofval(\val_1)] \dplus \tpool_1' \Ra \val_1 \in \Val +$ +and then we could derive the following from the main adequacy theorem: \begin{align*} - &\All \mask, \expr, \state, \vec\obs, \val, \vec\val, \state'. - \\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]% - {x.\; \stateinterp(\state',(),|\vec\val|) * \Sep_{y \in \vec\val} \pred_F(y) \vsW[\top][\emptyset] \pred(x,\state')}) \Ra - \\&([\expr], \state) \tpsteps[\vec\obs] (\val :: \vec\val, \state') \Ra - \\&(\val,\state') \in V + &(\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}) \Ra{}\\ + &\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{align*} + \paragraph{Hoare triples.} It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq. Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple: