Merge pull request #1108 from powdr-labs/fix-halo2-soundness-bug

Fix Soundness Bug in Halo2 implementation

halo2/src/circuit_builder.rs

@@ -181,22 +181,28 @@ impl<'a, T: FieldElement, F: PrimeField<Repr = [u8; 32]>> Circuit<F> for PowdrCi
         meta.enable_equality(config.instance);
 
         // Add polynomial identities
-        meta.create_gate("main", |meta| -> Vec<(String, Expression<F>)> {
-            analyzed
-                .identities_with_inlined_intermediate_polynomials()
-                .iter()
-                .filter_map(|id| match id.kind {
-                    IdentityKind::Polynomial => {
+        let identities = analyzed
+            .identities_with_inlined_intermediate_polynomials()
+            .into_iter()
+            .filter(|id| id.kind == IdentityKind::Polynomial)
+            .collect::<Vec<_>>();
+        if !identities.is_empty() {
+            meta.create_gate("main", |meta| -> Vec<(String, Expression<F>)> {
+                identities
+                    .iter()
+                    .map(|id| {
                         let expr = id.expression_for_poly_id();
                         let name = id.to_string();
                         let expr = to_halo2_expression(expr, &config, meta);
                         let expr = expr * meta.query_fixed(config.enable, Rotation::cur());
-                        Some((name, expr))
-                    }
-                    _ => None,
-                })
-                .collect()
-        });
+                        (name, expr)
+                    })
+                    .collect()
+            });
+        }
+
+        // Challenge used to combine the lookup tuple with the selector
+        let beta = Expression::Challenge(meta.challenge_usable_after(FirstPhase));
 
         let to_lookup_tuple = |expr: &SelectedExpressions<AlgebraicExpression<T>>,
                                meta: &mut VirtualCells<'_, F>| {
@@ -210,7 +216,15 @@ impl<'a, T: FieldElement, F: PrimeField<Repr = [u8; 32]>> Circuit<F> for PowdrCi
 
             expr.expressions
                 .iter()
-                .map(|expr| selector.clone() * to_halo2_expression(expr, &config, meta))
+                .map(|expr| {
+                    let expr = to_halo2_expression(expr, &config, meta);
+                    // Turns a selected lookup / permutation argument into an unselected lookup / permutation argument,
+                    // see Section 3.3, equation (24) of: https://eprint.iacr.org/2023/474.pdf
+                    // Note that they use a different transformation for lookups, because this transformation would fail
+                    // if the RHS selector was 1 on all rows (and not on the LHS). This is never the case for us though,
+                    // because we multiply with the __enable column!
+                    selector.clone() * (expr - beta.clone()) + beta.clone()
+                })
                 .collect::<Vec<_>>()
         };
 

halo2/src/prover.rs

@@ -110,7 +110,7 @@ impl<'a, F: FieldElement> Halo2Prover<'a, F> {
             &pk,
             circuit,
             &publics,
-        );
+        )?;
 
         let duration = start.elapsed();
         log::info!("Time taken: {:?}", duration);
@@ -182,7 +182,7 @@ impl<'a, F: FieldElement> Halo2Prover<'a, F> {
             &pk_aggr,
             agg_circuit_with_proof.clone(),
             &agg_circuit_with_proof.instances(),
-        );
+        )?;
         let duration = start.elapsed();
         log::info!("Time taken: {:?}", duration);
 
@@ -294,7 +294,7 @@ fn gen_proof<
     pk: &ProvingKey<G1Affine>,
     circuit: C,
     instances: &[Vec<Fr>],
-) -> Vec<u8> {
+) -> Result<Vec<u8>, String> {
     let instances = instances
         .iter()
         .map(|instances| instances.as_slice())
@@ -309,9 +309,9 @@ fn gen_proof<
             OsRng,
             &mut transcript,
         )
-        .unwrap();
+        .map_err(|e| e.to_string())?;
         transcript.finalize()
     };
 
-    proof
+    Ok(proof)
 }

pipeline/src/test_util.rs

