Range checks

See end of page for some progress so far.

Problem statement

We have a fixed prime $q \approx 2^{256}$; all values below are elements of the finite field $\mathbb{F}_q$.

We want to come up with a system of linear and quadratic equations in $x$, $y$, and some auxiliary variables $a_1, a_2, \ldots$, with the following properties:

• If $0 \leq y < 2^{64}$ and $x \in \{0, 1, \ldots, y-1\}$, then the equations have a simultaneous solution $(a_1, a_2, \ldots)$.
• If $0 \leq y < 2^{64}$ and $x \not \in \{0, 1, \ldots, y-1\}$, then the equations have no simultaneous solution.
• If $y$ is not in the range $[0, 2^{64})$, we impose no condition.

The “cost model” is: Linear equations are effectively free; we want to minimize the number of quadratic equations.

We know a way to do it with $2*64$ quadratic equations; we think the best possible bound is much closer to $64$.

Motivation: Range checks in zero-knowledge proofs.

A zero-knowledge proof lets a prover prove claims about a list of values in $\mathbb{F}_q$. The prover can natively prove only linear and quadratic polynomial equalities; any other sort of claim must be rewritten in terms of polynomials.

In practice, one often wants to prove claims like $0 \leq x < 2^{64}$ (i.e. that $x$ represents a valid 64-bit integer), or $0 \leq x < y$. (Note that a single inequality, like $0 \leq x$ or $x \leq y$, makes no sense in the context of a finite field. So, in a ZK circuit, “$0 \leq x$” will often be expressed as “$x$ is a 64-bit integer” and $0 \leq x$ – in other words, $0 \leq x < 2^{64}$.)

Known results

As a warmup, consider the simple “range check” $0 \leq x < 2$. This is equivalent to the single equation $x^2 - x = 0$.

The “range check” $0 \leq x < 2^{64}$ can be expressed by saying that “$x$ has a valid 64-bit binary expansion”. Algebraically, we introduce auxiliary variables $b_0, b_1, \ldots, b_{63}$, and require $x = b_0 + 2 b_1 + 4 b_2 + \cdots + 2^{63} b_{63}$, $b_0^2 - b_0 = 0$, $b_1^2 - b_1 = 0$, and so forth.

This gives a total of 64 quadratic equations; for heuristic reasons we expect that 64 is best possible.

Returning to the problem $0 \leq x < y$, one simple solution is to verify that both $x$ and $y - x$ lie in the range $[0, 2^{64})$; this solution uses $2^{64}$ quadratic constraints. We expect that this can be improved.

One potential idea is to change the power-of-2 coefficients in the binary expansion

$$x = b_0 + 2 b_1 + 4 b_2 + \cdots + 2^{62} b_{62} + 2^{63}b_{63},$$

depending on $y$. For example, replacing $2^{63}$ with a known constant $C$ with $0 \leq C \leq 2^{63}$ in

$$x = b_0 + 2 b_1 + 4 b_2 + \cdots + 2^{62} b_{62} + Cb_{63}$$

allows one to test a range of any length between $2^{63}$ and $2^{64}$.

Progress

Intuition from algebraic geometry suggests that it might not be possible to solve the general problem as stated.

But we found two solutions that offer more efficient range checks in slightly different contexts. If $y$ is publicly known, our first solution lets you cut the number of constraints from 128 to 64.

Alternatively, if prover and verifier are allowed an additional round of interaction, the range check can be done using a lookup argument in just 48 constraints.