@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.

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)

@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

@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.

@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!

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