[n13]

Why

Mainnet runs runtime spec 153 (chain v1.0.2-Qm), with the qp-wormhole 4.3.0 circuits at 7 leaves per private batch and 53 private batches per public batch. The wired capstones only existed at sizes 2 and 4, and each size is a different circuit, so the deployed ones were not covered. main has since moved to the proof-of-burn leaf, which is not deployed.

This PR proves the two wrappers at the deployed sizes. The traces and the tie to the on-chain wasm are in Quantus-Network/qp-zk-circuits#209.

Base branch

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

Result

• Plonky2Bridge.private_batch_end_to_end_wired_n7
• Plonky2Bridge.public_batch_end_to_end_wired_n53, on the recursion tree PublicWrapper53.tree over Wrapper7.tree over LeafCircuit.tree

Both depend on the standard Lean axioms plus Plonky2Bridge.proof_sound, the same single trusted axiom as before. Wrapper7.sound and PublicWrapper53.sound use standard axioms only. All five are in the CI axiom gate. Sizes 2 and 4 stay as fast regression checks.

Where to look

The diff is 450k lines, almost all generated. The hand-written part is about 700 lines:

File	Change
constraint-exporter/src/public_wrapper.rs	The public bridge generator, restructured (below). Most of the review is here.
constraint-exporter/src/private_wrapper.rs	Facts cited by name, consts reused from the decode module, heartbeat budget that grows with n³.
constraint-exporter/src/gadget.rs	rec_depth_option: maxRecDepth scaled with the longest list literal, only above 256 elements.
constraint-exporter/src/{lib,main,trace}.rs	One list of recorded sizes, PRIVATE_WRAPPER_SIZES and PUBLIC_WRAPPER_SIZES.
formal/Plonky2Bridge/PublicBatch.lean	One new generic lemma, flatten_eq_of_forall₂.
formal/Plonky2Bridge/{PrivateWrapper,PublicWrapper}.lean, formal/Plonky2Spec.lean, formal/ci/AxiomsCheck.lean	Imports, the two capstone aliases, axiom prints.
formal/PLAN.md	Step 11.
.github/workflows/ci.yml	Axiom checks for the new theorems; runner and timeout for the two formal jobs.

Generated, and reproducible with cargo run -p qp-plonky2-constraint-exporter --bin export-constraints (CI fails if they are stale):

• New: Plonky2Spec/Generated/{PrivateBatchWrapper7,PublicBatchWrapper53}.lean, Plonky2Bridge/Generated/{Wrapper7,PublicWrapper53}.lean.
• Regenerated in the new form: Plonky2Bridge/Generated/{Wrapper2,Wrapper4,PublicWrapper2,PublicWrapper4}.lean. The size-2 and size-4 decode modules are byte-identical.
• constraint-exporter/traces/*_n7.json and *_n53.json are copies of the files in qp-zk-circuits#209; the strict trace check compares them with the pinned package.

What scaling needed

The shape readers accepted both traces unchanged, including 7, the first odd leaf count. The Lean side did not scale as it was:

• Public bridge. PublicWrapper{N}.sound was one proof that projected every decode fact into its context. At 53 inners that is about 7,000 hypotheses; it held 16 GB without finishing. The generator now takes each fact from its own decode lemma and emits one lemma per inner (dummy{i}, consistent{i}, slots{i}, nulls{i}) and per reference value. sound assembles them.
• Private bridge. assumption searched the whole context for every fact. The generator now names each one.
• Limits. Row lookups by rfl and unfolding the circuit recurse once per list element, so maxRecDepth scales with the circuit. Files under the threshold are unchanged.
• Fin n matches. Lean rejects literal arms on Fin n as non-exhaustive from n = 16, so the generator emits ⟨k, _⟩ arms and an explicit out-of-range arm.

CI

The size-53 decode module peaks at 16.9 GB, which does not fit a standard 16 GB runner. The two formal jobs move to the org's 32 GB Large-Linux-x64-Runner with a 60-minute limit (was 25 and 30).

Building PublicBatchWrapper53 prints one PANIC line from Lean.LibrarySuggestions.SymbolFrequency. That is Lean's export pass for library suggestions hitting its fixed heartbeat limit on a module this size. It does not fail the build and does not touch the proofs.

Testing

Locally, on this commit:

• lake build Plonky2Spec Plonky2Bridge: 1255 jobs, no sorry.
• leanchecker on the two new decode modules: exit 0.
• The CI axiom-gate script: all 20 checks pass.
• cargo test -p qp-plonky2-constraint-exporter, including the strict vendored-trace check against the pinned package.
• cargo +nightly fmt --all -- --check.

Build cost on 18 cores: PrivateBatchWrapper7 268 s, PublicBatchWrapper53 502 s, Wrapper7 181 s, PublicWrapper53 143 s.

Merge order

wormholeSpec is pinned at 7c77311, the head of qp-zk-circuits#209. After that PR is squash-merged, the pin has to move to the merge commit before this one merges.

[n13]

Verdict: Approve
Reviewer: GPT-6.1 Sol

Reviewed head 8b2ac4436b88d4a5e1c4022e71867753d4645716 against base e0b7637f00d08995d5037aa1da490b0f26edbdf5. No blocking findings.

The public bridge split preserves dummy masking, first-real reference selection, consistency checks, and forwarding order. The new tree uses PublicWrapper53 over Wrapper7 over LeafCircuit; the existing size-2/4 theorem statements remain unchanged. The axiom gate includes both new capstones, Wrapper7.accepted_sound, and both new wrapper soundness theorems.

Validation in an isolated detached worktree:

• timeout 60 cargo +nightly test --locked --offline -p qp-plonky2-constraint-exporter: 41 passed.
• Strict vendored-trace checks: 3 passed, covering all seven traces against files extracted directly from pinned dependency commit 7c7731111d91b5d991c723030e388814792c2ad4.
• Ran export-constraints; all generated files reproduced with no diff.
• Rust formatting, git diff --check, and the formal-source placeholder scan passed.

Validation limits: Lean/Lake are unavailable locally, so I did not independently compile the proofs or execute the axiom gate. GitHub's Linux/macOS build-and-test, generation, format, documentation, and security checks passed; both formal Lean jobs remain in progress at review submission.

Keep the documented merge prerequisite: after qp-zk-circuits 0xPolygonZero#209 is squash-merged, update the dependency pin to its merge commit before merging this PR.