From 0dd400067686b9b599c7380a468f03b17525d699 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Mon, 5 Dec 2016 13:57:36 +0100
Subject: [PATCH] update documentation for the new OFE story

docs/algebra.tex  81 +++++++++++++++++++++++++
docs/constructions.tex  18 +++++
docs/ghoststate.tex  6 ++
docs/iris.sty  7 ++
docs/model.tex  2 +
docs/programlogic.tex  13 ++++
6 files changed, 73 insertions(+), 54 deletions()
diff git a/docs/algebra.tex b/docs/algebra.tex
index e9d12d74..b5050387 100644
 a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ 1,65 +1,82 @@
\section{Algebraic Structures}
\subsection{COFE}
+\subsection{OFE}
The model of Iris lives in the category of \emph{Complete Ordered Families of Equivalences} (COFEs).
+The model of Iris lives in the category of \emph{Ordered Families of Equivalences} (OFEs).
This definition varies slightly from the original one in~\cite{catlogic}.
\begin{defn}[Chain]
 Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
\end{defn}

\begin{defn}
 A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe, ({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}, \lim : \chain(\cofe) \to \cofe)$ satisfying
+ An \emph{ordered family of equivalences} (OFE) is a tuple $(\ofe, ({\nequiv{n}} \subseteq \ofe \times \ofe)_{n \in \nat})$ satisfying
\begin{align*}
 \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofeequiv} \\
 \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofemono} \\
 \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofelimit} \\
 \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofecompl}
+ \All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{ofeequiv} \\
+ \All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{ofemono} \\
+ \All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{ofelimit}
\end{align*}
\end{defn}
The key intuition behind COFEs is that elements $x$ and $y$ are $n$equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{cofemono})and in the limit, it agrees with plain equality (\ruleref{cofelimit}).
In order to solve the recursive domain equation in \Sref{sec:model} it is also essential that COFEs are \emph{complete}, \ie that any chain has a limit (\ruleref{cofecompl}).
+The key intuition behind OFEs is that elements $x$ and $y$ are $n$equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
+In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{ofemono})and in the limit, it agrees with plain equality (\ruleref{ofelimit}).
\begin{defn}
 An element $x \in \cofe$ of a COFE is called \emph{discrete} if
 \[ \All y \in \cofe. x \nequiv{0} y \Ra x = y\]
 A COFE $A$ is called \emph{discrete} if all its elements are discrete.
 For a set $X$, we write $\Delta X$ for the discrete COFE with $x \nequiv{n} x' \eqdef x = x'$

