zec
/
halo2
mirror of https://github.com/zcash/halo2.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Add support for Column annotations for MockProver debugging (#109) 

* 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`.

* feta: Update metadata/dbg structs to hold Col->Ann mapping

* feat: Update emitter module to print Column annotations

* 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.

* 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.

* 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.

* fix: Update ConstraintNotSatisfied testcase

* 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

* fix: Address clippy & warnings

* fix: Add final comments & polish

* fix: Resolve cherry-pick merge conflics & errors

* chore: Change DebugColumn visibility

* chore: Allow to fetch annotations from metadata

* chore: Fix clippy lints

* chore: Remove comments from code for testing

* feat: Add support for Advice and Instance anns in lookups

* feat: Allow `V1` layouter to annotate columns too

* fix: Support `Constant` & `Selector` for lookup exprs

* chore: Address review comments

* chore: Propagete write! result in `VerifyFailure::Display`

* chore: Address clippy lints
This commit is contained in:
Carlos Pérez 2023-01-17 00:39:10 +01:00 committed by GitHub
parent 4ad07d424e
commit 54e4c57d05
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
14 changed files with 842 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
halo2_proofs/src/circuit.rs
View File

@ -206,6 +206,20 @@ impl<'r, F: Field> Region<'r, F> {
.enable_selector(&|| annotation().into(), selector, offset)
}
/// 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<A, AR, T>(&mut self, annotation: A, column: T)
where
A: Fn() -> AR,
AR: Into<String>,
T: Into<Column<Any>>,
{
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.

8
halo2_proofs/src/circuit/floor_planner/single_pass.rs
View File

@ -279,6 +279,14 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
)
}
fn name_column<'v>(
&'v mut self,
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Any>,
) {
self.layouter.cs.annotate_column(annotation, column);
}
fn assign_advice<'v>(
&'v mut self,
annotation: &'v (dyn Fn() -> String + 'v),

8
halo2_proofs/src/circuit/floor_planner/v1.rs
View File

@ -481,6 +481,14 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r
Ok(())
}
fn name_column<'v>(
&'v mut self,
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Any>,
) {
self.plan.cs.annotate_column(annotation, column)
}
fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result<(), Error> {
self.plan.cs.copy(
left.column,

18
halo2_proofs/src/circuit/layouter.rs
View File

@ -48,6 +48,16 @@ pub trait RegionLayouter<F: Field>: fmt::Debug {
offset: usize,
) -> Result<(), Error>;
/// 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),
column: Column<Any>,
);
/// Assign an advice column value (witness)
fn assign_advice<'v>(
&'v mut self,
@ -275,6 +285,14 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
})
}
fn name_column<'v>(
&'v mut self,
_annotation: &'v (dyn Fn() -> String + 'v),
_column: Column<Any>,
) {
// Do nothing
}
fn constrain_constant(&mut self, _cell: Cell, _constant: Assigned<F>) -> Result<(), Error> {
// Global constants don't affect the region shape.
Ok(())

398
halo2_proofs/src/dev.rs
View File

@ -29,6 +29,7 @@ use rayon::{
};
pub mod metadata;
use metadata::Column as ColumnMetadata;
mod util;
mod failure;
@ -58,7 +59,9 @@ struct Region {
/// The selectors that have been enabled in this region. All other selectors are by
/// construction not enabled.
enabled_selectors: HashMap<Selector, Vec<usize>>,
/// The cells assigned in this region. We store this as a `HashMap` with count so that if any cells
/// Annotations given to Advice, Fixed or Instance columns within a region context.
annotations: HashMap<ColumnMetadata, String>,
/// 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<Any>, usize), usize>,
}
@ -317,6 +320,7 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
name: name().into(),
columns: HashSet::default(),
rows: None,
annotations: HashMap::default(),
enabled_selectors: HashMap::default(),
cells: HashMap::default(),
});
@ -326,6 +330,18 @@ impl<F: Field + Group> Assignment<F> for MockProver<F> {
self.regions.push(self.current_region.take().unwrap());
}
fn annotate_column<A, AR>(&mut self, annotation: A, column: Column<Any>)
where
A: FnOnce() -> AR,
AR: Into<String>,
{
if let Some(region) = self.current_region.as_mut() {
region
.annotations
.insert(ColumnMetadata::from(column), annotation().into());
}
}
fn enable_selector<A, AR>(&mut self, _: A, selector: &Selector, row: usize) -> Result<(), Error>
where
A: FnOnce() -> AR,
@ -638,12 +654,12 @@ impl<F: FieldExt> MockProver<F> {
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)) {
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()).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,
@ -1357,8 +1373,8 @@ mod tests {
use crate::{
circuit::{Layouter, SimpleFloorPlanner, Value},
plonk::{
Advice, Any, Circuit, Column, ConstraintSystem, Error, Expression, Selector,
TableColumn,
sealed::SealedPhase, Advice, Any, Circuit, Column, ConstraintSystem, Error, Expression,
FirstPhase, Fixed, Instance, Selector, TableColumn,
},
poly::Rotation,
};
@ -1370,6 +1386,7 @@ mod tests {
#[derive(Clone)]
struct FaultyCircuitConfig {
a: Column<Advice>,
b: Column<Advice>,
q: Selector,
}
@ -1393,7 +1410,7 @@ mod tests {
vec![q * (a - b)]
});
FaultyCircuitConfig { a, q }
FaultyCircuitConfig { a, b, q }
}
fn without_witnesses(&self) -> Self {
@ -1414,6 +1431,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.
@ -1430,14 +1453,189 @@ mod tests {
gate: (0, "Equality check").into(),
region: (0, "Faulty synthesis".to_owned()).into(),
gate_offset: 1,
column: Column::new(1, Any::advice()),
column: Column::new(
1,
Any::Advice(Advice {
phase: FirstPhase.to_sealed()
})
),
offset: 1,
}])
);
}
#[test]
fn bad_lookup() {
fn bad_lookup_any() {
const K: u32 = 4;
#[derive(Clone)]
struct FaultyCircuitConfig {
a: Column<Advice>,
table: Column<Instance>,
advice_table: Column<Advice>,
q: Selector,
}
struct FaultyCircuit {}
impl Circuit<Fp> for FaultyCircuit {
type Config = FaultyCircuitConfig;
type FloorPlanner = SimpleFloorPlanner;
fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
) -> 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)]
@ -1457,6 +1655,7 @@ mod tests {
let a = meta.advice_column();
let q = meta.complex_selector();
let table = meta.lookup_table_column();
meta.annotate_lookup_column(table, || "Table1");
meta.lookup("lookup", |cells| {
let a = cells.query_advice(a, Rotation::cur());
@ -1545,6 +1744,8 @@ mod tests {
|| Value::known(Fp::from(5)),
)?;
region.name_column(|| "Witness example", config.a);
Ok(())
},
)
@ -1564,4 +1765,185 @@ mod tests {
}])
);
}
#[test]
fn contraint_unsatisfied() {
const K: u32 = 4;
#[derive(Clone)]
struct FaultyCircuitConfig {
a: Column<Advice>,
b: Column<Advice>,
c: Column<Advice>,
d: Column<Fixed>,
q: Selector,
}
struct FaultyCircuit {}
impl Circuit<Fp> for FaultyCircuit {
type Config = FaultyCircuitConfig;
type FloorPlanner = SimpleFloorPlanner;
fn configure(meta: &mut ConstraintSystem<Fp>) -> 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<Fp>,
) -> 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();
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()),
],
},])
)
}
}

8
halo2_proofs/src/dev/cost.rs
View File

@ -122,6 +122,14 @@ impl<F: Field> Assignment<F> for Assembly {
Value::unknown()
}
fn annotate_column<A, AR>(&mut self, _annotation: A, _column: Column<Any>)
where
A: FnOnce() -> AR,
AR: Into<String>,
{
// Do nothing
}
fn push_namespace<NR, N>(&mut self, _: N)
where
NR: Into<String>,

163
halo2_proofs/src/dev/failure.rs
View File

@ -1,17 +1,19 @@
use std::collections::{BTreeMap, BTreeSet, HashSet};
use std::fmt;
use std::iter;
use std::collections::{BTreeMap, HashSet};
use std::fmt::{self, Debug};
use group::ff::Field;
use halo2curves::FieldExt;
use super::metadata::{DebugColumn, DebugVirtualCell};
use super::MockProver;
use super::{
metadata,
util::{self, AnyQuery},
MockProver, Region,
Region,
};
use crate::dev::metadata::Constraint;
use crate::{
dev::Value,
dev::{Instance, Value},
plonk::{Any, Column, ConstraintSystem, Expression, Gate},
poly::Rotation,
};
@ -19,12 +21,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, Clone)]
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 +38,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 +49,20 @@ impl fmt::Display for FailureLocation {
}
}
impl FailureLocation {
pub(super) fn find_expressions<'a, F: Field>(
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)),
}
}
pub(super) fn find_expressions<F: Field>(
cs: &ConstraintSystem<F>,
regions: &[Region],
regions: &'a [Region],
failure_row: usize,
failure_expressions: impl Iterator<Item = &'a Expression<F>>,
) -> Self {
@ -82,7 +94,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<Column<Any>>,
) -> Self {
@ -102,24 +114,22 @@ 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,
})
.unwrap_or_else(|| FailureLocation::OutsideRegion { row: failure_row })
}
}
/// The reasons why a particular circuit is not satisfied.
#[derive(Debug, PartialEq)]
pub enum VerifyFailure {
#[derive(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,
@ -138,7 +148,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)>,
},
@ -167,18 +177,18 @@ 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>,
},
/// 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 {
@ -190,8 +200,8 @@ impl fmt::Display for VerifyFailure {
} => {
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 {
@ -200,8 +210,17 @@ impl fmt::Display for VerifyFailure {
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(())
}
@ -226,14 +245,52 @@ impl fmt::Display for VerifyFailure {
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
)
}
}
}
}
impl<'a> Debug for VerifyFailure<'a> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
VerifyFailure::ConstraintNotSatisfied {
constraint,
location,
cell_values,
} => {
#[allow(dead_code)]
#[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,
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
@ -403,11 +460,41 @@ fn render_lookup<F: FieldExt>(
// 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"),
&|query| format!("F{}", query.column_index),
&|query| format! {"A{}", query.column_index},
&|query| format! {"I{}", query.column_index},
&|f| format! {"Const: {:#?}", f},
&|s| format! {"S{}", s.0},
&|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!("A{}", 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},
@ -443,6 +530,7 @@ fn render_lookup<F: FieldExt>(
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);
@ -501,6 +589,7 @@ fn render_lookup<F: FieldExt>(
emitter::expression_to_string(input, &layout)
);
eprintln!(" ^");
emitter::render_cell_layout(" | ", location, &columns, &layout, |_, rotation| {
if rotation == 0 {
eprint!(" <--{{ Lookup '{}' inputs queried here", name);
@ -516,7 +605,7 @@ fn render_lookup<F: FieldExt>(
}
}
impl VerifyFailure {
impl<'a> VerifyFailure<'a> {
/// Emits this failure in pretty-printed format to stderr.
pub(super) fn emit<F: FieldExt>(&self, prover: &MockProver<F>) {
match self {

81
halo2_proofs/src/dev/failure/emitter.rs
View File

@ -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::<String>(),
@ -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,75 @@ pub(super) fn render_cell_layout(
highlight_row: impl Fn(Option<i32>, 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<usize> = 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, _), &width) in columns.iter().zip(widths.iter()) {
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: _ } => {
region
.column_annotations
.and_then(|column_ann| column_ann.get(column).cloned())
.unwrap_or_else(|| column_type_and_idx(column))
}
FailureLocation::OutsideRegion { row: _ } => {
column_type_and_idx(column)
}
}
.to_string()
)
);
}
eprintln!();
eprint!("{} +--------+", prefix);
for cells in columns.values() {
eprint!("{}+", padded('-', col_width(*cells), ""));
for &width in widths.iter() {
eprint!("{}+", padded('-', width, ""));
}
eprintln!();
for (rotation, row) in layout {
@ -80,8 +122,7 @@ 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, _), &width) in columns.iter().zip(widths.iter()) {
eprint!(
"{}|",
padded(

8
halo2_proofs/src/dev/graph.rs
View File

@ -99,6 +99,14 @@ impl<F: Field> Assignment<F> for Graph {
Ok(())
}
fn annotate_column<A, AR>(&mut self, _annotation: A, _column: Column<Any>)
where
A: FnOnce() -> AR,
AR: Into<String>,
{
// Do nothing
}
fn query_instance(&self, _: Column<Instance>, _: usize) -> Result<Value<F>, Error> {
Ok(Value::unknown())
}

8
halo2_proofs/src/dev/graph/layout.rs
View File

@ -494,6 +494,14 @@ impl<F: Field> Assignment<F> for Layout {
Value::unknown()
}
fn annotate_column<A, AR>(&mut self, _annotation: A, _column: Column<Any>)
where
A: FnOnce() -> AR,
AR: Into<String>,
{
// Do nothing
}
fn push_namespace<NR, N>(&mut self, _: N)
where
NR: Into<String>,

147
halo2_proofs/src/dev/metadata.rs
View File

@ -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,
@ -33,6 +36,41 @@ 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)]
pub(super) 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
.and_then(|map| map.get(&info.0))
.cloned()
.unwrap_or_default(),
}
}
}
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)]
@ -82,8 +120,36 @@ 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,
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`.
@ -106,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,
@ -143,33 +209,90 @@ 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)]
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 annotations of the Columns that exist within this `Region`.
pub(super) column_annotations: Option<&'a HashMap<ColumnMetadata, String>>,
}
impl fmt::Display for Region {
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<String> {
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
}
}
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)
}
}
impl From<(usize, String)> for Region {
fn from((index, name): (usize, String)) -> Self {
Region { index, name }
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, &str)> for Region {
impl<'a> From<(usize, String)> for Region<'a> {
fn from((index, name): (usize, String)) -> Self {
Region {
index,
name,
column_annotations: None,
}
}
}
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<ColumnMetadata, String>)> for Region<'a> {
fn from(
(index, name, annotations): (usize, String, &'a HashMap<ColumnMetadata, String>),
) -> Self {
Region {
index,
name,
column_annotations: Some(annotations),
}
}
}
impl<'a> From<(usize, &str, &'a HashMap<ColumnMetadata, String>)> for Region<'a> {
fn from(
(index, name, annotations): (usize, &str, &'a HashMap<ColumnMetadata, String>),
) -> Self {
Region {
index,
name: name.to_owned(),
column_annotations: Some(annotations),
}
}
}

