A Register File Without an Algebraic Mux
Four registers, addressed by LOAD/STORE. The obvious way to prove "this instruction touched register 2, not register 0" needs a selection argument. This VM asserts it instead — and tests specifically that lying about it gets caught.
Adding a register file to a STARK VM is a natural second step after straight-line arithmetic — examples/counter.zkasm is the first program that needs to hold a value across unrelated computation. The obvious design question: when a row executes STORE r2, how does the AIR prove that register 2, specifically, got updated, and the other three didn't?
The one-hot column
Each row carries a one-hot reg_sel array — four field elements, one per register, exactly one of them equal to 1:
pub struct ProgramRow {
...
pub reg_sel: [BaseElement; NUM_REGISTERS],
}The same argument from the no-secret-witness post applies directly here: since the program is public, the verifier already knows which register every LOAD/STORE in the program addresses, at parse time. So reg_sel isn't derived by the AIR — it's asserted, one boundary constraint per register per row, exactly like the opcode selectors and the active flag.
What's actually constrained
Given reg_sel as already-known-correct, the register file's transition constraint for register k reads, roughly:
write_k = active * s_store * reg_sel[k]
next_register[k] = if write_k { acc } else { current_register[k] }One constraint per register, degree 4 in the worst case (active * s_store * reg_sel[k] multiplied against the value being written) — the same shape as the accumulator constraint, just gated by an extra one-hot factor. Four registers means four of these constraints running in parallel, each one only firing on the rows where its own reg_sel[k] is 1.
The negative test that actually matters
The soundness claim here isn't "the honest prover produces a correct proof" — that's the easy direction. It's "a prover cannot claim a different register was touched and still verify." The test suite checks this directly, not just conceptually:
#[test]
fn rejects_a_claimed_register_selector_that_does_not_match_the_proof() {
// ... generate a real proof, then tamper with reg_sel in the
// public inputs before verifying ...
assert!(verify_program(proof, tampered_inputs).is_err());
}That test exists specifically because the register selector is a value the AIR trusts without algebraic derivation — the whole soundness argument rests on the verifier building it correctly from the program, and on a mismatched one causing rejection every time. That's what the test actually exercises.
Why four, and why static
Four registers is a small, deliberately narrow slice: enough to prove something needs more than one live value (the accumulator alone isn't sufficient once a program has to hold a result across unrelated arithmetic), not enough to look like general memory. reg_sel being one-hot over a fixed set of four only works because the register a given instruction touches is baked into the instruction at parse time — STORE r2 is syntactically fixed, not a runtime-computed address. That's exactly the boundary the soundness-trick post flags: real memory, where the address is itself a trace value, is a materially different problem.