Halo2 Circuit Development: Sin7Y Tech Review (20)

In the previous article, we discussed how to use halo2 for circuit development. In this article, we will illustrate what we need to pay attention to when developing circuits. When writing this article, we referred to the halo2 code, version f9b3ff2aef09a5a3cb5489d0e7e747e9523d2e6e. Before we begin, let’s review the most critical content, namely the circuit definition.

// src/plonk/circuit.rs
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>;
}

As usual, when developing circuits, we need to implement this trait:

• Config
  • It defines the constraints of the circuit, mainly defined by the function create_gate().
• FloorPlanner
  • It is the floor planning strategy of the circuit, implementing the function synthesize(), which synthesizes the circuit using config, constants, and assignment provided.
• without_witnesses
  • It is the circuit without witnesses, typically using the function Self::default().
• configure
  • It is the process of develiping a description of the Gate Circuit and the constraints that apply to it.
• synthesize
  • It assigns a value to Layouter based on the config provided, and the core is using its function assin_region(), which uses closure and the parameter of the closure is Region.

As a result of the preceding definition, the halo2 circuit development consists of two critical functions: configure and synthesize. The former establishes the gate and defines the constraints, whereas the latter assigns witness and public data to the constraints.
Let’s take a closer look at what happens in detail during circuit development in this article. As a starting point, let’s use the official simple-example.

Configure

According to the declaration of the configure function, when defining a circuit, the ConstraintSystem will be modified and it will return to Config for later use.

// examples/simple-example.rs
fn MyCircuit::configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
    // We create the two advice columns that FieldChip uses for I/O.
    let advice = [meta.advice_column(), meta.advice_column()];

    // We also need an instance column to store public inputs.
    let instance = meta.instance_column();

    // Create a fixed column to load constants.
    let constant = meta.fixed_column();

    meta.enable_equality(instance);
    meta.enable_constant(constant);
    for column in &advice {
        meta.enable_equality(*column);
    }
    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_mul = meta.query_selector(s_mul);

        vec![s_mul * (lhs * rhs - out)]
    });

    FieldConfig {
        advice,
        instance,
        s_mul,
    }
}

Alright, let’s dive into it and analyze it. The configure did the following things:

1. Advice, instance, and fixed columns are created (for the purpose and significance of them, see the previous articles).
   • advice_column(), instance_column(), fixed_column() have the similar function, which is to create a corresponding type of column of advice / instance / fixed, add the count of the corresponding column in the ConstraintSystem by 1, and then return the new column.
2. Then the function enable_equality()of ConstraintSystem is called to put the columns instance and advice in and enable_constant()is then called to put constant in.
   • These two functions are used to enable the ability to enforce equality over cells in this column.
3. After that, the function selector is called to generate the selector.
4. Most importantly, the function create_gate of ConstraintSystem is called and a closure with &mut VirtualCells as the parameter is input in to create a gate.
   • In this closure, the function query_advice of VirtualCells is called. The advice column and selector generated above are input in, and column and rotation are used to construct the cell. At the same time, the expression with column and rotation as parameters is generated. Finally, the constraint dominated by expression is returned. It should be noted that the function query_advice() not only generates the cell but also puts the column and rotation into ConstraintSystem. In this way, the cell and cs are connected by column and rotation.
   • In the function create_gate, the constraints and cells generated in the closure are used to construct Gate and they are stored in the gates array of cs.
5. Finally, return to config for later use.

To sum up, first, create the corresponding column. Then, create the selector, and use the function create_ gate to generate cells and constraints from columns and selectors. Finally, the constraints and cells are used to generate gates which are saved in the end.

In a word, configure generates constraints.

Synthesize

The circuit is initialized through witness and public data. In the synthesize function, the data is input in. Since there are many structured codes in the official examples, we expand these codes in the synthesize function in this article, as follows:

