Block access list RLP decoding¶
Canonical list, byte-string, and integer field decoding shared by EIP-7928 validation.
function bal_ref_cursor¶
function bal_ref_cursor(f) =
let framing_canonical = rlp_ref_framing_canonical(f) in
if f.is_list & framing_canonical then {
rlp_decode_list(f)
} else {
fatal_error(InvalidBlockAccessList)
}function bal_ref_cursor(f) =
let framing_canonical = rlp_ref_framing_canonical(f) in
if f.is_list & framing_canonical then {
rlp_decode_list(f)
} else {
fatal_error(InvalidBlockAccessList)
}function fatal_error(_reason) = exit(())function rlp_decode_list(f) =
if f.is_list then {
sub_slice(f.source, f.source.len - f.content_len, f.content_len)
} else {
fatal_error(RlpDecode)
}Whether a field uses the unique canonical RLP framing for its payload.
function rlp_ref_framing_canonical 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
) = {
let n = f.content_len;
let payload_length = n;
let full_length = f.source.len;
let full_offset = 0;
let content_offset = full_length - payload_length;
let source = f.source;
let source_length = source.len;
if full_length == 0 then {
false
} else if f.is_list then {
if n <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(n);
(full_length == payload_length + 1) & (slice_byte(f.source, 0) == add_bits(0xc0, length_byte))
} else {
let length_word = rlp_length_word(n);
let length_width = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_width);
(full_length == 1 + length_width + payload_length)
& (slice_byte(f.source, 0) == add_bits(0xf7, length_byte))
& (if full_offset < source_length
then slice_load_n(f.source, full_offset + 1, length_width) == length_word
else false)
}
} else if payload_length == 0 then {
(full_length == 1) & (slice_byte(f.source, 0) == 0x80)
} else {
let first = slice_byte(f.source, content_offset);
if (payload_length == 1) & (first[7] == bitzero) then {
(full_length == 1) & (slice_byte(f.source, 0) == first)
} else if n <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(n);
(full_length == payload_length + 1) & (slice_byte(f.source, 0) == add_bits(0x80, length_byte))
} else {
let length_word = rlp_length_word(n);
let length_width = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_width);
(full_length == 1 + length_width + payload_length)
& (slice_byte(f.source, 0) == add_bits(0xb7, length_byte))
& (if full_offset < source_length
then slice_load_n(f.source, full_offset + 1, length_width) == length_word
else false)
}
}
}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,
}function bal_ref_bytes¶
Requires a canonical RLP byte string and returns its content slice.
function bal_ref_bytes 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)) -> (
StatelessInputSlice
) =
let canonical = rlp_ref_bytes_canonical(f) in
if canonical then {
rlp_item_content(f)
} else {
fatal_error(InvalidBlockAccessList)
}function fatal_error(_reason) = exit(())The content span of a field.
function rlp_item_content 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)) -> (
StatelessInputSlice
) =
sub_slice(f.source, f.source.len - f.content_len, f.content_len)Whether a field is a byte string with its unique canonical RLP framing.
function rlp_ref_bytes_canonical 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
) =
not_bool(f.is_list) & rlp_ref_framing_canonical(f)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,
}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 stateless-input range with its coordinate and length packed existentially.
type StatelessInputSlice = {
'off 'len,
stateless_input_valid_range('off, 'len).
StatelessInputSliceFields('off, 'len)
}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 bal_ref_word¶
Requires a canonical RLP integer in the EVM-word domain.
function bal_ref_word 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)) -> (
word
) =
let canonical = rlp_item_uint_canonical(f) in
if canonical & (f.content_len <= 32) then {
rlp_decode_word(f)
} else {
fatal_error(InvalidBlockAccessList)
}function fatal_error(_reason) = exit(())Decodes a string field of at most 32 bytes into a word.
function rlp_decode_word 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)) -> (
word
) = {
let n = f.content_len;
if f.is_list | (RLP_WORD_LENGTH_LIMIT < n) then {
fatal_error(RlpDecode)
} else {
slice_load_n(f.source, f.source.len - n, n)
}
}Whether a field is the canonical RLP encoding of a non-negative integer: minimal big-endian content with no leading zeros and the exact matching prefix.
function rlp_item_uint_canonical 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
) =
let bytes_canonical = rlp_ref_bytes_canonical(f) in
let invalid = not_bool(bytes_canonical) in
if invalid then {
false
} else {
(f.content_len == 0) | (slice_byte(f.source, f.source.len - f.content_len) != 0x00)
}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,
}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),
}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_lenThe 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 bal_ref_uint64¶
Requires a canonical RLP integer in the host-index/nonce domain.
function bal_ref_uint64 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)) -> (
ssz_uint
) =
let canonical = rlp_item_uint_canonical(f) in
if canonical & (f.content_len <= 8) then {
rlp_decode_uint64(f)
} else {
fatal_error(InvalidBlockAccessList)
}function fatal_error(_reason) = exit(())Decodes a canonical unsigned integer into the uint64 wire domain used by EIP-2681 account nonces and EIP-4844 excess blob gas.
function rlp_decode_uint64 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)) -> (
ssz_uint
) = {
let canonical = rlp_item_uint_canonical(f);
let invalid_encoding = not_bool(canonical);
if invalid_encoding | (RLP_UINT64_LENGTH_LIMIT < f.content_len) then {
fatal_error(RlpDecode)
};
let content_length = f.content_len;
let content = rlp_item_content(f);
/* The semantic check above establishes content_length <= 8. Modulo nine
* only exposes that already-proven bound to Sail's dependent type system. */
let width : range(0, 8) = tmod_nat(content_length, 9);
rlp_uint64_width(content, width)
}Whether a field is the canonical RLP encoding of a non-negative integer: minimal big-endian content with no leading zeros and the exact matching prefix.
function rlp_item_uint_canonical 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
) =
let bytes_canonical = rlp_ref_bytes_canonical(f) in
let invalid = not_bool(bytes_canonical) in
if invalid then {
false
} else {
(f.content_len == 0) | (slice_byte(f.source, f.source.len - f.content_len) != 0x00)
}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,
}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),
}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_lenAn eight-byte unsigned integer read from the stateless-input SSZ schema. This is a transport type; decoders widen or validate it into the semantic field type at the container boundary.
type ssz_uint = range(0, 2 ^ 64 - 1)function bal_expect_end¶
Requires that a decoded list has no unconsumed children.
function bal_expect_end forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (cursor :
RlpCursor('source_off, 'source_len)) -> (
unit
) = {
if cursor.len == 0 then {
return ()
};
fatal_error(InvalidBlockAccessList)
}function fatal_error(_reason) = exit(())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 one-pass RLP cursor is the unconsumed suffix of its source. Decoding yields a field whose length witnesses a valid advance; the caller owns the corresponding cursor transition.
type RlpCursor('source_off : Int, 'source_len : Int),
source_valid_range('source_off, 'source_len) =
StatelessInputSliceFields('source_off, 'source_len)Common bound for relative source coordinates used by generic cursor operations. Nominal slices retain their region-specific invariant.
type source_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= default_host_region_bound