diff --git a/docs/constructions.tex b/docs/constructions.tex index e11c63bbf8395ca3d2a4ab8e454f9ea803733b16..c8381082f26137c2e936a04c8751851706a9f878 100644 --- a/docs/constructions.tex +++ b/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{ifT_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 diff --git a/docs/derived.tex b/docs/derived.tex index df80640344bc8282f48d1f01beed61dc50a2fa45..696be132bc318fb8d6f73ab3350b1ba92bd16c28 100644 --- a/docs/derived.tex +++ b/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}$ diff --git a/docs/iris.sty b/docs/iris.sty index 73b727b20d0248caad5b24dc876f4967488f9455..8d893c58bec2787c3963d99ff92609d09e7b6c7c 100644 --- a/docs/iris.sty +++ b/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}] diff --git a/docs/logic.tex b/docs/logic.tex index 6b3c37119d6f9e2780cca18bd9b40338aaa7c0a9..0cd2a4df83876e4b1008a869dcf659f2d49fc103 100644 --- a/docs/logic.tex +++ b/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 \propcan 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} diff --git a/docs/model.tex b/docs/model.tex index aff36d7ae2aaf886ab3591b884e7cb4818d4893d..cd8565605419bf22fd5b2cfe2533d13e238d62b7 100644 --- a/docs/model.tex +++ b/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 {}&\\ diff --git a/naming.txt b/naming.txt index b98dd3d306340a0e9ce5b13b10bff3b9a85a27ea..191c1664e7b820563ec755f3554a0cf746ce9e0f 100644 --- a/naming.txt +++ b/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)