Harden the Solidity verifier: bytecode certification and EVM replay

[jtcoolen]

What this PR does

A correctness, fail-closed and assurance pass over proofs/solidity-verifier (87 commits, 76 files, +18,693 / −4,056), plus three pieces of new machinery: render-time self-certification of the emitted quotient-VM bytecode, an adversarial EVM replay suite for the public-accumulator decode path, and root-level CI that actually runs the crate's tests.

Calibration up front, because the commit count invites the wrong reading: nothing here is a soundness fix on a shipped artifact. No commit in this range changes whether any released or fixture verifier accepts an invalid proof. The fix set breaks down as codegen paths that could have emitted a wrong contract for a configuration we do not ship, a memory-layout rebase that removes a latent compiler-dependency rather than a known miscompilation, and a long tail of fail-closed hardening on paths that were verified unreachable before the change. Those three categories are kept separate below on purpose.

The load-bearing content of the PR is arguably the assurance work: the quotient lowering's shape recognizers were previously validated only indirectly by fixture trace differentials, and the accumulator decoder had no executing coverage at all — the tests that looked like coverage were verifier_template.contains("…") greps that never rendered or ran. That is why the always-false Yul guard below survived review.

Codegen paths that could have emitted a wrong verifier

Build-time defects: the generator produced, or could produce, bad output with no failure. No shipped fixture, example or deployed artifact is affected by any of them.

• The keccak transcript-buffer bound only sized the pre-first-squeeze run over advice phases up to phase 0, so a circuit whose first Fiat-Shamir challenge belongs to a later advice phase could under-reserve the buffer and write past VK_MPTR. Reachable only when the deferred phases add nine or more advice commitments and the instance vector is large enough for the initial run to dominate. The run is now sized across every advice phase up to the first challenge-bearing one (a01b1ea).
• g1_to_u256s / g2_to_u256s emitted all-zero words — the EIP-2537 infinity encoding — whenever coordinates() returned None, which in midnight-curves also covers off-curve points. Had a malformed point reached them, NEG_S_G2 = inf would make e(pi, O) = 1 and collapse the KZG check to final_com − v·G + x3·pi = O, which a prover can satisfy from public transcript data since x3 is squeezed before pi is read. The zero path is now gated on is_identity(); anything else aborts codegen (b24be9e). Worth knowing for review: the new assertion is unreachable in this build, because blst's on_curve ORs in vec_is_zero, so the genuine identity returns Some((0,0)) and never took the None arm. This is hardening against a future raw/FFI constructor or a curve backend without that special case, not a fix for a reachable path.
• generate_base_vk hard-coded G1Affine::generator() as G1_BASE while taking g2 / s_g2 from the deployer's params, so a params file whose SRS base is c·G built cleanly. G1_BASE_MPTR is consumed in exactly one place — the −v·G term of the final KZG linearization — so the pairing check degenerates to v·(c−1) = 0: for c ≠ 1 every honest proof reverts. The consequence is a bricked verifier discoverable only after deployment, not acceptance of anything false. sum(g_lagrange) is now asserted equal to the generator, which is the right check because the Lagrange basis satisfies Σ L_i(X) = 1, making that sum exactly the crate-private params.g[0] the codegen cannot read directly (fc42518). Note: this commit's message claims the emitted verifier would diverge from the native verifier. It would not — proofs/src/poly/kzg/mod.rs hard-codes -E::G1::generator() in the same position, so a rescaled SRS breaks both identically.
• The Lagrange batch-inversion input run was built in place from X_N_MPTR (theta word 26) with no bound against the first word live at Lagrange time, which is Q_EVAL_CPTR_MPTR at theta word 201. At num_instances + |rotation_last| ≥ 175 the run overwrote the q_eval calldata cursor; codegen and solc both succeeded, and the deployed contract then computed garbage q_evals and reverted on every proof. Fail-closed (the clobbered words are consumed downstream of the KZG check, and the overwritten values are transcript-derived, not attacker-chosen), but an undetectable-until-deployment brick. adc589f adds the codegen-time bound; 6753679 makes lagrange_denoms a planner-registered region allocated after batch_invert_scratch, so MemoryMap::validate enforces disjointness structurally and the ~165-instance cliff disappears.
• A caller-supplied num_instances implying an accumulator fixed-base scalar tail larger than the VK can supply bases for rendered trailing bases pointing past the fixed-commitment region; now a typed GeneratorError::AccumulatorFixedBaseTailMismatch (54907b5).
• Quotient-VM peepholes validated a const-table slot and then emitted a subexpression that could intern past slot 255, panicking during codegen. The fused product-add scalar and the LIN7/BILIN7 limb coefficients are now reserved before the base expression is emitted, and const-table overflow falls back to a generic op (de3bd7e, 7b498f7, a01b1ea).

