Comparisons in zero-knowledge proofs

Question

There is already a great survey on how to do range checks in a zero-knowledge setting. A range check allows to constrain a variable to be in a certain range. Comparisons seem to be similar, but they are actually very different in that they're allowed to be false.

E.g. if we write a range checks like this:

0 <= n < c

we can be sure that validation will never succeed if n is not in the given range. However if we have something like

if 0 <= n < c then x else y

then validation is supposed to succeed regardless of whether n is in the given range or not (provided the prover did its work honestly).

A similar issue arises in other situations such as n /= 0. It is trivial to require n not to equal 0:

n * inv n = 1

(because only 0 doesn't have an inverse) however in order to compile

if n /= 0 then x else y

we need to make use of non-determinism and introduce an auxiliary variable.

So my question is: how to compile 0 <= n < c when it's not a constraint, but rather a regular expression that I can use as a condition in an if statement?

Answer 1

(This answer assumes a proving system that supports general arithmetic constraints, e.g. R1CS, over a finite field $\mathbb{F}_p$. It can be adapted to other settings but that may be non-trivial.)

Consider that a comparison $0 \leq n < c$ in $\mathbb{F}_p$ has negation $c \leq n < p$. So a constraint system for $b = (0 \leq n < c)$ can be essentially

$\hspace{1em}b: \text{boolean}. \text{ if } b \text{ then assert } 0 \leq n < c. \text{ if not } b \text{ then assert } c \leq n < p$.

It might not be obvious how to make the assertions conditional on $b$ or on $\text{not } b$, but there's a trick for that. Let's say we're using the the approach in appendix A.3.2.2 of the Zcash protocol spec for the assertions, so that the numbers we're checking are actually given as a bit representations. Then, for a plain range check, there would need to be an additional constraint $n = \sum\limits_{i=0}^{k-1} 2^i n_i$.

Instead, pick two integers $x$ and $y$, with bit representations $x = \sum\limits_{i=0}^{k-1} 2^i x_i$ and $y = \sum\limits_{i=0}^{k'-1} 2^i y_i$. Unconditionally check that $0 \leq \langle x_{k-1} \cdots x_0 \rangle < c$ and $c \leq \langle y_{k'-1} \cdots y_0 \rangle < p$. Finally assert:

• $\left(n - \sum\limits_{i=0}^{k-1} 2^i x_i\right) \times b = 0$
• $\left(n - \sum\limits_{i=0}^{k'-1} 2^i y_i\right) \times (1-b) = 0$

The first constraint here asserts that either $b = 0$ or $n = x$, in other words (given that $b$ is constrained to be boolean) $(b = 1) \Rightarrow (n = x)$. The second asserts that either $b = 1$ or $n = y$, in other words $(b = 0) \Rightarrow (n = y)$. So we can infer that $(b = 1) \Rightarrow (0 \leq n < c)$ and $(b = 0) \Rightarrow (c \leq n < p)$, as required. One of $x$ and $y$ will not be constrained, so we just pick it to be something for which the corresponding range check passes.

Note that some care is required to implement the range checks correctly given that at least one of $k$ and $k'$ will be close to the length of $p$, but that's orthogonal to the main question you asked I think. For the method in appendix A.3.2.2 it should be fine, since that method supports bit representations of arbitrary length.

There's probably a way to optimize this further by not doing two full bit decompositions, but I'm not seeing it right now.

Answer 2

It seems that in order to compare a variable a and a constant c, all we need is to compare them bitwise. Since c is a constant, we do not need to introduce any new witness variables to get its unpacking. We can just directly use the bits of c as constants without specifying anywhere that those bits come from the c constant.

We'll use the convention that the most significant bit goes first and instead of R1CS we'll use the constraint system of Sonic/Bulletproofs.

Everything is summarized in the following truth table:

ai ci r   res
0  0  r    r
1  0  r    1
0  1  r    0
1  1  r    r

Here ai and ci are particular bits of a and c and r is the rest of the computation. This reads as "if ai equals ci (two bits are equal, the 1 and 4 cases), then look at lower bits, otherwise if ai is 1 while ci is 0, then return 1, otherwise return 0". I.e. we compare the bits of the variable and the constant until there's a mismatch, in which case we return the result depending on whether it's the variable's bit is 1 or the constant's one.

Since ci is known statically, we can break this truth table down into two cases: ci = 0 and ci = 1. Which we can compile as

ci = 0: res = ai OR r
ci = 1: res = ai AND r

If we ignore the problem of compiling consecutive ORs and ANDs efficiently, then this becomes:

ci = 0: res = ai + r - ai * r
ci = 1: res = ai * r

Let us now look at some examples. Consider a variable v that fits into 3 bits, which we compile as:

_3 = _3 * _3
_2 = _2 * _2
_1 = _1 * _1
0 = - v + _1 + 2 * _2 + 4 * _3

where _3 is the most significant bit, _1 is the least significant bit and _2 is in the middle. The first three equations ensure that _1, _2 and _3 are indeed bits (i.e. can either be 0 or 1). The last equation ensures that those bits together represent the v variable in binary form.

Now let's see what constraints we add to the above set if we compare the v variable and some constant c (v > c) and compile that.

For c = 7 we get

res = 0

I.e. there is no three-bit number that is greater than 7.

For c = 6 we get

_4 = _2 * _1
res = _3 * _4

The only three-bits number that is greater than 6 is 7, which is represented as 111 in binary form. I.e. all bits must be equal to 1. And this is exactly what the equations above say: if all bits of a three-bits number are 1, then the result is 1, i.e. the number is bigger than 6, otherwise the result is 0.

For c = 5 we get

res = _3 * _2

There are two three-bit numbers that are greater than 5: 6 (110) and 7 (111). I.e. a three-bit number is bigger than 5 whenever its two most significant bits are both 1 and this is exactly what the equation above says.

For c = 4 we get

_4 = _2 * _1
_5 = _1 + _2 - _4
res = _3 * _5

There are three three-bit numbers that are greater than 4: 5 (101), 6 (110) and 7 (111). I.e. the most significant bit must be 1 (the _3 part of the last equation) and (the * part of the last equation) the disjunction of the other two bits must be 1 as well (the _5 part pf the last equation). That disjunction is _2 or _1 and we compile this down to the first two constraints as per usual.

For c = 3 we get

res = _3

There are four three-bit numbers that are greater than 3: 4 (100), 5 (101), 6 (110) and 7 (111) and all of them start with 1, i.e. the most significant bit of v must be equal to 1 in order for v > 3 to hold.

This approach can be easily extended to handle the variable < constant as well as variable < variable cases.