Skip to main content

Dev Tooling: MockProver and friends

1. Why this chapter exists​

Writing a halo2 circuit without MockProver is theatre. Every gadget chapter in this course assumes you can run MockProver against your code and see a VerifyFailure that names the row and constraint at fault. This chapter is the catalogue of the dev module: what it does, what it does not do (it is not a substitute for verify_proof), and which dev tool to reach for in each debugging situation.

2. Definitions​

Definition (Mock proof). A row-by-row evaluation of every gate constraint, lookup, and permutation, performed without any commitment or Fiat-Shamir. A passing mock proof means the witness is consistent with the constraints; it does not prove that create_proof will produce a valid proof, because it does not exercise the polynomial commitment scheme. Conversely, a passing verify_proof does not imply that MockProver would also pass, because MockProver is stricter about row-level identities (a polynomial that vanishes on HH but is not identically zero passes verify_proof and fails MockProver).

Definition (Verify failure). A typed error reported by MockProver::verify that names exactly the gate / lookup / permutation constraint and the row that failed. The full set is in halo2_proofs/src/dev/failure.rs.

Definition (Circuit cost). A static estimate of the proof-time MSM cost, FFT cost, and proof size for a given circuit shape. Useful when comparing two ways of expressing the same constraint.

3. The code​

3.1 The dev module surface​

halo2_proofs/src/dev.rs
//! Tools for developing circuits.

use std::collections::HashMap;
use std::collections::HashSet;
use std::iter;
use std::ops::{Add, Mul, Neg, Range};

use ff::Field;

use crate::plonk::Assigned;
use crate::{
    circuit,
    plonk::{
        permutation, Advice, Any, Assignment, Circuit, Column, ConstraintSystem, Error, Expression,
        Fixed, FloorPlanner, Instance, Selector,
    },
};

pub mod metadata;
mod util;

mod failure;
pub use failure::{FailureLocation, VerifyFailure};

pub mod cost;
pub use cost::CircuitCost;

mod gates;
pub use gates::CircuitGates;

mod tfp;
pub use tfp::TracingFloorPlanner;

#[cfg(feature = "dev-graph")]
mod graph;

#[cfg(feature = "dev-graph")]
#[cfg_attr(docsrs, doc(cfg(feature = "dev-graph")))]
pub use graph::{circuit_dot_graph, layout::CircuitLayout};

#[derive(Debug)]
struct Region {

Public exports:

  • MockProver
  • VerifyFailure, FailureLocation
  • CircuitCost
  • CircuitGates
  • TracingFloorPlanner
  • CircuitLayout and circuit_dot_graph (gated by feature dev-graph).

3.2 MockProver​

halo2_proofs/src/dev.rs
/// ```
#[derive(Debug)]
pub struct MockProver<F: Field> {
    k: u32,
    n: u32,
    cs: ConstraintSystem<F>,

    /// The regions in the circuit.
    regions: Vec<Region>,
    /// The current region being assigned to. Will be `None` after the circuit has been
    /// synthesized.
    current_region: Option<Region>,

    // The fixed cells in the circuit, arranged as [column][row].
    fixed: Vec<Vec<CellValue<F>>>,
    // The advice cells in the circuit, arranged as [column][row].
    advice: Vec<Vec<CellValue<F>>>,
    // The instance cells in the circuit, arranged as [column][row].
    instance: Vec<Vec<InstanceValue<F>>>,

    selectors: Vec<Vec<bool>>,

    permutation: permutation::keygen::Assembly,

    // A range of available rows for assignment and copies.
    usable_rows: Range<usize>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
enum InstanceValue<F: Field> {
    Assigned(F),

Two entry points:

