Parameterize gas() by an ExternalGas environment oracle

[leonardoalt]

Why

gas() was interpreted as an unconstrained nondeterministic read: in the open-world dialects,
builtinWithExternal .gas [] admitted every word (∃ g, result = .ok [g] st).

That is a sound may-semantics, but it makes gas() unrealizable by any concrete machine. A
client proving a forward simulation into a target EVM is handed a source derivation that has
already picked some g, and must produce a target run yielding that same g; the target's GAS
instruction produces its own remaining gas. So the two can never be made to agree, and gas()
cannot enter a verified compiler's supported fragment at all — which is exactly the blocker in
powdr-labs/yul-compiler (real Solidity output is full of call(gas(), …)).

What

Make the oracle a parameter, on the same footing as ExternalCalls and ExternalCreates, and
for the same reason: what the surrounding environment reports is not determined by the state this
semantics tracks.

• new ExternalGas structure (Gas : EvmState → U256 → Prop) with
  • ExternalGas.any — every word; the previous behavior,
  • ExternalGas.none — stuck, matching ExternalCalls.none/ExternalCreates.none,
  • ExternalGas.ofFun — the deterministic oracle reporting f st;
• builtinWithExternal and evmWithExternal take it explicitly;
• builtin and evmWithCalls install ExternalGas.any.

Compatibility

Every existing client keeps exactly its current meaning: the two compatibility wrappers pin
ExternalGas.any, and evmWithExternal's new argument is the only source-level change callers see.
stepOp .gas = none is unchanged, so the closed-world executable dialect evm and its determinism /
interpreter / adequacy results are untouched.

New guards in Dialect/EVM.lean pin both directions: a general oracle only admits the words it
permits, and ExternalGas.none makes gas() stuck.

lake build is clean.

🤖 Generated with Claude Code

[chriseth]

Looks good, should we merge this? Any reason not to?

[leonardoalt]

Looks good, should we merge this? Any reason not to?

Done :)