The PLONKish Arithmetization

1. Why this chapter exists

Before any commitment, any FFT, any polynomial, halo2 starts with an arithmetization: a rectangular table of cells, a fixed list of columns, and a fixed list of low-degree polynomial constraints. The constraint system is the user-facing API. Almost every halo2 chip boils down to "allocate a few columns, write a few constraints relating them". If you understand chapter 04 (polynomial domains) and this chapter, you can read the prover in chapter 11 with no surprises. This is the most important chapter in the course.

2. Definitions

Fix the small domain $H = \{1, \omega, \dots, \omega^{n-1}\}$ from chapter 04, with $n = 2^k$ .

Definition (PLONKish table). A table of $n$ rows and $N = N_a + N_f + N_i$ columns, partitioned into:

$N_a$ advice columns (witness data),
$N_f$ fixed columns (selectors and lookup tables),
$N_i$ instance columns (public inputs).

Each column is a function $A : H \to \mathbb{F}_p$ (we identify the row $i$ with $\omega^i$ ).

Definition (Rotation). A rotation $r \in \mathbb{Z}$ acts on a column $A$ by $(A \cdot \omega^r)(\omega^i) = A(\omega^{i+r})$ . In the Lagrange basis this is the index shift by $r \bmod n$ . The relative rotations a gate may use are bounded: the verifier must preimage every distinct $(\text{column}, r)$ pair in the proof.

Definition (Expression). A formal arithmetic combination over constants, column queries, and selectors. The grammar:

\begin{aligned} E ::=&\ \mathsf{Constant}(c) \\ |&\ \mathsf{Selector}(s) \\ |&\ \mathsf{Fixed}(A, r)\ |\ \mathsf{Advice}(A, r)\ |\ \mathsf{Instance}(A, r) \\ |&\ -E\ |\ E + E\ |\ E \cdot E\ |\ \alpha \cdot E \end{aligned}

Definition (Custom gate). A list of expressions $(p_1, \dots, p_g)$ supplied to ConstraintSystem::create_gate. The proving system enforces $p_j(\omega^i) = 0$ for every row $i$ and every gate index $j$ ; that is, $t_H \mid p_j$ for each $j$ .

Definition (Simple selector). A selector $s$ promised by the caller to multiply at most one other selector at a time. Simple selectors can be combined into fewer fixed columns by the selector-combining optimization; see dev/util.rs and the design chapter referenced below.

Definition (Permutation argument). Equality constraints between cells (Region::constrain_equal) are realized by a permutation argument over the chosen equality columns; see chapter 08.

Definition (Lookup argument). A claim that the values in some columns at every row appear in a fixed table; see chapter 07.

3. The code

3.1 The four column types

halo2_proofs/src/plonk/circuit.rs
pub trait ColumnType:
    'static + Sized + Copy + std::fmt::Debug + PartialEq + Eq + Into<Any>
{
}

/// A column with an index and type
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct Column<C: ColumnType> {
    index: usize,
    column_type: C,
}

impl<C: ColumnType> Column<C> {
    #[cfg(test)]
    pub(crate) fn new(index: usize, column_type: C) -> Self {
        Column { index, column_type }
    }

    pub(crate) fn index(&self) -> usize {
        self.index
    }

    /// Type of this column.
    pub fn column_type(&self) -> &C {
        &self.column_type
    }
}

impl<C: ColumnType> Ord for Column<C> {
    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
        // This ordering is consensus-critical! The layouters rely on deterministic column
        // orderings.
        match self.column_type.into().cmp(&other.column_type.into()) {
            // Indices are assigned within column types.
            std::cmp::Ordering::Equal => self.index.cmp(&other.index),
            order => order,
        }
    }
}

impl<C: ColumnType> PartialOrd for Column<C> {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        Some(self.cmp(other))
    }
}

/// An advice column
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct Advice;

/// A fixed column
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct Fixed;

/// An instance column
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct Instance;

/// An enum over the Advice, Fixed, Instance structs
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub enum Any {
    /// An Advice variant
    Advice,
    /// A Fixed variant
    Fixed,
    /// An Instance variant
    Instance,
}

Tag types Advice, Fixed, Instance are zero-sized markers; Any is the runtime enum. Column<C> is (index, marker).

3.2 Selectors

halo2_proofs/src/plonk/circuit.rs
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub struct Selector(pub(crate) usize, bool);

impl Selector {
    /// Enable this selector at the given offset within the given region.
    pub fn enable<F: Field>(&self, region: &mut Region<F>, offset: usize) -> Result<(), Error> {
        region.enable_selector(|| "", self, offset)
    }