  • MockProver::run(k, &circuit, instances): synthesize and return the prover state.
  • MockProver::verify(): check every constraint and return Ok(()) or a vector of VerifyFailures.

The convenience method assert_satisfied panics on the first failure with a pretty-printed message. Use this in tests; use verify when you want to programmatically inspect failures.

A worked example, lifted from the doc comment of run:

let circuit = MyCircuit { ... };
MockProver::<Fp>::run(k, &circuit, vec![public_inputs])?
    .assert_satisfied();

3.3 CircuitCost​

halo2_proofs/src/dev/cost.rs
    poly::Rotation,
};

/// Measures a circuit to determine its costs, and explain what contributes to them.
#[allow(dead_code)]
#[derive(Debug)]
pub struct CircuitCost<G: PrimeGroup, ConcreteCircuit: Circuit<G::Scalar>> {
    /// Power-of-2 bound on the number of rows in the circuit.
    k: u32,
    /// Maximum degree of the circuit.
    max_deg: usize,
    /// Number of advice columns.
    advice_columns: usize,
    /// Number of direct queries for each column type.
    instance_queries: usize,
    advice_queries: usize,
    fixed_queries: usize,
    /// Number of lookup arguments.
    lookups: usize,
    /// Number of columns in the global permutation.
    permutation_cols: usize,
    /// Number of distinct sets of points in the multiopening argument.
    point_sets: usize,
    /// Maximum rows used over all columns
    max_rows: usize,
    /// Maximum rows used over all advice columns
    max_advice_rows: usize,
    /// Maximum rows used over all fixed columns
    max_fixed_rows: usize,
    num_fixed_columns: usize,
    num_advice_columns: usize,
    num_instance_columns: usize,
    num_total_columns: usize,

