proof(L2): Tier 4 — external calls & low-level mechanics (call frames, returndata, ECM)

[Th0rgal]

Child of #1723 (Tier 4). Most complex tier; scheduled after Tiers 1–3/5 so it can reuse the storage + ABI lemma libraries.

Goal

Eliminate stmtTouchesUnsupportedCallSurface, stmtTouchesUnsupportedForeignSurface, stmtTouchesUnsupportedLowLevelSurface: low-level call/staticcall/delegatecall, returndataSize/returndataCopy/returndataOptionalBoolAt, extcodesize, calldatacopy, revertReturndata, externalCallBind, ecm, externalCall.

Strategy

1. Model external calls as opaque state transitions with pre/post conditions (matching the existing ECM assumption pattern)
2. Prove the compiled Yul call sequence satisfies those pre/post conditions
3. External contract behavior stays an assumption (cannot prove other contracts correct)

Done when

• The three call/foreign/low-level surfaces removed/always-false
• 0 sorry, make check green, no differential-test regressions