\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 base logic.
So in the following, we assume that some language $\Lang$ was fixed.
Furthermore, we work in the logic with higher-order ghost state as described in \Sref{sec:composable-resources}.

\subsection{Later Credits}
Introducing a later modality is easy (see~\ruleref{later-intro}), but eliminating them can be tricky.
Laters often appear in the middle of our proofs after unfolding a circular construction (\eg by opening an invariant, see~\secref{sec:invariants}).
In these cases, we get to assume $\later \prop$, but we really want $\prop$ to continue in the proof.
Iris offers us four options to do so.
We have seen two of them already: timeless propositions (see~\secref{sec:timeless-props}) and the commuting rules for later.
Together, they can be used to turn $\later \prop$ into $\prop$, or to delay when we have to deal with the later modality by commuting it inward (\eg{} over an existential quantifer and a separating conjunction).
Another option, which we will encounter in~\secref{sec:weakest-pre}, is taking program steps: every program step allows us to eliminate (at least) one later (see~\ruleref{wp-lift-step}).
We now introduce the fourth option: \emph{later credits}.
Later credits turn the right to eliminate a later into an ownable separation-logic resource $\laterCredit{n}$, where $n$ is the number of laters that we can eliminate.

\paragraph{Resources}
We assume that the camera
\[ \textdom{LaterCredits} \eqdef{} \authm{(\nat^{+})} \]
is available (\ie{} part of $\Sigma$), where $\nat^{+}$ is the RA derived from the monoid $\nat$ with operation $+$, and that an instance of it has been created and made globally available at the beginning of verification under the name $\gname_{\textdom{Credits}}$.
We define the following notations for the fragments and authoritative part:
\begin{mathpar}
  \laterCredit{n} \eqdef{} \ownGhost{\gname_{\textdom{Credits}}}{\authfrag{n}}

  \laterCreditSupply{n} \eqdef{} \ownGhost{\gname_{\textdom{Credits}}}{\authfull{n}}
\end{mathpar}

This definition satisfies the following laws:
\begin{mathpar}
  \inferH{Credit-Split}{}{\laterCredit{(n + m)} \Leftrightarrow \laterCredit{n} * \laterCredit{m}}

  \inferH{Credit-Timeless}{}{\timeless{\laterCredit{n}}}\\

  \inferH{Credit-SupplyBound}{}{\laterCreditSupply{m} * \laterCredit{n} \proves m \geq n}

  \inferH{Credit-SupplyDecr}{}{\laterCreditSupply{(n + m)} * \laterCredit{n} \proves \pvs \laterCreditSupply{m}}

  \inferH{Credit-SupplyExcl}{}{\laterCreditSupply{m_1} * \laterCreditSupply{m_2} \proves \FALSE}
\end{mathpar}

\paragraph{Later Elimination Update}%
\label{sec:later-credits}
To eliminate laters by \emph{spending} later credits $\laterCredit{n}$, we define a \emph{later-elimination update} $\creditUpd{}\prop$ on top of the basic update modality.
It satisfies all the properties of basic updates, except for \ruleref{upd-plainly}, but with the additional rule
\begin{mathpar}
  \inferH{credit-upd-use}
  {}
  {\later \prop * \laterCredit{1} \proves \creditUpd{} \prop}
\end{mathpar}
\ruleref{credit-upd-use} allows to \emph{spend} one credit in exchange for stripping one later off of $\prop$.

The later-elimination update is defined by guarded recursion:
\begin{align*}
  \creditUpd{}&\eqdef \MU~\mathit{upd}. \Lam \prop. \All n. \laterCreditSupply{n} \wand \upd{} (\laterCreditSupply{n} * \prop) \lor (\Exists m < n. \laterCreditSupply{m} * \later \mathit{upd}(\prop))
\end{align*}
It threads through the authoritative resource $\laterCreditSupply{n}$, the credit supply, to control how many credits can be spent in total.
The basic update ensures that the later elimination update inherits the ability to update resources.
In the first disjunct (the \enquote{base case}), no credits are spent.
In the second disjunct (the \enquote{recursive case}), a later can be eliminated before going into recursion.
To take the second disjunct, the credit supply $\laterCreditSupply{n}$ has to be decreased, which means giving up at least $\laterCredit{1}$.

