From af017171df21f87fc8ad61936a283de7c0421efc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 8 Dec 2017 17:23:18 +0100
Subject: [PATCH] update docs: new upred definition, sProp for validity
---
docs/algebra.tex | 43 ++++++++++++++++++-----------
docs/constructions.tex | 61 +++++++++++++++---------------------------
docs/iris.sty | 3 ++-
docs/model.tex | 8 +++---
4 files changed, 55 insertions(+), 60 deletions(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 3ba096704..357a9db8b 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -53,6 +53,16 @@ In particular:
The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.
Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.
+One very important OFE is the OFE of \emph{step-indexed propositions}:
+For every step-index, such a proposition either holds or does not hold.
+Moreover, if a propositions holds for some $n$, it also has to hold for all smaller step-indices.
+\begin{align*}
+ \SProp \eqdef{}& \psetdown{\nat} \\
+ \eqdef{}& \setComp{X \in \pset{\nat}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\
+ X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y \\
+ X \nincl{n} Y \eqdef{}& \All m \leq n. m \in X \Ra m \in Y
+\end{align*}
+
\subsection{COFE}
COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary chains.
@@ -84,7 +94,7 @@ Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkeda
\begin{defn}
A \emph{resource algebra} (RA) is a tuple \\
- $(\monoid, \mval \subseteq \monoid, \mcore{{-}}:
+ $(\monoid, \mvalFull : \monoid \to \mProp, \mcore{{-}}:
\monoid \to \maybe\monoid, (\mtimes) : \monoid \times \monoid \to \monoid)$ satisfying:
\begin{align*}
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{ra-assoc} \\
@@ -92,16 +102,19 @@ Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkeda
\All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{ra-core-id} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{ra-core-idem} \\
\All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\
- \All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\
+ \All \melt, \meltB.& \mvalFull(\melt \mtimes \meltB) \Ra \mvalFull(\melt) \tagH{ra-valid-op} \\
\text{where}\qquad %\qquad\\
\maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\
\melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
\end{align*}
\end{defn}
-\noindent
+Here, $\mProp$ is the set of (meta-level) propositions.
+Think of \texttt{Prop} in Coq or $\mathbb{B}$ in classical mathematics.
+
RAs are closely related to \emph{Partial Commutative Monoids} (PCMs), with two key differences:
\begin{enumerate}
-\item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset $\mval$ of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).
+\item The composition operation on RAs is total (as opposed to the partial composition operation of a PCM), but there is a specific subset of \emph{valid} elements that is compatible with the composition operation (\ruleref{ra-valid-op}).
+These valid elements are identified by the \emph{validity predicate} $\mvalFull$.
This take on partiality is necessary when defining the structure of \emph{higher-order} ghost state, CMRAs, in the next subsection.
@@ -122,7 +135,7 @@ Notice also that the core of an RA is a strict generalization of the unit that a
\begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
- \[ \All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \maybe{\melt_\f} \in \mval \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \maybe{\melt_\f} \in \mval \]
+ \[ \All \maybe{\melt_\f} \in \maybe\monoid. \melt \mtimes \mvalFull(\maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \mvalFull(\maybe{\melt_\f}) \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
@@ -134,17 +147,15 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\subsection{CMRA}
\begin{defn}
- A \emph{CMRA} is a tuple $(\monoid : \OFEs, (\mval_n \subseteq \monoid)_{n \in \nat},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
+ A \emph{CMRA} is a tuple $(\monoid : \OFEs, \mval : \monoid \nfn \SProp, \mcore{{-}}: \monoid \nfn \maybe\monoid,\\ (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
\begin{align*}
- \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
- \All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmra-valid-mono} \\
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore\melt \mtimes \melt = \melt \tagH{cmra-core-id} \\
\All \melt.& \mcore\melt \in \monoid \Ra \mcore{\mcore\melt} = \mcore\melt \tagH{cmra-core-idem} \\
\All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{cmra-core-mono} \\
- \All n, \melt, \meltB.& (\melt \mtimes \meltB) \in \mval_n \Ra \melt \in \mval_n \tagH{cmra-valid-op} \\
- \All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$\melt \in \mval_n \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\
+ \All \melt, \meltB.& \mval(\melt \mtimes \meltB) \subseteq \mval(\melt) \tagH{cmra-valid-op} \\
+ \All n, \melt, \meltB_1, \meltB_2.& \omit\rlap{$n \in \mval(\melt) \land \melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \Ra {}$} \\
&\Exists \meltC_1, \meltC_2. \melt = \meltC_1 \mtimes \meltC_2 \land \meltC_1 \nequiv{n} \meltB_1 \land \meltC_2 \nequiv{n} \meltB_2 \tagH{cmra-extend} \\
\text{where}\qquad\qquad\\
\melt \mincl \meltB \eqdef{}& \Exists \meltC. \meltB = \melt \mtimes \meltC \tagH{cmra-incl} \\
@@ -154,8 +165,8 @@ Since Iris ensures that the global ghost state is valid, this means that we can
This is a natural generalization of RAs over OFEs.
All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
-We define the plain $\mval$ as the ``limit'' of the $\mval_n$:
-\[ \mval \eqdef \bigcap_{n \in \nat} \mval_n \]
+We define the plain $\mvalFull$ as the ``limit'' of the step-indexed approximation:
+\[ \mvalFull(\melt) \eqdef \All n. n \in \mval(\melt) \]
\paragraph{The extension axiom (\ruleref{cmra-extend}).}
Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq.
@@ -184,7 +195,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\begin{defn}
An element $\munit$ of a CMRA $\monoid$ is called the \emph{unit} of $\monoid$ if it satisfies the following conditions:
\begin{enumerate}[itemsep=0pt]
- \item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$
+ \item $\munit$ is valid: \\ $\All n. n \in \mval(\munit)$
\item $\munit$ is a left-identity of the operation: \\
$\All \melt \in M. \munit \mtimes \melt = \melt$
\item $\munit$ is its own core: \\ $\mcore\munit = \munit$
@@ -197,7 +208,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\begin{defn}
It is possible to do a \emph{frame-preserving update} from $\melt \in \monoid$ to $\meltsB \subseteq \monoid$, written $\melt \mupd \meltsB$, if
- \[ \All n, \maybe{\melt_\f}. \melt \mtimes \maybe{\melt_\f} \in \mval_n \Ra \Exists \meltB \in \meltsB. \meltB \mtimes \maybe{\melt_\f} \in \mval_n \]
+ \[ \All n, \maybe{\melt_\f}. \melt \mtimes n \in \mval(\maybe{\melt_\f}) \Ra \Exists \meltB \in \meltsB. \meltB \mtimes n \in\mval(\maybe{\melt_\f}) \]
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
@@ -208,7 +219,7 @@ Note that for RAs, this and the RA-based definition of a frame-preserving update
\begin{enumerate}[itemsep=0pt]
\item $\monoid$ is a discrete COFE
\item $\mval$ ignores the step-index: \\
- $\All \melt \in \monoid. \melt \in \mval_0 \Ra \All n, \melt \in \mval_n$
+ $\All \melt \in \monoid. 0 \in \mval(\melt) \Ra \All n. n \in \mval(\melt)$
\end{enumerate}
\end{defn}
Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation.
@@ -223,7 +234,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\item $f$ commutes with the core:\\
$\All \melt \in \monoid_1. \mcore{f(\melt)} = f(\mcore{\melt})$
\item $f$ preserves validity: \\
- $\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$
+ $\All n, \melt \in \monoid_1. n \in \mval(\melt) \Ra n \in \mval(f(\melt))$
\end{enumerate}
\end{defn}
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 7290dcf39..74925f689 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -21,32 +21,15 @@ $\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
\begin{align*}
- \UPred(\monoid) \eqdef{} \setComp{\pred: \nat \times \monoid \to \mProp}{
- \begin{inbox}[c]
- (\All n, x, y. \pred(n, x) \land x \nequiv{n} y \Ra \pred(n, y)) \land {}\\
- (\All n, m, x, y. \pred(n, x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra \pred(m, y))
- \end{inbox}
-}
+\monoid \monnra \SProp \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}
+{\All n, \melt, \meltB. \melt \mincl[n] \meltB \Ra \pred(\melt) \nincl{n} \pred(\meltB)} \\
+ \UPred(\monoid) \eqdef{}& \faktor{\monoid \monnra \SProp}{\equiv} \\
+ \pred \equiv \predB \eqdef{}& \All m, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff m \in \predB(\melt)) \\
+ \pred \nequiv{n} \predB \eqdef{}& \All m \le n, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff m \in \predB(\melt))
\end{align*}
-where $\mProp$ is the set of meta-level propositions, \eg Coq's \texttt{Prop}.
-$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
-
-One way to understand this definition is to re-write it a little.
-We start by defining the COFE of \emph{step-indexed propositions}: For every step-index, the proposition either holds or does not hold.
-\begin{align*}
- \SProp \eqdef{}& \psetdown{\nat} \\
- \eqdef{}& \setComp{X \in \pset{\nat}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\
- X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y
-\end{align*}
-Notice that this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA:
-We could equivalently require every CMRA to define $\mval_{-}(-) : \monoid \nfn \SProp$, replacing \ruleref{cmra-valid-ne} and \ruleref{cmra-valid-mono}.
+You can think of uniform predicates as monotone, step-indexed predicates over a CMRA that ``ignore'' invalid elements (as defined by the quotient).
-Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny.
-\begin{align*}
- \UPred(\monoid) \cong{}& \monoid \monra \SProp \\
- \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}{\All n, m, x, y. n \in \pred(x) \land x \mincl y \land m \leq n \land y \in \mval_m \Ra m \in \pred(y)}
-\end{align*}
-The reason we chose the first definition is that it is easier to work with in Coq.
+$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
\clearpage
\section{RA and CMRA constructions}
@@ -69,16 +52,16 @@ Frame-preserving updates on the $M_i$ lift to the product:
The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
\begin{align*}
\monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \mundef \\
- \mval_n \eqdef{}& \setComp{\cinl(\melt_1)}{\melt_1 \in \mval'_n}
- \cup \setComp{\cinr(\melt_2)}{\melt_2 \in \mval''_n} \\
+ \mval(\mundef) \eqdef{}& \emptyset \\
+ \mval(\cinl(\melt)) \eqdef{}& \mval_1(\melt) \\
\cinl(\melt_1) \mtimes \cinl(\meltB_1) \eqdef{}& \cinl(\melt_1 \mtimes \meltB_1) \\
% \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
% \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) \\
\mcore{\cinl(\melt_1)} \eqdef{}& \begin{cases}\mnocore & \text{if $\mcore{\melt_1} = \mnocore$} \\ \cinl({\mcore{\melt_1}}) & \text{otherwise} \end{cases}
\end{align*}
-The composition and core for $\cinr$ are defined symmetrically.
+Above, $\mval_1$ refers to the validity of $\monoid_1$.
+The validity, composition and core for $\cinr$ are defined symmetrically.
The remaining cases of the composition and core are all $\mundef$.
-Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$.
Notice that we added the artificial ``invalid'' (or ``undefined'') element $\mundef$ to this CMRA just in order to make certain compositions of elements (in this case, $\cinl$ and $\cinr$) invalid.
@@ -99,7 +82,7 @@ We obtain the following frame-preserving updates, as well as their symmetric cou
{\cinl(\melt) \mupd \setComp{ \cinl(\meltB)}{\meltB \in \meltsB}}
\inferH{sum-swap}
- {\All \melt_\f, n. \melt \mtimes \melt_\f \notin \mval'_n \and \meltB \in \mval''}
+ {\All \melt_\f \in M, n. n \notin \mval(\melt \mtimes \melt_\f) \and \mvalFull(\meltB)}
{\cinl(\melt) \mupd \cinr(\meltB)}
\end{mathpar}
Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}.
@@ -122,18 +105,18 @@ Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite par
We obtain the following frame-preserving updates:
\begin{mathpar}
\inferH{fpfn-alloc-strong}
- {\text{$G$ infinite} \and \melt \in \mval}
+ {\text{$G$ infinite} \and \mvalFull(\melt)}
{\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in G}}
\inferH{fpfn-alloc}
- {\melt \in \mval}
+ {\mvalFull(\melt)}
{\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}}
\inferH{fpfn-update}
{\melt \mupd_\monoid \meltsB}
{\mapinsert i \melt f] \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
\end{mathpar}
-Above, $\mval$ refers to the validity of $\monoid$.
+Above, $\mvalFull$ refers to the (full) validity of $\monoid$.
$K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
@@ -146,7 +129,7 @@ Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
\textnormal{where }& \melt \sim \meltB \eqdef{} \All n. \melt \nequiv{n} \meltB \\
~\\
% \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
- \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ \All x, y \in \melt. x \nequiv{n} y } \\
+ \mval(\melt) \eqdef{}& \setComp{n}{ \All x, y \in \melt. x \nequiv{n} y } \\
\mcore\melt \eqdef{}& \melt \\
\melt \mtimes \meltB \eqdef{}& \melt \cup \meltB
\end{align*}
@@ -158,11 +141,11 @@ We define a non-expansive injection $\aginj$ into $\agm(\cofe)$ as follows:
\[ \aginj(x) \eqdef \set{x} \]
There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
\begin{mathpar}
- \axiomH{ag-val}{\aginj(x) \in \mval_n}
+ \axiomH{ag-val}{\mvalFull(\aginj(x))}
\axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)}
- \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Lra x \nequiv{n} y}
+ \axiomH{ag-agree}{n \in \mval(\aginj(x) \mtimes \aginj(y)) \Ra x \nequiv{n} y}
\end{mathpar}
@@ -171,7 +154,7 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
Given an OFE $\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) \mid \mundef \\
- \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \mundef}
+ \mval(\melt) \eqdef{}& \setComp{n}{\melt \neq \mundef}
\end{align*}
All cases of composition go to $\mundef$.
\begin{align*}
@@ -281,7 +264,7 @@ We assume that $M$ has a unit $\munit$, and hence its core is total.
(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
\begin{align*}
\authm(M) \eqdef{}& \maybe{\exm(M)} \times M \\
-\mval_n \eqdef{}& \setComp{ (x, \meltB) \in \authm(M) }{ \meltB \in \mval_n \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
+\mval( (x, \meltB ) ) \eqdef{}& \setComp{ n }{ n \in \mval(\meltB) \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
(x_1, \meltB_1) \mtimes (x_2, \meltB_2) \eqdef{}& (x_1 \mtimes x_2, \meltB_2 \mtimes \meltB_2) \\
\mcore{(x, \meltB)} \eqdef{}& (\mnocore, \mcore\meltB) \\
(x_1, \meltB_1) \nequiv{n} (x_2, \meltB_2) \eqdef{}& x_1 \nequiv{n} x_2 \land \meltB_1 \nequiv{n} \meltB_2
@@ -295,7 +278,7 @@ The frame-preserving update involves the notion of a \emph{local update}:
\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
\begin{defn}
It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)$, if
- \[ \All n, \maybe{\melt_\f}. \melt_1 \in \mval_n \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra \melt_2 \in \mval_n \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
+ \[ \All n, \maybe{\melt_\f}. n \in \mval(\melt_1) \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra n \in \mval(\melt_2) \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
\end{defn}
In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.
@@ -327,7 +310,7 @@ We further define \emph{closed} sets of states (given a particular set of tokens
The STS RA is defined as follows
\begin{align*}
\monoid \eqdef{}& \STSauth(s:\STSS, T:\wp(\STST) \mid \STSL(s) \disj T) \mid{}\\& \STSfrag(S: \wp(\STSS), T: \wp(\STST) \mid \STSclsd(S, T) \land S \neq \emptyset) \mid \mundef \\
- \mval \eqdef{}& \setComp{\melt\in\monoid}{\melt \neq \mundef} \\
+ \mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\
\STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \disj T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\
\STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \disj T'$ and $s \in S$} \\
\mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
diff --git a/docs/iris.sty b/docs/iris.sty
index 9ba0f619e..d55611a86 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -36,7 +36,7 @@
\newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ }
-\newcommand{\spac}{\,} % a space
+\newcommand{\spac}{\hskip 0.2em plus 0.1em} % a space
\def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}%
@@ -117,6 +117,7 @@
\newcommand{\wtt}[2]{#1 : #2} % well-typed term
\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}}
+\newcommand{\nincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\subseteq}}}}
\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}}
\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
diff --git a/docs/model.tex b/docs/model.tex
index 6100fb39b..a241fdad7 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -42,7 +42,7 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\Lam \melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt) \cup \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt) \\
\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 {} \\
+ \All m, \meltB.& m \leq n \land \melt \mincl \meltB \land m \in \mval(\meltB) \Ra {} \\
& 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 \var : \type. \prop : \Prop}_\gamma &\eqdef
\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
@@ -54,15 +54,15 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\\
\Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &\eqdef
\Lam \melt. \setComp{n}{\begin{aligned}
- \All m, \meltB.& m \leq n \land \melt\mtimes\meltB \in \mval_m \Ra {} \\
+ \All m, \meltB.& m \leq n \land m \in \mval(\melt\mtimes\meltB) \Ra {} \\
& m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\
\Sem{\vctx \proves \ownM{\term} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mincl[n] \meltB} \\
- \Sem{\vctx \proves \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \in \mval_n} \\
+ \Sem{\vctx \proves \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \mval(\Sem{\vctx \proves \term : \textlog{M}}_\gamma) \\
\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
\Sem{\vctx \proves \plainly{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\munit) \\
\Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
\Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
- \All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_m \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
+ \All m, \melt'. & m \leq n \land m \in \mval(\melt \mtimes \melt') \Ra {}\\& \Exists \meltB. m \in \mval(\meltB \mtimes \melt') \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
\end{aligned}
}
\end{align*}
--
GitLab