Skip to content
Snippets Groups Projects
Commit 5dfdd35c authored by Ralf Jung's avatar Ralf Jung
Browse files

move the iris macros to a dedicated package

parent 101b65fc
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
docs/iris.sty 0 → 100644
+ 300
− 0
View file @ 5dfdd35c
\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
docs/logic.tex
+ 22
− 22
View file @ 5dfdd35c
......@@ -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]
......
docs/model.tex
+ 10
− 10
View file @ 5dfdd35c
......@@ -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'))
......
docs/setup.tex
+ 3
− 315
View file @ 5dfdd35c
......@@ -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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment