Remove redundant range check in rotation gadget

[mitschabaude]

This PR removes one range check used in Gadgets.rotate(), which was originally added as a conservative measure. What follows is a proof that the check is not needed for soundness.

The rotation gadget

The 64-bit rotation gate takes as inputs four variables: input $n$, rotated output $r$, shifted input $s$ and excess $x$. It also takes the limbs of a bound $b$. A coefficient of the gate is the number of bits to rotated, $R \in [0, 64]$.

The first check that the gate does is the defining equation of $s$ and $x$.

$$\tag{c1} n 2^R = s + x 2^{64} \mod{p} $$

This equation tells us the following: When we shift $n$ by $R$ bits to the left, the result is a shifted value $s < 2^{64}$, plus some excess bits $x$ which are shifted to bit positions higher than 64.

Like all constraints, $(c1)$ is an equation modulo the native field size $p$.

The rotated value $r$ is then simply defined by the following, second gate equation:

$$\tag{c2} r = s + x \mod{p} $$

This "moves" the excess bits $x$ to the other end which is what a rotation is supposed to do.

The excess $x$ is connected to the bound $b$ by the third gate equation:

$$\tag{c3} b = x + 2^{64} - 2^R \mod{p} $$

Finally, the gate constrains the bound limbs to represent $b$, and also range-checks the bound to 64 bits.
To finish the gate, a second row always has to be added which adds the same range-check on $s$. In summary, we have

$$\tag{c4} b \in [0, 2^{64}) $$

$$\tag{c5} s \in [0, 2^{64}) $$

Also, the rotation gadget assumes that the input is range-checked:

$$\tag{a} n \in [0, 2^{64}) $$

Soundness proof

Proposition. Equations $(c1-c5)$, together with the assumption on the input $(a)$, imply the following:

• The defining equations $(c1)$ and $(c2)$ are true over the integers, not just modulo $p$
• $x \in [0, 2^{64})$ and $r \in [0, 2^{64})$

Proof. The range check on $b$ means that $0 \le x + 2^{64} - 2^R < 2^{64}$. This by itself implies that $x$ belongs to one of two intervals:

$$ x \in [0, 2^R) \cup [p - 2^{64} + 2^R, p-1] $$

Let's call the interval on the right the "overflow case". We wish to rule out this case and show that $x \in [0, 2^R)$.

Let's assume we are in the overflow case. Then, $1 \le (p-x) < 2^{64}$. We can rearrange $(c1)$ to get

$$\tag{c1'} (p - x) 2^{64} = s - n 2^R \mod{p} $$

Since $(p-x)$ is multiplied by $2^{64}$, the LHS lies in the range $[2^{64}, 2^{128})$. We want to show that the residue of the right hand side modulo $p$ cannot fall within this range.

In fact, since $s, n \in [0, 2^{64})$, the RHS belongs to one of two intervals:

$$ s - n 2^R \in [0, 2^{64}) \cup [p - 2^{64 + R}, p) $$

The left interval (corresponding to the case $s > n 2^R$) clearly does not overlap with $[2^{64}, 2^{128})$. Since $R \le 64$, the right interval is contained in $[p - 2^{128}, p)$. Since in our case $p > 2^{129}$, this interval also does not overlap with the LHS.

Because the possible intervals of LHS and RHS modulo $p$ have no overlap, $(c1')$ and therefore $(c1)$ are not satisfied, which contradicts our assumptions. The "overflow case" can therefore be ruled out, and we conclude $x \in [0, 2^R)$.

With this information, both sides of equation $(c1)$ can be bounded to small values, so this equation holds over the integers.
In particular, $s$ is a multiple of $2^R$.

Since $s < 2^{64}$, being a multiple of $2^R$ implies that $s \le 2^{64} - 2^R$. Because we showed $x < 2^R$, we can deduce that

$$ r = s + x \in [0, 2^{64}) $$

and equation $(c2)$ holds over the integers. /qed

Conclusion

The soundness proof showed that we don't have to add an extra range check which constrains $x \in [0, 2^{64})$. In fact, this bound is already implied by the gadget and is redundant. This PR removes the extra check. The rotation gadget only needs 2 instead of 3 rows.

[mitschabaude]

Unrelated fix: Unit tests need equivalentProvable which tests implementations in a circuit

[Trivo25]

Since this improvement came after the new release I think we should add a quick paragraph to the changelog

[querolita]

Great improvement

[querolita]

Oh good, for checking the input is 64 bits in a stand-alone test