    /// Is this selector "simple"? Simple selectors can only be multiplied
    /// by expressions that contain no other simple selectors.
    pub fn is_simple(&self) -> bool {
        self.1
    }
}

A Selector(idx, is_simple) is a virtual fixed column that takes values in $\{0, 1\}$ . Two flavours exist:

Simple selectors (constructed by meta.selector()): may be combined together at keygen time to save columns.
Complex selectors (constructed by meta.complex_selector()): always materialize as their own fixed column. Required whenever the selector is multiplied by another selector inside a gate or used inside a lookup expression.

3.3 Queries

halo2_proofs/src/plonk/circuit.rs
#[derive(Copy, Clone, Debug)]
pub struct FixedQuery {
    /// Query index
    pub(crate) index: usize,
    /// Column index
    pub(crate) column_index: usize,
    /// Rotation of this query
    pub(crate) rotation: Rotation,
}

/// Query of advice column at a certain relative location
#[derive(Copy, Clone, Debug)]
pub struct AdviceQuery {
    /// Query index
    pub(crate) index: usize,
    /// Column index
    pub(crate) column_index: usize,
    /// Rotation of this query
    pub(crate) rotation: Rotation,
}

/// Query of instance column at a certain relative location
#[derive(Copy, Clone, Debug)]
pub struct InstanceQuery {
    /// Query index
    pub(crate) index: usize,
    /// Column index
    pub(crate) column_index: usize,
    /// Rotation of this query
    pub(crate) rotation: Rotation,
}

Every distinct (column, rotation) pair becomes one entry in the proof's evaluation list. Reusing the same query in many gates is free; introducing a new rotation costs one extra opening.

3.4 The `TableColumn` type

halo2_proofs/src/plonk/circuit.rs
/// A fixed column of a lookup table.
///
/// A lookup table can be loaded into this column via [`Layouter::assign_table`]. Columns
/// can currently only contain a single table, but they may be used in multiple lookup
/// arguments via [`ConstraintSystem::lookup`].
///
/// Lookup table columns are always "encumbered" by the lookup arguments they are used in;
/// they cannot simultaneously be used as general fixed columns.
///
/// [`Layouter::assign_table`]: crate::circuit::Layouter::assign_table
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
pub struct TableColumn {
    /// The fixed column that this table column is stored in.
    ///
    /// # Security
    ///
    /// This inner column MUST NOT be exposed in the public API, or else chip developers
    /// can load lookup tables into their circuits without default-value-filling the
    /// columns, which can cause soundness bugs.
    inner: Column<Fixed>,
}

impl TableColumn {
    pub(crate) fn inner(&self) -> Column<Fixed> {
        self.inner
    }

    /// Enable equality on this TableColumn.
    pub fn enable_equality<F: Field>(&self, meta: &mut ConstraintSystem<F>) {
        meta.enable_equality(self.inner)
    }
}

TableColumn wraps a Column<Fixed> for use inside lookup arguments. The wrapper exists to prevent chip authors from accidentally loading a lookup table into a column without default-padding the unused rows, which would create a soundness bug. The documentation comment on inner spells this out explicitly.

3.5 The `Circuit` trait

halo2_proofs/src/plonk/circuit.rs
pub trait Circuit<F: Field> {
    /// This is a configuration object that stores things like columns.
    type Config: Clone;
    /// The floor planner used for this circuit. This is an associated type of the
    /// `Circuit` trait because its behaviour is circuit-critical.
    type FloorPlanner: FloorPlanner;

    /// Returns a copy of this circuit with no witness values (i.e. all witnesses set to
    /// `None`). For most circuits, this will be equal to `Self::default()`.
    fn without_witnesses(&self) -> Self;

    /// The circuit is given an opportunity to describe the exact gate
    /// arrangement, column arrangement, etc.
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config;

    /// Given the provided `cs`, synthesize the circuit. The concrete type of
    /// the caller will be different depending on the context, and they may or
    /// may not expect to have a witness present.
    fn synthesize(&self, config: Self::Config, layouter: impl Layouter<F>) -> Result<(), Error>;
}

The two phases:

configure(meta): pure shape declaration. The implementer allocates columns, declares gates, declares lookups, returns the Config. No witness data is available here.
synthesize(config, layouter): assignment phase. The implementer walks the circuit and writes witness values into the cells via the Layouter (see chapter 06).

The third method without_witnesses returns a witness-less copy of self; it is what keygen and the verifier construct so they can call configure and discover the shape without ever seeing the witness.

3.6 `Expression`

