Merge pull request #726 from mir-protocol/zkevm-spec

zkEVM spec

evm/spec/.gitignore

@@ -0,0 +1,7 @@
+## Files generated by pdflatex, bibtex, etc.
+*.aux
+*.log
+*.out
+*.toc
+*.bbl
+*.blg

evm/spec/Makefile

@@ -0,0 +1,20 @@
+DOCNAME=zkevm
+
+all: pdf
+
+.PHONY: clean
+
+quick:
+	pdflatex $(DOCNAME).tex
+
+pdf:
+	pdflatex $(DOCNAME).tex
+	bibtex $(DOCNAME).aux
+	pdflatex $(DOCNAME).tex
+	pdflatex $(DOCNAME).tex
+
+view: pdf
+	open $(DOCNAME).pdf
+
+clean:
+	rm -f *.blg *.bbl *.aux *.log

evm/spec/bibliography.bib

@@ -0,0 +1,20 @@
+@misc{stark,
+    author       = {Eli Ben-Sasson and
+                    Iddo Bentov and
+                    Yinon Horesh and
+                    Michael Riabzev},
+    title        = {Scalable, transparent, and post-quantum secure computational integrity},
+    howpublished = {Cryptology ePrint Archive, Report 2018/046},
+    year         = {2018},
+    note         = {\url{https://ia.cr/2018/046}},
+}
+
+@misc{plonk,
+    author       = {Ariel Gabizon and
+                    Zachary J. Williamson and
+                    Oana Ciobotaru},
+    title        = {PLONK: Permutations over Lagrange-bases for Oecumenical Noninteractive arguments of Knowledge},
+    howpublished = {Cryptology ePrint Archive, Report 2019/953},
+    year         = {2019},
+    note         = {\url{https://ia.cr/2019/953}},
+}

evm/spec/framework.tex

@@ -0,0 +1,39 @@
+\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.
+
+More specifically, we target a constraint system of degree 3.
+
+
+\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

evm/spec/instructions.tex

@@ -0,0 +1,8 @@
+\section{Privileged instructions}
+\label{privileged-instructions}
+
+\begin{enumerate}
+  \item[0xFB.] \texttt{MLOAD\_GENERAL}. Returns
+  \item[0xFC.] \texttt{MSTORE\_GENERAL}. Returns
+  \item[TODO.] \texttt{STACK\_SIZE}. Returns
+\end{enumerate}

evm/spec/introduction.tex

@@ -0,0 +1,3 @@
+\section{Introduction}
+
+TODO

evm/spec/tables.tex

@@ -0,0 +1,9 @@
+\section{Tables}
+\label{tables}
+
+\input{tables/cpu}
+\input{tables/arithmetic}
+\input{tables/logic}
+\input{tables/memory}
+\input{tables/keccak-f}
+\input{tables/keccak-sponge}

evm/spec/tables/arithmetic.tex

@@ -0,0 +1,4 @@
+\subsection{Arithmetic}
+\label{arithmetic}
+
+TODO

evm/spec/tables/cpu.tex

@@ -0,0 +1,4 @@
+\subsection{CPU}
+\label{cpu}
+
+TODO

evm/spec/tables/keccak-f.tex

@@ -0,0 +1,4 @@
+\subsection{Keccak-f}
+\label{keccak-f}
+
+This table computes the Keccak-f[1600] permutation.

evm/spec/tables/keccak-sponge.tex

@@ -0,0 +1,4 @@
+\subsection{Keccak sponge}
+\label{keccak-sponge}
+
+This table computes the Keccak256 hash, a sponge-based hash built on top of the Keccak-f[1600] permutation.

evm/spec/tables/logic.tex

@@ -0,0 +1,4 @@
+\subsection{Logic}
+\label{logic}
+
+TODO

evm/spec/tables/memory.tex

@@ -0,0 +1,61 @@
+\subsection{Memory}
+\label{memory}
+
+For simplicity, let's treat addresses and values as individual field elements. The generalization to multi-element addresses and values is straightforward.
+
+Each row of the memory table corresponds to a single memory operation (a read or a write), and contains the following columns:
+
+\begin{enumerate}
+  \item $a$, the target address
+  \item $r$, an ``is read'' flag, which should be 1 for a read or 0 for a write
+  \item $v$, the value being read or written
+  \item $\tau$, the timestamp of the operation
+\end{enumerate}
+The memory table should be ordered by $(a, \tau)$. Note that the correctness memory could be checked as follows:
+\begin{enumerate}
+  \item Verify the ordering by checking that $(a_i, \tau_i) < (a_{i+1}, \tau_{i+1})$ for each consecutive pair.
+  \item Enumerate the purportedly-ordered log while tracking a ``current'' value $c$, which is initially zero.\footnote{EVM memory is zero-initialized.}
+  \begin{enumerate}
+    \item Upon observing an address which doesn't match that of the previous row, set $c \leftarrow 0$.
+    \item Upon observing a write, set $c \leftarrow v$.
+    \item Upon observing a read, check that $v = c$.
+  \end{enumerate}
+\end{enumerate}
+
+The ordering check is slightly involved since we are comparing multiple columns. To facilitate this, we add an additional column $e$, where the prover can indicate whether two consecutive addresses are equal. An honest prover will set
+$$
+e_i \leftarrow \begin{cases}
+  1 & \text{if } a_i = a_{i + 1}, \\
+  0 & \text{otherwise}.
+\end{cases}
+$$
+We then impose the following transition constraints:
+\begin{enumerate}
+  \item $e_i (e_i - 1) = 0$,
+  \item $e_i (a_i - a_{i + 1}) = 0$,
+  \item $e_i (\tau_{i + 1} - \tau_i) + (1 - e_i) (a_{i + 1} - a_i - 1) < 2^{32}$.
+\end{enumerate}
+The last constraint emulates a comparison between two addresses or timestamps by bounding their difference; this assumes that all addresses and timestamps fit in 32 bits and that the field is larger than that.
+
+Finally, the iterative checks can be arithmetized by introducing a trace column for the current value $c$. We add a boundary constraint $c_0 = 0$, and the following transition constraints:
+\todo{This is out of date, we don't actually need a $c$ column.}
+\begin{enumerate}
+  \item $v_{\text{from},i} = c_i$,
+  \item $c_{i + 1} = e_i v_{\text{to},i}$.
+\end{enumerate}
+
+
+\subsubsection{Virtual memory}
+
+In the EVM, each contract call has its own address space. Within that address space, there are separate segments for code, main memory, stack memory, calldata, and returndata. Thus each address actually has three compoments:
+\begin{enumerate}
+  \item an execution context, representing a contract call,
+  \item a segment ID, used to separate code, main memory, and so forth, and so on
+  \item a virtual address.
+\end{enumerate}
+The comparisons now involve several columns, which requires some minor adaptations to the technique described above; we will leave these as an exercise to the reader.
+
+
+\subsubsection{Timestamps}
+
+TODO: Explain $\tau = \texttt{NUM\_CHANNELS} \times \texttt{cycle} + \texttt{channel}$.

evm/spec/tries.tex

@@ -0,0 +1,4 @@
+\section{Merkle Patricia tries}
+\label{tries}
+
+TODO

evm/spec/zkevm.tex

@@ -0,0 +1,59 @@
+\documentclass[12pt]{article}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{cite}
+\usepackage{draftwatermark}
+\usepackage[margin=1.5in]{geometry}
+\usepackage{hyperref}
+\usepackage{makecell}
+\usepackage{mathtools}
+\usepackage{tabularx}
+\usepackage[textwidth=1.25in]{todonotes}
+
+% Scale for DRAFT watermark.
+\SetWatermarkFontSize{24cm}
+\SetWatermarkScale{5}
+\SetWatermarkLightness{0.92}
+
+% Hyperlink colors.
+\hypersetup{
+    colorlinks=true,
+    linkcolor=blue,
+    citecolor=blue,
+    urlcolor=blue,
+}
+
+% We want all section autorefs to say "Section".
+\def\sectionautorefname{Section}
+\let\subsectionautorefname\sectionautorefname
+\let\subsubsectionautorefname\sectionautorefname
+
+% \floor{...} and \ceil{...}
+\DeclarePairedDelimiter\ceil{\lceil}{\rceil}
+\DeclarePairedDelimiter\floor{\lfloor}{\rfloor}
+
+\title{The Polygon Zero zkEVM}
+%\author{Polygon Zero Team}
+\date{DRAFT\\\today}
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+  We describe the design of Polygon Zero's zkEVM, ...
+\end{abstract}
+
+\newpage
+{\hypersetup{hidelinks} \tableofcontents}
+\newpage
+
+\input{introduction}
+\input{framework}
+\input{tables}
+\input{tries}
+\input{instructions}
+
+\bibliography{bibliography}{}
+\bibliographystyle{ieeetr}
+
+\end{document}