// examples/simple-example.rs
fn synthesize(&self, config: Self::Config, layouter: impl Layouter<F>) -> Result<(), Error> {
    let a = layouter.assign_region(
        || "load a",
        |mut region| {
            region
            .assign_advice(
                || "private input",
                config.advice[0],
                0,
                || self.a.ok_or(Error::Synthesis),
            )
            .map(Number)
        },
    );
    let b = layouter.assign_region(
        || "load b",
        |mut region| {
            region
            .assign_advice(
                || "private input",
                config.advice[0],
                0,
                || self.b.ok_or(Error::Synthesis),
            )
            .map(Number)
        },
    );
    let constant = layouter.assign_region(
        || "load constant",
        |mut region| {
            region
            .assign_advice_from_constant(|| "constant value", config.advice[0], 0, self.constant)
            .map(Number)
        },
    );
    let ab = layouter.assign_region(
        || "a * b",
        |mut region: Region<'_, F>| {
            config.s_mul.enable(&mut region, 0)?;
            a.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
            b.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;

            let value = a.0.value().and_then(|a| b.0.value().map(|b| *a * *b));
            region
            .assign_advice(
                || "lhs * rhs",
                config.advice[0],
                1,
                || value.ok_or(Error::Synthesis),
            )
            .map(Number)
        },
    );
    let ab2 = ab.clone();
    let absq = layouter.assign_region(
        || "ab * ab",
        |mut region: Region<'_, F>| {
            config.s_mul.enable(&mut region, 0)?;
            ab.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
            ab2.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;

            let value = ab.0.value().and_then(|a| ab2.0.value().map(|b| *a * *b));
            region
            .assign_advice(
                || "lhs * rhs",
                config.advice[0],
                1,
                || value.ok_or(Error::Synthesis),
            )
            .map(Number)
        },
    );
    let c = layouter.assign_region(
        || "constant * absq",
        |mut region: Region<'_, F>| {
            config.s_mul.enable(&mut region, 0)?;
            constant.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
            absq.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;

            let value = constant.0.value().and_then(|a| absq.0.value().map(|b| *a * *b));
            region
            .assign_advice(
                || "lhs * rhs",
                config.advice[0],
                1,
                || value.ok_or(Error::Synthesis),
            )
            .map(Number)
        },
    );
    
    layouter.constrain_instance(c.0.cell(), config.instance, 0)
}

Let’s begin by examining the code that uses a, b, and constants to specify parameters. assign_region is a Layouter trait function. Prior to delving into this function, let’s examine the Layouter trait.

Layouter

Layouter is chip-agnostic. As mentioned previously in our guide to Halo 2 development, the chip is the heart of any circuit. As a result, it makes no difference to the layouter what the chip is used for or how it is defined. That is, the layouter and the chip are not connected. The layout is an abstract strategy trait that circuits assign a value to. What does this imply? That is, the layouter is used to assign circuits, such as row indices.

It is defined as follows:

// src/circuit.rs
pub trait Layouter<F: Field> {
    type Root: Layouter<F>;

    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>;

    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>;

    fn constrain_instance(
        &mut self,
        cell: Cell,
        column: Column<Instance>,
        row: usize,
    ) -> Result<(), Error>;

    fn get_root(&mut self) -> &mut Self::Root;

    fn push_namespace<NR, N>(&mut self, name_fn: N)
    where
        NR: Into<String>,
        N: FnOnce() -> NR;

    fn pop_namespace(&mut self, gadget_name: Option<String>);

    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)
    }
}

Let’s examine each function in turn:

• Let’s begin with the simplest, root/namespace-related functions. These namespace-related functions are used to identify the current layout.
• The function constrain_instance is used to constrain the row value of an instance column in a cell and an absolute position.
• The core functions are assign_region and assign_table, which, as their names imply, are used to assign regions and tables, respectively. This is also the trait’s primary function. The layouter trait is used to associate values with regions and tables. We shall discuss them afterwards.

Let’s investigate the function assign_region. This function receives a closure of string and FnMut(Region<'_, F>) -> Result<AR, Error>, and contains &mut self. Let’s examine the definition of this important Region:

pub struct Region<'r, F: Field> {
    region: &'r mut dyn layouter::RegionLayouter<F>,
}

It can be seen that Region is an encapsulation for RegionLayouter, which is a Layouter for Region. Before introducing RegionLayouter, we should avoid going into too many details. Let’s take a look at the specific case of Layouter. In the simple example, SingleChipLayouter implements Layouter trait.

// src/circuit/floor_planner/single_pass.rs
pub struct SingleChipLayouter<'a, F: Field, CS: Assignment<F> + 'a> {
    cs: &'a mut CS,
    constants: Vec<Column<Fixed>>,
    /// Stores the starting row for each region.
    regions: Vec<RegionStart>,
    /// Stores the first empty row for each column.
    columns: HashMap<RegionColumn, usize>,
    /// Stores the table fixed columns.
    table_columns: Vec<TableColumn>,
    _marker: PhantomData<F>,
}

