diff --git a/CHANGELOG.md b/CHANGELOG.md index 03bcb706..9add34da 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,9 @@ and this project adheres to Rust's notion of [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ## [Unreleased] +### Added +- `halo2::dev::LookupFailure` (used in `VerifyFailure::Lookup`) + ### Changed - `halo2::plonk::Error` has been overhauled: - `Error` now implements `std::fmt::Display` and `std::error::Error`. @@ -19,8 +22,12 @@ and this project adheres to Rust's notion of underlying `io::Error`. - `halo2::dev::CircuitLayout::render` now takes `k` as a `u32`, matching the regular parameter APIs. -- `halo2::dev::VerifyFailure::ConstraintNotSatisfied` now has a `cell_values` - field, storing the values of the cells used in the unsatisfied constraint. +- `halo2::dev::VerifyFailure` has been overhauled: + - `VerifyFailure::ConstraintNotSatisfied` now has a `cell_values` field, + storing the values of the cells used in the unsatisfied constraint. + - The `row` field of `VerifyFailure::Lookup` has been replaced by a `location` + field, which can now indicate whether the location falls within an assigned + region. - `halo2::plonk::ConstraintSystem::enable_equality` and `halo2::plonk::ConstraintSystem::query_any` now take `Into>` instead of `Column` as a parameter to avoid excesive `.into()` usage. diff --git a/src/dev.rs b/src/dev.rs index f3423eb0..bffd6c7d 100644 --- a/src/dev.rs +++ b/src/dev.rs @@ -33,6 +33,29 @@ mod graph; #[cfg_attr(docsrs, doc(cfg(feature = "dev-graph")))] pub use graph::{circuit_dot_graph, layout::CircuitLayout}; +/// The location at which a particular lookup is not satisfied. +#[derive(Debug, PartialEq)] +pub enum LookupFailure { + /// A location inside a region. This may be due to the intentional use of a lookup + /// (if its inputs are conditional on a complex selector), or an unintentional lookup + /// constraint that overlaps the region (indicating that the lookup's inputs should be + /// made conditional). + InRegion { + /// The region in which the lookup's input expressions were evaluated. + region: metadata::Region, + /// The offset (relative to the start of the region) at which the lookup's input + /// expressions were evaluated. + offset: usize, + }, + /// A location outside of a region. This most likely means the input expressions do + /// not correctly constrain a default value that exists in the table when the lookup + /// is not being used. + OutsideRegion { + /// The circuit row on which this lookup is not satisfied. + row: usize, + }, +} + /// The reasons why a particular circuit is not satisfied. #[derive(Debug, PartialEq)] pub enum VerifyFailure { @@ -69,8 +92,8 @@ pub enum VerifyFailure { /// the order in which `ConstraintSystem::lookup` is called during /// `Circuit::configure`. lookup_index: usize, - /// The row on which this lookup is not satisfied. - row: usize, + /// The location at which the lookup is not satisfied. + location: LookupFailure, }, /// A permutation did not preserve the original value of a cell. Permutation { @@ -114,9 +137,19 @@ impl fmt::Display for VerifyFailure { constraint ) } - Self::Lookup { lookup_index, row } => { - write!(f, "Lookup {} is not satisfied on row {}", lookup_index, row) - } + Self::Lookup { + lookup_index, + location, + } => match location { + LookupFailure::InRegion { region, offset } => write!( + f, + "Lookup {} is not satisfied in {} at offset {}", + lookup_index, region, offset + ), + LookupFailure::OutsideRegion { row } => { + write!(f, "Lookup {} is not satisfied on row {}", lookup_index, row) + } + }, Self::Permutation { column, row } => { write!( f, @@ -817,7 +850,9 @@ impl MockProver { } else { Some(VerifyFailure::Lookup { lookup_index, - row: input_row as usize, + location: LookupFailure::OutsideRegion { + row: input_row as usize, + }, }) } }) @@ -891,10 +926,10 @@ impl MockProver { mod tests { use pasta_curves::Fp; - use super::{MockProver, VerifyFailure}; + use super::{LookupFailure, MockProver, VerifyFailure}; use crate::{ circuit::{Layouter, SimpleFloorPlanner}, - plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector}, + plonk::{Advice, Any, Circuit, Column, ConstraintSystem, Error, Selector, TableColumn}, poly::Rotation, }; @@ -969,4 +1004,110 @@ mod tests { }]) ); } + + #[test] + fn bad_lookup() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + a: Column, + q: Selector, + table: TableColumn, + } + + struct FaultyCircuit {} + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let q = meta.complex_selector(); + let table = meta.lookup_table_column(); + + meta.lookup(|cells| { + let a = cells.query_advice(a, Rotation::cur()); + let q = cells.query_selector(q); + + // If q is enabled, a must be in the table. + // Zero is in the table, which satisfies the disabled case. + vec![(q * a, table)] + }); + + FaultyCircuitConfig { a, q, table } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_table( + || "Doubling table", + |mut table| { + (0..(1 << (K - 1))) + .map(|i| { + table.assign_cell( + || format!("table[{}] = {}", i, 2 * i), + config.table, + i, + || Ok(Fp::from(2 * i as u64)), + ) + }) + .fold(Ok(()), |acc, res| acc.and(res)) + }, + )?; + + 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, || Ok(Fp::from(2)))?; + region.assign_advice(|| "a = 6", config.a, 1, || Ok(Fp::from(6)))?; + + Ok(()) + }, + )?; + + layouter.assign_region( + || "Faulty 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 = 4. + region.assign_advice(|| "a = 4", config.a, 0, || Ok(Fp::from(4)))?; + + // BUG: Assign a = 5, which doesn't exist in the table! + region.assign_advice(|| "a = 5", config.a, 1, || Ok(Fp::from(5)))?; + + Ok(()) + }, + ) + } + } + + let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::Lookup { + lookup_index: 0, + location: LookupFailure::InRegion { + region: (2, "Faulty synthesis".to_owned()).into(), + offset: 1, + } + }]) + ); + } }