Minimal reproducer
Save as main.pl:
main(A: private u128, B: private u128, R: public u128) :-
A * B = R.
Use:
A = 0xffffffffffffffffffffffffffffffff
B = 0xffffffffffffffffffffffffffffffff
The two results are:
source: low128(A * B) = 0x00000000000000000000000000000001
R1CS: low128((A * B) mod p) = 0x5884b7fa0003480200000001ffffffff
At CirC 271f911, the raw evaluator accepts the source result and rejects the second. The R1CS and stock witness computation do the opposite.
A sibling trigger exercises wide addition:
main(A: private u255, B: private u255, R: public u255) :-
A + B = R.
For A = B = 2^254, source semantics return 0 mod 2^255, while the circuit returns 2^255 - p.
Why it happens
When the intermediate is too wide, multiplication/addition is still performed in the scalar field and only then bit-decomposed and truncated. Field reduction therefore occurs before bit-vector reduction.
Impact: wrong relation; the bundled witness computation follows the wrong result.
Proposed fix
fix/u128-mul-field-wrap at c08defc keeps the scalar fast path only when the intermediate is provably below the modulus. Otherwise it uses ripple-carry addition and shifted partial products over bit wires.
Self-contained regression:
cargo test --features r1cs target::r1cs::trans::test
All 18 focused R1CS translation tests pass.
Minimal reproducer
Save as
main.pl:Use:
The two results are:
At CirC
271f911, the raw evaluator accepts the source result and rejects the second. The R1CS and stock witness computation do the opposite.A sibling trigger exercises wide addition:
For
A = B = 2^254, source semantics return0 mod 2^255, while the circuit returns2^255 - p.Why it happens
When the intermediate is too wide, multiplication/addition is still performed in the scalar field and only then bit-decomposed and truncated. Field reduction therefore occurs before bit-vector reduction.
Impact: wrong relation; the bundled witness computation follows the wrong result.
Proposed fix
fix/u128-mul-field-wrapatc08defckeeps the scalar fast path only when the intermediate is provably below the modulus. Otherwise it uses ripple-carry addition and shifted partial products over bit wires.Self-contained regression:
cargo test --features r1cs target::r1cs::trans::testAll 18 focused R1CS translation tests pass.