Block header RLP codec¶
Canonical execution-header encoding and hashing over already recomputed payload commitments.
function block_header_hash¶
The block header hash: keccak256(rlp(header)) with the recomputed
body roots spliced in (YP §4.4; post-merge constants for ommers,
difficulty, and nonce).
function block_header_hash(
header : BlockHeader,
transactions_root : hash,
withdrawals_root : hash,
requests_hash : hash,
block_access_list_hash : hash,
) -> (
hash
) = {
let execution_profile = k_execution_profile;
let profile = execution_profile.protocol;
let word_length = rlp_word_size();
let address_length = rlp_addr_size();
let bloom_length = 3 + LOGS_BLOOM_BYTE_LENGTH;
let difficulty_length = rlp_uint_size(0);
let number_length = rlp_uint_size(header.number);
let gas_limit_length = rlp_uint_size(header.gas_limit);
let gas_used_length = rlp_uint_size(header.gas_used);
let timestamp_length = rlp_uint_size(header.timestamp);
let extra_data_length = rlp_scratch_slice_size(header.extra_data);
let nonce_length = 1 + EIGHT_BYTE_LENGTH;
var content_length : rlp_scratch_length = rlp_scratch_length_add(6 * word_length, address_length);
content_length = rlp_scratch_length_add(content_length, bloom_length);
content_length = rlp_scratch_length_add(content_length, difficulty_length);
content_length = rlp_scratch_length_add(content_length, number_length);
content_length = rlp_scratch_length_add(content_length, gas_limit_length);
content_length = rlp_scratch_length_add(content_length, gas_used_length);
content_length = rlp_scratch_length_add(content_length, timestamp_length);
content_length = rlp_scratch_length_add(content_length, extra_data_length);
content_length = rlp_scratch_length_add(content_length, nonce_length);
if profile.fork >= London then {
let field_length = rlp_uint_word_size(header.base_fee);
content_length = rlp_scratch_length_add(content_length, field_length)
};
if profile.fork >= Shanghai then {
content_length = rlp_scratch_length_add(content_length, word_length)
};
if profile.fork >= Cancun then {
let blob_gas_used_length = rlp_uint_size(header.blob_gas_used);
let excess_blob_gas_length = rlp_uint_size(header.excess_blob_gas);
content_length = rlp_scratch_length_add(content_length, blob_gas_used_length);
content_length = rlp_scratch_length_add(content_length, excess_blob_gas_length);
content_length = rlp_scratch_length_add(content_length, word_length)
};
if profile.fork >= Prague then {
content_length = rlp_scratch_length_add(content_length, word_length)
};
if profile.fork >= Amsterdam then {
let slot_number_length = rlp_uint_size(header.slot_number);
content_length = rlp_scratch_length_add(content_length, word_length);
content_length = rlp_scratch_length_add(content_length, slot_number_length)
};
/* Six fixed words plus the protocol-bounded variable fields give an
* Amsterdam header-content maximum of 749 bytes. Keep that semantic
* bound instead of reconstructing a generic backend byte length. */
if 749 < content_length then {
fatal_error(RlpDecode)
};
let bounded_content_length : range(0, 749) = tmod_nat(content_length, 750);
let content_len = bounded_content_length;
let encoded_length = rlp_list_size(content_len);
let encoder = rlp_encoder_begin(encoded_length);
rlp_write_list_prefix(content_len);
let parent_hash = hash_to_word(header.parent_hash);
rlp_write_word(parent_hash);
let ommer_hash = hash_to_word(EMPTY_OMMER_HASH);
rlp_write_word(ommer_hash);
rlp_write_addr(header.fee_recipient);
let state_root = hash_to_word(header.state_root);
rlp_write_word(state_root);
let transactions_root_word = hash_to_word(transactions_root);
rlp_write_word(transactions_root_word);
let receipts_root = hash_to_word(header.receipts_root);
rlp_write_word(receipts_root);
let logs_bloom = logs_bloom_from_ref(header.logs_bloom);
rlp_write_logs_bloom(logs_bloom);
rlp_write_uint(0);
rlp_write_uint(header.number);
rlp_write_uint(header.gas_limit);
rlp_write_uint(header.gas_used);
rlp_write_uint(header.timestamp);
rlp_write_slice(header.extra_data);
rlp_write_word(header.prev_randao);
rlp_write_string_prefix(EIGHT_BYTE_LENGTH, 0x00);
scratch_push_word_be(ZERO_WORD, EIGHT_BYTE_LENGTH);
if profile.fork >= London then {
rlp_write_uint_word(header.base_fee)
};
if profile.fork >= Shanghai then {
let withdrawals_root_word = hash_to_word(withdrawals_root);
rlp_write_word(withdrawals_root_word)
};
if profile.fork >= Cancun then {
rlp_write_uint(header.blob_gas_used);
rlp_write_uint(header.excess_blob_gas);
let parent_beacon_block_root = hash_to_word(header.parent_beacon_block_root);
rlp_write_word(parent_beacon_block_root)
};
if profile.fork >= Prague then {
let requests_hash_word = hash_to_word(requests_hash);
rlp_write_word(requests_hash_word)
};
if profile.fork >= Amsterdam then {
let block_access_list_hash_word = hash_to_word(block_access_list_hash);
rlp_write_word(block_access_list_hash_word);
rlp_write_uint(header.slot_number)
};
let encoded = rlp_encoder_finish(encoder);
let block_hash = keccak256(encoded);
rlp_encoder_rewind(encoder);
block_hash
}function fatal_error(_reason) = exit(())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],
)Materializes a referenced wire-order bloom into the decreasing-index semantic vector used by the Yellow Paper equations.
function logs_bloom_from_ref(reference : LogsBloomRef) -> LogsBloom = {
var out : LogsBloom = EMPTY_LOGS_BLOOM;
foreach (i from 0 to 255) {
out[255 - i] = slice_byte(reference, i)
};
out
}function rlp_addr_size() -> int(21) = RLP_ENCODED_ADDRESS_LENGTHfunction rlp_encoder_begin(expected_len) =
struct { start = scratch_reserve(expected_len), expected_len = expected_len }Finishes an exact-size construction and retains its encoded bytes.
function rlp_encoder_finish(encoder : RlpEncoder) -> ScratchSlice = {
let encoded = scratch_finish(encoder.start);
assert(encoded.len == encoder.expected_len, "RLP encoder length");
encoded
}Releases every byte appended by an encoder after its result is consumed.
function rlp_encoder_rewind(encoder : RlpEncoder) -> unit =
scratch_rewind(encoder.start)function rlp_list_size(content_len) = {
rlp_length_prefix_len(content_len) + content_len
}function rlp_scratch_length_add(left, right) =
if right <= sizeof(scratch_region_bound) - left then {
left + right
} else {
fatal_error(RlpDecode)
}function rlp_uint_word_size(w) = {
let len = rlp_minimal_word_len(w);
let first =
if len == 1 then word_low_byte(w) else 0x00;
if (len == 1) & (first[7] == bitzero) then {
1
} else {
1 + len
}
}function rlp_word_size() -> int(33) = RLP_ENCODED_WORD_LENGTHAppends one Ethereum address as an RLP byte string.
function rlp_write_addr(a : address) -> unit = {
rlp_write_string_prefix(ADDRESS_BYTE_LENGTH, a[0]);
scratch_push_address(a)
}function rlp_write_list_prefix(content_len) = {
if content_len <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(content_len);
let prefix = add_bits(0xc0, length_byte);
scratch_push_byte(prefix)
} else {
let length_word = rlp_length_word(content_len);
let length_len = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_len);
let prefix = add_bits(0xf7, length_byte);
scratch_push_byte(prefix);
scratch_push_word_be(length_word, length_len)
}
}Writes a bloom as its fixed-width RLP byte string without constructing a temporary Sail list.
function rlp_write_logs_bloom(bloom : LogsBloom) -> unit = {
rlp_write_string_prefix(LOGS_BLOOM_BYTE_LENGTH, 0x00);
scratch_push_fixed_bytes_256(bloom)
}function rlp_write_string_prefix(len, first) = {
if (len == 1) & (first[7] == bitzero) then {
return ()
};
if len <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(len);
let prefix = add_bits(0x80, length_byte);
scratch_push_byte(prefix)
} else {
let length_word = rlp_length_word(len);
let length_len = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_len);
let prefix = add_bits(0xb7, length_byte);
scratch_push_byte(prefix);
scratch_push_word_be(length_word, length_len)
}
}function rlp_write_uint_word(w) = {
let len = rlp_minimal_word_len(w);
let first =
if len == 1 then word_low_byte(w) else 0x00;
rlp_write_string_prefix(len, first);
let word = u256(w);
scratch_push_word_be(word, len)
}Appends one full-width EVM word as an RLP byte string.
function rlp_write_word(w : word) -> unit = {
rlp_write_string_prefix(WORD_BYTE_LENGTH, 0x00);
scratch_push_word_be(w, WORD_BYTE_LENGTH)
}Appends the low len bytes of a word in canonical big-endian order.
function scratch_push_word_be(data : word, len : range(0, 32)) -> unit = {
if len != 0 then {
let arena = scratch_arena;
scratch_arena = host_scratch_store_word(arena.len, data, len)
}
}Remainder specialized to a non-negative dividend and positive divisor. Singleton operands determine the exact natural-number result.
val tmod_nat = pure {smt: "mod", ocaml: "modulus", interpreter: "modulus", lem: "integerMod", c: "tmod_int", cpp: "tmod_int", systemverilog: "tmod_int", coq: "Z.rem", lean: "Nat.mod", _: "tmod_int"}: forall ('n : Int) ('m : Int), ('n >= 0 & 'm >= 1).
(int('n), int('m)) -> int(mod('n, 'm))EIP-7954 code/initcode size bump (65536/131072).
let Amsterdam : int(amsterdam_fork_value) = sizeof(amsterdam_fork_value)EIP-1153/4844; precompiles 0x01-0x0a.
let Cancun : int(first_blob_fork_value) = sizeof(first_blob_fork_value)let EIGHT_BYTE_LENGTH : int(8) = 8keccak256(rlp([])) — the ommers hash of every post-merge block
(EIP-3675 requires an empty ommers list).
let EMPTY_OMMER_HASH : hash = hash_from_bits(0x1dcc4de8dec75d7aab85b567b6ccd41ad312451b948a7413f0a142fd40d49347)let LOGS_BLOOM_BYTE_LENGTH : int(256) = 256EIP-1559 fee market and EIP-3529 refund reduction.
let London : int(london_fork_value) = sizeof(london_fork_value)EIP-7623 calldata floor; BLS precompiles 0x0b-0x11.
let Prague : int(prague_fork_value) = sizeof(prague_fork_value)EIP-3651 warm coinbase, EIP-3855 PUSH0, EIP-3860 initcode.
let Shanghai : int(shanghai_fork_value) = sizeof(shanghai_fork_value)let ZERO_WORD : word = word_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)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 execution-payload header fields the model reads and validates
(YP §4.4). Scalar wire bounds come from the consensus/Amsterdam SSZ
ExecutionPayload schema. gas_used <= gas_limit and the active
blob-schedule rules are execution-protocol constraints checked when the
payload is admitted. extra_data retains the schema's
ByteList[MAX_EXTRA_DATA_BYTES] bound while staying source-backed; it is
RLP-encoded whole for the header hash and never inspected. The fixed
logs_bloom commitment likewise stays source-backed until a semantic
consumer explicitly decodes it.
struct BlockHeader = {
number : block_number,
timestamp : block_timestamp,
gas_limit : block_gas_limit,
gas_used : block_gas,
prev_randao : word,
base_fee : word,
/* EIP-4844: a multiple of GAS_PER_BLOB within the active schedule. */
blob_gas_used : blob_gas_used,
/* EIP-4844 uint64 on the wire; narrowed to the documented reachable-chain
invariant at the authenticated input boundary. */
excess_blob_gas : excess_blob_gas,
state_root : hash,
receipts_root : hash,
logs_bloom : LogsBloomRef,
fee_recipient : address,
parent_hash : hash,
parent_beacon_block_root : hash,
/* uint64 (EIP-7843 and the Amsterdam stateless SSZ schema). */
slot_number : slot_number,
extra_data : StatelessInputSliceAtMost(extra_data_length_bound),
}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,
}Blob gas used by one supported block. The existential count retains that
every value is exactly a multiple of GAS_PER_BLOB; profile-indexed
decoding applies the selected schedule's tighter range before values enter
this heterogeneous header domain.
type blob_gas_used = {
'count,
0 <= 'count
& 'count <= bpo2_blob_max_count.
int(gas_per_blob_value * 'count)
}The accumulated excess blob gas carried between headers (EIP-4844).
type excess_blob_gas = range(0, excess_blob_gas_bound)The common digest type used by trie, code, and block hashes.
type hash = b256An RLP byte count that can be materialized in the scratch arena. The host scratch-region limit is enforced while recursive collection totals are accumulated.
type rlp_scratch_length = range(0, scratch_region_bound)A beacon-chain slot number. Provenance: EIP-7843 and Amsterdam's
stateless SSZ payload declare this field as uint64.
type slot_number = range(0, ssz_uint_bound)