program-logic.tex 29.3 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1

2
\section{Program Logic}
3
\label{sec:program-logic}
4

Ralf Jung's avatar
Ralf Jung committed
5
This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the base logic.
Ralf Jung's avatar
Ralf Jung committed
6
So in the following, we assume that some language $\Lang$ was fixed.
7
Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composeable-resources}.
Ralf Jung's avatar
Ralf Jung committed
8 9


10
\subsection{World Satisfaction, Invariants, Fancy Updates}
Ralf Jung's avatar
Ralf Jung committed
11
\label{sec:invariants}
Ralf Jung's avatar
Ralf Jung committed
12 13 14 15 16

To introduce invariants into our logic, we will define weakest precondition to explicitly thread through the proof that all the invariants are maintained throughout program execution.
However, in order to be able to access invariants, we will also have to provide a way to \emph{temporarily disable} (or ``open'') them.
To this end, we use tokens that manage which invariants are currently enabled.

17
We assume to have the following four cameras available:
Ralf Jung's avatar
Ralf Jung committed
18
\begin{align*}
19 20 21
  \InvName \eqdef{}& \nat \\
  \textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
  \textmon{En} \eqdef{}& \pset{\InvName} \\
22
  \textmon{Dis} \eqdef{}& \finpset{\InvName}
Ralf Jung's avatar
Ralf Jung committed
23 24 25
\end{align*}
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.

26
We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these cameras have been created, such that these names are globally known.
Ralf Jung's avatar
Ralf Jung committed
27

Ralf Jung's avatar
Ralf Jung committed
28
\paragraph{World Satisfaction.}
29
We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
Ralf Jung's avatar
Ralf Jung committed
30
\begin{align*}
31
  W \eqdef{}& \Exists I : \InvName \fpfn \Prop.
32
  \begin{array}[t]{@{} l}
33
    \ownGhost{\gname_{\textmon{Inv}}}{\authfull
Ralf Jung's avatar
Ralf Jung committed
34
      \mapComp {\iname}
35 36 37 38
        {\aginj(\latertinj(\wIso(I(\iname))))}
        {\iname \in \dom(I)}} * \\
    \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right)
  \end{array}
Ralf Jung's avatar
Ralf Jung committed
39 40 41
\end{align*}

\paragraph{Invariants.}
42
The following proposition states that an invariant with name $\iname$ exists and maintains proposition $\prop$:
43 44
\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}
  {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}} \]
Ralf Jung's avatar
Ralf Jung committed
45

46
\paragraph{Fancy Updates and View Shifts.}
Ralf Jung's avatar
Ralf Jung committed
47
Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
48
\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
Ralf Jung's avatar
Ralf Jung committed
49
Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
We use $\top$ as symbol for the largest possible mask, $\nat$, and $\bot$ for the smallest possible mask $\emptyset$.
51 52
We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
%
Ralf Jung's avatar
Ralf Jung committed
53
Fancy updates satisfy the following basic proof rules:
54
\begin{mathparpagebreakable}
Ralf Jung's avatar
Ralf Jung committed
55
\infer[fup-mono]
56 57 58
{\prop \proves \propB}
{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}

Ralf Jung's avatar
Ralf Jung committed
59
\infer[fup-intro-mask]
60
{\mask_2 \subseteq \mask_1}
61
{\prop \proves \pvs[\mask_1][\mask_2]\pvs[\mask_2][\mask_1] \prop}
62

Ralf Jung's avatar
Ralf Jung committed
63
\infer[fup-trans]
64 65 66
{}
{\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}

Ralf Jung's avatar
Ralf Jung committed
67
\infer[fup-upd]
68 69
{}{\upd\prop \proves \pvs[\mask] \prop}

Ralf Jung's avatar
Ralf Jung committed
70
\infer[fup-frame]
71
{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \propB * \prop}
72

Ralf Jung's avatar
Ralf Jung committed
73
\inferH{fup-update}
74 75 76
{\melt \mupd \meltsB}
{\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB}

