From 1c4f0990948d86dad4ed0b8f323eafc078e56ef7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 30 May 2020 15:12:54 +0200
Subject: [PATCH] sync iris.sty with my thesis, and small tweaks
---
tex/algebra.tex | 4 +-
tex/constructions.tex | 7 +-
tex/derived.tex | 6 +-
tex/iris.sty | 172 ++++++++++++++++++++++--------------------
tex/program-logic.tex | 26 +++----
5 files changed, 110 insertions(+), 105 deletions(-)
diff --git a/tex/algebra.tex b/tex/algebra.tex
index 0903115ef..f8a97c690 100644
--- a/tex/algebra.tex
+++ b/tex/algebra.tex
@@ -70,11 +70,11 @@ Moreover, if a propositions holds for some $n$, it also has to hold for all smal
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)$.
+ Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} $c \in \Chains(\cofe)$ 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
+ A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe : \OFEs, \lim : \Chains(\cofe) \to \cofe)$ satisfying
\begin{align*}
\All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
\end{align*}
diff --git a/tex/constructions.tex b/tex/constructions.tex
index 609dc4934..f1e0a10c2 100644
--- a/tex/constructions.tex
+++ b/tex/constructions.tex
@@ -219,7 +219,7 @@ This is useful in combination with \ruleref{sum-swap}, and also when used with p
%TODO: These need syncing with Coq
% \subsection{Finite Powerset Monoid}
-% Given an infinite set $X$, we define a monoid $\textmon{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows:
+% Given an infinite set $X$, we define a monoid $\textdom{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows:
% \[
% \melt \cdot \meltB \;\eqdef\; \melt \cup \meltB \quad \mbox{if } \melt \cap \meltB = \emptyset
% \]
@@ -265,7 +265,6 @@ Let $\melt, \meltB \in M$.
We write $\authfull \melt$ for full ownership $(\exinj(\melt), \munit)$ and $\authfrag \meltB$ for fragmental ownership $(\mnocore, \meltB)$ and $\authfull \melt , \authfrag \meltB$ for combined ownership $(\exinj(\melt), \meltB)$.
The frame-preserving update involves the notion of a \emph{local update}:
-\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
\begin{defn}
It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)$, if
\[ \All n, \maybe{\melt_\f}. n \in \mval(\melt_1) \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra n \in \mval(\melt_2) \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
@@ -326,9 +325,9 @@ In other words, the following does \emph{not} hold for the STS core as defined a
To see why, consider the following STS:
\newcommand\st{\textlog{s}}
-\newcommand\tok{\textmon{t}}
+\newcommand\tok{\textlog{t}}
\begin{center}
- \begin{tikzpicture}[sts]
+ \begin{tikzpicture}[every node/.style=sts_state]
\node at (0,0) (s1) {$\st_1$};
\node at (3,0) (s2) {$\st_2$};
\node at (9,0) (s3) {$\st_3$};
diff --git a/tex/derived.tex b/tex/derived.tex
index 95181ccb5..119a24fa9 100644
--- a/tex/derived.tex
+++ b/tex/derived.tex
@@ -7,7 +7,7 @@ However, based on them, it is possible to \emph{encode} a form of invariants tha
First, we need some ghost state:
\begin{align*}
- \textmon{CInvTok} \eqdef{}& \fracm
+ \textdom{CInvTok} \eqdef{}& \fracm
\end{align*}
Now we define:
@@ -48,7 +48,7 @@ As a consequence, they can be kept open around any sequence of expressions (\ie
Concretely, this is the monoid structure we need:
\begin{align*}
\textdom{PId} \eqdef{}& \GName \\
-\textmon{NaTok} \eqdef{}& \finpset{\InvName} \times \pset{\InvName}
+\textdom{NaTok} \eqdef{}& \finpset{\InvName} \times \pset{\InvName}
\end{align*}
For every pool, there is a set of tokens designating which invariants are \emph{enabled} (closed).
This corresponds to the mask of ``normal'' invariants.
@@ -135,7 +135,7 @@ This is essentially an \emph{optional later}, indicating that the lemmas can be
\begingroup
\paragraph{Model.}
-\newcommand\BoxM{\textmon{Box}}
+\newcommand\BoxM{\textdom{Box}}
\newcommand\SliceInv{\textlog{SliceInv}}
The above rules are validated by the following model.
diff --git a/tex/iris.sty b/tex/iris.sty
index 80cd264d3..82213c6fc 100644
--- a/tex/iris.sty
+++ b/tex/iris.sty
@@ -7,23 +7,32 @@
\RequirePackage{array}
\RequirePackage{dashbox}
\RequirePackage{tensor}
-\RequirePackage{xifthen}
\RequirePackage{xparse}
+\RequirePackage{xifthen}
\RequirePackage{mathtools}
\usetikzlibrary{shapes}
-%\usetikzlibrary{snakes}
\usetikzlibrary{arrows}
\usetikzlibrary{calc}
\usetikzlibrary{arrows.meta}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% FONTS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\textdom}[1]{\textit{#1}} % for domains/sets/types
+\newcommand{\textproj}[1]{\textsc{#1}} % for projections/fields
+\newcommand{\textlog}[1]{\textsf{\upshape #1}} % for mathematical/logic-level identifiers (make sure we do not inherit italic shape from the environment)
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MATH SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\nat}{\mathbb{N}}
-\newcommand*{\Sep}[1][]{\scalerel*{\ast}{\sum}\ifthenelse{\isempty{#1}}{}{_{#1}\;}}
+\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
\newcommand\pord{\sqsubseteq}
@@ -32,6 +41,7 @@
\newcommand\dplus{\mathbin{+\kern-1.0ex+}}
}{}
\makeatother%
+\newcommand\fmap{\mathrel{\langle\$\rangle}}
\newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ }
@@ -44,17 +54,18 @@
\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
-\newcommand{\judgment}[2][]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
+% For some reason \paragraph gives the weirdest errors ("missing \item").
+\newcommand{\judgment}[2][]{\bigskip\noindent\textit{#1}\hspace{\stretch{1}}\fbox{$#2$}}
\newcommand{\pfn}{\rightharpoonup}
-\newcommand\fpfn{\xrightharpoonup{\kern-0.25ex\textrm{fin}\kern-0.25ex}}
+\newcommand\fpfn{\xrightharpoonup{\smash{\raisebox{-.3ex}{\ensuremath{\scriptstyle\kern-0.25ex\textlog{fin}\kern-0.1ex}}}}}
\newcommand{\la}{\leftarrow}
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\Lra}{\Leftrightarrow}
-\newcommand\monra{\xrightarrow{\kern-0.15ex\textrm{mon}\kern-0.05ex}}
-\newcommand\monnra{\xrightarrow{\kern-0.15ex\textrm{mon,ne}\kern-0.05ex}}
-\newcommand\nfn{\xrightarrow{\kern-0.15ex\textrm{ne}\kern-0.05ex}}
+\newcommand\monra[1][]{\xrightarrow{\smash{\raisebox{-.3ex}{\ensuremath{\scriptstyle\kern-0.15ex\textlog{mon}_{#1}\kern-0.05ex}}}}}
+\newcommand\monnra{\xrightarrow{\smash{\raisebox{-.3ex}{\ensuremath{\scriptstyle\kern-0.15ex\textlog{mon,ne}\kern-0.05ex}}}}}
+\newcommand\nfn{\xrightarrow{\smash{\raisebox{-.3ex}{\ensuremath{\scriptstyle\kern-0.15ex\textlog{ne}\kern-0.05ex}}}}}
\newcommand{\eqdef}{\triangleq}
\newcommand{\bnfdef}{\vcentcolon\vcentcolon=}
@@ -71,23 +82,27 @@
\end{array}
}
-\newcommand{\op}{\textrm{op}}
-\newcommand{\dom}{\mathrm{dom}}
-\newcommand{\cod}{\mathrm{cod}}
-\newcommand{\chain}{\mathrm{chain}}
+\newcommand{\op}{\textlog{op}}
+\newcommand{\dom}{\textlog{dom}}
+\newcommand{\cod}{\textlog{cod}}
+\renewcommand{\lim}{\textlog{lim}}
+
+\newcommand{\Chains}{\textdom{Chains}}
\newcommand{\pset}[1]{\wp(#1)} % Powerset
\newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
-\newcommand{\finpset}[1]{\wp^\mathrm{fin}(#1)}
+\newcommand{\finpset}[1]{\wp^\textlog{fin}(#1)}
\newcommand{\pmultiset}[1]{\wp^{+}(#1)}
-\newcommand{\finpmultiset}[1]{\wp^{\mathrm{fin},+}(#1)}
+\newcommand{\finpmultiset}[1]{\wp^{\textlog{fin},+}(#1)}
\newcommand{\Func}{F} % functor
\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}
-\newcommand{\mapinsert}[3]{#3\left[#1\mathop{\la}#2\right]}
-\newcommand{\mapsingleton}[2]{\mapinsert{#1}{#2}{}}
+\newcommand{\mapelem}[2]{#1\mathop{\la}#2}
+\newcommand{\mapinsert}[3]{#3\!\left[\mapelem{#1}{#2}\right]}
+\newcommand{\mapdelete}[2]{#2\setminus\set{#1}}
+\newcommand{\mapsingleton}[2]{\mapinsert{#1}{#2}{\,}}
\newcommand{\mapinsertComp}[4]
{\mapinsert{#1}{#2 \spac\middle|\spac #3}{#4}}
\newcommand{\mapComp}[3]
@@ -101,7 +116,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\textdom}[1]{\textit{#1}}
\newcommand{\wIso}{\xi}
@@ -157,7 +171,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\textmon}[1]{\textsc{#1}}
\newcommand{\monoid}{M}
\newcommand{\mval}{\mathcal{V}}
@@ -169,7 +182,7 @@
\newcommand{\melts}{A}
\newcommand{\meltsB}{B}
-\newcommand{\f}{\mathrm{f}} % for "frame"
+\newcommand{\f}{\textlog{f}} % used as subscript, for "frame"
\newcommand{\munit}{\varepsilon}
\newcommand{\mcore}[1]{{\mid}#1{\mid}} % using "|" here makes LaTeX diverge. WTF.
@@ -178,9 +191,10 @@
\newcommand{\mtimes}{\mathbin{\cdot}}
\newcommand{\mundef}{\lightning}
-\newcommand{\exclusive}{\mathrm{exclusive}}
+\newcommand{\exclusive}{\textlog{exclusive}}
\newcommand{\mupd}{\rightsquigarrow}
+\newcommand{\lupd}{\rightsquigarrow_{\mathfrak{L}}}
\newcommand{\mincl}[1][]{%
\ensuremath{\mathrel{\vbox{\offinterlineskip\ialign{%
\hfil##\hfil\cr
@@ -189,12 +203,11 @@
$\preccurlyeq$\cr
}}}}}
-\newcommand{\CMRAs}{\mathbf{Camera}}
+\newcommand{\CMRAs}{\mathbf{Camera}} % category of Cameras/CMRAs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\textlog}[1]{\textsf{#1}}
\newcommand{\Sig}{\mathcal{S}}
\newcommand{\SigType}{\mathcal{T}}
@@ -240,16 +253,17 @@
\newcommand{\fixp}{\mathit{fix}}
%% various pieces of Syntax
-\def\MU #1.{\mu\,#1.\spac}%
-\def\Lam #1.{\lambda\,#1.\spac}%
+\def\MU #1.{\mu #1.\spac}%
+\def\Lam #1.{\lambda #1.\spac}%
\newcommand{\proves}{\vdash}
\newcommand{\provesIff}{\mathrel{\dashv\vdash}}
-\newcommand{\wand}{\mathrel{-\!\!*}}
+\newcommand{\wand}{\mathrel{-\!\!\ast}}
+\newcommand{\wandIff}{\mathrel{\ast\!\!{-}\!\!\ast}}
% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
-\newcommand{\fmapsto}[1][]{\xmapsto{#1}}
+\newcommand{\fmapsto}[1][]{\xmapsto{\smash{\raisebox{-.15ex}{\ensuremath{\scriptstyle #1}}}}}
\newcommand{\gmapsto}{\hookrightarrow}%
\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
@@ -264,8 +278,9 @@
\newcommand{\later}{\mathop{{\triangleright}}}
\newcommand*{\lateropt}[1]{\mathop{{\later}^{#1}}}
-\newcommand{\always}{\mathop{\Box}}
+\newcommand{\always}{\mathop{\boxempty}}
\newcommand{\plainly}{\mathop{\blacksquare}}
+\newcommand{\pers}{\mathop{\boxdot}}
%% Invariants and Ghost ownership
% PDS: Was 0pt inner, 2pt outer.
@@ -293,7 +308,7 @@
% Two masks
\tensor*[^{#1}]{#2}{^{#3}}
}%
- \kern0.2ex}}%
+ }}%
\NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
\NewDocumentCommand \bvs {O{} O{}} {\vsGen[#1]{\dispdot[0.02ex]{\Rrightarrow}}[#2]}
\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
@@ -304,33 +319,19 @@
\newcommand\vsWand{{\displaystyle\equiv\kern-1.6ex-\kern-1.5ex\smash{\scalerel*{\vphantom-\ast}{\sum}}\kern-0.2ex}}
\NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]}
+\newcommand\vsWandStep{{\displaystyle\raisebox{0.106ex}{\scaleobj{0.82}{\later}}\kern-1.65ex\equiv\kern-1.6ex-\kern-1.5ex\smash{\scalerel*{\vphantom-\ast}{\sum}}\kern-0.2ex}}
+\NewDocumentCommand \vsWS {O{} O{}} {\vsGen[#1]{\vsWandStep}[#2]}
+
% for now, the update modality looks like a pvs without masks.
\NewDocumentCommand \upd {} {\mathop{\dispdot[-0.2ex]{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}}
-\NewDocumentCommand\Acc{O{} O{} m m}{\langle #3 \vsE #4 \rangle_{#1}^{#2}}
+\NewDocumentCommand\Acc{O{} O{} m m}{#3 \mathrel{~\vsGen[#1]{\propto}[#2]~} #4}
%% Hoare Triples
-\newcommand*{\hoaresizebox}[1]{%
- \hbox{$\mathsurround=0pt{#1}\mathstrut$}}
-\newcommand*{\hoarescalebox}[2]{%
- \hbox{\scalerel*[1ex]{#1}{#2}}}
-\newcommand{\triple}[5]{%
- \setbox0=\hoaresizebox{{#3}{#5}}%
- \setbox1=\hoarescalebox{#1}{\copy0}%
- \setbox2=\hoarescalebox{#2}{\copy0}%
- \copy1{#3}\copy2%
- \; #4 \;%
- \copy1{#5}\copy2}
-
-\newcommand{\bracket}[4][]{%
- \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
- \scalerel*[1ex]{#2}{\copy0}%
- {#4}%
- \scalerel*[1ex]{#3}{\copy0}}
-% \curlybracket[other] x
-\newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}}
-\newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}}
+
+% needs extra {...} for some weird reason
+\newcommand{\curlybracket}[1]{{\left\{#1\right\}}}
\NewDocumentCommand \hoare {m m m O{}}{
\curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
@@ -341,32 +342,40 @@
{\begin{aligned}[#1]
&\curlybracket{#2} \\
&\quad{#3} \\
- &{\curlybracket{#4}}_{#5}
+ &\curlybracket{#4}_{#5}
\end{aligned}}%
}
% \hoareHV[t] pre c post [mask]
\NewDocumentCommand \hoareHV {O{c} m m m O{}}{
{\begin{aligned}[#1]
- &\curlybracket{#2} \; {#3} \\
- &{\curlybracket{#4}}_{#5}
+ &\curlybracket{#2} \spac {#3} \\
+ &\curlybracket{#4}_{#5}
+ \end{aligned}}%
+}
+% \hoareVH[t] pre c post [mask]
+\NewDocumentCommand \hoareVH {O{c} m m m O{}}{
+ {\begin{aligned}[#1]
+ &\curlybracket{#2} \\
+ & {#3}\spac \curlybracket{#4}_{#5}
\end{aligned}}%
}
%% Some commonly used identifiers
\newcommand{\inhabited}[1]{\textlog{inhabited}(#1)}
+\newcommand{\infinite}{\textlog{infinite}}
\newcommand{\timeless}[1]{\textlog{timeless}(#1)}
\newcommand{\persistent}[1]{\textlog{persistent}(#1)}
-\newcommand{\infinite}{\textlog{infinite}}
\newcommand\InvName{\textdom{InvName}}
\newcommand\GName{\textdom{GName}}
-\newcommand{\Prop}{\textlog{iProp}}
-\newcommand{\Pred}{\textlog{Pred}}
+\newcommand{\Prop}{\textdom{iProp}}
+\newcommand{\Pred}{\textdom{Pred}}
\newcommand{\TRUE}{\textlog{True}}
\newcommand{\FALSE}{\textlog{False}}
+\newcommand{\EMP}{\textlog{emp}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% GENERIC LANGUAGE SYNTAX AND SEMANTICS
@@ -375,10 +384,10 @@
\newcommand{\val}{v}
\newcommand{\valB}{w}
\newcommand{\state}{\sigma}
-\newcommand{\step}[1][]{\xrightarrow{{#1}}_{\mathsf{t}}}
-\newcommand{\hstep}[1][]{\xrightarrow{{#1}}_{\mathsf{h}}}
-\newcommand{\tpstep}[1][]{\xrightarrow{{#1}}_{\mathsf{tp}}}
-\newcommand{\tpsteps}[1][]{\xrightarrow{{#1}}\mathrel{\vphantom{\to}^{*}_{\mathsf{tp}}}}
+\newcommand{\step}[1][]{\xrightarrow{{#1}}_{\textlog{t}}}
+\newcommand{\hstep}[1][]{\xrightarrow{{#1}}_{\textlog{h}}}
+\newcommand{\tpstep}[1][]{\xrightarrow{{#1}}_{\textlog{tp}}}
+\newcommand{\tpsteps}[1][]{\xrightarrow{{#1}}\mathrel{\vphantom{\to}^{*}_{\textlog{tp}}}}
\newcommand{\lctx}{K}
\newcommand{\Lctx}{\textdom{Ctx}}
\newcommand{\obs}{\kappa}
@@ -391,11 +400,11 @@
\newcommand{\Obs}{\textdom{Obs}}
\newcommand{\ThreadPool}{\textdom{ThreadPool}}
-\newcommand{\toval}{\mathrm{expr\any to\any val}}
-\newcommand{\ofval}{\mathrm{val\any to\any expr}}
-\newcommand{\atomic}{\mathrm{atomic}}
-\newcommand{\stronglyAtomic}{\mathrm{strongly\any atomic}}
-\newcommand{\red}{\mathrm{red}}
+\newcommand{\toval}{\textlog{expr\any to\any val}}
+\newcommand{\ofval}{\textlog{val\any to\any expr}}
+\newcommand{\atomic}{\textlog{atomic}}
+\newcommand{\stronglyAtomic}{\textlog{strongly\any{}atomic}}
+\newcommand{\red}{\textlog{red}}
\newcommand{\Lang}{\Lambda}
\newcommand{\tpool}{T}
@@ -412,21 +421,22 @@
\newcommand{\unit}{1}
% Agreement
-\newcommand{\agm}{\ensuremath{\textmon{Ag}}}
+\newcommand{\agm}{\ensuremath{\textdom{Ag}}}
\newcommand{\aginj}{\textlog{ag}}
% Fraction
-\newcommand{\fracm}{\ensuremath{\textmon{Frac}}}
+\newcommand{\fracm}{\ensuremath{\textdom{Frac}}}
\newcommand{\fracinj}{\textlog{frac}}
% Exclusive
-\newcommand{\exm}{\ensuremath{\textmon{Ex}}}
+\newcommand{\exm}{\ensuremath{\textdom{Ex}}}
\newcommand{\exinj}{\textlog{ex}}
% Auth
-\newcommand{\authm}{\textmon{Auth}}
-\newcommand{\authfull}{\mathord{\bullet}\,}
-\newcommand{\authfrag}{\mathord{\circ}\,}
+\newcommand{\authm}{\textdom{Auth}}
+\newcommand{\authinj}{\textlog{auth}}
+\newcommand{\authfull}{\mathord{\bullet}}
+\newcommand{\authfrag}{\mathord{\circ}}
\newcommand{\AuthInv}{\textsf{AuthInv}}
\newcommand{\Auth}{\textsf{Auth}}
@@ -436,13 +446,9 @@
\newcommand{\cinl}{\textsf{inl}}
\newcommand{\cinr}{\textsf{inr}}
-% One-Shot
-\newcommand{\oneshotm}{\ensuremath{\textmon{OneShot}}}
-\newcommand{\ospending}{\textlog{pending}}
-\newcommand{\osshot}{\textlog{shot}}
-
% STSs
\newcommand{\STSCtx}{\textlog{StsCtx}}
+\newcommand{\STSInv}{\textlog{StsInv}}
\newcommand{\STSSt}{\textlog{StsSt}}
\newcommand{\STSclsd}{\textlog{closed}}
\newcommand{\STSauth}{\textlog{auth}}
@@ -454,32 +460,32 @@
\newcommand{\ststrans}{\ra^{*}}% the relation relevant to the STS rules
\newcommand{\stsfstep}[1]{\xrightarrow{#1}}
\newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}}
+\newcommand{\stsinterp}{\varphi}
-\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}]
+\tikzstyle{sts_state} = [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{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
%% Cancellable invariants
\newcommand\CInv[3]{\textlog{CInv}^{#1,#2}(#3)}
-\newcommand*\CInvTok[2]{{[}\textrm{CInv}:#1{]}_{#2}}
+\newcommand*\CInvTok[2]{{[}\textlog{CInv}:#1{]}_{#2}}
%% Non-atomic invariants
\newcommand*\pid{p}
\newcommand\NaInv[3]{\textlog{NaInv}^{#1.#2}(#3)}
-\newcommand*\NaTok[1]{{[}\textrm{NaInv}:#1{]}}
-\newcommand*\NaTokE[2]{{[}\textrm{NaInv}:#1.#2{]}}
+\newcommand*\NaTok[1]{{[}\textlog{NaInv}:#1{]}}
+\newcommand*\NaTokE[2]{{[}\textlog{NaInv}:#1.#2{]}}
%% Boxes
-\newcommand*\sname{i}
-\newcommand*\BoxState{\textlog{BoxState}}
+\newcommand*\sname{\iota}
+\newcommand*\BoxState{\textdom{BoxState}}
\newcommand*\BoxFull{\textlog{full}}
\newcommand*\BoxEmp{\textlog{empty}}
\newcommand*\BoxSlice[3]{\textlog{BoxSlice}(#1, #2, #3)}
\newcommand*\ABox[3]{\textlog{Box}(#1, #2, #3)}
-
\endinput
diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index ca1d0266c..754660ea0 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -17,35 +17,35 @@ To this end, we use tokens that manage which invariants are currently enabled.
We assume to have the following four cameras available:
\begin{align*}
\InvName \eqdef{}& \nat \\
- \textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
- \textmon{En} \eqdef{}& \pset{\InvName} \\
- \textmon{Dis} \eqdef{}& \finpset{\InvName}
+ \textdom{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
+ \textdom{En} \eqdef{}& \pset{\InvName} \\
+ \textdom{Dis} \eqdef{}& \finpset{\InvName}
\end{align*}
-The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
+The last two are the tokens used for managing invariants, $\textdom{Inv}$ is the monoid used to manage the invariants themselves.
-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 cameras have been created, such that these names are globally known.
+We assume that at the beginning of the verification, instances named $\gname_{\textdom{State}}$, $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
\paragraph{World Satisfaction.}
We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
W \eqdef{}& \Exists I : \InvName \fpfn \Prop.
\begin{array}[t]{@{} l}
- \ownGhost{\gname_{\textmon{Inv}}}{\authfull
+ \ownGhost{\gname_{\textdom{Inv}}}{\authfull
\mapComp {\iname}
{\aginj(\latertinj(\wIso(I(\iname))))}
{\iname \in \dom(I)}} * \\
- \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right)
+ \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textdom{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textdom{En}}}{\set{\iname}} \right)
\end{array}
\end{align*}
\paragraph{Invariants.}
The following proposition states that an invariant with name $\iname$ exists and maintains proposition $\prop$:
-\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}
+\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textdom{Inv}}}
{\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}} \]
\paragraph{Fancy Updates and View Shifts.}
Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
-\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
+\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textdom{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textdom{En}}}{\mask_2} * \prop) \]
Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
Masks are sets of natural numbers, \ie they are subsets of $\mathbb{N}$.%
\footnote{Actually, in the Coq development masks are restricted to a class of sets of natural numbers that contains all finite sets and is closed under union, intersection, difference and complement.
@@ -169,7 +169,7 @@ Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck,
& (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
& \Bigl(\toval(\expr) = \bot \land \All \state, \vec\obs, \vec\obs', n. \stateinterp(\state, \vec\obs \dplus \vec\obs', n) \vsW[\mask][\emptyset] {}\\
&\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step[\vec\obs] \expr', \state', \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
- &\qquad\qquad \stateinterp(\state', \vec\obs', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep[\expr'' \in \vec\expr] \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
+ &\qquad\qquad \stateinterp(\state', \vec\obs', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
\wpre[\stateinterp;\pred_F]\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\stateinterp,\pred_F,\stuckness)(\mask, \expr, \Lam\val.\prop)
\end{align*}
The $\stateinterp$ and $\pred_F$ will always be set by the context; typically, when instantiating Iris with a language, we also pick the corresponding state interpretation $\stateinterp$ and fork-postcondition $\pred_F$.
@@ -220,7 +220,7 @@ This basically just copies the second branch (the non-value case) of the definit
{ {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
~~\All \state_1,\vec\obs,\vec\obs',n. \stateinterp(\state_1,\vec\obs \dplus \vec\obs', n) \vsW[\mask][\emptyset] (\stuckness = \NotStuck \Ra \red(\expr_1,\state_1)) * {}\\
\qquad~ \All \expr_2, \state_2, \vec\expr. (\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
- \qquad\qquad\Bigl(\stateinterp(\state_2,\vec\obs',n+|\vec\expr|) * \wpre[\stateinterp;\pred_F]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep[\expr_\f \in \vec\expr] \wpre[\stateinterp\pred_F]{\expr_\f}[\stuckness;\top]{\pred_F}\Bigr) {}\\
+ \qquad\qquad\left(\stateinterp(\state_2,\vec\obs',n+|\vec\expr|) * \wpre[\stateinterp;\pred_F]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre[\stateinterp\pred_F]{\expr_\f}[\stuckness;\top]{\pred_F}\right) {}\\
\proves \wpre[\stateinterp\pred_F]{\expr_1}[\stuckness;\mask]{\Ret\var.\prop}
\end{inbox}} }
\end{mathpar}
@@ -245,7 +245,7 @@ where $\consstate$ describes states that are consistent with the state interpret
&\quad (s = \NotStuck \Ra \All \expr \in \tpool_2. \toval(\expr) \neq \bot \lor \red(\expr, \state_2) ) *{}\\
&\quad \stateinterp(\state_2, (), |\tpool_2'|) *{}\\
&\quad (\toval(\expr_2) \ne \bot \wand \pred(\toval(\expr_2))) *{}\\
- &\quad \left(\Sep[\expr \in \tpool_2'] \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))\right)
+ &\quad \left(\Sep_{\expr \in \tpool_2'} \toval(\expr) \ne \bot \wand \pred_F(\toval(\expr))\right)
\end{align*}
The $\hat\metaprop$ here arises because we need a way to talk about $\metaprop$ inside Iris.
To this end, we assume that the signature $\Sig$ contains some assertion $\hat{\metaprop}$:
@@ -484,7 +484,7 @@ For this reason, we also call such accessors \emph{non-atomic}.
The reasons accessors are useful is that they let us talk about ``opening X'' (\eg ``opening invariants'') without having to care what X is opened around.
Furthermore, as we construct more sophisticated and more interesting things that can be opened (\eg invariants that can be ``cancelled'', or STSs), accessors become a useful interface that allows us to mix and match different abstractions in arbitrary ways.
-For the special case that $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition:
+For the symmetric case where $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition:
\[ \Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop) \]
This accessor is ``idempotent'' in the sense that it does not actually change the state. After applying it, we get our $\prop$ back so we end up where we started.
--
GitLab