    _marker: PhantomData<(G, ConcreteCircuit)>,
}

/// Region implementation used by Layout
#[allow(dead_code)]
#[derive(Debug)]
pub(crate) struct LayoutRegion {
    /// The name of the region. Not required to be unique.
    pub(crate) name: String,
    /// The columns used by this region.
    pub(crate) columns: HashSet<RegionColumn>,
    /// The row that this region starts on, if known.
    pub(crate) offset: Option<usize>,
    /// The number of rows that this region takes up.
    pub(crate) rows: usize,
    /// The cells assigned in this region.
    pub(crate) cells: Vec<(RegionColumn, usize)>,
}

/// Cost and graphing layouter
#[derive(Default, Debug)]
pub(crate) struct Layout {
    /// k = 1 << n
    pub(crate) k: u32,
    /// Regions of the layout
    pub(crate) regions: Vec<LayoutRegion>,
    current_region: Option<usize>,

CircuitCost::measure(k, &circuit) returns a struct exposing the marginal cost per proof (advice columns, fixed columns, gates, lookup arguments, equality constraints, etc.). The marginal_proof_size method returns a byte count estimate.

3.4 CircuitGates​

halo2_proofs/src/dev/gates.rs
/// assert_eq!(
///     format!("{}", gates),
///     r#####"R1CS constraint:
/// - R1CS:
///   S0 * (A0@0 * A1@0 - A2@0)
/// Total gates: 1
/// Total custom constraint polynomials: 1
/// Total negations: 1
/// Total additions: 1
/// Total multiplications: 2
/// "#####,
/// );
/// ```
#[derive(Debug)]
pub struct CircuitGates {
    gates: Vec<Gate>,
    total_negations: usize,
    total_additions: usize,
    total_multiplications: usize,
}

impl CircuitGates {
    /// Collects the gates from within the circuit.
    pub fn collect<F: PrimeField, C: Circuit<F>>() -> Self {
        // Collect the graph details.
        let mut cs = ConstraintSystem::default();
        let _ = C::configure(&mut cs);

        let gates = cs
            .gates
            .iter()
            .map(|gate| Gate {
                name: gate.name(),
                constraints: gate
                    .polynomials()
                    .iter()
                    .enumerate()
                    .map(|(i, constraint)| Constraint {
                        name: gate.constraint_name(i),
                        expression: constraint.evaluate(
                            &util::format_value,
                            &|selector| format!("S{}", selector.0),
                            &|query| format!("F{}@{}", query.column_index, query.rotation.0),
                            &|query| format!("A{}@{}", query.column_index, query.rotation.0),
                            &|query| format!("I{}@{}", query.column_index, query.rotation.0),
                            &|a| {
                                if a.contains(' ') {
                                    format!("-({})", a)
                                } else {
                                    format!("-{}", a)
                                }
                            },
                            &|a, b| {
                                if let Some(b) = b.strip_prefix('-') {
                                    format!("{} - {}", a, b)
                                } else {
                                    format!("{} + {}", a, b)
                                }
                            },
                            &|a, b| match (a.contains(' '), b.contains(' ')) {
                                (false, false) => format!("{} * {}", a, b),
                                (false, true) => format!("{} * ({})", a, b),
                                (true, false) => format!("({}) * {}", a, b),
                                (true, true) => format!("({}) * ({})", a, b),
                            },
                            &|a, s| {
                                if a.contains(' ') {
                                    format!("({}) * {}", a, util::format_value(s))
                                } else {
                                    format!("{} * {}", a, util::format_value(s))
                                }

CircuitGates::collect::<MyCircuit>() walks the configure step and prints every gate's name, degree, and column references. Useful when chasing "why is my circuit's max degree 9 instead of 5".

3.5 TracingFloorPlanner​

halo2_proofs/src/dev/tfp.rs
/// #       todo!()
///     }
/// }
///
/// #[test]
/// fn some_circuit_test() {
///     // At the start of your test, enable tracing.
///     tracing_subscriber::fmt()
///         .with_max_level(tracing::Level::DEBUG)
///         .with_ansi(false)
///         .without_time()
///         .init();
///
///     // Now when the rest of the test runs, you will get `tracing` output for every
///     // operation that the circuit performs under the hood!
/// }
/// ```
#[derive(Debug)]
pub struct TracingFloorPlanner<P: FloorPlanner> {
    _phantom: PhantomData<P>,
}

impl<P: FloorPlanner> FloorPlanner for TracingFloorPlanner<P> {
    fn synthesize<F: Field, CS: Assignment<F>, C: Circuit<F>>(
        cs: &mut CS,
        circuit: &C,
        config: C::Config,
        constants: Vec<Column<Fixed>>,
    ) -> Result<(), Error> {
        P::synthesize(
            &mut TracingAssignment::new(cs),
            &TracingCircuit::borrowed(circuit),
            config,
            constants,
        )
    }
}

/// A helper type that augments a [`Circuit`] with [`tracing`] spans and events.
enum TracingCircuit<'c, F: Field, C: Circuit<F>> {
    Borrowed(&'c C, PhantomData<F>),
    Owned(C, PhantomData<F>),
}

impl<'c, F: Field, C: Circuit<F>> TracingCircuit<'c, F, C> {
    fn borrowed(circuit: &'c C) -> Self {
        Self::Borrowed(circuit, PhantomData)
    }

    fn owned(circuit: C) -> Self {
        Self::Owned(circuit, PhantomData)
    }

    fn inner_ref(&self) -> &C {
        match self {
            TracingCircuit::Borrowed(circuit, ..) => circuit,
            TracingCircuit::Owned(circuit, ..) => circuit,
        }
    }
}

Wraps any floor planner and emits tracing events for each region, table, and namespace push. Use it from a test by setting Circuit::FloorPlanner = TracingFloorPlanner<V1> and turning on tracing_subscriber at info level.

3.6 The dev-graph layout​

halo2_proofs/src/dev/graph/layout.rs
/// let drawing_area = drawing_area
///     .titled("Example Circuit Layout", ("sans-serif", 60))
///     .unwrap();
///
/// let circuit = MyCircuit::default();
/// let k = 5; // Suitable size for MyCircuit
/// CircuitLayout::default().render(k, &circuit, &drawing_area).unwrap();
/// ```
#[derive(Debug, Default)]
pub struct CircuitLayout {
    hide_labels: bool,
    mark_equality_cells: bool,
    show_equality_constraints: bool,
    view_width: Option<Range<usize>>,
    view_height: Option<Range<usize>>,
}

impl CircuitLayout {
    /// Sets the visibility of region labels.
    ///
    /// The default is to show labels.
    pub fn show_labels(mut self, show: bool) -> Self {
        self.hide_labels = !show;
        self
    }

    /// Marks cells involved in equality constraints, in red.
    ///
    /// The default is to not mark these cells.
    pub fn mark_equality_cells(mut self, show: bool) -> Self {
        self.mark_equality_cells = show;
        self
    }

    /// Draws red lines between equality-constrained cells.
    ///
    /// The default is to not show these, as they can get _very_ messy.
    pub fn show_equality_constraints(mut self, show: bool) -> Self {
        self.show_equality_constraints = show;
        self
    }

    /// Sets the view width for this layout, as a number of columns.
    pub fn view_width(mut self, width: Range<usize>) -> Self {
        self.view_width = Some(width);
        self
    }

    /// Sets the view height for this layout, as a number of rows.
    pub fn view_height(mut self, height: Range<usize>) -> Self {
        self.view_height = Some(height);
        self
    }

    /// Renders the given circuit on the given drawing area.
    pub fn render<F: Field, ConcreteCircuit: Circuit<F>, DB: DrawingBackend>(
        self,
        k: u32,
        circuit: &ConcreteCircuit,
        drawing_area: &DrawingArea<DB, Shift>,
    ) -> Result<(), DrawingAreaErrorKind<DB::ErrorType>> {
        use plotters::coord::types::RangedCoordusize;
        use plotters::prelude::*;

        let n = 1 << k;
        // Collect the layout details.
        let mut cs = ConstraintSystem::default();
        let config = ConcreteCircuit::configure(&mut cs);
        let mut layout = Layout::new(k, n, cs.num_selectors);
        ConcreteCircuit::FloorPlanner::synthesize(
            &mut layout,

CircuitLayout::default().render(k, &circuit, &drawing) renders the column-by-row occupancy as a PNG via plotters. The canonical use is halo2_proofs/examples/circuit-layout.rs. Compile with --features dev-graph (and test-dev-graph when running tests).

4. Failure modes​

  • Trusting MockProver::verify as a proof. It is not a proof. It is a faster, more diagnostic check of the same row identities, but it skips every commitment. A successful MockProver is necessary, not sufficient.
  • Forgetting --features dev-graph. CircuitLayout::render is gated behind this feature. Building it without the feature is a no-op.
  • assert_satisfied in production code. It panics; only call it inside #[test].
  • Reading CircuitCost::marginal_proof_size as the actual proof byte count. It is a static estimate that ignores feature-flag-driven differences. Always cross-check with a real proof.

5. Spec pointers​

6. Exercises​

  1. Run cargo test --release --features dev-graph -p halo2_proofs --example circuit-layout and inspect the resulting PNG. Identify which region in circuit-layout.rs corresponds to which colored rectangle in the image.
  2. Add a CircuitCost measurement to simple-example.rs and print the marginal proof size. Compare against the actual length of the proof bytes after create_proof.
  3. Take a known-buggy circuit (intentionally underconstrained) and run MockProver. Confirm the VerifyFailure reports the correct row and constraint name.
  4. Switch the simple-example to use TracingFloorPlanner<V1> and run with RUST_LOG=trace. Identify the region annotations the tracing output emits.

Answers in the code​

  • Exercise 1: each assign_region call in circuit-layout.rs produces one labeled rectangle. The labels are the strings passed to the region.

7. Further reading​

  • The tracing crate's introductory guide, since TracingFloorPlanner builds on it.