\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{\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 \]
\end{defn}

\begin{defn}[Context]
  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 $
  \end{enumerate}
\end{defn}

\subsection{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_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}

\clearpage
\section{Logic}

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
\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
      \munit \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. \term  \mid
    \Exists \var:\type. \prop \mid
    \All \var:\type. \prop \mid
\\&
    \knowInv{\term}{\prop} \mid
    \ownGGhost{\term} \mid \mval(\term) \mid
    \ownPhys{\term} \mid
    \always\prop \mid
    {\later\prop} \mid
    \pvs[\term][\term] \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}
 \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 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\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}

\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 $\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
\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 &\provesIff& \prop \\
  \prop * \propB &\provesIff& \propB * \prop \\
  (\prop * \propB) * \propC &\provesIff& \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} &\provesIff&  \ownGGhost{\melt \mtimes \meltB} \\
\ownGGhost{\melt} &\provesIff& \mval(\melt) \\
\TRUE &\proves&  \ownGGhost{\munit}
\end{array}
\and
\and
\begin{array}{c}
\ownPhys{\state} * \ownPhys{\state'} \proves \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)} &\provesIff& \later{\prop} \wedge \later{\propB}  \\
  \later{(\prop \vee \propB)} &\provesIff& \later{\prop} \vee \later{\propB} \\
\end{array}
\and
\begin{array}[c]{rMcMl}
  \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{}
{\timeless{\ownPhys\state}}

\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}


\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} \proves \prop}
\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
\begin{array}[c]{rMcMl}
  \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}
\and
{ \term =_\type \term' \proves \always \term =_\type \term'}
\and
{ \knowInv\iname\prop \proves \always \knowInv\iname\prop}
\and
{ \ownGGhost{\mcore\melt} \proves \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}

\inferH{pvs-allocI}
{\text{$\mask$ is infinite}}
{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}

\inferH{pvs-openI}
{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}

\inferH{pvs-closeI}
{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}

\inferH{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}[\mask]{\Ret\var.\prop}}

\infer[wp-mono]
{\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}}

\infer[pvs-wp]
{}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}

\infer[wp-pvs]
{}{\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}}

\infer[wp-frame]
{}{\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}}
\end{mathpar}

\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}}
\end{mathpar}

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:
\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}[\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.




%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: