Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

docs/constructions.tex

@@ -42,7 +42,7 @@ Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\
 The reason we chose the first definition is that it is easier to work with in Coq.
 
 \clearpage
-\section{CMRA constructions}
+\section{RA and CMRA constructions}
 
 \subsection{Product}
 \label{sec:prodm}
@@ -378,54 +378,79 @@ We obtain the following frame-preserving update:
 % 	}
 % \end{mathpar}
 
-% \subsection{STS with tokens monoid}
-% \label{sec:stsmon}
+\subsection{STS with tokens}
+\label{sec:stsmon}
 
-% Given a state-transition system~(STS) $(\STSS, \ra)$, a set of tokens $\STSS$, and a labeling $\STSL: \STSS \ra \mathcal{P}(\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 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.
 
-% The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
-% We first lift the transition relation to $\STSS \times \mathcal{P}(\STST)$ (implementing a \emph{law of token conservation}) and define upwards closure:
-% \begin{align*}
-%  (s, T) \ra (s', T') \eqdef&\, s \ra s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
-%  \textsf{frame}(s, T) \eqdef&\, (s, \STST \setminus (\STSL(s) \uplus T)) \\
-%  \upclose(S, T) \eqdef&\, \setComp{ s' \in \STSS}{\exists s \in S.\; \textsf{frame}(s, T) \ststrans \textsf{frame}(s', T) }
-% \end{align*}
+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:
+\begin{align*}
+ (s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
+ s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \disj \STSL(s) \cup T \l+and (s, T_1) \stsstep (s', T_2)
+\end{align*}
 
-% \noindent
-% We have
-% \begin{quote}
-% 	If $(s, T) \ra (s', T')$\\
-% 	and $T_\f \sep (T \uplus \STSL(s))$,\\
-% 	then $\textsf{frame}(s, T_\f) \ra \textsf{frame}(s', T_\f)$.
-% \end{quote}
-% \begin{proof}
-% This follows directly by framing the tokens in $\STST \setminus (T_\f \uplus T \uplus \STSL(s))$ around the given transition, which yields $(s, \STST \setminus (T_\f \uplus \STSL{T}(s))) \ra (s', T' \uplus (\STST \setminus (T_\f \uplus T \uplus \STSL{T}(s))))$.
-% This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s') \uplus T'$.
-% \end{proof}
+We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set:
+\begin{align*}
+\STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \disj T \land \All s'. s \stsfstep{T} s' \Ra s' \in S \\
+\upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
+\end{align*}
 
-% Let $\STSMon{\STSS}$ be the monoid with carrier
-% \[
-% 	\setComp{ (s, S, T) \in \exm{\STSS} \times \mathcal{P}(\STSS) \times \mathcal{P}(\STST) }{ \begin{aligned} &(s = \munit \lor s \in S) \land \upclose(S, T) = S   \land{} \\& S \neq \emptyset \land \All s \in S. \STSL(s) \sep T  \end{aligned} }
-% \]
-% and multiplication
-% \[
-% 	(s, S, T) \mtimes (s', S', T') \eqdef (s'' \eqdef s \mtimes_{\exm{\STSS}} s', S'' \eqdef S \cap S', T'' \eqdef T \cup T') \quad \text{if }\begin{aligned}[t] &(s = \munit \lor s' = \munit) \land T \sep T' \land{} \\& S'' \neq \emptyset \land (s'' \neq \munit \Ra s'' \in S'') \end{aligned}
-% \]
+The STS RA is defined as follows
+\begin{align*}
+  \monoid \eqdef{}& \setComp{\STSauth((s, T) \in \STSS \times \wp(\STST))}{\STSL(s) \disj T} +{}\\& \setComp{\STSfrag((S, T) \in \wp(\STSS) \times \wp(\STST))}{\STSclsd(S, T) \land S \neq \emptyset} + \bot \\
+  \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) \\
+  \mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset)
+\end{align*}
+The remaining cases are all $\bot$.
 
-% Some sugar makes it more convenient to assert being at least in a certain state and owning some tokens: $(s, T) : \STSMon{\STSS} \eqdef (\munit, \upclose(\{s\}, T), T) : \STSMon{\STSS}$, and
-% $s : \STSMon{\STSS} \eqdef (s, \emptyset) : \STSMon{\STSS}$.
+We will need the following frame-preserving update:
+\begin{mathpar}
+  \inferH{sts-step}{(s, T) \ststrans (s', T')}
+  {\STSauth(s, T) \mupd \STSauth(s', T')}
 
-% We will need the following frame-preserving update.
-% \begin{mathpar}
-% 	\inferH{StsStep}{(s, T) \ststrans (s', T')}
-% 	 {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')}
-% \end{mathpar}
-% \begin{proof}[Proof of \ruleref{StsStep}]
-% Assume some upwards-closed $S_\f, T_\f$ (the frame cannot be authoritative) s.t.\ $s \in S_\f$ and $T_\f \sep (T \uplus \STSL(s))$. We have to show that this frame combines with our final monoid element, which is the case if $s' \in S_\f$ and $T_\f \sep T'$.
-% By upward-closedness, it suffices to show $\textsf{frame}(s, T_\f) \ststrans \textsf{frame}(s', T_\f)$.
-% This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step.
-% \end{proof}
+  \inferH{sts-weaken}
+  {\STSclsd(S_2, T_2) \and S_1 \subseteq S_2 \and T_2 \subseteq T_1}
+  {\STSfrag(S_1, T_1) \mupd \STSfrag(S_2, T_2)}
+\end{mathpar}
+
+\paragraph{The core is not a homomorphism.}
+The core of the STS construction is only satisfying the RA axioms because we are \emph{not} demanding the core to be a homomorphism---all we demand is for the core to be monotone with respect the \ruleref{ra-incl}.
+
+In other words, the following does \emph{not} hold for the STS core as defined above:
+\[ \mcore\melt \mtimes \mcore\meltB = \mcore{\melt\mtimes\meltB} \]
+
+To see why, consider the following STS:
+\newcommand\st{\textlog{s}}
+\newcommand\tok{\textmon{t}}
+\begin{center}
+  \begin{tikzpicture}[sts]
+    \node at (0,0)   (s1) {$\st_1$};
+    \node at (3,0)  (s2) {$\st_2$};
+    \node at (9,0) (s3) {$\st_3$};
+    \node at (6,0)  (s4) {$\st_4$\\$[\tok_1, \tok_2]$};
+    
+    \path[sts_arrows] (s2) edge  (s4);
+    \path[sts_arrows] (s3) edge  (s4);
+  \end{tikzpicture}
+\end{center}
+Now consider the following two elements of the STS RA:
+\[ \melt \eqdef \STSfrag(\set{\st_1,\st_2}, \set{\tok_1}) \qquad\qquad
+  \meltB \eqdef \STSfrag(\set{\st_1,\st_3}, \set{\tok_2}) \]
+
+We have:
+\begin{mathpar}
+  {\melt\mtimes\meltB = \STSfrag(\set{\st_1}, \set{\tok_1, \tok_2})}
 
+  {\mcore\melt = \STSfrag(\set{\st_1, \st_2, \st_4}, \emptyset)}
+
+  {\mcore\meltB = \STSfrag(\set{\st_1, \st_3, \st_4}, \emptyset)}
+
+  {\mcore\melt \mtimes \mcore\meltB = \STSfrag(\set{\st_1, \st_4}, \emptyset) \neq
+    \mcore{\melt \mtimes \meltB} = \STSfrag(\set{\st_1}, \emptyset)}
+\end{mathpar}
 
 %%% Local Variables: 
 %%% mode: latex

docs/derived.tex

@@ -319,8 +319,8 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$
 We define the inclusion relation on namespaces as $\namesp_1 \sqsubseteq \namesp_2 \Lra \Exists \namesp_3. \namesp_2 = \namesp_3 \dplus \namesp_1$, \ie $\namesp_1$ is a suffix of $\namesp_2$.
 We have that $\namesp_1 \sqsubseteq \namesp_2 \Ra \namecl{\namesp_2} \subseteq \namecl{\namesp_1}$.
 
-Similarly, we define $\namesp_1 \sep \namesp_2 \eqdef   \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
-We have that $\namesp_1 \sep \namesp_2 \Ra \namecl{\namesp_2} \sep \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \sep \namesp.\iname_2$.
+Similarly, we define $\namesp_1 \disj \namesp_2 \eqdef   \Exists \namesp_1', \namesp_2'. \namesp_1' \sqsubseteq \namesp_1 \land \namesp_2' \sqsubseteq \namesp_2 \land |\namesp_1'| = |\namesp_2'| \land \namesp_1' \neq \namesp_2'$, \ie there exists a distinguishing suffix.
+We have that $\namesp_1 \disj \namesp_2 \Ra \namecl{\namesp_2} \disj \namecl{\namesp_1}$, and furthermore $\iname_1 \neq \iname_2 \Ra \namesp.\iname_1 \disj \namesp.\iname_2$.
 
 We will overload the usual Iris notation for invariant assertions in the following:
 \[ \knowInv\namesp\prop \eqdef \Exists \iname \in \namecl\namesp. \knowInv\iname{\prop} \]

docs/iris.sty

@@ -29,9 +29,8 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
-\newcommand{\bigast}{\Sep}
-
-\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}}	% bad name; it's a different "sep"
+\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
+\newcommand\pord{\sqsubseteq}
 \newcommand\dplus{\mathbin{+\kern-1.0ex+}}
 \newcommand{\upclose}{\mathord{\uparrow}}
 \newcommand{\ALT}{\ |\ }
@@ -44,10 +43,11 @@
 
 \newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
 
-\newcommand{\judgment}[2]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
+\newcommand{\judgment}[2][]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
 
 \newcommand{\pfn}{\rightharpoonup}
 \newcommand\fpfn{\xrightharpoonup{\kern-0.25ex\textrm{fin}\kern-0.25ex}}
+\newcommand{\la}{\leftarrow}
 \newcommand{\ra}{\rightarrow}
 \newcommand{\Ra}{\Rightarrow}
 \newcommand{\Lra}{\Leftrightarrow}
@@ -353,10 +353,16 @@
 % STSs
 \newcommand{\STSCtx}{\textlog{StsCtx}}
 \newcommand{\STSSt}{\textlog{StsSt}}
+\newcommand{\STSclsd}{\textlog{closed}}
+\newcommand{\STSauth}{\textlog{auth}}
+\newcommand{\STSfrag}{\textlog{frag}}
 \newcommand{\STSS}{\mathcal{S}} % states
 \newcommand{\STST}{\mathcal{T}} % tokens
 \newcommand{\STSL}{\mathcal{L}} % labels
+\newcommand{\stsstep}{\ra}
 \newcommand{\ststrans}{\ra^{*}}%	the relation relevant to the STS rules
+\newcommand{\stsfstep}[1]{\xrightarrow{#1}}
+\newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}}
 
 
 \tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}]

