Halo2

The skill is based on halo2 (halo2_proofs) at the version recorded in GENERATION.md, generated at 2026-02-24.

halo2 is a Rust library for building PLONK-based zero-knowledge proofs. The main crates are halo2_proofs (circuit API, keygen, prover, verifier) and halo2_gadgets (reusable gadgets). This skill focuses on agent-oriented usage: defining circuits, configuring constraints, assigning witnesses, and debugging with the mock prover.

Core References

Features

Best practices

Generation Info

• Source: sources/halo2
• Git SHA: 32a87582dfb0ad9364ef3ffe71751ceab2a502ea
• Generated: 2026-02-24

Documentation was derived from the halo2 repository (https://github.com/zcash/halo2). The repo contains primarily Rust source and READMEs; no dedicated docs/ tree exists. Content was synthesized from:

• halo2_proofs/ (src: plonk, circuit, dev, poly; examples: simple-example, two-chip, circuit-layout)
• Root and crate READMEs

Floor Planning and Circuit Size

The floor planner decides where each region is placed in the constraint table. Circuit size is determined by the number of rows (2^k); unused rows are padded.

SimpleFloorPlanner

Default: places regions one after another in the order assign_region is called. No optimization across regions.

type FloorPlanner = SimpleFloorPlanner;

Use when:

• Circuit is small or regions are few.
• You want predictable layout for debugging.

Choosing k

• k is the log of the maximum number of rows (e.g. k = 4 ⇒ 16 rows).
• Circuit must use at most 2^k - (blinding_factors + 1) rows for advice/instance; the rest are for the proof system.
• Pick the smallest k such that your circuit fits; larger k increases proof size and time.

let k = 4;
let prover = MockProver::run(k, &circuit, instance).unwrap();
// If verify() fails with "not enough rows", increase k.

Regions and columns

• One region can use multiple columns and multiple rows; the floor planner assigns a starting row per region.
• Offsets inside a region are relative (0, 1, 2, …); do not assume absolute row numbers in chips.
• Reuse columns across regions (e.g. same advice column in many regions) to reduce total columns and help the backend.

Custom floor planners

Implement FloorPlanner::synthesize: given the circuit’s Config, call circuit.synthesize(config, &mut layouter) once. Your layouter decides how assign_region maps to rows/columns. The TracingFloorPlanner (dev) can be used to inspect placement.

Key points

• Start with SimpleFloorPlanner; switch only if you need better packing or custom layout.
• Use MockProver::run(k, ...) to confirm the circuit fits before keygen and proving.
• Fewer columns and reuse (same column, many regions) generally improve performance.

<!-- Source references:

• https://github.com/zcash/halo2
• halo2_proofs/src/plonk/circuit.rs (FloorPlanner)
• halo2_proofs/src/circuit/floor_planner/single_pass.rs, v1.rs
• halo2_proofs/src/dev/tfp.rs (TracingFloorPlanner)

-->

Chip and Region

Chips encapsulate reusable constraint logic; regions are the scope in which advice/fixed cells and selectors are assigned. The layouter provides regions to the circuit’s synthesize implementation.

Chip trait

use halo2_proofs::circuit::Chip;

pub trait Chip<F: Field>: Sized {
    type Config: Debug + Clone;
    type Loaded: Debug + Clone;

    fn config(&self) -> &Self::Config;
    fn loaded(&self) -> &Self::Loaded;
}

• Config: Built in Circuit::configure, stored in the chip, holds columns and selectors.
• Loaded: Optional state loaded at the start of synthesis (e.g. fixed data). Access via Chip::load in the layouter if needed.

Chips are constructed with Config (and optionally Loaded) and used inside synthesize to assign cells and enable selectors.

Region operations

Inside layouter.assign_region(|| "name", |mut region| { ... }):

// Enable a selector at region-relative row offset
config.s_mul.enable(&mut region, 0)?;

// Assign advice (witness) cell
let cell = region.assign_advice(|| "label", config.advice[0], offset, || value)?;

// Assign constant into advice column (equality-constrained to constant)
region.assign_advice_from_constant(|| "constant", config.advice[0], 0, constant)?;

// Copy value from another cell and constrain equality (e.g. for cross-region wiring)
let b = a.copy_advice(|| "copy", &mut region, config.advice[1], 0)?;

// Constrain two cells to be equal
region.constrain_equal(cell_a.cell(), cell_b.cell())?;

// Expose a cell as public input (instance column)
layouter.constrain_instance(cell.cell(), config.instance, row)?;

• Offsets inside a region are relative (0, 1, 2, …). The floor planner assigns absolute rows; chips must not assume absolute positions.
• Use `copy_advice` or `constrain_equal` to wire values between regions or to instance column.

Layouter

• `assign_region`: Run a closure that receives a Region and performs the assignments above. Multiple regions can be created; the floor planner places them.
• `namespace`: Wrap a sub-layouter for naming (e.g. layouter.namespace(|| "load a", |layouter| { ... })).
• `constrain_instance`: Bind an assigned cell to a given (instance column, row) for public inputs.

Key points

• One region = one contiguous block of assignments; use multiple regions to let the floor planner reorder and pack.
• Selectors are enabled per region/offset; the same selector can be enabled in many regions.
• For cross-region equality, columns must have enable_equality and you must use constrain_equal or copy_advice.

<!-- Source references:

• https://github.com/zcash/halo2
• halo2_proofs/src/circuit.rs (Chip, Region, AssignedCell::copy_advice)
• halo2_proofs/src/circuit/layouter.rs (RegionLayouter, Layouter)
• halo2_proofs/examples/simple-example.rs

-->

Circuit API

Define a PLONK circuit by implementing the Circuit<F> trait. The backend uses configure to learn the constraint system and synthesize to fill in witnesses.

Trait definition

use halo2_proofs::plonk::{Circuit, ConstraintSystem, Error};

pub trait Circuit<F: Field> {
    type Config: Clone;
    type FloorPlanner: FloorPlanner;

    fn without_witnesses(&self) -> Self;
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config;
    fn synthesize(&self, config: Self::Config, layouter: impl Layouter<F>) -> Result<(), Error>;
}

• `without_witnesses`: Return a copy of the circuit with no witness values (e.g. Self::default()). Used during key generation when no private inputs exist.
• `configure`: Describe gates, columns, lookups, and equality; return a Config that stores column and selector references for use in synthesize.
• `synthesize`: Assign advice/fixed/instance cells and enable selectors using the layouter. Called once per proof with the actual witness.

Usage

use ff::Field;
use halo2_proofs::{
    circuit::{Layouter, SimpleFloorPlanner, Value},
    plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Selector},
    poly::Rotation,
};