Generated memory layout moved off solc's via-IR spill window

The generated layout started at 0x80, on top of the spill reservation solc emits for the assembly ("memory-safe") block the templates depend on — the deployed Sepolia runtime opens with mstore(0x40, 0x08e0), i.e. solc reserved [0x80, 0x8e0) while TRANSCRIPT_MPTR sat at 0x80. Dropping the annotation was tried and does not compile (stack too deep), so the fix removes the consequence. The overlap was real but never produced an incorrect verification result — under the pinned solc the overlapping slots are dead where the verifier writes. This removes a latent recompilation hazard, and it is the reason for the large regenerated-artifact diff.

• LOW_MEMORY_SCRATCH_START moves 0x80 → 0x1000, above the largest observed reservation, and a new test reads the free-memory-pointer prologue back out of the compiled runtime so the two cannot re-converge. VK_CONSTRUCTOR_PAYLOAD_START is deliberately decoupled and stays at 0x80 (6333673).
• The accumulator pairing-batch and final two-pair frames move 0x100 / 0x320 → 0x1000 / 0x1220, and the layout validator now rejects any generated region below the layout base (60f842b).
• FINAL_PAIRING_SCRATCH_START had ec_pairing's input frame sharing the ACC_LHS y_lo word inside the alpha keccak preimage — correct only because FinalPairing.yul hashes before it calls the precompile. It is now derived as PAIRING_BATCH_PTR + PAIRING_BATCH_HASH_BYTES with a disjointness assertion (a1bb2c4).
• The Lagrange denominator run is no longer written in place from X_N_MPTR over theta words 27–51 (the deployed artifact spilled four words past the cap). It is a registered lagrange_denoms region, so MemoryMap::validate enforces disjointness and 200/500-instance layouts build instead of being refused (6753679, 75f9f99).
• Five regions were invisible to the overlap checker: the four PCS fixed windows were Phase(PcsFixed) and so never co-live with anything, selector accumulators claimed a single phase although quotient evaluation writes them, MemoryPhase was declared out of execution order, the trace-only linearization MSM band was not a region at all, and the theta-window ends were missing from the trace-log bound. All fixed with no address or output change (4f272f0, bb6f463, 914c61c, ed547ae, bafd8d7).
• The phase ordering the Lagrange cap depends on is now pinned by a test asserting against rendered source, rather than resting on a comment (06e46be).

Fixes in the rendered on-chain templates

Only the first was a live defect in shipped code, and it is the most serious fix in this PR. The rest were each verified fail-closed before the fix, via a later range check, an earlier revert, or a conformant precompile; they harden the on-chain path rather than close exploitable holes.

