M3 gadget for 256-bit modular multiplication

[jimpo]

256-bit modular multiplication is an important operation to arithmetize efficiently. 256-bit multiplication modulo 2^256 would be used in EVM verification because the EVM uses 256-bit data words. More importantly 256-bit multiplication modulo a ~256-bit prime is used for ECDSA verification. We'll focus on the case of prime moduli.

To verify that C = A * B mod P, where P is a 256-bit prime, we would commit the quotient Q and check that A * B = Q * P + C and that C < P. In this way, we need to check 2 256-bit multiplications modulo 2^256.

One strategy for 256-bit multiplication is to represent the numbers with 4 64-bit limbs and apply the Karatsuba method recursively. For the 64-bit multiplications, we can use the existing MulUU64 gadget and the WideAdd gadget.

[alexeuler]

I wanted to start working on this but it looks like I might be missing something about the algorithm. For instance if I assume 3-bit modular arithmetics (R = 8) and prime P = 7 and A = 6, B = 6 then
6x6 = 1 (mod 7)

But also 6x6 = 6x7 + 2 = 4 (mod 8)

That means that if we check that A * B = Q * P + C (mod R) wouldn't necessary imply A * B = C (mod P)

Is my reasoning correct?