The later-elimination update satisfies the following laws:
\begin{mathpar}
  \inferH{credit-upd-mono}
  {\prop \proves \propB}
  {\creditUpd\prop \proves \creditUpd\propB}

  \inferH{credit-upd-intro}
  {}{\prop \proves \creditUpd \prop}

  \inferH{credit-upd-trans}
  {}
  {\creditUpd \creditUpd \prop \proves \creditUpd \prop}

  \inferH{credit-upd-frame}
  {}{\propB * \creditUpd\prop \proves \creditUpd (\propB * \prop)}

  \inferH{credit-upd-update}
  %{}
  %{\upd\creditUpd{} \prop \proves \creditUpd{} \prop}
  {\melt \mupd \meltsB}
  {\ownM\melt \proves \creditUpd \Exists\meltB\in\meltsB. \ownM\meltB}

  \inferH{credit-upd-later}
  {}
  {\laterCredit{1} * \later \creditUpd{} \prop \proves \creditUpd{} \prop}
  %\inferH{credit-upd-use}
  %{}
  %{\later \prop * \laterCredit{1} \proves \creditUpd{} \prop}
\end{mathpar}
The rule \ruleref{credit-upd-use} shown above can be derived from \ruleref{credit-upd-later} and \ruleref{credit-upd-intro}.

Note the absence of a rule corresponding to \ruleref{upd-plainly}, which is not validated by the model.
As some existing Iris developments rely on \ruleref{upd-plainly}, we parameterize the logic by a boolean constant $\LaterCreditsFlag$ that determines whether the later-elimination update is used instead of the basic update, in particular in the definition of fancy updates below.

\subsection{World Satisfaction, Invariants, Fancy Updates}
\label{sec:invariants}

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 cameras available:
\begin{align*}
  \InvName \eqdef{}& \nat \\
  \textdom{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
  \textdom{En} \eqdef{}& \pset{\InvName} \\
  \textdom{Dis} \eqdef{}& \finpset{\InvName}
\end{align*}
The last two are the tokens used for managing invariants, $\textdom{Inv}$ is the monoid used to manage the invariants themselves.

We assume that at the beginning of the verification, instances named $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.

\paragraph{World Satisfaction.}
We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
  W \eqdef{}& \Exists I : \InvName \fpfn \Prop.
  \begin{array}[t]{@{} l}
    \ownGhost{\gname_{\textdom{Inv}}}{\authfull
      \mapComp {\iname}
        {\aginj(\latertinj(\wIso(I(\iname))))}
        {\iname \in \dom(I)}} * \\
    \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textdom{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textdom{En}}}{\set{\iname}} \right)
  \end{array}
\end{align*}

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

\paragraph{Fancy Updates and View Shifts.}
Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$) or later-elimination updates (\Sref{sec:later-credits}), except that they also have access to world satisfaction and can enable and disable invariants.

Depending on how the logic is parameterized with the $\LaterCreditsFlag$, fancy updates are defined on top the basic update or the later-elimination update.
This influences which rules fancy updates satisfy: either fancy updates can be used to eliminate later credits, or they satisfy certain interaction laws with the plainly modality.

\[ \pvs[\mask_1][\mask_2] \prop \eqdef
  \begin{cases}
    W * \ownGhost{\gname_{\textdom{En}}}{\mask_1} \wand \creditUpd\diamond (W * \ownGhost{\gname_{\textdom{En}}}{\mask_2} * \prop) & \text{if } \LaterCreditsFlag = \textsf{true}\\
    W * \ownGhost{\gname_{\textdom{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textdom{En}}}{\mask_2} * \prop) & \text{if } \LaterCreditsFlag = \textsf{false}\\
  \end{cases}
  \]
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.
Masks are sets of natural numbers, \ie they are subsets of $\mathbb{N}$.%
\footnote{Actually, in the Coq development masks are restricted to a class of sets of natural numbers that contains all finite sets and is closed under union, intersection, difference and complement.
The restriction is necessary for engineering reasons to still obtain representation independence: two masks should be \emph{propositionally} equal iff they contain the same invariant names.}
We use $\top$ as symbol for the largest possible mask, $\nat$, and $\bot$ for the smallest possible mask $\emptyset$.
We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
%
Fancy updates satisfy the following basic proof rules:
\begin{mathparpagebreakable}
\infer[fup-mono]
{\prop \proves \propB}
{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}