• load_acc_coord_shifted gated the identity-flag strip on and(iszero(div(i, limbs_per_word)), first_adjust), and Yul and is bitwise. iszero(…) is 0 or 1 and first_adjust is a radix base (2^56), so they share no bit: the guard was false on every iteration of every call and packed := sub(packed, first_adjust) never executed. The consequence is not that the identity probe went dead — it went inverted. The probe compared the un-stripped decode against p−1, so the flagged encoding (BLS_P_MINUS_ONE_PACKED_0_WITH_ID_FLAG) no longer matched and fell through to the base-field range check, while the codec's unflagged (p−1, p−1) sentinel pair decoded to exactly p−1, set is_id := 1, and was accepted by the decoder as EIP-2537 infinity with ok = 1 — writing four zero words to ACC_LHS_MPTR/ACC_RHS_MPTR. That is precisely the non-canonical zero-like encoding the decoded_zero guard exists to reject, and it sits in the mutually exclusive iszero(is_id) arm, so it was skipped. The decode-stage canonicality barrier genuinely failed open. What actually rejected such calldata was downstream and incidental: the accumulator words are absorbed into Fiat-Shamir, so substituting them perturbs every challenge and the final KZG pairing fails. Confirmed empirically — with the pre-fix guard restored in the fixture contracts, the replay case "LHS accumulator decodes to zero without the identity flag" reverts only after 1,286,473 gas (a complete verification, then a pairing failure) against 1,286,528 for a fully accepted run; post-fix the same input reverts early, under the 643k decode-guard ceiling. No forgery was reachable, because it would need a valid outer proof whose committed accumulator instances are the (p−1, p−1) sentinel pair — a G1 point with x = y = 0, which the circuit's foreign-point codec cannot emit. But that is circuit-side reasoning plus transcript binding doing the work, which is exactly what the on-chain barrier exists to avoid relying on. The fix gates on the word index alone (72bc1b2). Note: this commit's own message claims is_id was always 0 and that load_acc_point's if is_id branch was dead. Both claims are wrong and were disproved by executing the pre-fix template; the branch was reachable.
• ec_pairing folded the precompile result as and(ret, mload(scratch)), testing only the low bit and accepting any odd result word; now and(ret, eq(mload(scratch), 1)) (9e714b7).
• Every EIP-2537 constructor probe used the all-zero infinity encoding — exactly the input a stub returning zeros, or echoing its input, answers correctly. The smoke test now also checks G1ADD(G, G) == 2G against constants computed from the curve library at render time (896fd04).
• validate_public_accumulator read carried and fixed-base tail scalars from calldata with no < r check of its own, so the negated-base path computed mod(r − s, r) for s ≥ r. The three read sites now enforce it locally (68adb90).
• batch_invert and scalar_inv rejected only the literal word 0 before modexp(x, r−2, r), which returns 0 for any x ≡ 0 mod r, and the multi-element path fed raw words into mulmod, so accept/reject depended on batch length. All paths now fail closed identically, with a revm test that reproduces the old acceptance against the unfixed template (d870dd1, aa62d19).
• A failed modexp in batch_invert set ret := 0 and continued, reading back the stale EIP-198 frame header and overwriting the input range with garbage; it now returns immediately (2e49d03).
• ec_pairing's entry guard was the one exit returning a zero flag instead of reverting, and TraceReturn.yul stored 1 without reading success; both now revert (636c7ec).
• The quotient-VM epilogue checked q_pc == q_end and iszero(q_has_top), which both pass for a FOLD run with more than one operand live, and the selector y-power table's slot 0 was reserved but never written. A q_sp == stack_mptr check and one mstore close both (b680bf2, 3f95c05).

New: the emitted quotient-VM bytecode certifies itself at render time

The quotient lowering's shape recognizers pattern-match algebraic forms out of an expression tree. They are now a checked optimization: certification runs from LoweringPlan::new and validate_generator_invariants, so a recognizer bug aborts the render instead of being pinned into a codehash-pinned VK.

• vm/reference.rs (+550) is a second, independent interpreter of the bytecode ABI — every Q_OP_*, including the LIN7 / BILIN7 / MODARITH7 / AFFINE_SUM / RUN_* compaction forms — over a Keccak-derived pseudorandom memory oracle. vm/certify.rs (+365) executes each identity's finalized bytecode against direct evaluation of the QuotientExpr tree it was lowered from, then repeats the comparison against a second build with limb superinstructions disabled (0b27485).
• The certification challenge is derived by derive_certify_seed from both builds' bytes and const tables, the oracle expression trees and the VK payload, so a miscompile cannot be crafted against a fixed sample point. The memoryguard test also extends to the plain and trace quotient evaluators and each accumulator variant, since every via-IR compilation unit gets its own spill reservation (0cd1bdb).
• Certification structurally cannot catch a pointer wrong in both the bytecode and the expression tree, so LoweringPlan::quotient_read_model() publishes the windows the verifier has populated by VM time and validate_quotient_mem_ptrs rejects any literal, u16, token, limb or pairwise-span address that is misaligned or outside them — with a total walker pinned by a test, so a new pointer-bearing opcode cannot silently lose coverage (20766cb).
• QuotientProgramBuilder::finish bounds-checks every const-table index the finalized stream decodes, so an encoder regression cannot ship a verifier loading a trailing VK word as a gate coefficient (8db58be).
• Only length inequalities related the VK-embedded const table and packed bytecode to the independent plan recompile; both are now compared word-for-word, so an ordering-dependent compile over hash-backed structures cannot pin a VK that permanently rejects valid proofs (1fa3b41).
• The limb7 chain rewriter's constant tracker ignored x := … reassignments, so a stale literal could be baked into a q_limb7 call while the Yul multiplied by a runtime value (c80cbc8).

New: adversarial replay of the accumulator decode path, runnable in CI

Fixtures were re-based from proving inputs to rendered outputs so this can run on a stock runner: a verifier cannot be rendered from a VK without the full SRS (SolidityGenerator consumes params.g_lagrange()), so a blob-based replay could never have run in CI.

