From 6ad188ccd39f0448a80a5400b837f29812710f8f Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Thu, 29 Feb 2024 17:17:05 +0100 Subject: [PATCH] Fix Soundness Bug in Halo2 implementation --- halo2/src/circuit_builder.rs | 40 +++++++++----- halo2/src/prover.rs | 10 ++-- pipeline/src/test_util.rs | 48 ++++++++++------- pipeline/tests/pil.rs | 60 ++++++++++++++++++++- test_data/pil/lookup_with_selector.pil | 11 ++++ test_data/pil/permutation_with_selector.pil | 11 ++++ 6 files changed, 140 insertions(+), 40 deletions(-) create mode 100644 test_data/pil/lookup_with_selector.pil create mode 100644 test_data/pil/permutation_with_selector.pil diff --git a/halo2/src/circuit_builder.rs b/halo2/src/circuit_builder.rs index 6719fa26f..9213eb101 100644 --- a/halo2/src/circuit_builder.rs +++ b/halo2/src/circuit_builder.rs @@ -181,22 +181,28 @@ impl<'a, T: FieldElement, F: PrimeField> Circuit for PowdrCi meta.enable_equality(config.instance); // Add polynomial identities - meta.create_gate("main", |meta| -> Vec<(String, Expression)> { - 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::>(); + if !identities.is_empty() { + meta.create_gate("main", |meta| -> Vec<(String, Expression)> { + 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>, meta: &mut VirtualCells<'_, F>| { @@ -210,7 +216,15 @@ impl<'a, T: FieldElement, F: PrimeField> Circuit 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::>() }; diff --git a/halo2/src/prover.rs b/halo2/src/prover.rs index fd528683d..f2343466e 100644 --- a/halo2/src/prover.rs +++ b/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, circuit: C, instances: &[Vec], -) -> Vec { +) -> Result, 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) } diff --git a/pipeline/src/test_util.rs b/pipeline/src/test_util.rs index b5dda8f64..7543f67de 100644 --- a/pipeline/src/test_util.rs +++ b/pipeline/src/test_util.rs @@ -57,11 +57,10 @@ pub fn verify_pipeline(pipeline: Pipeline) -> Result<(), String } pub fn gen_estark_proof(file_name: &str, inputs: Vec) { - 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) { 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) { 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(witness: &[(String, Vec)]) -> Vec<(Stri .collect() } -fn assert_proofs_fail_for_invalid_witnesses_gl(file_name: &str, witness: &[(String, Vec)]) { - 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)], +) { let tmp_dir = mktemp::Temp::new_dir().unwrap(); let pipeline = Pipeline::::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)], +) { + let pipeline = Pipeline::::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)]) { - 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)], +) { let pipeline = Pipeline::::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)], ) { } pub fn assert_proofs_fail_for_invalid_witnesses(file_name: &str, witness: &[(String, Vec)]) { - 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); } diff --git a/pipeline/tests/pil.rs b/pipeline/tests/pil.rs index 4da1db798..680294a68 100644 --- a/pipeline/tests/pil.rs +++ b/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"; diff --git a/test_data/pil/lookup_with_selector.pil b/test_data/pil/lookup_with_selector.pil new file mode 100644 index 000000000..aef00d688 --- /dev/null +++ b/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}; diff --git a/test_data/pil/permutation_with_selector.pil b/test_data/pil/permutation_with_selector.pil new file mode 100644 index 000000000..cc8a513c3 --- /dev/null +++ b/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};