[n13]

Why

Mainnet runs runtime spec 153 (chain v1.0.2-Qm). That runtime embeds the qp-wormhole 4.3.0 circuits at 7 leaves per private batch and 53 private batches per public batch. The Lean proofs do not cover those circuits today:

• main models the proof-of-burn leaf (Leaf as proof of burn: move outputs and fee to the private batch #198), which is not deployed.
• The traces recorded before that redesign only cover sizes 2 and 4, and each size is a different circuit.

This PR records the deployed sizes and ties them to the bytes on chain. The generated Lean proofs are in Quantus-Network/qp-plonky2#125.

Base branch

n13/rt153-base is fa5f57d (#194), the last commit before the leaf redesign. This is not meant to be merged into main.

Changes

• Traces: formal/traces/private_batch_wrapper_n7.json and formal/traces/public_batch_wrapper_n53.json (53 inners over 7-leaf batches), with the usual *_trace_is_current tests. check_public_batch_wrapper_trace now takes the leaf count instead of hard-wiring 2.
• Anchor: formal/deployed/*.bin are the private- and public-batch verifier and common data. generated_circuits_are_the_deployed_ones fails if this branch stops generating those bytes.
• Sizes: wormhole_aggregator::deployed::{NUM_LEAF_PROOFS, NUM_PRIVATE_BATCH_PROOFS} is the single source for 7 and 53.
• Docs: formal/SPEC.md gets a "Deployed circuits" section with the release, hashes and the commands to re-check the anchor.

How the deployed circuits were identified

1. The on-chain :code blake2-256 on mainnet equals the srtool hash of the v1.0.2-Qm release wasm. Later releases (v1.0.3 to v1.0.5) are node-only.
2. At that chain commit, Cargo.lock has qp-wormhole-* 4.3.0 and pallets/wormhole/build.rs defaults to 7 and 53.
3. Built at (7, 53), the leaf, private-batch and public-batch common.bin and verifier.bin are byte-identical between tag v4.3.0 and this branch.
4. The four files in formal/deployed/ occur verbatim in quantus-runtime-v153.compact.wasm. The leaf verifier key is a constant of the private-batch circuit, so that circuit's digest covers it.

Steps 3 and 4 can be re-run with the commands in formal/SPEC.md.

Testing

• cargo test -p qp-wormhole-aggregator --lib: 107 passed, including the six trace tests.
• cargo test -p qp-wormhole-circuit-builder: 11 passed, including the new anchor test.
• cargo clippy --workspace --all-targets --all-features --locked -- -D warnings and cargo +nightly fmt --all -- --check are clean.

Merge order

Quantus-Network/qp-plonky2#125 pins wormholeSpec at this branch's head (7c77311). After this one is squash-merged, that pin has to move to the merge commit.

[n13]

Verdict: Approve
Reviewer: GPT-6.1 Sol

Reviewed head 7c7731111d91b5d991c723030e388814792c2ad4 against base fa5f57dc1a1b755ff1b7f4fdb4309e1e06669ba2. No blocking findings.

The new traces use the production wrapper builders. The public trace correctly records 53 verifiers of the 7-leaf private wrapper, each with 162 public inputs, and 5,206 public outputs. The anchor test regenerates the actual circuit stack and compares all four verifier/common artifacts byte for byte.

Validation:

• timeout 60 cargo test --locked -p qp-wormhole-aggregator --lib wrapper_n -- --nocapture: all six trace freshness tests passed.
• timeout 60 cargo test --locked --release -p qp-wormhole-circuit-builder --lib generated_circuits_are_the_deployed_ones -- --nocapture: passed.
• cargo +nightly fmt --all -- --check and git diff --check: passed.
• Independently downloaded the v1.0.2-Qm runtime release: its compact wasm SHA-256 matches the documented 1401e066…f0d4a47c; all four fixtures occur verbatim in it. The srtool metadata confirms the chain commit and spec 153.
• Mainnet RPC at https://rpc1-mainnet.quantus.com independently returned spec 153 and :code hash 78389c85e3698b7e24cf292907f2eec0657297fd8a4d82669cf357974f15ec56, matching the release's compressed runtime hash.

GitHub format, Clippy/docs, Lean spec, and security-audit checks passed. Ubuntu/macOS workspace tests and the slow crypto job were still running at review time. Generated Lean proofs in the companion qp-plonky2 PR are outside this review.