\infer[fup-intro-mask]
{\mask_2 \subseteq \mask_1}
{\prop \proves \pvs[\mask_1][\mask_2]\pvs[\mask_2][\mask_1] \prop}

\infer[fup-trans]
{}
{\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}

\infer[fup-upd]
{}{\upd\prop \proves \pvs[\mask] \prop}

\infer[fup-frame]
{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \propB * \prop}

\inferH{fup-update}
{\melt \mupd \meltsB}
{\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB}

\infer[fup-timeless]
{\timeless\prop}
{\later\prop \proves \pvs[\mask] \prop}

\infer[fup-credit-use]
{\LaterCreditsFlag = \textsf{true}}
{\laterCredit{1} * \later \pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \prop}
\end{mathparpagebreakable}
(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.)

We can further define the notions of \emph{view shifts} and \emph{linear view shifts}:
\begin{align*}
  \prop \vsW[\mask_1][\mask_2] \propB \eqdef{}& \prop \wand \pvs[\mask_1][\mask_2] \propB \\
  \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
\end{align*}
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.
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}
  {\ownGhost\gname{\melt} \vs[\emptyset] \exists \meltB \in \meltsB.\; \ownGhost\gname{\meltB}}
\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}}
  {\later \prop \vs[\emptyset] \prop}
\and
\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}

\subsection{Weakest Precondition}
\label{sec:weakest-pre}

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.

\paragraph{Defining weakest precondition.}
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$).
We further assume (as a parameter) a predicate $\stateinterp : \State \times \mathbb N \times \List(\Obs) \times \mathbb N \to \iProp$ that interprets the machine state as an Iris proposition, a predicate $\pred_F: \Val \to \iProp$ that serves as postcondition for forked-off threads, and a function $n_\rhd: \mathbb N \to \mathbb N$ specifying the number of additional laters and later credits used for each physical step.
The state interpretation can depend on the current physical state, the number of steps since the beginning of the execution, 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).
It should be monotone with respect to the step counter: $\stateinterp(\state, n_s, \vec\obs, n_t) \vs[\emptyset] \stateinterp(\state, n_s + 1, \vec\obs, n_t)$.
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.
Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck, \MaybeStuck}$ indicating whether program execution is allowed to get stuck.

\begin{align*}
  \textdom{wp}(\stateinterp, \pred_F, \stuckness) \eqdef{}& \MU \textdom{wp\any rec}. \Lam \mask, \expr, \pred. \\
        & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
        & \Bigl(\toval(\expr) = \bot \land \All \state, n_s, \vec\obs, \vec\obs', n_t. \stateinterp(\state, n_s, \vec\obs \dplus \vec\obs', n_t) \vsW[\mask][\emptyset] {}\\
        &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step[\vec\obs] \expr', \state', \vec\expr) \wand \laterCredit{(n_\rhd(n_s)+1)} \wand {}\\
        &\qquad\qquad (\pvs[\emptyset]\later\pvs[\emptyset])^{n_\rhd(n_s)+1} \pvs[\emptyset][\mask]\stateinterp(\state', n_s + 1, \vec\obs', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * {}\\
        &\qquad\qquad\qquad \Sep_{\expr'' \in \vec\expr} \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
  \wpre[\stateinterp;\pred_F]\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\stateinterp,\pred_F,\stuckness)(\mask, \expr, \Lam\val.\prop)
\end{align*}
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.
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$.

\paragraph{Laws of weakest precondition.}
The following rules can all be derived:
\begin{mathpar}
\infer[wp-value]
{}{\prop[\val/\var] \proves \wpre{\val}[\stuckness;\mask]{\Ret\var.\prop}}

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

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

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

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

\infer[wp-frame]
{}{\propB * \wpre\expr[\stuckness;\mask]{\Ret\var.\prop} \proves \wpre\expr[\stuckness;\mask]{\Ret\var.\propB*\prop}}

\infer[wp-frame-step]
{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
{\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}}