#[derive(Default)]
struct MyCircuit<F: Field> {
    a: Value<F>,
    b: Value<F>,
}

impl<F: Field> Circuit<F> for MyCircuit<F> {
    type Config = (Column<Advice>, Column<Advice>, Selector);
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self {
        Self::default()
    }

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let a = meta.advice_column();
        let b = meta.advice_column();
        meta.enable_equality(a);
        meta.enable_equality(b);
        let s = meta.selector();
        meta.create_gate("my_gate", |meta| {
            let a = meta.query_advice(a, Rotation::cur());
            let b = meta.query_advice(b, Rotation::cur());
            let s = meta.query_selector(s);
            vec![s * (a * b - meta.query_advice(b, Rotation::next()))]
        });
        (a, b, s)
    }

    fn synthesize(&self, config: Self::Config, mut layouter: impl Layouter<F>) -> Result<(), Error> {
        let (a, b, s) = config;
        layouter.assign_region(|| "region", |mut region| {
            s.enable(&mut region, 0)?;
            region.assign_advice(|| "a", a, 0, || self.a)?;
            region.assign_advice(|| "b", b, 0, || self.b)?;
            region.assign_advice(|| "b_next", b, 1, || self.a * self.b)?;
            Ok(())
        })
    }
}

Key points

• Config is created once in configure and reused in synthesize; store columns and selectors there.
• Use Value::known(x) for witnesses during proving and Value::unknown() (or omit) when witnesses are not available (e.g. keygen).
• FloorPlanner controls how regions are placed in the table; SimpleFloorPlanner is the default and places regions sequentially.

<!-- Source references:

• https://github.com/zcash/halo2
• halo2_proofs/src/plonk/circuit.rs (Circuit, FloorPlanner)
• halo2_proofs/examples/simple-example.rs

-->

Columns and Values

Column kinds, the Value and Assigned types for optional/witness data, and AssignedCell for in-circuit references.

Column types

