diff --git a/docs/base-logic.tex b/docs/base-logic.tex
new file mode 100644
index 0000000000000000000000000000000000000000..85a49e129bdf20bd32cb859cab46d1d735db75b0
--- /dev/null
+++ b/docs/base-logic.tex
@@ -0,0 +1,397 @@
+\section{Base Logic}
+\label{sec:base-logic}
+
+The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit.
+This defines the structure of resources that can be owned.
+
+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{M}, \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$).
+Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
+
+\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
+ \melt \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
+\\&
+ \ownGGhost{\term} \mid \mval(\term) \mid
+ \always\prop \mid
+ {\later\prop} \mid
+ \upd \prop\mid
+\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 the modalities $\upd$, $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
+
+
+\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{\melt}{\textlog{M}}}
+ {\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
+\and
+ \infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a CMRA}}
+ {\vctx \proves \wtt{\mval(\melt)}{\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}
+ }{
+ \vctx \proves \wtt{\upd \prop}{\Prop}
+ }
+\end{mathparpagebreakable}
+
+\subsection{Proof rules}
+\label{sec: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}
+Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda$ and $\mu$.
+
+
+\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} &\proves& \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}
+A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ is derivable for some $\term$.
+
+\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 \land \propB)} &\proves& \always{(\prop * \propB)} \\
+ \always{\prop} \land \propB &\proves& \always{\prop} * \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
+{ \ownGGhost{\mcore\melt} \proves \always \ownGGhost{\mcore\melt}}
+\and
+{ \mval(\melt) \proves \always \mval(\melt)}
+\end{mathpar}
+
+\paragraph{Laws for the update modality.}
+\begin{mathpar}
+\infer[upd-intro]
+{}{\prop \proves \upd \prop}
+
+\infer[upd-trans]
+{}
+{\upd \upd \prop \proves \upd \prop}
+
+\infer[upd-frame]
+{}{\propB * \upd\prop \proves \upd (\propB * \prop)}
+
+\inferH{upd-update}
+{\melt \mupd \meltsB}
+{\ownGGhost\melt \proves \upd \Exists\meltB\in\meltsB. \ownGGhost\meltB}
+\end{mathpar}
+
+\subsection{Soundness}
+
+The soundness statement of the logic
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End:
diff --git a/docs/iris.sty b/docs/iris.sty
index c95c30e234666529908eb1cfc76aa0555699ecb4..ac183873e4bd6e0afedb10cefa9226d264d261c4 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -249,6 +249,9 @@
{\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}}
+% for now, the update modality looks like a pvs without masks.
+\NewDocumentCommand \upd {} {\mathord{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
+
%% Hoare Triples
\newcommand*{\hoaresizebox}[1]{%
diff --git a/docs/iris.tex b/docs/iris.tex
index 6774f9ad12bc203ab092bfad9221c16ece57a844..ff135e11fbfe60fbc43fc90a79f2619e538913bc 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -31,10 +31,12 @@
\endgroup\clearpage\begingroup
\input{constructions}
\endgroup\clearpage\begingroup
-\input{logic}
+\input{base-logic}
\endgroup\clearpage\begingroup
\input{model}
\endgroup\clearpage\begingroup
+\input{program-logic}
+\endgroup\clearpage\begingroup
\input{derived}
\endgroup\clearpage\begingroup
\printbibliography
diff --git a/docs/logic.tex b/docs/logic.tex
deleted file mode 100644
index a2c4e4fd400371e6646609516e4c782fa507a66a..0000000000000000000000000000000000000000
--- a/docs/logic.tex
+++ /dev/null
@@ -1,663 +0,0 @@
-\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_2$, a \emph{new thread} $\expr_\f$ is 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, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \]
-\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, \expr_\f. \expr, \state_1 \step \expr_2, \state_2, \expr_\f \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, \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{Expr}^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_1} \step
- \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_\f]}{\state_2}}
-\and\infer
- {\expr_1, \state_1 \step \expr_2, \state_2}
- {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
- \cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state_2}}
-\end{mathpar}
-
-\clearpage
-\section{Logic}
-\label{sec:logic}
-
-To instantiate Iris, you need to define the following parameters:
-\begin{itemize}
-\item A language $\Lang$, and
-\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. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(A)$ is a total function.)
-\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$.
-%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}
-\]
-
-\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}{\type} \and \text{$\type$ is a CMRA}}
- {\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}
-\label{sec: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}
-Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda$ and $\mu$.
-
-
-\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} &\proves& \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}
-A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ is derivable for some $\term$.
-
-\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 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}
-
-
-\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 \land \propB)} &\proves& \always{(\prop * \propB)} \\
- \always{\prop} \land \propB &\proves& \always{\prop} * \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}}
-\and
-{ \mval(\melt) \proves \always \mval(\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 \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).
-
-\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:
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
new file mode 100644
index 0000000000000000000000000000000000000000..9ccbc2c6617fb8f9ec70859cf1e613ada4848aa1
--- /dev/null
+++ b/docs/program-logic.tex
@@ -0,0 +1,247 @@
+\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_2$, a \emph{new thread} $\expr_\f$ is 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, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \]
+\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, \expr_\f. \expr, \state_1 \step \expr_2, \state_2, \expr_\f \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, \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{Expr}^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_1} \step
+ \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_\f]}{\state_2}}
+\and\infer
+ {\expr_1, \state_1 \step \expr_2, \state_2}
+ {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
+ \cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state_2}}
+\end{mathpar}
+
+\clearpage
+\section{Program Logic}
+
+\ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}
+
+To instantiate Iris, you need to define the following parameters:
+\begin{itemize}
+\item A language $\Lang$, and
+\item a locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $\cofe$, the CMRA $\iFunc(A)$ has a unit. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(\cofe)$ is a total function.)
+\end{itemize}
+
+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{\ownGGhost\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}
+{\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 \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 * \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.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End: