Fix soundness bug in conversion to Halo2

powdr-labs · Feb 8, 2024 · 5e16a94 · 5e16a94
1 parent b67641f
commit 5e16a94
Show file tree

Hide file tree

Showing 5 changed files with 53 additions and 59 deletions.
diff --git a/halo2/src/circuit_builder.rs b/halo2/src/circuit_builder.rs
@@ -19,6 +19,19 @@ use powdr_number::{BigInt, FieldElement};
 
 use super::circuit_data::CircuitData;
 
+fn convert_column<T: FieldElement>(column: &Vec<T>) -> Vec<Option<BigUint>> {
+    // Convert T -> Option<BigInt>
+    let mut column = column
+        .iter()
+        .map(|value| Some(value.to_arbitrary_integer()))
+        .collect::<Vec<_>>();
+
+    // Repeat the first row
+    column.push(column[0].clone());
+
+    column
+}
+
 /// Converts an analyzed PIL and fixed to a Plaf circuit.
 /// A Plaf circuit only contains the shape of the circuit.
 pub(crate) fn analyzed_to_plaf<T: FieldElement>(
@@ -27,39 +40,31 @@ pub(crate) fn analyzed_to_plaf<T: FieldElement>(
 ) -> Plaf {
     // The structure of the table is as following
     //
-    // | constant columns | __enable_cur | __enable_next |  witness columns | \
-    // |  c[0]            |    1         |       1       |   w[0]           |  |
-    // |  c[1]            |    1         |       1       |   w[1]           |  |>  N actual circuit rows
-    // |  ...             |   ...        |      ...      |   ...            |  |
-    // |  c[N - 2]        |    1         |       1       |   w[N - 2]       |  |
-    // |  c[N - 1]        |    1         |       0       |   w[N - 1]       | /     <- __enable_next == 0 since there's no state transition
-    // |  0               |    0         |       0       |   0              | \
-    // |  0               |    0         |       0       |   0              |  |
-    // |  ...             |   ...        |      ...      |   ...            |  |>  (2**(ceil(log2(N)) + 1) - N) padding rows to fit the halo2 unusable rows
-    // |  0               |    0         |       0       |   0              |  |
-    // |  0               |    0         |       0       |   <unusable>     |  |
-    // |  0               |    0         |       0       |   <unusable>     | /
+    // | constant columns | __enable     |  witness columns | \
+    // |  c[0]            |    1         |   w[0]           |  |
+    // |  c[1]            |    1         |   w[1]           |  |>  N actual circuit rows
+    // |  ...             |   ...        |   ...            |  |
+    // |  c[N - 2]        |    1         |   w[N - 2]       |  |
+    // |  c[N - 1]        |    1         |   w[N - 1]       | /
+    // |  c[0]            |    0         |   w[0]           | \  <-- Row 0 is copy-constrained to row N
+    // |  0               |    0         |   0              |  |
+    // |  ...             |   ...        |   ...            |  |>  2**(ceil(log2(N)) padding rows to fit the halo2 unusable rows
+    // |  0               |    0         |   0              |  |
+    // |  0               |    0         |   <unusable>     |  |
+    // |  0               |    0         |   <unusable>     | /
 
     // generate fixed and witness (witness).
 
     let query = |column, rotation| Expr::Var(PlonkVar::Query(ColumnQuery { column, rotation }));
 
     let mut cd = CircuitData::from(analyzed, fixed.to_owned());
 
-    // append two fixed columns:
-    // - one that enables constraints that do not have rotations (__enable_cur) in the actual circuit
-    // - and another that enables constraints that have a rotation (__enable_next) in the actual circuit except in the last actual row
-
-    let num_rows: usize = analyzed.degree() as usize;
+    let num_rows: usize = analyzed.degree() as usize + 1;
 
-    let q_enable_cur = query(
-        cd.insert_constant("__enable_cur", itertools::repeat_n(T::from(1), num_rows)),
-        0,
-    );
-
-    let q_enable_next = query(
+    // Append __enable fixed column
+    let q_enable = query(
         cd.insert_constant(
-            "__enable_next",
+            "__enable",
             itertools::repeat_n(T::from(1), num_rows - 1).chain(std::iter::once(T::from(0))),
         ),
         0,
@@ -106,16 +111,7 @@ pub(crate) fn analyzed_to_plaf<T: FieldElement>(
                 expression_2_expr(&cd, &expr)
             });
 
-        let contains_next_ref = set.expressions.iter().any(|exp| exp.contains_next_ref());
-
-        let selector = Expr::Mul(vec![
-            selector,
-            if contains_next_ref {
-                q_enable_next.clone()
-            } else {
-                q_enable_cur.clone()
-            },
-        ]);
+        let selector = Expr::Mul(vec![selector, q_enable.clone()]);
 
         set.expressions
             .iter()
@@ -134,21 +130,12 @@ pub(crate) fn analyzed_to_plaf<T: FieldElement>(
                 assert_eq!(id.left.expressions.len(), 0);
 
                 let exp = id.expression_for_poly_id();
-                let contains_next_ref = exp.contains_next_ref();
-
                 let exp = expression_2_expr(&cd, exp);
 
                 // depending whether this polynomial contains a rotation,
                 // enable for all rows or all except the last one.
 
-                let exp = Expr::Mul(vec![
-                    exp,
-                    if contains_next_ref {
-                        q_enable_next.clone()
-                    } else {
-                        q_enable_cur.clone()
-                    },
-                ]);
+                let exp = Expr::Mul(vec![exp, q_enable.clone()]);
                 polys.push(Poly {
                     name: "".to_string(),
                     exp,
@@ -190,11 +177,7 @@ pub(crate) fn analyzed_to_plaf<T: FieldElement>(
     let fixed: Vec<Vec<_>> = cd
         .fixed
         .iter()
-        .map(|(_, row)| {
-            row.iter()
-                .map(|value| Some(value.to_arbitrary_integer()))
-                .collect()
-        })
+        .map(|(_, column)| convert_column(column))
         .collect();
 
     Plaf {
@@ -210,6 +193,8 @@ pub(crate) fn analyzed_to_plaf<T: FieldElement>(
 }
 
 fn copy_constraints<T: FieldElement>(pil: &Analyzed<T>, cd: &CircuitData<T>) -> Vec<CopyC> {
+    let mut copies = vec![];
+
     // Enforce publics by copy-constraining to cells in the instance column.
     // For example, if we have the following public declarations:
     // - public out1 = A(2);
@@ -222,7 +207,6 @@ fn copy_constraints<T: FieldElement>(pil: &Analyzed<T>, cd: &CircuitData<T>) ->
     // |  1  |  1  |  6  |  *5*   |
     // |  2  | *2* |  7  |        |
     // |  3  |  4  |  8  |        |
-    let mut copies = vec![];
     for public_declaration in pil.public_declarations.values() {
         let witness_name = public_declaration.referenced_poly_name();
         let witness_col = cd.col(&witness_name);
@@ -239,6 +223,19 @@ fn copy_constraints<T: FieldElement>(pil: &Analyzed<T>, cd: &CircuitData<T>) ->
         });
     }
 
+    // Also, copy row 0 to row N.
+    for (poly_name, _) in pil
+        .committed_polys_in_source_order()
+        .into_iter()
+        .flat_map(|(p, _)| p.array_elements())
+    {
+        let witness_col = cd.col(&poly_name);
+        copies.push(CopyC {
+            columns: (witness_col, witness_col),
+            offsets: vec![(0, pil.degree() as usize)],
+        });
+    }
+
     copies
 }
 
@@ -318,11 +315,7 @@ pub(crate) fn analyzed_to_circuit_with_witness<T: FieldElement>(
 
     let converted_witness: Vec<Vec<_>> = witness
         .iter()
-        .map(|(_, row)| {
-            row.iter()
-                .map(|value| Some(value.to_arbitrary_integer()))
-                .collect()
-        })
+        .map(|(_, column)| convert_column(column))
         .collect();
 
     let wit = Witness {

diff --git a/halo2/src/mock_prover.rs b/halo2/src/mock_prover.rs
@@ -26,6 +26,7 @@ pub fn mock_prove<T: FieldElement>(
     let expanded_row_count_log = circuit_row_count_log + 1;
 
     log::debug!("{}", PlafDisplayBaseTOML(&circuit.plaf));
+    println!("Fixed len: {}", circuit.plaf.fixed[0].len());
 
     let mock_prover = MockProver::<Fr>::run(expanded_row_count_log, &circuit, publics).unwrap();
     mock_prover.assert_satisfied();

diff --git a/test_data/asm/full_pil_constant.asm b/test_data/asm/full_pil_constant.asm
@@ -1,5 +1,5 @@
 machine FullConstant {
-	degree 2;
+	degree 4;
 
 	pol constant C = [0, 1]*;
 	col commit w;

diff --git a/test_data/asm/pil_at_module_level.asm b/test_data/asm/pil_at_module_level.asm
@@ -24,7 +24,7 @@ mod R {
     use super::utils::make_array;
 
     machine FullConstant {
-        degree 2;
+        degree 4;
 
         let C: int -> fe = |i| match i % 2 {
             0 => x,

diff --git a/test_data/pil/halo_without_lookup.pil b/test_data/pil/halo_without_lookup.pil
@@ -1,5 +1,5 @@
 // There is a bug in halo2 that makes it fail if we do not have at least one lookup.
-namespace Assembly(2);
-    col fixed C = [0, 1];
+namespace Assembly(4);
+    col fixed C = [0, 1, 2, 3];
     col witness w;
     w = C;