Lower constraint degree for 256-Bit arithmetic machine (#2110)

This PR reduces the constraint degree of the 256-Bit arithmetic machines from 4 to 3, making it possible to create Plonky3 proofs. As explained in the comments, the current way to do it is not optimal, because it adds roughly 256 witness columns. There would be an alternative that only adds 5, but witgen doesn't currently work for that. This is a comparison for `test_data/std/arith256_memory_large_test.asm`: | Metric | `main` | `fix-arith` | |-------------------------------|--------|-------------| | Fixed columns (arith) | 32 | 32 | | Witness columns (arith) | 195 | 443 | | Number of constraints (arith) | 234 | 482 | | Max constraint degree | 4 | 3 | | Time witgen (BN254) | 12.18s | 22.17s | | Time witgen (GL) | 5.24s | 7.26s | | Halo2-Composite proof time | 0.91s | 1.65s | | Plonky3 proof time | N/A | 0.38s |
powdr-labs · Dec 4, 2024 · b96f32e · b96f32e
1 parent 06d7b6b
commit b96f32e
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 23 deletions.
diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs
@@ -129,20 +129,14 @@ fn arith_small_test() {
 #[ignore = "Too slow"]
 fn arith_large_test() {
     let f = "std/arith_large_test.asm";
-    let pipeline: Pipeline<GoldilocksField> = make_simple_prepared_pipeline(f);
-    test_mock_backend(pipeline);
-    // TODO We can't use P3 yet for this test because of degree 4 constraints.
-    //test_plonky3_with_backend_variant::<BabyBearField>(f, vec![], BackendVariant::Monolithic);
+    regular_test_gl(f, &[]);
 }
 
 #[test]
 #[ignore = "Too slow"]
 fn arith256_memory_large_test() {
     let f = "std/arith256_memory_large_test.asm";
-    let pipeline: Pipeline<GoldilocksField> = make_simple_prepared_pipeline(f);
-    test_mock_backend(pipeline);
-    // TODO We can't use P3 yet for this test because of degree 4 constraints.
-    //test_plonky3_with_backend_variant::<BabyBearField>(f, vec![], BackendVariant::Monolithic);
+    regular_test_gl(f, &[]);
 }
 
 #[test]

diff --git a/std/machines/large_field/arith.asm b/std/machines/large_field/arith.asm
@@ -220,7 +220,15 @@ machine Arith with
     /// returns a(0) * b(0) + ... + a(n - 1) * b(n - 1)
     let dot_prod = |n, a, b| sum(n, |i| a(i) * b(i));
     /// returns |n| a(0) * b(n) + ... + a(n) * b(0)
-    let product = |a, b| |n| dot_prod(n + 1, a, |i| b(n - i));
+    let product = constr |a, b| constr |n| {
+        // TODO: To reduce the degree of the constraints, we materialize the intermediate result here.
+        // this introduces ~256 additional witness columns & constraints.
+        let product_res;
+        product_res = dot_prod(n + 1, a, |i| b(n - i));
+        product_res
+    };
+    // Same as `product`, but does not materialize the result. Use this to multiply by constants (like `p`).
+    let product_inline = |a, b| |n| dot_prod(n + 1, a, |i| b(n - i));
     /// Converts array to function, extended by zeros.
     let array_as_fun: expr[] -> (int -> expr) = |arr| |i| if 0 <= i && i < array::len(arr) {
         arr[i]
@@ -241,7 +249,7 @@ machine Arith with
     let q2f = array_as_fun(q2);
 
     // Defined for arguments from 0 to 31 (inclusive)
-    let eq0 = |nr|
+    let eq0 = constr |nr|
         product(x1f, y1f)(nr)
         + x2f(nr)
         - shift_right(y2f, 16)(nr)
@@ -257,17 +265,17 @@ machine Arith with
 
     // The "- 4 * shift_right(p, 16)" effectively subtracts 4 * (p << 16 * 16) = 2 ** 258 * p
     // As a result, the term computes `(x - 2 ** 258) * p`.
-    let product_with_p = |x| |nr| product(p, x)(nr) - 4 * shift_right(p, 16)(nr);
+    let product_with_p = |x| |nr| product_inline(p, x)(nr) - 4 * shift_right(p, 16)(nr);
 
-    let eq1 = |nr| product(sf, x2f)(nr) - product(sf, x1f)(nr) - y2f(nr) + y1f(nr) + product_with_p(q0f)(nr);
+    let eq1 = constr |nr| product(sf, x2f)(nr) - product(sf, x1f)(nr) - y2f(nr) + y1f(nr) + product_with_p(q0f)(nr);
 
     /*******
     *
     * EQ2:  2 * s * y1 - 3 * x1 * x1 + (q0 * p)
     *
     *******/
 
-    let eq2 = |nr| 2 * product(sf, y1f)(nr) - 3 * product(x1f, x1f)(nr) + product_with_p(q0f)(nr);
+    let eq2 = constr |nr| 2 * product(sf, y1f)(nr) - 3 * product(x1f, x1f)(nr) + product_with_p(q0f)(nr);
 
     /*******
     *
@@ -278,7 +286,7 @@ machine Arith with
     // If we're doing the ec_double operation (selEq[2] == 1), x2 is so far unconstrained and should be set to x1
     array::new(16, |i| selEq[2] * (x1[i] - x2[i]) = 0);
 
-    let eq3 = |nr| product(sf, sf)(nr) - x1f(nr) - x2f(nr) - x3f(nr) + product_with_p(q1f)(nr);
+    let eq3 = constr |nr| product(sf, sf)(nr) - x1f(nr) - x2f(nr) - x3f(nr) + product_with_p(q1f)(nr);
 
 
     /*******
@@ -287,7 +295,7 @@ machine Arith with
     *
     *******/
 
-    let eq4 = |nr| product(sf, x1f)(nr) - product(sf, x3f)(nr) - y1f(nr) - y3f(nr) + product_with_p(q2f)(nr);
+    let eq4 = constr |nr| product(sf, x1f)(nr) - product(sf, x3f)(nr) - y1f(nr) - y3f(nr) + product_with_p(q2f)(nr);
 
 
     /*******
@@ -333,6 +341,9 @@ machine Arith with
     *
     *******/
 
+    // TODO: To reduce the degree of the constraints, these intermediate columns should be materialized.
+    // However, witgen doesn't work currently if we do, likely because for some operations, not all inputs are
+    // available.
     col eq0_sum = sum(32, |i| eq0(i) * CLK32[i]);
     col eq1_sum = sum(32, |i| eq1(i) * CLK32[i]);
     col eq2_sum = sum(32, |i| eq2(i) * CLK32[i]);

diff --git a/std/machines/large_field/arith256_memory.asm b/std/machines/large_field/arith256_memory.asm
@@ -351,7 +351,15 @@ machine Arith256Memory(mem: Memory) with
     /// returns a(0) * b(0) + ... + a(n - 1) * b(n - 1)
     let dot_prod = |n, a, b| sum(n, |i| a(i) * b(i));
     /// returns |n| a(0) * b(n) + ... + a(n) * b(0)
-    let product = |a, b| |n| dot_prod(n + 1, a, |i| b(n - i));
+    let product = constr |a, b| constr |n| {
+        // TODO: To reduce the degree of the constraints, we materialize the intermediate result here.
+        // this introduces ~256 additional witness columns & constraints.
+        let product_res;
+        product_res = dot_prod(n + 1, a, |i| b(n - i));
+        product_res
+    };
+    // Same as `product`, but does not materialize the result. Use this to multiply by constants (like `p`).
+    let product_inline = |a, b| |n| dot_prod(n + 1, a, |i| b(n - i));
     /// Converts array to function, extended by zeros.
     let array_as_fun: expr[] -> (int -> expr) = |arr| |i| if 0 <= i && i < array::len(arr) {
         arr[i]
@@ -372,7 +380,7 @@ machine Arith256Memory(mem: Memory) with
     let q2f = array_as_fun(q2);
 
     // Defined for arguments from 0 to 31 (inclusive)
-    let eq0 = |nr|
+    let eq0 = constr |nr|
         product(x1f, y1f)(nr)
         + x2f(nr)
         - shift_right(y2f, 16)(nr)
@@ -388,17 +396,17 @@ machine Arith256Memory(mem: Memory) with
 
     // The "- 4 * shift_right(p, 16)" effectively subtracts 4 * (p << 16 * 16) = 2 ** 258 * p
     // As a result, the term computes `(x - 2 ** 258) * p`.
-    let product_with_p = |x| |nr| product(p, x)(nr) - 4 * shift_right(p, 16)(nr);
+    let product_with_p = |x| |nr| product_inline(p, x)(nr) - 4 * shift_right(p, 16)(nr);
 
-    let eq1 = |nr| product(sf, x2f)(nr) - product(sf, x1f)(nr) - y2f(nr) + y1f(nr) + product_with_p(q0f)(nr);
+    let eq1 = constr |nr| product(sf, x2f)(nr) - product(sf, x1f)(nr) - y2f(nr) + y1f(nr) + product_with_p(q0f)(nr);
 
     /*******
     *
     * EQ2:  2 * s * y1 - 3 * x1 * x1 + (q0 * p)
     *
     *******/
 
-    let eq2 = |nr| 2 * product(sf, y1f)(nr) - 3 * product(x1f, x1f)(nr) + product_with_p(q0f)(nr);
+    let eq2 = constr |nr| 2 * product(sf, y1f)(nr) - 3 * product(x1f, x1f)(nr) + product_with_p(q0f)(nr);
 
     /*******
     *
@@ -409,7 +417,7 @@ machine Arith256Memory(mem: Memory) with
     // If we're doing the ec_double operation, x2 is so far unconstrained and should be set to x1
     array::new(16, |i| is_ec_double * (x1[i] - x2[i]) = 0);
 
-    let eq3 = |nr| product(sf, sf)(nr) - x1f(nr) - x2f(nr) - x3f(nr) + product_with_p(q1f)(nr);
+    let eq3 = constr |nr| product(sf, sf)(nr) - x1f(nr) - x2f(nr) - x3f(nr) + product_with_p(q1f)(nr);
 
 
     /*******
@@ -418,7 +426,7 @@ machine Arith256Memory(mem: Memory) with
     *
     *******/
 
-    let eq4 = |nr| product(sf, x1f)(nr) - product(sf, x3f)(nr) - y1f(nr) - y3f(nr) + product_with_p(q2f)(nr);
+    let eq4 = constr |nr| product(sf, x1f)(nr) - product(sf, x3f)(nr) - y1f(nr) - y3f(nr) + product_with_p(q2f)(nr);
 
 
     /*******
@@ -471,7 +479,10 @@ machine Arith256Memory(mem: Memory) with
     * Putting everything together
     *
     *******/
-
+
+    // TODO: To reduce the degree of the constraints, these intermediate columns should be materialized.
+    // However, witgen doesn't work currently if we do, likely because for some operations, not all inputs are
+    // available.
     col eq0_sum = sum(32, |i| eq0(i) * CLK32[i]);
     col eq1_sum = sum(32, |i| eq1(i) * CLK32[i]);
     col eq2_sum = sum(32, |i| eq2(i) * CLK32[i]);