fixing weak safety bug in template Modulo: adding Num2Bits check

[clararod9]

Potential safety bug in Modulo template:

The template Modulo (perlin.circom) presents a safety vulnerability that may affect to the behavior of the circuit. The template do not satisfy the weak safety property (https://www.techrxiv.org/articles/preprint/CIRCOM_A_Robust_and_Scalable_Language_for_Building_Complex_Zero-Knowledge_Circuits/19374986/1) as it accepts multiple outputs for a given input.

This template receives two inputs dividend, divisor and computes the outputs remainder and quotient expressing the result of the integer division of this values: that is, dividend = divisor * quotient + remainder with 0 <= remainder < divisor.

The template uses a call to the component LessThan(divisor_bits) to ensure that the second condition (0 <= remainder < divisor) is satisfied, but do not ensure that the conditions of the LessThan(divisor_bits) template are satisfied. The template LessThan(divisor_bits) has the expected behavior (i.e. out = in[0] < in[1]) when in[0] and in[1] are values that can be expressed using divisor_bits bits, which is not guaranteed in this case.

For example, the constraints in Modulo() for the inputs dividend = -8, divisor = 5 are satisfied by the following pairs of outputs:

Out1: remainder = 2, quotient = -2 (expected solution)
Out2: remainder = -3, quotient = -1 (buggy solution)

In order to fix this issue, we add an extra check forcing the signal remainder to be expressed using divisor_bits. We use the template Num2Bits(divisor_bits) to perform this check. The previous solution Out2 is not valid as remainder needs 254-bits to be expressed.