Halo2电路构建源代码导读

区块链技术 4 4 月 22, 2024 0 区块链315

理解Halo2，可以从两部分着手：1/ 电路构建 2/ 证明系统。从开发者的角度看，电路构建是接口。如何通过Halo2构建建电路，这些电路在Halo2的内部如何表示是理解电路构建的关键。本文就从源代码的角度深入浅出讲解Halo2的电路构建。

写在前面

在深入理解Halo2电路或者证明系统之前，请仔细查看Halo2的文档：

https://zcash.github.io/halo2/index.html

对应的中文翻译文档：

https://trapdoor-tech.github.io/halo2-book-chinese/

源代码目录结构

Halo2的源代码下载地址：

https://github.com/zcash/halo2.git

本文中采用的源代码的最后一个提交信息如下：

commit 658c2db4217b1b19b17ecd29577c0e370e1c4997Merge: 3850b9c b46ef35Author: str4d Date: Sat Oct 2 01:54:55 2021 +1300 Merge pull request #374 from zcash/trait-usage Clean up our trait usage

Halo2的目录结构如下：

主要逻辑在src目录下。benches是基准测试程序。book是Halo2的描述文档。examples目录下提供了简单电路示例。

电路结构

在深入Halo2电路细节之前，先介绍一下Halo2的整体的电路结构。Halo2和PLONK/Groth16的电路结构有一些区别。简单的说，PLONK/Groth16约束系统由一条条相对独立的约束组成（约束只能约束该行上的变量），并且一条约束指定了支持的计算（乘法或者加法组合）。Halo2的约束系统中的约束并不限定在一行上的变量，并且采用“custom gate”，任意指定约束需要的计算。

整体电路结构如下：

电路由列（Column）和行（Row）组成。列又分为三种类型：advice，instance和selector。列的类型定义在src/plonk/circuit.rs中。

pub enum Any { Advice, Fixed, Instance,}

Advice列是witness信息，Instance列是public信息。Selector列，也是Fixed列，是选择子，可以选择某些约束开启或者关闭。为了更好的电路模块化，电路构建往往是相对于一个Region。同一个电路模块，可以在不同的Region中“复制”。

Cell定义在src/circuit.rs：

pub struct Cell { region_index: RegionIndex, row_offset: usize, column: Column}

Cell指定在一个Region中的某行某列。

几个术语

理解Halo2的电路构建，可以从一个简单的例子开始：examples/simple-example.rs。理解这个例子前，需要介绍几个术语。

Chip

电路由一个个Chip逻辑堆砌而成。每个Chip的创建从“Config”开始。

Config

所谓的Config，就是申请Chip需要的Column以及配置Fixed列的逻辑含义。这些配置可能是Custom Gate，可能是lookup。

Instructions

每一个Chip都有指令（Instruction）。通过指令的调用，将Chip的部分或者全部功能加入电路中。

Layouter

将Chip添加到一个电路上需要布局。Layouter就是用来实现布局。Layouter接口定义在src/circuit.rs中：

pub trait Layouter type Root: Layouter fn assign_region where A: FnMut(Region<'_, F>) -> Result N: Fn() -> NR, NR: Into fn assign_table where A: FnMut(Table<'_, F>) -> Result<(), Error>, N: Fn() -> NR, NR: Into fn constrain_instance( &mut self, cell: Cell, column: Column row: usize, ) -> Result<(), Error>; fn get_root(&mut self) -> &mut Self::Root; fn push_namespace where NR: Into N: FnOnce() -> NR; fn pop_namespace(&mut self, gadget_name: Option fn namespace where NR: Into N: FnOnce() -> NR, { self.get_root().push_namespace(name_fn); NamespacedLayouter(self.get_root(), PhantomData) }}

{

;

(&mut self, name: N, assignment: A) -> Result

;

(&mut self, name: N, assignment: A) -> Result<(), Error>

;

(&mut self, name_fn: N)

);

(&mut self, name_fn: N) -> NamespacedLayouter<'_, F, Self::Root>