42
halo2_proofs/src/plonk/circuit.rs
View File

@ -1,12 +1,14 @@
use core::cmp::max;
use core::ops::{Add, Mul};
use ff::Field;
use std::collections::HashMap;
use std::{
convert::TryFrom,
ops::{Neg, Sub},
};
use super::{lookup, permutation, Assigned, Error};
use crate::dev::metadata;
use crate::{
circuit::{Layouter, Region, Value},
poly::Rotation,
@ -524,6 +526,14 @@ pub trait Assignment<F: Field> {
NR: Into<String>,
N: FnOnce() -> NR;
/// 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<A, AR>(&mut self, annotation: A, column: Column<Any>)
where
A: FnOnce() -> AR,
AR: Into<String>;
/// Exits the current region.
///
/// Panics if we are not currently in a region (if `enter_region` was not called).
@ -1373,6 +1383,9 @@ pub struct ConstraintSystem<F: Field> {
// input expressions and a sequence of table expressions involved in the lookup.
pub(crate) lookups: Vec<lookup::Argument<F>>,
// List of indexes of Fixed columns which are associated to a circuit-general Column tied to their annotation.
pub(crate) general_column_annotations: HashMap<metadata::Column, String>,
// Vector of fixed columns, which can be used to store constant values
// that are copied into advice columns.
pub(crate) constants: Vec<Column<Fixed>>,
@ -1456,6 +1469,7 @@ impl<F: Field> Default for ConstraintSystem<F> {
instance_queries: Vec::new(),
permutation: permutation::Argument::new(),
lookups: Vec::new(),
general_column_annotations: HashMap::new(),
constants: vec![],
minimum_degree: None,
}
@ -1840,6 +1854,34 @@ impl<F: Field> ConstraintSystem<F> {
}
}
/// Annotate a Lookup column.
pub fn annotate_lookup_column<A, AR>(&mut self, column: TableColumn, annotation: A)
where
A: Fn() -> AR,
AR: Into<String>,
{
// 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(),
);
}
/// Annotate an Instance column.
pub fn annotate_lookup_any_column<A, AR, T>(&mut self, column: T, annotation: A)
where
A: Fn() -> AR,
AR: Into<String>,
T: Into<Column<Any>>,
{
let col_any = column.into();
// 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(),
);
}
/// Allocate a new fixed column
pub fn fixed_column(&mut self) -> Column<Fixed> {
let tmp = Column {

8
halo2_proofs/src/plonk/keygen.rs
View File

@ -178,6 +178,14 @@ impl<F: Field> Assignment<F> for Assembly<F> {
Value::unknown()
}
fn annotate_column<A, AR>(&mut self, _annotation: A, _column: Column<Any>)
where
A: FnOnce() -> AR,
AR: Into<String>,
{
// Do nothing
}
fn push_namespace<NR, N>(&mut self, _: N)
where
NR: Into<String>,

8
halo2_proofs/src/plonk/prover.rs
View File

@ -170,6 +170,14 @@ pub fn create_proof<
Ok(())
}
fn annotate_column<A, AR>(&mut self, _annotation: A, _column: Column<Any>)
where
A: FnOnce() -> AR,
AR: Into<String>,
{
// Do nothing
}
fn query_instance(&self, column: Column<Instance>, row: usize) -> Result<Value<F>, Error> {
if !self.usable_rows.contains(&row) {
return Err(Error::not_enough_rows_available(self.k));