@@ -57,11 +57,10 @@ pub fn verify_pipeline(pipeline: Pipeline<GoldilocksField>) -> Result<(), String
 }
 
 pub fn gen_estark_proof(file_name: &str, inputs: Vec<GoldilocksField>) {
-    let file_name = format!("{}/../test_data/{file_name}", env!("CARGO_MANIFEST_DIR"));
     let tmp_dir = mktemp::Temp::new_dir().unwrap();
     Pipeline::default()
         .with_tmp_output(&tmp_dir)
-        .from_file(PathBuf::from(file_name))
+        .from_file(resolve_test_file(file_name))
         .with_prover_inputs(inputs)
         .with_backend(powdr_backend::BackendType::EStark)
         .compute_proof()
@@ -73,9 +72,8 @@ pub fn test_halo2(file_name: &str, inputs: Vec<Bn254Field>) {
     use std::env;
 
     // Generate a mock proof (fast and has good error messages)
-    let full_file_name = format!("{}/../test_data/{file_name}", env!("CARGO_MANIFEST_DIR"));
     Pipeline::default()
-        .from_file(PathBuf::from(full_file_name))
+        .from_file(resolve_test_file(file_name))
         .with_prover_inputs(inputs.clone())
         .with_backend(powdr_backend::BackendType::Halo2Mock)
         .compute_proof()
@@ -100,11 +98,10 @@ pub fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
 
     use crate::util::write_or_panic;
 
-    let file_name = format!("{}/../test_data/{file_name}", env!("CARGO_MANIFEST_DIR"));
     let tmp_dir = mktemp::Temp::new_dir().unwrap();
     let mut pipeline = Pipeline::default()
         .with_tmp_output(&tmp_dir)
-        .from_file(PathBuf::from(file_name))
+        .from_file(resolve_test_file(file_name))
         .with_prover_inputs(inputs)
         .with_backend(powdr_backend::BackendType::Halo2);
 
@@ -191,13 +188,25 @@ fn convert_witness<T: FieldElement>(witness: &[(String, Vec<u64>)]) -> Vec<(Stri
         .collect()
 }
 
-fn assert_proofs_fail_for_invalid_witnesses_gl(file_name: &str, witness: &[(String, Vec<u64>)]) {
-    let file_name = format!("{}/../test_data/{file_name}", env!("CARGO_MANIFEST_DIR"));
-
+pub fn assert_proofs_fail_for_invalid_witnesses_pilcom(
+    file_name: &str,
+    witness: &[(String, Vec<u64>)],
+) {
     let tmp_dir = mktemp::Temp::new_dir().unwrap();
     let pipeline = Pipeline::<GoldilocksField>::default()
         .with_tmp_output(&tmp_dir)
-        .from_file(PathBuf::from(file_name))
+        .from_file(resolve_test_file(file_name))
+        .set_witness(convert_witness(witness));
+
+    assert!(verify_pipeline(pipeline.clone()).is_err());
+}
+
+pub fn assert_proofs_fail_for_invalid_witnesses_estark(
+    file_name: &str,
+    witness: &[(String, Vec<u64>)],
+) {
+    let pipeline = Pipeline::<GoldilocksField>::default()
+        .from_file(resolve_test_file(file_name))
         .set_witness(convert_witness(witness));
 
     assert!(pipeline
@@ -205,17 +214,15 @@ fn assert_proofs_fail_for_invalid_witnesses_gl(file_name: &str, witness: &[(Stri
         .with_backend(powdr_backend::BackendType::EStark)
         .compute_proof()
         .is_err());
-    assert!(verify_pipeline(pipeline.clone()).is_err());
 }
 
 #[cfg(feature = "halo2")]
-fn assert_proofs_fail_for_invalid_witnesses_bn254(file_name: &str, witness: &[(String, Vec<u64>)]) {
-    let file_name = format!("{}/../test_data/{file_name}", env!("CARGO_MANIFEST_DIR"));
-
-    let tmp_dir = mktemp::Temp::new_dir().unwrap();
+pub fn assert_proofs_fail_for_invalid_witnesses_halo2(
+    file_name: &str,
+    witness: &[(String, Vec<u64>)],
+) {
     let pipeline = Pipeline::<Bn254Field>::default()
-        .with_tmp_output(&tmp_dir)
-        .from_file(PathBuf::from(file_name))
+        .from_file(resolve_test_file(file_name))
         .set_witness(convert_witness(witness));
 
     // This will panic, because Halo2's MockProver::assert_satisfied() panics if it is not.
@@ -237,13 +244,14 @@ fn assert_proofs_fail_for_invalid_witnesses_bn254(file_name: &str, witness: &[(S
 }
 
 #[cfg(not(feature = "halo2"))]
-fn assert_proofs_fail_for_invalid_witnesses_bn254(
+pub fn assert_proofs_fail_for_invalid_witnesses_bn254(
     _file_name: &str,
     _witness: &[(String, Vec<u64>)],
 ) {
 }
 
 pub fn assert_proofs_fail_for_invalid_witnesses(file_name: &str, witness: &[(String, Vec<u64>)]) {
-    assert_proofs_fail_for_invalid_witnesses_gl(file_name, witness);
-    assert_proofs_fail_for_invalid_witnesses_bn254(file_name, witness);
+    assert_proofs_fail_for_invalid_witnesses_pilcom(file_name, witness);
+    assert_proofs_fail_for_invalid_witnesses_estark(file_name, witness);
+    assert_proofs_fail_for_invalid_witnesses_halo2(file_name, witness);
 }

pipeline/tests/pil.rs

@@ -3,8 +3,10 @@ use powdr_number::Bn254Field;
 use powdr_number::GoldilocksField;
 use powdr_pipeline::{
     test_util::{
-        assert_proofs_fail_for_invalid_witnesses, gen_estark_proof, resolve_test_file, test_halo2,
-        verify_test_file,
+        assert_proofs_fail_for_invalid_witnesses, assert_proofs_fail_for_invalid_witnesses_estark,
+        assert_proofs_fail_for_invalid_witnesses_halo2,
+        assert_proofs_fail_for_invalid_witnesses_pilcom, gen_estark_proof, resolve_test_file,
+        test_halo2, verify_test_file,
     },
     Pipeline,
 };
@@ -35,6 +37,60 @@ fn test_invalid_witness_halo2mock() {
         .unwrap();
 }
 
+#[test]
+#[should_panic = "Number not included: F3G { cube: [Fr(0x0000000000000000), Fr(0x0000000000000000), Fr(0x0000000000000000)], dim: 3 }"]
+fn test_lookup_with_selector() {
+    // witness[0] and witness[2] have to be in {2, 4}
+
+    // Valid witness
+    let f = "pil/lookup_with_selector.pil";
+    let witness = [2, 42, 4, 17];
+    Pipeline::default()
+        .from_file(resolve_test_file(f))
+        .set_witness(vec![(
+            "main.w".to_string(),
+            witness.iter().cloned().map(Bn254Field::from).collect(),
+        )])
+        .with_backend(powdr_backend::BackendType::Halo2Mock)
+        .compute_proof()
+        .unwrap();
+
+    // Invalid witness: 0 is not in the set {2, 4}
+    let witness = vec![("main.w".to_string(), vec![0, 42, 4, 17])];
+    assert_proofs_fail_for_invalid_witnesses_halo2(f, &witness);
+    assert_proofs_fail_for_invalid_witnesses_pilcom(f, &witness);
+    // Unfortunately, eStark panics in this case. That's why the test is marked
+    // as should_panic, with the error message that would be coming from eStark...
+    assert_proofs_fail_for_invalid_witnesses_estark(f, &witness);
+}
+
+#[test]
+#[should_panic = "assertion failed: check_val._eq(&F::one())"]
+fn test_permutation_with_selector() {
+    // witness[0] and witness[2] have to be in {2, 4}
+
+    // Valid witness
+    let f = "pil/permutation_with_selector.pil";
+    let witness = [2, 42, 4, 17];
+    Pipeline::default()
+        .from_file(resolve_test_file(f))
+        .set_witness(vec![(
+            "main.w".to_string(),
+            witness.iter().cloned().map(Bn254Field::from).collect(),
+        )])
+        .with_backend(powdr_backend::BackendType::Halo2Mock)
+        .compute_proof()
+        .unwrap();
+
+    // Invalid witness: 0 is not in the set {2, 4}
+    let witness = vec![("main.w".to_string(), vec![0, 42, 4, 17])];
+    assert_proofs_fail_for_invalid_witnesses_halo2(f, &witness);
+    assert_proofs_fail_for_invalid_witnesses_pilcom(f, &witness);
+    // Unfortunately, eStark panics in this case. That's why the test is marked
+    // as should_panic, with the error message that would be coming from eStark...
+    assert_proofs_fail_for_invalid_witnesses_estark(f, &witness);
+}
+
 #[test]
 fn test_fibonacci() {
     let f = "pil/fibonacci.pil";

test_data/pil/lookup_with_selector.pil

@@ -0,0 +1,11 @@
+constant %N = 4;
+
+namespace main(%N);
+    col witness w;
+    col fixed s_w = [1, 0]*;
+
+    // t is essentially {2, 4}
+    col fixed t = [1, 2, 3, 4]*;
+    col fixed s_t = [0, 1]*;
+
+    s_w {w} in s_t {t};

test_data/pil/permutation_with_selector.pil

@@ -0,0 +1,11 @@
+constant %N = 4;
+
+namespace main(%N);
+    col witness w;
+    col fixed s_w = [1, 0]*;
+
+    // t is essentially {2, 4}
+    col fixed t = [1, 2, 3, 4]*;
+    col fixed s_t = [0, 1]*;
+
+    s_w {w} is s_t {t};