proof(L2): Tier 1 — storage & mapping operation preservation (mappingSlot bridge lemmas)

[Th0rgal]

Child of #1723 (Tier 1). Highest contract-coverage impact; parallelizable with #2080 (Tier 2).

Goal

Eliminate stmtTouchesUnsupportedStateSurface: prove compile-preservation for storage/storageAddr (extend existing partial proof), all mapping* read/write variants (mapping, mappingWord, mappingPackedWord, mapping2, mapping2Word, mappingUint, mappingChain), structMember*, and dynamic storage arrays (storageArrayLength/Element/Push/Pop/setStorageArrayElement).

Strategy

The mappingSlot kernel Keccak engine is already proven (solidityMappingSlot_lt_evmModulus). Build the storage-mapping bridge lemma library:

1. compileMapping correctness: compiled Yul sload(mappingSlot(base, key)) = source evalMapping field key
2. Extend to word offsets and packed words via arithmetic lemmas (feeds feat(storage): Solidity-compatible packed storage lowering for Midnight Yul identity #2060)
3. Array ops via length-slot and element-slot arithmetic
4. mappingChain last (recursive, hardest)

Done when

• stmtTouchesUnsupportedStateSurface removed/always-false
• 0 sorry, make check green, no differential-test regressions