poly: add formal proof documentation to poly.add lowering about heir HOT 4 CLOSED

Here's the poly.add lowering. For x, y inputs to the addition, with coefficient modulus mod and bit width B =2^N in the case that mod does not divide B.

c1, n1 = addui_extended(x, y)
c0 = [c1 % mod] + [n1 * (B % mod)] % mod

Is it possible that the following sum overflows mod 2^N?
[c1 % mod] + [n1 * (B % mod)]

The answer is no. If that were to happen, then

[[(x + y) % B] % mod] + [B % mod] > B

Note both left operands are less than mod. So if this were true, then

mod > B/2

(strictly greater because it does not divide it).

If so, then

[B % mod] < B/2

Which would imply that

[[(x + y) % B] % mod] >  B/2

But this is impossible because mod < B/2

cc @j2kun

from heir.

Why is mod < B/2 ? I can imagine a (maybe bizarre) case in which the ring is Z/pZ, where p is a prime of the form 2^N - 1, and N is the bit width of the container.

I don't think any of the Mersenne primes align with powers of two, so that's why this case is kind of bizarre. But 2^32 - 5 is prime, as is 2^32 - 17 (see https://t5k.org/lists/2small/0bit.html)

from heir.

It's derived from the assumption that the sum overflows (which reaches a contradiction)

[B % mod] < B/2

from heir.

@j2kun 's correction

Following mod > B/2, B % mod = B - mod

[[(x + y) % B] % mod] + [B % mod] > B
[[(x + y) % B] % mod] > mod

from heir.