零知识证明 - Halo2开发常见错误(Custom Gate)

  • Star Li
  • 更新于 2022-06-24 08:50
  • 阅读 1793

使用Halo2开发电路,不可避免会设计custom gate。在实际开发custom gate的过程中,经常会碰到一些错误。该篇文章总结并分析了在Halo2库基础上开发custom gate的一些错误和原理。

使用Halo2开发电路,不可避免会设计custom gate。在实际开发custom gate的过程中,经常会碰到一些错误。该篇文章总结并分析了在Halo2库基础上开发custom gate的一些错误和原理。

为了清晰地讲解这些错误的原因,先介绍一个简单电路。用这个例子讲解相应的错误原因。

电路由两个Column组成:一个是column A,一个是column B。这两个Column都是advice的。

+----------+----------+
| Column A | Column B |
+----------+----------+
| a_prev   | b_prev   |
| a_cur   | b_cur   |
| ...     | ...     |
+----------+----------+

并且设计一个custom gate (mul),保证a_cur = a_prev*b_prev。

let a_p = meta.query_advice(advice[0], Rotation::prev());
let b_p = meta.query_advice(advice[1], Rotation::prev());
let a = meta.query_advice(advice[0], Rotation::cur());
let b = meta.query_advice(advice[1], Rotation::cur());

vec![a - (a_p*b_p)]

电路的赋值情况如下:

region.assign_advice( || "a", config.advice[0], 0, || Ok(F::from(1)), )?;
region.assign_advice( || "b", config.advice[1], 0, || Ok(F::from(2)), )?;
region.assign_advice( || "a", config.advice[0], 1, || Ok(F::from(2)), )?;
region.assign_advice( || "b", config.advice[1], 1, || Ok(F::from(3)), )?;
region.assign_advice( || "a", config.advice[0], 2, || Ok(F::from(6)), )?;
region.assign_advice( || "b", config.advice[1], 2, || Ok(F::from(7)), )?;
  • ConstraintPoisoned

理解Constraint Poisoned之前,需要理解usable rows。在程序主动进行赋值的最大的row之内的row称为usable rows。电路row需要进行扩展,扩展出来的row就不是usable rows。这些rows中的advice column中的cell会被初始化为"Posioned"。

  • 相关的逻辑在halo2_proofs/src/dev.rs的MockProver的run函数:
    let mut column = vec![CellValue::Unassigned; n];
    // Poison unusable rows.
    for (i, cell) in column.iter_mut().enumerate().skip(usable_rows) {
    *cell = CellValue::Poison(i);
    }
    column

注意的是,这些Posioned的Cell(Expression)的计算结果也是Poisoned。到此,大家可以猜到,ConstraintPoisoned的意思就是一个Custom Gate中的某个Expression的计算结果是Poisoned。以示例电路为例,执行后会得到如下的错误:

  • ConstraintPoisoned { constraint: Constraint { gate: Gate { index: 0, name: "mul" }, index: 0, name: "" } },

再给出错误的同时,MockProver会提供详细的错误原因。上面的这个错误,就是第一个custom gate,名字是"mul"。错误产生是因为这个Custom Gate中的第一个Expression。

如何修复ConstraintPoisoned的问题?使用Selector。对于一个Selector,有默认的赋值0。即使电路中的其他Expression的计算结果是Poisoned,在和Selector(0)乘之后结果为0。这样就能保证一个Custom Gate的状态的确定性。

示例电路增加Selector,调整如下:

+----------+----------+----------+
| Selector | Column A | Column B |
+----------+----------+----------+
|       1 | a_prev   | b_prev   |
|       1 | a_cur   | b_cur   |
|     ... | ...     | ...     |
+----------+----------+----------+

Custom Gate (mul)调整为:

let a_p = meta.query_advice(advice[0], Rotation::prev());
let b_p = meta.query_advice(advice[1], Rotation::prev());
let a = meta.query_advice(advice[0], Rotation::cur());
let b = meta.query_advice(advice[1], Rotation::cur());

let enable = meta.query_selector(enable);

vec![enable*(a - (a_p*b_p))]

电路赋值调整为:

