Skip to content

Add configurable precompile execution profiles #142

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
leonardoalt merged 2 commits into from
Aug 4, 2026
Merged

Add configurable precompile execution profiles #142

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d69d73f
Add configurable precompile execution profiles
leonardoalt Aug 4, 2026
726e35d
Document precompile profile predicate
leonardoalt Aug 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion EvmSemantics/EVM/Equiv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 18 additions & 0 deletions EvmSemantics/EVM/Fork.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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:
Expand Down
24 changes: 24 additions & 0 deletions EvmSemantics/EVM/Precompile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
9 changes: 6 additions & 3 deletions EvmSemantics/EVM/State.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
16 changes: 10 additions & 6 deletions EvmSemantics/EVM/Step.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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)
Expand All @@ -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)
Expand Down
24 changes: 12 additions & 12 deletions EvmSemantics/EVM/StepComplete/Arith.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
24 changes: 12 additions & 12 deletions EvmSemantics/EVM/StepComplete/Block.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
Loading
Loading