Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for Column annotations for MockProver debugging #109

Merged
merged 21 commits into from
Jan 16, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
a86edfe
feat: Add `name_column` to `Layouter` & `RegionLayouter`
CPerezz Dec 12, 2022
fc2c76a
feta: Update metadata/dbg structs to hold Col->Ann mapping
CPerezz Dec 12, 2022
9215ee0
feat: Update emitter module to print Column annotations
CPerezz Dec 12, 2022
4aaf65d
feat: Add lookup column annotations
CPerezz Dec 12, 2022
d74c658
feat: Add Lookup TableColumn annotations
CPerezz Dec 13, 2022
0d720d3
fix: Customly derive PartialEq for metadata::Region
CPerezz Dec 13, 2022
2e79a26
fix: Update ConstraintNotSatisfied testcase
CPerezz Dec 13, 2022
c5d8401
fix: Update Debug & Display for VerifyFailure
CPerezz Dec 13, 2022
5c3a516
fix: Address clippy & warnings
CPerezz Dec 13, 2022
9807812
fix: Add final comments & polish
CPerezz Dec 13, 2022
1276faf
fix: Resolve cherry-pick merge conflics & errors
CPerezz Dec 13, 2022
5fc32fd
chore: Change DebugColumn visibility
CPerezz Jan 10, 2023
864aa3e
chore: Allow to fetch annotations from metadata
CPerezz Jan 10, 2023
6485966
chore: Fix clippy lints
CPerezz Jan 10, 2023
d3e38bd
chore: Remove comments from code for testing
CPerezz Jan 10, 2023
ea4662c
feat: Add support for Advice and Instance anns in lookups
CPerezz Jan 11, 2023
c65e290
feat: Allow `V1` layouter to annotate columns too
CPerezz Jan 16, 2023
bf6332a
fix: Support `Constant` & `Selector` for lookup exprs
CPerezz Jan 16, 2023
fabdcfe
chore: Address review comments
CPerezz Jan 16, 2023
24efdea
chore: Propagete write! result in `VerifyFailure::Display`
CPerezz Jan 16, 2023
8917cd3
chore: Address clippy lints
CPerezz Jan 16, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions halo2_proofs/src/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
8 changes: 8 additions & 0 deletions halo2_proofs/src/circuit/floor_planner/single_pass.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
8 changes: 8 additions & 0 deletions halo2_proofs/src/circuit/floor_planner/v1.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
18 changes: 18 additions & 0 deletions halo2_proofs/src/circuit/layouter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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(())
Expand Down
Loading