ADR-0008: One-step verification: instruction classes now, an SBF interpreter eventually

A one-step verifier receives the disputed instruction and the accounts it touches as Merkle witnesses. Those accounts are L2 accounts. They do not exist on Solana, they have no addresses the runtime knows, and…

Status: accepted. Dated 2026-08-26.

Status: accepted (2026-08-26) · Prompt: §6 C7, §5 D3

Context: the witnessed one-step verifier is real and measured — 19 216 CU for system transfers (svm-spike scenario M), and a second class for SPL token transfers alongside it (scenario S). Building the second class made the shape of the remaining work unambiguous, and that is worth recording before anyone plans around a wrong assumption.

The constraint nobody can design around

A one-step verifier receives the disputed instruction and the accounts it touches as Merkle witnesses. Those accounts are L2 accounts. They do not exist on Solana, they have no addresses the runtime knows, and no program owns them there.

Therefore the verifier cannot CPI into the program being disputed. There is nothing to invoke: invoke needs real accounts owned by real programs, and a witness is bytes with a proof. Every instruction class the verifier supports must have its semantics re-implemented inside the verifier program.

This is not a limitation of the current implementation. It follows from what a fraud proof is.

Decision

Support instruction classes explicitly, one at a time, and refuse everything else.

• Each class gets its own instruction on the dispute program, with the class boundary enforced in code (parse_token_account rejects delegated, frozen, uninitialized, and wrapped-SOL accounts rather than guessing at semantics it does not implement).
• Anything outside a supported class is StepNotExecutable — a rejection, never a default. Traces containing such steps fall back to the placeholder verifier and are, honestly, not yet trustlessly disputable.
• Every class carries a differential test against the real program. For SPL tokens the harness executes the batch with the actual SPL Token program and then plays an HONEST dispute game: it can only end in ProposerWins if the re-implementation reproduces the real program byte for byte. A one-unit divergence flips the verdict and fails the gate. Re-implementation risk is managed by test, not by assertion.

Classes supported today: system transfer, SPL token transfer (both in-place mutation of existing accounts — see ADR-0007 for why creation needs a different tree first).

The end state, named so it is not mistaken for the current one

General one-step verification — any instruction of any deployed program — requires executing SBF bytecode on-chain against witnessed accounts: an interpreter, with the program's own ELF supplied as part of the witness and proven against a commitment to the deployed binary. This is the well-trodden path in other ecosystems (MIPS and RISC-V interpreters serving exactly this role), and it is a large, self-contained piece of work rather than an extension of what exists.

Started, 2026-09-10: the interpreter and its one-step verifier exist as a rule

crates/solieum-sbf (adf88ba, 9b03aaf), pure and wired to nothing. Vm::root commits registers, program counter, memory and the halt flag — the state a bisection descends into. step takes exactly one instruction and leaves the machine untouched on any fault. verify_one_step takes the two roots bisection narrowed to, a machine hashing to the first, and one instruction proven out of a Merkle commitment over the instruction stream, and says whether the claimed post-state is true.

That Merkle commitment is how the ELF requirement above is met without putting an ELF in a transaction: a witness carries one instruction and its path, sixteen hashes for a 65,536-instruction program, so a whole verification is about nineteen hashes against the 700,000 CU a witnessed step is allowed. The commitment binds the instruction's index, the program's instruction COUNT (jump bounds are checked against it, so a prover free to name a different length could re-aim a jump) and its padding leaves.

It is a class, not an emulator, and that is deliberate. Division and modulo, 32-bit ALU, memory and call/syscall each fault rather than being guessed, because this interpreter and the node's execution must agree exactly and a step "verified" against semantics that differ from the runtime's would prove the wrong thing. A witness that does not hold up — including one for an unsupported instruction — decides NOTHING rather than deciding against the proposer, so an unsupported step stays opaque exactly as it is today.

The memory commitment followed (c56b6bb): a page tree of 32-byte pages at depth 59, covering the whole 64-bit address space so real SBF addresses sit where they actually are with no region map to get wrong. A proof is 59 hashes, about 9,000 CU, so a load and a store together cost roughly 18,000 of the 700,000 — which is why it is not the depth-256 account tree, whose proofs already account for most of an existing one-step's budget. An all-zero page hashes to the empty tag, so writing zeros returns the tree to its untouched state and two machines with identical memory cannot hold different roots.

That puts the 8-byte aligned load and store inside the class. Alignment is the safety property: an aligned 8-byte access always lies inside one page, so a verifier holding ONE witnessed page has provably seen the whole access. Unaligned faults rather than being split, since the second half would be in a page nobody proved; narrower forms stay out, because sub-word semantics are the kind of thing that is a consensus bug when guessed. The witnessed page must prove against the machine's own memory root before the step may read it, and a store folds back through the same proof, so a write lands where it was proven and nowhere else.