config.enable.enable(&mut region, 0);
region.assign_advice( || "a", config.advice[0], 0, || Ok(F::from(1)), )?;
region.assign_advice( || "b", config.advice[1], 0, || Ok(F::from(2)), )?;
config.enable.enable(&mut region, 1);
region.assign_advice( || "a", config.advice[0], 1, || Ok(F::from(2)), )?;
region.assign_advice( || "b", config.advice[1], 1, || Ok(F::from(3)), )?;
config.enable.enable(&mut region, 2);
region.assign_advice( || "a", config.advice[0], 2, || Ok(F::from(6)), )?;
region.assign_advice( || "b", config.advice[1], 2, || Ok(F::from(7)), )?;
  • CellNotAssigned

经过如上的电路调整,出现新的错误类型:CellNotAssigned。

CellNotAssigned { gate: Gate { index: 0, name: "mul" }, region: Region { index: 0, name: "mul" }, column: Column { index: 0, column_type: Advice }, offset: 15 },
CellNotAssigned { gate: Gate { index: 0, name: "mul" }, region: Region { index: 0, name: "mul" }, column: Column { index: 1, column_type: Advice }, offset: 15 },

上述的错误表示在第一个Region中的第一个和第二个Column(都是Advice)的偏移为15的Cell没有赋值。大家可能比较奇怪,在电路赋值的时候只对偏移为0/1/2的Cell赋值,按道理,其他的Cell应该由证明系统自动填充为Poisoned。为啥还出现CellNotAssigned的情况呢?

查看verify的逻辑,道理非常清晰:

gate.queried_cells().iter().filter_map(move |cell| {
  // Determine where this cell should have been assigned.
  let cell_row = ((gate_row + n + cell.rotation.0) % n) as usize;

  // Check that it was assigned!
  if r.cells.contains(&(cell.column, cell_row)) {
      None
  } else {
      Some(VerifyFailure::CellNotAssigned {
          gate: (gate_index, gate.name()).into(),
          region: (r_i, r.name.clone()).into(),
          column: cell.column,
          offset: cell_row as isize - r.rows.unwrap().0 as isize,
      })
  }
})

示例电路中的enable(Selector)是从第一个row使能的。观察gate_row=0的情况。对于a_prev/b_prev的Cell来说,cell.rotation=-1。这样的话,cell_row即为15。但是,在region范围内(r.cells),并没有对偏移15的Cell进行赋值。oops。简单的说,verify逻辑检查有Selector参与的Custom Gate对应的Cell是否都有赋值。检查时,只针对Selector使能的行进行检查。

除了这个错误外,这个电路还有另外一个错误。

  • ConstraintNotSatisfied

这个错误是最常见也是最容易理解的。电路出现了不满足。对一个custom gate来说,custom gate对应的Expression的计算结果不等于0。这种情况比较简单,开发者只需要详细分析每个cell的赋值即可。对于示例电路而言,custom gate在第一行就不满足,根本就没有偏移为15的赋值。

了解了原理,修复如上错误的方法也比较简单,调整电路赋值:

//config.enable.enable(&mut region, 0);
region.assign_advice( || "a", config.advice[0], 0, || Ok(F::from(1)), )?;
region.assign_advice( || "b", config.advice[1], 0, || Ok(F::from(2)), )?;
config.enable.enable(&mut region, 1);
region.assign_advice( || "a", config.advice[0], 1, || Ok(F::from(2)), )?;
region.assign_advice( || "b", config.advice[1], 1, || Ok(F::from(3)), )?;
config.enable.enable(&mut region, 2);
region.assign_advice( || "a", config.advice[0], 2, || Ok(F::from(6)), )?;
region.assign_advice( || "b", config.advice[1], 2, || Ok(F::from(7)), )?;

电路的第一行,不激活enable,从而不启用Custom Gate(mul)。

总结

本文结合示例电路,总结并分析了Halo2开发Custom Gate时常见的三种电路错误。

本文首发于:https://mp.weixin.qq.com/s/sqbuyzDIlVRdcrkWwHnvfQ

点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
Star Li
Star Li
Trapdoor Tech创始人,前猎豹移动技术总监,香港中文大学访问学者。