\section{STARK framework}
\label{framework}


\subsection{Cost model}

Our zkEVM is designed for efficient verification by STARKs \cite{stark}, particularly by an AIR with degree 3 constraints. In this model, the prover bottleneck is typically constructing Merkle trees, particularly constructing the tree containing low-degree extensions of witness polynomials.


\subsection{Field selection}
\label{field}
Our zkEVM is designed to have its execution traces encoded in a particular prime field $\mathbb{F}_p$, with $p = 2^{64} - 2^{32} + 1$. A nice property of this field is that it can represent the results of many common \texttt{u32} operations. For example, (widening) \texttt{u32} multiplication has a maximum value of $(2^{32} - 1)^2$, which is less than $p$. In fact a \texttt{u32} multiply-add has a maximum value of $p - 1$, so the result can be represented with a single field element, although if we were to add a carry in bit, this no longer holds.

This field also enables a very efficient reduction method. Observe that
$$
2^{64} \equiv 2^{32} - 1 \pmod p
$$
and consequently
\begin{align*}
  2^{96} &\equiv 2^{32} (2^{32} - 1) \pmod p \\
         &\equiv 2^{64} - 2^{32} \pmod p \\
         &\equiv -1 \pmod p.
\end{align*}
To reduce a 128-bit number $n$, we first rewrite $n$ as $n_0 + 2^{64} n_1 + 2^{96} n_2$, where $n_0$ is 64 bits and $n_1, n_2$ are 32 bits each. Then
\begin{align*}
  n &\equiv n_0 + 2^{64} n_1 + 2^{96} n_2 \pmod p \\
  &\equiv n_0 + (2^{32} - 1) n_1 - n_2 \pmod p
\end{align*}
After computing $(2^{32} - 1) n_1$, which can be done with a shift and subtraction, we add the first two terms, subtracting $p$ if overflow occurs. We then subtract $n_2$, adding $p$ if underflow occurs.

At this point we have reduced $n$ to a \texttt{u64}. This partial reduction is adequate for most purposes, but if we needed the result in canonical form, we would perform a final conditional subtraction.


\subsection{Cross-table lookups}
\label{ctl}

TODO