\infer[wp-frame-n-steps]
{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
{{ {\begin{inbox}
~~(\All \state, n_s, \vec\obs, n_t. \stateinterp(\state, n_s, \vec\obs, n_t) \vsW[\mask_1, \emptyset] n \leq n_\rhd(n_s) + 1) \land {}\\
~~\wpre\expr[\stuckness;\mask_2]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2](\later\pvs[\emptyset])^n\pvs[\mask_2][\mask_1]\propB {}\\
\proves \wpre\expr[\stuckness;\mask_1]{\Ret\var.\propB*\prop}
\end{inbox}} }}

\infer[wp-bind]
{\text{$\lctx$ is a context}}
{\wpre\expr[\stuckness;\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\stuckness;\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\stuckness;\mask]{\Ret\varB.\prop}}
\end{mathpar}

We will also want a rule that connect weakest preconditions to the operational semantics of the language.
This basically just copies the second branch (the non-value case) of the definition of weakest preconditions.

\begin{mathpar}
  \inferH{wp-lift-step}
  {\toval(\expr_1) = \bot}
  { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
        ~~\All \state_1,\vec\obs,\vec\obs',n. \stateinterp(\state_1,n_s,\vec\obs \dplus \vec\obs', n_t) \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) \wand \laterCredit{(n_\rhd(n_s) + 1)} \wand (\pvs[\emptyset]\later\pvs[\emptyset])^{n_\rhd(n_s)}\pvs[\emptyset][\mask] {}\\
        \qquad\qquad\left(\stateinterp(\state_2,n_s+1,\vec\obs',n_t+|\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}\right)  {}\\
        \proves \wpre[\stateinterp\pred_F]{\expr_1}[\stuckness;\mask]{\Ret\var.\prop}
      \end{inbox}} }
\end{mathpar}

\paragraph{Adequacy of weakest precondition.}

\newcommand\metaprop{p}
\newcommand\consstate{C}

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.
The most general form of the adequacy statement is about proving properties of an arbitrary program execution.

\begin{thm}[Adequacy]
  Assume we are given some $\vec\expr_1$, $\state_1$, $\vec\obs$, $\tpool_2$, $\state_2$ such that $(\vec\expr_1, \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$.
  Moreover, assume we are given a stuckness parameter $\stuckness$ and \emph{meta-level} property $\metaprop$ that we want to show.
  To verify that $\metaprop$ holds, it is sufficient to show the following Iris entailment:
\begin{align*}
 &\TRUE \proves \pvs[\top] \Exists \stateinterp, \vec\pred, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \left(\Sep_{\expr,\pred \in \vec\expr_1,\vec\pred} \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\top]{x.\; \pred(x)}\right) * \left(\consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \hat{\metaprop}\right)