• `Column<Advice>`: Witness column; prover fills during synthesis. Use for private inputs and intermediate values.
• `Column<Fixed>`: Same for all proofs; used for selector polynomials (after compression) and constants.
• `Column<Instance>`: Public inputs; verifier provides; constrain with layouter.constrain_instance(cell, instance_col, row).
• `TableColumn`: For lookup tables; assigned via TableLayouter::assign_cell; refer to same column in meta.lookup_table_column() and in the table layouter.

Columns are created in ConstraintSystem during configure and stored in circuit/chip config.

Value\<T\>

Used when the value might be unknown (e.g. during keygen):

use halo2_proofs::circuit::Value;

// Known witness (e.g. during proving)
let v = Value::known(field_element);

// Unknown (e.g. during keygen or dummy runs)
let v = Value::unknown();

// Map and combine
let out = a.zip(b).map(|(a, b)| a * b);

Use Value in assign_advice(..., || value) and in circuit structs that hold optional witnesses.

Assigned\<F\>

Represents a field element that may be stored as a fraction (for batch inversion):

• `Assigned::Zero`
• `Assigned::Trivial(f)`
• `Assigned::Rational(num, denom)` (denom zero is treated as zero)

Used inside regions and in Value<Assigned<F>> for assignment callbacks.

AssignedCell\<V, F\>

A cell that has been assigned and optionally constrained:

let cell: AssignedCell<F, F> = region.assign_advice(|| "a", col, 0, || self.a)?;

// Copy value to another cell and constrain equality
let copied = cell.copy_advice(|| "copy", &mut region, other_col, 0)?;

// Expose as public
layouter.constrain_instance(cell.cell(), instance_col, row)?;

• `cell.cell()`: Get the Cell (region index, row offset, column) for equality/instance constraints.
• `cell.value()`: Get Value<&V>; use value_field() when V converts to Assigned<F>.

Rotation

Row offset relative to “current” row in gate/lookup expressions:

• `Rotation::cur()`: 0
• `Rotation::next()`: 1
• `Rotation::prev()`: -1
• `Rotation(i)`: Arbitrary offset

Used in meta.query_advice(column, Rotation::cur()) and similar in create_gate / lookup.

Key points

• Use Value for any witness that might be missing (keygen vs prove).
• Use AssignedCell when you need to reference a cell for constraints or copying; use cell.cell() for constrain_equal / constrain_instance.
• Gate expressions use Rotation to refer to rows; more distinct rotations can increase cost.

<!-- Source references:

• https://github.com/zcash/halo2
• halo2_proofs/src/plonk/assigned.rs (Assigned)
• halo2_proofs/src/circuit/value.rs (Value)
• halo2_proofs/src/circuit.rs (AssignedCell, Cell)
• halo2_proofs/src/poly/domain.rs (Rotation)

-->

Constraint System

ConstraintSystem<F> is built in Circuit::configure to declare columns, gates, and lookup arguments. All column and selector creation happens here; synthesis only assigns values.

Column types

use halo2_proofs::plonk::{Advice, Column, ConstraintSystem, Fixed, Instance};

// Advice (witness) columns: prover fills these during synthesize
let advice = meta.advice_column();

// Fixed columns: same for all proofs (selectors get compiled here; constants go here too)
let fixed = meta.fixed_column();

// Instance column: public inputs; verifier provides these
let instance = meta.instance_column();

// For lookups: table columns (fixed at assignment time)
let table = meta.lookup_table_column();

Enabling equality and constants

• `meta.enable_equality(column)`: Include column in the permutation argument so you can constrain equality between cells (e.g. region.constrain_equal(a, b) or layouter.constrain_instance(...)).
• `meta.enable_constant(fixed_column)`: Mark a fixed column as usable for constants; then use region.assign_advice_from_constant or the layouter’s constant API.

Selectors and gates

use halo2_proofs::poly::Rotation;

let s_mul = meta.selector();

meta.create_gate("mul", |meta| {
    let lhs = meta.query_advice(advice[0], Rotation::cur());
    let rhs = meta.query_advice(advice[1], Rotation::cur());
    let out = meta.query_advice(advice[0], Rotation::next());
    let s = meta.query_selector(s_mul);
    // Constraint: when s = 1, lhs * rhs = out
    vec![s * (lhs * rhs - out)]
});

