diff --git a/docs/iris.sty b/docs/iris.sty
new file mode 100644
index 0000000000000000000000000000000000000000..ba2811f5279cad4fa8aed945cdbf63ab97c84630
--- /dev/null
+++ b/docs/iris.sty
@@ -0,0 +1,300 @@
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{iris}
+
+\RequirePackage{tikz}
+\RequirePackage{scalerel}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% SETUP
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\usetikzlibrary{shapes}
+%\usetikzlibrary{snakes}
+\usetikzlibrary{arrows}
+\usetikzlibrary{calc}
+\usetikzlibrary{arrows.meta}
+\tikzstyle{state}=[circle, draw, minimum size=1.2cm, align=center]
+\tikzstyle{trans}=[arrows={->[scale=1.4]}]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% MATH SYMBOLS & NOTATION & IDENTIFIERS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
+\newcommand{\bigast}{\Sep}
+
+\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}} % bad name; it's a different "sep"
+\newcommand\dplus{\mathbin{+\kern-1.0ex+}}
+\newcommand{\upclose}{\mathord{\uparrow}}
+\newcommand{\ALT}{\ |\ }
+
+\newcommand{\spac}{\;} % a space
+
+\def\All #1.{\forall #1.\spac}%
+\def\Exists #1.{\exists #1.\spac}%
+\def\Ret #1.{#1.\spac}%
+
+\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
+
+\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{\ra}{\rightarrow}
+\newcommand{\Ra}{\Rightarrow}
+\newcommand{\Lra}{\Leftrightarrow}
+\newcommand\monra{\xrightarrow{\kern-0.25ex\textrm{mon}\kern-0.25ex}}
+
+\newcommand{\eqdef}{\triangleq}
+\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
+\newcommand*\set[1]{\left\{#1\right\}}
+
+\newenvironment{inbox}[1][]{
+ \begin{array}[#1]{@{}l@{}}
+}{
+ \end{array}
+}
+
+\newcommand{\dom}{\mathrm{dom}}
+\newcommand{\cod}{\mathrm{cod}}
+\newcommand{\chain}{\mathrm{chain}}
+
+\newcommand{\pset}[1]{\wp(#1)} % Powerset
+\newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
+
+\newcommand{\Func}{F} % functor
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\textdom}[1]{\textit{#1}}
+
+\newcommand{\wIso}{\xi}
+
+\newcommand{\rs}{r}
+\newcommand{\rsB}{s}
+
+\newcommand{\pres}{\pi}
+\newcommand{\wld}{w}
+\newcommand{\ghostRes}{g}
+
+%% Various pieces of syntax
+\newcommand{\wsat}[4]{#1 \models_{#2} #3; #4}
+
+\newcommand{\wtt}[2]{#1 : #2} % well-typed term
+
+\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}}
+\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}}
+\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
+\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
+\newcommand{\latert}{\mathord{\blacktriangleright}}
+
+\newcommand{\Sem}[1]{\llbracket #1 \rrbracket}
+
+\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{\(#1\)}}}
+\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}}
+
+
+%% Some commonly used identifiers
+\newcommand{\UPred}{\textdom{UPred}}
+
+\newcommand{\PropDom}{\textdom{Prop}}
+\newcommand{\PredDom}{\textdom{Pred}}
+
+\newcommand{\COFEs}{\mathcal{U}} % category of COFEs
+\newcommand{\iFunc}{\Sigma}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\textmon}[1]{\textsc{#1}}
+
+\newcommand{\monoid}{M}
+\newcommand{\mval}{V}
+
+\newcommand{\melt}{a}
+\newcommand{\meltB}{b}
+\newcommand{\meltC}{c}
+\newcommand{\melts}{A}
+\newcommand{\meltsB}{B}
+
+\newcommand{\mcar}[1]{|#1|}
+\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
+\newcommand{\munit}{\mathord{\varepsilon}}
+\newcommand{\mtimes}{\mathbin{\cdot}}
+\newcommand{\mdiv}{\mathbin{\div}}
+
+\newcommand{\mupd}{\rightsquigarrow}
+\newcommand{\mincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\leq}}}}
+
+\newcommand{\CMRAs}{\mathcal{R}} % category of CMRAs
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\textlog}[1]{\textsf{#1}}
+
+\newcommand{\Sig}{\mathcal{S}}
+\newcommand{\SigType}{\mathcal{T}}
+\newcommand{\SigFn}{\mathcal{F}}
+\newcommand{\SigAx}{\mathcal{A}}
+\newcommand{\sigtype}{T}
+\newcommand{\sigfn}{F}
+\newcommand{\sigax}{A}
+
+\newcommand{\type}{\tau}
+
+\newcommand{\var}{x}
+\newcommand{\varB}{y}
+\newcommand{\varC}{z}
+
+\newcommand{\term}{t}
+\newcommand{\termB}{u}
+
+\newcommand{\vctx}{\Gamma}
+\newcommand{\pfctx}{\Theta}
+
+\newcommand{\prop}{P}
+\newcommand{\propB}{Q}
+\newcommand{\propC}{R}
+
+\newcommand{\pred}{\varphi}
+\newcommand{\predB}{\psi}
+\newcommand{\predC}{\zeta}
+
+\newcommand{\gname}{\gamma}
+\newcommand{\iname}{\iota}
+
+\newcommand{\mask}{\mathcal{E}}
+\newcommand{\namesp}{\mathcal{N}}
+
+%% various pieces of Syntax
+\def\MU #1.{\mu #1.\spac}%
+\def\Lam #1.{\lambda #1.\spac}%
+
+\newcommand{\proves}{\vdash}
+
+\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;}
+
+% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
+\newcommand{\fmapsto}[1][\mathrm{-}]{\xmapsto{#1}}
+\newcommand{\gmapsto}{\hookrightarrow}%
+\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
+
+\NewDocumentCommand\wpre{m m O{}}%
+ {{#1} \spac \prescript{}{#3}{\kern-0.2ex\{#2\}}}
+
+\newcommand{\later}{\mathord{\triangleright}}
+\newcommand{\always}{\Box{}}
+
+%% Invariants and Ghost ownership
+% PDS: Was 0pt inner, 2pt outer.
+% \boxedassert [tikzoptions] contents [name]
+\tikzstyle{boxedassert_border} = [sharp corners,line width=0.2pt]
+\NewDocumentCommand \boxedassert {O{} m o}{%
+ \tikz[baseline=(m.base)]{
+ % \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$};
+ \node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${#2}\mathstrut$};
+ \draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$);
+ }\IfNoValueF{#3}{^{\,#3}}%
+}
+\newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]}
+\newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]}
+\newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}}
+
+\newcommand{\ownPhys}[1]{\textlog{Phy}(#1)}
+
+%% View Shifts
+\NewDocumentCommand \vsGen {O{} m O{}}%
+ {\mathrel{%
+ \ifthenelse{\equal{#3}{}}{%
+ % Just one mask, or none
+ {#2}_{#1}%
+ }{%
+ % Two masks
+ \tensor*[^{#1}]{#2}{^{#3}}
+ }%
+ }}%
+\NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
+\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
+\NewDocumentCommand \vsE {O{} O{}} %
+ {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
+\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}}
+
+
+%% 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}
+\NewDocumentCommand \hoare {m m m O{}}{
+ \triple\{\}{#1}{#2}{#3}%
+ _{#4}%
+}
+
+\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}}
+% \hoareV[t] pre c post [mask]
+\NewDocumentCommand \hoareV {O{c} m m m O{}}{
+ {\begin{aligned}[#1]
+ &\curlybracket{#2} \\
+ &\quad{#3} \\
+ &{\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}
+ \end{aligned}}%
+}
+
+
+%% Some commonly used identifiers
+\newcommand{\timeless}[1]{\textlog{timeless}(#1)}
+\newcommand{\physatomic}[1]{\textlog{$#1$ phys.\ atomic}}
+\newcommand{\infinite}{\textlog{infinite}}
+
+\newcommand{\Prop}{\textlog{Prop}}
+\newcommand{\Pred}{\textlog{Pred}}
+
+\newcommand{\TRUE}{\textlog{True}}
+\newcommand{\FALSE}{\textlog{False}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% LANGUAGE SYNTAX AND SEMANTICS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\expr}{e}
+\newcommand{\val}{v}
+\newcommand{\valB}{w}
+\newcommand{\state}{\sigma}
+\newcommand{\step}{\ra}
+\newcommand{\lctx}{K}
+
+\newcommand{\toval}{\mathit{val}}
+\newcommand{\ofval}{\mathit{expr}}
+\newcommand{\atomic}{\mathit{atomic}}
+\newcommand{\Lang}{\Lambda}
+
+\newcommand{\tpool}{T}
+
+\newcommand{\cfg}[2]{{#1};{#2}}
+
+
+
+\endinput
diff --git a/docs/logic.tex b/docs/logic.tex
index 5ace55b79b2a99de72e9c25119aa1890ed749651..51b4d0290a22c785c871f7baf6de53b40cb6791a 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -72,7 +72,7 @@ To instantiate Iris, you need to define the following parameters:
As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language.
You have to make sure that $\SigType$ includes the base types:
\[
- \SigType \supseteq \{ \textsort{Val}, \textsort{Expr}, \textsort{State}, \textsort{M}, \textsort{InvName}, \textsort{InvMask}, \Prop \}
+ \SigType \supseteq \{ \textlog{Val}, \textlog{Expr}, \textlog{State}, \textlog{M}, \textlog{InvName}, \textlog{InvMask}, \Prop \}
\]
Elements of $\SigType$ are ranged over by $\sigtype$.
@@ -95,14 +95,14 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\begin{align*}
\type ::={}&
\sigtype \mid
- \unitsort \mid
+ 1 \mid
\type \times \type \mid
\type \to \type
\\[0.4em]
\term, \prop, \pred ::={}&
\var \mid
\sigfn(\term_1, \dots, \term_n) \mid
- \unitval \mid
+ () \mid
(\term, \term) \mid
\pi_i\; \term \mid
\Lam \var:\type.\term \mid
@@ -144,16 +144,16 @@ We introduce additional metavariables ranging over terms and generally let the c
\begin{array}{r|l}
\text{metavariable} & \text{type} \\\hline
\term, \termB & \text{arbitrary} \\
- \val, \valB & \textsort{Val} \\
- \expr & \textsort{Expr} \\
- \state & \textsort{State} \\
+ \val, \valB & \textlog{Val} \\
+ \expr & \textlog{Expr} \\
+ \state & \textlog{State} \\
\end{array}
\qquad\qquad
\begin{array}{r|l}
\text{metavariable} & \text{type} \\\hline
- \iname & \textsort{InvName} \\
- \mask & \textsort{InvMask} \\
- \melt, \meltB & \textsort{M} \\
+ \iname & \textlog{InvName} \\
+ \mask & \textlog{InvMask} \\
+ \melt, \meltB & \textlog{M} \\
\prop, \propB, \propC & \Prop \\
\pred, \predB, \predC & \type\to\Prop \text{ (when $\type$ is clear from context)} \\
\end{array}
@@ -197,7 +197,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
}
%%% products
\and
- \axiom{\vctx \proves \wtt{\unitval}{\unitsort}}
+ \axiom{\vctx \proves \wtt{()}{1}}
\and
\infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}}
{\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}}
@@ -214,10 +214,10 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
{\vctx \proves \wtt{\term(\termB)}{\type'}}
%%% monoids
\and
- \infer{}{\vctx \proves \wtt{\munit}{\textsort{M} \to \textsort{M}}}
+ \infer{}{\vctx \proves \wtt{\munit}{\textlog{M} \to \textlog{M}}}
\and
- \infer{\vctx \proves \wtt{\melt}{\textsort{M}} \and \vctx \proves \wtt{\meltB}{\textsort{M}}}
- {\vctx \proves \wtt{\melt \mtimes \meltB}{\textsort{M}}}
+ \infer{\vctx \proves \wtt{\melt}{\textlog{M}} \and \vctx \proves \wtt{\meltB}{\textlog{M}}}
+ {\vctx \proves \wtt{\melt \mtimes \meltB}{\textlog{M}}}
%%% props and predicates
\\
\axiom{\vctx \proves \wtt{\FALSE}{\Prop}}
@@ -257,15 +257,15 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{
\vctx \proves \wtt{\prop}{\Prop} \and
- \vctx \proves \wtt{\iname}{\textsort{InvName}}
+ \vctx \proves \wtt{\iname}{\textlog{InvName}}
}{
\vctx \proves \wtt{\knowInv{\iname}{\prop}}{\Prop}
}
\and
- \infer{\vctx \proves \wtt{\melt}{\textsort{M}}}
+ \infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
{\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
\and
- \infer{\vctx \proves \wtt{\state}{\textsort{State}}}
+ \infer{\vctx \proves \wtt{\state}{\textlog{State}}}
{\vctx \proves \wtt{\ownPhys{\state}}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
@@ -276,16 +276,16 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{
\vctx \proves \wtt{\prop}{\Prop} \and
- \vctx \proves \wtt{\mask}{\textsort{InvMask}} \and
- \vctx \proves \wtt{\mask'}{\textsort{InvMask}}
+ \vctx \proves \wtt{\mask}{\textlog{InvMask}} \and
+ \vctx \proves \wtt{\mask'}{\textlog{InvMask}}
}{
\vctx \proves \wtt{\pvs[\mask][\mask'] \prop}{\Prop}
}
\and
\infer{
- \vctx \proves \wtt{\expr}{\textsort{Expr}} \and
- \vctx,\var:\textsort{Val} \proves \wtt{\term}{\Prop} \and
- \vctx \proves \wtt{\mask}{\textsort{InvMask}}
+ \vctx \proves \wtt{\expr}{\textlog{Expr}} \and
+ \vctx,\var:\textlog{Val} \proves \wtt{\term}{\Prop} \and
+ \vctx \proves \wtt{\mask}{\textlog{InvMask}}
}{
\vctx \proves \wtt{\wpre{\expr}{\Ret\var.\term}[\mask]}{\Prop}
}
@@ -524,7 +524,7 @@ This is entirely standard.
{}{\prop[\val/\var] \proves \wpre{\val}{\Ret\var.\prop}[\mask]}
\infer[wp-mono]
-{\mask_1 \subseteq \mask_2 \and \var:\textsort{val}\mid\prop \proves \propB}
+{\mask_1 \subseteq \mask_2 \and \var:\textlog{val}\mid\prop \proves \propB}
{\wpre\expr{\Ret\var.\prop}[\mask_1] \proves \wpre\expr{\Ret\var.\propB}[\mask_2]}
\infer[pvs-wp]
diff --git a/docs/model.tex b/docs/model.tex
index c2391766731ed2b0994a027670c68b55ee01ad4b..2a7fd7bc71354630fdc45237c9731c18a3fdf6fc 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -227,14 +227,14 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
$\mathit{inv}$ is well-defined: $\mathit{inv}(\iota, p)$ is a valid proposition (this amounts to showing non-expansiveness), and $\mathit{inv}$ itself is a non-expansive map.
\end{lem}
-\typedsection{World satisfaction}{\fullSat{-}{-}{-}{-} :
+\typedsection{World satisfaction}{\wsat{-}{-}{-}{-} :
\textdom{State} \times
\pset{\mathbb{N}} \times
\textdom{Res} \times
\textdom{World} \to \psetdown{\mathbb{N}} \in {\cal U}}
\ralf{Make this Dave-compatible: Explicitly compose all the things in $s$}
\begin{align*}
- \fullSat{\state}{\mask}{\rs}{W} &=
+ \wsat{\state}{\mask}{\rs}{W} &=
\begin{aligned}[t]
\{\, n + 1 \in \mathbb{N} \mid &\Exists \rsB:\mathbb{N} \fpfn \textdom{Res}. (\rs \rtimes \rsB).\pres = \state \land{}\\
&\quad \All \iota \in \dom(W). \iota \in \dom(W) \leftrightarrow \iota \in \dom(\rsB) \land {}\\
@@ -242,7 +242,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\end{aligned}
\end{align*}
\begin{lem}\label{lem:fullsat-nonexpansive}
- $\fullSat{-}{-}{-}{-}$ is well-defined: It maps into $\psetdown{\mathbb{N}}$. (There is no need for it to be a non-expansive map, it doesn't itself live in $\cal U$.)
+ $\wsat{-}{-}{-}{-}$ is well-defined: It maps into $\psetdown{\mathbb{N}}$. (There is no need for it to be a non-expansive map, it doesn't itself live in $\cal U$.)
\end{lem}
\begin{lem}\label{lem:fullsat-weaken-mask}
@@ -252,7 +252,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\All \mask_1, \mask_2 \in \Delta(\pset{\mathbb{N}}).
\All \rs, \rsB \in \Delta(\textdom{Res}).
\All W \in \textdom{World}. \\&
- \mask_1 \subseteq \mask_2 \implies (\fullSat{\state}{\mask_2}{\rs}{W}) \subseteq (\fullSat{\state}{\mask_1}{\rs}{W})
+ \mask_1 \subseteq \mask_2 \implies (\wsat{\state}{\mask_2}{\rs}{W}) \subseteq (\wsat{\state}{\mask_1}{\rs}{W})
\end{align*}
\end{lem}
@@ -297,9 +297,9 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\begin{aligned}[t]
\{\, (n, \rs) &\mid \All W_F \geq W. \All \rs_F, \mask_F, \state. \All k \leq n.\\
&\qquad
- k \in (\fullSat{\state}{\mask_1 \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\
+ k \in (\wsat{\state}{\mask_1 \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \land k > 0 \land \mask_F \sep (\mask_1 \cup \mask_2) \implies{} \\
&\qquad
- \Exists W' \geq W_F. \Exists \rs'. k \in (\fullSat{\state}{\mask_2 \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(W')
+ \Exists W' \geq W_F. \Exists \rs'. k \in (\wsat{\state}{\mask_2 \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(W')
\,\}
\end{aligned}
\end{align*}
@@ -394,19 +394,19 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
% \begin{align*}
% \mathit{wp}_\mask(\expr, q) &\eqdef \Lam W.
% \begin{aligned}[t]
-% \{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \implies{}\\
+% \{\, (n, \rs) &\mid \All W_F \geq W; k \leq n; \rs_F; \state; \mask_F \sep \mask. k > 0 \land k \in (\wsat{\state}{\mask \cup \mask_F}{\rs \rtimes \rs_F}{W_F}) \implies{}\\
% &\qquad
% (\expr \in \textdom{Val} \implies \Exists W' \geq W_F. \Exists \rs'. \\
% &\qquad\qquad
-% k \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\
+% k \in (\wsat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k, \rs') \in q(\expr)(W'))~\land \\
% &\qquad
% (\All\ectx,\expr_0,\expr'_0,\state'. \expr = \ectx[\expr_0] \land \cfg{\state}{\expr_0} \step \cfg{\state'}{\expr'_0} \implies \Exists W' \geq W_F. \Exists \rs'. \\
% &\qquad\qquad
-% k - 1 \in (\fullSat{\state'}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
+% k - 1 \in (\wsat{\state'}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land (k-1, \rs') \in wp_\mask(\ectx[\expr_0'], q)(W'))~\land \\
% &\qquad
% (\All\ectx,\expr'. \expr = \ectx[\fork{\expr'}] \implies \Exists W' \geq W_F. \Exists \rs', \rs_1', \rs_2'. \\
% &\qquad\qquad
-% k - 1 \in (\fullSat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land \rs' = \rs_1' \rtimes \rs_2'~\land \\
+% k - 1 \in (\wsat{\state}{\mask \cup \mask_F}{\rs' \rtimes \rs_F}{W'}) \land \rs' = \rs_1' \rtimes \rs_2'~\land \\
% &\qquad\qquad
% (k-1, \rs_1') \in \mathit{wp}_\mask(\ectx[\textsf{fRet}], q)(W') \land
% (k-1, \rs_2') \in \mathit{wp}_\top(\expr', \Lam\any. \top)(W'))
diff --git a/docs/setup.tex b/docs/setup.tex
index dffcfb29c5cc15f2ffdbe1d4624516d0c7583351..f438ee57e7d73082efe48ce671f1de37c4b0a481 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -18,20 +18,19 @@
\usepackage{\basedir mathpartir}
\usepackage{array}
-\usepackage{tabu}
+%\usepackage{tabu}
\usepackage{dashbox}
\usepackage{tensor}
\usepackage{\basedir pftools}
+\usepackage{\basedir iris}
\usepackage{xcolor} % for print version
\usepackage{graphicx}
-\usepackage{tikz}
-\usepackage{scalerel}
-\usepackage{rotating}
+%\usepackage{rotating}
\usepackage{xparse}
\usepackage{xstring}
\usepackage{semantic}
@@ -61,16 +60,6 @@
\definecolor{CiteColor}{rgb}{0.55,0.0,0.3}
\definecolor{HighlightColor}{rgb}{0.0,0.0,0.0}
-\usetikzlibrary{shapes}
-%\usetikzlibrary{snakes}
-\usetikzlibrary{arrows}
-\usetikzlibrary{calc}
-\usetikzlibrary{arrows.meta}
-\tikzstyle{state}=[circle, draw, minimum size=1.2cm, align=center]
-\tikzstyle{trans}=[arrows={->[scale=1.4]}]
-
-\tikzstyle{layer}=[rounded corners=2pt, thin, align=center, draw, minimum width=4.2cm,minimum height=0.8cm]
-
\definecolor{grey}{rgb}{0.5,0.5,0.5}
\definecolor{red}{rgb}{1,0,0}
@@ -132,307 +121,6 @@
\let\dave\hush%
}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% MATH SYMBOLS & NOTATION & IDENTIFIERS
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
-\newcommand{\bigast}{\Sep}
-
-\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}} % bad name; it's a different "sep"
-
-\newcommand{\ALT}{\ |\ }
-
-\newcommand\dplus{\mathbin{+\kern-1.0ex+}}
-
-\newcommand{\upclose}{\mathord{\uparrow}}
-
-\newcommand{\spac}{\;} % a space
-
-\def\All #1.{\forall #1.\spac}%
-\def\Exists #1.{\exists #1.\spac}%
-\def\Ret #1.{#1.\spac}%
-
-\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
-\newcommand{\unitval}{()}%
-
-\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{\ra}{\rightarrow}
-\newcommand{\Ra}{\Rightarrow}
-\newcommand{\Lra}{\Leftrightarrow}
-\newcommand\monra{}%\xrightarrow{\kern-0.25ex\textrm{mon}\kern-0.25ex}}
-
-\newcommand{\eqdef}{\triangleq}
-
-\newcommand{\restr}[2]{\lfloor #1 \rfloor_{#2}}
-\newcommand{\pset}[1]{\wp(#1)} % Powerset
-\newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
-
-\newcommand{\dom}{\mathrm{dom}}
-\newcommand{\cod}{\mathrm{cod}}
-\newcommand{\chain}{\mathrm{chain}}
-
-\newcommand{\IF}{\mathrel{\text{if}}}
-\newcommand{\WHEN}{\textrm{when }}
-
-\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
-\newcommand*\set[1]{\left\{#1\right\}}
-
-\newenvironment{inbox}[1][]{
- \begin{array}[#1]{@{}l@{}}
-}{
- \end{array}
-}
-
-\newcommand{\tabubox}[2][]{%
- \begin{tabu}{@{#1}X[1,l,m]@{}}%
- #2 %
- \end{tabu}%
-}
-
-\newcommand{\Func}{F} % functor
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\textdom}[1]{\textit{#1}}
-
-\newcommand{\wIso}{\xi}
-
-\newcommand{\rs}{r}
-\newcommand{\rsB}{s}
-
-\newcommand{\pres}{\pi}
-\newcommand{\wld}{w}
-\newcommand{\ghostRes}{g}
-
-%% Various pieces of syntax
-\newcommand{\fullSat}[4]{#1 \models_{#2} #3; #4}
-
-\newcommand{\wtt}[2]{#1 : #2} % well-typed term
-
-\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}}
-\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}}
-\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
-\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
-\newcommand{\latert}{\mathord{\blacktriangleright}}
-
-\newcommand{\Sem}[1]{\llbracket #1 \rrbracket}
-
-\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{\(#1\)}}}
-\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}}
-
-
-%% Some commonly used identifiers
-\newcommand{\UPred}{\textdom{UPred}}
-\newcommand{\SPred}{\textdom{SPred}}
-
-\newcommand{\PropDom}{\textdom{Prop}}
-\newcommand{\PredDom}{\textdom{Pred}}
-
-\newcommand{\COFEs}{\mathcal{U}} % category of COFEs
-\newcommand{\iFunc}{\Sigma}
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\textmon}[1]{\textsc{#1}}
-
-\newcommand{\monoid}{M}
-\newcommand{\mval}{V}
-
-\newcommand{\melt}{a}
-\newcommand{\meltB}{b}
-\newcommand{\meltC}{c}
-\newcommand{\melts}{A}
-\newcommand{\meltsB}{B}
-
-\newcommand{\mcar}[1]{|#1|}
-\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
-\newcommand{\munit}{\mathord{\varepsilon}}
-\newcommand{\mtimes}{\mathbin{\cdot}}
-\newcommand{\mdiv}{\mathbin{\div}}
-
-\newcommand{\mupd}{\rightsquigarrow}
-\newcommand{\mincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\leq}}}}
-
-\newcommand{\CMRAs}{\mathcal{R}} % category of CMRAs
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\textlog}[1]{\textsf{#1}}
-\newcommand{\textsort}[1]{\textlog{#1}}
-
-\newcommand{\Sig}{\mathcal{S}}
-\newcommand{\SigType}{\mathcal{T}}
-\newcommand{\SigFn}{\mathcal{F}}
-\newcommand{\SigAx}{\mathcal{A}}
-\newcommand{\sigtype}{T}
-\newcommand{\sigfn}{F}
-\newcommand{\sigax}{A}
-
-\newcommand{\type}{\tau}
-
-\newcommand{\var}{x}
-\newcommand{\varB}{y}
-\newcommand{\varC}{z}
-
-\newcommand{\term}{t}
-\newcommand{\termB}{u}
-\newcommand{\termVal}{V}
-
-\newcommand{\vctx}{\Gamma}
-\newcommand{\pfctx}{\Theta}
-
-\newcommand{\prop}{P}
-\newcommand{\propB}{Q}
-\newcommand{\propC}{R}
-
-\newcommand{\pred}{\varphi}
-\newcommand{\predB}{\psi}
-\newcommand{\predC}{\zeta}
-
-\newcommand{\gname}{\gamma}
-\newcommand{\iname}{\iota}
-\newcommand{\inameB}{\iota'}
-
-\newcommand{\mask}{\mathcal{E}}
-\newcommand{\namesp}{\mathcal{N}}
-
-%% various pieces of Syntax
-\newcommand{\unitsort}{1}% \unit is bold.
-
-\def\MU #1.{\mu #1.\spac}%
-\def\Lam #1.{\lambda #1.\spac}%
-
-\newcommand{\proves}{\vdash}
-
-\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;}
-
-% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
-\newcommand{\fmapsto}[1][\mathrm{-}]{\xmapsto{#1}}
-\newcommand{\gmapsto}{\hookrightarrow}%
-\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
-
-\NewDocumentCommand\wpre{m m O{}}%
- {{#1} \spac \prescript{}{#3}{\kern-0.2ex\{#2\}}}
-
-\newcommand{\later}{\mathord{\triangleright}}
-\newcommand{\always}{\Box{}}
-
-%% Invariants and Ghost ownership
-% PDS: Was 0pt inner, 2pt outer.
-% \boxedassert [tikzoptions] contents [name]
-\tikzstyle{boxedassert_border} = [sharp corners,line width=0.2pt]
-\NewDocumentCommand \boxedassert {O{} m o}{%
- \tikz[baseline=(m.base)]{
- % \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$};
- \node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${#2}\mathstrut$};
- \draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$);
- }\IfNoValueF{#3}{^{\,#3}}%
-}
-\newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]}
-\newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]}
-\newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}}
-
-\newcommand{\ownPhys}[1]{\textlog{Phy}(#1)}
-
-%% View Shifts
-\NewDocumentCommand \vsGen {O{} m O{}}%
- {\mathrel{%
- \ifthenelse{\equal{#3}{}}{%
- % Just one mask, or none
- {#2}_{#1}%
- }{%
- % Two masks
- \tensor*[^{#1}]{#2}{^{#3}}
- }%
- }}%
-\NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
-\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
-\NewDocumentCommand \vsE {O{} O{}} %
- {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
-\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}}
-
-
-%% 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}
-\NewDocumentCommand \hoare {m m m O{}}{
- \triple\{\}{#1}{#2}{#3}%
- _{#4}%
-}
-
-\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}}
-% \hoareV[t] pre c post [mask]
-\NewDocumentCommand \hoareV {O{c} m m m O{}}{
- {\begin{aligned}[#1]
- &\curlybracket{#2} \\
- &\quad{#3} \\
- &{\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}
- \end{aligned}}%
-}
-
-
-%% Some commonly used identifiers
-\newcommand{\timeless}[1]{\textlog{timeless}(#1)}
-\newcommand{\physatomic}[1]{\textlog{$#1$ phys.\ atomic}}
-\newcommand{\infinite}{\textlog{infinite}}
-
-\newcommand{\Prop}{\textlog{Prop}}
-\newcommand{\Pred}{\textlog{Pred}}
-
-\newcommand{\TRUE}{\textlog{True}}
-\newcommand{\FALSE}{\textlog{False}}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% LANGUAGE SYNTAX AND SEMANTICS
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newcommand{\expr}{e}
-\newcommand{\val}{v}
-\newcommand{\valB}{w}
-\newcommand{\state}{\sigma}
-\newcommand{\step}{\ra}
-\newcommand{\lctx}{K}
-
-\newcommand{\toval}{\mathit{val}}
-\newcommand{\ofval}{\mathit{expr}}
-\newcommand{\atomic}{\mathit{atomic}}
-\newcommand{\Lang}{\Lambda}
-
-\newcommand{\tpool}{T}
-
-\newcommand{\cfg}[2]{{#1};{#2}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% DERIVED CONSTRUCTIONS