halo2 icon indicating copy to clipboard operation
halo2 copied to clipboard

User guide: explain what `Rotation` means, with an example

Open str4d opened this issue 2 years ago • 0 comments

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

str4d avatar Feb 01 '22 02:02 str4d