Skip to content

Commit

Permalink
fix: Update Debug & Display for VerifyFailure
Browse files Browse the repository at this point in the history
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 zcash#705
  • Loading branch information
CPerezz committed Dec 13, 2022
1 parent 69b8a8f commit b85089c
Show file tree
Hide file tree
Showing 2 changed files with 117 additions and 8 deletions.
58 changes: 52 additions & 6 deletions halo2_proofs/src/dev/failure.rs
Original file line number Diff line number Diff line change
@@ -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},
Expand All @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 } => {
Expand Down Expand Up @@ -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
Expand Down
67 changes: 65 additions & 2 deletions halo2_proofs/src/dev/metadata.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,42 @@ impl From<plonk::Column<Any>> 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<Column, String>>)> for DebugColumn {
fn from(info: (Column, Option<&HashMap<Column, String>>)) -> 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)]
Expand Down Expand Up @@ -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<Column, String>>)> for DebugVirtualCell {
fn from(info: (&VirtualCell, Option<&HashMap<Column, String>>)) -> 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`.
Expand All @@ -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,
Expand Down

0 comments on commit b85089c

Please sign in to comment.