Newer
Older
A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that
\begin{itemize}
\item There exist functions $\ofval : \textdom{Val} \to \textdom{Expr}$ and $\toval : \textdom{Expr} \pfn \textdom{val}$ (notice the latter is partial), such that
\begin{mathpar} {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All\val. \toval(\ofval(\val)) = \val}
\end{mathpar}
\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{\bot})\]
We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\
A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_f$ is forked off.
\item All values are stuck:
\[ \expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot \]
\item There is a predicate defining \emph{atomic} expressions satisfying
\let\oldcr\cr
\begin{mathpar}
{\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and
{{
\begin{inbox}
\All\expr_1, \state_1, \expr_2, \state_2, \expr_f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
\end{inbox}
}}
\end{mathpar}
In other words, atomic expression \emph{reduce in one step to a value}.
It does not matter whether they fork off an arbitrary expression.
\end{itemize}
\begin{defn}
An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
\[ \Exists \expr_2, \state_2, \expr_f. \expr,\state \step \expr_2,\state_2,\expr_f \]
A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
\begin{enumerate}[itemsep=0pt]
\item $\lctx$ does not turn non-values into values:\\
$\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $
\item One can perform reductions below $\lctx$:\\
$\All \expr_1, \state_1, \expr_2, \state_2, \expr_f. \expr_1, \state_1 \step \expr_2,\state_2,\expr_f \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr_f $
\item Reductions stay below $\lctx$ until there is a value in the hole:\\
$\All \expr_1', \state_1, \expr_2, \state_2, \expr_f. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr_f \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr_f $
For any language $\Lang$, we define the corresponding thread-pool semantics.
\paragraph{Machine syntax}
\[
\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n
\]
\judgment{Machine reduction} {\cfg{\tpool}{\state} \step
\cfg{\tpool'}{\state'}}
\begin{mathpar}
\infer
{\expr_1, \state_1 \step \expr_2, \state_2, \expr_f \and \expr_f \neq \bot}
{\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
\cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_f]}{\state'}}
\and\infer
{\expr_1, \state_1 \step \expr_2, \state_2}
{\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
\cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state'}}
\end{mathpar}
To instantiate Iris, you need to define the following parameters:
\begin{itemize}
\item A language $\Lang$
\item A locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit
\noindent
As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language.
You have to make sure that $\SigType$ includes the base types:
\[
\SigType \supseteq \{ \textlog{Val}, \textlog{Expr}, \textlog{State}, \textlog{M}, \textlog{InvName}, \textlog{InvMask}, \Prop \}
\]
Elements of $\SigType$ are ranged over by $\sigtype$.
Each function symbol in $\SigFn$ has an associated \emph{arity} comprising a natural number $n$ and an ordered list of $n+1$ types $\type$ (the grammar of $\type$ is defined below, and depends only on $\SigType$).
We write
\[
\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn
\]
to express that $\sigfn$ is a function symbol with the indicated arity.
Furthermore, $\SigAx$ is a set of \emph{axioms}, that is, terms $\term$ of type $\Prop$.
Again, the grammar of terms and their typing rules are defined below, and depends only on $\SigType$ and $\SigFn$, not on $\SigAx$.
Elements of $\SigAx$ are ranged over by $\sigax$.
\subsection{Grammar}\label{sec:grammar}
\paragraph{Syntax.}
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$):
\begin{align*}
\type \times \type \mid
\type \to \type
\\[0.4em]
\sigfn(\term_1, \dots, \term_n) \mid
(\term, \term) \mid
\pi_i\; \term \mid
\term \mtimes \term \mid
\\&
\FALSE \mid
\TRUE \mid
\prop \Ra \prop \mid
\prop \land \prop \mid
\prop \lor \prop \mid
\prop * \prop \mid
\prop \wand \prop \mid
\\&
\Exists \var:\type. \prop \mid
\All \var:\type. \prop \mid
\\&
\knowInv{\term}{\prop} \mid
\ownPhys{\term} \mid
\always\prop \mid
{\later\prop} \mid
\wpre{\term}[\term]{\Ret\var.\term}
\end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertions about propositions, defined as follows:
\[ \vctx \proves \timeless{\prop} \eqdef \vctx\mid\later\prop \proves \prop \lor \later\FALSE \]
\paragraph{Metavariable conventions.}
We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
\[
\begin{array}{r|l}
\term, \termB & \text{arbitrary} \\
\val, \valB & \textlog{Val} \\
\expr & \textlog{Expr} \\
\state & \textlog{State} \\
\end{array}
\qquad\qquad
\begin{array}{r|l}
\iname & \textlog{InvName} \\
\mask & \textlog{InvMask} \\
\melt, \meltB & \textlog{M} \\
\prop, \propB, \propC & \Prop \\
\pred, \predB, \predC & \type\to\Prop \text{ (when $\type$ is clear from context)} \\
\end{array}
\]
\paragraph{Variable conventions.}
We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence.
\subsection{Types}\label{sec:types}
Iris terms are simply-typed.
The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable context $\vctx$, the term $\term$ has type $\type$.
A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types.
In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$.
\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}}
\begin{mathparpagebreakable}
%%% variables and function symbols
\and
\infer{\vctx \proves \wtt{\term}{\type}}
{\vctx, x:\type' \proves \wtt{\term}{\type}}
\and
\infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}}
{\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}}
\and
\infer{\vctx_1, x:\type', y:\type'', \vctx_2 \proves \wtt{\term}{\type}}
{\vctx_1, x:\type'', y:\type', \vctx_2 \proves \wtt{\term[y/x,x/y]}{\type}}
\and
\infer{
\vctx \proves \wtt{\term_1}{\type_1} \and
\cdots \and
\vctx \proves \wtt{\term_n}{\type_n} \and
\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn
}{
\vctx \proves \wtt {\sigfn(\term_1, \dots, \term_n)} {\type_{n+1}}
}
%%% products
\and
\axiom{\vctx \proves \wtt{()}{1}}
\and
\infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}}
{\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}}
\and
\infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}}
{\vctx \proves \wtt{\pi_i\,\term}{\type_i}}
%%% functions
\and
\infer{\vctx, x:\type \proves \wtt{\term}{\type'}}
{\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}}
\and
\infer
{\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}}
{\vctx \proves \wtt{\term(\termB)}{\type'}}
%%% monoids
\and
\infer{}{\vctx \proves \wtt\munit{\textlog{M}}}
\and
\infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}}
\and
\infer{\vctx \proves \wtt{\melt}{\textlog{M}} \and \vctx \proves \wtt{\meltB}{\textlog{M}}}
{\vctx \proves \wtt{\melt \mtimes \meltB}{\textlog{M}}}
%%% props and predicates
\\
\axiom{\vctx \proves \wtt{\FALSE}{\Prop}}
\and
\axiom{\vctx \proves \wtt{\TRUE}{\Prop}}
\and
\infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}}
{\vctx \proves \wtt{\term =_\type \termB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop \Ra \propB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop \land \propB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop \lor \propB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop * \propB}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}}
{\vctx \proves \wtt{\prop \wand \propB}{\Prop}}
\and
\infer{
\vctx, \var:\type \proves \wtt{\term}{\type} \and
\text{$\var$ is guarded in $\term$}
}{
\vctx \proves \wtt{\MU \var:\type. \term}{\type}
}
\and
\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}}
\and
\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\All x:\type. \prop}{\Prop}}
\and
\infer{
\vctx \proves \wtt{\prop}{\Prop} \and
\vctx \proves \wtt{\iname}{\textlog{InvName}}
}{
\vctx \proves \wtt{\knowInv{\iname}{\prop}}{\Prop}
}
\and
\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
{\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
\and
\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
{\vctx \proves \wtt{\mval(\melt)}{\Prop}}
\and
\infer{\vctx \proves \wtt{\state}{\textlog{State}}}
{\vctx \proves \wtt{\ownPhys{\state}}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\always\prop}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\later\prop}{\Prop}}
\and
\infer{
\vctx \proves \wtt{\prop}{\Prop} \and
\vctx \proves \wtt{\mask}{\textlog{InvMask}} \and
\vctx \proves \wtt{\mask'}{\textlog{InvMask}}
}{
\vctx \proves \wtt{\pvs[\mask][\mask'] \prop}{\Prop}
}
\and
\infer{
\vctx \proves \wtt{\expr}{\textlog{Expr}} \and
\vctx,\var:\textlog{Val} \proves \wtt{\term}{\Prop} \and
\vctx \proves \wtt{\mask}{\textlog{InvMask}}
}{
\vctx \proves \wtt{\wpre{\expr}[\mask]{\Ret\var.\term}}{\Prop}
}
\end{mathparpagebreakable}
The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold.
We implicitly assume that an arbitrary variable context, $\vctx$, is added to every constituent of the rules.
Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ can be derived.
\judgment{}{\vctx \mid \pfctx \proves \prop}
\paragraph{Laws of intuitionistic higher-order logic with equality.}
This is entirely standard.
\begin{mathparpagebreakable}
\infer[Asm]
{\prop \in \pfctx}
{\pfctx \proves \prop}
\and
{\pfctx \proves \prop \\ \pfctx \proves \term =_\type \term'}
{\pfctx \proves \prop[\term'/\term]}
\and
\infer[Refl]
{}
{\pfctx \proves \term =_\type \term}
\and
\infer[$\bot$E]
{\pfctx \proves \FALSE}
{\pfctx \proves \prop}
\and
\infer[$\top$I]
{}
{\pfctx \proves \TRUE}
\and
\infer[$\wedge$I]
{\pfctx \proves \prop \\ \pfctx \proves \propB}
{\pfctx \proves \prop \wedge \propB}
\and
\infer[$\wedge$EL]
{\pfctx \proves \prop \wedge \propB}
{\pfctx \proves \prop}
\and
\infer[$\wedge$ER]
{\pfctx \proves \prop \wedge \propB}
{\pfctx \proves \propB}
\and
\infer[$\vee$IL]
{\pfctx \proves \prop }
{\pfctx \proves \prop \vee \propB}
\and
\infer[$\vee$IR]
{\pfctx \proves \propB}
{\pfctx \proves \prop \vee \propB}
\and
\infer[$\vee$E]
{\pfctx \proves \prop \vee \propB \\
\pfctx, \prop \proves \propC \\
\pfctx, \propB \proves \propC}
{\pfctx \proves \propC}
\and
\infer[$\Ra$I]
{\pfctx, \prop \proves \propB}
{\pfctx \proves \prop \Ra \propB}
\and
\infer[$\Ra$E]
{\pfctx \proves \prop \Ra \propB \\ \pfctx \proves \prop}
{\pfctx \proves \propB}
\and
\infer[$\forall$I]
{ \vctx,\var : \type\mid\pfctx \proves \prop}
{\vctx\mid\pfctx \proves \forall \var: \type.\; \prop}
\and
\infer[$\forall$E]
{\vctx\mid\pfctx \proves \forall \var :\type.\; \prop \\
\vctx \proves \wtt\term\type}
{\vctx\mid\pfctx \proves \prop[\term/\var]}
\and
\infer[$\exists$I]
{\vctx\mid\pfctx \proves \prop[\term/\var] \\
\vctx \proves \wtt\term\type}
{\vctx\mid\pfctx \proves \exists \var: \type. \prop}
\and
\infer[$\exists$E]
{\vctx\mid\pfctx \proves \exists \var: \type.\; \prop \\
\vctx,\var : \type\mid\pfctx , \prop \proves \propB}
{\vctx\mid\pfctx \proves \propB}
\and
\infer[$\lambda$]
{}
{\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
\and
\infer[$\mu$]
{}
{\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
\end{mathparpagebreakable}
\begin{mathpar}
\begin{array}{rMcMl}
\TRUE * \prop &\provesIff& \prop \\
\prop * \propB &\provesIff& \propB * \prop \\
(\prop * \propB) * \propC &\provesIff& \prop * (\propB * \propC)
\end{array}
\and
{\prop_1 \proves \propB_1 \and
\prop_2 \proves \propB_2}
{\prop_1 * \prop_2 \proves \propB_1 * \propB_2}
\and
{\prop * \propB \proves \propC}
{\prop \proves \propB \wand \propC}
\end{mathpar}
\paragraph{Laws for ghosts and physical resources.}
\begin{mathpar}
\begin{array}{rMcMl}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff& \ownGGhost{\melt \mtimes \meltB} \\
\end{array}
\and
\begin{array}{c}
\ownPhys{\state} * \ownPhys{\state'} \proves \FALSE
\end{array}
\end{mathpar}
\begin{mathpar}
{\pfctx \proves \prop}
{\pfctx \proves \later{\prop}}
\and
\infer[L{\"o}b]
{}
{(\later\prop\Ra\prop) \proves \prop}
\and
\infer[$\later$-$\exists$]
{\text{$\type$ is inhabited}}
{\later{\Exists x:\type.\prop} \proves \Exists x:\type. \later\prop}
\\\\
\begin{array}[c]{rMcMl}
\later{(\prop \wedge \propB)} &\provesIff& \later{\prop} \wedge \later{\propB} \\
\later{(\prop \vee \propB)} &\provesIff& \later{\prop} \vee \later{\propB} \\
\end{array}
\and
\later{\All x.\prop} &\provesIff& \All x. \later\prop \\
\Exists x. \later\prop &\proves& \later{\Exists x.\prop} \\
\later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB
\end{array}
\end{mathpar}
\begin{mathpar}
\infer
{\text{$\term$ or $\term'$ is a discrete COFE element}}
{\timeless{\term =_\type \term'}}
\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\ownGGhost\melt}}
\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\mval(\melt)}}
\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \Ra \propB}}
\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \wand \propB}}
\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\All\var:\type.\prop}}
\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\Exists\var:\type.\prop}}
\end{mathpar}
\begin{mathpar}
{\always{\pfctx} \proves \prop}
{\always{\pfctx} \proves \always{\prop}}
\and
\and
\begin{array}[c]{rMcMl}
\always{(\prop * \propB)} &\proves& \always{(\prop \land \propB)} \\
\always{\prop} * \propB &\proves& \always{\prop} \land \propB \\
\always{\later\prop} &\provesIff& \later\always{\prop} \\
\end{array}
\and
\always{(\prop \land \propB)} &\provesIff& \always{\prop} \land \always{\propB} \\
\always{(\prop \lor \propB)} &\provesIff& \always{\prop} \lor \always{\propB} \\
\always{\All x. \prop} &\provesIff& \All x. \always{\prop} \\
\always{\Exists x. \prop} &\provesIff& \Exists x. \always{\prop} \\
\end{array}
{ \term =_\type \term' \proves \always \term =_\type \term'}
{ \knowInv\iname\prop \proves \always \knowInv\iname\prop}
{ \ownGGhost{\mcore\melt} \proves \always \ownGGhost{\mcore\melt}}
\end{mathpar}
\begin{mathpar}
\infer[pvs-intro]
{}{\prop \proves \pvs[\mask] \prop}
\infer[pvs-mono]
{\prop \proves \propB}
{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}
\infer[pvs-timeless]
{\timeless\prop}
{\later\prop \proves \pvs[\mask] \prop}
\infer[pvs-trans]
{\mask_2 \subseteq \mask_1 \cup \mask_3}
{\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}
\infer[pvs-mask-frame]
{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_f][\mask_2 \uplus \mask_f] \prop}
\infer[pvs-frame]
{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop}
{\text{$\mask$ is infinite}}
{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
{\melt \mupd \meltsB}
{\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB}
\end{mathpar}
{}{\prop[\val/\var] \proves \wpre{\val}[\mask]{\Ret\var.\prop}}
{\mask_1 \subseteq \mask_2 \and \var:\textlog{val}\mid\prop \proves \propB}
{\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
{}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
{}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
\infer[wp-atomic]
{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
{\pvs[\mask_1][\mask_2] \wpre\expr[\mask_2]{\Ret\var. \pvs[\mask_2][\mask_1]\prop}
\proves \wpre\expr[\mask_1]{\Ret\var.\prop}}
{}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
\infer[wp-frame-step]
{\toval(\expr) = \bot}
{\later\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
\infer[wp-bind]
{\text{$\lctx$ is a context}}
{\wpre\expr[\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\mask]{\Ret\varB.\prop}}
\paragraph{Lifting of operational semantics.}~
\begin{mathpar}
\infer[wp-lift-step]
{\mask_2 \subseteq \mask_1 \and
\toval(\expr_1) = \bot \and
\red(\expr_1, \state_1) \and
\All \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \pred(\expr_2,\state_2,\expr_f)}
{ {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
~~\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_f. \pred(\expr_2, \state_2, \expr_f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
\end{inbox}} }
\infer[wp-lift-pure-step]
{\toval(\expr_1) = \bot \and
\All \state_1. \red(\expr_1, \state_1) \and
\All \state_1, \expr_2, \state_2, \expr_f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_f)}
{\later\All \expr_2, \expr_f. \pred(\expr_2, \expr_f) \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
Here we define $\wpre{\expr_f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
\subsection{Adequacy}
The adequacy statement concerning functional correctness reads as follows:
&\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'.
\\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
\\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{[\val] \dplus \tpool'} \Ra
\\&\pred(\val)
\end{align*}
where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants.
Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets \emph{stuck}: Every expression in the thread pool either is a value, or can reduce further.
\begin{align*}
&\All \mask, \expr, \state, \melt, \state', \tpool'.
\\&(\All n. \melt \in \mval_n) \Ra
\\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
\\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{\tpool'} \Ra
\\&\All\expr'\in\tpool'. \toval(\expr) \neq \bot \lor \red(\expr, \state')
\end{align*}
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.
% RJ: If we want this section back, we should port it to primitive view shifts and prove it in Coq.
% \subsection{Unsound rules}
% Some rule suggestions (or rather, wishes) keep coming up, which are unsound. We collect them here.
% \begin{mathpar}
% \infer
% {P \vs Q}
% {\later P \vs \later Q}
% \and
% \infer
% {\later(P \vs Q)}
% {\later P \vs \later Q}
% \end{mathpar}
% Of course, the second rule implies the first, so let's focus on that.
% Since implications work under $\later$, from $\later P$ we can get $\later \pvs{Q}$.
% If we now try to prove $\pvs{\later Q}$, we will be unable to establish world satisfaction in the new world:
% We have no choice but to use $\later \pvs{Q}$ at one step index below what we are operating on (because we have it under a $\later$).
% We can easily get world satisfaction for that lower step-index (by downwards-closedness of step-indexed predicates).
% We can, however, not make much use of the world satisfaction that we get out, becaase it is one step-index too low.