• `meta.selector()`: Simple selector; enable per row with selector.enable(&mut region, offset).
• `meta.complex_selector()`: For gates that need more than one selector value per row.
• `create_gate(name, f)`: f receives VirtualCells to build expressions; return a non-empty list of expressions (each must equal zero). Use Rotation::cur(), next(), prev() for row offsets.

Lookups

meta.lookup(|meta| {
    let a = meta.query_advice(advice_col, Rotation::cur());
    vec![(a, table_column)]
});

• `meta.lookup(name, table_map)`: table_map returns Vec<(Expression<F>, TableColumn)>. Input expressions must not contain a simple selector. Table columns are filled via the layouter’s table API (assign_cell on a TableLayouter).

Minimum degree

• `meta.set_minimum_degree(degree)`: Force a minimum circuit degree (e.g. for the permutation argument). Use when you need a larger degree than the gates imply.

Key points

• Do not create columns or gates outside configure; the prover/verifier use the same constraint system from keygen.
• Equality must be enabled on any column used in constrain_equal or for public inputs.
• Gates are additive: all returned expressions are constrained to zero; use selectors so constraints only apply where intended.

<!-- Source references:

• https://github.com/zcash/halo2
• halo2_proofs/src/plonk/circuit.rs (ConstraintSystem, create_gate, lookup, enable_equality)

-->

Key Generation, Prover, and Verifier

Generate proving/verifying keys from a circuit, create proofs with witnesses, and verify proofs with public inputs.

Parameters

Use a curve that implements the halo2 backend (e.g. Pasta, BN256). Parameters are tied to circuit size k (number of rows ≤ 2^k):

use halo2_proofs::poly::commitment::Params;

let params = Params::new(k); // or load from file / Params::read

Key generation

use halo2_proofs::plonk::{keygen_vk, keygen_pk, ProvingKey, VerifyingKey};

let vk = keygen_vk(&params, &circuit).expect("keygen_vk");
let pk = keygen_pk(&params, vk.clone(), &circuit).expect("keygen_pk");

• `keygen_vk`: Build verifying key from params and circuit (uses Circuit::configure and a dummy synthesis).
• `keygen_pk`: Build proving key from params, vk, and circuit. Circuit is typically without_witnesses() or default.

Creating a proof

use halo2_proofs::plonk::create_proof;
use halo2_proofs::transcript::{Blake2bWrite, Challenge255, TranscriptWriterBuffer};

let mut rng = rand::thread_rng();
let circuit = MyCircuit { a: Value::known(a), b: Value::known(b) };
let instances = &[&[&[public_inputs][..]][..]]; // one circuit, one instance set

let mut transcript = Blake2bWrite::<_, _, Challenge255<_>>::init(vec![]);
create_proof(&params, &pk, &[circuit], instances, rng, &mut transcript)?;
let proof = transcript.finalize();

• `instances`: &[&[&[F]]] — per circuit, per instance column, list of public values. Must match num_instance_columns and be zero-padded to the expected length if needed.
• Transcript: Backend-specific; must match verifier (e.g. Blake2bWrite + Challenge255).

Verifying

use halo2_proofs::plonk::verify_proof;

verify_proof(&params, pk.get_vk(), &[instances], &proof)?;

• `instances`: Same shape as at proving time (e.g. &[&[&[F]]] for one circuit and its instance columns).
• Verification is deterministic given params, vk, instances, and proof.

Key points

• Use the same k (and params) for keygen, proving, and verifying; circuit must fit in 2^k rows.
• Public inputs are passed as instances and must match the cells constrained via constrain_instance.
• Proving key holds the verifying key; use pk.get_vk() when you only need to verify.

<!-- Source references:

• https://github.com/zcash/halo2
• halo2_proofs/src/plonk/keygen.rs (keygen_vk, create_proving_key)
• halo2_proofs/src/plonk/prover.rs (create_proof)
• halo2_proofs/src/plonk/verifier.rs (verify_proof)

-->

Lookup Tables

Lookup arguments constrain that values in advice (or other) columns appear in a fixed table. Tables are assigned via TableLayouter; the constraint is declared in ConstraintSystem::lookup.

Declaring a lookup

In Circuit::configure:

let table_col = meta.lookup_table_column();
meta.enable_equality(advice_col); // if advice is used in the lookup input

meta.lookup(|meta| {
    let a = meta.query_advice(advice_col, Rotation::cur());
    vec![(a, table_col)]
});

