EVM Sail Specification¶

An executable specification of the Ethereum execution layer, written in Sail. It defines the state transition function — transaction validity and execution, the EVM, gas, precompiled contracts, and the state trie — together with the stateless validation of execution payloads. Every rule cites the Yellow Paper section or EIP it implements; fork-dependent rules are gated on the Fork ordering rather than duplicated per fork.

The state transition¶

Transactions — validity, upfront effects, execution, and settlement (YP §6).
Block execution — system calls, the transaction loop, withdrawals, and requests.
Stateless validation — the commitments an executed block must satisfy.
Exceptions — exceptional halts and block-validation failures.

The EVM¶

Halting — normal stops, exceptional halts, and frame status.
The interpreter — fetch/decode, the run loop, and message calls.
Opcode semantics — the single-step transition function.
The instruction set.
The gas schedule.
Precompiled contracts.
Machine state — the per-message-call registers, stack, and memory.

State and data structures¶

Accounts, Transactions, Blocks — the protocol data types.
The Merkle-Patricia trie and the state trie.
RLP and SSZ serialization; hash_tree_root.
Cryptographic primitives.

Architecture¶

The model is split into a user-space machine (the per-message-call compute state: program counter, stack, memory, gas) and a state kernel (the world-state semantics for accounts, storage, logs, and transactional overlays). Every world effect crosses that split as an explicit k_* kernel call, and world rollback is a kernel snapshot/revert. The kernel is part of the normative Sail specification under kernel/.

Beneath both sits the host interface, with two facets: regions — the stateless input, frame memory, code, log data, output, and scratch stores, each addressed by its own nominal {off, len} slice type without runtime source dispatch — and the accelerator interface, the cryptographic functions the implementation computes (hashing, secp256k1, the precompile accelerators). Pages under host/ document that interface and are non-normative: they specify the model's internal contracts, not protocol rules.