+ An element $x \in \ofe$ of an OFE is called \emph{discrete} if
+ \[ \All y \in \ofe. x \nequiv{0} y \Ra x = y\]
+ An OFE $A$ is called \emph{discrete} if all its elements are discrete.
+ For a set $X$, we write $\Delta X$ for the discrete OFE with $x \nequiv{n} x' \eqdef x = x'$
\end{defn}
\begin{defn}
 A function $f : \cofe \to \cofeB$ between two COFEs is \emph{nonexpansive} (written $f : \cofe \nfn \cofeB$) if
 \[\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
+ A function $f : \ofe \to \ofeB$ between two OFEs is \emph{nonexpansive} (written $f : \ofe \nfn \ofeB$) if
+ \[\All n, x \in \ofe, y \in \ofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
It is \emph{contractive} if
 \[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
+ \[ \All n, x \in \ofe, y \in \ofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
\end{defn}
Intuitively, applying a nonexpansive function to some data will not suddenly introduce differences between seemingly equal data.
Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$.
The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a \emph{unique} fixedpoint $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
\begin{defn}
 The category $\COFEs$ consists of COFEs as objects, and nonexpansive functions as arrows.
+ The category $\OFEs$ consists of OFEs as objects, and nonexpansive functions as arrows.
\end{defn}
Note that $\COFEs$ is cartesian closed. In particular:
+Note that $\OFEs$ is cartesian closed. In particular:
\begin{defn}
 Given two COFEs $\cofe$ and $\cofeB$, the set of nonexpansive functions $\set{f : \cofe \nfn \cofeB}$ is itself a COFE with
+ Given two OFEs $\ofe$ and $\ofeB$, the set of nonexpansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with
\begin{align*}
 f \nequiv{n} g \eqdef{}& \All x \in \cofe. f(x) \nequiv{n} g(x)
+ f \nequiv{n} g \eqdef{}& \All x \in \ofe. f(x) \nequiv{n} g(x)
\end{align*}
\end{defn}
\begin{defn}
 A (bi)functor $F : \COFEs \to \COFEs$ is called \emph{locally nonexpansive} if its action $F_1$ on arrows is itself a nonexpansive map.
+ A (bi)functor $F : \OFEs \to \OFEs$ is called \emph{locally nonexpansive} if its action $F_1$ on arrows is itself a nonexpansive map.
Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
\end{defn}
The function space $() \nfn ()$ is a locally nonexpansive bifunctor.
Note that the composition of nonexpansive (bi)functors is nonexpansive, and the composition of a nonexpansive and a contractive (bi)functor is contractive.
The reason contractive (bi)functors are interesting is that by America and Rutten's theorem~\cite{AmericaRutten:JCSS89,birkedal:metricspace}, they have a unique\footnote{Uniqueness is not proven in Coq.} fixedpoint.
+
+\subsection{COFE}
+
+COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary chains.
+
+\begin{defn}[Chain]
+ Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
+\end{defn}
+
+\begin{defn}
+ A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe : \OFEs, \lim : \chain(\cofe) \to \cofe)$ satisfying
+ \begin{align*}
+ \All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofecompl}
+ \end{align*}
+\end{defn}
+
+\begin{defn}
+ The category $\COFEs$ consists of COFEs as objects, and nonexpansive functions as arrows.
+\end{defn}
+
+The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the domain $\ofe$ can actually be just an OFE).
+
+Completeness is necessary to take fixedpoints.
+For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$ is a COFE and inhabited has a \emph{unique} fixedpoint $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
+Furthermore, by America and Rutten's theorem~\cite{AmericaRutten:JCSS89,birkedal:metricspace}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixedpoint.
+
\subsection{RA}
@@ 115,7 +132,7 @@ 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 : \COFEs, (\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_n \subseteq \monoid)_{n \in \nat},\\ \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{cmravalidne} \\
\All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmravalidmono} \\
@@ 133,7 +150,7 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\end{align*}
\end{defn}
This is a natural generalization of RAs over COFEs.
+This is a natural generalization of RAs over OFEs.
All operations have to be nonexpansive, and the validity predicate $\mval$ can now also depend on the stepindex.
We define the plain $\mval$ as the ``limit'' of the $\mval_n$:
\[ \mval \eqdef \bigcap_{n \in \nat} \mval_n \]
@@ 209,7 +226,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\begin{defn}
The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows.
\end{defn}
Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
+Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\OFEs$.
The notion of a locally nonexpansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
%TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.
diff git a/docs/constructions.tex b/docs/constructions.tex
index 28205478..eb72d0c8 100644
 a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ 1,20 +1,20 @@
\section{COFE constructions}
+\section{OFE and COFE constructions}
\subsection{Trivial pointwise lifting}
The COFE structure on many types can be easily obtained by pointwise lifting of the structure of the components.
+The (C)OFE structure on many types can be easily obtained by pointwise lifting of the structure of the components.
This is what we do for option $\maybe\cofe$, product $(M_i)_{i \in I}$ (with $I$ some finite index set), sum $\cofe + \cofe'$ and finite partial functions $K \fpfn \monoid$ (with $K$ infinite countable).
\subsection{Next (typelevel later)}
Given a COFE $\cofe$, we define $\latert\cofe$ as follows (using a datatypelike notation to define the type):
+Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatypelike notation to define the type):
\begin{align*}
\latert\cofe \eqdef{}& \latertinj(x:\cofe) \\
\latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n1} 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$.
+$\latert()$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
\subsection{Uniform Predicates}
@@ 117,7 +117,7 @@ Notice that this core is total, as the result always lies in $\maybe\monoid$ (ra
\subsection{Finite partial function}
\label{sec:fpfnm}
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.
+Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a CMRA structure by lifting everything pointwise.
We obtain the following framepreserving updates:
\begin{mathpar}
@@ 139,7 +139,7 @@ $K \fpfn ()$ is a locally nonexpansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
+Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
\begin{align*}
\agm(\cofe) \eqdef{}& \set{(c, V) \in (\nat \to \cofe) \times \SProp}/\ {\sim} \\[0.2em]
\textnormal{where }& \melt \sim \meltB \eqdef{} \melt.V = \meltB.V \land
@@ 152,7 +152,7 @@ Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\end{align*}
%Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
$\agm()$ is a locally nonexpansive functor from $\COFEs$ to $\CMRAs$.
+$\agm()$ is a locally nonexpansive functor from $\OFEs$ to $\CMRAs$.
You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in V$ steps.
The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
@@ 175,7 +175,7 @@ There are no interesting framepreserving 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 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}
@@ 193,7 +193,7 @@ The stepindexed equivalence is inductively defined as follows:
\axiom{\mundef \nequiv{n} \mundef}
\end{mathpar}
$\exm()$ is a locally nonexpansive functor from $\COFEs$ to $\CMRAs$.
+$\exm()$ is a locally nonexpansive functor from $\OFEs$ to $\CMRAs$.
We obtain the following framepreserving update:
\begin{mathpar}
diff git a/docs/ghoststate.tex b/docs/ghoststate.tex
index 95fa8e37..19084064 100644
 a/docs/ghoststate.tex
