The Lookup Argument

1. Why this chapter exists

Custom gates can express polynomial relations of bounded degree. Many useful relations (range checks, bit decomposition, AND / XOR tables, S-boxes) are easier to express as "this value is one of the rows of this table". The lookup argument lets a circuit assert exactly that. It is the second-most-used soundness mechanism in halo2 after the gate system itself, and it is the one most often misunderstood. This chapter covers the math and the code so that you can write your own lookup chip and reason about the proof-size cost.

2. Definitions

Fix $n = 2^k$ and the small domain $H$ from chapter 04.

Definition (Multiset equality). Two multisets $A$ and $S$ of size $n$ are equal as multisets iff their characteristic polynomials agree: $\prod_{i=0}^{n-1} (X - A_i) = \prod_{i=0}^{n-1} (X - S_i).$

Definition (Plookup argument). Given an input multiset $A = (a_0, \dots, a_{n-1})$ and a table multiset $S = (s_0, \dots, s_{n-1})$ , the prover wants to convince the verifier that $A \subseteq S$ as a multiset. Plookup reduces this to a multiset-equality check on the sorted concatenation $(A, S)$ vs a specific permutation; the resulting check is expressed as a degree-bounded grand product. See eprint 2020/315 for the full construction.

Definition (Multi-column lookup). When the lookup has $m$ input expressions and $m$ table expressions, the prover uses a verifier-supplied challenge $\theta$ to collapse them into one column: $\tilde a = \sum_{j=0}^{m-1} \theta^{m-1-j} a_j$ and similarly for $\tilde s$ . The single-column Plookup argument is then run on $\tilde a$ and $\tilde s$ .

Definition (Grand product polynomial $z$ ). The accumulator polynomial of the lookup argument; the prover commits to $z$ and the verifier checks four boundary and recurrence relations on it (see the comment block in plonk/lookup.rs).

3. The code

3.1 The argument struct

halo2_proofs/src/plonk/lookup.rs
use super::circuit::Expression;
use ff::Field;

pub(crate) mod prover;
pub(crate) mod verifier;

#[derive(Clone, Debug)]
pub(crate) struct Argument<F: Field> {
    pub input_expressions: Vec<Expression<F>>,
    pub table_expressions: Vec<Expression<F>>,
}

impl<F: Field> Argument<F> {
    /// Constructs a new lookup argument.
    ///
    /// `table_map` is a sequence of `(input, table)` tuples.
    pub fn new(table_map: Vec<(Expression<F>, Expression<F>)>) -> Self {
        let (input_expressions, table_expressions) = table_map.into_iter().unzip();
        Argument {
            input_expressions,
            table_expressions,
        }
    }

    pub(crate) fn required_degree(&self) -> usize {
        assert_eq!(self.input_expressions.len(), self.table_expressions.len());

        // The first value in the permutation poly should be one.
        // degree 2:
        // l_0(X) * (1 - z(X)) = 0
        //
        // The "last" value in the permutation poly should be a boolean, for
        // completeness and soundness.
        // degree 3:
        // l_last(X) * (z(X)^2 - z(X)) = 0
        //
        // Enable the permutation argument for only the rows involved.
        // degree (2 + input_degree + table_degree) or 4, whichever is larger:
        // (1 - (l_last(X) + l_blind(X))) * (
        //   z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
        //   - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
        // ) = 0
        //
        // The first two values of a' and s' should be the same.
        // degree 2:
        // l_0(X) * (a'(X) - s'(X)) = 0
        //
        // Either the two values are the same, or the previous
        // value of a' is the same as the current value.
        // degree 3:
        // (1 - (l_last(X) + l_blind(X))) * (a′(X) − s′(X))⋅(a′(X) − a′(\omega^{-1} X)) = 0
        let mut input_degree = 1;
        for expr in self.input_expressions.iter() {
            input_degree = std::cmp::max(input_degree, expr.degree());
        }
        let mut table_degree = 1;
        for expr in self.table_expressions.iter() {
            table_degree = std::cmp::max(table_degree, expr.degree());
        }

        // In practice because input_degree and table_degree are initialized to
        // one, the latter half of this max() invocation is at least 4 always,
        // rendering this call pointless except to be explicit in case we change
        // the initialization of input_degree/table_degree in the future.
        std::cmp::max(
            // (1 - (l_last + l_blind)) z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
            4,
            // (1 - (l_last + l_blind)) z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
            2 + input_degree + table_degree,
        )
    }
}

