深入解读 Halo2 电路开发
2022-08-0314:19
Sin7y
2022-08-03 14:19
Sin7y
2022-08-03 14:19
收藏文章
订阅专栏


我们在之前的《使用 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.rs fn 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>    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)    }}


让我们逐个函数来分析:

  先从简单处着手,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>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)}

如上面代码及注释所述,SingleChipLayouter 的 assign_region 函数,做了这么几件事:


a. 获取当前 SingleChipLayouter 的 region 数量, 构造一个 RegionShape, 且将该 RegionShape 传入 closure。此时, 执行这个 closure, 且会更改这个 RegionShape。

  看看这个 closure,它将传入的 mut region,调用 region 的 assign_advice 函数:

// src/circuit.rs     pub 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>     where       V: 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.rs     fn 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.rs fn MockProver::assign_advice<V,VR,A,AR>(         &mut self,    _: A,     column: Column,     row: usize,    to: V, ) -> Result<(), Error> 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(()) }

它会判断这个 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.rs fn 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


【免责声明】市场有风险,投资需谨慎。本文不构成投资建议,用户应考虑本文中的任何意见、观点或结论是否符合其特定状况。据此投资,责任自负。

专栏文章
查看更多
数据请求中

推荐专栏

数据请求中

一起「遇见」未来

DOWNLOAD FORESIGHT NEWS APP

Download QR Code