docs/logic.tex

@@ -50,7 +50,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
 	\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Exp}^n
 \]
 
-\judgment{Machine reduction} {\cfg{\tpool}{\state} \step
+\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
   \cfg{\tpool'}{\state'}}
 \begin{mathpar}
 \infer
@@ -181,7 +181,7 @@ The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable cont
 A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types.
 In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$.
 
-\judgment{Well-typed terms}{\vctx \proves_\Sig \wtt{\term}{\type}}
+\judgment[Well-typed terms]{\vctx \proves_\Sig \wtt{\term}{\type}}
 \begin{mathparpagebreakable}
 %%% variables and function symbols
 	\axiom{x : \type \proves \wtt{x}{\type}}
@@ -312,7 +312,7 @@ We implicitly assume that an arbitrary variable context, $\vctx$, is added to ev
 Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
 Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ can be derived.
 
-\judgment{}{\vctx \mid \pfctx \proves \prop}
+\judgment{\vctx \mid \pfctx \proves \prop}
 \paragraph{Laws of intuitionistic higher-order logic with equality.}
 This is entirely standard.
 \begin{mathparpagebreakable}

docs/model.tex

@@ -95,7 +95,7 @@ We only have to define the missing connectives, the most interesting bits being
 \typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}
 \begin{align*}
 	\mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}
