Parameterize gas() by an ExternalGas environment oracle

DESIGN.md

@@ -237,12 +237,19 @@ Two built-ins interact with gas and are classified as **impure / non-determinist
 do not model gas:
 
 - `gas()` returns *remaining* gas — a value that changes during execution. It is modeled as an
-  oracle / non-deterministic read (never a constant; two `gas()` calls may differ, so they cannot be
-  CSE'd). Concretely, the open-world dialects (`evmWithExternal`/`evmWithCalls`) interpret `gas()`
-  via `builtinWithExternal`: it returns an *arbitrary* word and leaves the state unchanged, so
-  `call(gas(), …)` — the idiomatic call pattern — is derivable. The executable reference dialect
-  `evm` has no oracle, so `gas()` stays stuck there (`stepOp .gas = none`); this is why `evm` is
-  deterministic while the open-world dialects are not.
+  oracle read (never a constant; two `gas()` calls may differ, so they cannot be CSE'd). Concretely,
+  `evmWithExternal calls creates gasOracle` interprets `gas()` via `builtinWithExternal`: it returns
+  a word the supplied `ExternalGas` oracle permits and leaves the state unchanged, so
+  `call(gas(), …)` — the idiomatic call pattern — is derivable. The oracle is a **parameter**, on
+  the same footing as `ExternalCalls`/`ExternalCreates`, for the same reason: what the environment
+  reports is not determined by the state this semantics tracks. `ExternalGas.any` is the maximally
+  open oracle (every word) and is what `evmWithCalls` installs, preserving the historical behavior;
+  `ExternalGas.none` leaves `gas()` stuck. A narrower oracle is what makes `gas()` *realizable* by a
+  concrete machine: a compiler forward simulation can only justify emitting the target's `GAS`
+  instruction when the source oracle is the one reporting exactly that machine's remaining gas —
+  with `ExternalGas.any` the source may pick a word the target will never produce. The executable
+  reference dialect `evm` has no oracle at all, so `gas()` stays stuck there (`stepOp .gas = none`);
+  this is why `evm` is deterministic while the open-world dialects are not.
 - gas forwarding + failure of `call`/`callcode`/`staticcall`/`delegatecall`: external call outcomes
   are modeled by the open-world relation (they can depend on out-of-gas in the callee, which a
   gas-free model cannot itself calculate).

YulSemantics/Dialect/EVM.lean

@@ -142,8 +142,9 @@ theorem effects_sound : evm.EffectsSound := by
 operations carry no determinism, non-writing, or non-halting promise (the call/create family is
 now marked `halts := true` to cover static-context write protection), so only the non-halting
 *local* built-ins remain to discharge; their `Builtin` is definitionally `stepOp`. -/
-theorem effects_sound_withExternal (calls : ExternalCalls) (creates : ExternalCreates) :
-    (evmWithExternal calls creates).EffectsSound := by
+theorem effects_sound_withExternal (calls : ExternalCalls) (creates : ExternalCreates)
+    (gasOracle : ExternalGas) :
+    (evmWithExternal calls creates gasOracle).EffectsSound := by
   refine ⟨?_, ?_, ?_, ?_⟩
   · intro op hd
     have hlocal := effects_sound.det op hd
@@ -186,7 +187,7 @@ theorem effects_sound_withExternal (calls : ExternalCalls) (creates : ExternalCr
 /-- Compatibility specialization for call-only clients. -/
 theorem effects_sound_withCalls (external : ExternalCalls) :
     (evmWithCalls external).EffectsSound :=
-  effects_sound_withExternal external ExternalCreates.none
+  effects_sound_withExternal external ExternalCreates.none ExternalGas.any
 
 example (x : U256) (st : EvmState) : stepOp .add [x, 0] st = some (.ok [x] st) := by simp [stepOp, bin]
 example (x : U256) (st : EvmState) : stepOp .mul [x, 1] st = some (.ok [x] st) := by simp [stepOp, bin]
@@ -260,10 +261,18 @@ example (external : ExternalCalls) (st : EvmState) (response : CallResponse)
   exact ⟨response, hresponse, rfl⟩
 
 example (external : ExternalCalls) (st : EvmState) (g : U256) :
-    (evmWithCalls external).Builtin .gas [] st (.ok [g] st) := ⟨g, rfl⟩
+    (evmWithCalls external).Builtin .gas [] st (.ok [g] st) := ⟨g, trivial, rfl⟩
 
+-- Under a general oracle, `gas()` may only report the words that oracle permits.
+example (calls : ExternalCalls) (creates : ExternalCreates) (gasOracle : ExternalGas)
+    (st : EvmState) (g : U256) (hg : gasOracle.Gas st g) :
+    (evmWithExternal calls creates gasOracle).Builtin .gas [] st (.ok [g] st) := ⟨g, hg, rfl⟩
+
+-- `ExternalGas.none` makes `gas()` stuck, exactly as `ExternalCalls.none` does for `call`.
 example (calls : ExternalCalls) (creates : ExternalCreates) (st : EvmState) (g : U256) :
-    (evmWithExternal calls creates).Builtin .gas [] st (.ok [g] st) := ⟨g, rfl⟩
+    ¬ (evmWithExternal calls creates ExternalGas.none).Builtin .gas [] st (.ok [g] st) := by
+  rintro ⟨g', hg', -⟩
+  exact hg'
 
 example (st : EvmState) : stepOp .gas [] st = none := rfl
 
@@ -276,7 +285,7 @@ example (external : ExternalCalls) (st : EvmState) (g : U256) (response : CallRe
     (evmWithCalls external).Builtin .gas [] st (.ok [g] st) ∧
     (evmWithCalls external).Builtin .call [g, 2, 3, 0, 0, 0, 0] st
       (.ok [response.flag] (finishCall .call st response 0 0 0 0)) := by
-  refine ⟨⟨g, rfl⟩, ?_⟩
+  refine ⟨⟨g, trivial, rfl⟩, ?_⟩
   have hc : ¬ (st.env.static ∧ (3 : U256) ≠ 0) := by simp [hstatic]
   simp only [evmWithCalls, evmWithExternal, builtinWithExternal, if_neg hc]
   exact ⟨response, hresponse, rfl⟩
@@ -316,7 +325,7 @@ example (creates : ExternalCreates) (st : EvmState) (response : CreateResponse)
     (hstatic : st.env.static = false)
     (hresponse : creates.Create
       { kind := .create2, value := 7, initCode := [], salt := some 11 } st response) :
-    (evmWithExternal ExternalCalls.none creates).Builtin .create2 [7, 0, 0, 11] st
+    (evmWithExternal ExternalCalls.none creates ExternalGas.any).Builtin .create2 [7, 0, 0, 11] st
       (.ok [response.result] (finishCreate st response 0 0)) := by
   have hc : ¬ (st.env.static = true) := by simp [hstatic]
   simp only [evmWithExternal, builtinWithExternal, if_neg hc]
@@ -358,14 +367,14 @@ example (st : EvmState) (b : U256) (hstatic : st.env.static = true) :
 /-- A static frame's value-bearing `call` halts exceptionally under `builtinWithExternal`. -/
 example (calls : ExternalCalls) (creates : ExternalCreates) (st : EvmState)
     (hstatic : st.env.static = true) :
-    builtinWithExternal calls creates .call [0, 0, 1, 0, 0, 0, 0] st
+    builtinWithExternal calls creates gasOracle .call [0, 0, 1, 0, 0, 0, 0] st
       (.halt { st with halted := some (.staticViolation, []) }) := by
   simp [builtinWithExternal, hstatic]
 
 /-- A static frame's `create` halts exceptionally under `builtinWithExternal`. -/
 example (calls : ExternalCalls) (creates : ExternalCreates) (st : EvmState)
     (hstatic : st.env.static = true) :
-    builtinWithExternal calls creates .create [0, 0, 0] st
+    builtinWithExternal calls creates gasOracle .create [0, 0, 0] st
       (.halt { st with halted := some (.staticViolation, []) }) := by
   simp [builtinWithExternal, hstatic]
 
@@ -375,7 +384,7 @@ example (calls : ExternalCalls) (creates : ExternalCreates) (st : EvmState) (res
     (hresponse : calls.Call
       { kind := .call, gas := 1, target := 2, value := 0,
         input := readBytes st.memory 0 0 } st response) :
-    builtinWithExternal calls creates .call [1, 2, 0, 0, 0, 0, 0] st
+    builtinWithExternal calls creates gasOracle .call [1, 2, 0, 0, 0, 0, 0] st
       (.ok [response.flag] (finishCall .call st response 0 0 0 0)) := by
   simp only [builtinWithExternal, hstatic]
   refine ⟨response, hresponse, rfl⟩
@@ -387,7 +396,7 @@ example (calls : ExternalCalls) (creates : ExternalCreates) (st : EvmState) (res
     (hresponse : calls.Call
       { kind := .callcode, gas := 1, target := 2, value := 3,
         input := readBytes st.memory 0 0 } st response) :
-    builtinWithExternal calls creates .callcode [1, 2, 3, 0, 0, 0, 0] st
+    builtinWithExternal calls creates gasOracle .callcode [1, 2, 3, 0, 0, 0, 0] st
       (.ok [response.flag] (finishCall .callcode st response 0 0 0 0)) := by
   simp only [builtinWithExternal]
   refine ⟨response, hresponse, rfl⟩

YulSemantics/Dialect/EVMExec.lean

@@ -23,19 +23,21 @@ about. The string↔`Op` correspondence (`opName`, `parse`) is confined to the f
   the object-data ops (`dataoffset`/`datasize`/`datacopy`, layout-abstracted — see below and
   `YulSemantics.Object`), and the halting ops (`stop`/`return`/`revert`/`invalid`).
 * **Open-world modeled**: `call`/`callcode`/`delegatecall`/`staticcall` and `create`/`create2` are
-  interpreted by `evmWithExternal calls creates`. The supplied relations describe completed
+  interpreted by `evmWithExternal calls creates gasOracle`. The supplied relations describe completed
   external executions and may include arbitrary nested calls, creations, and re-entrant callbacks.
   The call-only `evmWithCalls` API remains available. The original executable `evm` keeps these
   operations stuck because an open-world relation has no canonical evaluator.
 * **Fully modeled (terminal world update)**: `selfdestruct` transfers the executing account's
   balance, records the destruction scheduled for transaction finalization, and halts. The
   environment's `createdThisTx` bit selects the post-Cancun self-beneficiary behavior.
-* **Open-world modeled (nondeterministic oracle)**: `gas` is **deliberately** not a function of our
-  state — it is nondeterministic by design (`DESIGN.md`). In the open-world dialects
-  (`evmWithExternal`/`evmWithCalls`) `builtinWithExternal .gas []` returns an *arbitrary* word and
-  leaves the state unchanged, modeling remaining gas as an oracle read. It must not be given a
-  deterministic `stepOp` (that would license CSE), so it remains stuck in the executable reference
-  dialect `evm` (`stepOp .gas = none`), which has no oracle to consult.
+* **Open-world modeled (environment oracle)**: `gas` is **deliberately** not a function of our
+  state (`DESIGN.md`). In `evmWithExternal calls creates gasOracle` it returns a word permitted by
+  the supplied `ExternalGas` oracle and leaves the state unchanged. `ExternalGas.any` is the
+  historical unconstrained read (and what `evmWithCalls` installs); a narrower oracle lets a client
+  couple `gas()` to a concrete machine's remaining gas, which is what makes a compiler forward
+  simulation to the target `GAS` instruction possible at all. It must not be given a deterministic
+  `stepOp` (that would license CSE), so it remains stuck in the executable reference dialect `evm`
+  (`stepOp .gas = none`), which has no oracle to consult.
 * **Deliberately absent from `Op`**:
   - stack/control opcodes (`DUP*`, `SWAP*`, incl. EIP-663 `DUPN`/`SWAPN`, `PUSH*`, `POP`-as-stack-op,
     `JUMP*`, `PC`) — Yul has no stack; these are bytecode-level and belong to the EVM repo and the
@@ -504,6 +506,35 @@ def any : ExternalCreates where Create := fun _ _ _ => True
 
 end ExternalCreates
 
+/-- Open-world interpretation of the `gas()` oracle: which remaining-gas words the surrounding
+execution environment may report in a given state.
+
+Remaining gas is not a function of the state this semantics tracks — the source language
+deliberately has no gas accounting (`DESIGN.md` §1) — so, exactly like `ExternalCalls` and
+`ExternalCreates`, the environment supplies the permitted answers. Keeping it a *parameter* rather
+than hard-coding "any word" is what lets a client couple the oracle to a concrete machine: a
+compiler forward-simulation proof, for instance, can only realize `gas()` with a target `GAS`
+instruction when the source oracle is the one that reports exactly that machine's remaining gas.
+`ExternalGas.any` recovers the historical unconstrained read. -/
+structure ExternalGas where
+  /-- Relates a pre-state to any remaining-gas word `gas()` may report there. -/
+  Gas : EvmState → U256 → Prop
+
+namespace ExternalGas
+
+/-- The maximally open oracle: `gas()` may report any word. This is the historical behavior and the
+right choice for may-semantics; it admits no forward-simulation realization. -/
+def any : ExternalGas where Gas := fun _ _ => True
+
+/-- No remaining-gas answer is available, so `gas()` is stuck. The counterpart of
+`ExternalCalls.none`/`ExternalCreates.none` for a fully closed world. -/
+def none : ExternalGas where Gas := fun _ _ => False
+
+/-- The deterministic oracle that reports exactly `f st`. -/
+def ofFun (f : EvmState → U256) : ExternalGas where Gas := fun st g => g = f st
+
+end ExternalGas
+
 /-- Install the mutable world projection produced by a successful external call. Immutable frame
 context (address/caller/calldata/block fields), caller memory, returndata, and halt status are
 preserved here and handled separately by `finishCall`. -/
@@ -811,8 +842,10 @@ def externalCreate (external : ExternalCreates) (kind : CreateKind) (value offse
     result = .ok [response.result] (finishCreate st response offset.toNat size.toNat)
 
 /-- Combined open-world built-in relation. Local operations retain the executable `stepOp` graph;
-CALL-family and CREATE-family operations are interpreted by their respective relations. -/
+CALL-family and CREATE-family operations are interpreted by their respective relations, and `gas()`
+by the environment's remaining-gas oracle. -/
 def builtinWithExternal (calls : ExternalCalls) (creates : ExternalCreates)
+    (gasOracle : ExternalGas)
     (op : Op) (args : List U256) (st : EvmState)
     (result : BuiltinResult U256 EvmState) : Prop :=
   match op with
@@ -855,18 +888,19 @@ def builtinWithExternal (calls : ExternalCalls) (creates : ExternalCreates)
           if st.env.static then result = .halt { st with halted := some (.staticViolation, []) }
           else externalCreate creates .create2 value offset size (some salt) st result
       | _ => False
-  -- `gas()` is a nondeterministic oracle read: it returns an arbitrary remaining-gas word and
-  -- leaves the state unchanged. It is deliberately absent from the deterministic `stepOp` (which
-  -- has no oracle), so it lives only in this open-world relation. See `DESIGN.md` §1.
+  -- `gas()` is an oracle read: it returns a remaining-gas word the environment permits and leaves
+  -- the state unchanged. It is deliberately absent from the deterministic `stepOp` (which has no
+  -- oracle), so it lives only in this open-world relation. With `ExternalGas.any` this is the
+  -- historical unconstrained `∃ g`. See `DESIGN.md` §1.
   | .gas => match args with
-      | []   => ∃ g : U256, result = .ok [g] st
+      | []   => ∃ g : U256, gasOracle.Gas st g ∧ result = .ok [g] st
       | _    => False
   | _ => stepOp op args st = some result
 
-/-- Backwards-compatible call-only built-in relation. -/
+/-- Backwards-compatible call-only built-in relation, with the unconstrained gas oracle. -/
 def builtin (external : ExternalCalls) :
     Op → List U256 → EvmState → BuiltinResult U256 EvmState → Prop :=
-  builtinWithExternal external ExternalCreates.none
+  builtinWithExternal external ExternalCreates.none ExternalGas.any
 
 -- `effects`, `opName`, `parse`, and `mkCall` moved to `YulSemantics.Dialect.EVMOp`.
 
@@ -885,18 +919,19 @@ to the concrete `Value := BitVec 256` / `State := EvmState`. -/
 
 /-- The gas-free EVM reference dialect with open-world call and creation behavior. Unlike `evm`,
 this dialect may be nondeterministic and therefore has no canonical executable interpreter. -/
-@[reducible] def evmWithExternal (calls : ExternalCalls) (creates : ExternalCreates) : Dialect where
+@[reducible] def evmWithExternal (calls : ExternalCalls) (creates : ExternalCreates)
+    (gasOracle : ExternalGas) : Dialect where
   Op       := Op
   Value    := U256
   State    := EvmState
   litValue := litValue
   litWF    := litWF
-  Builtin  := builtinWithExternal calls creates
+  Builtin  := builtinWithExternal calls creates gasOracle
   effects  := effects
 
-/-- Backwards-compatible call-only open-world dialect. -/
+/-- Backwards-compatible call-only open-world dialect, with the unconstrained gas oracle. -/
 @[reducible] def evmWithCalls (external : ExternalCalls) : Dialect :=
-  evmWithExternal external ExternalCreates.none
+  evmWithExternal external ExternalCreates.none ExternalGas.any
 
 /-- The EVM dialect as an `ExecDialect`: `Builtin` is defined from `stepOp`, so the executable
 `builtinFn := stepOp` agrees with it by construction. `@[reducible]` for the same reason as `evm`. -/