Argument is the parsed declaration of one lookup: a pair of Vec<Expression<F>> of equal length, one for inputs, one for table cells. The required_degree method records, in code, the exact identities the verifier will check; it is the cleanest place in the codebase to read the Plookup algebra.

3.2 Declaring a lookup

ConstraintSystem::lookup is the public API:

halo2_proofs/src/plonk/circuit.rs
    /// Add a lookup argument for some input expressions and table columns.
    ///
    /// `table_map` returns a map between input expressions and the table columns
    /// they need to match.
    pub fn lookup(
        &mut self,
        table_map: impl FnOnce(&mut VirtualCells<'_, F>) -> Vec<(Expression<F>, TableColumn)>,
    ) -> usize {
        let mut cells = VirtualCells::new(self);
        let table_map = table_map(&mut cells)
            .into_iter()
            .map(|(input, table)| {
                if input.contains_simple_selector() {
                    panic!("expression containing simple selector supplied to lookup argument");
                }

                let table = cells.query_fixed(table.inner());

                (input, table)
            })
            .collect();

        let index = self.lookups.len();

        self.lookups.push(lookup::Argument::new(table_map));

        index
    }

The closure receives a VirtualCells (so it can call meta.query_advice etc.) and returns a vector of (input_expression, table_expression) pairs. The table expression must reference a TableColumn, never a plain Column<Fixed>. This is enforced by the types (query_lookup_table returns an Expression<F> that captures the table-column origin).

3.3 The prover

halo2_proofs/src/plonk/lookup/prover.rs
use super::super::{
    circuit::Expression, ChallengeBeta, ChallengeGamma, ChallengeTheta, ChallengeX, Error,
    ProvingKey,
};
use super::Argument;
use crate::{
    arithmetic::{eval_polynomial, parallelize, CurveAffine},
    poly::{
        self,
        commitment::{Blind, Params},
        multiopen::ProverQuery,
        Coeff, EvaluationDomain, ExtendedLagrangeCoeff, LagrangeCoeff, Polynomial, Rotation,
    },
    transcript::{EncodedChallenge, TranscriptWrite},
};
use ff::WithSmallOrderMulGroup;
use group::{
    ff::{BatchInvert, Field},
    Curve,
};
use rand_core::RngCore;
use std::{
    collections::BTreeMap,
    iter,
    ops::{Mul, MulAssign},
};

#[derive(Debug)]
pub(in crate::plonk) struct Permuted<C: CurveAffine, Ev> {
    compressed_input_expression: Polynomial<C::Scalar, LagrangeCoeff>,
    permuted_input_expression: Polynomial<C::Scalar, LagrangeCoeff>,
    compressed_input_coset: poly::Ast<Ev, C::Scalar, ExtendedLagrangeCoeff>,
    permuted_input_poly: Polynomial<C::Scalar, Coeff>,
    permuted_input_coset: poly::AstLeaf<Ev, ExtendedLagrangeCoeff>,
    permuted_input_blind: Blind<C::Scalar>,
    compressed_table_expression: Polynomial<C::Scalar, LagrangeCoeff>,
    compressed_table_coset: poly::Ast<Ev, C::Scalar, ExtendedLagrangeCoeff>,
    permuted_table_expression: Polynomial<C::Scalar, LagrangeCoeff>,
    permuted_table_poly: Polynomial<C::Scalar, Coeff>,
    permuted_table_coset: poly::AstLeaf<Ev, ExtendedLagrangeCoeff>,
    permuted_table_blind: Blind<C::Scalar>,
}

#[derive(Debug)]
pub(in crate::plonk) struct Committed<C: CurveAffine, Ev> {
    permuted: Permuted<C, Ev>,
    product_poly: Polynomial<C::Scalar, Coeff>,
    product_coset: poly::AstLeaf<Ev, ExtendedLagrangeCoeff>,
    product_blind: Blind<C::Scalar>,
}

pub(in crate::plonk) struct Constructed<C: CurveAffine> {
    permuted_input_poly: Polynomial<C::Scalar, Coeff>,
    permuted_input_blind: Blind<C::Scalar>,
    permuted_table_poly: Polynomial<C::Scalar, Coeff>,
    permuted_table_blind: Blind<C::Scalar>,
    product_poly: Polynomial<C::Scalar, Coeff>,
    product_blind: Blind<C::Scalar>,
}

The prover steps, in order:

Compute $\tilde a$ and $\tilde s$ in LagrangeCoeff, absorbing the challenge $\theta$ .
Sort $\tilde a$ into $a'$ and the matching slice of $\tilde s$ into $s'$ such that $a'$ is non-decreasing relative to $s'$ (the "compressed permutation").
Commit to $a'$ and $s'$ .
Squeeze $\beta$ and $\gamma$ from the transcript.
Compute the grand product $z$ with $z(\omega^0) = 1$ and $z(\omega^{i+1}) = z(\omega^i) \cdot \frac{(a_i + \beta)(s_i + \gamma)}{(a'_i + \beta)(s'_i + \gamma)}$ .
Commit to $z$ .

3.4 The verifier

halo2_proofs/src/plonk/lookup/verifier.rs
use std::iter;

use super::super::{
    circuit::Expression, ChallengeBeta, ChallengeGamma, ChallengeTheta, ChallengeX,
};
use super::Argument;
use crate::{
    arithmetic::CurveAffine,
    plonk::{Error, VerifyingKey},
    poly::{multiopen::VerifierQuery, Rotation},
    transcript::{EncodedChallenge, TranscriptRead},
};
use ff::Field;

pub struct PermutationCommitments<C: CurveAffine> {
    permuted_input_commitment: C,
    permuted_table_commitment: C,
}

pub struct Committed<C: CurveAffine> {
    permuted: PermutationCommitments<C>,
    product_commitment: C,
}

pub struct Evaluated<C: CurveAffine> {
    committed: Committed<C>,
    product_eval: C::Scalar,
    product_next_eval: C::Scalar,
    permuted_input_eval: C::Scalar,
    permuted_input_inv_eval: C::Scalar,
    permuted_table_eval: C::Scalar,
}

impl<F: Field> Argument<F> {
    pub(in crate::plonk) fn read_permuted_commitments<
        C: CurveAffine,
        E: EncodedChallenge<C>,
        T: TranscriptRead<C, E>,
    >(
        &self,
        transcript: &mut T,
    ) -> Result<PermutationCommitments<C>, Error> {
        let permuted_input_commitment = transcript.read_point()?;
        let permuted_table_commitment = transcript.read_point()?;

        Ok(PermutationCommitments {
            permuted_input_commitment,
            permuted_table_commitment,
        })
    }
}

impl<C: CurveAffine> PermutationCommitments<C> {
    pub(in crate::plonk) fn read_product_commitment<
        E: EncodedChallenge<C>,
        T: TranscriptRead<C, E>,
    >(
        self,
        transcript: &mut T,
    ) -> Result<Committed<C>, Error> {
        let product_commitment = transcript.read_point()?;

        Ok(Committed {
            permuted: self,
            product_commitment,
        })
    }
}

impl<C: CurveAffine> Committed<C> {
    pub(crate) fn evaluate<E: EncodedChallenge<C>, T: TranscriptRead<C, E>>(
        self,
        transcript: &mut T,
    ) -> Result<Evaluated<C>, Error> {
        let product_eval = transcript.read_scalar()?;
        let product_next_eval = transcript.read_scalar()?;
        let permuted_input_eval = transcript.read_scalar()?;
        let permuted_input_inv_eval = transcript.read_scalar()?;
        let permuted_table_eval = transcript.read_scalar()?;

        Ok(Evaluated {
            committed: self,
            product_eval,
            product_next_eval,
            permuted_input_eval,
            permuted_input_inv_eval,
            permuted_table_eval,
        })
    }
}

impl<C: CurveAffine> Evaluated<C> {
    #[allow(clippy::too_many_arguments)]
    pub(in crate::plonk) fn expressions<'a>(
        &'a self,
        l_0: C::Scalar,
        l_last: C::Scalar,
        l_blind: C::Scalar,
        argument: &'a Argument<C::Scalar>,
        theta: ChallengeTheta<C>,
        beta: ChallengeBeta<C>,
        gamma: ChallengeGamma<C>,
        advice_evals: &[C::Scalar],
        fixed_evals: &[C::Scalar],
        instance_evals: &[C::Scalar],
    ) -> impl Iterator<Item = C::Scalar> + 'a {
        let active_rows = C::Scalar::ONE - (l_last + l_blind);

        let product_expression = || {
            // z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
            // - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
            let left = self.product_next_eval
                * &(self.permuted_input_eval + &*beta)
                * &(self.permuted_table_eval + &*gamma);

            let compress_expressions = |expressions: &[Expression<C::Scalar>]| {
                expressions
                    .iter()
                    .map(|expression| {
                        expression.evaluate(
                            &|scalar| scalar,
                            &|_| panic!("virtual selectors are removed during optimization"),
                            &|query| fixed_evals[query.index],
                            &|query| advice_evals[query.index],
                            &|query| instance_evals[query.index],
                            &|a| -a,
                            &|a, b| a + &b,
                            &|a, b| a * &b,
                            &|a, scalar| a * &scalar,
                        )
                    })
                    .fold(C::Scalar::ZERO, |acc, eval| acc * &*theta + &eval)
            };
            let right = self.product_eval
                * &(compress_expressions(&argument.input_expressions) + &*beta)
                * &(compress_expressions(&argument.table_expressions) + &*gamma);

            (left - &right) * &active_rows
        };

        std::iter::empty()
            .chain(
                // l_0(X) * (1 - z(X)) = 0
                Some(l_0 * &(C::Scalar::ONE - &self.product_eval)),
            )
            .chain(
                // l_last(X) * (z(X)^2 - z(X)) = 0
                Some(l_last * &(self.product_eval.square() - &self.product_eval)),
            )
            .chain(
                // (1 - (l_last(X) + l_blind(X))) * (
                //   z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
                //   - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta) (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
                // ) = 0
                Some(product_expression()),
            )
            .chain(Some(
                // l_0(X) * (a'(X) - s'(X)) = 0
                l_0 * &(self.permuted_input_eval - &self.permuted_table_eval),
            ))
            .chain(Some(
                // (1 - (l_last(X) + l_blind(X))) * (a′(X) − s′(X))⋅(a′(X) − a′(\omega^{-1} X)) = 0
                (self.permuted_input_eval - &self.permuted_table_eval)
                    * &(self.permuted_input_eval - &self.permuted_input_inv_eval)
                    * &active_rows,
            ))
    }

    pub(in crate::plonk) fn queries<'r, 'params: 'r>(
        &'r self,
        vk: &'r VerifyingKey<C>,
        x: ChallengeX<C>,
    ) -> impl Iterator<Item = VerifierQuery<'r, 'params, C>> + Clone {
        let x_inv = vk.domain.rotate_omega(*x, Rotation::prev());
        let x_next = vk.domain.rotate_omega(*x, Rotation::next());

        iter::empty()
            // Open lookup product commitment at x
            .chain(Some(VerifierQuery::new_commitment(
                &self.committed.product_commitment,
                *x,
                self.product_eval,
            )))
            // Open lookup input commitments at x
            .chain(Some(VerifierQuery::new_commitment(
                &self.committed.permuted.permuted_input_commitment,
                *x,
                self.permuted_input_eval,
            )))
            // Open lookup table commitments at x
            .chain(Some(VerifierQuery::new_commitment(
                &self.committed.permuted.permuted_table_commitment,
                *x,
                self.permuted_table_eval,
            )))
            // Open lookup input commitments at \omega^{-1} x
            .chain(Some(VerifierQuery::new_commitment(
                &self.committed.permuted.permuted_input_commitment,
                x_inv,
                self.permuted_input_inv_eval,
            )))
            // Open lookup product commitment at \omega x
            .chain(Some(VerifierQuery::new_commitment(
                &self.committed.product_commitment,
                x_next,
                self.product_next_eval,
            )))
    }
}

