Semantics: model stateful external contract interactions

[Th0rgal]

Goal

Define a source/executable semantics for external calls against a stateful external world, so Verity can reason about calls to contracts that maintain their own state.

Motivation

Current external calls and ECMs are useful compiler boundaries, but they are not yet a clean semantic model of interacting contracts. Morpho-style verification needs to state assumptions about oracles, tokens, callbacks, and protocol peers in one place, while distinguishing caller state, callee state, returndata, reverts, and staticcall restrictions.

Proposed shape

Introduce an ExternalWorld indexed by address and interface summary. A summary should describe:

• selector and mutability (call vs staticcall);
• precondition on caller state, calldata, value, and external world;
• post-state relation for caller-visible effects and callee/external-world effects;
• returndata relation;
• revert relation and returndata bubbling.

view/staticcall summaries must not mutate external world state.

Acceptance criteria

• Typed interface ECMs can be interpreted against the same external-world semantics.
• Source and compiler semantics can share the same external oracle/world boundary.
• Failed calls model revert data and no committed caller continuation.
• Generated trust reports list each assumed external summary.