Skip to content

fix(r1cs): lower unsafe wide arithmetic bitwise - #253

Draft
NullWitnessZK wants to merge 1 commit into
circify:masterfrom
NullWitnessZK:fix/u128-mul-field-wrap
Draft

fix(r1cs): lower unsafe wide arithmetic bitwise#253
NullWitnessZK wants to merge 1 commit into
circify:masterfrom
NullWitnessZK:fix/u128-mul-field-wrap

Conversation

@NullWitnessZK

Copy link
Copy Markdown

Fixes #245.

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Wide bit-vector arithmetic wraps before truncation

1 participant