The verifier checks four identities at the challenge point $x$ :

$L_0(x) \cdot (1 - z(x)) = 0$ (boundary at $\omega^0$ ),
$L_{\text{last}}(x) \cdot (z(x)^2 - z(x)) = 0$ (boundary at $\omega^{n-1}$ ),
the main grand-product recurrence (the long expression from the comment in plonk/lookup.rs),
the two side constraints that pin $a'$ and $s'$ to the right permutation of $A$ and $S$ .

3.5 The dev tool's view

MockProver runs all four identities row by row in LagrangeCoeff without any commitment. If a circuit's lookup fails, MockProver reports a VerifyFailure::Lookup { lookup_index, location } (defined in halo2_proofs/src/dev/failure.rs) naming the offending row and the lookup index in declaration order.

4. Failure modes

Unpadded table column. A lookup table column with unfilled rows defaults its remaining cells to zero. If zero is not in the table semantically, the prover will fail to produce a valid $z$ for any row whose input is zero. The Layouter::assign_table API forces you to fill every row, but it is easy to bypass.
Reusing a TableColumn for something else. A column wrapped in TableColumn is encumbered for the lookup; trying to use it as a plain fixed column raises an error at keygen.
Forgetting that a complex selector is required. The lookup expression must not multiply two simple selectors. If you want to gate a lookup on a selector, use meta.complex_selector().
Order of (input, table) pairs. The pairs in the closure passed to meta.lookup(...) define the columns of the multi-column lookup. Permuting them changes the challenge $\theta$ 's effect; you cannot reorder them without changing the verifying key.

