Everything below is verified against crates/zkvm-isa/src/lib.rs directly -- including the exact error messages the parser produces.
One accumulator (acc), and 4 fixed registers (r0–r3) -- not general-purpose memory, scratch space for holding a second live value across arithmetic. No dynamic addressing, no stack, no heap.
INIT nSets the accumulator to n. Must be the first line of every program -- the parser rejects anything else.ADD nacc = acc + nSUB nacc = acc − nMUL nacc = acc × nJZ labelJump to label if acc == 0. Forward-only: the target must be a strictly later instruction, or parsing fails.JNZ labelJump to label if acc != 0. Same forward-only constraint as JZ.LOAD rNacc = registers[N]STORE rNregisters[N] = accINIT 5 # starting accumulator value ADD 3 # acc = acc + 3 STORE r0 # registers[0] = acc JZ done # forward jump to a label, taken if acc == 0 MUL 2 # acc = acc * 2 LOAD r0 # acc = registers[0] done: SUB 4 # acc = acc - 4
JZ/JNZ targets are labels, resolved at parse time, and must point to a strictly later instruction. This isn't a style preference -- it's why loops aren't supported yet: forward-only jumps guarantee no instruction is ever visited twice, so the trace has exactly one row per static instruction, known at parse time. A real loop would make trace length depend on runtime behavior, which the current AIR doesn't handle. See the FAQ and the real roadmap for what changes when that's added.
The actual parser error for a backward jump: "backward or self jump to '<label>' (target <=n> <= instruction <n>): only forward jumps are supported"
Parser, execution, and every rule above: crates/zkvm-isa/src/lib.rs. More real example programs: examples/.