Forked from
Iris / Iris
6928 commits behind the upstream repository.
logic.tex 23.59 KiB
\section{Language}
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{()})\]
We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$. \\
A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr'$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr'$ 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'. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr' \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}[Context]
A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
\begin{enumerate}
\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'. \expr_1, \state_1 \step \expr_2,\state_2,\expr' \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr' $
\item Reductions stay below $\lctx$ until there is a value in the hole:\\
$\All \expr_1', \state_1, \expr_2, \state_2, \expr'. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr' \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr' $
\end{enumerate}
\end{defn}
\subsection{The concurrent language}
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' \and \expr' \neq ()}
{\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
\cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr']}{\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}
\clearpage
\section{The logic}
To instantiate Iris, you need to define the following parameters:
\begin{itemize}
\item A language $\Lang$
\item A locally contractive functor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state
\ralf{$\iFunc$ also needs to have a single-unit.}
\end{itemize}
\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 \bnfdef{}&
\sigtype \mid
1 \mid
\type \times \type \mid
\type \to \type
\\[0.4em]
\term, \prop, \pred \bnfdef{}&
\var \mid
\sigfn(\term_1, \dots, \term_n) \mid
() \mid
(\term, \term) \mid
\pi_i\; \term \mid
\Lam \var:\type.\term \mid
\term(\term) \mid
\mcore\term \mid
\term \mtimes \term \mid
\\&
\FALSE \mid
\TRUE \mid
\term =_\type \term \mid
\prop \Ra \prop \mid
\prop \land \prop \mid
\prop \lor \prop \mid
\prop * \prop \mid
\prop \wand \prop \mid
\\&
\MU \var:\type. \pred \mid
\Exists \var:\type. \prop \mid
\All \var:\type. \prop \mid
\\&
\knowInv{\term}{\prop} \mid
\ownGGhost{\term} \mid
\ownPhys{\term} \mid
\always\prop \mid
{\later\prop} \mid
\pvs[\term][\term] \prop\mid
\wpre{\term}{\Ret\var.\term}[\term]
\end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, 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$.
\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}
\text{metavariable} & \text{type} \\\hline
\term, \termB & \text{arbitrary} \\
\val, \valB & \textlog{Val} \\
\expr & \textlog{Expr} \\
\state & \textlog{State} \\
\end{array}
\qquad\qquad
\begin{array}{r|l}
\text{metavariable} & \text{type} \\\hline
\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 often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}.
We omit type annotations in binders, when the type is clear from context.
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
\axiom{x : \type \proves \wtt{x}{\type}}
\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\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{\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}{\Ret\var.\term}[\mask]}{\Prop}
}
\end{mathparpagebreakable}
\subsection{Timeless propositions}
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 by the following judgment.
\judgment{Timeless Propositions}{\timeless{P}}
\ralf{Define a judgment that defines them.}
\subsection{Proof rules}
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 $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \Ra \propB$ with no assumptions.
(Bi-implications are analogous.)
\judgment{}{\vctx \mid \pfctx \proves \prop}
\paragraph{Laws of intuitionistic higher-order logic.}
This is entirely standard.
\begin{mathparpagebreakable}
\infer[Asm]
{\prop \in \pfctx}
{\pfctx \proves \prop}
\and
\infer[Eq]
{\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}
\paragraph{Laws of (affine) bunched implications.}
\begin{mathpar}
\begin{array}{rMcMl}
\TRUE * \prop &\Lra& \prop \\
\prop * \propB &\Lra& \propB * \prop \\
(\prop * \propB) * \propC &\Lra& \prop * (\propB * \propC)
\end{array}
\and
\infer[$*$-mono]
{\prop_1 \proves \propB_1 \and
\prop_2 \proves \propB_2}
{\prop_1 * \prop_2 \proves \propB_1 * \propB_2}
\and
\inferB[$\wand$I-E]
{\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} &\Lra& \ownGGhost{\melt \mtimes \meltB} \\
%\TRUE &\Ra& \ownGGhost{\munit}\\
\ownGGhost{\melt} &\Ra& \melt \in \mval % * \ownGGhost{\melt}\end{array}
\and
\begin{array}{c}
\ownPhys{\state} * \ownPhys{\state'} \Ra \FALSE
\end{array}
\end{mathpar}
\paragraph{Laws for the later modality.}
\begin{mathpar}
\infer[$\later$-mono]
{\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)} &\Lra& \later{\prop} \wedge \later{\propB} \\
\later{(\prop \vee \propB)} &\Lra& \later{\prop} \vee \later{\propB} \\
\end{array}
\and
\begin{array}[c]{rMcMl}
\later{\All x.\prop} &\Lra& \All x. \later\prop \\
\Exists x. \later\prop &\Ra& \later{\Exists x.\prop} \\
\later{(\prop * \propB)} &\Lra& \later\prop * \later\propB
\end{array}
\end{mathpar}
\paragraph{Laws for the always modality.}
\begin{mathpar}
\infer[$\always$I]
{\always{\pfctx} \proves \prop}
{\always{\pfctx} \proves \always{\prop}}
\and
\infer[$\always$E]{}
{\always{\prop} \Ra \prop}
\and
\begin{array}[c]{rMcMl}
\always{(\prop * \propB)} &\Ra& \always{(\prop \land \propB)} \\
\always{\prop} * \propB &\Ra& \always{\prop} \land \propB \\
\always{\later\prop} &\Lra& \later\always{\prop} \\
\end{array}
\and
\begin{array}[c]{rMcMl}
\always{(\prop \land \propB)} &\Lra& \always{\prop} \land \always{\propB} \\
\always{(\prop \lor \propB)} &\Lra& \always{\prop} \lor \always{\propB} \\
\always{\All x. \prop} &\Lra& \All x. \always{\prop} \\
\always{\Exists x. \prop} &\Lra& \Exists x. \always{\prop} \\
\end{array}
\and
{ \term =_\type \term' \Ra \always \term =_\type \term'}
\and
{ \knowInv\iname\prop \Ra \always \knowInv\iname\prop}
\and
{ \ownGGhost{\mcore\melt} \Ra \always \ownGGhost{\mcore\melt}}
\end{mathpar}
\paragraph{Laws of primitive view shifts.}
\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}
\infer[pvs-allocI]
{\text{$\mask$ is infinite}}
{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
\infer[pvs-openI]
{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
\infer[pvs-closeI]
{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
\infer[pvs-update]
{\melt \mupd \meltsB}
{\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB}
\end{mathpar}
\paragraph{Laws of weakest preconditions.}
\begin{mathpar}
\infer[wp-value]
{}{\prop[\val/\var] \proves \wpre{\val}{\Ret\var.\prop}[\mask]}
\infer[wp-mono]
{\mask_1 \subseteq \mask_2 \and \var:\textlog{val}\mid\prop \proves \propB}
{\wpre\expr{\Ret\var.\prop}[\mask_1] \proves \wpre\expr{\Ret\var.\propB}[\mask_2]}
\infer[pvs-wp]
{}{\pvs[\mask] \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\prop}[\mask]}
\infer[wp-pvs]
{}{\wpre\expr{\Ret\var.\pvs[\mask] \prop}[\mask] \proves \wpre\expr{\Ret\var.\prop}[\mask]}
\infer[wp-atomic]
{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
{\pvs[\mask_1][\mask_2] \wpre\expr{\Ret\var. \pvs[\mask_2][\mask_1]\prop}[\mask_2]
\proves \wpre\expr{\Ret\var.\prop}[\mask_1]}
\infer[wp-frame]
{}{\propB * \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\propB*\prop}[\mask]}
\infer[wp-frame-step]
{\toval(\expr) = \bot}
{\later\propB * \wpre\expr{\Ret\var.\prop}[\mask] \proves \wpre\expr{\Ret\var.\propB*\prop}[\mask]}
\infer[wp-bind]
{\text{$\lctx$ is a context}}
{\wpre\expr{\Ret\var. \wpre{\lctx(\ofval(\var))}{\Ret\varB.\prop}[\mask]}[\mask] \proves \wpre{\lctx(\expr)}{\Ret\varB.\prop}[\mask]}
\end{mathpar}
\subsection{Lifting of operational semantics}\label{sec:lifting}
~\\\ralf{Add this.}
% The following lemmas help in proving axioms for a particular language.
% The first applies to expressions with side-effects, and the second to side-effect-free expressions.
% \dave{Update the others, and the example, wrt the new treatment of $\predB$.}
% \begin{align*}
% &\All \expr, \state, \pred, \prop, \propB, \mask. \\% &\textlog{reducible}(e) \implies \\
% &(\All \expr', \state'. \cfg{\state}{\expr} \step \cfg{\state'}{\expr'} \implies \pred(\expr', \state')) \implies \\
% &{} \proves \bigl( (\All \expr', \state'. \pred (\expr', \state') \Ra \hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask]) \Ra \hoare{ \later \prop * \ownPhys{\state} }{\expr}{\Ret\val. \propB}[\mask] \bigr) \\
% \quad\\
% &\All \expr, \pred, \prop, \propB, \mask. \\
% &\textlog{reducible}(e) \implies \\
% &(\All \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \state_2 = \state \land \pred(\expr_2)) \implies \\
% &{} \proves \bigl( (\All \expr'. \pred(\expr') \Ra \hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask]) \Ra \hoare{\later\prop}{\expr}{\Ret\val. \propB}[\mask] \bigr)
% \end{align*}
% Note that $\pred$ is a meta-logic predicate---it does not depend on any world or resources being owned.
% The following specializations cover all cases of a heap-manipulating lambda calculus like $F_{\mu!}$.
% \begin{align*}
% &\All \expr, \expr', \prop, \propB, \mask. \\
% &\textlog{reducible}(e) \implies \\
% &(\All \state, \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \state_2 = \state \land \expr_2 = \expr') \implies \\
% &{} \proves (\hoare{\prop}{\expr'}{\Ret\val. \propB}[\mask] \Ra \hoare{\later\prop}{\expr}{\Ret\val. \propB}[\mask] ) \\
% \quad \\
% &\All \expr, \state, \pred, \mask. \\
% &\textlog{atomic}(e) \implies \\
% &\bigl(\All \expr_2, \state_2. \cfg{\state}{\expr} \step \cfg{\state_2}{\expr_2} \implies \pred(\expr_2, \state_2)\bigr) \implies \\
% &{} \proves (\hoare{ \ownPhys{\state} }{\expr}{\Ret\val. \Exists\state'. \ownPhys{\state'} \land \pred(\val, \state') }[\mask] )
% \end{align*}
% The first is restricted to deterministic pure reductions, like $\beta$-reduction.
% The second is suited to proving triples for (possibly non-deterministic) atomic expressions; for example, with $\expr \eqdef \;!\ell$ (dereferencing $\ell$) and $\state \eqdef h \mtimes \ell \mapsto \valB$ and $\pred(\val, \state') \eqdef \state' = (h \mtimes \ell \mapsto \valB) \land \val = \valB$, one obtains the axiom $\All h, \ell, \valB. \hoare{\ownPhys{h \mtimes \ell \mapsto \valB}}{!\ell}{\Ret\val. \val = \valB \land \ownPhys{h \mtimes \ell \mapsto \valB} }$.
% %Axioms for CAS-like operations can be obtained by first deriving rules for the two possible cases, and then using the disjunction rule.
\subsection{Adequacy}
The adequacy statement reads as follows:
\begin{align*}
&\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'.
\\&(\All n. \melt \in \mval_n) \Ra
\\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}{x.\; \pred(x)}[\mask]) \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.
% 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.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: