# 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\_FIELD-1$. $SNARK\_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()`](https://github.com/iden3/circomlib/blob/cff5ab6288b55ef23602221694a6a38a0239dcc0/circuits/babyjub.circom#L96-L97) (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\_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 \implies
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