Before audit - code quality robustness and improvements

[jtcoolen]

Robustness & Quality Assessment and Redesign Proposals

Companion to
../architecture/ARCHITECTURE_REVIEW_2026-08.md.
Produced 2026-08-08 against the misc-fixes branch by an independent
multi-reviewer pass: nine subsystem mapping reviews, four assessment lenses
(soundness, library robustness, on-chain security, architecture quality),
and a second adversarial pass in which every finding cited below was
re-verified against the source by a reviewer instructed to refute it.
Findings are labeled Confirmed (every element checked in code) or
Partial (core claim holds; stated corrections apply). Line numbers are
as of this snapshot. As with any review, verify accuracy and completeness
against the current sources before acting on it.

1. Overall verdict

Lens	Score	Summary
Soundness of generated verifiers	8/10	No accept-invalid path or calldata malleability found. Calldata parsing is injective and fully pinned; every scalar/coordinate ingress is canonicality-checked; subgroup checking is delegated under a machine-checked coverage invariant; the quotient-VM certification chain is genuine defense-in-depth. Residual risk sits in what is assumed rather than proven (§3.2) and in assurance-process gaps (F1).
Robustness as a library	7/10	Two well-executed tiers — typed errors at the boundary, fail-closed asserts inside — that contradict each other's contracts: legal-but-unusual circuits pass try_new and then panic inside render()/encode_calldata() (F2), and per-proof encoding rebuilds the whole pipeline (F4).
Security of generated on-chain code	8/10	Precompile discipline, pinning, and fail-closed parsing are unusually strong. Must-fix hardening: the false memory-safe annotation + floating pragma with no runtime guard (F3), and dead unpinned-quotient template branches (F13).
Architecture quality & maintainability	7/10	Clean, verified macro-architecture (facade → snapshot → converged plan → declarative render). Liabilities are consistent in kind: strings and conventions doing work types should do (F7, F8, F10, F11), two oversized modules (F14), and measurable docs rot in the audit chain (F6, F15).

The failure direction is consistently crash-or-reject — the right default
for this domain. Nothing found blocks the bounded correctness claim in
docs/audit/CODEGEN_ASSURANCE_DOSSIER.md; most of what follows lowers the
cost and raises the credibility of the external audit this repo is explicitly
preparing for.

2. What is strong — and should not be redesigned

Explicit non-goals for any redesign; these choices are earning their keep:

• The narrow supported envelope and fail-fast try_new validation.
• The static absolute memory layout with the lifetime-aware overlap
  validator. (Harden its seams — F5, F9 — do not replace it with FMP-based
  allocation.)
• The compact quotient VM in the codehash-pinned VK payload, and the
  render-time certification chain: 3-stage validators, pointer whitelist,
  reference-interpreter certification at an artifact-seeded challenge,
  dual-build (recognizers on/off) agreement, and word-for-word re-comparison
  of VK-embedded program bytes. Keep vm/reference.rs deliberately
  independent of the emitter — the N-version leg is the point.
• Single converged LoweringPlan per render() call (extend it with
  caching, F4 — don't weaken it).
• Pinning by runtime length + codehash, re-checked per call.
• Templates-consume-facts and QUOTIENT_VM_SPEC as the single VM ABI
  source.
• Loud-failure test prerequisites, gas-based stage attribution in replay
  tests, and self-describing fixtures.

3. Findings register

3.1 High severity (all Confirmed)

F1 — The adversarial EVM suite is excluded from every CI workflow by the
pbt_ name filter; the CI comment claims otherwise.
.github/workflows/ci.yaml (EVM job) runs
cargo test -p halo2_solidity_verifier --release --all-features pbt_ plus the
Poseidon fixture; the default job leaves HALO2_SOLIDITY_RUN_EVM_TESTS unset
so EVM tests self-skip; the bench workflow runs only the IVC bench scripts.
Tests that therefore run in no workflow include the strongest
security-relevant negatives: every_proof_g1_rejects_noncanonical_coordinates
(src/test.rs:2868), ..._base_modulus_coordinates (:2914),
..._off_curve_coordinates (:2948),
compiled_memoryguard_does_not_overlap_generated_layout (:1441),
compiled_verifier_runtime_fits_the_eip170_limit (:1495),
batch_invert_fails_closed_on_noncanonical_words_in_all_paths (:1584),
malformed_embedded_calldata_variants_are_rejected (:1284),
vk_payload_section_mutations_are_rejected (:1349),
supported_shape_circuit_fuzz_e2e (:501), and
same_srs_distinct_shape_matrix_rejects_cross_wiring (:629). The CI step
comment explicitly claims "non-canonical scalar and G1 rejection, EIP-170
runtime size, and the memoryguard overlap check" run in that step — they do
not. A regression in any of these merges green. → Proposal P0.1.

F2 — Extensive panic surface behind the Result-typed public API.
render(), render_quotient_evaluator(), repack_proof(),
encode_calldata(), and both diagnostics route through LoweringPlan::new,
which converts every post-constructor failure into a panic
(src/lowering/plan.rs:167,183; convergence panics at
src/lowering/vk.rs:231-234,367; model validation at
src/lowering/artifacts.rs:66,296; plan validation .expect at
src/lowering/quotient.rs:469). Legal shapes that pass try_new and then
panic include: >28 distinct PCS rotation points, rotation spans >4096,
circuits whose VK payload exceeds EIP-170, and VKs with unremoved virtual
selectors — while try_new's docs promise "a typed error when the supplied
constraint system is outside the currently supported shape" and
GeneratorConfig's docs claim the constructor validates the entire shape up
front. vm/reference.rs:129-130 even documents that a malformed stream "must
surface as a GeneratorError, not a process abort," yet its only production
call site converts the Result to a panic. → Proposal P1.1.

F3 — False ("memory-safe") annotation + floating pragma ^0.8.24, with
no per-PR or on-chain enforcement of spill-window disjointness.
The terminal assembly block writes absolute addresses from 0x1000 up and
never allocates via the free-memory pointer; the annotation is documented
in-repo as "a false promise" that is load-bearing (the block does not compile
without it). Disjointness of solc's via-IR spill reservation (observed up to
0x8e0 of the 0xF80 headroom) from the generated layout is checked only by
compiled_memoryguard_does_not_overlap_generated_layout — env-gated and, per
F1, not run in CI. The floating pragma permits deployers to compile with any
0.8.x ≥ 24, unbinding the artifact from the pinned compiler the check was
measured against. Nothing at deploy or run time detects an overlap; a live
spill slot sharing bytes with the transcript buffer would corrupt verifier
state silently. → Proposal P0.2.

F4 — Every per-proof repack_proof/encode_calldata call rebuilds the
entire lowering pipeline, including an O(2^k) SRS fold and two certification
passes. src/lowering/calldata.rs:157-159 calls
self.lowering_plan().repacked_proof_layout_plan() per proof;
LoweringPlan::new runs generate_vk — whose generate_base_vk folds every
g_lagrange point to assert the SRS base (src/lowering/vk.rs:81-92; k=20
for the IVC shape) — plus both convergence loops, full VM compilation, and
both certifications. render(), proof_evaluation_counts(), and
quotient_identity_manifest() each independently rebuild the same plan;
nothing on SolidityGenerator caches it, and the doc comment states each
path builds its own plan. Cross-call consistency rests on determinism by
convention (pinned by one repeated-plan test). This is seconds of latency and
a realistic DoS surface for a service encoding many proofs. → Proposal P1.2.

F5 — Cross-phase memory-overlap soundness hangs on MemoryPhase
declaration order matching template include order, enforced only by a
comment. MemoryLifetime::intersects treats distinct Phase lifetimes as
never co-live and compares PhaseSpans with the derived Ord
(src/lowering/layout/memory.rs:192); the sync requirement with
Halo2Verifier.sol include order exists only as a doc comment
(memory.rs:121-127). A mis-ordered variant silently disables overlap
detection for the affected pair. The model's acknowledged blind spot — the
0x1000-band AccumulatorPairingBatch/FinalPairing frames — is asserted
disjoint only under cfg(test) (memory.rs:1522-1539), not in
VerifierMemoryLayout::validate(). (Correction from verification: that
specific pair is currently disjoint by construction —
FINAL_PAIRING_SCRATCH_START = PAIRING_BATCH_PTR + PAIRING_BATCH_HASH_BYTES
— so the exposure is to future edits, not the current layout.) → Proposal
P0.3 / P2.2.

---