Ralf Jung's avatar
Ralf Jung committed
77
\infer[fup-timeless]
78 79
{\timeless\prop}
{\later\prop \proves \pvs[\mask] \prop}
80
%
Ralf Jung's avatar
Ralf Jung committed
81
% \inferH{fup-allocI}
82 83 84
% {\text{$\mask$ is infinite}}
% {\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
%gov
Ralf Jung's avatar
Ralf Jung committed
85
% \inferH{fup-openI}
86 87
% {}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
%
Ralf Jung's avatar
Ralf Jung committed
88
% \inferH{fup-closeI}
89
% {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
90
\end{mathparpagebreakable}
91
(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.)
Ralf Jung's avatar
Ralf Jung committed
92

Ralf Jung's avatar
Ralf Jung committed
93
We can further define the notions of \emph{view shifts} and \emph{linear view shifts}:
Ralf Jung's avatar
Ralf Jung committed
94
\begin{align*}
95
  \prop \vsW[\mask_1][\mask_2] \propB \eqdef{}& \prop \wand \pvs[\mask_1][\mask_2] \propB \\
96 97
  \prop \vs[\mask_1][\mask_2] \propB \eqdef{}& \always(\prop \wand \pvs[\mask_1][\mask_2] \propB) \\
  \prop \vs[\mask] \propB \eqdef{}& \prop \vs[\mask][\mask] \propB
Ralf Jung's avatar
Ralf Jung committed
98
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
99
These two are useful when writing down specifications and for comparing with previous versions of Iris, but for reasoning, it is typically easier to just work directly with fancy updates.
100 101 102 103
Still, just to give an idea of what view shifts ``are'', here are some proof rules for them:
\begin{mathparpagebreakable}
\inferH{vs-update}
  {\melt \mupd \meltsB}
104
  {\ownGhost\gname{\melt} \vs[\emptyset] \exists \meltB \in \meltsB.\; \ownGhost\gname{\meltB}}
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
\and
\inferH{vs-trans}
  {\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC}
  {\prop \vs[\mask_1][\mask_3] \propC}
\and
\inferH{vs-imp}
  {\always{(\prop \Ra \propB)}}
  {\prop \vs[\emptyset] \propB}
\and
\inferH{vs-mask-frame}
  {\prop \vs[\mask_1][\mask_2] \propB}
  {\prop \vs[\mask_1 \uplus \mask'][\mask_2 \uplus \mask'] \propB}
\and
\inferH{vs-frame}
  {\prop \vs[\mask_1][\mask_2] \propB}
  {\prop * \propC \vs[\mask_1][\mask_2] \propB * \propC}
\and
\inferH{vs-timeless}
  {\timeless{\prop}}
124
  {\later \prop \vs[\emptyset] \prop}
125

126 127 128 129 130 131 132 133 134 135
% \inferH{vs-allocI}
%   {\infinite(\mask)}
%   {\later{\prop} \vs[\mask] \exists \iname\in\mask.\; \knowInv{\iname}{\prop}}
% \and
% \axiomH{vs-openI}
%   {\knowInv{\iname}{\prop} \proves \TRUE \vs[\{ \iname \} ][\emptyset] \later \prop}
% \and
% \axiomH{vs-closeI}
%   {\knowInv{\iname}{\prop} \proves \later \prop \vs[\emptyset][\{ \iname \} ] \TRUE }
%
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
\inferHB{vs-disj}
  {\prop \vs[\mask_1][\mask_2] \propC \and \propB \vs[\mask_1][\mask_2] \propC}
  {\prop \lor \propB \vs[\mask_1][\mask_2] \propC}
\and
\inferHB{vs-exist}
  {\All \var. (\prop \vs[\mask_1][\mask_2] \propB)}
  {(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB}
\and
\inferHB{vs-always}
  {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC}
  {\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC}
 \and
\inferH{vs-false}
  {}
  {\FALSE \vs[\mask_1][\mask_2] \prop }
\end{mathparpagebreakable}

153
\subsection{Weakest Precondition}
Ralf Jung's avatar
Ralf Jung committed
154

155
Finally, we can define the core piece of the program logic, the proposition that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived.
156 157

\paragraph{Defining weakest precondition.}
Ralf Jung's avatar
Ralf Jung committed
158
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$).
Ralf Jung's avatar
Ralf Jung committed
159 160
We further assume (as a parameter) a predicate $\stateinterp : \State \times \List(\Obs) \times \mathbb N \to \iProp$ that interprets the machine state as an Iris proposition, and a predicate $\pred_F: \Val \to \iProp$ that serves as postcondition for forked-of threads.
The state interpretation can depend on the current physical state, the list of \emph{future} observations as well as the total number of \emph{forked} threads (that is one less that the total number of threads).
161
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.
Ralf Jung's avatar
Ralf Jung committed
162
Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck, \MaybeStuck}$ indicating whether program execution is allowed to get stuck.
Ralf Jung's avatar
Ralf Jung committed
163 164

\begin{align*}
165
  \textdom{wp}(\stateinterp, \pred_F, \stuckness) \eqdef{}& \MU \textdom{wp\any rec}. \Lam \mask, \expr, \pred. \\
166
        & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
Ralf Jung's avatar
Ralf Jung committed
167 168 169
        & \Bigl(\toval(\expr) = \bot \land \All \state, \vec\obs, \vec\obs', n. \stateinterp(\state, \vec\obs \dplus \vec\obs', n) \vsW[\mask][\emptyset] {}\\
        &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step[\vec\obs] \expr', \state', \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
        &\qquad\qquad \stateinterp(\state', \vec\obs', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep[\expr'' \in \vec\expr] \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
170
  \wpre[\stateinterp;\pred_F]\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\stateinterp,\pred_F,\stuckness)(\mask, \expr, \Lam\val.\prop)
Ralf Jung's avatar
Ralf Jung committed
171
\end{align*}
172 173
The $\stateinterp$ and $\pred_F$ will always be set by the context; typically, when instantiating Iris with a language, we also pick the corresponding state interpretation $\stateinterp$ and fork-postcondition $\pred_F$.
All proof rules leave $\stateinterp$ and $\pred_F$ unchanged.
Ralf Jung's avatar
Ralf Jung committed
174 175
If we leave away the mask $\mask$, we assume it to default to $\top$.
If we leave away the stuckness $\stuckness$, it defaults to $\NotStuck$.
Ralf Jung's avatar
Ralf Jung committed
176

177
\paragraph{Laws of weakest precondition.}
Ralf Jung's avatar
Ralf Jung committed
178
The following rules can all be derived:
179 180
\begin{mathpar}
\infer[wp-value]
Ralf Jung's avatar
Ralf Jung committed
181
{}{\prop[\val/\var] \proves \wpre{\val}[\stuckness;\mask]{\Ret\var.\prop}}
182 183

\infer[wp-mono]
Ralf Jung's avatar
Ralf Jung committed
184 185
{\mask_1 \subseteq \mask_2 \and \vctx,\var:\textlog{val}\mid\prop \proves \propB \and (\stuckness_2 = \MaybeStuck \lor \stuckness_1 = \stuckness_2)}
{\vctx\mid\wpre\expr[\stuckness_1;\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\stuckness_2;\mask_2]{\Ret\var.\propB}}
186

Ralf Jung's avatar
Ralf Jung committed
187
\infer[fup-wp]
Ralf Jung's avatar
Ralf Jung committed
188
{}{\pvs[\mask] \wpre\expr[\stuckness;\mask]{\Ret\var.\prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\prop}}
189

Ralf Jung's avatar
Ralf Jung committed
190
\infer[wp-fup]
Ralf Jung's avatar
Ralf Jung committed
191
{}{\wpre\expr[\stuckness;\mask]{\Ret\var.\pvs[\stuckness;\mask] \prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\prop}}
192 193

\infer[wp-atomic]
Ralf Jung's avatar
Ralf Jung committed
194 195 196 197
{\stuckness = \NotStuck \Ra \atomic(\expr) \and
 \stuckness = \MaybeStuck \Ra \stronglyAtomic(\expr)}
{\pvs[\mask_1][\mask_2] \wpre\expr[\stuckness;\mask_2]{\Ret\var. \pvs[\mask_2][\mask_1]\prop}
 \proves \wpre\expr[\stuckness;\mask_1]{\Ret\var.\prop}}
198 199

\infer[wp-frame]
Ralf Jung's avatar
Ralf Jung committed
200
{}{\propB * \wpre\expr[\stuckness;\mask]{\Ret\var.\prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\propB*\prop}}
201 202 203

\infer[wp-frame-step]
{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
Ralf Jung's avatar
Ralf Jung committed
204
{\wpre\expr[\stuckness;\mask_2]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\stuckness;\mask_1]{\Ret\var.\propB*\prop}}
205 206 207

\infer[wp-bind]
{\text{$\lctx$ is a context}}
Ralf Jung's avatar
Ralf Jung committed
208
{\wpre\expr[\stuckness;\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\stuckness;\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\stuckness;\mask]{\Ret\varB.\prop}}
209 210
\end{mathpar}

211
We will also want a rule that connect weakest preconditions to the operational semantics of the language.
Ralf Jung's avatar
Ralf Jung committed
212 213
This basically just copies the second branch (the non-value case) of the definition of weakest preconditions.

214 215
\begin{mathpar}
  \infer[wp-lift-step]
216
  {\toval(\expr_1) = \bot}
217
  { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
Ralf Jung's avatar
Ralf Jung committed
218 219 220
        ~~\All \state_1,\vec\obs,\vec\obs',n. \stateinterp(\state_1,\vec\obs \dplus \vec\obs', n) \vsW[\mask][\emptyset] (\stuckness = \NotStuck \Ra \red(\expr_1,\state_1)) * {}\\
        \qquad~ \All \expr_2, \state_2, \vec\expr.  (\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr)  \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
        \qquad\qquad\Bigl(\stateinterp(\state_2,\vec\obs',n+|\vec\expr|) * \wpre[\stateinterp;\pred_F]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep[\expr_\f \in \vec\expr] \wpre[\stateinterp\pred_F]{\expr_\f}[\stuckness;\top]{\pred_F}\Bigr)  {}\\
221
        \proves \wpre[\stateinterp\pred_F]{\expr_1}[\stuckness;\mask]{\Ret\var.\prop}
222 223 224
      \end{inbox}} }
\end{mathpar}

225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
% We can further derive some slightly simpler rules for special cases.
% \begin{mathparpagebreakable}
%   \infer[wp-lift-pure-step]
%   {\All \state_1. \red(\expr_1, \state_1) \and
%    \All \state_1, \expr_2, \state_2, \vec\expr. \expr_1,\state_1 \step \expr_2,\state_2,\vec\expr \Ra \state_1 = \state_2 }
%   {\later\All \state, \expr_2, \vec\expr. (\expr_1,\state \step \expr_2, \state,\vec\expr)  \Ra \wpre{\expr_2}[\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask]{\Ret\var.\prop}}

%   \infer[wp-lift-atomic-step]
%   {\atomic(\expr_1) \and
%    \red(\expr_1, \state_1)}
%   { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \vec\expr. (\expr_1,\state_1 \step \ofval(\val),\state_2,\vec\expr)  * \ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\ \proves  \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
%   \end{inbox}} }

