Emit an annotated listing and identity manifest for the quotient VM

[jtcoolen]

Summary

Adds an annotated disassembly listing and a machine-readable identity manifest to the quotient-VM output. The goal is that an audit of the generated contracts alone can see which VM bytes implement which gate polynomial, and can regenerate that view from the deployed VK bytes. The generated .sol files are unchanged.

• RenderedArtifacts gains quotient_listing: Option<String> (text) and quotient_manifest: Option<String> (JSON). Both are always produced for VM output; on Moonlight this costs about 10 ms of render time.

• Manifest. It has one entry per identity, in partially_evaluate_identities order. Each entry gives:

  • gate index, name and polynomial index, or the family (permutation / lookup / trash);
  • target bucket (simple-selector fixed column, or main) and y exponent;
  • execution kind: inline prefix, VM bytecode with its byte range, native gate callback with its index, permutation, lookup, or trash block.

  It also contains:

  • the constant table with VK payload offsets;
  • the evaluation-slot map (address → column, rotation, eval index);
  • keccak hashes of the program and the constants, and the pinned VK codehash.

  All of it comes from the existing execution_manifest / QuotientIdentitySource metadata.

• Listing. It is decoded from the final program bytes as embedded in the VK, after run compaction and packing.

  • For each VM identity: every instruction with symbolic operands (a_3_next, 2^56, r - 0x…), MODARITH7/LIN7/BILIN7/AFFINE_SUM/run opcodes expanded into their terms, and the polynomial rebuilt from the bytes.
  • For inline and native identities: the Yul the verifier contains, printed verbatim.

• Validation (fails closed). The new decoder and interpreter (vm/disasm.rs, all 31 opcodes, written from the Yul operand layouts) evaluates every VM identity at 4 random points and symbolically, and compares against Expression::evaluate of the gate polynomial. It also checks that every program byte and every identity is covered exactly once. On failure render returns GeneratorError::Planning { stage: "quotient listing" }. This is a new way for render to fail on a generator bug; valid programs are unaffected.

• Auditor tool. cargo run --example quotient_listing -- <Halo2VerifyingKey.sol|runtime.hex> <manifest.json> --listing <listing.txt> --verifier <Halo2Verifier.sol> re-derives the listing from the VK bytes and checks the hashes, the verifier's pins and anchors, and every block against the shipped listing. Exit status: 0 exact match, 2 match after a reported layout shift, 1 failure. The workflow is documented in docs/reference/QUOTIENT_LISTING.md and referenced from docs/audit/REVIEW_PACKET.md.

Tests

• cargo test --release --lib: 156 passed. With evm,rust-verifier-trace and HALO2_SOLIDITY_RUN_EVM_TESTS=1: 191 passed.

• The 12 new unit tests cover:

  • every opcode against hand-computed values;
  • the decoder against the builder after compaction;
  • identical Solidity with the listing on and off;
  • rejection of a corrupted program byte or constant, naming the identity;
  • rejection of payload drift and reserved opcodes;
  • listing blocks equal to standalone regeneration.

• tests/quotient_listing_tool.rs: an exact round trip, a reported one-word header shift, and rejection of corrupted inputs.

• Fixture results (listing produced, full coverage, validation passes, and the tool round trip passes on each):

  Fixture	m	VM identities	Program bytes
  poseidon	22	4	88
  rsa	15	0	5
  sha_preimage	35	14	411
  hybrid_mt	42	20	605
  IVC decider	49	21	4,559

• .sol byte identity: the tracked fixture dumps are unchanged, and the Moonlight B64/B8 renders are byte-identical to renders from 6b3d2096.

Moonlight wrap (Nightfall fee_12345, B64 and B8)

• Listing and manifest were produced from the committed production VKs. Each listing is about 4,000 lines.
• All 49 identities agree with an earlier audit's manifest: gate and polynomial, y power, bucket, execution kind, callback index and offsets. The 27 program stream items agree with an independent Python disassembly.
• The committed contracts were generated by bd482567, whose VK has one extra header word (the quotient certificate). The constants and commitments match word for word; the program matches once its memory pointers are shifted by one word. The tool detects this and passes the production files with exit 2, and --out writes the blocks in production addresses.

Limitations

• Validation ties the VK bytes to the Rust expressions through a Rust interpreter. The Yul interpreter's semantics are covered by the EVM tests, not by this check.
• The Yul of inline and native-callback identities is printed but not validated.
• The tool uses the crate's own decoder, so it is not independent of the generator. The gate names come from the manifest; the auditor compares the printed polynomial with the circuit source.
• The symbolic check is capped at 4,096 monomials per identity. No identity in these circuits reaches the cap.

This branch is based on 6b3d2096, which is not yet on main (the same base as #10), so it is included here.

🤖 Generated with Claude Code