-            \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \sep \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
+            \All \rs_\f, m, \mask_\f, \state.& 0 < m \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
             \Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f}
           \end{aligned}}
 \end{align*}
@@ -105,7 +105,7 @@ We only have to define the missing connectives, the most interesting bits being
 $\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 \sep \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
+        \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 {}\\
         &(\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 {}&\\

naming.txt

@@ -4,8 +4,8 @@ b : B : cmraT or cofeT
 c
 d
 e : expr = expressions
-f
-g
+f : some generic function
+g : some generic function
 h : heap
 i
 j
@@ -16,8 +16,8 @@ n
 o
 p
 q
-r : res = resources
-s
+r : iRes = resources
+s : state (STSs)
 t
 u
 v : val = values of language
@@ -32,14 +32,15 @@ B : Type, cmraT or cofeT
 C
 D   
 E : coPset = Viewshift masks
-F
+F : a functor
 G
-H = hypotheses
+H : hypotheses
 I : indexing sets
 J
 K : ectx = evaluation contexts
+    keys of a map
 L
-M = maps / global CMRA
+M : maps / global CMRA
 N : namespace
 O 
 P : uPred, iProp or Prop
@@ -48,12 +49,17 @@ R : uPred, iProp or Prop
 S : set state = state sets in STSs
 T : set token = token sets in STSs
 U
-V : abstraction of values in frame shift assertions
+V : abstraction of value type in frame shift assertions
 W
 X : sets
 Y : sets
 Z : sets
 
 == small greek letters ==
-γ : gname.
+γ : gname
 σ : state = state of language
+φ : interpretation of STS/Auth
+
+== capital greek letters ==
+Φ : general predicate (over uPred, iProp or Prop)
+Ψ : general predicate (over uPred, iProp or Prop)