Why F5 isn't critical: nothing is wrong at the audited commit. The enum order does match the template include order today — evidenced indirectly but strongly: the overlap validator runs on every render, the rendered-source tests pin scratch usage to registered regions, and the e2e fixtures (Poseidon, IVC k=20, Moonlight) verify real proofs on-chain, which they wouldn't if a live-range collision existed for those shapes. The verification pass also softened the known blind spot: the AccumulatorPairingBatch/FinalPairing pair isn't just "asserted in cfg(test)" — FINAL_PAIRING_SCRATCH_START is defined as PAIRING_BATCH_PTR + PAIRING_BATCH_HASH_BYTES, so that specific overlap is impossible by construction. F5 is a regression hazard: the invariant is real, currently true, and guarded by the weakest mechanism in the codebase (a doc comment).

Why it's high and not medium: the consequence class if it ever fires is the worst one. If a future edit adds a MemoryPhase variant in the wrong position or reorders a template include, MemoryLifetime::intersects starts answering the wrong question for the affected pair — and the failure mode isn't a loud error, it's the validator wrongly certifying a layout as overlap-free. A live-range collision in the generated Yul corrupts intermediate verifier state. That usually means honest proofs fail (fail-closed), but not necessarily: if the corrupted word is a challenge or the quotient eval, and the corrupting value is calldata-influenced, you're in Fiat-Shamir-weakening territory — i.e., the class of bug this finding guards against is potentially critical, even though the finding itself is not a present defect. That asymmetry is exactly why the memory planner exists at all.

The compounding interaction with F1: F5's realistic safety net today is the EVM tier — a real collision on a fixture shape would show up as a trace-differential mismatch or a failed e2e verify. But those are the env-gated tests that CI doesn't run. So the two findings multiply: a mis-ordered phase merges green through the codegen-only test job, and the check that would catch the corruption runs only when someone remembers to run it. Fixing F1 (P0.1) is half the F5 mitigation for free.

What to do with it — and why it's cheap:

• P0.3 (now, ~an hour): move the pairing-frame disjointness assertion from cfg(test) into VerifierMemoryLayout::validate() so it gates every generation, not just test builds.
• P2.2 (before the audit, small): mechanize the ordering contract — a const schedule manifest that (a) the enum order is asserted against and (b) a test extracts from rendered verifier output via per-section markers, so a reordered include or misplaced variant fails a test instead of silently disabling detection. Optionally give the 0x1000 band explicit sub-phase ordering so its aliasing becomes checkable rather than exempt-by-definition.

Audit relevance: the hand-planned absolute memory model is where all three firms will concentrate — it's the most unusual, highest-blast-radius design choice in the codebase, and "soundness-relevant invariant enforced by comment" is a textbook finding. Landing P0.3 + P2.2 beforehand converts "the overlap validator can be silently disabled by an enum reorder" from a finding they write into a control you demonstrate — and it keeps their attention on the residual questions you actually want senior auditor hours on (the reference→Yul leg and the solc spill-window assumption, F3).

---

F6 — REPRODUCIBLE_BUILDS.md's dependency-pinning claim contradicts
Cargo.toml. The doc claims "All Midfall crates are resolved from the
pinned git revision in Cargo.toml"; Cargo.toml declares only workspace path
dependencies (midnight-proofs = { path = ".." }, etc.), so published
runtime hashes are a function of the enclosing workspace checkout. Mitigating
nuance: the doc records the Midfall revision in prose, so a careful reader
can still reproduce — but the stated mechanism is false in the document that
underwrites the hashes. → Proposal P0.4.

3.2 Residual assurance boundary (documented, not a defect)

The certification chain proves the emitter → reference-interpreter leg
per render. The reference-interpreter → Yul leg rests on opcode-table
conformance tests (a case exists per opcode — not that the case body is
correct) plus native/Solidity trace differentials on fixture circuits; an
opcode no fixture emits has unverified runtime semantics. Identities executed
as inline Yul, native callbacks, or the structured tail are never lowered to
bytecode and are covered only by the trace differentials. This is honestly
documented (LOWERING_ARCHITECTURE_SPEC.md §12.1, vm/reference.rs:20-27)
— listed here because Proposal P2.5 can close most of it, and because the
trace differential that covers it is itself env-gated (F1).

3.3 Medium severity

F7 — Yul text is an internal IR (Partial — corrected). The evaluator
emits Yul strings; permutation/lookup/trash identities are re-parsed from
those strings into QuotientExpr trees by a shallow parser
(src/lowering/quotient.rs:939-945 → vm/mod.rs:1236-1279); limb7 fusion is
textual pattern-matching (quotient.rs:1172-1311); helper inclusion is
substring scanning (quotient.rs:93-118). Correction from verification: in
actual builds the parsed families become native callbacks/structured tail,
which certify_quotient_program skips (certify.rs:176-180) — interpreted
gate identities are certified against trees from typed Expression<Fq>
lowering, not the parse. Net effect stands: no check compares the parsed
trees against an independent source, so a parser bug on those families is
invisible to certification and caught only by the env-gated EVM trace
differential. → Proposal P2.6.

F8 — MODARITH7/AFFINE_SUM operand layouts hand-decoded in five Rust sites
plus the template (Confirmed, sites enumerated):
validate_quotient_const_slots (vm/mod.rs:2134-2192), the pointer walker
quotient_read_pointers (:2424-2506), the checked length walkers
(:2578-2680), the separate trusted length walkers (:3073-3105), the reference
interpreter (reference.rs:280-376, 436+), and
QuotientNumeratorBlock.yul:715-757, 896-1052. Certification cannot catch a
validator walker diverging from the emitter/reference pair. → Proposal P2.1.

F9 — Panicking "trusted" bytecode walkers are safe only under a
validate-first convention (Confirmed). quotient_op_len panics on
unknown opcodes and reads without bounds checks; the run-after-validation
convention lives in doc comments only, and one call site
(compact_quotient_runs, vm/mod.rs:1931-1983) walks builder-emitted bytes
before validation runs in finish(). → Proposal P2.1.

F10 — Injected code blocks couple to template scope by naming convention
(Confirmed). Vec<Vec<String>> Yul lines (models.rs:519-526, 635-640) are
spliced verbatim and reference template locals (r, y, delta,
quotient_eval_numer, …) with no identifier validation; only solc would
catch a mismatch. Related (Partial): models validate at construction inside
generate_*_from_plan (panicking), but render() itself does not enforce
validate_layout() — a future direct-construction call site could render an
unvalidated model. → Proposals P1.3, P2.6.

F11 — Template security behavior pinned by raw-text contains()
assertions (Partial — incident nuance). Guard tests assert substrings of
the unrendered template corpus (src/lowering/tests.rs:1624-1690).
Verification surfaced a concrete prior incident: commit 72bc1b2
(2026-07-19) fixed an always-false Yul guard in AccumulatorHelpers.yul
that left load_acc_point's if is_id branch dead while the adjacent
contains() test stayed green (the decoder remained fail-closed; no forgery
was possible — the incident shows the test style's blindness, not a
vulnerability). → Proposal P2.5.

F12 — Feature profile recorded nowhere machine-readable in artifacts
(Partial). truncated-challenges, outer-fewer-point-sets, and
outer-single-h-commitment change the proof schema the rendered verifier
expects; a mismatch fails as bare revert(0,0) (hardcoded proof-length check
or failed pairing) with no diagnostic. Correction: truncated-challenges is
human-discernible via a rendered comment; the other two leave no named trace.
Also (Confirmed): RenderDiagnostics::default() is intentionally
feature-gated, so default render shape depends on compile features.
→ Proposal P1.4.

F13 — Dead unpinned external-quotient template branches (Partial —
guards stronger than claimed). Constructors.sol:63-82 (and the two-arg
variant) render a constructor without a codehash require when
expected_quotient_codehash is None, and QuotientAndLinearization.yul
omits the pre-call codehash re-check in the same case. Corrections: the
configuration is unrepresentable through the public API (RenderQuotient has
only Inline and ExternalPinned), and the "deprecated panicking APIs"
mentioned in the spec no longer exist in source — the guards are the enum
shape plus an artifacts.rs assert. The hole-shaped template text is still
dead weight that an auditor must reason away. → Proposal P1.3.

F14 — Module hygiene: two monoliths (Confirmed). vm/mod.rs is 4,382
lines mixing the opcode ABI, builder, three validators, shape recognizers,
the Yul parser, and proof-repack layout types that belong to the calldata
boundary (RepackedProofLayoutPlan). kzg::computations is one 1,014-line
function (kzg/mod.rs:834-1847) whose trace-only q_com walk (:1226-1334)
structurally duplicates Block 5's final-MSM term enumeration (:1673-1731).
→ Proposal P2.3.

