Transaction RLP decoding¶
The EIP-2718 transaction envelope decoder: per-envelope destructuring into the Transaction type (one walk, against each envelope's exact field shape), plus the EIP-2930 access-list and EIP-7702 authorization-tuple decoders. Standalone and purely structural: the envelope and public key are immutable stateless-input spans; the signature rules and the cryptography live in their own modules.
type AccessListDecode¶
A decoded access list and the counts needed for intrinsic gas.
struct AccessListDecode('address_bound : Int, 'slot_bound : Int),
source_valid_length('address_bound) & source_valid_length('slot_bound) = {
address_count : range(0, 'address_bound),
slot_count : range(0, 'slot_bound),
}Whether one relative source coordinate is representable.
type source_valid_length('value : Int) -> Bool =
0 <= 'value & 'value <= default_host_region_boundlet EMPTY_ACCESS_LIST_DECODE¶
let EMPTY_ACCESS_LIST_DECODE : AccessListDecode(0, 0) = struct { address_count = 0, slot_count = 0 }A decoded access list and the counts needed for intrinsic gas.
struct AccessListDecode('address_bound : Int, 'slot_bound : Int),
source_valid_length('address_bound) & source_valid_length('slot_bound) = {
address_count : range(0, 'address_bound),
slot_count : range(0, 'slot_bound),
}function transaction_rlp_content¶
Reclassifies transaction RLP content as an immutable input span. Every cursor in this module originates in the transaction envelope.
function transaction_rlp_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
) = {
let content = rlp_item_content(f);
stateless_input_slice(content.bytes, content.len)
}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)function stateless_input_slice(off, len) =
struct { bytes = off, len = len }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 decode_access_list_keys¶
function decode_access_list_keys(cursor, addr, tail) =
if cursor.len == 0 then {
struct { address_count = tail.address_count, slot_count = tail.slot_count }
} else {
let key = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, key.source.len);
let _ : StorageKey = struct { addr = addr, slot = rlp_decode_word(key) };
let result = decode_access_list_keys(next, addr, tail);
struct { address_count = result.address_count, slot_count = result.slot_count + 1 }
}function decode_access_list_keys(cursor, addr, tail) =
if cursor.len == 0 then {
struct { address_count = tail.address_count, slot_count = tail.slot_count }
} else {
let key = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, key.source.len);
let _ : StorageKey = struct { addr = addr, slot = rlp_decode_word(key) };
let result = decode_access_list_keys(next, addr, tail);
struct { address_count = result.address_count, slot_count = result.slot_count + 1 }
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}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)
}
}A fully qualified storage key: account address and 256-bit slot.
struct StorageKey = { addr : address, slot : word }function decode_access_list_entries¶
function decode_access_list_entries(cursor) =
if cursor.len == 0 then {
EMPTY_ACCESS_LIST_DECODE
} else {
let entry = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, entry.source.len);
let entry_fields = rlp_decode_list(entry);
let addr_f = rlp_decode_item(entry_fields);
let entry_fields = rlp_cursor_advance(entry_fields, addr_f.source.len);
let keys_f = rlp_decode_item(entry_fields);
let entry_fields = rlp_cursor_advance(entry_fields, keys_f.source.len);
rlp_cursor_expect_end(entry_fields);
let address_word = rlp_decode_word(addr_f);
let addr = word_to_address(address_word);
let tail = decode_access_list_entries(next);
let keys = rlp_decode_list(keys_f);
let result = decode_access_list_keys(keys, addr, tail);
struct { address_count = result.address_count + 1, slot_count = result.slot_count }
}function decode_access_list_entries(cursor) =
if cursor.len == 0 then {
EMPTY_ACCESS_LIST_DECODE
} else {
let entry = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, entry.source.len);
let entry_fields = rlp_decode_list(entry);
let addr_f = rlp_decode_item(entry_fields);
let entry_fields = rlp_cursor_advance(entry_fields, addr_f.source.len);
let keys_f = rlp_decode_item(entry_fields);
let entry_fields = rlp_cursor_advance(entry_fields, keys_f.source.len);
rlp_cursor_expect_end(entry_fields);
let address_word = rlp_decode_word(addr_f);
let addr = word_to_address(address_word);
let tail = decode_access_list_entries(next);
let keys = rlp_decode_list(keys_f);
let result = decode_access_list_keys(keys, addr, tail);
struct { address_count = result.address_count + 1, slot_count = result.slot_count }
}function decode_access_list_keys(cursor, addr, tail) =
if cursor.len == 0 then {
struct { address_count = tail.address_count, slot_count = tail.slot_count }
} else {
let key = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, key.source.len);
let _ : StorageKey = struct { addr = addr, slot = rlp_decode_word(key) };
let result = decode_access_list_keys(next, addr, tail);
struct { address_count = result.address_count, slot_count = result.slot_count + 1 }
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}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)
}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)
}
}Converts a word to its low 160-bit address in canonical byte order.
function word_to_address(value : word) -> address = {
let zero_bytes = vector_init(20, 0x00);
var result : address = Address(zero_bytes);
result[0] = get_slice_int(8, value, 152);
result[1] = get_slice_int(8, value, 144);
result[2] = get_slice_int(8, value, 136);
result[3] = get_slice_int(8, value, 128);
result[4] = get_slice_int(8, value, 120);
result[5] = get_slice_int(8, value, 112);
result[6] = get_slice_int(8, value, 104);
result[7] = get_slice_int(8, value, 96);
result[8] = get_slice_int(8, value, 88);
result[9] = get_slice_int(8, value, 80);
result[10] = get_slice_int(8, value, 72);
result[11] = get_slice_int(8, value, 64);
result[12] = get_slice_int(8, value, 56);
result[13] = get_slice_int(8, value, 48);
result[14] = get_slice_int(8, value, 40);
result[15] = get_slice_int(8, value, 32);
result[16] = get_slice_int(8, value, 24);
result[17] = get_slice_int(8, value, 16);
result[18] = get_slice_int(8, value, 8);
result[19] = get_slice_int(8, value, 0);
result
}let EMPTY_ACCESS_LIST_DECODE : AccessListDecode(0, 0) = struct { address_count = 0, slot_count = 0 }function decode_access_list¶
Decodes an EIP-2930 access list — RLP [[address, [slot, …]], …] —
without materializing its entries.
function decode_access_list 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)) -> (
AccessListRef
) = {
if f.source.len <= sizeof(transaction_length_bound) then {
let entries = rlp_decode_list(f);
let decoded = decode_access_list_entries(entries);
struct {
encoded = transaction_rlp_content(f),
address_count = decoded.address_count,
slot_count = decoded.slot_count,
}
} else {
fatal_error(RlpDecode)
}
}function decode_access_list_entries(cursor) =
if cursor.len == 0 then {
EMPTY_ACCESS_LIST_DECODE
} else {
let entry = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, entry.source.len);
let entry_fields = rlp_decode_list(entry);
let addr_f = rlp_decode_item(entry_fields);
let entry_fields = rlp_cursor_advance(entry_fields, addr_f.source.len);
let keys_f = rlp_decode_item(entry_fields);
let entry_fields = rlp_cursor_advance(entry_fields, keys_f.source.len);
rlp_cursor_expect_end(entry_fields);
let address_word = rlp_decode_word(addr_f);
let addr = word_to_address(address_word);
let tail = decode_access_list_entries(next);
let keys = rlp_decode_list(keys_f);
let result = decode_access_list_keys(keys, addr, tail);
struct { address_count = result.address_count + 1, slot_count = result.slot_count }
}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)
}Reclassifies transaction RLP content as an immutable input span. Every cursor in this module originates in the transaction envelope.
function transaction_rlp_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
) = {
let content = rlp_item_content(f);
stateless_input_slice(content.bytes, content.len)
}A validated EIP-2930 access-list content span. Entries remain in their canonical RLP encoding and are consumed with a cursor when prewarming.
struct AccessListRef = {
encoded : StatelessInputSlice,
address_count : transaction_item_count,
slot_count : transaction_item_count,
}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_lenMaximum byte length of one encoded transaction envelope. Provenance:
Amsterdam MAX_BYTES_PER_TRANSACTION in
SszExecutionPayload.transactions.
type transaction_length_bound : Int = 2 ^ 30Constants¶
Typed transaction decoding uses the fixed RLP widths of versioned blob hashes and the domain tags and field counts defined by the transaction EIPs.
let BLOB_HASH_RLP_LENGTH¶
let BLOB_HASH_RLP_LENGTH : int(33) = 33let BLOB_HASH_LENGTH¶
let BLOB_HASH_LENGTH : int(32) = WORD_BYTE_LENGTHlet WORD_BYTE_LENGTH : int(32) = 32function decode_blob_hash_items¶
Validates every fixed-width versioned-hash item and returns their count. The cursor exits immediately for an empty list and checks the version byte while each item is already live, avoiding a second fixed-width pass.
function decode_blob_hash_items forall 'source_off 'source_len 'limit,
source_valid_range('source_off, 'source_len) & transaction_blob_limit_value('limit). (
cursor : RlpCursor('source_off, 'source_len),
limit : int('limit),
count : transaction_blob_count('limit),
) -> (
transaction_blob_count('limit)
) =
if cursor.len == 0 then {
count
} else {
let item = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, item.source.len);
let item_prefix = slice_byte(item.source, 0);
if item.is_list
| item.source.len
!= BLOB_HASH_RLP_LENGTH
| item.content_len
!= BLOB_HASH_LENGTH
| item_prefix
!= 0xa0 then {
fatal_error(RlpDecode)
};
let version = slice_byte(item.source, 1);
if version != 0x01 then {
fatal_error(ExecutionInvalid)
};
if count < limit then {
decode_blob_hash_items(next, limit, count + 1)
} else {
fatal_error(RlpDecode)
}
}Validates every fixed-width versioned-hash item and returns their count. The cursor exits immediately for an empty list and checks the version byte while each item is already live, avoiding a second fixed-width pass.
function decode_blob_hash_items forall 'source_off 'source_len 'limit,
source_valid_range('source_off, 'source_len) & transaction_blob_limit_value('limit). (
cursor : RlpCursor('source_off, 'source_len),
limit : int('limit),
count : transaction_blob_count('limit),
) -> (
transaction_blob_count('limit)
) =
if cursor.len == 0 then {
count
} else {
let item = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, item.source.len);
let item_prefix = slice_byte(item.source, 0);
if item.is_list
| item.source.len
!= BLOB_HASH_RLP_LENGTH
| item.content_len
!= BLOB_HASH_LENGTH
| item_prefix
!= 0xa0 then {
fatal_error(RlpDecode)
};
let version = slice_byte(item.source, 1);
if version != 0x01 then {
fatal_error(ExecutionInvalid)
};
if count < limit then {
decode_blob_hash_items(next, limit, count + 1)
} else {
fatal_error(RlpDecode)
}
}function fatal_error(_reason) = exit(())function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}let BLOB_HASH_LENGTH : int(32) = WORD_BYTE_LENGTHlet BLOB_HASH_RLP_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,
}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_boundA transaction blob count under one fork-selected transaction limit. The limit is a finite-set profile parameter; the observed count occupies the complete contiguous range beneath that selected limit.
type transaction_blob_count('limit : Int) = range(0, 'limit)The fork-selected maximum number of blobs carried by one transaction. Zero denotes a profile before blob transactions activate.
type transaction_blob_limit_value('value : Int) -> Bool =
'value == blob_schedule_inactive_count
| 'value == cancun_blob_max_count
| 'value == prague_blob_max_countfunction decode_blob_hashes¶
Validates the canonical RLP list of bytes32 blob versioned hashes
once, then retains its encoded content as a fixed-stride source view:
each element is exactly 0xa0 followed by 32 bytes, so BLOBHASH can
load item i at 33·i + 1.
function decode_blob_hashes forall 'source_off 'source_len 'content_len 'limit,
rlp_field_ref_valid('source_off, 'source_len, 'content_len) &
transaction_blob_limit_value('limit). (
f : RlpFieldRef('source_off, 'source_len, 'content_len),
limit : int('limit),
) -> (
BlobHashesFields('limit)
) = {
let bytes = transaction_rlp_content(f);
let items = rlp_decode_list(f);
let count = decode_blob_hash_items(items, limit, 0);
struct { bytes = bytes, count = count }
}Validates every fixed-width versioned-hash item and returns their count. The cursor exits immediately for an empty list and checks the version byte while each item is already live, avoiding a second fixed-width pass.
function decode_blob_hash_items forall 'source_off 'source_len 'limit,
source_valid_range('source_off, 'source_len) & transaction_blob_limit_value('limit). (
cursor : RlpCursor('source_off, 'source_len),
limit : int('limit),
count : transaction_blob_count('limit),
) -> (
transaction_blob_count('limit)
) =
if cursor.len == 0 then {
count
} else {
let item = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, item.source.len);
let item_prefix = slice_byte(item.source, 0);
if item.is_list
| item.source.len
!= BLOB_HASH_RLP_LENGTH
| item.content_len
!= BLOB_HASH_LENGTH
| item_prefix
!= 0xa0 then {
fatal_error(RlpDecode)
};
let version = slice_byte(item.source, 1);
if version != 0x01 then {
fatal_error(ExecutionInvalid)
};
if count < limit then {
decode_blob_hash_items(next, limit, count + 1)
} else {
fatal_error(RlpDecode)
}
}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)
}Reclassifies transaction RLP content as an immutable input span. Every cursor in this module originates in the transaction envelope.
function transaction_rlp_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
) = {
let content = rlp_item_content(f);
stateless_input_slice(content.bytes, content.len)
}The source-backed EIP-4844 versioned blob hashes of a transaction. The
limit index records which fork-selected transaction range admitted the
observed count. It is carried by the enclosing transaction rather than
hidden in a nested existential, so consumers retain count <= limit.
struct BlobHashesFields('limit : Int), transaction_blob_limit_value('limit) = {
bytes : StatelessInputSlice,
count : transaction_blob_count('limit),
}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 fork-selected maximum number of blobs carried by one transaction. Zero denotes a profile before blob transactions activate.
type transaction_blob_limit_value('value : Int) -> Bool =
'value == blob_schedule_inactive_count
| 'value == cancun_blob_max_count
| 'value == prague_blob_max_countfunction validate_auth_tuples¶
function validate_auth_tuples(cursor, count) =
if cursor.len == 0 then {
count
} else {
let tuple = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, tuple.source.len);
let _ = rlp_decode_list(tuple);
if count < sizeof(transaction_length_bound) then {
validate_auth_tuples(next, count + 1)
} else {
fatal_error(RlpDecode)
}
}function fatal_error(_reason) = exit(())function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}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)
}function validate_auth_tuples(cursor, count) =
if cursor.len == 0 then {
count
} else {
let tuple = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, tuple.source.len);
let _ = rlp_decode_list(tuple);
if count < sizeof(transaction_length_bound) then {
validate_auth_tuples(next, count + 1)
} else {
fatal_error(RlpDecode)
}
}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,
}Maximum byte length of one encoded transaction envelope. Provenance:
Amsterdam MAX_BYTES_PER_TRANSACTION in
SszExecutionPayload.transactions.
type transaction_length_bound : Int = 2 ^ 30function decode_auth_list¶
Decodes an EIP-7702 authorization list into a validated source-backed cursor view.
function decode_auth_list 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)) -> (
AuthorizationListRef
) = {
if f.source.len <= sizeof(transaction_length_bound) then {
let content = transaction_rlp_content(f);
let tuples = rlp_decode_list(f);
let count = validate_auth_tuples(tuples, 0);
authorization_list_ref(content, count)
} else {
fatal_error(RlpDecode)
}
}function authorization_list_ref(encoded, count) =
struct { encoded = encoded, count = count }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)
}Reclassifies transaction RLP content as an immutable input span. Every cursor in this module originates in the transaction envelope.
function transaction_rlp_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
) = {
let content = rlp_item_content(f);
stateless_input_slice(content.bytes, content.len)
}function validate_auth_tuples(cursor, count) =
if cursor.len == 0 then {
count
} else {
let tuple = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, tuple.source.len);
let _ = rlp_decode_list(tuple);
if count < sizeof(transaction_length_bound) then {
validate_auth_tuples(next, count + 1)
} else {
fatal_error(RlpDecode)
}
}An authorization-list reference packing its admitted tuple count existentially.
type AuthorizationListRef = {
'count,
0 <= 'count & 'count <= transaction_length_bound.
AuthorizationListRefFields('count)
}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_lenMaximum byte length of one encoded transaction envelope. Provenance:
Amsterdam MAX_BYTES_PER_TRANSACTION in
SszExecutionPayload.transactions.
type transaction_length_bound : Int = 2 ^ 30function decode_authorization¶
function decode_authorization(tuple) = {
let fields = rlp_decode_list(tuple);
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let addr_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, addr_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let y_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, y_f.source.len);
let y = rlp_decode_bool(y_f);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let chain_id = rlp_decode_u256(chain_f);
let auth_nonce : account_nonce = rlp_decode_uint64(nonce_f);
let r = rlp_decode_u256(r_f);
let s = rlp_decode_u256(s_f);
let address_word = rlp_decode_word(addr_f);
let auth_addr = word_to_address(address_word);
let signing_hash = auth_signing_hash(chain_id, auth_addr, auth_nonce);
let recovered : AddressResult = match y {
RlpOk(false) => ecrecover_addr(signing_hash, 0, r, s),
RlpOk(true) => ecrecover_addr(signing_hash, 1, r, s),
RlpInvalidValue() => struct { success = false, address = ZERO_ADDRESS },
};
struct {
valid_sig =
recovered.success
& word_ult(ZERO_WORD, r)
& word_ult(r, SECP_N_FULL)
& word_ult(ZERO_WORD, s)
& word_ule(s, SECP_N_HALF)
& (auth_nonce != sizeof(account_nonce_bound)),
authority = recovered.address,
address = auth_addr,
nonce = auth_nonce,
chain_id = chain_id,
}
}The EIP-7702 authorization signing hash:
keccak256(0x05 || rlp([chain_id, address, nonce])).
function auth_signing_hash(chain_id : word, addr : address, nonce : account_nonce) -> hash = {
let chain_id_length = rlp_uint_word_size(chain_id);
let address_length = rlp_addr_size();
let nonce_length = rlp_uint_size(nonce);
let content_len : range(0, 87) = chain_id_length + address_length + nonce_length;
let preimage_len : range(0, 121) = 1 + rlp_list_size(content_len);
let encoder = rlp_encoder_begin(preimage_len);
scratch_push_byte(0x05);
rlp_write_list_prefix(content_len);
rlp_write_uint_word(chain_id);
rlp_write_addr(addr);
rlp_write_uint(nonce);
let encoded = rlp_encoder_finish(encoder);
let signing_hash = keccak256(encoded);
rlp_encoder_rewind(encoder);
signing_hash
}function decode_authorization(tuple) = {
let fields = rlp_decode_list(tuple);
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let addr_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, addr_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let y_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, y_f.source.len);
let y = rlp_decode_bool(y_f);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let chain_id = rlp_decode_u256(chain_f);
let auth_nonce : account_nonce = rlp_decode_uint64(nonce_f);
let r = rlp_decode_u256(r_f);
let s = rlp_decode_u256(s_f);
let address_word = rlp_decode_word(addr_f);
let auth_addr = word_to_address(address_word);
let signing_hash = auth_signing_hash(chain_id, auth_addr, auth_nonce);
let recovered : AddressResult = match y {
RlpOk(false) => ecrecover_addr(signing_hash, 0, r, s),
RlpOk(true) => ecrecover_addr(signing_hash, 1, r, s),
RlpInvalidValue() => struct { success = false, address = ZERO_ADDRESS },
};
struct {
valid_sig =
recovered.success
& word_ult(ZERO_WORD, r)
& word_ult(r, SECP_N_FULL)
& word_ult(ZERO_WORD, s)
& word_ule(s, SECP_N_HALF)
& (auth_nonce != sizeof(account_nonce_bound)),
authority = recovered.address,
address = auth_addr,
nonce = auth_nonce,
chain_id = chain_id,
}
}Recovers the signer address from (h, y_parity, r, s), returning
recovery success and the recovered address (used by EIP-7702).
function ecrecover_addr(h : hash, yparity : y_parity, r : word, s : word) -> AddressResult = {
host_ecrecover(h, yparity, r, s)
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}function rlp_decode_bool(field) = {
let value = rlp_decode_uint64(field);
match value {
0 => RlpOk(false),
1 => RlpOk(true),
_ => RlpInvalidValue(),
}
}function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}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)
}Decodes a canonical unsigned integer field into a word; throws otherwise.
function rlp_decode_u256 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 then {
rlp_decode_word(f)
} else {
fatal_error(RlpDecode)
}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)
}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)
}
}Converts a word to its low 160-bit address in canonical byte order.
function word_to_address(value : word) -> address = {
let zero_bytes = vector_init(20, 0x00);
var result : address = Address(zero_bytes);
result[0] = get_slice_int(8, value, 152);
result[1] = get_slice_int(8, value, 144);
result[2] = get_slice_int(8, value, 136);
result[3] = get_slice_int(8, value, 128);
result[4] = get_slice_int(8, value, 120);
result[5] = get_slice_int(8, value, 112);
result[6] = get_slice_int(8, value, 104);
result[7] = get_slice_int(8, value, 96);
result[8] = get_slice_int(8, value, 88);
result[9] = get_slice_int(8, value, 80);
result[10] = get_slice_int(8, value, 72);
result[11] = get_slice_int(8, value, 64);
result[12] = get_slice_int(8, value, 56);
result[13] = get_slice_int(8, value, 48);
result[14] = get_slice_int(8, value, 40);
result[15] = get_slice_int(8, value, 32);
result[16] = get_slice_int(8, value, 24);
result[17] = get_slice_int(8, value, 16);
result[18] = get_slice_int(8, value, 8);
result[19] = get_slice_int(8, value, 0);
result
}function word_ule(a, b) = {
let greater = word_ult(b, a);
not_bool(greater)
}function word_ult(a, b) = a < bn of the secp256k1 group order.
let SECP_N_FULL : word = word_from_bits(0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141)n/2 of the secp256k1 group order — the EIP-2 low-s malleability
bound.
let SECP_N_HALF : word = word_from_bits(0x7fffffffffffffffffffffffffffffff5d576e7357a4501ddfe92f46681b20a0)let ZERO_ADDRESS : address = address_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)let ZERO_WORD : word = word_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)A host address operation's success flag and address result.
struct AddressResult = {
success : bool,
address : address,
}The result of applying an RLP field's protocol-level value constraint.
Structurally invalid or non-canonical RLP remains an InvalidBlock
exception; this result distinguishes a well-formed value outside the
requested field domain.
union RlpResult('value : Type) = {
/* the decoded value satisfies the requested field domain */
RlpOk : 'value,
/* well-formed RLP whose value falls outside the field domain */
RlpInvalidValue : unit
}An account transaction-count nonce (EIP-2681).
type account_nonce = range(0, account_nonce_bound)The largest account nonce admitted by EIP-2681.
type account_nonce_bound : Int = 2 ^ 64 - 1A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)function prepare_authorization_entries¶
function prepare_authorization_entries(cursor, count) =
if count == 0 then {
if cursor.len != 0 then {
fatal_error(RlpDecode)
};
[||]
} else {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let tuple = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, tuple.source.len);
let authorization = decode_authorization(tuple);
authorization :: prepare_authorization_entries(next, count - 1)
}function decode_authorization(tuple) = {
let fields = rlp_decode_list(tuple);
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let addr_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, addr_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let y_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, y_f.source.len);
let y = rlp_decode_bool(y_f);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let chain_id = rlp_decode_u256(chain_f);
let auth_nonce : account_nonce = rlp_decode_uint64(nonce_f);
let r = rlp_decode_u256(r_f);
let s = rlp_decode_u256(s_f);
let address_word = rlp_decode_word(addr_f);
let auth_addr = word_to_address(address_word);
let signing_hash = auth_signing_hash(chain_id, auth_addr, auth_nonce);
let recovered : AddressResult = match y {
RlpOk(false) => ecrecover_addr(signing_hash, 0, r, s),
RlpOk(true) => ecrecover_addr(signing_hash, 1, r, s),
RlpInvalidValue() => struct { success = false, address = ZERO_ADDRESS },
};
struct {
valid_sig =
recovered.success
& word_ult(ZERO_WORD, r)
& word_ult(r, SECP_N_FULL)
& word_ult(ZERO_WORD, s)
& word_ule(s, SECP_N_HALF)
& (auth_nonce != sizeof(account_nonce_bound)),
authority = recovered.address,
address = auth_addr,
nonce = auth_nonce,
chain_id = chain_id,
}
}function fatal_error(_reason) = exit(())function prepare_authorization_entries(cursor, count) =
if count == 0 then {
if cursor.len != 0 then {
fatal_error(RlpDecode)
};
[||]
} else {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let tuple = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, tuple.source.len);
let authorization = decode_authorization(tuple);
authorization :: prepare_authorization_entries(next, count - 1)
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}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 prepare_authorizations¶
Materializes a transaction's authorizations only after successful validity has made this narrowing guard unreachable for protocol-valid input.
function prepare_authorizations(authorizations : AuthorizationListRef) -> PreparedAuthorizationList = {
if authorizations.count <= sizeof(prepared_authorization_count_bound) then {
let encoded : StatelessInputSlice = authorizations.encoded;
let entries = prepare_authorization_entries(encoded, authorizations.count);
struct { entries = entries, count = authorizations.count }
} else {
fatal_error(ExecutionInvalid)
}
}function fatal_error(_reason) = exit(())function prepare_authorization_entries(cursor, count) =
if count == 0 then {
if cursor.len != 0 then {
fatal_error(RlpDecode)
};
[||]
} else {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let tuple = rlp_decode_item(cursor);
let next = rlp_cursor_advance(cursor, tuple.source.len);
let authorization = decode_authorization(tuple);
authorization :: prepare_authorization_entries(next, count - 1)
}An authorization-list reference packing its admitted tuple count existentially.
type AuthorizationListRef = {
'count,
0 <= 'count & 'count <= transaction_length_bound.
AuthorizationListRefFields('count)
}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,
}Authorizations decoded and signature-recovered after transaction validity but before any world-state mutation. The semantic model retains an immutable list. Optimized C represents the same ordered collection as a cursor into a fixed-capacity transaction workspace.
struct PreparedAuthorizationList = {
entries : list(Authorization),
count : prepared_authorization_count,
}A stateless-input range with its coordinate and length packed existentially.
type StatelessInputSlice = {
'off 'len,
stateless_input_valid_range('off, 'len).
StatelessInputSliceFields('off, 'len)
}EIP-7825 bounds a post-Prague transaction to 2^24 regular gas, while Amsterdam's least expensive authorization costs 7,816 execution gas. Successful transaction validity therefore proves that no executable authorization list can contain more entries than this bound.
type prepared_authorization_count_bound : Int = div(eip7825_transaction_gas_limit, 7816)function prepared_authorization_head¶
Reads the current prepared entry. Callers carry the decreasing count that proves this operation is not applied to the empty collection.
function prepared_authorization_head(authorizations : PreparedAuthorizationList) -> Authorization =
match authorizations.entries {
authorization :: _ => authorization,
[||] => fatal_error(ExecutionInvalid),
}function fatal_error(_reason) = exit(())An EIP-7702 set-code authorization tuple. RLP decoding recovers the
authority and validates the signature (s <= n/2, y_parity, r);
valid_sig records that result, and process_auth applies the
chain-id/nonce/code checks.
struct Authorization = {
valid_sig : bool, authority : address, address : address,
nonce : account_nonce, chain_id : word,
}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,
}Authorizations decoded and signature-recovered after transaction validity but before any world-state mutation. The semantic model retains an immutable list. Optimized C represents the same ordered collection as a cursor into a fixed-capacity transaction workspace.
struct PreparedAuthorizationList = {
entries : list(Authorization),
count : prepared_authorization_count,
}function prepared_authorization_tail¶
function prepared_authorization_tail(authorizations, count) =
match authorizations.entries {
_ :: entries => struct { entries = entries, count = count - 1 },
[||] => fatal_error(ExecutionInvalid),
}function fatal_error(_reason) = exit(())function prepared_authorization_tail(authorizations, count) =
match authorizations.entries {
_ :: entries => struct { entries = entries, count = count - 1 },
[||] => 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,
}function tx_input_span¶
The calldata/initcode span of the data field within the envelope. The RLP cursor existentially hides its bounded source length, so this boundary reifies the already-established transaction-envelope invariant.
function tx_input_span forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (data :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
TransactionInputSlice
) = {
let content = transaction_rlp_content(data);
if content.len <= sizeof(transaction_length_bound) then {
content
} else {
fatal_error(RlpDecode)
}
}function fatal_error(_reason) = exit(())Reclassifies transaction RLP content as an immutable input span. Every cursor in this module originates in the transaction envelope.
function transaction_rlp_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
) = {
let content = rlp_item_content(f);
stateless_input_slice(content.bytes, content.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,
}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 byte span contained by one SSZ transaction envelope. This structural bound is independent of fork-specific calldata and initcode limits.
type TransactionInputSlice = {
'off 'len,
source_valid_range('off, 'len) & 0 <= 'len & 'len <= transaction_length_bound.
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_lenMaximum byte length of one encoded transaction envelope. Provenance:
Amsterdam MAX_BYTES_PER_TRANSACTION in
SszExecutionPayload.transactions.
type transaction_length_bound : Int = 2 ^ 30function tx_sig_span¶
function tx_sig_span(first, signature) = {
let start = first.source.bytes;
let stop = signature.source.bytes;
let start_offset = start;
let stop_offset = stop;
if stop_offset < start_offset then {
fatal_error(RlpDecode)
} else {
stateless_input_slice(start_offset, stop_offset - start_offset)
}
}function fatal_error(_reason) = exit(())function stateless_input_slice(off, len) =
struct { bytes = off, len = len }function tx_sig_span(first, signature) = {
let start = first.source.bytes;
let stop = signature.source.bytes;
let start_offset = start;
let stop_offset = stop;
if stop_offset < start_offset then {
fatal_error(RlpDecode)
} else {
stateless_input_slice(start_offset, stop_offset - start_offset)
}
}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 rlp_decode_gas¶
Decodes transaction gas structurally. Admission against the executing block's correlated gas limits belongs to transaction validation, after the envelope has been decoded.
function rlp_decode_gas 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)) -> (
transaction_gas
) =
rlp_decode_uint64(f)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)
}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_lenGas supplied by a transaction before fork-specific validation. Any value
above the execution payload's SSZ uint64 block-gas-limit domain cannot be
admitted, so the RLP boundary rejects it before constructing a
transaction.
type transaction_gas = range(0, block_gas_limit_bound)function decode_legacy_tx¶
Decodes the payload fields of a legacy transaction. Kept separate from the envelope dispatcher so extraction backends compile each transaction shape as an independent function.
function decode_legacy_tx forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields(blob_schedule_inactive_count)
) = {
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let gp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gp_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let gp = rlp_decode_u256(gp_f);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(nonce_f, v_f);
let signing_hash = tx_signing_hash(LegacyTx, signing_span, v);
struct {
tx_type = LegacyTx,
sender = sender,
raw = tx,
nonce = rlp_decode_u256(nonce_f),
chain_id = 0,
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = EMPTY_ACCESS_LIST_REF,
max_fee = gp,
max_blob_fee = ZERO_WORD,
max_priority_fee = gp,
authorizations = EMPTY_AUTHORIZATION_LIST_REF,
blob_hashes = EMPTY_BLOB_HASHES,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}Decodes transaction gas structurally. Admission against the executing block's correlated gas limits belongs to transaction validation, after the envelope has been decoded.
function rlp_decode_gas 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)) -> (
transaction_gas
) =
rlp_decode_uint64(f)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}Decodes a canonical unsigned integer field into a word; throws otherwise.
function rlp_decode_u256 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 then {
rlp_decode_word(f)
} else {
fatal_error(RlpDecode)
}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)
}
}The calldata/initcode span of the data field within the envelope. The RLP cursor existentially hides its bounded source length, so this boundary reifies the already-established transaction-envelope invariant.
function tx_input_span forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (data :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
TransactionInputSlice
) = {
let content = transaction_rlp_content(data);
if content.len <= sizeof(transaction_length_bound) then {
content
} else {
fatal_error(RlpDecode)
}
}function tx_sig_span(first, signature) = {
let start = first.source.bytes;
let stop = signature.source.bytes;
let start_offset = start;
let stop_offset = stop;
if stop_offset < start_offset then {
fatal_error(RlpDecode)
} else {
stateless_input_slice(start_offset, stop_offset - start_offset)
}
}The transaction signing-preimage hash. content_src spans the RLP of
the pre-signature fields in the witness and is copied once into the final
contiguous preimage; legacy EIP-155 transactions append
(chain_id, 0, 0), typed transactions prepend the type byte as a
domain separator (EIP-2718).
function tx_signing_hash(t : TxType, content_src : StatelessInputSlice, v : word) -> hash = {
let tb : byte = tx_envelope_type(t);
let eip155 = (tb == 0x00) & word_ule(35, v);
let chain_id =
if eip155 then legacy_sig_chain_id(v) else ZERO_WORD;
let suffix_len : range(0, 35) =
if eip155 then {
let chain_id_length = rlp_uint_word_size(chain_id);
let suffix_length = LEGACY_SIGNATURE_SUFFIX_LENGTH;
chain_id_length + suffix_length
} else {
0
};
let content_length : transaction_byte_length =
if content_src.len <= sizeof(transaction_length_bound) then content_src.len else fatal_error(RlpDecode);
let suffix_length = suffix_len;
let content_len : range(0, transaction_length_bound + 35) = content_length + suffix_length;
let prefix_len = rlp_length_prefix_len(content_len);
let type_len : range(0, 1) =
if tb == 0x00 then 0 else 1;
let preimage_len : range(0, transaction_length_bound + 69) = type_len + prefix_len + content_len;
let encoder = rlp_encoder_begin(preimage_len);
if tb != 0x00 then {
scratch_push_byte(tb)
};
rlp_write_list_prefix(content_len);
scratch_push_slice(content_src);
if eip155 then {
rlp_write_uint_word(chain_id);
scratch_push_byte(0x80);
scratch_push_byte(0x80)
};
let preimage = rlp_encoder_finish(encoder);
let signing_hash = keccak256(preimage);
rlp_encoder_rewind(encoder);
signing_hash
}Converts a word to its low 160-bit address in canonical byte order.
function word_to_address(value : word) -> address = {
let zero_bytes = vector_init(20, 0x00);
var result : address = Address(zero_bytes);
result[0] = get_slice_int(8, value, 152);
result[1] = get_slice_int(8, value, 144);
result[2] = get_slice_int(8, value, 136);
result[3] = get_slice_int(8, value, 128);
result[4] = get_slice_int(8, value, 120);
result[5] = get_slice_int(8, value, 112);
result[6] = get_slice_int(8, value, 104);
result[7] = get_slice_int(8, value, 96);
result[8] = get_slice_int(8, value, 88);
result[9] = get_slice_int(8, value, 80);
result[10] = get_slice_int(8, value, 72);
result[11] = get_slice_int(8, value, 64);
result[12] = get_slice_int(8, value, 56);
result[13] = get_slice_int(8, value, 48);
result[14] = get_slice_int(8, value, 40);
result[15] = get_slice_int(8, value, 32);
result[16] = get_slice_int(8, value, 24);
result[17] = get_slice_int(8, value, 16);
result[18] = get_slice_int(8, value, 8);
result[19] = get_slice_int(8, value, 0);
result
}let EMPTY_ACCESS_LIST_REF : AccessListRef = struct {
encoded = EMPTY_STATELESS_INPUT_SLICE,
address_count = 0,
slot_count = 0,
}let EMPTY_AUTHORIZATION_LIST_REF : AuthorizationListRef = authorization_list_ref(EMPTY_STATELESS_INPUT_SLICE, 0)let EMPTY_BLOB_HASHES : BlobHashesFields(blob_schedule_inactive_count) = struct {
bytes = EMPTY_STATELESS_INPUT_SLICE,
count = 0,
} :
BlobHashesFields(blob_schedule_inactive_count)let ZERO_WORD : word = word_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)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)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 decoded transaction. Covers the EIP-2718 typed envelopes 0–4: legacy, EIP-2930 (access list), EIP-1559 (fee market), EIP-4844 (blob), and EIP-7702 (set code); the type-specific fields are validity-relevant per their EIP.
struct TransactionFields('blob_limit : Int), transaction_blob_limit_value('blob_limit) = {
/* EIP-2718 envelope type (the discriminant) */
tx_type : TxType,
sender : address, nonce : word,
/* typed-envelope chain id; 0 for legacy txs */
chain_id : chain_identifier,
gas_limit : transaction_gas, is_create : bool, recipient : address, value : word,
/* the EIP-2718 envelope span this tx decoded from
(the transactions-trie leaf value) */
raw : StatelessInputSlice,
/* calldata / creation initcode as a host byte source
(normally a span of the stateless input) */
input_src : TransactionInputSlice,
/* source-backed EIP-2930 access-list entries */
access_list : AccessListRef,
/* EIP-1559 max_fee_per_gas (cap, for validity) */
max_fee : word,
/* EIP-4844 max_fee_per_blob_gas (cap, for validity) */
max_blob_fee : word,
/* EIP-1559 max_priority_fee_per_gas (cap, for validity) */
max_priority_fee : word,
/* source-backed EIP-7702 set-code authorization tuples */
authorizations : AuthorizationListRef,
/* source-backed EIP-4844 BLOBHASH operands */
blob_hashes : BlobHashesFields('blob_limit),
/* witnessed sender public key (0x04 ++ X ++ Y span); NOT trusted -- its
derived address must equal the signer recovered at execution */
pubkey : StatelessInputSlice,
/* keccak of the signing preimage (EIP-155 / EIP-2718 domain applied),
computed structurally at decode */
signing_hash : hash,
/* v (legacy, EIP-155-bearing) / y_parity (typed) */
sig_v : word,
sig_r : word,
sig_s : word
}A byte span contained by one SSZ transaction envelope. This structural bound is independent of fork-specific calldata and initcode limits.
type TransactionInputSlice = {
'off 'len,
source_valid_range('off, 'len) & 0 <= 'len & 'len <= transaction_length_bound.
StatelessInputSliceFields('off, 'len)
}The EIP-2718 envelope type: the single transaction discriminant. Its closed semantic descriptor below derives fork and feature requirements; transactions do not store redundant boolean flags.
enum TxType = {
/* type 0: pre-EIP-2718 RLP list */
LegacyTx,
/* type 1: EIP-2930 access list */
AccessListTx,
/* type 2: EIP-1559 fee market */
FeeMarketTx,
/* type 3: EIP-4844 blob */
BlobTx,
/* type 4: EIP-7702 set code */
SetCodeTx,
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)Named blob-schedule constants retained by the profile domains below.
type blob_schedule_inactive_count : Int = 0Common 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_boundfunction decode_access_list_tx¶
Decodes the payload fields of an EIP-2930 transaction.
function decode_access_list_tx forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields(blob_schedule_inactive_count)
) = {
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let gp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gp_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let al_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, al_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let gp = rlp_decode_u256(gp_f);
let access_list = decode_access_list(al_f);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(chain_f, v_f);
let signing_hash = tx_signing_hash(AccessListTx, signing_span, v);
struct {
tx_type = AccessListTx,
sender = sender,
raw = tx,
nonce = rlp_decode_u256(nonce_f),
chain_id = rlp_decode_uint64(chain_f),
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = access_list,
max_fee = gp,
max_blob_fee = ZERO_WORD,
max_priority_fee = gp,
authorizations = EMPTY_AUTHORIZATION_LIST_REF,
blob_hashes = EMPTY_BLOB_HASHES,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}Decodes an EIP-2930 access list — RLP [[address, [slot, …]], …] —
without materializing its entries.
function decode_access_list 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)) -> (
AccessListRef
) = {
if f.source.len <= sizeof(transaction_length_bound) then {
let entries = rlp_decode_list(f);
let decoded = decode_access_list_entries(entries);
struct {
encoded = transaction_rlp_content(f),
address_count = decoded.address_count,
slot_count = decoded.slot_count,
}
} else {
fatal_error(RlpDecode)
}
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}Decodes transaction gas structurally. Admission against the executing block's correlated gas limits belongs to transaction validation, after the envelope has been decoded.
function rlp_decode_gas 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)) -> (
transaction_gas
) =
rlp_decode_uint64(f)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}Decodes a canonical unsigned integer field into a word; throws otherwise.
function rlp_decode_u256 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 then {
rlp_decode_word(f)
} else {
fatal_error(RlpDecode)
}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)
}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)
}
}The calldata/initcode span of the data field within the envelope. The RLP cursor existentially hides its bounded source length, so this boundary reifies the already-established transaction-envelope invariant.
function tx_input_span forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (data :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
TransactionInputSlice
) = {
let content = transaction_rlp_content(data);
if content.len <= sizeof(transaction_length_bound) then {
content
} else {
fatal_error(RlpDecode)
}
}function tx_sig_span(first, signature) = {
let start = first.source.bytes;
let stop = signature.source.bytes;
let start_offset = start;
let stop_offset = stop;
if stop_offset < start_offset then {
fatal_error(RlpDecode)
} else {
stateless_input_slice(start_offset, stop_offset - start_offset)
}
}The transaction signing-preimage hash. content_src spans the RLP of
the pre-signature fields in the witness and is copied once into the final
contiguous preimage; legacy EIP-155 transactions append
(chain_id, 0, 0), typed transactions prepend the type byte as a
domain separator (EIP-2718).
function tx_signing_hash(t : TxType, content_src : StatelessInputSlice, v : word) -> hash = {
let tb : byte = tx_envelope_type(t);
let eip155 = (tb == 0x00) & word_ule(35, v);
let chain_id =
if eip155 then legacy_sig_chain_id(v) else ZERO_WORD;
let suffix_len : range(0, 35) =
if eip155 then {
let chain_id_length = rlp_uint_word_size(chain_id);
let suffix_length = LEGACY_SIGNATURE_SUFFIX_LENGTH;
chain_id_length + suffix_length
} else {
0
};
let content_length : transaction_byte_length =
if content_src.len <= sizeof(transaction_length_bound) then content_src.len else fatal_error(RlpDecode);
let suffix_length = suffix_len;
let content_len : range(0, transaction_length_bound + 35) = content_length + suffix_length;
let prefix_len = rlp_length_prefix_len(content_len);
let type_len : range(0, 1) =
if tb == 0x00 then 0 else 1;
let preimage_len : range(0, transaction_length_bound + 69) = type_len + prefix_len + content_len;
let encoder = rlp_encoder_begin(preimage_len);
if tb != 0x00 then {
scratch_push_byte(tb)
};
rlp_write_list_prefix(content_len);
scratch_push_slice(content_src);
if eip155 then {
rlp_write_uint_word(chain_id);
scratch_push_byte(0x80);
scratch_push_byte(0x80)
};
let preimage = rlp_encoder_finish(encoder);
let signing_hash = keccak256(preimage);
rlp_encoder_rewind(encoder);
signing_hash
}Converts a word to its low 160-bit address in canonical byte order.
function word_to_address(value : word) -> address = {
let zero_bytes = vector_init(20, 0x00);
var result : address = Address(zero_bytes);
result[0] = get_slice_int(8, value, 152);
result[1] = get_slice_int(8, value, 144);
result[2] = get_slice_int(8, value, 136);
result[3] = get_slice_int(8, value, 128);
result[4] = get_slice_int(8, value, 120);
result[5] = get_slice_int(8, value, 112);
result[6] = get_slice_int(8, value, 104);
result[7] = get_slice_int(8, value, 96);
result[8] = get_slice_int(8, value, 88);
result[9] = get_slice_int(8, value, 80);
result[10] = get_slice_int(8, value, 72);
result[11] = get_slice_int(8, value, 64);
result[12] = get_slice_int(8, value, 56);
result[13] = get_slice_int(8, value, 48);
result[14] = get_slice_int(8, value, 40);
result[15] = get_slice_int(8, value, 32);
result[16] = get_slice_int(8, value, 24);
result[17] = get_slice_int(8, value, 16);
result[18] = get_slice_int(8, value, 8);
result[19] = get_slice_int(8, value, 0);
result
}let EMPTY_AUTHORIZATION_LIST_REF : AuthorizationListRef = authorization_list_ref(EMPTY_STATELESS_INPUT_SLICE, 0)let EMPTY_BLOB_HASHES : BlobHashesFields(blob_schedule_inactive_count) = struct {
bytes = EMPTY_STATELESS_INPUT_SLICE,
count = 0,
} :
BlobHashesFields(blob_schedule_inactive_count)let ZERO_WORD : word = word_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)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)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 decoded transaction. Covers the EIP-2718 typed envelopes 0–4: legacy, EIP-2930 (access list), EIP-1559 (fee market), EIP-4844 (blob), and EIP-7702 (set code); the type-specific fields are validity-relevant per their EIP.
struct TransactionFields('blob_limit : Int), transaction_blob_limit_value('blob_limit) = {
/* EIP-2718 envelope type (the discriminant) */
tx_type : TxType,
sender : address, nonce : word,
/* typed-envelope chain id; 0 for legacy txs */
chain_id : chain_identifier,
gas_limit : transaction_gas, is_create : bool, recipient : address, value : word,
/* the EIP-2718 envelope span this tx decoded from
(the transactions-trie leaf value) */
raw : StatelessInputSlice,
/* calldata / creation initcode as a host byte source
(normally a span of the stateless input) */
input_src : TransactionInputSlice,
/* source-backed EIP-2930 access-list entries */
access_list : AccessListRef,
/* EIP-1559 max_fee_per_gas (cap, for validity) */
max_fee : word,
/* EIP-4844 max_fee_per_blob_gas (cap, for validity) */
max_blob_fee : word,
/* EIP-1559 max_priority_fee_per_gas (cap, for validity) */
max_priority_fee : word,
/* source-backed EIP-7702 set-code authorization tuples */
authorizations : AuthorizationListRef,
/* source-backed EIP-4844 BLOBHASH operands */
blob_hashes : BlobHashesFields('blob_limit),
/* witnessed sender public key (0x04 ++ X ++ Y span); NOT trusted -- its
derived address must equal the signer recovered at execution */
pubkey : StatelessInputSlice,
/* keccak of the signing preimage (EIP-155 / EIP-2718 domain applied),
computed structurally at decode */
signing_hash : hash,
/* v (legacy, EIP-155-bearing) / y_parity (typed) */
sig_v : word,
sig_r : word,
sig_s : word
}A byte span contained by one SSZ transaction envelope. This structural bound is independent of fork-specific calldata and initcode limits.
type TransactionInputSlice = {
'off 'len,
source_valid_range('off, 'len) & 0 <= 'len & 'len <= transaction_length_bound.
StatelessInputSliceFields('off, 'len)
}The EIP-2718 envelope type: the single transaction discriminant. Its closed semantic descriptor below derives fork and feature requirements; transactions do not store redundant boolean flags.
enum TxType = {
/* type 0: pre-EIP-2718 RLP list */
LegacyTx,
/* type 1: EIP-2930 access list */
AccessListTx,
/* type 2: EIP-1559 fee market */
FeeMarketTx,
/* type 3: EIP-4844 blob */
BlobTx,
/* type 4: EIP-7702 set code */
SetCodeTx,
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)Named blob-schedule constants retained by the profile domains below.
type blob_schedule_inactive_count : Int = 0Common 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_boundfunction decode_fee_market_tx¶
Decodes the payload fields of an EIP-1559 transaction.
function decode_fee_market_tx forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields(blob_schedule_inactive_count)
) = {
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let mp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mp_f.source.len);
let mf_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mf_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let al_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, al_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let access_list = decode_access_list(al_f);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(chain_f, v_f);
let signing_hash = tx_signing_hash(FeeMarketTx, signing_span, v);
struct {
tx_type = FeeMarketTx,
sender = sender,
raw = tx,
nonce = rlp_decode_u256(nonce_f),
chain_id = rlp_decode_uint64(chain_f),
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = access_list,
max_fee = rlp_decode_u256(mf_f),
max_blob_fee = ZERO_WORD,
max_priority_fee = rlp_decode_u256(mp_f),
authorizations = EMPTY_AUTHORIZATION_LIST_REF,
blob_hashes = EMPTY_BLOB_HASHES,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}Decodes an EIP-2930 access list — RLP [[address, [slot, …]], …] —
without materializing its entries.
function decode_access_list 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)) -> (
AccessListRef
) = {
if f.source.len <= sizeof(transaction_length_bound) then {
let entries = rlp_decode_list(f);
let decoded = decode_access_list_entries(entries);
struct {
encoded = transaction_rlp_content(f),
address_count = decoded.address_count,
slot_count = decoded.slot_count,
}
} else {
fatal_error(RlpDecode)
}
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}Decodes transaction gas structurally. Admission against the executing block's correlated gas limits belongs to transaction validation, after the envelope has been decoded.
function rlp_decode_gas 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)) -> (
transaction_gas
) =
rlp_decode_uint64(f)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}Decodes a canonical unsigned integer field into a word; throws otherwise.
function rlp_decode_u256 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 then {
rlp_decode_word(f)
} else {
fatal_error(RlpDecode)
}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)
}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)
}
}The calldata/initcode span of the data field within the envelope. The RLP cursor existentially hides its bounded source length, so this boundary reifies the already-established transaction-envelope invariant.
function tx_input_span forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (data :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
TransactionInputSlice
) = {
let content = transaction_rlp_content(data);
if content.len <= sizeof(transaction_length_bound) then {
content
} else {
fatal_error(RlpDecode)
}
}function tx_sig_span(first, signature) = {
let start = first.source.bytes;
let stop = signature.source.bytes;
let start_offset = start;
let stop_offset = stop;
if stop_offset < start_offset then {
fatal_error(RlpDecode)
} else {
stateless_input_slice(start_offset, stop_offset - start_offset)
}
}The transaction signing-preimage hash. content_src spans the RLP of
the pre-signature fields in the witness and is copied once into the final
contiguous preimage; legacy EIP-155 transactions append
(chain_id, 0, 0), typed transactions prepend the type byte as a
domain separator (EIP-2718).
function tx_signing_hash(t : TxType, content_src : StatelessInputSlice, v : word) -> hash = {
let tb : byte = tx_envelope_type(t);
let eip155 = (tb == 0x00) & word_ule(35, v);
let chain_id =
if eip155 then legacy_sig_chain_id(v) else ZERO_WORD;
let suffix_len : range(0, 35) =
if eip155 then {
let chain_id_length = rlp_uint_word_size(chain_id);
let suffix_length = LEGACY_SIGNATURE_SUFFIX_LENGTH;
chain_id_length + suffix_length
} else {
0
};
let content_length : transaction_byte_length =
if content_src.len <= sizeof(transaction_length_bound) then content_src.len else fatal_error(RlpDecode);
let suffix_length = suffix_len;
let content_len : range(0, transaction_length_bound + 35) = content_length + suffix_length;
let prefix_len = rlp_length_prefix_len(content_len);
let type_len : range(0, 1) =
if tb == 0x00 then 0 else 1;
let preimage_len : range(0, transaction_length_bound + 69) = type_len + prefix_len + content_len;
let encoder = rlp_encoder_begin(preimage_len);
if tb != 0x00 then {
scratch_push_byte(tb)
};
rlp_write_list_prefix(content_len);
scratch_push_slice(content_src);
if eip155 then {
rlp_write_uint_word(chain_id);
scratch_push_byte(0x80);
scratch_push_byte(0x80)
};
let preimage = rlp_encoder_finish(encoder);
let signing_hash = keccak256(preimage);
rlp_encoder_rewind(encoder);
signing_hash
}Converts a word to its low 160-bit address in canonical byte order.
function word_to_address(value : word) -> address = {
let zero_bytes = vector_init(20, 0x00);
var result : address = Address(zero_bytes);
result[0] = get_slice_int(8, value, 152);
result[1] = get_slice_int(8, value, 144);
result[2] = get_slice_int(8, value, 136);
result[3] = get_slice_int(8, value, 128);
result[4] = get_slice_int(8, value, 120);
result[5] = get_slice_int(8, value, 112);
result[6] = get_slice_int(8, value, 104);
result[7] = get_slice_int(8, value, 96);
result[8] = get_slice_int(8, value, 88);
result[9] = get_slice_int(8, value, 80);
result[10] = get_slice_int(8, value, 72);
result[11] = get_slice_int(8, value, 64);
result[12] = get_slice_int(8, value, 56);
result[13] = get_slice_int(8, value, 48);
result[14] = get_slice_int(8, value, 40);
result[15] = get_slice_int(8, value, 32);
result[16] = get_slice_int(8, value, 24);
result[17] = get_slice_int(8, value, 16);
result[18] = get_slice_int(8, value, 8);
result[19] = get_slice_int(8, value, 0);
result
}let EMPTY_AUTHORIZATION_LIST_REF : AuthorizationListRef = authorization_list_ref(EMPTY_STATELESS_INPUT_SLICE, 0)let EMPTY_BLOB_HASHES : BlobHashesFields(blob_schedule_inactive_count) = struct {
bytes = EMPTY_STATELESS_INPUT_SLICE,
count = 0,
} :
BlobHashesFields(blob_schedule_inactive_count)let ZERO_WORD : word = word_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)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)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 decoded transaction. Covers the EIP-2718 typed envelopes 0–4: legacy, EIP-2930 (access list), EIP-1559 (fee market), EIP-4844 (blob), and EIP-7702 (set code); the type-specific fields are validity-relevant per their EIP.
struct TransactionFields('blob_limit : Int), transaction_blob_limit_value('blob_limit) = {
/* EIP-2718 envelope type (the discriminant) */
tx_type : TxType,
sender : address, nonce : word,
/* typed-envelope chain id; 0 for legacy txs */
chain_id : chain_identifier,
gas_limit : transaction_gas, is_create : bool, recipient : address, value : word,
/* the EIP-2718 envelope span this tx decoded from
(the transactions-trie leaf value) */
raw : StatelessInputSlice,
/* calldata / creation initcode as a host byte source
(normally a span of the stateless input) */
input_src : TransactionInputSlice,
/* source-backed EIP-2930 access-list entries */
access_list : AccessListRef,
/* EIP-1559 max_fee_per_gas (cap, for validity) */
max_fee : word,
/* EIP-4844 max_fee_per_blob_gas (cap, for validity) */
max_blob_fee : word,
/* EIP-1559 max_priority_fee_per_gas (cap, for validity) */
max_priority_fee : word,
/* source-backed EIP-7702 set-code authorization tuples */
authorizations : AuthorizationListRef,
/* source-backed EIP-4844 BLOBHASH operands */
blob_hashes : BlobHashesFields('blob_limit),
/* witnessed sender public key (0x04 ++ X ++ Y span); NOT trusted -- its
derived address must equal the signer recovered at execution */
pubkey : StatelessInputSlice,
/* keccak of the signing preimage (EIP-155 / EIP-2718 domain applied),
computed structurally at decode */
signing_hash : hash,
/* v (legacy, EIP-155-bearing) / y_parity (typed) */
sig_v : word,
sig_r : word,
sig_s : word
}A byte span contained by one SSZ transaction envelope. This structural bound is independent of fork-specific calldata and initcode limits.
type TransactionInputSlice = {
'off 'len,
source_valid_range('off, 'len) & 0 <= 'len & 'len <= transaction_length_bound.
StatelessInputSliceFields('off, 'len)
}The EIP-2718 envelope type: the single transaction discriminant. Its closed semantic descriptor below derives fork and feature requirements; transactions do not store redundant boolean flags.
enum TxType = {
/* type 0: pre-EIP-2718 RLP list */
LegacyTx,
/* type 1: EIP-2930 access list */
AccessListTx,
/* type 2: EIP-1559 fee market */
FeeMarketTx,
/* type 3: EIP-4844 blob */
BlobTx,
/* type 4: EIP-7702 set code */
SetCodeTx,
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)Named blob-schedule constants retained by the profile domains below.
type blob_schedule_inactive_count : Int = 0Common 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_boundfunction decode_blob_tx¶
Decodes the payload fields of an EIP-4844 transaction.
function decode_blob_tx forall 'source_off 'source_len 'blob_limit,
source_valid_range('source_off, 'source_len) & transaction_blob_limit_value('blob_limit). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
blob_limit : int('blob_limit),
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields('blob_limit)
) = {
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let mp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mp_f.source.len);
let mf_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mf_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let al_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, al_f.source.len);
let mbf_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mbf_f.source.len);
let bh_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, bh_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let access_list = decode_access_list(al_f);
let blob_hashes = decode_blob_hashes(bh_f, blob_limit);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(chain_f, v_f);
let signing_hash = tx_signing_hash(BlobTx, signing_span, v);
struct {
tx_type = BlobTx,
sender = sender,
raw = tx,
nonce = rlp_decode_u256(nonce_f),
chain_id = rlp_decode_uint64(chain_f),
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = access_list,
max_fee = rlp_decode_u256(mf_f),
max_blob_fee = rlp_decode_u256(mbf_f),
max_priority_fee = rlp_decode_u256(mp_f),
authorizations = EMPTY_AUTHORIZATION_LIST_REF,
blob_hashes = blob_hashes,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}Decodes an EIP-2930 access list — RLP [[address, [slot, …]], …] —
without materializing its entries.
function decode_access_list 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)) -> (
AccessListRef
) = {
if f.source.len <= sizeof(transaction_length_bound) then {
let entries = rlp_decode_list(f);
let decoded = decode_access_list_entries(entries);
struct {
encoded = transaction_rlp_content(f),
address_count = decoded.address_count,
slot_count = decoded.slot_count,
}
} else {
fatal_error(RlpDecode)
}
}Validates the canonical RLP list of bytes32 blob versioned hashes
once, then retains its encoded content as a fixed-stride source view:
each element is exactly 0xa0 followed by 32 bytes, so BLOBHASH can
load item i at 33·i + 1.
function decode_blob_hashes forall 'source_off 'source_len 'content_len 'limit,
rlp_field_ref_valid('source_off, 'source_len, 'content_len) &
transaction_blob_limit_value('limit). (
f : RlpFieldRef('source_off, 'source_len, 'content_len),
limit : int('limit),
) -> (
BlobHashesFields('limit)
) = {
let bytes = transaction_rlp_content(f);
let items = rlp_decode_list(f);
let count = decode_blob_hash_items(items, limit, 0);
struct { bytes = bytes, count = count }
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}Decodes transaction gas structurally. Admission against the executing block's correlated gas limits belongs to transaction validation, after the envelope has been decoded.
function rlp_decode_gas 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)) -> (
transaction_gas
) =
rlp_decode_uint64(f)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}Decodes a canonical unsigned integer field into a word; throws otherwise.
function rlp_decode_u256 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 then {
rlp_decode_word(f)
} else {
fatal_error(RlpDecode)
}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)
}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)
}
}The calldata/initcode span of the data field within the envelope. The RLP cursor existentially hides its bounded source length, so this boundary reifies the already-established transaction-envelope invariant.
function tx_input_span forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (data :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
TransactionInputSlice
) = {
let content = transaction_rlp_content(data);
if content.len <= sizeof(transaction_length_bound) then {
content
} else {
fatal_error(RlpDecode)
}
}function tx_sig_span(first, signature) = {
let start = first.source.bytes;
let stop = signature.source.bytes;
let start_offset = start;
let stop_offset = stop;
if stop_offset < start_offset then {
fatal_error(RlpDecode)
} else {
stateless_input_slice(start_offset, stop_offset - start_offset)
}
}The transaction signing-preimage hash. content_src spans the RLP of
the pre-signature fields in the witness and is copied once into the final
contiguous preimage; legacy EIP-155 transactions append
(chain_id, 0, 0), typed transactions prepend the type byte as a
domain separator (EIP-2718).
function tx_signing_hash(t : TxType, content_src : StatelessInputSlice, v : word) -> hash = {
let tb : byte = tx_envelope_type(t);
let eip155 = (tb == 0x00) & word_ule(35, v);
let chain_id =
if eip155 then legacy_sig_chain_id(v) else ZERO_WORD;
let suffix_len : range(0, 35) =
if eip155 then {
let chain_id_length = rlp_uint_word_size(chain_id);
let suffix_length = LEGACY_SIGNATURE_SUFFIX_LENGTH;
chain_id_length + suffix_length
} else {
0
};
let content_length : transaction_byte_length =
if content_src.len <= sizeof(transaction_length_bound) then content_src.len else fatal_error(RlpDecode);
let suffix_length = suffix_len;
let content_len : range(0, transaction_length_bound + 35) = content_length + suffix_length;
let prefix_len = rlp_length_prefix_len(content_len);
let type_len : range(0, 1) =
if tb == 0x00 then 0 else 1;
let preimage_len : range(0, transaction_length_bound + 69) = type_len + prefix_len + content_len;
let encoder = rlp_encoder_begin(preimage_len);
if tb != 0x00 then {
scratch_push_byte(tb)
};
rlp_write_list_prefix(content_len);
scratch_push_slice(content_src);
if eip155 then {
rlp_write_uint_word(chain_id);
scratch_push_byte(0x80);
scratch_push_byte(0x80)
};
let preimage = rlp_encoder_finish(encoder);
let signing_hash = keccak256(preimage);
rlp_encoder_rewind(encoder);
signing_hash
}Converts a word to its low 160-bit address in canonical byte order.
function word_to_address(value : word) -> address = {
let zero_bytes = vector_init(20, 0x00);
var result : address = Address(zero_bytes);
result[0] = get_slice_int(8, value, 152);
result[1] = get_slice_int(8, value, 144);
result[2] = get_slice_int(8, value, 136);
result[3] = get_slice_int(8, value, 128);
result[4] = get_slice_int(8, value, 120);
result[5] = get_slice_int(8, value, 112);
result[6] = get_slice_int(8, value, 104);
result[7] = get_slice_int(8, value, 96);
result[8] = get_slice_int(8, value, 88);
result[9] = get_slice_int(8, value, 80);
result[10] = get_slice_int(8, value, 72);
result[11] = get_slice_int(8, value, 64);
result[12] = get_slice_int(8, value, 56);
result[13] = get_slice_int(8, value, 48);
result[14] = get_slice_int(8, value, 40);
result[15] = get_slice_int(8, value, 32);
result[16] = get_slice_int(8, value, 24);
result[17] = get_slice_int(8, value, 16);
result[18] = get_slice_int(8, value, 8);
result[19] = get_slice_int(8, value, 0);
result
}let EMPTY_AUTHORIZATION_LIST_REF : AuthorizationListRef = authorization_list_ref(EMPTY_STATELESS_INPUT_SLICE, 0)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)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 decoded transaction. Covers the EIP-2718 typed envelopes 0–4: legacy, EIP-2930 (access list), EIP-1559 (fee market), EIP-4844 (blob), and EIP-7702 (set code); the type-specific fields are validity-relevant per their EIP.
struct TransactionFields('blob_limit : Int), transaction_blob_limit_value('blob_limit) = {
/* EIP-2718 envelope type (the discriminant) */
tx_type : TxType,
sender : address, nonce : word,
/* typed-envelope chain id; 0 for legacy txs */
chain_id : chain_identifier,
gas_limit : transaction_gas, is_create : bool, recipient : address, value : word,
/* the EIP-2718 envelope span this tx decoded from
(the transactions-trie leaf value) */
raw : StatelessInputSlice,
/* calldata / creation initcode as a host byte source
(normally a span of the stateless input) */
input_src : TransactionInputSlice,
/* source-backed EIP-2930 access-list entries */
access_list : AccessListRef,
/* EIP-1559 max_fee_per_gas (cap, for validity) */
max_fee : word,
/* EIP-4844 max_fee_per_blob_gas (cap, for validity) */
max_blob_fee : word,
/* EIP-1559 max_priority_fee_per_gas (cap, for validity) */
max_priority_fee : word,
/* source-backed EIP-7702 set-code authorization tuples */
authorizations : AuthorizationListRef,
/* source-backed EIP-4844 BLOBHASH operands */
blob_hashes : BlobHashesFields('blob_limit),
/* witnessed sender public key (0x04 ++ X ++ Y span); NOT trusted -- its
derived address must equal the signer recovered at execution */
pubkey : StatelessInputSlice,
/* keccak of the signing preimage (EIP-155 / EIP-2718 domain applied),
computed structurally at decode */
signing_hash : hash,
/* v (legacy, EIP-155-bearing) / y_parity (typed) */
sig_v : word,
sig_r : word,
sig_s : word
}A byte span contained by one SSZ transaction envelope. This structural bound is independent of fork-specific calldata and initcode limits.
type TransactionInputSlice = {
'off 'len,
source_valid_range('off, 'len) & 0 <= 'len & 'len <= transaction_length_bound.
StatelessInputSliceFields('off, 'len)
}The EIP-2718 envelope type: the single transaction discriminant. Its closed semantic descriptor below derives fork and feature requirements; transactions do not store redundant boolean flags.
enum TxType = {
/* type 0: pre-EIP-2718 RLP list */
LegacyTx,
/* type 1: EIP-2930 access list */
AccessListTx,
/* type 2: EIP-1559 fee market */
FeeMarketTx,
/* type 3: EIP-4844 blob */
BlobTx,
/* type 4: EIP-7702 set code */
SetCodeTx,
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)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_boundThe fork-selected maximum number of blobs carried by one transaction. Zero denotes a profile before blob transactions activate.
type transaction_blob_limit_value('value : Int) -> Bool =
'value == blob_schedule_inactive_count
| 'value == cancun_blob_max_count
| 'value == prague_blob_max_countfunction decode_set_code_tx¶
Decodes the payload fields of an EIP-7702 transaction.
function decode_set_code_tx forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields(blob_schedule_inactive_count)
) = {
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let mp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mp_f.source.len);
let mf_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mf_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let al_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, al_f.source.len);
let auth_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, auth_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let access_list = decode_access_list(al_f);
let authorizations = decode_auth_list(auth_f);
let decoded_nonce = rlp_decode_uint64(nonce_f);
let nonce = word_of_account_nonce(decoded_nonce);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(chain_f, v_f);
let signing_hash = tx_signing_hash(SetCodeTx, signing_span, v);
struct {
tx_type = SetCodeTx,
sender = sender,
raw = tx,
nonce = nonce,
chain_id = rlp_decode_uint64(chain_f),
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = access_list,
max_fee = rlp_decode_u256(mf_f),
max_blob_fee = ZERO_WORD,
max_priority_fee = rlp_decode_u256(mp_f),
authorizations = authorizations,
blob_hashes = EMPTY_BLOB_HASHES,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}Decodes an EIP-2930 access list — RLP [[address, [slot, …]], …] —
without materializing its entries.
function decode_access_list 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)) -> (
AccessListRef
) = {
if f.source.len <= sizeof(transaction_length_bound) then {
let entries = rlp_decode_list(f);
let decoded = decode_access_list_entries(entries);
struct {
encoded = transaction_rlp_content(f),
address_count = decoded.address_count,
slot_count = decoded.slot_count,
}
} else {
fatal_error(RlpDecode)
}
}Decodes an EIP-7702 authorization list into a validated source-backed cursor view.
function decode_auth_list 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)) -> (
AuthorizationListRef
) = {
if f.source.len <= sizeof(transaction_length_bound) then {
let content = transaction_rlp_content(f);
let tuples = rlp_decode_list(f);
let count = validate_auth_tuples(tuples, 0);
authorization_list_ref(content, count)
} else {
fatal_error(RlpDecode)
}
}function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}Decodes transaction gas structurally. Admission against the executing block's correlated gas limits belongs to transaction validation, after the envelope has been decoded.
function rlp_decode_gas 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)) -> (
transaction_gas
) =
rlp_decode_uint64(f)function rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = rlp_ref_hdr(cursor);
let (content_len as 'content_len) = content_len_value;
if cursor.len < content_off then {
fatal_error(RlpDecode)
};
if cursor.len - content_off < content_len then {
fatal_error(RlpDecode)
};
let (full_len as 'full_len) = content_off + content_len;
if (0 < full_len) & (full_len <= cursor.len) then {
let field_source = sub_slice(cursor, 0, full_len);
let field : RlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}Decodes a canonical unsigned integer field into a word; throws otherwise.
function rlp_decode_u256 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 then {
rlp_decode_word(f)
} else {
fatal_error(RlpDecode)
}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)
}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)
}
}The calldata/initcode span of the data field within the envelope. The RLP cursor existentially hides its bounded source length, so this boundary reifies the already-established transaction-envelope invariant.
function tx_input_span forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (data :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
TransactionInputSlice
) = {
let content = transaction_rlp_content(data);
if content.len <= sizeof(transaction_length_bound) then {
content
} else {
fatal_error(RlpDecode)
}
}function tx_sig_span(first, signature) = {
let start = first.source.bytes;
let stop = signature.source.bytes;
let start_offset = start;
let stop_offset = stop;
if stop_offset < start_offset then {
fatal_error(RlpDecode)
} else {
stateless_input_slice(start_offset, stop_offset - start_offset)
}
}The transaction signing-preimage hash. content_src spans the RLP of
the pre-signature fields in the witness and is copied once into the final
contiguous preimage; legacy EIP-155 transactions append
(chain_id, 0, 0), typed transactions prepend the type byte as a
domain separator (EIP-2718).
function tx_signing_hash(t : TxType, content_src : StatelessInputSlice, v : word) -> hash = {
let tb : byte = tx_envelope_type(t);
let eip155 = (tb == 0x00) & word_ule(35, v);
let chain_id =
if eip155 then legacy_sig_chain_id(v) else ZERO_WORD;
let suffix_len : range(0, 35) =
if eip155 then {
let chain_id_length = rlp_uint_word_size(chain_id);
let suffix_length = LEGACY_SIGNATURE_SUFFIX_LENGTH;
chain_id_length + suffix_length
} else {
0
};
let content_length : transaction_byte_length =
if content_src.len <= sizeof(transaction_length_bound) then content_src.len else fatal_error(RlpDecode);
let suffix_length = suffix_len;
let content_len : range(0, transaction_length_bound + 35) = content_length + suffix_length;
let prefix_len = rlp_length_prefix_len(content_len);
let type_len : range(0, 1) =
if tb == 0x00 then 0 else 1;
let preimage_len : range(0, transaction_length_bound + 69) = type_len + prefix_len + content_len;
let encoder = rlp_encoder_begin(preimage_len);
if tb != 0x00 then {
scratch_push_byte(tb)
};
rlp_write_list_prefix(content_len);
scratch_push_slice(content_src);
if eip155 then {
rlp_write_uint_word(chain_id);
scratch_push_byte(0x80);
scratch_push_byte(0x80)
};
let preimage = rlp_encoder_finish(encoder);
let signing_hash = keccak256(preimage);
rlp_encoder_rewind(encoder);
signing_hash
}Embeds an EIP-2681 account nonce in the EVM word domain.
function word_of_account_nonce(value : account_nonce) -> account_nonce = valueConverts a word to its low 160-bit address in canonical byte order.
function word_to_address(value : word) -> address = {
let zero_bytes = vector_init(20, 0x00);
var result : address = Address(zero_bytes);
result[0] = get_slice_int(8, value, 152);
result[1] = get_slice_int(8, value, 144);
result[2] = get_slice_int(8, value, 136);
result[3] = get_slice_int(8, value, 128);
result[4] = get_slice_int(8, value, 120);
result[5] = get_slice_int(8, value, 112);
result[6] = get_slice_int(8, value, 104);
result[7] = get_slice_int(8, value, 96);
result[8] = get_slice_int(8, value, 88);
result[9] = get_slice_int(8, value, 80);
result[10] = get_slice_int(8, value, 72);
result[11] = get_slice_int(8, value, 64);
result[12] = get_slice_int(8, value, 56);
result[13] = get_slice_int(8, value, 48);
result[14] = get_slice_int(8, value, 40);
result[15] = get_slice_int(8, value, 32);
result[16] = get_slice_int(8, value, 24);
result[17] = get_slice_int(8, value, 16);
result[18] = get_slice_int(8, value, 8);
result[19] = get_slice_int(8, value, 0);
result
}let EMPTY_BLOB_HASHES : BlobHashesFields(blob_schedule_inactive_count) = struct {
bytes = EMPTY_STATELESS_INPUT_SLICE,
count = 0,
} :
BlobHashesFields(blob_schedule_inactive_count)let ZERO_WORD : word = word_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)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)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 decoded transaction. Covers the EIP-2718 typed envelopes 0–4: legacy, EIP-2930 (access list), EIP-1559 (fee market), EIP-4844 (blob), and EIP-7702 (set code); the type-specific fields are validity-relevant per their EIP.
struct TransactionFields('blob_limit : Int), transaction_blob_limit_value('blob_limit) = {
/* EIP-2718 envelope type (the discriminant) */
tx_type : TxType,
sender : address, nonce : word,
/* typed-envelope chain id; 0 for legacy txs */
chain_id : chain_identifier,
gas_limit : transaction_gas, is_create : bool, recipient : address, value : word,
/* the EIP-2718 envelope span this tx decoded from
(the transactions-trie leaf value) */
raw : StatelessInputSlice,
/* calldata / creation initcode as a host byte source
(normally a span of the stateless input) */
input_src : TransactionInputSlice,
/* source-backed EIP-2930 access-list entries */
access_list : AccessListRef,
/* EIP-1559 max_fee_per_gas (cap, for validity) */
max_fee : word,
/* EIP-4844 max_fee_per_blob_gas (cap, for validity) */
max_blob_fee : word,
/* EIP-1559 max_priority_fee_per_gas (cap, for validity) */
max_priority_fee : word,
/* source-backed EIP-7702 set-code authorization tuples */
authorizations : AuthorizationListRef,
/* source-backed EIP-4844 BLOBHASH operands */
blob_hashes : BlobHashesFields('blob_limit),
/* witnessed sender public key (0x04 ++ X ++ Y span); NOT trusted -- its
derived address must equal the signer recovered at execution */
pubkey : StatelessInputSlice,
/* keccak of the signing preimage (EIP-155 / EIP-2718 domain applied),
computed structurally at decode */
signing_hash : hash,
/* v (legacy, EIP-155-bearing) / y_parity (typed) */
sig_v : word,
sig_r : word,
sig_s : word
}A byte span contained by one SSZ transaction envelope. This structural bound is independent of fork-specific calldata and initcode limits.
type TransactionInputSlice = {
'off 'len,
source_valid_range('off, 'len) & 0 <= 'len & 'len <= transaction_length_bound.
StatelessInputSliceFields('off, 'len)
}The EIP-2718 envelope type: the single transaction discriminant. Its closed semantic descriptor below derives fork and feature requirements; transactions do not store redundant boolean flags.
enum TxType = {
/* type 0: pre-EIP-2718 RLP list */
LegacyTx,
/* type 1: EIP-2930 access list */
AccessListTx,
/* type 2: EIP-1559 fee market */
FeeMarketTx,
/* type 3: EIP-4844 blob */
BlobTx,
/* type 4: EIP-7702 set code */
SetCodeTx,
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)Named blob-schedule constants retained by the profile domains below.
type blob_schedule_inactive_count : Int = 0Common 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_boundfunction rlp_decode_tx¶
function rlp_decode_tx(tx, pubkey, blob_limit) = {
let public_key_body = sub_slice(pubkey, 1, PUBLIC_KEY_BODY_LENGTH);
let public_key_hash = keccak256(public_key_body);
let public_key_word = hash_to_word(public_key_hash);
let sender = word_to_address(public_key_word);
let tx_length = tx.len;
let b0 : byte =
if tx_length == 0 then fatal_error(RlpDecode) else slice_byte(tx, 0);
let ttype : byte =
if b0[7 .. 6] == 0b11 then 0x00 else b0; /* 0xc0 = RLP list tag */
let typed = ttype != 0x00;
let payload : TransactionInputSlice =
if typed then if 1 <= tx_length then sub_slice(tx, 1, tx_length - 1) else fatal_error(RlpDecode) else tx;
let payload_input : StatelessInputSlice = payload;
let fields = rlp_node_cursor(payload_input);
let tx_type : TxType = match ttype {
0x00 => LegacyTx,
0x01 => AccessListTx,
0x02 => FeeMarketTx,
0x03 => BlobTx,
0x04 => SetCodeTx,
_ => fatal_error(RlpDecode),
};
match tx_type {
LegacyTx => {
let decoded = decode_legacy_tx(tx, pubkey, sender, fields);
pack_transaction(decoded)
},
AccessListTx => {
let decoded = decode_access_list_tx(tx, pubkey, sender, fields);
pack_transaction(decoded)
},
FeeMarketTx => {
let decoded = decode_fee_market_tx(tx, pubkey, sender, fields);
pack_transaction(decoded)
},
BlobTx => {
let decoded = decode_blob_tx(tx, pubkey, blob_limit, sender, fields);
pack_transaction(decoded)
},
SetCodeTx => {
let decoded = decode_set_code_tx(tx, pubkey, sender, fields);
pack_transaction(decoded)
},
}
}Decodes the payload fields of an EIP-2930 transaction.
function decode_access_list_tx forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields(blob_schedule_inactive_count)
) = {
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let gp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gp_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let al_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, al_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let gp = rlp_decode_u256(gp_f);
let access_list = decode_access_list(al_f);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(chain_f, v_f);
let signing_hash = tx_signing_hash(AccessListTx, signing_span, v);
struct {
tx_type = AccessListTx,
sender = sender,
raw = tx,
nonce = rlp_decode_u256(nonce_f),
chain_id = rlp_decode_uint64(chain_f),
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = access_list,
max_fee = gp,
max_blob_fee = ZERO_WORD,
max_priority_fee = gp,
authorizations = EMPTY_AUTHORIZATION_LIST_REF,
blob_hashes = EMPTY_BLOB_HASHES,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}Decodes the payload fields of an EIP-4844 transaction.
function decode_blob_tx forall 'source_off 'source_len 'blob_limit,
source_valid_range('source_off, 'source_len) & transaction_blob_limit_value('blob_limit). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
blob_limit : int('blob_limit),
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields('blob_limit)
) = {
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let mp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mp_f.source.len);
let mf_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mf_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let al_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, al_f.source.len);
let mbf_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mbf_f.source.len);
let bh_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, bh_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let access_list = decode_access_list(al_f);
let blob_hashes = decode_blob_hashes(bh_f, blob_limit);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(chain_f, v_f);
let signing_hash = tx_signing_hash(BlobTx, signing_span, v);
struct {
tx_type = BlobTx,
sender = sender,
raw = tx,
nonce = rlp_decode_u256(nonce_f),
chain_id = rlp_decode_uint64(chain_f),
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = access_list,
max_fee = rlp_decode_u256(mf_f),
max_blob_fee = rlp_decode_u256(mbf_f),
max_priority_fee = rlp_decode_u256(mp_f),
authorizations = EMPTY_AUTHORIZATION_LIST_REF,
blob_hashes = blob_hashes,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}Decodes the payload fields of an EIP-1559 transaction.
function decode_fee_market_tx forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields(blob_schedule_inactive_count)
) = {
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let mp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mp_f.source.len);
let mf_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mf_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let al_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, al_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let access_list = decode_access_list(al_f);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(chain_f, v_f);
let signing_hash = tx_signing_hash(FeeMarketTx, signing_span, v);
struct {
tx_type = FeeMarketTx,
sender = sender,
raw = tx,
nonce = rlp_decode_u256(nonce_f),
chain_id = rlp_decode_uint64(chain_f),
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = access_list,
max_fee = rlp_decode_u256(mf_f),
max_blob_fee = ZERO_WORD,
max_priority_fee = rlp_decode_u256(mp_f),
authorizations = EMPTY_AUTHORIZATION_LIST_REF,
blob_hashes = EMPTY_BLOB_HASHES,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}Decodes the payload fields of a legacy transaction. Kept separate from the envelope dispatcher so extraction backends compile each transaction shape as an independent function.
function decode_legacy_tx forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields(blob_schedule_inactive_count)
) = {
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let gp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gp_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let gp = rlp_decode_u256(gp_f);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(nonce_f, v_f);
let signing_hash = tx_signing_hash(LegacyTx, signing_span, v);
struct {
tx_type = LegacyTx,
sender = sender,
raw = tx,
nonce = rlp_decode_u256(nonce_f),
chain_id = 0,
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = EMPTY_ACCESS_LIST_REF,
max_fee = gp,
max_blob_fee = ZERO_WORD,
max_priority_fee = gp,
authorizations = EMPTY_AUTHORIZATION_LIST_REF,
blob_hashes = EMPTY_BLOB_HASHES,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}Decodes the payload fields of an EIP-7702 transaction.
function decode_set_code_tx forall 'source_off 'source_len, source_valid_range('source_off, 'source_len). (
tx : TransactionInputSlice,
pubkey : StatelessInputSlice,
sender : address,
fields : RlpCursor('source_off, 'source_len),
) -> (
TransactionFields(blob_schedule_inactive_count)
) = {
let chain_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, chain_f.source.len);
let nonce_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, nonce_f.source.len);
let mp_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mp_f.source.len);
let mf_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, mf_f.source.len);
let gas_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, gas_f.source.len);
let to_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, to_f.source.len);
let value_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, value_f.source.len);
let data_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, data_f.source.len);
let al_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, al_f.source.len);
let auth_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, auth_f.source.len);
let v_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, v_f.source.len);
let r_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, r_f.source.len);
let s_f = rlp_decode_item(fields);
let fields = rlp_cursor_advance(fields, s_f.source.len);
rlp_cursor_expect_end(fields);
let v = rlp_decode_word(v_f);
let access_list = decode_access_list(al_f);
let authorizations = decode_auth_list(auth_f);
let decoded_nonce = rlp_decode_uint64(nonce_f);
let nonce = word_of_account_nonce(decoded_nonce);
let recipient_word = rlp_decode_word(to_f);
let recipient = word_to_address(recipient_word);
let signing_span = tx_sig_span(chain_f, v_f);
let signing_hash = tx_signing_hash(SetCodeTx, signing_span, v);
struct {
tx_type = SetCodeTx,
sender = sender,
raw = tx,
nonce = nonce,
chain_id = rlp_decode_uint64(chain_f),
gas_limit = rlp_decode_gas(gas_f),
is_create = to_f.content_len == 0,
recipient = recipient,
value = rlp_decode_u256(value_f),
input_src = tx_input_span(data_f),
access_list = access_list,
max_fee = rlp_decode_u256(mf_f),
max_blob_fee = ZERO_WORD,
max_priority_fee = rlp_decode_u256(mp_f),
authorizations = authorizations,
blob_hashes = EMPTY_BLOB_HASHES,
pubkey = pubkey,
signing_hash = signing_hash,
sig_v = v,
sig_r = rlp_decode_u256(r_f),
sig_s = rlp_decode_u256(s_f),
}
}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],
)Packs a transaction whose concrete blob limit is still in scope into the existential transaction surface used by envelope dispatch.
function pack_transaction forall 'blob_limit, transaction_blob_limit_value('blob_limit). (tx :
TransactionFields('blob_limit)) -> (
Transaction
) =
txfunction rlp_decode_tx(tx, pubkey, blob_limit) = {
let public_key_body = sub_slice(pubkey, 1, PUBLIC_KEY_BODY_LENGTH);
let public_key_hash = keccak256(public_key_body);
let public_key_word = hash_to_word(public_key_hash);
let sender = word_to_address(public_key_word);
let tx_length = tx.len;
let b0 : byte =
if tx_length == 0 then fatal_error(RlpDecode) else slice_byte(tx, 0);
let ttype : byte =
if b0[7 .. 6] == 0b11 then 0x00 else b0; /* 0xc0 = RLP list tag */
let typed = ttype != 0x00;
let payload : TransactionInputSlice =
if typed then if 1 <= tx_length then sub_slice(tx, 1, tx_length - 1) else fatal_error(RlpDecode) else tx;
let payload_input : StatelessInputSlice = payload;
let fields = rlp_node_cursor(payload_input);
let tx_type : TxType = match ttype {
0x00 => LegacyTx,
0x01 => AccessListTx,
0x02 => FeeMarketTx,
0x03 => BlobTx,
0x04 => SetCodeTx,
_ => fatal_error(RlpDecode),
};
match tx_type {
LegacyTx => {
let decoded = decode_legacy_tx(tx, pubkey, sender, fields);
pack_transaction(decoded)
},
AccessListTx => {
let decoded = decode_access_list_tx(tx, pubkey, sender, fields);
pack_transaction(decoded)
},
FeeMarketTx => {
let decoded = decode_fee_market_tx(tx, pubkey, sender, fields);
pack_transaction(decoded)
},
BlobTx => {
let decoded = decode_blob_tx(tx, pubkey, blob_limit, sender, fields);
pack_transaction(decoded)
},
SetCodeTx => {
let decoded = decode_set_code_tx(tx, pubkey, sender, fields);
pack_transaction(decoded)
},
}
}A cursor over the children of a byte sequence that must be exactly one RLP list (e.g. a trie node).
function rlp_node_cursor(node : StatelessInputSlice) -> (
{'source_off 'source_len,
source_valid_range('source_off, 'source_len).
RlpCursor('source_off, 'source_len)}
) = {
if node.len == 0 then {
fatal_error(RlpDecode)
} else {
let item = rlp_single_ref(node);
rlp_decode_list(item)
}
}Converts a word to its low 160-bit address in canonical byte order.
function word_to_address(value : word) -> address = {
let zero_bytes = vector_init(20, 0x00);
var result : address = Address(zero_bytes);
result[0] = get_slice_int(8, value, 152);
result[1] = get_slice_int(8, value, 144);
result[2] = get_slice_int(8, value, 136);
result[3] = get_slice_int(8, value, 128);
result[4] = get_slice_int(8, value, 120);
result[5] = get_slice_int(8, value, 112);
result[6] = get_slice_int(8, value, 104);
result[7] = get_slice_int(8, value, 96);
result[8] = get_slice_int(8, value, 88);
result[9] = get_slice_int(8, value, 80);
result[10] = get_slice_int(8, value, 72);
result[11] = get_slice_int(8, value, 64);
result[12] = get_slice_int(8, value, 56);
result[13] = get_slice_int(8, value, 48);
result[14] = get_slice_int(8, value, 40);
result[15] = get_slice_int(8, value, 32);
result[16] = get_slice_int(8, value, 24);
result[17] = get_slice_int(8, value, 16);
result[18] = get_slice_int(8, value, 8);
result[19] = get_slice_int(8, value, 0);
result
}let PUBLIC_KEY_BODY_LENGTH : int(64) = DOUBLE_WORD_BYTE_LENGTHThe 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 byte span contained by one SSZ transaction envelope. This structural bound is independent of fork-specific calldata and initcode limits.
type TransactionInputSlice = {
'off 'len,
source_valid_range('off, 'len) & 0 <= 'len & 'len <= transaction_length_bound.
StatelessInputSliceFields('off, 'len)
}The EIP-2718 envelope type: the single transaction discriminant. Its closed semantic descriptor below derives fork and feature requirements; transactions do not store redundant boolean flags.
enum TxType = {
/* type 0: pre-EIP-2718 RLP list */
LegacyTx,
/* type 1: EIP-2930 access list */
AccessListTx,
/* type 2: EIP-1559 fee market */
FeeMarketTx,
/* type 3: EIP-4844 blob */
BlobTx,
/* type 4: EIP-7702 set code */
SetCodeTx,
}An 8-bit byte.
type byte = bits(8)