• tests/ivc_accumulator_replay.rs (+689) deploys shipped rendered contracts plus matching calldata under revm in about two seconds, asserts the fixture proof is accepted as a baseline, then asserts rejection of non-canonical limb packing, malformed coordinates and the canonical encoded point at infinity. Two gas-based helpers attribute each revert to a stage, so a deleted guard cannot leave the test green for the wrong reason (70dd1a8).
• A second fixture covers the point_pair encoding — the expected_acc_has_carried_scalars = false arms the deployed Moonlight wrap verifier uses, previously only ever compiled — and both fixtures gain framing / truncation / selector / ABI-head / length mutations, every proof commitment against off-curve, base-modulus and non-canonical-padding G1 vectors, and every eval scalar and non-accumulator instance set to the Fr modulus: roughly 230 EVM calls per fixture (6f78686).
• Because every accumulator word is also absorbed into the transcript, those mutations would revert at the pairing regardless, so a further commit adds 15 low-bit public-input flips that must fail at the pairing and four accumulator cases that must revert before the transcript — covering load_acc_point's malformed-infinity and decoded_zero guards, which had only template greps (07d9a9d).
• The harness carries no per-fixture constants: has_accumulator, acc_offset and num_acc_limbs are parsed back out of the rendered VK payload comments, the encoding kind is recovered from the payload width, the G1 commitment run is discovered from the EIP-2537 padding signature, and the modulus/infinity sentinels are read out of the verifier source under test (70dd1a8, 6f78686).
• The default EVM gate now compiles the accumulator render arm at all: accumulator_verifier_variants_compile_with_pinned_solc renders three accumulator shapes against the Poseidon VK and compiles both contracts under the pinned solc (5912061).

CI: the suite now gates PRs, and gates fail loudly

• The crate's workflow lived at proofs/solidity-verifier/.github/workflows/ci.yml. GitHub Actions only reads workflows from the repository root, so once the crate was vendored into midfall that file never executed and nothing in the suite gated a merge. It is deleted (−153); root ci.yaml gains three fast per-PR jobs — unit / --all-targets, real-EVM property tests, and the native↔Solidity trace differential — while the two ~90-minute IVC jobs and the release bytecode size/hash gate move to a new solidity_verifier_bench.yml on push-to-main, a weekly cron and workflow_dispatch (ffd39db).
• With HALO2_SOLIDITY_RUN_EVM_TESTS=1 set, a missing SRS or unpinned solc printed a skip line and returned green while compiling no Solidity and verifying no proof — 28 of 34 end-to-end tests returned early, which is how the tracked dumps drifted unnoticed. Prerequisites are now assertion failures carrying fetch instructions once the gate is opted into; not opting in stays a quiet skip (bea362e).
• Only Halo2VerifyingKey was size-checked, and the revm harness deliberately sets limit_contract_code_size = usize::MAX, so an over-limit verifier passed the entire suite and then failed to deploy. compiled_verifier_runtime_fits_the_eip170_limit now compiles the embedded, separate, quotient and VK renders and checks each runtime against 24,576 bytes, and the hand-rolled VK data-contract blob gets a codegen-time limit check (a30fef4, 69889be).
• --all-features was a broken configuration: every Poseidon and shape-fuzz test failed with SrsError(64, 252) because the test SRS sized its monomial basis without the prover's single-h-commitment setting. The helpers now extend the basis to k + ceil(log2(cs_degree − 1)) (0aab0cf).
• The workspace clippy gate was failing with four errors in this crate; it is now clean, with the panicking ConstraintSystemMeta::new and ProtocolPlan::from_constraint_system moved behind #[cfg(test)] (743d5da).

Fail-closed hardening on paths that are not reachable today

Listed separately on purpose: none of these fixes a defect that can occur in a current build. They remove the possibility of a future one shipping silently.