F15 — Audit-chain docs rot (Confirmed).
CODEGEN_ASSURANCE_DOSSIER.md:59-64, AUDIT.md, and AUDIT_FINDINGS.md
cite the vanished src/codegen/ tree (REVIEW_PACKET.md is current — the
audit docs disagree with each other); README carries two stale,
self-contradictory test counts (167+4 at line 49, 177 at line 389; actual at
snapshot: 202 lib + 9 integration) and a broken ./TESTING_STRATEGY.md link;
ROADMAP.md links a nonexistent ./AUDIT.md and presents fixed blockers as
open; STATUS/dossier are a dated snapshot ("suite was not rerun") with no
re-assessment trigger. → Proposal P0.4.

F16 — Diagnostics re-derivation (Partial). Public
quotient_identity_manifest re-derives gates/targets from vk.cs() without
consulting the executed plan; the plan-derived manifest exists but is
cfg(test)-only (vm/mod.rs:258-282). Correction: the selector-detection
method is identical to the plan's, not divergent as originally claimed;
ProofEvaluationCounts hand-duplicates protocol formulas with a total-sum
assert as the only cross-check. → Proposal P1.5.

F17 — Test-hygiene trio (Confirmed). (a) The bit-flip malleation PBT
reaches only the first 512 proof bytes (bit_idx ∈ 0..4096, byte 511 max;
the repacked proof is several thousand bytes — the tail G1s/q_evals/π are
never flipped by this test; scalar-sweep tests do cover deeper offsets
structurally). (b) Nine adversarial tests pass vacuously (stderr notice only)
when the accept baseline breaks, via solidity_output_is_true_or_skip
(test.rs:3411-3429); a loud variant exists and is used by the malleation
baseline. (c) The PBT runner defaults to 3 cases with
failure_persistence: None (test.rs:4295-4306); the two libFuzzer targets
are wired to no workflow. → Proposal P0.1.

3.4 Low severity (verified; batch as hygiene)

• L1 scalar_inv scratch registers 0xc0 of the historical 0x100 window;
  the 0x40 gap is unused padding but unregistered/unvalidated
  (memory.rs:700-705).
• L2 num_instances has no sanity bound on the non-accumulator path (an
  absurd value renders a verifier demanding num_instances*32 bytes of
  calldata); accumulator configs do bound it via the fixed-base tail check.
• L3 evm.rs harness: pervasive documented panics, substring parsing of
  solc's human-readable output (single-contract, trailing-newline
  assumptions), publicly re-exported behind the evm feature;
  Evm::code_size doc/impl mismatch.
• L4 Several consistency checks are debug_assert!-only and compile out
  in release (diagnostics.rs:18, calldata.rs:127, memory.rs:97-103/277,
  encoding/mod.rs:881/970, protocol/mod.rs:676, kzg/mod.rs:1117-1119);
  Constants.sol:24 unwraps expected_quotient_len inside the
  expected_quotient_codehash match arm — safe only via the artifacts.rs
  pairing invariant.
• L5 The constructor precompile smoke cannot detect a G1MSM
  implementation that omits subgroup checks (its MSM probe is identity-only;
  acknowledged in the file's own comments) — the exact property the
  verifier's soundness delegates to the precompile.
• L6 Stale NatSpec in the template and every rendered fixture/deployment
  claims generated scratch starts at 0x80; the actual base is 0x1000.
• L7 Trace renders switch the evaluator staticcall to CALL and drop
  view with no structured non-production marker (buried comments only;
  state change limited to LOG1 by the pinned callee).
• L8 Small duplications/dead code reported by reviewers: u256_string
  duplicated verbatim (yul_emit.rs:1175 / vm/mod.rs:4168), two pow5
  recognizers, dead _quotient_max_stack binding (quotient.rs:134), empty
  render/yul.rs, dead hex_padded branch and duplicate proof_len check
  in models.rs. (Note: the hardcoded 8/10 accumulator word constants in
  api.rs originally reported here turned out to have a tying test —
  lowering/tests.rs:1692-1707 — and are dropped as a finding.)

4. Redesign proposals

Ordered by (leverage ÷ risk). P0 items are small and should land before the
audit; none change verifier semantics. Items marked ⚠ change rendered
bytecode and require regenerating pinned fixtures and the
REPRODUCIBLE_BUILDS.md hashes — batch them into one regeneration.

P0 — Assurance-process fixes (small, high leverage)

P0.1 Fix CI test selection and skip semantics (F1, F17).
Enumerate the env-gated EVM tests explicitly in ci.yaml (or adopt one
enforced prefix and add a meta-test asserting the filter matches every
#[test] in src/test.rs); add a post-step check that the executed-test
count is non-zero and matches expectation so a filter regression fails
loudly. Replace solidity_output_is_true_or_skip with the existing loud
variant when HALO2_SOLIDITY_RUN_EVM_TESTS=1 (matching the suite's own
loud-prerequisite philosophy). Draw bit_idx from 0..proof_len*8. Wire the
two libFuzzer targets into a scheduled workflow with a committed corpus; give
the PBT runner a persistence file and a higher default in CI. Move the
slowest tests to the weekly workflow if per-PR time matters — but into some
workflow. Fix the misleading CI step comment. Risk: CI minutes.

P0.2 Runtime free-memory-pointer guard + pragma pin (F3) ⚠.
Emit if gt(mload(0x40), TRANSCRIPT_MPTR) { revert(0, 0) } as the first
statement of the terminal assembly block in both Halo2Verifier and
Halo2QuotientEvaluator — via-IR initializes the FMP to the memoryguard
value, so this converts the spill-window assumption into a fail-closed
on-chain check for ~10 gas per proof. Pin the pragma to the audited compiler
(or document why not). Keep the memoryguard host test and run it per-PR
(P0.1). Risk: minimal; confirm the legacy pipeline also initializes 0x40
before the block (it does).

P0.3 Promote by-construction frame checks into validate() (F5).
Move the AccumulatorPairingBatch/FinalPairing disjointness assertion from
cfg(test) into VerifierMemoryLayout::validate() so every generation is
gated on it. Cheap, generation-time only.

P0.4 One documentation-refresh pass with drift guards (F6, F15, L6).
Correct the REPRODUCIBLE_BUILDS.md pinning claim and record the workspace
commit alongside published hashes (the bench script can emit it into
contract-sizes.txt); update src/codegen paths in the dossier and audit
docs; replace README test counts with the command that produces them; fix
broken links; add status markers to ROADMAP; fix the 0x80 NatSpec ⚠; define a
re-assessment trigger (any change under src/lowering or templates/ bumps
a dated stamp). Guard recurrence with a CI link checker plus a small test
asserting every path cited in docs/audit exists. No code risk; high
audit-readiness leverage.

P1 — API contract and performance (small–medium)

P1.1 Make the lowering pipeline fallible end-to-end (F2, F9-adjacent).
The leaf validators already return Result<_, String>: change
LoweringPlan::new to try_new -> Result<LoweringPlan, GeneratorError>,
threading through generate_vk, meta_data_for_stable_static_layout,
model validation, and certification. Introduce an internal error taxonomy
{UnsupportedShape, ResourceLimit, InternalInvariant} carried in
GeneratorError::Planning so callers can distinguish rejection classes.
Keep panics only for true internal-invariant bugs, and document them under
# Panics on every public method that retains one. Honor the
reference.rs contract that certification failures surface as
GeneratorError. Risk: low functionally; moderate churn (~8 modules); keep
the current panic messages as error text.

P1.2 Cache one converged plan per generator; decouple repacking (F4).
Store OnceCell<Result<Arc<LoweringPlan>, GeneratorError>> on
SolidityGenerator (inputs are already immutable; determinism is pinned by
the repeated-plan test) and route every entry point through it — this also
structurally guarantees render/repack/diagnostics agree on one plan instead
of by convention. Additionally derive RepackedProofLayoutPlan directly from
ProofCalldataLayout::from_protocol + meta counts so per-proof calldata
encoding never needs VK generation or certification at all. Risk: low.

P1.3 Make invalid render states unrepresentable (F10, F13, L4) ⚠.
Collapse quotient_external + expected_quotient_{len,codehash} into one
Option<PinnedQuotient { frame, len, codehash }> model field; delete the
when None codehash-free branches from Constructors.sol and
QuotientAndLinearization.yul (already unreachable; removing them deletes
the hole-shaped text and the template-level unwrap()). Seal model
construction behind validating constructors (or have render() call
validate_layout() first) so an unvalidated model cannot render. Risk:
none functionally; fixture regeneration.

P1.4 Record the feature/build profile in rendered artifacts (F12) ⚠.
Emit a feature-profile constant (bitmask or three booleans + crate version)
and a NatSpec line in Halo2Verifier.sol; expose it as a typed field on
RenderedArtifacts; include it in the reproducible-builds manifest; surface
it in RepackError context so an off-chain repack against the wrong profile
is diagnosable in one step. Consider making RenderDiagnostics::default()
feature-independent (breaking change to a documented-intentional behavior —
decide explicitly). Add a CI matrix job compiling + running lib tests under
default features and each outer-* feature alone. Risk: pinned-hash
regeneration.

P1.5 Plan-derived diagnostics only (F16).
Remove the cfg(test) gate on the plan-derived manifest and implement
quotient_identity_manifest as plan.quotient_identity_parts().manifest()
via the cached plan; derive ProofEvaluationCounts from the protocol plan's
per-family counts, keeping the meta.num_evals assert as the net. Risk:
low; output shape already pinned by tests.

P2 — Structural improvements (medium–large)

P2.1 Single operand-layout descriptor + ValidatedProgram newtype
(F8, F9). Define each opcode's operand schema once (typed field sequence:
u8 const-slot, u16 ptr, counted blocks) attached to QUOTIENT_VM_SPEC, and
drive the checked length walker, const-slot validator, pointer walker, and
trusted walker from it; render the schema into the template's case
documentation so the Yul reviewer diffs against the same source. Keep
reference.rs's decoder deliberately independent (document that choice — it
is the N-version defense). Add ValidatedProgram<'a> constructible only via
validate_quotient_program, and make the panicking walkers take it. *Risk:
touches the trusted emission path; land under the existing conformance tests

