From a1c067e55512998015826d44cb9be25d1050a47b Mon Sep 17 00:00:00 2001 From: Jack Grigg Date: Tue, 18 May 2021 14:40:45 +0100 Subject: [PATCH] book: Add page describing developer tools --- book/src/SUMMARY.md | 1 + book/src/user/dev-tools.md | 80 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 81 insertions(+) create mode 100644 book/src/user/dev-tools.md diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index da89606f..ab6c2731 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -8,6 +8,7 @@ - [Chips](concepts/chips.md) - [Gadgets](concepts/gadgets.md) - [User Documentation](user.md) + - [Developer tools](user/dev-tools.md) - [A simple example](user/simple-example.md) - [Lookup tables](user/lookup-tables.md) - [Gadgets](user/gadgets.md) diff --git a/book/src/user/dev-tools.md b/book/src/user/dev-tools.md new file mode 100644 index 00000000..8f54a704 --- /dev/null +++ b/book/src/user/dev-tools.md @@ -0,0 +1,80 @@ +# Developer tools + +The `halo2` crate includes several utilities to help you design and implement your +circuits. + +## Mock prover + +`halo2::dev::MockProver` is a tool for debugging circuits, as well as cheaply verifying +their correctness in unit tests. The private and public inputs to the circuit are +constructed as would normally be done to create a proof, but `MockProver::run` instead +creates an object that will test every constraint in the circuit directly. It returns +granular error messages that indicate which specific constraint (if any) is not satisfied. + +## Circuit visualizations + +The `dev-graph` feature flag exposes several helper methods for creating graphical +representations of circuits. + +`halo2::dev::circuit_layout` renders the circuit layout as a grid: + +- Columns are layed out from left to right as advice, instance, and fixed. The order of + columns is otherwise without meaning. + - Advice columns have a red background. + - Instance columns have a white background. + - Fixed columns have a blue background. +- Regions are shown as labelled green boxes (overlaying the background colour). A region + may appear as multiple boxes if some of its columns happen to not be adjacent. +- Cells that have been assigned to by the circuit will be shaded in grey. If any cells are + assigned to more than once (which is usually a mistake), they will be shaded darker than + the surrounding cells. + +`halo2::dev::circuit_dot_graph` builds a [DOT graph string] representing the given +circuit, which can then be rendered witha variety of [layout programs]. The graph is built +from calls to `Layouter::namespace` both within the circuit, and inside the gadgets and +chips that it uses. + +[DOT graph string]: https://graphviz.org/doc/info/lang.html +[layout programs]: https://en.wikipedia.org/wiki/DOT_(graph_description_language)#Layout_programs + +## Cost estimator + +The `cost-model` binary takes high-level parameters for a circuit design, and estimates +the verification cost, as well as resulting proof size. + +``` +Usage: cargo run --example cost-model -- [OPTIONS] k + +Positional arguments: + k 2^K bound on the number of rows. + +Optional arguments: + -h, --help Print this message. + -a, --advice R[,R..] An advice column with the given rotations. May be repeated. + -i, --instance R[,R..] An instance column with the given rotations. May be repeated. + -f, --fixed R[,R..] A fixed column with the given rotations. May be repeated. + -g, --gate-degree D Maximum degree of the custom gates. + -l, --lookup N,I,T A lookup over N columns with max input degree I and max table degree T. May be repeated. + -p, --permutation N A permutation over N columns. May be repeated. +``` + +For example, to estimate the cost of a circuit with three advice columns and one fixed +column (with various rotations), and a maximum gate degree of 4: + +```shell +$ cargo run --example cost-model -- -a 0,1 -a 0 -a-0,-1,1 -f 0 -g 4 11 + Finished dev [unoptimized + debuginfo] target(s) in 0.03s + Running `target/debug/examples/cost-model -a 0,1 -a 0 -a 0,-1,1 -f 0 -g 4 11` +Circuit { + k: 11, + max_deg: 4, + advice_columns: 3, + lookups: 0, + permutations: [], + column_queries: 7, + point_sets: 3, + estimator: Estimator, +} +Proof size: 1440 bytes +Verification: at least 81.689ms +```