diff --git a/docs/algebra.tex b/docs/algebra.tex
index d6f2de09aa54f52fcc8c1b9f980e216878cdb8af..4479a15967e3fe54df1385952d7f7ed4aa4d4aec 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -45,7 +45,7 @@ The reason that contractive functions are interesting is that for every contract
The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
\end{defn}
-Note that $\COFEs$ is cartesian closed:
+Note that $\COFEs$ is cartesian closed. In particular:
\begin{defn}
Given two COFEs $\cofe$ and $\cofeB$, the set of non-expansive functions $\set{f : \cofe \nfn \cofeB}$ is itself a COFE with
\begin{align*}
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 40571188f68a0ca7b4ec90de8acce72c8bd96b63..4dc0a2910c9b7ca43af2de1ac504a1b23e6ba972 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -91,7 +91,7 @@ Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that
\subsection{Finite partial function}
\label{sec:fpfnm}
-Given some countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a COFE and CMRA structure by lifting everything pointwise.
+Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a COFE and CMRA structure by lifting everything pointwise.
We obtain the following frame-preserving updates:
\begin{mathpar}
@@ -149,7 +149,7 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
\subsection{Exclusive CMRA}
-Given a cofe $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
+Given a COFE $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
\begin{align*}
\exm(\cofe) \eqdef{}& \exinj(\cofe) + \bot \\
\mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot}
@@ -375,7 +375,7 @@ We obtain the following frame-preserving update:
\subsection{STS with tokens}
\label{sec:stsmon}
-Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep} \subseteq \STSS \times \STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS \ra \wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct a monoid modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
+Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep} \subseteq \STSS \times \STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS \ra \wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing a \emph{law of token conservation}) and define a stepping relation for the \emph{frame} of a given token set:
diff --git a/docs/derived.tex b/docs/derived.tex
index 34471d0804706e0c67c8d15e08368f9c957567a5..38674cb70679a666e240d533dccc6e460170804e 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -1,6 +1,6 @@
\section{Derived proof rules and other constructions}
-We will below abuse notation, using the \emph{term} meta-variables like $\val$ to range over (bound) \emph{variables} of the corresponding type..
+We will below abuse notation, using the \emph{term} meta-variables like $\val$ to range over (bound) \emph{variables} of the corresponding type.
We omit type annotations in binders and equality, when the type is clear from context.
We assume that the signature $\Sig$ embeds all the meta-level concepts we use, and their properties, into the logic.
(The Coq formalization is a \emph{shallow embedding} of the logic, so we have direct access to all meta-level notions within the logic anyways.)
diff --git a/docs/logic.tex b/docs/logic.tex
index a7b4dd401e756c02d549bfed91cff0ccd9f052aa..01d904d71ef8edf12da59d84654008e63779814d 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -7,7 +7,7 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
\end{mathpar}
\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{\bot})\]
We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\
- A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_\f$ is forked off.
+ 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}
@@ -40,7 +40,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\paragraph{Machine syntax}
\[
- \tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n
+ \tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Expr}^n
\]
\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
@@ -48,12 +48,12 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\begin{mathpar}
\infer
{\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \and \expr_\f \neq \bot}
- {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state} \step
- \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_\f]}{\state'}}
+ {\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} \step
- \cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state'}}
+ {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
+ \cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state_2}}
\end{mathpar}
\clearpage
@@ -595,15 +595,16 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i
{\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} * \later\All \expr_2, \state_2, \expr_\f. (\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
+ ~~\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).
diff --git a/docs/model.tex b/docs/model.tex
index 6f5f765550487e683bfd39835b87019590399e08..166b3ef6e8e640a94d4f4694845d027e6dcd69d9 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -26,7 +26,7 @@ We introduce an additional logical connective $\ownM\melt$, which will later be
\Sem{\vctx \proves \prop \Ra \propB : \Prop}_\gamma &\eqdef
\Lam \melt. \setComp{n}{\begin{aligned}
\All m, \meltB.& m \leq n \land \melt \mincl \meltB \land \meltB \in \mval_m \Ra {} \\
- & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt)\end{aligned}}\\
+ & m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB)\end{aligned}}\\
\Sem{\vctx \proves \All x : \type. \prop : \Prop}_\gamma &\eqdef
\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, x : \type \proves \prop : \Prop}_{\gamma[x \mapsto v]}(\melt) } \\
\Sem{\vctx \proves \Exists x : \type. \prop : \Prop}_\gamma &\eqdef
@@ -58,7 +58,7 @@ Above, $\maybe\monoid$ is the monoid obtained by adding a unit to $\monoid$.
(It's not a coincidence that we used the same notation for the range of the core; it's the same type either way: $\monoid + 1$.)
Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$ (see~\Sref{sec:logic}).
$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
-Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}$.
+Furthermore, since $\Sigma$ is locally contractive, so is $\textdom{ResF}$.
Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
@@ -187,10 +187,10 @@ $\rho(x)\in\Sem{\vctx(x)}$.
\paragraph{Logical entailment.}
We can now define \emph{semantic} logical entailment.
-\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : 2}
+\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : \mProp}
\[
-\Sem{\vctx \mid \pfctx \proves \propB} \eqdef
+\Sem{\vctx \mid \pfctx \proves \prop} \eqdef
\begin{aligned}[t]
\MoveEqLeft
\forall n \in \mathbb{N}.\;