\end{align*}
where $\consstate$ describes states that are consistent with the state interpretation and postconditions:
\begin{align*}
 \consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2) \eqdef{}&\Exists \vec\expr_2, \tpool_2'. \tpool_2 = \vec\expr_2 \dplus \tpool_2' * {}\\
 &\quad |\vec\expr_1| = |\vec\expr_2| *{}\\
 &\quad (s = \NotStuck \Ra \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2) ) *{}\\
 &\quad \stateinterp(\state_2, (), |\tpool_2'|) *{}\\
 &\quad \left(\Sep_{\expr,\pred \in \vec\expr_2,\vec\pred} \toval(\expr) \ne \bot \wand \pred(\toval(\expr))\right) *{}\\
 &\quad \left(\Sep_{\expr \in \tpool_2'} \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))\right)
\end{align*}
The $\hat\metaprop$ here arises because we need a way to talk about $\metaprop$ inside Iris.
To this end, we assume that the signature $\Sig$ contains some assertion $\hat{\metaprop}$:
\[ \hat{\metaprop} : \Prop \in \SigFn \]
Furthermore, we assume that the \emph{interpretation} $\Sem{\hat{\metaprop}}$ of $\hat{\metaprop}$ reflects $\metaprop$ (also see \Sref{sec:model}):
\[\begin{array}{rMcMl}
  \Sem{\hat{\metaprop}} &:& \Sem\Prop \\
  \Sem{\hat{\metaprop}} &\eqdef& \Lam \any. \setComp{n}{\metaprop}
\end{array}\]
The signature can of course state arbitrary additional properties of $\hat{\metaprop}$, as long as they are proven sound.
\end{thm}

In other words, to show that $\metaprop$ holds, we have to prove an entailment in Iris that, starting from the empty context, chooses some state interpretation, postconditions for the initial threads, forked-thread postcondition and stuckness and then proves:
\begin{itemize}
  \item the initial state interpretation,
  \item a weakest-precondition,
  \item and a view shift showing the desired $\hat\metaprop$ under the extra assumption $\consstate(\tpool_2, \state_2)$.
\end{itemize}
Notice that the state interpretation and the postconditions are chosen \emph{after} doing a fancy update, which allows them to depend on the names of ghost variables that are picked in that initial fancy update.
This gives us a chance to allocate some ``global'' ghost state that state interpretation and postcondition can refer to (\eg the name $\gname_{\textdom{Credits}}$).

$\consstate^{\stateinterp;\vec\pred;\pred_F}_{\stuckness}(\tpool_2, \state_2)$ says that:
\begin{itemize}
\item The final thread-pool $\tpool_2$ contains the final state of the initial threads $\vec\expr_2$, and any number of additional forked threads in $\tpool_2'$.
\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_2$.
\item The state interpretation $\stateinterp$ holds for the final state.
\item If one of the initial threads reduced to a value, the corresponding post-condition $\pred \in \vec\pred$ 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}

~\par

As an example for how to use this adequacy theorem, let us say we wanted to prove that a program $\expr_1$ for which we derived a $\NotStuck$ weakest-precondition cannot get stuck:
\begin{cor}[Stuck-freedom]
  Assume we are given some $\expr_1$ such that the following holds:
\[
\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\NotStuck;\top]{x.\; \pred(x)}
\]
  Then it is the case that:
\[
\All \state_1, \vec\obs, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2) \Ra \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2)
\]
\end{cor}
To prove the conclusion of this corollary, we assume some $\state_1, \vec\obs, \tpool_2, \state_2$ and $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we instantiate the main theorem with this execution and $\metaprop \eqdef \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2)$.
We can then show the premise of adequacy using the Iris entailment that we assumed in the corollary and:
\[ \TRUE \proves \consstate^{\stateinterp;[\pred];\pred_F}_{\NotStuck}(\tpool_2, \state_2) \vs[\top][\emptyset] \metaprop \]
This proof, just like the following, also exploits that we can freely swap between meta-level universal quantification ($\All x. \TRUE \proves \prop$) and quantification in Iris ($\TRUE \proves \All x. \prop$).

~\par

Similarly we could show that the postcondition makes adequate statements about the possible final value of the main thread:
\begin{cor}[Adequate postcondition]
  Assume we are given some $\expr_1$ and a set $V \subseteq \Val$ such that the following holds (assuming we can talk about sets like $V$ inside the logic):
\[
\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{x.\; x \in V}
\]
  Then it is the case that:
\[
\All \state_1, \vec\obs, \val_2, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] ([\ofval(\val_2)] \dplus \tpool_2, \state_2) \Ra \val_2 \in V
\]
\end{cor}
To show this, we assume some $\state_1, \vec\obs, \val_2, \tpool_2, \state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] ([\ofval(\val_2)] \dplus \tpool_2, \state_2)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \val_2 \in \Val$.
Then we only have to show:
$$\TRUE \proves \consstate^{\stateinterp;[(\Lam \val. \val \in \Val)];\pred_F}_{\stuckness}([\ofval(\val_2)] \dplus \tpool_2, \state_2) \vs[\top][\emptyset] \val_2 \in \Val $$

~\par

As a final example, we could use adequacy to show that the state $\state$ of the program is always in some set $\Sigma \subseteq \State$:
\begin{cor}[Adequate state interpretation]
  Assume we are given some $\expr_1$ and a set $\Sigma \subseteq \State$ such that the following holds (assuming we can talk about sets like $\Sigma$ inside the logic):
\[
\TRUE \proves \All\state_1, \vec\obs. \pvs[\top] \Exists \stateinterp, \pred, \pred_F. \stateinterp(\state_1,0,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr_1}[\stuckness;\top]{\pred} * (\All \state_2, n_s, n_t. \stateinterp(\state_2,n_s,(),n_t) \!\vs[\top][\emptyset] \state_2 \in \Sigma)
\]
  Then it is the case that:
