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.
Minimal reproducer
Save as
main.pl:Use:
Compare the two public results:
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-shiftate47a41buses 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::testThe full focused R1CS translation group passes all 18 tests, including
u128SHL, LSHR, and ASHR.