• dual-build certification as the net.*

P2.2 Mechanize the MemoryPhase ↔ template-schedule contract (F5).
Introduce a schedule manifest — a const ordered list of (phase, template
partial, marker) — that (a) the enum order is asserted against and (b) a lib
test extracts from rendered verifier output (per-section markers already
exist in gas-checkpoint form; add a non-feature-gated comment marker) so a
reordered include or misplaced enum variant fails a test instead of silently
disabling overlap detection. Optionally add explicit sub-phase ordering for
the 0x1000 band so its aliasing becomes checkable rather than exempt.

P2.3 Split the monoliths; move repack types to the ABI boundary (F14).
Mechanical split of vm/mod.rs into vm/{spec,builder,validate,recognize, yul_parse}.rs; move RepackedProofLayoutPlan (and friends) to
lowering/abi/. Split kzg::computations into per-block functions sharing
one linearization-term enumeration source, eliminating the trace/Block-5
duplicate walk. Risk: low; no output change; pure pub(crate) refactor.

P2.4 Negative-conformance subgroup probe at deployment (L5) ⚠.
Embed one constant on-curve, non-subgroup G1 point in the constructor smoke
and require the G1MSM staticcall on it to fail (optionally a non-subgroup
G2 for the pairing). This makes the deployment gate test the exact rejection
behavior the runtime soundness delegates to the precompile. Generate the
constants once with a Rust-side test proving on-curve ∧ outside r-torsion.
Risk: slight deployment gas.

P2.5 Render-time differential execution of the assembled quotient Yul
(§3.2, F7, F11). Behind the evm feature (or a release-render gate),
execute the rendered quotient block on revm against a memory image generated
from QuotientRefMemory's address-derived assignment and compare -nu_y(x)
plus every selector bucket with the reference interpreter. This closes the
reference→Yul leg and covers inline/native/tail identities per artifact
instead of per fixture — converting the two weakest assurance legs into a
render gate. Complements, not replaces, the raw-text template tests (which
should migrate to rendered-output assertions where feasible). Risk: needs
the EVM harness inside generation (feature-gated); the memory image must
respect the structural constraints native kernels assume — the read-model
windows already describe them.

P2.6 Typed statement IR instead of the Yul-string round-trip (F7, F10)
⚠ (large; do last). Extend QuotientExpr into a small statement IR
(let-bindings + expression), make yul_emit::Evaluator produce it once per
identity, and derive everything from it: (a) one printer to Yul text for
inline/native blocks, (b) direct VM compilation (emit_expr already consumes
QuotientExpr), (c) limb7 fusion and pow5/helper detection as structural
rewrites/queries. Delete the assignment parser, the textual
specialize_limb7_chains matcher, one of the two pow5 recognizers, and the
substring helper-flag scan. This removes the largest class of convention
coupling and the certification blind spot at the parse seam. Risk: medium —
output text will change, churning fixtures and published hashes; stage with
output-identity checks first, then the P2.5 differential as the semantic
net.

P3 — Hygiene batch (small, opportunistic)

Bound num_instances sanely at try_new (L2); promote the
security-adjacent debug_assert!s to assert! or validate() checks —
codegen is not hot enough to care (L4); register the full scalar_inv
0x100 window or update the stale comment (L1); harden evm.rs (solc
--combined-json output instead of substring parsing, fix the code_size
doc, deduplicate the two compile/two run-tx paths) (L3); add a structured
non-production marker to trace renders (contract-name suffix or NatSpec tag)
(L7) ⚠; delete the small duplications/dead code (L8).

5. Suggested sequencing

1. Week 1 (audit-readiness): P0.1–P0.4. Nothing here changes semantics;
   P0.2 and the NatSpec fix change bytecode — do one coordinated fixture/hash
   regeneration.
2. Next: P1.2 (caching — smallest high-value code change), then P1.1
   (Result threading) since its churn benefits from the single cached entry
   point; P1.3–P1.5 ride the same fixture regeneration as P0.2.
3. Then: P2.1–P2.4 in any order (independent); P2.5 before P2.6 so the
   IR migration lands under a per-render semantic differential.

6. Verification note

This assessment was produced by automated review with per-finding
adversarial re-verification against the source; corrections discovered
during that pass are recorded inline. Findings describe the snapshot above.
Review the accuracy and completeness of both documents against the current
tree before relying on them — responsibility for verification remains with
the reader.

[jtcoolen]

Must do before engagement (P0 — days, not weeks)

These would otherwise become findings in the report, and two of them undermine the evidence you'll hand over:

• P0.1 CI fix (F1). Audit the assurance process, not just code. A dossier claiming adversarial coverage while the pbt_ filter excludes the G1-rejection/memoryguard/EIP-170 suite from every workflow — with a CI comment claiming otherwise — is a credibility hit on the whole evidence chain. They will also ask why the two libFuzzer targets run in no workflow.
• P0.2 FMP guard + pragma pin (F3). The floating ^0.8.24 pragma and the false memory-safe annotation are automatic flags static tooling (slither/semgrep) in the first week. Landing the ~10-gas runtime guard converts their finding into "already mitigated."
• P0.4 docs refresh (F6, F15). All three firms will read CODEGEN_ASSURANCE_DOSSIER.md and REVIEW_PACKET.md first — audit works methodically off supplied documentation. Audit docs citing a nonexistent src/codegen/ tree, contradictory test counts, and a false reproducibility claim waste paid hours and seed doubt about everything else.

Should do (P1 — contract fixes, ~1–2 weeks)

• P1.3 delete the dead unpinned-quotient template branches (F13). find the codehash-free constructor branch and have to reason it unreachable across two layers of Rust. Deleting hole-shaped text is cheaper than defending it.
• P1.1 Result threading (F2). The try_new-promises/render-panics contradiction is a certain finding ("library robustness / DoS"), and it touches the per-proof path.
• P1.2 plan caching and P1.4 feature-profile stamping — small, and F12 (silent prover/verifier feature mismatch) is the kind of operational-soundness issue flagged.

Bounded refactors worth doing (P2 subset)

• P2.3 module splits — mechanical, zero output change. Audits are quoted by scope and complexity; a 4,382-line vm/mod.rs and a 1,014-line function directly raise the price and slow reviewers on the most security-critical module.
• P2.1 operand-layout descriptor + ValidatedProgram newtype — reduces "five hand-decoders of the same byte layout" to a story a reviewer can check once.
• P2.5 render-time differential of the assembled Yul — this is the highest-leverage item: it closes the reference→Yul assurance leg that the spec itself admits is unverified for unexercised opcodes, turning your weakest documented gap into a per-render gate you can demo.
• P2.4 subgroup negative probe — cheap, and subgroup-check delegation is a guaranteed line of questioning.

Defer until after the audit

P2.6 (typed statement IR) — the only true "targeted rewrite" on the list. Unless the engagement is 3+ months out, don't: it churns the exact code being audited, invalidates fixtures/hashes, and its risk (the parse-leg blindness) is largely mitigated by P2.5 at a fraction of the diff. Same for the P3 hygiene batch except items tooling will trip on.

