From 11069713a94be0a5ac213daa9110a615a043f88a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 11 Mar 2016 15:16:11 +0100 Subject: [PATCH] docs: update iris.sty, some more on agreement --- docs/constructions.tex | 21 ++++++++++++++------- docs/iris.sty | 36 ++++++++++++++++++++++++++++++++++++ docs/setup.tex | 28 ---------------------------- 3 files changed, 50 insertions(+), 35 deletions(-) diff --git a/docs/constructions.tex b/docs/constructions.tex index 9405ecd7..7a08fa78 100644 --- a/docs/constructions.tex +++ b/docs/constructions.tex @@ -5,24 +5,31 @@ \subsection{Agreement} Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows: +\newcommand{\agc}{\mathrm{c}} % the "c" field of an agreement element +\newcommand{\agV}{\mathrm{V}} % the "V" field of an agreement element \begin{align*} - \monoid \eqdef{}& \recordComp{c : \mathbb{N} \to T , V : \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in V \Ra m \in V } \\ + \monoid \eqdef{}& \recordComp{\agc : \mathbb{N} \to T , \agV : \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in \agV \Ra m \in \agV } \\ & \text{quotiented by} \\ - \melt \equiv \meltB \eqdef{}& \melt.V = \meltB.V \land \All n. n \in \melt.V \Ra \melt.c(n) \nequiv{n} \meltB.c(n) \\ - \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.V \Lra m \in \meltB.V) \land (\All m \leq n. m \in \melt.V \Ra \melt.c(m) \nequiv{m} \meltB.c(m)) \\ - \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.V \land \All m \leq n. \melt.c(n) \nequiv{m} \melt.c(m) } \\ + \melt \equiv \meltB \eqdef{}& \melt.\agV = \meltB.\agV \land \All n. n \in \melt.\agV \Ra \melt.\agc(n) \nequiv{n} \meltB.\agc(n) \\ + \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\agV \Lra m \in \meltB.\agV) \land (\All m \leq n. m \in \melt.\agV \Ra \melt.\agc(m) \nequiv{m} \meltB.\agc(m)) \\ + \mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.\agV \land \All m \leq n. \melt.\agc(n) \nequiv{m} \melt.\agc(m) } \\ \mcore\melt \eqdef{}& \melt \\ - \melt \mtimes \meltB \eqdef{}& (\melt.c, \setComp{n}{n \in \melt.V \land n \in \meltB.V_2 \land \melt \nequiv{n} \meltB }) + \melt \mtimes \meltB \eqdef{}& (\melt.\agc, \setComp{n}{n \in \melt.\agV \land n \in \meltB.\agV \land \melt \nequiv{n} \meltB }) \end{align*} $\agm(-)$ is a locally non-expansive bifunctor from $\COFEs$ to $\CMRAs$. The reason we store a \emph{chain} $c$ of elements of $T$, 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. \ralf{Figure out why exactly this is not possible without adding an explicit chain here.} +We define an injection $\ag$ into $\agm(\cofe)$ as follows: +$\ag(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \mathbb{N}}$ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following: \begin{mathpar} - \axiomH{ag-dup}{\melt = \melt \mtimes \melt} - \and\axiomH{ag-agree}{\melt \mtimes \meltB \in \mval_n \Ra \melt \nequiv{n} \meltB} + \axiomH{ag-val}{\ag(x) \in \mval_n} + + \axiomH{ag-dup}{\ag(x) = \ag(x)\mtimes\ag(x)} + + \axiomH{ag-agree}{\ag(x) \mtimes \ag(y) \in \mval_n \Ra x \nequiv{n} y} \end{mathpar} diff --git a/docs/iris.sty b/docs/iris.sty index b9953fba..0c73ddd2 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -313,6 +313,42 @@ \newcommand{\cfg}[2]{{#1};{#2}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% STANDARD DERIVED CONSTRUCTIONS +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Agreement +\newcommand{\agm}{\ensuremath{\textmon{Ag}}} +\newcommand{\ag}{\textlog{ag}} + +% Fraction +\newcommand{\fracm}{\ensuremath{\textmon{Frac}}} + +% Exclusive +\newcommand{\exm}{\ensuremath{\textmon{Ex}}} + +% Auth +\newcommand{\authm}{\textmon{Auth}} +\newcommand{\authfull}{\mathord{\bullet}\,} +\newcommand{\authfrag}{\mathord{\circ}\,} + +\newcommand{\AuthInv}{\textsf{AuthInv}} +\newcommand{\Auth}{\textsf{Auth}} + +%% STSs +\newcommand{\STSCtx}{\textlog{StsCtx}} +\newcommand{\STSSt}{\textlog{StsSt}} +\newcommand{\STSS}{\mathcal{S}} % states +\newcommand{\STST}{\mathcal{T}} % tokens +\newcommand{\STSL}{\mathcal{L}} % labels +\newcommand{\ststrans}{\ra^{*}}% the relation relevant to the STS rules + + +\tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}] +\tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}] + +%% Stored Propositions +\newcommand{\mapstoprop}{\mathrel{\mapstochar\Ra}} \endinput diff --git a/docs/setup.tex b/docs/setup.tex index 849e8362..8c5b9219 100644 --- a/docs/setup.tex +++ b/docs/setup.tex @@ -110,31 +110,3 @@ \let\ralf\hush% \let\dave\hush% } - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% DERIVED CONSTRUCTIONS -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%% Commonly used identifiers -\newcommand{\FHeap}{\textmon{FHeap}} -\newcommand{\AFHeap}{\textmon{AFHeap}} - -\newcommand{\auth}[1]{\textmon{Auth}} -\newcommand{\authfull}{\mathord{\bullet}\,} -\newcommand{\authfrag}{\mathord{\circ}\,} - -\newcommand{\fracm}{\ensuremath{\textmon{Frac}}} -\newcommand{\exm}{\ensuremath{\textmon{Ex}}} -\newcommand{\agm}{\ensuremath{\textmon{Ag}}} - -\newcommand{\STSMon}[1]{\textmon{Sts}_{#1}} -\newcommand{\STSInv}{\textsf{STSInv}} -\newcommand{\STS}{\textsf{STS}} -\newcommand{\STSS}{\mathcal{S}} % states -\newcommand{\STST}{\mathcal{T}} % tokens -\newcommand{\STSL}{\mathcal{L}} % labels -\newcommand{\ststrans}{\ra^{*}}% the relation relevant to the STS rules - -\newcommand{\AuthInv}{\textsf{AuthInv}} -\newcommand{\Auth}{\textsf{Auth}} -- GitLab