From a86edfec5edee0b946f849903b382fea61ab6d2d Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 12 Dec 2022 15:29:03 +0100 Subject: [PATCH 01/21] feat: Add `name_column` to `Layouter` & `RegionLayouter` This adds the trait-associated function `name_column` in order to enable the possibility of the Layouter to store annotations aobut the colums. This function does nothing for all the trait implementors (V1, SimpleFloor, Assembly....) except for the `MockProver`. Which is responsible of storing a map that links within a `Region` index, the `column::Metadata` to the annotation `String`. --- halo2_proofs/src/circuit.rs | 11 + .../src/circuit/floor_planner/single_pass.rs | 8 + halo2_proofs/src/circuit/floor_planner/v1.rs | 8 + halo2_proofs/src/circuit/layouter.rs | 15 + halo2_proofs/src/dev.rs | 257 +++++++++++++++--- halo2_proofs/src/dev/cost.rs | 8 + halo2_proofs/src/plonk/keygen.rs | 8 + halo2_proofs/src/plonk/prover.rs | 135 +++++++-- 8 files changed, 399 insertions(+), 51 deletions(-) diff --git a/halo2_proofs/src/circuit.rs b/halo2_proofs/src/circuit.rs index 0f0646fa85..4f8c26b35c 100644 --- a/halo2_proofs/src/circuit.rs +++ b/halo2_proofs/src/circuit.rs @@ -206,6 +206,17 @@ impl<'r, F: Field> Region<'r, F> { .enable_selector(&|| annotation().into(), selector, offset) } + /// Annotates a column. + pub(crate) fn name_column(&mut self, annotation: A, column: T) + where + A: Fn() -> AR, + AR: Into, + T: Into>, + { + self.region + .name_column(&|| annotation().into(), column.into()); + } + /// Assign an advice column value (witness). /// /// Even though `to` has `FnMut` bounds, it is guaranteed to be called at most once. diff --git a/halo2_proofs/src/circuit/floor_planner/single_pass.rs b/halo2_proofs/src/circuit/floor_planner/single_pass.rs index 3798efbe54..f5b80bf833 100644 --- a/halo2_proofs/src/circuit/floor_planner/single_pass.rs +++ b/halo2_proofs/src/circuit/floor_planner/single_pass.rs @@ -279,6 +279,14 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> RegionLayouter ) } + fn name_column<'v>( + &'v mut self, + annotation: &'v (dyn Fn() -> String + 'v), + column: Column, + ) { + self.layouter.cs.annotate_column(annotation, column); + } + fn assign_advice<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), diff --git a/halo2_proofs/src/circuit/floor_planner/v1.rs b/halo2_proofs/src/circuit/floor_planner/v1.rs index 62207a91a7..45cafee8e2 100644 --- a/halo2_proofs/src/circuit/floor_planner/v1.rs +++ b/halo2_proofs/src/circuit/floor_planner/v1.rs @@ -481,6 +481,14 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> RegionLayouter for V1Region<'r Ok(()) } + fn name_column<'v>( + &'v mut self, + annotation: &'v (dyn Fn() -> String + 'v), + column: Column, + ) { + unimplemented!() + } + fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result<(), Error> { self.plan.cs.copy( left.column, diff --git a/halo2_proofs/src/circuit/layouter.rs b/halo2_proofs/src/circuit/layouter.rs index 9436011fdc..e0fd0b5de4 100644 --- a/halo2_proofs/src/circuit/layouter.rs +++ b/halo2_proofs/src/circuit/layouter.rs @@ -48,6 +48,13 @@ pub trait RegionLayouter: fmt::Debug { offset: usize, ) -> Result<(), Error>; + /// Annotate a Column within a Region context. + fn name_column<'v>( + &'v mut self, + annotation: &'v (dyn Fn() -> String + 'v), + column: Column, + ); + /// Assign an advice column value (witness) fn assign_advice<'v>( &'v mut self, @@ -275,6 +282,14 @@ impl RegionLayouter for RegionShape { }) } + fn name_column<'v>( + &'v mut self, + annotation: &'v (dyn Fn() -> String + 'v), + column: Column, + ) { + // Do nothing + } + fn constrain_constant(&mut self, _cell: Cell, _constant: Assigned) -> Result<(), Error> { // Global constants don't affect the region shape. Ok(()) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index e275f198c3..acf5901700 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -28,6 +28,7 @@ use rayon::{ }; pub mod metadata; +use metadata::Column as ColumnMetadata; mod util; mod failure; @@ -57,7 +58,9 @@ struct Region { /// The selectors that have been enabled in this region. All other selectors are by /// construction not enabled. enabled_selectors: HashMap>, - /// The cells assigned in this region. We store this as a `HashMap` with count so that if any cells + /// Annotations of the columns. + annotations: HashMap, + /// The cells assigned in this region. We store this as a `Vec` so that if any cells /// are double-assigned, they will be visibly darker. cells: HashMap<(Column, usize), usize>, } @@ -316,6 +319,7 @@ impl Assignment for MockProver { name: name().into(), columns: HashSet::default(), rows: None, + annotations: HashMap::default(), enabled_selectors: HashMap::default(), cells: HashMap::default(), }); @@ -325,6 +329,18 @@ impl Assignment for MockProver { self.regions.push(self.current_region.take().unwrap()); } + fn annotate_column(&mut self, annotation: A, column: Column) + where + A: FnOnce() -> AR, + AR: Into, + { + if let Some(region) = self.current_region.as_mut() { + region + .annotations + .insert(ColumnMetadata::from(column), annotation().into()); + } + } + fn enable_selector(&mut self, _: A, selector: &Selector, row: usize) -> Result<(), Error> where A: FnOnce() -> AR, @@ -636,17 +652,39 @@ impl MockProver { // Determine where this cell should have been assigned. let cell_row = ((gate_row + n + cell.rotation.0) % n) as usize; - // Check that it was assigned! - if r.cells.contains_key(&(cell.column, cell_row)) { - None - } else { - Some(VerifyFailure::CellNotAssigned { - gate: (gate_index, gate.name()).into(), - region: (r_i, r.name.clone()).into(), - gate_offset: *selector_row, - column: cell.column, - offset: cell_row as isize - r.rows.unwrap().0 as isize, - }) + match cell.column.column_type() { + Any::Instance => { + // Handle instance cells, which are not in the region. + let instance_value = + &self.instance[cell.column.index()][cell_row]; + match instance_value { + InstanceValue::Assigned(_) => None, + _ => Some(VerifyFailure::InstanceCellNotAssigned { + gate: (gate_index, gate.name()).into(), + region: (r_i, r.name.clone(), &r.annotations) + .into(), + gate_offset: *selector_row, + column: cell.column.try_into().unwrap(), + row: cell_row, + }), + } + } + _ => { + // Check that it was assigned! + if r.cells.contains(&(cell.column, cell_row)) { + None + } else { + Some(VerifyFailure::CellNotAssigned { + gate: (gate_index, gate.name()).into(), + region: (r_i, r.name.clone(), &r.annotations) + .into(), + gate_offset: *selector_row, + column: cell.column, + offset: cell_row as isize + - r.rows.unwrap().0 as isize, + }) + } + } } }) }) @@ -860,6 +898,7 @@ impl MockProver { *input_row, lookup.input_expressions.iter(), ), + //annotations: Some(&self.cs.lookup_annotations), }) } else { None @@ -1346,7 +1385,7 @@ mod tests { use crate::{ circuit::{Layouter, SimpleFloorPlanner, Value}, plonk::{ - Advice, Any, Circuit, Column, ConstraintSystem, Error, Expression, Selector, + Advice, Any, Circuit, Column, ConstraintSystem, Error, Expression, Fixed, Selector, TableColumn, }, poly::Rotation, @@ -1359,6 +1398,7 @@ mod tests { #[derive(Clone)] struct FaultyCircuitConfig { a: Column, + b: Column, q: Selector, } @@ -1382,7 +1422,7 @@ mod tests { vec![q * (a - b)] }); - FaultyCircuitConfig { a, q } + FaultyCircuitConfig { a, b, q } } fn without_witnesses(&self) -> Self { @@ -1403,6 +1443,12 @@ mod tests { // Assign a = 0. region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::zero()))?; + // Name Column a + region.name_column(|| "This is annotated!", config.a); + + // Name Column b + region.name_column(|| "This is also annotated!", config.b); + // BUG: Forget to assign b = 0! This could go unnoticed during // development, because cell values default to zero, which in this // case is fine, but for other assignments would be broken. @@ -1413,16 +1459,17 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - assert_eq!( - prover.verify(), - Err(vec![VerifyFailure::CellNotAssigned { - gate: (0, "Equality check").into(), - region: (0, "Faulty synthesis".to_owned()).into(), - gate_offset: 1, - column: Column::new(1, Any::advice()), - offset: 1, - }]) - ); + prover.assert_satisfied(); + // assert_eq!( + // prover.verify(), + // Err(vec![VerifyFailure::CellNotAssigned { + // gate: (0, "Equality check").into(), + // region: (0, "Faulty synthesis".to_owned()).into(), + // gate_offset: 1, + // column: Column::new(1, Any::Advice), + // offset: 1, + // }]) + // ); } #[test] @@ -1446,6 +1493,7 @@ mod tests { let a = meta.advice_column(); let q = meta.complex_selector(); let table = meta.lookup_table_column(); + meta.annotate_lookup_column(table, || "Table Lookup"); meta.lookup("lookup", |cells| { let a = cells.query_advice(a, Rotation::cur()); @@ -1534,6 +1582,8 @@ mod tests { || Value::known(Fp::from(5)), )?; + region.name_column(|| "Witness example", config.a); + Ok(()) }, ) @@ -1541,16 +1591,153 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - assert_eq!( - prover.verify(), - Err(vec![VerifyFailure::Lookup { - name: "lookup", - lookup_index: 0, - location: FailureLocation::InRegion { - region: (2, "Faulty synthesis").into(), - offset: 1, - } - }]) - ); + prover.assert_satisfied(); + // assert_eq!( + // prover.verify(), + // Err(vec![VerifyFailure::Lookup { + // lookup_index: 0, + // location: FailureLocation::InRegion { + // region: (2, "Faulty synthesis").into(), + // offset: 1, + // } + // }]) + // ); + } + + #[test] + fn contraint_unsatisfied() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + a: Column, + b: Column, + c: Column, + d: Column, + q: Selector, + } + + 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 b = meta.advice_column(); + let c = meta.advice_column(); + let d = meta.fixed_column(); + let q = meta.selector(); + + meta.create_gate("Equality check", |cells| { + let a = cells.query_advice(a, Rotation::cur()); + let b = cells.query_advice(b, Rotation::cur()); + let c = cells.query_advice(c, Rotation::cur()); + let d = cells.query_fixed(d, Rotation::cur()); + let q = cells.query_selector(q); + + // If q is enabled, a and b must be assigned to. + vec![q * (a - b) * (c - d)] + }); + + FaultyCircuitConfig { a, b, c, d, q } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_region( + || "Correct synthesis", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Assign b = 1. + region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::one()))?; + + // Assign c = 5. + region.assign_advice( + || "c", + config.c, + 0, + || Value::known(Fp::from(5u64)), + )?; + // Assign d = 7. + region.assign_fixed( + || "d", + config.d, + 0, + || Value::known(Fp::from(7u64)), + )?; + Ok(()) + }, + )?; + layouter.assign_region( + || "Wrong synthesis", + |mut region| { + // Enable the equality gate. + config.q.enable(&mut region, 0)?; + + // Assign a = 1. + region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::one()))?; + + // Assign b = 0. + region.assign_advice(|| "b", config.b, 0, || Value::known(Fp::zero()))?; + + // Name Column a + region.name_column(|| "This is Advice!", config.a); + // Name Column b + region.name_column(|| "This is Advice too!", config.b); + + // Assign c = 5. + region.assign_advice( + || "c", + config.c, + 0, + || Value::known(Fp::from(5u64)), + )?; + // Assign d = 7. + region.assign_fixed( + || "d", + config.d, + 0, + || Value::known(Fp::from(7u64)), + )?; + + // Name Column c + region.name_column(|| "Another one!", config.c); + // Name Column d + region.name_column(|| "This is a Fixed!", config.d); + + // Note that none of the terms cancel eachother. Therefore we will have a constraint that is non satisfied for + // the `Equalty check` gate. + Ok(()) + }, + ) + } + } + + let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); + prover.assert_satisfied(); + // assert_eq!( + // prover.verify(), + // Err(vec![VerifyFailure::CellNotAssigned { + // gate: (0, "Equality check").into(), + // region: (0, "Faulty synthesis".to_owned()).into(), + // gate_offset: 1, + // column: Column::new(1, Any::Advice), + // offset: 1, + // }]) + // ); } } diff --git a/halo2_proofs/src/dev/cost.rs b/halo2_proofs/src/dev/cost.rs index ad6f8b1eec..ed25e5ce91 100644 --- a/halo2_proofs/src/dev/cost.rs +++ b/halo2_proofs/src/dev/cost.rs @@ -122,6 +122,14 @@ impl Assignment for Assembly { Value::unknown() } + fn annotate_column(&mut self, annotation: A, column: Column) + where + A: FnOnce() -> AR, + AR: Into, + { + unimplemented!() + } + fn push_namespace(&mut self, _: N) where NR: Into, diff --git a/halo2_proofs/src/plonk/keygen.rs b/halo2_proofs/src/plonk/keygen.rs index a3fe3dc3d7..6586c6014a 100644 --- a/halo2_proofs/src/plonk/keygen.rs +++ b/halo2_proofs/src/plonk/keygen.rs @@ -178,6 +178,14 @@ impl Assignment for Assembly { Value::unknown() } + fn annotate_column(&mut self, annotation: A, column: Column) + where + A: FnOnce() -> AR, + AR: Into, + { + unimplemented!() + } + fn push_namespace(&mut self, _: N) where NR: Into, diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index 65a01873d2..b725832502 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -182,22 +182,125 @@ pub fn create_proof< .ok_or(Error::BoundsFailure) } - fn assign_advice( - &mut self, - _: A, - column: Column, - row: usize, - to: V, - ) -> Result<(), Error> - where - V: FnOnce() -> Value, - VR: Into>, - A: FnOnce() -> AR, - AR: Into, - { - // Ignore assignment of advice column in different phase than current one. - if self.current_phase != column.column_type().phase { - return Ok(()); + fn exit_region(&mut self) { + // Do nothing; we don't care about regions in this context. + } + + fn enable_selector( + &mut self, + _: A, + _: &Selector, + _: usize, + ) -> Result<(), Error> + where + A: FnOnce() -> AR, + AR: Into, + { + // We only care about advice columns here + + Ok(()) + } + + fn query_instance( + &self, + column: Column, + row: usize, + ) -> Result, Error> { + if !self.usable_rows.contains(&row) { + return Err(Error::not_enough_rows_available(self.k)); + } + + self.instances + .get(column.index()) + .and_then(|column| column.get(row)) + .map(|v| Value::known(*v)) + .ok_or(Error::BoundsFailure) + } + + fn assign_advice( + &mut self, + _: A, + column: Column, + row: usize, + to: V, + ) -> Result<(), Error> + where + V: FnOnce() -> Value, + VR: Into>, + A: FnOnce() -> AR, + AR: Into, + { + if !self.usable_rows.contains(&row) { + return Err(Error::not_enough_rows_available(self.k)); + } + + *self + .advice + .get_mut(column.index()) + .and_then(|v| v.get_mut(row)) + .ok_or(Error::BoundsFailure)? = to().into_field().assign()?; + + Ok(()) + } + + fn assign_fixed( + &mut self, + _: A, + _: Column, + _: usize, + _: V, + ) -> Result<(), Error> + where + V: FnOnce() -> Value, + VR: Into>, + A: FnOnce() -> AR, + AR: Into, + { + // We only care about advice columns here + + Ok(()) + } + + fn copy( + &mut self, + _: Column, + _: usize, + _: Column, + _: usize, + ) -> Result<(), Error> { + // We only care about advice columns here + + Ok(()) + } + + fn fill_from_row( + &mut self, + _: Column, + _: usize, + _: Value>, + ) -> Result<(), Error> { + Ok(()) + } + + fn annotate_column(&mut self, annotation: A, column: Column) + where + A: FnOnce() -> AR, + AR: Into, + { + unimplemented!() + } + + fn push_namespace(&mut self, _: N) + where + NR: Into, + N: FnOnce() -> NR, + { + // Do nothing; we don't care about namespaces in this context. + } + + fn pop_namespace(&mut self, _: Option) { + // Do nothing; we don't care about namespaces in this context. + } } if !self.usable_rows.contains(&row) { From fc2c76a009773ce530a85349242320a13d2fa5c2 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 12 Dec 2022 15:36:40 +0100 Subject: [PATCH 02/21] feta: Update metadata/dbg structs to hold Col->Ann mapping --- halo2_proofs/src/dev/failure.rs | 78 +++++++++++++++++++++++--------- halo2_proofs/src/dev/metadata.rs | 62 +++++++++++++++++++++---- 2 files changed, 109 insertions(+), 31 deletions(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 2fcb2a1fc8..c253e210f8 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -1,4 +1,4 @@ -use std::collections::{BTreeMap, BTreeSet, HashSet}; +use std::collections::{BTreeMap, HashMap, HashSet}; use std::fmt; use std::iter; @@ -19,12 +19,12 @@ use crate::{ mod emitter; /// The location within the circuit at which a particular [`VerifyFailure`] occurred. -#[derive(Debug, PartialEq)] -pub enum FailureLocation { +#[derive(Debug, PartialEq, Eq)] +pub enum FailureLocation<'a> { /// A location inside a region. InRegion { /// The region in which the failure occurred. - region: metadata::Region, + region: metadata::Region<'a>, /// The offset (relative to the start of the region) at which the failure /// occurred. offset: usize, @@ -36,7 +36,7 @@ pub enum FailureLocation { }, } -impl fmt::Display for FailureLocation { +impl<'a> fmt::Display for FailureLocation<'a> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Self::InRegion { region, offset } => write!(f, "in {} at offset {}", region, offset), @@ -47,10 +47,10 @@ impl fmt::Display for FailureLocation { } } -impl FailureLocation { - pub(super) fn find_expressions<'a, F: Field>( +impl<'a> FailureLocation<'a> { + pub(super) fn find_expressions( cs: &ConstraintSystem, - regions: &[Region], + regions: &'a [Region], failure_row: usize, failure_expressions: impl Iterator>, ) -> Self { @@ -82,7 +82,7 @@ impl FailureLocation { /// Figures out whether the given row and columns overlap an assigned region. pub(super) fn find( - regions: &[Region], + regions: &'a [Region], failure_row: usize, failure_columns: HashSet>, ) -> Self { @@ -99,24 +99,21 @@ impl FailureLocation { (start..=end).contains(&failure_row) && !failure_columns.is_disjoint(&r.columns) }) .map(|(r_i, r)| FailureLocation::InRegion { - region: (r_i, r.name.clone()).into(), - offset: failure_row as usize - r.rows.unwrap().0 as usize, - }) - .unwrap_or_else(|| FailureLocation::OutsideRegion { - row: failure_row as usize, + region: (r_i, r.name.clone(), &r.annotations).into(), + offset: failure_row - r.rows.unwrap().0, }) } } /// The reasons why a particular circuit is not satisfied. -#[derive(Debug, PartialEq)] -pub enum VerifyFailure { +#[derive(Debug, PartialEq, Eq)] +pub enum VerifyFailure<'a> { /// A cell used in an active gate was not assigned to. CellNotAssigned { /// The index of the active gate. gate: metadata::Gate, /// The region in which this cell should be assigned. - region: metadata::Region, + region: metadata::Region<'a>, /// The offset (relative to the start of the region) at which the active gate /// queries this cell. gate_offset: usize, @@ -127,6 +124,20 @@ pub enum VerifyFailure { /// offset 0, but the gate uses `Rotation::prev()`). offset: isize, }, + /// An instance cell used in an active gate was not assigned to. + InstanceCellNotAssigned { + /// The index of the active gate. + gate: metadata::Gate, + /// The region in which this gate was activated. + region: metadata::Region<'a>, + /// The offset (relative to the start of the region) at which the active gate + /// queries this cell. + gate_offset: usize, + /// The column in which this cell should be assigned. + column: Column, + /// The absolute row at which this cell should be assigned. + row: usize, + }, /// A constraint was not satisfied for a particular row. ConstraintNotSatisfied { /// The polynomial constraint that is not satisfied. @@ -135,7 +146,7 @@ pub enum VerifyFailure { /// /// `FailureLocation::OutsideRegion` is usually caused by a constraint that does /// not contain a selector, and as a result is active on every row. - location: FailureLocation, + location: FailureLocation<'a>, /// The values of the virtual cells used by this constraint. cell_values: Vec<(metadata::VirtualCell, String)>, }, @@ -164,18 +175,20 @@ pub enum VerifyFailure { /// in the table when the lookup is not being used. /// - The input expressions use a column queried at a non-zero `Rotation`, and the /// lookup is active on a row adjacent to an unrelated region. - location: FailureLocation, + location: FailureLocation<'a>, + // Maps lookup columns to their annotations from an outside-region perspective. + //annotations: Option<&'a HashMap>, }, /// A permutation did not preserve the original value of a cell. Permutation { /// The column in which this permutation is not satisfied. column: metadata::Column, /// The location at which the permutation is not satisfied. - location: FailureLocation, + location: FailureLocation<'a>, }, } -impl fmt::Display for VerifyFailure { +impl<'a> fmt::Display for VerifyFailure<'a> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Self::CellNotAssigned { @@ -333,6 +346,8 @@ fn render_constraint_not_satisfied( .or_insert(format!("x{}", i)); } + dbg!(location); + eprintln!("error: constraint not satisfied"); emitter::render_cell_layout(" ", location, &columns, &layout, |_, rotation| { if rotation == 0 { @@ -498,6 +513,25 @@ fn render_lookup( emitter::expression_to_string(input, &layout) ); eprintln!(" ^"); + // // Include into the FailureLocation the TableColumns that we want to be annotated when displayed. + // let mut location_extended = location.clone(); + // match location_extended { + // FailureLocation::InRegion { mut region, offset } => { + // if region.column_annotations.is_none() { + // () + // } else if let Some(annotation) = prover.cs.lookup_annotations.get(&lookup_index) { + // region + // .column_annotations + // .as_mut() + // .unwrap() + // .insert(lookup_index, annotation.clone()); + // } else { + // () + // } + // } + // _ => (), + // }; + emitter::render_cell_layout(" | ", location, &columns, &layout, |_, rotation| { if rotation == 0 { eprint!(" <--{{ Lookup '{}' inputs queried here", name); @@ -513,7 +547,7 @@ fn render_lookup( } } -impl VerifyFailure { +impl<'a> VerifyFailure<'a> { /// Emits this failure in pretty-printed format to stderr. pub(super) fn emit(&self, prover: &MockProver) { match self { diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index d7d2443e7d..dd54b8f18f 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -1,10 +1,13 @@ //! Metadata about circuits. +use super::metadata::Column as ColumnMetadata; use crate::plonk::{self, Any}; -use std::fmt; - +use std::{ + collections::HashMap, + fmt::{self, Debug}, +}; /// Metadata about a column within a circuit. -#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct Column { /// The type of the column. pub(super) column_type: Any, @@ -143,33 +146,74 @@ impl From<(Gate, usize, &'static str)> for Constraint { } /// Metadata about an assigned region within a circuit. -#[derive(Clone, Debug, PartialEq)] -pub struct Region { +#[derive(Clone, PartialEq, Eq)] +pub struct Region<'a> { /// The index of the region. These indices are assigned in the order in which /// `Layouter::assign_region` is called during `Circuit::synthesize`. pub(super) index: usize, /// The name of the region. This is specified by the region creator (such as a chip /// implementation), and is not enforced to be unique. pub(super) name: String, + /// A reference to the in-Region annotations + pub(super) column_annotations: Option<&'a HashMap>, } -impl fmt::Display for Region { +impl<'a> Debug for Region<'a> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!( + f, + "Region {} ('{}') with annotations: \n{:#?}", + self.index, self.name, self.column_annotations + ) + } +} + +impl<'a> fmt::Display for Region<'a> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "Region {} ('{}')", self.index, self.name) } } -impl From<(usize, String)> for Region { +impl<'a> From<(usize, String)> for Region<'a> { fn from((index, name): (usize, String)) -> Self { - Region { index, name } + Region { + index, + name, + column_annotations: None, + } } } -impl From<(usize, &str)> for Region { +impl<'a> From<(usize, &str)> for Region<'a> { fn from((index, name): (usize, &str)) -> Self { Region { index, name: name.to_owned(), + column_annotations: None, + } + } +} + +impl<'a> From<(usize, String, &'a HashMap)> for Region<'a> { + fn from( + (index, name, annotations): (usize, String, &'a HashMap), + ) -> Self { + Region { + index, + name, + column_annotations: Some(annotations), + } + } +} + +impl<'a> From<(usize, &str, &'a HashMap)> for Region<'a> { + fn from( + (index, name, annotations): (usize, &str, &'a HashMap), + ) -> Self { + Region { + index, + name: name.to_owned(), + column_annotations: Some(annotations), } } } From 9215ee0146e8f6eb120faae6c6f75c3eb921e91b Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 12 Dec 2022 15:37:00 +0100 Subject: [PATCH 03/21] feat: Update emitter module to print Column annotations --- halo2_proofs/src/dev/failure/emitter.rs | 86 +++++++++++++++++++------ 1 file changed, 68 insertions(+), 18 deletions(-) diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index 91525a20aa..f9413d9352 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -11,6 +11,7 @@ use crate::{ fn padded(p: char, width: usize, text: &str) -> String { let pad = width - text.len(); + format!( "{}{}{}", iter::repeat(p).take(pad - pad / 2).collect::(), @@ -19,6 +20,18 @@ fn padded(p: char, width: usize, text: &str) -> String { ) } +fn column_type_and_idx(column: &metadata::Column) -> String { + format!( + "{}{}", + match column.column_type { + Any::Advice => "A", + Any::Fixed => "F", + Any::Instance => "I", + }, + column.index + ) +} + /// Renders a cell layout around a given failure location. /// /// `highlight_row` is called at the end of each row, with the offset of the active row @@ -32,46 +45,83 @@ pub(super) fn render_cell_layout( highlight_row: impl Fn(Option, i32), ) { let col_width = |cells: usize| cells.to_string().len() + 3; + let mut col_headers = String::new(); // If we are in a region, show rows at offsets relative to it. Otherwise, just show // the rotations directly. let offset = match location { FailureLocation::InRegion { region, offset } => { - eprintln!("{}Cell layout in region '{}':", prefix, region.name); - eprint!("{} | Offset |", prefix); + col_headers + .push_str(format!("{}Cell layout in region '{}':\n", prefix, region.name).as_str()); + col_headers.push_str(format!("{} | Offset |", prefix).as_str()); Some(*offset as i32) } FailureLocation::OutsideRegion { row } => { - eprintln!("{}Cell layout at row {}:", prefix, row); - eprint!("{} |Rotation|", prefix); + col_headers.push_str(format!("{}Cell layout at row {}:\n", prefix, row).as_str()); + col_headers.push_str(format!("{} |Rotation|", prefix).as_str()); None } }; + eprint!("\n{}", col_headers); - // Print the assigned cells, and their region offset or rotation. - for (column, cells) in columns { - let width = col_width(*cells); + let widths: Vec = columns + .iter() + .map(|(col, _)| { + let size = match location { + FailureLocation::InRegion { region, offset } => { + if let Some(column_ann) = region.column_annotations { + if let Some(ann) = column_ann.get(&col) { + ann.len() + } else { + col_width(column_type_and_idx(col).as_str().len()) + } + } else { + col_width(column_type_and_idx(col).as_str().len()) + } + } + FailureLocation::OutsideRegion { row } => { + col_width(column_type_and_idx(col).as_str().len()) + } + }; + size + }) + .collect(); + + // Print the assigned cells, and their region offset or rotation + the column name at which they're assigned to. + for ((column, cells), &width) in columns.iter().zip(widths.iter()) { + //let width = col_width(*cells); eprint!( "{}|", padded( ' ', width, &format!( - "{}{}", - match column.column_type { - Any::Advice(_) => "A", - Any::Fixed => "F", - Any::Instance => "I", - }, - column.index, + "{}", + match location { + FailureLocation::InRegion { region, offset } => { + if let Some(column_ann) = region.column_annotations { + if let Some(ann) = column_ann.get(&column) { + format!("{}{}", ann.as_str(), "".to_string()) + } else { + column_type_and_idx(column) + } + } else { + column_type_and_idx(column) + } + } + FailureLocation::OutsideRegion { row } => { + column_type_and_idx(column) + } + } ) ) ); } + eprintln!(); eprint!("{} +--------+", prefix); - for cells in columns.values() { - eprint!("{}+", padded('-', col_width(*cells), "")); + for (cells, &width) in columns.values().zip(widths.iter()) { + eprint!("{}+", padded('-', width, "")); } eprintln!(); for (rotation, row) in layout { @@ -80,8 +130,8 @@ pub(super) fn render_cell_layout( prefix, padded(' ', 8, &(offset.unwrap_or(0) + rotation).to_string()) ); - for (col, cells) in columns { - let width = col_width(*cells); + for ((col, cells), &width) in columns.iter().zip(widths.iter()) { + //let width = col_width(*cells); eprint!( "{}|", padded( From 4aaf65d719abf17a54ed20f0cdd8b15acf27291d Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 12 Dec 2022 15:37:26 +0100 Subject: [PATCH 04/21] feat: Add lookup column annotations This adds the fn `annotate_lookup_column` for `ConstraintSystem` which allows to carry annotations for the lookup columns declared for a circuit within a CS. --- halo2_proofs/src/plonk/circuit.rs | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index a512c28ff3..cd7d8c8922 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -1,6 +1,7 @@ use core::cmp::max; use core::ops::{Add, Mul}; use ff::Field; +use std::collections::HashMap; use std::{ convert::TryFrom, ops::{Neg, Sub}, @@ -524,6 +525,12 @@ pub trait Assignment { NR: Into, N: FnOnce() -> NR; + /// TODO: Document + fn annotate_column(&mut self, annotation: A, column: Column) + where + A: FnOnce() -> AR, + AR: Into; + /// Exits the current region. /// /// Panics if we are not currently in a region (if `enter_region` was not called). @@ -1373,6 +1380,9 @@ pub struct ConstraintSystem { // input expressions and a sequence of table expressions involved in the lookup. pub(crate) lookups: Vec>, + // List of indexes of Fixed columns which are associated to a `TableColumn` tied to their annotation. + pub(crate) lookup_annotations: HashMap, + // Vector of fixed columns, which can be used to store constant values // that are copied into advice columns. pub(crate) constants: Vec>, @@ -1456,6 +1466,7 @@ impl Default for ConstraintSystem { instance_queries: Vec::new(), permutation: permutation::Argument::new(), lookups: Vec::new(), + lookup_annotations: HashMap::new(), constants: vec![], minimum_degree: None, } @@ -1840,6 +1851,17 @@ impl ConstraintSystem { } } + /// Annotate a Lookup column. + pub fn annotate_lookup_column(&mut self, column: TableColumn, annotation: A) + where + A: Fn() -> AR, + AR: Into, + { + // We don't care if the table has already an annotation. If it's the case we keep the original one. + self.lookup_annotations + .insert(column.inner().index, annotation().into()); + } + /// Allocate a new fixed column pub fn fixed_column(&mut self) -> Column { let tmp = Column { From d74c65816e2b1e04b6ab2a9ea765d6bf69154515 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 13 Dec 2022 13:35:59 +0100 Subject: [PATCH 05/21] feat: Add Lookup TableColumn annotations This allows to annotate lookup `TableColumn`s and print it's annotation within the `assert_satisfied` fn. This has required to change the `ConstraintSystem::lookup_annotations` to have keys as `metadata::Column` rather than `usize` as otherwise it's impossible within the `emitter` scope to distinguish between regular advice columns (local to the Region) and fixed columns which come from `TableColumn`s. --- halo2_proofs/src/dev.rs | 66 ++++++++++++------------- halo2_proofs/src/dev/failure.rs | 34 +++++-------- halo2_proofs/src/dev/failure/emitter.rs | 18 +++---- halo2_proofs/src/dev/metadata.rs | 6 +-- halo2_proofs/src/plonk/circuit.rs | 9 ++-- 5 files changed, 57 insertions(+), 76 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index acf5901700..b3234a7079 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -898,7 +898,6 @@ impl MockProver { *input_row, lookup.input_expressions.iter(), ), - //annotations: Some(&self.cs.lookup_annotations), }) } else { None @@ -1459,17 +1458,16 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - prover.assert_satisfied(); - // assert_eq!( - // prover.verify(), - // Err(vec![VerifyFailure::CellNotAssigned { - // gate: (0, "Equality check").into(), - // region: (0, "Faulty synthesis".to_owned()).into(), - // gate_offset: 1, - // column: Column::new(1, Any::Advice), - // offset: 1, - // }]) - // ); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::CellNotAssigned { + gate: (0, "Equality check").into(), + region: (0, "Faulty synthesis".to_owned()).into(), + gate_offset: 1, + column: Column::new(1, Any::Advice), + offset: 1, + }]) + ); } #[test] @@ -1493,7 +1491,7 @@ mod tests { let a = meta.advice_column(); let q = meta.complex_selector(); let table = meta.lookup_table_column(); - meta.annotate_lookup_column(table, || "Table Lookup"); + meta.annotate_lookup_column(table, || "Table1"); meta.lookup("lookup", |cells| { let a = cells.query_advice(a, Rotation::cur()); @@ -1591,17 +1589,16 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - prover.assert_satisfied(); - // assert_eq!( - // prover.verify(), - // Err(vec![VerifyFailure::Lookup { - // lookup_index: 0, - // location: FailureLocation::InRegion { - // region: (2, "Faulty synthesis").into(), - // offset: 1, - // } - // }]) - // ); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::Lookup { + lookup_index: 0, + location: FailureLocation::InRegion { + region: (2, "Faulty synthesis").into(), + offset: 1, + } + }]) + ); } #[test] @@ -1728,16 +1725,15 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - prover.assert_satisfied(); - // assert_eq!( - // prover.verify(), - // Err(vec![VerifyFailure::CellNotAssigned { - // gate: (0, "Equality check").into(), - // region: (0, "Faulty synthesis".to_owned()).into(), - // gate_offset: 1, - // column: Column::new(1, Any::Advice), - // offset: 1, - // }]) - // ); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::CellNotAssigned { + gate: (0, "Equality check").into(), + region: (0, "Faulty synthesis".to_owned()).into(), + gate_offset: 1, + column: Column::new(1, Any::Advice), + offset: 1, + }]) + ); } } diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index c253e210f8..9b8ab805da 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -346,8 +346,6 @@ fn render_constraint_not_satisfied( .or_insert(format!("x{}", i)); } - dbg!(location); - eprintln!("error: constraint not satisfied"); emitter::render_cell_layout(" ", location, &columns, &layout, |_, rotation| { if rotation == 0 { @@ -455,9 +453,19 @@ fn render_lookup( for i in 0..lookup.input_expressions.len() { eprint!("{}L{}", if i == 0 { "" } else { ", " }, i); } + eprint!(") ∉ ("); - for (i, column) in lookup_columns.enumerate() { - eprint!("{}{}", if i == 0 { "" } else { ", " }, column); + for (i, column) in table_columns.enumerate() { + eprint!( + "{}{}", + if i == 0 { "" } else { ", " }, + prover + .cs + .lookup_annotations + .get(&column) + .cloned() + .unwrap_or_else(|| format!("{}", column)) + ); } eprintln!(")"); @@ -513,24 +521,6 @@ fn render_lookup( emitter::expression_to_string(input, &layout) ); eprintln!(" ^"); - // // Include into the FailureLocation the TableColumns that we want to be annotated when displayed. - // let mut location_extended = location.clone(); - // match location_extended { - // FailureLocation::InRegion { mut region, offset } => { - // if region.column_annotations.is_none() { - // () - // } else if let Some(annotation) = prover.cs.lookup_annotations.get(&lookup_index) { - // region - // .column_annotations - // .as_mut() - // .unwrap() - // .insert(lookup_index, annotation.clone()); - // } else { - // () - // } - // } - // _ => (), - // }; emitter::render_cell_layout(" | ", location, &columns, &layout, |_, rotation| { if rotation == 0 { diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index f9413d9352..989663c289 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -5,8 +5,8 @@ use group::ff::Field; use super::FailureLocation; use crate::{ - dev::{metadata, util}, - plonk::{Advice, Any, Expression}, + dev::{metadata, util, MockProver}, + plonk::{Any, Expression}, }; fn padded(p: char, width: usize, text: &str) -> String { @@ -99,15 +99,11 @@ pub(super) fn render_cell_layout( "{}", match location { FailureLocation::InRegion { region, offset } => { - if let Some(column_ann) = region.column_annotations { - if let Some(ann) = column_ann.get(&column) { - format!("{}{}", ann.as_str(), "".to_string()) - } else { - column_type_and_idx(column) - } - } else { - column_type_and_idx(column) - } + region + .column_annotations + .map(|column_ann| column_ann.get(&column).cloned()) + .flatten() + .unwrap_or_else(|| column_type_and_idx(column)) } FailureLocation::OutsideRegion { row } => { column_type_and_idx(column) diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index dd54b8f18f..68ca54004c 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -160,11 +160,7 @@ pub struct Region<'a> { impl<'a> Debug for Region<'a> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!( - f, - "Region {} ('{}') with annotations: \n{:#?}", - self.index, self.name, self.column_annotations - ) + write!(f, "Region {} ('{}')", self.index, self.name) } } diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index cd7d8c8922..934feaad8d 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -8,6 +8,7 @@ use std::{ }; use super::{lookup, permutation, Assigned, Error}; +use crate::dev::metadata; use crate::{ circuit::{Layouter, Region, Value}, poly::Rotation, @@ -1381,7 +1382,7 @@ pub struct ConstraintSystem { pub(crate) lookups: Vec>, // List of indexes of Fixed columns which are associated to a `TableColumn` tied to their annotation. - pub(crate) lookup_annotations: HashMap, + pub(crate) lookup_annotations: HashMap, // Vector of fixed columns, which can be used to store constant values // that are copied into advice columns. @@ -1858,8 +1859,10 @@ impl ConstraintSystem { AR: Into, { // We don't care if the table has already an annotation. If it's the case we keep the original one. - self.lookup_annotations - .insert(column.inner().index, annotation().into()); + self.lookup_annotations.insert( + metadata::Column::from((Any::Fixed, column.inner().index)), + annotation().into(), + ); } /// Allocate a new fixed column From 0d720d3ece9241d79df8d56f708de8ed3d469635 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 13 Dec 2022 15:08:42 +0100 Subject: [PATCH 06/21] fix: Customly derive PartialEq for metadata::Region This allows to ignore the annotation map of the metadata::Region so that is easier to match against `VerifyFailure` errors in tests. --- halo2_proofs/src/dev/metadata.rs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index 68ca54004c..1848ccb75e 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -146,7 +146,7 @@ impl From<(Gate, usize, &'static str)> for Constraint { } /// Metadata about an assigned region within a circuit. -#[derive(Clone, PartialEq, Eq)] +#[derive(Clone)] pub struct Region<'a> { /// The index of the region. These indices are assigned in the order in which /// `Layouter::assign_region` is called during `Circuit::synthesize`. @@ -158,6 +158,18 @@ pub struct Region<'a> { pub(super) column_annotations: Option<&'a HashMap>, } +impl<'a> PartialEq for Region<'a> { + fn eq(&self, other: &Self) -> bool { + if self.index == other.index && self.name == other.name { + true + } else { + false + } + } +} + +impl<'a> Eq for Region<'a> {} + impl<'a> Debug for Region<'a> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "Region {} ('{}')", self.index, self.name) From 2e79a268731ffddb38327e3aef9aa07c735626ab Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 13 Dec 2022 15:09:23 +0100 Subject: [PATCH 07/21] fix: Update ConstraintNotSatisfied testcase --- halo2_proofs/src/dev.rs | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index b3234a7079..ae1a8b788b 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -1727,13 +1727,19 @@ mod tests { let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); assert_eq!( prover.verify(), - Err(vec![VerifyFailure::CellNotAssigned { - gate: (0, "Equality check").into(), - region: (0, "Faulty synthesis".to_owned()).into(), - gate_offset: 1, - column: Column::new(1, Any::Advice), - offset: 1, - }]) - ); + Err(vec![VerifyFailure::ConstraintNotSatisfied { + constraint: ((0, "Equality check").into(), 0, "").into(), + location: FailureLocation::InRegion { + region: (1, "Wrong synthesis").into(), + offset: 0, + }, + cell_values: vec![ + (((Any::Advice, 0).into(), 0).into(), "1".to_string()), + (((Any::Advice, 1).into(), 0).into(), "0".to_string()), + (((Any::Advice, 2).into(), 0).into(), "0x5".to_string()), + (((Any::Fixed, 0).into(), 0).into(), "0x7".to_string()), + ], + },]) + ) } } From c5d8401cdb8fbe3b8aa8aedb420cb4c1b4c02e3a Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 13 Dec 2022 17:55:51 +0100 Subject: [PATCH 08/21] fix: Update Debug & Display for VerifyFailure It was necessary to improve the `prover.verify` output also. To do so, this required auxiliary types which are obfuscated to any other part of the lib but that are necessary in order to be able to inject the Column names inside of the `Column` section itself. This also required to re-implement manually `Debug` and `Display` for this enum. This closes #705 --- halo2_proofs/src/dev/failure.rs | 58 ++++++++++++++++++++++++--- halo2_proofs/src/dev/metadata.rs | 67 +++++++++++++++++++++++++++++++- 2 files changed, 117 insertions(+), 8 deletions(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 9b8ab805da..39906d0fb0 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -1,15 +1,16 @@ use std::collections::{BTreeMap, HashMap, HashSet}; -use std::fmt; -use std::iter; +use std::fmt::{self, Debug}; use group::ff::Field; use halo2curves::FieldExt; +use super::metadata::DebugVirtualCell; use super::{ metadata, util::{self, AnyQuery}, MockProver, Region, }; +use crate::dev::metadata::Constraint; use crate::{ dev::Value, plonk::{Any, Column, ConstraintSystem, Expression, Gate}, @@ -19,7 +20,7 @@ use crate::{ mod emitter; /// The location within the circuit at which a particular [`VerifyFailure`] occurred. -#[derive(Debug, PartialEq, Eq)] +#[derive(Debug, PartialEq, Eq, Clone)] pub enum FailureLocation<'a> { /// A location inside a region. InRegion { @@ -106,7 +107,7 @@ impl<'a> FailureLocation<'a> { } /// The reasons why a particular circuit is not satisfied. -#[derive(Debug, PartialEq, Eq)] +#[derive(PartialEq, Eq)] pub enum VerifyFailure<'a> { /// A cell used in an active gate was not assigned to. CellNotAssigned { @@ -210,9 +211,17 @@ impl<'a> fmt::Display for VerifyFailure<'a> { cell_values, } => { writeln!(f, "{} is not satisfied {}", constraint, location)?; - for (name, value) in cell_values { - writeln!(f, "- {} = {}", name, value)?; + for (dvc, value) in cell_values.iter().map(|(vc, string)| { + let ann_map = match location { + FailureLocation::InRegion { region, offset } => region.column_annotations, + _ => None, + }; + + (DebugVirtualCell::from((vc, ann_map)), string) + }) { + writeln!(f, "- {} = {}", dvc, value); } + Ok(()) } Self::ConstraintPoisoned { constraint } => { @@ -244,6 +253,43 @@ impl<'a> fmt::Display for VerifyFailure<'a> { } } +impl<'a> Debug for VerifyFailure<'a> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + VerifyFailure::ConstraintNotSatisfied { + constraint, + location, + cell_values, + } => { + let constraint: Constraint = constraint.clone(); + #[derive(Debug)] + struct ConstraintCaseDebug<'a> { + constraint: Constraint, + location: FailureLocation<'a>, + cell_values: Vec<(DebugVirtualCell, String)>, + } + + let ann_map = match location { + FailureLocation::InRegion { region, offset } => region.column_annotations, + _ => None, + }; + + let debug = ConstraintCaseDebug { + constraint: constraint.clone(), + location: location.clone(), + cell_values: cell_values + .iter() + .map(|(vc, value)| (DebugVirtualCell::from((vc, ann_map)), value.clone())) + .collect(), + }; + + write!(f, "{:#?}", debug) + } + _ => write!(f, "{:#?}", self), + } + } +} + /// Renders `VerifyFailure::CellNotAssigned`. /// /// ```text diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index 1848ccb75e..a8e89f8532 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -36,6 +36,42 @@ impl From> for Column { } } +/// A helper structure that allows to print a Column with it's annotation as a single structure. +#[derive(Debug, Clone)] +struct DebugColumn { + /// The type of the column. + column_type: Any, + /// The index of the column. + index: usize, + /// Annotation of the column + annotation: String, +} + +impl From<(Column, Option<&HashMap>)> for DebugColumn { + fn from(info: (Column, Option<&HashMap>)) -> Self { + DebugColumn { + column_type: info.0.column_type, + index: info.0.index, + annotation: info + .1 + .map(|map| map.get(&info.0)) + .flatten() + .cloned() + .unwrap_or_else(|| String::new()), + } + } +} + +impl fmt::Display for DebugColumn { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!( + f, + "Column('{:?}', {} - {})", + self.column_type, self.index, self.annotation + ) + } +} + /// A "virtual cell" is a PLONK cell that has been queried at a particular relative offset /// within a custom gate. #[derive(Debug, PartialEq, Eq, PartialOrd, Ord)] @@ -85,8 +121,35 @@ impl fmt::Display for VirtualCell { } } +#[derive(Clone, Debug)] +pub(super) struct DebugVirtualCell { + name: &'static str, + column: DebugColumn, + rotation: i32, +} + +impl From<(&VirtualCell, Option<&HashMap>)> for DebugVirtualCell { + fn from(info: (&VirtualCell, Option<&HashMap>)) -> Self { + DebugVirtualCell { + name: info.0.name, + column: DebugColumn::from((info.0.column, info.1)), + rotation: info.0.rotation, + } + } +} + +impl fmt::Display for DebugVirtualCell { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}@{}", self.column, self.rotation)?; + if !self.name.is_empty() { + write!(f, "({})", self.name)?; + } + Ok(()) + } +} + /// Metadata about a configured gate within a circuit. -#[derive(Debug, PartialEq)] +#[derive(Debug, PartialEq, Eq, Clone, Copy)] pub struct Gate { /// The index of the active gate. These indices are assigned in the order in which /// `ConstraintSystem::create_gate` is called during `Circuit::configure`. @@ -109,7 +172,7 @@ impl From<(usize, &'static str)> for Gate { } /// Metadata about a configured constraint within a circuit. -#[derive(Debug, PartialEq)] +#[derive(Debug, PartialEq, Eq, Clone, Copy)] pub struct Constraint { /// The gate containing the constraint. pub(super) gate: Gate, From 5c3a5164fff170b379bd64ec5f2c1d27f2b741e0 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 13 Dec 2022 18:38:31 +0100 Subject: [PATCH 09/21] fix: Address clippy & warnings --- halo2_proofs/src/circuit.rs | 2 +- halo2_proofs/src/circuit/floor_planner/v1.rs | 6 +-- halo2_proofs/src/circuit/layouter.rs | 4 +- halo2_proofs/src/dev/cost.rs | 4 +- halo2_proofs/src/dev/failure.rs | 16 ++++---- halo2_proofs/src/dev/failure/emitter.rs | 40 ++++++++++---------- halo2_proofs/src/dev/metadata.rs | 8 +--- halo2_proofs/src/plonk/keygen.rs | 4 +- halo2_proofs/src/plonk/prover.rs | 4 +- 9 files changed, 42 insertions(+), 46 deletions(-) diff --git a/halo2_proofs/src/circuit.rs b/halo2_proofs/src/circuit.rs index 4f8c26b35c..8fea4330d9 100644 --- a/halo2_proofs/src/circuit.rs +++ b/halo2_proofs/src/circuit.rs @@ -207,7 +207,7 @@ impl<'r, F: Field> Region<'r, F> { } /// Annotates a column. - pub(crate) fn name_column(&mut self, annotation: A, column: T) + pub fn name_column(&mut self, annotation: A, column: T) where A: Fn() -> AR, AR: Into, diff --git a/halo2_proofs/src/circuit/floor_planner/v1.rs b/halo2_proofs/src/circuit/floor_planner/v1.rs index 45cafee8e2..7f9253c047 100644 --- a/halo2_proofs/src/circuit/floor_planner/v1.rs +++ b/halo2_proofs/src/circuit/floor_planner/v1.rs @@ -483,10 +483,10 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> RegionLayouter for V1Region<'r fn name_column<'v>( &'v mut self, - annotation: &'v (dyn Fn() -> String + 'v), - column: Column, + _annotation: &'v (dyn Fn() -> String + 'v), + _column: Column, ) { - unimplemented!() + // Do nothing } fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result<(), Error> { diff --git a/halo2_proofs/src/circuit/layouter.rs b/halo2_proofs/src/circuit/layouter.rs index e0fd0b5de4..394760ab65 100644 --- a/halo2_proofs/src/circuit/layouter.rs +++ b/halo2_proofs/src/circuit/layouter.rs @@ -284,8 +284,8 @@ impl RegionLayouter for RegionShape { fn name_column<'v>( &'v mut self, - annotation: &'v (dyn Fn() -> String + 'v), - column: Column, + _annotation: &'v (dyn Fn() -> String + 'v), + _column: Column, ) { // Do nothing } diff --git a/halo2_proofs/src/dev/cost.rs b/halo2_proofs/src/dev/cost.rs index ed25e5ce91..d3043508f5 100644 --- a/halo2_proofs/src/dev/cost.rs +++ b/halo2_proofs/src/dev/cost.rs @@ -122,12 +122,12 @@ impl Assignment for Assembly { Value::unknown() } - fn annotate_column(&mut self, annotation: A, column: Column) + fn annotate_column(&mut self, _annotation: A, _column: Column) where A: FnOnce() -> AR, AR: Into, { - unimplemented!() + // Do nothing } fn push_namespace(&mut self, _: N) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 39906d0fb0..fc915423fe 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -1,14 +1,15 @@ -use std::collections::{BTreeMap, HashMap, HashSet}; +use std::collections::{BTreeMap, HashSet}; use std::fmt::{self, Debug}; use group::ff::Field; use halo2curves::FieldExt; use super::metadata::DebugVirtualCell; +use super::MockProver; use super::{ metadata, util::{self, AnyQuery}, - MockProver, Region, + Region, }; use crate::dev::metadata::Constraint; use crate::{ @@ -213,13 +214,15 @@ impl<'a> fmt::Display for VerifyFailure<'a> { writeln!(f, "{} is not satisfied {}", constraint, location)?; for (dvc, value) in cell_values.iter().map(|(vc, string)| { let ann_map = match location { - FailureLocation::InRegion { region, offset } => region.column_annotations, + FailureLocation::InRegion { region, offset: _ } => { + region.column_annotations + } _ => None, }; (DebugVirtualCell::from((vc, ann_map)), string) }) { - writeln!(f, "- {} = {}", dvc, value); + let _ = writeln!(f, "- {} = {}", dvc, value); } Ok(()) @@ -261,7 +264,6 @@ impl<'a> Debug for VerifyFailure<'a> { location, cell_values, } => { - let constraint: Constraint = constraint.clone(); #[derive(Debug)] struct ConstraintCaseDebug<'a> { constraint: Constraint, @@ -270,12 +272,12 @@ impl<'a> Debug for VerifyFailure<'a> { } let ann_map = match location { - FailureLocation::InRegion { region, offset } => region.column_annotations, + FailureLocation::InRegion { region, offset: _ } => region.column_annotations, _ => None, }; let debug = ConstraintCaseDebug { - constraint: constraint.clone(), + constraint: *constraint, location: location.clone(), cell_values: cell_values .iter() diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index 989663c289..ad63d1dbd0 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -5,7 +5,7 @@ use group::ff::Field; use super::FailureLocation; use crate::{ - dev::{metadata, util, MockProver}, + dev::{metadata, util}, plonk::{Any, Expression}, }; @@ -68,9 +68,9 @@ pub(super) fn render_cell_layout( .iter() .map(|(col, _)| { let size = match location { - FailureLocation::InRegion { region, offset } => { + FailureLocation::InRegion { region, offset: _ } => { if let Some(column_ann) = region.column_annotations { - if let Some(ann) = column_ann.get(&col) { + if let Some(ann) = column_ann.get(col) { ann.len() } else { col_width(column_type_and_idx(col).as_str().len()) @@ -79,7 +79,7 @@ pub(super) fn render_cell_layout( col_width(column_type_and_idx(col).as_str().len()) } } - FailureLocation::OutsideRegion { row } => { + FailureLocation::OutsideRegion { row: _ } => { col_width(column_type_and_idx(col).as_str().len()) } }; @@ -88,35 +88,33 @@ pub(super) fn render_cell_layout( .collect(); // Print the assigned cells, and their region offset or rotation + the column name at which they're assigned to. - for ((column, cells), &width) in columns.iter().zip(widths.iter()) { + for ((column, _), &width) in columns.iter().zip(widths.iter()) { //let width = col_width(*cells); eprint!( "{}|", padded( ' ', width, - &format!( - "{}", - match location { - FailureLocation::InRegion { region, offset } => { - region - .column_annotations - .map(|column_ann| column_ann.get(&column).cloned()) - .flatten() - .unwrap_or_else(|| column_type_and_idx(column)) - } - FailureLocation::OutsideRegion { row } => { - column_type_and_idx(column) - } + &match location { + FailureLocation::InRegion { region, offset: _ } => { + region + .column_annotations + .map(|column_ann| column_ann.get(column).cloned()) + .flatten() + .unwrap_or_else(|| column_type_and_idx(column)) } - ) + FailureLocation::OutsideRegion { row: _ } => { + column_type_and_idx(column) + } + } + .to_string() ) ); } eprintln!(); eprint!("{} +--------+", prefix); - for (cells, &width) in columns.values().zip(widths.iter()) { + for &width in widths.iter() { eprint!("{}+", padded('-', width, "")); } eprintln!(); @@ -126,7 +124,7 @@ pub(super) fn render_cell_layout( prefix, padded(' ', 8, &(offset.unwrap_or(0) + rotation).to_string()) ); - for ((col, cells), &width) in columns.iter().zip(widths.iter()) { + for ((col, _), &width) in columns.iter().zip(widths.iter()) { //let width = col_width(*cells); eprint!( "{}|", diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index a8e89f8532..919ca79352 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -57,7 +57,7 @@ impl From<(Column, Option<&HashMap>)> for DebugColumn { .map(|map| map.get(&info.0)) .flatten() .cloned() - .unwrap_or_else(|| String::new()), + .unwrap_or_else(String::new), } } } @@ -223,11 +223,7 @@ pub struct Region<'a> { impl<'a> PartialEq for Region<'a> { fn eq(&self, other: &Self) -> bool { - if self.index == other.index && self.name == other.name { - true - } else { - false - } + self.index == other.index && self.name == other.name } } diff --git a/halo2_proofs/src/plonk/keygen.rs b/halo2_proofs/src/plonk/keygen.rs index 6586c6014a..7a8d3dcacd 100644 --- a/halo2_proofs/src/plonk/keygen.rs +++ b/halo2_proofs/src/plonk/keygen.rs @@ -178,12 +178,12 @@ impl Assignment for Assembly { Value::unknown() } - fn annotate_column(&mut self, annotation: A, column: Column) + fn annotate_column(&mut self, _annotation: A, _column: Column) where A: FnOnce() -> AR, AR: Into, { - unimplemented!() + // Do nothing } fn push_namespace(&mut self, _: N) diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index b725832502..4114c4e707 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -282,12 +282,12 @@ pub fn create_proof< Ok(()) } - fn annotate_column(&mut self, annotation: A, column: Column) + fn annotate_column(&mut self, _annotation: A, _column: Column) where A: FnOnce() -> AR, AR: Into, { - unimplemented!() + // Do nothing } fn push_namespace(&mut self, _: N) From 9807812c5c23a84156fbf0e71e7004bf26f88c74 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 13 Dec 2022 18:59:17 +0100 Subject: [PATCH 10/21] fix: Add final comments & polish --- halo2_proofs/src/circuit.rs | 5 ++++- halo2_proofs/src/circuit/layouter.rs | 5 ++++- halo2_proofs/src/dev.rs | 2 +- halo2_proofs/src/dev/failure.rs | 2 -- halo2_proofs/src/dev/failure/emitter.rs | 2 -- halo2_proofs/src/dev/metadata.rs | 3 ++- 6 files changed, 11 insertions(+), 8 deletions(-) diff --git a/halo2_proofs/src/circuit.rs b/halo2_proofs/src/circuit.rs index 8fea4330d9..d0b1e0c02b 100644 --- a/halo2_proofs/src/circuit.rs +++ b/halo2_proofs/src/circuit.rs @@ -206,7 +206,10 @@ impl<'r, F: Field> Region<'r, F> { .enable_selector(&|| annotation().into(), selector, offset) } - /// Annotates a column. + /// Allows the circuit implementor to name/annotate a Column within a Region context. + /// + /// This is useful in order to improve the amount of information that `prover.verify()` + /// and `prover.assert_satisfied()` can provide. pub fn name_column(&mut self, annotation: A, column: T) where A: Fn() -> AR, diff --git a/halo2_proofs/src/circuit/layouter.rs b/halo2_proofs/src/circuit/layouter.rs index 394760ab65..f73d7d7d73 100644 --- a/halo2_proofs/src/circuit/layouter.rs +++ b/halo2_proofs/src/circuit/layouter.rs @@ -48,7 +48,10 @@ pub trait RegionLayouter: fmt::Debug { offset: usize, ) -> Result<(), Error>; - /// Annotate a Column within a Region context. + /// Allows the circuit implementor to name/annotate a Column within a Region context. + /// + /// This is useful in order to improve the amount of information that `prover.verify()` + /// and `prover.assert_satisfied()` can provide. fn name_column<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index ae1a8b788b..d6f7fa01ec 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -58,7 +58,7 @@ struct Region { /// The selectors that have been enabled in this region. All other selectors are by /// construction not enabled. enabled_selectors: HashMap>, - /// Annotations of the columns. + /// Annotations given to Advice, Fixed or Instance columns within a region context. annotations: HashMap, /// The cells assigned in this region. We store this as a `Vec` so that if any cells /// are double-assigned, they will be visibly darker. diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index fc915423fe..0d7897adda 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -178,8 +178,6 @@ pub enum VerifyFailure<'a> { /// - The input expressions use a column queried at a non-zero `Rotation`, and the /// lookup is active on a row adjacent to an unrelated region. location: FailureLocation<'a>, - // Maps lookup columns to their annotations from an outside-region perspective. - //annotations: Option<&'a HashMap>, }, /// A permutation did not preserve the original value of a cell. Permutation { diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index ad63d1dbd0..52ce461682 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -89,7 +89,6 @@ pub(super) fn render_cell_layout( // Print the assigned cells, and their region offset or rotation + the column name at which they're assigned to. for ((column, _), &width) in columns.iter().zip(widths.iter()) { - //let width = col_width(*cells); eprint!( "{}|", padded( @@ -125,7 +124,6 @@ pub(super) fn render_cell_layout( padded(' ', 8, &(offset.unwrap_or(0) + rotation).to_string()) ); for ((col, _), &width) in columns.iter().zip(widths.iter()) { - //let width = col_width(*cells); eprint!( "{}|", padded( diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index 919ca79352..47ffb90604 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -121,6 +121,7 @@ impl fmt::Display for VirtualCell { } } +/// Helper structure used to be able to inject Column annotations inside a `Display` or `Debug` call. #[derive(Clone, Debug)] pub(super) struct DebugVirtualCell { name: &'static str, @@ -217,7 +218,7 @@ pub struct Region<'a> { /// The name of the region. This is specified by the region creator (such as a chip /// implementation), and is not enforced to be unique. pub(super) name: String, - /// A reference to the in-Region annotations + /// A reference to the annotations of the Columns that exist within this `Region`. pub(super) column_annotations: Option<&'a HashMap>, } From 1276fafa911e6f1fd97b5d70851311c42d886a82 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 13 Dec 2022 23:33:49 +0100 Subject: [PATCH 11/21] fix: Resolve cherry-pick merge conflics & errors --- halo2_proofs/src/dev.rs | 171 ++++++++++++++---------- halo2_proofs/src/dev/failure.rs | 17 +-- halo2_proofs/src/dev/failure/emitter.rs | 4 +- halo2_proofs/src/plonk/prover.rs | 143 ++++---------------- 4 files changed, 128 insertions(+), 207 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index d6f7fa01ec..2541ead9f7 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -652,39 +652,17 @@ impl MockProver { // Determine where this cell should have been assigned. let cell_row = ((gate_row + n + cell.rotation.0) % n) as usize; - match cell.column.column_type() { - Any::Instance => { - // Handle instance cells, which are not in the region. - let instance_value = - &self.instance[cell.column.index()][cell_row]; - match instance_value { - InstanceValue::Assigned(_) => None, - _ => Some(VerifyFailure::InstanceCellNotAssigned { - gate: (gate_index, gate.name()).into(), - region: (r_i, r.name.clone(), &r.annotations) - .into(), - gate_offset: *selector_row, - column: cell.column.try_into().unwrap(), - row: cell_row, - }), - } - } - _ => { - // Check that it was assigned! - if r.cells.contains(&(cell.column, cell_row)) { - None - } else { - Some(VerifyFailure::CellNotAssigned { - gate: (gate_index, gate.name()).into(), - region: (r_i, r.name.clone(), &r.annotations) - .into(), - gate_offset: *selector_row, - column: cell.column, - offset: cell_row as isize - - r.rows.unwrap().0 as isize, - }) - } - } + // Check that it was assigned! + if r.cells.get(&(cell.column, cell_row)).is_some() { + None + } else { + Some(VerifyFailure::CellNotAssigned { + gate: (gate_index, gate.name()).into(), + region: (r_i, r.name.clone(), &r.annotations).into(), + gate_offset: *selector_row, + column: cell.column, + offset: cell_row as isize - r.rows.unwrap().0 as isize, + }) } }) }) @@ -1384,8 +1362,8 @@ mod tests { use crate::{ circuit::{Layouter, SimpleFloorPlanner, Value}, plonk::{ - Advice, Any, Circuit, Column, ConstraintSystem, Error, Expression, Fixed, Selector, - TableColumn, + sealed::SealedPhase, Advice, Any, Circuit, Column, ConstraintSystem, Error, Expression, + FirstPhase, Fixed, Selector, TableColumn, }, poly::Rotation, }; @@ -1458,16 +1436,23 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - assert_eq!( - prover.verify(), - Err(vec![VerifyFailure::CellNotAssigned { - gate: (0, "Equality check").into(), - region: (0, "Faulty synthesis".to_owned()).into(), - gate_offset: 1, - column: Column::new(1, Any::Advice), - offset: 1, - }]) - ); + //print!("{:?}", prover.verify()); + prover.assert_satisfied(); + // assert_eq!( + // prover.verify(), + // Err(vec![VerifyFailure::CellNotAssigned { + // gate: (0, "Equality check").into(), + // region: (0, "Faulty synthesis".to_owned()).into(), + // gate_offset: 1, + // column: Column::new( + // 1, + // Any::Advice(Advice { + // phase: FirstPhase.to_sealed() + // }) + // ), + // offset: 1, + // }]) + // ); } #[test] @@ -1589,16 +1574,19 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - assert_eq!( - prover.verify(), - Err(vec![VerifyFailure::Lookup { - lookup_index: 0, - location: FailureLocation::InRegion { - region: (2, "Faulty synthesis").into(), - offset: 1, - } - }]) - ); + //print!("{:?}", prover.verify()); + prover.assert_satisfied(); + // assert_eq!( + // prover.verify(), + // Err(vec![VerifyFailure::Lookup { + // name: "lookup", + // lookup_index: 0, + // location: FailureLocation::InRegion { + // region: (2, "Faulty synthesis").into(), + // offset: 1, + // } + // }]) + // ); } #[test] @@ -1725,21 +1713,62 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - assert_eq!( - prover.verify(), - Err(vec![VerifyFailure::ConstraintNotSatisfied { - constraint: ((0, "Equality check").into(), 0, "").into(), - location: FailureLocation::InRegion { - region: (1, "Wrong synthesis").into(), - offset: 0, - }, - cell_values: vec![ - (((Any::Advice, 0).into(), 0).into(), "1".to_string()), - (((Any::Advice, 1).into(), 0).into(), "0".to_string()), - (((Any::Advice, 2).into(), 0).into(), "0x5".to_string()), - (((Any::Fixed, 0).into(), 0).into(), "0x7".to_string()), - ], - },]) - ) + //print!("{:?}", prover.verify()); + prover.assert_satisfied(); + // assert_eq!( + // prover.verify(), + // Err(vec![VerifyFailure::ConstraintNotSatisfied { + // constraint: ((0, "Equality check").into(), 0, "").into(), + // location: FailureLocation::InRegion { + // region: (1, "Wrong synthesis").into(), + // offset: 0, + // }, + // cell_values: vec![ + // ( + // ( + // ( + // Any::Advice(Advice { + // phase: FirstPhase.to_sealed() + // }), + // 0 + // ) + // .into(), + // 0 + // ) + // .into(), + // "1".to_string() + // ), + // ( + // ( + // ( + // Any::Advice(Advice { + // phase: FirstPhase.to_sealed() + // }), + // 1 + // ) + // .into(), + // 0 + // ) + // .into(), + // "0".to_string() + // ), + // ( + // ( + // ( + // Any::Advice(Advice { + // phase: FirstPhase.to_sealed() + // }), + // 2 + // ) + // .into(), + // 0 + // ) + // .into(), + // "0x5".to_string() + // ), + // (((Any::Fixed, 0).into(), 0).into(), "0x7".to_string()), + // ], + // },]) + // ) } } diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 0d7897adda..d8009d58f4 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -13,7 +13,7 @@ use super::{ }; use crate::dev::metadata::Constraint; use crate::{ - dev::Value, + dev::{Instance, Value}, plonk::{Any, Column, ConstraintSystem, Expression, Gate}, poly::Rotation, }; @@ -104,6 +104,7 @@ impl<'a> FailureLocation<'a> { region: (r_i, r.name.clone(), &r.annotations).into(), offset: failure_row - r.rows.unwrap().0, }) + .unwrap_or_else(|| FailureLocation::OutsideRegion { row: failure_row }) } } @@ -126,20 +127,6 @@ pub enum VerifyFailure<'a> { /// offset 0, but the gate uses `Rotation::prev()`). offset: isize, }, - /// An instance cell used in an active gate was not assigned to. - InstanceCellNotAssigned { - /// The index of the active gate. - gate: metadata::Gate, - /// The region in which this gate was activated. - region: metadata::Region<'a>, - /// The offset (relative to the start of the region) at which the active gate - /// queries this cell. - gate_offset: usize, - /// The column in which this cell should be assigned. - column: Column, - /// The absolute row at which this cell should be assigned. - row: usize, - }, /// A constraint was not satisfied for a particular row. ConstraintNotSatisfied { /// The polynomial constraint that is not satisfied. diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index 52ce461682..712d2ef65d 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -6,7 +6,7 @@ use group::ff::Field; use super::FailureLocation; use crate::{ dev::{metadata, util}, - plonk::{Any, Expression}, + plonk::{Advice, Any, Expression}, }; fn padded(p: char, width: usize, text: &str) -> String { @@ -24,7 +24,7 @@ fn column_type_and_idx(column: &metadata::Column) -> String { format!( "{}{}", match column.column_type { - Any::Advice => "A", + Any::Advice(_) => "A", Any::Fixed => "F", Any::Instance => "I", }, diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index 4114c4e707..dcb3855687 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -170,6 +170,14 @@ pub fn create_proof< Ok(()) } + fn annotate_column(&mut self, annotation: A, column: Column) + where + A: FnOnce() -> AR, + AR: Into, + { + // Do nothing + } + fn query_instance(&self, column: Column, row: usize) -> Result, Error> { if !self.usable_rows.contains(&row) { return Err(Error::not_enough_rows_available(self.k)); @@ -182,125 +190,22 @@ pub fn create_proof< .ok_or(Error::BoundsFailure) } - fn exit_region(&mut self) { - // Do nothing; we don't care about regions in this context. - } - - fn enable_selector( - &mut self, - _: A, - _: &Selector, - _: usize, - ) -> Result<(), Error> - where - A: FnOnce() -> AR, - AR: Into, - { - // We only care about advice columns here - - Ok(()) - } - - fn query_instance( - &self, - column: Column, - row: usize, - ) -> Result, Error> { - if !self.usable_rows.contains(&row) { - return Err(Error::not_enough_rows_available(self.k)); - } - - self.instances - .get(column.index()) - .and_then(|column| column.get(row)) - .map(|v| Value::known(*v)) - .ok_or(Error::BoundsFailure) - } - - fn assign_advice( - &mut self, - _: A, - column: Column, - row: usize, - to: V, - ) -> Result<(), Error> - where - V: FnOnce() -> Value, - VR: Into>, - A: FnOnce() -> AR, - AR: Into, - { - if !self.usable_rows.contains(&row) { - return Err(Error::not_enough_rows_available(self.k)); - } - - *self - .advice - .get_mut(column.index()) - .and_then(|v| v.get_mut(row)) - .ok_or(Error::BoundsFailure)? = to().into_field().assign()?; - - Ok(()) - } - - fn assign_fixed( - &mut self, - _: A, - _: Column, - _: usize, - _: V, - ) -> Result<(), Error> - where - V: FnOnce() -> Value, - VR: Into>, - A: FnOnce() -> AR, - AR: Into, - { - // We only care about advice columns here - - Ok(()) - } - - fn copy( - &mut self, - _: Column, - _: usize, - _: Column, - _: usize, - ) -> Result<(), Error> { - // We only care about advice columns here - - Ok(()) - } - - fn fill_from_row( - &mut self, - _: Column, - _: usize, - _: Value>, - ) -> Result<(), Error> { - Ok(()) - } - - fn annotate_column(&mut self, _annotation: A, _column: Column) - where - A: FnOnce() -> AR, - AR: Into, - { - // Do nothing - } - - fn push_namespace(&mut self, _: N) - where - NR: Into, - N: FnOnce() -> NR, - { - // Do nothing; we don't care about namespaces in this context. - } - - fn pop_namespace(&mut self, _: Option) { - // Do nothing; we don't care about namespaces in this context. - } + fn assign_advice( + &mut self, + _: A, + column: Column, + row: usize, + to: V, + ) -> Result<(), Error> + where + V: FnOnce() -> Value, + VR: Into>, + A: FnOnce() -> AR, + AR: Into, + { + // Ignore assignment of advice column in different phase than current one. + if self.current_phase != column.column_type().phase { + return Ok(()); } if !self.usable_rows.contains(&row) { From 5fc32fdada62deb2fa8d2f36dc13f9b753f6040c Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 10 Jan 2023 11:41:53 +0100 Subject: [PATCH 12/21] chore: Change DebugColumn visibility --- halo2_proofs/src/dev/metadata.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index 47ffb90604..4e05f3ff9a 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -38,7 +38,7 @@ impl From> for Column { /// A helper structure that allows to print a Column with it's annotation as a single structure. #[derive(Debug, Clone)] -struct DebugColumn { +pub(super) struct DebugColumn { /// The type of the column. column_type: Any, /// The index of the column. @@ -57,7 +57,7 @@ impl From<(Column, Option<&HashMap>)> for DebugColumn { .map(|map| map.get(&info.0)) .flatten() .cloned() - .unwrap_or_else(String::new), + .unwrap_or_default(), } } } From 864aa3e54d95e2ff28c253e592eecb7528dfeff3 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 10 Jan 2023 11:57:01 +0100 Subject: [PATCH 13/21] chore: Allow to fetch annotations from metadata --- halo2_proofs/src/dev/failure.rs | 39 +++++++++++++++++++++++++------- halo2_proofs/src/dev/metadata.rs | 12 ++++++++++ 2 files changed, 43 insertions(+), 8 deletions(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index d8009d58f4..3415e33d4d 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -4,7 +4,7 @@ use std::fmt::{self, Debug}; use group::ff::Field; use halo2curves::FieldExt; -use super::metadata::DebugVirtualCell; +use super::metadata::{DebugColumn, DebugVirtualCell}; use super::MockProver; use super::{ metadata, @@ -50,6 +50,28 @@ impl<'a> fmt::Display for FailureLocation<'a> { } impl<'a> FailureLocation<'a> { + /// Returns a `DebugColumn` from Column metadata and `&self`. + pub(super) fn get_debug_column(&self, metadata: metadata::Column) -> DebugColumn { + match self { + Self::InRegion { region, .. } => { + DebugColumn::from((metadata, region.column_annotations)) + } + _ => DebugColumn::from((metadata, None)), + } + } + + /// Fetch the annotation of a `Column` within a `FailureLocation` providing it's associated metadata. + /// + /// This function will return `None` if: + /// - `self` matches to `Self::OutsideRegion`. + /// - There's no annotation map generated for the `Region` inside `self`. + /// - There's no entry on the annotation map corresponding to the metadata provided. + pub(super) fn get_column_annotation(&self, metadata: metadata::Column) -> Option { + match self { + Self::InRegion { region, .. } => region.get_column_annotation(metadata), + _ => None, + } + } pub(super) fn find_expressions( cs: &ConstraintSystem, regions: &'a [Region], @@ -187,8 +209,8 @@ impl<'a> fmt::Display for VerifyFailure<'a> { } => { write!( f, - "{} uses {} at offset {}, which requires cell in column {:?} at offset {} to be assigned.", - region, gate, gate_offset, column, offset + "{} uses {} at offset {}, which requires cell in column {:?} at offset {} with annotation {:?} to be assigned.", + region, gate, gate_offset, column, offset, region.get_column_annotation((*column).into()) ) } Self::ConstraintNotSatisfied { @@ -197,6 +219,7 @@ impl<'a> fmt::Display for VerifyFailure<'a> { cell_values, } => { writeln!(f, "{} is not satisfied {}", constraint, location)?; + println!("All OK"); for (dvc, value) in cell_values.iter().map(|(vc, string)| { let ann_map = match location { FailureLocation::InRegion { region, offset: _ } => { @@ -209,7 +232,6 @@ impl<'a> fmt::Display for VerifyFailure<'a> { }) { let _ = writeln!(f, "- {} = {}", dvc, value); } - Ok(()) } Self::ConstraintPoisoned { constraint } => { @@ -233,8 +255,9 @@ impl<'a> fmt::Display for VerifyFailure<'a> { Self::Permutation { column, location } => { write!( f, - "Equality constraint not satisfied by cell ({:?}, {})", - column, location + "Equality constraint not satisfied by cell ({}, {})", + location.get_debug_column(*column), + location ) } } @@ -272,7 +295,7 @@ impl<'a> Debug for VerifyFailure<'a> { write!(f, "{:#?}", debug) } - _ => write!(f, "{:#?}", self), + _ => write!(f, "{:#}", self), } } } @@ -494,7 +517,7 @@ fn render_lookup( if i == 0 { "" } else { ", " }, prover .cs - .lookup_annotations + .general_column_annotations .get(&column) .cloned() .unwrap_or_else(|| format!("{}", column)) diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index 4e05f3ff9a..e56e482773 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -222,6 +222,18 @@ pub struct Region<'a> { pub(super) column_annotations: Option<&'a HashMap>, } +impl<'a> Region<'a> { + /// Fetch the annotation of a `Column` within a `Region` providing it's associated metadata. + /// + /// This function will return `None` if: + /// - There's no annotation map generated for this `Region`. + /// - There's no entry on the annotation map corresponding to the metadata provided. + pub(crate) fn get_column_annotation(&self, metadata: ColumnMetadata) -> Option { + self.column_annotations + .and_then(|map| map.get(&metadata).cloned()) + } +} + impl<'a> PartialEq for Region<'a> { fn eq(&self, other: &Self) -> bool { self.index == other.index && self.name == other.name From 6485966728914e74b448d0b8ccc96af6bdad23be Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 10 Jan 2023 14:13:57 +0100 Subject: [PATCH 14/21] chore: Fix clippy lints --- halo2_proofs/src/dev/failure.rs | 14 +------------- halo2_proofs/src/dev/failure/emitter.rs | 3 +-- halo2_proofs/src/dev/graph.rs | 8 ++++++++ halo2_proofs/src/dev/graph/layout.rs | 8 ++++++++ halo2_proofs/src/dev/metadata.rs | 3 +-- halo2_proofs/src/plonk/circuit.rs | 6 +++--- halo2_proofs/src/plonk/prover.rs | 2 +- 7 files changed, 23 insertions(+), 21 deletions(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 3415e33d4d..806f77aac8 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -60,18 +60,6 @@ impl<'a> FailureLocation<'a> { } } - /// Fetch the annotation of a `Column` within a `FailureLocation` providing it's associated metadata. - /// - /// This function will return `None` if: - /// - `self` matches to `Self::OutsideRegion`. - /// - There's no annotation map generated for the `Region` inside `self`. - /// - There's no entry on the annotation map corresponding to the metadata provided. - pub(super) fn get_column_annotation(&self, metadata: metadata::Column) -> Option { - match self { - Self::InRegion { region, .. } => region.get_column_annotation(metadata), - _ => None, - } - } pub(super) fn find_expressions( cs: &ConstraintSystem, regions: &'a [Region], @@ -219,7 +207,6 @@ impl<'a> fmt::Display for VerifyFailure<'a> { cell_values, } => { writeln!(f, "{} is not satisfied {}", constraint, location)?; - println!("All OK"); for (dvc, value) in cell_values.iter().map(|(vc, string)| { let ann_map = match location { FailureLocation::InRegion { region, offset: _ } => { @@ -272,6 +259,7 @@ impl<'a> Debug for VerifyFailure<'a> { location, cell_values, } => { + #[allow(dead_code)] #[derive(Debug)] struct ConstraintCaseDebug<'a> { constraint: Constraint, diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index 712d2ef65d..13d4f25db6 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -98,8 +98,7 @@ pub(super) fn render_cell_layout( FailureLocation::InRegion { region, offset: _ } => { region .column_annotations - .map(|column_ann| column_ann.get(column).cloned()) - .flatten() + .and_then(|column_ann| column_ann.get(column).cloned()) .unwrap_or_else(|| column_type_and_idx(column)) } FailureLocation::OutsideRegion { row: _ } => { diff --git a/halo2_proofs/src/dev/graph.rs b/halo2_proofs/src/dev/graph.rs index b8c6fd90d7..5a43313dea 100644 --- a/halo2_proofs/src/dev/graph.rs +++ b/halo2_proofs/src/dev/graph.rs @@ -99,6 +99,14 @@ impl Assignment for Graph { Ok(()) } + fn annotate_column(&mut self, _annotation: A, _column: Column) + where + A: FnOnce() -> AR, + AR: Into, + { + // Do nothing + } + fn query_instance(&self, _: Column, _: usize) -> Result, Error> { Ok(Value::unknown()) } diff --git a/halo2_proofs/src/dev/graph/layout.rs b/halo2_proofs/src/dev/graph/layout.rs index 81f45a9010..0f2e67a81d 100644 --- a/halo2_proofs/src/dev/graph/layout.rs +++ b/halo2_proofs/src/dev/graph/layout.rs @@ -494,6 +494,14 @@ impl Assignment for Layout { Value::unknown() } + fn annotate_column(&mut self, _annotation: A, _column: Column) + where + A: FnOnce() -> AR, + AR: Into, + { + // Do nothing + } + fn push_namespace(&mut self, _: N) where NR: Into, diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index e56e482773..d0ab317e2e 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -54,8 +54,7 @@ impl From<(Column, Option<&HashMap>)> for DebugColumn { index: info.0.index, annotation: info .1 - .map(|map| map.get(&info.0)) - .flatten() + .and_then(|map| map.get(&info.0)) .cloned() .unwrap_or_default(), } diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 934feaad8d..0e2a91151c 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -1382,7 +1382,7 @@ pub struct ConstraintSystem { pub(crate) lookups: Vec>, // List of indexes of Fixed columns which are associated to a `TableColumn` tied to their annotation. - pub(crate) lookup_annotations: HashMap, + pub(crate) general_column_annotations: HashMap, // Vector of fixed columns, which can be used to store constant values // that are copied into advice columns. @@ -1467,7 +1467,7 @@ impl Default for ConstraintSystem { instance_queries: Vec::new(), permutation: permutation::Argument::new(), lookups: Vec::new(), - lookup_annotations: HashMap::new(), + general_column_annotations: HashMap::new(), constants: vec![], minimum_degree: None, } @@ -1859,7 +1859,7 @@ impl ConstraintSystem { AR: Into, { // We don't care if the table has already an annotation. If it's the case we keep the original one. - self.lookup_annotations.insert( + self.general_column_annotations.insert( metadata::Column::from((Any::Fixed, column.inner().index)), annotation().into(), ); diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index dcb3855687..502011af27 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -170,7 +170,7 @@ pub fn create_proof< Ok(()) } - fn annotate_column(&mut self, annotation: A, column: Column) + fn annotate_column(&mut self, _annotation: A, _column: Column) where A: FnOnce() -> AR, AR: Into, From d3e38bd3701f618dcea534ee52020a5149660234 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 10 Jan 2023 14:20:07 +0100 Subject: [PATCH 15/21] chore: Remove comments from code for testing --- halo2_proofs/src/dev.rs | 168 +++++++++++++++++++--------------------- 1 file changed, 81 insertions(+), 87 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index 2541ead9f7..aa7a6ea142 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -1436,23 +1436,21 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - //print!("{:?}", prover.verify()); - prover.assert_satisfied(); - // assert_eq!( - // prover.verify(), - // Err(vec![VerifyFailure::CellNotAssigned { - // gate: (0, "Equality check").into(), - // region: (0, "Faulty synthesis".to_owned()).into(), - // gate_offset: 1, - // column: Column::new( - // 1, - // Any::Advice(Advice { - // phase: FirstPhase.to_sealed() - // }) - // ), - // offset: 1, - // }]) - // ); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::CellNotAssigned { + gate: (0, "Equality check").into(), + region: (0, "Faulty synthesis".to_owned()).into(), + gate_offset: 1, + column: Column::new( + 1, + Any::Advice(Advice { + phase: FirstPhase.to_sealed() + }) + ), + offset: 1, + }]) + ); } #[test] @@ -1574,19 +1572,17 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - //print!("{:?}", prover.verify()); - prover.assert_satisfied(); - // assert_eq!( - // prover.verify(), - // Err(vec![VerifyFailure::Lookup { - // name: "lookup", - // lookup_index: 0, - // location: FailureLocation::InRegion { - // region: (2, "Faulty synthesis").into(), - // offset: 1, - // } - // }]) - // ); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::Lookup { + name: "lookup", + lookup_index: 0, + location: FailureLocation::InRegion { + region: (2, "Faulty synthesis").into(), + offset: 1, + } + }]) + ); } #[test] @@ -1713,62 +1709,60 @@ mod tests { } let prover = MockProver::run(K, &FaultyCircuit {}, vec![]).unwrap(); - //print!("{:?}", prover.verify()); - prover.assert_satisfied(); - // assert_eq!( - // prover.verify(), - // Err(vec![VerifyFailure::ConstraintNotSatisfied { - // constraint: ((0, "Equality check").into(), 0, "").into(), - // location: FailureLocation::InRegion { - // region: (1, "Wrong synthesis").into(), - // offset: 0, - // }, - // cell_values: vec![ - // ( - // ( - // ( - // Any::Advice(Advice { - // phase: FirstPhase.to_sealed() - // }), - // 0 - // ) - // .into(), - // 0 - // ) - // .into(), - // "1".to_string() - // ), - // ( - // ( - // ( - // Any::Advice(Advice { - // phase: FirstPhase.to_sealed() - // }), - // 1 - // ) - // .into(), - // 0 - // ) - // .into(), - // "0".to_string() - // ), - // ( - // ( - // ( - // Any::Advice(Advice { - // phase: FirstPhase.to_sealed() - // }), - // 2 - // ) - // .into(), - // 0 - // ) - // .into(), - // "0x5".to_string() - // ), - // (((Any::Fixed, 0).into(), 0).into(), "0x7".to_string()), - // ], - // },]) - // ) + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::ConstraintNotSatisfied { + constraint: ((0, "Equality check").into(), 0, "").into(), + location: FailureLocation::InRegion { + region: (1, "Wrong synthesis").into(), + offset: 0, + }, + cell_values: vec![ + ( + ( + ( + Any::Advice(Advice { + phase: FirstPhase.to_sealed() + }), + 0 + ) + .into(), + 0 + ) + .into(), + "1".to_string() + ), + ( + ( + ( + Any::Advice(Advice { + phase: FirstPhase.to_sealed() + }), + 1 + ) + .into(), + 0 + ) + .into(), + "0".to_string() + ), + ( + ( + ( + Any::Advice(Advice { + phase: FirstPhase.to_sealed() + }), + 2 + ) + .into(), + 0 + ) + .into(), + "0x5".to_string() + ), + (((Any::Fixed, 0).into(), 0).into(), "0x7".to_string()), + ], + },]) + ) } } From ea4662cc8cf42eeb260373de17367b8c0df7bda8 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Wed, 11 Jan 2023 11:34:26 +0100 Subject: [PATCH 16/21] feat: Add support for Advice and Instance anns in lookups --- halo2_proofs/src/dev.rs | 174 +++++++++++++++++++++++++++++- halo2_proofs/src/dev/failure.rs | 49 ++++++--- halo2_proofs/src/plonk/circuit.rs | 15 +++ 3 files changed, 222 insertions(+), 16 deletions(-) diff --git a/halo2_proofs/src/dev.rs b/halo2_proofs/src/dev.rs index aa7a6ea142..ed245cdeaa 100644 --- a/halo2_proofs/src/dev.rs +++ b/halo2_proofs/src/dev.rs @@ -1363,7 +1363,7 @@ mod tests { circuit::{Layouter, SimpleFloorPlanner, Value}, plonk::{ sealed::SealedPhase, Advice, Any, Circuit, Column, ConstraintSystem, Error, Expression, - FirstPhase, Fixed, Selector, TableColumn, + FirstPhase, Fixed, Instance, Selector, TableColumn, }, poly::Rotation, }; @@ -1454,7 +1454,177 @@ mod tests { } #[test] - fn bad_lookup() { + fn bad_lookup_any() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + a: Column, + table: Column, + advice_table: Column, + q: Selector, + } + + 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.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. + // 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)); + vec![ + ( + q.clone() * a.clone() + not_q.clone() * default.clone(), + table, + ), + (q * a + not_q * default, advice_table), + ] + }); + + FaultyCircuitConfig { + a, + q, + table, + advice_table, + } + } + + fn without_witnesses(&self) -> Self { + Self {} + } + + fn synthesize( + &self, + 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", + |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( + || "Advice from instance tables", + config.table, + i, + 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)), + )?; + + 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)?; + + 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", + config.a, + 0, + || Value::known(Fp::from(4)), + )?; + + // BUG: Assign a = 5, which doesn't exist in the table! + region.assign_advice( + || "a = 5", + config.a, + 1, + || Value::known(Fp::from(5)), + )?; + + region.name_column(|| "Witness example", config.a); + + Ok(()) + }, + ) + } + } + + let prover = MockProver::run( + K, + &FaultyCircuit {}, + // This is our "lookup table". + vec![vec![ + Fp::from(1u64), + Fp::from(2u64), + Fp::from(4u64), + Fp::from(6u64), + ]], + ) + .unwrap(); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::Lookup { + name: "lookup", + lookup_index: 0, + location: FailureLocation::InRegion { + region: (1, "Faulty synthesis").into(), + offset: 1, + } + }]) + ); + } + + #[test] + fn bad_fixed_lookup() { const K: u32 = 4; #[derive(Clone)] diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 806f77aac8..8e41aaa213 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -459,9 +459,39 @@ fn render_lookup( expr.evaluate( &|_| panic!("no constants in table expressions"), &|_| panic!("no selectors in table expressions"), - &|query| format!("F{}", query.column_index), - &|query| format! {"A{}", query.column_index}, - &|query| format! {"I{}", query.column_index}, + &|query| { + format!( + "{:?}", + prover + .cs + .general_column_annotations + .get(&metadata::Column::from((Any::Fixed, query.column_index))) + .cloned() + .unwrap_or_else(|| format!("F{}", query.column_index())) + ) + }, + &|query| { + format!( + "{:?}", + prover + .cs + .general_column_annotations + .get(&metadata::Column::from((Any::advice(), query.column_index))) + .cloned() + .unwrap_or_else(|| format!("I{}", query.column_index())) + ) + }, + &|query| { + format!( + "{:?}", + prover + .cs + .general_column_annotations + .get(&metadata::Column::from((Any::Instance, query.column_index))) + .cloned() + .unwrap_or_else(|| format!("I{}", query.column_index())) + ) + }, &|challenge| format! {"C{}", challenge.index()}, &|query| format! {"-{}", query}, &|a, b| format! {"{} + {}", a,b}, @@ -499,17 +529,8 @@ fn render_lookup( } eprint!(") ∉ ("); - for (i, column) in table_columns.enumerate() { - eprint!( - "{}{}", - if i == 0 { "" } else { ", " }, - prover - .cs - .general_column_annotations - .get(&column) - .cloned() - .unwrap_or_else(|| format!("{}", column)) - ); + for (i, column) in lookup_columns.enumerate() { + eprint!("{}{}", if i == 0 { "" } else { ", " }, column); } eprintln!(")"); diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 0e2a91151c..52a9e47254 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -1865,6 +1865,21 @@ impl ConstraintSystem { ); } + /// Annotate an Instance column. + pub fn annotate_lookup_any_column(&mut self, column: T, annotation: A) + where + A: Fn() -> AR, + AR: Into, + T: Into>, + { + let col_any = column.into(); + // We don't care if the table has already an annotation. If it's the case we keep the original one. + self.general_column_annotations.insert( + metadata::Column::from((col_any.column_type, col_any.index)), + annotation().into(), + ); + } + /// Allocate a new fixed column pub fn fixed_column(&mut self) -> Column { let tmp = Column { From c65e2903ea6c5fdda7e7b2701266b53365f1c210 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 16 Jan 2023 19:38:21 +0100 Subject: [PATCH 17/21] feat: Allow `V1` layouter to annotate columns too --- halo2_proofs/src/circuit/floor_planner/v1.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/halo2_proofs/src/circuit/floor_planner/v1.rs b/halo2_proofs/src/circuit/floor_planner/v1.rs index 7f9253c047..eb139cb946 100644 --- a/halo2_proofs/src/circuit/floor_planner/v1.rs +++ b/halo2_proofs/src/circuit/floor_planner/v1.rs @@ -483,10 +483,10 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> RegionLayouter for V1Region<'r fn name_column<'v>( &'v mut self, - _annotation: &'v (dyn Fn() -> String + 'v), - _column: Column, + annotation: &'v (dyn Fn() -> String + 'v), + column: Column, ) { - // Do nothing + self.plan.cs.annotate_column(annotation, column) } fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result<(), Error> { From bf6332ae725556523497ef2b52f96907bd94b4ca Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 16 Jan 2023 19:41:48 +0100 Subject: [PATCH 18/21] fix: Support `Constant` & `Selector` for lookup exprs --- halo2_proofs/src/dev/failure.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 8e41aaa213..0b01a03439 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -457,8 +457,8 @@ fn render_lookup( // expressions for the table side of lookups. let lookup_columns = lookup.table_expressions.iter().map(|expr| { expr.evaluate( - &|_| panic!("no constants in table expressions"), - &|_| panic!("no selectors in table expressions"), + &|f| format! {"Const: {:#?}", f}, + &|s| format! {"S{}", s.0}, &|query| { format!( "{:?}", @@ -478,7 +478,7 @@ fn render_lookup( .general_column_annotations .get(&metadata::Column::from((Any::advice(), query.column_index))) .cloned() - .unwrap_or_else(|| format!("I{}", query.column_index())) + .unwrap_or_else(|| format!("A{}", query.column_index())) ) }, &|query| { From fabdcfe62c1bbcd7171c565e13d7196ce49c4195 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 16 Jan 2023 21:09:35 +0100 Subject: [PATCH 19/21] chore: Address review comments --- halo2_proofs/src/plonk/circuit.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 52a9e47254..964ec7bf24 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -526,7 +526,9 @@ pub trait Assignment { NR: Into, N: FnOnce() -> NR; - /// TODO: Document + /// Allows the developer to include an annotation for an specific column within a `Region`. + /// + /// This is usually useful for debugging circuit failures. fn annotate_column(&mut self, annotation: A, column: Column) where A: FnOnce() -> AR, @@ -1381,7 +1383,7 @@ pub struct ConstraintSystem { // input expressions and a sequence of table expressions involved in the lookup. pub(crate) lookups: Vec>, - // List of indexes of Fixed columns which are associated to a `TableColumn` tied to their annotation. + // List of indexes of Fixed columns which are associated to a circuit-general Column tied to their annotation. pub(crate) general_column_annotations: HashMap, // Vector of fixed columns, which can be used to store constant values @@ -1858,7 +1860,7 @@ impl ConstraintSystem { A: Fn() -> AR, AR: Into, { - // We don't care if the table has already an annotation. If it's the case we keep the original one. + // We don't care if the table has already an annotation. If it's the case we keep the new one. self.general_column_annotations.insert( metadata::Column::from((Any::Fixed, column.inner().index)), annotation().into(), @@ -1873,7 +1875,7 @@ impl ConstraintSystem { T: Into>, { let col_any = column.into(); - // We don't care if the table has already an annotation. If it's the case we keep the original one. + // We don't care if the table has already an annotation. If it's the case we keep the new one. self.general_column_annotations.insert( metadata::Column::from((col_any.column_type, col_any.index)), annotation().into(), From 24efdea63d4b052bf2bc71e24e399f31b8e883f8 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 16 Jan 2023 21:11:51 +0100 Subject: [PATCH 20/21] chore: Propagete write! result in `VerifyFailure::Display` --- halo2_proofs/src/dev/failure.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 0b01a03439..5a485b98ab 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -217,7 +217,7 @@ impl<'a> fmt::Display for VerifyFailure<'a> { (DebugVirtualCell::from((vc, ann_map)), string) }) { - let _ = writeln!(f, "- {} = {}", dvc, value); + let _ = writeln!(f, "- {} = {}", dvc, value)?; } Ok(()) } From 8917cd3ffea2b365dc8177deea85af4d95876743 Mon Sep 17 00:00:00 2001 From: CPerezz Date: Mon, 16 Jan 2023 21:17:44 +0100 Subject: [PATCH 21/21] chore: Address clippy lints --- halo2_proofs/src/dev/failure.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 5a485b98ab..217de4957d 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -217,7 +217,7 @@ impl<'a> fmt::Display for VerifyFailure<'a> { (DebugVirtualCell::from((vc, ann_map)), string) }) { - let _ = writeln!(f, "- {} = {}", dvc, value)?; + writeln!(f, "- {} = {}", dvc, value)?; } Ok(()) }