diff --git a/doc/mem/.gitignore b/doc/mem/.gitignore
new file mode 100644
index 00000000..378eac25
--- /dev/null
+++ b/doc/mem/.gitignore
@@ -0,0 +1 @@
+build
diff --git a/doc/mem/Makefile b/doc/mem/Makefile
new file mode 100644
index 00000000..d17f2d0a
--- /dev/null
+++ b/doc/mem/Makefile
@@ -0,0 +1,12 @@
+.PHONY: main.pdf auto clean sync
+main: build/main.pdf
+
+build/main.pdf:
+	latexmk -pdf -halt-on-error -interaction=nonstopmode -shell-escape main.tex -outdir=build
+
+auto:
+	latexmk -pvc -pdf -halt-on-error -interaction=nonstopmode -shell-escape main.tex -outdir=build
+
+clean:
+	latexmk -C main.tex
+	rm -rf build
diff --git a/doc/mem/comments.sty b/doc/mem/comments.sty
new file mode 100644
index 00000000..8418e7ea
--- /dev/null
+++ b/doc/mem/comments.sty
@@ -0,0 +1,135 @@
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{comments}[2022/10/11 Inline and margin comments]
+% Written by Alex Ozdemir
+% Inspired by the peanutgallery package of Riad S. Wahby (and possibly others).
+
+\RequirePackage{options}
+\RequirePackage{xcolor}
+\RequirePackage{etoolbox}
+
+\newcounter{commentcoloruse}
+\newcounter{commentcolorsave}
+
+\newlength{\totalmargin}
+\newcommand{\SaveColor}[1]{%
+  \expandafter\def\csname CommentColorNumber\thecommentcolorsave\endcsname{#1}%
+  \stepcounter{commentcolorsave}%
+}
+\newcommand{\GetColor}{%
+  \expandafter\csname CommentColorNumber\thecommentcoloruse\endcsname%
+}
+\newcommand{\NextColor}{%
+  \stepcounter{commentcoloruse}
+}
+\def\primerlist{}
+
+\definecolor{BrewerQualitative0}{HTML}{1b9e77}
+\definecolor{BrewerQualitative1}{HTML}{d95f02}
+\definecolor{BrewerQualitative2}{HTML}{7570b3}
+\definecolor{BrewerQualitative3}{HTML}{e7298a}
+\definecolor{BrewerQualitative4}{HTML}{66a61e}
+\definecolor{BrewerQualitative5}{HTML}{e6ab02}
+\definecolor{BrewerQualitative6}{HTML}{a6761d}
+\definecolor{BrewerQualitative7}{HTML}{666666}
+\SaveColor{BrewerQualitative0}
+\SaveColor{BrewerQualitative1}
+\SaveColor{BrewerQualitative2}
+\SaveColor{BrewerQualitative3}
+\SaveColor{BrewerQualitative4}
+\SaveColor{BrewerQualitative5}
+\SaveColor{BrewerQualitative6}
+\SaveColor{BrewerQualitative7}
+
+\options{
+  /comments/.new family,
+  /comments/hide/.new toggle = false,
+  /comments/marginparsep/.new dim = \dimexpr1pt\relax,
+  /comments/marginparpush/.new dim = \dimexpr0.5em\relax,
+  /comments/marginparwidth/.new dim = \dimexpr0.5\totalmargin-2pt\relax,
+}
+
+\options@ProcessOptions{/comments}
+
+\iftoggle{/comments/hide}{%
+  \newcommand{\InlineComment}[2]{}
+  \newcommand{\MarginComment}[2]{\unskip}
+  \newcommand{\changebars}[2]{[{\color{magenta}\em\begingroup{#1}\endgroup}][{\color{magenta}\sout{#2}}]}
+}{%
+  \newcommand{\InlineComment}[2]{\begingroup \color{#1}{#2}\endgroup}
+  \newcommand{\MarginComment}[2]{\unskip{\color{#1}\vrule\vrule}{\marginpar{\raggedright\color{#1}\sffamily\selectfont\scriptsize #2}}}
+  \newcommand{\changebars}[2]{[{\color{magenta}\em\begingroup{#1}\endgroup}][{\color{magenta}\sout{#2}}]}
+}
+
+% \CommenterWithColor{INITIALS_ANYCASE}{COLORNAME}
+\newcommand{\CommenterWithColor}[2]{
+  \uppercase{\def\commentcsuppercase{#1}}%
+  \lowercase{\def\commentcslowercase{#1}}%
+  \expandafter\newcommand\csname \commentcslowercase\endcsname[1]{%
+    \InlineComment{#2}{\uppercase{#1}: ##1}}
+  \expandafter\newcommand\csname \commentcsuppercase\endcsname[1]{%
+    \MarginComment{#2}{\uppercase{#1}: ##1}}
+  \expandafter\def\expandafter\primerlist\expandafter{\primerlist
+
+    \noindent\texttt{-} {\small\color{#2} \texttt{\textbackslash \lowercase{#1}\{Test\}}} creates an
+    inline comment:
+    \lowercase{\csname#1\endcsname}{Test}
+
+    \noindent\texttt{-} {\small\color{#2} \texttt{\textbackslash \uppercase{#1}\{Test\}}}
+    creates a margin comment:
+    \uppercase{\csname#1\endcsname}{Test}
+  }
+}
+
+\def\commentprimer{
+  \subsection*{Comment System}
+
+  \noindent Welcome to \texttt{comments.sty}.
+
+  \noindent Macros:
+
+  \noindent\texttt{-} {\small\texttt{\textbackslash Commenter\{AO\}}}
+  creates macros
+  {\small\texttt{\textbackslash ao}}
+  and
+  {\small\texttt{\textbackslash AO}}.
+
+  \noindent\texttt{-} {\small\texttt{\textbackslash
+    CommenterWithColor\{AO\}\{COLOR\_NAME\}}}
+    is similar.
+
+  \noindent\texttt{-} {\small\texttt{\textbackslash changebars\{new\}\{old\}}} yields
+  \changebars{new}{old}.
+
+  \noindent\texttt{-} {\small\texttt{\textbackslash commentprimer}}
+    outputs this help message.
+
+  \primerlist
+
+
+  \noindent Package options:
+
+  \noindent\texttt{-} \texttt{\small hide} hide all comments and apply changes
+
+  \noindent\texttt{-} \texttt{\small marginparpush=LEN} distance between comments
+
+  \noindent\texttt{-} \texttt{\small marginparsep=LEN} distance from column
+
+  \noindent\texttt{-} \texttt{\small marginparwidth=LEN} width
+}
+
+% Utility for expanding macro arguments to text before expanding the macro
+\long\gdef\expandargumentsof#1#2\stopexpansion{%
+  \edef\tmp{\noexpand#1#2}\tmp%
+}
+
+\newcommand{\Commenter}[1]{
+  \expandargumentsof\CommenterWithColor{#1}{\GetColor}\stopexpansion
+  \NextColor
+}
+
+\AtEndPreamble{
+  \setlength{\totalmargin}{\dimexpr\paperwidth-\textwidth\relax}
+  \setlength{\marginparsep}{\option{/comments/marginparsep}}
+  \setlength{\marginparpush}{\option{/comments/marginparpush}}
+  \setlength{\marginparwidth}{\option{/comments/marginparwidth}}
+}
diff --git a/doc/mem/der_xgcd/dnc.py b/doc/mem/der_xgcd/dnc.py
new file mode 100755
index 00000000..7cdf4571
--- /dev/null
+++ b/doc/mem/der_xgcd/dnc.py
@@ -0,0 +1,48 @@
+#!/usr/bin/env python
+
+from sage.misc.misc_c import prod
+from sage.rings.finite_rings.finite_field_constructor import GF
+from sage.rings.polynomial.polynomial_ring_constructor import PolynomialRing
+
+p = 31
+F = GF(p)
+R = PolynomialRing(F, "x")
+x = R.gen(0)
+
+
+def v(*xs):
+    if len(xs) == 1 and isinstance(xs, list):
+        xs = xs[0]
+    return prod([x - a for a in xs])
+
+
+def dgcd(p):
+    g, s, t = p.xgcd(p.derivative())
+    return g, s, t, s.factor(), t.factor()
+
+
+f = v(2, 5, 7)
+g = v(1, 3, 8)
+print("f", f)
+print("g", g)
+_, fg, gf = f.xgcd(g)
+print("fg", fg)
+print("gf", gf)
+_, fF, Ff = f.xgcd(f.derivative())
+print("fF", fF)
+print("Ff", Ff)
+_, gG, Gg = g.xgcd(g.derivative())
+print("gG", gG)
+print("Gg", Gg)
+h = f * g
+print("h", h)
+print("h", h.factor())
+print("H", h.derivative().factor())
+_, hH, Hh = h.xgcd(h.derivative())
+print("hH", hH)
+print("Hh", Hh)
+c = Hh.coefficients()[-1]
+print(dgcd(v(-1, -2, -3, -4, -5)))
+print(dgcd(v(-1, -2, -3, -4)))
+print(dgcd(v(-1, -2, -3)))
+print(dgcd(v(-1, -2)))
diff --git a/doc/mem/macros.tex b/doc/mem/macros.tex
new file mode 100644
index 00000000..ca470a98
--- /dev/null
+++ b/doc/mem/macros.tex
@@ -0,0 +1,53 @@
+\newcommand{\xspacemm}{\ifmmode\else\xspace\fi}
+
+\newcommand{\prover}{\ensuremath{\mathcal{P}}\xspacemm}
+\newcommand{\verifier}{\ensuremath{\mathcal{V}}\xspacemm}
+\newcommand{\constraints}{\ensuremath{\mathcal{C}}\xspacemm}
+\newcommand{\FF}{\ensuremath{\mathbb{F}}\xspace}
+\newcommand{\NN}{\ensuremath{\mathbb{N}}\xspace}
+\newcommand{\zo}{\ensuremath{\{0,1\}}\xspace}
+\newcommand{\ext}{\mathsf{Ext}\xspacemm}
+\newcommand{\enc}{\mathsf{Enc}\xspacemm}
+\newcommand{\Prove}{\mathsf{Prove}\xspacemm}
+\newcommand{\Verify}{\mathsf{Verify}\xspacemm}
+\newcommand{\negl}{\mathsf{negl}\xspacemm}
+\newcommand{\rfrom}{\xleftarrow{\text{\$}}}
+
+\newcommand{\MA}{\ensuremath{\mathcal{MA}}\xspacemm}
+\newcommand{\NP}{\ensuremath{\mathcal{NP}}\xspacemm}
+\newcommand{\ZoK}{ZoKrates\xspacemm}
+\newcommand{\zkSNARK}{zkSNARK\xspacemm}
+\newcommand{\zkSNARKs}{zkSNARKs\xspacemm}
+\newcommand{\zsharp}{Z\#\xspacemm}
+
+\newcommand{\pp}{\ensuremath{\mathsf{pp}}\xspacemm}
+\newcommand{\bnds}{\ensuremath{\mathsf{bnds}}\xspacemm}
+
+% Memory
+\newcommand{\MemAcc}{\ensuremath{\mathsf{acc}}\xspacemm}
+\newcommand{\MemWr}{\ensuremath{\mathsf{wr}}\xspacemm}
+\newcommand{\MemAdr}{\ensuremath{\mathsf{adr}}\xspacemm}
+\newcommand{\MemVal}{\ensuremath{\mathsf{val}}\xspacemm}
+\newcommand{\MemTime}{\ensuremath{\mathsf{t}}\xspacemm}
+
+\newcommand{\CtxElem}{\ensuremath{\mathsf{CtxElem}}\xspacemm}
+\newcommand{\MsHash}{\ensuremath{{H_\text{r}}}\xspacemm}
+\newcommand{\Uhf}{\ensuremath{{H_\text{c}}}\xspacemm}
+
+% CIC/lean terms
+\newcommand{\dbrk}[1]{\ensuremath{{[\![{#1}]\!]}}\xspacemm}
+\newcommand{\nat}{\ensuremath{\texttt{nat}}\xspacemm}
+\newcommand{\add}{\ensuremath{\texttt{add}}\xspacemm}
+
+% Eval
+\newcommand{\stdlib}{\ensuremath{\mathsf{stdlib}}\xspacemm}
+\newcommand{\mathlib}{\ensuremath{\mathsf{mathlib}}\xspacemm}
+\newcommand{\program}{\ensuremath{\mathsf{program}}\xspacemm}
+
+% \let\oldvec\vec
+\renewcommand{\vec}[1]{\ensuremath{\mathbf{#1}}\xspacemm}
+
+\newcommand{\csPerA}[1]{{\color{blue}\ensuremath{#1\cdot A} constraints}}
+\newcommand{\romCsPerA}[1]{{\color{purple}(ROM: \ensuremath{#1\cdot A} constraints)}}
+\newcommand{\csPerN}[1]{{\color{red}\ensuremath{#1 \cdot N} constraints}}
+\newcommand{\csPerT}[1]{{\color{blue}\ensuremath{#1\cdot 3A} constraints}}
diff --git a/doc/mem/main.tex b/doc/mem/main.tex
new file mode 100644
index 00000000..1d9d6798
--- /dev/null
+++ b/doc/mem/main.tex
@@ -0,0 +1,134 @@
+\documentclass[conference,compsoc]{article}
+%\documentclass[conference,compsoc]{IEEEtran}
+%% \BibTeX command to typeset BibTeX logo in the docs
+\AtBeginDocument{%
+  \providecommand\BibTeX{{%
+    \normalfont B\kern-0.5em{\scshape i\kern-0.25em b}\kern-0.8em\TeX}}}
+
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage[normalem]{ulem}
+\usepackage[]{outlines}
+\usepackage[dvipsnames]{xcolor}
+\usepackage{amsmath,amssymb,comment}
+\usepackage[bookmarksnumbered,unicode]{hyperref}
+\hypersetup{                    % ...like so
+  pdftex,
+  colorlinks,
+  pdfborder={0 0 0},
+  pdfmenubar=false,
+  pdfpagemode=UseNone,
+  pdfnonfullscreenpagemode=UseNone,
+  bookmarksopen=false,
+  bookmarks=false,
+  breaklinks=true,
+  linkcolor={green!50!black},
+  citecolor={red!50!black},
+  urlcolor={blue!50!black}
+}
+
+% add `hide` to hide comments
+\usepackage[]{comments}
+\Commenter{EL}
+\Commenter{AO}
+\Commenter{DB}
+
+\usepackage[square,comma,numbers,sort&compress]{natbib}
+
+\usepackage{xspace}
+\usepackage[htt]{hyphenat}
+\usepackage{listings}
+\usepackage{nicefrac}
+\usepackage{tikz}
+\usetikzlibrary{arrows.meta}
+\tikzset{>=Latex[]}
+\usepackage{booktabs}
+\usepackage{menukeys}
+\bibliographystyle{ieeetr}
+\usepackage{caption}
+\usepackage{subcaption}
+% \usepackage[nohead,
+%             left=0.625in,right=0.625in,top=0.75in,bottom=0.75in,
+%             %left=0.633in,right=0.633in,top=0.75in,bottom=0.75in,
+%             columnsep=0.25in
+%             ]{geometry}
+
+\usepackage{bussproofs}
+\usepackage{backnaur}
+
+% AO: Oakland minimum is 11pt, but that's crazy.
+\usepackage{leading}
+
+\newcommand\sysname{ZkPi\xspace}
+\newcommand\sys{\sysname}
+\newcommand\CIC{CIC\xspace}
+
+\input{macros}
+
+%\usepackage[text=DRAFT\ do\ not\ distribute,fontsize=0.08\paperwidth,angle=0,vpos=0.95\paperheight]{draftwatermark}
+
+% careful
+\hyphenation{an-aly-sis}
+
+% Eddie Kohler protect us
+\frenchspacing
+
+\begin{document}
+
+%%
+%% The "title" command has an optional parameter,
+\title{
+%\vspace*{-1cm}
+Persistent Memory
+%\vspace*{-0.25cm}
+}
+%\subtitle{Shared Compiler Infrastructure for Constraint Solvers and Cryptosystems}
+
+\author{}
+% \author{%
+%   \IEEEauthorblockN{%
+%     Evan Laufer\quad
+%     Alex Ozdemir\quad
+%     Dan Boneh
+%   }%\\
+%   \IEEEauthorblockA{%
+%     Stanford University
+%   }
+% }
+
+
+%%
+%% By default, the full list of authors will be used in the page %% headers. Often, this list is too long, and will overlap %% other information printed in the page headers. This command allows
+%% the author to define a more concise list
+%% of authors' names for this purpose.
+%\renewcommand{\shortauthors}{Trovato and Tobin, et al.}
+
+\maketitle
+
+\begin{abstract}
+  TODO
+% \input{abstract}
+\end{abstract}
+
+\commentprimer
+
+\input{persistent}
+\input{sparse}
+\input{volatile}
+
+\pagebreak
+
+\begin{flushleft}
+\footnotesize
+\setlength{\parskip}{0pt}
+\setlength{\itemsep}{0pt}
+%\bibliographystyle{abbrv}
+%\bibliography{myabbrev,cryptobib/crypto,refs}
+\bibliography{refs}
+\end{flushleft}
+
+%% If your work has an appendix, this is the place to put it.
+% \appendices
+
+\end{document}
+\endinput
diff --git a/doc/mem/models/Makefile b/doc/mem/models/Makefile
new file mode 100644
index 00000000..c3e2a214
--- /dev/null
+++ b/doc/mem/models/Makefile
@@ -0,0 +1,5 @@
+data.csv: gcd_uniq.py
+	python $< > $@
+
+
+
diff --git a/doc/mem/models/data.csv b/doc/mem/models/data.csv
new file mode 100644
index 00000000..56a4dff2
--- /dev/null
+++ b/doc/mem/models/data.csv
@@ -0,0 +1,1709 @@
+log2_accesses,addr_bits,name,cost,k
+0,4,bitsplit,4.0,
+0,4,sort,51.0,
+0,4,subbitsplit,18.0,2
+0,4,gcd_uniq,6.0,
+3,4,bitsplit,32.0,
+3,4,sort,72.0,
+3,4,subbitsplit,56.0,3
+3,4,gcd_uniq,48.0,
+6,4,bitsplit,256.0,
+6,4,sort,240.0,
+6,4,subbitsplit,240.0,4
+6,4,gcd_uniq,384.0,
+9,4,bitsplit,2048.0,
+9,4,sort,1584.0,
+9,4,subbitsplit,1584.0,4
+9,4,gcd_uniq,3072.0,
+12,4,bitsplit,16384.0,
+12,4,sort,12336.0,
+12,4,subbitsplit,12336.0,4
+12,4,gcd_uniq,24576.0,
+15,4,bitsplit,131072.0,
+15,4,sort,98352.0,
+15,4,subbitsplit,98352.0,4
+15,4,gcd_uniq,196608.0,
+18,4,bitsplit,1048576.0,
+18,4,sort,786480.0,
+18,4,subbitsplit,786480.0,4
+18,4,gcd_uniq,1572864.0,
+0,5,bitsplit,5.0,
+0,5,sort,99.0,
+0,5,subbitsplit,19.0,2
+0,5,gcd_uniq,6.0,
+3,5,bitsplit,40.0,
+3,5,sort,120.0,
+3,5,subbitsplit,64.0,3
+3,5,gcd_uniq,48.0,
+6,5,bitsplit,320.0,
+6,5,sort,288.0,
+6,5,subbitsplit,288.0,5
+6,5,gcd_uniq,384.0,
+9,5,bitsplit,2560.0,
+9,5,sort,1632.0,
+9,5,subbitsplit,1632.0,5
+9,5,gcd_uniq,3072.0,
+12,5,bitsplit,20480.0,
+12,5,sort,12384.0,
+12,5,subbitsplit,12384.0,5
+12,5,gcd_uniq,24576.0,
+15,5,bitsplit,163840.0,
+15,5,sort,98400.0,
+15,5,subbitsplit,98400.0,5
+15,5,gcd_uniq,196608.0,
+18,5,bitsplit,1310720.0,
+18,5,sort,786528.0,
+18,5,subbitsplit,786528.0,5
+18,5,gcd_uniq,1572864.0,
+0,6,bitsplit,6.0,
+0,6,sort,195.0,
+0,6,subbitsplit,21.0,2
+0,6,gcd_uniq,6.0,
+3,6,bitsplit,48.0,
+3,6,sort,216.0,
+3,6,subbitsplit,72.0,3
+3,6,gcd_uniq,48.0,
+6,6,bitsplit,384.0,
+6,6,sort,384.0,
+6,6,subbitsplit,352.0,5
+6,6,gcd_uniq,384.0,
+9,6,bitsplit,3072.0,
+9,6,sort,1728.0,
+9,6,subbitsplit,1728.0,6
+9,6,gcd_uniq,3072.0,
+12,6,bitsplit,24576.0,
+12,6,sort,12480.0,
+12,6,subbitsplit,12480.0,6
+12,6,gcd_uniq,24576.0,
+15,6,bitsplit,196608.0,
+15,6,sort,98496.0,
+15,6,subbitsplit,98496.0,6
+15,6,gcd_uniq,196608.0,
+18,6,bitsplit,1572864.0,
+18,6,sort,786624.0,
+18,6,subbitsplit,786624.0,6
+18,6,gcd_uniq,1572864.0,
+0,7,bitsplit,7.0,
+0,7,sort,387.0,
+0,7,subbitsplit,22.0,2
+0,7,gcd_uniq,6.0,
+3,7,bitsplit,56.0,
+3,7,sort,408.0,
+3,7,subbitsplit,80.0,3
+3,7,gcd_uniq,48.0,
+6,7,bitsplit,448.0,
+6,7,sort,576.0,
+6,7,subbitsplit,416.0,5
+6,7,gcd_uniq,384.0,
+9,7,bitsplit,3584.0,
+9,7,sort,1920.0,
+9,7,subbitsplit,1920.0,7
+9,7,gcd_uniq,3072.0,
+12,7,bitsplit,28672.0,
+12,7,sort,12672.0,
+12,7,subbitsplit,12672.0,7
+12,7,gcd_uniq,24576.0,
+15,7,bitsplit,229376.0,
+15,7,sort,98688.0,
+15,7,subbitsplit,98688.0,7
+15,7,gcd_uniq,196608.0,
+18,7,bitsplit,1835008.0,
+18,7,sort,786816.0,
+18,7,subbitsplit,786816.0,7
+18,7,gcd_uniq,1572864.0,
+0,8,bitsplit,8.0,
+0,8,sort,771.0,
+0,8,subbitsplit,24.0,2
+0,8,gcd_uniq,6.0,
+3,8,bitsplit,64.0,
+3,8,sort,792.0,
+3,8,subbitsplit,88.0,3
+3,8,gcd_uniq,48.0,
+6,8,bitsplit,512.0,
+6,8,sort,960.0,
+6,8,subbitsplit,432.0,4
+6,8,gcd_uniq,384.0,
+9,8,bitsplit,4096.0,
+9,8,sort,2304.0,
+9,8,subbitsplit,2304.0,8
+9,8,gcd_uniq,3072.0,
+12,8,bitsplit,32768.0,
+12,8,sort,13056.0,
+12,8,subbitsplit,13056.0,8
+12,8,gcd_uniq,24576.0,
+15,8,bitsplit,262144.0,
+15,8,sort,99072.0,
+15,8,subbitsplit,99072.0,8
+15,8,gcd_uniq,196608.0,
+18,8,bitsplit,2097152.0,
+18,8,sort,787200.0,
+18,8,subbitsplit,787200.0,8
+18,8,gcd_uniq,1572864.0,
+0,9,bitsplit,9.0,
+0,9,sort,1539.0,
+0,9,subbitsplit,25.0,2
+0,9,gcd_uniq,6.0,
+3,9,bitsplit,72.0,
+3,9,sort,1560.0,
+3,9,subbitsplit,96.0,3
+3,9,gcd_uniq,48.0,
+6,9,bitsplit,576.0,
+6,9,sort,1728.0,
+6,9,subbitsplit,496.0,4
+6,9,gcd_uniq,384.0,
+9,9,bitsplit,4608.0,
+9,9,sort,3072.0,
+9,9,subbitsplit,2816.0,8
+9,9,gcd_uniq,3072.0,
+12,9,bitsplit,36864.0,
+12,9,sort,13824.0,
+12,9,subbitsplit,13824.0,9
+12,9,gcd_uniq,24576.0,
+15,9,bitsplit,294912.0,
+15,9,sort,99840.0,
+15,9,subbitsplit,99840.0,9
+15,9,gcd_uniq,196608.0,
+18,9,bitsplit,2359296.0,
+18,9,sort,787968.0,
+18,9,subbitsplit,787968.0,9
+18,9,gcd_uniq,1572864.0,
+0,10,bitsplit,10.0,
+0,10,sort,3075.0,
+0,10,subbitsplit,27.0,2
+0,10,gcd_uniq,6.0,
+3,10,bitsplit,80.0,
+3,10,sort,3096.0,
+3,10,subbitsplit,104.0,3
+3,10,gcd_uniq,48.0,
+6,10,bitsplit,640.0,
+6,10,sort,3264.0,
+6,10,subbitsplit,480.0,5
+6,10,gcd_uniq,384.0,
+9,10,bitsplit,5120.0,
+9,10,sort,4608.0,
+9,10,subbitsplit,3168.0,5
+9,10,gcd_uniq,3072.0,
+12,10,bitsplit,40960.0,
+12,10,sort,15360.0,
+12,10,subbitsplit,15360.0,10
+12,10,gcd_uniq,24576.0,
+15,10,bitsplit,327680.0,
+15,10,sort,101376.0,
+15,10,subbitsplit,101376.0,10
+15,10,gcd_uniq,196608.0,
+18,10,bitsplit,2621440.0,
+18,10,sort,789504.0,
+18,10,subbitsplit,789504.0,10
+18,10,gcd_uniq,1572864.0,
+0,11,bitsplit,11.0,
+0,11,sort,6147.0,
+0,11,subbitsplit,28.0,2
+0,11,gcd_uniq,6.0,
+3,11,bitsplit,88.0,
+3,11,sort,6168.0,
+3,11,subbitsplit,112.0,3
+3,11,gcd_uniq,48.0,
+6,11,bitsplit,704.0,
+6,11,sort,6336.0,
+6,11,subbitsplit,544.0,5
+6,11,gcd_uniq,384.0,
+9,11,bitsplit,5632.0,
+9,11,sort,7680.0,
+9,11,subbitsplit,3680.0,5
+9,11,gcd_uniq,3072.0,
+12,11,bitsplit,45056.0,
+12,11,sort,18432.0,
+12,11,subbitsplit,18432.0,11
+12,11,gcd_uniq,24576.0,
+15,11,bitsplit,360448.0,
+15,11,sort,104448.0,
+15,11,subbitsplit,104448.0,11
+15,11,gcd_uniq,196608.0,
+18,11,bitsplit,2883584.0,
+18,11,sort,792576.0,
+18,11,subbitsplit,792576.0,11
+18,11,gcd_uniq,1572864.0,
+0,12,bitsplit,12.0,
+0,12,sort,12291.0,
+0,12,subbitsplit,30.0,2
+0,12,gcd_uniq,6.0,
+3,12,bitsplit,96.0,
+3,12,sort,12312.0,
+3,12,subbitsplit,120.0,4
+3,12,gcd_uniq,48.0,
+6,12,bitsplit,768.0,
+6,12,sort,12480.0,
+6,12,subbitsplit,576.0,6
+6,12,gcd_uniq,384.0,
+9,12,bitsplit,6144.0,
+9,12,sort,13824.0,
+9,12,subbitsplit,3264.0,6
+9,12,gcd_uniq,3072.0,
+12,12,bitsplit,49152.0,
+12,12,sort,24576.0,
+12,12,subbitsplit,22528.0,11
+12,12,gcd_uniq,24576.0,
+15,12,bitsplit,393216.0,
+15,12,sort,110592.0,
+15,12,subbitsplit,110592.0,12
+15,12,gcd_uniq,196608.0,
+18,12,bitsplit,3145728.0,
+18,12,sort,798720.0,
+18,12,subbitsplit,798720.0,12
+18,12,gcd_uniq,1572864.0,
+0,13,bitsplit,13.0,
+0,13,sort,24579.0,
+0,13,subbitsplit,31.0,2
+0,13,gcd_uniq,6.0,
+3,13,bitsplit,104.0,
+3,13,sort,24600.0,
+3,13,subbitsplit,128.0,4
+3,13,gcd_uniq,48.0,
+6,13,bitsplit,832.0,
+6,13,sort,24768.0,
+6,13,subbitsplit,640.0,6
+6,13,gcd_uniq,384.0,
+9,13,bitsplit,6656.0,
+9,13,sort,26112.0,
+9,13,subbitsplit,3776.0,6
+9,13,gcd_uniq,3072.0,
+12,13,bitsplit,53248.0,
+12,13,sort,36864.0,
+12,13,subbitsplit,26624.0,11
+12,13,gcd_uniq,24576.0,
+15,13,bitsplit,425984.0,
+15,13,sort,122880.0,
+15,13,subbitsplit,122880.0,13
+15,13,gcd_uniq,196608.0,
+18,13,bitsplit,3407872.0,
+18,13,sort,811008.0,
+18,13,subbitsplit,811008.0,13
+18,13,gcd_uniq,1572864.0,
+0,14,bitsplit,14.0,
+0,14,sort,49155.0,
+0,14,subbitsplit,33.0,2
+0,14,gcd_uniq,6.0,
+3,14,bitsplit,112.0,
+3,14,sort,49176.0,
+3,14,subbitsplit,136.0,4
+3,14,gcd_uniq,48.0,
+6,14,bitsplit,896.0,
+6,14,sort,49344.0,
+6,14,subbitsplit,704.0,6
+6,14,gcd_uniq,384.0,
+9,14,bitsplit,7168.0,
+9,14,sort,50688.0,
+9,14,subbitsplit,3456.0,7
+9,14,gcd_uniq,3072.0,
+12,14,bitsplit,57344.0,
+12,14,sort,61440.0,
+12,14,subbitsplit,24960.0,7
+12,14,gcd_uniq,24576.0,
+15,14,bitsplit,458752.0,
+15,14,sort,147456.0,
+15,14,subbitsplit,147456.0,14
+15,14,gcd_uniq,196608.0,
+18,14,bitsplit,3670016.0,
+18,14,sort,835584.0,
+18,14,subbitsplit,835584.0,14
+18,14,gcd_uniq,1572864.0,
+0,15,bitsplit,15.0,
+0,15,sort,98307.0,
+0,15,subbitsplit,34.0,2
+0,15,gcd_uniq,6.0,
+3,15,bitsplit,120.0,
+3,15,sort,98328.0,
+3,15,subbitsplit,144.0,4
+3,15,gcd_uniq,48.0,
+6,15,bitsplit,960.0,
+6,15,sort,98496.0,
+6,15,subbitsplit,672.0,5
+6,15,gcd_uniq,384.0,
+9,15,bitsplit,7680.0,
+9,15,sort,99840.0,
+9,15,subbitsplit,3968.0,7
+9,15,gcd_uniq,3072.0,
+12,15,bitsplit,61440.0,
+12,15,sort,110592.0,
+12,15,subbitsplit,29056.0,7
+12,15,gcd_uniq,24576.0,
+15,15,bitsplit,491520.0,
+15,15,sort,196608.0,
+15,15,subbitsplit,180224.0,14
+15,15,gcd_uniq,196608.0,
+18,15,bitsplit,3932160.0,
+18,15,sort,884736.0,
+18,15,subbitsplit,884736.0,15
+18,15,gcd_uniq,1572864.0,
+0,16,bitsplit,16.0,
+0,16,sort,196611.0,
+0,16,subbitsplit,36.0,2
+0,16,gcd_uniq,6.0,
+3,16,bitsplit,128.0,
+3,16,sort,196632.0,
+3,16,subbitsplit,144.0,4
+3,16,gcd_uniq,48.0,
+6,16,bitsplit,1024.0,
+6,16,sort,196800.0,
+6,16,subbitsplit,736.0,5
+6,16,gcd_uniq,384.0,
+9,16,bitsplit,8192.0,
+9,16,sort,198144.0,
+9,16,subbitsplit,3840.0,8
+9,16,gcd_uniq,3072.0,
+12,16,bitsplit,65536.0,
+12,16,sort,208896.0,
+12,16,subbitsplit,25344.0,8
+12,16,gcd_uniq,24576.0,
+15,16,bitsplit,524288.0,
+15,16,sort,294912.0,
+15,16,subbitsplit,197376.0,8
+15,16,gcd_uniq,196608.0,
+18,16,bitsplit,4194304.0,
+18,16,sort,983040.0,
+18,16,subbitsplit,983040.0,16
+18,16,gcd_uniq,1572864.0,
+0,17,bitsplit,17.0,
+0,17,sort,393219.0,
+0,17,subbitsplit,37.0,2
+0,17,gcd_uniq,6.0,
+3,17,bitsplit,136.0,
+3,17,sort,393240.0,
+3,17,subbitsplit,152.0,4
+3,17,gcd_uniq,48.0,
+6,17,bitsplit,1088.0,
+6,17,sort,393408.0,
+6,17,subbitsplit,800.0,5
+6,17,gcd_uniq,384.0,
+9,17,bitsplit,8704.0,
+9,17,sort,394752.0,
+9,17,subbitsplit,4352.0,8
+9,17,gcd_uniq,3072.0,
+12,17,bitsplit,69632.0,
+12,17,sort,405504.0,
+12,17,subbitsplit,29440.0,8
+12,17,gcd_uniq,24576.0,
+15,17,bitsplit,557056.0,
+15,17,sort,491520.0,
+15,17,subbitsplit,230144.0,8
+15,17,gcd_uniq,196608.0,
+18,17,bitsplit,4456448.0,
+18,17,sort,1179648.0,
+18,17,subbitsplit,1179648.0,17
+18,17,gcd_uniq,1572864.0,
+0,18,bitsplit,18.0,
+0,18,sort,786435.0,
+0,18,subbitsplit,39.0,2
+0,18,gcd_uniq,6.0,
+3,18,bitsplit,144.0,
+3,18,sort,786456.0,
+3,18,subbitsplit,160.0,4
+3,18,gcd_uniq,48.0,
+6,18,bitsplit,1152.0,
+6,18,sort,786624.0,
+6,18,subbitsplit,768.0,6
+6,18,gcd_uniq,384.0,
+9,18,bitsplit,9216.0,
+9,18,sort,787968.0,
+9,18,subbitsplit,4608.0,9
+9,18,gcd_uniq,3072.0,
+12,18,bitsplit,73728.0,
+12,18,sort,798720.0,
+12,18,subbitsplit,26112.0,9
+12,18,gcd_uniq,24576.0,
+15,18,bitsplit,589824.0,
+15,18,sort,884736.0,
+15,18,subbitsplit,198144.0,9
+15,18,gcd_uniq,196608.0,
+18,18,bitsplit,4718592.0,
+18,18,sort,1572864.0,
+18,18,subbitsplit,1441792.0,17
+18,18,gcd_uniq,1572864.0,
+0,19,bitsplit,19.0,
+0,19,sort,1572867.0,
+0,19,subbitsplit,40.0,2
+0,19,gcd_uniq,6.0,
+3,19,bitsplit,152.0,
+3,19,sort,1572888.0,
+3,19,subbitsplit,168.0,4
+3,19,gcd_uniq,48.0,
+6,19,bitsplit,1216.0,
+6,19,sort,1573056.0,
+6,19,subbitsplit,832.0,6
+6,19,gcd_uniq,384.0,
+9,19,bitsplit,9728.0,
+9,19,sort,1574400.0,
+9,19,subbitsplit,5120.0,9
+9,19,gcd_uniq,3072.0,
+12,19,bitsplit,77824.0,
+12,19,sort,1585152.0,
+12,19,subbitsplit,30208.0,9
+12,19,gcd_uniq,24576.0,
+15,19,bitsplit,622592.0,
+15,19,sort,1671168.0,
+15,19,subbitsplit,230912.0,9
+15,19,gcd_uniq,196608.0,
+18,19,bitsplit,4980736.0,
+18,19,sort,2359296.0,
+18,19,subbitsplit,1703936.0,17
+18,19,gcd_uniq,1572864.0,
+0,20,bitsplit,20.0,
+0,20,sort,3145731.0,
+0,20,subbitsplit,42.0,2
+0,20,gcd_uniq,6.0,
+3,20,bitsplit,160.0,
+3,20,sort,3145752.0,
+3,20,subbitsplit,168.0,4
+3,20,gcd_uniq,48.0,
+6,20,bitsplit,1280.0,
+6,20,sort,3145920.0,
+6,20,subbitsplit,864.0,5
+6,20,gcd_uniq,384.0,
+9,20,bitsplit,10240.0,
+9,20,sort,3147264.0,
+9,20,subbitsplit,5632.0,9
+9,20,gcd_uniq,3072.0,
+12,20,bitsplit,81920.0,
+12,20,sort,3158016.0,
+12,20,subbitsplit,27648.0,10
+12,20,gcd_uniq,24576.0,
+15,20,bitsplit,655360.0,
+15,20,sort,3244032.0,
+15,20,subbitsplit,199680.0,10
+15,20,gcd_uniq,196608.0,
+18,20,bitsplit,5242880.0,
+18,20,sort,3932160.0,
+18,20,subbitsplit,1575936.0,10
+18,20,gcd_uniq,1572864.0,
+0,21,bitsplit,21.0,
+0,21,sort,6291459.0,
+0,21,subbitsplit,43.0,2
+0,21,gcd_uniq,6.0,
+3,21,bitsplit,168.0,
+3,21,sort,6291480.0,
+3,21,subbitsplit,176.0,4
+3,21,gcd_uniq,48.0,
+6,21,bitsplit,1344.0,
+6,21,sort,6291648.0,
+6,21,subbitsplit,928.0,5
+6,21,gcd_uniq,384.0,
+9,21,bitsplit,10752.0,
+9,21,sort,6292992.0,
+9,21,subbitsplit,4992.0,7
+9,21,gcd_uniq,3072.0,
+12,21,bitsplit,86016.0,
+12,21,sort,6303744.0,
+12,21,subbitsplit,31744.0,10
+12,21,gcd_uniq,24576.0,
+15,21,bitsplit,688128.0,
+15,21,sort,6389760.0,
+15,21,subbitsplit,232448.0,10
+15,21,gcd_uniq,196608.0,
+18,21,bitsplit,5505024.0,
+18,21,sort,7077888.0,
+18,21,subbitsplit,1838080.0,10
+18,21,gcd_uniq,1572864.0,
+0,22,bitsplit,22.0,
+0,22,sort,12582915.0,
+0,22,subbitsplit,45.0,2
+0,22,gcd_uniq,6.0,
+3,22,bitsplit,176.0,
+3,22,sort,12582936.0,
+3,22,subbitsplit,184.0,4
+3,22,gcd_uniq,48.0,
+6,22,bitsplit,1408.0,
+6,22,sort,12583104.0,
+6,22,subbitsplit,992.0,5
+6,22,gcd_uniq,384.0,
+9,22,bitsplit,11264.0,
+9,22,sort,12584448.0,
+9,22,subbitsplit,5504.0,7
+9,22,gcd_uniq,3072.0,
+12,22,bitsplit,90112.0,
+12,22,sort,12595200.0,
+12,22,subbitsplit,30720.0,11
+12,22,gcd_uniq,24576.0,
+15,22,bitsplit,720896.0,
+15,22,sort,12681216.0,
+15,22,subbitsplit,202752.0,11
+15,22,gcd_uniq,196608.0,
+18,22,bitsplit,5767168.0,
+18,22,sort,13369344.0,
+18,22,subbitsplit,1579008.0,11
+18,22,gcd_uniq,1572864.0,
+0,23,bitsplit,23.0,
+0,23,sort,25165827.0,
+0,23,subbitsplit,46.0,2
+0,23,gcd_uniq,6.0,
+3,23,bitsplit,184.0,
+3,23,sort,25165848.0,
+3,23,subbitsplit,192.0,4
+3,23,gcd_uniq,48.0,
+6,23,bitsplit,1472.0,
+6,23,sort,25166016.0,
+6,23,subbitsplit,1056.0,5
+6,23,gcd_uniq,384.0,
+9,23,bitsplit,11776.0,
+9,23,sort,25167360.0,
+9,23,subbitsplit,6016.0,7
+9,23,gcd_uniq,3072.0,
+12,23,bitsplit,94208.0,
+12,23,sort,25178112.0,
+12,23,subbitsplit,34816.0,11
+12,23,gcd_uniq,24576.0,
+15,23,bitsplit,753664.0,
+15,23,sort,25264128.0,
+15,23,subbitsplit,235520.0,11
+15,23,gcd_uniq,196608.0,
+18,23,bitsplit,6029312.0,
+18,23,sort,25952256.0,
+18,23,subbitsplit,1841152.0,11
+18,23,gcd_uniq,1572864.0,
+0,24,bitsplit,24.0,
+0,24,sort,50331651.0,
+0,24,subbitsplit,48.0,3
+0,24,gcd_uniq,6.0,
+3,24,bitsplit,192.0,
+3,24,sort,50331672.0,
+3,24,subbitsplit,192.0,4
+3,24,gcd_uniq,48.0,
+6,24,bitsplit,1536.0,
+6,24,sort,50331840.0,
+6,24,subbitsplit,960.0,6
+6,24,gcd_uniq,384.0,
+9,24,bitsplit,12288.0,
+9,24,sort,50333184.0,
+9,24,subbitsplit,5376.0,8
+9,24,gcd_uniq,3072.0,
+12,24,bitsplit,98304.0,
+12,24,sort,50343936.0,
+12,24,subbitsplit,36864.0,12
+12,24,gcd_uniq,24576.0,
+15,24,bitsplit,786432.0,
+15,24,sort,50429952.0,
+15,24,subbitsplit,208896.0,12
+15,24,gcd_uniq,196608.0,
+18,24,bitsplit,6291456.0,
+18,24,sort,51118080.0,
+18,24,subbitsplit,1585152.0,12
+18,24,gcd_uniq,1572864.0,
+0,25,bitsplit,25.0,
+0,25,sort,100663299.0,
+0,25,subbitsplit,49.0,3
+0,25,gcd_uniq,6.0,
+3,25,bitsplit,200.0,
+3,25,sort,100663320.0,
+3,25,subbitsplit,200.0,4
+3,25,gcd_uniq,48.0,
+6,25,bitsplit,1600.0,
+6,25,sort,100663488.0,
+6,25,subbitsplit,1024.0,6
+6,25,gcd_uniq,384.0,
+9,25,bitsplit,12800.0,
+9,25,sort,100664832.0,
+9,25,subbitsplit,5888.0,8
+9,25,gcd_uniq,3072.0,
+12,25,bitsplit,102400.0,
+12,25,sort,100675584.0,
+12,25,subbitsplit,40960.0,12
+12,25,gcd_uniq,24576.0,
+15,25,bitsplit,819200.0,
+15,25,sort,100761600.0,
+15,25,subbitsplit,241664.0,12
+15,25,gcd_uniq,196608.0,
+18,25,bitsplit,6553600.0,
+18,25,sort,101449728.0,
+18,25,subbitsplit,1847296.0,12
+18,25,gcd_uniq,1572864.0,
+0,26,bitsplit,26.0,
+0,26,sort,201326595.0,
+0,26,subbitsplit,50.0,3
+0,26,gcd_uniq,6.0,
+3,26,bitsplit,208.0,
+3,26,sort,201326616.0,
+3,26,subbitsplit,208.0,4
+3,26,gcd_uniq,48.0,
+6,26,bitsplit,1664.0,
+6,26,sort,201326784.0,
+6,26,subbitsplit,1088.0,6
+6,26,gcd_uniq,384.0,
+9,26,bitsplit,13312.0,
+9,26,sort,201328128.0,
+9,26,subbitsplit,6400.0,8
+9,26,gcd_uniq,3072.0,
+12,26,bitsplit,106496.0,
+12,26,sort,201338880.0,
+12,26,subbitsplit,45056.0,12
+12,26,gcd_uniq,24576.0,
+15,26,bitsplit,851968.0,
+15,26,sort,201424896.0,
+15,26,subbitsplit,221184.0,13
+15,26,gcd_uniq,196608.0,
+18,26,bitsplit,6815744.0,
+18,26,sort,202113024.0,
+18,26,subbitsplit,1597440.0,13
+18,26,gcd_uniq,1572864.0,
+0,27,bitsplit,27.0,
+0,27,sort,402653187.0,
+0,27,subbitsplit,51.0,3
+0,27,gcd_uniq,6.0,
+3,27,bitsplit,216.0,
+3,27,sort,402653208.0,
+3,27,subbitsplit,216.0,4
+3,27,gcd_uniq,48.0,
+6,27,bitsplit,1728.0,
+6,27,sort,402653376.0,
+6,27,subbitsplit,1152.0,6
+6,27,gcd_uniq,384.0,
+9,27,bitsplit,13824.0,
+9,27,sort,402654720.0,
+9,27,subbitsplit,6144.0,9
+9,27,gcd_uniq,3072.0,
+12,27,bitsplit,110592.0,
+12,27,sort,402665472.0,
+12,27,subbitsplit,38400.0,9
+12,27,gcd_uniq,24576.0,
+15,27,bitsplit,884736.0,
+15,27,sort,402751488.0,
+15,27,subbitsplit,253952.0,13
+15,27,gcd_uniq,196608.0,
+18,27,bitsplit,7077888.0,
+18,27,sort,403439616.0,
+18,27,subbitsplit,1859584.0,13
+18,27,gcd_uniq,1572864.0,
+0,28,bitsplit,28.0,
+0,28,sort,805306371.0,
+0,28,subbitsplit,52.0,3
+0,28,gcd_uniq,6.0,
+3,28,bitsplit,224.0,
+3,28,sort,805306392.0,
+3,28,subbitsplit,216.0,4
+3,28,gcd_uniq,48.0,
+6,28,bitsplit,1792.0,
+6,28,sort,805306560.0,
+6,28,subbitsplit,1152.0,7
+6,28,gcd_uniq,384.0,
+9,28,bitsplit,14336.0,
+9,28,sort,805307904.0,
+9,28,subbitsplit,6528.0,7
+9,28,gcd_uniq,3072.0,
+12,28,bitsplit,114688.0,
+12,28,sort,805318656.0,
+12,28,subbitsplit,42496.0,9
+12,28,gcd_uniq,24576.0,
+15,28,bitsplit,917504.0,
+15,28,sort,805404672.0,
+15,28,subbitsplit,245760.0,14
+15,28,gcd_uniq,196608.0,
+18,28,bitsplit,7340032.0,
+18,28,sort,806092800.0,
+18,28,subbitsplit,1622016.0,14
+18,28,gcd_uniq,1572864.0,
+0,29,bitsplit,29.0,
+0,29,sort,1610612739.0,
+0,29,subbitsplit,53.0,3
+0,29,gcd_uniq,6.0,
+3,29,bitsplit,232.0,
+3,29,sort,1610612760.0,
+3,29,subbitsplit,224.0,4
+3,29,gcd_uniq,48.0,
+6,29,bitsplit,1856.0,
+6,29,sort,1610612928.0,
+6,29,subbitsplit,1216.0,7
+6,29,gcd_uniq,384.0,
+9,29,bitsplit,14848.0,
+9,29,sort,1610614272.0,
+9,29,subbitsplit,7040.0,7
+9,29,gcd_uniq,3072.0,
+12,29,bitsplit,118784.0,
+12,29,sort,1610625024.0,
+12,29,subbitsplit,46592.0,9
+12,29,gcd_uniq,24576.0,
+15,29,bitsplit,950272.0,
+15,29,sort,1610711040.0,
+15,29,subbitsplit,278528.0,14
+15,29,gcd_uniq,196608.0,
+18,29,bitsplit,7602176.0,
+18,29,sort,1611399168.0,
+18,29,subbitsplit,1884160.0,14
+18,29,gcd_uniq,1572864.0,
+0,30,bitsplit,30.0,
+0,30,sort,3221225475.0,
+0,30,subbitsplit,54.0,3
+0,30,gcd_uniq,6.0,
+3,30,bitsplit,240.0,
+3,30,sort,3221225496.0,
+3,30,subbitsplit,232.0,4
+3,30,gcd_uniq,48.0,
+6,30,bitsplit,1920.0,
+6,30,sort,3221225664.0,
+6,30,subbitsplit,1152.0,6
+6,30,gcd_uniq,384.0,
+9,30,bitsplit,15360.0,
+9,30,sort,3221227008.0,
+9,30,subbitsplit,7552.0,7
+9,30,gcd_uniq,3072.0,
+12,30,bitsplit,122880.0,
+12,30,sort,3221237760.0,
+12,30,subbitsplit,39936.0,10
+12,30,gcd_uniq,24576.0,
+15,30,bitsplit,983040.0,
+15,30,sort,3221323776.0,
+15,30,subbitsplit,294912.0,15
+15,30,gcd_uniq,196608.0,
+18,30,bitsplit,7864320.0,
+18,30,sort,3222011904.0,
+18,30,subbitsplit,1671168.0,15
+18,30,gcd_uniq,1572864.0,
+0,31,bitsplit,31.0,
+0,31,sort,6442450947.0,
+0,31,subbitsplit,55.0,3
+0,31,gcd_uniq,6.0,
+3,31,bitsplit,248.0,
+3,31,sort,6442450968.0,
+3,31,subbitsplit,240.0,4
+3,31,gcd_uniq,48.0,
+6,31,bitsplit,1984.0,
+6,31,sort,6442451136.0,
+6,31,subbitsplit,1216.0,6
+6,31,gcd_uniq,384.0,
+9,31,bitsplit,15872.0,
+9,31,sort,6442452480.0,
+9,31,subbitsplit,8064.0,7
+9,31,gcd_uniq,3072.0,
+12,31,bitsplit,126976.0,
+12,31,sort,6442463232.0,
+12,31,subbitsplit,44032.0,10
+12,31,gcd_uniq,24576.0,
+15,31,bitsplit,1015808.0,
+15,31,sort,6442549248.0,
+15,31,subbitsplit,327680.0,15
+15,31,gcd_uniq,196608.0,
+18,31,bitsplit,8126464.0,
+18,31,sort,6443237376.0,
+18,31,subbitsplit,1933312.0,15
+18,31,gcd_uniq,1572864.0,
+0,32,bitsplit,32.0,
+0,32,sort,12884901891.0,
+0,32,subbitsplit,56.0,3
+0,32,gcd_uniq,6.0,
+3,32,bitsplit,256.0,
+3,32,sort,12884901912.0,
+3,32,subbitsplit,240.0,4
+3,32,gcd_uniq,48.0,
+6,32,bitsplit,2048.0,
+6,32,sort,12884902080.0,
+6,32,subbitsplit,1280.0,6
+6,32,gcd_uniq,384.0,
+9,32,bitsplit,16384.0,
+9,32,sort,12884903424.0,
+9,32,subbitsplit,6912.0,8
+9,32,gcd_uniq,3072.0,
+12,32,bitsplit,131072.0,
+12,32,sort,12884914176.0,
+12,32,subbitsplit,48128.0,10
+12,32,gcd_uniq,24576.0,
+15,32,bitsplit,1048576.0,
+15,32,sort,12885000192.0,
+15,32,subbitsplit,360448.0,15
+15,32,gcd_uniq,196608.0,
+18,32,bitsplit,8388608.0,
+18,32,sort,12885688320.0,
+18,32,subbitsplit,1769472.0,16
+18,32,gcd_uniq,1572864.0,
+0,33,bitsplit,33.0,
+0,33,sort,25769803779.0,
+0,33,subbitsplit,57.0,3
+0,33,gcd_uniq,6.0,
+3,33,bitsplit,264.0,
+3,33,sort,25769803800.0,
+3,33,subbitsplit,248.0,4
+3,33,gcd_uniq,48.0,
+6,33,bitsplit,2112.0,
+6,33,sort,25769803968.0,
+6,33,subbitsplit,1344.0,6
+6,33,gcd_uniq,384.0,
+9,33,bitsplit,16896.0,
+9,33,sort,25769805312.0,
+9,33,subbitsplit,7424.0,8
+9,33,gcd_uniq,3072.0,
+12,33,bitsplit,135168.0,
+12,33,sort,25769816064.0,
+12,33,subbitsplit,43008.0,11
+12,33,gcd_uniq,24576.0,
+15,33,bitsplit,1081344.0,
+15,33,sort,25769902080.0,
+15,33,subbitsplit,301056.0,11
+15,33,gcd_uniq,196608.0,
+18,33,bitsplit,8650752.0,
+18,33,sort,25770590208.0,
+18,33,subbitsplit,2031616.0,16
+18,33,gcd_uniq,1572864.0,
+0,34,bitsplit,34.0,
+0,34,sort,51539607555.0,
+0,34,subbitsplit,58.0,3
+0,34,gcd_uniq,6.0,
+3,34,bitsplit,272.0,
+3,34,sort,51539607576.0,
+3,34,subbitsplit,256.0,4
+3,34,gcd_uniq,48.0,
+6,34,bitsplit,2176.0,
+6,34,sort,51539607744.0,
+6,34,subbitsplit,1408.0,6
+6,34,gcd_uniq,384.0,
+9,34,bitsplit,17408.0,
+9,34,sort,51539609088.0,
+9,34,subbitsplit,7936.0,8
+9,34,gcd_uniq,3072.0,
+12,34,bitsplit,139264.0,
+12,34,sort,51539619840.0,
+12,34,subbitsplit,47104.0,11
+12,34,gcd_uniq,24576.0,
+15,34,bitsplit,1114112.0,
+15,34,sort,51539705856.0,
+15,34,subbitsplit,333824.0,11
+15,34,gcd_uniq,196608.0,
+18,34,bitsplit,8912896.0,
+18,34,sort,51540393984.0,
+18,34,subbitsplit,1966080.0,17
+18,34,gcd_uniq,1572864.0,
+0,35,bitsplit,35.0,
+0,35,sort,103079215107.0,
+0,35,subbitsplit,59.0,3
+0,35,gcd_uniq,6.0,
+3,35,bitsplit,280.0,
+3,35,sort,103079215128.0,
+3,35,subbitsplit,264.0,5
+3,35,gcd_uniq,48.0,
+6,35,bitsplit,2240.0,
+6,35,sort,103079215296.0,
+6,35,subbitsplit,1344.0,7
+6,35,gcd_uniq,384.0,
+9,35,bitsplit,17920.0,
+9,35,sort,103079216640.0,
+9,35,subbitsplit,8064.0,7
+9,35,gcd_uniq,3072.0,
+12,35,bitsplit,143360.0,
+12,35,sort,103079227392.0,
+12,35,subbitsplit,51200.0,11
+12,35,gcd_uniq,24576.0,
+15,35,bitsplit,1146880.0,
+15,35,sort,103079313408.0,
+15,35,subbitsplit,366592.0,11
+15,35,gcd_uniq,196608.0,
+18,35,bitsplit,9175040.0,
+18,35,sort,103080001536.0,
+18,35,subbitsplit,2228224.0,17
+18,35,gcd_uniq,1572864.0,
+0,36,bitsplit,36.0,
+0,36,sort,206158430211.0,
+0,36,subbitsplit,60.0,3
+0,36,gcd_uniq,6.0,
+3,36,bitsplit,288.0,
+3,36,sort,206158430232.0,
+3,36,subbitsplit,264.0,4
+3,36,gcd_uniq,48.0,
+6,36,bitsplit,2304.0,
+6,36,sort,206158430400.0,
+6,36,subbitsplit,1344.0,6
+6,36,gcd_uniq,384.0,
+9,36,bitsplit,18432.0,
+9,36,sort,206158431744.0,
+9,36,subbitsplit,7680.0,9
+9,36,gcd_uniq,3072.0,
+12,36,bitsplit,147456.0,
+12,36,sort,206158442496.0,
+12,36,subbitsplit,49152.0,12
+12,36,gcd_uniq,24576.0,
+15,36,bitsplit,1179648.0,
+15,36,sort,206158528512.0,
+15,36,subbitsplit,307200.0,12
+15,36,gcd_uniq,196608.0,
+18,36,bitsplit,9437184.0,
+18,36,sort,206159216640.0,
+18,36,subbitsplit,2359296.0,18
+18,36,gcd_uniq,1572864.0,
+0,37,bitsplit,37.0,
+0,37,sort,412316860419.0,
+0,37,subbitsplit,61.0,3
+0,37,gcd_uniq,6.0,
+3,37,bitsplit,296.0,
+3,37,sort,412316860440.0,
+3,37,subbitsplit,272.0,4
+3,37,gcd_uniq,48.0,
+6,37,bitsplit,2368.0,
+6,37,sort,412316860608.0,
+6,37,subbitsplit,1408.0,6
+6,37,gcd_uniq,384.0,
+9,37,bitsplit,18944.0,
+9,37,sort,412316861952.0,
+9,37,subbitsplit,8192.0,9
+9,37,gcd_uniq,3072.0,
+12,37,bitsplit,151552.0,
+12,37,sort,412316872704.0,
+12,37,subbitsplit,53248.0,12
+12,37,gcd_uniq,24576.0,
+15,37,bitsplit,1212416.0,
+15,37,sort,412316958720.0,
+15,37,subbitsplit,339968.0,12
+15,37,gcd_uniq,196608.0,
+18,37,bitsplit,9699328.0,
+18,37,sort,412317646848.0,
+18,37,subbitsplit,2621440.0,18
+18,37,gcd_uniq,1572864.0,
+0,38,bitsplit,38.0,
+0,38,sort,824633720835.0,
+0,38,subbitsplit,62.0,3
+0,38,gcd_uniq,6.0,
+3,38,bitsplit,304.0,
+3,38,sort,824633720856.0,
+3,38,subbitsplit,280.0,4
+3,38,gcd_uniq,48.0,
+6,38,bitsplit,2432.0,
+6,38,sort,824633721024.0,
+6,38,subbitsplit,1472.0,6
+6,38,gcd_uniq,384.0,
+9,38,bitsplit,19456.0,
+9,38,sort,824633722368.0,
+9,38,subbitsplit,8704.0,9
+9,38,gcd_uniq,3072.0,
+12,38,bitsplit,155648.0,
+12,38,sort,824633733120.0,
+12,38,subbitsplit,57344.0,12
+12,38,gcd_uniq,24576.0,
+15,38,bitsplit,1245184.0,
+15,38,sort,824633819136.0,
+15,38,subbitsplit,372736.0,12
+15,38,gcd_uniq,196608.0,
+18,38,bitsplit,9961472.0,
+18,38,sort,824634507264.0,
+18,38,subbitsplit,2883584.0,18
+18,38,gcd_uniq,1572864.0,
+0,39,bitsplit,39.0,
+0,39,sort,1649267441667.0,
+0,39,subbitsplit,63.0,3
+0,39,gcd_uniq,6.0,
+3,39,bitsplit,312.0,
+3,39,sort,1649267441688.0,
+3,39,subbitsplit,288.0,4
+3,39,gcd_uniq,48.0,
+6,39,bitsplit,2496.0,
+6,39,sort,1649267441856.0,
+6,39,subbitsplit,1536.0,6
+6,39,gcd_uniq,384.0,
+9,39,bitsplit,19968.0,
+9,39,sort,1649267443200.0,
+9,39,subbitsplit,9216.0,9
+9,39,gcd_uniq,3072.0,
+12,39,bitsplit,159744.0,
+12,39,sort,1649267453952.0,
+12,39,subbitsplit,61440.0,13
+12,39,gcd_uniq,24576.0,
+15,39,bitsplit,1277952.0,
+15,39,sort,1649267539968.0,
+15,39,subbitsplit,319488.0,13
+15,39,gcd_uniq,196608.0,
+18,39,bitsplit,10223616.0,
+18,39,sort,1649268228096.0,
+18,39,subbitsplit,2383872.0,13
+18,39,gcd_uniq,1572864.0,
+0,40,bitsplit,40.0,
+0,40,sort,3298534883331.0,
+0,40,subbitsplit,64.0,3
+0,40,gcd_uniq,6.0,
+3,40,bitsplit,320.0,
+3,40,sort,3298534883352.0,
+3,40,subbitsplit,288.0,5
+3,40,gcd_uniq,48.0,
+6,40,bitsplit,2560.0,
+6,40,sort,3298534883520.0,
+6,40,subbitsplit,1600.0,6
+6,40,gcd_uniq,384.0,
+9,40,bitsplit,20480.0,
+9,40,sort,3298534884864.0,
+9,40,subbitsplit,8448.0,8
+9,40,gcd_uniq,3072.0,
+12,40,bitsplit,163840.0,
+12,40,sort,3298534895616.0,
+12,40,subbitsplit,52224.0,10
+12,40,gcd_uniq,24576.0,
+15,40,bitsplit,1310720.0,
+15,40,sort,3298534981632.0,
+15,40,subbitsplit,352256.0,13
+15,40,gcd_uniq,196608.0,
+18,40,bitsplit,10485760.0,
+18,40,sort,3298535669760.0,
+18,40,subbitsplit,2646016.0,13
+18,40,gcd_uniq,1572864.0,
+0,41,bitsplit,41.0,
+0,41,sort,6597069766659.0,
+0,41,subbitsplit,65.0,3
+0,41,gcd_uniq,6.0,
+3,41,bitsplit,328.0,
+3,41,sort,6597069766680.0,
+3,41,subbitsplit,296.0,5
+3,41,gcd_uniq,48.0,
+6,41,bitsplit,2624.0,
+6,41,sort,6597069766848.0,
+6,41,subbitsplit,1664.0,6
+6,41,gcd_uniq,384.0,
+9,41,bitsplit,20992.0,
+9,41,sort,6597069768192.0,
+9,41,subbitsplit,8960.0,8
+9,41,gcd_uniq,3072.0,
+12,41,bitsplit,167936.0,
+12,41,sort,6597069778944.0,
+12,41,subbitsplit,56320.0,10
+12,41,gcd_uniq,24576.0,
+15,41,bitsplit,1343488.0,
+15,41,sort,6597069864960.0,
+15,41,subbitsplit,385024.0,13
+15,41,gcd_uniq,196608.0,
+18,41,bitsplit,10747904.0,
+18,41,sort,6597070553088.0,
+18,41,subbitsplit,2908160.0,13
+18,41,gcd_uniq,1572864.0,
+0,42,bitsplit,42.0,
+0,42,sort,13194139533315.0,
+0,42,subbitsplit,66.0,3
+0,42,gcd_uniq,6.0,
+3,42,bitsplit,336.0,
+3,42,sort,13194139533336.0,
+3,42,subbitsplit,304.0,5
+3,42,gcd_uniq,48.0,
+6,42,bitsplit,2688.0,
+6,42,sort,13194139533504.0,
+6,42,subbitsplit,1536.0,7
+6,42,gcd_uniq,384.0,
+9,42,bitsplit,21504.0,
+9,42,sort,13194139534848.0,
+9,42,subbitsplit,9472.0,8
+9,42,gcd_uniq,3072.0,
+12,42,bitsplit,172032.0,
+12,42,sort,13194139545600.0,
+12,42,subbitsplit,60416.0,10
+12,42,gcd_uniq,24576.0,
+15,42,bitsplit,1376256.0,
+15,42,sort,13194139631616.0,
+15,42,subbitsplit,344064.0,14
+15,42,gcd_uniq,196608.0,
+18,42,bitsplit,11010048.0,
+18,42,sort,13194140319744.0,
+18,42,subbitsplit,2408448.0,14
+18,42,gcd_uniq,1572864.0,
+0,43,bitsplit,43.0,
+0,43,sort,26388279066627.0,
+0,43,subbitsplit,67.0,3
+0,43,gcd_uniq,6.0,
+3,43,bitsplit,344.0,
+3,43,sort,26388279066648.0,
+3,43,subbitsplit,312.0,5
+3,43,gcd_uniq,48.0,
+6,43,bitsplit,2752.0,
+6,43,sort,26388279066816.0,
+6,43,subbitsplit,1600.0,7
+6,43,gcd_uniq,384.0,
+9,43,bitsplit,22016.0,
+9,43,sort,26388279068160.0,
+9,43,subbitsplit,9984.0,8
+9,43,gcd_uniq,3072.0,
+12,43,bitsplit,176128.0,
+12,43,sort,26388279078912.0,
+12,43,subbitsplit,64512.0,10
+12,43,gcd_uniq,24576.0,
+15,43,bitsplit,1409024.0,
+15,43,sort,26388279164928.0,
+15,43,subbitsplit,376832.0,14
+15,43,gcd_uniq,196608.0,
+18,43,bitsplit,11272192.0,
+18,43,sort,26388279853056.0,
+18,43,subbitsplit,2670592.0,14
+18,43,gcd_uniq,1572864.0,
+0,44,bitsplit,44.0,
+0,44,sort,52776558133251.0,
+0,44,subbitsplit,68.0,3
+0,44,gcd_uniq,6.0,
+3,44,bitsplit,352.0,
+3,44,sort,52776558133272.0,
+3,44,subbitsplit,312.0,4
+3,44,gcd_uniq,48.0,
+6,44,bitsplit,2816.0,
+6,44,sort,52776558133440.0,
+6,44,subbitsplit,1664.0,7
+6,44,gcd_uniq,384.0,
+9,44,bitsplit,22528.0,
+9,44,sort,52776558134784.0,
+9,44,subbitsplit,10496.0,8
+9,44,gcd_uniq,3072.0,
+12,44,bitsplit,180224.0,
+12,44,sort,52776558145536.0,
+12,44,subbitsplit,55296.0,11
+12,44,gcd_uniq,24576.0,
+15,44,bitsplit,1441792.0,
+15,44,sort,52776558231552.0,
+15,44,subbitsplit,399360.0,11
+15,44,gcd_uniq,196608.0,
+18,44,bitsplit,11534336.0,
+18,44,sort,52776558919680.0,
+18,44,subbitsplit,2932736.0,14
+18,44,gcd_uniq,1572864.0,
+0,45,bitsplit,45.0,
+0,45,sort,105553116266499.0,
+0,45,subbitsplit,69.0,3
+0,45,gcd_uniq,6.0,
+3,45,bitsplit,360.0,
+3,45,sort,105553116266520.0,
+3,45,subbitsplit,312.0,5
+3,45,gcd_uniq,48.0,
+6,45,bitsplit,2880.0,
+6,45,sort,105553116266688.0,
+6,45,subbitsplit,1728.0,7
+6,45,gcd_uniq,384.0,
+9,45,bitsplit,23040.0,
+9,45,sort,105553116268032.0,
+9,45,subbitsplit,9216.0,9
+9,45,gcd_uniq,3072.0,
+12,45,bitsplit,184320.0,
+12,45,sort,105553116278784.0,
+12,45,subbitsplit,59392.0,11
+12,45,gcd_uniq,24576.0,
+15,45,bitsplit,1474560.0,
+15,45,sort,105553116364800.0,
+15,45,subbitsplit,393216.0,15
+15,45,gcd_uniq,196608.0,
+18,45,bitsplit,11796480.0,
+18,45,sort,105553117052928.0,
+18,45,subbitsplit,2457600.0,15
+18,45,gcd_uniq,1572864.0,
+0,46,bitsplit,46.0,
+0,46,sort,211106232532995.0,
+0,46,subbitsplit,70.0,3
+0,46,gcd_uniq,6.0,
+3,46,bitsplit,368.0,
+3,46,sort,211106232533016.0,
+3,46,subbitsplit,320.0,5
+3,46,gcd_uniq,48.0,
+6,46,bitsplit,2944.0,
+6,46,sort,211106232533184.0,
+6,46,subbitsplit,1792.0,7
+6,46,gcd_uniq,384.0,
+9,46,bitsplit,23552.0,
+9,46,sort,211106232534528.0,
+9,46,subbitsplit,9728.0,9
+9,46,gcd_uniq,3072.0,
+12,46,bitsplit,188416.0,
+12,46,sort,211106232545280.0,
+12,46,subbitsplit,63488.0,11
+12,46,gcd_uniq,24576.0,
+15,46,bitsplit,1507328.0,
+15,46,sort,211106232631296.0,
+15,46,subbitsplit,425984.0,15
+15,46,gcd_uniq,196608.0,
+18,46,bitsplit,12058624.0,
+18,46,sort,211106233319424.0,
+18,46,subbitsplit,2719744.0,15
+18,46,gcd_uniq,1572864.0,
+0,47,bitsplit,47.0,
+0,47,sort,422212465065987.0,
+0,47,subbitsplit,71.0,3
+0,47,gcd_uniq,6.0,
+3,47,bitsplit,376.0,
+3,47,sort,422212465066008.0,
+3,47,subbitsplit,328.0,5
+3,47,gcd_uniq,48.0,
+6,47,bitsplit,3008.0,
+6,47,sort,422212465066176.0,
+6,47,subbitsplit,1856.0,7
+6,47,gcd_uniq,384.0,
+9,47,bitsplit,24064.0,
+9,47,sort,422212465067520.0,
+9,47,subbitsplit,10240.0,9
+9,47,gcd_uniq,3072.0,
+12,47,bitsplit,192512.0,
+12,47,sort,422212465078272.0,
+12,47,subbitsplit,67584.0,11
+12,47,gcd_uniq,24576.0,
+15,47,bitsplit,1540096.0,
+15,47,sort,422212465164288.0,
+15,47,subbitsplit,458752.0,15
+15,47,gcd_uniq,196608.0,
+18,47,bitsplit,12320768.0,
+18,47,sort,422212465852416.0,
+18,47,subbitsplit,2981888.0,15
+18,47,gcd_uniq,1572864.0,
+0,48,bitsplit,48.0,
+0,48,sort,844424930131971.0,
+0,48,subbitsplit,72.0,3
+0,48,gcd_uniq,6.0,
+3,48,bitsplit,384.0,
+3,48,sort,844424930131992.0,
+3,48,subbitsplit,336.0,5
+3,48,gcd_uniq,48.0,
+6,48,bitsplit,3072.0,
+6,48,sort,844424930132160.0,
+6,48,subbitsplit,1728.0,6
+6,48,gcd_uniq,384.0,
+9,48,bitsplit,24576.0,
+9,48,sort,844424930133504.0,
+9,48,subbitsplit,9984.0,8
+9,48,gcd_uniq,3072.0,
+12,48,bitsplit,196608.0,
+12,48,sort,844424930144256.0,
+12,48,subbitsplit,61440.0,12
+12,48,gcd_uniq,24576.0,
+15,48,bitsplit,1572864.0,
+15,48,sort,844424930230272.0,
+15,48,subbitsplit,405504.0,12
+15,48,gcd_uniq,196608.0,
+18,48,bitsplit,12582912.0,
+18,48,sort,844424930918400.0,
+18,48,subbitsplit,2555904.0,16
+18,48,gcd_uniq,1572864.0,
+0,49,bitsplit,49.0,
+0,49,sort,1688849860263939.0,
+0,49,subbitsplit,73.0,3
+0,49,gcd_uniq,6.0,
+3,49,bitsplit,392.0,
+3,49,sort,1688849860263960.0,
+3,49,subbitsplit,344.0,5
+3,49,gcd_uniq,48.0,
+6,49,bitsplit,3136.0,
+6,49,sort,1688849860264128.0,
+6,49,subbitsplit,1728.0,7
+6,49,gcd_uniq,384.0,
+9,49,bitsplit,25088.0,
+9,49,sort,1688849860265472.0,
+9,49,subbitsplit,10496.0,8
+9,49,gcd_uniq,3072.0,
+12,49,bitsplit,200704.0,
+12,49,sort,1688849860276224.0,
+12,49,subbitsplit,65536.0,12
+12,49,gcd_uniq,24576.0,
+15,49,bitsplit,1605632.0,
+15,49,sort,1688849860362240.0,
+15,49,subbitsplit,438272.0,12
+15,49,gcd_uniq,196608.0,
+18,49,bitsplit,12845056.0,
+18,49,sort,1688849861050368.0,
+18,49,subbitsplit,2818048.0,16
+18,49,gcd_uniq,1572864.0,
+0,50,bitsplit,50.0,
+0,50,sort,3377699720527875.0,
+0,50,subbitsplit,74.0,3
+0,50,gcd_uniq,6.0,
+3,50,bitsplit,400.0,
+3,50,sort,3377699720527896.0,
+3,50,subbitsplit,336.0,5
+3,50,gcd_uniq,48.0,
+6,50,bitsplit,3200.0,
+6,50,sort,3377699720528064.0,
+6,50,subbitsplit,1792.0,7
+6,50,gcd_uniq,384.0,
+9,50,bitsplit,25600.0,
+9,50,sort,3377699720529408.0,
+9,50,subbitsplit,10752.0,10
+9,50,gcd_uniq,3072.0,
+12,50,bitsplit,204800.0,
+12,50,sort,3377699720540160.0,
+12,50,subbitsplit,64512.0,10
+12,50,gcd_uniq,24576.0,
+15,50,bitsplit,1638400.0,
+15,50,sort,3377699720626176.0,
+15,50,subbitsplit,471040.0,12
+15,50,gcd_uniq,196608.0,
+18,50,bitsplit,13107200.0,
+18,50,sort,3377699721314304.0,
+18,50,subbitsplit,3080192.0,16
+18,50,gcd_uniq,1572864.0,
+0,51,bitsplit,51.0,
+0,51,sort,6755399441055747.0,
+0,51,subbitsplit,75.0,3
+0,51,gcd_uniq,6.0,
+3,51,bitsplit,408.0,
+3,51,sort,6755399441055768.0,
+3,51,subbitsplit,344.0,5
+3,51,gcd_uniq,48.0,
+6,51,bitsplit,3264.0,
+6,51,sort,6755399441055936.0,
+6,51,subbitsplit,1856.0,7
+6,51,gcd_uniq,384.0,
+9,51,bitsplit,26112.0,
+9,51,sort,6755399441057280.0,
+9,51,subbitsplit,11264.0,10
+9,51,gcd_uniq,3072.0,
+12,51,bitsplit,208896.0,
+12,51,sort,6755399441068032.0,
+12,51,subbitsplit,68608.0,10
+12,51,gcd_uniq,24576.0,
+15,51,bitsplit,1671168.0,
+15,51,sort,6755399441154048.0,
+15,51,subbitsplit,503808.0,12
+15,51,gcd_uniq,196608.0,
+18,51,bitsplit,13369344.0,
+18,51,sort,6755399441842176.0,
+18,51,subbitsplit,2752512.0,17
+18,51,gcd_uniq,1572864.0,
+0,52,bitsplit,52.0,
+0,52,sort,1.3510798882111492e+16,
+0,52,subbitsplit,76.0,3
+0,52,gcd_uniq,6.0,
+3,52,bitsplit,416.0,
+3,52,sort,1.3510798882111512e+16,
+3,52,subbitsplit,352.0,5
+3,52,gcd_uniq,48.0,
+6,52,bitsplit,3328.0,
+6,52,sort,1.351079888211168e+16,
+6,52,subbitsplit,1920.0,7
+6,52,gcd_uniq,384.0,
+9,52,bitsplit,26624.0,
+9,52,sort,1.3510798882113024e+16,
+9,52,subbitsplit,11776.0,10
+9,52,gcd_uniq,3072.0,
+12,52,bitsplit,212992.0,
+12,52,sort,1.3510798882123776e+16,
+12,52,subbitsplit,72704.0,10
+12,52,gcd_uniq,24576.0,
+15,52,bitsplit,1703936.0,
+15,52,sort,1.3510798882209792e+16,
+15,52,subbitsplit,417792.0,13
+15,52,gcd_uniq,196608.0,
+18,52,bitsplit,13631488.0,
+18,52,sort,1.351079888289792e+16,
+18,52,subbitsplit,3014656.0,17
+18,52,gcd_uniq,1572864.0,
+0,53,bitsplit,53.0,
+0,53,sort,2.702159776422298e+16,
+0,53,subbitsplit,77.0,3
+0,53,gcd_uniq,6.0,
+3,53,bitsplit,424.0,
+3,53,sort,2.7021597764223e+16,
+3,53,subbitsplit,360.0,5
+3,53,gcd_uniq,48.0,
+6,53,bitsplit,3392.0,
+6,53,sort,2.702159776422317e+16,
+6,53,subbitsplit,1984.0,7
+6,53,gcd_uniq,384.0,
+9,53,bitsplit,27136.0,
+9,53,sort,2.702159776422451e+16,
+9,53,subbitsplit,12288.0,10
+9,53,gcd_uniq,3072.0,
+12,53,bitsplit,217088.0,
+12,53,sort,2.7021597764235264e+16,
+12,53,subbitsplit,76800.0,10
+12,53,gcd_uniq,24576.0,
+15,53,bitsplit,1736704.0,
+15,53,sort,2.702159776432128e+16,
+15,53,subbitsplit,450560.0,13
+15,53,gcd_uniq,196608.0,
+18,53,bitsplit,13893632.0,
+18,53,sort,2.702159776500941e+16,
+18,53,subbitsplit,3276800.0,17
+18,53,gcd_uniq,1572864.0,
+0,54,bitsplit,54.0,
+0,54,sort,5.404319552844595e+16,
+0,54,subbitsplit,78.0,3
+0,54,gcd_uniq,6.0,
+3,54,bitsplit,432.0,
+3,54,sort,5.4043195528445976e+16,
+3,54,subbitsplit,368.0,5
+3,54,gcd_uniq,48.0,
+6,54,bitsplit,3456.0,
+6,54,sort,5.404319552844614e+16,
+6,54,subbitsplit,1920.0,6
+6,54,gcd_uniq,384.0,
+9,54,bitsplit,27648.0,
+9,54,sort,5.404319552844749e+16,
+9,54,subbitsplit,10752.0,9
+9,54,gcd_uniq,3072.0,
+12,54,bitsplit,221184.0,
+12,54,sort,5.404319552845824e+16,
+12,54,subbitsplit,75264.0,9
+12,54,gcd_uniq,24576.0,
+15,54,bitsplit,1769472.0,
+15,54,sort,5.404319552854426e+16,
+15,54,subbitsplit,483328.0,13
+15,54,gcd_uniq,196608.0,
+18,54,bitsplit,14155776.0,
+18,54,sort,5.404319552923238e+16,
+18,54,subbitsplit,3145728.0,18
+18,54,gcd_uniq,1572864.0,
+0,55,bitsplit,55.0,
+0,55,sort,1.080863910568919e+17,
+0,55,subbitsplit,79.0,3
+0,55,gcd_uniq,6.0,
+3,55,bitsplit,440.0,
+3,55,sort,1.0808639105689194e+17,
+3,55,subbitsplit,360.0,5
+3,55,gcd_uniq,48.0,
+6,55,bitsplit,3520.0,
+6,55,sort,1.080863910568921e+17,
+6,55,subbitsplit,1984.0,6
+6,55,gcd_uniq,384.0,
+9,55,bitsplit,28160.0,
+9,55,sort,1.0808639105689344e+17,
+9,55,subbitsplit,11264.0,9
+9,55,gcd_uniq,3072.0,
+12,55,bitsplit,225280.0,
+12,55,sort,1.080863910569042e+17,
+12,55,subbitsplit,67584.0,11
+12,55,gcd_uniq,24576.0,
+15,55,bitsplit,1802240.0,
+15,55,sort,1.080863910569902e+17,
+15,55,subbitsplit,497664.0,11
+15,55,gcd_uniq,196608.0,
+18,55,bitsplit,14417920.0,
+18,55,sort,1.0808639105767834e+17,
+18,55,subbitsplit,3407872.0,18
+18,55,gcd_uniq,1572864.0,
+0,56,bitsplit,56.0,
+0,56,sort,2.161727821137838e+17,
+0,56,subbitsplit,80.0,3
+0,56,gcd_uniq,6.0,
+3,56,bitsplit,448.0,
+3,56,sort,2.1617278211378384e+17,
+3,56,subbitsplit,368.0,5
+3,56,gcd_uniq,48.0,
+6,56,bitsplit,3584.0,
+6,56,sort,2.16172782113784e+17,
+6,56,subbitsplit,1920.0,7
+6,56,gcd_uniq,384.0,
+9,56,bitsplit,28672.0,
+9,56,sort,2.1617278211378534e+17,
+9,56,subbitsplit,11520.0,8
+9,56,gcd_uniq,3072.0,
+12,56,bitsplit,229376.0,
+12,56,sort,2.161727821137961e+17,
+12,56,subbitsplit,71680.0,11
+12,56,gcd_uniq,24576.0,
+15,56,bitsplit,1835008.0,
+15,56,sort,2.161727821138821e+17,
+15,56,subbitsplit,442368.0,14
+15,56,gcd_uniq,196608.0,
+18,56,bitsplit,14680064.0,
+18,56,sort,2.1617278211457024e+17,
+18,56,subbitsplit,3194880.0,14
+18,56,gcd_uniq,1572864.0,
+0,57,bitsplit,57.0,
+0,57,sort,4.323455642275676e+17,
+0,57,subbitsplit,81.0,3
+0,57,gcd_uniq,6.0,
+3,57,bitsplit,456.0,
+3,57,sort,4.323455642275676e+17,
+3,57,subbitsplit,376.0,5
+3,57,gcd_uniq,48.0,
+6,57,bitsplit,3648.0,
+6,57,sort,4.323455642275678e+17,
+6,57,subbitsplit,1984.0,7
+6,57,gcd_uniq,384.0,
+9,57,bitsplit,29184.0,
+9,57,sort,4.3234556422756915e+17,
+9,57,subbitsplit,12032.0,8
+9,57,gcd_uniq,3072.0,
+12,57,bitsplit,233472.0,
+12,57,sort,4.323455642275799e+17,
+12,57,subbitsplit,75776.0,11
+12,57,gcd_uniq,24576.0,
+15,57,bitsplit,1867776.0,
+15,57,sort,4.323455642276659e+17,
+15,57,subbitsplit,475136.0,14
+15,57,gcd_uniq,196608.0,
+18,57,bitsplit,14942208.0,
+18,57,sort,4.3234556422835405e+17,
+18,57,subbitsplit,3457024.0,14
+18,57,gcd_uniq,1572864.0,
+0,58,bitsplit,58.0,
+0,58,sort,8.646911284551352e+17,
+0,58,subbitsplit,82.0,3
+0,58,gcd_uniq,6.0,
+3,58,bitsplit,464.0,
+3,58,sort,8.646911284551352e+17,
+3,58,subbitsplit,384.0,5
+3,58,gcd_uniq,48.0,
+6,58,bitsplit,3712.0,
+6,58,sort,8.646911284551355e+17,
+6,58,subbitsplit,2048.0,7
+6,58,gcd_uniq,384.0,
+9,58,bitsplit,29696.0,
+9,58,sort,8.646911284551368e+17,
+9,58,subbitsplit,12544.0,8
+9,58,gcd_uniq,3072.0,
+12,58,bitsplit,237568.0,
+12,58,sort,8.646911284551475e+17,
+12,58,subbitsplit,79872.0,11
+12,58,gcd_uniq,24576.0,
+15,58,bitsplit,1900544.0,
+15,58,sort,8.646911284552335e+17,
+15,58,subbitsplit,507904.0,14
+15,58,gcd_uniq,196608.0,
+18,58,bitsplit,15204352.0,
+18,58,sort,8.646911284559217e+17,
+18,58,subbitsplit,3719168.0,14
+18,58,gcd_uniq,1572864.0,
+0,59,bitsplit,59.0,
+0,59,sort,1.7293822569102705e+18,
+0,59,subbitsplit,83.0,3
+0,59,gcd_uniq,6.0,
+3,59,bitsplit,472.0,
+3,59,sort,1.7293822569102705e+18,
+3,59,subbitsplit,392.0,5
+3,59,gcd_uniq,48.0,
+6,59,bitsplit,3776.0,
+6,59,sort,1.7293822569102707e+18,
+6,59,subbitsplit,2112.0,7
+6,59,gcd_uniq,384.0,
+9,59,bitsplit,30208.0,
+9,59,sort,1.729382256910272e+18,
+9,59,subbitsplit,13056.0,8
+9,59,gcd_uniq,3072.0,
+12,59,bitsplit,241664.0,
+12,59,sort,1.7293822569102828e+18,
+12,59,subbitsplit,83968.0,11
+12,59,gcd_uniq,24576.0,
+15,59,bitsplit,1933312.0,
+15,59,sort,1.7293822569103688e+18,
+15,59,subbitsplit,540672.0,14
+15,59,gcd_uniq,196608.0,
+18,59,bitsplit,15466496.0,
+18,59,sort,1.729382256911057e+18,
+18,59,subbitsplit,3981312.0,14
+18,59,gcd_uniq,1572864.0,
+0,60,bitsplit,60.0,
+0,60,sort,3.458764513820541e+18,
+0,60,subbitsplit,84.0,3
+0,60,gcd_uniq,6.0,
+3,60,bitsplit,480.0,
+3,60,sort,3.458764513820541e+18,
+3,60,subbitsplit,384.0,5
+3,60,gcd_uniq,48.0,
+6,60,bitsplit,3840.0,
+6,60,sort,3.458764513820541e+18,
+6,60,subbitsplit,2112.0,6
+6,60,gcd_uniq,384.0,
+9,60,bitsplit,30720.0,
+9,60,sort,3.4587645138205425e+18,
+9,60,subbitsplit,12288.0,10
+9,60,gcd_uniq,3072.0,
+12,60,bitsplit,245760.0,
+12,60,sort,3.458764513820553e+18,
+12,60,subbitsplit,73728.0,12
+12,60,gcd_uniq,24576.0,
+15,60,bitsplit,1966080.0,
+15,60,sort,3.458764513820639e+18,
+15,60,subbitsplit,491520.0,15
+15,60,gcd_uniq,196608.0,
+18,60,bitsplit,15728640.0,
+18,60,sort,3.4587645138213274e+18,
+18,60,subbitsplit,3244032.0,15
+18,60,gcd_uniq,1572864.0,
+0,61,bitsplit,61.0,
+0,61,sort,6.917529027641082e+18,
+0,61,subbitsplit,85.0,3
+0,61,gcd_uniq,6.0,
+3,61,bitsplit,488.0,
+3,61,sort,6.917529027641082e+18,
+3,61,subbitsplit,392.0,5
+3,61,gcd_uniq,48.0,
+6,61,bitsplit,3904.0,
+6,61,sort,6.917529027641082e+18,
+6,61,subbitsplit,2176.0,6
+6,61,gcd_uniq,384.0,
+9,61,bitsplit,31232.0,
+9,61,sort,6.917529027641084e+18,
+9,61,subbitsplit,12800.0,10
+9,61,gcd_uniq,3072.0,
+12,61,bitsplit,249856.0,
+12,61,sort,6.917529027641094e+18,
+12,61,subbitsplit,77824.0,12
+12,61,gcd_uniq,24576.0,
+15,61,bitsplit,1998848.0,
+15,61,sort,6.91752902764118e+18,
+15,61,subbitsplit,524288.0,15
+15,61,gcd_uniq,196608.0,
+18,61,bitsplit,15990784.0,
+18,61,sort,6.917529027641868e+18,
+18,61,subbitsplit,3506176.0,15
+18,61,gcd_uniq,1572864.0,
+0,62,bitsplit,62.0,
+0,62,sort,1.3835058055282164e+19,
+0,62,subbitsplit,86.0,3
+0,62,gcd_uniq,6.0,
+3,62,bitsplit,496.0,
+3,62,sort,1.3835058055282164e+19,
+3,62,subbitsplit,400.0,5
+3,62,gcd_uniq,48.0,
+6,62,bitsplit,3968.0,
+6,62,sort,1.3835058055282164e+19,
+6,62,subbitsplit,2240.0,6
+6,62,gcd_uniq,384.0,
+9,62,bitsplit,31744.0,
+9,62,sort,1.3835058055282166e+19,
+9,62,subbitsplit,13312.0,10
+9,62,gcd_uniq,3072.0,
+12,62,bitsplit,253952.0,
+12,62,sort,1.3835058055282176e+19,
+12,62,subbitsplit,81920.0,12
+12,62,gcd_uniq,24576.0,
+15,62,bitsplit,2031616.0,
+15,62,sort,1.3835058055282262e+19,
+15,62,subbitsplit,557056.0,15
+15,62,gcd_uniq,196608.0,
+18,62,bitsplit,16252928.0,
+18,62,sort,1.383505805528295e+19,
+18,62,subbitsplit,3768320.0,15
+18,62,gcd_uniq,1572864.0,
+0,63,bitsplit,63.0,
+0,63,sort,2.7670116110564327e+19,
+0,63,subbitsplit,87.0,3
+0,63,gcd_uniq,6.0,
+3,63,bitsplit,504.0,
+3,63,sort,2.7670116110564327e+19,
+3,63,subbitsplit,408.0,5
+3,63,gcd_uniq,48.0,
+6,63,bitsplit,4032.0,
+6,63,sort,2.7670116110564327e+19,
+6,63,subbitsplit,2112.0,7
+6,63,gcd_uniq,384.0,
+9,63,bitsplit,32256.0,
+9,63,sort,2.7670116110564327e+19,
+9,63,subbitsplit,12288.0,9
+9,63,gcd_uniq,3072.0,
+12,63,bitsplit,258048.0,
+12,63,sort,2.767011611056434e+19,
+12,63,subbitsplit,86016.0,12
+12,63,gcd_uniq,24576.0,
+15,63,bitsplit,2064384.0,
+15,63,sort,2.7670116110564426e+19,
+15,63,subbitsplit,589824.0,15
+15,63,gcd_uniq,196608.0,
+18,63,bitsplit,16515072.0,
+18,63,sort,2.7670116110565114e+19,
+18,63,subbitsplit,4030464.0,15
+18,63,gcd_uniq,1572864.0,
+0,64,bitsplit,64.0,
+0,64,sort,5.5340232221128655e+19,
+0,64,subbitsplit,88.0,3
+0,64,gcd_uniq,6.0,
+3,64,bitsplit,512.0,
+3,64,sort,5.5340232221128655e+19,
+3,64,subbitsplit,416.0,5
+3,64,gcd_uniq,48.0,
+6,64,bitsplit,4096.0,
+6,64,sort,5.5340232221128655e+19,
+6,64,subbitsplit,2176.0,7
+6,64,gcd_uniq,384.0,
+9,64,bitsplit,32768.0,
+9,64,sort,5.5340232221128655e+19,
+9,64,subbitsplit,12800.0,9
+9,64,gcd_uniq,3072.0,
+12,64,bitsplit,262144.0,
+12,64,sort,5.534023222112867e+19,
+12,64,subbitsplit,90112.0,12
+12,64,gcd_uniq,24576.0,
+15,64,bitsplit,2097152.0,
+15,64,sort,5.534023222112875e+19,
+15,64,subbitsplit,589824.0,16
+15,64,gcd_uniq,196608.0,
+18,64,bitsplit,16777216.0,
+18,64,sort,5.534023222112944e+19,
+18,64,subbitsplit,3342336.0,16
+18,64,gcd_uniq,1572864.0,
diff --git a/doc/mem/models/gcd_uniq.py b/doc/mem/models/gcd_uniq.py
new file mode 100755
index 00000000..0d769c0d
--- /dev/null
+++ b/doc/mem/models/gcd_uniq.py
@@ -0,0 +1,38 @@
+#!/usr/bin/env python
+
+from math import log2
+
+
+def cost_gcd_uniq(N: int, r: int) -> (int, str):
+    return 6 * N, ""
+
+
+def cost_bitsplit(N: int, r: int) -> (int, str):
+    return r * N, ""
+
+
+def cost_sort(N: int, r: int) -> (int, str):
+    return 3 * (2**r + N), ""
+
+
+def cost_subbitsplit(N: int, r: int) -> (int, str):
+    def cost_subbitsplit_window(N: int, r: int, k: int) -> int:
+        blocks = r // k
+        remainder = r - blocks * k
+        return 3 * 2**k + min(
+            3 * N * blocks + N * remainder,  # bitsplit remainder
+            3 * N * (blocks + 2),  # double-window remainder
+        )
+
+    cost, _, k = min([(cost_subbitsplit_window(N, r, k), -k, k) for k in range(1, r + 1)])
+    return cost, f"{k}"
+
+
+print("log2_accesses,addr_bits,name,cost,k")
+for r in range(4, 65):
+    for N in [2**i for i in range(0, 21, 3)]:
+        for f in [cost_bitsplit, cost_sort, cost_subbitsplit, cost_gcd_uniq]:
+            name = f.__name__.removeprefix("cost_")
+            cost, note = f(N, r)
+            log2N = int(log2(N))
+            print(f"{log2N},{r},{name},{float(cost)},{note}")
diff --git a/doc/mem/models/plot.R b/doc/mem/models/plot.R
new file mode 100644
index 00000000..7c592c04
--- /dev/null
+++ b/doc/mem/models/plot.R
@@ -0,0 +1,22 @@
+library(tidyverse)
+d <- read_csv("data.csv")
+with_norm_cost <- d %>% 
+  left_join(d %>%
+              filter(name == "gcd_uniq") %>%
+              mutate(norm_cost = cost) %>%
+              select(log2_accesses, addr_bits, norm_cost) %>%
+              mutate(),
+            by=c("log2_accesses", "addr_bits")) %>%
+  mutate(norm_cost = cost / norm_cost)
+with_norm_cost %>%
+  filter(name != "sort") %>%
+  ggplot(aes(x = addr_bits, y = norm_cost, color = name)) +
+  geom_point() +
+  geom_line() +
+  facet_wrap(vars(log2_accesses), scales = "free", labeller = label_both)
+d %>%
+  filter(name == "subbitsplit") %>%
+  ggplot(aes(x = addr_bits, y = k)) +
+  geom_point() +
+  geom_line() +
+  facet_wrap(vars(log2_accesses), scales = "free", labeller = label_both)
diff --git a/doc/mem/persistent.tex b/doc/mem/persistent.tex
new file mode 100644
index 00000000..3c725239
--- /dev/null
+++ b/doc/mem/persistent.tex
@@ -0,0 +1,120 @@
+\section{Persistent}
+\begin{outline}
+\1 initial definitions
+  \2 \FF: target field
+  \2 $N$: persistent array size
+  \2 $\vec a, \vec b \in \FF^N$: initial and final arrays
+  \2 $c_a, c_b$: commitments to arrays with randomness $r_a, r_b$
+  \2 $R$: a witness relation $R(c_a, c_b, x, \vec a, \vec b, w, r_a, r_b)$ for a CP-SNARK
+    \3 $x$ extra instance material
+    \3 $w$ extra witness material
+    \3 $\vec a$ represents the initial state of a RAM that $R$ makes $A$
+    accesses to; $\vec b$ is the final state.
+    \2 $A$: number of accesses 
+  \2 $[A]$: $\{0, \dots, A-1\}$
+  \2 hashes
+    \3 root hash: $H_r(k, \vec x) = \prod_i (x_i - k)$
+      \4 used for ``permutation arguments''
+      \4 used to hash multisets to scalars
+    \3 coefficient hash: $H_c(k, \vec x) = \sum_{i=0} k^ix_i$
+      \4 used to hash vectors to scalars
+\1 coalesce the memory footprint
+  \2 goal: from the $N$ entries, isolate up to $A$ that $R$ will be able to
+  touch
+    \3 route the remaining entries from $\vec a$ to $\vec b$ as cheaply as
+       possible
+  \2 witness: $\vec c$: $A$ index-value pairs of $\vec a$ including all touched entries.
+  \2 witness: $\vec d$: similar, with $\vec b$ (same indices and order).
+  \2 challenge $\alpha$
+  \2 compute $\vec a'$, defined by $a'_i = H_c(\alpha, (a_i, i))$ and $\vec b'$ similarly
+    \3 free (linear)
+  \2 compute $\vec c'$, a length $N$ vector
+    \3 First $A$ entries: root-hashes, similarly from $\vec c$.
+      \4 $v + \alpha i$
+      \4 \csPerA{1} (could share with main?)
+    \3 For the rest, hashes of other $\vec a$ entries, in original order (witness)
+  \2 compute $\vec d'$ similarly, from $\vec d$ and $\vec b$.
+    \3 \csPerA{1}
+  \2 challenge $\beta$
+  \2 equate last $N-A$ entries of $\vec c'$ and $\vec d'$.
+    \3 free (linear)
+  \2 permutation arguments for $\vec a', \vec c'$ and $\vec b', \vec d'$ (key $\beta$)
+    \3 \csPerN{3} + \csPerA{2}
+    \3 because some is shared.
+  \2 outputs
+    \3 $\vec c$ initial index-value pairs
+    \3 $\vec d$ final index-value pairs
+\1 build the main transcript
+  \2 goal: define access-order and index-order transcripts, and ensure they're
+  permutations of one another
+  \2 $T$: number of entries ($3A$)
+  \2 entries: (value, idx, time, write?, create?, active?)
+    \3 create is a bit that is set if this is an access writing from the initial persistent RAM
+    \3 active is a bit that is set if this \textbf{write} is active (it's always set for reads)
+      \4 if inactive, this write has no effect.
+    \3 times are in $[A+1]$, not $[3A]$
+      \4 accesses from $R$ gets times in $[A]$, as standard
+      \4 all initial writes to have time 0
+      \4 all final reads have time $A$
+  \2 denote the transcript $\vec e$
+  \2 witness: $\vec f$: the transcript ordered on index and then time
+  \2 challenge $\alpha$
+  \2 compute $\vec e'$ with element-wise coefficient hash over $\vec e$ keyed on $\alpha$.
+    \3 The computations is something like $v + \alpha i + k_2 \alpha^2 + w \alpha^3 + k_4 \alpha^4 + k_5 \alpha^5$
+      \4 $w$ is write
+    \3 The $k$'s are all fixed
+    \3 \csPerT{2} - \csPerA{2}
+      \4 the minus is b/c the $w$s are fixed
+         for the initialization and finalization accesses
+    \3 Furthermore, the single non-linear product $\alpha i$ is shared with the
+    hashes needed for coalescing.
+  \2 compute $\vec f'$ similarly from $\vec f$
+    \3 \csPerT{5} for hashing
+    \3 the hash ensures well-formedness for booleans
+  \2 challenge $\beta$
+  \2 permutation argument for $\vec e', \vec f'$ (key $\beta$)
+    \3 \csPerT{2}
+  \2 three properties remain to be checked
+    \3 transcript is grouped by index
+    \3 within that, sorted by time
+    \3 read-over-write semantics
+      \4 with no writing to fresh indices
+\1 checking the index-order transcript
+  \2 goal: check array semantics (modulo residual range checks)
+  \2 Refer to one entry as $(v, i, t, w, c, a)$ and the next as $(v', i', t', w', c', a')$
+  \2 First, redef $w'$ to be $w'$ if $a=1$, else $w$
+    \3 \csPerT{1}
+  \2 Recall that the ranges of each value are ensured by hashing
+    \3 $i \in [N]$
+    \3 $t \in [A+1]$
+    \3 $w, c, a \in \zo$
+  \2 rules:
+    \3 start with a create
+    \3 $t$ grows or next $c=1$
+    \3 $v$ is constant or next $w=1$
+    \3 $i$ is constant or next $c=1$
+  \2 constraints:
+    \3 $c_0 = 1$
+    \3 $(v'-v)(w'-1)=0$
+    \3 $(i'-i)(c'-1)=0$
+    \3 compute $\Delta_t = (1-c')(t'-t)$
+    \3 cost: \csPerT{3}
+      \4 and range check
+      \4 and one for $c_0 = 1$
+    \3 we must show (next section) that each $\Delta_t \in [A+1]$
+\1 range check
+  \2 goal: check that each $\Delta_t$ is in $[A+1]$
+  \2 let $\vec g$ denote all $\Delta_t$s concatenated to $[A+1]$ (length $4A+1$)
+  \2 witness $\vec h$: sort $\vec g$
+    \3 check that each delta is 0 or 1. \csPerA{4}
+  \2 challenge $\alpha$
+  \2 permutation argument for $\vec g, \vec h$ (key $\alpha$)
+    \3 \csPerA{8}
+\1 Accounting
+  \2 two verifier challenges ($\alpha,\beta$)
+  \2 \csPerN{3}
+    \3 plus an extra MSM of size $2\cdot N$.
+  \2 \csPerA{53}
+    \3 The cost of a linear scan (per element scanned) is $3$ by my reckoning
+    \3 So if $A < 53/3 < 18$, you should do linear scans instead.
+\end{outline}
diff --git a/doc/mem/refs.bib b/doc/mem/refs.bib
new file mode 100644
index 00000000..d55ead9c
--- /dev/null
+++ b/doc/mem/refs.bib
@@ -0,0 +1,1985 @@
+
+% Journals
+
+% First the Full Name is given, then the abbreviation used in the AMS Math
+% Reviews, with an indication if it could not be found there.
+% Note the 2nd overwrites the 1st, so swap them if you want the full name.
+
+ %{AMS}
+ @String{AMSTrans = "American Mathematical Society Translations" }
+ @String{AMSTrans = "Amer. Math. Soc. Transl." }
+ @String{BullAMS = "Bulletin of the American Mathematical Society" }
+ @String{BullAMS = "Bull. Amer. Math. Soc." }
+ @String{ProcAMS = "Proceedings of the American Mathematical Society" }
+ @String{ProcAMS = "Proc. Amer. Math. Soc." }
+ @String{TransAMS = "Transactions of the American Mathematical Society" }
+ @String{TransAMS = "Trans. Amer. Math. Soc." }
+
+ %ACM
+ @String{CACM = "CACM" }
+ @String{CACM = "CACM" }
+ @String{CompServ = "Comput. Surveys" }
+ @String{JACM = "J. ACM" }
+ @String{ACMMathSoft = "{ACM} Transactions on Mathematical Software" }
+ @String{ACMMathSoft = "{ACM} Trans. Math. Software" }
+ @String{SIGNUM = "{ACM} {SIGNUM} Newsletter" }
+ @String{SIGNUM = "{ACM} {SIGNUM} Newslett." }
+ @String{CCS = "{ACM} {CCS}" }
+
+ @String{AmerSocio = "American Journal of Sociology" }
+ @String{AmerStatAssoc = "Journal of the American Statistical Association" }
+ @String{AmerStatAssoc = "J. Amer. Statist. Assoc." }
+ @String{ApplMathComp = "Applied Mathematics and Computation" }
+ @String{ApplMathComp = "Appl. Math. Comput." }
+ @String{AmerMathMonthly = "American Mathematical Monthly" }
+ @String{AmerMathMonthly = "Amer. Math. Monthly" }
+ @String{BIT = "{BIT}" }
+ @String{BritStatPsych = "British Journal of Mathematical and Statistical
+          Psychology" }
+ @String{BritStatPsych = "Brit. J. Math. Statist. Psych." }
+ @String{CanMathBull = "Canadian Mathematical Bulletin" }
+ @String{CanMathBull = "Canad. Math. Bull." }
+ @String{CompApplMath = "Journal of Computational and Applied Mathematics" }
+ @String{CompApplMath = "J. Comput. Appl. Math." }
+ @String{CompPhys = "Journal of Computational Physics" }
+ @String{CompPhys = "J. Comput. Phys." }
+ @String{CompStruct = "Computers and Structures" }
+ @String{CompStruct = "Comput. \& Structures" }
+ @String{CompJour = "The Computer Journal" }
+ @String{CompJour = "Comput. J." }
+ @String{CompSysSci = "Journal of Computer and System Sciences" }
+ @String{CompSysSci = "J. Comput. System Sci." }
+ @String{Computing = "Computing" }
+ @String{ContempMath = "Contemporary Mathematics" }
+ @String{ContempMath = "Contemp. Math." }
+ @String{Crelle = "Crelle's Journal" }
+ @String{GiornaleMath = "Giornale di Mathematiche" }
+ @String{GiornaleMath = "Giorn. Mat." } % didn't find in AMS MR., ibid.
+
+ %IEEE
+ @String{Computer = "{IEEE} Computer" }
+ @String{IEEETransComp = "{IEEE} Transactions on Computers" }
+ @String{IEEETransComp = "{IEEE} Trans. Comput." }
+ @String{IEEETransAC = "{IEEE} Transactions on Automatic Control" }
+ @String{IEEETransAC = "{IEEE} Trans. Automat. Control" }
+ @String{IEEESpec = "{IEEE} Spectrum" } % didn't find in AMS MR
+ @String{ProcIEEE = "Proceedings of the {IEEE}" }
+ @String{ProcIEEE = "Proc. {IEEE}" } % didn't find in AMS MR
+ @String{IEEETransAeroElec = "{IEEE} Transactions on Aerospace and Electronic
+     Systems" }
+ @String{IEEETransAeroElec = "{IEEE} Trans. Aerospace Electron. Systems" }
+
+ @String{IMANumerAna = "{IMA} Journal of Numerical Analysis" }
+ @String{IMANumerAna = "{IMA} J. Numer. Anal." }
+ @String{InfProcLet = "Information Processing Letters" }
+ @String{InfProcLet = "Inform. Process. Lett." }
+ @String{InstMathApp = "Journal of the Institute of Mathematics and
+     its Applications" }
+ @String{InstMathApp = "J. Inst. Math. Appl." }
+ @String{IntControl = "International Journal of Control" }
+ @String{IntControl = "Internat. J. Control" }
+ @String{IntNumerEng = "International Journal for Numerical Methods in
+     Engineering" }
+ @String{IntNumerEng = "Internat. J. Numer. Methods Engrg." }
+ @String{IntSuper = "International Journal of Supercomputing Applications" }
+ @String{IntSuper = "Internat. J. Supercomputing Applic." } % didn't find
+%% in AMS MR
+ @String{Kibernetika = "Kibernetika" }
+ @String{JResNatBurStand = "Journal of Research of the National Bureau
+     of Standards" }
+ @String{JResNatBurStand = "J. Res. Nat. Bur. Standards" }
+ @String{LinAlgApp = "Linear Algebra and its Applications" }
+ @String{LinAlgApp = "Linear Algebra Appl." }
+ @String{MathAnaAppl = "Journal of Mathematical Analysis and Applications" }
+ @String{MathAnaAppl = "J. Math. Anal. Appl." }
+ @String{MathAnnalen = "Mathematische Annalen" }
+ @String{MathAnnalen = "Math. Ann." }
+ @String{MathPhys = "Journal of Mathematical Physics" }
+ @String{MathPhys = "J. Math. Phys." }
+ @String{MathComp = "Mathematics of Computation" }
+ @String{MathComp = "Math. Comp." }
+ @String{MathScand = "Mathematica Scandinavica" }
+ @String{MathScand = "Math. Scand." }
+ @String{TablesAidsComp = "Mathematical Tables and Other Aids to Computation" }
+ @String{TablesAidsComp = "Math. Tables Aids Comput." }
+ @String{NumerMath = "Numerische Mathematik" }
+ @String{NumerMath = "Numer. Math." }
+ @String{PacificMath = "Pacific Journal of Mathematics" }
+ @String{PacificMath = "Pacific J. Math." }
+ @String{ParDistComp = "Journal of Parallel and Distributed Computing" }
+ @String{ParDistComp = "J. Parallel and Distrib. Comput." } % didn't find
+%% in AMS MR
+ @String{ParComputing = "Parallel Computing" }
+ @String{ParComputing = "Parallel Comput." }
+ @String{PhilMag = "Philosophical Magazine" }
+ @String{PhilMag = "Philos. Mag." }
+ @String{ProcNAS = "Proceedings of the National Academy of Sciences
+                    of the USA" }
+ @String{ProcNAS = "Proc. Nat. Acad. Sci. U. S. A." }
+ @String{Psychometrika = "Psychometrika" }
+ @String{QuartMath = "Quarterly Journal of Mathematics, Oxford, Series (2)" }
+ @String{QuartMath = "Quart. J. Math. Oxford Ser. (2)" }
+ @String{QuartApplMath = "Quarterly of Applied Mathematics" }
+ @String{QuartApplMath = "Quart. Appl. Math." }
+ @String{RevueInstStat = "Review of the International Statisical Institute" }
+ @String{RevueInstStat = "Rev. Inst. Internat. Statist." }
+
+ %SIAM
+ @String{JSIAM = "Journal of the Society for Industrial and Applied
+     Mathematics" }
+ @String{JSIAM = "J. Soc. Indust. Appl. Math." }
+ @String{JSIAMB = "Journal of the Society for Industrial and Applied
+     Mathematics, Series B, Numerical Analysis" }
+ @String{JSIAMB = "J. Soc. Indust. Appl. Math. Ser. B Numer. Anal." }
+ @String{SIAMAlgMeth = "{SIAM} Journal on Algebraic and Discrete Methods" }
+ @String{SIAMAlgMeth = "{SIAM} J. Algebraic Discrete Methods" }
+ @String{SIAMAppMath = "{SIAM} Journal on Applied Mathematics" }
+ @String{SIAMAppMath = "{SIAM} J. Appl. Math." }
+ @String{SIAMComp = "{SIAM} Journal on Computing" }
+ @String{SIAMComp = "{SIAM} J. Comput." }
+ @String{SIAMMatrix = "{SIAM} Journal on Matrix Analysis and Applications" }
+ @String{SIAMMatrix = "{SIAM} J. Matrix Anal. Appl." }
+ @String{SIAMNumAnal = "{SIAM} Journal on Numerical Analysis" }
+ @String{SIAMNumAnal = "{SIAM} J. Numer. Anal." }
+ @String{SIAMReview = "{SIAM} Review" }
+ @String{SIAMReview = "{SIAM} Rev." }
+ @String{SIAMSciStat = "{SIAM} Journal on Scientific and Statistical
+     Computing" }
+ @String{SIAMSciStat = "{SIAM} J. Sci. Statist. Comput." }
+
+ @String{SoftPracExp = "Software Practice and Experience" }
+ @String{SoftPracExp = "Software Prac. Experience" } % didn't find in AMS MR
+ @String{StatScience = "Statistical Science" }
+ @String{StatScience = "Statist. Sci." }
+ @String{Techno = "Technometrics" }
+ @String{USSRCompMathPhys = "{USSR} Computational Mathematics and Mathematical
+     Physics" }
+ @String{USSRCompMathPhys = "{U. S. S. R.} Comput. Math. and Math. Phys." }
+ @String{VLSICompSys = "Journal of {VLSI} and Computer Systems" }
+ @String{VLSICompSys = "J. {VLSI} Comput. Syst." }
+ @String{ZAngewMathMech = "Zeitschrift fur Angewandte Mathematik und
+     Mechanik" }
+ @String{ZAngewMathMech = "Z. Angew. Math. Mech." }
+ @String{ZAngewMathPhys = "Zeitschrift fur Angewandte Mathematik und Physik" }
+ @String{ZAngewMathPhys = "Z. Angew. Math. Phys." }
+
+% Publishers % ================================================= |
+
+ @String{Academic = "Academic Press" }
+ @String{ACMPress = "{ACM} Press" }
+ @String{AdamHilger = "Adam Hilger" }
+ @String{AddisonWesley = "Addison-Wesley" }
+ @String{AllynBacon = "Allyn and Bacon" }
+ @String{AMS = "American Mathematical Society" }
+ @String{Birkhauser = "Birkha{\"u}ser" }
+ @String{CambridgePress = "Cambridge University Press" }
+ @String{Chelsea = "Chelsea" }
+ @String{ClaredonPress = "Claredon Press" }
+ @String{DoverPub = "Dover Publications" }
+ @String{Eyolles = "Eyolles" }
+ @String{HoltRinehartWinston = "Holt, Rinehart and Winston" }
+ @String{Interscience = "Interscience" }
+ @String{JohnsHopkinsPress = "The Johns Hopkins University Press" }
+ @String{JohnWileySons = "John Wiley and Sons" }
+ @String{Macmillan = "Macmillan" }
+ @String{MathWorks = "The Math Works Inc." }
+ @String{McGrawHill = "McGraw-Hill" }
+ @String{NatBurStd = "National Bureau of Standards" }
+ @String{NorthHolland = "North-Holland" }
+ @String{OxfordPress = "Oxford University Press" }  %address Oxford or London?
+ @String{PergamonPress = "Pergamon Press" }
+ @String{PlenumPress = "Plenum Press" }
+ @String{PrenticeHall = "Prentice-Hall" }
+ @String{SIAMPub = "{SIAM} Publications" }
+ @String{Springer = "Springer-Verlag" }
+ @String{TexasPress = "University of Texas Press" }
+ @String{VanNostrand = "Van Nostrand" }
+ @String{WHFreeman = "W. H. Freeman and Co." }
+
+@string{SOSP = {SOSP}}
+@string{NDSS = {NDSS}}
+@string{SECURITY = {USENIX Security}}
+@string{OAKLAND = {IEEE S\&P}}
+@string{CRYPTO = {CRYPTO}}
+@string{EUROCRYPT = {EUROCRYPT}}
+@string{CCS = {CCS}}
+@string{CAV = {CAV}}
+@string{FC = {Financial Cryptography}}
+@string{PLDI = {PLDI}}
+@string{POPL = {POPL}}
+@string{SAT = {SAT}}
+
+%Entries
+
+
+@inproceedings{cadar2008klee,
+  title={{KLEE}: Unassisted and automatic generation of high-coverage tests for complex systems programs},
+  author={Cadar, Cristian and Dunbar, Daniel and Engler, Dawson R},
+  booktitle={OSDI},
+  year={2008}
+}
+
+@inproceedings{brown2020towards,
+  title={Towards a verified range analysis for JavaScript JITs.},
+  author={Brown, Fraser and Renner, John and N{\"o}tzli, Andres and Lerner, Sorin and Shacham, Hovav and Stefan, Deian},
+  booktitle=PLDI,
+  year={2020}
+}
+
+@inproceedings{lopes2015provably,
+  title={Provably correct peephole optimizations with {Alive}},
+  author={Lopes, Nuno P and Menendez, David and Nagarakatte, Santosh and Regehr, John},
+  booktitle=PLDI,
+  year={2015}
+}
+
+@inproceedings{xie2007saturn,
+  title={Saturn: A scalable framework for error detection using boolean satisfiability},
+  author={Xie, Yichen and Aiken, Alex},
+  booktitle={TOPLAS},
+  year={2007},
+}
+
+@inproceedings{bjorner2014applications,
+  title={Applications of {SMT} solvers to program verification},
+  author={Bj{\o}rner, Nikolaj and de Moura, Leonardo},
+  booktitle={Notes for the Summer School on Formal Techniques},
+  year={2014}
+}
+
+@inproceedings{yun2018qsym,
+  title={{QSYM}: A practical concolic execution engine tailored for hybrid fuzzing},
+  author={Yun, Insu and Lee, Sangho and Xu, Meng and Jang, Yeongjin and Kim, Taesoo},
+  booktitle=SECURITY,
+  year={2018}
+}
+
+@inproceedings{leino2010dafny,
+  title={Dafny: An automatic program verifier for functional correctness},
+  author={Leino, K. Rustan M.},
+  xbooktitle={International Conference on Logic for Programming Artificial Intelligence and Reasoning},
+  booktitle = {LPAR},
+  year={2010},
+}
+
+@inproceedings{barnett2005boogie,
+  title={Boogie: A modular reusable verifier for object-oriented programs},
+  author={Barnett, Mike and Chang, Bor-Yuh Evan and DeLine, Robert and Jacobs, Bart and Leino, K Rustan M},
+  xbooktitle={International Symposium on Formal Methods for Components and Objects},
+  booktitle = {FMCO},
+  year={2005},
+}
+
+@inproceedings{rakamaric2014smack,
+  title={SMACK: Decoupling source language details from verifier implementations},
+  author={Rakamari{\'c}, Zvonimir and Emmi, Michael},
+  booktitle=CAV,
+  year={2014},
+}
+
+@phdthesis{vazou2016liquid,
+  title={Liquid Haskell: Haskell as a theorem prover},
+  author={Vazou, Niki},
+  year={2016},
+  school={UC San Diego}
+}
+
+@inproceedings{torlak2013growing,
+  title={Growing solver-aided languages with {Rosette}},
+  author={Torlak, Emina and Bodik, Rastislav},
+  xbooktitle={Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming \& software},
+  booktitle = {Onward{!}},
+  year={2013}
+}
+
+@inproceedings{filliatre2013why3,
+  title={Why3—where programs meet provers},
+  author={Filli{\^a}tre, Jean-Christophe and Paskevich, Andrei},
+  xbooktitle={European symposium on programming},
+  booktitle = {ESOP},
+  year={2013},
+}
+
+@inproceedings{cauligi2019fact,
+  title={FaCT: a DSL for timing-sensitive computation},
+  author={Cauligi, Sunjay and Soeller, Gary and Johannesmeyer, Brian and Brown, Fraser and Wahby, Riad S and Renner, John and Gr{\'e}goire, Benjamin and Barthe, Gilles and Jhala, Ranjit and Stefan, Deian},
+  booktitle=PLDI,
+  year={2019}
+}
+
+@inproceedings{barthe2019formal,
+  title={Formal verification of a constant-time preserving C compiler},
+  author={Barthe, Gilles and Blazy, Sandrine and Gr{\'e}goire, Benjamin and Hutin, R{\'e}mi and Laporte, Vincent and Pichardie, David and Trieu, Alix},
+  booktitle=POPL,
+  year={2019},
+}
+
+@inproceedings{menendez2016alive,
+  title={Alive-{FP}: Automated verification of floating point based peephole optimizations in {LLVM}},
+  author={Menendez, David and Nagarakatte, Santosh and Gupta, Aarti},
+  xbooktitle={International Static Analysis Symposium},
+  booktitle = {SAS},
+  year={2016},
+}
+
+@inproceedings{notzli2016lifejacket,
+  title={LifeJacket: Verifying precise floating-point optimizations in {LLVM}},
+  author={N{\"o}tzli, Andres and Brown, Fraser},
+  xbooktitle={Proceedings of the 5th ACM SIGPLAN International Workshop on State of the Art in Program Analysis},
+  booktitle = {SOAP},
+  year={2016}
+}
+	  
+@inproceedings{andrysco2018towards,
+  title={Towards verified, constant-time floating point operations},
+  author={Andrysco, Marc and N{\"o}tzli, Andres and Brown, Fraser and Jhala, Ranjit and Stefan, Deian},
+  booktitle=CCS,
+  year={2018}
+}
+
+@inproceedings{leino2016trigger,
+  title={Trigger selection strategies to stabilize program verifiers},
+  author={Leino, K Rustan M and Pit-Claudel, Cl{\'e}ment},
+  booktitle={CAV},
+  year={2016},
+  organization={Springer}
+}
+
+@inproceedings{notzli2018p4pktgen,
+  title={P4pktgen: Automated test case generation for p4 programs},
+  author={N{\"o}tzli, Andres and Khan, Jehandad and Fingerhut, Andy and Barrett, Clark and Athanas, Peter},
+  booktitle={Proceedings of the Symposium on SDN Research},
+  year={2018}
+}
+
+@inproceedings{v2019pretend,
+  title={Pretend synchrony: synchronous verification of asynchronous distributed programs},
+  author={v. Gleissenthall, Klaus and K{\i}c{\i}, Rami G{\"o}khan and Bakst, Alexander and Stefan, Deian and Jhala, Ranjit},
+  booktitle=POPL,
+  year={2019},
+}
+
+@inproceedings{zhong2020move,
+  title={The Move Prover},
+  author={Zhong, Jingyi Emma and Cheang, Kevin and Qadeer, Shaz and Grieskamp, Wolfgang and Blackshear, Sam and Park, Junkil and Zohar, Yoni and Barrett, Clark and Dill, David L},
+  booktitle=CAV,
+  year={2020},
+}
+
+@techreport{park2020end,
+  title={End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract},
+  author={Park, Daejun and Zhang, Yi and Rosu, Grigore},
+  year={2020}
+}  
+
+@misc{circom,
+    title       = {Circom},
+    howpublished= {\url{https://github.com/iden3/circom}},
+    author      = {Jordi Baylina},
+    key         = "circom"
+}
+
+@misc{zinc,
+    title       = {Zinc},
+    howpublished= {\url{https://zinc.matterlabs.dev/}},
+    key = "zinc",
+}
+@misc{noir,
+    title       = {Noir},
+    howpublished= {\url{https://noir-lang.github.io/book/index.html}},
+    key = "noir",
+}
+@misc{leo,
+    title       = {Leo},
+    howpublished= {\url{https://developer.aleo.org/aleo/getting_started/overview/}},
+    key = "leo",
+}
+@misc{leo_paper,
+    author       = {Collin Chin and
+                    Howard Wu and
+                    Raymond Chu and
+                    Alessandro Coglio and
+                    Eric McCarthy and
+                    Eric Smith},
+    title        = {Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications},
+    xhowpublished = {Cryptology ePrint Archive, Report 2021/651},
+    year         = {2021},
+    note         = {\url{https://ia.cr/2021/651}},
+}
+
+@misc{CVE-2014-3570,
+    title       = {CVE-2014-3570},
+    howpublished= {\url{https://nvd.nist.gov/vuln/detail/CVE-2014-3570}},
+    key = "cve-2014-3570",
+}
+
+@misc{opensslbugblog,
+    title       = {OpenSSL's squaring bug, and opportunistic formal verification},
+    howpublished= {\url{http://kryptoslogic.blogspot.com/2015/01/openssls-squaring-bug-and-opportunistic.html}},
+    key = "opensslbug",
+}
+
+@misc{zokrates,
+    title       = {{ZoKrates}},
+    howpublished= {\url{https://zokrates.github.io/}},
+    key = "zokrates",
+}
+
+@inproceedings{bensasson13snarks,
+  author = {Eli Ben-Sasson and Alessandro Chiesa and Daniel Genkin and Eran Tromer and Madars Virza},
+  title = {{SNARKs} for {C}: Verifying Program Executions Succinctly and in Zero Knowledge},
+  booktitle = CRYPTO,
+  year = {2013},
+  month = aug,
+  xpages = {90-108}
+}
+
+@inproceedings{bensasson14succinct,
+    author = "Eli Ben-Sasson and Alessandro Chiesa and Eran Tromer and
+        Madars Virza",
+    title = "Succinct Non-Interactive Zero Knowledge for a von {N}eumann
+        Architecture",
+    booktitle = SECURITY,
+    year = 2014,
+    month = aug,
+    xnote = "\url{http://eprint.iacr.org/2013/879/20140901:001903}"
+}
+
+@inproceedings{braun13verifying,
+    author = "Benjamin Braun and Ariel J. Feldman and Zuocheng Ren and
+        Srinath Setty and Andrew J. Blumberg and Michael Walfish",
+    title = "Verifying computations with state",
+    year = 2013,
+    month = nov,
+    booktitle = SOSP,
+    xpages = {341--357},
+    note = "Extended version: \url{http://eprint.iacr.org/2013/356}"
+}
+
+@inproceedings{wahby15efficient,
+    author = "Riad S. Wahby and Srinath Setty and Zuocheng Ren and
+        Andrew J. Blumberg and Michael Walfish",
+  title = "Efficient {RAM} and control flow in verifiable outsourced
+      computation",
+  year = 2015,
+  month = feb,
+  booktitle = NDSS,
+  xnote = {Preprint: http://eprint.iacr.org/2014/674}
+}
+
+@inproceedings{kosba18xjsnark,
+  author =       "Ahmed E. Kosba and
+                  Charalampos Papamanthou and
+                  Elaine Shi",
+  title =        "{xJsnark}: {A} Framework for Efficient Verifiable Computation",
+  booktitle =    OAKLAND,
+  month =        may,
+  year =         2018,
+}
+
+@inproceedings{ozdemir20scaling,
+  author = "Alex Ozdemir and Riad S. Wahby and Barry Whitehat and Dan Boneh",
+  title = "Scaling verifiable computation using efficient set accumulators",
+  booktitle = SECURITY,
+  month = aug,
+  year = 2020,
+}
+
+@misc{rollup,
+  title = {roll\_up: Scale ethereum with {SNARK}s},
+  author = {Barry Whitehat},
+  howpublished = {\url{https://github.com/barryWhiteHat/roll_up}},
+  key = {rollup},
+}
+
+@inproceedings{lee20replicated,
+  author = {Jonathan Lee and Kirill Nikitin and Srinath Setty},
+  title = {Replicated state machines without replicated execution},
+  booktitle = OAKLAND,
+  month = may,
+  year = 2020,
+}
+
+@inproceedings{bowe20zexe,
+  author = {Sean Bowe and Alessandro Chiesa and Matthew Green and Ian Miers and Pratyush Mishra and Howard Wu},
+  title = {{ZEXE}: Enabling decentralized private computation},
+  booktitle = OAKLAND,
+  month = may,
+  year = 2020,
+}
+
+@article{breidenbach2019hydra,
+  title={The {Hydra} framework for principled, automated bug bounties},
+  author={Breidenbach, Lorenz and Daian, Philip and Tram{\`e}r, Florian and Juels, Ari},
+  journal={IEEE Security \& Privacy Magazine},
+  year={2019},
+  month=jul,
+  volume=17,
+  number=4,
+  pages={53--61},
+}
+
+@inproceedings{breidenbach2018enter,
+  title={Enter the {H}ydra: Towards principled bug bounties and exploit-resistant smart contracts},
+  author={Breidenbach, Lorenz and Daian, Philip and Tram{\`e}r, Florian and Juels, Ari},
+  booktitle=SECURITY,
+  year={2018}
+}
+
+@inproceedings{tramer2017sealed,
+  title={Sealed-glass proofs: Using transparent enclaves to prove and sell knowledge},
+  author={Tram{\`e}r, Florian and Zhang, Fan and Lin, Huang and Hubaux, Jean-Pierre and Juels, Ari and Shi, Elaine},
+  booktitle=OAKLAND,
+  year={2017},
+}
+
+@inproceedings{laszka2016banishing,
+  title={Banishing misaligned incentives for validating reports in bug-bounty platforms},
+  author={Laszka, Aron and Zhao, Mingyi and Grossklags, Jens},
+  xbooktitle={European Symposium on Research in Computer Security},
+  booktitle = {ESORICS},
+  year={2016},
+}
+
+@inproceedings{laszka2018rules,
+  title={The rules of engagement for bug bounty programs},
+  author={Laszka, Aron and Zhao, Mingyi and Malbari, Akash and Grossklags, Jens},
+  booktitle=FC,
+  year={2018},
+}
+
+@misc{tob,
+  title     = {Reinventing Vulnerability Disclosure using Zero-knowledge Proofs},
+  author = {Ben Perez},
+  year      = 2020,
+  xmonth = may,
+  xday = 21,
+  xkey ={reinventing},
+  howpublished = {\url{https://blog.trailofbits.com/2020/05/21/reinventing-vulnerability-disclosure-using-zero-knowledge-proofs/}},
+}
+
+@article{godefroid2012sage,
+  title={{SAGE}: Whitebox fuzzing for security testing},
+  author={Godefroid, Patrice and Levin, Michael Y and Molnar, David},
+  journal={CACM},
+  volume={55},
+  number={3},
+  pages={40--44},
+  year={2012},
+}
+}
+
+@inproceedings{ramos2015under,
+  title={Under-constrained symbolic execution: Correctness checking for real code},
+  author={Ramos, David A and Engler, Dawson},
+  booktitle=SECURITY,
+  year={2015}
+}
+
+@inproceedings{chipounov2011s2e,
+  title={{S2E}: A platform for in-vivo multi-path analysis of software systems},
+  author={Chipounov, Vitaly and Kuznetsov, Volodymyr and Candea, George},
+  booktitle={ASPLOS},
+  year={2011},
+}		
+
+@inproceedings{stephens2016driller,
+  title={Driller: Augmenting Fuzzing Through Selective Symbolic Execution},
+  author={Stephens, Nick and Grosen, John and Salls, Christopher and Dutcher, Andrew and Wang, Ruoyu and Corbetta, Jacopo and Shoshitaishvili, Yan and Kruegel, Christopher and Vigna, Giovanni},
+  booktitle={NDSS},
+  year={2016}
+}
+
+@inproceedings{brown2020sys,
+  title={Sys: A static/symbolic tool for finding good bugs in good (browser) code},
+  author={Brown, Fraser and Stefan, Deian and Engler, Dawson},
+  booktitle=SECURITY,
+  year={2020}
+}
+
+@inproceedings{poeplau2020symbolic,
+  title={Symbolic execution with {SymCC}: Don't interpret, compile!},
+  author={Poeplau, Sebastian and Francillon, Aur{\'e}lien},
+  booktitle=SECURITY,
+  year={2020}
+}
+
+@misc{sasnauskas2017souper,
+  title={Souper: A synthesizing superoptimizer},
+  author={Sasnauskas, Raimondas and Chen, Yang and Collingbourne, Peter and Ketema, Jeroen and Lup, Gratian and Taneja, Jubi and Regehr, John},
+  howpublished={arXiv:1711.04422},
+  key="sasnauskas2017souper",
+  year={2017}
+}
+
+@inproceedings{albert2020synthesis,
+  title={Synthesis of Super-Optimized Smart Contracts Using {Max-SMT}},
+  author={Albert, Elvira and Gordillo, Pablo and Rubio, Albert and Schett, Maria A},
+  booktitle=CAV,
+  year={2020},
+}
+
+@inproceedings{jia2019taso,
+  title={{TASO}: optimizing deep learning computation with automatic generation of graph substitutions},
+  author={Jia, Zhihao and Padon, Oded and Thomas, James and Warszawski, Todd and Zaharia, Matei and Aiken, Alex},
+  booktitle={SOSP},
+  year={2019}
+}
+
+inproceedings{eberhardt18zokrates,
+  author    = {Jacob Eberhardt and
+               Stefan Tai},
+  title     = {ZoKrates - Scalable Privacy-Preserving Off-Chain Computations},
+  xbooktitle = {{IEEE} International Conference on Internet of Things (iThings) and
+               {IEEE} Green Computing and Communications (GreenCom) and {IEEE} Cyber,
+               Physical and Social Computing (CPSCom) and {IEEE} Smart Data (SmartData),
+               iThings/GreenCom/CPSCom/SmartData 2018, Halifax, NS, Canada, July
+               30 - August 3, 2018},
+  booktitle = {IEEE Blockchain},
+  xpages     = {1084--1091},
+  xpublisher = {{IEEE}},
+  year      = {2018},
+  xurl       = {https://doi.org/10.1109/Cybermatics\_2018.2018.00199},
+  xdoi       = {10.1109/Cybermatics\_2018.2018.00199},
+  xtimestamp = {Wed, 16 Oct 2019 14:14:56 +0200},
+  xbiburl    = {https://dblp.org/rec/conf/ithings/EberhardtT18.bib},
+  xbibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@misc{haskell:alex,
+    title       = {Alex: A lexical analyser generator for Haskell},
+    howpublished= {\url{https://www.haskell.org/alex/}},
+    key          = "alex",
+}
+
+@misc{cvc4:shl_by_const,
+    title       = {CVC4, ShlByConst Rewrite Rule},
+    howpublished= {\url{https://github.com/CVC4/CVC4/blob/d7f92f70bb8ff221dc3d7cb086e5e2e237dadc67/src/theory/bv/theory_bv_rewrite_rules_simplification.h\#L312}},
+    key = "cvc4 rewrite rule"
+}
+
+@misc{gill1995happy,
+  title={Happy: the parser generator for Haskell},
+  author={Gill, Andy and Marlow, Simon},
+  howpublished={\url{https://www.haskell.org/happy/doc/html/}},
+  key=gill1995happy
+}
+
+@inproceedings{barrett2010smt,
+  title={The {SMT-LIB} standard: Version 2.0},
+  author={Barrett, Clark and Stump, Aaron and Tinelli, Cesare},
+  xbooktitle={Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England)},
+  booktitle = {SMT},
+  xvolume={13},
+  xpages={14},
+  year={2010}
+}
+
+@misc{zokdeloitte,
+    title        = {Zero-Knowledge taxation on Ethereum},
+    author       = {Kobi Gurkan},
+    xmonth        = jun,
+    xyear         = 2018,
+    xday          = 24,
+    howpublished = {\url{https://medium.com/qed-it/zero-knowledge-qed-it-sdk-b20a6526e0a6}},
+    key = {gurkan},
+
+}
+
+@misc{deloitte,
+    title        = {Deloitte},
+    howpublished = {\url{deloitte.com}},
+    key          = "deloitte"
+}
+  
+@misc{cvc4issue5354,
+    title        = {Performance issue on {QF\_NIRA} formula. {CVC4} {I}ssue 5354},
+    author       = {Mu Chang},
+    xmonth        = nov,
+    xyear         = 2020,
+    xday          = 9,
+    key          = "cvc4 issue 5354",
+    howpublished = {\url{https://github.com/CVC4/CVC4/issues/5354}}
+}
+
+@inproceedings{godefroid2005dart,
+  title={{DART}: Directed automated random testing},
+  author={Godefroid, Patrice and Klarlund, Nils and Sen, Koushik},
+  booktitle=PLDI,
+  year={2005}
+}
+	  
+@inproceedings{sen2005cute,
+  title={{CUTE}: A concolic unit testing engine for {C}},
+  author={Sen, Koushik and Marinov, Darko and Agha, Gul},
+  booktitle={ESEC-FSE},
+  year={2005},
+}
+		
+@inproceedings{torlak2014lightweight,
+  title={A lightweight symbolic virtual machine for solver-aided host languages},
+  author={Torlak, Emina and Bodik, Rastislav},
+  booktitle={PLDI},
+  year={2014},
+}
+
+@inproceedings{solar2006combinatorial,
+  title={Combinatorial sketching for finite programs},
+  author={Solar-Lezama, Armando and Tancau, Liviu and Bodik, Rastislav and Seshia, Sanjit and Saraswat, Vijay},
+  booktitle={ASPLOS},
+  year={2006}
+}
+	  
+@inproceedings{kneuss2013synthesis,
+  title={Synthesis modulo recursive functions},
+  author={Kneuss, Etienne and Kuraj, Ivan and Kuncak, Viktor and Suter, Philippe},
+  booktitle={OOPSLA},
+  year={2013}
+}
+
+@inproceedings{srivastava2010program,
+  title={From program verification to program synthesis},
+  author={Srivastava, Saurabh and Gulwani, Sumit and Foster, Jeffrey S},
+  booktitle=POPL,
+  year={2010}
+}
+
+@inproceedings{gurfinkel2017context,
+  title={A context-sensitive memory model for verification of {C/C++} programs},
+  author={Gurfinkel, Arie and Navas, Jorge A},
+  xbooktitle={International Static Analysis Symposium},
+  booktitle = {SAS},
+  year={2017},
+}
+
+@inproceedings{sinz2010precise,
+  title={A precise memory model for low-level bounded model checking},
+  author={Sinz, Carsten and Falke, Stephan and Merz, Florian},
+  xbooktitle={Conference on Systems software verification},
+  booktitle = {SSV},
+  year={2010}
+}
+
+@misc{leino2008boogie,
+  title={This is {Boogie} 2},
+  author={Leino, K. Rustan M.},
+  xjournal={manuscript KRML},
+  xvolume={178},
+  xnumber={131},
+  xpages={9},
+  year={2008},
+  howpublished = {\url{https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml178.pdf}},
+}
+
+
+@inproceedings{cohen2009precise,
+  title={A precise yet efficient memory model for {C}},
+  author={Cohen, Ernie and Moskal, Micha{\l} and Tobies, Stephan and Schulte, Wolfram},
+  booktitle = {SSV},
+  xjournal={Electronic Notes in Theoretical Computer Science},
+  xvolume={254},
+  xpages={85--103},
+  year={2009},
+  month=oct,
+}
+
+@inproceedings{mitchell2012information,
+  title={Information-flow control for programming on encrypted data},
+  author={Mitchell, John C and Sharma, Rahul and Stefan, Deian and Zimmerman, Joe},
+  booktitle={CSF},
+  year={2012},
+}
+
+@inproceedings{notzli2019sat,
+  author    = {Andres N{\"{o}}tzli and
+               Andrew Reynolds and
+               Haniel Barbosa and
+               Aina Niemetz and
+               Mathias Preiner and
+               Clark W. Barrett and
+               Cesare Tinelli},
+  xeditor    = {Mikol{\'{a}}s Janota and
+               In{\^{e}}s Lynce},
+  title     = {Syntax-Guided Rewrite Rule Enumeration for {SMT} Solvers},
+  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2019 - 22nd
+               International Conference, {SAT} 2019, Lisbon, Portugal, July 9-12,
+               2019, Proceedings},
+  xseries    = {Lecture Notes in Computer Science},
+  xvolume    = {11628},
+  xpages     = {279--297},
+  xpublisher = {Springer},
+  year      = {2019},
+  xurl       = {https://doi.org/10.1007/978-3-030-24258-9\_20},
+  xdoi       = {10.1007/978-3-030-24258-9\_20},
+  xtimestamp = {Fri, 05 Jul 2019 09:41:26 +0200},
+  xbiburl    = {https://dblp.org/rec/conf/sat/NotzliRBNPBT19.bib},
+  xbibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+% solvers
+@inproceedings{boolector,
+  author    = {Aina Niemetz and
+               Mathias Preiner and
+               Clifford Wolf and
+               Armin Biere},
+  xeditor    = {Hana Chockler and
+               Georg Weissenbacher},
+  title     = {{Btor2} , {BtorMC} and {B}oolector 3.0},
+  booktitle = {CAV},
+  xseries    = {Lecture Notes in Computer Science},
+  xvolume    = {10981},
+  xpages     = {587--595},
+  xpublisher = {Springer},
+  year      = {2018},
+  xurl       = {https://doi.org/10.1007/978-3-319-96145-3\_32},
+  xdoi       = {10.1007/978-3-319-96145-3\_32},
+  xtimestamp = {Fri, 31 Jan 2020 21:32:18 +0100},
+  xbiburl    = {https://dblp.org/rec/conf/cav/NiemetzPWB18.bib},
+  xbibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@misc{bitwuzla,
+  title={{B}itwuzla at the {SMT-COMP} 2020},
+  author={Niemetz, Aina and Preiner, Mathias},
+  howpublished={arXiv:2006.01621},
+  year={2020},
+  key={bitwuzla},
+}
+@inproceedings{z3,
+  title={Z3: An efficient {SMT} solver},
+  author={De Moura, Leonardo and Bj{\o}rner, Nikolaj},
+  xbooktitle={International conference on Tools and Algorithms for the Construction and Analysis of Systems},
+  booktitle = {TACAS},
+  xpages={337--340},
+  year={2008},
+  xorganization={Springer}
+}
+@book{baader1999term,
+  title={Term rewriting and all that},
+  author={Baader, Franz and Nipkow, Tobias},
+  year={1999},
+  publisher={Cambridge University Press},
+  address = {Cambridge, UK},
+}
+@inproceedings{yices22,
+  title={Yices 2.2},
+  author={Dutertre, Bruno},
+  xbooktitle={International Conference on Computer Aided Verification},
+  booktitle = {CAV},
+  xpages={737--744},
+  year={2014},
+  xorganization={Springer}
+}
+@inproceedings{mathsat4,
+  title={The {MathSAT} 4 {SMT} solver},
+  author={Bruttomesso, Roberto and Cimatti, Alessandro and Franz{\'e}n, Anders and Griggio, Alberto and Sebastiani, Roberto},
+  xbooktitle={International Conference on Computer Aided Verification},
+  booktitle = {CAV},
+  xpages={299--303},
+  year={2008},
+  xorganization={Springer}
+}
+@inproceedings{cvc4,
+  title={{CVC4}},
+  author={Barrett, Clark and Conway, Christopher L and Deters, Morgan and Hadarean, Liana and Jovanovi{\'c}, Dejan and King, Tim and Reynolds, Andrew and Tinelli, Cesare},
+  xbooktitle={International Conference on Computer Aided Verification},
+  booktitle = {CAV},
+  xpages={171--177},
+  year={2011},
+  xorganization={Springer}
+}
+
+@inproceedings{beyer2019automatic,
+  title={Automatic verification of {C} and {Java} programs: {SV-COMP} 2019},
+  author={Beyer, Dirk},
+  booktitle={TACAS},
+  year={2019},
+}
+
+@inproceedings{mullen2016verified,
+  title={Verified peephole optimizations for {CompCert}},
+  author={Mullen, Eric and Zuniga, Daryl and Tatlock, Zachary and Grossman, Dan},
+  booktitle=PLDI,
+  year={2016}
+}
+
+@misc{bellman,
+  title = {Bellman Circuit Library and zkSNARK},
+  author = {Zcash developers},
+  xhowpublished = {\url{https://github.com/matter-labs/bellman}},
+  xtitle = {bellman},
+  howpublished = {\url{https://github.com/zkcrypto/bellman}},
+  key = {bellman},
+}
+
+@misc{libsnark,
+  key={libsnark},
+  howpublished={\url{https://github.com/scipr-lab/libsnark}},
+  title="libsnark",
+  xyear="2016",
+}
+
+@InProceedings{bensasson14zerocash,
+  author =       "Eli {Ben-Sasson} and
+                  Alessandro Chiesa and
+                  Christina Garman and
+                  Matthew Green and
+                  Ian Miers and
+                  Eran Tromer and
+                  Madars Virza",
+  title =        {Zerocash: Decentralized Anonymous Payments from {B}itcoin},
+  booktitle =    OAKLAND,
+  month =        may,
+  publisher =    ieeesppub,
+  year =         2014,
+  xdoi =          "10.1109/SP.2014.36",
+}
+
+@InProceedings{bendavid08fairplaymp,
+  author =       "Assaf {Ben-David} and
+                  Noam Nisan and
+                  Benny Pinkas",
+  title =        "{FairplayMP}: a system for secure multi-party computation",
+  booktitle =    CCS,
+  month =        oct,
+  year =         2008,
+}
+
+@InProceedings{buescher18hycc,
+  author =       "Niklas B{\"u}scher and
+                  Daniel Demmler and
+                  Stefan Katzenbeisser and
+                  David Kretzmer and
+                  Thomas Schneider",
+  title =        "{HyCC}: Compilation of Hybrid Protocols for Practical Secure Computation",
+  booktitle =    CCS,
+  month =        oct,
+  year =         2018,
+}
+
+@InProceedings{costello15geppetto,
+  author =       "Craig Costello and
+                  C{\'e}dric Fournet and
+                  Jon Howell and
+                  Markulf Kohlweiss and
+                  Benjamin Kreuter and
+                  Michael Naehrig and
+                  Bryan Parno and
+                  Samee Zahur",
+  title =        "Geppetto: Versatile Verifiable Computation",
+  booktitle =    OAKLAND,
+  month =        may,
+  year =         2015,
+}
+
+@InProceedings{malkhi04fairplay,
+  author =       "Dahlia Malkhi and
+                  Noam Nisan and
+                  Benny Pinkas and
+                  Yaron Sella",
+  title =        "Fairplay--{A} Secure Two-Party Computation System",
+  booktitle =    SECURITY,
+  month =        aug,
+  year =         2004,
+}
+
+@InProceedings{parno13pinocchio,
+  author =       "Bryan Parno and
+                  Jon Howell and
+                  Craig Gentry and
+                  Mariana Raykova",
+  title =        "Pinocchio: Nearly Practical Verifiable Computation",
+  booktitle =    OAKLAND,
+  month =        may,
+  year =         2013,
+}
+
+@InProceedings{henecka10tasty,
+  author =       "Wilko Henecka and
+                  Stefan K{\"o}gl and
+                  Ahmad-Reza Sadeghi and
+                  Thomas Schneider and
+                  Immo Wehrenberg",
+  title =        "{TASTY}: tool for automating secure two-party computations",
+  booktitle =    CCS,
+  month =        oct,
+  year =         2010,
+}
+
+@InProceedings{holzer12secure,
+  author =       "Andreas Holzer and
+                  Martin Franz and
+                  Stefan Katzenbeisser and
+                  Helmut Veith",
+  title =        "Secure two-party computations in {ANSI} {C}",
+  booktitle =    CCS,
+  month =        oct,
+  year =         2012,
+}
+
+@InProceedings{setty12taking,
+  author =       "Srinath T. V. Setty and
+                  Victor Vu and
+                  Nikhil Panpalia and
+                  Benjamin Braun and
+                  Andrew J. Blumberg and
+                  Michael Walfish",
+  title =        "Taking Proof-Based Verified Computation a Few Steps Closer to Practicality",
+  booktitle =    SECURITY,
+  month =        aug,
+  year =         2012,
+  note =         {Extended version: \url{https://ia.cr/2012/598}},
+}
+
+@InProceedings{setty13resolving,
+  author =       "Srinath Setty and
+                  Benjamin Braun and
+                  Victor Vu and
+                  Andrew J. Blumberg and
+                  Bryan Parno and
+                  Michael Walfish",
+  title =        "Resolving the conflict between generality and plausibility in verified computation",
+  booktitle =    {EuroSys},
+  month =        apr,
+  year =         2013,
+}
+
+@misc{thaler20proofs,
+   author = {Justin Thaler},
+   title = {Proofs, arguments, and zero-knowledge},
+   howpublished = {\url{http://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf}},
+   xyear = 2020,
+}
+
+@inproceedings{cormode12practical,
+    author = "Graham Cormode and Michael Mitzenmacher and Justin Thaler",
+    title = "Practical Verified Computation with Streaming Interactive Proofs",
+    booktitle = {ITCS},
+    year = 2012,
+    month = jan,
+}
+
+@inproceedings{bensasson14scalable,
+    author = "E. Ben-Sasson and A. Chiesa and E. Tromer and M. Virza",
+    title = "Scalable Zero Knowledge via Cycles of Elliptic Curves",
+    booktitle = {CRYPTO},
+    month = aug,
+    year = 2014,
+}
+
+@InProceedings{fredrikson14z0,
+  author =       "Matthew Fredrikson and
+                  Benjamin Livshits",
+  title =        "Z{\O}: An Optimizing Distributing Zero-Knowledge Compiler",
+  booktitle =    SECURITY,
+  month =        aug,
+  year =         2014,
+}
+
+@inproceedings{daoud14survey,
+  author = {Luka Daoud and Dawid Zydek and Henry Selvaraj},
+  title = {A Survey of High Level Synthesis Languages, Tools, and Compilers for Reconfigurable High Performance Computing},
+  booktitle = {ICSS},
+  year = 2013,
+  month = apr,
+}
+
+@misc{mlir,
+  title = {{MLIR}: Multi-Level {IR} Compiler Framework},
+  howpublished = {\url{https://mlir.llvm.org/}},
+  key = {mlir},
+}
+
+@misc{lattner2020mlir,
+  author    = {Chris Lattner and
+               Jacques A. Pienaar and
+               Mehdi Amini and
+               Uday Bondhugula and
+               River Riddle and
+               Albert Cohen and
+               Tatiana Shpeisman and
+               Andy Davis and
+               Nicolas Vasilache and
+               Oleksandr Zinenko},
+  title     = {{MLIR:} {A} Compiler Infrastructure for the End of {Moore's} Law},
+  xjournal   = {CoRR},
+  xvolume    = {abs/2002.11054},
+  xyear      = {2020},
+  howpublished = {https://arxiv.org/abs/2002.11054},
+  key="lattner2020mlir",
+  xarchivePrefix = {arXiv},
+  xeprint    = {2002.11054},
+  timestamp = {Tue, 03 Mar 2020 14:32:13 +0100},
+  biburl    = {https://dblp.org/rec/journals/corr/abs-2002-11054.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+
+@misc{pequin,
+  title = {Pequin: A system for verifying outsourced computations and applying {SNARKs}},
+  howpublished = {\url{https://github.com/pepper-project/pequin}},
+  key = {pequin},
+}
+@inproceedings{bootle2018arya,
+  title={Arya: Nearly linear-time zero-knowledge proofs for correct program execution},
+  author={Bootle, Jonathan and Cerulli, Andrea and Groth, Jens and Jakobsen, Sune and Maller, Mary},
+  xbooktitle={International Conference on the Theory and Application of Cryptology and Information Security},
+  booktitle = {ASIACRYPT},
+  xpages={595--626},
+  year={2018},
+  xorganization={Springer}
+}
+@inproceedings{becker2019axiom,
+  title={The {Axiom Profiler}: Understanding and debugging {SMT} quantifier instantiations},
+  author={Becker, Nils and M{\"u}ller, Peter and Summers, Alexander J},
+  xbooktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
+  booktitle = {TACAS},
+  xpages={99--116},
+  year={2019},
+  xorganization={Springer}
+}
+@inproceedings{yao1982protocols,
+  title={Protocols for secure computations},
+  author={Yao, Andrew C},
+  xbooktitle={23rd annual symposium on foundations of computer science (sfcs 1982)},
+  booktitle = {FOCS},
+  xpages={160--164},
+  year={1982},
+  xorganization={IEEE}
+}
+
+@inproceedings{beaver1991efficient,
+  title={Efficient multiparty protocols using circuit randomization},
+  author={Beaver, Donald},
+  xbooktitle={Annual International Cryptology Conference},
+  booktitle = CRYPTO,
+  xpages={420--432},
+  year={1991},
+  xorganization={Springer}
+}
+@inproceedings{damgaard2012multiparty,
+  title={Multiparty computation from somewhat homomorphic encryption},
+  author={Damg{\aa}rd, Ivan and Pastro, Valerio and Smart, Nigel and Zakarias, Sarah},
+  booktitle={Annual Cryptology Conference},
+  xpages={643--662},
+  year={2012},
+  xorganization={Springer}
+}
+@inproceedings{damgaard2013practical,
+  title={Practical covertly secure MPC for dishonest majority--or: breaking the SPDZ limits},
+  author={Damg{\aa}rd, Ivan and Keller, Marcel and Larraia, Enrique and Pastro, Valerio and Scholl, Peter and Smart, Nigel P},
+  xbooktitle={European Symposium on Research in Computer Security},
+  booktitle = {ESORICS},
+  xpages={1--18},
+  year={2013},
+  xorganization={Springer}
+}
+
+@inproceedings{wahby17full,
+  author = {Riad S. Wahby and Ye Ji and Andrew J. Blumberg and {a.} shelat and Justin Thaler and Michael Walfish and Thomas Wies},
+  title = {Full accounting for verifiable outsourcing},
+  booktitle = CCS,
+  xmonth = oct,
+  year = 2017,
+  xnote = "Full version: \url{https://eprint.iacr.org/2017/242/}",
+}
+
+@inproceedings{wahby16verifiable,
+  author = {Riad S. Wahby and Max Howald and Siddharth Garg and {a.} {s}helat and Michael Walfish},
+  title = {Verifiable {ASICs}},
+  booktitle = OAKLAND,
+  year = 2016,
+  xmonth = may,
+}
+
+@inproceedings{cordeiro2011smt,
+  title={{SMT}-based bounded model checking for embedded {ANSI-C} software},
+  author={Cordeiro, Lucas and Fischer, Bernd and Marques-Silva, Joao},
+  booktitle={ASE},
+  year={2009},
+}
+
+@inproceedings{kroening2014cbmc,
+  title={{CBMC}--{C} bounded model checker},
+  author={Kroening, Daniel and Tautschnig, Michael},
+  booktitle={TACAS},
+  year={2014},
+}	    
+
+@inproceedings{cuoq2012frama,
+  title={Frama-{C}},
+  author={Cuoq, Pascal and Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
+  xbooktitle={International conference on software engineering and formal methods},
+  booktitle = {SEFM},
+  year={2012},
+}
+@inproceedings{kirchner2015frama,
+  title={Frama-{C}: A software analysis perspective},
+  author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
+  booktitle={FAC},
+  year={2015},
+}
+
+@article{ball2011decade,
+  title={A decade of software model checking with {SLAM}},
+  author={Ball, Thomas and Levin, Vladimir and Rajamani, Sriram K},
+  journal={CACM},
+  volume={54},
+  number={7},
+  pages={68--76},
+  year={2011},
+  month=jul,
+}
+
+
+@inproceedings{ball2010static,
+  title={The {Static Driver Verifier} research platform},
+  author={Ball, Thomas and Bounimova, Ella and Levin, Vladimir and Kumar, Rahul and Lichtenberg, Jakob},
+  booktitle=CAV, 
+  year={2010},
+}
+
+@incollection{leino2009verification,
+  title={Verification of concurrent programs with {Chalice}},
+  author={Leino, K. Rustan M. and M{\"u}ller, Peter and Smans, Jan},
+  xbooktitle={Foundations of Security Analysis and Design V},
+  booktitle = {FOSAD},
+  year={2009},
+}
+
+@inproceedings{jacobs2011verifast,
+  title={{VeriFast: A powerful, sound, predictable, fast verifier for C and Java}},
+  author={Jacobs, Bart and Smans, Jan and Philippaerts, Pieter and Vogels, Fr{\'e}d{\'e}ric and Penninckx, Willem and Piessens, Frank},
+  booktitle={NASA Formal Methods Symposium},
+  year={2011},
+}
+@techreport{jacobs2008verifast,
+  title={The {VeriFast} program verifier},
+  author={Jacobs, Bart and Piessens, Frank},
+  xjournal={CW Reports},
+  xhowpublished={\url{https://lirias.kuleuven.be/1652504?limo=0}},
+  xkey="jacobs2008verifast",
+  year={2008},
+  month = aug,
+  number = {CW-520},
+  institution = {Dept. of Computer Science, KU Leuven},
+  xpublisher={Department of Computer Science, KU Leuven; Leuven, Belgium}
+}
+
+@inproceedings{vazou2014refinement,
+  title={Refinement types for Haskell},
+  author={Vazou, Niki and Seidel, Eric L and Jhala, Ranjit and Vytiniotis, Dimitrios and Peyton-Jones, Simon},
+  booktitle={ICFP}, 
+  year={2014}
+}
+
+@inproceedings{swamy2016dependent,
+  title={Dependent types and multi-monadic effects in {F}{$^\star$}},
+  author={Swamy, Nikhil and Hri{\c{t}}cu, C{\u{a}}t{\u{a}}lin and Keller, Chantal and Rastogi, Aseem and Delignat-Lavaud, Antoine and Forest, Simon and Bhargavan, Karthikeyan and Fournet, C{\'e}dric and Strub, Pierre-Yves and Kohlweiss, Markulf and Zinzindohoue, Jean-Karim and Zanella-B{\'e}guelin, Santiago},
+  booktitle=POPL,
+  year={2016}
+}
+
+@inproceedings{nelson2019scaling,
+  title={Scaling symbolic evaluation for automated verification of systems code with {Serval}},
+  author={Nelson, Luke and Bornholt, James and Gu, Ronghui and Baumann, Andrew and Torlak, Emina and Wang, Xi},
+  booktitle=SOSP,
+  year={2019}
+}
+
+@misc{nehai2019deductive,
+  title={Deductive proof of {Ethereum} smart contracts using {Why3}},
+  author={Nehai, Zeinab and Bobot, Fran{\c{c}}ois},
+  howpublished={arXiv:1904.11281},
+  year={2019},
+  key="nehai2019deductive",
+}
+
+@inproceedings{baranowski2018verifying,
+  title={Verifying {Rust} programs with {SMACK}},
+  author={Baranowski, Marek and He, Shaobo and Rakamari{\'c}, Zvonimir},
+  booktitle={ATVA},
+  year={2018},
+}	    
+
+@inproceedings{hajdu2019solc,
+  title={solc-verify: A modular verifier for {Solidity} smart contracts},
+  author={Hajdu, {\'A}kos and Jovanovi{\'c}, Dejan},
+  xbooktitle={Working Conference on Verified Software: Theories, Tools, and Experiments},
+  booktitle = {VSTTE},
+  year={2019},
+}
+
+@inproceedings{cordeiro2018jbmc,
+  title={{JBMC}: A bounded model checking tool for verifying {Java} bytecode},
+  author={Cordeiro, Lucas and Kesseli, Pascal and Kroening, Daniel and Schrammel, Peter and Trtik, Marek},
+  booktitle=CAV, 
+  year={2018},
+}
+
+@inproceedings{ckl2004,
+  AUTHOR    = { Clarke, Edmund and Kroening, Daniel and Lerda, Flavio },
+  TITLE     = { A Tool for Checking {ANSI-C} Programs },
+  BOOKTITLE = { TACAS }, 
+  YEAR      = { 2004 },
+}
+
+@inproceedings{KoeksalETAL12ConstraintsControl,
+  author = {{Ali Sinan} K\"oksal and Viktor Kuncak and Philippe Suter},
+  title = {Constraints as Control},
+  booktitle = POPL,
+  year=2012,
+}
+
+@inproceedings{uhler2014smten,
+  title={Smten with satisfiability-based search},
+  author={Uhler, Richard and Dave, Nirav},
+  booktitle={OOPSLA},
+  year={2014},
+}
+
+@misc{mouraz3py,
+  title={{Z3Py guide: Z3 API in Python}},
+  author={Moura, L},
+  key={z3pyapi},
+  howpublished={\url{https://ericpony.github.io/z3py-tutorial/guide-examples.htm}}
+}
+
+@misc{haskellz3,
+  title={Haskell {Z3} Bindings},
+  author={Iago Abal},
+  key={haskellz3},
+  howpublished={\url{https://github.com/PLSysSec/haskell-z3}}
+}
+
+@misc{erkok2019sbv,
+  title={{SBV}: {SMT} based verification in {Haskell}},
+  author={Erk{\"o}k, L},
+  howpublished={\url{https://hackage.haskell.org/package/sbv}},
+  xyear={2019}
+}
+
+@misc{zkproofref,
+  title = {{ZKProof} Community Reference},
+  xyear = 2020,
+  key = {zkproof},
+  howpublished = {\url{https://docs.zkproof.org/reference.pdf}},
+}
+
+@misc{lindell20mpc,
+  title = {Secure Multiparty Computation ({MPC})},
+  xyear = 2020,
+  author = {Yehuda Lindell},
+  howpublished = {\url{https://eprint.iacr.org/2020/300}},
+  note = {To appear in \textit{CACM}},
+}
+
+@book{arora09computational,
+ author = {Sanjeev Arora and Boaz Barak},
+ title = {Computational Complexity: A Modern Approach},
+ year = {2009},
+ xisbn = {978-0-521-42426-4},
+ xedition = {1st},
+ publisher = {Cambridge University Press},
+ address = {Cambridge, UK},
+}
+
+@misc{vaas13paypal,
+  title = {{PayPal} refuses to pay bug-finding teen},
+  author = {Lisa Vaas},
+  xyear = 2013,
+  key = {paypal},
+  howpublished = {\url{https://nakedsecurity.sophos.com/2013/05/29/paypal-refuses-to-pay-bug-finding-teen/}},
+}
+
+@misc{arghire16researchers,
+  title = {Researchers Claim {Wickr} Patched Flaws but Didn't Pay Rewards},
+  author = {Ionut Arghire},
+  key = {wickr},
+  xyear = 2016,
+  howpublished = {\url{https://www.securityweek.com/researchers-claim-wickr-patched-flaws-didnt-pay-rewards}},
+}
+
+@misc{baron19securing,
+  title = {Securing Information for Encrypted Verification and Evaluation},
+  note = {DARPA SIEVE Program Proposers Day Slides},
+  howpublished = {\url{https://web.archive.org/web/20200221151433/https://www.darpa.mil/attachments/SIEVEProposersDaySlidesv4.pdf}},
+  year = 2019,
+  key={securing},
+  author = {Joshua Baron},
+}
+
+@misc{darpa21researchers,
+  title = {Researchers Demonstrate Potential for Zero-Knowledge Proofs in Vulnerability Disclosure},
+  note = {DARPA Press Release},
+  howpublished = {\url{https://www.darpa.mil/news-events/2021-04-22}},
+  year = 2021,
+  key = {researchers},
+}
+
+@article{baldoni2018survey,
+  title={A survey of symbolic execution techniques},
+  author={Baldoni, Roberto and Coppa, Emilio and D’elia, Daniele Cono and Demetrescu, Camil and Finocchi, Irene},
+  journal={ACM Computing Surveys},
+  volume={51},
+  number={3},
+  pages={1--39},
+  year={2018},
+  xpublisher={ACM New York, NY, USA}
+}
+
+@article{cadar2013symbolic,
+  title={Symbolic execution for software testing: Three decades later},
+  author={Cadar, Cristian and Sen, Koushik},
+  xjournal={Communications of the ACM},
+  journal = CACM,
+  volume={56},
+  number={2},
+  pages={82--90},
+  year={2013},
+  xpublisher={ACM New York, NY, USA}
+}
+
+
+@book{fourer02ampl,
+  title = {{AMPL}: A Modeling Language for Mathematical Programming},
+  author = {Robert Fourer and David M. Gay and Brian W. Kernighan},
+  year = 2002,
+  publisher = {Cengage Learning},
+  address = {Boston, MA, USA},
+  edition = {2nd},
+}
+
+@inproceedings{lattner04llvm,
+  title = {{LLVM}: A compilation framework for lifelong program analysis and transformation},
+  author = {Chris Lattner and Vikram Adve},
+  year = 2004,
+  booktitle = {CGO},
+  xmonth = mar,
+}
+
+@article{hall96maximizing,
+  title = {Maximizing multiprocessor performance with the {SUIF} compiler},
+  author = {M. W. Hall and J. M. Anderson and S. P. Amarasinghe and B. R. Murphy and S.-W. Liao and E. Bugnion and M. S. Lam},
+  year = 1996,
+  journal = {{IEEE} {C}omputer},
+}
+
+@InProceedings{danezis2013pinocchio,
+    author = {Danezis, George and Fournet, Cédric and Kohlweiss, Markulf and Parno, Bryan},
+    title = {Pinocchio Coin: Building {Zerocoin} from a Succinct Pairing-based Proof System},
+    xbooktitle = {Workshop on Language Support for Privacy Enhancing Technologies},
+    booktitle = {{PETShop}},
+    year = {2013},
+    xmonth = nov,
+}
+
+@inproceedings{zhang17vsql,
+  author = {Yupeng Zhang and Daniel Genkin and Jonathan Katz and Dimitris Papadopoulos and Charalampos Papamanthou},
+  title = {{vSQL}: Verifying Arbitrary {SQL} Queries over Dynamic Outsourced Databases},
+  booktitle = OAKLAND,
+  year = 2017,
+  xmonth = may,
+}
+
+@InProceedings{STOC:GolMicWig87,
+  author =       "Oded Goldreich and
+                  Silvio Micali and
+                  Avi Wigderson",
+  title =        "How to Play any Mental Game or {A} Completeness Theorem for Protocols with Honest Majority",
+  booktitle =    {STOC},
+  xmonth =        may,
+  year =         1987,
+}
+
+@InProceedings{STOC:BenGolWig88,
+  author =       "Michael {Ben-Or} and
+                  Shafi Goldwasser and
+                  Avi Wigderson",
+  title =        "Completeness Theorems for Non-Cryptographic Fault-Tolerant Distributed Computation (Extended Abstract)",
+  booktitle =    {STOC},
+  xmonth =        may,
+  year =         1988,
+}
+
+@InProceedings{STOC:IKOS07,
+  author =       "Yuval Ishai and
+                  Eyal Kushilevitz and
+                  Rafail Ostrovsky and
+                  Amit Sahai",
+  title =        "Zero-knowledge from secure multiparty computation",
+  booktitle =    {STOC},
+  xmonth =        jun,
+  year =         2007,
+}
+
+@inproceedings{vu13hybrid,
+    author = "Victor Vu and Srinath Setty and Andrew J. Blumberg and Michael Walfish",
+    title = "A Hybrid Architecture for Interactive Verifiable Computation",
+    booktitle = OAKLAND,
+    year = 2013,
+    xmonth = may,
+    xpages = {223-237},
+}
+
+@article{pagnia03fair,
+  title = {Fair exchange},
+  author = {Henning Pagnia and Holger Vogt and Felix C. G\"{a}rtner},
+  journal = {The Computer Journal},
+  volume = 46,
+  number = 1,
+  month = jan,
+  year = 2003,
+  pages = {55--75},
+}
+
+
+@misc{ffloc,
+  title = {Engineering code quality in the {Firefox} browser: a look at our tools and challenges},
+  author = {Bastien Abadie and Sylvestre Ledru},
+  howpublished={\url{https://hacks.mozilla.org/2020/04/code-quality-tools-at-mozilla/}},
+  month=april,
+  year={2020}
+}
+
+@misc{ffbounty,
+  title = {Security Bug Bounty Program},
+  author = {Mozilla},
+  howpublished={\url{https://www.mozilla.org/en-US/security/bug-bounty/}}
+}
+
+@inproceedings{blum91checking,
+  author =       "Manuel Blum and
+                  William S. Evans and
+                  Peter Gemmell and
+                  Sampath Kannan and
+                  Moni Naor",
+  title =        "Checking the Correctness of Memories",
+  booktitle =    {FOCS},
+  xmonth =        oct,
+  year =         1991,
+}
+
+@misc{bugbountysuccess,
+  title = {Google’s bug bounty program just had a record-breaking year of payouts},
+  author = {Daphne Leprince-Ringuet},
+  howpublished={\url{https://www.zdnet.com/article/googles-bug-bounty-program-just-had-a-record-breaking-year-of-payouts}},
+  month=jan,
+  year={2020}
+}
+
+@inproceedings{wang2017partitioned,
+  title={Partitioned memory models for program analysis},
+  author={Wei Wang and Clark Barrett and Thomas Wies},
+  booktitle={VMCAI},
+  year={2017},
+}
+
+@article{burstall1972some,
+  title={Some techniques for proving correctness of programs which alter data structures},
+  author={Burstall, Rodney M},
+  journal={Machine intelligence},
+  volume={7},
+  number={23-50},
+  pages={3},
+  year=1972,
+}
+
+@misc{braun12compiling,
+    author = "Benjamin Braun",
+    title = "Compiling computations to constraints for verified computation",
+    year = 2012,
+    month = dec,
+   howpublished = "UT Austin Honors Thesis HR-12-10"
+}
+
+@inproceedings{swamy2013verifying,
+  title={Verifying higher-order programs with the {Dijkstra} monad},
+  author={Swamy, Nikhil and Weinberger, Joel and Schlesinger, Cole and Chen, Juan and Livshits, Benjamin},
+  booktitle={PLDI},
+  year={2013},
+}
+
+@inproceedings{muller2016viper,
+  title={Viper: A verification infrastructure for permission-based reasoning},
+  author={M{\"u}ller, Peter and Schwerhoff, Malte and Summers, Alexander J},
+  booktitle={VMCAI},
+  year={2016},
+}
+
+@inproceedings{filliatre2006type,
+  title={Type-safe modular hash-consing},
+  author={Filli{\^a}tre, Jean-Christophe and Conchon, Sylvain},
+  booktitle={ML},
+  xpages={12--19},
+  year={2006}
+}
+@article{ershov1958programming,
+  title={On programming of arithmetic operations},
+  author={Ershov, Andrei P.},
+  journal={CACM},
+  volume={1},
+  number={8},
+  pages={3--6},
+  year={1958},
+}
+
+@book{hart2017pyomo,
+  title={Pyomo-optimization modeling in {Python}},
+  author={Hart, William E and Laird, Carl D and Watson, Jean-Paul and Woodruff, David L and Hackebeil, Gabriel A and Nicholson, Bethany L and Siirola, John D},
+  volume={67},
+  year={2017},
+  publisher={Springer}
+}
+@incollection{forrest2005cbc,
+  title={{CBC} user guide},
+  author={Forrest, John and Lougee-Heimer, Robin},
+  booktitle={Emerging theory, methods, and applications},
+  pages={257--277},
+  year={2005},
+}
+@misc{gurobi,
+  title={Gurobi},
+  howpublished={\url{https://www.gurobi.com/}}
+}
+@misc{gocomp,
+  title={Grid Optimization Competition},
+  howpublished={\url{https://gocompetition.energy.gov/}},
+  accessed={19 October 2021},
+  author={ARPA-E}
+}
+@misc{kaggle,
+  title={Compeitions},
+  howpublished={\url{https://www.kaggle.com/docs/competitions}},
+  accessed={19 October 2021},
+  author={Kaggle}
+}
+@inproceedings{brinkmann2002rtl,
+  title={{RTL}-datapath verification using integer linear programming},
+  author={Brinkmann, Raik and Drechsler, Rolf},
+  booktitle={{ASP-DAC/VLSI}},
+  xpages={741--746},
+  year={2002},
+  xorganization={IEEE}
+}
+@inproceedings{zeng2001lpsat,
+  title={{LPSAT}: A unified approach to {RTL} satisfiability},
+  author={Zeng, Zhihong and Kalla, Priyank and Ciesielski, Maciej},
+  booktitle={DATE}, 
+  year={2001},
+}
+@book{aho1986compilers,
+  title={Compilers, principles, techniques},
+  author={Aho, Alfred V and Sethi, Ravi and Ullman, Jeffrey D},
+  publisher={Addison Wesley},
+  year={1986}
+}
+@inproceedings{heath2021textsf,
+  title={Stacked Garbling with {O}(b log b) Computation},
+  author={Heath, David and Kolesnikov, Vladimir},
+  booktitle=EUROCRYPT,
+  year={2021},
+  xorganization={Springer}
+}
+@article{heath2020stacked_zk,
+  title={Stacked Garbling for Disjunctive Zero-Knowledge Proofs.},
+  author={Heath, David and Kolesnikov, Vladimir},
+  journal=EUROCRYPT,
+  year={2020}
+}
+@inproceedings{heath2020stacked,
+  title={Stacked Garbling},
+  author={Heath, David and Kolesnikov, Vladimir},
+  booktitle=CRYPTO,
+  year={2020},
+  xorganization={Springer}
+}
+@inproceedings{heath2021zero,
+  title={Zero knowledge for everything and everyone: Fast {ZK} processor with cached {ORAM} for {ANSI C} programs},
+  author={Heath, David and Yang, Yibin and Devecsery, David and Kolesnikov, Vladimir},
+  booktitle=OAKLAND,
+  xpages={1538--1556},
+  year={2021},
+  xorganization={IEEE}
+}
+
+@inproceedings{baum2021mathsf,
+  title={Mac'n'Cheese: Zero-Knowledge Proofs for Boolean and Arithmetic Circuits with Nested Disjunctions},
+  author={Baum, Carsten and Malozemoff, Alex J and Rosen, Marc B and Scholl, Peter},
+  booktitle=CRYPTO,
+  year={2021},
+  xorganization={Springer}
+}
+
+@inproceedings{zhang13picco,
+  title={{PICCO}: A general-purpose compiler for private distributed computation},
+  author={Yihua Zhang and Aaron Steele and Marina Blanton},
+  year=2013,
+  month=nov,
+  booktitle=CCS,
+}
+@inproceedings{viaduct,
+author = {Acay, Co\c{s}ku and Recto, Rolph and Gancher, Joshua and Myers, Andrew C. and Shi, Elaine},
+title = {Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs},
+year = {2021},
+booktitle = {PLDI},
+xisbn = {9781450383912},
+xpublisher = {Association for Computing Machinery},
+xaddress = {New York, NY, USA},
+xurl = {https://doi.org/10.1145/3453483.3454074},
+xdoi = {10.1145/3453483.3454074},
+xabstract = {Modern distributed systems involve interactions between principals with limited trust, so cryptographic mechanisms are needed to protect confidentiality and integrity. At the same time, most developers lack the training to securely employ cryptography. We present Viaduct, a compiler that transforms high-level programs into secure, efficient distributed realizations. Viaduct's source language allows developers to declaratively specify security policies by annotating their programs with information flow labels. The compiler uses these labels to synthesize distributed programs that use cryptography efficiently while still defending the source-level security policy. The Viaduct approach is general, and can be easily extended with new security mechanisms.  Our implementation of the Viaduct compiler comes with an extensible runtime system that includes plug-in support for multiparty computation, commitments, and zero-knowledge proofs. We have evaluated the system on a set of benchmarks, and the results indicate that our approach is feasible and can use cryptography in efficient, nontrivial ways.},
+xbooktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
+xpages = {740–755},
+xnumpages = {16},
+xkeywords = {multiparty computation, zero knowledge, information flow},
+xlocation = {Virtual, Canada},
+xseries = {PLDI 2021}
+}
+@misc{zcash,
+  title={Zcash protocol specification},
+  author={Hopwood, Daira and Bowe, Sean and Hornby, Taylor and Wilcox, Nathan},
+  year={2016},
+  howpublished={\url{https://zips.z.cash/protocol/protocol.pdf}}
+}
+@misc{zcash_sapling,
+  title={Zcash {Sapling} circuit library},
+  year={2018},
+  howpublished={\url{https://github.com/zcash-hackworks/sapling-crypto}}
+}
+@inproceedings{vaikuntanathan11computing,
+  author = {Vinod Vaikuntanathan},
+  title = {Computing Blindfolded: New Developments in Fully Homomorphic Encryption},
+  booktitle = {FOCS},
+  year = {2011},
+  month = oct,
+}
+@misc{sapling_pedersen_hash,
+  title = {{pedersen\_hash.rs}},
+  year = {2018},
+  howpublished = {\url{https://github.com/zcash-hackworks/sapling-crypto/blob/49017b4e055ba4322dad1f03fe7d80dc0ed449cc/src/circuit/pedersen_hash.rs}},
+}
+@misc{circ,
+  author = {Alex Ozdemir and Fraser Brown and Riad S. Wahby},
+  title = {{CirC}: Compiler infrastructure for proof systems, software verification, and more},
+  booktitle = OAKLAND,
+  year =2022,
+}
+@misc{circFull,
+  author = {Alex Ozdemir and Fraser Brown and Riad S. Wahby},
+  title = {{CirC}: Compiler infrastructure for proof systems, software verification, and more},
+  howpublished = {\url{https://eprint.iacr.org/2020/1586}},
+  note = {Extended version},
+}
+
+@inproceedings{eberhardt18zokrates,
+  author = {Jacob Eberhardt and Stefan Tai},
+  title = {{ZoKrates}---Scalable Privacy-Preserving Off-Chain Computations},
+  booktitle = {IEEE Blockchain},
+  year = 2018,
+  month = jul,
+}
+
+@misc{zkunsat,
+  author = {Ning Luo and Timos Antonopoulos and William Harris and Ruzica Piskac and Eran Tromer and Xiao Wang},
+  title = {Proving UNSAT in Zero Knowledge},
+  year = {2022},
+  note = {To appear in \textit{ACM CCS}},
+  howpublished = {\url{https://eprint.iacr.org/2022/206}}
+}
+
+@misc{ppSAT,
+  author = {Ning Luo and Samuel Judson and Timos Antonopoulos and Ruzica Piskac and Xiao Wang},
+  title = {ppSAT: Towards Two-Party Private SAT Solving},
+  year = {2022},
+  howpublished = {\url{https://eprint.iacr.org/2021/1584}},
+  note = {To appear in \textit{USENIX Security}},
+  xend = {}
+}
+
+@inproceedings{judson2020privacy,
+  title={Privacy Preserving CTL Model Checking through Oblivious Graph Algorithms},
+  author={Judson, Samuel and Luo, Ning and Antonopoulos, Timos and Piskac, Ruzica},
+  xbooktitle={Proceedings of the 19th Workshop on Privacy in the Electronic Society},
+  booktitle={{WPES}},
+  xpages={101--115},
+  year={2020}
+}
+
+@inproceedings{fang2021zero,
+  title={Zero Knowledge Static Program Analysis},
+  author={Fang, Zhiyong and Darais, David and Near, Joseph P and Zhang, Yupeng},
+  booktitle=CCS,
+  xpages={2951--2967},
+  year={2021}
+}
+@article{walfish15verifying,
+    author = "Michael Walfish and Andrew J. Blumberg",
+    title = "Verifying computations without reexecuting them: from
+        theoretical possibility to near practicality",
+    year = 2015,
+    month = feb,
+    journal = CACM,
+}
+@misc{emptoolkit,
+  author = {Xiao Wang and Alex J. Malozemoff and Jonathan Katz},
+  title = {EMP-toolkit: Efficient Multi Party computation toolkit},
+  note = {\url{https://github.com/emp-toolkit}},
+}
+@inproceedings{thaler12verifiable,
+    author = "Justin Thaler and Mike Roberts and Michael Mitzenmacher and Hanspeter
+	Pfister",
+    title = "Verifiable Computation with Massively Parallel Interactive
+	Proofs",
+    booktitle = {{HotCloud}},
+    year = 2012,
+    xmonth = jun,
+    xnote =  "Full paper at \url{http://arxiv.org/abs/1202.1350}, Feb.  2012.",
+}
+@book{bonehshoup,
+  title={A graduate course in applied cryptography},
+  author={Boneh, Dan and Shoup, Victor},
+  note={Draft 0.6},
+  year={2021}
+}
+
+@article{waksman1968permutation,
+  title={A permutation network},
+  author={Waksman, Abraham},
+  journal={JACM},
+  volume={15},
+  number={1},
+  xpages={159--163},
+  year={1968},
+  xpublisher={ACM New York, NY, USA}
+}
+@article{howard1980formulae,
+  title={The formulae-as-types notion of construction},
+  author={Howard, William A},
+  journal={To HB Curry: essays on combinatory logic, lambda calculus and formalism},
+  volume={44},
+  pages={479--490},
+  year={1980}
+}
+@book{bertot2013interactive,
+  title={Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions},
+  author={Bertot, Yves and Cast{\'e}ran, Pierre},
+  year={2013},
+  publisher={Springer}
+}
+@inproceedings{moura2015lean,
+  title={The Lean theorem prover (system description)},
+  author={Moura, Leonardo de and Kong, Soonho and Avigad, Jeremy and Doorn, Floris van and Raumer, Jakob von},
+  booktitle={International Conference on Automated Deduction},
+  pages={378--388},
+  year={2015},
+  organization={Springer}
+}
+
+@book{nipkow2002isabelle,
+  title={Isabelle/HOL: a proof assistant for higher-order logic},
+  author={Nipkow, Tobias and Wenzel, Markus and Paulson, Lawrence C},
+  year={2002},
+  publisher={Springer}
+}
+
+@book{kaufmann2013computer,
+  title={Computer-aided reasoning: ACL2 case studies},
+  author={Kaufmann, Matt and Manolios, Panagiotis and Moore, J Strother},
+  volume={4},
+  year={2013},
+  xpublisher={Springer Science \& Business Media}
+}
+
+@misc{zkexploit,
+      author = {Matthew Green and Mathias Hall-Andersen and Eric Hennenfent and Gabriel Kaptchuk and Benjamin Perez and Gijs Van Laer},
+      title = {Efficient Proofs of Software Exploitability for Real-world Processors},
+      xhowpublished = {Cryptology ePrint Archive, Paper 2022/1223},
+      year = {2022},
+      note = {\url{https://eprint.iacr.org/2022/1223}},
+      xurl = {https://eprint.iacr.org/2022/1223}
+}
+@incollection{blum2019non,
+  booktitle={Providing Sound Foundations for Cryptography: On the Work of Shafi Goldwasser and Silvio Micali},
+  pages={329--349},
+  year={2019}
+}
+@inproceedings{heath2021zero,
+  title={Zero knowledge for everything and everyone: fast ZK processor with cached ORAM for ANSI C programs},
+  author={Heath, David and Yang, Yibin and Devecsery, David and Kolesnikov, Vladimir},
+  booktitle=OAKLAND,
+  year={2021},
+  xorganization={IEEE}
+}
+
+@article{wahby2015efficient,
+  title={Efficient RAM and control flow in verifiable outsourced computation},
+  author={Wahby, Riad S and Setty, Srinath and Howald, Max and Ren, Zuocheng and Blumberg, Andrew J and Walfish, Michael},
+  journal=NDSS,
+  year={2015}
+}
+@inproceedings{wetzler2014drat,
+  title={DRAT-trim: Efficient checking and trimming using expressive clausal proofs},
+  author={Wetzler, Nathan and Heule, Marijn JH and Hunt, Warren A},
+  booktitle={SAT},
+  xpages={422--429},
+  year={2014},
+  xorganization={Springer}
+}
+@inproceedings{pfenning1989inductively,
+  title={Inductively defined types in the Calculus of Constructions},
+  author={Pfenning, Frank and Paulin-Mohring, Christine},
+  booktitle={International Conference on Mathematical Foundations of Programming Semantics},
+  xpages={209--228},
+  year={1989},
+  xorganization={Springer}
+}
+
+@inproceedings{coquand1988inductively,
+author = {Coquand, Thierry and Paulin, Christine},
+title = {Inductively Defined Types},
+year = {1988},
+isbn = {3540523359},
+publisher = {Springer-Verlag},
+address = {Berlin, Heidelberg},
+booktitle = {Proceedings of the International Conference on Computer Logic},
+pages = {50–66},
+numpages = {17},
+series = {COLOG '88}
+}
+
+@inproceedings{mathlib2019,
+	doi = {10.1145/3372885.3373824},
+	url = {https://doi.org/10.1145%2F3372885.3373824},
+	year = 2020,
+	month = {jan},
+	publisher = {{ACM}
+    },
+	author = {{\relax The mathlib Community}},
+	title = {The lean mathematical library},
+	booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs}
+}
+@article{lfsc,
+  title={SMT proof checking using a logical framework},
+  author={Stump, Aaron and Oe, Duckki and Reynolds, Andrew and Hadarean, Liana and Tinelli, Cesare},
+  journal={Formal Methods in System Design},
+  xvolume={42},
+  xnumber={1},
+  xpages={91--118},
+  year={2013},
+  xpublisher={Springer}
+}
+
+@misc{mathlibgit,
+  author       = {{\relax The mathlib Community}},
+  title        = {mathlib},
+  howpublished = {\url{https://github.com/leanprover-community/mathlib}},
+  key          = {mathlib}
+}
+@misc{leangit,
+  author       = {{\relax The Lean Community}},
+  title        = {Lean},
+  howpublished = {\url{https://github.com/leanprover-community/lean}},
+  key          = {lean},
+  note         = {Version 3.43.0}
+}
diff --git a/doc/mem/sage/.gitignore b/doc/mem/sage/.gitignore
new file mode 100644
index 00000000..7c974cf2
--- /dev/null
+++ b/doc/mem/sage/.gitignore
@@ -0,0 +1 @@
+*.sage.py
diff --git a/doc/mem/sage/poly.sage b/doc/mem/sage/poly.sage
new file mode 100644
index 00000000..65886bfc
--- /dev/null
+++ b/doc/mem/sage/poly.sage
@@ -0,0 +1,31 @@
+P = PolynomialRing(GF(17), "X")
+X = P.gen(0)
+p = (X-1)*(X-3)*(X-7)*(X-10)
+p_prime = p.derivative()
+
+def poly_gcd_ext_int(x, y, x_c_a, x_c_b, y_c_a, y_c_b):
+    if x == 0:
+        lc = y.leading_coefficient()
+        return y/lc, y_c_a/lc, y_c_b/lc
+    # x = a * x_c_a + b * x_c_b
+    # y = a * y_c_a + b * y_c_b
+    if x.degree() > y.degree():
+        return poly_gcd_ext_int(y, x, y_c_a, y_c_b, x_c_a, x_c_b)
+    # y = qx + r    r = y - qx
+    q, r = y.quo_rem(x)
+    r_c_a = y_c_a - q*x_c_a
+    r_c_b = y_c_b - q*x_c_b
+    return poly_gcd_ext_int(r, x, r_c_a, r_c_b, x_c_a, x_c_b)
+    # (a, b) = (r, a)
+
+def poly_gcd_ext(x, y):
+    g, a, b = poly_gcd_ext_int(x, y, 1, 0, 0, 1)
+    assert g == x.gcd(y)
+    assert a * x + b * y == g
+    return g, a, b
+
+g, a, b = poly_gcd_ext(p, p_prime)
+print(g)
+print(a)
+print(b)
+print(a*p+b*p_prime)
diff --git a/doc/mem/sparse.tex b/doc/mem/sparse.tex
new file mode 100644
index 00000000..f3a55c43
--- /dev/null
+++ b/doc/mem/sparse.tex
@@ -0,0 +1,33 @@
+\section{Sparse Persistent}
+We want to use (nearly) the whole field
+as our index space, without cost.
+\begin{outline}
+  \1 What if you want $\vec a$ and $\vec b$ to be index-value pairs, where the
+  indices are from a large space (rather than $[N]$)?
+\1 params
+  \2 Now, $N$ becomes the capacity
+  \2 $C$ is the number of creations
+\1 Three operations:
+  \2 read
+  \2 conditional write
+  \2 create
+    \3 these happen *before* the reads/writes
+\1 approach
+  \2 use a dummy key value to indicate dead spots
+     \3 zero is a natural choice
+  \2 essentially, you inject creates into the initial store,
+     and filter out some dummies afterwards
+  \2 you just add a conditional uniqueness check
+    \3 uniqueness check: \csPerN{4}
+    \3 with a condition: \csPerN{2}
+    \3 computing the condition (field eq): \csPerN{2}
+  \2 base cost of the permutation: \csPerN{4}
+    \3 one from initial coefficient hash
+    \3 one from root hash
+    \3 one from root hash again
+    \3 one from coefficient hash again
+\1 accounting
+  \2 \csPerN{12}
+  \2 very similar dependence on $A$
+  \2 some dependence on $C$ too (like 10--30)
+\end{outline}
diff --git a/doc/mem/volatile.tex b/doc/mem/volatile.tex
new file mode 100644
index 00000000..579ec3d0
--- /dev/null
+++ b/doc/mem/volatile.tex
@@ -0,0 +1,86 @@
+\section{Volatile}
+\begin{outline}
+\1 initial definitions
+  \2 \FF: target field
+  \2 $N$: RAM size
+  \2 reads from uninit memory are undefined
+  \2 $R$: a witness relation $R(x, w)$ for a CC-SNARK
+    \3 $A$: number of RAM accesses
+      \4 each access is a conditional write
+\1 build the main transcript
+  \2 goal: define access-order and index-order transcripts, and ensure they're
+  permutations of one another
+  \2 entries: (value, idx, time, write?, active?) $(v, i, t, w, a)$
+    \3 write indicates read/write.
+    \3 active is a bit that is set for a write if it takes effect; otherwise, it has no effect. It is always set for reads.
+    \3 times are in $[A]$
+    \3 ROM case: entries are (value, idx)
+  \2 $\vec a$: time-order access sequence
+  \2 witness: $\vec b$: index-order access sequence
+  \2 challenge $\alpha$
+  \2 compute $\vec a'$: coefficient-hashes of time-order accesses with key
+  $\alpha$.
+    \3 Since time and write are fixed, \csPerA{2}.
+  \2 compute $\vec b'$: same for $\vec b$
+    \3 \csPerA{4}
+  \2 challenge $\beta$, use root-hash to do permutation argument
+    \3 \csPerA{2}
+\1 check the index-order transcript
+  \2 adjacent entries: $(v, i, t, w, a)$ and then $(v', i', t', w', a')$
+  \2 rules:
+    \3 (A) values can change only if indices do, or if $w'=1$
+    \3 (B) times increase, or indices change
+    \3 (C) first indices in index-constant blocks are unique
+  \2 witness sequence $\vec d$ that indicates index change
+    \3 defined by $d_0=1$ and $d'=1$ if $i \ne i'$, else $d'=0$
+    \3 cost: \csPerA{2}
+  \2 compute $\delta_t = (t'-t)(1-d')$. \csPerA{1}
+  \2 compute $v_p = d'(s-v) + v$. \csPerA{1}
+  \2 redef $v'$ to $v'$ if $a$, else $v$. \csPerA{1}
+  \2 $(v'-v_p)(1-w')=0$ \csPerA{1}
+  \2 range-check $\delta_t$s (next section)
+\1 uniqueness check
+  \2 define polynomial $p(X)$ by $\prod_j (w_j(X - i_j - 1) + 1)$
+  \2 it's derivative is $p'(X)$
+  \2 for an index-order transcript, $\gcd(p,p')=1$
+    \3 so there exist polynomials $f,g$ of degree at most $A-1$ such that $1 = pf + p'g$
+  \2 witness $\vec f$ of length $A$ is the coefficients of $f$
+  \2 witness $\vec g$ of length $A$ is the coefficients of $g$
+  \2 challenge $\gamma$ (same round as $\beta$)
+  \2 check $p(\gamma)f(\gamma) + p'(\gamma)g(\gamma)=1$
+  \2 eval $f(\gamma), g(\gamma)$: \csPerA{2} total
+  \2 eval $p(\gamma)$: \csPerA{2}
+    \3 one constraint for conditional
+    \3 one for product accumulation
+  \2 eval $p'(\gamma)$: \csPerA{2}
+    \3 as $p(\gamma)\sum_j\frac{p(\gamma)}{\gamma-i_j}$
+    \3 one constraint for inversion
+    \3 one constraint for conditional
+    \3 sum is free
+\1 range check
+  \2 concat $\delta_t$s and $[A]$
+  \2 sort (length $2A$)
+  \2 check const-or-plus-1 \csPerA{2}
+  \2 permutation check $(\beta)$ \csPerA{4}
+\1 accounting
+  \2 \csPerA{26}
+\1 ROM case
+  \2 assume $A$ reads, including at least one read to every index
+  \2 entries are (value, idx)
+  \2 permutation argument: \romCsPerA{4}
+  \2 checking the sorted transcript:
+    \3 adjacent entries $(i, v), (i', v')$
+    \3 logically:
+      \4 $i = i' \lor i + 1 = i'$
+      \4 $i = i' \implies v = v'$ ($i \ne i' \lor v = v'$)
+    \3 R1CS:
+      \4 $(i'-i)(i'-i-1)=0$
+      \4 $(i'-i)r(v'-v)=(v'-v)$
+      \4 \romCsPerA{3}
+    \3 some boundary conditions
+  \2 accounting: {\color{purple}{$7\cdot A$}}
+    \3 values of size $\ell$: {\color{purple}{$(5 + 2\ell)\cdot A$}}
+      \4 NB: to get this, process value equalities over value \textit{hashes}
+
+\end{outline}
+