5. Spec pointers

Gabizon and Williamson, "plookup", eprint 2020/315.
The Halo 2 Book "Lookup argument" chapter reproduces the algebra of the comment block above with worked examples.
The Halo 2 Book "Lookup tables" chapter is a user-side walk-through.

6. Exercises

Open halo2_proofs/src/plonk/lookup.rs and read the doc comment of required_degree. Write down the four identities it enumerates in your own words.
Read the lookup chapter of the Halo 2 Book and identify each of the four identities in section 3.4 above with a numbered line in the comment block.
Open the SHA-256 table16 chip: halo2_gadgets/src/sha256/table16/spread_table.rs. Find the meta.lookup(...) call. What does the table contain and how many rows?
Trigger a lookup failure in MockProver. Take any test that uses lookup_range_check and modify the witness so that a value is out of range. Run the test and inspect the VerifyFailure::Lookup message.

Answers in the code

Exercise 1: the four identities are (i) $z(\omega^0) = 1$ , (ii) $z(\omega^{n-1}) \in \{0, 1\}$ , (iii) the grand-product recurrence, (iv) the boundary and step constraints on $(a', s')$ . All four are in the same comment.
Exercise 3: the spread table maps 16-bit dense values to their "spread" form (bits interleaved with zeros); it has $2^{16}$ rows.

7. Further reading

The original PLONK + plookup blog post.
Section "Plookup" of the Halo 2 design book.

1. Why this chapter exists​

2. Definitions​

3. The code​

3.1 The argument struct​

3.2 Declaring a lookup​

3.3 The prover​

3.4 The verifier​

3.5 The dev tool's view​

4. Failure modes​

5. Spec pointers​

6. Exercises​

Answers in the code​

7. Further reading​