Skip to main content

Circuit Synthesis: Chip, Region, FloorPlanner

1. Why this chapter exists​

Chapter 05 covered what a circuit declares. This chapter covers what a circuit does: how synthesis walks the table, assigns values, and produces the witness consumed by the prover. The chip-and-region API is what every gadget author writes against, and it carries a few invariants that are not obvious from the type signatures. Get these wrong and your circuit will be either unsound or unprovable.

2. Definitions​

Definition (Region). A contiguous, opaque block of rows owned by a single chip. Inside a region, the chip uses relative offsets (0,1,2,…0, 1, 2, \dots); the layouter decides the absolute starting row. Cells inside a region can be freely cross-referenced; cells across regions must be tied together with an explicit equality constraint.

Definition (Cell). A pointer (region index,row offset,column)(\text{region index}, \text{row offset}, \text{column}) into the table. The cell does not own a value; it identifies a location.

Definition (AssignedCell). A (Value, Cell) pair. The Value is the witness data (in Some(_) mode during proving, in None mode during keygen and verification).

Definition (Layouter). The object that drives the synthesize method. The layouter exposes a single primitive, assign_region, which takes a closure that operates on a Region. The layouter is responsible for placing regions in the table.

Definition (Floor planner). The strategy the layouter uses to place regions. Two are shipped:

  • SimpleFloorPlanner: places regions back to back, one after another, in the order they are declared. Predictable, but wasteful: a region that uses few columns leaves the others empty.
  • V1 (first-pass-second-pass planner): measures the shapes of every region in a first pass, then places them by packing columns. Substantially denser layouts, but the planner runs the synthesis closure twice, so closures must be deterministic and must not depend on side effects.

3. The code​

3.1 The Chip trait​

halo2_proofs/src/circuit.rs
/// A chip implements a set of instructions that can be used by gadgets.
///
/// The chip stores state that is required at circuit synthesis time in
/// [`Chip::Config`], which can be fetched via [`Chip::config`].
///
/// The chip also loads any fixed configuration needed at synthesis time
/// using its own implementation of `load`, and stores it in [`Chip::Loaded`].
/// This can be accessed via [`Chip::loaded`].
pub trait Chip<F: Field>: Sized {
    /// A type that holds the configuration for this chip, and any other state it may need
    /// during circuit synthesis, that can be derived during [`Circuit::configure`].
    ///
    /// [`Circuit::configure`]: crate::plonk::Circuit::configure
    type Config: fmt::Debug + Clone;

    /// A type that holds any general chip state that needs to be loaded at the start of
    /// [`Circuit::synthesize`]. This might simply be `()` for some chips.
    ///
    /// [`Circuit::synthesize`]: crate::plonk::Circuit::synthesize
    type Loaded: fmt::Debug + Clone;

    /// The chip holds its own configuration.
    fn config(&self) -> &Self::Config;

    /// Provides access to general chip state loaded at the beginning of circuit
    /// synthesis.
    ///
    /// Panics if called before `Chip::load`.
    fn loaded(&self) -> &Self::Loaded;
}

Chip::Config is the type returned by your chip's configure function and consumed by synthesize. Chip::Loaded is for chip state loaded at the start of synthesis (e.g. a precomputed lookup table); use () if you have none.

3.2 Cell and AssignedCell​

halo2_proofs/src/circuit.rs

/// A pointer to a cell within a circuit.
#[derive(Clone, Copy, Debug)]
pub struct Cell {
    /// Identifies the region in which this cell resides.
    region_index: RegionIndex,
    /// The relative offset of this cell within its region.
    row_offset: usize,
    /// The column of this cell.
    column: Column<Any>,
}

/// An assigned cell.
#[derive(Clone, Debug)]
pub struct AssignedCell<V, F: Field> {
    value: Value<V>,
    cell: Cell,
    _marker: PhantomData<F>,
}

impl<V, F: Field> AssignedCell<V, F> {
    /// Returns the value of the [`AssignedCell`].
    pub fn value(&self) -> Value<&V> {
        self.value.as_ref()
    }

    /// Returns the cell.
    pub fn cell(&self) -> Cell {
        self.cell
    }
}