• Input: One or more Expression<F> (e.g. from query_advice). Must not contain a simple selector.
• Table: One or more TableColumn; each pair (input_expr, table_column) means “input must appear in that table column”.

Filling the table

Tables are filled in synthesize using the layouter’s table API. The default layouter provides assign_table (or equivalent) that gives a TableLayouter:

layouter.assign_table(|| "my_table", |mut table| {
    for (i, value) in table_values.iter().enumerate() {
        table.assign_cell(|| "cell", table_col, i, || Value::known(Assigned::from(*value)))?;
    }
    Ok(())
})?;

• Table columns are assigned starting at row 0; the same table column must not be used in more than one assign_table (or equivalent) scope for the same table.
• Row 0 is often used as a default; the rest are the allowed values for the lookup.

Multiple columns and multiple lookups

• One lookup can have multiple pairs: vec![(a, t1), (b, t2)] constrains a in table t1 and b in table t2.
• You can call meta.lookup multiple times for different lookup arguments.

Key points

• `TableColumn` is created with meta.lookup_table_column() and used both in meta.lookup(...) and in assign_cell on the table layouter.
• Input expressions to lookup must not contain a simple selector; use rotations (e.g. Rotation::cur()) as needed.
• Table assignment is fixed at synthesis time; ensure the table contains all values the prover will use for the lookup inputs.

<!-- Source references:

• https://github.com/zcash/halo2
• halo2_proofs/src/plonk/circuit.rs (lookup, lookup_table_column)
• halo2_proofs/src/circuit/table_layouter.rs (TableLayouter, assign_cell)
• halo2_proofs/src/plonk/lookup/

-->

Mock Prover

MockProver runs the circuit with concrete values and checks all constraints locally. Use it to debug constraint violations without generating real proofs.

Basic usage

use halo2_proofs::dev::MockProver;

let k = 4; // circuit size 2^k
let circuit = MyCircuit { a: Value::known(a), b: Value::known(b) };
let public_inputs = vec![expected_public];

let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();

assert_eq!(prover.verify(), Ok(()));

• `MockProver::run(k, circuit, instances)`: instances is Vec<Vec<F>> (one vec per instance column). Same shape as the instances argument to create_proof.
• `prover.verify()`: Returns Ok(()) if all constraints and lookups pass, or Err(Vec<VerifyFailure>) with failure details.

Interpreting failures

if let Err(failures) = prover.verify() {
    for f in failures {
        println!("{:?}", f);
    }
}

Common VerifyFailure variants:

• `ConstraintNotSatisfied`: A gate polynomial was non-zero (gate name, column, row).
• `Lookup`: A lookup input was not in the table (lookup name, row, etc.).
• `Permutation`: A permutation constraint failed (column, row).
• `CellNotAssigned`: A cell was used but never assigned.

Use these to locate the exact constraint or cell that failed.

When to use

• After changing gates or assignments: run MockProver before spending time on full proving.
• To check that a circuit rejects bad inputs: pass wrong public inputs or wrong witness and assert prover.verify().is_err().
• No params or keys needed; only the circuit and instance/public inputs.

Key points

• Use the same k as you will use for real params; circuit must fit in 2^k rows.
• Instance list must match constrain_instance usage (one vec per instance column, correct length).
• MockProver is in the dev module and may not be enabled in all feature sets; typically available with default features.

<!-- Source references:

• https://github.com/zcash/halo2
• halo2_proofs/src/dev.rs (MockProver, VerifyFailure)
• halo2_proofs/examples/simple-example.rs

-->

Parallelism

halo2 uses rayon for parallel computation. You can control the number of threads or disable parallelism.

Environment variable

export RAYON_NUM_THREADS=8

Set before running keygen or proving. If unset, rayon uses the default (often all logical cores).

Disabling multicore

Disable the "multicore" feature on halo2_proofs:

[dependencies]
halo2_proofs = { version = "...", default-features = false }

Warning: disabling multicore significantly reduces performance; use only when needed (e.g. embedded or single-threaded environments).

Key points

• No code changes required; parallelism is used internally in FFT, MSM, and other steps.
• Use RAYON_NUM_THREADS to cap or fix thread count for reproducible or resource-limited runs.

<!-- Source references:

• https://github.com/zcash/halo2 (root README)
• halo2_proofs uses rayon for parallel computation

-->