Diagram, then explanation, then the actual invariants and implementation -- with links to the source and tests that enforce them. This is the whole AIR; nothing is summarized away.
One row per static instruction — never revisited (see the Loops section below) — holding: the accumulator value, four register values, 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, an active flag (did this row actually run, or was it skipped by an earlier taken jump), and a one-hot reg_sel (which register a LOAD/STORE addresses). Ten fixed columns, plus two per register.
This system has no private input. The verifier already re-executes the program to know the correct value of every column at every row — the same way it knows the initial accumulator value and the claimed final result. Because of that, every column except the accumulator and the registers — including active and reg_sel — is individually asserted (as a boundary constraint) against the specific program and its actual execution, for every row, not just the first and last.
That's sound without an algebraic is-zero/lookup gadget deriving branch outcomes or a mux selecting a register, specifically because there's no witness to hide it behind. The things that are checked algebraically — via the AIR's transition constraints — are whether the accumulator's and each register's trajectory are consistent with that already-known-correct sequence.
Only two things need algebra: the accumulator's update, and each register's update.
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. Because the opcode selectors are already known-correct from the boundary assertions, at most one term in applied is non-zero for any row — a selector-weighted sum standing in for a match statement. The register update 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);
The worst-case term (active * s_mul * acc * right) is degree 4, so that's the declared bound — even though the interpolated degree degenerates to 3 on straight-line traces. Winterfell's debug-only self-check is stricter than that, which is why this workspace's tests run under --release.
A prover cannot swap in a different sequence of instructions, a different control-flow outcome, or a different register access, for the same instructions, and still produce a proof that verifies. The test suite checks this directly: tampering with the claimed result, program, active flags, or register selectors after proof generation causes verification to fail.
What this does not cover: forward-only jumps mean loops aren't supported yet (a trace-length-depends-on-runtime problem), the fixed 4-register file isn't general-purpose memory, and the on-chain path is an attested trust bridge, not a cryptographic on-chain check — see the FAQ for the trust boundary stated plainly.
VmAir::evaluate_transition, VmAir::get_assertions