# Range checks

Tables often deal with 256-bit words which are split into 16-bit limbs. This helps to avoid field overflows. Range-checks are used for examining integrity of values in these 16-bit limbs.

### What to range-check?¶

The idea here is to range-check every field element pushed into the Stack, as well as every memory writes. That is, Range-checking the PUSH and MSTORE opcodes.

Other range-checks are:

- Pushes and memory writes for
`MSTORE_32BYTES`

, range-checked in the “BytePackingStark”. - Syscalls, exceptions and prover inputs are range-checked in “ArithmeticStark”.
- Inputs and outputs of binary and ternary arithmetic operations are range-checked in “ArithmeticStark”.
- Inputs’ bits of logic operations are checked to be either \(1\) or \(0\) in “LogicStark”. Since “LogicStark” only deals with bitwise operations, it is sufficient to range-check outputs.
- Inputs to 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.

### What not to range-check¶

Some operations do not require range-checks, including the following:

`MSTORE_GENERAL`

, which writes values read from Stack. Therefore, the written values were already range-checked by previous pushes.`EQ`

, which reads two – already range-checked – elements on the Stack, and checks their equality. The output is either 0 or 1, and therefore need not be range-checked.`NOT`

, which reads one – already range-checked – element. The result is constrained to be equal to \(\texttt{0xFFFFFFFF} - \texttt{input}\), which implicitly enforces the range-check.`PC`

, the Program Counter, which 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 JUMP destinations, JUMPDESTs. Moreover, when in kernel mode, every JUMP’s destination is a location within the kernel, and the kernel code is smaller than \(2^{32}\). These two points implicitly enforce range-check on PC’s.`GET_CONTEXT`

,`DUP`

, and`SWAP`

, all read and push values that were already written in memory. These pushed values were therefore already range-checked.

Note that range-checks are performed on the range \([0, 2^{16} - 1]\), so as to limit the trace length.

### Lookup argument¶

Enforcement of range-checks leverages LogUp, a lookup argument introduced by Ulrich Häbock.

Given a `looking table`

\(s = (s_1, ..., s_n)\) and a `looked table`

\(t = (t_1, ..., t_m)\), the goal is to prove that

In our case, \(t = (0, .., 2^{16} - 1)\) and \(s\) is composed of all the columns in each STARK that must be range-checked.

The LogUp paper explains that proving the previous assertion is equivalent to proving that there exists a sequence \(\{l_j \}\) such that:

The values in the `looking table`

\(s = (s_1, ..., s_n)\), can be stored in columns each of length \(n\). And if these columns are \(c\) in number, the above equality becomes:

The `multiplicity`

\(m_i\) of each value \(t_i\) is defined as the number of times \(t_i\) appears in the `looking table`

\(s = (s_1, ..., s_n)\). In other words, \(m_i\) is the cardinality of a set, given by:

Multiplicities of the \(\{ t_j \}\) form a sequence \(\{ m_j \}\) and thus proves existence of the required \(\{ l_j \}\) sequence of Equation \(1\) above. This means Equation \(2\) can be rewritten as:

For each random challenge \(\alpha\), provided by the verifier, proving the lookup argument amounts to checking this equation:

However, this yields a high degree equation.

Häbock suggests circumventing this issue by providing helper columns \(\{h_i\}\) and \(d\) , such that at any given row \(i\):

The \(h\) helper columns can be batched together to save columns. At most \(\texttt{constraint\_degree} - 1\) helper functions can be batched together.

In our case, they are batched 2 by 2. For row \(i\), we therefore obtain:

If the number of column \(c\) is odd, we have one extra helper column:

We henceforth assume \(c\) to be even.

Now, let \(g\) be a generator of a subgroup of order \(n\). Extrapolate \(h\), \(m\), and \(d\) in order to get polynomials such that,

Define the following polynomial:

### Constraints¶

Given the above definitions and a challenge \(\alpha\), the following constraints can be used to determine whether the assertion holds true:

It still remains to ensure that \(h^k\) is well constructed for all \(1 \leq k \leq c/2\):

Note that, if \(c\) is odd, then ther is one unbatched helper column \(\{h^{{(c/2)}+1}\}\) for which we need a last constraint:

Finally, the verifier needs to ensure that the `looked table`

\(t = (t_1, ..., t_m)\), was correctly computed.

In each STARK, \(t\) is computed starting from 0 and adding at most 1 at each row. This construction is constrained as follows: