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 , version f9b3ff2aef09a5a3cb5489d0e7e747e9523d2e6e. Before we begin, let’s review the most critical content, namely the circuit definition. halo2 code // src/plonk/circuit.rs pub trait Circuit { type Config: Clone; type FloorPlanner: FloorPlanner; fn without_witnesses(&self) -> Self; fn configure(meta: &mut ConstraintSystem ) -> Self::Config; fn synthesize(&self, config: Self::Config, layouter: impl Layouter ) -> Result ; } 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 , which synthesizes the circuit using config, constants, and assignment provided. synthesize() 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 based on the config provided, and the core is using its function , which uses closure and the parameter of the closure is Region. Layouter assin_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 function, when defining a circuit, the will be modified and it will return to for later use. configure ConstraintSystem Config // examples/simple-example.rs fn MyCircuit::configure(meta: &mut ConstraintSystem ) -> 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 did the following things: configure , , and columns are created (for the purpose and significance of them, see the previous articles). Advice instance fixed , , 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 by 1, and then return the new column. advice_column() instance_column() fixed_column() ConstraintSystem Then the function of is called to put the columns and in and is then called to put in. enable_equality() ConstraintSystem instance advice enable_constant() constant These two functions are used to enable the ability to enforce equality over cells in this column. After that, the function is called to generate the selector. selector Most importantly, the function of is called and a closure with as the parameter is input in to create a gate. create_gate ConstraintSystem &mut VirtualCells In this closure, the function of 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 not only generates the cell but also puts the column and rotation into . In this way, the cell and cs are connected by column and rotation. query_advice VirtualCells query_advice() ConstraintSystem In the function , the constraints and cells generated in the closure are used to construct and they are stored in the gates array of cs. create_gate Gate 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 ) -> Result { 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 | { 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 | { 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 | { 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. is a trait function. Prior to delving into this function, let’s examine the trait. assign_region Layouter Layouter Layouter is . 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. Layouter chip-agnostic It is defined as follows: // src/circuit.rs pub trait Layouter { type Root: Layouter ; fn assign_region (&mut self, name: N, assignment: A) -> Result where A: FnMut(Region ) -> Result , N: Fn() -> NR, NR: Into ; fn assign_table (&mut self, name: N, assignment: A) -> Result where A: FnMut(Table ) -> Result , N: Fn() -> NR, NR: Into ; fn constrain_instance( &mut self, cell: Cell, column: Column , row: usize, ) -> Result ; fn get_root(&mut self) -> &mut Self::Root; fn push_namespace (&mut self, name_fn: N) where NR: Into , N: FnOnce() -> NR; fn pop_namespace(&mut self, gadget_name: Option ); fn namespace (&mut self, name_fn: N) -> NamespacedLayouter where NR: Into , 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 is used to constrain the row value of an instance column in a and an absolute position. constrain_instance cell The core functions are and , 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. assign_region assign_table Let’s investigate the function . This function receives a closure of and , and contains . Let’s examine the definition of this important : assign_region string FnMut(Region ) -> Result &mut self Region pub struct Region { region: &'r mut dyn layouter::RegionLayouter , } 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 . In the , implements trait. Layouter simple example SingleChipLayouter Layouter // src/circuit/floor_planner/single_pass.rs pub struct SingleChipLayouter + 'a> { cs: &'a mut CS, constants: Vec >, /// Stores the starting row for each region. regions: Vec , /// Stores the first empty row for each column. columns: HashMap , /// Stores the table fixed columns. table_columns: Vec , _marker: PhantomData , } fn SingleChipLayouter::assign_region (&mut self, name: N, mut assignment: A) -> Result where A: FnMut(Region ) -> Result , N: Fn() -> NR, NR: Into , { 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 = &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 = &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:: ::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 functions of accomplished the following: assign_region SingleChipLayouter Grasp the number of regions of the current to construct a , and input this into the closure. At this point, execute the closure and will be modified. SingleChipLayouter RegionShape RegionShape RegionShape Take a look at this closure. It calls the function of the region with the input the mut region: assign_advice // src/circuit.rs pub fn Region::assign_advice ( &'v mut self, annotation: A, column: Column , offset: usize, mut to: V, ) -> Result , Error> where V: FnMut() -> Result + 'v, for Assigned : From , A: Fn() -> AR, AR: Into , { 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 of . The above implements trait, so the function of is employed in the end. assign_advice RegionLayouter RegionShape RegionLayouter assign_advice RegionShape // src/circuit/layouter.rs fn RegionShape::assign_advice ( &'v mut self, _: &'v (dyn Fn() -> String + 'v), column: Column , offset: usize, _to: &'v mut (dyn FnMut() -> Result , Error> + 'v), ) -> Result { self.columns.insert(Column:: ::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. Compare all columns in RegionShape, locate and update the column and region start values in SingleChipLayouter. Assign values to region cells to create a that will be turned to a , and then call the closure function. The only modification from step 1 is the implementation of the ’s function. SingleChipLayouterRegion RegionLayouter SingleChipLayouterRegion assign_advice // src/circuit/floor_planner/single_pass.rs fn SingleChipLayouterRegion::assign_advice ( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), column: Column , offset: usize, to: &'v mut (dyn FnMut() -> Result , Error> + 'v), ) -> Result { 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 of in is adopted. In this example, the trait is implemented by . assign_advice Assignment SingleChipLayouter Assignment MockProver // src/dev.rs fn MockProver::assign_advice ( &mut self, _: A, column: Column , row: usize, to: V, ) -> Result where V: FnOnce() -> Result , VR: Into >, A: FnOnce() -> AR, AR: Into , { 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 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 . Therefore, it is MockProver that stores advice data. The constraintsystem previously used in is also a field of MockProver. current_region to configure 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, is used to constraint the calculation result with the instance column to check whether the calculated 0xfc is equal to the public input. constrain_instance 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 – Halo2 book – Halo2 book Chinese – https://github.com/zcash/halo2 https://zcash.github.io/halo2 https://trapdoor-tech.github.io/halo2-book-chinese