Safe Add and Safe Subtract

[HarryR]

For many applications there's a need for a safe add and safe subtract.

This should be an N bit number with overflow protection.

This is related to #64

[HarryR]

A bitwise magnitude comparitor could be implemented to do a bit-wise comparison of two numbers, e.g.

• https://www.electronicshub.org/digital-comparator-and-magnitude-comparator/#2-Bit_Comparator
• https://en.wikipedia.org/wiki/Digital_comparator

Division and Multiplication can be verified with a single constraint, however greater than or less than comparisons can't be performed directly on field elements.

On page 27 of https://www.csee.umbc.edu/~tinoosh/cmpe415/slides/03NumericBasics.pdf an inequality comparison circuit is defined. To compare x > y for two N bit numbers it requires about 4*N constraints if implemented on a per-gate basis, and an additional few for an or equals. Likewise with http://pami.uwaterloo.ca/~basir/ECE124/week4-2.pdf page 17 describes the same circuit.

However, this might be reducible N constraints using a 3 bit lookup table where the third bit is a chained result of the previous.

s_0 = and(x, not(y))
s_1 = or(and(s_0, eor(x_1,y_1)), and(x_1, not(y_1)))
s_2 = or(and(s_1, eor(x_2,y_2)), and(x_2, not(y_2)))
....

Where s_n = x > y

These can then be used to enforce the constraints to prevent overflows etc. similar to the safemath package for Solidity.

A binary adder/subtracter could be implemented using 2*N constraints, where one constraint selects the output bit and the other selects the carry flag, with an additional constraint to verify the carry flag is zero (preventing overflow).

[HarryR]

The other option is having a 'safe subtract N from A then add N to B' gadget, used to perform a transfer of value from one person to another (or to accumulate the fees).

c = A-N
d = B+N

This would require two gadgets, one to verify that N>=A and one to ensure that B+N != overflow, but is there any cheaper way of doing this?

When adding two N bit numbers, the result will be at most a N+1 bit number. If the MSB of the N+1 bit number is 1, then there has been an overflow. However, this requires an additional N+2 constraints to sum the result then convert back into bits, then ensure that the highest bit is zero.

The easiest way to implement overflow detection is to implement a full adder which only outputs the carry flag as a 3-bit lookup table. Where if the final output (carry bit) is 1 then there's been an overflow. This requires 2*N constraints for two N bit numbers. (one for the 3bit window, one for the selector for each bit).

[HarryR]

To verify overflowing the naive way by verifying the N+1th bit of the sum is zero:

Take two N bit numbers, A and B.

• Verify A is N bits, via packer
• Verify B is N bits, via packer
• Verify A+B == C
• Verify C is N+1 bits via packer
• Ensure the N+1th bit is 0

This requires the following constraints:

• N * bitness for A
• N * bitness for B
• pack(A_bits) = A
• pack(B_bits) = B
• A+B=C
• N+1 * bitness for C
• pack(C_bits) = C
• ensure N+1th bit of C is zero.

Which is 3*N + 6 constraints.

For two 32 bit numbers, this is 102 constraints.

Assuming the bitness constraints have already been enforced elsewhere, as have the pack(A_bits)=A and pack(B_bits)=B constraints, then this only requires N+4 constraints for the overflow check.

Using the 3 bit lookup table requires more constraints because each lookup requires an additional constraint for the AND operation.

[barryWhiteHat]

Say we want to add a number a and b. We can require the witness to provide us with a_b , b_b which are binary representations of a and b. We can then pack them into a field elements.

We know that a + b = c that c will be at most max(len(a), len(b)) +1 bits. So if we make sure that c_b is less than 252 we don't need to worry about overflow. We can do that by ensuring that both a_b and b_b are less than 252 bits in length.