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

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

Start with the parent issue #1723 and the existing ECM assumption pattern, then trace the three unsupported-surface checks and the compiled Yul call sequence for call, returndata, calldata, and external-call operations. The work is complete when those surfaces are removed or always false, there are 0 sorry declarations, make check is green, and differential tests have no regressions.