我们在之前的《使用 halo2 开发电路》文章里,介绍了如果使用 halo2 进行电路开发。在这篇文章里,我们详细讲讲,在开发电路的时,还需要注意什么。
在撰写这篇文章的时候, 参考的 halo2 代码是 https://github.com/zcash/halo2 ,版本是
f9b3ff2aef09a5a3cb5489d0e7e747e9523d2e6e。
在开始之前,先重温一下最核心的 circuit 定义:
// src/plonk/circuit.rspub 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>;}
一如往常,我们开发电路时,需要实现这个 trait:
Config
• 定义电路的约束,主要是 create_gate() 函数来定义。
FloorPlanner
• 电路的 floor planing 策略,实现 synthesize() 函数,使用提供的 Config、constants、以及 Assignment 来 synthesize 电路。
without_witnesses
• 没有 witness 的电路,一般使用 Self::default()。
configure
• 电路门的描述创建,约束的构建。
synthesize
• 根据提供的 config,来对 Layouter 进行赋值,核心用到了它的 assin_region() 函数,而这个函数用到了 closure,它的参数是 Region。
所以从上面的定义来看, halo2 的电路开发,核心就是两个函数:configure 和 synthesize,前者创建门定义约束,后者将 witness 和 public 数据,赋值到约束中。
这篇文章我们就来看看,在电路开发的皮肤之下,发生了什么。
1. configure
由 configure 函数的声明可知,在定义电路时,会修改 ConstraintSystem,且返回 Config 留待后用。
// examples/simple-example.rsfn 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,让我们深入其中,抽丝剥茧。configure 做了这么几件事:
a.先是创建了 advice,instance 以及 fixed column(这几个 column 的用途和意义,请参见我们之前的文章)。
• advice_column(), instance_column(), fixed_column() 的功能类似,都是创建一个相应类型(advice / instance / fixed)的 cloumn,将 ConstraintSystem 中相应 column 的计数加 1,再将这个新建的 column 返回出来。
b. 然后调用 ConstraintSystem 的 enable_equality() 函数,将 instance 和 advice column 放入,再调用 enable_constant () 将 constant 放入。
• 而这两个函数的作用是 Enable the ability to enforce equality over cells in this column。
c. 之后调用 selector 函数,生成 selector。
d. 最重要的,调用 ConstraintSystem 的 create_gate 函数,传入一个以&mut VirtualCells 为参数的 closure,创建 gate。
•在这个 closure 中,调用了 VirtualCells 的 query_advice 函数,传入上面生成的 advice column,和 selector,且使用 column 和 rotation 构造 cell。同时生成以 column 和 rotation 为参数的 Expression,最后返回以 Expression 为主的约束。需要注意的是,这个 query_advice() 函数,既生成了 cell,又将 column 和 rotation 放入 ConstraintSystem 中,这样,将 cell 和 cs 通过 column 和 rotation 的方式联系起来。
• create_gate 函数中,就是将 closure 里生成的约束和 cell,构造 Gate,并存入 cs 的 gates 数组里。
e. 最后返回 Config 留待后用。
我们总结一下,上面先是创建了相应的 column,接着创建 selector,最后使用 create_gate 函数,将 column 和 selector 生成 cells 和约束,最后将约束和 cells 用于生成 gate,最后保存 gate。
一言以蔽之,configure 做的事,就是生成约束关系。
2. synthesize
circuit 是通过 witness 和 public 数据初始化的。在 synthesize 函数中,会将数据传入。由于官方的例子中有很多的结构化代码,我们在此文中,将这些代码展开在 synthsize 函数中,如下所示:
// examples/simple-example.rsfn synthesize(&self, config: Self::Config, layouter: impl Layouter) -> 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)}
Wah, that's a lot of assign_region s
我们先来看看,使用了 a,b,constant 这些传入参数的代码做了什么。assign_region 是 Layouter trait 的一个函数,在深入这个函数之前,我们先看看 Layouter 这个 trait。
3. Layouter
Layouter 是 chip-agnostic 的,我们在之前的 halo2 开发导读中讲过,电路开发时,有个重要的核心是 chip,所以对 Layouter 来说,chip 是用来干什么的,chip 是如何定义的,它统统不关心,即 Layouter 和 chip 是解耦的。而 Layouter 本身,是一个电路赋值的抽象策略 trait,如何理解这句话?即 Layouter 用于电路的赋值,比如处理 row indices。
它的定义如下:
// src/circuit.rspub trait Layouter<F: Field> {type Root: Layouter<F>;fn assign_region<A, AR, N, NR>(&mut self, name: N, assignment: A) -> Result<AR, Error>whereA: 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>whereA: 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)whereNR: 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>whereNR: Into<String>,N: FnOnce() -> NR,{self.get_root().push_namespace(name_fn);NamespacedLayouter(self.get_root(), PhantomData)}}
让我们逐个函数来分析:
• 先从简单处着手,root/namespace 相关的函数,都是涉及到 namespace,用于标识当前 Layouter。
• constrain_instance 函数用于对某个 Cell 和绝对位置下 instance column 的 row value 进行约束。
• 最核心的函数是 assign_region 和 assign_table,根据其函数名可知,这两个函数分别用于 region,table 的赋值。这也是这个 trait 最重要的功能——即 Layouter trait 就是用于 region,table 的赋值。关于 region 和 table,我们在后面会讲到。
我们话接上文,深入看看 assign_region 函数。这个函数接收一个 string 和 FnMut(Region<'_, F>) -> Result< AR, Error >的 closure,且含有&mut self。我们看看这个重要的 Region 的定义:
pub struct Region<'r, F: Field> {region: &'r mut dyn layouter::RegionLayouter<F>,}
可知 Region 是对 RegionLayouter 的封装,而 RegionLayouter 是一个用于 Region 的 Layouter, 在介绍 RegionLayouter 之前, 我们要避免深入细节太多, 我们先看看 Layouter 的具体实现。simple-example 这个例子里, SingleChipLayouter 实现了 Layouter 的 trait。
// src/circuit/floor_planner/single_pass.rspub 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>whereA: 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)}
如上面代码及注释所述,SingleChipLayouter 的 assign_region 函数,做了这么几件事:
a. 获取当前 SingleChipLayouter 的 region 数量, 构造一个 RegionShape, 且将该 RegionShape 传入 closure。此时, 执行这个 closure, 且会更改这个 RegionShape。
• 看看这个 closure,它将传入的 mut region,调用 region 的 assign_advice 函数:
// src/circuit.rspub fn Region::assign_advice<'v, V, VR, A, AR>(&'v mut self,annotation: A,column: Column,offset: usize,mut to: V,) -> Result,<AssignedCell<VR,F>, Error>whereV: FnMut() -> Result + 'v,for<'vr> Assigned: From<&'vr VR>,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,})}
这个函数内部会调用 RegionLayouter 的 assign_advice, 上面的 RegionShape 实现了 RegionLayouter trait,所以最后用到了 RegionShape 的 assign_advice 函数:
// src/circuit/layouter.rsfn 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(),})}
此时, RegionShape 会记录 column, 即 config.advice[0], 且会将 offset+1 和 row_count 相比较, 更新 row_count。
b.比较 RegionShape 中的所有 column,找到 SingleChipLayouter 中记录的 column 和 region_start,更新之。
c.给 region cells 赋值,构造一个 SingleChipLayouterRegion, 将其转为 RegionLayouter, 再调用 closure 函数。只是这次和 1 不同的是, 在 closure 中执行了 SingleChipLayouterRegion 的
assign_advice 函数:
// src/circuit/floor_planner/single_pass.rsfn SingleChipLayouterRegion::assign_advice<'v>(&'v mut self,annotation: &'v (dyn Fn() -> String + 'v),column: Column,offset: usize,to: &'v mut (dyn FnMut() -> Result, 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(),})}
可以看到,这个函数中,调用了 SingleChipLayouter 中 Assignment 的 assign_advice 函数,而在当前这个例子中,Assignment trait 是由 MockProver 实现的:
// src/dev.rsfn MockProver::assign_advice<V,VR,A,AR>(&mut self,_: A,column: Column,row: usize,to: V,) -> Result<(), Error>whereV: 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(())}
它会判断这个 region 的 row 是否超出了可用的 rows 范围; 然后会修改 current_region, 将用到的 column 和 row 写入 region 中; 且将 advice 中相应 column/row 位置的值改成 to。所以真实存储 advice 数据的是 MockProver, 之前在 configure 中用到的 constraintsystem, 也是 MockProver 的一个字段。简而言之,MockProver 将 configure 和 systhesize 联系起来了。
对电路开发者来说,我们真正关心的是,该如何设计开发高效安全的电路,而不需要关心太多底层电路系统的设计。我们想知道,在 configure 阶段,如何创建 column 和 row,如何创建 gate;在 systhesize 阶段,是否需要按照顺序给 column 和 row 赋值。
我们对例子代码稍加如下改动:
// simple-example.rsfn main() {...let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();println!("{:?}", prover);// assert_eq!(prover.verify(), Ok(()));...}
这样就可以打印 MockProver 的内容,其中 advice 的结果如下:
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)]]
可以看出,advice 有两个 column,我们将其可视化。

第 1~3 行,都是 load_private/load_constant 数据,将其放入第一列中。第 4 行,调用 mul,从该行的第 1,2 列取数据,将计算结果保存在下一行的第一列,即第 5 行。后面都是大同小异的 mul 运算。
最后使用 constrain_instance 将计算的结果,和 instance column 约束起来,就是检查计算的 0xfc 是否等于输入的 public input。
我们可以看到,MockProver 的 instance 的结果是:

参考文献
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
关于我们
Sin7y 成立于 2021 年,由顶尖的区块链开发者组成。我们既是项目孵化器也是区块链技术研究团队,探索 EVM、Layer2、跨链、隐私计算、自主支付解决方案等最重要和最前沿的技术。

微信公众号:Sin7y
GitHub: Sin7y
Twitter: @Sin7y_Labs
Medium: Sin7y
Mirror: Sin7y
HackMD: Sin7y
HackerNoon: Sin7y
Email: contact@sin7y.org
【免责声明】市场有风险,投资需谨慎。本文不构成投资建议,用户应考虑本文中的任何意见、观点或结论是否符合其特定状况。据此投资,责任自负。
