halo2
halo2 copied to clipboard
User guide: explain what `Rotation` means, with an example
A user was trying to implement a decomposition constraint, and wrote the following code:
let q_decompose = meta.query_selector(q_decompose);
let x = meta.query_advice(config.advice, Rotation::cur());
let x0 = meta.query_advice(config.advice, Rotation::next());
let x1 = meta.query_advice(config.advice, Rotation::next());
let x2 = meta.query_advice(config.advice, Rotation::next());
let x3 = meta.query_advice(config.advice, Rotation::next());
let decomposition_check = x0
+ x1 * F::from(1 << 8)
+ x2 * F::from(1 << 16)
+ x3 * F::from(1 << 24)
- x;
and obtained the following MockProver
failure:
ConstraintNotSatisfied {
constraint: Constraint { gate: Gate { index: 0, name: "constraint decompose" }, index: 0, name: "" },
row: 1,
cell_values: [
(VirtualCell { name: "", column: Column { column_type: Advice, index: 0 }, rotation: 0 }, "0x5"),
(VirtualCell { name: "", column: Column { column_type: Advice, index: 0 }, rotation: 1 }, "0x5"),
]
}
The problem is obvious to someone already skilled in halo2
: the constraint is querying the same cell four times for four different variables, so is trying to constrain 5 + 5 * (1 << 8) + 5 * (1 << 16) + 5 * (1 << 24) - 5 = 0
, which is false.
When I inquired further, the user said that they thought Rotation::next()
was querying 1, 2, 3, ...
and that each time they called it, they'd get the next row. I suspect the confusion arises from the naming similarity to mutating APIs like Iterator::next()
, which could indeed return a sequence. This is an unfortunate semantic collision, that we need to do a better job of heading off in the user guide.
We should add a section to the user guide / tutorial that explains how Rotation
works, what it is useful for, and how to use it to write constraints. A visual guide could also help (I usually use the "Tetris piece" analogy).