Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

译自 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