Reading a Winterfell AIR: One Degree-4 Constraint, Two Kinds of Check

Most "how STARKs work" explainers stop at "transition constraints and boundary constraints." Here's what those two categories actually look like as Rust, in a trace with 10 fixed columns plus two per register.

2026-09-01 · crates/zkvm-stark/src/lib.rs

The column layout

Ten fixed columns — the accumulator, seven one-hot opcode selectors (s_add/s_sub/s_mul/s_jz/s_jnz/s_load/s_store), the shared immediate/target/register operand (right), and an active flag — plus NUM_REGISTERS one-hot "which register" selectors and NUM_REGISTERS register-value columns. One row per static instruction, not per executed step: a skipped branch still gets a row, with active = 0.

Boundary constraints: nine per row, asserted directly

get_assertions asserts every selector, right, active, and every reg_sel[k] — for every row — against the specific program being proven. That's possible because there's no secret witness: the verifier already re-executed the program and knows the correct value for all of these at every step, the same way it knows the initial accumulator value and the claimed final result (the only two boundary assertions on the accumulator column itself). See the no-secret-witness post for why that's sound rather than a shortcut.

Transition constraints: the two things that actually need algebra

Only the accumulator's and each register's trajectory can't be asserted directly, because a boundary assertion only pins a value at one specific step — it can't say "this value evolves consistently step to step." That needs evaluate_transition:

let applied = s_add * (acc + right)
    + s_sub * (acc - right)
    + s_mul * (acc * right)
    + (s_jz + s_jnz + s_store) * acc
    + s_load * loaded;

result[0] = next_acc - (active * applied + (E::ONE - active) * acc);

loaded is the one-hot-selected register value (reg_sel[k] * registers[k], summed). Because s_add through s_load are already known-correct one-hot values from the boundary assertions, at most one term in applied is non-zero for any given row — this is a selector-weighted sum standing in for a match statement, not five separate additions actually happening. The register update constraint follows the same shape, once per register:

let write_k = active * s_store * reg_sel[k];
result[1 + k] = next_r_k - (write_k * acc + (E::ONE - write_k) * r_k);

Why the declared degree is 4 when the real one is usually 3

The worst-case term — active * s_mul * acc * right, four trace columns multiplied together — is degree 4, so TransitionConstraintDegree::new(4) is the declared bound. But on a trace where active is constant (straight-line programs, or an untaken branch), the interpolated polynomial's actual degree degenerates to 3. Winterfell's own debug-only validate_transition_degrees self-check demands the actual degree match the declared one exactly, which only happens on inputs that hit the true degree-4 case — see the Winterfell debug-assertion post for the full reproduction and why --release is required for tests.