\[
\All \state_1, \vec\obs, \tpool_2, \state_2. ([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2) \Ra \state_2 \in \Sigma
\]
\end{cor}
To show this, we assume some $\state_1, \vec\obs, \tpool_2, \state_2$ such that $([\expr_1], \state_1) \tpsteps[\vec\obs] (\tpool_2, \state_2)$, and we instantiate adequacy with this execution and $\metaprop \eqdef \state_2 \in \Sigma$.
Then we have to show:
\[
(\All \state_2, n_s, n_t. \stateinterp(\state_2,n_s,(),n_t) \!\vs[\top][\emptyset] \state_2 \in \Sigma) \proves \consstate^{\stateinterp;[\pred];\pred_F}_{\stuckness}(\tpool_2, \state_2) \vs[\top][\emptyset] \state_2 \in \Sigma
\]

\paragraph{Hoare triples.}
It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq.
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 \wand \wpre{\expr}[\mask]{\Ret\val.\propB})}
\]
We assume the state interpretation $\stateinterp$ to be fixed by the context.

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 \\
   \atomic(\expr)
  }
  {\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]}
\end{mathparpagebreakable}

\subsection{Invariant Namespaces}
\label{sec:namespaces}

In \Sref{sec:invariants}, we defined a proposition $\invM\iname\prop$ expressing knowledge (\ie the proposition is persistent) that $\prop$ is maintained as invariant with name $\iname$.
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.
Namespaces are sets of invariants, following a tree-like structure:
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.

Formally speaking, let $\namesp \in \textlog{InvNamesp} \eqdef \List(\nat)$ be the type of \emph{invariant namespaces}.
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).
They, too, are lists of $\nat$, the same type as namespaces.
In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structured 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.
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)}\]

We will overload the notation for invariant propositions for using namespaces instead of names:
\[ \invM\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \invM\iname{\prop} \]
We can now derive the following rules (this involves unfolding the definition of fancy updates):
\begin{mathpar}
  \axiomH{inv-persist}{\invM\namesp\prop \proves \always\invM\namesp\prop}

  \axiomH{inv-alloc}{\later\prop \proves \pvs[\emptyset] \invM\namesp\prop}

  \inferH{inv-open}
  {\namesp \subseteq \mask}
  {\invM\namesp\prop \vs[\mask][\mask\setminus\namesp] \later\prop * (\later\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)}

  \inferH{inv-open-timeless}
  {\namesp \subseteq \mask \and \timeless\prop}
  {\invM\namesp\prop \vs[\mask][\mask\setminus\namesp] \prop * (\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)}
\end{mathpar}

\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.
Accessors are propositions of the form
\[ \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\All\varB. \propB' \vsW[\mask_2][\mask_1] \propC) \]

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

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
   \atomic(\expr)}
  {\hoare{\prop * \prop_F}\expr{\propC * \prop_F}[\mask_1]}
\end{mathpar}

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.

For the symmetric case where $\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)  \]
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.

\paragraph{Accessor-style invariants.}
In fact, the user-visible notion of invariants $\knowInv\namesp\prop$ is defined via \ruleref{inv-open}:
\begin{align*}
  \knowInv\namesp\prop \eqdef \always\All\mask. \pvs[\mask][\mask\setminus\namesp] \later\prop * (\later\prop \vsW[\mask\setminus\namesp][\mask] \TRUE)
\end{align*}
All the invariant laws shown above for $\invM\namesp\prop$ also hold for $\knowInv\namesp\prop$, but we can also show some additional laws that would otherwise not hold:
\begin{mathpar}
  \inferH{inv-combine}
  {\namesp_1 \disj \namesp_2 \and \namesp_1 \cup \namesp_2 \subseteq \namesp}
  {\knowInv{\namesp_1}{\prop_1} * \knowInv{\namesp_2}{\prop_2} \vdash \knowInv{\namesp}{\prop_1 * \prop_2}}

  \inferH{inv-split}
  {}
  {\knowInv{\namesp}{\prop_1 * \prop_2} \vdash \knowInv{\namesp}{\prop_1} * \knowInv{\namesp}{\prop_2}}

  \inferH{inv-alter}
  {}
  {\later\always(\prop \wand \propB * (\propB \wand \prop)) \vdash \knowInv\namesp\prop \wand \knowInv\namesp\propB}
\end{mathpar}

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