book: Add page describing developer tools

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)

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
+```