+++ b/docs/ghoststate.tex
@@ 51,7 +51,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
One of the troubles of working in a stepindexed logic is the ``later'' modality $\later$.
It turns out that we can somewhat mitigate this trouble by working below the following \emph{except0} modality:
\[ \diamond \prop \eqdef \later\FALSE \lor \Prop \]
+\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]
This modality is useful because there is a class of assertions which we call \emph{timeless} assertions, for which we have
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
@@ 122,11 +122,11 @@ The following rules identify the class of timeless assertions:
\axiom{\timeless{\FALSE}}
\infer
{\text{$\term$ or $\term'$ is a discrete COFE element}}
+{\text{$\term$ or $\term'$ is a discrete OFE element}}
{\timeless{\term =_\type \term'}}
\infer
{\text{$\melt$ is a discrete COFE element}}
+{\text{$\melt$ is a discrete OFE element}}
{\timeless{\ownM\melt}}
\infer
diff git a/docs/iris.sty b/docs/iris.sty
index 9c5becfc..51d4ebae 100644
 a/docs/iris.sty
+++ b/docs/iris.sty
@@ 146,8 +146,11 @@
% List
\newcommand{\List}{\ensuremath{\textdom{List}}}
\newcommand{\cofe}{T}
\newcommand{\cofeB}{U}
+\newcommand{\ofe}{T}
+\newcommand{\ofeB}{U}
+\newcommand{\cofe}{\ofe}
+\newcommand{\cofeB}{\ofeB}
+\newcommand{\OFEs}{\mathcal{OFE}} % category of OFEs
\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs
\newcommand{\iFunc}{\Sigma}
\newcommand{\fix}{\textdom{fix}}
diff git a/docs/model.tex b/docs/model.tex
index fcb9d727..f91d3d37 100644
 a/docs/model.tex
+++ b/docs/model.tex
@@ 18,7 +18,7 @@ The semantic domains are interpreted as follows:
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]
For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\COFEs$ and define
+For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\OFEs$ and define
\[
\Sem{\type} \eqdef X_\type
\]
diff git a/docs/programlogic.tex b/docs/programlogic.tex
index 0f3be291..1d33f1f1 100644
 a/docs/programlogic.tex
+++ b/docs/programlogic.tex
@@ 22,16 +22,16 @@ The purpose of this section is to describe how we solve these issues.
\paragraph{Picking the resources.}
The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
+To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.
(This is in contrast to the base logic, where the user picks a single, fixed CMRA that has a unit.)
From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
\mathcal G \eqdef{}& \nat \\
 \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\cofe^\op, \cofe)
+ \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\ofe^\op, \ofe)
\end{align*}
We will motivate both the use of a product and the finite partial function below.
$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
+$\textdom{ResF}(\ofe^\op, \ofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$.
Now we can write down the recursive domain equation:
@@ 93,7 +93,7 @@ We can show the following properties for this form of ownership:
{\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}
\inferH{restimeless}
 {\text{$\melt$ is a discrete COFE element}}
+ {\text{$\melt$ is a discrete OFE element}}
{\timeless{\ownGhost\gname{\melt : M_i}}}
\end{mathparpagebreakable}
@@ 121,8 +121,7 @@ We assume to have the following four CMRAs available:
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine.
Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created.
(We will discuss later how this assumption is discharged.)
+We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created, such that these names are globally known.
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
@@ 187,7 +186,7 @@ Fancy updates satisfy the following basic proof rules:
% \inferH{fupcloseI}
% {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
\end{mathparpagebreakable}
(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:invariants}.)
+(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.)
We can further define the notions of \emph{view shifts} and \emph{linear view shifts}:
\begin{align*}

2.26.2