• kzg::memory_requirements / kzg::computations returned an empty result for n_sets == 0. Block 6 is the only code in the generator that writes PAIRING_LHS_MPTR / PAIRING_RHS_MPTR, those are fixed theta slots never aliased by scratch, and four zero words are exactly the EIP-2537 encoding of the point at infinity — so the emitted verifier would compute e(O, [1]₂)·e(O, [−s]₂) = 1 and return true for any calldata that survives transcript parsing, with no opening ever checked. This is the most severe potential consequence in the PR, and it is unreachable twice over: ProtocolPlan::try_from_constraint_system unconditionally pushes the Linearization query and validate rejects any schedule not ending with it (so n_sets ≥ 1), and independently validate_absorbed_g1_precompile_coverage would report every absorbed commitment as unconsumed. Both early returns are now assert! — which, unlike debug_assert!, survives release builds (700af6d).
• Three count-parity checks become hard asserts: VK permutation commitments against meta.permutation_columns, vk.fixed_comms.len() against meta.num_fixeds before deriving permutation_comm_mptr, and the accumulator fixed-base/scalar counts — promoted from debug_assert_eq!, so it no longer compiles out in release (79dd945, a9032f8, 01f4549).
• Both lookup emitters zipped input chunks against helper evals, truncating to the shorter side on drift, and their k == 0 branches emitted 0 instead of h_eval, dropping the h == 0 binding while the accumulator still folded that eval into sum_h. The zips now assert equal lengths and both branches match plonk/logup.rs; an empty h_evals vector no longer panics (63be029, e5f77f8, d67a2e9, 33e183e).
• Rotated non-committed instance queries resolved to the single Rotation::cur INSTANCE_EVAL word in both the VM and the Yul emitter; instance_eval_at / expression_memory_ptr now fail closed, with reachability still blocked by the try_new constructor check plus a new regression test (098f6a1, 2286dff, 5d7afe9).
• Pointer and offset arithmetic in the encoding layer is now total: Value::as_usize asserts non-negative before casting, Display panics on a negative concrete offset instead of rendering sub(0, N), quotient memory pointers use checked u32::try_from and assert 32-byte alignment at the single construction choke point, and column_eval_var uses unsigned_abs so Rotation(i32::MIN) cannot produce a non-identifier name (b8b4c39, 9d7081b, 16f43b5, 56f20be, d149f96).
• VK payload section reservation used unchecked usize arithmetic on externally-derived counts, so a wrapped count would produce a section map whose extcodecopy ranges alias earlier sections; both sites now return a layout error (b2e99e8).
• An unrolled PCS rotation walk emitted one mulmod per unit step across the whole span, so a large rotation passed every capacity check and produced an undeployable over-24 KB verifier with no diagnostic. Codegen caps the span at 4,096 with an explicit remedy, and the quotient stack scratch is floored at one word (6e14bfe, 0b56186).

Caller-facing API and error surface

GeneratorError and RepackError are public and not #[non_exhaustive], so the new variants break exhaustive matches downstream.

• SolidityGenerator::try_new — documented as the panic-free constructor — called plan.validate().unwrap_or_else(|err| panic!(…)), turning every ProtocolPlan::validate arm (most reachably an advice column declared but never queried) into a panic. ConstraintSystemMeta::try_new and ProtocolPlan::try_from_constraint_system now propagate as GeneratorError::Planning { stage: "constraint system" } (58824e8).
• Two new typed errors reject previously-accepted configurations: AccumulatorFixedBaseTailMismatch and TooManyInstances (54907b5, 75f9f99).
• repack_proof subgroup-checked G1 commitments but passed every eval and q_eval word through unchecked, returning Ok for scalars the on-chain parser is guaranteed to revert on; now RepackError::NonCanonicalScalar { offset, bytes_hex } (b4319da).
• LightAggregator::verify gains the <T::Hash as TranscriptHash>::Input: TranscriptInputBytes bound that plonk::prepare already grew upstream; without it cargo check --workspace failed before reaching anything else. Satisfied by both concrete transcript input types, so no call site changed (2938a40).
• lib.rs exports two new feature = "evm" test helpers, compile_solidity_runtime and runtime_free_memory_pointer_init (6333673, 0cd1bdb).
• Crate-internal signatures a reviewer will meet in the diff: TranscriptBufferLayout::from_proof_layout gains a phase_challenge_counts: &[usize] argument, and QuotientProgramBuilder::with_limb_vm_ops loses its #[cfg(test)] gate because the dual-build certifier needs it in production (a01b1ea, 0b27485).

Docs, comments and formatting

No behaviour change: corrected comments on the KZG batch-inversion non-zero argument, the deliberately swapped pairing orientation, the pointer-identity query-grouping invariant, the proxy selector_gap, the pairing-batch domain tag and two field docs (36fc616, 66c32f9, 688efde, fd3842c, 822980e, 55d548b); named-constant substitutions with identical values (4352a71, 14cb772); a numerically wrong AUDIT.md challenge-bias item corrected, stale paths fixed in the lowering spec, the Sepolia deployment record annotated, and two new architecture/redesign documents (3f89a98, 277c096, 29b4eb9, 4ae8053); rustfmt, intra-doc links and two CHANGELOG entries (11928d1, bee1833, ac9604d).

How to test this PR

Pinned solc, required by every Solidity job:

export SOLC="$(proofs/solidity-verifier/scripts/install_pinned_solc.sh "$PWD/.solc" | tail -1)"

Per-PR gate test-solidity-verifier — includes the new certification, pointer-validator and accumulator-replay tests. Needs solc; needs no SRS:

cargo test -p halo2_solidity_verifier --all-features --all-targets -- --nocapture

Just the new adversarial accumulator replay (both fixtures, ~2 s each):

cargo test -p halo2_solidity_verifier --all-features --test ivc_accumulator_replay -- --nocapture

SRS for the EVM and trace jobs (CI restores this from the fixed-srs-cache):

mkdir -p zk_stdlib/examples/assets && curl -L -o zk_stdlib/examples/assets/bls_filecoin_2p19 https://midnight-s3-fileshare-dev-eu-west-1.s3.eu-west-1.amazonaws.com/bls_filecoin_2p19

Per-PR gate test-solidity-verifier-evm — adversarial property tests, then the end-to-end Poseidon fixture (real proof → render → solc → Prague revm):

HALO2_SOLIDITY_RUN_EVM_TESTS=1 cargo test -p halo2_solidity_verifier --release --all-features pbt_ -- --nocapture

HALO2_SOLIDITY_RUN_EVM_TESTS=1 cargo test -p halo2_solidity_verifier --release --features evm,truncated-challenges --test poseidon_fixture -- --nocapture

Per-PR gate test-solidity-verifier-trace — the per-identity differential between the native Midfall verifier and the generated Solidity verifier, and the only check comparing quotient-VM semantics against the Rust verifier end to end:

HALO2_SOLIDITY_RUN_EVM_TESTS=1 cargo test -p halo2_solidity_verifier --release --features evm,truncated-challenges,rust-verifier-trace,solidity-trace --lib native_midfall_verifier_trace_matches_solidity_trace -- --nocapture

The three compiled-artifact tests that the pbt_ filter does not select (see reviewer notes):

HALO2_SOLIDITY_RUN_EVM_TESTS=1 cargo test -p halo2_solidity_verifier --release --all-features --lib compiled_memoryguard_does_not_overlap_generated_layout compiled_verifier_runtime_fits_the_eip170_limit batch_invert_fails_closed_on_noncanonical_words_in_all_paths -- --nocapture

Heavy IVC jobs, now in solidity_verifier_bench.yml (~90 min each):

export SRS_DIR="$PWD/.srs" && proofs/solidity-verifier/scripts/ensure_srs_assets.sh && proofs/solidity-verifier/scripts/run_ivc_bench.sh --skip-srs-download

Aggregation crate, for the LightAggregator::verify bound change:

cargo test -p midnight-aggregation --release --all-features

Gating env vars, all read by proofs/solidity-verifier: HALO2_SOLIDITY_RUN_EVM_TESTS=1 enables the real-EVM and proving cases (once set, a missing SRS or solc now fails instead of skipping); HALO2_SOLIDITY_RUN_IVC_BENCH=1 enables the k=20 decider (~300 MB SRS); SRS_DIR defaults to <crate>/../../zk_stdlib/examples/assets; SOLC / SOLC_INSTALL_DIR point at solc 0.8.30+commit.73712a01; HALO2_SOLIDITY_ALLOW_UNPINNED_SOLC=1 accepts a non-pinned solc, which makes gas and bytecode figures ad hoc. Note that tests/ivc_accumulator_replay.rs is gated only on #![cfg(feature = "evm")] with no env var, so under --all-features it hard-fails rather than skips if pinned solc is absent.

Notes for reviewers

• Generated artifacts. Everything under target/*-fixture-dump/ and target/ivc-keccak-solidity-dump/ was regenerated for the 0x80 → 0x1000 rebase and the template guard changes (48a6f0c, 9bf8c51, 3fb6d84). Every diff is accounted for by an upstream source change: TRANSCRIPT_MPTR/RETURN_MPTR 0x80 → 0x1000, quotient-program pointers shifting by exactly 0xf80, ec_pairing comparing against 1, the accumulator identity guard keyed on the word index, the added G1ADD(G,G)==2G smoke vector, and LAGRANGE_DENOMS_MPTR. These bodies are generated output and were not line-reviewed.
• Three dumps are still stale on the branch tip. target/{hybrid-mt,rsa-signature,sha-preimage}-fixture-dump/Halo2Verifier.sol regenerate with a diff (they are missing LAGRANGE_DENOMS_MPTR and still write the Lagrange run in place from X_N_MPTR). Please regenerate and commit before merge.
• The release bytecode gate will fail on first push to main. scripts/check_release_bytecode_sizes.sh is not in this diff, so its pinned runtime hashes predate the layout rebase — and the new bench workflow runs that script as its release size/hash step on push-to-main. Refresh the hashes as part of this PR or immediately after.
• A known CI gap ships unfixed. The test-solidity-verifier-evm step comment claims it covers non-canonical scalar and G1 rejection, EIP-170 runtime size and the memoryguard overlap check, but its pbt_ name filter selects none of them: compiled_memoryguard_does_not_overlap_generated_layout, compiled_verifier_runtime_fits_the_eip170_limit, batch_invert_fails_closed_on_noncanonical_words_in_all_paths and the G1 sweeps are plain #[test]s and run in no workflow. This PR's own docs/plans/REDESIGN_PROPOSALS_2026-08.md records it as finding F1 / proposal P0.1. Either fix the filter or fix the comment before merge.
• Public API. GeneratorError and RepackError each gain a variant and are not #[non_exhaustive]; SolidityGenerator::try_new converts former panics into typed errors and rejects two previously-accepted configurations; repack_proof / encode_calldata now reject non-canonical Fr scalars; LightAggregator::verify gains a TranscriptInputBytes bound.
• CI topology moved. Two side effects worth naming: the crate is now built with the workspace rust-toolchain.toml instead of a hardcoded 1.90.0, and the ~90-minute IVC jobs no longer run per PR. Please trigger solidity_verifier_bench.yml manually before merging this one, since it touches memory layout, proof layout, the quotient VM and the templates.
• The deployed Sepolia verifier is no longer reproducible from current codegen (source 206,619 → 212,419 bytes; runtime 21,161 → 21,203). deployments/sepolia/moonlight-wrap/ is deliberately left as deployed and the drift documented instead, including which fixes the on-chain code does not carry and why a local solc --bin-runtime differs from the recorded codehash in exactly 40 bytes (the two 20-byte AUTHORIZED_VK immutable placeholders at 0x51 and 0x125).
• Replay fixtures are frozen rendered artifacts, so they stay self-consistent — and therefore keep passing — after a codegen change. Drift is tracked only by the commit stamp in each README, because detecting it automatically would need the SRS again. Both were regenerated at 6753679; if you land further template or layout changes, re-run the commands in those READMEs.
• Assurance boundary, stated so it is not overread. Certification proves the emitter → reference-interpreter leg only. Reference-interpreter → Yul per-opcode conformance still rests on the opcode table plus the fixture trace differentials, and the overlap checker proves registered regions do not conflict, not that emitted Yul stays inside them. Both limits are written into docs/architecture/LOWERING_ARCHITECTURE_SPEC.md.
• Not covered. The accumulator arms are compiled and replayed but still never executed against a freshly proved accumulator-carrying proof outside the opt-in k=20 bench; the G1MSM and pairing constructor probes remain identity-only, so a subgroup-check-less G1MSM would still pass the smoke test.

[jtcoolen]

Here are the six most consequential issues, ranked by what actually went wrong.

1. The bitwise-and guard — the only live defect in shipped on-chain code (72bc1b2)

load_acc_coord_shifted gated the identity-flag strip on and(iszero(div(i, limbs_per_word)), first_adjust). Yul and is bitwise, iszero(…) is 0 or 1, and first_adjust is a radix base (2^56) — they share no bit, so the guard was false on every iteration of every call and the subtraction never ran.

The commit message says this made is_id always 0 and load_acc_point's if is_id branch dead. That's wrong. The probe didn't go dead, it went inverted: it compared the un-stripped decode against p−1, so the flagged encoding stopped matching and fell through to the range check, while the codec's unflagged (p−1, p−1) sentinel pair decoded to exactly p−1, set is_id := 1, and was accepted as EIP-2537 infinity with ok = 1 — four zero words written to ACC_LHS_MPTR/ACC_RHS_MPTR. The decoded_zero guard that rejects exactly that lives in the mutually exclusive iszero(is_id) arm and was skipped. The decode-stage canonicality barrier failed open.

This was verified by execution, not reading: restoring the pre-fix guard in the fixture contracts makes the replay case "LHS accumulator decodes to zero without the identity flag" revert only after 1,286,473 gas — a complete verification followed by a pairing failure — versus 1,286,528 for a fully accepted run. Post-fix it reverts under the 643k decode-guard ceiling.

No forgery was reachable: it would need a valid outer proof whose accumulator instances are that sentinel pair, i.e. a G1 point with x = y = 0, which the circuit's codec can't emit. But transcript binding and circuit-side reasoning were doing the work the on-chain barrier exists to avoid relying on.

Fix: gate on the word index alone — if iszero(div(i, limbs_per_word)). The subtraction is already a no-op when first_adjust is zero, so the conjunction was never needed.

2. Zero KZG point sets → accept-any-proof (700af6d)

Most severe potential consequence in the PR. memory_requirements/computations returned empty for n_sets == 0. Block 6 is the only writer of PAIRING_LHS/RHS_MPTR; those are fixed theta slots never aliased by scratch; four zero words are the infinity encoding. So the verifier computes e(O, [1]₂)·e(O, [−s]₂) = 1 and returns true for anything that parses — no opening checked at all.

Unreachable twice over: try_from_constraint_system unconditionally pushes the Linearization query and validate rejects any schedule not ending with it, so n_sets ≥ 1; independently, validate_absorbed_g1_precompile_coverage would flag every absorbed commitment as unconsumed. Fix: both early returns become assert! — which unlike debug_assert! survives release builds.

3. Transcript buffer under-reservation (a01b1ea)

words = max(initial_run, eval_run, total_run), and transcript_end is what places VK_MPTR with zero slack. squeeze_to is the only thing that resets buf_len, and TranscriptProofParser.yul emits it only for phases with num_challenges > 0 — but the bound used only advice_phases.first(). A circuit declaring its challenge via challenge_usable_after(SecondPhase) absorbs later-phase commitments into the same unsqueezed run, unaccounted for. The absorb helpers do a bare mstore(buf_len, …) with no upper bound, so the overrun writes proof-supplied calldata over vk_digest, then n_inv and omega, which Lagrange.yul reads afterwards.

Needs ≥9 deferred advice commitments (the 1024-byte cushion hides fewer) and ~86+ public inputs for total_run not to dominate. Realistic outcome is a broken verifier or an unbounded-gas Lagrange spin — DoS, not a demonstrated soundness break. Fix: walk advice_phases accumulating until the first phase with phase_challenge_counts[phase] > 0.

4. Lagrange run clobbering live memory (adc589f → 6753679)

The denominator run was built in place from X_N_MPTR (theta word 26); the first word live at Lagrange time is Q_EVAL_CPTR_MPTR at word 201. At num_instances + |rotation_last| ≥ 175 the run overwrote the q_eval calldata cursor — codegen and solc both succeeded, then the immutable contract reverted on every proof. Fail-closed (clobbered words are consumed downstream of the KZG check, and their values are transcript-derived, not attacker-chosen), but an undetectable-until-deployment brick. The deployed Sepolia artifact runs 30 words, stopping 145 words short of anything live. Fix: adc589f adds the codegen bound; 6753679 makes lagrange_denoms a planner-registered region so MemoryMap::validate enforces disjointness and the cliff disappears.

5. ec_pairing low-bit test (9e714b7)

ret := and(ret, mload(scratch)) — ret is already 0/1, so this tested only the low bit of the pairing result, promoting any odd word to acceptance. This is the terminal soundness gate. The sole backstop is the precompile itself: a conformant EIP-2537 PAIRING_CHECK returns exactly 0 or 1, so "odd" and "== 1" coincide. The constructor smoke test only probes a true identity pairing, so it does not certify the false-case encoding. On a non-conformant L2 returning an odd non-1 word for a failing check, the pre-fix code would have accepted an invalid proof. Fix: and(ret, eq(mload(scratch), 1)).

6. SRS base never checked (fc42518)

G1_BASE was hard-coded to the generator while g2/s_g2 came from the deployer's params. G1_BASE_MPTR is consumed in exactly one place, so with base c·G the check degenerates to v·(c−1) = 0 — every honest proof reverts. Bricked verifier, not false acceptance. The commit message claims divergence from the native verifier; it's wrong — proofs/src/poly/kzg/mod.rs hard-codes -E::G1::generator() in the same position, so a rescaled SRS breaks both identically. Fix: assert Σ g_lagrange == generator, which works because Σ L_i(X) = 1 makes that sum exactly the crate-private params.g[0].