Trie paths and hex-prefix encoding¶
Nibble paths through the Merkle-Patricia trie and the compact (hex-prefix) encoding of YP Appendix C.
type trie_depth¶
The depth of a branch node in a fixed 64-nibble secure key.
type trie_depth = range(0, 63)type trie_path_cursor¶
A cursor at or immediately after a position in a trie path.
type trie_path_cursor = range(0, 64)type hex_prefix_cursor¶
A cursor through the at-most-65 positions used by hex-prefix decoding.
type hex_prefix_cursor = range(0, 65)type TriePath¶
A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A KECCAK-256 / storage-key sized digest, in canonical protocol byte order.
type b256 = vector(32, inc, byte)The number of nibbles in a trie path.
type trie_path_len = range(0, 64)let HEX_PREFIX_MAX_LENGTH¶
let HEX_PREFIX_MAX_LENGTH : int(33) = 33function path_len¶
The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenA trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }The number of nibbles in a trie path.
type trie_path_len = range(0, 64)function path_new¶
Constructs a path from high-aligned data and a nibble length.
function path_new(data : b256, len : trie_path_len) -> TriePath =
struct { data = data, len = len }A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A KECCAK-256 / storage-key sized digest, in canonical protocol byte order.
type b256 = vector(32, inc, byte)The number of nibbles in a trie path.
type trie_path_len = range(0, 64)function path_empty¶
The empty path.
Constructs a path from high-aligned data and a nibble length.
function path_new(data : b256, len : trie_path_len) -> TriePath =
struct { data = data, len = len }let ZERO_HASH : hash = hash_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }function path_byte_index¶
Maps a nibble cursor to the corresponding canonical-order path byte.
function path_byte_index(i : trie_path_cursor) -> b256_index = {
let quotient = tdiv_nat(i, 2);
let natural_index : b256_index =
if (0 <= quotient) & (quotient <= 31) then {
quotient
} else {
assert(false);
0
};
natural_index
}Truncating division specialized to a non-negative dividend and positive divisor. Singleton operands determine the exact natural-number result.
val tdiv_nat = pure {smt: "div", ocaml: "quotient", interpreter: "quotient", lem: "integerDiv", c: "tdiv_int", cpp: "tdiv_int", systemverilog: "tdiv_int", coq: "Z.quot", lean: "Nat.div", _: "tdiv_int"}: forall ('n : Int) ('m : Int), ('n >= 0 & 'm >= 1).
(int('n), int('m)) -> int(div('n, 'm))A byte position in a 32-byte secure key.
type b256_index = range(0, 31)A cursor at or immediately after a position in a trie path.
type trie_path_cursor = range(0, 64)function path_nibble¶
The i-th nibble, most significant first; out of range yields 0.
function path_nibble(path : TriePath, i : trie_path_cursor) -> nibble =
let length = path_len(path) in
if length <= i then {
0x0
} else {
let bytes = path.data;
let byte_index = path_byte_index(i);
let parity = tmod_int(i, 2);
if parity == 0 then {
bytes[byte_index][7 .. 4]
} else {
bytes[byte_index][3 .. 0]
}
}Maps a nibble cursor to the corresponding canonical-order path byte.
function path_byte_index(i : trie_path_cursor) -> b256_index = {
let quotient = tdiv_nat(i, 2);
let natural_index : b256_index =
if (0 <= quotient) & (quotient <= 31) then {
quotient
} else {
assert(false);
0
};
natural_index
}The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenA trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A four-bit path element (YP Appendix D).
type nibble = bits(4)A cursor at or immediately after a position in a trie path.
type trie_path_cursor = range(0, 64)function path_append_nibble¶
Appends one nibble to a path, rejecting paths already at the key bound.
function path_append_nibble(path : TriePath, value : nibble) -> TriePath = {
let length = path_len(path);
if length < 64 then {
let original = path.data;
var bytes = original;
let byte_index = path_byte_index(length);
let parity = tmod_int(length, 2);
if parity == 0 then {
bytes[byte_index] = append(value, 0x0)
} else {
bytes[byte_index] = append(bytes[byte_index][7 .. 4], value)
};
let path_data = B256(bytes);
path_new(path_data, length + 1)
} else {
fatal_error(WitnessDeficient)
}
}function B256(bytes : vector(32, inc, byte)) -> b256 = bytesfunction fatal_error(_reason) = exit(())Maps a nibble cursor to the corresponding canonical-order path byte.
function path_byte_index(i : trie_path_cursor) -> b256_index = {
let quotient = tdiv_nat(i, 2);
let natural_index : b256_index =
if (0 <= quotient) & (quotient <= 31) then {
quotient
} else {
assert(false);
0
};
natural_index
}The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenConstructs a path from high-aligned data and a nibble length.
function path_new(data : b256, len : trie_path_len) -> TriePath =
struct { data = data, len = len }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 trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A four-bit path element (YP Appendix D).
type nibble = bits(4)function path_append_byte¶
Appends both nibbles of a byte to a path, high nibble first.
function path_append_byte(path : TriePath, value : byte) -> TriePath = {
let high_nibble = path_append_nibble(path, value[7 .. 4]);
path_append_nibble(high_nibble, value[3 .. 0])
}Appends one nibble to a path, rejecting paths already at the key bound.
function path_append_nibble(path : TriePath, value : nibble) -> TriePath = {
let length = path_len(path);
if length < 64 then {
let original = path.data;
var bytes = original;
let byte_index = path_byte_index(length);
let parity = tmod_int(length, 2);
if parity == 0 then {
bytes[byte_index] = append(value, 0x0)
} else {
bytes[byte_index] = append(bytes[byte_index][7 .. 4], value)
};
let path_data = B256(bytes);
path_new(path_data, length + 1)
} else {
fatal_error(WitnessDeficient)
}
}A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }An 8-bit byte.
type byte = bits(8)function path_single¶
A one-nibble path.
function path_single(n : nibble) -> TriePath = {
let empty_path = path_empty();
path_append_nibble(empty_path, n)
}Appends one nibble to a path, rejecting paths already at the key bound.
function path_append_nibble(path : TriePath, value : nibble) -> TriePath = {
let length = path_len(path);
if length < 64 then {
let original = path.data;
var bytes = original;
let byte_index = path_byte_index(length);
let parity = tmod_int(length, 2);
if parity == 0 then {
bytes[byte_index] = append(value, 0x0)
} else {
bytes[byte_index] = append(bytes[byte_index][7 .. 4], value)
};
let path_data = B256(bytes);
path_new(path_data, length + 1)
} else {
fatal_error(WitnessDeficient)
}
}The empty path.
function path_empty() -> TriePath =
path_new(ZERO_HASH, 0)A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A four-bit path element (YP Appendix D).
type nibble = bits(4)function path_concat¶
Path concatenation; over 64 nibbles is a witness fault.
function path_concat(a : TriePath, b : TriePath) -> TriePath = {
let alen = path_len(a);
let blen = path_len(b);
let combined = alen + blen;
if combined <= 64 then {
var result = a;
var index : trie_path_len = 0;
while index < blen termination_measure(blen - index) do {
let nibble = path_nibble(b, index);
result = path_append_nibble(result, nibble);
let current_index = index;
index =
if current_index < 64 then {
current_index + 1
} else {
fatal_error(WitnessDeficient)
}
};
result
} else {
fatal_error(WitnessDeficient)
}
}function fatal_error(_reason) = exit(())Appends one nibble to a path, rejecting paths already at the key bound.
function path_append_nibble(path : TriePath, value : nibble) -> TriePath = {
let length = path_len(path);
if length < 64 then {
let original = path.data;
var bytes = original;
let byte_index = path_byte_index(length);
let parity = tmod_int(length, 2);
if parity == 0 then {
bytes[byte_index] = append(value, 0x0)
} else {
bytes[byte_index] = append(bytes[byte_index][7 .. 4], value)
};
let path_data = B256(bytes);
path_new(path_data, length + 1)
} else {
fatal_error(WitnessDeficient)
}
}The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenThe i-th nibble, most significant first; out of range yields 0.
function path_nibble(path : TriePath, i : trie_path_cursor) -> nibble =
let length = path_len(path) in
if length <= i then {
0x0
} else {
let bytes = path.data;
let byte_index = path_byte_index(i);
let parity = tmod_int(i, 2);
if parity == 0 then {
bytes[byte_index][7 .. 4]
} else {
bytes[byte_index][3 .. 0]
}
}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 trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A four-bit path element (YP Appendix D).
type nibble = bits(4)The number of nibbles in a trie path.
type trie_path_len = range(0, 64)function path_drop¶
The path with its first n nibbles removed.
function path_drop(path : TriePath, n : trie_path_len) -> TriePath = {
let length = path_len(path);
if length <= n then {
path_empty()
} else if n == 0 then {
path
} else {
let remain : trie_path_len = length - n;
var result = path_empty();
var offset : trie_path_len = 0;
while offset < remain termination_measure(remain - offset) do {
let candidate = n + offset;
let source_index : trie_path_cursor =
if (0 <= candidate) & (candidate <= 64) then {
candidate
} else {
assert(false);
0
};
let nibble = path_nibble(path, source_index);
result = path_append_nibble(result, nibble);
let current_offset = offset;
offset =
if current_offset < 64 then {
current_offset + 1
} else {
fatal_error(WitnessDeficient)
}
};
result
}
}function fatal_error(_reason) = exit(())Appends one nibble to a path, rejecting paths already at the key bound.
function path_append_nibble(path : TriePath, value : nibble) -> TriePath = {
let length = path_len(path);
if length < 64 then {
let original = path.data;
var bytes = original;
let byte_index = path_byte_index(length);
let parity = tmod_int(length, 2);
if parity == 0 then {
bytes[byte_index] = append(value, 0x0)
} else {
bytes[byte_index] = append(bytes[byte_index][7 .. 4], value)
};
let path_data = B256(bytes);
path_new(path_data, length + 1)
} else {
fatal_error(WitnessDeficient)
}
}The empty path.
function path_empty() -> TriePath =
path_new(ZERO_HASH, 0)The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenThe i-th nibble, most significant first; out of range yields 0.
function path_nibble(path : TriePath, i : trie_path_cursor) -> nibble =
let length = path_len(path) in
if length <= i then {
0x0
} else {
let bytes = path.data;
let byte_index = path_byte_index(i);
let parity = tmod_int(i, 2);
if parity == 0 then {
bytes[byte_index][7 .. 4]
} else {
bytes[byte_index][3 .. 0]
}
}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 trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A four-bit path element (YP Appendix D).
type nibble = bits(4)A cursor at or immediately after a position in a trie path.
type trie_path_cursor = range(0, 64)The number of nibbles in a trie path.
type trie_path_len = range(0, 64)function path_eq¶
Path equality.
A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }function path_matches¶
Whether seg occurs in key at nibble position pos.
function path_matches(key : TriePath, pos : trie_path_cursor, seg : TriePath) -> bool = {
let segment_len = path_len(seg);
let key_len = path_len(key);
let stop = pos + segment_len;
if key_len < stop then {
false
} else {
var ok : bool = true;
var offset : trie_path_len = 0;
while ok & offset < segment_len termination_measure(segment_len - offset) do {
let key_index = pos + offset;
if key_index <= 64 then {
let key_nibble = path_nibble(key, key_index);
let segment_nibble = path_nibble(seg, offset);
if key_nibble != segment_nibble then {
ok = false
}
} else {
ok = false
};
let current_offset = offset;
offset =
if current_offset < 64 then {
current_offset + 1
} else {
fatal_error(WitnessDeficient)
}
};
ok
}
}function fatal_error(_reason) = exit(())The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenThe i-th nibble, most significant first; out of range yields 0.
function path_nibble(path : TriePath, i : trie_path_cursor) -> nibble =
let length = path_len(path) in
if length <= i then {
0x0
} else {
let bytes = path.data;
let byte_index = path_byte_index(i);
let parity = tmod_int(i, 2);
if parity == 0 then {
bytes[byte_index][7 .. 4]
} else {
bytes[byte_index][3 .. 0]
}
}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 trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A cursor at or immediately after a position in a trie path.
type trie_path_cursor = range(0, 64)The number of nibbles in a trie path.
type trie_path_len = range(0, 64)function path_prefix_of¶
Whether prefix is a prefix of path.
function path_prefix_of(prefix : TriePath, path : TriePath) -> bool =
path_matches(path, 0, prefix)Whether seg occurs in key at nibble position pos.
function path_matches(key : TriePath, pos : trie_path_cursor, seg : TriePath) -> bool = {
let segment_len = path_len(seg);
let key_len = path_len(key);
let stop = pos + segment_len;
if key_len < stop then {
false
} else {
var ok : bool = true;
var offset : trie_path_len = 0;
while ok & offset < segment_len termination_measure(segment_len - offset) do {
let key_index = pos + offset;
if key_index <= 64 then {
let key_nibble = path_nibble(key, key_index);
let segment_nibble = path_nibble(seg, offset);
if key_nibble != segment_nibble then {
ok = false
}
} else {
ok = false
};
let current_offset = offset;
offset =
if current_offset < 64 then {
current_offset + 1
} else {
fatal_error(WitnessDeficient)
}
};
ok
}
}A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }function common_prefix_length¶
The common-prefix length of two canonical nibble paths.
function common_prefix_length(a : TriePath, b : TriePath) -> trie_path_len = {
let alen = path_len(a);
let blen = path_len(b);
let stop =
if alen < blen then alen else blen;
var length : trie_path_len = 0;
var matching : bool = true;
while matching & length < stop termination_measure(stop - length) do {
let a_nibble = path_nibble(a, length);
let b_nibble = path_nibble(b, length);
if a_nibble == b_nibble then {
let current_length = length;
length =
if current_length < 64 then {
current_length + 1
} else {
fatal_error(WitnessDeficient)
}
} else {
matching = false
}
};
length
}function fatal_error(_reason) = exit(())The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenThe i-th nibble, most significant first; out of range yields 0.
function path_nibble(path : TriePath, i : trie_path_cursor) -> nibble =
let length = path_len(path) in
if length <= i then {
0x0
} else {
let bytes = path.data;
let byte_index = path_byte_index(i);
let parity = tmod_int(i, 2);
if parity == 0 then {
bytes[byte_index][7 .. 4]
} else {
bytes[byte_index][3 .. 0]
}
}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 trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }The number of nibbles in a trie path.
type trie_path_len = range(0, 64)function hex_prefix_encoded_length¶
The encoded byte length of the hex-prefix form of a trie path.
function hex_prefix_encoded_length(path : TriePath) -> range(1, 33) = {
let length : trie_path_len = path_len(path);
let packed_pair_count : range(0, 32) = tdiv_nat(length, 2);
1 + packed_pair_count
}The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenTruncating division specialized to a non-negative dividend and positive divisor. Singleton operands determine the exact natural-number result.
val tdiv_nat = pure {smt: "div", ocaml: "quotient", interpreter: "quotient", lem: "integerDiv", c: "tdiv_int", cpp: "tdiv_int", systemverilog: "tdiv_int", coq: "Z.quot", lean: "Nat.div", _: "tdiv_int"}: forall ('n : Int) ('m : Int), ('n >= 0 & 'm >= 1).
(int('n), int('m)) -> int(div('n, 'm))A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }The number of nibbles in a trie path.
type trie_path_len = range(0, 64)function hex_prefix_first_byte¶
The flag byte beginning the hex-prefix form of a trie path.
function hex_prefix_first_byte(path : TriePath, is_leaf : bool) -> byte = {
let length : trie_path_len = path_len(path);
let odd = tmod_nat(length, 2) != 0;
let flag : nibble =
if is_leaf then 0x2 else 0x0;
if odd then {
let first_nibble = path_nibble(path, 0);
append(flag | 0x1, first_nibble)
} else {
append(flag, 0x0)
}
}The path length in nibbles.
function path_len(path : TriePath) -> trie_path_len = path.lenThe i-th nibble, most significant first; out of range yields 0.
function path_nibble(path : TriePath, i : trie_path_cursor) -> nibble =
let length = path_len(path) in
if length <= i then {
0x0
} else {
let bytes = path.data;
let byte_index = path_byte_index(i);
let parity = tmod_int(i, 2);
if parity == 0 then {
bytes[byte_index][7 .. 4]
} else {
bytes[byte_index][3 .. 0]
}
}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))A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }An 8-bit byte.
type byte = bits(8)A four-bit path element (YP Appendix D).
type nibble = bits(4)The number of nibbles in a trie path.
type trie_path_len = range(0, 64)function hex_prefix_decode_ref¶
Decodes a compact path directly from its RLP source span, returning the leaf flag and the path.
function hex_prefix_decode_ref forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
(bool, TriePath)
) = {
if f.is_list then {
fatal_error(RlpDecode)
};
let n = f.content_len;
if n == 0 then {
(false, path_empty())
} else {
let maximum_length = HEX_PREFIX_MAX_LENGTH;
if maximum_length < n then {
fatal_error(RlpDecode)
} else {
let content = sub_slice(f.source, f.source.len - n, n);
let fb = slice_byte(content, 0);
let flag : nibble = fb[7 .. 4];
let is_leaf : bool = flag[1] == bitone;
let odd : bool = flag[0] == bitone;
let tail_length : range(0, 32) = n - 1;
let tail = slice_suffix(content, 1);
let packed = slice_load(tail, 0);
let paired_nibbles : range(0, 64) = tail_length * 2;
if odd then {
if paired_nibbles < 64 then {
let shifted = word_shift_right(packed, 4);
var bytes = word_to_hash(shifted);
bytes[0] = append(fb[3 .. 0], bytes[0][3 .. 0]);
let path_data = B256(bytes);
let path = path_new(path_data, paired_nibbles + 1);
(is_leaf, path)
} else {
fatal_error(WitnessDeficient)
}
} else {
let path_data = word_to_hash(packed);
let path = path_new(path_data, paired_nibbles);
(is_leaf, path)
}
}
}
}function B256(bytes : vector(32, inc, byte)) -> b256 = bytesfunction fatal_error(_reason) = exit(())The empty path.
function path_empty() -> TriePath =
path_new(ZERO_HASH, 0)Constructs a path from high-aligned data and a nibble length.
function path_new(data : b256, len : trie_path_len) -> TriePath =
struct { data = data, len = len }Shifts a word right logically by a bounded count.
function word_shift_right(value : word, amount : word_bit_count) -> word = {
let value_bits = get_slice_int(256, value, 0);
let shifted_bits = sail_shiftright(value_bits, amount);
unsigned(shifted_bits)
}Serializes an EVM word as a 32-byte big-endian digest.
function word_to_hash(value : word) -> hash = {
let zero_bytes = vector_init(32, 0x00);
var result : hash = B256(zero_bytes);
result[0] = get_slice_int(8, value, 248);
result[1] = get_slice_int(8, value, 240);
result[2] = get_slice_int(8, value, 232);
result[3] = get_slice_int(8, value, 224);
result[4] = get_slice_int(8, value, 216);
result[5] = get_slice_int(8, value, 208);
result[6] = get_slice_int(8, value, 200);
result[7] = get_slice_int(8, value, 192);
result[8] = get_slice_int(8, value, 184);
result[9] = get_slice_int(8, value, 176);
result[10] = get_slice_int(8, value, 168);
result[11] = get_slice_int(8, value, 160);
result[12] = get_slice_int(8, value, 152);
result[13] = get_slice_int(8, value, 144);
result[14] = get_slice_int(8, value, 136);
result[15] = get_slice_int(8, value, 128);
result[16] = get_slice_int(8, value, 120);
result[17] = get_slice_int(8, value, 112);
result[18] = get_slice_int(8, value, 104);
result[19] = get_slice_int(8, value, 96);
result[20] = get_slice_int(8, value, 88);
result[21] = get_slice_int(8, value, 80);
result[22] = get_slice_int(8, value, 72);
result[23] = get_slice_int(8, value, 64);
result[24] = get_slice_int(8, value, 56);
result[25] = get_slice_int(8, value, 48);
result[26] = get_slice_int(8, value, 40);
result[27] = get_slice_int(8, value, 32);
result[28] = get_slice_int(8, value, 24);
result[29] = get_slice_int(8, value, 16);
result[30] = get_slice_int(8, value, 8);
result[31] = get_slice_int(8, value, 0);
result
}let HEX_PREFIX_MAX_LENGTH : int(33) = 33The 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,
}The witness-carrying fields of a decoded RLP reference. Both the complete encoding and its content are statically contained by the source slice.
struct RlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : StatelessInputSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A four-bit path element (YP Appendix D).
type nibble = bits(4)The complete containment invariant for an RLP field reference. source
is normalized to the complete encoded item. RLP content is its suffix, so
the content offset is derived as source.len - content_len.
type rlp_field_ref_valid(
'source_off : Int,
'source_len : Int,
'content_len : Int,
) -> Bool =
source_valid_range('source_off, 'source_len)
& 0 <= 'content_len
& 'content_len <= 'source_lenfunction scratch_hex_prefix_decode_ref¶
Scratch-backed counterpart used only when canonicalization reopens an embedded node that it just encoded.
function scratch_hex_prefix_decode_ref forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
ScratchRlpFieldRef('source_off, 'source_len, 'content_len)) -> (
(bool, TriePath)
) = {
if f.is_list then {
fatal_error(RlpDecode)
};
let n = f.content_len;
if n == 0 then {
(false, path_empty())
} else {
let maximum_length = HEX_PREFIX_MAX_LENGTH;
if maximum_length < n then {
fatal_error(RlpDecode)
} else {
let content = sub_slice(f.source, f.source.len - n, n);
let fb = slice_byte(content, 0);
let flag : nibble = fb[7 .. 4];
let is_leaf : bool = flag[1] == bitone;
let odd : bool = flag[0] == bitone;
let tail_length : range(0, 32) = n - 1;
let tail = slice_suffix(content, 1);
let packed = slice_load(tail, 0);
let paired_nibbles : range(0, 64) = tail_length * 2;
if odd then {
if paired_nibbles < 64 then {
let shifted = word_shift_right(packed, 4);
var bytes = word_to_hash(shifted);
bytes[0] = append(fb[3 .. 0], bytes[0][3 .. 0]);
let path_data = B256(bytes);
let path = path_new(path_data, paired_nibbles + 1);
(is_leaf, path)
} else {
fatal_error(WitnessDeficient)
}
} else {
let path_data = word_to_hash(packed);
let path = path_new(path_data, paired_nibbles);
(is_leaf, path)
}
}
}
}function B256(bytes : vector(32, inc, byte)) -> b256 = bytesfunction fatal_error(_reason) = exit(())The empty path.
function path_empty() -> TriePath =
path_new(ZERO_HASH, 0)Constructs a path from high-aligned data and a nibble length.
function path_new(data : b256, len : trie_path_len) -> TriePath =
struct { data = data, len = len }function scratch_byte(s, off) =
if off < s.len then {
scratch_slice_byte_at(s, off)
} else {
0x00
}Shifts a word right logically by a bounded count.
function word_shift_right(value : word, amount : word_bit_count) -> word = {
let value_bits = get_slice_int(256, value, 0);
let shifted_bits = sail_shiftright(value_bits, amount);
unsigned(shifted_bits)
}Serializes an EVM word as a 32-byte big-endian digest.
function word_to_hash(value : word) -> hash = {
let zero_bytes = vector_init(32, 0x00);
var result : hash = B256(zero_bytes);
result[0] = get_slice_int(8, value, 248);
result[1] = get_slice_int(8, value, 240);
result[2] = get_slice_int(8, value, 232);
result[3] = get_slice_int(8, value, 224);
result[4] = get_slice_int(8, value, 216);
result[5] = get_slice_int(8, value, 208);
result[6] = get_slice_int(8, value, 200);
result[7] = get_slice_int(8, value, 192);
result[8] = get_slice_int(8, value, 184);
result[9] = get_slice_int(8, value, 176);
result[10] = get_slice_int(8, value, 168);
result[11] = get_slice_int(8, value, 160);
result[12] = get_slice_int(8, value, 152);
result[13] = get_slice_int(8, value, 144);
result[14] = get_slice_int(8, value, 136);
result[15] = get_slice_int(8, value, 128);
result[16] = get_slice_int(8, value, 120);
result[17] = get_slice_int(8, value, 112);
result[18] = get_slice_int(8, value, 104);
result[19] = get_slice_int(8, value, 96);
result[20] = get_slice_int(8, value, 88);
result[21] = get_slice_int(8, value, 80);
result[22] = get_slice_int(8, value, 72);
result[23] = get_slice_int(8, value, 64);
result[24] = get_slice_int(8, value, 56);
result[25] = get_slice_int(8, value, 48);
result[26] = get_slice_int(8, value, 40);
result[27] = get_slice_int(8, value, 32);
result[28] = get_slice_int(8, value, 24);
result[29] = get_slice_int(8, value, 16);
result[30] = get_slice_int(8, value, 8);
result[31] = get_slice_int(8, value, 0);
result
}let HEX_PREFIX_MAX_LENGTH : int(33) = 33The 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,
}The same RLP framing invariants over a node encoding held in the scratch arena. Keeping this nominally separate prevents decoded input fields from acquiring a runtime byte-source tag.
struct ScratchRlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : ScratchSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}A trie path of at most 64 nibbles — secure state and storage keys are
32-byte hashes, and list tries use short RLP indices. data is
high-aligned; len preserves leading zeroes and prefixes.
struct TriePath = { data : b256, len : trie_path_len }A four-bit path element (YP Appendix D).
type nibble = bits(4)The complete containment invariant for an RLP field reference. source
is normalized to the complete encoded item. RLP content is its suffix, so
the content offset is derived as source.len - content_len.
type rlp_field_ref_valid(
'source_off : Int,
'source_len : Int,
'content_len : Int,
) -> Bool =
source_valid_range('source_off, 'source_len)
& 0 <= 'content_len
& 'content_len <= 'source_len