# Sin7Y Tech Review (20): Halo2 Circuit Development
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](https://github.com/zcash/halo2), version f9b3ff2aef09a5a3cb5489d0e7e747e9523d2e6e. Before we begin, let’s review the most critical content, namely the circuit definition.
```rust=
// 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.
```rust=
// 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:
```rust=
// 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:
```rust=
// 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`:
```rust=
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.
```rust=
// 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:
```rust=
// 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.
```rust=
// 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.
```rust=
// 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`.
```rust=
// 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.
```rust=
// 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.
| Column 1 | Column 2 |
| -------- | -------- |
| 0x2 | |
| 0x3 | |
| 0x7 | |
| 0x2 | 0x3 |
| 0x6 | |
| 0x6 | 0x6 |
| 0x24 | |
| 0x7 | 0x24 |
| 0xfc | |
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
Sign in with Wallet
Connect another wallet