impl<V, F: Field> AssignedCell<V, F>
where
    for<'v> Assigned<F>: From<&'v V>,
{
    /// Returns the field element value of the [`AssignedCell`].
    pub fn value_field(&self) -> Value<Assigned<F>> {
        self.value.to_field()
    }
}

impl<F: Field> AssignedCell<Assigned<F>, F> {
    /// Evaluates this assigned cell's value directly, performing an unbatched inversion
    /// if necessary.
    ///
    /// If the denominator is zero, the returned cell's value is zero.
    pub fn evaluate(self) -> AssignedCell<F, F> {
        AssignedCell {
            value: self.value.evaluate(),
            cell: self.cell,
            _marker: Default::default(),
        }
    }
}

impl<F: Field> From<AssignedCell<F, F>> for AssignedCell<Assigned<F>, F> {
    fn from(ac: AssignedCell<F, F>) -> Self {
        AssignedCell {
            value: ac.value.map(|a| a.into()),
            cell: ac.cell,
            _marker: Default::default(),
        }
    }
}

impl<V: Clone, F: Field> AssignedCell<V, F>
where
    for<'v> Assigned<F>: From<&'v V>,
{
    /// Copies the value to a given advice cell and constrains them to be equal.
    ///
    /// Returns an error if either this cell or the given cell are in columns
    /// where equality has not been enabled.
    pub fn copy_advice<A, AR>(
        &self,
        annotation: A,
        region: &mut Region<'_, F>,
        column: Column<Advice>,
        offset: usize,
    ) -> Result<Self, Error>
    where
        A: Fn() -> AR,
        AR: Into<String>,
    {
        let assigned_cell =
            region.assign_advice(annotation, column, offset, || self.value.clone())?;
        region.constrain_equal(assigned_cell.cell(), self.cell())?;

        Ok(assigned_cell)
    }
}

/// A region of the circuit in which a [`Chip`] can assign cells.
///
/// Inside a region, the chip may freely use relative offsets; the [`Layouter`] will
/// treat these assignments as a single "region" within the circuit.
///

The two layered types:

  • Cell: pure pointer.
  • AssignedCell<V, F>: pointer + value. The value type V is often F for plain witness data, but Assigned<F> for cells that participate in lazy inversions (see plonk/assigned.rs).

AssignedCell::copy_advice is the canonical way to forward a witness value from one region into another: it assigns the value into the new cell and issues the equality constraint.

3.3 The Region API​

halo2_proofs/src/circuit.rs
/// [`Region::constrain_equal`] to copy in variables assigned in other regions.
///
/// TODO: It would be great if we could constrain the columns in these types to be
/// "logical" columns that are guaranteed to correspond to the chip (and have come from
/// `Chip::Config`).
#[derive(Debug)]
pub struct Region<'r, F: Field> {
    region: &'r mut dyn layouter::RegionLayouter<F>,
}

impl<'r, F: Field> From<&'r mut dyn layouter::RegionLayouter<F>> for Region<'r, F> {
    fn from(region: &'r mut dyn layouter::RegionLayouter<F>) -> Self {
        Region { region }
    }
}

impl<'r, F: Field> Region<'r, F> {
    /// Enables a selector at the given offset.
    pub(crate) fn enable_selector<A, AR>(
        &mut self,
        annotation: A,
        selector: &Selector,
        offset: usize,
    ) -> Result<(), Error>
    where
        A: Fn() -> AR,

The methods you will use most:

  • assign_advice(annotation, column, offset, value): write to an advice cell.
  • assign_fixed(annotation, column, offset, value): write to a fixed cell.
  • assign_advice_from_instance(...): write to advice and constrain it equal to a cell in an instance column.
  • assign_advice_from_constant(...): write to advice and constrain it equal to a constant (uses one of the ConstraintSystem::constants columns).
  • constrain_equal(left, right): add an equality constraint between two cells. Both columns must be in the permutation.
  • enable_selector(annotation, selector, offset): turn on a selector at a given row in the region.

3.4 The Layouter trait​

halo2_proofs/src/circuit.rs
///
pub trait Layouter<F: Field> {
    /// Represents the type of the "root" of this layouter, so that nested namespaces
    /// can minimize indirection.
    type Root: Layouter<F>;

