diff --git a/EvmSemantics/EVM/Equiv.lean b/EvmSemantics/EVM/Equiv.lean
index ec8a1c9..804e081 100644
--- a/EvmSemantics/EVM/Equiv.lean
+++ b/EvmSemantics/EVM/Equiv.lean
@@ -4983,7 +4983,8 @@ private theorem Operation.pushArity_le_1024 (op : Operation) :
 private theorem stepFE_sound_error' (s : State) (e : ExecutionException)
     (h : stepFE s = .error e) :
     s.halt = .Running ∧
-    Precompile.isPrecompile s.executionEnv.fork s.executionEnv.codeAddr = false ∧
+    Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig
+      s.executionEnv.fork s.executionEnv.codeAddr = false ∧
     StepRunning s ({ s with halt := .Exception e }) := by
   unfold stepFE at h
   simp only [Id.run] at h
diff --git a/EvmSemantics/EVM/Fork.lean b/EvmSemantics/EVM/Fork.lean
index a80232c..017c3bf 100644
--- a/EvmSemantics/EVM/Fork.lean
+++ b/EvmSemantics/EVM/Fork.lean
@@ -1,5 +1,7 @@
 module
 
+public import EvmSemantics.State.Account
+
 /-!
 `Fork` — the EVM hard-fork version against which gas costs (and any
 fork-conditional semantics) are computed. Threaded through the
@@ -24,6 +26,22 @@ below via the standard `LE` / `LT` / `Decidable` instances.
 
 namespace EvmSemantics
 
+/-- Execution-level overrides for the canonical fork precompile set.
+
+    `Fork` remains the Ethereum hard-fork schedule. This profile hook lets
+    embedders disable a native precompile without inventing a fake fork. -/
+structure PrecompileConfig where
+  /-- Addresses that execute as ordinary accounts, not native precompiles. -/
+  disabled : List AccountAddress := []
+
+namespace PrecompileConfig
+
+/-- Returns whether an execution profile disables a native precompile address. -/
+@[inline] def disables (config : PrecompileConfig) (addr : AccountAddress) : Bool :=
+  config.disabled.any (· == addr)
+
+end PrecompileConfig
+
 /-- The EVM hard-fork version. Listed in canonical activation order.
 
     Per-constructor EIPs of note:
diff --git a/EvmSemantics/EVM/Precompile.lean b/EvmSemantics/EVM/Precompile.lean
index e21e41b..e0e4402 100644
--- a/EvmSemantics/EVM/Precompile.lean
+++ b/EvmSemantics/EVM/Precompile.lean
@@ -731,6 +731,22 @@ def isPrecompile (fork : Fork) (addr : AccountAddress) : Bool :=
        addr = blsMapFpToG1Address || addr = blsMapFp2ToG2Address)) ||
     (fork ≥ .Osaka && addr = p256VerifyAddress)
 
+/-- Fork-aware precompile membership with execution-level overrides.
+
+    The canonical `isPrecompile` predicate is intentionally unchanged.  A
+    caller that needs to model a replacement environment can disable selected
+    addresses without changing the hard-fork gas schedule. -/
+def isPrecompileWithConfig (config : PrecompileConfig) (fork : Fork)
+    (addr : AccountAddress) : Bool :=
+  !config.disables addr && isPrecompile fork addr
+
+theorem isPrecompile_of_isPrecompileWithConfig
+    (config : PrecompileConfig) (fork : Fork) (addr : AccountAddress)
+    (h : isPrecompileWithConfig config fork addr = true) :
+    isPrecompile fork addr = true := by
+  simp [isPrecompileWithConfig] at h ⊢
+  exact h.2
+
 /-- Run a precompile. Total only on the subset
     `isPrecompile fork addr = true`; the hypothesis `h` discharges
     totality by guaranteeing one of the branches below matches.
@@ -787,6 +803,14 @@ def run (fork : Fork) (addr : AccountAddress)
                                      h_bg1, h_bm1, h_bg2, h_bm2, h_bp,
                                      h_mf1, h_mf2, h_p256])
 
+/-- Configured counterpart of `run`, used by the executable and relational
+    EVM semantics when an execution profile disables native precompiles. -/
+def runWithConfig (config : PrecompileConfig) (fork : Fork) (addr : AccountAddress)
+    (input : ByteArray) (childGas : Nat)
+    (h : isPrecompileWithConfig config fork addr = true) : Result :=
+  run fork addr input childGas
+    (isPrecompile_of_isPrecompileWithConfig config fork addr h)
+
 end Precompile
 end EVM
 end EvmSemantics
diff --git a/EvmSemantics/EVM/State.lean b/EvmSemantics/EVM/State.lean
index a5bc2c3..b4c71e8 100644
--- a/EvmSemantics/EVM/State.lean
+++ b/EvmSemantics/EVM/State.lean
@@ -292,7 +292,8 @@ def calleeEnvForCall (sc : State) (tgt : AccountAddress) (codeAddr : AccountAddr
     depth                := sc.executionEnv.depth + 1
     permitStateMutation  := sc.executionEnv.permitStateMutation
     blobVersionedHashes  := sc.executionEnv.blobVersionedHashes
-    fork                 := sc.executionEnv.fork }
+    fork                 := sc.executionEnv.fork
+    precompileConfig     := sc.executionEnv.precompileConfig }
 
 /-- EIP-7702 (Prague+) delegate address for a CALL-family target `tgt`: the
     address `tgt`'s delegation designator points to, if any; `none` otherwise