%   \infer[wp-lift-atomic-det-step]
%   {\atomic(\expr_1) \and
%    \red(\expr_1, \state_1) \and
%    \All \expr'_2, \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_2 = \state_2' \land \toval(\expr_2') = \val_2 \land \vec\expr = \vec\expr'}
%   {\later\ownPhys{\state_1} * \later \Bigl(\ownPhys{\state_2} \wand \prop[\val_2/\var] * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}

%   \infer[wp-lift-pure-det-step]
%   {\All \state_1. \red(\expr_1, \state_1) \\
%    \All \state_1, \expr_2', \state'_2, \vec\expr'. \expr_1,\state_1 \step \expr'_2,\state'_2,\vec\expr' \Ra \state_1 = \state'_2 \land \expr_2 = \expr_2' \land \vec\expr = \vec\expr'}
%   {\later \Bigl( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \Bigr) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
% \end{mathparpagebreakable}
249 250


Ralf Jung's avatar
Ralf Jung committed
251
\paragraph{Adequacy of weakest precondition.}
252

253 254
\newcommand\traceprop{\Sigma}

255
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.
256 257 258 259 260 261 262 263 264 265 266
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}):
267
\[\begin{array}{rMcMl}
268 269
  \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}
270
\end{array}\]
271 272
The signature can of course state arbitrary additional properties of $\hat{\traceprop}$, as long as they are proven sound.

273
The adequacy statement now reads as follows:
274
\begin{align*}
275 276 277 278 279 280 281 282 283 284 285
 &\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
286
\end{align*}
287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311
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)
\]
312

