Protocol quantities¶
Semantic numeric domains used outside the EVM's 256-bit word algebra. Protocol fields retain their wire bounds, structural counters carry the limits imposed by their data structures, and byte positions remain exact non-negative quantities after operand validation.
Types¶
The aliases below name the semantic role of protocol and structural quantities while preserving their mathematical values. Where the protocol or data structure supplies a bound, the alias records it explicitly.
type account_nonce_bound¶
The largest account nonce admitted by EIP-2681.
type account_nonce_bound : Int = 2 ^ 64 - 1type account_nonce¶
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 - 1type ssz_uint_bound¶
Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type block_number¶
An execution block number. Provenance: the execution-payload SSZ schema
declares block_number: uint64. The execution rules do not impose a
tighter supported-fork bound.
type block_number = range(0, ssz_uint_bound)Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type block_timestamp¶
An execution block timestamp in seconds. Provenance: the
execution-payload SSZ schema declares timestamp: uint64; no tighter
supported-fork protocol bound is applied.
type block_timestamp = range(0, ssz_uint_bound)Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type gas_per_blob_value¶
Blob gas charged per blob, 2^17 (EIP-4844).
type gas_per_blob_value : Int = 2 ^ 17type blob_schedule_inactive_count¶
Named blob-schedule constants retained by the profile domains below.
type blob_schedule_inactive_count : Int = 0type cancun_blob_target_count¶
Cancun's per-block blob target of 3 (EIP-4844).
type cancun_blob_target_count : Int = 3type prague_blob_target_count¶
Prague's per-block blob target of 6 (EIP-7691).
type prague_blob_target_count : Int = 6type bpo1_blob_target_count¶
The BPO1 per-block blob target of 10.
type bpo1_blob_target_count : Int = 10type bpo2_blob_target_count¶
The BPO2 per-block blob target of 14.
type bpo2_blob_target_count : Int = 14type cancun_blob_max_count¶
Cancun's per-block blob maximum of 6 (EIP-4844).
type cancun_blob_max_count : Int = 6type prague_blob_max_count¶
Prague's per-block blob maximum of 9 (EIP-7691).
type prague_blob_max_count : Int = 9type blob_fee_update_fraction_bound¶
Largest fee-update fraction in the supported blob schedules: BPO2's
BLOB_BASE_FEE_UPDATE_FRACTION = 11684671 (EIP-8135).
type blob_fee_update_fraction_bound : Int = 11684671type blob_fee_word_exponent_limit¶
A conservative exponent at which an EIP-4844 blob base fee can no longer
fit in the EVM's 256-bit word domain: e^256 > 2^256.
type blob_fee_word_exponent_limit : Int = 256type blob_schedule_target_value¶
Whether a value is the inactive zero or one of the supported schedules' per-block blob targets.
type blob_schedule_target_value('value : Int) -> Bool =
'value == blob_schedule_inactive_count
| 'value == cancun_blob_target_count
| 'value == prague_blob_target_count
| 'value == bpo1_blob_target_count
| 'value == bpo2_blob_target_countNamed blob-schedule constants retained by the profile domains below.
type blob_schedule_inactive_count : Int = 0The BPO1 per-block blob target of 10.
type bpo1_blob_target_count : Int = 10The BPO2 per-block blob target of 14.
type bpo2_blob_target_count : Int = 14Cancun's per-block blob target of 3 (EIP-4844).
type cancun_blob_target_count : Int = 3Prague's per-block blob target of 6 (EIP-7691).
type prague_blob_target_count : Int = 6type blob_schedule_max_value¶
Whether a value is the inactive zero or one of the supported schedules' per-block blob maxima.
type blob_schedule_max_value('value : Int) -> Bool =
'value == blob_schedule_inactive_count
| 'value == cancun_blob_max_count
| 'value == prague_blob_max_count
| 'value == bpo1_blob_max_count
| 'value == bpo2_blob_max_countNamed blob-schedule constants retained by the profile domains below.
type blob_schedule_inactive_count : Int = 0The BPO1 per-block blob maximum of 15.
type bpo1_blob_max_count : Int = 15The BPO2 per-block blob maximum of 21.
type bpo2_blob_max_count : Int = 21Cancun's per-block blob maximum of 6 (EIP-4844).
type cancun_blob_max_count : Int = 6Prague's per-block blob maximum of 9 (EIP-7691).
type prague_blob_max_count : Int = 9type blob_schedule_target_count¶
A target selected by one of the blob schedules supported by the schema. This is distinct from an observed blob count, which may be any value in its contiguous range.
type blob_schedule_target_count = {
'value,
blob_schedule_target_value('value).
int('value)
}Whether a value is the inactive zero or one of the supported schedules' per-block blob targets.
type blob_schedule_target_value('value : Int) -> Bool =
'value == blob_schedule_inactive_count
| 'value == cancun_blob_target_count
| 'value == prague_blob_target_count
| 'value == bpo1_blob_target_count
| 'value == bpo2_blob_target_counttype blob_schedule_max_count¶
A maximum selected by one of the blob schedules supported by the schema.
type blob_schedule_max_count = {
'value,
blob_schedule_max_value('value).
int('value)
}Whether a value is the inactive zero or one of the supported schedules' per-block blob maxima.
type blob_schedule_max_value('value : Int) -> Bool =
'value == blob_schedule_inactive_count
| 'value == cancun_blob_max_count
| 'value == prague_blob_max_count
| 'value == bpo1_blob_max_count
| 'value == bpo2_blob_max_counttype transaction_blob_limit_value¶
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_countNamed blob-schedule constants retained by the profile domains below.
type blob_schedule_inactive_count : Int = 0Cancun's per-block blob maximum of 6 (EIP-4844).
type cancun_blob_max_count : Int = 6Prague's per-block blob maximum of 9 (EIP-7691).
type prague_blob_max_count : Int = 9type transaction_blob_limit¶
A fork-selected per-transaction blob limit drawn from the supported schedules; zero for profiles before blob transactions activate.
type transaction_blob_limit = {
'value,
transaction_blob_limit_value('value).
int('value)
}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_counttype transaction_blob_count¶
A 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)type blob_gas_used¶
Blob gas used by one supported block. The existential count retains that
every value is exactly a multiple of GAS_PER_BLOB; profile-indexed
decoding applies the selected schedule's tighter range before values enter
this heterogeneous header domain.
type blob_gas_used = {
'count,
0 <= 'count
& 'count <= bpo2_blob_max_count.
int(gas_per_blob_value * 'count)
}The BPO2 per-block blob maximum of 21.
type bpo2_blob_max_count : Int = 21Blob gas charged per blob, 2^17 (EIP-4844).
type gas_per_blob_value : Int = 2 ^ 17type transaction_blob_gas¶
Blob gas contributed by one transaction. Profile-indexed blob-hash decoding establishes the selected limit before this derived quantity is widened to the common transaction-cost domain.
type transaction_blob_gas = {
'count,
0 <= 'count
& 'count <= prague_blob_max_count.
int(gas_per_blob_value * 'count)
}Blob gas charged per blob, 2^17 (EIP-4844).
type gas_per_blob_value : Int = 2 ^ 17Prague's per-block blob maximum of 9 (EIP-7691).
type prague_blob_max_count : Int = 9type excess_blob_gas_wire_bound¶
Wire ceiling for the EIP-4844 excess_blob_gas header field.
Provenance: both the Deneb consensus ExecutionPayload and Amsterdam's
stateless SSZ payload encode the field as uint64.
type excess_blob_gas_wire_bound : Int = ssz_uint_boundLargest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type excess_blob_gas_reachable_bound¶
Union ceiling of the fork-indexed inductive equations retained by
ProtocolProfile. The expression deliberately uses the largest admitted
denominator and block growth rather than embedding a precomputed result.
type excess_blob_gas_reachable_bound : Int =
blob_fee_word_exponent_limit * blob_fee_update_fraction_bound
+ bpo2_blob_max_count * gas_per_blob_valueLargest fee-update fraction in the supported blob schedules: BPO2's
BLOB_BASE_FEE_UPDATE_FRACTION = 11684671 (EIP-8135).
type blob_fee_update_fraction_bound : Int = 11684671A conservative exponent at which an EIP-4844 blob base fee can no longer
fit in the EVM's 256-bit word domain: e^256 > 2^256.
type blob_fee_word_exponent_limit : Int = 256The BPO2 per-block blob maximum of 21.
type bpo2_blob_max_count : Int = 21Blob gas charged per blob, 2^17 (EIP-4844).
type gas_per_blob_value : Int = 2 ^ 17type excess_blob_gas_bound¶
The supported-fork reachable accumulated excess-blob-gas value.
type excess_blob_gas_bound : Int = excess_blob_gas_reachable_boundUnion ceiling of the fork-indexed inductive equations retained by
ProtocolProfile. The expression deliberately uses the largest admitted
denominator and block growth rather than embedding a precomputed result.
type excess_blob_gas_reachable_bound : Int =
blob_fee_word_exponent_limit * blob_fee_update_fraction_bound
+ bpo2_blob_max_count * gas_per_blob_valuetype excess_blob_gas¶
The accumulated excess blob gas carried between headers (EIP-4844).
type excess_blob_gas = range(0, excess_blob_gas_bound)The supported-fork reachable accumulated excess-blob-gas value.
type excess_blob_gas_bound : Int = excess_blob_gas_reachable_boundtype blob_fee_update_fraction¶
The positive denominator governing excess-blob-gas fee adjustment.
type blob_fee_update_fraction = range(1, blob_fee_update_fraction_bound)Largest fee-update fraction in the supported blob schedules: BPO2's
BLOB_BASE_FEE_UPDATE_FRACTION = 11684671 (EIP-8135).
type blob_fee_update_fraction_bound : Int = 11684671type inactive_blob_fee_update_fraction¶
Named EIP-4844/BPO fee-update fractions.
type inactive_blob_fee_update_fraction : Int = 1type cancun_blob_fee_update_fraction¶
Cancun's BLOB_BASE_FEE_UPDATE_FRACTION (EIP-4844).
type cancun_blob_fee_update_fraction : Int = 3338477type prague_blob_fee_update_fraction¶
Prague's BLOB_BASE_FEE_UPDATE_FRACTION (EIP-7691).
type prague_blob_fee_update_fraction : Int = 5007716type bpo1_blob_fee_update_fraction¶
The BPO1 blob-fee update fraction.
type bpo1_blob_fee_update_fraction : Int = 8346193type bpo2_blob_fee_update_fraction¶
The BPO2 blob-fee update fraction (EIP-8135).
type bpo2_blob_fee_update_fraction : Int = 11684671type blob_schedule_fee_update_fraction_value¶
Whether a value is the inactive unit denominator or one of the supported schedules' fee-update fractions.
type blob_schedule_fee_update_fraction_value('value : Int) -> Bool =
'value == inactive_blob_fee_update_fraction
| 'value == cancun_blob_fee_update_fraction
| 'value == prague_blob_fee_update_fraction
| 'value == bpo1_blob_fee_update_fraction
| 'value == bpo2_blob_fee_update_fractionThe BPO1 blob-fee update fraction.
type bpo1_blob_fee_update_fraction : Int = 8346193The BPO2 blob-fee update fraction (EIP-8135).
type bpo2_blob_fee_update_fraction : Int = 11684671Cancun's BLOB_BASE_FEE_UPDATE_FRACTION (EIP-4844).
type cancun_blob_fee_update_fraction : Int = 3338477Named EIP-4844/BPO fee-update fractions.
type inactive_blob_fee_update_fraction : Int = 1Prague's BLOB_BASE_FEE_UPDATE_FRACTION (EIP-7691).
type prague_blob_fee_update_fraction : Int = 5007716type blob_schedule_fee_update_fraction¶
A fee-update denominator selected by one of the supported blob schedules. Observed arithmetic still uses the broader positive denominator domain; configuration itself can only choose these protocol constants.
type blob_schedule_fee_update_fraction = {
'value,
blob_schedule_fee_update_fraction_value('value).
int('value)
}Whether a value is the inactive unit denominator or one of the supported schedules' fee-update fractions.
type blob_schedule_fee_update_fraction_value('value : Int) -> Bool =
'value == inactive_blob_fee_update_fraction
| 'value == cancun_blob_fee_update_fraction
| 'value == prague_blob_fee_update_fraction
| 'value == bpo1_blob_fee_update_fraction
| 'value == bpo2_blob_fee_update_fractiontype pre_amsterdam_deployed_code_size_limit¶
Fork-selected limits retained in the validated protocol profile. A fork
without a stricter transaction-gas cap admits the complete SSZ uint64
block-gas domain; the concrete header limit is applied separately.
type pre_amsterdam_deployed_code_size_limit : Int = 24576type amsterdam_deployed_code_size_limit¶
Amsterdam's raised deployed-code size limit of 65,536 bytes.
type amsterdam_deployed_code_size_limit : Int = 65536type inactive_initcode_size_limit¶
The zero initcode limit for profiles before EIP-3860 activates.
type inactive_initcode_size_limit : Int = 0type pre_amsterdam_initcode_size_limit¶
The EIP-3860 initcode size limit of 49,152 bytes.
type pre_amsterdam_initcode_size_limit : Int = 49152type amsterdam_initcode_size_limit¶
Amsterdam's raised initcode size limit of 131,072 bytes.
type amsterdam_initcode_size_limit : Int = 131072type eip7825_transaction_gas_limit¶
The EIP-7825 per-transaction gas cap of 2^24.
type eip7825_transaction_gas_limit : Int = 2 ^ 24type protocol_deployed_code_size_limit_value¶
Whether a value is one of the supported deployed-code size limits.
type protocol_deployed_code_size_limit_value('value : Int) -> Bool =
'value == pre_amsterdam_deployed_code_size_limit
| 'value == amsterdam_deployed_code_size_limitAmsterdam's raised deployed-code size limit of 65,536 bytes.
type amsterdam_deployed_code_size_limit : Int = 65536Fork-selected limits retained in the validated protocol profile. A fork
without a stricter transaction-gas cap admits the complete SSZ uint64
block-gas domain; the concrete header limit is applied separately.
type pre_amsterdam_deployed_code_size_limit : Int = 24576type protocol_deployed_code_size_limit¶
The fork-selected deployed-code size limit.
type protocol_deployed_code_size_limit = {
'value,
protocol_deployed_code_size_limit_value('value).
int('value)
}Whether a value is one of the supported deployed-code size limits.
type protocol_deployed_code_size_limit_value('value : Int) -> Bool =
'value == pre_amsterdam_deployed_code_size_limit
| 'value == amsterdam_deployed_code_size_limittype protocol_initcode_size_limit_value¶
Whether a value is the inactive zero or one of the supported initcode size limits.
type protocol_initcode_size_limit_value('value : Int) -> Bool =
'value == inactive_initcode_size_limit
| 'value == pre_amsterdam_initcode_size_limit
| 'value == amsterdam_initcode_size_limitAmsterdam's raised initcode size limit of 131,072 bytes.
type amsterdam_initcode_size_limit : Int = 131072The zero initcode limit for profiles before EIP-3860 activates.
type inactive_initcode_size_limit : Int = 0The EIP-3860 initcode size limit of 49,152 bytes.
type pre_amsterdam_initcode_size_limit : Int = 49152type protocol_initcode_size_limit¶
The fork-selected initcode size limit. Zero denotes a profile before EIP-3860 activates.
type protocol_initcode_size_limit = {
'value,
protocol_initcode_size_limit_value('value).
int('value)
}Whether a value is the inactive zero or one of the supported initcode size limits.
type protocol_initcode_size_limit_value('value : Int) -> Bool =
'value == inactive_initcode_size_limit
| 'value == pre_amsterdam_initcode_size_limit
| 'value == amsterdam_initcode_size_limittype protocol_transaction_total_gas_limit_value¶
Whether a value is a supported per-transaction total-gas ceiling: the EIP-7825 cap or the unrestricted SSZ block-gas domain.
type protocol_transaction_total_gas_limit_value('value : Int) -> Bool =
'value == eip7825_transaction_gas_limit
| 'value == ssz_uint_boundThe EIP-7825 per-transaction gas cap of 2^24.
type eip7825_transaction_gas_limit : Int = 2 ^ 24Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type protocol_transaction_total_gas_limit¶
The fork-selected per-transaction total-gas ceiling.
type protocol_transaction_total_gas_limit = {
'value,
protocol_transaction_total_gas_limit_value('value).
int('value)
}Whether a value is a supported per-transaction total-gas ceiling: the EIP-7825 cap or the unrestricted SSZ block-gas domain.
type protocol_transaction_total_gas_limit_value('value : Int) -> Bool =
'value == eip7825_transaction_gas_limit
| 'value == ssz_uint_boundtype protocol_transaction_regular_gas_limit_value¶
Whether a value is a supported per-transaction regular-gas ceiling: the EIP-7825 cap or the unrestricted SSZ block-gas domain.
type protocol_transaction_regular_gas_limit_value('value : Int) -> Bool =
'value == eip7825_transaction_gas_limit
| 'value == ssz_uint_boundThe EIP-7825 per-transaction gas cap of 2^24.
type eip7825_transaction_gas_limit : Int = 2 ^ 24Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type protocol_transaction_regular_gas_limit¶
The fork-selected per-transaction regular-gas ceiling.
type protocol_transaction_regular_gas_limit = {
'value,
protocol_transaction_regular_gas_limit_value('value).
int('value)
}Whether a value is a supported per-transaction regular-gas ceiling: the EIP-7825 cap or the unrestricted SSZ block-gas domain.
type protocol_transaction_regular_gas_limit_value('value : Int) -> Bool =
'value == eip7825_transaction_gas_limit
| 'value == ssz_uint_boundtype chain_identifier_bound¶
Largest chain identifier admitted by the typed-transaction wire decoder.
type chain_identifier_bound : Int = 2 ^ 64 - 1type chain_identifier¶
A chain identifier. Typed-transaction chain identifiers and the stateless chain configuration are decoded as unsigned 64-bit integers.
type chain_identifier = range(0, chain_identifier_bound)Largest chain identifier admitted by the typed-transaction wire decoder.
type chain_identifier_bound : Int = 2 ^ 64 - 1type slot_number¶
A beacon-chain slot number. Provenance: EIP-7843 and Amsterdam's
stateless SSZ payload declare this field as uint64.
type slot_number = range(0, ssz_uint_bound)Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type withdrawal_index¶
An EIP-4895 withdrawal index, encoded as SSZ uint64.
type withdrawal_index = range(0, ssz_uint_bound)Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type validator_index¶
An EIP-4895 validator index, encoded as SSZ uint64.
type validator_index = range(0, ssz_uint_bound)Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type withdrawal_amount¶
An EIP-4895 withdrawal amount in gwei, encoded as SSZ uint64.
type withdrawal_amount = range(0, ssz_uint_bound)Largest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type ssz_uint¶
An 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)type ssz_offset¶
A container-relative offset carried by an SSZ uint32.
type ssz_offset = range(0, 2 ^ 32 - 1)type ssz_offset_index¶
An index into a table of four-byte SSZ offsets.
type ssz_offset_index = range(0, 2 ^ 30 - 1)type call_depth_limit¶
The EVM call-frame depth ceiling (Yellow Paper I_e).
type call_depth_limit : Int = 1024type frame_depth¶
The nesting depth of an execution frame.
type frame_depth = range(0, call_depth_limit)The EVM call-frame depth ceiling (Yellow Paper I_e).
type call_depth_limit : Int = 1024type operand_stack_height¶
The number of words on an operand stack.
type operand_stack_height = range(0, 1024)type stack_index¶
A zero-based index from the top of the operand stack.
type stack_index = range(0, 1023)type StackPointer¶
The operand-stack cursor for the active frame, threaded by value through
the interpreter in the state-passing convention and held in the
stack_top frame register at frame boundaries. storage is an opaque
host coordinate while height is the semantic stack height. Keeping the
height in the cursor makes stack validation independent of the host stack
representation. Optimized C refines storage to a native u256 *.
struct StackPointer = {
storage : bits(64),
height : operand_stack_height,
}The number of words on an operand stack.
type operand_stack_height = range(0, 1024)type stack_slot_count¶
The number of slots an operand-stack cursor moves in one advance or retreat.
type stack_slot_count = range(0, 1024)type stack_operation_index¶
A nonzero operand-stack position used by DUP and SWAP.
type stack_operation_index = range(1, 16)type deep_stack_index¶
The one-based deep-stack index decoded by EIP-8024 DUPN and SWAPN.
type deep_stack_index = range(17, 235)type log_topic_count¶
The number of indexed topics attached to one log.
type log_topic_count = range(0, 4)type PrecompileId¶
The closed first-order selector for the precompile catalog. Availability, gas pricing, and execution are separate interpreters of this identifier so their protocol equations remain explicit without function-valued records.
enum PrecompileId = {
/* the closed sentinel: the address is not a precompiled contract */
NotPrecompile,
/* addresses 0x01-0x04: the original Frontier precompiles */
Ecrecover,
Sha256,
Ripemd160,
Identity,
/* address 0x05: EIP-198 modular exponentiation */
Modexp,
/* addresses 0x06-0x08: the EIP-196/EIP-197 BN254 curve precompiles */
Bn254Add,
Bn254Mul,
Bn254Pairing,
/* address 0x09: EIP-152 BLAKE2 compression */
Blake2f,
/* address 0x0a: EIP-4844 KZG point evaluation */
KzgPointEvaluation,
/* addresses 0x0b-0x11: the EIP-2537 BLS12-381 precompiles */
BlsG1Add,
BlsG1Msm,
BlsG2Add,
BlsG2Msm,
BlsPairing,
BlsMapFpToG1,
BlsMapFp2ToG2,
/* address 0x100: EIP-7951 secp256r1 signature verification */
P256Verify,
}type precompile_id¶
The quantity alias carried by the precompile interpreters for the closed selector above.
type precompile_id = PrecompileIdThe closed first-order selector for the precompile catalog. Availability, gas pricing, and execution are separate interpreters of this identifier so their protocol equations remain explicit without function-valued records.
enum PrecompileId = {
/* the closed sentinel: the address is not a precompiled contract */
NotPrecompile,
/* addresses 0x01-0x04: the original Frontier precompiles */
Ecrecover,
Sha256,
Ripemd160,
Identity,
/* address 0x05: EIP-198 modular exponentiation */
Modexp,
/* addresses 0x06-0x08: the EIP-196/EIP-197 BN254 curve precompiles */
Bn254Add,
Bn254Mul,
Bn254Pairing,
/* address 0x09: EIP-152 BLAKE2 compression */
Blake2f,
/* address 0x0a: EIP-4844 KZG point evaluation */
KzgPointEvaluation,
/* addresses 0x0b-0x11: the EIP-2537 BLS12-381 precompiles */
BlsG1Add,
BlsG1Msm,
BlsG2Add,
BlsG2Msm,
BlsPairing,
BlsMapFpToG1,
BlsMapFp2ToG2,
/* address 0x100: EIP-7951 secp256r1 signature verification */
P256Verify,
}type blake2_rounds¶
The round count supplied to the BLAKE2 compression precompile.
type blake2_rounds = range(0, 2 ^ 32 - 1)type bls_discount¶
A fixed-point discount factor used by BLS precompile pricing.
type bls_discount = range(0, 2 ^ 16 - 1)type ancestor_hash_count¶
The number of authenticated ancestor hashes available to BLOCKHASH.
type ancestor_hash_count = range(0, 256)type ancestor_index¶
An index into the 256 most recent ancestor block hashes.
type ancestor_index = range(0, 255)function word_of_account_nonce¶
Embeds an EIP-2681 account nonce in the EVM word domain.
function word_of_account_nonce(value : account_nonce) -> account_nonce = valueAn account transaction-count nonce (EIP-2681).
type account_nonce = range(0, account_nonce_bound)function word_of_withdrawal_amount¶
Embeds an EIP-4895 withdrawal amount in the EVM word domain.
function word_of_withdrawal_amount(value : withdrawal_amount) -> withdrawal_amount = valueAn EIP-4895 withdrawal amount in gwei, encoded as SSZ uint64.
type withdrawal_amount = range(0, ssz_uint_bound)function word_of_slot_number¶
Embeds an EIP-7843 slot number in the EVM word domain.
function word_of_slot_number(value : slot_number) -> slot_number = valueA beacon-chain slot number. Provenance: EIP-7843 and Amsterdam's
stateless SSZ payload declare this field as uint64.
type slot_number = range(0, ssz_uint_bound)function word_of_block_number¶
Embeds the SSZ-bounded block number in the EVM word domain. The uint64 schema proof makes a runtime 256-bit range check unnecessary.
function word_of_block_number(value : block_number) -> block_number = valueAn execution block number. Provenance: the execution-payload SSZ schema
declares block_number: uint64. The execution rules do not impose a
tighter supported-fork bound.
type block_number = range(0, ssz_uint_bound)function word_of_block_timestamp¶
Embeds the SSZ-bounded block timestamp in the EVM word domain. The uint64 schema proof makes a runtime 256-bit range check unnecessary.
function word_of_block_timestamp(value : block_timestamp) -> block_timestamp = valueAn execution block timestamp in seconds. Provenance: the
execution-payload SSZ schema declares timestamp: uint64; no tighter
supported-fork protocol bound is applied.
type block_timestamp = range(0, ssz_uint_bound)function word_of_chain_identifier¶
Converts a chain identifier to the value exposed by CHAINID.
function word_of_chain_identifier(value : chain_identifier) -> chain_identifier = valueA chain identifier. Typed-transaction chain identifiers and the stateless chain configuration are decoded as unsigned 64-bit integers.
type chain_identifier = range(0, chain_identifier_bound)type default_host_region_bound¶
Default capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type stateless_input_region_bound¶
Immutable stateless-input envelope capacity.
type stateless_input_region_bound : Int = default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type scratch_region_bound¶
Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type memory_region_bound¶
Shared per-frame EVM-memory arena capacity.
type memory_region_bound : Int = default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type code_region_bound¶
Content-addressed executable-code arena capacity.
type code_region_bound : Int = default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type log_data_region_bound¶
Retained transaction-log data arena capacity.
type log_data_region_bound : Int = default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type output_region_bound¶
Guest output-buffer capacity.
type output_region_bound : Int = default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type host_valid_range¶
Whether an offset/length pair is representable by a generic host interface. Region-bearing values use the more specific predicates below.
type host_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type source_valid_range¶
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_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type stateless_input_valid_range¶
Whether an offset/length pair is contained by the immutable stateless-input envelope.
type stateless_input_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= stateless_input_region_boundImmutable stateless-input envelope capacity.
type stateless_input_region_bound : Int = default_host_region_boundtype scratch_valid_range¶
Whether an offset/length pair is contained by the executor scratch arena.
type scratch_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= scratch_region_boundExecutor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundtype memory_region_valid_range¶
Whether an offset/length pair is contained by the shared EVM-memory arena.
type memory_region_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= memory_region_boundShared per-frame EVM-memory arena capacity.
type memory_region_bound : Int = default_host_region_boundtype code_region_valid_range¶
Whether an offset/length pair is contained by the executable-code arena.
type code_region_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= code_region_boundContent-addressed executable-code arena capacity.
type code_region_bound : Int = default_host_region_boundtype log_data_valid_range¶
Whether an offset/length pair is contained by retained log-data storage.
type log_data_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= log_data_region_boundRetained transaction-log data arena capacity.
type log_data_region_bound : Int = default_host_region_boundtype output_region_valid_range¶
Whether an offset/length pair is contained by the guest output region.
type output_region_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= output_region_boundGuest output-buffer capacity.
type output_region_bound : Int = default_host_region_boundtype host_valid_access¶
Whether one host byte quantity is representable. Unlike
host_valid_range, this does not assert that two quantities can be added
without overflow.
type host_valid_access('value : Int) -> Bool =
0 <= 'value & 'value <= default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type source_valid_length¶
Whether one relative source coordinate is representable.
type source_valid_length('value : Int) -> Bool =
0 <= 'value & 'value <= default_host_region_boundDefault capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type host_access¶
A position representable by a generic host byte-store interface.
type host_access = range(0, default_host_region_bound)Default capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type source_pointer¶
An absolute byte position in a named source region.
type source_pointer = range(0, default_host_region_bound)Default capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type source_length¶
A byte length or regular-layout count derived from a source region.
type source_length = range(0, default_host_region_bound)Default capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type stateless_input_pointer¶
A coordinate in the immutable stateless-input envelope.
type stateless_input_pointer = range(0, stateless_input_region_bound)Immutable stateless-input envelope capacity.
type stateless_input_region_bound : Int = default_host_region_boundtype stateless_input_length¶
A length in the immutable stateless-input envelope.
type stateless_input_length = range(0, stateless_input_region_bound)Immutable stateless-input envelope capacity.
type stateless_input_region_bound : Int = default_host_region_boundtype scratch_pointer¶
A coordinate in the executor scratch arena.
type scratch_pointer = range(0, scratch_region_bound)Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundtype scratch_length¶
A length in the executor scratch arena.
type scratch_length = range(0, scratch_region_bound)Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundtype log_data_pointer¶
A coordinate in retained log-data storage.
type log_data_pointer = range(0, log_data_region_bound)Retained transaction-log data arena capacity.
type log_data_region_bound : Int = default_host_region_boundtype log_data_length¶
A length in retained log-data storage.
type log_data_length = range(0, log_data_region_bound)A length in retained log-data storage.
type log_data_length = range(0, log_data_region_bound)Retained transaction-log data arena capacity.
type log_data_region_bound : Int = default_host_region_boundtype output_pointer¶
A coordinate in the guest output region.
type output_pointer = range(0, output_region_bound)Guest output-buffer capacity.
type output_region_bound : Int = default_host_region_boundtype output_length¶
A length in the guest output region.
type output_length = range(0, output_region_bound)Guest output-buffer capacity.
type output_region_bound : Int = default_host_region_boundtype calldata_pointer¶
A relative coordinate in calldata. Calldata may borrow either immutable stateless input or the active EVM-memory frame, so this is the semantic boundary for that explicit sum type rather than a generic host quantity.
type calldata_pointer = range(0, default_host_region_bound)Default capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type calldata_length¶
A byte length in calldata, independent of which calldata variant owns the bytes.
type calldata_length = range(0, default_host_region_bound)Default capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type word_byte_count¶
The number of bytes loaded into one EVM word.
type word_byte_count = range(0, 32)type journal_cursor¶
A cursor into a transaction-local journal-owned worklist.
type journal_cursor = range(0, default_host_region_bound)Default capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type storage_generation¶
The monotonically increasing storage incarnation owned by an account. Generation zero is reserved for the absence of a generation.
type storage_generation = range(0, default_host_region_bound)Default capacity of an implementation-owned byte arena.
type default_host_region_bound : Int = 2 ^ 32 - 1type memory_base¶
An absolute byte position in the shared EVM-memory arena.
type memory_base = range(0, memory_region_bound)Shared per-frame EVM-memory arena capacity.
type memory_region_bound : Int = default_host_region_boundtype memory_length¶
A materialized length or allocation size in the EVM-memory arena.
type memory_length = range(0, memory_region_bound)Shared per-frame EVM-memory arena capacity.
type memory_region_bound : Int = default_host_region_boundtype memory_height¶
The active EVM frame's exact relative byte high-water mark. It is carried
beside the frame's absolute memory_base; the host retains no hidden
frame coordinate or lifecycle state.
type memory_height = memory_lengthA materialized length or allocation size in the EVM-memory arena.
type memory_length = range(0, memory_region_bound)type memory_expansion_proof_gas_ceiling¶
Largest possible initial/live gas value from the SSZ-backed block-gas domain. Fork and header limits may make this ceiling smaller; this union ceiling is sufficient to prove one representation valid for every supported profile. Runtime affordability continues to use remaining gas.
type memory_expansion_proof_gas_ceiling : Int = ssz_uint_boundLargest value represented by an SSZ uint64. This is a wire-schema
constraint, sourced from the consensus ExecutionPayload container and
the Amsterdam SszExecutionPayload, rather than an implementation word
size.
type ssz_uint_bound : Int = 2 ^ 64 - 1type memory_unaffordable_word_threshold¶
First memory word count whose quadratic Yellow Paper charge alone exceeds
memory_expansion_proof_gas_ceiling:
(2^37)^2 / 512 = 2^65 > 2^64 - 1. This is a derived proof threshold,
not a runtime memory or host-allocation limit.
type memory_unaffordable_word_threshold : Int = 2 ^ 37type memory_affordable_word_bound¶
Largest whole-word endpoint which can precede that threshold.
type memory_affordable_word_bound : Int =
memory_unaffordable_word_threshold - 1First memory word count whose quadratic Yellow Paper charge alone exceeds
memory_expansion_proof_gas_ceiling:
(2^37)^2 / 512 = 2^65 > 2^64 - 1. This is a derived proof threshold,
not a runtime memory or host-allocation limit.
type memory_unaffordable_word_threshold : Int = 2 ^ 37type memory_affordable_byte_bound¶
Largest byte endpoint retained by optimized expansion planning after the
maximum-gas proof. Each attempted expansion is still checked against its
exact live gas_remaining.
type memory_affordable_byte_bound : Int =
32 * memory_affordable_word_boundLargest whole-word endpoint which can precede that threshold.
type memory_affordable_word_bound : Int =
memory_unaffordable_word_threshold - 1type memory_region_word_bound¶
Largest word count representable by the current EVM-memory region.
type memory_region_word_bound : Int = 2 ^ 27type memory_cost_input¶
Whether a word count may be presented to the cumulative memory-cost equation. This follows from the independently configured host-region boundary; the exact live-gas check remains the protocol affordability rule.
type memory_cost_input('words : Int) -> Bool =
0 <= 'wordstype memory_valid_range¶
The invariant carried by every canonical EVM memory range.
type memory_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= memory_region_boundShared per-frame EVM-memory arena capacity.
type memory_region_bound : Int = default_host_region_boundtype memory_expansion_endpoint¶
A memory endpoint which may be presented to the expansion-cost equation. The canonical specification admits every mathematical byte position; executable splices may strengthen this representation boundary after proving that every excluded endpoint is unaffordable.
type memory_expansion_endpoint('required : Int) -> Bool =
0 <= 'requiredtype memory_access_relation¶
Relates a canonical memory operand to its exclusive endpoint. A zero-size operand accesses no memory, so both its retained range and endpoint are canonicalized to zero.
type memory_access_relation(
'off : Int,
'len : Int,
'required : Int,
) -> Bool =
memory_valid_range('off, 'len)
& memory_expansion_endpoint('required)
& (
('len == 0 & 'off == 0 & 'required == 0)
| (0 < 'len & 'required == 'off + 'len)
)A memory endpoint which may be presented to the expansion-cost equation. The canonical specification admits every mathematical byte position; executable splices may strengthen this representation boundary after proving that every excluded endpoint is unaffordable.
type memory_expansion_endpoint('required : Int) -> Bool =
0 <= 'requiredThe invariant carried by every canonical EVM memory range.
type memory_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= memory_region_boundtype MemoryRangeFields¶
The indexed fields of an EVM memory range.
struct MemoryRangeFields('off : Int, 'len : Int), memory_valid_range('off, 'len) = {
off : int('off),
len : int('len),
}The invariant carried by every canonical EVM memory range.
type memory_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= memory_region_boundtype MemoryRange¶
A memory range retaining its offset, length, and containment proof.
type MemoryRange = {
'off 'len,
memory_valid_range('off, 'len). MemoryRangeFields('off, 'len)
}The indexed fields of an EVM memory range.
struct MemoryRangeFields('off : Int, 'len : Int), memory_valid_range('off, 'len) = {
off : int('off),
len : int('len),
}The invariant carried by every canonical EVM memory range.
type memory_valid_range('off : Int, 'len : Int) -> Bool =
0 <= 'off & 0 <= 'len & 'off + 'len <= memory_region_boundtype MemoryAccessFields¶
One logical EVM memory operand together with the exact endpoint which contributes to the shared expansion plan.
struct MemoryAccessFields('off : Int, 'len : Int, 'required : Int),
memory_access_relation('off, 'len, 'required) = {
range : MemoryRangeFields('off, 'len),
requested_height : int('required),
}The indexed fields of an EVM memory range.
struct MemoryRangeFields('off : Int, 'len : Int), memory_valid_range('off, 'len) = {
off : int('off),
len : int('len),
}Relates a canonical memory operand to its exclusive endpoint. A zero-size operand accesses no memory, so both its retained range and endpoint are canonicalized to zero.
type memory_access_relation(
'off : Int,
'len : Int,
'required : Int,
) -> Bool =
memory_valid_range('off, 'len)
& memory_expansion_endpoint('required)
& (
('len == 0 & 'off == 0 & 'required == 0)
| (0 < 'len & 'required == 'off + 'len)
)type MemoryAccess¶
A memory operand retaining its range/endpoint relationship existentially.
type MemoryAccess = {
'off 'len 'required,
memory_access_relation('off, 'len, 'required).
MemoryAccessFields('off, 'len, 'required)
}One logical EVM memory operand together with the exact endpoint which contributes to the shared expansion plan.
struct MemoryAccessFields('off : Int, 'len : Int, 'required : Int),
memory_access_relation('off, 'len, 'required) = {
range : MemoryRangeFields('off, 'len),
requested_height : int('required),
}Relates a canonical memory operand to its exclusive endpoint. A zero-size operand accesses no memory, so both its retained range and endpoint are canonicalized to zero.
type memory_access_relation(
'off : Int,
'len : Int,
'required : Int,
) -> Bool =
memory_valid_range('off, 'len)
& memory_expansion_endpoint('required)
& (
('len == 0 & 'off == 0 & 'required == 0)
| (0 < 'len & 'required == 'off + 'len)
)function memory_range¶
function memory_range(off, len) = struct { off = off, len = len }function memory_range(off, len) = struct { off = off, len = len }let EMPTY_MEMORY_RANGE¶
The canonical inactive range used for a zero-sized operand or halt.
let EMPTY_MEMORY_RANGE : MemoryRangeFields(0, 0) = memory_range(0, 0)function memory_range(off, len) = struct { off = off, len = len }The indexed fields of an EVM memory range.
struct MemoryRangeFields('off : Int, 'len : Int), memory_valid_range('off, 'len) = {
off : int('off),
len : int('len),
}let EMPTY_MEMORY_ACCESS¶
The canonical inactive memory operand.
let EMPTY_MEMORY_ACCESS : MemoryAccessFields(0, 0, 0) = struct { range = EMPTY_MEMORY_RANGE, requested_height = 0 }The canonical inactive range used for a zero-sized operand or halt.
let EMPTY_MEMORY_RANGE : MemoryRangeFields(0, 0) = memory_range(0, 0)One logical EVM memory operand together with the exact endpoint which contributes to the shared expansion plan.
struct MemoryAccessFields('off : Int, 'len : Int, 'required : Int),
memory_access_relation('off, 'len, 'required) = {
range : MemoryRangeFields('off, 'len),
requested_height : int('required),
}type code_pointer¶
An absolute byte position in the code arena.
type code_pointer = range(0, code_region_bound)Content-addressed executable-code arena capacity.
type code_region_bound : Int = default_host_region_boundtype code_length¶
A contract-code length.
type code_length = range(0, code_region_bound)Content-addressed executable-code arena capacity.
type code_region_bound : Int = default_host_region_boundtype code_valid_length¶
The representation invariant required of executable code, including enough cursor headroom for a complete PUSH32 immediate.
type code_valid_length('len : Int) -> Bool =
0 <= 'len & 'len + 32 <= code_region_boundContent-addressed executable-code arena capacity.
type code_region_bound : Int = default_host_region_boundtype code_scan_position¶
An opcode-aligned scan cursor: a code position that still carries the PUSH32 immediate headroom, so reading past the current opcode stays in the code region.
type code_scan_position = range(0, code_region_bound - 32)Content-addressed executable-code arena capacity.
type code_region_bound : Int = default_host_region_boundfunction word_of_nat_byte_count¶
function word_of_nat_byte_count(value) =
if value < 2 ^ 256 then {
u256(value)
} else {
assert(false);
WORD_ZERO
}We have special support for raising values to the power of two. Any Sail expression 2 ^ x will be compiled to this builtin.
val pow2 = pure {lean: "_lean_pow2i", _: "pow2"}: forall ('n : Int). int('n) -> int(2 ^ 'n)function u256(value) = valuefunction word_of_nat_byte_count(value) =
if value < 2 ^ 256 then {
u256(value)
} else {
assert(false);
WORD_ZERO
}let WORD_ZERO : word = word_from_bits(0x0000000000000000000000000000000000000000000000000000000000000000)function word_of_source_byte_count¶
function word_of_source_byte_count(value) = word_of_nat_byte_count(value)function word_of_nat_byte_count(value) =
if value < 2 ^ 256 then {
u256(value)
} else {
assert(false);
WORD_ZERO
}function word_of_source_byte_count(value) = word_of_nat_byte_count(value)