[jtcoolen]

Summary

Addresses audit finding QVM-01: "Quotient-VM operand fields are bound-checked neither at run time nor by the byte validator".

Build time (fails closed) — validate_quotient_program_operands, run from LoweringPlan::validate_generator_invariants:

• every emitted memory pointer (literal, u16, token, 7-limb vector and base, pairwise span, MODARITH7 condition) is aligned and inside a window the verifier populates before the VM runs: the VK payload, the challenge blocks, and the decoded proof evaluations;
• constant slots are within the table;
• selector buckets are below the number of simple selectors, and y-power gaps are within the power table;
• the stack stays within the planned region.

The walker is total over the opcode table; a test pins this, so a new opcode that forgets it fails the render. The interpreter guards read their bounds from the same operand model.

Run time (plain revert(0, 0); rendered only inside the opcode arms that are rendered):

• FOLD needs exactly one live value;
• pops cannot go below the stack floor, and spills cannot pass the planned ceiling;
• native callbacks require an empty stack instead of resetting it;
• FOLD_SELECTOR bucket and gap are range-checked, and MODARITH7 flag bits are checked;
• the epilogue also requires q_sp == base, alongside q_pc == q_end and q_has_top == 0;
• u16 constant slots are clamped to the table length. These are only rendered when the table has more than 256 entries, and an out-of-range u16 slot can reach far outside the pinned VK data.

Measured and left out: runtime pointer clamps and u8 constant clamps.

• On the Moonlight wrap they cost about 56k and 31k gas per verification.
• In a 400-mutation experiment on the program, the coarse runtime clamps still let 261 wrong in-range operands through.
• The exact build-time checks plus the VK codehash pin are therefore the stronger layer. The rationale and numbers are in docs/reference/QUOTIENT_NUMERATOR_EVALUATOR.md ("Interpreter Bounds Checks (QVM-01)").

Ported from misc-fixes: 86b262e (clamps and stack floor), 580a912 (MF-3 only), b680bf2 (epilogue q_sp check) and 20766cb (build-time pointer windows). Their typed errors, the alpha/vk_digest binding and the precompile error split are not included.

Measurements

Moonlight wrap (Nightfall fee_12345), rendered from the committed production VKs. Settings: solc 0.8.35 via-IR, runs 200, cancun; anvil prague with the default size limit.

	main (VM)	this PR
Verifier runtime	21,214 B	21,302 B
B64 verify gas (full / padded)	1,277,190 / 1,277,178	1,278,677 / 1,278,665
B8 verify gas (full / padded)	1,277,262 / 1,277,178	1,278,749 / 1,278,665
Quotient section gas	301,746	303,233

• The VK output is byte-identical to main (same codehash), so only the verifier changes.
• 15 single-byte proof mutants are rejected on both block sizes, and the numerator and selector buckets match production on 14/14 inputs.

Fixtures (pinned solc 0.8.30):

	Runtime bytes	Verify gas
poseidon	12,674 → 12,713	636,758 → 636,300
rsa	8,901 → 8,894	593,499 → 593,504
sha_preimage	15,068 → 15,171	829,405 → 830,306
hybrid_mt	17,952 → 18,055	852,406 → 853,924
IVC decider (evaluator)	10,251 → 10,335	2,284,779 → 2,286,007

Tests

• cargo test --release --lib: 148 passed. With evm,rust-verifier-trace and HALO2_SOLIDITY_RUN_EVM_TESTS=1: 185 passed.
• Fixtures (poseidon, rsa, sha_preimage, hybrid_mt) and the IVC decider pass.
• Negative tests corrupt a fixture VK program and re-pin the codehash:
  • bucket, gap, fold without a live value, ADD underflow, native marker with a live stack, stack overflow and u16 slot each revert in revm at the named guard;
  • pointer below, above or misaligned, and a u8 slot past the table, are rejected by the build-time validator;
  • a 264-constant test circuit exercises the u16 arms.

Notes

• This overlaps with Emit an annotated listing and identity manifest for the quotient VM #11 (quotient listing) in vm/mod.rs, so whichever merges second needs a small rebase.
• This branch is based on 6b3d2096, which is not yet on main (the same base as Add opt-in direct quotient lowering for the Solidity verifier #10).

🤖 Generated with Claude Code