%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% PACKAGES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{mathtools}
%\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{stmaryrd}
\SetSymbolFont{stmry}{bold}{U}{stmry}{m}{n} % this fixes warnings when \boldsymbol is used with stmaryrd included
\usepackage{mathpartir}
\usepackage{array}\extrarowheight=\jot % else, arrays are scrunched compared to, say, aligned
\newcolumntype{.}{@{}}
% Array {rMcMl} modifies array {rcl}, putting mathrel-style spacing
% around the centered column. (We used this, for example, in laying
% out some of Iris' axioms. Generally, aligned is simpler but aligned
% does not work in mathpar because \\ inherits mathpar's 2em vskip.)
% The capital M stands for THICKMuskip. The smaller medmuskip would be
% right for mathbin-style spacing.
\newcolumntype{M}{@{\mskip\thickmuskip}}
\usepackage{tabu}%\tabulinesep=_0pt^\jot
\usepackage{dashbox}
%\usepackage{arydshln}
%\setlength{\dashlinegap}{1pt}
%\setlength{\dashlinedash}{3pt}
\usepackage{hyperref}
\hypersetup{%
linktocpage=true, pdfstartview=FitV,
breaklinks=true, pageanchor=true, pdfpagemode=UseOutlines,
plainpages=false, bookmarksnumbered, bookmarksopen=true, bookmarksopenlevel=3,
hypertexnames=true, pdfhighlight=/O,
colorlinks=true,linkcolor=LinkColor,citecolor=CiteColor,
urlcolor=LinkColor
}
\newcommand*{\Sref}[1]{\hyperref[#1]{\S\ref*{#1}}}
\newcommand*{\secref}[1]{\hyperref[#1]{Section~\ref*{#1}}}
\newcommand*{\lemref}[1]{\hyperref[#1]{Lemma~\ref*{#1}}}
\newcommand{\corref}[1]{\hyperref[#1]{Cor.~\ref*{#1}}}
\newcommand*{\defref}[1]{\hyperref[#1]{Definition~\ref*{#1}}}
\newcommand*{\egref}[1]{\hyperref[#1]{Example~\ref*{#1}}}
\newcommand*{\appendixref}[1]{\hyperref[#1]{Appendix~\ref*{#1}}}
\newcommand*{\figref}[1]{\hyperref[#1]{Figure~\ref*{#1}}}
\newcommand*{\tabref}[1]{\hyperref[#1]{Table~\ref*{#1}}}
\usepackage{pftools}
%\usepackage{pfsteps}
%\newcommand*{\pflab}[1]{\steppfcounter[#1](\thepfcounter)}
%\newcommand*{\pftag}[1]{\steppfcounter[#1]\tag{\thepfcounter}}
%\renewcommand\byCasesEveryCase{} % turn off counter reset on cases
%\renewcommand\byCasesEveryOtherwise{}
%\usepackage[monochrome]{color} % for print version
\usepackage{xcolor} % for print version
\usepackage{graphicx}
\definecolor{StringRed}{rgb}{.637,0.082,0.082}
\definecolor{CommentGreen}{rgb}{0.0,0.55,0.3}
\definecolor{KeywordBlue}{rgb}{0.0,0.3,0.55}
\definecolor{LinkColor}{rgb}{0.55,0.0,0.3}
\definecolor{CiteColor}{rgb}{0.55,0.0,0.3}
\definecolor{HighlightColor}{rgb}{0.0,0.0,0.0}
\usepackage{tikz}
\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}
%\renewcommand{\pfcounteranchor}[1]
% {{\scriptsize#1\color{grey}.}\ \ }
% {{\scriptsize{\color{grey}(}#1{\color{grey})}}\ \ }
% \usepackage[all,cmtip]{xy}
% \usepackage{diagxy}
%\theoremstyle{definition}
%\newtheorem{prop}{Prop}
\newtheorem{defn}{Definition}
\newtheorem{cor}{Corollary}
\newtheorem{conj}{Conj}
\newtheorem{lem}{Lemma}
\newtheorem{thm}{Theorem}
\newtheorem{exercise}{Exercise}
\usepackage{rotating}
\usepackage{xparse}
\usepackage{xstring}
\usepackage{semantic}
\usepackage{csquotes}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% MACROS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\changes}{{\bf\color{red}{Changes}}}
\newcommand{\TODO}{\vskip 4pt {\color{red}\bf TODO}}
%\newcommand{\bigast}{\scalebox{3}{\raisebox{-0.3ex}{$\ast$}}}
%\newcommand{\bigtimes}{\scalebox{2.5}{\raisebox{-0.3ex}{$\times$}}}
\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
\newcommand{\bigast}{\Sep}
\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}} % bad name; it's a different "sep"
\newcommand{\kw}[1]{\textbf{\textsf{#1}}}
\newcommand{\ALT}{\ |\ }
\newenvironment{pf}
{\resetpfcounter\begin{proof}}
{\end{proof}}
% superscript to the left
\def\presuper#1#2%
{\mathop{}%
\mathopen{\vphantom{#2}}^{#1}%
\kern-\scriptspace%
#2}
\newcommand{\upclose}{\mathord{\uparrow}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% METAVARIABLES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\aexpr}{a}
\newcommand{\expr}{e}
\newcommand{\type}{\tau}
\newcommand{\htype}{\sigma}
\newcommand{\ctype}{\sigma}
\newcommand{\heap}{h}
\newcommand{\tyvar}{\alpha}
\newcommand{\tyvarB}{\beta}
\newcommand{\val}{v}
\newcommand{\valB}{w}
\newcommand{\hval}{u}
\newcommand{\tls}{L}
\newcommand{\tlsVar}{L}
\newcommand{\cenv}{\Omega}
\newcommand{\tenv}{\Gamma}
\newcommand{\tvenv}{\Delta}
%\newcommand{\vctx}{\mathcal{X}}
\newcommand{\pvar}{p}
\newcommand{\pvarB}{q}
%\newcommand{\pvarC}{r}
\newcommand{\ectx}{K}
\newcommand{\tpool}{T}
% \newcommand{\progexpr}{p}
% \newcommand{\progctx}{D}
\newcommand{\subst}{\gamma}
\newcommand{\island}{I}
\newcommand{\sisland}{\iota}
%\newcommand{\islands}{\omega}
\newcommand{\islands}{\mathbf{\island}}
\newcommand{\predinterp}{\PRED}
\newcommand{\propinterp}{\mathcal{P}}
\newcommand{\PROP}{\mathcal{P}}
\newcommand{\PROPB}{\mathcal{Q}}
\newcommand{\interp}{\textrm{interp}}
\newcommand{\interps}{\textrm{interpAll}}
\newcommand{\restype}{\theta}
\newcommand{\restypes}{\boldsymbol{\theta}}
\newcommand{\aprop}{{\color{red}A}}
\newcommand{\prop}{P}
\newcommand{\propB}{Q}
\newcommand{\propC}{R}
\newcommand{\pred}{\varphi}
\newcommand{\predB}{\psi}
\newcommand{\predC}{\zeta}
\newcommand{\Prop}{\textlog{Prop}}
\newcommand{\Pred}{\textlog{Pred}}
\newcommand{\PropDom}{\textit{Prop}}
\newcommand{\PredDom}{\textit{Pred}}
% \newcommand{\Prop}{\mathbb{B}}
% \newcommand{\Pred}{\mathbb{P}}
\newcommand{\rs}{r}
\newcommand{\rsB}{s}
%\newcommand{\propSet}{\mathcal{P}}
%\newcommand{\apropSet}{\mathcal{A}}
%\newcommand{\pfctx}{\mathcal{C}}
\newcommand{\vctx}{\Gamma}
\newcommand{\pfctx}{\Theta}
\newcommand{\PCLCTX}{Prop context}
\newcommand{\PCVARS}{Variables}
\newcommand{\PContextStyle}[1]{\fbox{\extrasepB{0.5pt}\color{CommentGreen}$#1$}}
%\newcommand{\PContextStyle}[1]{\ensuremath{\color{CommentGreen}\left[#1\right]}}
\newcommand{\PContext}[1]{\PContextStyle{\begin{array}{@{}l@{}}\textbf{\PCLCTX: }\\#1\end{array}}}
\newcommand{\PContextB}[2]{\PContextStyle{\begin{array}{@{}l@{}}
\textbf{\PCLCTX: }\hspace{\stretch{1}}\textbf{\PCVARS: }{#1}
\\#2
\end{array}}}
\newcommand{\PContextC}[2]{\PContextStyle{\begin{array}{@{}l@{}}
\textbf{\PCLCTX: }\qquad\textbf{\PCVARS: }{#1}
\\#2
\end{array}}}
\newcommand{\PContextD}[2]{\PContextStyle{
\textbf{\PCLCTX: }{#2}\qquad\textbf{\PCVARS: }{#1}}}
\newcommand{\PContextE}[1]{\PContextStyle{\textbf{\PCVARS: }{#1}}}
\newcommand{\assert}{\varphi}
\newcommand{\assertB}{\psi}
\newcommand{\PRED}{\Phi}
%% \newcommand{\pname}{\pi}
%% \newcommand{\prot}{\pi}
%% \newcommand{\prots}{\boldsymbol{\pi}}
%% \newcommand{\protSet}{\mathcal{N}}
\newcommand{\iname}{\iota}
\newcommand{\inameB}{\iota'}
\newcommand{\inv}{I}
\newcommand{\invs}{\mathcal{I}}
\newcommand{\mask}{\mathcal{E}}
\newcommand{\consistent}{\textsf{consistent}}
\newcommand{\fullSat}[4]{#1 \models_{#2} #3; #4}
\newcommand{\fullNSat}[6]{#2 \models_{#3}^{#1} #4; #5; #6}
\newcommand{\state}{\varsigma}
\newcommand{\prescar}{\Pi}
\newcommand{\pres}{\pi}
\newcommand{\erasestate}[1]{|#1|_\state}
\newcommand{\eraseexp}[1]{|#1|_\expr}
\newcommand{\var}{x}
\newcommand{\varB}{y}
\newcommand{\varC}{z}
%\newcommand{\VAL}{d}
\newcommand{\ectxVar}{\kappa}
\newcommand{\term}{t}
\newcommand{\termB}{u}
\newcommand{\termVal}{V}
\newcommand{\sort}{\sigma}
\newcommand{\SigNat}{\Sigma}
\newcommand{\SigType}{\mathcal{T}}
\newcommand{\SigFn}{\mathcal{F}}
\newcommand{\sigfn}{F}
\newcommand{\tmap}{B}
\newcommand{\ttokSet}{I}
\newcommand{\monoid}{M}
\newcommand{\mcar}[1]{|#1|}
\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
\newcommand{\mzero}{\bot}
\newcommand{\munit}{\mathord{\varepsilon}}
\newcommand{\mtimes}{\mathbin{\cdot}}
%\newcommand{\mvar}{a}
%\newcommand{\mvarB}{b}
\newcommand{\melt}{a}
\newcommand{\meltB}{b}
\newcommand{\meltC}{c}
\newcommand{\melts}{A}
\newcommand{\meltsB}{B}
\newcommand{\ghostRes}{g}
\newcommand{\gtimes}{\bullet}
\newcommand{\monoids}{\textrm{ProdMonoid}}
\newcommand{\gname}{\gamma}
\newcommand{\valid}{\textsf{valid}}
\newcommand{\textmon}[1]{\textsc{#1}}
\newcommand{\textstate}[1]{\textsf{#1}}
\newcommand{\texttok}[1]{\textsc{#1}}
\newcommand{\atlas}{A}
\newcommand{\chmap}{C}
\newcommand{\bag}{M}
\newcommand{\chan}{c}
\newcommand{\chanmaps}{\Yleft}
\newcommand{\fchanmaps}[1][-]{\stackrel{#1}{\chanmaps}}
\newcommand{\msg}{m}
\newcommand{\dest}{d}
\let\mkbag=\bag
\newcommand{\bagB}{N}
\newcommand{\emptybag}{\emptyset}
\newcommand{\MASK}{InvMask}
\newcommand{\CHAN}{Chan}
\newcommand{\VAR}{Var}
\newcommand{\VAL}{Val}
\newcommand{\EXP}{Exp}
\newcommand{\ECTX}{Ctx}
\newcommand{\hole}{[]}
\newcommand{\BAG}{Bag}
\newcommand{\STATE}{State}
\newcommand{\rvar}{r}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SYNTAX
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\All #1.{\forall #1.\;}%
\def\Exists #1.{\exists #1.\;}%
\def\Absp #1.{({#1}).\;}
\def\Ret #1.{#1.\;}%
\def\Lam #1.{\lambda #1.\;}%
\def\MU #1.{\mu #1.\;}%
\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
\newcommand{\unitval}{()}%
%\newcommand{\emptytenv}{\bullet}
%\newcommand{\fn}[2]{\lambda {#1}. {#2}}
%\newcommand{\app}[2]{{#1}\;{#2}}
%\newcommand{\pair}[1]{\llparenthesis #1 \rrparenthesis}
%\newcommand{\true}{\kw{true}}
%\newcommand{\false}{\kw{false}}
%\newcommand{\ite}[3]{\kw{if}\ #1\ \kw{then}\ #2\ \kw{else}\ #3}
%\newcommand{\new}{\kw{new}\;}
%\newcommand{\deref}[1]{\kw{get}\;{#1}}
%\newcommand{\assign}[2]{{#1}\;:=\;{#2}}
%\newcommand{\cas}{\kw{CAS}}
%\newcommand{\unfold}{\kw{unfold}\ }
%\newcommand{\fold}{\kw{fold}\ }
%\newcommand{\unroll}{\kw{unroll}\ }
%\newcommand{\roll}{\kw{roll}\ }
%\newcommand{\rec}[2]{\kw{rec}\; {#1}.{#2}}
%\newcommand{\recf}[3]{\kw{rec}\;{#1}({#2}).{#3}}
%\newcommand{\recf}[3]{\mu{#1}({#2}).{#3}}
%\newcommand{\fix}[2]{\kw{fix}\ {#1}.{#2}}
%\newcommand{\pack}[1]{\kw{pack}\;{#1}}
%\newcommand{\unpack}[3]{\kw{unpack}\ #1\ \kw{as}\ #2\ \kw{in}\ #3}
%\newcommand{\atomic}[1]{\kw{atomic}\;{#1}}
%\newcommand{\inatomic}[1]{\kw{inatomic}\;{#1}}
%\newcommand{\bind}[2]{\kw{let}\;{#1}\;\kw{in}\;{#2}}
%
%\newcommand{\lnew}{\kw{newLcl}}
%\newcommand{\lderef}[1]{\kw{getLcl}({#1})}
%\newcommand{\lassign}[2]{\kw{setLcl}({#1},{#2})}
%
%\newcommand{\makeAtomic}{\textsf{mkAtomic}}
%\newcommand{\withLock}{\textsf{withLock}}
\newcommand{\inj}[2]{\kw{inj}_{#1}\;#2}
\newcommand{\inl}[1]{\inj{1}{#1}}
\newcommand{\inr}[1]{\inj{2}{#1}}
\newcommand{\prj}[2]{\kw{prj}_{#1}\;#2}
\newcommand{\prl}[1]{\prj{1}{#1}}
\newcommand{\prr}[1]{\prj{2}{#1}}
%% \newcommand{\match}[5]{\kw{case}\;{#1}\;\kw{of}\;
%% \inl{#2} \Rightarrow {#3}\;|\;
%% \inr{#4} \Rightarrow {#5}}
\newcommand{\match}[5]{
\kw{case}({#1}, #2 \Rightarrow {#3}, {#4} \Rightarrow {#5})}
\newcommand{\tabs}[1]{\Lambda. {#1}}
\newcommand{\tapp}[1]{{#1}\;\any}
\newcommand{\fork}[1]{\kw{fork}\;{#1}}
\newcommand{\forkid}[1]{\textsf{forkID}\;{#1}}
\newcommand{\join}[1]{\textsf{join}\;{#1}}
\newcommand{\tryAcq}{\textsf{tryAcq}}
\newcommand{\acq}{\textsf{acq}}
\newcommand{\rel}{\textsf{rel}}
%\newcommand{\sync}[2]{\textsf{sync}(#1)\;\{\;{#2}\;\}}
\newcommand{\sync}{\textsf{sync}}
\newcommand{\mkSync}{\textsf{mkSync}}
\definecolor{Erased}{rgb}{0.35,0.35,0.35}
\definecolor{ErasedLight}{rgb}{0.5,0.5,0.5}
\newcommand{\erased}[1]{{\color{ErasedLight}[}{\color{Erased}#1}{\color{ErasedLight}]}}
%\newcommand{\erased}[1]{\underline{#1}}
\newcommand{\bool}{\kw{B}}
\newcommand{\nat}{\kw{N}}
\newcommand{\unit}{\kw{1}}
%% \newcommand{\b\ool}{\kw{bool}}
%% \newcommand{\nat}{\kw{nat}}
%% \newcommand{\unit}{\kw{unit}}
%\newcommand{\refTy}[1]{\kw{ref}\;{#1}}
%\newcommand{\lrefTy}[1]{\kw{refLcl}\;{#1}}
%\newcommand{\optrefTy}[1]{\kw{ref}_{?}({#1})}
%\newcommand{\optTy}[1]{{#1}_{?}}
%\newcommand{\none}{\textsf{none}}
%\newcommand{\some}{\textsf{some}}
%\newcommand{\threadTy}[1]{\kw{thread}\;{#1}}
%\newcommand{\all}[2]{\forall {#1}.{#2}}
%\newcommand{\ex}[2]{\exists {#1}.{#2}}
%\newcommand{\recTy}[2]{\mu {#1}.{#2}}
%\newcommand{\thread}[1]{\kw{thread}\;{#1}}
%
%\newcommand{\derefi}[2]{\kw{get}({#1}[{#2}])}
%\newcommand{\assigni}[3]{{#1}[#2]\;:=\;{#3}}
%\newcommand{\casi}[4]{\cas({#1}[{#2}], #3, #4)}
%
%\newcommand{\casF}[3]{\cas({#1}, #2, #3)}
%% \newcommand{\mpair}[2]{#1 \otimes #2}
%% \newcommand{\assignL}[2]{{#1}\;:=_1\;{#2}}
%% \newcommand{\assignR}[2]{{#1}\;:=_2\;{#2}}
\newcommand{\emptyivar}{\bot}
\newcommand{\cfg}[2]{{#1};{#2}}
\newcommand{\acfg}[3]{{#1};\;{#2};\;{#3}}
\newcommand{\enables}[2]{#1\mbox{ enables }#2}
\newcommand{\R}[1]{\mbox{$\{\;\begin{array}[t]{@{}l@{}}{#1}\;\}\end{array}$}}
\newcommand{\id}{\bot}
\newcommand{\isvar}{N}
\newcommand{\iset}{N}
%\newcommand*\kwd[1]{\textup{\textbf{\texttt{#1}}}}
\let\kwd\kw
\newcommand*\dform[1]{\textsf{#1}}
\newcommand*{\ide}[1]{\mathit{#1}}
\reservestyle{\keyword}{\kw}
\reservestyle{\langop}{\mathrm}
\reservestyle{\derivedform}{\dform}
\reservestyle{\identifier}{\ide}
\keyword{let[let\:],let*[let],in[\:in\:],if[if\:],then[\:then\:],else[\:else\:],skip,skip*[skip]}
\keyword{case[case\:],of[\:of\:]}%
\keyword{rec[rec\:],rec*[rec]}
\def\Rec #1.{\<rec>{#1}.\;}
\keyword{fork[fork\:],newch,newch*[newch],send,send*[send],tryrecv[tryrecv\:],tryrecv*[tryrecv]}%
\derivedform{recv[recv\:],recv*[recv]}%
\derivedform{cas,cas*[cas],ref[ref\:],ref*[ref]}
%\newcommand{\cas}{\<cas*>}% override setup's \kw{CAS}
\langop{!,:=}
\derivedform{true,false}
\derivedform{Some,None}
\derivedform{null}
\identifier{reply}%
\derivedform{srv,rpc,rpc*[rpc],Get,Set,Cas}%
\derivedform{spawn,join}
\newcommand\parcomp{\mathrel{||}}
\identifier{loop}%
\newcommand*{\Esend}[2]{\<send>(#1, #2)}
\newcommand{\Eref}{\mask_\textsf{ref}}
\newcommand*{\refmaps}{\mapsto}
\newcommand{\Echan}{\mask_\mathsf{chan}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ASSERTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\protAt}[3]{\mbox{$
\begin{array}{|@{}l@{}|@{}l@{}|}
\firsthline \;#1 : #2\;\; & \;#3\;\; \\
\lasthline
\end{array}$}}
\newcommand{\protAtB}[2]{\mbox{$
\begin{array}{|@{}l@{}|}
\firsthline \;#1 : #2\;\; \\
\lasthline
\end{array}$}}
% PDS: The baseline of the boxed contents of
% \oldKnowInv and \oldOwnGGhost and \oldOwnGhost isn't right:
% It can be lower than the surrounding formula.
%\newcommand{\oldKnowInv}[2]{\mbox{$
% \begin{array}{|@{\;}c@{\;}|}
% \firsthline #2 \\
% \lasthline
% \end{array}$}{}^{\,#1}}
%% \newcommand{\ownGhost}[2]{{\dbox{$#1 : #2$}}}
%% \newcommand{\ownGhostB}[3]{\dbox{$#1 : #2$}{}_{#3}}
% \newcommand{\ownGhost}[3]{\mbox{$
% \begin{array}{:@{}l@{}:@{}l@{}:}
% \firsthdashline \;#1 : #2\;\; & \;#3\;\; \\
% \lasthdashline
% \end{array}$}}
%\newcommand{\oldOwnGhost}[2]{\mbox{$
% \begin{array}{:@{\;}c@{\;}:}
% \firsthdashline #2 \\
% \lasthdashline
% \end{array}$}{}^{\,#1}}
%\newcommand{\oldOwnGGhost}[1]{\mbox{$
% \begin{array}{:@{\;}c@{\;}:}
% \firsthdashline #1 \\
% \lasthdashline
% \end{array}$}}
% 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]{\lfloor#1\rfloor}
\newcommand{\supported}[1]{\left[ #1 \right]}
%\newcommand*{\know}[2]{\knowInv{#1}{#2}}%
%\newcommand*{\own}[2]{\ownGhost{#1}{#2}}%
%\newcommand{\varset}{\mathcal{X}}
\newcommand{\simpl}{\textsc{i}}
\newcommand{\sspec}{\textsc{s}}
\newcommand{\IMSP}{\simpl\sspec}
\newcommand{\pointsto}{\hookrightarrow}
\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;}
%\newcommand{\gm}{\Rrightarrow}
\NewDocumentCommand \vsGen {O{} m O{}}%
{\mathrel{%
\ifthenelse{\equal{#3}{}}{%
% Just one mask, or none
{#2}_{#1}%
}{%
% Two masks
\presuper{#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]}
\newcommand{\mupd}{\rightsquigarrow}
\newcommand{\heapmaps}[1]{\hookrightarrow_{#1}}
\newcommand{\codemaps}[1]{\Mapsto_{#1}}
\newcommand{\implmaps}{\heapmaps{\IM}}
\newcommand{\implmapscode}{\codemaps{\IM}}
\newcommand{\specmaps}{\heapmaps{\SP}}
\newcommand{\specmapscode}{\codemaps{\SP}}
\newcommand{\IM}{\simpl}
\newcommand{\SP}{\sspec}
%\newcommand{\tRole}[1]{\texttok{Tid}(#1)}
\newcommand{\bij}[2]{{#1} \bowtie {#2}}
\newcommand{\iassert}[3]{\fbox{$#1$}{}^{#2}_{#3}}
%\newcommand{\mown}[2]{\textsf{own}(#1, #2)}
\newcommand{\mown}[3]{\fbox{$#1$}^{#2}_{#3}}
\newcommand{\minterp}[2]{\textsf{interp}(#1) = #2}
\newcommand{\mdisable}[2]{\delta_{#1}(#2)}
\newcommand{\TRUE}{\textlog{True}}
\newcommand{\FALSE}{\textlog{False}}
\newcommand{\emp}{\textsf{emp}}
\newcommand{\const}{\textlog{Inv}}
\newcommand{\infinite}{\textlog{infinite}}
\newcommand{\tokPure}{\textlog{TokPure}}
\newcommand{\timeless}[1]{\textlog{timeless}(#1)}
\newcommand{\physatomic}[1]{\text{$#1$ phys.\ atomic}}
\newcommand{\unlimRely}[1]{\cdot \geqRely {#1}}
\newcommand{\fmapsto}[1][-]{\stackrel{#1}{\mapsto}}
\newcommand{\gmapsto}{\hookrightarrow}%
\newcommand{\fgmapsto}[1][-]{\stackrel{#1}{\gmapsto}}%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% EXAMPLES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\onemany}[3]{
\draw[thick,->] (#1) to node [swap] {#2} (#3)
% \draw[-,thick] (#1) to node [swap] {#2} (#3)
}
\newcommand{\onemanyB}[3]{
\draw[thick,->] (#1) to node {#2} (#3)
% \draw[-,thick] (#1) to node [swap] {#2} (#3)
}
\newcommand{\onemanyabove}[3]{
\draw[thick,->] (#1) to [out=90,in=90] node [swap] {#2} (#3)
% \draw[-,thick] (#1) to [out=90,in=90] node [swap] {#2} (#3)
}
\newcommand{\ret}{\textsf{ret}}
\newcommand{\try}{\textsf{try}}
%\newcommand{\lock}{\textsf{lock}}
%\newcommand{\unlock}{\textsf{unlock}}
%\newcommand{\newlock}{\textsf{newlock}}
\newcommand{\head}{\textsf{hd}}
\newcommand{\optionTy}{\textsf{option}}
\newcommand{\extract}[1]{\textsf{getVal}(#1)}
\newcommand{\listTy}{\textsf{list}}
\newcommand{\cons}{\textsf{cons}}
\newcommand{\nil}{\textsf{nil}}
\newcommand{\nullv}{\textsf{null}}
%\newcommand{\nil}{\none}
\newcommand{\setNext}{\textsf{setNext}}
\newcommand{\consAtI}[3]{{#1} \propto_\simpl \cons({#2}, {#3})}
\newcommand{\consAtS}[3]{{#1} \propto_\sspec \cons({#2}, {#3})}
%\newcommand{\consAt}[3]{\cons({#1}, {#2})@{#3}}
\newcommand{\enq}{\textsf{enq}}
%\newcommand{\tryDeq}{\textsf{tryDeq}}
\newcommand{\deq}{\textsf{deq}}
\newcommand{\live}{\textsf{Live}}
\newcommand{\dead}{\textsf{Dead}}
\newcommand{\sentinel}{\textsf{Sentinel}}
\newcommand{\link}{\textlog{Link}}
%\newcommand{\lateChoice}{\textsf{lateChoice}}
%\newcommand{\earlyChoice}{\textsf{earlyChoice}}
%\newcommand{\rand}{\textsf{rand}}
%\newcommand{\redFlag}{\textsf{redFlag}}
%\newcommand{\blueFlag}{\textsf{blueFlag}}
%\newcommand{\flag}{\textit{flag}}
%\newcommand{\chan}{\textit{chan}}
%\newcommand{\flip}{\textsf{flip}}
%\newcommand{\flipBody}{\textsf{flipBody}}
%\newcommand{\read}{\textsf{read}}
%\newcommand{\install}{\textsf{install}}
%\newcommand{\commit}{\textsf{commit}}
%\newcommand{\abort}{\textsf{abort}}
%\newcommand{\complete}{\textsf{complete}}
\newcommand{\undecided}{\textsf{U}}
\newcommand{\committed}{\textsf{C}}
\newcommand{\aborted}{\textsf{A}}
\newcommand{\descriptor}{\textsf{descriptor}}
\newcommand{\ccas}{\widehat{\textsf{ccas}}}
\newcommand{\ccasCAS}{\widehat{\textsf{cas}}}
\newcommand{\ccasRead}{\widehat{\textsf{read}}}
\newcommand{\Empty}{\textsf{Empty}}
\newcommand{\Offered}{\textsf{Offered}}
\newcommand{\Accepted}{\textsf{Accepted}}
\newcommand{\counter}{\textsf{counter}}
\newcommand{\fun}{\textsf{fun}}
\newcommand{\get}{\textsf{get}}
\newcommand{\complete}{\textsf{complete}}
\newcommand{\setFlag}{\textsf{setFlag}}
\newcommand{\condInc}{\textsf{cinc}}
\newcommand{\Signaled}{\textsf{Signaled}}
\newcommand{\Speculated}{\textsf{Speculated}}
\newcommand{\Completed}{\textsf{Done}}
\newcommand{\Withdrawn}{\textsf{Gone}}
\newcommand{\Upd}{\textsf{Upd}}
\newcommand{\Const}{\textsf{Const}}
\newcommand{\reach}{\textsf{reach}}
\newcommand{\ann}[1]{
{\color{KeywordBlue}\ensuremath{
\{
\begin{array}[t]{@{}l@{}}
#1
\end{array}
\}}}
}
\newcommand{\annB}[1]{
{\color{KeywordBlue}\ensuremath{
\left\{
\begin{array}{@{}l@{}}
#1
\end{array}
\right\}}}
}
\newcommand{\aann}[1]{
{\color{KeywordBlue}
\begin{array}{@{}l@{}}
\llparenthesis #1 \rrparenthesis
\end{array}}
}
\newcommand{\sortOf}{\textlog{sort}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% JUDGMENTS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\wfte}[1]{{#1}\;\mbox{tyenv}}
\newcommand{\wtt}[2]{#1 : #2}
\newcommand{\wt}[3]{#1 \proves #2 : #3}
\newcommand{\wtd}[4]{#1; #2 \proves #3 : #4}
\newcommand{\judgment}[2]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
\newcommand{\judgmentB}[2]{\paragraph{#1}\hspace{\stretch{1}}{$#2$}}
\newcommand{\judgmentC}[2]{{\normalsize\textbf{\emph{#1}}}\hspace{\stretch{1}}{\fbox{$#2$}}}
\newcommand{\judgmentD}[2]{{\normalsize\textbf{\emph{#1}}}\quad{\fbox{$#2$}}}
\newcommand{\isAtomic}[2]{\cfg{#1}{#2}\ \textrm{atomic}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% MATH
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\pabs}{\lambda}
\newcommand{\textdom}[1]{\textit{#1}}
%\newcommand{\texttok}[1]{\textit{#1}}
\newcommand{\textlog}[1]{\textsf{#1}}
\newcommand{\textsort}[1]{\textlog{#1}}
\newcommand{\textvar}[1]{\textit{#1}}
\newcommand{\erase}[1]{\lfloor #1 \rfloor}
\newcommand{\UNLIMITED}{\textdom{UWorld}}
\newcommand{\sat}[3]{(#1,#2) : {#3}}
\newcommand{\satw}[3]{#1, #2 : #3}
\newcommand{\satwi}[4]{#1, #2 : #3, #4}
\newcommand{\satwiB}[3]{#1 : #2, #3}
\newcommand{\satall}[5]{#1, #2 \models_{#3} #4, #5}
\newcommand{\ftv}[1]{\mathrm{ftv}(#1)}
\newcommand{\tv}[1]{\mathrm{tyvars}(#1)}
\newcommand{\vars}[1]{\mathrm{vars}(#1)}
\newcommand{\threads}[1]{\mathrm{threads}(#1)}
\newcommand{\spec}[2]{\mathrm{spec}(#1,#2)}
\newcommand{\refisland}[2]{\mathrm{ref}(#1, #2)}
\newcommand{\hvalisland}[2]{\mathrm{hval}(#1, #2)}
\newcommand{\halloc}[2]{\mathrm{halloc}\left(#1, #2\right)}
\newcommand{\withIsland}{\blacktriangleleft}
\newcommand{\withIslands}{\blacktriangleleft}
\newcommand{\wimplspecextend}[2]{#1 \blacktriangleleft #2}
\newcommand{\whvalalloc}[3]{#1 \blacktriangleleft_{#2} #3}
\newcommand{\wok}[1]{{#1}\;\mbox{valid}} % ``World OK''
\newcommand{\pfn}{\rightharpoonup}
\newcommand{\fpfn}{\stackrel{\textrm{fin}}{\rightharpoonup}}
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\Lra}{\Leftrightarrow}
\newcommand{\monra}{\stackrel{\textrm{mon}}{\rightarrow}}
%\newcommand{\res}{\upharpoonright}
\newcommand{\restr}[2]{\lfloor #1 \rfloor_{#2}}
\newcommand{\zipTo}{\upharpoonright}
\newcommand{\OLDPRIMSTEP}[1]{{\color{red}\hookrightarrow}}
\newcommand{\reachable}{\diamond}
\newcommand{\cstep}{\rightrightarrows}
\newcommand{\primstep}[1]{\stackrel{#1}{\rightarrow}}
\newcommand{\purestep}{\stackrel{\textrm{pure}}{\rightarrow}}%
\newcommand{\step}{\ra}
\newcommand{\lstep}[1]{\stackrel{#1}{\step}}
\newcommand{\starstep}{\step^{*}}
\newcommand{\stepstar}{\starstep}
\newcommand{\resstep}[3]{#1 \vdash #2 \step #3}
\newcommand{\lresstep}[4]{#1 \vdash #2 \lstep{#4} #3}
\newcommand{\heapOf}{\textrm{heap}}
\newcommand{\mstep}[1]{\stackrel{#1}{\leadsto}}
\newcommand{\exclusive}[1]{\textrm{ex}(#1)}
\newcommand{\tpalg}[1]{\overline{\wp}(#1)}
\newcommand{\optional}[1]{{#1}_\id}
\newcommand{\tsys}[1]{\textrm{trans}(#1)}
\newcommand{\pstep}{\leadsto}
\newcommand{\lpstep}[1]{\stackrel{#1}{\pstep}}
\newcommand{\downto}{\searrow}
\newcommand{\wstep}[5]{\langle#1, #2\rangle \stackrel{#3}{\rightarrow} \langle#4, #5\rangle}
\newcommand{\wsplit}{\bullet}
\newcommand{\rsplit}{\bullet}
\newcommand{\issplit}{\otimes}
\newcommand{\ssplit}{\otimes}
\newcommand{\orspec}{\oplus}
\newcommand{\withCtx}{\triangleleft}
\newcommand{\protStatus}{E}
\newcommand{\disabled}{\textsf{disabled}}
\newcommand{\enabled}{\textsf{enabled}}
%\newcommand{\monora}{\stackrel{\textrm{mono}}{\longrightarrow}}
\newcommand{\monora}{\Rightarrow}
% LB
\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{\UPred}{\textdom{UPred}}
\newcommand{\SPred}{\textdom{SPred}}
\newcommand{\latert}{\mathord{\blacktriangleright}}
%\newcommand{\emp}{1}
% \newcommand{\lget}{\textrm{get}}
% \newcommand{\lput}{\textrm{put}}
% \newcommand{\trans}{\textrm{trans}}
\newcommand{\lift}[1]{\lfloor {#1} \rfloor}
\newcommand{\Sem}[1]{\llbracket #1 \rrbracket}
\newcommand{\semSort}[1]{\Sem{#1}}
\newcommand{\semTerm}[1]{\Sem{#1}}
\newcommand{\semVCtx}[1]{\Sem{#1}}
\newcommand{\semProtSet}[1]{\Sem{#1}}
\newcommand{\semAProp}[1]{\Sem{#1}}
%\newcommand{\semProp}[3]{#1 \models^{#2} #3}
\newcommand{\semProp}[3]{#1 \in \llbracket #3 \rrbracket^{#2}}
\newcommand{\semPropB}[2]{\llbracket #2 \rrbracket^{#1}}
\newcommand{\semPred}[2]{\llbracket{#1}\rrbracket^{#2}}
\newcommand{\Interp}[1]{\mathcal{I}\llbracket #1 \rrbracket}
\newcommand{\Val}[1]{\llbracket #1 \rrbracket}
\newcommand{\ValB}{\mathbb{V}}
\newcommand{\LiftVal}[1]{\widehat{\mathcal{V}}\llbracket #1 \rrbracket}
\newcommand{\Exp}[1]{\mathcal{E}\llbracket #1 \rrbracket}
\newcommand{\LiftExp}[1]{\widehat{\mathcal{E}}\llbracket #1 \rrbracket}
\newcommand{\expPred}[3]{(#1, #2) \downarrow #3}
\newcommand{\expPredPure}[3]{(#1, #2) \downarrow^{\textrm{pure}} #3}
\newcommand{\Store}[1]{\mathcal{H}\llbracket #1 \rrbracket}
\newcommand{\Heap}[1]{\mathcal{H}\llbracket #1 \rrbracket}
\newcommand{\Env}[1]{\mathcal{G}\llbracket #1 \rrbracket}
\newcommand{\TEnv}[1]{\mathcal{D}\llbracket #1 \rrbracket}
\newcommand{\Ctx}[1]{\mathcal{K}\llbracket #1 \rrbracket}
% \newcommand{\Thread}[1]{\mathcal{T}\llbracket #1 \rrbracket}
% \newcommand{\ThreadRel}[3]{\mathcal{T}(#1,#2,#3)}
% \newcommand{\TRel}[4]{\mathcal{T}(#1,#2,#3,#4)}
% \newcommand{\TRelD}[1]{\mathcal{T}\llbracket{#1}\rrbracket}
\newcommand{\HVal}[1]{\mathcal{H}\llbracket #1 \rrbracket}
\newcommand{\Obs}[1]{\mathcal{O}(#1)}
\newcommand{\dyn}[2]{\textlog{wp}({#1}, {#2})}
\newcommand{\adyn}[2]{{#1}\;\llparenthesis{#2}\rrparenthesis}
\newcommand{\dynpred}[2]{\textdom{wp}({#1}, {#2})}
\newcommand{\dynA}[3]{\textlog{wp}_{#3}({#1}, {#2})}
\newcommand{\pvs}[1]{\textlog{vs}({#1})}
\newcommand{\pvsA}[3]{\textlog{vs}_{#2}^{#3}({#1})}
\usepackage{scalerel}
% \hoaresizebox pre post
% \hoarescalebox char sizebox
\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}}%
}
\newcommand{\ttrip}[4]{
\semPropB{#1}{\rho}{\safe(#2, #3, #4)}
}
%% \newcommand{\ttrip}[4]{
%% #1 \models^\rho
%% {#2}@{#3}\;
%% \big\{ #4 \big\}
%% }
\newcommand{\halfttrip}[3]{
{#1}@{#2}\;
\big\{ #3 \big\}
}
\newcommand{\rewriteSpec}{\ra_\SP}
%\newcommand{\dyn}[2]{{#1}\;\{{#2}\}}
\newcommand{\safe}{\textsf{safe}}
\newcommand{\mthread}{m}
\newcommand{\absent}{\textsf{none}}
\newcommand{\PROG}[1]{\textrm{prog}\llbracket #1 \rrbracket}
\newcommand{\PRES}[1]{\textrm{pres}\llbracket #1 \rrbracket}
\newcommand{\pset}[1]{\wp(#1)}
\newcommand{\pmset}[1]{\wp_{m}(#1)}
\newcommand{\psetup}[1]{\wp^\uparrow(#1)}
\newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
\newcommand{\fpset}[1]{\wp_{\textrm{fin}}(#1)}
\newcommand{\mset}[1]{\mathrm{bag}(#1)}
%\newcommand{\bag}[1]{\Lbag #1 \Rbag}
\newcommand{\eqdef}{\triangleq}
\newcommand{\extendseq}{\sqsupseteq}
\newcommand{\extends}{\sqsupset}
\newcommand{\beforeeq}{\sqsubseteq}
\newcommand{\extby}{\sqsubseteq}
%\newcommand{\ntime}{\triangleright}
\newcommand{\later}{\mathord{\triangleright}}
%\newcommand{\always}[1]{\Box{#1}}
\newcommand{\always}{\Box{}}
\newcommand{\dup}[1]{\textrm{dup}({#1})}
\newcommand{\restrict}[2]{\lfloor #1 \rfloor_{#2}}
\newcommand{\extendseqCtx}{\stackrel{\textrm{ctx}}{\sqsupseteq}}
\newcommand{\extbyCtx}{\stackrel{\textrm{ctx}}{\sqsubseteq}}
\newcommand{\leqWT}{\sqsubseteq}
\newcommand{\geqWT}{\sqsubseteq}
\newcommand{\lubWT}{\sqcup}
\newcommand{\leqRes}{\leq}
\newcommand{\geqRes}{\geq}
\newcommand{\geqIS}{\sqsupseteq}
\newcommand{\relyguar}{\textrm{rg}}
\newcommand{\leqRG}{\stackrel{\relyguar}{\sqsubseteq}}
\newcommand{\leqRGB}[1]{\stackrel{\textrm{rg}}{\sqsubseteq_{#1}}}
\newcommand{\geqAll}{\sqsupseteq}
\newcommand{\geqRely}{\stackrel{\textrm{rely}}{\sqsupseteq}}
\newcommand{\geqRelyB}[1]{\stackrel{\textrm{rely}}{\sqsupseteq_{#1}}}
\newcommand{\geqRelyC}[1]{\sqsupseteq^{\textrm{rely}}_{#1}}
\newcommand{\geqGuar}{\stackrel{\textrm{guar}}{\sqsupseteq}}
\newcommand{\geqGuarB}[1]{\stackrel{\textrm{guar}}{\sqsupseteq_{#1}}}
\newcommand{\geqGuarC}[1]{\sqsupseteq^{\textrm{guar}}_{#1}}
\newcommand{\leqRely}{\stackrel{\textrm{rely}}{\sqsubseteq}}
\newcommand{\leqRelyB}[1]{\stackrel{\textrm{rely}}{\sqsubseteq_{#1}}}
\newcommand{\leqRelyC}[1]{\sqsubseteq^{\textrm{rely}}_{#1}}
\newcommand{\leqGuar}{\stackrel{\textrm{guar}}{\sqsubseteq}}
\newcommand{\leqGuarB}[1]{\stackrel{\textrm{guar}}{\sqsubseteq_{#1}}}
\newcommand{\leqGuarC}[1]{\sqsubseteq^{\textrm{guar}}_{#1}}
\newcommand{\intleq}{\stackrel{\textrm{int}}{\sqsubseteq}}
\newcommand{\extleq}{\stackrel{\textrm{ext}}{\sqsubseteq}}
\newcommand{\intgeq}{\stackrel{\textrm{int}}{\sqsupseteq}}
\newcommand{\extgeq}{\stackrel{\textrm{ext}}{\sqsupseteq}}
\newcommand{\withframe}{\ \mbox{${<}\!\!*$}\ }
\newcommand{\proves}{\vdash}
\newcommand{\provesalways}{\vdash_{\!\!\boxempty}}
\newcommand{\refines}{\leq}
\newcommand{\pbrk}{\mbox{\phantom{.}}}
\newcommand{\hasHVal}[3]{#1 \Ra \textrm{hval}(#2, #3)}
\newcommand{\multi}[1]{\!\!\!\begin{array}[t]{l}
#1
\end{array}
}
\newcommand{\multic}[1]{\!\!\!\begin{array}[c]{l}
#1
\end{array}
}
\newcommand{\pureleq}{\preceq_{\textrm{pure}}}
\newcommand{\logleq}[4]{#1 \proves #2 \preceq #3 : #4}
\newcommand{\semleq}[4]{#1 \models #2 \preceq #3 : #4}
\newcommand{\hypleq}[6]{{#1}; {#2} \models {#3} \proves {#4} \preceq {#5} : {#6}}
\newcommand{\progleq}[4]{#1 \models #2 \stackrel{\textrm{prog}}{\preceq} #3 : #4}
\newcommand{\specleq}[4]{#1 \models #2 \stackrel{\textrm{spec}}{\preceq} #3 : #4}
\newcommand{\mixleq}[4]{#1 \models #2 \stackrel{\textrm{mix}}{\preceq} #3 : #4}
\newcommand{\result}[2]{\pbrk
\begin{quotation}
\hskip -0.25in
$\begin{array}{@{}ll}
\textrm{If} & #1 \\
\textrm{then} & #2
\end{array}$
\end{quotation}
}
\newcommand{\resrule}[2]{\pbrk
\begin{quotation}
\hskip -0.25in
$\infer{#1}{#2}$
\end{quotation}
}
%\newcommand{\rand}{\\&}
\newcommand{\randB}{\qquad}
%\renewcommand{\labelitemi}{$\bullet$}
%\renewcommand{\labelitemii}{$\bullet$}
%\renewcommand{\labelitemiii}{$\bullet$}
%\renewcommand{\labelitemiv}{$\bullet$}
\newcommand{\mc}[1]{\multicolumn{2}{@{}l}{#1}}
\newcommand{\mcl}[2]{\multicolumn{#1}{@{}l}{#2}}
\newcommand{\citem}[1]{\item\textit{Case: } \fbox{$#1$}\quad}
\newcommand{\cand}{\textrm{ and }}
\newcommand{\claim}[1]{\vskip 5pt \noindent \mbox{\textit{Claim: } \fbox{$#1$}}\quad}
\newcommand{\case}[1]{\vskip 5pt \noindent \textit{Case: } \fbox{$#1$}\quad}
\newcommand{\casec}[1]{\vskip 5pt \noindent \mbox{\textit{Case \textsc{#1}}: \ }}
\newcommand{\subcase}[1]{\vskip 5pt \textit{Subcase: } \fbox{$#1$}\ }
\newcommand{\subcasec}[1]{\vskip 5pt \noindent \qquad \mbox{\textit{Subcase \textsc{#1}}: \ }}
\newcommand{\subcasen}{\vskip 5pt \noindent \qquad \mbox{\textit{Subcase: } \ }}
\newcommand{\have}[1]{$\begin{array}[t]{@{}l} #1 \end{array}$}
\newcommand{\TIME}{\textrm{time}}
\newcommand{\MAP}{\textrm{map}}
\newcommand{\dom}{\textrm{dom}}
\newcommand{\rng}{\textrm{rng}}
\newcommand{\cod}{\textrm{cod}}
\newcommand{\elide}[1]{}
\newcommand{\ov}[1]{\overline{#1}}
\newcommand{\CR}{\mathcal{R}}
\newcommand{\CS}{\mathcal{S}}
\newcommand{\IF}{\mathrel{\text{if}}}
\newcommand{\OW}{\text{otherwise}} % not a relation
\newcommand{\WHEN}{\textrm{when }}
\newcommand{\FIX}{\textrm{Fix }}
\newcommand{\LET}{\textrm{Let }}
\newcommand{\IN}{\textrm{ in }}
\newcommand{\SUPPOSE}{\textrm{Suppose }}
\newcommand{\HAVE}{\textrm{Have }}
\newcommand{\RAND}{\textrm{ and }}
\newcommand{\WHERE}{\mathrel{\text{where}}}
\newcommand{\ASSUMPTION}{\textrm{assumption}}
\newcommand{\THEN}{\textrm{Then }}
\newcommand{\WRITE}{\textrm{Write }}
\newcommand{\PICK}{\textrm{Pick }}
\newcommand{\WITH}{\textrm{ with }}
\newcommand{\WLOG}{\textrm{ WLOG}}
%newcommand{\STS}{\textrm{Suffices to show }}
\newcommand{\extrasep}{\setlength{\extrarowheight}{1.5pt}}
\newcommand{\extrasepB}[1]{\setlength{\extrarowheight}{#1}}
\newcommand{\medextrasep}{\setlength{\extrarowheight}{2pt}}
\newcommand{\bigextrasep}{\setlength{\extrarowheight}{3pt}}
\newcommand{\hugeextrasep}{\setlength{\extrarowheight}{5pt}}
\newcommand{\noextrasep}{\setlength{\extrarowheight}{0pt}}
\newcommand{\iffrule}{\mprset{fraction={===}}}
\newcommand{\ie}{\emph{i.e.,} }
\newcommand{\eg}{\emph{e.g.,} }
\newcommand{\etal}{\emph{et~al.}}
\newcommand{\wrt}{w.r.t.~}
\newcommand{\deadfootnote}[1]{}
\newcommand{\idisl}[2]{{#1} \mapsto {#2}}
%\newcommand{\region}[4]
\newcommand{\SET}[2]{
\left\{%
#1%
\;\middle|\;%
#2%
\right\}
}
\newcommand{\SETB}[1]{
\left\{%
#1%
\right\}
}
\newcommand{\SETC}[2]{#1 & #2}
\newcommand{\SPACER}{\;\;\;}
\newcommand{\wIso}{\xi}
\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{\(#1\)}}}
\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}}
% what are we calling the manuscript?
\newcommand{\book}{book}
\newcommand{\aaron}[1]{{\color{red}\textbf{AT: #1}}}
\newcommand{\derek}[1]{{\color{red}\textbf{DD: #1}}}
\newcommand{\lars}[1]{{\color{red}\textbf{LB: #1}}}
\newcommand{\kasper}[1]{{\color{red}\textbf{KS: #1}}}
\newcommand{\ralf}[1]{{\color{red}\textbf{RJ: #1}}}
\newcommand{\dave}[1]{{\color{red}\textbf{PDS: #1}}}
\newcommand{\hush}[1]{}
\newcommand{\relaxguys}{%
\let\aaron\hush%
\let\derek\hush%
\let\lars\hush%
\let\kasper\hush%
\let\ralf\hush%
\let\dave\hush%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ATOMIC SHIFTS
\newcommand{\funnyforall}{\boldsymbol\forall}
\newcommand{\funnyexists}{\boldsymbol\exists}
\newcommand{\aspre}{P}
\newcommand{\asfrom}{\alpha}
\newcommand{\asto}{\beta}
\newcommand{\aspost}{Q}
%\newcommand{\asprop}{\aspost}
%\newcommand{\aspred}{\aspost}
\newcommand{\asframe}{R}
\newcommand{\asfmask}{\mask_{\asframe}}
\newcommand\nomask{\,\!}% to avoid \as defaults. It ain't empty, but it looks empty.
% we need 10 arguments, so use some magic to get that...
\newcommand\ascore[1]{%
\def\tempflags{#1}%
\ascoreContinued%
}
\newcommand{\ascoreContinued}[9]{
{\stretchleftright[450]{\langle}{ %
\IfSubStr{\tempflags}{l}{ \begin{inbox} }{} %
#2
\IfSubStr{\tempflags}{b}{\vsE}{\vs} %
\IfSubStr{\tempflags}{a}{ #1.\;}{} %
#3 %
\IfSubStr{\tempflags}{x}{ \mid #4}{} %
\IfSubStr{\tempflags}{f}{ %
\mid %
\IfSubStr{\tempflags}{l}{ \\ }{} %
\IfSubStr{\tempflags}{e}{ #5.\;}{} %
#6 \vs #7 %
}{} %
\IfSubStr{\tempflags}{l}{ \end{inbox} }{} %
}{\rangle}}_{#9}^{#8} %
}
\NewDocumentCommand \as {d() m m o d() m m O{\top} O{}}
{ \ascore{ %
\IfNoValueF{#1}{a} % universal quantifier
b % arrow back to start
\IfNoValueF{#4}{x} % explicit R and E
f % add forwards shift to final state
\IfNoValueF{#5}{e} % existential quantifier
}{#1}{#2}{#3}{#4}{#5}{#6}{#7}{#8}{#9} %
}
\NewDocumentCommand \asl {d() m m o d() m m O{\top} O{}}
{ \ascore{ %
l % use multiple lines
\IfNoValueF{#1}{a} % universal quantifier
b % arrow back to start
\IfNoValueF{#4}{x} % explicit R and E
f % add forwards shift to final state
\IfNoValueF{#5}{e} % existential quantifier
}{#1}{#2}{#3}{#4}{#5}{#6}{#7}{#8}{#9} %
}
% \NewDocumentCommand \am {d() m m o m}
% { \ascore{ %
% \IfNoValueF{#1}{a} % universal quantifier
% b % arrow back to start
% \IfNoValueF{#4}{x} % explicit R and E
% }{#1}{#2}{#3}{#4}{#5}{}{}{} %
% }
%%% Atomic triples
\NewDocumentCommand \ahoare {m m m O{} O{}}{
\triple\langle\rangle{#1}{#2}{#3}%
_{#5}^{#4}%
}
\NewDocumentCommand \ahoareV {O{c} m m m O{} O{}}{
{\begin{aligned}[#1]
&\anglebracket{#2} \\
&\quad{#3} \\
&{\anglebracket{#4}}_{#6}^{#5}
\end{aligned}}%
}
\NewDocumentCommand \ahoareHV {O{c} m m m O{} O{}}{
{\begin{aligned}[#1]
&\anglebracket{#2}\;\;\; {#3} \\
&{\anglebracket{#4}}_{#6}^{#5}
\end{aligned}}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% hoare proof typesetting
\newenvironment{inbox}[1][]{
\begin{array}[#1]{@{}l@{}}
}{
\end{array}
}
\newcommand{\tabubox}[2][]{%
\begin{tabu}{@{#1}X[1,l,m]@{}}%
#2 %
\end{tabu}%
}
\newcommand{\hproofnospace}[1]{\noindent\parbox{\linewidth}{#1}} %
\newcommand{\hproof}[1]{\vspace{0.5em}\hproofnospace{#1}\vspace{0.5em}} %
\newcommand\psub[2]{%
\begin{tabu}{ m{0.9em} | X[1,l,m] }%
\begin{sideways}#1\end{sideways} &%
\tabubox{#2}%
\end{tabu}%
}%
\newcommand\pind[1]{\tabubox[\hspace{1em}]{#1}}
\newcommand{\pline}[2][\empty]{\ensuremath{\left\{{#2\mathstrut}\right\}_{#1}}}
\newcommand{\pmline}[2][\empty]{\ensuremath{\left\{\begin{inbox}#2\end{inbox}\right\}_{#1}}}
\newcommand{\aline}[2][\empty]{\ensuremath{{\stretchleftright[450]{\langle}{#2\mathstrut}{\rangle}}_{#1}}}
\newcommand{\amline}[2][\empty]{\ensuremath{{\stretchleftright[450]{\langle}{\begin{inbox}#2\end{inbox}}{\rangle}}_{#1}}}
\definecolor{code_color}{rgb}{0, 0, 0.6}
\newcommand{\cdline}[1]{\ensuremath{\color{code_color}#1}}
\definecolor{interp_p_backgr}{rgb}{0.8, 0.8, 1.0}
\definecolor{interp_q_backgr}{rgb}{0.8, 1.0, 0.8}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Monoid and other constructions
\newcommand{\FHeap}{\textsc{FHeap}}
\newcommand{\AFHeap}{\textsc{AFHeap}}
\newcommand{\auth}[1]{\ensuremath{\textsc{Auth}(#1)}}
\newcommand{\authfull}{\mathord{\bullet}\,}
\newcommand{\authfrag}{\mathord{\circ}\,}
\newcommand{\fpfunm}[2]{\ensuremath{\textsc{FpFun}(#1, #2)}}
\newcommand{\fracm}[1]{\ensuremath{\textsc{Frac}(#1)}}
\newcommand{\exm}[1]{\ensuremath{\textsc{Ex}(#1)}}
\newcommand{\agm}[1]{\ensuremath{\textsc{Ag}(#1)}}
%\newcommand{\dispm}[1]{\ensuremath{\textsc{Disp}(#1)}}
%\newcommand{\disposed}{\mathord{\dagger}}
\newcommand{\STSMon}[1]{\textsc{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}}