Scratch arena¶
Host storage for the executor's contiguous scratch byte arena. Sail owns the allocation cursor; the host only stores bytes at that explicit offset.
Non-normative
This page documents the model's host interface — internal contracts of the executable specification, not protocol rules.
val host_scratch_reserve¶
Ensures that len bytes can be appended at the current explicit arena
offset without changing the Sail-owned high-water mark.
val host_scratch_reserve = impure { c: "scratch_reserve_at" } : forall 'off 'len,
0
<= 'off
& 'off
<= scratch_region_bound
& 0
<= 'len
& 'len
<= scratch_region_bound. (int('off), int('len)) -> boolExecutor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundval host_scratch_store_byte¶
Stores one byte at an explicit arena offset.
val host_scratch_store_byte = impure { c: "scratch_store_byte" } : forall 'off,
0 <= 'off & 'off <= scratch_region_bound. (
int('off),
byte,
) -> ScratchSliceLength('off + 1)A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}An 8-bit byte.
type byte = bits(8)Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundval host_scratch_store_stateless_input¶
Stores a source-backed slice at an explicit arena offset. Success carries the resulting arena high-water mark.
val host_scratch_store_stateless_input = impure { c: "scratch_store_stateless_input" } : forall 'dst 'off 'len,
0
<= 'dst
& 'dst
<= scratch_region_bound
& stateless_input_valid_range(
'off,
'len,
). (
int('dst),
StatelessInputSliceFields('off, 'len),
) -> ScratchSliceLength('dst + 'len)A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}A range in the immutable stateless-input envelope. Its source is carried by the nominal type rather than a runtime field.
struct StatelessInputSliceFields('off : Int, 'len : Int), stateless_input_valid_range('off, 'len) = {
bytes : int('off),
len : int('len),
}Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundWhether 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_boundval host_scratch_store_scratch¶
Stores an existing arena-backed slice at an explicit arena offset; the result carries the new arena high-water mark.
val host_scratch_store_scratch = impure { c: "scratch_store_scratch" } : forall 'dst 'off 'len,
0
<= 'dst
& 'dst
<= scratch_region_bound
& scratch_valid_range('off, 'len). (
int('dst),
ScratchSliceFields('off, 'len),
) -> ScratchSliceLength('dst + 'len)A range in the executor's reusable scratch arena. Its source is carried by the nominal type rather than a runtime field.
struct ScratchSliceFields('off : Int, 'len : Int), scratch_valid_range('off, 'len) = {
bytes : int('off),
len : int('len),
}A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundWhether 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_boundval host_scratch_store_log_data¶
Stores a retained-log-data slice at an explicit arena offset; the result carries the new arena high-water mark.
val host_scratch_store_log_data = impure { c: "scratch_store_log_data" } : forall 'dst 'off 'len,
0
<= 'dst
& 'dst
<= scratch_region_bound
& log_data_valid_range('off, 'len). (
int('dst),
LogDataSliceFields('off, 'len),
) -> ScratchSliceLength('dst + 'len)A range in the transaction-log data arena.
struct LogDataSliceFields('off : Int, 'len : Int), log_data_valid_range('off, 'len) = {
bytes : int('off),
len : int('len),
}A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}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_boundExecutor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundval host_scratch_store_output¶
Stores an output-buffer-backed slice at an explicit arena offset; the result carries the new arena high-water mark.
val host_scratch_store_output = impure { c: "scratch_store_output" } : forall 'dst 'off 'len,
0
<= 'dst
& 'dst
<= scratch_region_bound
& output_region_valid_range('off, 'len). (
int('dst),
OutputSliceFields('off, 'len),
) -> ScratchSliceLength('dst + 'len)A range in the frame-output buffer.
struct OutputSliceFields('off : Int, 'len : Int), output_region_valid_range('off, 'len) = {
bytes : int('off),
len : int('len),
}A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}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_boundExecutor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundval host_scratch_store_address¶
Stores a fixed 20-byte address in wire order.
val host_scratch_store_address = impure { c: "scratch_store_address" } : forall 'off,
0 <= 'off & 'off <= scratch_region_bound. (
int('off),
address,
) -> ScratchSliceLength('off + 20)A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}A 20-byte account address (YP §4.1), in canonical protocol byte order.
type address = vector(20, inc, byte)Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundval host_scratch_store_b256¶
Stores the first len wire-order bytes of a fixed 32-byte value.
val host_scratch_store_b256 = impure { c: "scratch_store_b256" } : forall 'off 'len,
0
<= 'off
& 'off
<= scratch_region_bound
& 0
<= 'len
& 'len
<= 32. (int('off), b256, int('len)) -> ScratchSliceLength(
'off + 'len,
)A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}A KECCAK-256 / storage-key sized digest, in canonical protocol byte order.
type b256 = vector(32, inc, byte)Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundval host_scratch_store_fixed_bytes_256¶
Stores a decreasing fixed 256-byte vector in canonical wire order.
val host_scratch_store_fixed_bytes_256 = impure { c: "scratch_store_fixed_bytes_256" } : forall 'off,
0
<= 'off
& 'off
<= scratch_region_bound. (
int('off),
vector(256, dec, byte),
) -> ScratchSliceLength('off + 256)A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}An 8-bit byte.
type byte = bits(8)Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundval host_scratch_store_word¶
Stores the low len bytes of a word in canonical big-endian order.
val host_scratch_store_word = impure { c: "scratch_store_word" } : forall 'off 'len,
0
<= 'off
& 'off
<= scratch_region_bound
& 0
<= 'len
& 'len
<= 32. (int('off), word, int('len)) -> ScratchSliceLength(
'off + 'len,
)A scratch-arena range of exactly 'required bytes.
type ScratchSliceLength('required : Int) = {
'off 'len,
scratch_valid_range('off, 'len) & 'len == 'required.
ScratchSliceFields('off, 'len)
}Executor scratch-arena capacity.
type scratch_region_bound : Int = default_host_region_boundThe 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)val host_scratch_truncate¶
Discards arena contents from the given offset on; the axiom behind scratch_rewind and scratch_reset.
val host_scratch_truncate = impure { c: "scratch_truncate" } : scratch_pointer -> unitA coordinate in the executor scratch arena.
type scratch_pointer = range(0, scratch_region_bound)