Fix for Geometry's bug for projects that want to continue using unfixed BabyPbk() version

NOTE:

$l$ used in this document is the same as

$l$ used in https://eips.ethereum.org/EIPS/eip-2494, and same as

$r$ used in Geometry's bug report.

The theoretical fix is to ensure

$secret<l$. In circom, it'll look like this:

LessThan(251)([secret, l]) === 1;

Readers may know that just using LessThan template doesn't protect against all cases. For example, run this in zkrepl.dev: https://gist.github.com/0xbok/3f87b9c79fde41759f31fc62de218b80. It shows that LessThan passes when

$secret=SNARK\mathrm{\_}FIELD-1$.

$SNARK\mathrm{\_}FIELD-1$ is the maximum value in circom and hence it's greater than

$l$, but LessThan returns 1 interpreting it as

$p-1<l$.

We show that enforcing LessThan(251)[secret, l].out === 1 and then using BabyPbk() (as defined in current master branch of circomlib) on

$secret$ is enough to enforce that

$secret<l$.

Proof

We do this by proof of contradiction. We try to find

$secret\in [l,SNARK\mathrm{\_}FIELD-1]$ such that LessThan(251)[secret, l].out === 1 and BabyPbk() check also passes.

We can shorten our search for such a

$secret$ in range

$[l,2^{253}-1]$ since BabyPbk constrains secret to 253 bits here: https://github.com/iden3/circomlib/blob/cff5ab6288b55ef23602221694a6a38a0239dcc0/circuits/babyjub.circom#L96-L97.

Now, here is LessThan template:

template LessThan(n) {
    assert(n <= 252);
    signal input in[2];
    signal output out;

    component n2b = Num2Bits(n+1);

    n2b.in <== in[0]+ (1<<n) - in[1];

    out <== 1-n2b.out[n];
}

LessThan(251)([secret, l]) computes: 1<<251 - l + secret. We know

$l$, so 1<<251 - l is also known. Let's call it

$y$.

$y+secret$ is constrained to 252 bits by LessThan. This expression is always < SNARK_FIELD because of

$secret$'s range (confirmed by line 11 and 12 in the code below). So we can ignore mod SNARK_FIELD for the rest of the discussion.

We've already established that LessThan enforces that

$y+secret$ is of 252 bits. If we want LessThan.out = 1, n2b.out[251] has to be 0. This implies the most significant bit of

$y+secret$ has to be 0.

$y+secret$ is of 252 bits with the most significant bit as 0. This means

$y+secret$ is of 251 bits. So:

$$y+secret<2^{251}-1⟹secret<2^{251}-1-y$$

Since

$2^{251}-1-y<l$ (line 14 in code below), we get:

$$secret<l$$

But our initial range of

$secret$ is

$[l,2^{253}-1]$. Hence, there is no such secret.

---

Code to verify some claims in the proof:

var SNARK_FIELD = 21888242871839275222246405745257275088548364400416034343698204186575808495616n; // 254 bits
var l = 2736030358979909402780800718157159386076813972158567259200215660948447373041n; 
2736030358979909402780800718157159386076813972158567259200215660948447373039n// 251 bits
var one251 = 1n << 251n; // 252 bits
var y = one251 - l; // 249 bits

var secret_min = l;
var secret_max = 2n**253n-1n;

// ensure that y+secret never overflows p (SNARK_FIELD)
console.log("y+l < SNARK_FIELD-1", y+l < SNARK_FIELD-1n);
console.log("y+2^253-1 < SNARK_FIELD-1", y+(2n**253n-1n) < SNARK_FIELD-1n);

console.log("2**251-1 - y < l", 2n**251n-1n - y < l);

reach out at twitter.com/blockdeveth