add SafeLessThan template to comparators with range checks over inputs

[enricobottazzi]

@BlakeMScurr recently spotted an anomalous behavior in the LessThan(n) template when the first input doesn't fit in n bits. This issue was discussed in Sismo, Iden3 and fully analysed and tested by Blake.

After discussing with Blake and @clararod9 we propose a SafeLessThan(n) template that uses Num2Bits(252) to
perform a range check over the two inputs. As long as both the inputs don't overflow 252 bits, the operation is safe.

Performing SafeLessThan(n) adds 252*2 constraints compared to LessThan(n) therefore, it should be used either if the range check over the inputs has already been performed outside the template or the inputs are not expected to overflow 252 bits.

[BlakeMScurr]

Looks good! Couple of minor comments.

[BlakeMScurr]

We can save some constraints by restricting to n bits instead. It will always be safe since n <= 252 anyway. Also, that way we can interpret SafeLessThan(n) as meaning "safely compare two n-bit numbers." This makes it easier to understand why in[0]+ (1<<n) - in[1] should be an n+1 bit number.

[enricobottazzi]

Thanks for the comment. Good point. Added to the PR.

[BlakeMScurr]

Perhaps we could use a normal LessThan component here to avoid code reuse. It makes it clearer what the difference between LessThan and SafeLessThan is, and if LessThan changes in the future we don't risk two difference implementations.

[enricobottazzi]

Agree, applied change in this commit

[AndriianChestnykh]

@enricobottazzi , @BlakeMScurr if I don't miss something, you can have only 2 additional constraints instead of 252*2 by having this:

        signal aInRange;
        aInRange <-- (in[0] >> (n-1)) & 1;
        aInRange * (aInRange -1 ) === 0;

instead of this:

    component aInRange = Num2Bits(n);
    aInRange.in <== in[0];

Although I haven't checked it yet.

[clararod9]

Hi all! Everything looks good!

@AndriianChestnykh I am not sure, but I think that your proposal would not be safe: it is using the operator <-- for the first assignment which does not introduce any constraint. This way, the R1CS system will only contain the check
aInRange * (aInRange -1 ) === 0;
with respect to the variable aInRange that is not enough to force in[0] to be of n bits (it only makes aInRange to be binary but there is not any constraint establishing the relation between aInRange and in[0] as the assignment is not added to the constraints)

[AndriianChestnykh]

@clararod9 , thanks. I totally missed that my proposal won't work.
However, thinking a bit more I can do another proposal.
As far as I got it, we use this expression just to check that all bits in[0] starting from n-th position and greater are zero:

    component aInRange = Num2Bits(n);
    aInRange.in <== in[0];

The Num2Bits template solves this task but it adds excessive amount of constraints (+252) than what is needed for the goal as it needs to "split" the bits in addition.
We can reach the same by doing the following instead those two lines:

    in[0] >> n === 0

[BlakeMScurr]

@AndriianChestnykh yes the Num2Bits component checks that bits n and greater are 0, but it also checks that the bits from 0-n are 0 or 1, which is important for a valid range check. I'm pretty sure you always require one constraint per bit for an R1CS range check (though I'd love to be proved wrong).

I haven't tried it, but I think in[0] >> n === 0 would have a compiler error like "Non quadratic constraints not allowed", as per the docs.

[AndriianChestnykh]

@BlakeMScurr, yes I'm wrong here as well. in[0] >> n === 0 triggers the "Non quadratic constraints not allowed" exception as you said. So it does something "non-quadratic" under the hood, which I don't understand yet.
And I did not fully understand why we need one constraint per bit for an R1CS range check as you said.
I may miss something how the modular arithmetic, R1CS or Circom works, so need to deepen my knowledge to understand.
Thanks!

[0xknon]

This is a really helpful update. When can this be merged ?