Skip to content
This repository has been archived by the owner on Feb 21, 2024. It is now read-only.

Commit

Permalink
proofreading (0xPolygonZero#1466)
Browse files Browse the repository at this point in the history
  • Loading branch information
Ursulafe authored Jan 13, 2024
1 parent c4319dc commit 5c1ec52
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions evm/spec/framework.tex
Original file line number Diff line number Diff line change
Expand Up @@ -86,14 +86,14 @@ \subsubsection{What to range-check?}
\item Syscalls, exceptions and prover inputs are range-checked in ``ArithmeticStark''.
\item The inputs and outputs of binary and ternary arithmetic operations are range-checked in ``ArithmeticStark''.
\item The inputs' bits of logic operations are checked to be either 1 or 0 in ``LogicStark''. Since ``LogicStark'' only deals with bitwise operations, this is enough to have range-checked outputs as well.
\item The inputs of Keccak operations are range-checked in ``KeccakStark''. The output digest is written as bytes in ``KeccakStark''. Those bytes are used to reconstruct the associated 32-bit limbs checked against the limbs in ``CpuStark''. This implictly ensures that the output is range-checked.
\item The inputs of Keccak operations are range-checked in ``KeccakStark''. The output digest is written as bytes in ``KeccakStark''. Those bytes are used to reconstruct the associated 32-bit limbs checked against the limbs in ``CpuStark''. This implicitly ensures that the output is range-checked.
\end{enumerate}
Note that some operations do not require a range-check:
\begin{enumerate}
\item ``MSTORE\_GENERAL'' read the value to write from the stack. Thus, the written value was already range-checked by a previous push.
\item ``EQ'' reads two -- already range-checked -- elements on the stack, and checks they are equal. The output is either 0 or 1, and does therefore not need to be checked.
\item ``NOT'' reads one -- already range-checked -- element. The result is constrained to be equal to $\texttt{0xFFFFFFFF} - \texttt{input}$, which implicitly enforces the range check.
\item ``PC'': the program counter cannot be greater than $2^{32}$ in user mode. Indeed, the user code cannot be longer than $2^{32}$, and jumps are constrainted to be JUMPDESTs. Moreover, in kernel mode, every jump is towards a location within the kernel, and the kernel code is smaller than $2^{32}$. These two points implicitly enforce $PC$'s range check.
\item ``PC'': the program counter cannot be greater than $2^{32}$ in user mode. Indeed, the user code cannot be longer than $2^{32}$, and jumps are constrained to be JUMPDESTs. Moreover, in kernel mode, every jump is towards a location within the kernel, and the kernel code is smaller than $2^{32}$. These two points implicitly enforce $PC$'s range check.
\item ``GET\_CONTEXT'', ``DUP'' and ``SWAP'' all read and push values that were already written in memory. The pushed values were therefore already range-checked.
\end{enumerate}
Range-checks are performed on the range $[0, 2^{16} - 1]$, to limit the trace length.
Expand All @@ -120,7 +120,7 @@ \subsubsection{Lookup Argument}
d_i = \frac{1}{\alpha + t_i}
\end{gather*}

The $h$ helper columns can be batched together to save columns. We can batch at most $\texttt{contraint\_degree} - 1$ helper functions together. In our case, we batch them 2 by 2. At row $i$, we now have:
The $h$ helper columns can be batched together to save columns. We can batch at most $\texttt{constraint\_degree} - 1$ helper functions together. In our case, we batch them 2 by 2. At row $i$, we now have:
\begin{align*}
h_i^k = \frac{1}{\alpha + s_i^{2k}} + \frac{1}{\alpha + s_i^{2k+1}} \forall 1 \leq k \leq c/2 \\
\end{align*}
Expand Down

0 comments on commit 5c1ec52

Please sign in to comment.