From b85089c45d90afaa5cda933fea0e3d717f33f5bc Mon Sep 17 00:00:00 2001 From: CPerezz Date: Tue, 13 Dec 2022 17:55:51 +0100 Subject: [PATCH] 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 ddb48bf770..cc9ab48c4c 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,