    /// Assign a region of gates to an absolute row number.
    ///
    /// Inside the closure, the chip may freely use relative offsets; the `Layouter` will
    /// treat these assignments as a single "region" within the circuit. Outside this
    /// closure, the `Layouter` is allowed to optimise as it sees fit.
    ///
    /// ```ignore
    /// fn assign_region(&mut self, || "region name", |region| {
    ///     let config = chip.config();
    ///     region.assign_advice(config.a, offset, || { Some(value)});
    /// });
    /// ```
    fn assign_region<A, AR, N, NR>(&mut self, name: N, assignment: A) -> Result<AR, Error>
    where
        A: FnMut(Region<'_, F>) -> Result<AR, Error>,
        N: Fn() -> NR,
        NR: Into<String>;

    /// Assign a table region to an absolute row number.
    ///
    /// ```ignore
    /// fn assign_table(&mut self, || "table name", |table| {
    ///     let config = chip.config();
    ///     table.assign_fixed(config.a, offset, || { Some(value)});
    /// });
    /// ```
    fn assign_table<A, N, NR>(&mut self, name: N, assignment: A) -> Result<(), Error>
    where
        A: FnMut(Table<'_, F>) -> Result<(), Error>,
        N: Fn() -> NR,
        NR: Into<String>;

    /// Constrains a [`Cell`] to equal an instance column's row value at an
    /// absolute position.
    fn constrain_instance(
        &mut self,
        cell: Cell,
        column: Column<Instance>,
        row: usize,
    ) -> Result<(), Error>;

    /// Gets the "root" of this assignment, bypassing the namespacing.
    ///
    /// Not intended for downstream consumption; use [`Layouter::namespace`] instead.
    fn get_root(&mut self) -> &mut Self::Root;

    /// Creates a new (sub)namespace and enters into it.
    ///
    /// Not intended for downstream consumption; use [`Layouter::namespace`] instead.
    fn push_namespace<NR, N>(&mut self, name_fn: N)
    where
        NR: Into<String>,
        N: FnOnce() -> NR;

    /// Exits out of the existing namespace.
    ///
    /// Not intended for downstream consumption; use [`Layouter::namespace`] instead.
    fn pop_namespace(&mut self, gadget_name: Option<String>);

    /// Enters into a namespace.
    fn namespace<NR, N>(&mut self, name_fn: N) -> NamespacedLayouter<'_, F, Self::Root>
    where
        NR: Into<String>,
        N: FnOnce() -> NR,
    {
        self.get_root().push_namespace(name_fn);

        NamespacedLayouter(self.get_root(), PhantomData)
    }
}

Most of the time, a chip only calls:

  • layouter.assign_region(name, closure)
  • layouter.assign_table(name, closure) (for filling lookup tables; uses Table instead of Region).
  • layouter.constrain_instance(cell, column, row) (to expose a cell to a public-input row).
  • layouter.namespace(name): a debug-only annotation that nests region names for traces and dev output. Returns a NamespacedLayouter that flushes the namespace on Drop.

3.5 SimpleFloorPlanner​

halo2_proofs/src/circuit/floor_planner/single_pass.rs
/// A simple [`FloorPlanner`] that performs minimal optimizations.
///
/// This floor planner is suitable for debugging circuits. It aims to reflect the circuit
/// "business logic" in the circuit layout as closely as possible. It uses a single-pass
/// layouter that does not reorder regions for optimal packing.
#[derive(Debug)]
pub struct SimpleFloorPlanner;

impl FloorPlanner for SimpleFloorPlanner {
    fn synthesize<F: Field, CS: Assignment<F>, C: Circuit<F>>(
        cs: &mut CS,
        circuit: &C,
        config: C::Config,
        constants: Vec<Column<Fixed>>,
    ) -> Result<(), Error> {
        let layouter = SingleChipLayouter::new(cs, constants)?;
        circuit.synthesize(config, layouter)
    }
}

Single-pass. Each region starts on the row after the previous region ended, regardless of column usage. The closure is invoked once. Use this for clarity in tests and for any circuit small enough that layout density does not matter.

3.6 V1 floor planner​

halo2_proofs/src/circuit/floor_planner/v1.rs
///
/// - No column optimizations are performed. Circuit configuration is left entirely to the
///   circuit designer.
/// - A dual-pass layouter is used to measures regions prior to assignment.
/// - Regions are measured as rectangles, bounded on the cells they assign.
/// - Regions are laid out using a greedy first-fit strategy, after sorting regions by
///   their "advice area" (number of advice columns * rows).
#[derive(Debug)]
pub struct V1;

struct V1Plan<'a, F: Field, CS: Assignment<F> + 'a> {
    cs: &'a mut CS,
    /// Stores the starting row for each region.
    regions: Vec<RegionStart>,
    /// Stores the constants to be assigned, and the cells to which they are copied.
    constants: Vec<(Assigned<F>, Cell)>,
    /// Stores the table fixed columns.
    table_columns: Vec<TableColumn>,
}

impl<'a, F: Field, CS: Assignment<F> + 'a> fmt::Debug for V1Plan<'a, F, CS> {

Two passes:

  • Measurement pass: a fake layouter (V1Pass in measurement mode) records the shape of each region (which columns it uses, how many rows). No witness values are written.
  • Assignment pass: a solver assigns each region a starting row based on the measured shapes, then the closures are invoked a second time and this time the values are actually written.

This is why your assign_region closure must be a pure function of its inputs: it will run twice. Capturing a Cell::new() counter or a file handle inside the closure is wrong.

The 0.3.0 release contains the cautionary tale: the V1 planner used to depend on slice::sort_unstable_by_key, which is deterministic on a given target but produces different orderings across 32-bit and 64-bit targets. The fix in halo2_proofs/CHANGELOG.md was to switch to a stable sort, and to gate the old behaviour behind floor-planner-v1-legacy-pdqsort to keep the Orchard Verifying Key bit-identical.

4. Failure modes​

  • Side-effecting region closures. Anything stored in a Cell::new() outside the closure will be observed twice by V1. The fix is to capture only values that are computed deterministically from the closure arguments.
  • Cross-region cells without equality. Forgetting constrain_equal (or, equivalently, copy_advice) means the two cells are independent witness slots; the witness can be made consistent locally but the constraint is missing globally. This is a soundness bug.
  • assign_advice_from_constant without enable_constant. The constant-loading workflow requires meta.enable_constant(column) in configure. Without it the layouter has no fixed column to store the constant in, and synthesis returns Error::NotEnoughColumnsForConstants.
  • Mixing SimpleFloorPlanner and V1 between keygen and prove. The floor planner is part of the verifying key. If keygen used V1 and proving uses SimpleFloorPlanner, the column assignments will not match the committed fixed columns. The Circuit::FloorPlanner associated type exists precisely so this cannot happen accidentally.

5. Spec pointers​

6. Exercises​

  1. Open the two-chip example halo2_proofs/examples/two-chip.rs. Identify (a) which chip allocates each column, (b) which cells are passed between chips and how (AssignedCell returned from one and consumed by the next).
  2. Change simple-example.rs from SimpleFloorPlanner to V1 (the type alias is halo2_proofs::circuit::floor_planner::V1) and re-run. Does the proof still verify?
  3. Modify two-chip.rs so that the multiplication chip writes its output to a new region and intentionally omits the constrain_equal that ties it to the consumer. Run the example under MockProver::verify (replace the proof code with a MockProver::run) and observe the VerifyFailure that the dev tool reports.
  4. The doc comment on Region mentions a TODO about "logical columns guaranteed to correspond to the chip". Find it in halo2_proofs/src/circuit.rs and propose, in two sentences, what a fix could look like.

Answers in the code​

  • Exercise 1: the FieldChip allocates the advice and the multiplication selector; the AddChip allocates the addition selector; the chips share advice columns and pass AssignedCells between them.
  • Exercise 3: the resulting VerifyFailure will be Permutation { column, location } for the location of the omitted equality.

7. Further reading​

  • The dev tool TracingFloorPlanner in halo2_proofs/src/dev/tfp.rs wraps any floor planner and logs each region assignment via the tracing crate. Wrap your circuit in it once if you ever wonder why layout looks the way it does.