@@ -462,7 +463,8 @@ def calleeEnvFor (sc : State) (kind : CallKind) (tgt : AccountAddress)
     depth                := sc.executionEnv.depth + 1
     permitStateMutation  := kind.calleePermit sc
     blobVersionedHashes  := sc.executionEnv.blobVersionedHashes
-    fork                 := sc.executionEnv.fork }
+    fork                 := sc.executionEnv.fork
+    precompileConfig     := sc.executionEnv.precompileConfig }
 
 /-- Generalised `enterCall`, parameterised over `CallKind`. Used by the
     `Step.delegatecall` / `Step.staticcall` constructors (and could be
@@ -594,7 +596,8 @@ def calleeEnvForCreate (sc : State) (newAddr : AccountAddress)
     depth                := sc.executionEnv.depth + 1
     permitStateMutation  := sc.executionEnv.permitStateMutation
     blobVersionedHashes  := sc.executionEnv.blobVersionedHashes
-    fork                 := sc.executionEnv.fork }
+    fork                 := sc.executionEnv.fork
+    precompileConfig     := sc.executionEnv.precompileConfig }
 
 /-- Enter a CREATE/CREATE2 init-code sub-frame. `sc` is the caller state
     after the static + memory + base-gas deductions; `rest` is the
diff --git a/EvmSemantics/EVM/Step.lean b/EvmSemantics/EVM/Step.lean
index 77b5e2b..1067f53 100644
--- a/EvmSemantics/EVM/Step.lean
+++ b/EvmSemantics/EVM/Step.lean
@@ -2301,7 +2301,8 @@ inductive Step : State → State → Prop
       per-opcode logic encoded by `StepRunning`, plus the explicit
       `s.halt = .Running` guard (so `not_from_done` rules out successors
       from done states) and the **precompile gate**
