Protocol system calls¶
The block-level system calls the protocol issues around the transactions:
the EIP-4788 / EIP-2935 block-start writes (unchecked — skipped if the
contract is absent) and the EIP-7002 / EIP-7251 / EIP-8282 block-end
request dequeues (checked — absence or failure invalidates the block). Each is a
30M-gas frame from SYSTEM_ADDRESS whose committed storage writes shape
the post-state root.
Constants¶
The deposit offsets describe the ABI-encoded DepositEvent payload, while
SYSTEM_CALL_INPUT_LENGTH is the fixed input length of each block-start
system call.
The block-start writes¶
Before the transactions, the protocol issues unchecked system calls from
SYSTEM_ADDRESS to the beacon-roots (EIP-4788) and block-hash-history
(EIP-2935) contracts, writing the parent beacon-block root and the parent
block hash into their ring buffers. Each takes a 32-byte input and 30M
gas, and bumps no nonce, charges no fee, and counts toward no block gas;
it is skipped if the contract has no code.
let SYSTEM_CALL_INPUT_LENGTH¶
let SYSTEM_CALL_INPUT_LENGTH : int(32) = WORD_BYTE_LENGTHlet WORD_BYTE_LENGTH : int(32) = 32let DEPOSIT_EVENT_DATA_LENGTH¶
let DEPOSIT_EVENT_DATA_LENGTH : int(576) = 576let DEPOSIT_PUBKEY_HEAD¶
let DEPOSIT_PUBKEY_HEAD : int(0) = 0let DEPOSIT_WITHDRAWAL_CREDENTIALS_HEAD¶
let DEPOSIT_WITHDRAWAL_CREDENTIALS_HEAD : int(32) = 32let DEPOSIT_AMOUNT_HEAD¶
let DEPOSIT_AMOUNT_HEAD : int(64) = 64let DEPOSIT_SIGNATURE_HEAD¶
let DEPOSIT_SIGNATURE_HEAD : int(96) = 96let DEPOSIT_INDEX_HEAD¶
let DEPOSIT_INDEX_HEAD : int(128) = 128let DEPOSIT_PUBKEY_LENGTH_WORD¶
let DEPOSIT_PUBKEY_LENGTH_WORD : int(160) = 160let DEPOSIT_PUBKEY_DATA¶
let DEPOSIT_PUBKEY_DATA : int(192) = 192let DEPOSIT_PUBKEY_LENGTH¶
let DEPOSIT_PUBKEY_LENGTH : int(48) = 48let DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH_WORD¶
let DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH_WORD : int(256) = 256let DEPOSIT_WITHDRAWAL_CREDENTIALS_DATA¶
let DEPOSIT_WITHDRAWAL_CREDENTIALS_DATA : int(288) = 288let DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH¶
let DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH : int(32) = WORD_BYTE_LENGTHlet WORD_BYTE_LENGTH : int(32) = 32let DEPOSIT_AMOUNT_LENGTH_WORD¶
let DEPOSIT_AMOUNT_LENGTH_WORD : int(320) = 320let DEPOSIT_AMOUNT_DATA¶
let DEPOSIT_AMOUNT_DATA : int(352) = 352let DEPOSIT_AMOUNT_LENGTH¶
let DEPOSIT_AMOUNT_LENGTH : int(8) = EIGHT_BYTE_LENGTHlet EIGHT_BYTE_LENGTH : int(8) = 8let DEPOSIT_SIGNATURE_LENGTH_WORD¶
let DEPOSIT_SIGNATURE_LENGTH_WORD : int(384) = 384let DEPOSIT_SIGNATURE_DATA¶
let DEPOSIT_SIGNATURE_DATA : int(416) = 416let DEPOSIT_SIGNATURE_LENGTH¶
let DEPOSIT_SIGNATURE_LENGTH : int(96) = 96let DEPOSIT_INDEX_LENGTH_WORD¶
let DEPOSIT_INDEX_LENGTH_WORD : int(512) = 512let DEPOSIT_INDEX_DATA¶
let DEPOSIT_INDEX_DATA : int(544) = 544let DEPOSIT_INDEX_LENGTH¶
let DEPOSIT_INDEX_LENGTH : int(8) = EIGHT_BYTE_LENGTHlet EIGHT_BYTE_LENGTH : int(8) = 8let DEPOSIT_REQUEST_LENGTH¶
let DEPOSIT_REQUEST_LENGTH : int(192) = 192let DEPOSIT_REQUEST_PUBKEY¶
let DEPOSIT_REQUEST_PUBKEY : int(0) = 0let DEPOSIT_REQUEST_WITHDRAWAL_CREDENTIALS¶
let DEPOSIT_REQUEST_WITHDRAWAL_CREDENTIALS : int(48) = 48let DEPOSIT_REQUEST_AMOUNT¶
let DEPOSIT_REQUEST_AMOUNT : int(80) = 80let DEPOSIT_REQUEST_SIGNATURE¶
let DEPOSIT_REQUEST_SIGNATURE : int(88) = 88let DEPOSIT_REQUEST_INDEX¶
let DEPOSIT_REQUEST_INDEX : int(184) = 184function run_system_call_frame¶
Runs a top-level protocol system-call frame. The caller has already
resolved code, made a fresh memory frame and, for a word input, frozen
the parent-memory span that input references.
function run_system_call_frame(
tgt : address,
code : Code,
input : CalldataSlice,
memory_base : memory_base,
) -> (
(gas, state_gas, state_gas_spill, gas_refund, FrameStatus, OutputSlice)
) = {
k_journal_checkpoint();
let stack_top = stack_reset();
interpret(
SYSTEM_CALL_GAS_LIMIT,
STATE_GAS_ZERO,
STATE_GAS_SPILL_ZERO,
GAS_REFUND_ZERO,
stack_top,
memory_base,
MEMORY_HEIGHT_ZERO,
SYSTEM_ADDRESS,
tgt,
tgt,
ZERO_WORD,
STATE_GAS_ZERO,
false,
0,
code,
input,
)
}The non-recursive step loop for one complete call tree. It executes
the active frame, resumes suspended parents through
frame_stack_pop as children halt, and returns the top-level
frame's output. Each step's carried state is supplied from the frame
registers and its returned state is assigned back; the handlers
themselves never touch the registers. STOP, SELFDESTRUCT, and
exceptional halts return the empty slice; RETURN and REVERT carry
their frozen memory slice in the halt value.
function interpret(
initial_gas : gas,
initial_state_gas : state_gas,
initial_state_spill : state_gas_spill,
initial_refund : gas_refund,
initial_sp : StackPointer,
initial_memory_base : memory_base,
initial_memory_height : memory_height,
initial_caller : address,
initial_address : address,
initial_code_address : address,
initial_value : word,
initial_state_gas_reservoir : state_gas,
initial_is_static : bool,
initial_depth : frame_depth,
initial_code : Code,
initial_calldata : CalldataSlice,
) -> (
(gas, state_gas, state_gas_spill, gas_refund, FrameStatus, OutputSlice)
) = {
let execution_profile = k_execution_profile;
let profile = execution_profile.protocol;
let fork = profile.fork;
let blob_fee = blob_base_fee(fork, profile.blob_schedule, profile.excess_blob_gas_limit, k_header.excess_blob_gas);
frame_stack_reset();
var interpreting : bool = true;
var result : OutputSlice = EMPTY_OUTPUT_SLICE;
var carried_pc : code_pointer = 0;
var carried_sp : StackPointer = initial_sp;
var carried_memory_base : memory_base = initial_memory_base;
var carried_memory_height : memory_height = initial_memory_height;
var carried_gas : gas = initial_gas;
var carried_state_gas : state_gas = initial_state_gas;
var carried_state_spill : state_gas_spill = initial_state_spill;
var carried_refund : gas_refund = initial_refund;
var carried_status : FrameStatus = Running();
var carried_caller : address = initial_caller;
var carried_address : address = initial_address;
var carried_account_context : AccountExecutionContext = account_execution_context(initial_address);
var carried_code_address : address = initial_code_address;
var carried_value : word = initial_value;
var carried_state_gas_reservoir : state_gas = initial_state_gas_reservoir;
var carried_is_static : bool = initial_is_static;
var carried_depth : frame_depth = initial_depth;
var carried_code : Code = initial_code;
var carried_calldata : CalldataSlice = initial_calldata;
var carried_returndata : OutputSlice = EMPTY_OUTPUT_SLICE;
let initial_call_tree_gas = initial_gas + initial_state_gas;
var call_tree_steps_remaining : call_tree_steps = 3 * initial_call_tree_gas + 2;
while interpreting termination_measure(call_tree_steps_remaining) do {
let running = is_running(carried_status);
if running then {
let (fetched_pc, instruction) = fetch(carried_code, carried_pc, fork);
carried_pc = fetched_pc;
match instruction {
opcode_CREATE() => {
let previous_address = carried_address;
let transition = run_create(
carried_pc,
carried_gas,
carried_state_gas,
carried_state_spill,
carried_refund,
carried_sp,
carried_memory_base,
carried_memory_height,
carried_caller,
carried_address,
carried_code_address,
carried_value,
carried_state_gas_reservoir,
carried_is_static,
carried_depth,
carried_code,
carried_calldata,
carried_returndata,
CreateByNonce,
);
carried_pc = transition.pc;
carried_gas = transition.gas_remaining;
carried_state_gas = transition.state_gas_remaining;
carried_state_spill = transition.state_gas_spilled;
carried_refund = transition.refund;
carried_status = transition.status;
carried_sp = transition.stack_top;
carried_memory_base = transition.memory_base;
carried_memory_height = transition.memory_height;
carried_caller = transition.message.caller;
carried_address = transition.message.address;
carried_code_address = transition.message.code_address;
carried_value = transition.message.value;
carried_state_gas_reservoir = transition.message.state_gas_reservoir;
carried_is_static = transition.message.is_static;
carried_depth = transition.message.depth;
carried_code = transition.code;
carried_calldata = transition.calldata;
carried_returndata = transition.returndata;
carried_account_context = refresh_account_execution_context(
carried_account_context,
previous_address,
carried_address,
)
},
CREATE2() => {
let previous_address = carried_address;
let transition = run_create(
carried_pc,
carried_gas,
carried_state_gas,
carried_state_spill,
carried_refund,
carried_sp,
carried_memory_base,
carried_memory_height,
carried_caller,
carried_address,
carried_code_address,
carried_value,
carried_state_gas_reservoir,
…Appends a frame marker to the state journal. The suspended frame stores its refund counter separately.
function k_journal_checkpoint() -> unit = state_journal_checkpoint()function stack_reset() -> StackPointer =
struct { storage = stack_reset_host(), height = 0 }let GAS_REFUND_ZERO : gas_refund = 0The empty EVM-memory high-water mark.
let MEMORY_HEIGHT_ZERO : memory_height = 0let STATE_GAS_SPILL_ZERO : int(0) = 0let STATE_GAS_ZERO : int(0) = 0The pseudo-caller of protocol system calls (EIP-4788, EIP-2935, EIP-7002, EIP-7251, EIP-8282).
let SYSTEM_ADDRESS : address = address_from_bits(0x000000000000000000000000fffffffffffffffffffffffffffffffffffffffe)The execution-gas allowance of each protocol system call (EIP-4788, EIP-2935, EIP-7002, EIP-7251, and EIP-8282).
let SYSTEM_CALL_GAS_LIMIT : int(30000000) = 30000000let ZERO_WORD : word = word_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)Calldata is either the immutable top-level transaction input or a frozen range of the suspended caller's memory. The variants state the only two protocol-valid provenances instead of exposing the host's region enum.
union CalldataSlice = {
/* the immutable top-level transaction input */
InputCalldata : StatelessInputSlice,
/* a frozen range of the suspended caller's memory */
MemoryCalldata : EvmMemorySlice,
}Existential executable-code value whose concrete byte address and length
remain correlated inside CodeFields.
type Code = {
'off 'len,
code_region_valid_range('off, 'len) & code_valid_length('len).
CodeFields('off, 'len)
}Per-frame execution status: running, halted normally, or exceptionally halted.
union FrameStatus = {
/* mid-execution */
Running : unit,
/* halted normally (YP §9.4.4) */
Halted : HaltKind,
/* halted exceptionally: all frame gas consumed, effects void */
Exceptional : ExceptionKind
}A frame-output range with its coordinate and length packed existentially.
type OutputSlice = {
'off 'len,
output_region_valid_range('off, 'len).
OutputSliceFields('off, 'len)
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)Available gas in a running EVM frame. Every admitted transaction gas
limit originates in the execution payload's SSZ uint64 gas-limit
domain, and child frames can only receive gas from their parent.
type gas = range(0, 2 ^ 64 - 1)The signed transaction refund accumulator before capping.
type gas_refund = range(
-gas_refund_bound,
gas_refund_bound,
)An absolute byte position in the shared EVM-memory arena.
type memory_base = range(0, memory_region_bound)Amsterdam's per-frame state-gas reservoir. The transaction's total gas
allowance remains in the execution payload's uint64 domain; only the
regular-gas portion and state-gas spill into that portion are capped by
EIP-7825.
type state_gas = range(0, 2 ^ 64 - 1)Execution gas temporarily consumed by Amsterdam state charges. EIP-8037 draws spill only from the regular-gas pool, which is capped by EIP-7825.
type state_gas_spill = range(0, transaction_execution_gas_limit_value)function system_call¶
Issues one unchecked block-start system call: a 30M-gas frame from
SYSTEM_ADDRESS with a 32-byte input; skipped when the target has no
code, and its output is discarded.
function system_call(tgt : address, input : hash) -> unit = {
let code_hash = k_code_key(tgt);
if code_hash == KECCAK_EMPTY then {
return () /* system contract absent -> skip (EIP-4788 / EIP-2935) */
};
let code = code_db_resolve(code_hash);
/* Freeze the word below the system-call frame, so the child's memory
* writes cannot mutate its calldata. */
let initial_memory_base = MEMORY_BASE_ZERO;
let initial_memory_height = MEMORY_HEIGHT_ZERO;
let input_range : MemoryRange = memory_range(0, SYSTEM_CALL_INPUT_LENGTH);
let expanded_memory = expand_memory(initial_memory_base, initial_memory_height, input_range.len);
let input_word = hash_to_word(input);
mem_store(initial_memory_base, input_range.off, input_word);
let input_slice = active_memory_slice(initial_memory_base, expanded_memory, input_range.off, input_range.len);
let child_memory_base = memory_absolute(initial_memory_base, expanded_memory);
let memory_input = evm_memory_slice(input_slice.bytes, input_slice.len);
let frame_input = MemoryCalldata(memory_input);
let (_, _, _, _, status, _) = run_system_call_frame(tgt, code, frame_input, child_memory_base);
let succeeded = frame_succeeded(status);
let failed = not_bool(succeeded);
if failed then {
k_journal_revert()
} else {
k_journal_commit()
};
k_tx_merge() /* system call is a top-level boundary: merge its storage */
}function active_memory_slice(base, mem, off, len) =
if len == 0 then {
EMPTY_EVM_MEMORY_SLICE
} else if mem <= sizeof(memory_region_bound) - base & off + len <= mem then {
let window = mem_view(base, mem, off + len);
sub_slice(window, off, len)
} else {
fatal_error(ExecutionInvalid)
}The code for a code hash; KECCAK_EMPTY resolves to empty code, and
an unwitnessed hash is a deficient witness.
function code_db_resolve(code_hash : hash) -> Code =
if code_hash == KECCAK_EMPTY then {
EMPTY_CODE
} else {
let code = code_db_lookup(code_hash);
if code.len == 0 then {
fatal_error(WitnessDeficient)
} else {
code
}
}function evm_memory_slice(off, len) =
struct { bytes = off, len = len }Materializes an already-charged memory high-water mark and returns its updated scalar height.
function expand_memory(base : memory_base, height : memory_height, requested_height : memory_length) -> memory_height = {
if requested_height <= sizeof(memory_region_bound) - base then {
if height < requested_height then {
mem_expand(base, height, requested_height);
requested_height
} else {
height
}
} else {
fatal_error(ExecutionInvalid)
}
}Whether the just-finished frame ended successfully: a normal halt
succeeds; a REVERT and any exceptional halt do not (their world
effects are rolled back and CALL/CREATE reports failure).
function frame_succeeded(frame_status : FrameStatus) -> bool =
match frame_status {
Halted(HaltRevert(_)) => false,
Halted(_) => true,
Running() => true,
Exceptional(_) => false,
}Interprets a digest as the corresponding big-endian EVM word.
function hash_to_word(bytes : hash) -> word =
unsigned(
bytes[0]
@ bytes[1]
@ bytes[2]
@ bytes[3]
@ bytes[4]
@ bytes[5]
@ bytes[6]
@ bytes[7]
@ bytes[8]
@ bytes[9]
@ bytes[10]
@ bytes[11]
@ bytes[12]
@ bytes[13]
@ bytes[14]
@ bytes[15]
@ bytes[16]
@ bytes[17]
@ bytes[18]
@ bytes[19]
@ bytes[20]
@ bytes[21]
@ bytes[22]
@ bytes[23]
@ bytes[24]
@ bytes[25]
@ bytes[26]
@ bytes[27]
@ bytes[28]
@ bytes[29]
@ bytes[30]
@ bytes[31],
)The account's code hash — the code-store key.
function k_code_key(a : address) -> hash = k_aload(a).info.code_hashRecords a successful child frame without discarding its reversible entries.
function k_journal_commit() -> unit = state_journal_commit()Replays the state journal backwards to its innermost open frame boundary.
function k_journal_revert() -> unit = state_journal_revert()The transaction-end merge: drains the transaction overlays into the block layer, applying the fork-specific selfdestruct clearing rule, storage-clear generations, and recording nonce/balance/code/storage changes for the EIP-7928 block access list. Lifecycle flags reset as rows merge.
function k_tx_merge() -> unit = {
let execution_profile = k_execution_profile;
let profile = execution_profile.protocol;
let semantics = transaction_merge_semantics(profile.fork);
var more : bool = true;
/* Each pop advances a cursor over a protocol-sized host table. */
while more termination_measure(2 ^ 64) do {
let popped_account = acct_tx_pop();
match popped_account {
AcctTxPopRow(e) => {
var curr : Account = e.value.curr;
let deleted = account_deleted_at_tx_end(semantics, curr);
if deleted then {
let cleared_account =
if semantics.preserve_selfdestruct_balance
then account_clear_preserving_balance(curr)
else account_delete(curr);
curr = cleared_account;
/* The account's active transaction generation belongs to
the deleted incarnation. Retire it before the storage
drain so its writes cannot be reinserted after the
block-layer clear. */
storage_tx_clear(e.addr)
};
let original_storage_retained = not_bool(e.value.orig.storage_cleared);
if deleted | (curr.storage_cleared & original_storage_retained) then {
storage_block_clear(e.addr)
};
if curr.info.nonce != e.value.orig.info.nonce then {
bal_nonce_change(k_current_transaction_epoch, e.addr, curr.info.nonce)
};
if curr.info.balance != e.value.orig.info.balance then {
bal_balance_change(k_current_transaction_epoch, e.addr, curr.info.balance)
};
if curr.info.code_hash != e.value.orig.info.code_hash then {
bal_code_change(k_current_transaction_epoch, e.addr, curr.info.code_hash)
};
curr = { curr with created = false, selfdestructed = false };
let changed = account_changed(curr, e.value.orig);
if changed then {
acct_block_write(struct { addr = e.addr, value = struct { curr = curr, orig = e.value.orig } })
}
},
AcctTxPopExhausted(_) => more = false,
}
};
more = true;
/* Each pop advances a cursor over a protocol-sized host table. */
while more termination_measure(2 ^ 64) do {
let popped_storage = storage_tx_pop();
match popped_storage {
StorageTxPopRow(e) => {
let account = acct_block_get(e.key.addr);
if account.found then {
let acc = account.account;
if acc.present & e.value.curr != e.value.orig then {
bal_storage_change(k_current_transaction_epoch, e.key.addr, e.key.slot, e.value.curr);
storage_block_put(e)
}
}
},
StorageTxPopExhausted(_) => more = false,
}
};
storage_tx_reset();
acct_tx_reset()
}MSTORE: writes the big-endian word at off and raises the
high-water mark.
function mem_store(base : memory_base, off : memory_base, w : word) -> unit = {
let absolute_offset = memory_absolute(base, off);
mem_store_word(absolute_offset, w)
}Converts a frame-relative coordinate to an absolute arena coordinate.
function memory_absolute(base : memory_base, relative : memory_length) -> memory_base =
if relative <= sizeof(memory_region_bound) - base then {
base + relative
} else {
fatal_error(ExecutionInvalid)
}function memory_range(off, len) = struct { off = off, len = len }val not_bool = pure {coq: "negb", lean: "_lean_not", _: "not"}: forall ('p : Bool). bool('p) -> bool(not('p))Runs a top-level protocol system-call frame. The caller has already
resolved code, made a fresh memory frame and, for a word input, frozen
the parent-memory span that input references.
function run_system_call_frame(
tgt : address,
code : Code,
input : CalldataSlice,
memory_base : memory_base,
) -> (
(gas, state_gas, state_gas_spill, gas_refund, FrameStatus, OutputSlice)
) = {
k_journal_checkpoint();
let stack_top = stack_reset();
interpret(
SYSTEM_CALL_GAS_LIMIT,
STATE_GAS_ZERO,
STATE_GAS_SPILL_ZERO,
GAS_REFUND_ZERO,
stack_top,
memory_base,
MEMORY_HEIGHT_ZERO,
SYSTEM_ADDRESS,
tgt,
tgt,
ZERO_WORD,
STATE_GAS_ZERO,
false,
0,
code,
input,
)
}keccak256 of the empty string: the codeHash of every codeless
account.
let KECCAK_EMPTY : hash = hash_from_bits(0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470)The top-level frame begins at the shared arena's semantic offset zero.
let MEMORY_BASE_ZERO : memory_base = 0The empty EVM-memory high-water mark.
let MEMORY_HEIGHT_ZERO : memory_height = 0let SYSTEM_CALL_INPUT_LENGTH : int(32) = WORD_BYTE_LENGTHA memory range retaining its offset, length, and containment proof.
type MemoryRange = {
'off 'len,
memory_valid_range('off, 'len). MemoryRangeFields('off, 'len)
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)The common digest type used by trie, code, and block hashes.
type hash = b256function system_call_checked¶
Issues one checked block-end system call (EIP-7002/EIP-7251/EIP-8282): the target must exist and the call must succeed. Missing code or frame failure throws immediately; a successful call returns the dequeued requests.
function system_call_checked(tgt : address) -> ScratchSlice = {
let code_hash = k_code_key(tgt);
if code_hash == KECCAK_EMPTY then {
fatal_error(ExecutionInvalid)
} else {
let code = code_db_resolve(code_hash);
let (_, _, _, _, status, output) = run_system_call_frame(tgt, code, EMPTY_CALLDATA, MEMORY_BASE_ZERO);
let succeeded = frame_succeeded(status);
if succeeded then {
let start = scratch_reserve(output.len);
scratch_push_slice(output);
let result = scratch_finish(start);
k_journal_commit();
k_tx_merge(); /* system call is a top-level boundary: merge its storage */
result
} else {
k_journal_revert();
k_tx_merge();
fatal_error(ExecutionInvalid)
}
}
}The code for a code hash; KECCAK_EMPTY resolves to empty code, and
an unwitnessed hash is a deficient witness.
function code_db_resolve(code_hash : hash) -> Code =
if code_hash == KECCAK_EMPTY then {
EMPTY_CODE
} else {
let code = code_db_lookup(code_hash);
if code.len == 0 then {
fatal_error(WitnessDeficient)
} else {
code
}
}function fatal_error(_reason) = exit(())Whether the just-finished frame ended successfully: a normal halt
succeeds; a REVERT and any exceptional halt do not (their world
effects are rolled back and CALL/CREATE reports failure).
function frame_succeeded(frame_status : FrameStatus) -> bool =
match frame_status {
Halted(HaltRevert(_)) => false,
Halted(_) => true,
Running() => true,
Exceptional(_) => false,
}The account's code hash — the code-store key.
function k_code_key(a : address) -> hash = k_aload(a).info.code_hashRecords a successful child frame without discarding its reversible entries.
function k_journal_commit() -> unit = state_journal_commit()Replays the state journal backwards to its innermost open frame boundary.
function k_journal_revert() -> unit = state_journal_revert()The transaction-end merge: drains the transaction overlays into the block layer, applying the fork-specific selfdestruct clearing rule, storage-clear generations, and recording nonce/balance/code/storage changes for the EIP-7928 block access list. Lifecycle flags reset as rows merge.
function k_tx_merge() -> unit = {
let execution_profile = k_execution_profile;
let profile = execution_profile.protocol;
let semantics = transaction_merge_semantics(profile.fork);
var more : bool = true;
/* Each pop advances a cursor over a protocol-sized host table. */
while more termination_measure(2 ^ 64) do {
let popped_account = acct_tx_pop();
match popped_account {
AcctTxPopRow(e) => {
var curr : Account = e.value.curr;
let deleted = account_deleted_at_tx_end(semantics, curr);
if deleted then {
let cleared_account =
if semantics.preserve_selfdestruct_balance
then account_clear_preserving_balance(curr)
else account_delete(curr);
curr = cleared_account;
/* The account's active transaction generation belongs to
the deleted incarnation. Retire it before the storage
drain so its writes cannot be reinserted after the
block-layer clear. */
storage_tx_clear(e.addr)
};
let original_storage_retained = not_bool(e.value.orig.storage_cleared);
if deleted | (curr.storage_cleared & original_storage_retained) then {
storage_block_clear(e.addr)
};
if curr.info.nonce != e.value.orig.info.nonce then {
bal_nonce_change(k_current_transaction_epoch, e.addr, curr.info.nonce)
};
if curr.info.balance != e.value.orig.info.balance then {
bal_balance_change(k_current_transaction_epoch, e.addr, curr.info.balance)
};
if curr.info.code_hash != e.value.orig.info.code_hash then {
bal_code_change(k_current_transaction_epoch, e.addr, curr.info.code_hash)
};
curr = { curr with created = false, selfdestructed = false };
let changed = account_changed(curr, e.value.orig);
if changed then {
acct_block_write(struct { addr = e.addr, value = struct { curr = curr, orig = e.value.orig } })
}
},
AcctTxPopExhausted(_) => more = false,
}
};
more = true;
/* Each pop advances a cursor over a protocol-sized host table. */
while more termination_measure(2 ^ 64) do {
let popped_storage = storage_tx_pop();
match popped_storage {
StorageTxPopRow(e) => {
let account = acct_block_get(e.key.addr);
if account.found then {
let acc = account.account;
if acc.present & e.value.curr != e.value.orig then {
bal_storage_change(k_current_transaction_epoch, e.key.addr, e.key.slot, e.value.curr);
storage_block_put(e)
}
}
},
StorageTxPopExhausted(_) => more = false,
}
};
storage_tx_reset();
acct_tx_reset()
}Runs a top-level protocol system-call frame. The caller has already
resolved code, made a fresh memory frame and, for a word input, frozen
the parent-memory span that input references.
function run_system_call_frame(
tgt : address,
code : Code,
input : CalldataSlice,
memory_base : memory_base,
) -> (
(gas, state_gas, state_gas_spill, gas_refund, FrameStatus, OutputSlice)
) = {
k_journal_checkpoint();
let stack_top = stack_reset();
interpret(
SYSTEM_CALL_GAS_LIMIT,
STATE_GAS_ZERO,
STATE_GAS_SPILL_ZERO,
GAS_REFUND_ZERO,
stack_top,
memory_base,
MEMORY_HEIGHT_ZERO,
SYSTEM_ADDRESS,
tgt,
tgt,
ZERO_WORD,
STATE_GAS_ZERO,
false,
0,
code,
input,
)
}The slice covering everything pushed since start.
function scratch_finish(start : source_pointer) -> ScratchSlice =
let start_offset = start in
let arena = scratch_arena in
let stop_offset = arena.len in
if start_offset <= stop_offset then {
sub_slice(arena, start, stop_offset - start_offset)
} else {
assert(false, "scratch finish mark");
EMPTY_SCRATCH_SLICE
}function scratch_reserve(len) = {
let arena = scratch_arena;
let reserved = host_scratch_reserve(arena.len, len);
assert(reserved, "scratch reserve");
arena.len
}let EMPTY_CALLDATA : CalldataSlice = InputCalldata(EMPTY_STATELESS_INPUT_SLICE)keccak256 of the empty string: the codeHash of every codeless
account.
let KECCAK_EMPTY : hash = hash_from_bits(0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470)The top-level frame begins at the shared arena's semantic offset zero.
let MEMORY_BASE_ZERO : memory_base = 0The reason a block fails validation; one variant per violated block-validity rule.
enum FatalError = {
/* chain config: wrong fork / inactive activation */
InvalidConfig,
/* witness ancestor headers not contiguous */
HeaderChainBroken,
/* a transaction failed to RLP-decode */
RlpDecode,
/* a tx signature did not authenticate its sender */
InvalidSignature,
/* header.gas_limit is outside the consensus domain */
InvalidGasLimit,
/* EIP-7778: a tx exceeds the block's remaining gas */
GasUsedExceedsLimit,
/* a tx exceeds the block's remaining blob gas */
BlobGasLimitExceeded,
/* an invalid tx or a failed block-end system call */
ExecutionInvalid,
/* recomputed cumulative gas != header.gas_used */
InvalidGasUsed,
/* recomputed blob gas != header.blob_gas_used */
InvalidBlobGasUsed,
/* header.excess_blob_gas != expected */
InvalidExcessBlobGas,
/* recomputed post-state root != header.state_root */
InvalidStateRoot,
/* recomputed receipts root != header.receipts_root */
InvalidReceiptsRoot,
/* recomputed logs bloom != header.logs_bloom */
InvalidLogsBloom,
/* recomputed block hash != payload expected hash */
InvalidBlockHash,
/* header.parent_hash != authenticated parent */
InvalidParentHash,
/* EIP-7928: BAL item count > gas_limit / 2000 */
BlockAccessListTooLarge,
/* reconstructed EIP-7928 BAL bytes mismatch */
InvalidBlockAccessList,
/* reconstructed EIP-7685 request bytes mismatch */
InvalidExecutionRequests,
/* a missing/inconsistent proof node (thrown at use) */
WitnessDeficient,
/* an exact protocol integer exceeds its bounded execution representation */
NumericOverflow,
}A scratch-arena range with its coordinate and length packed existentially.
type ScratchSlice = {
'off 'len,
scratch_valid_range('off, 'len).
ScratchSliceFields('off, 'len)
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)function deposit_log_matches¶
Whether a retained log is a DepositEvent from the deposit contract
(EIP-6110).
function deposit_log_matches(index : log_store_index) -> bool =
let address = log_address(index) in
if address != DEPOSIT_CONTRACT_ADDR then {
false
} else {
let topic_count = log_topics_count(index);
if topic_count == 0 then {
false
} else {
let first_topic = log_topic(index, 0);
first_topic == DEPOSIT_EVENT_TOPIC
}
}Indexed access to a retained log record.
val log_address = impure { c: "log_addr" } : log_store_index -> addressReads one topic from an indexed retained log.
val log_topic = impure { c: "log_topic" } : (log_store_index, log_store_index) -> wordNumber of topics attached to an indexed retained log.
val log_topics_count = impure { c: "log_topic_count" } : log_store_index -> log_store_indexlet DEPOSIT_CONTRACT_ADDR : address = address_from_bits(
0x00000000000000000000000000000000219ab540356cbb839cbe05303d7705fa,
)let DEPOSIT_EVENT_TOPIC : word = word_from_bits(0x649bbc62d0e31342afea4e5cd82d4049e7e1ee912fc0889aa790803be39038c5)A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)A position in the block-lifetime host log store.
type log_store_index = range(0, log_store_index_bound)function authenticate_deposit_request¶
Validates one DepositEvent ABI payload against the next authenticated
consensus-layer deposit request and returns the unconsumed request
suffix (EIP-6110).
function authenticate_deposit_request(data : LogDataSlice, expected : StatelessInputSlice) -> StatelessInputSlice = {
let data : LogDataSliceLength(576) =
if data.len == DEPOSIT_EVENT_DATA_LENGTH then data else fatal_error(InvalidExecutionRequests);
let pubkey_head = slice_load(data, DEPOSIT_PUBKEY_HEAD);
let withdrawal_credentials_head = slice_load(data, DEPOSIT_WITHDRAWAL_CREDENTIALS_HEAD);
let amount_head = slice_load(data, DEPOSIT_AMOUNT_HEAD);
let signature_head = slice_load(data, DEPOSIT_SIGNATURE_HEAD);
let index_head = slice_load(data, DEPOSIT_INDEX_HEAD);
let pubkey_length = slice_load(data, DEPOSIT_PUBKEY_LENGTH_WORD);
let withdrawal_credentials_length = slice_load(data, DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH_WORD);
let amount_length = slice_load(data, DEPOSIT_AMOUNT_LENGTH_WORD);
let signature_length = slice_load(data, DEPOSIT_SIGNATURE_LENGTH_WORD);
let index_length = slice_load(data, DEPOSIT_INDEX_LENGTH_WORD);
let expected_pubkey_head : word = u256(160);
let expected_withdrawal_credentials_head : word = u256(256);
let expected_amount_head : word = u256(320);
let expected_signature_head : word = u256(384);
let expected_index_head : word = u256(512);
let expected_pubkey_length : word = u256(48);
let expected_withdrawal_credentials_length : word = u256(32);
let expected_amount_length : word = u256(8);
let expected_signature_length : word = u256(96);
let expected_index_length : word = u256(8);
if pubkey_head != expected_pubkey_head then {
fatal_error(InvalidExecutionRequests)
};
if withdrawal_credentials_head != expected_withdrawal_credentials_head then {
fatal_error(InvalidExecutionRequests)
};
if amount_head != expected_amount_head then {
fatal_error(InvalidExecutionRequests)
};
if signature_head != expected_signature_head then {
fatal_error(InvalidExecutionRequests)
};
if index_head != expected_index_head then {
fatal_error(InvalidExecutionRequests)
};
if pubkey_length != expected_pubkey_length then {
fatal_error(InvalidExecutionRequests)
};
if withdrawal_credentials_length != expected_withdrawal_credentials_length then {
fatal_error(InvalidExecutionRequests)
};
if amount_length != expected_amount_length then {
fatal_error(InvalidExecutionRequests)
};
if signature_length != expected_signature_length then {
fatal_error(InvalidExecutionRequests)
};
if index_length != expected_index_length then {
fatal_error(InvalidExecutionRequests)
};
if DEPOSIT_REQUEST_LENGTH <= expected.len then {
let log_pubkey = sub_slice(data, DEPOSIT_PUBKEY_DATA, DEPOSIT_PUBKEY_LENGTH);
let expected_pubkey = sub_slice(expected, DEPOSIT_REQUEST_PUBKEY, DEPOSIT_PUBKEY_LENGTH);
let pubkey_matches = region_slices_equal(log_pubkey, expected_pubkey);
let pubkey_mismatch = not_bool(pubkey_matches);
let log_withdrawal_credentials = sub_slice(
data,
DEPOSIT_WITHDRAWAL_CREDENTIALS_DATA,
DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH,
);
let expected_withdrawal_credentials = sub_slice(
expected,
DEPOSIT_REQUEST_WITHDRAWAL_CREDENTIALS,
DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH,
);
let withdrawal_credentials_match = region_slices_equal(
log_withdrawal_credentials,
expected_withdrawal_credentials,
);
let withdrawal_credentials_mismatch = not_bool(withdrawal_credentials_match);
let log_amount = sub_slice(data, DEPOSIT_AMOUNT_DATA, DEPOSIT_AMOUNT_LENGTH);
let expected_amount = sub_slice(expected, DEPOSIT_REQUEST_AMOUNT, DEPOSIT_AMOUNT_LENGTH);
let amount_matches = region_slices_equal(log_amount, expected_amount);
let amount_mismatch = not_bool(amount_matches);
let log_signature = sub_slice(data, DEPOSIT_SIGNATURE_DATA, DEPOSIT_SIGNATURE_LENGTH);
let expected_signature = sub_slice(expected, DEPOSIT_REQUEST_SIGNATURE, DEPOSIT_SIGNATURE_LENGTH);
let signature_matches = region_slices_equal(log_signature, expected_signature);
let signature_mismatch = not_bool(signature_matches);
let log_index = sub_slice(data, DEPOSIT_INDEX_DATA, DEPOSIT_INDEX_LENGTH);
let expected_index = sub_slice(expected, DEPOSIT_REQUEST_INDEX, DEPOSIT_INDEX_LENGTH);
let index_matches = region_slices_equal(log_index, expected_index);
let index_mismatch = not_bool(index_matches);
if pubkey_mismatch | withdrawal_credentials_mismatch | amount_mismatch | signature_mismatch | index_mismatch then {
fatal_error(InvalidExecutionRequests)
};
slice_suffix(expected, DEPOSIT_REQUEST_LENGTH)
} else {
fatal_error(InvalidExecutionRequests)
}
}function fatal_error(_reason) = exit(())Reports byte-for-byte equality of a retained-log-data span and a stateless-input span; spans of unequal length are unequal.
val log_input_slices_equal = impure { c: "log_input_slices_equal" } : (LogDataSlice, StatelessInputSlice) -> boolval not_bool = pure {coq: "negb", lean: "_lean_not", _: "not"}: forall ('p : Bool). bool('p) -> bool(not('p))function u256(value) = valuelet DEPOSIT_AMOUNT_DATA : int(352) = 352let DEPOSIT_AMOUNT_HEAD : int(64) = 64let DEPOSIT_AMOUNT_LENGTH : int(8) = EIGHT_BYTE_LENGTHlet DEPOSIT_AMOUNT_LENGTH_WORD : int(320) = 320let DEPOSIT_EVENT_DATA_LENGTH : int(576) = 576let DEPOSIT_INDEX_DATA : int(544) = 544let DEPOSIT_INDEX_HEAD : int(128) = 128let DEPOSIT_INDEX_LENGTH : int(8) = EIGHT_BYTE_LENGTHlet DEPOSIT_INDEX_LENGTH_WORD : int(512) = 512let DEPOSIT_PUBKEY_DATA : int(192) = 192let DEPOSIT_PUBKEY_LENGTH : int(48) = 48let DEPOSIT_PUBKEY_LENGTH_WORD : int(160) = 160let DEPOSIT_REQUEST_AMOUNT : int(80) = 80let DEPOSIT_REQUEST_INDEX : int(184) = 184let DEPOSIT_REQUEST_LENGTH : int(192) = 192let DEPOSIT_REQUEST_PUBKEY : int(0) = 0let DEPOSIT_REQUEST_SIGNATURE : int(88) = 88let DEPOSIT_REQUEST_WITHDRAWAL_CREDENTIALS : int(48) = 48let DEPOSIT_SIGNATURE_DATA : int(416) = 416let DEPOSIT_SIGNATURE_HEAD : int(96) = 96let DEPOSIT_SIGNATURE_LENGTH : int(96) = 96let DEPOSIT_SIGNATURE_LENGTH_WORD : int(384) = 384let DEPOSIT_WITHDRAWAL_CREDENTIALS_DATA : int(288) = 288let DEPOSIT_WITHDRAWAL_CREDENTIALS_HEAD : int(32) = 32let DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH : int(32) = WORD_BYTE_LENGTHlet DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH_WORD : int(256) = 256The reason a block fails validation; one variant per violated block-validity rule.
enum FatalError = {
/* chain config: wrong fork / inactive activation */
InvalidConfig,
/* witness ancestor headers not contiguous */
HeaderChainBroken,
/* a transaction failed to RLP-decode */
RlpDecode,
/* a tx signature did not authenticate its sender */
InvalidSignature,
/* header.gas_limit is outside the consensus domain */
InvalidGasLimit,
/* EIP-7778: a tx exceeds the block's remaining gas */
GasUsedExceedsLimit,
/* a tx exceeds the block's remaining blob gas */
BlobGasLimitExceeded,
/* an invalid tx or a failed block-end system call */
ExecutionInvalid,
/* recomputed cumulative gas != header.gas_used */
InvalidGasUsed,
/* recomputed blob gas != header.blob_gas_used */
InvalidBlobGasUsed,
/* header.excess_blob_gas != expected */
InvalidExcessBlobGas,
/* recomputed post-state root != header.state_root */
InvalidStateRoot,
/* recomputed receipts root != header.receipts_root */
InvalidReceiptsRoot,
/* recomputed logs bloom != header.logs_bloom */
InvalidLogsBloom,
/* recomputed block hash != payload expected hash */
InvalidBlockHash,
/* header.parent_hash != authenticated parent */
InvalidParentHash,
/* EIP-7928: BAL item count > gas_limit / 2000 */
BlockAccessListTooLarge,
/* reconstructed EIP-7928 BAL bytes mismatch */
InvalidBlockAccessList,
/* reconstructed EIP-7685 request bytes mismatch */
InvalidExecutionRequests,
/* a missing/inconsistent proof node (thrown at use) */
WitnessDeficient,
/* an exact protocol integer exceeds its bounded execution representation */
NumericOverflow,
}A log-data range with its coordinate and length packed existentially.
type LogDataSlice = {
'off 'len,
log_data_valid_range('off, 'len).
LogDataSliceFields('off, 'len)
}A log-data range of exactly 'required bytes.
type LogDataSliceLength('required : Int) = {
'off,
log_data_valid_range('off, 'required).
LogDataSliceFields('off, 'required)
}A stateless-input range with its coordinate and length packed existentially.
type StatelessInputSlice = {
'off 'len,
stateless_input_valid_range('off, 'len).
StatelessInputSliceFields('off, 'len)
}The EVM 256-bit machine word (YP §9.1). A transparent range keeps the mathematical subtype relation visible: narrower non-negative ranges can be passed as words without a model-level conversion.
type word = range(0, 2 ^ 256 - 1)function authenticate_deposit_logs¶
Authenticates matching deposit logs in emission order and returns the unconsumed suffix of the expected request bytes.
function authenticate_deposit_logs(logs : LogSeriesRef, expected : StatelessInputSlice) -> StatelessInputSlice = {
var remaining : StatelessInputSlice = expected;
var offset : log_store_index = 0;
while offset < logs.count termination_measure(logs.count - offset) do {
let index = log_store_index_add(logs.start, offset);
let matches = deposit_log_matches(index);
if matches then {
let data = read_log_data(index);
remaining = authenticate_deposit_request(data, remaining)
};
offset = log_store_index_increment(offset)
};
remaining
}Validates one DepositEvent ABI payload against the next authenticated
consensus-layer deposit request and returns the unconsumed request
suffix (EIP-6110).
function authenticate_deposit_request(data : LogDataSlice, expected : StatelessInputSlice) -> StatelessInputSlice = {
let data : LogDataSliceLength(576) =
if data.len == DEPOSIT_EVENT_DATA_LENGTH then data else fatal_error(InvalidExecutionRequests);
let pubkey_head = slice_load(data, DEPOSIT_PUBKEY_HEAD);
let withdrawal_credentials_head = slice_load(data, DEPOSIT_WITHDRAWAL_CREDENTIALS_HEAD);
let amount_head = slice_load(data, DEPOSIT_AMOUNT_HEAD);
let signature_head = slice_load(data, DEPOSIT_SIGNATURE_HEAD);
let index_head = slice_load(data, DEPOSIT_INDEX_HEAD);
let pubkey_length = slice_load(data, DEPOSIT_PUBKEY_LENGTH_WORD);
let withdrawal_credentials_length = slice_load(data, DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH_WORD);
let amount_length = slice_load(data, DEPOSIT_AMOUNT_LENGTH_WORD);
let signature_length = slice_load(data, DEPOSIT_SIGNATURE_LENGTH_WORD);
let index_length = slice_load(data, DEPOSIT_INDEX_LENGTH_WORD);
let expected_pubkey_head : word = u256(160);
let expected_withdrawal_credentials_head : word = u256(256);
let expected_amount_head : word = u256(320);
let expected_signature_head : word = u256(384);
let expected_index_head : word = u256(512);
let expected_pubkey_length : word = u256(48);
let expected_withdrawal_credentials_length : word = u256(32);
let expected_amount_length : word = u256(8);
let expected_signature_length : word = u256(96);
let expected_index_length : word = u256(8);
if pubkey_head != expected_pubkey_head then {
fatal_error(InvalidExecutionRequests)
};
if withdrawal_credentials_head != expected_withdrawal_credentials_head then {
fatal_error(InvalidExecutionRequests)
};
if amount_head != expected_amount_head then {
fatal_error(InvalidExecutionRequests)
};
if signature_head != expected_signature_head then {
fatal_error(InvalidExecutionRequests)
};
if index_head != expected_index_head then {
fatal_error(InvalidExecutionRequests)
};
if pubkey_length != expected_pubkey_length then {
fatal_error(InvalidExecutionRequests)
};
if withdrawal_credentials_length != expected_withdrawal_credentials_length then {
fatal_error(InvalidExecutionRequests)
};
if amount_length != expected_amount_length then {
fatal_error(InvalidExecutionRequests)
};
if signature_length != expected_signature_length then {
fatal_error(InvalidExecutionRequests)
};
if index_length != expected_index_length then {
fatal_error(InvalidExecutionRequests)
};
if DEPOSIT_REQUEST_LENGTH <= expected.len then {
let log_pubkey = sub_slice(data, DEPOSIT_PUBKEY_DATA, DEPOSIT_PUBKEY_LENGTH);
let expected_pubkey = sub_slice(expected, DEPOSIT_REQUEST_PUBKEY, DEPOSIT_PUBKEY_LENGTH);
let pubkey_matches = region_slices_equal(log_pubkey, expected_pubkey);
let pubkey_mismatch = not_bool(pubkey_matches);
let log_withdrawal_credentials = sub_slice(
data,
DEPOSIT_WITHDRAWAL_CREDENTIALS_DATA,
DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH,
);
let expected_withdrawal_credentials = sub_slice(
expected,
DEPOSIT_REQUEST_WITHDRAWAL_CREDENTIALS,
DEPOSIT_WITHDRAWAL_CREDENTIALS_LENGTH,
);
let withdrawal_credentials_match = region_slices_equal(
log_withdrawal_credentials,
expected_withdrawal_credentials,
);
let withdrawal_credentials_mismatch = not_bool(withdrawal_credentials_match);
let log_amount = sub_slice(data, DEPOSIT_AMOUNT_DATA, DEPOSIT_AMOUNT_LENGTH);
let expected_amount = sub_slice(expected, DEPOSIT_REQUEST_AMOUNT, DEPOSIT_AMOUNT_LENGTH);
let amount_matches = region_slices_equal(log_amount, expected_amount);
let amount_mismatch = not_bool(amount_matches);
let log_signature = sub_slice(data, DEPOSIT_SIGNATURE_DATA, DEPOSIT_SIGNATURE_LENGTH);
let expected_signature = sub_slice(expected, DEPOSIT_REQUEST_SIGNATURE, DEPOSIT_SIGNATURE_LENGTH);
let signature_matches = region_slices_equal(log_signature, expected_signature);
let signature_mismatch = not_bool(signature_matches);
let log_index = sub_slice(data, DEPOSIT_INDEX_DATA, DEPOSIT_INDEX_LENGTH);
let expected_index = sub_slice(expected, DEPOSIT_REQUEST_INDEX, DEPOSIT_INDEX_LENGTH);
let index_matches = region_slices_equal(log_index, expected_index);
let index_mismatch = not_bool(index_matches);
if pubkey_mismatch | withdrawal_credentials_mismatch | amount_mismatch | signature_mismatch | index_mismatch then {
fatal_error(InvalidExecutionRequests)
};
slice_suffix(expected, DEPOSIT_REQUEST_LENGTH)
} else {
fatal_error(InvalidExecutionRequests)
}
}Whether a retained log is a DepositEvent from the deposit contract
(EIP-6110).
function deposit_log_matches(index : log_store_index) -> bool =
let address = log_address(index) in
if address != DEPOSIT_CONTRACT_ADDR then {
false
} else {
let topic_count = log_topics_count(index);
if topic_count == 0 then {
false
} else {
let first_topic = log_topic(index, 0);
first_topic == DEPOSIT_EVENT_TOPIC
}
}Adds a relative log offset to its series start without wrapping.
function log_store_index_add(left : log_store_index, right : log_store_index) -> log_store_index =
if right <= sizeof(log_store_index_bound) - left then {
left + right
} else {
assert(false, "log store index overflow");
0
}Advances a valid log cursor without fixed-width wrapping.
function log_store_index_increment(value : log_store_index) -> log_store_index =
if value < sizeof(log_store_index_bound) then {
value + 1
} else {
assert(false, "log store index overflow");
0
}Returns the source-backed payload of one retained log record.
function read_log_data(index : log_store_index) -> LogDataSlice = {
let off = log_data_offset(index);
let len = log_data_length(index);
if len <= sizeof(log_data_region_bound) - off then {
log_data_slice(off, len)
} else {
assert(false, "log data slice overflow");
EMPTY_LOG_DATA_SLICE
}
}A consecutive transaction-local view into the block-lifetime host log store. Reverted frame records are removed before this view is captured.
struct LogSeriesRef = {
start : log_store_index,
count : log_store_index,
}A stateless-input range with its coordinate and length packed existentially.
type StatelessInputSlice = {
'off 'len,
stateless_input_valid_range('off, 'len).
StatelessInputSliceFields('off, 'len)
}A position in the block-lifetime host log store.
type log_store_index = range(0, log_store_index_bound)function validate_request_stream¶
Dequeues one block-end request stream and validates it byte for byte against the input's committed request bytes.
function validate_request_stream(tgt : address, expected : StatelessInputSlice) -> unit = {
let dequeued = system_call_checked(tgt);
let matches = region_slices_equal(dequeued, expected);
let mismatch = not_bool(matches);
if mismatch then {
fatal_error(InvalidExecutionRequests)
}
}function fatal_error(_reason) = exit(())val not_bool = pure {coq: "negb", lean: "_lean_not", _: "not"}: forall ('p : Bool). bool('p) -> bool(not('p))Issues one checked block-end system call (EIP-7002/EIP-7251/EIP-8282): the target must exist and the call must succeed. Missing code or frame failure throws immediately; a successful call returns the dequeued requests.
function system_call_checked(tgt : address) -> ScratchSlice = {
let code_hash = k_code_key(tgt);
if code_hash == KECCAK_EMPTY then {
fatal_error(ExecutionInvalid)
} else {
let code = code_db_resolve(code_hash);
let (_, _, _, _, status, output) = run_system_call_frame(tgt, code, EMPTY_CALLDATA, MEMORY_BASE_ZERO);
let succeeded = frame_succeeded(status);
if succeeded then {
let start = scratch_reserve(output.len);
scratch_push_slice(output);
let result = scratch_finish(start);
k_journal_commit();
k_tx_merge(); /* system call is a top-level boundary: merge its storage */
result
} else {
k_journal_revert();
k_tx_merge();
fatal_error(ExecutionInvalid)
}
}
}The reason a block fails validation; one variant per violated block-validity rule.
enum FatalError = {
/* chain config: wrong fork / inactive activation */
InvalidConfig,
/* witness ancestor headers not contiguous */
HeaderChainBroken,
/* a transaction failed to RLP-decode */
RlpDecode,
/* a tx signature did not authenticate its sender */
InvalidSignature,
/* header.gas_limit is outside the consensus domain */
InvalidGasLimit,
/* EIP-7778: a tx exceeds the block's remaining gas */
GasUsedExceedsLimit,
/* a tx exceeds the block's remaining blob gas */
BlobGasLimitExceeded,
/* an invalid tx or a failed block-end system call */
ExecutionInvalid,
/* recomputed cumulative gas != header.gas_used */
InvalidGasUsed,
/* recomputed blob gas != header.blob_gas_used */
InvalidBlobGasUsed,
/* header.excess_blob_gas != expected */
InvalidExcessBlobGas,
/* recomputed post-state root != header.state_root */
InvalidStateRoot,
/* recomputed receipts root != header.receipts_root */
InvalidReceiptsRoot,
/* recomputed logs bloom != header.logs_bloom */
InvalidLogsBloom,
/* recomputed block hash != payload expected hash */
InvalidBlockHash,
/* header.parent_hash != authenticated parent */
InvalidParentHash,
/* EIP-7928: BAL item count > gas_limit / 2000 */
BlockAccessListTooLarge,
/* reconstructed EIP-7928 BAL bytes mismatch */
InvalidBlockAccessList,
/* reconstructed EIP-7685 request bytes mismatch */
InvalidExecutionRequests,
/* a missing/inconsistent proof node (thrown at use) */
WitnessDeficient,
/* an exact protocol integer exceeds its bounded execution representation */
NumericOverflow,
}A stateless-input range with its coordinate and length packed existentially.
type StatelessInputSlice = {
'off 'len,
stateless_input_valid_range('off, 'len).
StatelessInputSliceFields('off, 'len)
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)function validate_execution_requests¶
Validates the EIP-7685 execution requests at block end in request-type order against the input's committed request bytes: withdrawal (EIP-7002), consolidation (EIP-7251), and, from Amsterdam, builder deposit and builder exit (EIP-8282). Before Amsterdam the input must commit to empty builder request streams. Deposits (EIP-6110) are authenticated inline against the transaction receipt logs.
function validate_execution_requests(input_ref : StatelessInputRef) -> unit = {
let execution_profile = k_execution_profile;
let profile = execution_profile.protocol;
validate_request_stream(WITHDRAWAL_REQUEST_ADDR, input_ref.withdrawal_requests);
validate_request_stream(CONSOLIDATION_REQUEST_ADDR, input_ref.consolidation_requests);
if profile.fork >= Amsterdam then {
validate_request_stream(BUILDER_DEPOSIT_REQUEST_ADDR, input_ref.builder_deposit_requests);
validate_request_stream(BUILDER_EXIT_REQUEST_ADDR, input_ref.builder_exit_requests)
} else {
let builder_deposit_length = region_slice_length(input_ref.builder_deposit_requests);
let builder_exit_length = region_slice_length(input_ref.builder_exit_requests);
if (builder_deposit_length != 0) | (builder_exit_length != 0) then {
fatal_error(InvalidExecutionRequests)
}
}
}function fatal_error(_reason) = exit(())Dequeues one block-end request stream and validates it byte for byte against the input's committed request bytes.
function validate_request_stream(tgt : address, expected : StatelessInputSlice) -> unit = {
let dequeued = system_call_checked(tgt);
let matches = region_slices_equal(dequeued, expected);
let mismatch = not_bool(matches);
if mismatch then {
fatal_error(InvalidExecutionRequests)
}
}EIP-7954 code/initcode size bump (65536/131072).
let Amsterdam : int(amsterdam_fork_value) = sizeof(amsterdam_fork_value)let BUILDER_DEPOSIT_REQUEST_ADDR : address = address_from_bits(
0x0000000000000000000000000000bff46984e3725691fa540a8c7589300d8282,
)let BUILDER_EXIT_REQUEST_ADDR : address = address_from_bits(
0x000000000000000000000000000064d678505ad48f8ccb093bc65613800e8282,
)let CONSOLIDATION_REQUEST_ADDR : address = address_from_bits(
0x0000000000000000000000000000bbddc7ce488642fb579f8b00f3a590007251,
)let WITHDRAWAL_REQUEST_ADDR : address = address_from_bits(
0x00000000000000000000000000000961ef480eb55e80d19ad83579a64c007002,
)The active protocol policy and all gas limits derived from the executing header, selected together while decoding the stateless input.
register k_execution_profile : ExecutionProfile = DEFAULT_EXECUTION_PROFILEThe reason a block fails validation; one variant per violated block-validity rule.
enum FatalError = {
/* chain config: wrong fork / inactive activation */
InvalidConfig,
/* witness ancestor headers not contiguous */
HeaderChainBroken,
/* a transaction failed to RLP-decode */
RlpDecode,
/* a tx signature did not authenticate its sender */
InvalidSignature,
/* header.gas_limit is outside the consensus domain */
InvalidGasLimit,
/* EIP-7778: a tx exceeds the block's remaining gas */
GasUsedExceedsLimit,
/* a tx exceeds the block's remaining blob gas */
BlobGasLimitExceeded,
/* an invalid tx or a failed block-end system call */
ExecutionInvalid,
/* recomputed cumulative gas != header.gas_used */
InvalidGasUsed,
/* recomputed blob gas != header.blob_gas_used */
InvalidBlobGasUsed,
/* header.excess_blob_gas != expected */
InvalidExcessBlobGas,
/* recomputed post-state root != header.state_root */
InvalidStateRoot,
/* recomputed receipts root != header.receipts_root */
InvalidReceiptsRoot,
/* recomputed logs bloom != header.logs_bloom */
InvalidLogsBloom,
/* recomputed block hash != payload expected hash */
InvalidBlockHash,
/* header.parent_hash != authenticated parent */
InvalidParentHash,
/* EIP-7928: BAL item count > gas_limit / 2000 */
BlockAccessListTooLarge,
/* reconstructed EIP-7928 BAL bytes mismatch */
InvalidBlockAccessList,
/* reconstructed EIP-7685 request bytes mismatch */
InvalidExecutionRequests,
/* a missing/inconsistent proof node (thrown at use) */
WitnessDeficient,
/* an exact protocol integer exceeds its bounded execution representation */
NumericOverflow,
}Every variable region of the input, resolved once before decoding. Consumers receive explicit source spans instead of re-reading nested SSZ offset tables.
struct StatelessInputRef = {
protocol : ProtocolProfile,
new_payload_request : StatelessInputSlice,
execution_payload : StatelessInputSliceAtLeast(540),
versioned_hashes : StatelessInputSlice,
deposits : StatelessInputSlice,
withdrawal_requests : StatelessInputSlice,
consolidation_requests : StatelessInputSlice,
builder_deposit_requests : StatelessInputSlice,
builder_exit_requests : StatelessInputSlice,
extra_data : StatelessInputSliceAtMost(extra_data_length_bound),
transactions : TransactionListRef,
withdrawals : WithdrawalListRef,
block_access_list : StatelessInputSliceAtMost(block_access_list_length_bound),
witness_state : WitnessNodeListRef,
witness_codes : WitnessCodeListRef,
witness_headers : WitnessHeaderListRef,
chain_config : StatelessInputSlice,
public_keys : StatelessInputSlice,
}