So what exists covers registers, control flow and aligned 8-byte memory access inside the supported class. A program that logs, does a CPI or otherwise reaches a syscall is still opaque.

Read before building the serialization: this node uses DIRECT MAPPING

Surveyed 2026-09-10 against solana-bpf-loader-program 1.18.26, which is what the node actually runs. The finding changes the shape of the account-witnessing step, so it is recorded before anything is built on the wrong one.

serialize_parameters is called with copy_account_data = !direct_mapping, and direct_mapping is bpf_account_data_direct_mapping in the feature set. exec.rs builds its runtime with FeatureSet::all_enabled(), so the feature is ON and account data is never copied into the input buffer. Instead:

• The input buffer carries only headers per account — duplicate marker or 0xff, the signer/writable/executable flags, four zero bytes, key, owner, lamports, data length — then MAX_PERMITTED_DATA_INCREASE (10,240) plus 16 bytes of zero realloc padding, then the rent epoch. Where the data would sit under the copying path, nothing is written.
• Each account's data becomes its own MemoryRegion, mapped at a computed virtual address and aliasing the account's real bytes — readonly, writable or copy-on-write depending on the account.
• An account with empty data gets no region at all.

Two consequences, and the first is good news:

The data the VM reads IS the account's data, not a copy. So the page tree that now commits account data (ca26aa6) is already the right commitment for those memory regions: one tree serves both the state leaf and the VM's view of it, and account data is not committed twice. That was not obvious before looking.

But VM memory is not one flat space, so committing it as one is wrong. solieum-sbf's MEMORY page tree suits the stack and heap, which are genuinely flat; the input region is a small header buffer plus a set of regions that alias account data. The memory commitment for a program call should therefore be COMPOSED — the header buffer, plus each account's existing data root — rather than a single flat tree that would copy every account into a second commitment and then have to keep the two agreeing.

What that leaves for the serialization step is the layout arithmetic: where each header sits and at which virtual address each account's data region begins, which is a deterministic function of the account set. It must be verified against the runtime rather than transcribed from it, because a verifier that disagrees with the runtime about an address disputes the wrong bytes. solana_bpf_loader_program::serialization is public and the node already depends on it, so a differential test against the real serializer is available and is the gate that step should pass before it is trusted.

The remaining pieces, in order, are that layout with its differential test, the composed memory commitment above, the dispute game instruction that calls this verifier, and only then the multi-transaction stepping the section below describes.

Measured, 2026-08-27: it costs 95 CU per interpreted instruction

The sentence above originally ended at "large piece of work", which is an estimate, so it was measured instead (programs/solieum-sbf-spike, harness scenario U). A minimal interpreter runs the same bytecode at two instruction counts and the difference cancels fixed overhead:

Marginal cost: 95.2 CU per interpreted SBF instruction ⇒ ~14,700 instructions per 1,400,000 CU transaction.

This is a floor. The spike interprets a subset with no memory, no bounds checking and no bytecode verification; every one of those omissions makes a real implementation cost more.

What the number decides. Solana meters SBF execution at roughly one CU per instruction, so a program instruction that natively costs ~N CU needs ~N interpreted instructions to re-execute. Therefore:

• A small instruction — a transfer, a simple state update, a few thousand CU natively — fits inside one transaction with margin. The interpreter path is viable for that band.
• Anything doing substantial work (an AMM swap, a large CPI chain, tens of thousands of CU natively) does not fit, and no amount of optimisation closes a 10× gap.

So an interpreter alone does not deliver "dispute any transaction". Reaching arbitrary programs additionally requires splitting one step across multiple transactions — checkpointing interpreter state (registers, pc, memory commitment) into an account between transactions so a single disputed instruction can be verified over several L1 transactions. That is a second mechanism with its own state machine and griefing surface, not a detail of the first.

Recording this now because it is the kind of finding that quietly invalidates a roadmap: the honest sequence is classes → interpreter for small instructions → multi-transaction stepping, and each stage should be justified by observed dispute traffic rather than built speculatively.

Until it is built, "Solieum can trustlessly dispute any transaction" is false, and no Solieum material may say it. What is true is stated per class, with its measured cost.

Reversal trigger

If the class-by-class path covers observed dispute traffic well enough that an interpreter never pays for itself, that is a legitimate end state — but it must be stated as such publicly (a rollup whose fraud proofs cover a subset of instructions has a subset security argument), not presented as generality. Revisit when either the second condition holds or a class outside in-place mutation becomes necessary.