Withdrawal RLP codec¶
The header-level commitments recomputed from the payload: the transactions and withdrawals tries, the EIP-7685 requests hash, and the block header hash itself.
function withdrawal_rlp¶
The RLP of one withdrawal (EIP-4895), assembled in the scratch arena.
function withdrawal_rlp(withdrawal : StatelessInputSliceLength(44)) -> ScratchSlice = {
let index = decode_ssz_uint(withdrawal, WD_INDEX);
let validator_index = decode_ssz_uint(withdrawal, WD_VALIDATOR_INDEX);
let address = sub_slice(withdrawal, WD_ADDRESS, ADDRESS_BYTE_LENGTH);
let amount = decode_ssz_uint(withdrawal, WD_AMOUNT);
let index_length = rlp_uint_size(index);
let validator_index_length = rlp_uint_size(validator_index);
let address_length = rlp_slice_size(address);
let amount_length = rlp_uint_size(amount);
let content_length = index_length + validator_index_length + address_length + amount_length;
if 48 < content_length then {
fatal_error(RlpDecode)
};
let bounded_content_length : range(0, 48) = tmod_nat(content_length, 49);
let content_len = bounded_content_length;
let encoded_length = rlp_list_size(content_len);
let encoder = rlp_encoder_begin(encoded_length);
rlp_write_list_prefix(content_len);
rlp_write_uint(index);
rlp_write_uint(validator_index);
rlp_write_slice(address);
rlp_write_uint(amount);
rlp_encoder_finish(encoder)
}function decode_ssz_uint(input, offset) = {
let byte0 = slice_byte(input, offset);
let offset1 = ssz_field_offset(offset, 1);
let byte1 = slice_byte(input, offset1);
let offset2 = ssz_field_offset(offset, 2);
let byte2 = slice_byte(input, offset2);
let offset3 = ssz_field_offset(offset, 3);
let byte3 = slice_byte(input, offset3);
let offset4 = ssz_field_offset(offset, 4);
let byte4 = slice_byte(input, offset4);
let offset5 = ssz_field_offset(offset, 5);
let byte5 = slice_byte(input, offset5);
let offset6 = ssz_field_offset(offset, 6);
let byte6 = slice_byte(input, offset6);
let offset7 = ssz_field_offset(offset, 7);
let byte7 = slice_byte(input, offset7);
unsigned(byte0)
+ unsigned(byte1)
* 2 ^ 8
+ unsigned(byte2)
* 2 ^ 16
+ unsigned(byte3)
* 2 ^ 24
+ unsigned(byte4)
* 2 ^ 32
+ unsigned(byte5)
* 2 ^ 40
+ unsigned(byte6)
* 2 ^ 48
+ unsigned(byte7)
* 2 ^ 56
}function fatal_error(_reason) = exit(())function rlp_encoder_begin(expected_len) =
struct { start = scratch_reserve(expected_len), expected_len = expected_len }Finishes an exact-size construction and retains its encoded bytes.
function rlp_encoder_finish(encoder : RlpEncoder) -> ScratchSlice = {
let encoded = scratch_finish(encoder.start);
assert(encoded.len == encoder.expected_len, "RLP encoder length");
encoded
}function rlp_list_size(content_len) = {
rlp_length_prefix_len(content_len) + content_len
}function rlp_write_list_prefix(content_len) = {
if content_len <= RLP_SHORT_LENGTH_LIMIT then {
let length_byte = rlp_length_byte(content_len);
let prefix = add_bits(0xc0, length_byte);
scratch_push_byte(prefix)
} else {
let length_word = rlp_length_word(content_len);
let length_len = rlp_minimal_word_len(length_word);
let length_byte = rlp_length_byte(length_len);
let prefix = add_bits(0xf7, length_byte);
scratch_push_byte(prefix);
scratch_push_word_be(length_word, length_len)
}
}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 ADDRESS_BYTE_LENGTH : int(20) = 20let WD_ADDRESS : int(16) = 16let WD_AMOUNT : int(36) = 36let WD_INDEX : int(0) = 0let WD_VALIDATOR_INDEX : int(8) = 8The 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)
}A stateless-input range of exactly 'required bytes.
type StatelessInputSliceLength('required : Int) = {
'off 'len,
stateless_input_valid_range('off, 'len) & 'len == 'required.
StatelessInputSliceFields('off, 'len)
}A 20-byte account address (YP ยง4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)An EIP-4895 validator index, encoded as SSZ uint64.
type validator_index = range(0, ssz_uint_bound)