Zero Knowledge Proof — Error Explanation when developing Custom Gate

To develop circuits on Halo2, we have to design custom gates. Occasionally, some errors occur while developing costume gates, this article summarizes and analyzes some errors and their implementation logic for developing costume gates on Halo2.

To make the cause of the errors clear, let’s first introduce a simple circuit to demonstrate the errors and their causes.

The circuit consists of two Columns: Column A and Column B, both of which are advice.

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

Let’s design a custom gate of mul and ensure that 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)]

The value assignment for the circuit is shown below:

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

Before moving on to the Constraint Poisoned, we must understand usable rows. The rows within the largest rows the program actively assigns are called usable rows. When the circuit rows need to be expanded, the expanded rows are not considered usable rows. The cells in the advice column of these rows are initialized to “Poisoned”.

The related code is shown in the run function of halo2_proofs/src/dev.rs MockProver:

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

Note that the computation results of these Poisoned Cell(Expression) are also Poisoned. By this point, you can guess that ConstraintPoisoned means that the computation result of a certain Expression in a Custom Gate is Poisoned. Taking the following circuit as an example, the following error will be returned after the execution:

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

Alongside the returned error, Mockprover also provides specific error details. As for the example above, the error occurs in the first custom gate named “mul”. The error is caused by the first Expression in the Custom Gate.

How to fix the ConstraintPoisoned error? Use a Selector. For a selector, the default initial value is 0. Even if the computation result of the other Expression in the circuit is Poisoned, the product with Selector(0) is 0. This ensures the stability of the Custom Gate state.

The following circuit adds the Selector, with adjustments as follows:

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

Custom gate of mul adjusts to:

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))]

The circuit assignment adjusts to:

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

With the previous circuit adjustment, there’s a new error: 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 },

The error above indicates that the Cell with an offset of 15 is not assigned a value in the first and second Column (both are Advice) of the first Region. You may be confused that only the Cell with an offset of 0/1/2 is assigned a value when assigning values to the circuit. Logically, other Cell should be automatically assigned as Poisoned by the proof system. Why does the CellNotAssigned error still occur?

Let’s take a look at the verify process, then it’s easy to figure out:

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,
    })
}
})

The enable(Selector) in the example circuit is effective starting from the first row. Take a look at the data of gate_row=0. For the a_prev/b_prev Cell, cell.rotation=-1, which means cell_row is 15. However, in the region of (r.cells), there’s no value assigned for the Cell with an offset of 15. Basically, the verify logic checks whether all the cells of the Custom Gate with a Selector have been assigned values. So only the rows enabled by the Selector will be checked.

Other than this error, there’s another one in this circuit.

ConstraintNotSatisfied

This error is most commonly seen and easiest to understand: the constraints of the circuit are not satisfied. For a custom gate, the result of its Expression is not 0. This error is easy to solve, the developer only needs to carefully check the value assigned to each cell. For the example circuit, the constraint for the first line in the custom gate is not satisfied — there’s no value assigned for the offset of 15.

After understanding the principle, the solution to this error is simple — adjusting the circuit value assignments:

//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)), )?;

Deactivate enable in the first row of the circuit, so Custom Gate of mul is not enabled.

Summary:

This article summarizes and analyzes three commonly seen circuit errors when developing Custom Gate on Halo2.