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