proof(L2): Tier 3 — effects & observables (ABI encoding correctness; emit, typed reverts, returns)

[Th0rgal]

Child of #1723 (Tier 3). Requires the ABI lemma groundwork; overlaps the codec work tracked in #1982.

Goal

Eliminate stmtTouchesUnsupportedEffectSurface: emit, rawLog, requireError, revertError, returnValues, returnArray, returnBytes, returnStorageWords.

Strategy

Build an ABI encoding correctness library first:

1. Scalar ABI encoding (uint256, address, bool, bytes32)
2. Dynamic offset/length encoding for bytes/arrays
3. Compose with mstore correctness → memory layout matches ABI spec
4. Thread through LOG opcodes (topics = indexed args, data = non-indexed encoding) and typed reverts

Done when

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

[Th0rgal]

Tier-3 foundation progress (2026-08-12): the ABI round-trip library now covers every decoder shape in DynamicAbi (#2263-#2270, #2281: static canonical words incl. intN/bytesN fixed points, aligned/bounded reads, dynamic heads, element words, nested member length/data-offset/elements, byte-level reads) plus the payload observables Panic(uint256) (#2280) and Error(string) (#2283) with the reusable mstore-block execution infrastructure (#2282). Remaining for Tier 3 closure: the emit/event surface (symbolic __evt_ptr stores need binding-aware evaluation) and typed reverts beyond Error(string), then the stmtTouchesUnsupportedEffectSurface retirement.