Comparisons in zero-knowledge proofs 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 &lt;= n &lt; 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 &lt;= n &lt; 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 &lt;= n &lt; c when it's not a constraint, but rather a regular expression that I can use as a condition in an if statement?
(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 &lt; c$ in $\mathbb{F}_p$ has negation $c \leq n &lt; p$. So a constraint system for $b = (0 \leq n &lt; c)$ can be essentially
$\hspace{1em}b: \text{boolean}. \text{ if } b \text{ then assert } 0 \leq n &lt; c. \text{ if not } b \text{ then assert } c \leq n &lt; 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 &lt; c$ and $c \leq \langle y_{k'-1} \cdots y_0 \rangle &lt; 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 &lt; c)$ and $(b = 0) \Rightarrow (c \leq n &lt; 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.