Chapter 1: Endless Spreadsheets

Less circuit, more Excel.

Configuration

To get going, we start by adding two columns to the circuit during configuration:

#![allow(unused)]
fn main() {
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let q_enable = meta.complex_selector();
        let advice = meta.advice_column();
}

Each column comes along with a type, in the case above:

  • advice: an "advice" column which the prover can assign values to freely.
  • q_enable: a "selector" column, used to turn gates on and off.
    It contains constants (that the prover can't change).

This can be visualized as a "spreadsheet" with two columns (and an infinite number of rows):

The circuit is defined by fixing certain cells in this "spreadsheet" and the prover gets to fill in the rest of the spreadsheet. If we stop here, we have a spreadsheet where:

  • The first column is completely unconstrained.
  • The second column is a column of constant zeros.

For this to do anything useful, we need to define some gates. Gates in Halo2 is kind of a misnomer - it's more useful to think of them as constraints over the cells in this "spreadsheet": to enforce relationships between the cells (e.g. constraint the first column).

So here is a very simple example of a gate:

#![allow(unused)]
fn main() {
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let q_enable = meta.complex_selector();
        let advice = meta.advice_column();

        // define a new gate:
        // next = curr + 1 if q_enable is 1
        meta.create_gate("step", |meta| {
            let curr = meta.query_advice(advice, Rotation::cur());
            let next = meta.query_advice(advice, Rotation::next());
            let q_enable = meta.query_selector(q_enable);
            vec![q_enable * (curr - next + Expression::Constant(F::ONE))]
        });
}

This enforces a global constraint on the cells in the spreadsheet, i.e. every row of the spreadsheet:

  • The advice cell in the current row: meta.query_advice(advice, Rotation::cur())
  • Minus the advice cell in the next row: meta.query_advice(advice, Rotation::next())
  • Plus one: Expression::Constant(F::ONE)
  • Times the q_enable "selector": meta.query_selector(q_enable)

Must be zero. Like this:

In other words:

  • If q_enable = 1, then next = curr + 1.
  • If q_enable = 0, then next can be anything.

This is why we need "selector" columns: to turn gates off.

If we did not multiply by a selector (e.g. q_enable) the gate would always be on and the prover would have to satisfy every gate for every row. By turning selectors on/off we can "program" the spreadsheet to enforce different constraints over different rows -- that's the job of the synthesize step in Halo2. Observe that at the next row, the current row is the next row of the previous row:

This means that enabling this gate over a sequence of rows will enforce that the advice column contains a sequence (e, e+1, e+2, ...).

We will do that in the next section.

Note

Key takeaway: the goal of "configuration" is to define this spreadsheet and the gates (constraints) that act on it. The goal of synthesis will be to fill in the spreadsheet.

Info

The ability to refer to the "next" cell in a column is readily applied in Halo2 circuit design, when the same function needs to be applied over and over again to an input. A classical example is a hash function where the gate might constrain a single round of the hash function.

Synthesize

Creating Regions

A set of consecutive rows are called a region in Halo2. The way they work is as follows:

  1. You ask Halo2 to create a region.
  2. You can then refer to the cells in the region relative to its start.

Creating regions and assigning cells in them is exactly the job of the synthesize step in Halo2. The smallest possible region is a single row, the largest is the entire spreadsheet. In this example, we will have just a single region. We create this region using layouter.assign_region.

    fn synthesize(
        &self,
        config: Self::Config, //
        mut layouter: impl Layouter<F>,
    ) -> Result<(), Error> {
        layouter.assign_region(
            || "steps",
            |mut region| {

A couple of natural questions about regions:

Why does Halo2 need regions?

For usability.

In fact, you could create your circuit by just having a single giant region which contains the entire spreadsheet. However, this would be very cumbersome to work with, you would have to refer to cells by their absolute position in the spreadsheet and manage all the indexing yourself. With regions, you can break the spreadsheet into smaller logical pieces, reuse them and give them names for easier debugging etc.

How does Halo2 know where in the spreadsheet the region is?

That's easy actually: Halo2 (more specifically the "layouter") decides that for you. You can only refer to cells in the region relative to the region's start, which means Halo2 may place the "region" (some subset of rows) anywhere in the spreadsheet.

In practice, it will place the region starting at the next available row in the spreadsheet.

How does Halo2 know how many rows are in the region?

It figures it out automatically: the number of rows in the region is the largest relative offset you use in the region. i.e. if you refer to the 5th row in a region, Halo2 knows that the region has at least 5 rows.

Can regions be next to each other?

Yes, assuming they don't use the same columns.

Assigning Cells in a Region

We now have a region.

Time to occupy the cells in it, but first: where should the values come from? i.e. where do we get the values that the prover should fill the advice column with? In other ZK-words, where is the witness?

We feed the witness into synthesize by adding a member to the circuit struct:

struct TestCircuit<F: Field> {
    _ph: PhantomData<F>,
    values: Value<Vec<F>>,
}

A natural question arises: what the heck is a Value?

What is a Value?

A Value<T> is a glorified Option<T>, nothing more.

It exists to contain values that only the prover knows (the witness), i.e.

  • For the verifier the Value is Value::unknown()
  • For the prover it is Value::known(some_witness).

When creating a proof you assign the Values in the circuit struct with the witness and run synthesis. Synthesis then assigns the values in the spreadsheet according to the Values in the circuit struct.

In the case above, the Value contains the witness for the advice column: some vector of field elements. Naturally we must update the without_witnesses function from the circuit to return a Value::unknown():

impl<F: Field> Circuit<F> for TestCircuit<F> {
    type Config = TestConfig<F>;
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self {
        TestCircuit {
            _ph: PhantomData,
            values: Value::unknown(),
        }
    }

Okay back to filling out our new region, this looks as follows:

    fn synthesize(
        &self,
        config: Self::Config, //
        mut layouter: impl Layouter<F>,
    ) -> Result<(), Error> {
        layouter.assign_region(
            || "steps",
            |mut region| {
                // apply the "step" gate STEPS = 5 times
                for i in 0..STEPS {
                    // assign the witness value to the advice column
                    region.assign_advice(
                        || "assign advice",
                        config.advice,
                        i,
                        || self.values.as_ref().map(|values| values[i]),
                    )?;

                    // turn on the gate
                    config.q_enable.enable(&mut region, i)?;
                }

                // assign the final "next" value
                region.assign_advice(
                    || "assign advice",
                    config.advice,
                    STEPS,
                    || self.values.as_ref().map(|values| values[STEPS]),
                )?;

                Ok(())
            },
        )?;
        Ok(())
    }

If we assume that:

self.values = Value::known(vec![1, 2, 3, 4, 5, 6])

The assignment is as follows:

Exercises

The full code is at the end.

Exercise

Exercise:

  • Implement the main function to create a (valid) TestCircuit instance
  • Call prove on the TestCircuit instance.

Exercise

Exercise:

  • Try filling in an invalid value in the advice column: e.g. [1, 2, 3, 4, 5, 5].
  • Does it fail?

Exercise

Exercise:

Create a circuit which computes the Fibonacci sequence, i.e. enforces next = curr + prev.

  • Add a Fibonacci gate or change the existing gate to enforce this relation.
  • Create valid witness assignments for the circuit: change how values is assigned in the TestCircuit struct.

Hint

You can access the previous row in a region by using Rotation::prev().

use std::marker::PhantomData;

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

use ff::Field;

const STEPS: usize = 5;

struct TestCircuit<F: Field> {
    _ph: PhantomData<F>,
    values: Value<Vec<F>>,
}

#[derive(Clone, Debug)]
struct TestConfig<F: Field + Clone> {
    _ph: PhantomData<F>,
    q_enable: Selector,
    advice: Column<Advice>,
}

impl<F: Field> Circuit<F> for TestCircuit<F> {
    type Config = TestConfig<F>;
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self {
        TestCircuit {
            _ph: PhantomData,
            values: Value::unknown(),
        }
    }

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let q_enable = meta.complex_selector();
        let advice = meta.advice_column();

        // define a new gate:
        // next = curr + 1 if q_enable is 1
        meta.create_gate("step", |meta| {
            let curr = meta.query_advice(advice, Rotation::cur());
            let next = meta.query_advice(advice, Rotation::next());
            let q_enable = meta.query_selector(q_enable);
            vec![q_enable * (curr - next + Expression::Constant(F::ONE))]
        });

        TestConfig {
            _ph: PhantomData,
            q_enable,
            advice,
        }
    }

    fn synthesize(
        &self,
        config: Self::Config, //
        mut layouter: impl Layouter<F>,
    ) -> Result<(), Error> {
        layouter.assign_region(
            || "steps",
            |mut region| {
                // apply the "step" gate STEPS = 5 times
                for i in 0..STEPS {
                    // assign the witness value to the advice column
                    region.assign_advice(
                        || "assign advice",
                        config.advice,
                        i,
                        || self.values.as_ref().map(|values| values[i]),
                    )?;

                    // turn on the gate
                    config.q_enable.enable(&mut region, i)?;
                }

                // assign the final "next" value
                region.assign_advice(
                    || "assign advice",
                    config.advice,
                    STEPS,
                    || self.values.as_ref().map(|values| values[STEPS]),
                )?;

                Ok(())
            },
        )?;
        Ok(())
    }
}