Skip to content

fix(r1cs): route wide shifts at the bit level - #251

Draft
NullWitnessZK wants to merge 1 commit into
circify:masterfrom
NullWitnessZK:fix/u128-variable-shift
Draft

fix(r1cs): route wide shifts at the bit level#251
NullWitnessZK wants to merge 1 commit into
circify:masterfrom
NullWitnessZK:fix/u128-variable-shift

Conversation

@NullWitnessZK

Copy link
Copy Markdown

Fixes #242.

Minimal reproducer

Save as main.pl:

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

Use:

A = 0xffffffffffffffffffffffffffffffff
B = 127

Compare the two public results:

source-correct R = 0x80000000000000000000000000000000
R1CS-accepted R  = 0x2c425bfd0001a40100000000ffffffff

At CirC 271f911, raw and optimized CircIR accept only the first value. R1CS lowering and the finalized proof relation reject it and accept the second. A fresh stock proof verifies for the wrong public result.

Expected

low128((2^128 - 1) << 127) = 2^127.

Actual

The relation computes the low 128 bits after scalar-field reduction.

Why it happens

The lowering packs the 255-bit shifted intermediate into one BLS12-381 scalar before decomposing it. The integer exceeds the scalar modulus, so it is first reduced modulo the field.

Impact: wrong relation—both soundness and completeness.

Proposed fix

fix/u128-variable-shift at e47a41b uses an LSB-first bit-routing barrel shifter and never packs the oversized intermediate into a field element.

Self-contained regression:

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

The full focused R1CS translation group passes all 18 tests, including u128 SHL, LSHR, and ASHR.

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 variable shifts wrap in the scalar field

1 participant