High-leverage roadmap to shrink ECM surface and manual modeling (dynamic ABI codec, typed dynamic CodeData/SSTORE2, packed storage layouts, transient, bitmap iteration, multicall/delegatecall)

[Th0rgal]

High-leverage roadmap to shrink ECM surface and manual modeling

Context: Recent work (including #1971 "Reject unsupported typed interface ABI params", typed SafeERC20 helpers, keccakString/keccak lit, multi-arg intrinsics, storage layout reports #1897, typed CodeData facade #1967, transient-storage nonreentrant guards #1893, and the general ECM framework) has made significant progress on external call patterns, typed interfaces, and audit artifacts.

Child issue index (added 2026-06-12)

Every roadmap item below is now tracked by a standalone issue. This issue remains the living index/prioritization document; implementation discussion belongs in the children. Source for prioritization: the Morpho Blue/Midnight fidelity analysis (Th0rgal/morpho-verity) and verity-benchmark#32 (ERC-4337 EntryPoint), which converge on the same gaps.

Tier	Item	Child issue(s)	Downstream kill-site
P0-1	Dynamic/nested ABI codec	#1975 (struct-array calldata), #1889 (helper-arg lowering), #1974 (revertError args), #2000 (dynamic events = encoder half)	6+ midnight_*_callback_dynamic_abi ECMs (Midnight/Contract.lean:189–959); most of the 75/214 Yul identity-gate drift
P0-2	Typed CREATE2 + SSTORE2 code-as-data	facade done in #1967; byte-layout preimage/decode proof remains (needs a dedicated follow-up issue when scoped)	midnight_idlib_toid_market_abi_create2_preimage + initcode-layout ECMs (Contract.lean:1313–1724)
P0-3	Packed fixed arrays in mapping structs	#1976	uint128[128] stored as 128 words (Contract.lean:2433)
P1	Transient storage (arbitrary slots/locks)	#1995	liquidation-lock ECMs (Contract.lean:1109–1274)
P1	CLZ/MSB + bitmap iterator	#1996	index-scan collateral walk in isHealthy/liquidate
P1	Multicall + delegatecall frame semantics	#1997	hand-rolled multicall ECM + delegatecall-context axiom (Contract.lean:22–95)
P2	TickLib ln/exp as source + proof	#1998	tickToPriceModule Yul ECM (Contract.lean:97–159)
P2	Panic payload emission	#1999	solidity_panic_revert_payload (Contract.lean:1765)
P2	Dynamic/struct event surface	#2000	non-source-shaped EventsLib emits
New	Bytecode immutables	#1992	INITIAL_CHAIN_ID as storage slot 1024 (Contract.lean:2425)
New	Automatic checked-arithmetic obligations	#1993	checked_* Yul drift + Blue LocalNoOverflowFor axioms
New (proof)	Generated-body execution summaries	#1994 (with #1990, #1895)	Blue Proofs/Disciplines.lean local axioms
Deferred	Loc.slot_inj discharge via layout certificates	#2001	Blue StorageFrame.lean:69
Deferred	Typed EIP-712/ecrecover signature flow	#2002	per-contract digest/recover obligations

Related external-world track (oracle/IRM trust surface): #1891 → #1963 → #1964.

However, analysis of downstream usage (e.g. patterns in morpho-midnight-verity/Midnight/Proofs/TRUST_BOUNDARIES.md, Yul unsupported manifests, mapping manifest "source faithfulness" columns, and Contract.lean specs) shows that the largest remaining clusters of custom ExternalCallModules, hand-rolled calldataload/offset math, and per-contract modeling come from gaps in first-class support for:

Highest leverage (would eliminate the biggest clusters of manual code/ECMs)

1. First-class dynamic/nested ABI codec (top priority)
   Typed abi.encode / field projections / return encoding for structs containing dynamic arrays (CollateralParams[]), bytes, tuples, and complex memory returns (toMarket returns Market memory, Offer containing Market + bytes).
   This would kill or shrink the majority of the callback ECMs (*_callback_*_dynamic_abi), ratifier, market id/store/return, and most of the scattered calldataload offset math.
   It would also enable source-level keccak256(abi.encode(...)) on rich types and full multi-word (including dynamic) typed interface external calls.

2. Typed CREATE2 + SSTORE2 / code-as-data
   Proper CodeData.store[Market] / CodeData.read[Market], plus the exact SSTORE2_PREFIX ++ abi.encode(market) preimage and runtime decode for IdLib.toId / touchMarket / toMarket.
   Would collapse the entire marketIdModule / storeMarketInCodeModule / marketReturnFromCodeModule cluster (currently the largest single ECM group).
   Note: Current Compiler.Modules.CodeData + ABI.Frame intentionally gates on layoutSourcesSupported (rejects dynamic fields) because SSTORE2-style code-as-data is only sound for static layouts in many cases. We need a clear path for the encode preimage + decode use cases while respecting safety.

3. Exact Solidity storage layout, especially packed fixed arrays inside mapping structs
   Example: uint128[128] collateral inside Position[id][user]. Current model expands to 128 full Uint256 words.
   This is a visible gap in supplyCollateral/withdrawCollateral + collateral loop projections.
   Affects the storage layout report's "source faithfulness" for packed subfields inside mappingStruct values.
   (Recent Storage: emit reviewable storage layout artifacts #1897 work added rich reports, mappingStruct/structMember, non-alias certificates, and opt-in namespaces, but packed fixed-array elements inside nested mapping structs are not yet modeled at the bit level.)

High value next

• Transient storage primitives (instead of per-slot midnight_liquidation_lock_transient_* ECMs). We have tload/tstore in the EDSL + Core + synthesized nonreentrant guards (transient storage via EIP-1153), but general first-class use for arbitrary computed slots/locks is still expressed via custom ECMs in some downstreams.

• Better loops + CLZ/MSB (or a source-level bitmap iterator). The collateral walk in isHealthy and liquidate is currently a forEach scan or manual; Solidity uses while (_collateralBitmap != 0) + msb + clear. This affects both fidelity and the refinement extraction for the liquidation loop trace. (CLZ is available via consumer verity_intrinsic for EIP-7939; we need first-class or verified MSB + iterator sugar.)

• First-class delegatecall with storage context + bytes[] calldata iteration (or a source multicall helper) so multicall isn't a giant hand-rolled ECM with manual length/offset walking + delegatecall + returndatacopy + revert bubbling. (Low-level delegatecall exists and is tracked under notModeledProxyUpgradeability; higher-level helpers are missing.)

Supporting / nice-to-have

• Memory-safe assembly surface or richer raw memory primitives (reduce mstore/calldatacopy scaffolding inside ECMs).
• Library support for TickLib (the wExp approximation + tickToPrice) so tickToPriceModule can become ordinary source + proof.
• Better panic payload emission (currently a small solidityPanicModule ECM).
• More complete event surface (many EventsLib events are still not source-shaped emit).

Relation to prior ECM reduction work

These items subsume and amplify earlier priorities:

• Source-level keccak256(abi.encode(...)) (and EIP-712) becomes feasible once the dynamic/nested ABI codec exists and can feed the general keccak256(offset, size) path (or a thin compiler-owned helper) while still surfacing the standard keccak256_memory_slice_matches_evm + layout assumptions.
• Multi-word (static + dynamic) external call ABI encoding via typed interfaces is a direct subset of the dynamic/nested ABI codec work.
• Configurable SafeERC20 revert strings/guards becomes easier once a general ABI codec can express custom error shapes.

Many of the ECMs in the downstream retained table (callbacks, market code-as-data, ratifier, oracle reads with complex params, liquidation locks, multicall, tick math, etc.) would move from per-contract "assumed" ECMs into compiler-supported or standard surfaces, dramatically shrinking the trust surface in --trust-report / audit artifacts.

Cross-cutting requirements (per project conventions)

• Keep AUDIT.md, TRUST_ASSUMPTIONS.md, and AXIOMS.md synchronized with any semantic/trust/CI boundary change.
• Widen the supported fragment in proofs where appropriate (SupportedSpec, ExprCore, FunctionBody, IR/Yul bridges, etc.) while keeping explicit proved/assumed/unchecked + boundary classes (abiBoundary, storageLayoutAssumption, notModeledProxyUpgradeability, etc.).
• Update storage layout reports, trust reports, verification status, and the generator/check scripts.
• Add macro property tests, CompilationModelFeatureTest smokes, Foundry differentials, and end-to-end examples.
• Update docs (EXTERNAL_CALL_MODULES.md, ROADMAP.md, EDSL reference, capabilities, production patterns, etc.).
• All changes must pass lake build, make check (including layout drift, layer boundaries, Yul identity, proof length, hygiene), make test-foundry, etc.
• New surfaces should be fail-closed by default where they expand trust (--deny-* gates).

Proposed rough phases (subject to scoping)

• P0 (highest leverage): Dynamic/nested ABI codec for encode/projections/calls/returns (including for keccak preimages); lift dynamic gate in typed CodeData + support for Market-like dynamic payloads + exact preimage handling; precise bit-packed fixed-array storage inside mappingStruct values (report + projections).
• P1: General transient storage (beyond synthesized locks); CLZ/MSB + bitmap iterator primitives or sugar; first-class multicall/delegatecall helper with bytes[] iteration and storage context.
• P2: Richer raw memory / memory-safe assembly surface; TickLib as ordinary source; improved panic payloads; broader event emission surface.

References (internal to this repo)

• docs/EXTERNAL_CALL_MODULES.md (ECM architecture, CodeData facade, hashing helpers, typed interfaces)
• docs/ROADMAP.md, TRUST_ASSUMPTIONS.md, AUDIT.md, AXIOMS.md
• Compiler/Modules/CodeData.lean, Compiler/ABI/Frame.lean (the layoutSourcesSupported gate)
• Verity/Macro/Translate/Expr.lean (typed interface call gates, abiEncode, requireTypedInterfaceStatic*)
• scripts/generate_storage_layout_report.py, artifacts/storage_layout_report.json, STORAGE_LAYOUT_SUMMARY.md
• Recent related work: Reject unsupported typed interface ABI params #1971 (typed interface param guard + SafeERC20), storage layout Storage: emit reviewable storage layout artifacts #1897, transient nonreentrant Safety: implement real nonreentrant guard semantics #1893, typed CodeData CodeData: add typed source-level store/read/id API #1967, keccakString, etc.
• Compiler/CompilationModel/Types.lean, ParamLoading.lean, Dispatch.lean, proof modules for dynamic shapes and returnCodeData/structMember etc.

This issue is intended as a living planning document. Feedback on scoping, exact syntax (e.g. for keccak256(abi.encode(...)) or multicall), safety considerations for dynamic CodeData, and prioritization is very welcome.

Never claim completion without evidence and passing checks.