diff --git a/halo2_proofs/src/dev/failure.rs b/halo2_proofs/src/dev/failure.rs index 60f1ba0f..d382e88f 100644 --- a/halo2_proofs/src/dev/failure.rs +++ b/halo2_proofs/src/dev/failure.rs @@ -213,6 +213,70 @@ impl fmt::Display for VerifyFailure { } } +/// Renders `VerifyFailure::CellNotAssigned`. +/// +/// ```text +/// error: cell not assigned +/// Cell layout in region 'Faulty synthesis': +/// | Offset | A0 | A1 | +/// +--------+----+----+ +/// | 0 | x0 | | +/// | 1 | | X | <--{ X marks the spot! 🦜 +/// +/// Gate 'Equality check' (applied at offset 1) queries these cells. +/// ``` +fn render_cell_not_assigned( + gates: &[Gate], + gate: &metadata::Gate, + region: &metadata::Region, + gate_offset: usize, + column: Column, + offset: isize, +) { + // Collect the necessary rendering information: + // - The columns involved in this gate. + // - How many cells are in each column. + // - The grid of cell values, indexed by rotation. + let mut columns = BTreeMap::::default(); + let mut layout = BTreeMap::>::default(); + for (i, cell) in gates[gate.index].queried_cells().iter().enumerate() { + let cell_column = cell.column.into(); + *columns.entry(cell_column).or_default() += 1; + layout + .entry(cell.rotation.0) + .or_default() + .entry(cell_column) + .or_insert_with(|| { + if cell.column == column && gate_offset as i32 + cell.rotation.0 == offset as i32 { + "X".to_string() + } else { + format!("x{}", i) + } + }); + } + + eprintln!("error: cell not assigned"); + emitter::render_cell_layout( + " ", + &FailureLocation::InRegion { + region: region.clone(), + offset: gate_offset, + }, + &columns, + &layout, + |row_offset, rotation| { + if (row_offset.unwrap() + rotation) as isize == offset { + eprint!(" <--{{ X marks the spot! 🦜"); + } + }, + ); + eprintln!(); + eprintln!( + " Gate '{}' (applied at offset {}) queries these cells.", + gate.name, gate_offset + ); +} + /// Renders `VerifyFailure::ConstraintNotSatisfied`. /// /// ```text @@ -241,14 +305,14 @@ fn render_constraint_not_satisfied( // - How many cells are in each column. // - The grid of cell values, indexed by rotation. let mut columns = BTreeMap::::default(); - let mut layout = BTreeMap::>::default(); + let mut layout = BTreeMap::>::default(); for (i, (cell, _)) in cell_values.iter().enumerate() { *columns.entry(cell.column).or_default() += 1; layout .entry(cell.rotation) .or_default() .entry(cell.column) - .or_insert(i); + .or_insert(format!("x{}", i)); } eprintln!("error: constraint not satisfied"); @@ -393,14 +457,14 @@ fn render_lookup( // - How many cells are in each column. // - The grid of cell values, indexed by rotation. let mut columns = BTreeMap::::default(); - let mut layout = BTreeMap::>::default(); + let mut layout = BTreeMap::>::default(); for (i, (cell, _)) in cell_values.iter().enumerate() { *columns.entry(cell.column).or_default() += 1; layout .entry(cell.rotation) .or_default() .entry(cell.column) - .or_insert(i); + .or_insert(format!("x{}", i)); } if i != 0 { @@ -431,6 +495,20 @@ impl VerifyFailure { /// Emits this failure in pretty-printed format to stderr. pub(super) fn emit(&self, prover: &MockProver) { match self { + Self::CellNotAssigned { + gate, + region, + gate_offset, + column, + offset, + } => render_cell_not_assigned( + &prover.cs.gates, + gate, + region, + *gate_offset, + *column, + *offset, + ), Self::ConstraintNotSatisfied { constraint, location, diff --git a/halo2_proofs/src/dev/failure/emitter.rs b/halo2_proofs/src/dev/failure/emitter.rs index 461b89c7..4baaf372 100644 --- a/halo2_proofs/src/dev/failure/emitter.rs +++ b/halo2_proofs/src/dev/failure/emitter.rs @@ -28,7 +28,7 @@ pub(super) fn render_cell_layout( prefix: &str, location: &FailureLocation, columns: &BTreeMap, - layout: &BTreeMap>, + layout: &BTreeMap>, highlight_row: impl Fn(Option, i32), ) { let col_width = |cells: usize| cells.to_string().len() + 3; @@ -87,7 +87,7 @@ pub(super) fn render_cell_layout( padded( ' ', width, - &row.get(col).map(|i| format!("x{}", i)).unwrap_or_default() + row.get(col).map(|s| s.as_str()).unwrap_or_default() ) ); } @@ -98,17 +98,17 @@ pub(super) fn render_cell_layout( pub(super) fn expression_to_string( expr: &Expression, - layout: &BTreeMap>, + layout: &BTreeMap>, ) -> String { expr.evaluate( &util::format_value, &|_| panic!("virtual selectors are removed during optimization"), &|query, column, rotation| { - if let Some(i) = layout + if let Some(label) = layout .get(&rotation.0) .and_then(|row| row.get(&(Any::Fixed, column).into())) { - format!("x{}", i) + label.clone() } else if rotation.0 == 0 { // This is most likely a merged selector format!("S{}", query) @@ -118,24 +118,20 @@ pub(super) fn expression_to_string( } }, &|_, column, rotation| { - format!( - "x{}", - layout - .get(&rotation.0) - .unwrap() - .get(&(Any::Advice, column).into()) - .unwrap() - ) + layout + .get(&rotation.0) + .unwrap() + .get(&(Any::Advice, column).into()) + .unwrap() + .clone() }, &|_, column, rotation| { - format!( - "x{}", - layout - .get(&rotation.0) - .unwrap() - .get(&(Any::Instance, column).into()) - .unwrap() - ) + layout + .get(&rotation.0) + .unwrap() + .get(&(Any::Instance, column).into()) + .unwrap() + .clone() }, &|a| { if a.contains(' ') { diff --git a/halo2_proofs/src/dev/metadata.rs b/halo2_proofs/src/dev/metadata.rs index 756ce594..d7d2443e 100644 --- a/halo2_proofs/src/dev/metadata.rs +++ b/halo2_proofs/src/dev/metadata.rs @@ -143,7 +143,7 @@ impl From<(Gate, usize, &'static str)> for Constraint { } /// Metadata about an assigned region within a circuit. -#[derive(Debug, PartialEq)] +#[derive(Clone, Debug, PartialEq)] pub struct Region { /// The index of the region. These indices are assigned in the order in which /// `Layouter::assign_region` is called during `Circuit::synthesize`.