diff --git a/docs/tex/.gitignore b/docs/tex/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..7969c4f55c81e769b2facb814aa4d2e95e681c84
--- /dev/null
+++ b/docs/tex/.gitignore
@@ -0,0 +1,14 @@
+*.pdf
+*.aux
+*.log
+*.out
+*.synctex.gz
+*.txss
+*.thm
+*.toc
+*.bbl
+*.blg
+*.bcf
+*.run.xml
+_*_.tex
+auto/*.el
diff --git a/docs/tex/atomic.tex b/docs/tex/atomic.tex
new file mode 100644
index 0000000000000000000000000000000000000000..3221a0157dff753e51ef1962d9f9ec338e2a0fee
--- /dev/null
+++ b/docs/tex/atomic.tex
@@ -0,0 +1,242 @@
+\documentclass[10pt]{article}
+\usepackage{lmodern}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage{fontspec}
+\setmonofont{Source Code Pro}
+
+\newif\ifslow\slowfalse %\slowtrue
+\ifslow
+ \usepackage[english]{babel}
+ \usepackage[babel=true]{microtype}
+\fi
+\usepackage[top=1in, bottom=1in, left=1.25in, right=1.25in]{geometry}
+
+\usepackage[backend=biber]{biblatex}
+\bibliography{bib}
+
+\newcommand{\bdia}{\blacklozenge}
+\newcommand{\dia}{\Diamond}
+\newcommand{\injR}{\texttt{injR}}
+\newcommand{\injL}{\texttt{injL}}
+
+\input{setup}
+
+\begin{document}
+
+\title{\bfseries iris-atomic}
+\author{Zhen Zhang}
+\maketitle
+
+\section{sync.v}
+
+
+\[\begin{aligned}
+ \text{synced}(R, f', f) \eqdef
+ \All P, Q, x.
+ &\hoare{ R * P(x)}{f(x)}{ v.\,R * Q(x,v) } \ra \\
+ &\hoare{ P(x)}{f'(x)}{ v.\,Q(x,v) }
+ \end{aligned}\]
+
+\[
+ \text{is\_syncer}(R, s) \eqdef
+ \All f. \wpre{s(f)}{ f'.\, \text{synced}(R, f', f)} \]
+
+
+\[
+ mk\_syncer\_spec (mk\_syncer) :=
+ \All R.
+ \hoare{R}{mk\_syncer()}{ s.\,\always (is\_syncer(R, s)} \]
+
+
+\section{atomic.v}
+
+Logically atomic triple:
+
+\[
+ \lahoare{g.\, \alpha(g)}{e}{v.\, \beta(g, v)}[E_i][E_o] \eqdef
+ \All P, Q.
+ \begin{aligned}
+ &P \vs[Eo][Ei] \Exists g, \alpha(g) * (\alpha(g) \vsW[Ei][Eo] P \land \All v. \beta(g, v) \vsW[Ei][Eo] Q(g, v)) \wand \\
+ &\hoare{P}{e}{v.\, \Exists g. Q(g, v)}
+ \end{aligned}\]
+
+\section{simple\_sync.v}
+
+\begin{verbatim}
+mk_sync :=
+ λ: <>,
+ let l := newlock() in
+ λ: f x,
+ acquire l;
+ let ret := f x in
+ release l;
+ ret.
+\end{verbatim}
+
+\section{atomic\_sync.v}
+
+Specialized logically atomic triple:
+
+\[ \lahoare{g.\, \ownGhost{\gname}{g^{1/2}} * \always \alpha(g)}
+ {f(x)}
+ {v.\, \Exists g'. \ownGhost{\gname}{g'^{1/2}} * \beta(x, g, g', v)}[E_i][E_o]\]
+
+\begin{verbatim}
+sync(mk_syncer) :=
+ λ: f_seq l,
+ let s := mk_syncer() in
+ s (f_seq l).
+\end{verbatim}
+
+\[seq\_spec(f, \phi, \alpha, \beta, E) \eqdef
+ \All l.
+ \hoare{\top}{f(l)}{f'.\,
+ \begin{aligned}
+ \pure &\All x, \Phi, g.\\
+ &\phi (l, g) * \always \alpha(x) *\\
+ &(\All v, g'. \phi(l, g') \wand \beta(x, g, g', v) \wand \pvs[E][E] \Phi(v))\\
+ &\proves \wpre{f'(x)}[E]{ \Phi }
+ \end{aligned}
+ }\]
+
+\[\begin{aligned}
+ &\text{atomic\_spec}(mk\_syncer, f\_seq, l, \phi, \alpha, \beta, E_i) \eqdef\\
+ &\All g_0.
+ seq\_spec(f\_seq, \phi, \alpha, \beta, \top) \ra
+ mk\_syncer\_spec(mk\_syncer) \ra\\
+ &\phi(l, g_0)
+ \proves \wpre{sync(mk\_syncer, f\_seq, l)}{ f.\,
+ \Exists \gname. \ownGhost{\gname}{g_0^{1/2}} *
+ \All x. \always \lahoare{g.\, \ownGhost{\gname}{g^{1/2}} * \always \alpha(g)}{f(x)}
+ {v.\, \Exists g'. \ownGhost{\gname}{g'^{1/2}} * \beta(x, g, g', v)}[E_i][\top]}
+ \end{aligned} \]
+
+\[ (\Exists g. \phi(l, g') * \ownGhost{\gname}{g^{1/2}} * P x \]
+
+\section{treiber.v}
+
+\begin{verbatim}
+push s x :=
+ let hd := !s in
+ let s' := ref SOME (x, hd) in
+ if CAS s hd s'
+ then ()
+ else push s x.
+
+pop s :=
+ let hd := !s in
+ match !hd with
+ | SOME (x, hd') =>
+ if: CAS s hd hd'
+ then SOME x
+ else pop s
+ | NONE => NONE
+ end.
+
+iter hd f :=
+ match !hd with
+ | NONE => ()
+ | SOME (x, hd') => f x ; iter hd' f
+ end.
+
+\end{verbatim}
+
+Logiall atomic spec (version 1):
+
+\[ \lahoare{xs.\, stack(s, xs)}{push(s, x)}{stack(s, x::xs)}[heapN][\top]\]
+\[ \lahoare{xs.\, stack(s, xs)}{pop(s)}{v. \begin{split} (&\Exists x, xs'. v = SOME(x) * stack(s, xs')) \lor\\
+ (&v = NONE * xs = \emptyset * stack(s, \emptyset)) \end{split}}[heapN][\top]\]
+
+
+Logiall atomic spec (version 2):
+
+\[ \lahoare{hd, xs.\, s \mapsto hd * list(hd, xs)}{push(s, x)}{\Exists hd'. s \mapsto hd' * hd' \mapsto SOME(x, hd) * list(hd, xs)}[heapN][\top]\]
+\[ \lahoare{hd, xs.\, s \mapsto hd * list(hd, xs)}{pop(s)}{v.
+ \begin{split}
+ (&\Exists x, xs', hd'. v = SOME(x) * hd \mapsto SOME(x, hd') * s \mapsto hd' * list(hd', xs')) \lor\\
+ (&v = NONE * xs = \emptyset * hd \mapsto NONE)
+ \end{split}
+ }[heapN][\top]
+ \]
+
+
+\section{peritem.v}
+
+A crappy but working spec:
+
+\[f\_spec (\gname, xs, s, f, Rf, RI) \eqdef
+ \All x.
+ \hoare{x \in xs * \knowInv\iname{\Exists xs. stack'(\gname, xs, s) * RI} * Rf}{f(x)}{ v.\, v = () }.\]
+
+\[\begin{split}
+ iter\_spec(\gname, s, Rf, RI) \eqdef
+ &\All xs, hd, f.\\
+ &f\_spec(xs, s, f', Rf, RI) \ra\\
+ &\hoare{\knowInv\iname{\Exists xs. stack'(xs, s) * RI} * list'(\gname, hd, xs) * Rf}{iter(hd, f)}{ v.\, v = () * Rf}
+ \end{split}\]
+
+\[push\_spec (\gname, s, x, RI) \eqdef
+ \hoare{R(x) * \knowInv\iname{\Exists xs. stack'(xs, s) * RI}}{push(s, x)}{v.\, v = () * (\Exists hd. ev(\gname, hd, x))}\]
+
+\section{flat.v}
+
+\begin{verbatim}
+doOp :=
+ λ: p,
+ match !p with
+ | InjL (f, x) => p <- InjR (f x)
+ | InjR _ => ()
+ end.
+
+try_srv :=
+ λ: lk s,
+ if try_acquire lk
+ then let hd := !s in
+ iter hd doOp;
+ release lk
+ else ().
+
+loop p s lk :=
+ match !p with
+ | InjL _ =>
+ try_srv lk s;
+ loop p s lk
+ | InjR r => r
+ end.
+
+install :=
+ λ: f x s,
+ let p := ref (InjL (f, x)) in
+ push s p;
+ p.
+
+mk_flat :=
+ λ: <>,
+ let lk := newlock() in
+ let s := new_stack() in
+ λ: f x,
+ let p := install f x s in
+ let r := loop p s lk in
+ r.
+\end{verbatim}
+
+\[p \mapsto \injR(-)\]
+\[p \mapsto \texttt{injL}(f, x)\]
+\[p \mapsto \injR(y)\]
+\[\circ_i, \bullet_i, \dia_i, \bdia, \dia_i \circ_i, \dia_i \bullet_i, \bdia \bullet_i\]
+
+
+\begin{align*}
+ &\Exists y. &&p \fmapsto[1/2] \injR(-) * \dia_i * \circ_i\\
+\lor &\Exists f, x, P, Q. &&p \fmapsto[1/2] \injL(f, x) * \ownGhost{\gname}{x^{1/2}} *
+ P(x) * (\hoare{R * P(x)}{f(x)}{v.\,R * Q(x, v)}) * \gamma \mapstoprop Q(x) * \dia_i * \bullet_i\\
+\lor &\Exists x. &&p \fmapsto[1/2] \injL(-, x) * \ownGhost{\gname}{x^{1/4}} * \bdia * \bullet_i\\
+\lor &\Exists x, y. &&p \fmapsto[1/2] \injR(y) * \ownGhost{\gname}{x^{1/2}} * \gamma \mapstoprop Q(x) * Q(x, y) * \dia_i * \bullet_i
+\end{align*}
+
+\[\alpha = \alpha_a * \alpha_o, \alpha = \alpha_a' * \alpha_o\]
+\[\alpha = \alpha_o * \alpha_a, \alpha_a' * \alpha_o = \beta\]
+\[\alpha = \alpha_a * \alpha_o, \alpha = \alpha_a' * \alpha_o\]
+
+\end{document}
diff --git a/docs/tex/iris.sty b/docs/tex/iris.sty
new file mode 100644
index 0000000000000000000000000000000000000000..41f41271a7eaa95a6d8da5a2e2fdce88d8424d70
--- /dev/null
+++ b/docs/tex/iris.sty
@@ -0,0 +1,476 @@
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{iris}
+
+\RequirePackage{tikz}
+\RequirePackage{scalerel}
+\RequirePackage{array}
+\RequirePackage{dashbox}
+\RequirePackage{tensor}
+\RequirePackage{xparse}
+\RequirePackage{xstring}
+\RequirePackage{mathtools}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% 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
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\nat}{\mathbb{N}}
+
+\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
+\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
+\newcommand\pord{\sqsubseteq}
+\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{\la}{\leftarrow}
+\newcommand{\ra}{\rightarrow}
+\newcommand{\Ra}{\Rightarrow}
+\newcommand{\Lra}{\Leftrightarrow}
+\newcommand\monra{\xrightarrow{\kern-0.15ex\textrm{mon}\kern-0.05ex}}
+\newcommand\nfn{\xrightarrow{\kern-0.15ex\textrm{ne}\kern-0.05ex}}
+\newcommand{\eqdef}{\triangleq}
+\newcommand{\bnfdef}{\vcentcolon\vcentcolon=}
+
+% \newcommand{\lor}{\wedge}
+\newcommand{\maybe}[1]{#1^?}
+
+\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
+\newcommand*\set[1]{\left\{#1\right\}}
+\newcommand*\record[1]{\left\{\spac#1\spac\right\}}
+\newcommand*\recordComp[2]{\left\{\spac#1\spac\middle|\spac#2\spac\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{\finpset}[1]{\wp^\mathrm{fin}(#1)}
+
+\newcommand{\Func}{F} % functor
+
+\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}
+
+\newcommand{\mapinsert}[3]{#3[#1:=#2]}
+
+\newcommand{\nil}{\epsilon}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\textdom}[1]{\textit{#1}}
+
+\newcommand{\wIso}{\xi}
+
+\newcommand{\rs}{r}
+\newcommand{\rsB}{s}
+\newcommand{\rss}{R}
+
+\newcommand{\pres}{\pi}
+\newcommand{\wld}{w}
+\newcommand{\ghostRes}{g}
+
+%% Various pieces of syntax
+\newcommand{\wsat}[3]{#1 \models_{#2} #3}
+\newcommand{\wsatpre}{\textdom{pre-wsat}}
+
+\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{\latertinj}{\textlog{next}}
+
+\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{\SProp}{\textdom{SProp}}
+\newcommand{\UPred}{\textdom{UPred}}
+\newcommand{\mProp}{\textdom{Prop}} % meta-level prop
+\newcommand{\iProp}{\textdom{iProp}}
+\newcommand{\iPreProp}{\textdom{iPreProp}}
+\newcommand{\Wld}{\textdom{Wld}}
+\newcommand{\Res}{\textdom{Res}}
+\newcommand{\State}{\textdom{State}}
+\newcommand{\Val}{\textdom{Val}}
+\newcommand{\Loc}{\textdom{Loc}}
+\newcommand{\Expr}{\textdom{Expr}}
+
+\newcommand{\cofe}{T}
+\newcommand{\cofeB}{U}
+\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs
+\newcommand{\iFunc}{\Sigma}
+\newcommand{\fix}{\textdom{fix}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\textmon}[1]{\textsc{#1}}
+
+\newcommand{\monoid}{M}
+\newcommand{\mval}{\mathcal{V}}
+
+\newcommand{\melt}{a}
+\newcommand{\meltB}{b}
+\newcommand{\meltC}{c}
+\newcommand{\melts}{A}
+\newcommand{\meltsB}{B}
+
+\newcommand{\f}{\mathrm{f}} % for "frame"
+
+\newcommand{\mcar}[1]{|#1|}
+\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
+\newcommand{\munit}{\varepsilon}
+\newcommand{\mcore}[1]{{\mid}#1{\mid}} % using "|" here makes LaTeX diverge. WTF.
+\newcommand{\mnocore}\top
+\newcommand{\mtimes}{\mathbin{\cdot}}
+
+\newcommand{\mupd}{\rightsquigarrow}
+\newcommand{\mincl}[1][]{\ensuremath{\mathrel{\stackrel{#1}{\preccurlyeq}}}}
+
+\newcommand{\CMRAs}{\mathcal{CMRA}} % 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{\typeB}{\sigma}
+
+\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}
+
+% pure propositions
+\newcommand{\pprop}{\phi}
+\newcommand{\ppropB}{\psi}
+
+\newcommand{\pred}{\varPhi}
+\newcommand{\predB}{\Psi}
+\newcommand{\predC}{\Zeta}
+
+\newcommand{\gname}{\gamma}
+\newcommand{\iname}{\iota}
+
+\newcommand{\mask}{\mathcal{E}}
+\newcommand{\namesp}{\mathcal{N}}
+\newcommand{\namecl}[1]{{#1^{\kern0.2ex\uparrow}}}
+
+%% various pieces of Syntax
+\def\MU #1.{\mu #1.\spac}%
+\def\Lam #1.{\lambda #1.\spac}%
+
+\newcommand{\proves}{\vdash}
+\newcommand{\provesCoq}{\mathrel{\vdash_{\mbox{\!\includegraphics[width=0.7em]{rooster.jpg}}}}}
+\newcommand{\provesIff}{\mathrel{\dashv\vdash}}
+
+\newcommand{\wand}{\mathrel{-\!\!*}}
+
+% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
+\newcommand{\fmapsto}[1][]{\xmapsto{#1}}
+\newcommand{\gmapsto}{\hookrightarrow}%
+\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
+
+\NewDocumentCommand\wpre{m O{} m}%
+ {\textlog{wp}_{#2}\spac#1\spac{\big\{#3\big\}}}
+
+\newcommand{\later}{\mathop{\triangleright}}
+\newcommand{\always}{\mathop{\Box}}
+\newcommand{\pure}{\mathop{\blacksquare}}
+
+%% 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{\ownM}[1]{\textlog{Own}(#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
+ \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}}
+
+\newcommand\vsWand{\kern0.1ex\tikz[baseline=(base),line width=0.375pt]{%
+ \draw (0, 0) -- (0.4, 0); \draw (0, -0.075) -- (0.28, -0.075); \draw (0, 0.075) -- (0.28, 0.075);
+ \node at (0.4, -0.235) (ast) {$\smash{\scaleto{\ast}{1.2em}}$};
+ \node at (0.4, -0.095) (base) {};
+}{\vphantom{\Rrightarrow}}\kern-1.2ex}
+\NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]}
+
+% for now, the update modality looks like a pvs without masks.
+\NewDocumentCommand \upd {} {\mathop{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
+
+
+%% Hoare Triples
+\newcommand*{\hoaresizebox}[1]{%
+ \hbox{$\mathsurround=0pt{#1}\mathstrut$}}
+\newcommand*{\hoarescalebox}[2]{%
+ \hbox{\scalerel*[1ex]{#1}{#2}}}
+\newcommand{\triple}[5]{%
+ \setbox0=\hoaresizebox{{#3}{#5}}%
+ \setbox1=\hoarescalebox{#1}{\copy0}%
+ \setbox2=\hoarescalebox{#2}{\copy0}%
+ \copy1{#3}\copy2%
+ \; #4 \;%
+ \copy1{#5}\copy2}
+
+\newcommand{\bracket}[4][]{%
+ \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
+ \scalerel*[1ex]{#2}{\copy0}%
+ {#4}%
+ \scalerel*[1ex]{#3}{\copy0}}
+% \curlybracket[other] x
+\newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}}
+\newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}}
+
+\NewDocumentCommand \hoare {m m m O{}}{
+ \curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
+}
+
+\NewDocumentCommand \lahoare {m m m O{} O{}}{
+ \anglebracket{#1}\spac #2 \spac \anglebracket{#3}_{#4}^{#5}%
+}
+
+% \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{\persistent}[1]{\textlog{persistent}(#1)}
+\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)}
+\newcommand{\infinite}{\textlog{infinite}}
+
+\newcommand{\Prop}{\textlog{Prop}}
+\newcommand{\Pred}{\textlog{Pred}}
+
+\newcommand{\TRUE}{\textlog{True}}
+\newcommand{\FALSE}{\textlog{False}}
+\newcommand{\TLam}{\Lambda\spac}%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% GENERIC LANGUAGE SYNTAX AND SEMANTICS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\expr}{e}
+\newcommand{\val}{v}
+\newcommand{\valB}{w}
+\newcommand{\state}{\sigma}
+\newcommand{\step}{\ra}
+\newcommand{\hstep}{\ra_{\mathsf{h}}}
+\newcommand{\tpstep}{\ra_{\mathsf{tp}}}
+\newcommand{\lctx}{K}
+\newcommand{\Lctx}{\textdom{Ctx}}
+
+\newcommand{\toval}{\mathrm{to\_val}}
+\newcommand{\ofval}{\mathrm{val2expr}}
+\newcommand{\atomic}{\mathrm{atomic}}
+\newcommand{\red}{\mathrm{red}}
+\newcommand{\Lang}{\Lambda}
+
+\newcommand{\tpool}{T}
+
+\newcommand{\cfg}{\rho}
+
+\def\fill#1[#2]{#1 {[}\, #2\,{]} }
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% STANDARD DERIVED CONSTRUCTIONS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Option
+\newcommand{\option}[1]{#1^?}
+\newcommand{\Some}{}
+\newcommand{\None}{\textlog{None}}
+
+% Agreement
+\newcommand{\agm}{\ensuremath{\textmon{Ag}}}
+\newcommand{\aginj}{\textlog{ag}}
+
+% Fraction
+\newcommand{\fracm}{\ensuremath{\textmon{Frac}}}
+
+% Exclusive
+\newcommand{\exm}{\ensuremath{\textmon{Ex}}}
+\newcommand{\exinj}{\textlog{ex}}
+
+% Auth
+\newcommand{\authm}{\textmon{Auth}}
+\newcommand{\authfull}{\mathord{\bullet}\,}
+\newcommand{\authfrag}{\mathord{\circ}\,}
+
+\newcommand{\AuthInv}{\textsf{AuthInv}}
+\newcommand{\Auth}{\textsf{Auth}}
+
+% One-Shot
+\newcommand{\oneshotm}{\ensuremath{\textmon{OneShot}}}
+\newcommand{\ospending}{\textlog{pending}}
+\newcommand{\osshot}{\textlog{shot}}
+
+% STSs
+\newcommand{\STSCtx}{\textlog{StsCtx}}
+\newcommand{\STSSt}{\textlog{StsSt}}
+\newcommand{\STSclsd}{\textlog{closed}}
+\newcommand{\STSauth}{\textlog{auth}}
+\newcommand{\STSfrag}{\textlog{frag}}
+\newcommand{\STSS}{\mathcal{S}} % states
+\newcommand{\STST}{\mathcal{T}} % tokens
+\newcommand{\STSL}{\mathcal{L}} % labels
+\newcommand{\stsstep}{\ra}
+\newcommand{\ststrans}{\ra^{*}}% the relation relevant to the STS rules
+\newcommand{\stsfstep}[1]{\xrightarrow{#1}}
+\newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}}
+
+\tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}]
+\tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}]
+
+%% Stored Propositions
+\newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% CONCRETE LANGUAGE SYNTAX AND SEMANTICS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\textlang}[1]{\texttt{#1}}
+\newcommand{\langkw}[1]{\textlang{\color{blue} #1}}
+\newcommand{\lvar}[1]{\textit{#1}} % Yes, this makes language-level variables look like logic-level variables. but we still distinguish locally bound variables from global definitions.
+\newcommand{\lvarA}{\lvar{\var}}
+\newcommand{\lvarB}{\lvar{\varB}}
+\newcommand{\lvarC}{\lvar{\varC}}
+
+\newcommand{\loc}{\ell}
+
+\def\Let#1=#2in{\langkw{let} \spac #1 \mathrel{=} #2 \spac \langkw{in} \spac}
+\def\If#1then{\langkw{if} \spac #1 \spac \langkw{then} \spac}
+\def\Else{\spac\langkw{else} \spac}
+\def\Ref(#1){\langkw{ref}(#1)}
+\def\Rec#1 #2={\langkw{rec}\spac{#1}({#2}) \mathrel{=} }
+\def\Skip{\langkw{skip}}
+\def\Assert{\langkw{assert}}
+\newcommand\Inj[1]{\langkw{inj}_{#1}\spac}
+\newcommand\Proj[1]{\pi_{#1}\spac}
+\def\True{\langkw{true}}
+\def\False{\langkw{false}}
+\def\Match#1with#2=>#3|#4=>#5end{\langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\mid#4\Ra#5\spac\langkw{end}}
+\def\MatchML#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
+ \multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
+ &\Ra#3\\|&\Ra#5\\%
+ \multicolumn{3}{l}{\langkw{end}#6}%
+ \end{array}}}
+\def\MatchMLL#1with#2=>#3|#4=>#5|#6=>#7end#8{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
+ \multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
+ &\Ra#3\\|&\Ra#5\\|&\Ra#7\\%
+ \multicolumn{3}{l}{\langkw{end}#8}%
+ \end{array}}}
+\def\MatchS#1with#2=>#3end{
+ \langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\spac\langkw{end}}
+\newcommand\CAS{\langkw{CAS}}
+\newcommand*\Fork[1]{\langkw{fork}\spac\set{#1}}
+\newcommand\deref{\mathop{!}}
+\let\gets\leftarrow
+
+\newcommand{\fold}{\langkw{fold}\spac}
+\newcommand{\unfold}{\langkw{unfold}\spac}
+
+\newcommand{\op}[1]{\mathrel{#1}}
+
+\newcommand{\binop}{\circledcirc}
+\newcommand{\Plus}{\op{+}}
+\newcommand{\Minus}{\op{-}}
+\newcommand{\Mult}{\op{*}}
+\newcommand{\Eq}{\op{=}}
+\newcommand{\Lt}{\op{<}}
+
+\newcommand{\TT}{()}
+
+\endinput
diff --git a/docs/tex/listproc.sty b/docs/tex/listproc.sty
new file mode 100644
index 0000000000000000000000000000000000000000..1e3b167e8ae6779580cbc4454ec1a49435f23639
--- /dev/null
+++ b/docs/tex/listproc.sty
@@ -0,0 +1,349 @@
+%%
+%% This is file `listproc.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% listproc.dtx (with options: `package')
+%%
+%% Copyright (C) 2011 by Jesse A. Tov
+%%
+%% This file may be distributed and/or modified under the conditions of the
+%% LaTeX Project Public License, either version 1.2 of this license or (at
+%% your option) any later version. The latest version of this license is
+%% in:
+%%
+%% http://www.latex-project.org/lppl.txt
+%%
+%% and version 1.2 or later is part of all distributions of LaTeX
+%% version 1999/12/01 or later.
+%%
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{listproc}[2011/03/26 v0.1 (list processing)]
+\newcommand\newlist{\@lstp@def{}\newcommand}
+\newcommand\renewlist{\@lstp@def{}\renewcommand}
+\newcommand\deflist{\@lstp@def{}\def}
+\newcommand\gdeflist{\@lstp@def\global\def}
+\newcommand\@lstp@def[4]{%
+ #2#3{}%
+ \@for\lstp@def@temp:=#4\do{%
+ \eSnocTo\lstp@def@temp#3%
+ }%
+ #1\let#3#3%
+ \let\lstp@def@temp\@undefined
+}
+\newtoks\lstp@ta
+\newtoks\lstp@tb
+\newcommand\ConsTo{\@lstp@ConsTo\relax\def}
+\newcommand\gConsTo{\@lstp@ConsTo\global\def}
+\newcommand\eConsTo{\@lstp@ConsTo\relax\edef}
+\newcommand\xConsTo{\@lstp@ConsTo\global\edef}
+\newcommand\@lstp@ConsTo[4]{%
+ \long#2\lstp@temp{#3}%
+ \lstp@ta=\expandafter{\expandafter\listitem\expandafter{\lstp@temp}}%
+ \lstp@tb=\expandafter{#4}%
+ #1\edef#4{\the\lstp@ta\the\lstp@tb}%
+}
+\newcommand\SnocTo{\@lstp@SnocTo\relax\def}
+\newcommand\gSnocTo{\@lstp@SnocTo\global\def}
+\newcommand\eSnocTo{\@lstp@SnocTo\relax\edef}
+\newcommand\xSnocTo{\@lstp@SnocTo\global\edef}
+\newcommand\@lstp@SnocTo[4]{%
+ \long#2\lstp@temp{#3}%
+ \lstp@ta=\expandafter{\expandafter\listitem\expandafter{\lstp@temp}}%
+ \lstp@tb=\expandafter{#4}%
+ #1\edef#4{\the\lstp@tb\the\lstp@ta}%
+}
+\newcommand\AppendTo{\@lstp@AppendTo\relax}
+\newcommand\gAppendTo{\@lstp@AppendTo\global}
+\newcommand\@lstp@AppendTo[3]{%
+ \lstp@ta=\expandafter{#2}%
+ \lstp@tb=\expandafter{#3}%
+ #1\edef#3{\the\lstp@ta\the\lstp@tb}%
+}
+\long\def\@LopOff\listitem#1#2\@LopOff#3#4{%
+ #3{#1}%
+ #4{#2}%
+}
+\newcommand\@lstp@LopTo[4]{\expandafter\@LopOff#3\@LopOff{#1\def#4}{#2\def#3}}
+\newcommand\@lstp@RestTo[3]{\expandafter\@LopOff#2\@LopOff{\@gobble}{#1\def#3}}
+\newcommand\LopTo{\@lstp@LopTo\relax\relax}
+\newcommand\gLopTo{\@lstp@LopTo\global\global}
+\newcommand\glLopTo{\@lstp@LopTo\global\relax}
+\newcommand\lgLopTo{\@lstp@LopTo\relax\global}
+\newcommand\FirstTo{\@lstp@LopTo\relax\@gobblethree}
+\newcommand\gFirstTo{\@lstp@LopTo\global\@gobblethree}
+\newcommand\RestTo{\@lstp@RestTo\relax}
+\newcommand\gRestTo{\@lstp@RestTo\global}
+\newcommand*\IfList[1]{%
+ {%
+ \expandafter\@IfList#1\@IfList
+ }%
+}
+\def\@IfList#1#2\@IfList{%
+ \ifx\listitem#1\relax
+ \aftergroup\@firstoftwo
+ \else
+ \aftergroup\@secondoftwo
+ \fi
+}
+\def\@forList#1:=#2\do#3{%
+ \long\def\lstp@for@listitem##1{%
+ \long\def#1{##1}%
+ #3%
+ \let\listitem\lstp@for@listitem%
+ }%
+ \let\listitem\lstp@for@listitem%
+ #2%
+ \let\listitem\@undefined%
+}
+\newcommand\SetToListLength[2]{%
+ \lstp@length{#2}{\value{#1}}%
+}
+\newcommand\lstp@length[2]{%
+ #2=0 %
+ \long\def\listitem##1{\advance#2 by1 }%
+ #1\let\listitem\@undefined%
+}
+\newcommand\MapListTo{\@lstp@MapListTo\relax}
+\newcommand\gMapListTo{\@lstp@MapListTo\global}
+\newcommand\MapAndAppendTo{\@lstp@MapAndAppendTo\relax}
+\newcommand\gMapAndAppendTo{\@lstp@MapAndAppendTo\global}
+\newcommand\@lstp@MapListTo[4]{%
+ \let\lstp@map@temp#3%
+ #1\let#4\empty%
+ \@lstp@MapAndAppendTo{#1}{#2}\lstp@map@temp#4%
+ \let\lstp@map@temp\@undefined%
+}
+\newcommand\@lstp@MapAndAppendTo[4]{%
+ \long\def\listitem##1{\@lstp@SnocTo{#1}\def{#2}{#4}}%
+ #3%
+ \let\listitem\@undefined%
+}
+\newcommand\lstp@insert[3]{%
+ \edef\lstp@insert@temp@a{#2{#1}}%
+ \let\lstp@insert@temp@i#3%
+ \let#3\empty
+ \long\def\lstp@insert@listitem##1{%
+ \edef\lstp@insert@temp@b{#2{##1}}%
+ \ifnum\lstp@insert@temp@a<\lstp@insert@temp@b
+ \SnocTo{#1}{#3}%
+ \let\listitem\lstp@insert@listitem@done
+ \else
+ \let\listitem\lstp@insert@listitem
+ \fi
+ \SnocTo{##1}{#3}%
+ }%
+ \long\def\lstp@insert@listitem@done##1{\SnocTo{##1}{#3}}%
+ \let\listitem\lstp@insert@listitem
+ \lstp@insert@temp@i%
+ \ifx\listitem\lstp@insert@listitem%
+ \SnocTo{#1}{#3}%
+ \fi%
+ \let\lstp@insert@temp@i\@undefined%
+ \let\listitem\@undefined%
+}
+\providecommand\@apply@group[2]{#1#2}
+\newcommand\SortList[2][\@apply@group{}]{%
+ \let\lstp@sort@temp@i#2%
+ \let#2\empty
+ \long\def\lstp@sort@listitem##1{%
+ \lstp@insert{##1}{#1}{#2}%
+ \let\listitem\lstp@sort@listitem
+ }%
+ \let\listitem\lstp@sort@listitem
+ \lstp@sort@temp@i
+ \let\lstp@sort@temp@i\@undefined
+ \let\listitem\@undefined
+}
+\newcounter{lstp@ifsucc}
+\newcommand\lstp@ifsucc[2]{%
+ \setcounter{lstp@ifsucc}{#1}%
+ \addtocounter{lstp@ifsucc}{1}%
+ \ifnum#2=\value{lstp@ifsucc}%
+ \let\@lstp@ifsucc@kont\@firstoftwo
+ \else
+ \let\@lstp@ifsucc@kont\@secondoftwo
+ \fi
+ \@lstp@ifsucc@kont
+}
+\newcommand\CompressList[2][\@apply@group{}]{%
+ \let\lstp@compress@temp@i#2%
+ \let#2\empty
+ \def\lstp@compress@add@single{%
+ \expandafter\SnocTo\expandafter
+ {\expandafter\@single\expandafter{\lstp@compress@temp@a}}{#2}%
+ }%
+ \def\lstp@compress@add@range{%
+ \expandafter\expandafter\expandafter\SnocTo
+ \expandafter\expandafter\expandafter{%
+ \expandafter\expandafter\expandafter\@range
+ \expandafter\expandafter\expandafter{%
+ \expandafter\lstp@compress@temp@a\expandafter}%
+ \expandafter{\lstp@compress@temp@b}}#2%
+ }%
+ \long\def\lstp@compress@listitem@start##1{%
+ \def\lstp@compress@temp@a{##1}%
+ \edef\lstp@compress@temp@a@key{#1{##1}}%
+ \let\listitem\lstp@compress@listitem@single
+ }%
+ \long\def\lstp@compress@listitem@single##1{%
+ \def\lstp@compress@temp@b{##1}%
+ \edef\lstp@compress@temp@b@key{#1{##1}}%
+ \ifnum\lstp@compress@temp@a@key=\lstp@compress@temp@b@key
+ \let\listitem\lstp@compress@listitem@single
+ \else
+ \lstp@ifsucc{\lstp@compress@temp@a@key}{\lstp@compress@temp@b@key}
+ {\let\listitem\lstp@compress@listitem@range}
+ {\lstp@compress@add@single
+ \let\lstp@compress@temp@a\lstp@compress@temp@b
+ \let\lstp@compress@temp@a@key\lstp@compress@temp@b@key
+ \let\listitem\lstp@compress@listitem@single}%
+ \fi
+ }%
+ \long\def\lstp@compress@listitem@range##1{%
+ \def\lstp@compress@temp@c{##1}%
+ \edef\lstp@compress@temp@c@key{#1{##1}}%
+ \ifnum\lstp@compress@temp@b@key=\lstp@compress@temp@c@key
+ \let\listitem\lstp@compress@listitem@range
+ \else
+ \lstp@ifsucc{\lstp@compress@temp@b@key}{\lstp@compress@temp@c@key}
+ {%
+ \let\lstp@compress@temp@b\lstp@compress@temp@c
+ \let\lstp@compress@temp@b@key\lstp@compress@temp@c@key
+ \let\listitem\lstp@compress@listitem@range
+ }
+ {%
+ \lstp@compress@add@range
+ \let\lstp@compress@temp@a\lstp@compress@temp@c
+ \let\lstp@compress@temp@a@key\lstp@compress@temp@c@key
+ \let\listitem\lstp@compress@listitem@single
+ }%
+ \fi
+ }%
+ \let\listitem\lstp@compress@listitem@start
+ \lstp@compress@temp@i
+ \ifx\listitem\lstp@compress@listitem@single
+ \lstp@compress@add@single
+ \else
+ \ifx\listitem\lstp@compress@listitem@range
+ \lstp@compress@add@range
+ \fi
+ \fi
+ \let\lstp@compress@temp@a\@undefined
+ \let\lstp@compress@temp@b\@undefined
+ \let\lstp@compress@temp@c\@undefined
+ \let\lstp@compress@temp@a@key\@undefined
+ \let\lstp@compress@temp@b@key\@undefined
+ \let\lstp@compress@temp@c@key\@undefined
+ \let\lstp@compress@temp@i\@undefined
+ \let\listitem\@undefined
+}
+\newcommand\FormatListSepTwo{ and }
+\newcommand\FormatListSepMore{, }
+\newcommand\FormatListSepLast{, and }
+\newcounter{lstp@FormatList@length}
+\newcounter{lstp@FormatList@posn}
+\newcommand\FormatList[4]{{%
+ \deflist\lstp@FormatList@list{#4}%
+ \SetToListLength{lstp@FormatList@length}\lstp@FormatList@list%
+ \setcounter{lstp@FormatList@posn}{0}%
+ \ifnum\value{lstp@FormatList@length}=1%
+ #1%
+ \else%
+ #2%
+ \fi%
+ \def\listitem##1{%
+ \addtocounter{lstp@FormatList@posn}{1}%
+ \ifnum1<\value{lstp@FormatList@posn}%
+ \ifnum2=\value{lstp@FormatList@length}%
+ \FormatListSepTwo
+ \else
+ \ifnum\value{lstp@FormatList@length}=\value{lstp@FormatList@posn}%
+ \FormatListSepLast
+ \else
+ \FormatListSepMore
+ \fi
+ \fi
+ \fi
+ #3{##1}%
+ }%
+ \lstp@FormatList@list
+}}
+\newcommand\ListExpr[1]{\@lstp@ListExpr{#1}\relax}
+\newcommand\ListExprTo[2]{\@lstp@ListExpr{#1}{\def#2}}
+\newcommand\gListExprTo[2]{\@lstp@ListExpr{#1}{\gdef#2}}
+\newcommand\@lstp@defbinop[2]{%
+ \newcommand#1[2]{%
+ \Eval{##1}\let\@lstp@tmp\@lstp@acc
+ {\Eval{##2}}%
+ #2\@lstp@tmp\@lstp@acc
+ }%
+}
+\newcommand\@lstp@defunop[2]{%
+ \newcommand#1[1]{%
+ \Eval{##1}%
+ #2\@lstp@acc\@lstp@acc
+ }%
+}
+\newcommand\@lstp@definplaceunopopt[3][]{%
+ \newcommand#2[2][#1]{%
+ \Eval{##2}%
+ #3[##1]\@lstp@acc
+ \global\let\@lstp@acc\@lstp@acc
+ }%
+}
+\newcommand\@lstp@ListExpr[2]{%
+ {%
+ \gdef\@lstp@acc{}%
+ \def\Eval##1{%
+ \IfList{##1}{%
+ \global\let\@lstp@acc##1%
+ }{%
+ \@lstp@ifListOp##1\@lstp@ifListOp{%
+ ##1%
+ }{%
+ \xdef\@lstp@acc{##1}%
+ }%
+ }%
+ }%
+ \def\Q##1{\gdef\@lstp@acc{##1}}%
+ \def\Nil{\global\let\@lstp@acc\empty}%
+ \def\List##1{\gdeflist\@lstp@acc{##1}}%
+ \@lstp@defbinop\Cons\xConsTo
+ \@lstp@defbinop\Snoc\xSnocTo
+ \@lstp@defunop\First\gFirstTo
+ \@lstp@defunop\Rest\gRestTo
+ \@lstp@defbinop\Append\gAppendTo
+ \@lstp@definplaceunopopt[\@apply@group{}]\Sort\SortList
+ \@lstp@definplaceunopopt[\@apply@group{}]\Compress\CompressList
+ \newcommand\Map[2]{%
+ \Eval{##2}%
+ \gMapListTo{##1}\@lstp@acc\@lstp@acc
+ }%
+ \Eval{#1}%
+ }%
+ \def\@lstp@finish##1{#2{##1}}%
+ \expandafter\@lstp@finish\expandafter{\@lstp@acc}%
+}
+\def\@lstp@ifListOp#1#2\@lstp@ifListOp{%
+ \@lstp@ifInToks#1{
+ \Q\Nil\List\Cons\Snoc\Append
+ \First\Rest\Sort\Compress\Map
+ }
+}
+\newcommand\@lstp@ifInToks[2]{%
+ {%
+ \def\@tester##1#1##2\@tester{%
+ \ifx\@notfound##2\relax
+ \aftergroup\@secondoftwo
+ \else
+ \aftergroup\@firstoftwo
+ \fi
+ }%
+ \@tester#2\@lstp@ifInToks#1\@notfound\@tester
+ }%
+}
+\endinput
+%%
+%% End of file `listproc.sty'.
diff --git a/docs/tex/locallabel.sty b/docs/tex/locallabel.sty
new file mode 100644
index 0000000000000000000000000000000000000000..6c28e92e6364e8dda324b978030a45598b5942c4
--- /dev/null
+++ b/docs/tex/locallabel.sty
@@ -0,0 +1,118 @@
+% Locallabel
+%
+% Copyright (C) 2001, 2002, 2003 Didier R�my
+%
+% Author : Didier Remy
+% Version : 1.1.1
+% Bug Reports : to author
+% Web Site : http://pauillac.inria.fr/~remy/latex/
+%
+% Locallabel is free software; you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either version 2, or (at your option)
+% any later version.
+%
+% Locallabel is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details
+% (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File locallabel.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%
+
+%% Identification
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{locallabel}
+ [2001/23/02 v0.92 Locallabel]
+
+%% Preliminary declarations
+
+%% Options
+
+%% More declarations
+
+%% We use two counters: The global counter is incremented at each reset.
+%% Its value is the ``group'' of a local.
+%% The local counter is the last numeric value of a bound label in the
+%% current group. The value of a label #1 is globally set to
+%% \csname llb@\the\c@llb@global-#1\endcsname
+%% The global command \csname llb@\the\c@llb@global-#1*\endcsname is
+%% use to ensure that a label is only bound once. Usually a label is
+%% bound and declared at the same time with \llabel. It may also be bound in
+%% advance, with \lbind, for instance so as to control the numbering.
+%% Then, another \llabel must be used to declare it in the text.
+%% If no \lbind has been used before, the \llabel calls \lbind implicitlt.
+
+\newcounter{llb@global}
+\newcounter{llb@local}
+
+\newcommand \llb@find [1]
+ {\expandafter \ifx \csname llb@\the\c@llb@global-#1\endcsname \relax
+ \message {*** Local label #1 undefined in this context}%
+ \edef \llb@current {#1??}%
+ \else
+ \edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname}%
+ \fi}
+
+\newcommand \llb@make [1]
+ {\expandafter \ifx \csname llb@\the\c@llb@global-#1\endcsname \relax
+ \stepcounter{llb@local}\relax \expandafter
+ \xdef \csname llb@\the\c@llb@global-#1\endcsname {\the\c@llb@local}%
+ \edef \llb@current {\the\c@llb@local}%
+ \else
+ \expandafter \ifx \csname llb@\the\c@llb@global-#1*\endcsname \relax
+ \message {*** Local label #1 already defined in this countext!}%
+ \edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname ??}%
+ \else
+ \expandafter \global \expandafter \let
+ \csname llb@\the\c@llb@global-#1*\endcsname \relax
+ \edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname}
+ \fi
+ \fi
+}
+
+%%% Redefine those macros to change typsetting
+
+\newcommand \thelocallabel {\the \c@llb@local}
+
+\newcommand \LlabelTypeset [1] {(\textrm {\bfseries #1})}
+\newcommand \LrefTypeset [1] {(\textrm {#1)}}
+\newcommand \glabel [1]{\LlabelTypeset{\softtarget {#1}{#1}}}
+\newcommand \gref [1]{\LrefTypeset{\softlink {#1}{#1}}}
+
+%%% To reset all local labels---which just increment a global prefix.
+\newcommand \locallabelreset[1][0]%
+ {\stepcounter {llb@global}\setcounter {llb@local}{#1}}
+
+%%% Make a new local label, typeset it, and bind to the given name
+\def \llb@relax {\relax}
+\newcommand {\llabel}[2][\relax]%
+ {\llb@make{#2}%
+ \def \@test {#1}\ifx \@test\llb@relax\else
+ \edef \@currentlabel {\the\c@llb@local}%
+ \def \@test {#1}\ifx \@test\empty \def \@test{#2}\fi
+ \label{\@test}%
+ \fi%
+ \LlabelTypeset {\softtarget{llb@\the\c@llb@global-#2}{\llb@current}}}
+
+%%% Retreive the local label of given name and type set it.
+\newcommand \lref [1]
+ {\llb@find {#1}%
+ \LrefTypeset {\softlink {llb@\the\c@llb@global-#1}{\llb@current}}}
+
+%%% Make a new local label and bind it to the given name but do not typeset
+%%% it. Typesetting may then be done with \llabel non locally. Useful to
+%%% control the order of numberring.
+\newcommand \lbind [1]
+ {\llb@make {#1}%
+ \expandafter \global \expandafter
+ \let \csname llb@\the\c@llb@global-#1*\endcsname \empty}
+
+\AtBeginDocument {%
+ \@ifundefined{softlink}{\let \softlink \@secondoftwo}{}%
+ \@ifundefined{softtarget}{\let \softtarget \@secondoftwo}{}%
+}
diff --git a/docs/tex/pftools.sty b/docs/tex/pftools.sty
new file mode 100644
index 0000000000000000000000000000000000000000..56507b17dcb913596b5c615fc680272d18c91dba
--- /dev/null
+++ b/docs/tex/pftools.sty
@@ -0,0 +1,135 @@
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{pftools}
+
+\@ifundefined{basedir}{%
+\RequirePackage{locallabel}
+}{%
+\RequirePackage{\basedir locallabel}
+}%
+
+\RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
+\RequirePackage{xparse}
+\RequirePackage{xcolor}
+
+%% Biimplication inference rules
+% \biimp above below
+% The double lines obtained by the simpler
+% "\mprset{fraction={===}}" overlap the conclusion (e.g., the
+% mask E_M in an atomic triple).
+\newcommand*{\biimp}[2]{%
+ \hbox{%
+ \ooalign{%
+ $\genfrac{}{}{1.6pt}1{#1}{#2}$\cr%
+ $\color{white}\genfrac{}{}{0.8pt}1{\phantom{#1}}{\phantom{#2}}$%
+ }%
+ }%
+}
+\newcommand{\BIIMP}{\mprset{myfraction=\biimp}}
+
+
+%% inferH is infer with hyperlinked names.
+% \savelabel lab text: Arrange for \ref{lab} to print text and to link to the current spot.
+\newcommand*{\savelabel}[2]{%
+ % Think @currentlabel : text ref.
+ \edef\@currentlabel{#2}% Save text
+ \phantomsection% Correct hyper reference link
+ \label{#1}% Print text and store name↦text.
+}
+% \textlabel label text: Print and label text.
+\newcommand*{\textlabel}[2]{{#2}\savelabel{#1}{#2}}
+% \rulenamestyle visible
+\newcommand*{\rulenamestyle}[1]{{\TirNameStyle{#1}}} % From mathpartir.sty.
+% \ruleref [discharged] lab
+\def\optionaldischarge#1{%
+ \if\relax\detokenize{#1}\relax\else\ensuremath{^{#1}}\fi}
+\newcommand*{\ruleref}[2][]{\textmd{\rulenamestyle{\ref{#2}}}\optionaldischarge{#1}}
+\newcommand*{\fakeruleref}[2][]{\rulenamestyle{#2}\optionaldischarge{#1}}
+% \rulename label
+\newcommand*{\rulename}[1]{\rulenamestyle{\textlabel{#1}{#1}}}
+% \inferhref name lab premise conclusion
+\newcommand*{\inferhref}[4]{%
+ \inferrule*[lab=\textlabel{#2}{#1}]{#3}{#4}%
+}
+% \infernH name premise conclusion, if name a valid label.
+\newcommand*{\inferH}[3]{\inferhref{#1}{#1}{#2}{#3}}
+\newcommand*{\axiom}[1]{\infer{}{#1}}
+\newcommand*{\axiomhref}[3]{\inferhref{#1}{#2}{}{#3}}
+\newcommand*{\axiomH}[2]{\inferH{#1}{}{#2}}
+\newcommand*{\inferhrefB}[4]{{\BIIMP\inferhref{#1}{#2}{#3}{#4}}}
+\newcommand*{\inferB}[3][]{{\BIIMP\infer[#1]{#2}{#3}}}
+\newcommand*{\inferHB}[3]{{\BIIMP\inferH{#1}{#2}{#3}}}
+\newcommand*{\taghref}[2]{\label{#2}\tag{\rulenamestyle{#1}}}
+\newcommand*{\tagH}[1]{\taghref{#1}{#1}}
+
+% The sanity checks in \lbind and \llabel
+% don't work properly in amsmath environments
+% which perhaps lay out their contents more
+% than once. Use \lbind in such cases.
+% Sigh.
+
+\newcommand*{\tagL}[1]{\lbind{#1}\tag*{\llabel{#1}}}
+
+\newcommand*\ind[1][\quad]{#1\TAB=\TAB+}
+\newcommand*\unind{\TAB-}
+
+\newcommand\IND[1][\quad]{\\*\ind[#1]}
+\newcommand\UNIND{\unind \\}
+
+% Attribution: http://tex.stackexchange.com/questions/119473/tabbing-and-line-wrapping
+\newlength\pf@width
+\newcommand*{\CMT}[1]{%
+ \setlength\pf@width{\linewidth}%
+ \addtolength\pf@width{\@totalleftmargin}%
+ \addtolength\pf@width{-\dimen\@curtab}%
+ \parbox[t]{\pf@width}{\nobelowdisplayskip{#1}\ifhmode\strut\fi}}
+
+\colorlet{rescolor}{rgb:red,0;green,30;blue,55}
+\colorlet{ctxcolor}{black}
+\colorlet{codecolor}{rgb:red,76;green,177;blue,36}
+
+\newcommand*\res[1]{{\color{rescolor}\ensuremath{#1}}}
+%When \left\{ … \right\} looks ugly, remember Dave says you want \bracket.
+\NewDocumentCommand{\RES}{s m O{}}{%
+ $\displaystyle{{\left\{\res{%
+ \IfBooleanTF{#1}{\begin{inbox}[l]#2\end{inbox}}{#2}%
+ }\right\}}_{#3}}$}
+
+\NewDocumentCommand{\ARES}{m O{}}{%
+ ${\displaystyle{\bracket\langle\rangle{\color{rescolor}{#1}}}_{#2}}$}
+
+\newcommand*{\CODE}[1]{%
+ ${\displaystyle{\color{codecolor}#1}}$}
+
+\newcommand*{\VARS}[1]{%
+ Vars: ${\color{ctxcolor}\displaystyle{#1}}$}
+\newcommand*{\CTX}[1]{%
+ Context: ${\color{ctxcolor}\displaystyle{#1}}$}
+
+\newcommand*{\GOAL}[1]{%
+ Goal: ${\displaystyle{#1}}$}
+\newcommand*{\SUFF}[1]{%
+ Suff: ${\displaystyle{#1}}$}
+
+\newcommand*{\PFHAVE}[1]{%
+ Have: ${\displaystyle{#1}}$}
+
+\let\pf@origqedhere\qedhere
+\def\pf@setup{%
+ % A version of \qedhere that accounts for tabbing.
+ \def\qedhere{\TAB`\pf@origqedhere}%
+}
+
+\newcommand*{\TAGL}[1]{\TAB`\llabel{#1}}
+
+% The starred version lacks leading and trailing vertical space.
+\newenvironment{proofoutline*}
+{\partopsep=\z@skip \topsep=\z@skip% avoid initial space
+ \parskip\z@skip% avoid trailing space
+ \pf@setup\par\begingroup\Tabbing\ignorespaces}
+{\endTabbing\endgroup\unskip\ignorespacesafterend}
+
+\newenvironment{proofoutline}
+{\pf@setup\par\begingroup\Tabbing\ignorespaces}
+{\endTabbing\endgroup\ignorespacesafterend}
+
+\endinput
diff --git a/docs/tex/setup.tex b/docs/tex/setup.tex
new file mode 100644
index 0000000000000000000000000000000000000000..8c5b92196c1351dd6338fe89b83b3394d4d77514
--- /dev/null
+++ b/docs/tex/setup.tex
@@ -0,0 +1,112 @@
+
+\makeatletter%
+\@ifundefined{basedir}{%
+\newcommand\basedir{}%
+}{}%
+\makeatother%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% PACKAGES
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amsthm}
+\usepackage{amssymb}
+\usepackage{stmaryrd}
+
+\usepackage{\basedir mathpartir}
+
+\usepackage{\basedir pftools}
+\usepackage{\basedir iris}
+
+\usepackage{xcolor} % for print version
+
+\usepackage{graphicx}
+\usepackage{enumitem}
+\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}
+
+\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%
+}