译自 halo2 book:user/dev-tools.md
开发者工具
halo2 crate 包含若干实用工具,帮助你设计和实现电路(circuit)。
模拟证明器(Mock prover)
halo2_proofs::dev::MockProver 是一个用于调试电路的工具,也可以在单元测试中以很低的成本验证电路的正确性。电路的私有输入和公开输入按照通常生成证明(proof)的方式构造,但 MockProver::run 不会真的生成证明,而是创建一个对象来直接测试电路中的每一条约束(constraint)。它会返回细粒度的错误消息,指出具体是哪一条约束(如果有的话)未被满足。
电路可视化
dev-graph 特性标志(feature flag)暴露了若干辅助方法,用于创建电路的图形化表示。
在 Debian 系统上,你需要安装以下额外的软件包:
sudo apt install cmake libexpat1-dev libfreetype6-dev libcairo2-dev
电路布局(Circuit layout)
halo2_proofs::dev::CircuitLayout 将电路布局渲染为一张网格:
fn main() {
// Prepare the circuit you want to render.
// You don't need to include any witness variables.
let a = Fp::random(OsRng);
let instance = Fp::ONE + Fp::ONE;
let lookup_table = vec![instance, a, a, Fp::zero()];
let circuit: MyCircuit<Fp> = MyCircuit {
a: Value::unknown(),
lookup_table,
};
// Create the area you want to draw on.
// Use SVGBackend if you want to render to .svg instead.
use plotters::prelude::*;
let root = BitMapBackend::new("layout.png", (1024, 768)).into_drawing_area();
root.fill(&WHITE).unwrap();
let root = root
.titled("Example Circuit Layout", ("sans-serif", 60))
.unwrap();
halo2_proofs::dev::CircuitLayout::default()
// You can optionally render only a section of the circuit.
.view_width(0..2)
.view_height(0..16)
// You can hide labels, which can be useful with smaller areas.
.show_labels(false)
// Render the circuit onto your area!
// The first argument is the size parameter for the circuit.
.render(5, &circuit, &root)
.unwrap();
}
- 列(column)从左到右依次排布为 instance、advice 和 fixed。除此之外,列的顺序没有特定含义。
- Instance 列采用白色背景。
- Advice 列采用红色背景。
- Fixed 列采用蓝色背景。
- 区域(region)显示为带标签的绿色方框(叠加在背景色之上)。如果某个区域的部分列恰好不相邻,它可能会显示为多个方框。
- 被电路赋值过的单元格(cell)会被涂成灰色。如果某些单元格被赋值了不止一次(这通常是个错误),它们会被涂得比周围的单元格更深。
电路结构
halo2_proofs::dev::circuit_dot_graph 会构建一个表示给定电路的 DOT 图字符串,然后可以用各种布局程序来渲染它。该图是根据电路内部以及它所使用的小工具(gadget)和芯片(chip)内部对 Layouter::namespace 的调用构建的。
fn main() {
// Prepare the circuit you want to render.
// You don't need to include any witness variables.
let a = Fp::rand();
let instance = Fp::one() + Fp::one();
let lookup_table = vec![instance, a, a, Fp::zero()];
let circuit: MyCircuit<Fp> = MyCircuit {
a: None,
lookup_table,
};
// Generate the DOT graph string.
let dot_string = halo2_proofs::dev::circuit_dot_graph(&circuit);
// Now you can either handle it in Rust, or just
// print it out to use with command-line tools.
print!("{}", dot_string);
}
成本估算器(Cost estimator)
cost-model 二进制程序接收电路设计的高层参数,并估算验证成本以及最终的证明大小。
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.
例如,要估算一个具有三个 advice 列和一个 fixed 列(带各种旋转(rotation))、且自定义门(custom gate)最大次数(degree)为 4 的电路的成本:
> 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