313 314 315 316 317
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:
318
\begin{align*}
319 320
 &(\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
321 322
\end{align*}

323

Ralf Jung's avatar
Ralf Jung committed
324
\paragraph{Hoare triples.}
Robbert Krebbers's avatar
Robbert Krebbers committed
325
It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq.
Ralf Jung's avatar
Ralf Jung committed
326 327
Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
\[
328
\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \wand \wpre{\expr}[\mask]{\Ret\val.\propB})}
Ralf Jung's avatar
Ralf Jung committed
329
\]
330
We assume the state interpretation $\stateinterp$ to be fixed by the context.
Ralf Jung's avatar
Ralf Jung committed
331

Ralf Jung's avatar
Ralf Jung committed
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364
We only give some of the proof rules for Hoare triples here, since we usually do all our reasoning directly with weakest preconditions and use Hoare triples only to write specifications.
\begin{mathparpagebreakable}
\inferH{Ht-ret}
  {}
  {\hoare{\TRUE}{\valB}{\Ret\val. \val = \valB}[\mask]}
\and
\inferH{Ht-bind}
  {\text{$\lctx$ is a context} \and \hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \\
   \All \val. \hoare{\propB}{\lctx(\val)}{\Ret\valB.\propC}[\mask]}
  {\hoare{\prop}{\lctx(\expr)}{\Ret\valB.\propC}[\mask]}
