feat(CodeData): typed byte-layout proof surface for CREATE2/SSTORE2 code-as-storage

Motivation

morpho-midnight-verity keeps its IdLib/SSTORE2 machinery behind ECMs because Verity has no typed surface for byte-exact code/data layouts. The affected modules (Midnight/Contract.lean ~1304–1780) carry 5 distinct ECM axioms:

• midnight_idlib_toid_market_abi_create2_preimage (2 sites — marketIdModule, marketIdAtOffsetModule): IdLib.toId over SSTORE2_PREFIX ++ abi.encode(market) implements the real preimage but can't be expressed as typed source
• midnight_sstore2_market_initcode_layout + create2_address_derivation (2 sites — storeMarketInCodeModule and the touch path): CREATE2-SSTORE2 storage where the emitted Yul is the source algorithm; typed CodeData.store[Market] is the intended replacement
• midnight_sstore2_market_runtime_abi_decode / midnight_sstore2_market_runtime_abi_return: reading back the stored runtime code and decoding/returning the Market payload

Proposed surface

1. CodeData layout type: a first-class description of prefix ++ payload byte layouts (SSTORE2-style: STOP-prefixed runtime code carrying an ABI-encoded payload), with lemmas relating layout length/offsets to the payload encoding.
2. Preimage construction: a verified builder for initcode that returns the given runtime code, with a theorem that the deployed code equals prefix ++ payload (initcode layout proof — kills midnight_sstore2_market_initcode_layout).
3. CREATE2 address derivation: model-level create2Address salt initcodeHash deployer with the keccak preimage structured as a typed record rather than raw bytes, so the IdLib.toId preimage becomes a definitional unfolding (kills *_create2_preimage; create2_address_derivation becomes a model definition rather than an axiom).
4. Round-trip decode: CodeData.load[T] with decode (encode x) = x for supported payload types (kills the runtime decode/return axioms).

Dependencies / notes

• Payloads like Market are dynamic structs, so the decode half depends on the dynamic ABI codec work (#1982 family / Tier 1: #1975, #1889).
• The address-derivation and initcode-layout halves are independent of #1982 and can land first.
• Downstream goal: replace the 6 ECM axiom occurrences in morpho-midnight-verity with typed CodeData.store/CodeData.load calls plus per-contract certificates.

Start in Midnight/Contract.lean, around lines 1304–1780, and inspect the six ECM axioms and their sites in marketIdModule, marketIdAtOffsetModule, storeMarketInCodeModule, and the touch path. Review the dynamic ABI codec dependencies in #1982, #1975, and #1889. Done means a typed CodeData surface covers the independent initcode and CREATE2 pieces, with the decode work aligned to the codec dependency and the downstream axioms replaceable.