fn SingleChipLayouter::assign_region<A, AR, N, NR>(&mut self, name: N, mut assignment: A) -> Result<AR, Error>
where
    A: FnMut(Region<'_, F>) -> Result<AR, Error>,
    N: Fn() -> NR,
    NR: Into<String>,
{
    let region_index = self.regions.len();

    // 1. Get shape of the region.
    let mut shape = RegionShape::new(region_index.into());
    {
        let region: &mut dyn RegionLayouter<F> = &mut shape;
        assignment(region.into())?;
    }

    // 2. Lay out this region. We implement the simplest approach here: position the
    // region starting at the earliest row for which none of the columns are in use.
    let mut region_start = 0;
    for column in &shape.columns {
        region_start = cmp::max(region_start, self.columns.get(column).cloned().unwrap_or(0));
    }
    self.regions.push(region_start.into());

    // Update column usage information.
    for column in shape.columns {
        self.columns.insert(column, region_start + shape.row_count);
    }

    // 3. Assign region cells.
    self.cs.enter_region(name);
    let mut region = SingleChipLayouterRegion::new(self, region_index.into());
    let result = {
        let region: &mut dyn RegionLayouter<F> = &mut region;
        assignment(region.into())
    }?;
    let constants_to_assign = region.constants;
    self.cs.exit_region();

    // 4. Assign constants. For the simple floor planner, we assign constants in order in
    // the first `constants` column.
    if self.constants.is_empty() {
        if !constants_to_assign.is_empty() {
            return Err(Error::NotEnoughColumnsForConstants);
        }
    } else {
        let constants_column = self.constants[0];
        let next_constant_row = self
            .columns
            .entry(Column::<Any>::from(constants_column).into())
            .or_default();
        for (constant, advice) in constants_to_assign {
            self.cs.assign_fixed(
                || format!("Constant({:?})", constant.evaluate()),
                constants_column,
                *next_constant_row,
                || Ok(constant),
            )?;
            self.cs.copy(
                constants_column.into(),
                *next_constant_row,
                advice.column,
                *self.regions[*advice.region_index] + advice.row_offset,
            )?;
            *next_constant_row += 1;
        }
    }

    Ok(result)
}

As described in the preceding code and comments, the assign_region functions of SingleChipLayouter accomplished the following:

1. Grasp the number of regions of the current SingleChipLayouter to construct a RegionShape, and input this RegionShape into the closure. At this point, execute the closure and RegionShape will be modified.
   • Take a look at this closure. It calls the function assign_advice of the region with the input the mut region:

// src/circuit.rs
pub fn Region::assign_advice<'v, V, VR, A, AR>(
    &'v mut self,
    annotation: A,
    column: Column<Advice>,
    offset: usize,
    mut to: V,
) -> Result<AssignedCell<VR, F>, Error>
where
    V: FnMut() -> Result<VR, Error> + 'v,
    for<'vr> Assigned<F>: From<&'vr VR>,
    A: Fn() -> AR,
    AR: Into<String>,
{
    let mut value = None;
    let cell =
        self.region
            .assign_advice(&|| annotation().into(), column, offset, &mut || {
                let v = to()?;
                let value_f = (&v).into();
                value = Some(v);
                Ok(value_f)
            })?;

    Ok(AssignedCell {
        value,
        cell,
        _marker: PhantomData,
    })
}

This function internally will call assign_advice of RegionLayouter. The above RegionShape implements RegionLayouter trait, so the function assign_advice of RegionShape is employed in the end.

// src/circuit/layouter.rs
fn RegionShape::assign_advice<'v>(
    &'v mut self,
    _: &'v (dyn Fn() -> String + 'v),
    column: Column<Advice>,
    offset: usize,
    _to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
) -> Result<Cell, Error> {
    self.columns.insert(Column::<Any>::from(column).into());
    self.row_count = cmp::max(self.row_count, offset + 1);

    Ok(Cell {
        region_index: self.region_index,
        row_offset: offset,
        column: column.into(),
    })
}

At this point, RegionShape will record the column, config advice [0], and compare offset+1 and row count, updating row count.

2. Compare all columns in RegionShape, locate and update the column and region start values in SingleChipLayouter.

   
   

3. Assign values to region cells to create a SingleChipLayouterRegion that will be turned to a RegionLayouter, and then call the closure function. The only modification from step 1 is the implementation of the SingleChipLayouterRegion’s assign_advice function.

// src/circuit/floor_planner/single_pass.rs
fn SingleChipLayouterRegion::assign_advice<'v>(
    &'v mut self,
    annotation: &'v (dyn Fn() -> String + 'v),
    column: Column<Advice>,
    offset: usize,
    to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
) -> Result<Cell, Error> {
    self.layouter.cs.assign_advice(
        annotation,
        column,
        *self.layouter.regions[*self.region_index] + offset,
        to,
    )?;

    Ok(Cell {
        region_index: self.region_index,
        row_offset: offset,
        column: column.into(),
    })
}

It can be seen in this function, the function assign_advice of Assignment in SingleChipLayouter is adopted. In this example, the Assignment trait is implemented by MockProver.

// src/dev.rs
fn MockProver::assign_advice<V, VR, A, AR>(
    &mut self,
    _: A,
    column: Column<Advice>,
    row: usize,
    to: V,
) -> Result<(), Error>
where
    V: FnOnce() -> Result<VR, Error>,
    VR: Into<Assigned<F>>,
    A: FnOnce() -> AR,
    AR: Into<String>,
{
    if !self.usable_rows.contains(&row) {
        return Err(Error::not_enough_rows_available(self.k));
    }

    if let Some(region) = self.current_region.as_mut() {
        region.update_extent(column.into(), row);
        region.cells.push((column.into(), row));
    }

    *self
        .advice
        .get_mut(column.index())
        .and_then(|v| v.get_mut(row))
        .ok_or(Error::BoundsFailure)? = CellValue::Assigned(to()?.into().evaluate());

    Ok(())
}

It will determine whether the row in this region exceeds the number of available rows. Then current_region will be modified. The columns and rows used are written into the region. And the value of the corresponding column/row in advice is changed into to. Therefore, it is MockProver that stores advice data. The constraintsystem previously used in configure is also a field of MockProver. In short, MockProver links configure to synthesize.

For circuit developers, what matters is how to build and develop efficient and safe circuits, with little regard for fundamental circuit architecture. What we want to know is how to build columns and rows, as well as how to make gates in the configure phase. Also, whether to assign values to columns and rows in sequence in the synthesize phase.

The following changes are made to the example code.

// simple-example.rs
fn main() {
    ...
    let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
    println!("{:?}", prover);
    // assert_eq!(prover.verify(), Ok(()));
    ...
}

In this way, MockProver can be printed, and the result of the advice is as follows.

advice: [
        [Assigned(0x0000000000000000000000000000000000000000000000000000000000000002), Assigned(0x0000000000000000000000000000000000000000000000000000000000000003), Assigned(0x0000000000000000000000000000000000000000000000000000000000000007), Assigned(0x0000000000000000000000000000000000000000000000000000000000000002), Assigned(0x0000000000000000000000000000000000000000000000000000000000000006), Assigned(0x0000000000000000000000000000000000000000000000000000000000000006), Assigned(0x0000000000000000000000000000000000000000000000000000000000000024), Assigned(0x0000000000000000000000000000000000000000000000000000000000000007), Assigned(0x00000000000000000000000000000000000000000000000000000000000000fc), Unassigned, Poison(10), Poison(11), Poison(12), Poison(13), Poison(14), Poison(15)
        ],
        [Unassigned, Unassigned, Unassigned, Assigned(0x0000000000000000000000000000000000000000000000000000000000000003), Unassigned, Assigned(0x0000000000000000000000000000000000000000000000000000000000000006), Unassigned, Assigned(0x0000000000000000000000000000000000000000000000000000000000000024), Unassigned, Unassigned, Poison(10), Poison(11), Poison(12), Poison(13), Poison(14), Poison(15)
        ]
    ]

As you can see, there are two columns in the advice, which can be visualized as follows.

Line 1 to line 3 are all load private/load constant data, which are put in the first column. In line 4, call mul, get the data from the first column and the second column of the row, and save the calculation result in the first column of the next row, that is, row 5. The following are similar mul calculations.

Finally, constrain_instance is used to constraint the calculation result with the instance column to check whether the calculated 0xfc is equal to the public input.

We can see that the result of instance in MockProver is:

instance: [
        [
            0x00000000000000000000000000000000000000000000000000000000000000fc,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000,
            0x0000000000000000000000000000000000000000000000000000000000000000
        ]
    ]

References

Halo2 repo – https://github.com/zcash/halo2
Halo2 book –https://zcash.github.io/halo2
Halo2 book Chinese –https://trapdoor-tech.github.io/halo2-book-chinese