3
$\begingroup$

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?

$\endgroup$
3
  • 2
    $\begingroup$ The question you linked explains the basics of range check ZK proofs. This looks like a question, for which an answer would surpass the common length and complexity of an answer by a lot. Translating pseudo-code into ZK proofs can be done, but it has - depending on the algorithm - massive blowups, because actually for something like if c then x else y would mean you have to do both x and y to not reveal anything about c. This only works for a small number of if-then-else statements. $\endgroup$ – tylo Jun 28 '19 at 19:24
  • 2
    $\begingroup$ You might want to look at EzPC: Programmable and Efficient Secure Two-Party Computation for Machine Learning by Chandran et.al. for current research on a compiler for this kind of two party computation, which possibly could be used for producing such a proof. $\endgroup$ – tylo Jun 28 '19 at 19:26
  • $\begingroup$ @tylo, yeah, I know about exponential blowups. In fact, I already have a compiler that compiles if statements and equality checks just fine. I'm specifically interested in comparisons, because I can't find any references on them. Thank you for the amazing reference! I had a cursory look and I do not yet understand how they handle comparisons, but hopefully I'll figure this out. All: a direct answer would still be appreciated, though! $\endgroup$ – user3237465 Jun 28 '19 at 20:17
2
$\begingroup$

(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.

$\endgroup$
5
  • 1
    $\begingroup$ Thank you for the answer. This will probably sound extremely stupid, but I don't know how to compile an assert when it's inside an if (apart from compiling if b then assert 0 <= n < c as assert b || 0 <= n < c, but then we're back to the original problem). Do you happen to have a reference? I'd really appreciate some sort of explanation. $\endgroup$ – user3237465 Aug 27 '20 at 21:52
  • 1
    $\begingroup$ Thank you very much for expanding the answer. $\endgroup$ – user3237465 Aug 28 '20 at 16:45
  • 1
    $\begingroup$ You're welcome. This was less obvious than I thought it was when I first wrote my answer. $\endgroup$ – Daira Hopwood Aug 28 '20 at 23:04
  • $\begingroup$ I posted an answer on how I ended up implementing compilation of comparisons a year ago or so. It's rather different to what you propose. Any chance you could take a look and say if there any obvious flaws in the described strategy? $\endgroup$ – user3237465 Sep 7 '20 at 13:27
  • 1
    $\begingroup$ That looks to be along the right lines, yes. It's similar to the method of appendix A.3.2.2 of the Zcash protocol spec in spirit, but computing a boolean result after each bit rather than just constraining the comparison to hold. $\endgroup$ – Daira Hopwood Sep 14 '20 at 21:41
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.