Layouter本身存在层级关系，所以Layouter的接口定义了get_root/push_namespace/pop_namespace/namespace相关的函数。核心逻辑在其他三个函数：

assign_region - 获取一个region，在这个region上可以进行各种“assignment”，定义在RegionLayouter接口中。
assign_table - 获取一个table，并设置table，接口定义在TableLayouter接口中。
constrain_instance - 限制一个Cell和Instance列中的某个Cell一致。

Assignment

Assignment是一个电路“赋值”的接口，定义在src/plonk/circuit.rs：

pub trait Assignment fn enter_region where NR: Into N: FnOnce() -> NR; fn exit_region(&mut self); fn enable_selector &mut self, annotation: A, selector: &Selector, row: usize, ) -> Result<(), Error> where A: FnOnce() -> AR, AR: Into fn query_instance(&self, column: Column fn assign_advice &mut self, annotation: A, column: Column row: usize, to: V, ) -> Result<(), Error> where V: FnOnce() -> Result VR: Into A: FnOnce() -> AR, AR: Into fn assign_fixed &mut self, annotation: A, column: Column row: usize, to: V, ) -> Result<(), Error> where V: FnOnce() -> Result VR: Into A: FnOnce() -> AR, AR: Into fn copy( &mut self, left_column: Column left_row: usize, right_column: Column right_row: usize, ) -> Result<(), Error>; fn fill_from_row( &mut self, column: Column row: usize, to: Option ) -> Result<(), Error>; fn push_namespace where NR: Into N: FnOnce() -> NR; fn pop_namespace(&mut self, gadget_name: Option}

