Update specs for Logic and Arithmetic Tables (#1363)

* Update specs for Logic and Arithmetic

* Apply comments

evm/spec/tables/arithmetic.tex

@@ -1,4 +1,54 @@
 \subsection{Arithmetic}
 \label{arithmetic}
 
-TODO
+Each row of the arithmetic table corresponds to a binary or ternary arithmetic operation. Each of these operations has an associated flag $f_{op}$ in the table, such that $f_{\texttt{op}} = 1$ whenever the operation is $\texttt{op}$ and 0 otherwise. The full list of operations carried out by the table is as follows:
+\paragraph*{Binary operations:} \begin{itemize}
+        \item basic operations: ``add'', ``mul'', ``sub'' and ``div'',
+        \item comparisons: ``lt'' and ``gt'',
+        \item shifts: ``shr'' and ``shl'',
+        \item ``byte'': given $x_1, x_2$, returns the $x_1$-th ``byte'' in $x_2$,
+        \item modular operations: ``mod'', ``AddFp254'', ``MulFp254'' and ``SubFp254'',
+        \item range-check: no operation is performed, as this is only used to range-check the input and output limbs in the range [$0, 2^{16} - 1$].
+    \end{itemize}
+For `mod', the second input is the modulus. ``AddFp254'', ``MulFp254'' and ``SubFp254'' are modular operations modulo ``Fp254'` -- the prime for the BN curve's base field.
+
+\paragraph*{Ternary operations:} There are three ternary operations: modular addition ``AddMod'', modular multiplication ``MulMod'' and modular subtraction ``SubMod''.
+
+Besides the flags, the arithmetic table needs to store the inputs, output and some auxiliary values necessary to constraints. The input and output values are range-checked to ensure their canonical representation. Inputs are 256-bits words. To avoid having too large a range-check, inputs are therefore split into sixteen 16-bits limbs, and range-checked in the range $[0, 2^{16}-1]$.
+
+Overall, the table comprises the following columns:
+\begin{itemize}
+    \item 17 columns for the operation flags $f_{op}$,
+    \item 1 column $op$ containing the opcode,
+    \item 16 columns for the 16-bit limbs $x_{0, i}$ of the first input $x_{0}$,
+    \item 16 columns for the 16-bit limbs $x_{1, i}$ of the second input $x_{1}$,
+    \item 16 columns for the 16-bit limbs $x_{2, i}$ of the third input $x_{2}$,
+    \item 16 columns for the 16-bit limbs $r_i$ of the output $r$,
+    \item 32 columns for auxiliary values $\texttt{aux}_i$,
+    \item 1 column $\texttt{range\_counter}$ containing values in the range [$0, 2^{16}-1$], for the range-check,
+    \item 1 column storing the frequency of appearance of each value in the range $[0, 2^{16} - 1]$.
+\end{itemize}
+
+\paragraph{Note on $op$:} The opcode column is only used for range-checks. For optimization purposes, we check all arithmetic operations against the cpu table together. To ensure correctness, we also check that the operation's opcode corresponds to its behavior. But range-check is not associated to a unique operation: any operation in the cpu table might require its values to be checked. Thus, the arithmetic table cannot know its opcode in advance: it needs to store the value provided by the cpu table.
+
+\subsubsection{Auxiliary columns}
+The way auxiliary values are leveraged to efficiently check correctness is not trivial, but it is explained in detail in each dedicated file. Overall, five files explain the implementations of the various checks. Refer to:
+\begin{enumerate}
+    \item ``mul.rs'' for details on multiplications.
+    \item ``addcy.rs'' for details on addition, subtraction, ``lt'' and ``gt''. 
+    \item ``modular.rs'' for details on how modular operations are checked. Note that even though ``div'' and ``mod'' are generated and checked in a separate file, they leverage the logic for modular operations described in ``modular.rs''. 
+    \item ``byte'' for details on how ``byte'' is checked.
+    \item ``shift.rs'' for details on how shifts are checked. 
+\end{enumerate}
+
+\paragraph*{Note on ``lt'' and ``gt'':} For ``lt'' and ``gt'', auxiliary columns hold the difference $d$ between the two inputs $x_1, x_2$. We can then treat them similarly to subtractions by ensuring that $x_1 - x_2 = d$ for ``lt'' and $x_2 - x_1 = d$ for ``gt''. An auxiliary column $cy$ is used for the carry in additions and subtractions. In the comparisons case, it holds the overflow flag. Contrary to subtractions, the output of ``lt'' and ``gt'' operations is not $d$ but $cy$. 
+
+\paragraph*{Note on ``div'':} It might be unclear why ``div'' and ``mod'' are dealt with in the same file. 
+
+Given numerator and denominator $n, d$, we compute, like for other modular operations, the quotient $q$ and remainder $\texttt{rem}$: 
+$$div(x_1, x_2) = q * x_2 + \texttt{rem}$$. 
+We then set the associated auxiliary columns to $\texttt{rem}$ and the output to $q$. 
+
+This is why ``div'' is essentially a modulo operation, and can be addressed in almost the same way as ``mod''. The only difference is that in the ``mod'' case, the output is $\texttt{rem}$ and the auxiliary value is $q$.
+
+\paragraph{Note on shifts:} ``shr'' and ``shl'' are internally constrained as ``div'' and ``mul'' respectively with shifted operands. Indeed, given inputs $s, x$, the output should be $x >> s$ for ``shr'' (resp. $x << s$ for ``shl''). Since shifts are binary operations, we can use the third input columns to store $s_{\texttt{shifted}} = 1 << s$. Then, we can use the ``div'' logic (resp. ``mul'' logic) to ensure that the output is $\frac{x}{s_{\texttt{shifted}}}$ (resp. $x * s_{\texttt{shifted}}$).

evm/spec/tables/logic.tex

@@ -1,4 +1,18 @@
 \subsection{Logic}
 \label{logic}
 
-TODO
+Each row of the logic table corresponds to one bitwise logic operation: either AND, OR or XOR. Each input for these operations is represented as 256 bits, while the output is stored as eight 32-bit limbs. 
+
+Each row therefore contains the following columns:
+\begin{enumerate}
+    \item $f_{\texttt{and}}$, an ``is and'' flag, which should be 1 for an OR operation and 0 otherwise,
+    \item $f_{\texttt{or}}$, an ``is or'' flag, which should be 1 for an OR operation and 0 otherwise,
+    \item $f_{\texttt{xor}}$, an ``is xor'' flag, which should be 1 for a XOR operation and 0 otherwise,
+    \item 256 columns $x_{1, i}$ for the bits of the first input $x_1$,
+    \item 256 columns $x_{2, i}$ for the bits of the second input $x_2$,
+    \item 8 columns $r_i$ for the 32-bit limbs of the output $r$.
+\end{enumerate}
+
+Note that we need all three flags because we need to be able to distinguish between an operation row and a padding row -- where all flags are set to 0.
+
+The subdivision into bits is required for the two inputs as the table carries out bitwise operations. The result, on the other hand, is represented in 32-bit limbs since we do not need individual bits and can therefore save the remaining 248 columns. Moreover, the output is checked against the cpu, which stores values in the same way.