RLP decoding¶
Canonical Recursive Length Prefix framing, cursor traversal, and typed scalar decoding. Input- and scratch-backed cursors remain nominally distinct so a decoder never pays for a runtime provenance tag.
function rlp_uint64_append¶
function rlp_uint64_append(_width, prefix, next) =
prefix * 256 + unsigned(next)function rlp_uint64_append(_width, prefix, next) =
prefix * 256 + unsigned(next)converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$.
val unsigned = pure {ocaml: "uint", lem: "uint", interpreter: "uint", coq: "uint", lean: "BitVec.toNatInt", _: "sail_unsigned"}: forall ('n : Int).
bits('n) -> range(0, 2 ^ 'n - 1)function rlp_uint64_width¶
Decodes exactly width big-endian bytes into a bounded unsigned value.
function rlp_uint64_width forall 'n, 0 <= 'n <= 8. (
content : StatelessInputSlice,
width : int('n),
) -> (
range(0, 2 ^ (8 * 'n) - 1)
) =
if width == 0 then {
0
} else {
let prefix = rlp_uint64_width(content, width - 1);
let next = slice_byte(content, width - 1);
rlp_uint64_append(width, prefix, next)
}function rlp_uint64_append(_width, prefix, next) =
prefix * 256 + unsigned(next)Decodes exactly width big-endian bytes into a bounded unsigned value.
function rlp_uint64_width forall 'n, 0 <= 'n <= 8. (
content : StatelessInputSlice,
width : int('n),
) -> (
range(0, 2 ^ (8 * 'n) - 1)
) =
if width == 0 then {
0
} else {
let prefix = rlp_uint64_width(content, width - 1);
let next = slice_byte(content, width - 1);
rlp_uint64_append(width, prefix, next)
}A stateless-input range with its coordinate and length packed existentially.
type StatelessInputSlice = {
'off 'len,
stateless_input_valid_range('off, 'len).
StatelessInputSliceFields('off, 'len)
}function rlp_ref_hdr¶
Decodes the first RLP header in an exact remaining source slice:
(is_list, content_offset, content_length).
function rlp_ref_hdr(b : StatelessInputSlice) -> (bool, source_pointer, range(0, 2 ^ 64 - 1)) = {
let source_len = b.len;
if source_len == 0 then {
fatal_error(RlpDecode)
};
let first_byte = slice_byte(b, 0);
let h = unsigned(first_byte);
if h < 128 then {
(false, 0, 1)
} else if h < 184 then {
(false, 1, h - 128)
} else if h < 192 then {
let length_width : range(1, 8) = h - 183;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(false, 1 + length_width, rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
} else if h < 248 then {
(true, 1, h - 192)
} else {
let length_width : range(1, 8) = h - 247;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(true, 1 + length_width, rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
}
}function fatal_error(_reason) = exit(())Decodes exactly width big-endian bytes into a bounded unsigned value.
function rlp_uint64_width forall 'n, 0 <= 'n <= 8. (
content : StatelessInputSlice,
width : int('n),
) -> (
range(0, 2 ^ (8 * 'n) - 1)
) =
if width == 0 then {
0
} else {
let prefix = rlp_uint64_width(content, width - 1);
let next = slice_byte(content, width - 1);
rlp_uint64_append(width, prefix, next)
}converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$.
val unsigned = pure {ocaml: "uint", lem: "uint", interpreter: "uint", coq: "uint", lean: "BitVec.toNatInt", _: "sail_unsigned"}: forall ('n : Int).
bits('n) -> range(0, 2 ^ 'n - 1)The reason a block fails validation; one variant per violated block-validity rule.
enum FatalError = {
/* chain config: wrong fork / inactive activation */
InvalidConfig,
/* witness ancestor headers not contiguous */
HeaderChainBroken,
/* a transaction failed to RLP-decode */
RlpDecode,
/* a tx signature did not authenticate its sender */
InvalidSignature,
/* header.gas_limit is outside the consensus domain */
InvalidGasLimit,
/* EIP-7778: a tx exceeds the block's remaining gas */
GasUsedExceedsLimit,
/* a tx exceeds the block's remaining blob gas */
BlobGasLimitExceeded,
/* an invalid tx or a failed block-end system call */
ExecutionInvalid,
/* recomputed cumulative gas != header.gas_used */
InvalidGasUsed,
/* recomputed blob gas != header.blob_gas_used */
InvalidBlobGasUsed,
/* header.excess_blob_gas != expected */
InvalidExcessBlobGas,
/* recomputed post-state root != header.state_root */
InvalidStateRoot,
/* recomputed receipts root != header.receipts_root */
InvalidReceiptsRoot,
/* recomputed logs bloom != header.logs_bloom */
InvalidLogsBloom,
/* recomputed block hash != payload expected hash */
InvalidBlockHash,
/* header.parent_hash != authenticated parent */
InvalidParentHash,
/* EIP-7928: BAL item count > gas_limit / 2000 */
BlockAccessListTooLarge,
/* reconstructed EIP-7928 BAL bytes mismatch */
InvalidBlockAccessList,
/* reconstructed EIP-7685 request bytes mismatch */
InvalidExecutionRequests,
/* a missing/inconsistent proof node (thrown at use) */
WitnessDeficient,
/* an exact protocol integer exceeds its bounded execution representation */
NumericOverflow,
}A stateless-input range with its coordinate and length packed existentially.
type StatelessInputSlice = {
'off 'len,
stateless_input_valid_range('off, 'len).
StatelessInputSliceFields('off, 'len)
}An absolute byte position in a named source region.
type source_pointer = range(0, default_host_region_bound)function rlp_decode_list¶
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 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)
}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_item¶
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 fatal_error(_reason) = exit(())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 the first RLP header in an exact remaining source slice:
(is_list, content_offset, content_length).
function rlp_ref_hdr(b : StatelessInputSlice) -> (bool, source_pointer, range(0, 2 ^ 64 - 1)) = {
let source_len = b.len;
if source_len == 0 then {
fatal_error(RlpDecode)
};
let first_byte = slice_byte(b, 0);
let h = unsigned(first_byte);
if h < 128 then {
(false, 0, 1)
} else if h < 184 then {
(false, 1, h - 128)
} else if h < 192 then {
let length_width : range(1, 8) = h - 183;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(false, 1 + length_width, rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
} else if h < 248 then {
(true, 1, h - 192)
} else {
let length_width : range(1, 8) = h - 247;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(true, 1 + length_width, rlp_uint64_width(length_bytes, length_width))
} 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,
}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),
}function rlp_cursor_advance¶
function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function rlp_cursor_expect_end¶
function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}function fatal_error(_reason) = exit(())function rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
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 rlp_single_ref¶
function rlp_single_ref(item) = {
let item_length = item.len;
if item_length == 0 then {
fatal_error(RlpDecode)
} else {
let (is_list, content_off, content_len_value) = rlp_ref_hdr(item);
let (content_len as 'content_len) = content_len_value;
if (content_off <= item_length) & (content_len == item_length - content_off) then {
let field : RlpFieldRef('source_off, 'source_len, 'content_len) = struct {
source = item,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}
}function fatal_error(_reason) = exit(())Decodes the first RLP header in an exact remaining source slice:
(is_list, content_offset, content_length).
function rlp_ref_hdr(b : StatelessInputSlice) -> (bool, source_pointer, range(0, 2 ^ 64 - 1)) = {
let source_len = b.len;
if source_len == 0 then {
fatal_error(RlpDecode)
};
let first_byte = slice_byte(b, 0);
let h = unsigned(first_byte);
if h < 128 then {
(false, 0, 1)
} else if h < 184 then {
(false, 1, h - 128)
} else if h < 192 then {
let length_width : range(1, 8) = h - 183;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(false, 1 + length_width, rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
} else if h < 248 then {
(true, 1, h - 192)
} else {
let length_width : range(1, 8) = h - 247;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(true, 1 + length_width, rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
}
}function rlp_single_ref(item) = {
let item_length = item.len;
if item_length == 0 then {
fatal_error(RlpDecode)
} else {
let (is_list, content_off, content_len_value) = rlp_ref_hdr(item);
let (content_len as 'content_len) = content_len_value;
if (content_off <= item_length) & (content_len == item_length - content_off) then {
let field : RlpFieldRef('source_off, 'source_len, 'content_len) = struct {
source = item,
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,
}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),
}function rlp_node_cursor¶
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)
}
}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)
}function rlp_single_ref(item) = {
let item_length = item.len;
if item_length == 0 then {
fatal_error(RlpDecode)
} else {
let (is_list, content_off, content_len_value) = rlp_ref_hdr(item);
let (content_len as 'content_len) = content_len_value;
if (content_off <= item_length) & (content_len == item_length - content_off) then {
let field : RlpFieldRef('source_off, 'source_len, 'content_len) = struct {
source = item,
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,
}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)
}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_boundfunction rlp_item_content¶
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)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_lenScratch-node decoding¶
Canonical MPT construction can embed a freshly encoded child in its parent. Those sub-32-byte encodings live in scratch, so they use a separate cursor family rather than a generic source-tagged RLP cursor.
function scratch_rlp_uint64_width¶
rlp_uint64_width over a scratch-backed content slice.
function scratch_rlp_uint64_width forall 'n, 0 <= 'n <= 8. (
content : ScratchSlice,
width : int('n),
) -> (
range(0, 2 ^ (8 * 'n) - 1)
) =
if width == 0 then {
0
} else {
let prefix = scratch_rlp_uint64_width(content, width - 1);
let next = slice_byte(content, width - 1);
rlp_uint64_append(width, prefix, next)
}function rlp_uint64_append(_width, prefix, next) =
prefix * 256 + unsigned(next)rlp_uint64_width over a scratch-backed content slice.
function scratch_rlp_uint64_width forall 'n, 0 <= 'n <= 8. (
content : ScratchSlice,
width : int('n),
) -> (
range(0, 2 ^ (8 * 'n) - 1)
) =
if width == 0 then {
0
} else {
let prefix = scratch_rlp_uint64_width(content, width - 1);
let next = slice_byte(content, width - 1);
rlp_uint64_append(width, prefix, next)
}A scratch-arena range with its coordinate and length packed existentially.
type ScratchSlice = {
'off 'len,
scratch_valid_range('off, 'len).
ScratchSliceFields('off, 'len)
}function scratch_rlp_ref_hdr¶
rlp_ref_hdr over a scratch-backed source slice.
function scratch_rlp_ref_hdr(b : ScratchSlice) -> (bool, source_pointer, range(0, 2 ^ 64 - 1)) = {
let source_len = b.len;
if source_len == 0 then {
fatal_error(RlpDecode)
};
let first_byte = slice_byte(b, 0);
let h = unsigned(first_byte);
if h < 128 then {
(false, 0, 1)
} else if h < 184 then {
(false, 1, h - 128)
} else if h < 192 then {
let length_width : range(1, 8) = h - 183;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(false, 1 + length_width, scratch_rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
} else if h < 248 then {
(true, 1, h - 192)
} else {
let length_width : range(1, 8) = h - 247;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(true, 1 + length_width, scratch_rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
}
}function fatal_error(_reason) = exit(())rlp_uint64_width over a scratch-backed content slice.
function scratch_rlp_uint64_width forall 'n, 0 <= 'n <= 8. (
content : ScratchSlice,
width : int('n),
) -> (
range(0, 2 ^ (8 * 'n) - 1)
) =
if width == 0 then {
0
} else {
let prefix = scratch_rlp_uint64_width(content, width - 1);
let next = slice_byte(content, width - 1);
rlp_uint64_append(width, prefix, next)
}converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$.
val unsigned = pure {ocaml: "uint", lem: "uint", interpreter: "uint", coq: "uint", lean: "BitVec.toNatInt", _: "sail_unsigned"}: forall ('n : Int).
bits('n) -> range(0, 2 ^ 'n - 1)The reason a block fails validation; one variant per violated block-validity rule.
enum FatalError = {
/* chain config: wrong fork / inactive activation */
InvalidConfig,
/* witness ancestor headers not contiguous */
HeaderChainBroken,
/* a transaction failed to RLP-decode */
RlpDecode,
/* a tx signature did not authenticate its sender */
InvalidSignature,
/* header.gas_limit is outside the consensus domain */
InvalidGasLimit,
/* EIP-7778: a tx exceeds the block's remaining gas */
GasUsedExceedsLimit,
/* a tx exceeds the block's remaining blob gas */
BlobGasLimitExceeded,
/* an invalid tx or a failed block-end system call */
ExecutionInvalid,
/* recomputed cumulative gas != header.gas_used */
InvalidGasUsed,
/* recomputed blob gas != header.blob_gas_used */
InvalidBlobGasUsed,
/* header.excess_blob_gas != expected */
InvalidExcessBlobGas,
/* recomputed post-state root != header.state_root */
InvalidStateRoot,
/* recomputed receipts root != header.receipts_root */
InvalidReceiptsRoot,
/* recomputed logs bloom != header.logs_bloom */
InvalidLogsBloom,
/* recomputed block hash != payload expected hash */
InvalidBlockHash,
/* header.parent_hash != authenticated parent */
InvalidParentHash,
/* EIP-7928: BAL item count > gas_limit / 2000 */
BlockAccessListTooLarge,
/* reconstructed EIP-7928 BAL bytes mismatch */
InvalidBlockAccessList,
/* reconstructed EIP-7685 request bytes mismatch */
InvalidExecutionRequests,
/* a missing/inconsistent proof node (thrown at use) */
WitnessDeficient,
/* an exact protocol integer exceeds its bounded execution representation */
NumericOverflow,
}A scratch-arena range with its coordinate and length packed existentially.
type ScratchSlice = {
'off 'len,
scratch_valid_range('off, 'len).
ScratchSliceFields('off, 'len)
}An absolute byte position in a named source region.
type source_pointer = range(0, default_host_region_bound)function scratch_rlp_decode_list¶
function scratch_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 fatal_error(_reason) = exit(())function scratch_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)
}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 scratch_rlp_decode_item¶
function scratch_rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = scratch_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 : ScratchRlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}function fatal_error(_reason) = exit(())function scratch_rlp_decode_item(cursor) = {
if cursor.len == 0 then {
fatal_error(RlpDecode)
};
let (is_list, content_off, content_len_value) = scratch_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 : ScratchRlpFieldRef('source_off, 'full_len, 'content_len) = struct {
source = field_source,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}rlp_ref_hdr over a scratch-backed source slice.
function scratch_rlp_ref_hdr(b : ScratchSlice) -> (bool, source_pointer, range(0, 2 ^ 64 - 1)) = {
let source_len = b.len;
if source_len == 0 then {
fatal_error(RlpDecode)
};
let first_byte = slice_byte(b, 0);
let h = unsigned(first_byte);
if h < 128 then {
(false, 0, 1)
} else if h < 184 then {
(false, 1, h - 128)
} else if h < 192 then {
let length_width : range(1, 8) = h - 183;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(false, 1 + length_width, scratch_rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
} else if h < 248 then {
(true, 1, h - 192)
} else {
let length_width : range(1, 8) = h - 247;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(true, 1 + length_width, scratch_rlp_uint64_width(length_bytes, length_width))
} 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,
}The same RLP framing invariants over a node encoding held in the scratch arena. Keeping this nominally separate prevents decoded input fields from acquiring a runtime byte-source tag.
struct ScratchRlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : ScratchSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}function scratch_rlp_cursor_advance¶
function scratch_rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function scratch_rlp_cursor_advance(cursor, consumed) =
slice_suffix(cursor, consumed)function scratch_rlp_cursor_expect_end¶
function scratch_rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
fatal_error(RlpDecode)
}function fatal_error(_reason) = exit(())function scratch_rlp_cursor_expect_end(cursor) = {
if cursor.len == 0 then {
return ()
};
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 scratch_rlp_single_ref¶
function scratch_rlp_single_ref(item) = {
let item_length = item.len;
if item_length == 0 then {
fatal_error(RlpDecode)
} else {
let (is_list, content_off, content_len_value) = scratch_rlp_ref_hdr(item);
let (content_len as 'content_len) = content_len_value;
if (content_off <= item_length) & (content_len == item_length - content_off) then {
let field : ScratchRlpFieldRef('source_off, 'source_len, 'content_len) = struct {
source = item,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}
}function fatal_error(_reason) = exit(())rlp_ref_hdr over a scratch-backed source slice.
function scratch_rlp_ref_hdr(b : ScratchSlice) -> (bool, source_pointer, range(0, 2 ^ 64 - 1)) = {
let source_len = b.len;
if source_len == 0 then {
fatal_error(RlpDecode)
};
let first_byte = slice_byte(b, 0);
let h = unsigned(first_byte);
if h < 128 then {
(false, 0, 1)
} else if h < 184 then {
(false, 1, h - 128)
} else if h < 192 then {
let length_width : range(1, 8) = h - 183;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(false, 1 + length_width, scratch_rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
} else if h < 248 then {
(true, 1, h - 192)
} else {
let length_width : range(1, 8) = h - 247;
if length_width <= source_len - 1 then {
let length_bytes = sub_slice(b, 1, length_width);
(true, 1 + length_width, scratch_rlp_uint64_width(length_bytes, length_width))
} else {
fatal_error(RlpDecode)
}
}
}function scratch_rlp_single_ref(item) = {
let item_length = item.len;
if item_length == 0 then {
fatal_error(RlpDecode)
} else {
let (is_list, content_off, content_len_value) = scratch_rlp_ref_hdr(item);
let (content_len as 'content_len) = content_len_value;
if (content_off <= item_length) & (content_len == item_length - content_off) then {
let field : ScratchRlpFieldRef('source_off, 'source_len, 'content_len) = struct {
source = item,
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,
}The same RLP framing invariants over a node encoding held in the scratch arena. Keeping this nominally separate prevents decoded input fields from acquiring a runtime byte-source tag.
struct ScratchRlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : ScratchSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}function scratch_rlp_node_cursor¶
rlp_node_cursor over a freshly encoded scratch node.
function scratch_rlp_node_cursor(node : ScratchSlice) -> (
{'source_off 'source_len,
source_valid_range('source_off, 'source_len).
ScratchRlpCursor('source_off, 'source_len)}
) =
let item = scratch_rlp_single_ref(node) in
scratch_rlp_decode_list(item)function scratch_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 scratch_rlp_single_ref(item) = {
let item_length = item.len;
if item_length == 0 then {
fatal_error(RlpDecode)
} else {
let (is_list, content_off, content_len_value) = scratch_rlp_ref_hdr(item);
let (content_len as 'content_len) = content_len_value;
if (content_off <= item_length) & (content_len == item_length - content_off) then {
let field : ScratchRlpFieldRef('source_off, 'source_len, 'content_len) = struct {
source = item,
is_list = is_list,
content_len = content_len,
};
field
} else {
fatal_error(RlpDecode)
}
}
}A one-pass RLP cursor over a scratch-arena node encoding, nominally distinct from the stateless-input cursor.
type ScratchRlpCursor('source_off : Int, 'source_len : Int),
source_valid_range('source_off, 'source_len) =
ScratchSliceFields('source_off, 'source_len)A scratch-arena range with its coordinate and length packed existentially.
type ScratchSlice = {
'off 'len,
scratch_valid_range('off, 'len).
ScratchSliceFields('off, '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_boundfunction scratch_rlp_item_content¶
rlp_item_content for a scratch-backed field.
function scratch_rlp_item_content forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
ScratchRlpFieldRef('source_off, 'source_len, 'content_len)) -> (
ScratchSlice
) =
sub_slice(f.source, f.source.len - f.content_len, f.content_len)The same RLP framing invariants over a node encoding held in the scratch arena. Keeping this nominally separate prevents decoded input fields from acquiring a runtime byte-source tag.
struct ScratchRlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : ScratchSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}A scratch-arena range with its coordinate and length packed existentially.
type ScratchSlice = {
'off 'len,
scratch_valid_range('off, 'len).
ScratchSliceFields('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 scratch_rlp_decode_word¶
rlp_decode_word for a scratch-backed field.
function scratch_rlp_decode_word forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
ScratchRlpFieldRef('source_off, 'source_len, 'content_len)) -> (
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)
}
}function fatal_error(_reason) = exit(())let RLP_WORD_LENGTH_LIMIT : int(32) = 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,
}The same RLP framing invariants over a node encoding held in the scratch arena. Keeping this nominally separate prevents decoded input fields from acquiring a runtime byte-source tag.
struct ScratchRlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : ScratchSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}The complete containment invariant for an RLP field reference. source
is normalized to the complete encoded item. RLP content is its suffix, so
the content offset is derived as source.len - content_len.
type rlp_field_ref_valid(
'source_off : Int,
'source_len : Int,
'content_len : Int,
) -> Bool =
source_valid_range('source_off, 'source_len)
& 0 <= 'content_len
& 'content_len <= 'source_lenThe EVM 256-bit machine word (YP §9.1). A transparent range keeps the mathematical subtype relation visible: narrower non-negative ranges can be passed as words without a model-level conversion.
type word = range(0, 2 ^ 256 - 1)function rlp_ref_framing_canonical¶
Whether a field uses the unique canonical RLP framing for its payload.
function rlp_ref_framing_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) = {
let n = f.content_len;
let payload_length = n;
let full_length = f.source.len;
let full_offset = 0;
let content_offset = full_length - payload_length;
let source = f.source;
let source_length = source.len;
if full_length == 0 then {
false
} else if f.is_list then {
if n <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(n);
(full_length == payload_length + 1) & (slice_byte(f.source, 0) == add_bits(0xc0, length_byte))
} else {
let length_word = rlp_length_word(n);
let length_width = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_width);
(full_length == 1 + length_width + payload_length)
& (slice_byte(f.source, 0) == add_bits(0xf7, length_byte))
& (if full_offset < source_length
then slice_load_n(f.source, full_offset + 1, length_width) == length_word
else false)
}
} else if payload_length == 0 then {
(full_length == 1) & (slice_byte(f.source, 0) == 0x80)
} else {
let first = slice_byte(f.source, content_offset);
if (payload_length == 1) & (first[7] == bitzero) then {
(full_length == 1) & (slice_byte(f.source, 0) == first)
} else if n <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(n);
(full_length == payload_length + 1) & (slice_byte(f.source, 0) == add_bits(0x80, length_byte))
} else {
let length_word = rlp_length_word(n);
let length_width = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_width);
(full_length == 1 + length_width + payload_length)
& (slice_byte(f.source, 0) == add_bits(0xb7, length_byte))
& (if full_offset < source_length
then slice_load_n(f.source, full_offset + 1, length_width) == length_word
else false)
}
}
}val add_bits = pure {ocaml: "add_vec", interpreter: "add_vec", lem: "add_vec", coq: "add_vec", lean: "_lean_add", _: "add_bits"}: forall ('n : Int).
(bits('n), bits('n)) -> bits('n)function rlp_length_word(value) = {
word_of_nat_byte_count(value)
}function rlp_minimal_word_len(w) = {
word_byte_length(w)
}let RLP_SHORT_LENGTH_LIMIT : int(55) = 55The 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_lenA byte length or regular-layout count derived from a source region.
type source_length = range(0, default_host_region_bound)function rlp_ref_bytes_canonical¶
Whether a field is a byte string with its unique canonical RLP framing.
function rlp_ref_bytes_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) =
not_bool(f.is_list) & rlp_ref_framing_canonical(f)val not_bool = pure {coq: "negb", lean: "_lean_not", _: "not"}: forall ('p : Bool). bool('p) -> bool(not('p))Whether a field uses the unique canonical RLP framing for its payload.
function rlp_ref_framing_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) = {
let n = f.content_len;
let payload_length = n;
let full_length = f.source.len;
let full_offset = 0;
let content_offset = full_length - payload_length;
let source = f.source;
let source_length = source.len;
if full_length == 0 then {
false
} else if f.is_list then {
if n <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(n);
(full_length == payload_length + 1) & (slice_byte(f.source, 0) == add_bits(0xc0, length_byte))
} else {
let length_word = rlp_length_word(n);
let length_width = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_width);
(full_length == 1 + length_width + payload_length)
& (slice_byte(f.source, 0) == add_bits(0xf7, length_byte))
& (if full_offset < source_length
then slice_load_n(f.source, full_offset + 1, length_width) == length_word
else false)
}
} else if payload_length == 0 then {
(full_length == 1) & (slice_byte(f.source, 0) == 0x80)
} else {
let first = slice_byte(f.source, content_offset);
if (payload_length == 1) & (first[7] == bitzero) then {
(full_length == 1) & (slice_byte(f.source, 0) == first)
} else if n <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(n);
(full_length == payload_length + 1) & (slice_byte(f.source, 0) == add_bits(0x80, length_byte))
} else {
let length_word = rlp_length_word(n);
let length_width = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_width);
(full_length == 1 + length_width + payload_length)
& (slice_byte(f.source, 0) == add_bits(0xb7, length_byte))
& (if full_offset < source_length
then slice_load_n(f.source, full_offset + 1, length_width) == length_word
else false)
}
}
}The 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_lenfunction rlp_item_uint_canonical¶
Whether a field is the canonical RLP encoding of a non-negative integer: minimal big-endian content with no leading zeros and the exact matching prefix.
function rlp_item_uint_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) =
let bytes_canonical = rlp_ref_bytes_canonical(f) in
let invalid = not_bool(bytes_canonical) in
if invalid then {
false
} else {
(f.content_len == 0) | (slice_byte(f.source, f.source.len - f.content_len) != 0x00)
}val not_bool = pure {coq: "negb", lean: "_lean_not", _: "not"}: forall ('p : Bool). bool('p) -> bool(not('p))Whether a field is a byte string with its unique canonical RLP framing.
function rlp_ref_bytes_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) =
not_bool(f.is_list) & rlp_ref_framing_canonical(f)The 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_lenfunction rlp_word_valid¶
Whether a string field fits one EVM word. This is the non-throwing form used by structural validation passes that do not need the decoded value.
function rlp_word_valid forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) =
not_bool(f.is_list) & (f.content_len <= RLP_WORD_LENGTH_LIMIT)val not_bool = pure {coq: "negb", lean: "_lean_not", _: "not"}: forall ('p : Bool). bool('p) -> bool(not('p))let RLP_WORD_LENGTH_LIMIT : int(32) = WORD_BYTE_LENGTHThe 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_lenfunction rlp_u256_valid¶
Whether a field is a canonical unsigned EVM-word integer.
function rlp_u256_valid forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) = {
let canonical = rlp_item_uint_canonical(f);
canonical & (f.content_len <= RLP_WORD_LENGTH_LIMIT)
}Whether a field is the canonical RLP encoding of a non-negative integer: minimal big-endian content with no leading zeros and the exact matching prefix.
function rlp_item_uint_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) =
let bytes_canonical = rlp_ref_bytes_canonical(f) in
let invalid = not_bool(bytes_canonical) in
if invalid then {
false
} else {
(f.content_len == 0) | (slice_byte(f.source, f.source.len - f.content_len) != 0x00)
}let RLP_WORD_LENGTH_LIMIT : int(32) = WORD_BYTE_LENGTHThe 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_lenfunction rlp_uint64_valid¶
Whether a field is a canonical unsigned 64-bit integer.
function rlp_uint64_valid forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) = {
let canonical = rlp_item_uint_canonical(f);
canonical & (f.content_len <= RLP_UINT64_LENGTH_LIMIT)
}Whether a field is the canonical RLP encoding of a non-negative integer: minimal big-endian content with no leading zeros and the exact matching prefix.
function rlp_item_uint_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) =
let bytes_canonical = rlp_ref_bytes_canonical(f) in
let invalid = not_bool(bytes_canonical) in
if invalid then {
false
} else {
(f.content_len == 0) | (slice_byte(f.source, f.source.len - f.content_len) != 0x00)
}let RLP_UINT64_LENGTH_LIMIT : int(8) = EIGHT_BYTE_LENGTHThe 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_lenfunction rlp_decode_word¶
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)
}
}function fatal_error(_reason) = exit(())let RLP_WORD_LENGTH_LIMIT : int(32) = 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,
}The witness-carrying fields of a decoded RLP reference. Both the complete encoding and its content are statically contained by the source slice.
struct RlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : StatelessInputSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}The complete containment invariant for an RLP field reference. source
is normalized to the complete encoded item. RLP content is its suffix, so
the content offset is derived as source.len - content_len.
type rlp_field_ref_valid(
'source_off : Int,
'source_len : Int,
'content_len : Int,
) -> Bool =
source_valid_range('source_off, 'source_len)
& 0 <= 'content_len
& 'content_len <= 'source_lenThe EVM 256-bit machine word (YP §9.1). A transparent range keeps the mathematical subtype relation visible: narrower non-negative ranges can be passed as words without a model-level conversion.
type word = range(0, 2 ^ 256 - 1)function rlp_decode_u256¶
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)
}function fatal_error(_reason) = exit(())Decodes a string field of at most 32 bytes into a word.
function rlp_decode_word forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
word
) = {
let n = f.content_len;
if f.is_list | (RLP_WORD_LENGTH_LIMIT < n) then {
fatal_error(RlpDecode)
} else {
slice_load_n(f.source, f.source.len - n, n)
}
}Whether a field is the canonical RLP encoding of a non-negative integer: minimal big-endian content with no leading zeros and the exact matching prefix.
function rlp_item_uint_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) =
let bytes_canonical = rlp_ref_bytes_canonical(f) in
let invalid = not_bool(bytes_canonical) in
if invalid then {
false
} else {
(f.content_len == 0) | (slice_byte(f.source, f.source.len - f.content_len) != 0x00)
}The reason a block fails validation; one variant per violated block-validity rule.
enum FatalError = {
/* chain config: wrong fork / inactive activation */
InvalidConfig,
/* witness ancestor headers not contiguous */
HeaderChainBroken,
/* a transaction failed to RLP-decode */
RlpDecode,
/* a tx signature did not authenticate its sender */
InvalidSignature,
/* header.gas_limit is outside the consensus domain */
InvalidGasLimit,
/* EIP-7778: a tx exceeds the block's remaining gas */
GasUsedExceedsLimit,
/* a tx exceeds the block's remaining blob gas */
BlobGasLimitExceeded,
/* an invalid tx or a failed block-end system call */
ExecutionInvalid,
/* recomputed cumulative gas != header.gas_used */
InvalidGasUsed,
/* recomputed blob gas != header.blob_gas_used */
InvalidBlobGasUsed,
/* header.excess_blob_gas != expected */
InvalidExcessBlobGas,
/* recomputed post-state root != header.state_root */
InvalidStateRoot,
/* recomputed receipts root != header.receipts_root */
InvalidReceiptsRoot,
/* recomputed logs bloom != header.logs_bloom */
InvalidLogsBloom,
/* recomputed block hash != payload expected hash */
InvalidBlockHash,
/* header.parent_hash != authenticated parent */
InvalidParentHash,
/* EIP-7928: BAL item count > gas_limit / 2000 */
BlockAccessListTooLarge,
/* reconstructed EIP-7928 BAL bytes mismatch */
InvalidBlockAccessList,
/* reconstructed EIP-7685 request bytes mismatch */
InvalidExecutionRequests,
/* a missing/inconsistent proof node (thrown at use) */
WitnessDeficient,
/* an exact protocol integer exceeds its bounded execution representation */
NumericOverflow,
}The witness-carrying fields of a decoded RLP reference. Both the complete encoding and its content are statically contained by the source slice.
struct RlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : StatelessInputSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}The complete containment invariant for an RLP field reference. source
is normalized to the complete encoded item. RLP content is its suffix, so
the content offset is derived as source.len - content_len.
type rlp_field_ref_valid(
'source_off : Int,
'source_len : Int,
'content_len : Int,
) -> Bool =
source_valid_range('source_off, 'source_len)
& 0 <= 'content_len
& 'content_len <= 'source_lenThe EVM 256-bit machine word (YP §9.1). A transparent range keeps the mathematical subtype relation visible: narrower non-negative ranges can be passed as words without a model-level conversion.
type word = range(0, 2 ^ 256 - 1)function rlp_decode_uint64¶
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)
}function fatal_error(_reason) = exit(())val not_bool = pure {coq: "negb", lean: "_lean_not", _: "not"}: forall ('p : Bool). bool('p) -> bool(not('p))The content span of a field.
function rlp_item_content forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
StatelessInputSlice
) =
sub_slice(f.source, f.source.len - f.content_len, f.content_len)Whether a field is the canonical RLP encoding of a non-negative integer: minimal big-endian content with no leading zeros and the exact matching prefix.
function rlp_item_uint_canonical forall 'source_off 'source_len 'content_len,
rlp_field_ref_valid('source_off, 'source_len, 'content_len). (f :
RlpFieldRef('source_off, 'source_len, 'content_len)) -> (
bool
) =
let bytes_canonical = rlp_ref_bytes_canonical(f) in
let invalid = not_bool(bytes_canonical) in
if invalid then {
false
} else {
(f.content_len == 0) | (slice_byte(f.source, f.source.len - f.content_len) != 0x00)
}Decodes exactly width big-endian bytes into a bounded unsigned value.
function rlp_uint64_width forall 'n, 0 <= 'n <= 8. (
content : StatelessInputSlice,
width : int('n),
) -> (
range(0, 2 ^ (8 * 'n) - 1)
) =
if width == 0 then {
0
} else {
let prefix = rlp_uint64_width(content, width - 1);
let next = slice_byte(content, width - 1);
rlp_uint64_append(width, prefix, next)
}Remainder specialized to a non-negative dividend and positive divisor. Singleton operands determine the exact natural-number result.
val tmod_nat = pure {smt: "mod", ocaml: "modulus", interpreter: "modulus", lem: "integerMod", c: "tmod_int", cpp: "tmod_int", systemverilog: "tmod_int", coq: "Z.rem", lean: "Nat.mod", _: "tmod_int"}: forall ('n : Int) ('m : Int), ('n >= 0 & 'm >= 1).
(int('n), int('m)) -> int(mod('n, 'm))let RLP_UINT64_LENGTH_LIMIT : int(8) = EIGHT_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,
}The witness-carrying fields of a decoded RLP reference. Both the complete encoding and its content are statically contained by the source slice.
struct RlpFieldRef(
'source_off : Int,
'source_len : Int,
'content_len : Int,
),
rlp_field_ref_valid(
'source_off,
'source_len,
'content_len,
) = {
source : StatelessInputSliceFields('source_off, 'source_len),
is_list : bool,
content_len : int('content_len),
}The complete containment invariant for an RLP field reference. source
is normalized to the complete encoded item. RLP content is its suffix, so
the content offset is derived as source.len - content_len.
type rlp_field_ref_valid(
'source_off : Int,
'source_len : Int,
'content_len : Int,
) -> Bool =
source_valid_range('source_off, 'source_len)
& 0 <= 'content_len
& 'content_len <= 'source_lenAn eight-byte unsigned integer read from the stateless-input SSZ schema. This is a transport type; decoders widen or validate it into the semantic field type at the container boundary.
type ssz_uint = range(0, 2 ^ 64 - 1)function rlp_decode_bool¶
function rlp_decode_bool(field) = {
let value = rlp_decode_uint64(field);
match value {
0 => RlpOk(false),
1 => RlpOk(true),
_ => RlpInvalidValue(),
}
}function rlp_decode_bool(field) = {
let value = rlp_decode_uint64(field);
match value {
0 => RlpOk(false),
1 => RlpOk(true),
_ => RlpInvalidValue(),
}
}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)
}