{

(&mut self, name_fn: N)

(

;

, row: usize) -> Result

, Error>;

(

;

(

;

(&mut self, name_fn: N)

);

电路内部框架

为了方便简化开发人员开发电路，Halo2的内部框架抽象了布局的接口（以SimpleFloorPlanner为例）：

目前有两套Layouter的实现：1/ SimpleFloorPlanner 2/ V1/V1Plan。为了方便理解Halo2的内部逻辑，详细讲解一下SimpleFloorPlanner。整个框架由四个接口组成：FloorPlanner，Layouter，RegionLayout/TableLayout以及Assignment。

简单的说，一个FloorPlanner拥有一个Layouter，一个Layouter可以分配多个RegionLayout或者TableLayout。电路对Cell的assignment都是通过Assignment实现。

先从三者的整体调用关系讲起：

SimpleFloorPlanner是对FloorPlanner接口的实现，定义在src/circuit/floor_planner/single_pass.rs中：
pub struct SimpleFloorPlanner;impl FloorPlanner for SimpleFloorPlanner { fn synthesize cs: &mut CS, circuit: &C, config: C::Config, constants: Vec ) -> Result<(), Error> { let layouter = SingleChipLayouter::new(cs, constants)?; circuit.synthesize(config, layouter) }}
, C: Circuit
>(
>,
SimpleFloorPlanner实现了FloorPlanner接口的synthesize函数。容易看出，该函数创建出SingleChipLayouter对象，并直接调用相应的synthesize函数开始电路的synthesize。
SingleChipLayouter定义在src/circuit/floor_planner/single_pass.rs中，包括了电路的所有的信息。
pub struct SingleChipLayouter<'a, F: Field, CS: Assignment 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}
+ 'a> {
>,
,
,
,
,
SingleChipLayouter的Region管理比较简单，某行整体属于某个Region。regions记录每个Region的行的开始偏移。cs是Assignment接口的实现，存储所有电路的赋值信息。columns记录当前操作RegionColumn对应的空的row的偏移。table_columns记录Table需要的Fixed的Column。简单的说，SingleChipLayouter记录了电路（包括布局）需要的所有信息。
SingleChipLayouter's assign_region 函数实现一个Region的synthesize过程。简单的说，SingleChipLayouter的assign_region函数的主要逻辑就是创建一个region，并将region内的布局转化为全局布局。SingleChipLayouter的assign_region逻辑可以分成两部分：
1/ 通过RegionShape获取Region的“形状”。所谓的“形状”，包括主要是采用的Column的信息。
2/ 根据上一步获取的Column信息，找出和其他Region不冲突的起始问题。
可以查看代码中的注释理解相应逻辑：
fn assign_regionwhere A: FnMut(Region<'_, F>) -> Result N: Fn() -> NR, NR: Into{ let region_index = self.regions.len(); //获取当前Region的编号 // Get shape of the region. //调用RegionShape的Region接口，收集该Region的电路涉及到的Column信息 let mut shape = RegionShape::new(region_index.into()); { let region: &mut dyn RegionLayouter assignment(region.into())?; } // 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; //根据收集到的Column信息，获取Region开始的行号 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. //在Region中记录下所有使用的Column的信息 for column in shape.columns { self.columns.insert(column, region_start + shape.row_count); } // Assign region cells. self.cs.enter_region(name); //创建Region let mut region = SingleChipLayouterRegion::new(self, region_index.into()); let result = { let region: &mut dyn RegionLayouter assignment(region.into()) //采用SingleChipLayouterRegion对电路赋值 }?; let constants_to_assign = region.constants; self.cs.exit_region(); //退出Region // Assign constants. For the simple floor planner, we assign constants in order in // the first `constants` column. if self.constants.is_empty() {//如果制定了constants，需要增加置换限制 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:: .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)}
(&mut self, name: N, mut assignment: A) -> Result
,
,
= &mut shape;
= &mut region;
::from(constants_column).into())
SingleChipLayouter's assign_table 函数当前的电路中增加查找表逻辑：
fn assign_tablewhere A: FnMut(Table<'_, F>) -> Result<(), Error>, N: Fn() -> NR, NR: Into{ // Maintenance hazard: there is near-duplicate code in `v1::AssignmentPass::assign_table`. // Assign table cells. self.cs.enter_region(name); //创建一个Region let mut table = SimpleTableLayouter::new(self.cs, &self.table_columns); { let table: &mut dyn TableLayouter assignment(table.into()) //查找表赋值 }?; let default_and_assigned = table.default_and_assigned; self.cs.exit_region(); //退出当前Region // Check that all table columns have the same length `first_unused`, // and all cells up to that length are assigned. let first_unused = { //获取出所有查找表相关的Column对应的最大使用行数 match default_and_assigned .values() .map(|(_, assigned)| { if assigned.iter().all(|b| *b) { Some(assigned.len()) } else { None } }) .reduce(|acc, item| match (acc, item) { (Some(a), Some(b)) if a == b => Some(a), _ => None, }) { Some(Some(len)) => len, _ => return Err(Error::SynthesisError), // TODO better error } }; // Record these columns so that we can prevent them from being used again. for column in default_and_assigned.keys() { self.table_columns.push(*column); } //根据default_and_assigned信息，采用default值扩展所有的column for (col, (default_val, _)) in default_and_assigned { // default_val must be Some because we must have assigned // at least one cell in each column, and in that case we checked // that all cells up to first_unused were assigned. self.cs .fill_from_row(col.inner(), first_unused, default_val.unwrap())?; } Ok(())}
(&mut self, name: N, mut assignment: A) -> Result<(), Error>
,
= &mut table;
default_and_assigned记录了在一个Fixed Column上的default值以及某个cell是否已经设置。
SingleChipLayouterRegion实现了Region接口。如果在Region中需要给一个Advice列中Cell赋值，可以采用assign_advice函数：
fn assign_advice<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), column: Column offset: usize, to: &'v mut (dyn FnMut() -> Result) -> Result self.layouter.cs.assign_advice( //调用Assignment接口设置相应的Cell信息，特别注意的是在设置的时候需要Cell的全局偏移 annotation, column, *self.layouter.regions[*self.region_index] + offset, to, )?; Ok(Cell { region_index: self.region_index, row_offset: offset, column: column.into(), })}
,
, Error> + 'v),
{
cs.assign_fixed函数，对fixed Column进行赋值。可以参考MockProver的实现，定义在src/dev.rs。
fn assign_fixed &mut self, _: A, column: Column row: usize, to: V,) -> Result<(), Error>where V: FnOnce() -> Result VR: Into A: FnOnce() -> AR, AR: Into{ ... //在一些检查后，设置Fixed列中的某个Cell（column，row指定） *self .fixed .get_mut(column.index()) .and_then(|v| v.get_mut(row)) .ok_or(Error::BoundsFailure)? = CellValue::Assigned(to()?.into().evaluate()); Ok(())}
(
,
,
>,
,
cs.copy函数，增加置换信息。
fn copy( &mut self, left_column: Column left_row: usize, right_column: Column right_row: usize,) -> Result<(), crate::plonk::Error> { if !self.usable_rows.contains(&left_row) || !self.usable_rows.contains(&right_row) { return Err(Error::BoundsFailure); } self.permutation //增加Permutation信息 .copy(left_column, left_row, right_column, right_row)}
,
,

接着我们再详细看看RegionLayouter和TableLayouter。RegionLayouter定义在src/circuit/layouter.rs：

pub trait RegionLayouter //enable选择子 fn enable_selector<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), selector: &Selector, offset: usize, ) -> Result<(), Error>; //advice或者fixed赋值 fn assign_advice<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), column: Column offset: usize, to: &'v mut (dyn FnMut() -> Result ) -> Result fn assign_advice_from_constant<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), column: Column offset: usize, constant: Assigned ) -> Result fn assign_advice_from_instance<'v>( &mut self, annotation: &'v (dyn Fn() -> String + 'v), instance: Column row: usize, advice: Column offset: usize, ) -> Result<(Cell, Option fn assign_fixed<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), column: Column offset: usize, to: &'v mut (dyn FnMut() -> Result ) -> Result //cell相等约束 fn constrain_constant(&mut self, cell: Cell, constant: Assigned fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result<(), Error>;}

: fmt::Debug {

, Error> + 'v),

;

), Error>;

, Error> + 'v),

;

) -> Result<(), Error>;

RegionLayouter的接口很容易理解，包括设置选择子，给cell赋值，约束cell相等。

TableLayouter的接口定义如下：

pub trait TableLayouter fn assign_cell<'v>( &'v mut self, annotation: &'v (dyn Fn() -> String + 'v), column: TableColumn, offset: usize, to: &'v mut (dyn FnMut() -> Result ) -> Result<(), Error>;}

: fmt::Debug {

, Error> + 'v),

TableLayouter只有一个接口：assign_cell。assign_cell是对表中的某个TableColumn的Cell进行赋值。

至此，大体的电路构造的逻辑的框架相对清楚：Halo2中的Chip电路由一个个Region组成，在Halo2的框架中，Region通过Layouter进行分配。电路的所有的信息都存储在Assignment的接口中。MockProver是一个可以参考的Assignment的实现。

ConstraintSystem

ConstraintSystem描述了电路相关的信息：

#[derive(Debug, Clone)]pub struct ConstraintSystem pub(crate) num_fixed_columns: usize, pub(crate) num_advice_columns: usize, pub(crate) num_instance_columns: usize, pub(crate) num_selectors: usize, pub(crate) selector_map: Vec pub(crate) gates: Vec pub(crate) advice_queries: Vec<(Column // Contains an integer for each advice column // identifying how many distinct queries it has // so far; should be same length as num_advice_columns. num_advice_queries: Vec pub(crate) instance_queries: Vec<(Column pub(crate) fixed_queries: Vec<(Column // Permutation argument for performing equality constraints pub(crate) permutation: permutation::Argument, // Vector of lookup arguments, where each corresponds to a sequence of // input expressions and a sequence of table expressions involved in the lookup. pub(crate) lookups: Vec // Vector of fixed columns, which can be used to store constant values // that are copied into advice columns. pub(crate) constants: Vec pub(crate) minimum_degree: Option}

{

, Rotation)>,

大部分字段都比较好理解。gates描述了“Custom Gate”的限制表达式：

#[derive(Clone, Debug)]pub(crate) struct Gate name: &'static str, constraint_names: Vec<&'static str>, polys: Vec /// We track queried selectors separately from other cells, so that we can use them to /// trigger debug checks on gates. queried_selectors: Vec queried_cells: Vec}

{

注意polys中的表达式Expression就是用来表示“Custom Gate”。Halo2的电路构建分为两部分：1/Configure （电路配置）2/ Synthesize（电路综合）。简单的说，Configure就是进行电路本身的配置。Synthesize进行某个电路实例的综合。

看看示例

理解了如上的逻辑，来看看Halo2代码提供的简单的示例程序：examples/simple-example.rs

Configure过程
Configure调用ConstraintSystem申请各种列以及Gate的信息。调用某个Circuit的Configure函数会顺序调用电路涉及到的Chip的Configure信息，这些信息都记录在ConstraintSystem中。
查看实例中的Chip的Configure函数：
impl ... fn configure(meta: &mut ConstraintSystem let advice = [meta.advice_column(), meta.advice_column()]; let instance = meta.instance_column(); let constant = meta.fixed_column(); FieldChip::configure(meta, advice, instance, constant) } ...}impl fn construct(config: Self { config, _marker: PhantomData, } } fn configure( meta: &mut ConstraintSystem advice: [Column instance: Column constant: Column ) -> meta.enable_equality(instance.into()); meta.enable_constant(constant); for column in &advice { meta.enable_equality((*column).into()); } let s_mul = meta.selector(); meta.create_gate("mul", |meta| { // | a0 | a1 | s_mul | // |-----|-----|-------| // | lhs | rhs | s_mul | // | out | | | 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, constant, } }}
Circuit
for MyCircuit
{
) -> Self::Config {
FieldChip
{
>::Config) -> Self {
,
; 2],
,
,
>::Config {
示例电路申请了两个advice列，一个instance和fixed列。同时电路构造了一个乘法Gate：
vec![s_mul * (lhs * rhs - out)]
该乘法Gate就是相应的限制表达式。注意和其他零知识证明的约束系统不一样的是，一个约束可以采用多个行上的Cell。整个调用关系如下：

Synthesize过程

在Configure完电路后，可以调用synthesize综合某个电路实例。整个调用关系如下：

某个Chip调用Layouter分配Region，并在Region中指定约束。可以查看FieldChip的mul函数：

impl fn mul( &self, mut layouter: impl Layouter a: Self::Num, b: Self::Num, ) -> Result let config = self.config(); let mut out = None; layouter.assign_region( || "mul", |mut region: Region<'_, F>| { config.s_mul.enable(&mut region, 0)?; //获取到一个Region后，enable该row对应的乘法selector。 let lhs = region.assign_advice( //对两个advice进行赋值 || "lhs", config.advice[0], 0, || a.value.ok_or(Error::SynthesisError), )?; let rhs = region.assign_advice( || "rhs", config.advice[1], 0, || b.value.ok_or(Error::SynthesisError), )?; region.constrain_equal(a.cell, lhs)?; //限制两个advice和之前的load的Cell一致 region.constrain_equal(b.cell, rhs)?; // Now we can assign the multiplication result into the output position. let value = a.value.and_then(|a| b.value.map(|b| a * b)); let cell = region.assign_advice( //对乘法的输出进行赋值 || "lhs * rhs", config.advice[0], 1, || value.ok_or(Error::SynthesisError), )?; // Finally, we return a variable representing the output, // to be used in another part of the circuit. out = Some(Number { cell, value }); Ok(()) }, )?; Ok(out.unwrap()) } ...}

NumericInstructions

for FieldChip

{

总结：

理解Halo2，可以从两部分着手：1/ 电路构建 2/ 证明系统。从开发者的角度看，电路构建是接口。如何通过Halo2创建电路，这些电路在Halo2的内部如何表示是理解电路构建的关键。Halo2中的Chip电路由一个个Region组成，在Halo2的框架中，Region通过Layouter进行分配。电路的所有的信息都存储在Assignment的接口中。Halo2的电路构建分为两部分：1/Configure （电路配置）2/ Synthesize（电路综合）。简单的说，Configure就是进行电路本身的配置。Synthesize进行某个电路实例的综合。