From d7c6279d6d9fe7904ac6e50beae51ba17e7b02d8 Mon Sep 17 00:00:00 2001 From: guorong009 Date: Mon, 17 Jun 2024 21:33:16 +0800 Subject: [PATCH] feat: add assertion for dynamic lookup (#347) * feat: improve the "lookup_any" assertion checks * feat: add new feature "lookup-any-sanity-checks" * doc: add comments for new feature checks --- .github/scripts/wasm-target-test-build.sh | 2 +- .github/workflows/ci.yml | 2 +- halo2_frontend/Cargo.toml | 3 +- halo2_frontend/src/dev.rs | 417 ++++++++++++++++-- .../src/plonk/circuit/constraint_system.rs | 40 ++ .../src/plonk/circuit/expression.rs | 37 ++ halo2_proofs/Cargo.toml | 3 +- 7 files changed, 458 insertions(+), 46 deletions(-) diff --git a/.github/scripts/wasm-target-test-build.sh b/.github/scripts/wasm-target-test-build.sh index c8fa0371cd..eb486aed8e 100755 --- a/.github/scripts/wasm-target-test-build.sh +++ b/.github/scripts/wasm-target-test-build.sh @@ -15,7 +15,7 @@ cp "${GIT_ROOT}/rust-toolchain" . rustup target add wasm32-unknown-unknown wasm32-wasi # add dependencies -cargo add --path "${GIT_ROOT}/halo2_proofs" --features batch,dev-graph,gadget-traces +cargo add --path "${GIT_ROOT}/halo2_proofs" --features batch,dev-graph,gadget-traces,lookup-any-sanity-checks cargo add getrandom --features js --target wasm32-unknown-unknown # test build for wasm32-* targets diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 558785df5a..d3d0ce27d0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -19,7 +19,7 @@ jobs: - feature_set: basic features: batch,dev-graph,gadget-traces - feature_set: all - features: batch,dev-graph,gadget-traces,test-dev-graph,thread-safe-region,sanity-checks,circuit-params + features: batch,dev-graph,gadget-traces,test-dev-graph,thread-safe-region,sanity-checks,circuit-params,lookup-any-sanity-checks steps: - uses: actions/checkout@v3 diff --git a/halo2_frontend/Cargo.toml b/halo2_frontend/Cargo.toml index 3714c7dca7..f9627bac28 100644 --- a/halo2_frontend/Cargo.toml +++ b/halo2_frontend/Cargo.toml @@ -48,7 +48,7 @@ serde_json = "1" getrandom = { version = "0.2", features = ["js"] } [features] -default = ["bits"] +default = ["bits", "lookup-any-sanity-checks"] dev-graph = ["plotters", "tabbycat"] test-dev-graph = [ "dev-graph", @@ -63,6 +63,7 @@ circuit-params = [] heap-profiling = [] cost-estimator = ["serde", "serde_derive"] derive_serde = ["halo2curves/derive_serde"] +lookup-any-sanity-checks = [] [lib] bench = false diff --git a/halo2_frontend/src/dev.rs b/halo2_frontend/src/dev.rs index f6cc12ce82..bdea7ec883 100644 --- a/halo2_frontend/src/dev.rs +++ b/halo2_frontend/src/dev.rs @@ -1336,7 +1336,7 @@ mod tests { } #[test] - fn bad_lookup_any() { + fn bad_lookup_any_faulty_synthesis() { const K: u32 = 4; #[derive(Clone)] @@ -1345,6 +1345,7 @@ mod tests { table: Column, advice_table: Column, q: Selector, + s_ltable: Selector, } struct FaultyCircuit {} @@ -1360,6 +1361,7 @@ mod tests { let q = meta.complex_selector(); let table = meta.instance_column(); let advice_table = meta.advice_column(); + let s_ltable = meta.complex_selector(); meta.annotate_lookup_any_column(table, || "Inst-Table"); meta.enable_equality(table); @@ -1371,17 +1373,14 @@ mod tests { let q = cells.query_selector(q); let advice_table = cells.query_advice(advice_table, Rotation::cur()); let table = cells.query_instance(table, Rotation::cur()); + let s_ltable = cells.query_selector(s_ltable); // If q is enabled, a must be in the table. - // When q is not enabled, lookup the default value instead. - let not_q = Expression::Constant(Fp::one()) - q.clone(); - let default = Expression::Constant(Fp::from(2)); + // If `s_ltable` is enabled, the value of `advice_table` & `table` is used as lookup table. vec![ - ( - q.clone() * a.clone() + not_q.clone() * default.clone(), - table, - ), - (q * a + not_q * default, advice_table), + (q.clone() * a.clone(), table * s_ltable.clone()), + (q.clone() * a, advice_table * s_ltable.clone()), + (q, s_ltable), ] }); @@ -1390,6 +1389,7 @@ mod tests { q, table, advice_table, + s_ltable, } } @@ -1402,15 +1402,9 @@ mod tests { config: Self::Config, mut layouter: impl Layouter, ) -> Result<(), Error> { - // No assignment needed for the table as is an Instance Column. - layouter.assign_region( - || "Good synthesis", + || "Assign dynamic table", |mut region| { - // Enable the lookup on rows 0 and 1. - config.q.enable(&mut region, 0)?; - config.q.enable(&mut region, 1)?; - for i in 0..4 { // Load Advice lookup table with Instance lookup table values. region.assign_advice_from_instance( @@ -1420,22 +1414,14 @@ mod tests { config.advice_table, i, )?; - } - - // Assign a = 2 and a = 6. - region.assign_advice( - || "a = 2", - config.a, - 0, - || Value::known(Fp::from(2)), - )?; - region.assign_advice( - || "a = 6", - config.a, - 1, - || Value::known(Fp::from(6)), - )?; + // Enable the rows, which are used for lookup table values. + region.enable_selector( + || format!("enabling table row {}", i), + &config.s_ltable, + i, + )?; + } Ok(()) }, )?; @@ -1447,17 +1433,6 @@ mod tests { config.q.enable(&mut region, 0)?; config.q.enable(&mut region, 1)?; - for i in 0..4 { - // Load Advice lookup table with Instance lookup table values. - region.assign_advice_from_instance( - || "Advice from instance tables", - config.table, - i, - config.advice_table, - i, - )?; - } - // Assign a = 4. region.assign_advice( || "a = 4", @@ -1507,6 +1482,364 @@ mod tests { ); } + #[test] + #[should_panic( + expected = "pair of tagging expressions(query of the tag columns or mutiple query combinations) should be included" + )] + fn bad_lookup_any_not_add_tagging_pairs() { + const K: u32 = 4; + + #[derive(Clone)] + #[allow(dead_code)] + struct FaultyCircuitConfig { + a: Column, + table: Column, + advice_table: Column, + q: Selector, + s_ltable: Selector, + } + + struct FaultyCircuit {} + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.instance_column(); + let advice_table = meta.advice_column(); + let s_ltable = meta.complex_selector(); + + meta.annotate_lookup_any_column(table, || "Inst-Table"); + meta.enable_equality(table); + meta.annotate_lookup_any_column(advice_table, || "Adv-Table"); + meta.enable_equality(advice_table); + + meta.lookup_any("lookup", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let q = cells.query_selector(q); + let advice_table = cells.query_advice(advice_table, Rotation::cur()); + let table = cells.query_instance(table, Rotation::cur()); + let s_ltable = cells.query_selector(s_ltable); + + // If q is enabled, a must be in the table. + vec![ + (q.clone() * a.clone(), s_ltable.clone() * table), + (q * a, s_ltable * advice_table), + ] + }); + + FaultyCircuitConfig { + a, + q, + table, + advice_table, + s_ltable, + } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize(&self, _: Self::Config, _: impl Layouter) -> Result<(), Error> { + unreachable!("Should not be called because of configuration error"); + } + } + + let _ = MockProver::run( + K, + &FaultyCircuit {}, + // This is our "lookup table". + vec![vec![ + Fp::from(1u64), + Fp::from(2u64), + Fp::from(4u64), + Fp::from(6u64), + ]], + ) + .unwrap(); + } + + #[test] + #[should_panic(expected = "all table expressions need selector/fixed query for tagging")] + fn bad_lookup_any_no_fixed_col_or_selector() { + const K: u32 = 4; + + #[derive(Clone)] + #[allow(dead_code)] + struct FaultyCircuitConfig { + a: Column, + table: Column, + advice_table: Column, + q: Selector, + } + + struct FaultyCircuit {} + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.instance_column(); + let advice_table = meta.advice_column(); + + meta.annotate_lookup_any_column(table, || "Inst-Table"); + meta.enable_equality(table); + meta.annotate_lookup_any_column(advice_table, || "Adv-Table"); + meta.enable_equality(advice_table); + + meta.lookup_any("lookup", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let q = cells.query_selector(q); + let advice_table = cells.query_advice(advice_table, Rotation::cur()); + let table = cells.query_instance(table, Rotation::cur()); + + // If q is enabled, a must be in the table. + vec![(q.clone() * a.clone(), table), (q * a, advice_table)] + }); + + FaultyCircuitConfig { + a, + q, + table, + advice_table, + } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize(&self, _: Self::Config, _: impl Layouter) -> Result<(), Error> { + unreachable!("Should not be called because of configuration error"); + } + } + + let _ = MockProver::run( + K, + &FaultyCircuit {}, + // This is our "lookup table". + vec![vec![ + Fp::from(1u64), + Fp::from(2u64), + Fp::from(4u64), + Fp::from(6u64), + ]], + ) + .unwrap(); + } + + #[test] + #[should_panic( + expected = "all table expressions contain only fixed query, should use `lookup` api instead of `lookup_any`" + )] + fn bad_lookup_any_use_only_fixed_col() { + const K: u32 = 4; + + #[derive(Clone)] + #[allow(dead_code)] + struct FaultyCircuitConfig { + a: Column, + fixed_table: Column, + q: Selector, + } + + struct FaultyCircuit {} + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let q = meta.complex_selector(); + let fixed_table = meta.fixed_column(); + + meta.annotate_lookup_any_column(fixed_table, || "Fixed-Table"); + meta.enable_equality(fixed_table); + + meta.lookup_any("lookup", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let q = cells.query_selector(q); + let fixed_table = cells.query_fixed(fixed_table, Rotation::cur()); + + // If q is enabled, a must be in the table. + vec![(q * a, fixed_table)] + }); + + FaultyCircuitConfig { a, q, fixed_table } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize(&self, _: Self::Config, _: impl Layouter) -> Result<(), Error> { + unreachable!("Should not be called because of configuration error"); + } + } + + let _ = MockProver::run( + K, + &FaultyCircuit {}, + // This is our "lookup table". + vec![vec![ + Fp::from(1u64), + Fp::from(2u64), + Fp::from(4u64), + Fp::from(6u64), + ]], + ) + .unwrap(); + } + + #[test] + fn good_lookup_any() { + const K: u32 = 4; + + #[derive(Clone)] + struct GoodLookupAnyCircuitConfig { + a: Column, + table: Column, + advice_table: Column, + q: Selector, + s_ltable: Selector, + } + + struct GoodLookupAnyCircuit {} + + impl Circuit for GoodLookupAnyCircuit { + type Config = GoodLookupAnyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.instance_column(); + let advice_table = meta.advice_column(); + let s_ltable = meta.complex_selector(); + + meta.annotate_lookup_any_column(table, || "Inst-Table"); + meta.enable_equality(table); + meta.annotate_lookup_any_column(advice_table, || "Adv-Table"); + meta.enable_equality(advice_table); + + meta.lookup_any("lookup", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let q = cells.query_selector(q); + let advice_table = cells.query_advice(advice_table, Rotation::cur()); + let table = cells.query_instance(table, Rotation::cur()); + let s_ltable = cells.query_selector(s_ltable); + + // If q is enabled, a must be in the table. + // If `s_ltable` is enabled, the value of `advice_table` & `table` is used as lookup table. + vec![ + (q.clone() * a.clone(), table * s_ltable.clone()), + (q.clone() * a, advice_table * s_ltable.clone()), + (q, s_ltable), + ] + }); + + GoodLookupAnyCircuitConfig { + a, + q, + table, + advice_table, + s_ltable, + } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "Assign dynamic table", + |mut region| { + for i in 0..4 { + // Load Advice lookup table with Instance lookup table values. + region.assign_advice_from_instance( + || "Advice from instance tables", + config.table, + i, + config.advice_table, + i, + )?; + + // Enable the rows, which are used for lookup table values. + region.enable_selector( + || format!("enabling table row {}", i), + &config.s_ltable, + i, + )?; + } + Ok(()) + }, + )?; + + layouter.assign_region( + || "Good synthesis", + |mut region| { + // Enable the lookup on rows 0 and 1. + config.q.enable(&mut region, 0)?; + config.q.enable(&mut region, 1)?; + + // Assign a = 2 and a = 6. + region.assign_advice( + || "a = 2", + config.a, + 0, + || Value::known(Fp::from(2)), + )?; + region.assign_advice( + || "a = 6", + config.a, + 1, + || Value::known(Fp::from(6)), + )?; + + Ok(()) + }, + )?; + + Ok(()) + } + } + + let prover = MockProver::run( + K, + &GoodLookupAnyCircuit {}, + // This is our "lookup table". + vec![vec![ + Fp::from(1u64), + Fp::from(2u64), + Fp::from(4u64), + Fp::from(6u64), + ]], + ) + .unwrap(); + assert_eq!(prover.verify(), Ok(())); + } + #[test] fn bad_fixed_lookup() { const K: u32 = 4; diff --git a/halo2_frontend/src/plonk/circuit/constraint_system.rs b/halo2_frontend/src/plonk/circuit/constraint_system.rs index cabe718042..b5b6a42912 100644 --- a/halo2_frontend/src/plonk/circuit/constraint_system.rs +++ b/halo2_frontend/src/plonk/circuit/constraint_system.rs @@ -389,12 +389,25 @@ impl ConstraintSystem { /// /// `table_map` returns a map between input expressions and the table expressions /// they need to match. + /// + /// **NOTE:** + /// We should use extra `Fixed` column or `Selector` for tagging the table rows. + /// Also, it is needed to include a pair of tagging expressions(`[lookup_activator, table_activator]`) in the `table_map`. + /// Otherwise, we have soundness error.(See [here](https://github.com/privacy-scaling-explorations/halo2/issues/335)) + /// For correct use, please reference + /// [here](https://github.com/privacy-scaling-explorations/halo2/blob/main/halo2_proofs/tests/frontend_backend_split.rs) + /// and [here](https://github.com/privacy-scaling-explorations/halo2/blob/main/halo2_frontend/src/dev.rs). pub fn lookup_any>( &mut self, name: S, table_map: impl FnOnce(&mut VirtualCells<'_, F>) -> Vec<(Expression, Expression)>, ) -> usize { let mut cells = VirtualCells::new(self); + + let mut is_all_table_expr_single_fixed = true; + let mut is_all_table_expr_contain_fixed_or_selector = true; + let mut is_tagging_exprs_pair_exists = false; + let table_map = table_map(&mut cells) .into_iter() .map(|(mut input, mut table)| { @@ -404,11 +417,38 @@ impl ConstraintSystem { if table.contains_simple_selector() { panic!("expression containing simple selector supplied to lookup argument"); } + + is_all_table_expr_single_fixed &= table.degree() == 1 && table.contains_fixed_col(); + is_all_table_expr_contain_fixed_or_selector &= + table.contains_fixed_col_or_selector(); + is_tagging_exprs_pair_exists |= + table.contains_fixed_col_or_selector() && table.degree() == 1; + input.query_cells(&mut cells); table.query_cells(&mut cells); (input, table) }) .collect(); + + #[cfg(feature = "lookup-any-sanity-checks")] + { + // NOTE: These checks try to detect unsound cases of lookups and are only active + // with the `lookup-any-sanity-checks`. False positives may exist: in some + // particular scenarios the lookup can be sound but these checks will not pass, + // leading to panics. For those cases you can disable the + // `lookup-any-sanity-checks` feature. We will appreciate it if you report false + // positives by opening issues on the repository. + if is_all_table_expr_single_fixed { + panic!("all table expressions contain only fixed query, should use `lookup` api instead of `lookup_any`"); + } + if !is_all_table_expr_contain_fixed_or_selector { + panic!("all table expressions need selector/fixed query for tagging"); + } + if !is_tagging_exprs_pair_exists { + panic!("pair of tagging expressions(query of the tag columns or mutiple query combinations) should be included"); + } + } + let index = self.lookups.len(); self.lookups diff --git a/halo2_frontend/src/plonk/circuit/expression.rs b/halo2_frontend/src/plonk/circuit/expression.rs index 9b869f6ef2..3a991d1980 100644 --- a/halo2_frontend/src/plonk/circuit/expression.rs +++ b/halo2_frontend/src/plonk/circuit/expression.rs @@ -946,6 +946,43 @@ impl Expression { &|a, _| a, ) } + + /// Returns whether or not this expression contains a `Fixed` column. + pub(super) fn contains_fixed_col(&self) -> bool { + self.evaluate( + &|_| false, + &|_| false, + &|_| true, + &|_| false, + &|_| false, + &|_| false, + &|a| a, + &|a, b| a || b, + &|a, b| a || b, + &|a, _| a, + ) + } + + /// Returns whether or not this expression contains a `Selector`. + pub(super) fn contains_selector(&self) -> bool { + self.evaluate( + &|_| false, + &|_| true, + &|_| false, + &|_| false, + &|_| false, + &|_| false, + &|a| a, + &|a, b| a || b, + &|a, b| a || b, + &|a, _| a, + ) + } + + /// Returns whether or not this expression contains a `Selector` or `Fixed` column. + pub(super) fn contains_fixed_col_or_selector(&self) -> bool { + self.contains_fixed_col() || self.contains_selector() + } } impl std::fmt::Debug for Expression { diff --git a/halo2_proofs/Cargo.toml b/halo2_proofs/Cargo.toml index 4302dd7276..e84af4eafa 100644 --- a/halo2_proofs/Cargo.toml +++ b/halo2_proofs/Cargo.toml @@ -67,7 +67,7 @@ halo2_debug = { path = "../halo2_debug" } getrandom = { version = "0.2", features = ["js"] } [features] -default = ["batch", "bits", "halo2_frontend/default", "halo2_backend/default"] +default = ["batch", "bits", "halo2_frontend/default", "halo2_backend/default", "lookup-any-sanity-checks"] dev-graph = ["halo2_frontend/dev-graph", "plotters"] test-dev-graph = [ "halo2_frontend/test-dev-graph", @@ -85,6 +85,7 @@ circuit-params = ["halo2_frontend/circuit-params"] heap-profiling = ["halo2_frontend/heap-profiling"] cost-estimator = ["halo2_frontend/cost-estimator"] derive_serde = ["halo2curves/derive_serde", "halo2_frontend/derive_serde", "halo2_backend/derive_serde"] +lookup-any-sanity-checks = ["halo2_frontend/lookup-any-sanity-checks"] [lib] bench = false