Why This zkVM's Soundness Doesn't Need a Lookup Argument

Branch outcomes and register accesses are usually the hard part of a STARK AIR. Here they're asserted directly, for one specific reason this post spells out precisely — including where the reason stops applying.

2026-08-31 · crates/zkvm-stark/src/lib.rs

Most STARK-based VMs need an algebraic gadget to prove that a program's control flow was followed correctly: an is-zero check to derive a branch outcome, a permutation argument to prove a memory access hit the right address, a mux to select which register a load or store touched. Building those gadgets correctly is a large fraction of the actual work in a STARK VM.

This one doesn't have any of them, for a specific, narrow reason: there is no secret witness anywhere in this system.

What "the verifier already knows" actually means

A .zkasm program is entirely public — the instructions, the starting accumulator value, everything. When a verifier checks a proof, it doesn't just check the STARK; it first re-executes the program itself:

let padded = program.padded();
let pub_inputs = public_inputs_for_program(&padded);
verify_program(proof, pub_inputs)

public_inputs_for_program runs the real interpreter over the real program and builds the exact sequence of values a correct execution must have had — the opcode at every row, whether a branch was taken, which register a LOAD or STORE touched. Every one of those values is then a boundary assertion, checked directly against the trace at every row, not derived algebraically.

That's the whole trick. A lookup/permutation argument exists to answer "does this row's claim correspond to a value the prover chose secretly, without revealing which one?" When there's no secret value — the verifier already computed the one correct answer itself — that question doesn't need asking. The proof only needs to check that the trace's trajectory (the accumulator's value, each register's value, row over row) is consistent with a sequence of opcodes and flags the verifier already independently knows are correct.

What's actually still algebraic

Not everything is a direct assertion. The accumulator and the four registers are checked through real transition constraints — for example, the accumulator constraint has to express "if this row is an active MUL, next row's accumulator equals this row's accumulator times the right operand; otherwise it's unchanged" as a single polynomial identity, combining seven possible opcodes and the active flag multiplicatively. That's a real degree-4 constraint doing real work — see the AIR's actual degree behavior for what that costs.

So the AIR splits into two categories:

• Directly asserted (no gadget needed): all seven opcode selectors, the active flag, the one-hot register selector, the shared operand — anything the verifier can just compute from the program and pin down row by row.
• Algebraically constrained (real transition constraints): the accumulator's value and each register's value, whose trajectories depend on the already-asserted-correct selectors above.

Where this stops working

This is the part worth being precise about, because it's easy to overstate. The trick works specifically because nothing in this system is hidden from the verifier. Two changes would break it:

1. Private inputs. If a program could take a witness the verifier doesn't see, the verifier can no longer just re-execute to find "the" correct trace — there could be many traces consistent with the public claim, and picking the right one requires exactly the algebraic machinery this system currently avoids.
2. Dynamic addressing. Today's LOAD/STORE address one of four statically-named registers — the instruction itself says which one. Real memory, where the address is a runtime value (LD r0, [r1]), is a different problem: the verifier still knows the correct value at every access by re-executing, but proving which address was touched, when that address is itself a trace value rather than a constant baked into the instruction, needs either a permutation argument or a fresh argument for why one still isn't needed. That's an open question, not a solved one — see the note in docs/ROADMAP.md.

The honest framing: this makes the system a STARK-verifiable virtual machine for public, deterministic computation — not a zero-knowledge VM in the RISC Zero/SP1 sense, which is built specifically to hide a private witness. That distinction matters enough that it shapes how this project describes itself; see the threat model for the fuller picture of what is and isn't trustless here.