Why Forward-Only Jumps, and What Loops Would Actually Require
"No loops" is the single biggest capability gap listed in this project's roadmap. Here's the actual, specific reason it's there, and why it's a bigger change than it sounds.
JZ and JNZ are real conditional jumps — the parser resolves label targets, the interpreter tracks a runtime program counter separate from the static row index, and the AIR asserts which row actually ran via the active flag (see how that assertion is made sound). What they can't do is jump backward. That's not an oversight; it's load-bearing for everything else about how this VM's trace works.
One row per instruction, always
The execution trace has exactly one row per static instruction in the program — never revisited. A program with 10 instructions produces a 10-row trace (padded to a power of two for the STARK), regardless of which branches were actually taken. That's what makes the trace length fixed and known at parse time, before any execution happens.
A backward jump breaks that immediately: if instruction 3 can jump back to instruction 1, a single static instruction can execute an unbounded number of times depending on runtime data. The trace can no longer have "one row per instruction" — it needs "one row per execution step," and the number of steps isn't knowable until the program actually runs.
What actually has to change
Real loops need a trace whose length depends on the specific execution, not just the program text:
- A maximum cycle count. STARKs need a trace length fixed at proving time (padded to a power of two), so there has to be some upper bound on how many steps a program can take — a real design parameter, not a detail.
- Padding for executions shorter than the max. Most programs won't use every available cycle; the unused rows need a well-defined "halted" state that doesn't corrupt the constraints checking the rows that did real work.
- Proof-size variability. Today, every program of the same instruction count produces a same-shape proof. Once trace length depends on runtime behavior (how many loop iterations actually ran), proof size becomes a function of execution, not just program text — a real, user-visible change.
The part that doesn't change
Here's the thing worth being specific about: the "verifier re-executes and asserts everything" trick from the soundness post still works with loops. The verifier can run the interpreter itself regardless of how many iterations a loop takes — re-execution doesn't care about trace-length mechanics. What's genuinely new work is the trace-length selection and padding scheme, not the soundness argument underneath it.
That's specifically why this is first on the suggested-next-slice list, ahead of memory or RISC-V compatibility: it's a real, scoped, self-contained problem, distinct from whether the underlying soundness technique holds — which it does.