\makeatletter%
\@ifundefined{basedir}{%
\newcommand\basedir{}%
}{}%
\makeatother%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% PACKAGES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\usepackage{mathtools}
%\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{stmaryrd}

\usepackage{\basedir mathpartir}

\usepackage{array}
\usepackage{tabu}

\usepackage{dashbox}

\usepackage{\basedir pftools}

\usepackage{xcolor}  % for print version

\usepackage{graphicx}
\usepackage{tikz}
\usepackage{scalerel}

\usepackage{rotating}
\usepackage{xparse}
\usepackage{xstring}
\usepackage{semantic}
\usepackage{csquotes}

\usepackage{hyperref}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% SETUP
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\SetSymbolFont{stmry}{bold}{U}{stmry}{m}{n} % this fixes warnings when \boldsymbol is used with stmaryrd included

\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}}

\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}

\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}

\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
}


%\theoremstyle{definition}
%\newtheorem{prop}{Prop}
\newtheorem{defn}{Definition}
\newtheorem{cor}{Corollary}
\newtheorem{conj}{Conj}
\newtheorem{lem}{Lemma}
\newtheorem{thm}{Theorem}

\newtheorem{exercise}{Exercise}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% GENERIC MACROS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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}}}

\newcommand{\changes}{{\bf\color{red}{Changes}}}
\newcommand{\TODO}{\vskip 4pt {\color{red}\bf TODO}}


\newcommand{\ie}{\emph{i.e.,} }
\newcommand{\eg}{\emph{e.g.,} }
\newcommand{\etal}{\emph{et~al.}}
\newcommand{\wrt}{w.r.t.~}

\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%
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MATH SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% superscript to the left
\def\presuper#1#2%
  {\mathop{}%
   \mathopen{\vphantom{#2}}^{#1}%
   \kern-\scriptspace%
   #2}

\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 \{#2\}_{#3}}

\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]{\lfloor#1\rfloor}

%% View Shifts
\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]}
\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow}}[#2]}}


%% 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{\toval}{\mathit{val}}
\newcommand{\ofval}{\mathit{expr}}
\newcommand{\atomic}{\mathit{atomic}}
\newcommand{\Lang}{\Lambda}

\newcommand{\tpool}{T}

\newcommand{\cfg}[2]{{#1};{#2}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% DERIVED CONSTRUCTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Commonly used identifiers
\newcommand{\FHeap}{\textmon{FHeap}}
\newcommand{\AFHeap}{\textmon{AFHeap}}

\newcommand{\auth}[1]{\textmon{Auth}}
\newcommand{\authfull}{\mathord{\bullet}\,}
\newcommand{\authfrag}{\mathord{\circ}\,}

\newcommand{\fracm}{\ensuremath{\textmon{Frac}}}
\newcommand{\exm}{\ensuremath{\textmon{Ex}}}
\newcommand{\agm}{\ensuremath{\textmon{Ag}}}

\newcommand{\STSMon}[1]{\textmon{Sts}_{#1}}
\newcommand{\STSInv}{\textsf{STSInv}}
\newcommand{\STS}{\textsf{STS}}
\newcommand{\STSS}{\mathcal{S}} % states
\newcommand{\STST}{\mathcal{T}} % tokens
\newcommand{\STSL}{\mathcal{L}} % labels
\newcommand{\ststrans}{\ra^{*}}%	the relation relevant to the STS rules

\newcommand{\AuthInv}{\textsf{AuthInv}}
\newcommand{\Auth}{\textsf{Auth}}