docs: fix some typos

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

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:

docs/derived.tex

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

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

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