diff --git a/docs/constructions.tex b/docs/constructions.tex
index c8381082f26137c2e936a04c8751851706a9f878..8481c53f17cf4513539f3cf91ddfb098ab9e9ec2 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -5,11 +5,14 @@
Given a COFE $\cofe$, we define $\latert\cofe$ as follows:
\begin{align*}
- \latert\cofe \eqdef{}& \latertinj(\cofe) \\
+ \latert\cofe \eqdef{}& \latertinj(x:\cofe) \\
\latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
\end{align*}
+Note that in the definition of the carrier $\latert\cofe$, $\latertinj$ is a constructor (like the constructors in Coq), \ie this is short for $\setComp{\latertinj(x)}{x \in \cofe}$.
+
$\latert(-)$ is a locally \emph{contractive} functor from $\COFEs$ to $\COFEs$.
+
\subsection{Uniform Predicates}
Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
@@ -25,13 +28,13 @@ 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, we proposition either holds or does not hold.
+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{\mathbb{N}} \\
\eqdef{}& \setComp{X \in \pset{\mathbb{N}}}{ \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 with this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA:
+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}.
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.
@@ -75,6 +78,8 @@ We obtain the following frame-preserving updates:
{\melt \mupd \meltsB}
{f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
\end{mathpar}
+Remember that $\mval$ is the set of elements of a CMRA that are valid at \emph{all} step-indices.
+
$K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
@@ -87,10 +92,12 @@ Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
& \text{quotiented by} \\
\melt \equiv \meltB \eqdef{}& \melt.\aginjV = \meltB.\aginjV \land \All n. n \in \melt.\aginjV \Ra \melt.\aginjc(n) \nequiv{n} \meltB.\aginjc(n) \\
\melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\aginjV \Lra m \in \meltB.\aginjV) \land (\All m \leq n. m \in \melt.\aginjV \Ra \melt.\aginjc(m) \nequiv{m} \meltB.\aginjc(m)) \\
- \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\
+ \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ n \in \melt.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\
\mcore\melt \eqdef{}& \melt \\
\melt \mtimes \meltB \eqdef{}& (\melt.\aginjc, \setComp{n}{n \in \melt.\aginjV \land n \in \meltB.\aginjV \land \melt \nequiv{n} \meltB })
\end{align*}
+Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $\aginjc$ and $\aginjV$.
+
$\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
You can think of the $\aginjc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in \aginjV$ steps.
@@ -124,6 +131,7 @@ Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows:
\munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
\munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt)
\end{align*}%
+Notice that $\oneshotm(\monoid)$ is a disjoint sum with the four constructors (injections) $\ospending$, $\osshot$, $\munit$ and $\bot$.
The remaining cases of composition go to $\bot$.
\begin{align*}
\mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\
diff --git a/docs/iris.sty b/docs/iris.sty
index 8d893c58bec2787c3963d99ff92609d09e7b6c7c..fe64b4e90ac11fe9a53c47a4269b948610819e75 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -112,6 +112,8 @@
%% Some commonly used identifiers
+\newcommand{\op}{\textrm{op}}
+
\newcommand{\SProp}{\textdom{SProp}}
\newcommand{\UPred}{\textdom{UPred}}
\newcommand{\mProp}{\textdom{Prop}} % meta-level prop
diff --git a/docs/logic.tex b/docs/logic.tex
index 0cd2a4df83876e4b1008a869dcf659f2d49fc103..7e17741b50d85b4aac5ece5009d1687fdaca6c13 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -141,9 +141,10 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
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$.
+\ralf{$\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} assertions about propositions, defined as follows:
+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 \]
@@ -631,7 +632,7 @@ Furthermore, the following adequacy statement shows that our weakest preconditio
\\&( \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')
+ \\&\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.
diff --git a/docs/model.tex b/docs/model.tex
index cd8565605419bf22fd5b2cfe2533d13e238d62b7..d8595b6bae293ca094ea2efda9123c55edea95df 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -53,19 +53,19 @@ For every definition, we have to show all the side-conditions: The maps have to
The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$.
We start by defining the functor that assembles the CMRAs we need to the global resource CMRA:
\begin{align*}
- \textdom{ResF}(\cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: F(\cofe)}
+ \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}
\end{align*}
-where $F$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
-$\textdom{ResF}(\cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
-Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$.
+Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
+$\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}$.
Now we can write down the recursive domain equation:
-\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp)) \]
+\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
We do not need to consider how the object is constructed.
We only need the isomorphism, given by
\begin{align*}
- \Res &\eqdef \textdom{ResF}(\iPreProp) \\
+ \Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
\iProp &\eqdef \UPred(\Res) \\
\wIso &: \iProp \nfn \iPreProp \\
\wIso^{-1} &: \iPreProp \nfn \iProp
@@ -77,7 +77,7 @@ We then pick $\iProp$ as the interpretation of $\Prop$:
\paragraph{Interpretation of assertions.}
$\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply.
-We only have to define the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.
+We only have to define the interpretation of the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.
\typedsection{World satisfaction}{\wsat{-}{-}{-} :
\Delta\textdom{State} \times
@@ -87,7 +87,7 @@ We only have to define the missing connectives, the most interesting bits being
\wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t]
\rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land
\dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\
- \All\iname \in \mask, \prop. \rs.\wld(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
+ \All\iname \in \mask, \prop. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
\end{inbox}\\
\wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))}
\end{align*}
@@ -106,9 +106,9 @@ $\textdom{wp}$ is defined as the fixed-point of a contractive function.
\begin{align*}
\textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned}
\All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \disj \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
- &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\
+ &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \pred(\rsB) \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f}) \land {}\\
&(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\
- &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
+ &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
&\qquad\qquad (\expr_\f = \bot \lor m \in \textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2))
\end{aligned}} \\
\textdom{wp}_\mask(\expr, \pred) &\eqdef \mathit{fix}(\textdom{pre-wp})(\mask, \expr, \pred)
@@ -117,10 +117,12 @@ $\textdom{wp}$ is defined as the fixed-point of a contractive function.
\typedsection{Interpretation of program logic assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \iProp}
+$\knowInv\iname\prop$, $\ownGGhost\melt$ and $\ownPhys\state$ are just syntactic sugar for forms of $\ownM{-}$.
\begin{align*}
- \Sem{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &\eqdef \ownM{[\iname \mapsto \aginj(\latertinj(\wIso(\prop)))], \munit, \munit} \\
- \Sem{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &\eqdef \ownM{\munit, \munit, \melt} \\
- \Sem{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &\eqdef \ownM{\munit, \exinj(\state), \munit} \\
+ \knowInv{\iname}{\prop} &\eqdef \ownM{[\iname \mapsto \aginj(\latertinj(\wIso(\prop)))], \munit, \munit} \\
+ \ownGGhost{\melt} &\eqdef \ownM{\munit, \munit, \melt} \\
+ \ownPhys{\state} &\eqdef \ownM{\munit, \exinj(\state), \munit} \\
+~\\
\Sem{\vctx \proves \pvs[\mask_1][\mask_2] \prop : \Prop}_\gamma &\eqdef
\textdom{pvs}^{\Sem{\vctx \proves \mask_2 : \textlog{InvMask}}_\gamma}_{\Sem{\vctx \proves \mask_1 : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \\
\Sem{\vctx \proves \wpre{\expr}[\mask]{\Ret\var.\prop} : \Prop}_\gamma &\eqdef
@@ -149,9 +151,7 @@ The remaining domains are interpreted as follows:
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]
-
-The balance of our signature $\Sig$ is interpreted as follows.
-For each base type $\type$ not covered by the preceding table, we pick an object $X_\type$ in $\cal U$ and define
+For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\cal U$ and define
\[
\Sem{\type} \eqdef X_\type
\]