零知识证明 - 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