One process point: freeze the tree 2–4 weeks before the start date, regenerate fixtures/hashes once (P0.2, P1.3, P1.4 all change bytecode — batch them), and pin the audit commit in REPRODUCIBLE_BUILDS.md. Everything above P2.6 fits comfortably before a freeze on a normal lead time.

[jtcoolen]

 Audit-Readiness Plan — proofs/solidity-verifier (Trail of Bits / Kudelski / ZkSecurity)

 Context

 The crate is a halo2→Solidity verifier code generator (Midfall/Midnight KZG proofs on BLS12-381), produced in a rushed ~2-week AI-assisted translation of the Rust verifier on top of an existing Solidity verifier-codegen base. Three audit firms engage in ~4–8 weeks. Two review docs produced 2026-08-08 against this exact tree (docs/architecture/ARCHITECTURE_REVIEW_2026-08.md, docs/plans/REDESIGN_PROPOSALS_2026-08.md) provide a verified findings register (F1–F17, L1–L8) and prioritized proposals (P0–P3). This plan turns those into an executable program plus the owner's additional goals: familiarity, robustness, stale-doc removal, minimal code surface, and a clear supported-subset statement in doc and code.

 Decisions made with the owner:
 - Timeline: 4–8 weeks → everything through P2.5 fits; P2.6 (typed IR) deferred until after the audit; freeze the tree 2–4 weeks before the start date.
 - Deletions: aggressive — delete Tier-A docs, demo scripts, orphaned fixtures; keep deployments/ (honest on-chain provenance record); move historical AUDIT.md → docs/audit/history/.
 - Feature flags: keep all; stamp the profile in artifacts (P1.4) + CI feature matrix; supported-subset doc scopes the production profile (truncated-challenges ON, outer-* OFF).
 - Support claim: envelope + evidence — supported = any circuit whose compiled constraint system fits the validated envelope and hard limits; exercised shapes listed as evidence, not the boundary.

 Ground truth added by recon (2026-08-08, HEAD 4ae8053, clean tree)

 All review-doc findings reconfirmed; recon added:
 - scripts/check_release_bytecode_sizes.sh:49-50 hard-codes hashes matching neither REPRODUCIBLE_BUILDS.md table; it never checks Halo2QuotientEvaluator (23,221 of 24,576 B — closest to EIP-170); the bench-workflow comment claiming doc validation is false.
 - 32 of 40 compiled src/test.rs tests run in no workflow; 4 of 7 integration test files run nowhere; tests/ivc_accumulator_replay.rs needs no SRS yet isn't in per-PR CI.
 - fixtures/poseidon/ (18 files) + fixtures/rsa_signature/ (3 files) orphaned; REVIEW_PACKET.md:67 cites a nonexistent (pre-import) commit; fixtures/moonlight-wrap/README.md:17 provenance off by one commit.
 - Docs: 44 md files / 30,862 lines (more than src/); MIDFALL_PROOFS_COMMENT_CORPUS.md alone is 10,966 machine-generated lines.
 - Design-pass corrections to the review docs: Constructors.sol:63-82 is NOT wholly dead (only the inner when None codehash arms are); the evaluator FMP-guard bound must be a new SCRATCH_FLOOR_MPTR (= LOW_MEMORY_SCRATCH_START 0x1000) since TRANSCRIPT_MPTR doesn't exist there; a Solidity internal constant that's never read is optimized out, so the feature-profile constant must be public; DEFAULT_OPTIMIZE_RUNS is used internally — only its lib.rs:63 re-export is dead; the two pow5 recognizers operate on different IRs and are NOT unifiable without output change (that's P2.6 — defer).

 ---
 WS0 — Render-snapshot net (do first, ~100 LoC)

 No plain-cargo test check pins rendered bytes across commits (standard_plonk_render_is_deterministic_for_same_seed only proves self-determinism; the ivc replay executes fixtures but never diffs them against fresh renders). Add render_snapshot_guards_refactors to src/lowering/tests.rs: render all three artifacts for 2–3 in-repo circuits (reuse lowering_plan_test_vk + one lookup/trash-bearing circuit), assert Keccak256 of each rendered string equals a committed constant (feature profile in the constant name). This is the acceptance gate for every no-output-change item (WS3, WS4); WS2 regenerates the constants once in its regeneration commit.

 WS1 — CI / assurance process (P0.1, F1, F17) — first PR, protects everything else

 Selection mechanism: enforced prefix + meta-test (YAML enumeration rots like the docs did):
 - Rename the 32 unexecuted env-gated tests in src/test.rs to evm_*; keep pbt_* (8); trace tests selected by exact name go on an allowlist const.
 - New host-only meta_ci_filter_selects_every_env_gated_test: include_str!("test.rs"), detect gating by gate-helper references (HALO2_SOLIDITY_RUN_EVM_TESTS, poseidon_inputs_available_for_evm, …; assert the helper names still exist), assert gated ⇒ prefixed/allowlisted, ungated ⇒ unprefixed, plus expected totals. Runs in the plain per-PR job.
 - New scripts/ci_run_gated_tests.sh: --list → expected count (assert >0) → run → assert N passed == expected.

 .github/workflows/ci.yaml:
 - test-solidity-verifier-evm: replace the pbt_ filter (line 225) with the script (pbt_ evm_); POSEIDON_PBT_CASES: 8; add --test ivc_accumulator_replay step (no SRS; only executed coverage of AccumulatorHelpers.yul decode guards); delete the false comment at :221-223. ~25–40 min; timeout-minutes: 60; shard pbt_|evm_ if needed — never drop coverage.
 - New test-solidity-verifier-features matrix (lib tests): "", truncated-challenges, outer-fewer-point-sets, outer-single-h-commitment, in-circuit-fewer-point-sets, evm,truncated-challenges.
 - New per-PR docs-links job: lychee offline over crate md (pinned action SHA); external URLs weekly only.
 - New solidity_verifier_weekly.yml: deep PBT (POSEIDON_PBT_CASES: 64); heavy fixtures (sha_preimage k=13, rsa_signature k=12, hybrid_mt k=13 — currently run NOWHERE); fuzz job (cargo-fuzz, -max_total_time=1800 per target, committed seed corpora under fuzz/corpus/, crash artifacts uploaded + fail); doc-staleness soft guard (WS5).

 Test-code fixes (same PR):
 - solidity_output_is_true_or_skip (src/test.rs:3411): when HALO2_SOLIDITY_RUN_EVM_TESTS is set, delegate to the loupath — un-silences all 9 adversarial skips at once.
 - PBT runner (src/test.rs:4297): FileFailurePersistence into committed proptest-regressions/.
 - Bit-flip strategy (src/test.rs:1214): any::<prop::sample::Index>() resolved against proof.len()*8 (today only the are reachable).

 Doc guards: new tests/docs_paths.rs (host-only, per-PR): every backtick path cited in README + docs/audit/*.md (excTED_CIRCUITS.md exists in-tree; ships with a shrink-only allowlist that must be EMPTY after WS5 Tier C.

 WS2 — Bytecode-changing batch (P0.2, L6, P1.3, P1.4, P2.4 + hash single-source) — ONE PR, ONE regeneration

 Each step passes the local gate: cargo test -p halo2_solidity_verifier + HALO2_SOLIDITY_RUN_EVM_TESTS=1 cargo test .

 0. De-risk day 1: pinned solc 0.8.30, SRS 2p19/2p20 (+2p22 for single-H), and verify the Moonlight sibling checkoutcherry-picks + [patch] block per fixtures/moonlight-wrap/README.md:31-43) still builds. The batch must not merge ifthis has rotted.
 1. P1.3: collapse quotient_external/expected_quotient_len/expected_quotient_codehash (models.rs:516-518) → Option<Ptime_len, codehash }>; delete only the dead inner arms (Constructors.sol:29-30, :35-38, :68-76 else-arm, :78-81;QuotientAndLinearization.yul:25-26; Constants.sol:27-28) + the Constants.sol:24 unwrap; delete the two now-unrepresentable asserts (artifacts.rs:81-89); add render_validated() (validate_layout → render) as the only path builder/render.rs calls. The
 4-constructor structure survives (count-of-4 pin, lowering/tests.rs:1483-1487).
 2. Pragma pin =0.8.30: 3 templates + inline test contracts (src/test.rs:77, :1553); new non-gated PINNED_SOLC_SEMVER const composed into both the template pin test and evm.rs::PINNED_SOLC_VERSION; document that HALO2_SOLIDITY_ALLOW_UNPINNED_SOLC can no longer
 swap 0.8.x (intended fail-closed, F3).
 3. FMP guard + L6: new VerifierMemoryLayout.scratch_floor_mptr (= 0x1000) + validate() invariant "no region below floor"; render SCRATCH_FLOOR_MPTR into both constant blocks; if gt(mload(0x40), SCRATCH_FLOOR_MPTR) { revert(0, 0) } as first statement of both
 terminal blocks AND of require_eip2537_precompiles(). Fix the 0x80 NatSpec lies + docs/MEMORY_LAYOUT.md path (leave— its 0x80 is true). Tests: guard-text pin; mutation testfmp_guard_reverts_when_scratch_floor_is_below_solc_reservation (floor→0x20, compile, assert revert — proves the guard is live; the 72bc1b2 lesson); strengthen compiled_memoryguard_… to assert runtime_free_memory_pointer_init(runtime) ≤ floor == 0x1000
 (src/evm.rs:248).
 4. P1.4 stamping: FeatureProfile in src/api.rs (current() from lib.rs consts, bits(), Display); RenderedArtifacts.feature_profile; profile context in RepackError::LengthMismatch; uint256 public constant CODEGEN_FEATURE_PROFILE (bit0 truncated-challenges, bit1
 outer-fewer-point-sets, bit2 outer-single-h) + NatSpec header line with crate version; contract-sizes.txt gains coderDiagnostics::default() STAYS feature-dependent (documented-intentional; F12's real gap was discoverability).Diagnostics features excluded from the bitmask.
 5. P2.4 negative subgroup probe: hardcoded on-curve non-subgroup G1+G2 constants on Eip2537TemplateConstants; two rnded to require_eip2537_precompiles() (G1MSM on non-subgroup G1 must fail; PAIRING with non-subgroup G2 must fail —EIP-2537 mandates subgroup checks there). Proof tests: on-curve via G1ADD identity; non-torsion via [r]P ≠ O computed by G1ADD double-and-add (independent of G1MSM); liveness test swaps in the generator and asserts constructor revert.
 6. Hash single source of truth (reconciled across workstreams — ONE mechanism): new scripts/release-bytecode-expect × runtime_bytes × keccak256, emitted by the bench flow from contract-sizes.txt); check_release_bytecode_sizes.sh reads it (drops the stale :49-50 hard-codes, adds the missing Halo2QuotientEvaluator size+hash checks); always-run lib test reproducible_builds_doc_and_release_expectations_agree asserts REPRODUCIBLE_BUILDS.md tables == TSV; fix the false comment at
 solidity_verifier_bench.yml:60-62.
 7. THE regeneration (one commit): fixtures/ivc (HALO2_SOLIDITY_RUN_IVC_BENCH=1 … --test ivc_keccak_solidity, copy from target/ivc-keccak-solidity-dump/); fixtures/moonlight-wrap from the Moonlight checkout run (fixes the off-by-one provenance stamp); run both
 bench profiles → fill TSV + rewrite REPRODUCIBLE_BUILDS tables; refresh WS0 snapshot constants. Never touch deploymits 0x80 NatSpec is accurate for what's on-chain).
 8. Post-regen: full gate + both fixture replays + check_release_bytecode_sizes.sh both profiles + doc-sync test.

 Risks: dead-guard text (mutation test), evaluator EIP-170 headroom (now checked), Moonlight rot (step 0), CI hash gate (single PR carries code + fixtures + TSV together).

 WS3 — Rust robustness (P1.2 → P0.3 → P1.1 → P1.5) — no rendered-output change (WS0 is the gate)

 A. P1.2 plan caching + VK-free repacking (~300 LoC, do first):
 - OnceLock<Result<Arc<LoweringPlan>, GeneratorError>> on SolidityGenerator (OnceLock not OnceCell — the generator i so); pub(crate) fn plan(); route render/render_quotient_evaluator/repack/encode_calldata/both diagnostics through it.Pin caching with an Arc pointer-equality assert in lowering_plan_reuses_stable_layout_facts.
 - Repack decoupling: RepackedProofLayoutPlan needs only commitment_read_groups() + num_evals + num_point_sets; add ummy-query math mirrors meta_data_for_vk, gated on outer-fewer-point-sets), generic-core refactor ofcompute_dummy_queries/construct_intermediate_sets_impl over commitment-identity keys (verified: eval words never affect counts). Mandatory cross-check: plan invariant validation asserts proof_wire_counts == (meta.num_evals, meta.num_point_sets) — the duplicate
 derivation becomes a checked invariant. Per-proof encoding drops from seconds (O(2^k) SRS fold + 2 certifications)  DoS surface.

 B. P0.3 (~30 LoC): drop #[cfg(test)] from MemoryMap::region() (memory.rs:262-266); in VerifierMemoryLayout::validat()? (:1149), require both regions registered (fail closed) and batch.start+len ≤ final_pairing.start, reusing thetest's message text (:1530-1539).

 C. P1.1 Result threading (~600–800 LoC, after WS2 to avoid artifacts.rs churn collisions):
 - PlanningErrorKind { UnsupportedShape, ResourceLimit, InternalInvariant } on GeneratorError::Planning; LoweringPlary_generate_vk, meta_data_for_stable_static_layout, both generate_*_from_plan, builder/*;proof_evaluation_counts/quotient_identity_manifest become Result (one public break together with C/D). Keep panic messages verbatim as error text.
 - Per-site dispositions (full verified table in the WS3 design): Err — plan.rs:167 (InternalInvariant; ResourceLimiplan.rs:183 (honors the reference.rs:129-130 contract), vk.rs:87-92 SRS base (UnsupportedShape — reachable callerinput), vk.rs:154/:176/:243, vk convergence :231/:367 (ResourceLimit), vk.rs:291 EIP-170 (ResourceLimit), artifacts.rs:66/:296, quotient.rs:469. Keep-panic + # Panics docs — pure internal-consistency asserts (vk.rs:250-274, abi/proof.rs drift asserts,
 encoding/mod.rs:514, artifacts acc-count asserts). New try_new pre-checks (UnsupportedShape/ResourceLimit): virtualet, rotation-span cap (expose rotation_walk_steps from PcsMemoryRequirements), theta-window caps compared beforevalidate().
 - New negative tests per Err class; existing negatives keep passing (messages preserved).

 D. P1.5 plan-derived diagnostics (~150 LoC, net negative): un-cfg the vm manifest (vm/mod.rs:257-296) as the singleidentity_manifest = plan-derived via the cache (delete the cs-re-derivation in diagnostics.rs:74-187);ProofEvaluationCounts from protocol per-family counts, keeping the num_evals assert as net. Output pinned by lowering/tests.rs:1250 + two integration tests; add old-vs-new equality test on a lookup+trash+selector circuit.

 WS3 owns updating SUPPORTED_CIRCUITS.md §4's Behavior column when C lands.

 WS4 — Module splits + reduction (P2.3, P2.1, dead code) — no rendered-output change

 Order: deletions → splits → operand schema (deletions shrink what moves; schema lands in the post-split files).

 - Dead code (~−100 net): empty render/yul.rs + decl; models.rs:787-793 duplicate proof_len check; models.rs:934-936 dead hex_padded branch; quotient.rs:134 dead binding; DEFAULT_OPTIMIZE_RUNS re-export only (const is used); u256_string dedupe; UsedQueries
 (protocol/mod.rs:182-250) → test module; evm.rs hygiene (rename pub(crate) mod test → mod harness keeping lib.rs rethe 9 consumers don't break; fix code_size doc; #[doc(hidden)] the pub use revm). pow5 recognizers + helper-flagdetectors: keep both, add cross-referencing comments (unification = P2.6, deferred).
 - P2.3 splits (~5,400 LoC moved, ~300 real): vm/mod.rs → vm/{isa,builder,shapes,validate,parse}.rs along the verifis plan/expr types + re-exports so no external call site changes; RepackedProofLayoutPlan/ScalarLayout → newsrc/lowering/abi/repack.rs (kills the 4-hop re-export chain); kzg::computations → 6 per-block fns along the existing blocks.push seams + shared linearization_msm_terms() enumerator consumed by both the trace walk (:1226-1334) and Block 5 (:1673-1731), keeping
 the pair_idx assert as net; extract kzg/coverage.rs (TrackedG1 G1-coverage validation). Pure-move commits reviewed nce.rs/certify.rs untouched (N-version independence).
 - P2.1 operand schema + ValidatedProgram (~600 LoC): OperandLayout per opcode attached to QUOTIENT_VM_SPEC in vm/isa.rs; one schema interpreter (checked + trusted flavors) drives the four walkers (checked length, const-slot, pointer, trusted); reference.rs
 stays hand-written with a comment naming it the deliberate N-version leg. ValidatedProgram<'a> constructible only vam; finish() validates the pre-compaction stream first (fixes F9's compact-before-validate). In-template schema docswould change bytes — instead a conformance test asserts rendered case set/order matches the schema now; template docs ride a future regen batch. Property test: random schema-assembled programs round-trip checked == trusted == reference lengths.

 WS5 — Docs overhaul + reduction (P0.4, F6, F15): 44 files / 30,862 lines → 25 files / ~13.5k

 Order: guards permissive → Tier A → Tier B → WS6 doc lands → Tier C (pointers need a target).

 - Tier A delete (~−14k lines + 1,400 script lines): MIDFALL_PROOFS_COMMENT_CORPUS.md, spec-migration.md, SPLIT_NWAY_NOTES.md, PORTING_NOTES.md, IMPROVEMENTS.md, MIGRATION.md, TEAM_DEMO_SETUP.md; scripts run_team_demo.sh, extract_midfall_comments.py,
 deploy_moonlight_sepolia.sh, prove_and_verify_moonlight_sepolia.sh; orphaned fixtures/poseidon/ + fixtures/rsa_signdit/history/ with a frozen banner, excluded from guards. deployments/ stays + one banner line pointing atfixtures/moonlight-wrap as canonical.
 - Tier B merges: benchmarks 5→1 (BENCH.md + dated appendices); quotient docs 4→1 (QUOTIENT_NUMERATOR_EVALUATOR.md a plans, ARCHITECTURE.md, and the 9KB narrative); optimization plans 3→1 (OPTIMISATIONS.md, every itemDone/Open/Rejected); the twin 16-section checklists get ONE home — docs/audit/TESTING.md (moved from reference/), absorbing surviving open items from the 2,593-line TESTING_STRATEGY.md.
 - Tier C refresh: DOSSIER (5 dead src/codegen paths :59-64 → real owners; stale pinned rev :36); REVIEW_PACKET (:67ad in this order" map for the three firms); AUDIT_FINDINGS (paths + old repo name); README (test counts → the commandsthat produce them; broken link; full 7-file integration inventory); ROADMAP (mark all 7 "production blockers" FIXED with commit refs — each verified done; absorb STATUS.md as a stamped status header); moonlight-wrap README provenance fix (in WS2's regen).
 - Staleness convention: every audit-facing doc gets Assessed-at / Assessed-commit / Re-assess-when headers; weekly templates changed AND the stamp is >90 days old.
 - REPRODUCIBLE_BUILDS: rewritten around the WS2 TSV (tables asserted equal by the lib test); the false pinning claim corrected to the truth (workspace path deps + [patch], pinned by the recorded workspace commit).

 WS6 — Supported-subset statement (owner's explicit priority)

 New docs/SUPPORTED_CIRCUITS.md (~350 lines), the single authoritative envelope doc: (1) authority statement + assessed-at header; (2) support model — "gadget-agnostic: a circuit is supported iff its compiled constraint system satisfies this envelope; gadget
 lists are evidence, not the boundary"; (3) typed-error envelope (try_new checks, builder/api.rs:33-115 + the 20 Proants by category); (4) hard-limits table with stable id column (rot points ≤28, x1 powers ≤65, q_eval sets ≤56,rotation span ≤4096, VK EIP-170, convergence caps; enforced-at path; honest "Behavior today: panic → typed error after WS3-C"); (5) implicit unchecked assumptions (chunk_len = degree−2, num_quotients = degree−1 or 1, rotation_last = −(blinding+1)); (6) feature
 profiles + production profile + the prover/verifier matching requirement (mismatch ⇒ fail-closed rejection with no 4 stamp); (7) exercised shapes as EVIDENCE (Poseidon k=6, SHA-256 k=13, RSA k=12, hybrid MT k=13, IVC decider k=19/20+ 7×56 accumulator, Moonlight wrap point_pair, 7-axis shape-fuzz matrix k=5 — each with test file + CI tier); (8) never-exercised upstream families (sha512, ripemd160, keccak-in-circuit, blake2b, jubjub, secp256k1, foreign-field/ECC, hash-to-curve, base64,
 automaton, map, vector, zkir, light_aggregator); (9) non-goals; (10) enforcement + change process.

 Code side: new public src/supported.rs — definition point for the limit constants (move ROT_POINTS/X1_POWERS/Q_EVAL/mod.rs:604-608, MAX_ROTATION_WALK_STEPS from kzg/mod.rs:917, EIP_170_MAX_RUNTIME_BYTES from models.rs:284; re-exportthe scattered SUPPORTED_*), rustdoc linking the doc; doc-sync test supported_doc_limits_match_constants parses the md table by id and asserts values == constants; GeneratorError rustdoc points at the doc; try_new gains the L2 num_instances sanity bound (typed
 error). The four existing partial envelope statements (README, LOWERING_ARCHITECTURE_SPEC §2, HALO2_MIDNIGHT_VERIFI§1) become ≤2-line pointers.

 WS7 — P2.5 render-time differential of the assembled quotient Yul (~450 LoC)

 Key insight: the standalone Halo2QuotientEvaluator IS the assembled quotient Yul behind a raw-frame ABI (calldata =turn = [magic, -nu_y(x), selector buckets]) and includes the same QuotientNumeratorBlock.yul as the inline path — soexecuting it covers inline-prefix, VM-interpreted, native-callback, AND structured-tail identities per artifact with no new Yul wrapper.
 - New src/lowering/quotient_numerator/differential.rs (#[cfg(feature = "evm")]): build an address-resolved memory is at vk_mptr so the VM reads its genuine tables; seed-derived words for every other frame address, tokens resolvedthrough plan.quotient_read_model().token_bases; read-model windows are exactly what generated code may load, and native kernels are straight-line Fr arithmetic over those slots, so random values are valid); oracle folds every identity in y-batch order via
 QuotientProgramPlan::execution_manifest() (every identity carries its expr, including native/tail); render evaluatoy on the existing Prague/blst Evm, call the fallback with the frame, assert magic + -nu_y(x) + every selector bucket.
 - Exposure: (a) wired into the evm-feature suite for every fixture circuit + the lowering-test corpus; (b) opt-in SolidityGenerator::certify_rendered_quotient() behind evm for release pipelines. NOT inside render() unconditionally (needs solc + revm). Budget:
 ~1–3 s compile + sub-second revm call per artifact. This closes the reference→Yul leg the spec admits is unverifiedassurance gap becomes a demoable per-artifact gate.

 ---
 Sequencing (calendar, 4–8-week runway)

 ┌──────────────────────────────┬───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │             When             │                                                                                     Work                                                                                                                │
 ├──────────────────────────────┼───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
 │ Week 1                       │ WS1 (CI PR) · WS0 snapshot net · WS2 step 0 de-risk (solc/SRS/Moonlight checkout) tions · WS3-A (plan caching) + WS3-B (P0.3)                                                                           │
 ├──────────────────────────────┼───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
 │ Week 2                       │ WS2 batch (steps 1–6) → regeneration (step 7–8) · WS5 Tier B merges in parallel                                                                                                                         │
 ├──────────────────────────────┼───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
 │ Week 2–3                     │ WS3-C (Result threading) + WS3-D (diagnostics) · WS6 doc + src/supported.rs (Behav WS3-C)                                                                                                               │
 ├──────────────────────────────┼───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
 │ Week 3–4                     │ WS4 (deletions → splits → operand schema) · WS5 Tier C refresh (pointers now have ) · WS7 differential                                                                                                  │
 ├──────────────────────────────┼───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
 │ Freeze (2–4 wks before       │ Re-run both bench profiles; verify TSV/doc/fixtures agree; pin the audit commit inREVIEW_PACKET; tag; auditor dry-run: cold-read REVIEW_PACKET → DOSSIER → SUPPORTED_CIRCUITS → TESTING with zero dead  │
 │ start)                       │ paths                                                                                                                                                                                                                             │
 └──────────────────────────────┴─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

 Deferred until after the audit: P2.6 (typed statement IR — churns the audited code, largely mitigated by WS7), pow5remaining P3 hygiene not tripped by tooling.

 Net surface reduction: docs −~17k lines (44 → 25 files), scripts −1,400 lines, 21 orphaned fixture files gone, deadlines, vm/mod.rs 4,382 → 5 files none near the old size, kzg::computations 1,014-line fn → 6 block fns, and theper-proof encode path drops its O(2^k) rebuild.

 Verification (end-to-end)

 1. Per-refactor: WS0 snapshot test green on every WS3/WS4 commit; full local EVM gate (HALO2_SOLIDITY_RUN_EVM_TESTS=1 … --features evm) at each WS2 step.
 2. CI proves itself: deliberately rename one gated test → meta-test fails; break the accept-baseline with env set →ing adversarial" lines in green logs); mutate one TSV hash byte → bench check fails and names Halo2QuotientEvaluator;-- --list count == passed count on green runs.
 3. Guards prove live, not textual: FMP-guard mutation test (floor→0x20 ⇒ revert); subgroup-probe liveness test (swaor reverts); non-torsion proof via G1ADD double-and-add.
 4. Docs: lychee green; tests/docs_paths.rs allowlist empty; find docs -name '*.md' | wc -l == target; supported_doc_limits_match_constants fails when a constant changes without a doc edit (rehearse once); every audit-facing doc carries fresh Assessed-at
 headers.
 5. WS7 demo: run certify_rendered_quotient() on the IVC artifact and show the differential passing — the concrete answer to "how do you know the rendered Yul computes the same quotient as the reference?"
 6. Fixture replays exercise current codegen: post-regen, both ivc_accumulator_replay arms replay freshly-provenance
                                                                                                                                                                                                                                                             Key files
                                                                                                                                                                                                                                                             src/test.rs, .github/workflows/{ci.yaml,solidity_verifier_bench.yml,+weekly}, scripts/{ci_run_gated_tests.sh,check_release-bytecode-expected.tsv} · templates: Halo2Verifier.sol, Halo2QuotientEvaluator.sol,partials/verifier/{Constants,Constructors,PrecompileSmoke}.sol, QuotientAndLinearization.yul · src/lowering/{plan.rs,vk.rs,artifacts.rs,quotient.rs,calldata.rs,diagnostics.rs,layout/memory.rs,kzg/mod.rs,render/models.rs,quotient_numerator/vm/mod.rs} · src/{api.rs,supported.rs(new),builder/*} · docs/SUPPORTED_CIRCUITS.md(new), docs/audit/*, docs/reference/REPRODUCIBc,moonlight-wrap}/.

[jtcoolen]

The verdict

The architecture is sound where it faces the chain and misaligned where it faces the auditor. The deployed artifact — three-contract split, STATICCALL boundary, INVALID-prefixed VK, per-call codehash re-pinning, exact-size calldata discipline, static 0x1000 layout, canonicality checks on every ingress — is better defended than most hand-written verifiers these firms review. The on-chain VM survives scrutiny: the measured alternative was ~107KB of straight-line Yul across 16 helper contracts, so interpretation is forced by EIP-170, not a stylistic choice.

The central flaw is one misallocation with four faces: your best verification machinery is anchored one level below where the risk lives. N-version certification triple-checks the expr-tree→bytecode encoder — the component least likely to hold a protocol bug — while the facts that define the verified statement exist only as template text and emitter strings, coupled by comments, and checked per-render by nothing.

Four root causes (these explain nearly all 30 findings)

1. Protocol semantics live as text, not data. The Fiat-Shamir absorb/squeeze schedule — the fact that defines what statement is verified — has four hand-mirrored implementations: the template's control flow, the buffer-sizing formula, the repacker's ordering, and the native verifier. The hand-written transcript-buffer bound has already been wrong once for a legal multi-phase shape, and an overrun overwrites VK words mid-verify — a shape-dependent soundness failure fixture sampling structurally can't see. Worse: temporal FS constraints (each challenge squeezed after everything it must bind — the Frozen Heart class) are represented nowhere and checked by nothing.

2. Certification is anchored at the encoder, below the translation risk. There's no kzg/reference.rs — the entire 1,014-line multi-open scalar pipeline's correctness argument is "mirrors multi_prepare" in comments. The routing knapsack sends the heaviest gates to native Yul, which certification skips by construction. The reference interpreter rejects FOLD opcodes rather than implementing them, so y-fold arithmetic is never checked by value. And the accumulator limb decoder — the most intricate bijectivity argument in the system, with a real prior incident (the 72bc1b2 dead guard) — has no reference implementation at all. As the assurance critic put it: the hand-mirrored PLONK formulas are the one thing a two-week AI-assisted port is most likely to get wrong, and nothing at render time ever evaluates them.

3. Address space is the universal interface, bound too early. VM operands carry absolute EVM addresses, so program bytes depend on VK length which depends on program size — and a third of the machinery an auditor must trust (both panic-on-non-convergence loops, the 200-line pointer whitelist, the word-for-word VK re-comparison) exists only to police that self-inflicted circularity. It also means the evaluator's frame ABI ships the executable VM program through the caller's memory, making the deployed evaluator an open bytecode-interpreter endpoint whose inertness rests on an unstated invariant.

4. Trust anchors and evidence are human-carried. The single most security-critical constant — the pinned evaluator codehash — is caller-supplied and trusted verbatim, while the VK hash is generator-computed. The "magic word" NatSpec sells a version guard that is actually one crate-wide constant. The rebuild-grade spec contradicts the code on the transcript-buffer base (0x80 vs 0x1000). Forty anonymous revert(0,0) sites make guard coverage unmeasurable in principle. Every render re-proves a once-per-SRS constant with an O(2²⁰) fold, which cascades into the 300MB regeneration prerequisite and the out-of-repo Moonlight dependency.

The better architecture

Keep the macro-shape — facade → lowering → render, three contracts, the VM, the static layout, the pinning. Re-anchor what the trusted base is, in six layers:

• L1 — Protocol facts as data: a TranscriptSchedule (typed event list: absorb/squeeze/truncate) and PcsFoldPlan derived once from ProtocolPlan. The buffer bound becomes a fold over events instead of a hand formula; a ~40-line challenge-dependency table makes the Frozen Heart class a codegen failure; the coverage invariant's absorbed side becomes schedule.g1_slots() instead of a hand mirror.
• L2 — One oracle, total differential: a small address-free ProtocolOracle evaluating all identities from one cited transcription of the formulas; kzg/reference.rs for the PCS blocks; a Rust reference decoder for the accumulator; every execution representation (inline/VM/native/tail) differentially executed against it per render. This is your existing certify.rs pattern aimed at the right level.
• L3 — Late address binding: window-relative VM operands ((window_tag, u16) over the four read-model windows — the escape hatch already exists in embryo as memory tokens). Compile once, place once; both convergence loops, the pointer walker, and the re-comparison get deleted, not maintained.
• L4 — One implementation per fact: typed identity constructors + a single printer (P2.6 re-scoped); the parser-of-own-output and the textual limb7 matcher die; walkers generated from one operand schema; the reference decoder stays hand-written as the deliberate N-version leg.
• L5 — Machine-emitted evidence: a RenderReport + certification transcript serializing what already exists in memory (layout, sections, schedule, identity routing, seeds, guard inventory, explicit ASSUMED list); generator-computed evaluator pin; a one-time SrsFacts attestation making render/repack SRS-free.
• L6 — Artifact end-state (post-audit only): evaluator gets its own VK trust root and a scalars-only ~10KB frame instead of the 27KB program-carrying image; optionally bare Yul objects with a generator-declared memoryguard(0x1000), which makes the memory-safe claim true by construction instead of a documented lie.

How and why — the sequencing that matters for you

The panel's sharpest internal fight was "add differentials now" vs "don't churn code about to be audited," resolved along the bytecode axis: everything above that's a pure Rust-side checker lands pre-audit with zero bytecode change (schedule-as-checker, FOLD semantics in the reference interpreter, parser-repurposed-as-checker, accumulator reference decoder, generator-computed evaluator pin, RenderReport v1 — each is roughly a day or two); everything that rewrites structure waits (window-relative ISA, staged types, template generation, FrameV2). Exactly one bytecode regeneration happens pre-audit — the FMP guard + pragma pin batch you already planned, with the negative subgroup probe riding along.

Clean slate? No — argued honestly: the deployed artifact would come out almost identical (EIP-170, EIP-2537, and gas force it, which is itself evidence the design found the right constraints), and a rewrite discards exactly the most valuable assets — the certification mechanism, the fixture corpus, and the encoded incident history. The migration above is ~2–3 engineer-months of individually shippable steps under differential nets; a rewrite is 6+ months to reach assurance parity. Rebuild the anchoring, not the system.

One correction the synthesizer caught while spot-checking: the "strongest tests run in no CI" claim is partially stale — the pbt_ mutation suite, Poseidon fixture, and trace-equivalence do run per-PR today. The surviving finding is narrower but real: one-shape coverage, the differential runs against a trace render rather than the production artifact, and the G1-rejection sweeps / memoryguard / EIP-170 / IVC end-to-end still run nowhere.