\and
\inferH{Ht-csq}
  {\prop \vs \prop' \\
    \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\   
   \All \val. \propB' \vs \propB}
  {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
\and
% \inferH{Ht-mask-weaken}
%   {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]}
%   {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask \uplus \mask']}
% \\\\
\inferH{Ht-frame}
  {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask]}
  {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
\and
% \inferH{Ht-frame-step}
%   {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot \and \mask_2 \subseteq \mask_2 \\\\ \propC_1 \vs[\mask_1][\mask_2] \later\propC_2 \and \propC_2 \vs[\mask_2][\mask_1] \propC_3}
%   {\hoare{\prop * \propC_1}{\expr}{\Ret\val. \propB * \propC_3}[\mask \uplus \mask_1]}
% \and
\inferH{Ht-atomic}
  {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\
    \hoare{\prop'}{\expr}{\Ret\val.\propB'}[\mask] \\   
   \All\val. \propB' \vs[\mask][\mask \uplus \mask'] \propB \\
Ralf Jung's avatar
Ralf Jung committed
365
   \atomic(\expr)
Ralf Jung's avatar
Ralf Jung committed
366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396
  }
  {\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \mask']}
\and
\inferH{Ht-false}
  {}
  {\hoare{\FALSE}{\expr}{\Ret \val. \prop}[\mask]}
\and
\inferHB{Ht-disj}
  {\hoare{\prop}{\expr}{\Ret\val.\propC}[\mask] \and \hoare{\propB}{\expr}{\Ret\val.\propC}[\mask]}
  {\hoare{\prop \lor \propB}{\expr}{\Ret\val.\propC}[\mask]}
\and
\inferHB{Ht-exist}
  {\All \var. \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask]}
  {\hoare{\Exists \var. \prop}{\expr}{\Ret\val.\propB}[\mask]}
\and
\inferHB{Ht-box}
  {\always\propB \proves \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]}
  {\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]}