-      `Precompile.isPrecompile s.executionEnv.fork s.executionEnv.codeAddr
+      `Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig
+        s.executionEnv.fork s.executionEnv.codeAddr
       = false` (so a precompile-frame state cannot derive a bytecode
       transition — only the `precompile*` constructors below fire for
       it). The gate is what makes the bytecode and precompile sides
@@ -2310,7 +2311,8 @@ inductive Step : State → State → Prop
       shape. -/
   | running : ∀ {s s' : State},
                 s.halt = .Running →
-                Precompile.isPrecompile s.executionEnv.fork
+                Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig
+                    s.executionEnv.fork
                     s.executionEnv.codeAddr = false →
                 StepRunning s s' → Step s s'
   /-- YP §9 precompile dispatch (success arm). Fires when the frame's
@@ -2323,9 +2325,10 @@ inductive Step : State → State → Prop
       gas refund. -/
   | precompileSuccess (s : State) (output : ByteArray) (gasUsed : Nat)
         (h_running : s.halt = .Running)
-        (h_isPrec  : Precompile.isPrecompile s.executionEnv.fork
+        (h_isPrec  : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig
+                        s.executionEnv.fork
                         s.executionEnv.codeAddr = true)
-        (h_prec    : Precompile.run s.executionEnv.fork
+        (h_prec    : Precompile.runWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                       s.executionEnv.codeAddr s.executionEnv.calldata
                       s.gasAvailable h_isPrec
                     = .success output gasUsed)
@@ -2343,9 +2346,10 @@ inductive Step : State → State → Prop
       pushes `0` on the caller's stack. -/
   | precompileOog (s : State)
         (h_running : s.halt = .Running)
-        (h_isPrec  : Precompile.isPrecompile s.executionEnv.fork
+        (h_isPrec  : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig
+                        s.executionEnv.fork
                         s.executionEnv.codeAddr = true)
-        (h_prec    : Precompile.run s.executionEnv.fork
+        (h_prec    : Precompile.runWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                       s.executionEnv.codeAddr s.executionEnv.calldata
                       s.gasAvailable h_isPrec
                     = .outOfGas)
diff --git a/EvmSemantics/EVM/StepComplete/Arith.lean b/EvmSemantics/EVM/StepComplete/Arith.lean
index 7621f12..76e0faf 100644
--- a/EvmSemantics/EVM/StepComplete/Arith.lean
+++ b/EvmSemantics/EVM/StepComplete/Arith.lean
@@ -23,7 +23,7 @@ theorem complete_add (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .ADD
                      ≤ 1024 + Operation.popArity .ADD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -45,7 +45,7 @@ theorem complete_mul (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .MUL
                      ≤ 1024 + Operation.popArity .MUL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -67,7 +67,7 @@ theorem complete_sub (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SUB
                      ≤ 1024 + Operation.popArity .SUB)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -89,7 +89,7 @@ theorem complete_div (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .DIV
                      ≤ 1024 + Operation.popArity .DIV)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -111,7 +111,7 @@ theorem complete_sdiv (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SDIV
                      ≤ 1024 + Operation.popArity .SDIV)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -133,7 +133,7 @@ theorem complete_mod (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .MOD
                      ≤ 1024 + Operation.popArity .MOD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -155,7 +155,7 @@ theorem complete_smod (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SMOD
                      ≤ 1024 + Operation.popArity .SMOD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -177,7 +177,7 @@ theorem complete_addmod (s : State) (a b n : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .ADDMOD
                      ≤ 1024 + Operation.popArity .ADDMOD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -199,7 +199,7 @@ theorem complete_mulmod (s : State) (a b n : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .MULMOD
                      ≤ 1024 + Operation.popArity .MULMOD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -221,7 +221,7 @@ theorem complete_exp (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .EXP
                      ≤ 1024 + Operation.popArity .EXP)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -251,7 +251,7 @@ theorem complete_signextend (s : State) (b x : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SIGNEXTEND
                      ≤ 1024 + Operation.popArity .SIGNEXTEND)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -271,7 +271,7 @@ theorem complete_stop (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .STOP
                      ≤ 1024 + Operation.popArity .STOP)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = { s with halt := .Success, hReturn := .empty }
     := by
diff --git a/EvmSemantics/EVM/StepComplete/Block.lean b/EvmSemantics/EVM/StepComplete/Block.lean
index 3272d24..eb0aeb0 100644
--- a/EvmSemantics/EVM/StepComplete/Block.lean
+++ b/EvmSemantics/EVM/StepComplete/Block.lean
@@ -31,7 +31,7 @@ theorem complete_blockhash (s : State) (n : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .BLOCKHASH
                      ≤ 1024 + Operation.popArity .BLOCKHASH)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -51,7 +51,7 @@ theorem complete_coinbase (s : State)
         (h_gas     : Gas.baseCost s.fork .COINBASE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -71,7 +71,7 @@ theorem complete_timestamp (s : State)
         (h_gas     : Gas.baseCost s.fork .TIMESTAMP ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -91,7 +91,7 @@ theorem complete_number (s : State)
         (h_gas     : Gas.baseCost s.fork .NUMBER ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -111,7 +111,7 @@ theorem complete_prevrandao (s : State)
         (h_gas     : Gas.baseCost s.fork .PREVRANDAO ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -131,7 +131,7 @@ theorem complete_gaslimit (s : State)
         (h_gas     : Gas.baseCost s.fork .GASLIMIT ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -151,7 +151,7 @@ theorem complete_chainid (s : State)
         (h_gas     : Gas.baseCost s.fork .CHAINID ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -171,7 +171,7 @@ theorem complete_selfbalance (s : State)
         (h_gas     : Gas.baseCost s.fork .SELFBALANCE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -191,7 +191,7 @@ theorem complete_basefee (s : State)
         (h_gas     : Gas.baseCost s.fork .BASEFEE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -214,7 +214,7 @@ theorem complete_blobhash (s : State) (i : UInt256) (rest : List UInt256) (h : U
         (h_cap   : s.stack.length + Operation.pushArity .BLOBHASH
                      ≤ 1024 + Operation.popArity .BLOBHASH)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -237,7 +237,7 @@ theorem complete_blobhash_oob (s : State) (i : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .BLOBHASH
                      ≤ 1024 + Operation.popArity .BLOBHASH)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -257,7 +257,7 @@ theorem complete_blobbasefee (s : State)
         (h_gas     : Gas.baseCost s.fork .BLOBBASEFEE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
diff --git a/EvmSemantics/EVM/StepComplete/Calls.lean b/EvmSemantics/EVM/StepComplete/Calls.lean
index 061f121..5302f2d 100644
--- a/EvmSemantics/EVM/StepComplete/Calls.lean
+++ b/EvmSemantics/EVM/StepComplete/Calls.lean
@@ -28,7 +28,7 @@ theorem complete_callStatic (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CALL
                      ≤ 1024 + Operation.popArity .CALL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .StaticModeViolation })
     := by
@@ -67,7 +67,7 @@ theorem complete_call (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CALL
                      ≤ 1024 + Operation.popArity .CALL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           (({ s with
@@ -163,7 +163,7 @@ theorem complete_callFail (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CALL
                      ≤ 1024 + Operation.popArity .CALL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           ({ s with
@@ -238,7 +238,7 @@ theorem complete_callcode (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CALLCODE
                      ≤ 1024 + Operation.popArity .CALLCODE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           (({ s with
@@ -313,7 +313,7 @@ theorem complete_callcodeFail (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CALLCODE
                      ≤ 1024 + Operation.popArity .CALLCODE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           ({ s with
@@ -385,7 +385,7 @@ theorem complete_delegatecall (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .DELEGATECALL
                      ≤ 1024 + Operation.popArity .DELEGATECALL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           (({ s with
@@ -458,7 +458,7 @@ theorem complete_delegatecallFail (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .DELEGATECALL
                      ≤ 1024 + Operation.popArity .DELEGATECALL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           ({ s with
@@ -527,7 +527,7 @@ theorem complete_staticcall (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .STATICCALL
                      ≤ 1024 + Operation.popArity .STATICCALL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           (({ s with
@@ -600,7 +600,7 @@ theorem complete_staticcallFail (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .STATICCALL
                      ≤ 1024 + Operation.popArity .STATICCALL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           ({ s with
diff --git a/EvmSemantics/EVM/StepComplete/CompBit.lean b/EvmSemantics/EVM/StepComplete/CompBit.lean
index 0158b53..6887ab1 100644
--- a/EvmSemantics/EVM/StepComplete/CompBit.lean
+++ b/EvmSemantics/EVM/StepComplete/CompBit.lean
@@ -23,7 +23,7 @@ theorem complete_lt (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .LT
                      ≤ 1024 + Operation.popArity .LT)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -45,7 +45,7 @@ theorem complete_gt (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .GT
                      ≤ 1024 + Operation.popArity .GT)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -67,7 +67,7 @@ theorem complete_slt (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SLT
                      ≤ 1024 + Operation.popArity .SLT)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -89,7 +89,7 @@ theorem complete_sgt (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SGT
                      ≤ 1024 + Operation.popArity .SGT)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -111,7 +111,7 @@ theorem complete_eq (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .EQ
                      ≤ 1024 + Operation.popArity .EQ)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -133,7 +133,7 @@ theorem complete_iszero (s : State) (a : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .ISZERO
                      ≤ 1024 + Operation.popArity .ISZERO)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -155,7 +155,7 @@ theorem complete_and (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .AND
                      ≤ 1024 + Operation.popArity .AND)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -177,7 +177,7 @@ theorem complete_or (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .OR
                      ≤ 1024 + Operation.popArity .OR)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -199,7 +199,7 @@ theorem complete_xor_ (s : State) (a b : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .XOR
                      ≤ 1024 + Operation.popArity .XOR)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -221,7 +221,7 @@ theorem complete_not (s : State) (a : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .NOT
                      ≤ 1024 + Operation.popArity .NOT)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -243,7 +243,7 @@ theorem complete_clz (s : State) (a : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .CLZ
                      ≤ 1024 + Operation.popArity .CLZ)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -265,7 +265,7 @@ theorem complete_byte_ (s : State) (i x : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .BYTE
                      ≤ 1024 + Operation.popArity .BYTE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -287,7 +287,7 @@ theorem complete_shl (s : State) (shift v : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SHL
                      ≤ 1024 + Operation.popArity .SHL)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -309,7 +309,7 @@ theorem complete_shr (s : State) (shift v : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SHR
                      ≤ 1024 + Operation.popArity .SHR)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -331,7 +331,7 @@ theorem complete_sar (s : State) (shift v : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SAR
                      ≤ 1024 + Operation.popArity .SAR)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
diff --git a/EvmSemantics/EVM/StepComplete/CopiesKeccak.lean b/EvmSemantics/EVM/StepComplete/CopiesKeccak.lean
index 823bdbd..3db55e3 100644
--- a/EvmSemantics/EVM/StepComplete/CopiesKeccak.lean
+++ b/EvmSemantics/EVM/StepComplete/CopiesKeccak.lean
@@ -23,7 +23,7 @@ theorem complete_keccak256 (s : State) (offset size : UInt256) (rest : List UInt
         (h_cap   : s.stack.length + Operation.pushArity .KECCAK256
                      ≤ 1024 + Operation.popArity .KECCAK256)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -68,7 +68,7 @@ theorem complete_calldatacopy (s : State) (destOff srcOff sz : UInt256) (rest :
         (h_cap   : s.stack.length + Operation.pushArity .CALLDATACOPY
                      ≤ 1024 + Operation.popArity .CALLDATACOPY)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -114,7 +114,7 @@ theorem complete_codecopy (s : State) (destOff srcOff sz : UInt256) (rest : List
         (h_cap   : s.stack.length + Operation.pushArity .CODECOPY
                      ≤ 1024 + Operation.popArity .CODECOPY)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -160,7 +160,7 @@ theorem complete_extcodecopy (s : State) (addr destOff srcOff sz : UInt256) (res
         (h_cap   : s.stack.length + Operation.pushArity .EXTCODECOPY
                      ≤ 1024 + Operation.popArity .EXTCODECOPY)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -213,7 +213,7 @@ theorem complete_returndatacopy (s : State) (destOff srcOff sz : UInt256) (rest
         (h_cap   : s.stack.length + Operation.pushArity .RETURNDATACOPY
                      ≤ 1024 + Operation.popArity .RETURNDATACOPY)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
diff --git a/EvmSemantics/EVM/StepComplete/Creates.lean b/EvmSemantics/EVM/StepComplete/Creates.lean
index 19d1c85..88d2f13 100644
--- a/EvmSemantics/EVM/StepComplete/Creates.lean
+++ b/EvmSemantics/EVM/StepComplete/Creates.lean
@@ -23,7 +23,7 @@ theorem complete_return_ (s : State) (offset size : UInt256) (rest : List UInt25
         (h_cap   : s.stack.length + Operation.pushArity .RETURN
                      ≤ 1024 + Operation.popArity .RETURN)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -62,7 +62,7 @@ theorem complete_revert (s : State) (offset size : UInt256) (rest : List UInt256
         (h_cap   : s.stack.length + Operation.pushArity .REVERT
                      ≤ 1024 + Operation.popArity .REVERT)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -103,7 +103,7 @@ theorem complete_createStatic (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CREATE
                      ≤ 1024 + Operation.popArity .CREATE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .StaticModeViolation })
     := by
@@ -128,7 +128,7 @@ theorem complete_createFail (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CREATE
                      ≤ 1024 + Operation.popArity .CREATE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -183,7 +183,7 @@ theorem complete_createCollision (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CREATE
                      ≤ 1024 + Operation.popArity .CREATE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -238,7 +238,7 @@ theorem complete_create (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CREATE
                      ≤ 1024 + Operation.popArity .CREATE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           (({ s with
@@ -281,7 +281,7 @@ theorem complete_create2Static (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CREATE2
                      ≤ 1024 + Operation.popArity .CREATE2)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .StaticModeViolation })
     := by
@@ -306,7 +306,7 @@ theorem complete_create2Fail (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CREATE2
                      ≤ 1024 + Operation.popArity .CREATE2)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -363,7 +363,7 @@ theorem complete_create2Collision (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CREATE2
                      ≤ 1024 + Operation.popArity .CREATE2)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -424,7 +424,7 @@ theorem complete_create2 (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .CREATE2
                      ≤ 1024 + Operation.popArity .CREATE2)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           (({ s with
@@ -474,7 +474,7 @@ theorem complete_selfDestructStatic (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .SELFDESTRUCT
                      ≤ 1024 + Operation.popArity .SELFDESTRUCT)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .StaticModeViolation })
     := by
@@ -495,7 +495,7 @@ theorem complete_selfDestruct (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .SELFDESTRUCT
                      ≤ 1024 + Operation.popArity .SELFDESTRUCT)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           (({ s with gasAvailable := s.gasAvailable - Gas.selfDestructTotal s beneficiary
diff --git a/EvmSemantics/EVM/StepComplete/Dispatch.lean b/EvmSemantics/EVM/StepComplete/Dispatch.lean
index b262cb7..e25ab53 100644
--- a/EvmSemantics/EVM/StepComplete/Dispatch.lean
+++ b/EvmSemantics/EVM/StepComplete/Dispatch.lean
@@ -48,7 +48,7 @@ theorem stepF_eq_error {s : State} {e : ExecutionException}
 theorem stepFE_dispatch {s : State} {op : Operation}
     {argOpt : Option (UInt256 × Nat)}
     (h_run : s.halt = .Running)
-    (h_np : Precompile.isPrecompile s.executionEnv.fork
+    (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
               s.executionEnv.codeAddr = false)
     (h_dec : s.decoded = some (op, argOpt))
     (h_cap : s.stack.length + op.pushArity ≤ 1024 + op.popArity)
@@ -95,7 +95,7 @@ theorem stepFE_dispatch {s : State} {op : Operation}
     decode: `InvalidInstruction`. -/
 theorem stepFE_decodeNone {s : State}
     (h_run : s.halt = .Running)
-    (h_np : Precompile.isPrecompile s.executionEnv.fork
+    (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
               s.executionEnv.codeAddr = false)
     (h_none : s.decoded = none) :
     stepFE s = .error .InvalidInstruction := by
@@ -110,7 +110,7 @@ theorem stepFE_decodeNone {s : State}
 theorem stepFE_overflow {s : State} {op : Operation}
     {argOpt : Option (UInt256 × Nat)}
     (h_run : s.halt = .Running)
-    (h_np : Precompile.isPrecompile s.executionEnv.fork
+    (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
               s.executionEnv.codeAddr = false)
     (h_dec : s.decoded = some (op, argOpt))
     (h_over : s.stack.length + op.pushArity > 1024 + op.popArity) :
@@ -127,7 +127,7 @@ theorem stepFE_overflow {s : State} {op : Operation}
 theorem stepFE_baseOog {s : State} {op : Operation}
     {argOpt : Option (UInt256 × Nat)}
     (h_run : s.halt = .Running)
-    (h_np : Precompile.isPrecompile s.executionEnv.fork
+    (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
               s.executionEnv.codeAddr = false)
     (h_dec : s.decoded = some (op, argOpt))
     (h_cap : s.stack.length + op.pushArity ≤ 1024 + op.popArity)
diff --git a/EvmSemantics/EVM/StepComplete/EnvReads.lean b/EvmSemantics/EVM/StepComplete/EnvReads.lean
index 3d94b37..b2afa67 100644
--- a/EvmSemantics/EVM/StepComplete/EnvReads.lean
+++ b/EvmSemantics/EVM/StepComplete/EnvReads.lean
@@ -30,7 +30,7 @@ theorem complete_address (s : State)
         (h_gas     : Gas.baseCost s.fork .ADDRESS ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -52,7 +52,7 @@ theorem complete_balance (s : State) (addr : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .BALANCE
                      ≤ 1024 + Operation.popArity .BALANCE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -79,7 +79,7 @@ theorem complete_origin (s : State)
         (h_gas     : Gas.baseCost s.fork .ORIGIN ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -99,7 +99,7 @@ theorem complete_caller (s : State)
         (h_gas     : Gas.baseCost s.fork .CALLER ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -119,7 +119,7 @@ theorem complete_callvalue (s : State)
         (h_gas     : Gas.baseCost s.fork .CALLVALUE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -141,7 +141,7 @@ theorem complete_calldataload (s : State) (i : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .CALLDATALOAD
                      ≤ 1024 + Operation.popArity .CALLDATALOAD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -161,7 +161,7 @@ theorem complete_calldatasize (s : State)
         (h_gas     : Gas.baseCost s.fork .CALLDATASIZE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -181,7 +181,7 @@ theorem complete_codesize (s : State)
         (h_gas     : Gas.baseCost s.fork .CODESIZE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -201,7 +201,7 @@ theorem complete_gasprice (s : State)
         (h_gas     : Gas.baseCost s.fork .GASPRICE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -223,7 +223,7 @@ theorem complete_extcodesize (s : State) (addr : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .EXTCODESIZE
                      ≤ 1024 + Operation.popArity .EXTCODESIZE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -252,7 +252,7 @@ theorem complete_returndatasize (s : State)
         (h_gas     : Gas.baseCost s.fork .RETURNDATASIZE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -274,7 +274,7 @@ theorem complete_extcodehash (s : State) (addr : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .EXTCODEHASH
                      ≤ 1024 + Operation.popArity .EXTCODEHASH)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
diff --git a/EvmSemantics/EVM/StepComplete/Exceptions.lean b/EvmSemantics/EVM/StepComplete/Exceptions.lean
index 375673a..e5632f6 100644
--- a/EvmSemantics/EVM/StepComplete/Exceptions.lean
+++ b/EvmSemantics/EVM/StepComplete/Exceptions.lean
@@ -19,7 +19,7 @@ namespace StepComplete
 theorem complete_decodeFailure (s : State)
         (h_none    : s.decoded = none)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .InvalidInstruction })
     := by
@@ -31,7 +31,7 @@ theorem complete_invalidOpcode (s : State)
         (h_cap     : s.stack.length + Operation.pushArity .INVALID
                        ≤ 1024 + Operation.popArity .INVALID)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .InvalidInstruction })
     := by
@@ -57,7 +57,7 @@ theorem complete_initCodeSizeOog (s : State) (op : Operation)
         (h_perm     : s.executionEnv.permitStateMutation = true)
         (h_large    : Gas.initCodeTooLarge s.fork size.toNat = true)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .OutOfGas })
     := by
@@ -84,7 +84,7 @@ theorem complete_stackOverflow (s : State) (op : Operation)
         (h_pop_ok  : op.popArity ≤ s.stack.length)
         (h_over    : s.stack.length - op.popArity + op.pushArity > 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .StackOverflow })
     := by
@@ -101,7 +101,7 @@ theorem complete_staticModeViolation (s : State) (op : Operation)
         (h_reach   : s.staticReach op)
         (h_perm    : s.executionEnv.permitStateMutation = false)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .StaticModeViolation })
     := by
@@ -166,7 +166,7 @@ theorem complete_jumpBadDest (s : State) (dest : UInt256) (rest : List UInt256)
         (h_stack   : s.stack = dest :: rest)
         (h_bad     : Decode.isValidJumpDest s.executionEnv.code dest.toNat = false)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .BadJumpDestination })
     := by
@@ -186,7 +186,7 @@ theorem complete_jumpiBadDest (s : State) (dest cond : UInt256) (rest : List UIn
         (h_cond    : UInt256.isTrue cond)
         (h_bad     : Decode.isValidJumpDest s.executionEnv.code dest.toNat = false)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .BadJumpDestination })
     := by
@@ -205,7 +205,7 @@ theorem complete_returndatacopyOob (s : State) (destOff srcOff sz : UInt256) (re
         (h_stack   : s.stack = destOff :: srcOff :: sz :: rest)
         (h_oob     : srcOff.toNat + sz.toNat > s.returnData.size)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .InvalidMemoryAccess })
     := by
diff --git a/EvmSemantics/EVM/StepComplete/Flow.lean b/EvmSemantics/EVM/StepComplete/Flow.lean
index e4505f1..1723698 100644
--- a/EvmSemantics/EVM/StepComplete/Flow.lean
+++ b/EvmSemantics/EVM/StepComplete/Flow.lean
@@ -37,7 +37,7 @@ theorem complete_push0 (s : State)
         (h_gas     : Gas.baseCost s.fork (.Push ⟨0, by decide⟩) ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -59,7 +59,7 @@ theorem complete_pushN (s : State) (k : Fin 33) (data : UInt256) (immWidth : Nat
         (h_gas     : Gas.baseCost s.fork (.Push ⟨k, k.isLt⟩) ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -86,7 +86,7 @@ theorem complete_dup (s : State) (n : Fin 16) (v : UInt256)
         (h_get     : s.stack[n.val]? = some v)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -109,7 +109,7 @@ theorem complete_swap (s : State) (n : Fin 16) (stk' : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity (.Swap ⟨n⟩)
                      ≤ 1024 + Operation.popArity (.Swap ⟨n⟩))
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -132,7 +132,7 @@ theorem complete_jump (s : State) (dest : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .JUMP
                      ≤ 1024 + Operation.popArity .JUMP)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -157,7 +157,7 @@ theorem complete_jumpi_taken (s : State) (dest cond : UInt256) (rest : List UInt
         (h_cap   : s.stack.length + Operation.pushArity .JUMPI
                      ≤ 1024 + Operation.popArity .JUMPI)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -181,7 +181,7 @@ theorem complete_jumpi_notTaken (s : State) (dest cond : UInt256) (rest : List U
         (h_cap   : s.stack.length + Operation.pushArity .JUMPI
                      ≤ 1024 + Operation.popArity .JUMPI)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -202,7 +202,7 @@ theorem complete_pc (s : State)
         (h_gas     : Gas.baseCost s.fork .PC ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -223,7 +223,7 @@ theorem complete_gas (s : State)
         (h_gas     : Gas.baseCost s.fork .GAS ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -246,7 +246,7 @@ theorem complete_jumpdest (s : State)
         (h_cap   : s.stack.length + Operation.pushArity .JUMPDEST
                      ≤ 1024 + Operation.popArity .JUMPDEST)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -270,7 +270,7 @@ theorem complete_log (s : State) (n : Fin 5) (offset size : UInt256)
         (h_cap   : s.stack.length + Operation.pushArity (.Log ⟨n⟩)
                      ≤ 1024 + Operation.popArity (.Log ⟨n⟩))
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -321,7 +321,7 @@ theorem complete_dupN (s : State) (n : Fin 256) (v : UInt256)
         (h_get     : s.stack[n.val]? = some v)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -344,7 +344,7 @@ theorem complete_swapN (s : State) (n : Fin 256) (stk' : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity (.SwapN ⟨n⟩)
                      ≤ 1024 + Operation.popArity (.SwapN ⟨n⟩))
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -368,7 +368,7 @@ theorem complete_exchange (s : State) (b : Fin 256) (stk' : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity (.Exchange ⟨b⟩)
                      ≤ 1024 + Operation.popArity (.Exchange ⟨b⟩))
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
diff --git a/EvmSemantics/EVM/StepComplete/Oog.lean b/EvmSemantics/EVM/StepComplete/Oog.lean
index 6ff43ad..6878d70 100644
--- a/EvmSemantics/EVM/StepComplete/Oog.lean
+++ b/EvmSemantics/EVM/StepComplete/Oog.lean
@@ -223,7 +223,7 @@ theorem complete_outOfGas (s : State) (op : Operation) (cost : Nat)
         (h_cost_ub  : cost ≤ Gas.totalCost s op)
         (h_gas      : s.gasAvailable < cost)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .OutOfGas })
     := by
diff --git a/EvmSemantics/EVM/StepComplete/StackMem.lean b/EvmSemantics/EVM/StepComplete/StackMem.lean
index f19c37a..c6e95ee 100644
--- a/EvmSemantics/EVM/StepComplete/StackMem.lean
+++ b/EvmSemantics/EVM/StepComplete/StackMem.lean
@@ -23,7 +23,7 @@ theorem complete_pop (s : State) (a : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .POP
                      ≤ 1024 + Operation.popArity .POP)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -45,7 +45,7 @@ theorem complete_mload (s : State) (offset : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .MLOAD
                      ≤ 1024 + Operation.popArity .MLOAD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -80,7 +80,7 @@ theorem complete_mstore (s : State) (offset value : UInt256) (rest : List UInt25
         (h_cap   : s.stack.length + Operation.pushArity .MSTORE
                      ≤ 1024 + Operation.popArity .MSTORE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -117,7 +117,7 @@ theorem complete_mstore8 (s : State) (offset value : UInt256) (rest : List UInt2
         (h_cap   : s.stack.length + Operation.pushArity .MSTORE8
                      ≤ 1024 + Operation.popArity .MSTORE8)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -153,7 +153,7 @@ theorem complete_msize (s : State)
         (h_gas     : Gas.baseCost s.fork .MSIZE ≤ s.gasAvailable)
         (h_cap     : s.stack.length < 1024)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -176,7 +176,7 @@ theorem complete_mcopy (s : State) (destOff srcOff sz : UInt256) (rest : List UI
         (h_cap   : s.stack.length + Operation.pushArity .MCOPY
                      ≤ 1024 + Operation.popArity .MCOPY)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -226,7 +226,7 @@ theorem complete_sload (s : State) (key : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SLOAD
                      ≤ 1024 + Operation.popArity .SLOAD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -258,7 +258,7 @@ theorem complete_sstore (s : State) (key value : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .SSTORE
                      ≤ 1024 + Operation.popArity .SSTORE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -311,7 +311,7 @@ theorem complete_tload (s : State) (key : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .TLOAD
                      ≤ 1024 + Operation.popArity .TLOAD)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
@@ -334,7 +334,7 @@ theorem complete_tstore (s : State) (key value : UInt256) (rest : List UInt256)
         (h_cap   : s.stack.length + Operation.pushArity .TSTORE
                      ≤ 1024 + Operation.popArity .TSTORE)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s =
           { s with
diff --git a/EvmSemantics/EVM/StepComplete/Underflow.lean b/EvmSemantics/EVM/StepComplete/Underflow.lean
index 2e0b1a1..1ab8de5 100644
--- a/EvmSemantics/EVM/StepComplete/Underflow.lean
+++ b/EvmSemantics/EVM/StepComplete/Underflow.lean
@@ -67,7 +67,7 @@ theorem complete_stackUnderflow (s : State) (op : Operation)
         (h_reach   : s.underflowReach op)
         (h_under   : s.stack.length < op.popArity)
         (h_run : s.halt = .Running)
-        (h_np : Precompile.isPrecompile s.executionEnv.fork
+        (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
                   s.executionEnv.codeAddr = false) :
     stepF s = ({ s with halt := .Exception .StackUnderflow })
     := by
diff --git a/EvmSemantics/EVM/StepDeterminism.lean b/EvmSemantics/EVM/StepDeterminism.lean
index b7341e6..db31ef7 100644
--- a/EvmSemantics/EVM/StepDeterminism.lean
+++ b/EvmSemantics/EVM/StepDeterminism.lean
@@ -60,7 +60,7 @@ theorem stepFE_resume {s : State} {f : Frame} {rest : List Frame}
     of a running, non-precompile frame is exactly the `stepF` step. -/
 theorem stepRunning_complete {s s' : State}
     (h_run : s.halt = .Running)
-    (h_np : Precompile.isPrecompile s.executionEnv.fork
+    (h_np : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
               s.executionEnv.codeAddr = false)
     (h : StepRunning s s') :
     stepF s = s' := by
@@ -375,7 +375,7 @@ theorem step_complete {s s' : State} (h : Step s s') : stepF s = s' := by
     simp only [Id.run, h_run]
     split
     · rename_i hp
-      have h_prec' : Precompile.run s.executionEnv.fork s.executionEnv.codeAddr
+      have h_prec' : Precompile.runWithConfig s.executionEnv.precompileConfig s.executionEnv.fork s.executionEnv.codeAddr
           s.executionEnv.calldata s.gasAvailable hp = .success out gasUsed := h_prec
       simp only [h_prec']
     · rename_i hp; rw [h_isPrec] at hp; cases hp
@@ -385,7 +385,7 @@ theorem step_complete {s s' : State} (h : Step s s') : stepF s = s' := by
     simp only [Id.run, h_run]
     split
     · rename_i hp
-      have h_prec' : Precompile.run s.executionEnv.fork s.executionEnv.codeAddr
+      have h_prec' : Precompile.runWithConfig s.executionEnv.precompileConfig s.executionEnv.fork s.executionEnv.codeAddr
           s.executionEnv.calldata s.gasAvailable hp = .outOfGas := h_prec
       simp only [h_prec']
     · rename_i hp; rw [h_isPrec] at hp; cases hp
diff --git a/EvmSemantics/EVM/StepF.lean b/EvmSemantics/EVM/StepF.lean
index 97f4b5c..1e8ea76 100644
--- a/EvmSemantics/EVM/StepF.lean
+++ b/EvmSemantics/EVM/StepF.lean
@@ -1046,10 +1046,12 @@ def stepFE (s : State) : Except ExecutionException State := Id.run do
     -- borrowed-from address ≠ `address`), and a transaction whose
     -- `to` is itself a precompile (where `buildInitState` sets
     -- `codeAddr := tx.recipient`).
-    match h_isPrec : Precompile.isPrecompile s.executionEnv.fork
+    match h_isPrec : Precompile.isPrecompileWithConfig s.executionEnv.precompileConfig
+                       s.executionEnv.fork
                        s.executionEnv.codeAddr with
     | true =>
-      match Precompile.run s.executionEnv.fork s.executionEnv.codeAddr
+      match Precompile.runWithConfig s.executionEnv.precompileConfig s.executionEnv.fork
+              s.executionEnv.codeAddr
               s.executionEnv.calldata s.gasAvailable h_isPrec with
       | .success out gasUsed =>
         .ok { s with
diff --git a/EvmSemantics/State/ExecutionEnv.lean b/EvmSemantics/State/ExecutionEnv.lean
index 95fcffe..e15ef3b 100644
--- a/EvmSemantics/State/ExecutionEnv.lean
+++ b/EvmSemantics/State/ExecutionEnv.lean
@@ -61,6 +61,8 @@ structure ExecutionEnv where
   /-- EVM hard-fork version against which gas costs and any
       fork-conditional semantics are computed. -/
   fork                : Fork
+  /-- Execution-level precompile overrides, inherited by child frames. -/
+  precompileConfig    : PrecompileConfig := {}
   deriving Inhabited
 
 end EvmSemantics