feat: Implement Column annotations for MockProver debugging

halo2_proofs/CHANGELOG.md

@@ -19,6 +19,11 @@ and this project adheres to Rust's notion of
 - `halo2_proofs::circuit::layouter`:
   - `RegionLayouter::instance_value` method added to provide access to
     instance values within a region.
+  - `RegionLayouter::annotate_column` method added to provide annotation capabilities
+    to the circuit Columns.
+- `halo2_proofs::plonk::circuit`:
+  - `ConstraintSystem::annotate_lookup_column` method added to allow for 
+    `TableColumn` annotation capabilities.
 
 ### Changed
 - Migrated to `ff 0.13`, `group 0.13`, `pasta_curves 0.5`.

halo2_proofs/src/circuit.rs

@@ -201,6 +201,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 annotate_column<A, AR, T>(&mut self, annotation: A, column: T)
+    where
+        A: Fn() -> AR,
+        AR: Into<String>,
+        T: Into<Column<Any>>,
+    {
+        self.region
+            .annotate_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.

halo2_proofs/src/circuit/floor_planner/single_pass.rs

@@ -275,6 +275,14 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>
         )
     }
 
+    fn annotate_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),

halo2_proofs/src/circuit/floor_planner/v1.rs

@@ -482,6 +482,14 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F> for V1Region<'r
         Ok(())
     }
 
+    fn annotate_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,

halo2_proofs/src/circuit/layouter.rs

@@ -48,6 +48,15 @@ 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 [`crate::dev::MockProver::assert_satisfied()`] can provide.
+    fn annotate_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,
@@ -288,6 +297,14 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
         })
     }
 
+    fn annotate_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(())

halo2_proofs/src/dev.rs

@@ -17,6 +17,7 @@ use crate::{
 };
 
 pub mod metadata;
+use metadata::Column as ColumnMetadata;
 mod util;
 
 mod failure;
@@ -46,6 +47,8 @@ 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>>,
+    /// 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: Vec<(Column<Any>, usize)>,
@@ -318,6 +321,7 @@ impl<F: Field> Assignment<F> for MockProver<F> {
             name: name().into(),
             columns: HashSet::default(),
             rows: None,
+            annotations: HashMap::default(),
             enabled_selectors: HashMap::default(),
             cells: vec![],
         });
@@ -327,6 +331,18 @@ impl<F: Field> 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,
@@ -565,6 +581,10 @@ impl<F: Field + Ord> MockProver<F> {
 
     /// Returns `Ok(())` if this `MockProver` is satisfied, or a list of errors indicating
     /// the reasons that the circuit is not satisfied.
+    ///
+    /// ### Note
+    /// This method will not print any annotations (in case they've been placed). If annotation printing is desired
+    /// please use [`MockProver::assert_satisfied`].
     pub fn verify(&self) -> Result<(), Vec<VerifyFailure>> {
         let n = self.n as i32;
 
@@ -603,7 +623,12 @@ impl<F: Field + Ord> MockProver<F> {
                                             InstanceValue::Assigned(_) => None,
                                             _ => Some(VerifyFailure::InstanceCellNotAssigned {
                                                 gate: (gate_index, gate.name()).into(),
-                                                region: (r_i, r.name.clone()).into(),
+                                                region: (
+                                                    r_i,
+                                                    r.name.clone(),
+                                                    r.annotations.clone(),
+                                                )
+                                                    .into(),
                                                 gate_offset: *selector_row,
                                                 column: cell.column.try_into().unwrap(),
                                                 row: cell_row,
@@ -617,7 +642,12 @@ impl<F: Field + Ord> MockProver<F> {
                                         } 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.clone(),
+                                                )
+                                                    .into(),
                                                 gate_offset: *selector_row,
                                                 column: cell.column,
                                                 offset: cell_row as isize
@@ -898,7 +928,7 @@ impl<F: Field + Ord> MockProver<F> {
     /// Panics if the circuit being checked by this `MockProver` is not satisfied.
     ///
     /// Any verification failures will be pretty-printed to stderr before the function
-    /// panics.
+    /// panics. These will also include annotations (in case they've been placed).
     ///
     /// Apart from the stderr output, this method is equivalent to:
     /// ```ignore
@@ -924,7 +954,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,
@@ -937,6 +967,7 @@ mod tests {
         #[derive(Clone)]
         struct FaultyCircuitConfig {
             a: Column<Advice>,
+            b: Column<Advice>,
             q: Selector,
         }
 
@@ -960,7 +991,7 @@ mod tests {
                     vec![q * (a - b)]
                 });
 
-                FaultyCircuitConfig { a, q }
+                FaultyCircuitConfig { a, b, q }
             }
 
             fn without_witnesses(&self) -> Self {
@@ -981,6 +1012,12 @@ mod tests {
                         // Assign a = 0.
                         region.assign_advice(|| "a", config.a, 0, || Value::known(Fp::ZERO))?;
 
+                        // Name Column a
+                        region.annotate_column(|| "This is annotated!", config.a);
+
+                        // Name Column b
+                        region.annotate_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.
@@ -1024,6 +1061,7 @@ mod tests {
                 let a = meta.advice_column();
                 let q = meta.complex_selector();
                 let table = meta.lookup_table_column();
+                meta.annotate_lookup_column(|| "Table1", table);
 
                 meta.lookup(|cells| {
                     let a = cells.query_advice(a, Rotation::cur());
@@ -1112,6 +1150,8 @@ mod tests {
                             || Value::known(Fp::from(5)),
                         )?;
 
+                        region.annotate_column(|| "Witness example", config.a);
+
                         Ok(())
                     },
                 )
@@ -1130,4 +1170,146 @@ 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);
+                    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.annotate_column(|| "This is Advice!", config.a);
+                        // Name Column b
+                        region.annotate_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.annotate_column(|| "Another one!", config.c);
+                        // Name Column d
+                        region.annotate_column(|| "This is a Fixed!", config.d);
+
+                        // Note that none of the terms cancel each other. Therefore we will have a constraint that is not satisfied for
+                        // the `Equality 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, 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()),
+                ],
+            },])
+        )
+    }
 }