% \and
% \inferH{Ht-inv}
%   {\hoare{\later\propC*\prop}{\expr}{\Ret\val.\later\propC*\propB}[\mask] \and
%    \physatomic{\expr}
%   }
%   {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
% \and
% \inferH{Ht-inv-timeless}
%   {\hoare{\propC*\prop}{\expr}{\Ret\val.\propC*\propB}[\mask] \and
%    \physatomic{\expr} \and \timeless\propC
%   }
%   {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
\end{mathparpagebreakable}
Ralf Jung's avatar
Ralf Jung committed
397

398
\subsection{Invariant Namespaces}
Ralf Jung's avatar
Ralf Jung committed
399 400
\label{sec:namespaces}

401
In \Sref{sec:invariants}, we defined a proposition $\knowInv\iname\prop$ expressing knowledge (\ie the proposition is persistent) that $\prop$ is maintained as invariant with name $\iname$.
Ralf Jung's avatar
Ralf Jung committed
402 403 404 405 406 407
The concrete name $\iname$ is picked when the invariant is allocated, so it cannot possibly be statically known -- it will always be a variable that's threaded through everything.
However, we hardly care about the actual, concrete name.
All we need to know is that this name is \emph{different} from the names of other invariants that we want to open at the same time.
Keeping track of the $n^2$ mutual inequalities that arise with $n$ invariants quickly gets in the way of the actual proof.

To solve this issue, instead of remembering the exact name picked for an invariant, we will keep track of the \emph{namespace} the invariant was allocated in.
408
Namespaces are sets of invariants, following a tree-like structure:
Ralf Jung's avatar
Ralf Jung committed
409 410 411 412 413 414 415 416
Think of the name of an invariant as a sequence of identifiers, much like a fully qualified Java class name.
A \emph{namespace} $\namesp$ then is like a Java package: it is a sequence of identifiers that we think of as \emph{containing} all invariant names that begin with this sequence. For example, \texttt{org.mpi-sws.iris} is a namespace containing the invariant name \texttt{org.mpi-sws.iris.heap}.

The crux is that all namespaces contain infinitely many invariants, and hence we can \emph{freely pick} the namespace an invariant is allocated in -- no further, unpredictable choice has to be made.
Furthermore, we will often know that namespaces are \emph{disjoint} just by looking at them.
The namespaces $\namesp.\texttt{iris}$ and $\namesp.\texttt{gps}$ are disjoint no matter the choice of $\namesp$.
As a result, there is often no need to track disjointness of namespaces, we just have to pick the namespaces that we allocate our invariants in accordingly.

Robbert Krebbers's avatar
Robbert Krebbers committed
417
Formally speaking, let $\namesp \in \textlog{InvNamesp} \eqdef \List(\nat)$ be the type of \emph{invariant namespaces}.
Ralf Jung's avatar
Ralf Jung committed
418 419 420 421
We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$.
(In other words, the list is ``backwards''. This is because cons-ing to the list, like the dot does above, is easier to deal with in Coq than appending at the end.)

The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name).
Robbert Krebbers's avatar
Robbert Krebbers committed
422
They, too, are lists of $\nat$, the same type as namespaces.
423 424
In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\InvName$, the type of ``plain'' invariant names.
Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\InvName$ is infinite.
Ralf Jung's avatar
Ralf Jung committed
425 426
Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]

427
We will overload the notation for invariant propositions for using namespaces instead of names:
Ralf Jung's avatar
Ralf Jung committed
428
\[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]
Ralf Jung's avatar
Ralf Jung committed
429
We can now derive the following rules (this involves unfolding the definition of fancy updates):
Ralf Jung's avatar
Ralf Jung committed
430 431
\begin{mathpar}
  \axiomH{inv-persist}{\knowInv\namesp\prop \proves \always\knowInv\namesp\prop}
