\let\bar\overline

\section{Language}
\label{sec: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 (\cup_n \textdom{Expr}^n)\]
  A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off.
  We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$, \ie when no threads are forked off. \\
\item All values are stuck:
\[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
\end{itemize}

\begin{defn}
  An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
  \[ \Exists \expr_2, \state_2, \bar\expr. \expr,\state \step \expr_2,\state_2,\bar\expr \]
\end{defn}

\begin{defn}
  An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value:
  \[ \All\state_1, \expr_2, \state_2, \bar\expr. \expr, \state_1 \step \expr_2, \state_2, \bar\expr \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
\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, \bar\expr. \expr_1, \state_1 \step \expr_2,\state_2,\bar\expr \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\bar\expr $
  \item Reductions stay below $\lctx$ until there is a value in the hole:\\
    $\All \expr_1', \state_1, \expr_2, \state_2, \bar\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\bar\expr \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\bar\expr $
  \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{Expr}^n
\]

\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
  \cfg{\tpool'}{\state'}}
\begin{mathpar}
\infer
  {\expr_1, \state_1 \step \expr_2, \state_2, \bar\expr}
  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
     \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \bar\expr}{\state_2}}
\end{mathpar}

\clearpage
\section{Program Logic}
\label{sec:program-logic}

This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the logic described in \Sref{sec:hogs}.
So in the following, we assume that some language $\Lang$ was fixed.

\subsection{World Satisfaction, Invariants, View Shifts}

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.

We assume to have the following four CMRAs available:
\begin{align*}
  \textmon{State} \eqdef{}& \authm(\exm(\textdom{State})) \\
  \textmon{Inv} \eqdef{}& \authm(\mathbb N \fpfn \agm(\latert \iPreProp)) \\
  \textmon{En} \eqdef{}& \pset{\mathbb N} \\
  \textmon{Dis} \eqdef{}& \finpset{\mathbb N}
\end{align*}
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine.

Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created.
(We will discuss later how this assumption is discharged.)

\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
  W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull \aginj(\latertinj(\wIso(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{align*}

\paragraph{Invariants.}
The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$:
\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}{\authfrag \aginj(\latertinj(\wIso(\prop)))} \]

\paragraph{View Shifts.}
Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop \]

We further define the notions of \emph{view shifts} and \emph{linear view shifts}:
\begin{align*}
  \prop \vs[\mask_1][\mask_2] \propB \eqdef{}& \always(\prop \Ra \pvs[\mask_1][\mask_2] \propB) \\
  \prop \vsW[\mask_1][\mask_2] \propB \eqdef{}& \prop \wand \pvs[\mask_1][\mask_2] \propB
\end{align*}

\ralf{Show some proof rules.}

\subsection{Hoare Triples}

Finally, we can define the core piece of the program logic, the assertion that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived.
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$).

\begin{align*}
  \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) \eqdef{}&
    (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \prop) \lor {}\\
        &\Bigl(\toval(\expr) = \bot \land \All \state. \ownGhost{\gname_{\textmon{State}}}{\authfull \state} \vsW[\mask][\emptyset] {}\\
        &\qquad \red(\expr, \state) * \later\All \expr', \state', \bar\expr. (\expr, \state \step \expr', \state', \bar\expr) \vsW[\emptyset][\mask] {}\\
        &\qquad\qquad \ownGhost{\gname_{\textmon{State}}}{\authfull \state'} * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \bar\expr} \textdom{wp}(\mathbb N, \expr'', \Lam \any. \TRUE)\Bigr) \\
%  (* value case *)
  \wpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& (\MU \textdom{wp}. \textdom{pre-wp}(\textdom{wp}))(\mask, \expr, \Lam\val.\prop)
\end{align*}

This ties the authoritative part of \textmon{State} to the actual physical state of the reduction witnessed by the weakest precondition.
The fragment will then be available to the user of the logic, as their way of talking about the physical state:
\[ \ownPhys\state \eqdef \ownGhost{\gname_{\textmon{State}}}{\authfrag \state} \]

It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs on paper.
Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
\[
\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\lambda\Ret\val.\propB})}
\]

\subsection{Lost stuff}
\ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}


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$.
%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.

Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertion 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}
\]

\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{\ownM\melt}}

\infer
{\text{$\melt$ is an element of a discrete CMRA}}
{\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}

\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}
{\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\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 \and \mask_2 \subseteq \mask_1}
{\wpre\expr[\mask]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask \uplus \mask_1]{\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}
  { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
        ~~\pvs[\mask_1][\mask_2] \Exists \state_1. \red(\expr_1,\state_1) \land \later\ownPhys{\state_1} * {}\\\qquad\qquad\qquad \later\All \expr_2, \state_2, \expr_\f. \left( (\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f) \land \ownPhys{\state_2} \right) \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 }
  {\later\All \state, \expr_2, \expr_\f. (\expr_1,\state \step \expr_2, \state,\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}
Notice that primitive view shifts cover everything to their right, \ie $\pvs \prop * \propB \eqdef \pvs (\prop * \propB)$.

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).

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 * \ownM\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 * \ownM\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.

\subsection{Iris model}

\paragraph{Semantic domain of assertions.}



\paragraph{Interpretation of assertions.}
$\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply.
We only have to define the interpretation of the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.

\typedsection{World satisfaction}{\wsat{-}{-}{-} : 
	\Delta\textdom{State} \times
	\Delta\pset{\mathbb{N}} \times
	\textdom{Res} \nfn \SProp }
\begin{align*}
  \wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t]
    \rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land 
    \dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\
    \All\iname \in \mask, \prop \in \iProp. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
  \end{inbox}\\
	\wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))}
\end{align*}

\typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}
\begin{align*}
	\mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}
            \All \rs_\f, k, \mask_\f, \state.& 0 < k \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
            \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f}
          \end{aligned}}
\end{align*}

\typedsection{Weakest precondition}{\mathit{wp}_{-}(-, -) : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp}

$\textdom{wp}$ is defined as the fixed-point of a contractive function.
\begin{align*}
  \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned}
        \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \disj \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
        &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \pred(\val)(\rsB) \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f}) \land {}\\
        &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\
        &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rsB_1 \mtimes \rsB_2 \mtimes \rs_\f} \land  m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
        &\qquad\qquad (\expr_\f = \bot \lor m \in \textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2))
    \end{aligned}} \\
  \textdom{wp}_\mask(\expr, \pred) &\eqdef \mathit{fix}(\textdom{pre-wp})(\mask, \expr, \pred)
\end{align*}



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