u128 division admits spurious quotient and remainder witnesses

[NullWitnessZK]

Minimal reproducer

Unsigned division:

main(A: private u128, B: private u128, R: public u128) :-
    A / B = R.

Unsigned remainder uses the same trigger with A % B = R.

Choose:

A = 1
B = 0x80000000000000000000000000000000  # 2^127

Source semantics require:

quotient  = 0
remainder = 1

But the R1CS also admits the quotient/remainder obtained by dividing A + p by B:

q' = 0xe7db4ea6533afa906673b0101343b00a
r' = 0x53bda402fffe5bfeffffffff00000002

These values are individually within 128 bits and satisfy q' * B + r' = A + p, so they satisfy the current relation modulo p even though they are not the source result.

Expected

Only (q, r) = (0, 1) is accepted.

Actual

A custom witness using (q', r') satisfies all 651 pre- and post-reduction constraints. The normal witness computation still produces the correct pair, so exploitation requires a custom witness.

Why it happens

The gadget constrains q * B == A - r in the scalar field. For u128, q * B can exceed the modulus, making this a modular rather than integer equality.

Impact: custom-witness underconstraint/soundness.

Proposed fix

fix/u128-divmod-field-wrap at 032a74a implements unsigned restoring division over bit wires, including bitwise subtraction and borrow propagation.

Self-contained regression:

cargo test --features r1cs target::r1cs::trans::test

All 18 focused R1CS translation tests pass.