halo2_proofs/src/plonk/circuit.rs
#[derive(Clone)]
pub enum Expression<F> {
    /// This is a constant polynomial
    Constant(F),
    /// This is a virtual selector
    Selector(Selector),
    /// This is a fixed column queried at a certain relative location
    Fixed(FixedQuery),
    /// This is an advice (witness) column queried at a certain relative location
    Advice(AdviceQuery),
    /// This is an instance (external) column queried at a certain relative location
    Instance(InstanceQuery),
    /// This is a negated polynomial
    Negated(Box<Expression<F>>),
    /// This is the sum of two polynomials
    Sum(Box<Expression<F>>, Box<Expression<F>>),
    /// This is the product of two polynomials
    Product(Box<Expression<F>>, Box<Expression<F>>),
    /// This is a scaled polynomial
    Scaled(Box<Expression<F>>, F),
}

impl<F: Field> Expression<F> {

Expression<F> is a tree of column queries, selector references, constants, and arithmetic combinators. Its core operation is evaluate, a fold parameterized by callbacks for each variant; this is how the same expression is reused by the prover (evaluated on the extended coset), the verifier (evaluated at a single point), and the dev tools (evaluated row by row).

3.7 `Constraints::with_selector`

halo2_proofs/src/plonk/circuit.rs
pub struct Constraints<F: Field, C: Into<Constraint<F>>, Iter: IntoIterator<Item = C>> {
    selector: Expression<F>,
    constraints: Iter,
}

impl<F: Field, C: Into<Constraint<F>>, Iter: IntoIterator<Item = C>> Constraints<F, C, Iter> {
    /// Constructs a set of constraints that are controlled by the given selector.
    ///
    /// Each constraint `c` in `iterator` will be converted into the constraint
    /// `selector * c`.
    pub fn with_selector(selector: Expression<F>, constraints: Iter) -> Self {
        Constraints {
            selector,
            constraints,
        }
    }
}

fn apply_selector_to_constraint<F: Field, C: Into<Constraint<F>>>(
    (selector, c): (Expression<F>, C),
) -> Constraint<F> {
    let constraint: Constraint<F> = c.into();
    Constraint {
        name: constraint.name,
        poly: selector * constraint.poly,

Constraints::with_selector(s, iter) multiplies every constraint in iter by the selector expression s. This is the idiom for "these constraints are only enforced where the selector is 1". Use it instead of manually multiplying by s inside each expression: the helper handles the iterator-of-tuple conversion and keeps the named-constraint debug labels intact.

3.8 `ConstraintSystem`

halo2_proofs/src/plonk/circuit.rs
/// permutation arrangements.
#[derive(Debug, Clone)]
pub struct ConstraintSystem<F: Field> {
    pub(crate) num_fixed_columns: usize,
    pub(crate) num_advice_columns: usize,
    pub(crate) num_instance_columns: usize,
    pub(crate) num_selectors: usize,

    /// This is a cached vector that maps virtual selectors to the concrete
    /// fixed column that they were compressed into. This is just used by dev
    /// tooling right now.
    pub(crate) selector_map: Vec<Column<Fixed>>,

    pub(crate) gates: Vec<Gate<F>>,
    pub(crate) advice_queries: Vec<(Column<Advice>, Rotation)>,
    // Contains an integer for each advice column
    // identifying how many distinct queries it has
    // so far; should be same length as num_advice_columns.
    num_advice_queries: Vec<usize>,
    pub(crate) instance_queries: Vec<(Column<Instance>, Rotation)>,
    pub(crate) fixed_queries: Vec<(Column<Fixed>, Rotation)>,

    // Permutation argument for performing equality constraints
    pub(crate) permutation: permutation::Argument,

    // Vector of lookup arguments, where each corresponds to a sequence of
    // input expressions and a sequence of table expressions involved in the lookup.
    pub(crate) lookups: Vec<lookup::Argument<F>>,

    // Vector of fixed columns, which can be used to store constant values
    // that are copied into advice columns.
    pub(crate) constants: Vec<Column<Fixed>>,

    pub(crate) minimum_degree: Option<usize>,

The bag of state that configure builds up. The interesting fields:

num_advice_columns, num_fixed_columns, num_instance_columns, num_selectors: the shape counts.
gates: the list of custom gates.
advice_queries, instance_queries, fixed_queries: deduplicated (column, rotation) lookups. Their length feeds the proof size.
permutation: the permutation argument's accumulator of columns that must support equality constraints.
lookups: the list of lookup arguments.
constants: a small set of fixed columns reserved for the constant-loading workflow.
minimum_degree: a contributor-overridable lower bound on the global degree, used when the user wants to leave room for future growth without rebuilding the keys.

3.9 A minimal worked example

The canonical example circuit lives in halo2_proofs/examples/simple-example.rs. The multiplication gate is declared inside the configure block:

halo2_proofs/examples/simple-example.rs

    // We need a selector to enable the multiplication gate, so that we aren't placing
    // any constraints on cells where `NumericInstructions::mul` is not being used.
    // This is important when building larger circuits, where columns are used by
    // multiple sets of instructions.
    s_mul: Selector,
}

impl<F: Field> FieldChip<F> {
    fn construct(config: <Self as Chip<F>>::Config) -> Self {
        Self {
            config,
            _marker: PhantomData,
        }
    }

    fn configure(
        meta: &mut ConstraintSystem<F>,
        advice: [Column<Advice>; 2],
        instance: Column<Instance>,
        constant: Column<Fixed>,
    ) -> <Self as Chip<F>>::Config {
        meta.enable_equality(instance);
        meta.enable_constant(constant);
        for column in &advice {
            meta.enable_equality(*column);
        }
        let s_mul = meta.selector();

        // Define our multiplication gate!
        meta.create_gate("mul", |meta| {
            // To implement multiplication, we need three advice cells and a selector
            // cell. We arrange them like so:
            //
            // | a0  | a1  | s_mul |
            // |-----|-----|-------|
            // | lhs | rhs | s_mul |
            // | out |     |       |
            //
            // Gates may refer to any relative offsets we want, but each distinct
            // offset adds a cost to the proof. The most common offsets are 0 (the
            // current row), 1 (the next row), and -1 (the previous row), for which
            // `Rotation` has specific constructors.
            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_mul = meta.query_selector(s_mul);

            // Finally, we return the polynomial expressions that constrain this gate.
            // For our multiplication gate, we only need a single polynomial constraint.
            //
            // The polynomial expressions returned from `create_gate` will be
            // constrained by the proving system to equal zero. Our expression
            // has the following properties:
            // - When s_mul = 0, any value is allowed in lhs, rhs, and out.
            // - When s_mul != 0, this constrains lhs * rhs = out.

The constraint s_mul * (lhs * rhs - out) = 0 becomes a single Expression<F> evaluated row by row.

4. Failure modes

Simple selector misuse. Multiplying two simple selectors inside the same gate breaks the selector-combining optimization and produces a wrong proving key. Use complex_selector() if you need this.
Forgetting to call meta.enable_equality(col). Equality constraints (region.constrain_equal) only work on columns the permutation argument was told about. The error surface is Error::ColumnNotInPermutation.
High-degree gates. The gate degree directly drives extended_k in chapter 04. A degree-9 gate roughly doubles the extended domain size relative to a degree-5 gate; that doubles prover time and proof size.
Lookup encumbrance. A TableColumn is exclusive to its lookup; you cannot also use the underlying Column<Fixed> as a general-purpose fixed column. Trying to results in Error::ColumnNotInPermutation or a MockProver failure.

5. Spec pointers

PLONK paper, eprint 2019/953, section 4: the standard PLONK arithmetization. The halo2 arithmetization generalizes this by allowing custom gates and more advice columns.
The Halo 2 Book "PLONKish Arithmetization" chapter covers the same material from a user's perspective.
The Halo 2 Book "Selector combining" chapter explains the simple-vs-complex selector distinction and the packing algorithm that justifies it.

6. Exercises

Open halo2_proofs/examples/simple-example.rs and identify the columns the example declares. How many advice, fixed, instance columns? Which one is the multiplication selector?
Extend the example with a second gate add that enforces s_add * (lhs + rhs - out) = 0 on the same advice columns. Run cargo run --release --example simple-example to check the proof still verifies.
Find the assertion in halo2_proofs/src/plonk/circuit.rs that forbids two simple selectors from multiplying each other inside a gate. (Hint: search for "simple selector".) State in one sentence what the constraint is.
Why does Circuit::without_witnesses exist? Answer in one sentence by reading the doc comment in halo2_proofs/src/plonk/circuit.rs.

Answers in the code

Exercise 1: two advice columns [a0, a1], one instance column, one fixed column for the constant, one selector s_mul. See the FieldConfig struct in simple-example.rs.
Exercise 3: the check is in ConstraintSystem::create_gate; the error message mentions "Simple selectors are not allowed to be multiplied by other simple selectors".
Exercise 4: keygen and the verifier need to call configure without knowing the witness; without_witnesses returns a copy with all Values set to None.

7. Further reading

Daira Hopwood's PLONKish arithmetization explainer.
The "Custom gates" section of the Halo 2 Book.

1. Why this chapter exists​

2. Definitions​

3. The code​

3.1 The four column types​

3.2 Selectors​

3.3 Queries​

3.4 The TableColumn type​

3.5 The Circuit trait​

3.6 Expression​

3.7 Constraints::with_selector​

3.8 ConstraintSystem​

3.9 A minimal worked example​

4. Failure modes​

5. Spec pointers​

6. Exercises​

Answers in the code​

7. Further reading​