fixing template ModSubThree

[clararod9]

Template ModSubThree(n) accepts unexpected solutions when a - b - c + (1 << n) >= 0.

The template ModSubThree(n) receives three inputs a, b, c that can be expressed using n bits and performs the operation a - b - c. It returns the result of the operation using n bits (signal out), along with a signal indicating if there has been an underflow (borrow).

The condition a - b - c + (1 << n) >= 0 is introduced as an assert that is not checked at compile time as it is unknown (https://docs.circom.io/circom-language/code-quality/code-assertion/). The assert is only included in the witness generation code but it is not added to the constraint system describing the circuit, which may generate unexpected behaviors.

For example, for n = 3, the constraints of ModSubThree(3) for the inputs a = 0, b = 7, c = 7 are satisfied by the output borrow = 1, out = -6. However, this solution does not satisfy the specification of the circuit as out cannot be expressed using 3 bits.

The proposed fix incorporates the check a - b - c + (1 << n) >= 0 to the constraint system without adding extra constraints (same number of non-linear constraints, less linear constraints) by using a call to Num2Bits to both compute the value of borrow and perform this check.