Skip to content

Commit

Permalink
Fix arith machine for bus linker mode (#2297)
Browse files Browse the repository at this point in the history
  • Loading branch information
leonardoalt authored Jan 2, 2025
1 parent fc2426d commit ce673bb
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 6 deletions.
1 change: 0 additions & 1 deletion .github/workflows/nightly_tests_list.txt
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,5 @@ test(=sum) |
test(=trivial) |
test(=two_sums_serde) |
test(=zero_with_values) |
test(=arith_large_test) |
(package(powdr-riscv) and test(=evm)) |
(package(powdr-riscv) and test(=features))
19 changes: 14 additions & 5 deletions std/machines/large_field/arith.asm
Original file line number Diff line number Diff line change
Expand Up @@ -182,12 +182,21 @@ machine Arith with
*
*****/

link => byte2.check(sum(16, |i| x1[i] * CLK32[i]) + sum(16, |i| y1[i] * CLK32[16 + i]));
link => byte2.check(sum(16, |i| x2[i] * CLK32[i]) + sum(16, |i| y2[i] * CLK32[16 + i]));
link => byte2.check(sum(16, |i| x3[i] * CLK32[i]) + sum(16, |i| y3[i] * CLK32[16 + i]));
// sum0 (and the others) used to be inlined inside `byte2.check(...)`,
// but that causes an issue in the bus linker mode due to the expressions
// being copied syntactically before resolving the closures.
// Moving these expressions out of the link fixes it.
let sum0 = sum(16, |i| x1[i] * CLK32[i]) + sum(16, |i| y1[i] * CLK32[16 + i]);
link => byte2.check(sum0);
let sum1 = sum(16, |i| x2[i] * CLK32[i]) + sum(16, |i| y2[i] * CLK32[16 + i]);
link => byte2.check(sum1);
let sum2 = sum(16, |i| x3[i] * CLK32[i]) + sum(16, |i| y3[i] * CLK32[16 + i]);
link => byte2.check(sum2);
// Note that for q0-q2, we only range-constrain the first 15 limbs here
link => byte2.check(sum(16, |i| s[i] * CLK32[i]) + sum(15, |i| q0[i] * CLK32[16 + i]));
link => byte2.check(sum(15, |i| q1[i] * CLK32[i]) + sum(15, |i| q2[i] * CLK32[16 + i]));
let sum3 = sum(16, |i| s[i] * CLK32[i]) + sum(15, |i| q0[i] * CLK32[16 + i]);
link => byte2.check(sum3);
let sum4 = sum(15, |i| q1[i] * CLK32[i]) + sum(15, |i| q2[i] * CLK32[16 + i]);
link => byte2.check(sum4);

// The most significant limbs of q0-q2 are constrained to be 32 bits
// In Polygon's version they are 19 bits, but that requires increasing the minimum degree
Expand Down

0 comments on commit ce673bb

Please sign in to comment.