Ralf Jung's avatar
Ralf Jung committed
432

433
  \axiomH{inv-alloc}{\later\prop \proves \pvs[\emptyset] \knowInv\namesp\prop}
Ralf Jung's avatar
Ralf Jung committed
434

Ralf Jung's avatar
Ralf Jung committed
435 436 437
  \inferH{inv-open}
  {\namesp \subseteq \mask}
  {\knowInv\namesp\prop \vs[\mask][\mask\setminus\namesp] \later\prop * (\later\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)}
Ralf Jung's avatar
Ralf Jung committed
438

Ralf Jung's avatar
Ralf Jung committed
439 440 441 442
  \inferH{inv-open-timeless}
  {\namesp \subseteq \mask \and \timeless\prop}
  {\knowInv\namesp\prop \vs[\mask][\mask\setminus\namesp] \prop * (\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)}
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
443

Ralf Jung's avatar
Ralf Jung committed
444 445 446 447
\subsection{Accessors}

The two rules \ruleref{inv-open} and \ruleref{inv-open-timeless} above may look a little surprising, in the sense that it is not clear on first sight how they would be applied.
The rules are the first \emph{accessors} that show up in this document.
448
Accessors are propositions of the form
Ralf Jung's avatar
Ralf Jung committed
449 450
\[ \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC) \]

451 452
One way to think about such propositions is as follows:
Given some accessor, if during our verification we have the proposition $\prop$ and the mask $\mask_1$ available, we can use the accessor to \emph{access} $\propB$ and obtain the witness $\var$.
Ralf Jung's avatar
Ralf Jung committed
453 454 455 456 457
We call this \emph{opening} the accessor, and it changes the mask to $\mask_2$.
Additionally, opening the accessor provides us with $\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC$, a \emph{linear view shift} (\ie a view shift that can only be used once).
This linear view shift tells us that in order to \emph{close} the accessor again and go back to mask $\mask_1$, we have to pick some $\varB$ and establish the corresponding $\propB'$.
After closing, we will obtain $\propC$.

458 459 460 461 462 463 464 465 466 467
Using \ruleref{vs-trans} and \ruleref{Ht-atomic} (or the corresponding proof rules for fancy updates and weakest preconditions), we can show that it is possible to open an accessor around any view shift and any \emph{atomic} expression:
\begin{mathpar}
  \inferH{Acc-vs}
  {\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC) \and
   \All\var. \propB * \prop_F \vs[\mask_2] \Exists\varB. \propB' * \prop_F}
  {\prop * \prop_F \vs[\mask_1] \propC * \prop_F}

  \inferH{Acc-Ht}
  {\prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC) \and
   \All\var. \hoare{\propB * \prop_F}\expr{\Exists\varB. \propB' * \prop_F}[\mask_2] \and
Ralf Jung's avatar
Ralf Jung committed
468
   \atomic(\expr)}
469 470 471
  {\hoare{\prop * \prop_F}\expr{\propC * \prop_F}[\mask_1]}
\end{mathpar}

Ralf Jung's avatar
Ralf Jung committed
472 473 474 475 476
Furthermore, in the special case that $\mask_1 = \mask_2$, the accessor can be opened around \emph{any} expression.
For this reason, we also call such accessors \emph{non-atomic}.

The reasons accessors are useful is that they let us talk about ``opening X'' (\eg ``opening invariants'') without having to care what X is opened around.
Furthermore, as we construct more sophisticated and more interesting things that can be opened (\eg invariants that can be ``cancelled'', or STSs), accessors become a useful interface that allows us to mix and match different abstractions in arbitrary ways.
477

478 479
For the special case that $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition:
\[ \Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop)  \]
Robbert Krebbers's avatar
Robbert Krebbers committed
480
This accessor is ``idempotent'' in the sense that it does not actually change the state.  After applying it, we get our $\prop$ back so we end up where we started.
481

482 483 484 485
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: