Miscellaneous fixes

aggregation/src/light_aggregator/mod.rs

@@ -81,7 +81,9 @@ use midnight_proofs::{
         },
         EvaluationDomain,
     },
-    transcript::{CircuitTranscript, Hashable, Sampleable, Transcript},
+    transcript::{
+        CircuitTranscript, Hashable, Sampleable, Transcript, TranscriptHash, TranscriptInputBytes,
+    },
 };
 use rand::{CryptoRng, RngCore};
 
@@ -414,6 +416,11 @@ impl<const NB_PROOFS: usize> LightAggregator<NB_PROOFS> {
         C: Hashable<T::Hash>,
         F: Sampleable<T::Hash> + Hashable<T::Hash>,
         u32: Hashable<T::Hash>,
+        // Required by `plonk::prepare`, which this method delegates to. The
+        // bound is satisfied by both real transcript input types (`Vec<u8>`
+        // and `Vec<Fq>`); propagating it here mirrors the other `prepare`
+        // callers in `proofs/tests/plonk_api.rs`.
+        <T::Hash as TranscriptHash>::Input: TranscriptInputBytes,
     {
         // Read the LHS of the acc from the transcript.
         let acc_lhs: Msm<S> = {

proofs/solidity-verifier/deployments/sepolia/moonlight-wrap/README.md

@@ -4,6 +4,64 @@ This directory contains the generated Moonlight wrap verifier contracts that
 were deployed to Sepolia, plus the exact runtime bytecode fetched back from the
 chain.
 
+## Status: deployed code predates current codegen
+
+**The contracts at the addresses below are still the ones described here, but
+the generator has since moved on. They are not reproducible from current
+`main`.** Nothing in this directory has been regenerated -- the sources and
+bytecode remain exactly what was deployed, because they are the record of what
+is on chain.
+
+Re-rendering the same circuit at `e5300d4` produces a different verifier:
+
+| | Deployed | Current codegen |
+| --- | ---: | ---: |
+| `Halo2Verifier.sol` | 206,619 bytes | 212,419 bytes |
+| Verifier runtime | 21,161 bytes | 21,203 bytes |
+| `TRANSCRIPT_MPTR` | `0x80` | `0x1000` |
+
+The verifying key also differs, in its `quotient_program` section; the circuit
+itself is unchanged (`acc_offset = 11`, 19 public inputs, `point_pair`).
+
+Fixes made after this deployment that it therefore does **not** carry:
+
+- **Memory layout rebase.** The deployed verifier bases its layout at `0x80`,
+  inside the `[0x80, 0x8e0)` window solc reserves for via-IR stack-to-memory
+  spill slots -- see AUDIT.md TA-5. It has not misbehaved, but the separation
+  rests on spill placement rather than on anything enforced.
+- **Accumulator identity guard.** `load_acc_coord_shifted` used a bitwise `and`
+  against a radix base, making the guard false on every call; the identity
+  branch was dead and the canonicality barrier ineffective. Fail-closed, not a
+  forgery path.
+- **Pairing result check.** `ec_pairing` folded the precompile result with a
+  bitwise `and`, accepting any odd return word rather than exactly `1`.
+- **Constructor smoke test.** Probes used identity-only EIP-2537 vectors, which
+  a non-conformant precompile can satisfy without doing curve arithmetic.
+
+Redeploying is a deliberate on-chain action requiring a funded keystore and an
+RPC endpoint; see "Recreate The Deployment" below. Until then this record stays
+as-is and accurate.
+
+## Verifying the deployed bytecode
+
+The tracked source reproduces the on-chain runtime exactly, apart from the
+immutable address slots that are substituted at deployment:
+
+```bash
+solc --bin-runtime --optimize --optimize-runs 200 --via-ir \
+  --evm-version cancun --no-cbor-metadata Halo2Verifier.sol
+```
+
+That yields 21,161 bytes -- matching `runtimeBytes` -- with codehash
+`0x79432a36a98570db8c04b9c5cc23994477089eabd2501cfe0b0a78ae5f3c38f8`.
+
+It does **not** equal the recorded `runtimeCodeHash`, and should not: comparing
+compiled output byte-for-byte against on-chain code shows exactly 40 differing
+bytes, in two 20-byte runs at offsets `0x51` and `0x125`. Those are the two
+placeholder slots for `address public immutable AUTHORIZED_VK`, filled in by the
+constructor. Every other byte is identical. Verified at `e5300d4` with
+`solc 0.8.30+commit.73712a01`.
+
 ## Addresses
 
 | Contract | Address |

proofs/solidity-verifier/docs/architecture/MEMORY_LAYOUT.md

@@ -27,10 +27,35 @@ Solidity reserves the first four words of memory for compiler conventions:
 
 The generated verifier intentionally does not follow Solidity allocation by
 reading and bumping `mload(0x40)`. Instead, every generated absolute memory
-region is planned at or above `0x80`. The streaming transcript buffer, the main
-verifier return word, the split quotient return frame, the VK constructor
-payload buffer, and low-memory precompile scratch all start from named
-Rust-side layout constants rooted at `SOLIDITY_ALLOCATABLE_MEMORY_START`.
+region is planned from named Rust-side layout constants.
+
+Those constants are **not** rooted at `0x80`. The verifier body is wrapped in
+`assembly ("memory-safe")`, which is load-bearing -- without it the block does
+not compile under `--via-ir` (stack too deep) -- but also factually untrue,
+since the block writes memory it never obtained from the free-memory pointer.
+The annotation is what enables solc's stack-to-memory mover, which reserves
+spill slots upward from `0x80` and records the top in the runtime's
+`mstore(0x40, ...)` prologue. Observed reservations range from `0x80` (none) to
+`0x8e0`, varying with the circuit, the solc release, and the optimizer
+schedule.
+
+Basing the layout at `0x80` therefore put solc's spill slots and the verifier's
+own transcript buffer in the same bytes, separated only by live ranges that
+nothing enforced -- a recompilation could silently place a live spill across a
+verifier write and corrupt a challenge or pairing input. So the streaming
+transcript buffer, the main verifier return word, the split quotient return
+frame, low-memory precompile scratch, the accumulator/KZG pairing-batch hash
+frame, and the final two-pair pairing frame are rooted at
+`LOW_MEMORY_SCRATCH_START` (`0x1000`), above the largest observed reservation.
+`VerifierMemoryLayout::validate()` rejects any generated region below that
+base, and `compiled_memoryguard_does_not_overlap_generated_layout` compiles
+each rendered variant -- including the accumulator-bearing ones -- and fails
+the build if a future circuit or compiler pushes the reservation past it.
+
+The VK constructor payload buffer is the exception: it lives in
+`Halo2VerifyingKey`, whose assembly carries no `memory-safe` annotation, so
+solc reserves nothing there and it stays at
+`SOLIDITY_ALLOCATABLE_MEMORY_START`.
 
 The code generator treats `[0x00..0x80)` as off limits for generated writes:
 `VerifierMemoryLayout::validate()` rejects any registered region inside that
@@ -140,6 +165,8 @@ which changes the transcript-buffer bound. The verifier reserves:
 
 - unaligned starts or lengths;
 - any generated region inside Solidity-reserved memory `[0x00..0x80)`;
+- any generated region below `LOW_MEMORY_SCRATCH_START` (`0x1000`), where a
+  live via-IR spill slot could share its bytes;
 - overlapping permanent regions;
 - overlapping scratch regions that are live in the same `MemoryPhase`;
 - PCS fixed-window overflows.
@@ -245,16 +272,16 @@ The planner validates by lifetime, not just by address.
 
 | Phase | Region examples | Notes |
 | --- | --- | --- |
-| `Transcript` | `[0, transcript_words * 0x20)` | Must stay below `VK_MPTR`. |
+| `Transcript` | `[0x1000, 0x1000 + transcript_words * 0x20)` | Must stay below `VK_MPTR`. |
 | `ScalarInv` | `VK_MPTR - 0x100` frame | Historical modexp scratch near the VK payload. |
 | `LagrangeBatchInvert` | `batch_invert_scratch_mptr` | Reuses selector bytes before selector accumulators are live. |
 | `QuotientVm` | quotient temps and stack | Used before PCS final MSM. |
 | `PcsQEvalSourceTable` | rolled q_eval address table | Aliases `pcs_scratch_mptr`. |
 | `PcsQComTrace` | optional q_com trace MSM | Aliases `pcs_scratch_mptr`; trace-only. |
 | `PcsFinalMsm` | final MSM input and selector accumulators | Selector accumulators and final MSM must not overlap in this phase. |
 | `AccumulatorMsm` | public accumulator MSM input | Length is derived from accumulator/VK shape. |
-| `AccumulatorPairingBatch` | `[0x100, 0x320)` | Hash domain plus four G1 points for accumulator pairing batching. |
-| `FinalPairing` | two-pair KZG pairing frame | Low-memory final precompile frame. |
+| `AccumulatorPairingBatch` | `[0x1000, 0x1220)` | Hash domain plus four G1 points for accumulator pairing batching. |
+| `FinalPairing` | `[0x1220, 0x1540)` two-pair KZG pairing frame | Final precompile frame, placed past the pairing-batch frame by construction. |
 
 ## Update Rules
 

proofs/solidity-verifier/docs/architecture/MIGRATION.md

@@ -343,6 +343,10 @@ The `cargo test --lib` suite now stands at 7/7 green:
   `assembly ("memory-safe") { ... }` to silence the legacy
   stack-too-deep error path; with `--via-ir` solc 0.8.30 now
   compiles the full ~117 kB output cleanly.
+  Note the annotation is not merely cosmetic: it enables solc's
+  stack-to-memory mover, which reserves spill slots upward from
+  `0x80`. See AUDIT.md TA-5 and `docs/architecture/MEMORY_LAYOUT.md`
+  for why the generated layout is based at `0x1000` rather than `0x80`.
 * `tests/poseidon_fixture.rs` — new integration test (gated behind
   `feature = "evm"` and currently `#[ignore]`d, see below) that:
     1. Configures `SRS_DIR` to point at

proofs/solidity-verifier/docs/audit/AUDIT.md

@@ -2314,10 +2314,33 @@ memory-safety rules. If future edits add Solidity code after the block, or if
 the compiler reasons across the block in an unexpected way, this becomes a
 miscompilation risk.
 
+**Status: addressed.** The risk was not hypothetical. `solc 0.8.30` with the
+pinned flags emits `mstore(0x40, 0x08e0)` for the moonlight-wrap render, i.e.
+it reserved `[0x80, 0x8e0)` for via-IR stack-to-memory spill slots -- directly
+on top of a generated layout that started at `0x80`. Reservations observed
+across renders: `0x80` (ivc-keccak, none), `0xe0` (rsa), `0x3c0` (poseidon),
+`0x8e0` (moonlight-wrap). At least one spill (`mstore(0x300, mload(0x6a00))`,
+the `y` challenge, re-read ~600 IR lines later) sits in that window.
+
+The recommendation below to remove the annotation was tested and does not work:
+the block then fails to compile with `Cannot swap Variable usr$f_4 ... too deep
+in the stack by 1 slots`, and solc itself suggests re-adding the annotation.
+The annotation is load-bearing.
+
+The fix instead moves the generated layout above the reservation
+(`LOW_MEMORY_SCRATCH_START = 0x1000`), making the two regions disjoint in space
+so their liveness no longer matters, and adds
+`compiled_memoryguard_does_not_overlap_generated_layout`, which compiles each
+rendered variant and fails if the reservation ever grows past that base. Note
+this removes the *consequence*, not the false annotation itself; making the
+annotation honest would require runtime `mload(0x40)`-based re-basing at the
+cost of an `ADD` per memory access.
+
 Recommendation:
 
-- Prefer removing `"memory-safe"` from the terminal verifier block unless there
-  is a compiler-specific proof that this pattern is accepted.
+- ~~Prefer removing `"memory-safe"` from the terminal verifier block unless
+  there is a compiler-specific proof that this pattern is accepted.~~
+  Superseded: removal does not compile. See status note above.
 - Pin the exact compiler and EVM version. The Renegade audit's recommendation
   to use fixed pragmas rather than floating `^0.8.x` is especially relevant for
   generated verifier code.

proofs/solidity-verifier/docs/reference/QUOTIENT_EVALUATOR_9KB_BYTECODE.md

@@ -104,8 +104,16 @@ normal ABI call.
 The largest win was the compact quotient VM.
 
 Instead of rendering most identities as Yul source, the generator lowers them to
-a small bytecode language in `src/lowering/quotient/mod.rs`. The runtime consumer
-is `templates/partials/quotient_numerator/QuotientNumeratorBlock.yul`.
+a small bytecode language in `src/lowering/quotient_numerator/vm/mod.rs`. The
+runtime consumer is
+`templates/partials/quotient_numerator/QuotientNumeratorBlock.yul`.
+
+Every emitted program is certified before it can be pinned into a verifying key:
+`src/lowering/quotient_numerator/vm/certify.rs` re-executes the finalized
+bytecode with the independent interpreter in
+`src/lowering/quotient_numerator/vm/reference.rs` and compares each identity
+against direct evaluation of the expression tree it was lowered from, and
+against a second build with the limb superinstructions disabled.
 
 The VK payload carries: