Typed byte regions

Unmaterialized byte sequences. The specification's bulk data lives in named host regions. A slice's nominal type identifies its region; the semantic value contains only a source coordinate and a length. There is deliberately no generic slice and no runtime source discriminant.

The standard C ABI lowers the coordinate to an offset in the named region. The fixed-capacity optimized C ABI lowers the same coordinate to a validated absolute pointer, after allocating every mutable region before Sail execution. This representation choice is not part of the protocol semantics: subslicing is coordinate addition in both builds, and the nominal type retains provenance.

Constants

The fixed lengths identify addresses, words, limbs, and double words.

type StatelessInputSliceFields

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),
}

type StatelessInputSlice

A stateless-input range with its coordinate and length packed existentially.

type StatelessInputSlice = {
    'off 'len,
    stateless_input_valid_range('off, 'len).
    StatelessInputSliceFields('off, 'len)
}

type StatelessInputSliceLength

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)
}

type StatelessInputSliceAtLeast

A stateless-input range of at least 'minimum bytes.

type StatelessInputSliceAtLeast('minimum : Int) = {
    'off 'len,
    stateless_input_valid_range('off, 'len) & 0 <= 'minimum & 'minimum <= 'len.
    StatelessInputSliceFields('off, 'len)
}

type StatelessInputSliceAtMost

A stateless-input range of at most 'maximum bytes.

type StatelessInputSliceAtMost('maximum : Int) = {
    'off 'len,
    stateless_input_valid_range('off, 'len) & 0 <= 'maximum & 'len <= 'maximum.
    StatelessInputSliceFields('off, 'len)
}

type ScratchSliceFields

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),
}

type ScratchSlice

A scratch-arena range with its coordinate and length packed existentially.

type ScratchSlice = {
    'off 'len,
    scratch_valid_range('off, 'len).
    ScratchSliceFields('off, 'len)
}

type ScratchSliceLength

A scratch-arena range of exactly 'required bytes.

type ScratchSliceLength('required : Int) = {
    'off 'len,
    scratch_valid_range('off, 'len) & 'len == 'required.
    ScratchSliceFields('off, 'len)
}

type ScratchSliceAtLeast

A scratch-arena range of at least 'minimum bytes.

type ScratchSliceAtLeast('minimum : Int) = {
    'off 'len,
    scratch_valid_range('off, 'len) & 0 <= 'minimum & 'minimum <= 'len.
    ScratchSliceFields('off, 'len)
}

type EvmMemorySliceFields

A borrowed range in the shared EVM-memory arena. Its coordinate is absolute within the arena (an offset in the standard ABI and a stable pointer in the optimized ABI), so calldata borrowed from a suspended parent remains valid while a child frame is active. The machine carries only memory_height; this pointer-bearing value exists at derived-view boundaries.

struct EvmMemorySliceFields('off : Int, 'len : Int), memory_region_valid_range('off, 'len) = {
    bytes : int('off),
    len : int('len),
}

type EvmMemorySlice

An EVM-memory range with its coordinate and length packed existentially.

type EvmMemorySlice = {
    'off 'len,
    memory_region_valid_range('off, 'len).
    EvmMemorySliceFields('off, 'len)
}

type EvmMemorySliceLength

An EVM-memory range of exactly 'required bytes.

type EvmMemorySliceLength('required : Int) = {
    'off 'len,
    memory_region_valid_range('off, 'len) & 'len == 'required.
    EvmMemorySliceFields('off, 'len)
}

type EvmMemorySliceAtLeast

An EVM-memory range of at least 'minimum bytes.

type EvmMemorySliceAtLeast('minimum : Int) = {
    'off 'len,
    memory_region_valid_range('off, 'len) & 0 <= 'minimum & 'minimum <= 'len.
    EvmMemorySliceFields('off, 'len)
}

type CodeRegionSliceFields

A range in the content-addressed executable-code arena.

struct CodeRegionSliceFields('off : Int, 'len : Int), code_region_valid_range('off, 'len) = {
    bytes : int('off),
    len : int('len),
}

type CodeRegionSlice

A code-region range with its coordinate and length packed existentially.

type CodeRegionSlice = {
    'off 'len,
    code_region_valid_range('off, 'len).
    CodeRegionSliceFields('off, 'len)
}

type LogDataSliceFields

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),
}

type LogDataSlice

A log-data range with its coordinate and length packed existentially.

type LogDataSlice = {
    'off 'len,
    log_data_valid_range('off, 'len).
    LogDataSliceFields('off, 'len)
}

type LogDataSliceLength

A log-data range of exactly 'required bytes.

type LogDataSliceLength('required : Int) = {
    'off,
    log_data_valid_range('off, 'required).
    LogDataSliceFields('off, 'required)
}

type OutputSliceFields

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),
}

type OutputSlice

A frame-output range with its coordinate and length packed existentially.

type OutputSlice = {
    'off 'len,
    output_region_valid_range('off, 'len).
    OutputSliceFields('off, 'len)
}

type CalldataSlice

Calldata is either the immutable top-level transaction input or a frozen range of the suspended caller's memory. The variants state the only two protocol-valid provenances instead of exposing the host's region enum.

union CalldataSlice = {
    /* the immutable top-level transaction input */
    InputCalldata : StatelessInputSlice,
    /* a frozen range of the suspended caller's memory */
    MemoryCalldata : EvmMemorySlice,
}

function calldata_slice_length

The byte length of a calldata slice, independent of its provenance.

function calldata_slice_length(s : CalldataSlice) -> source_length =
    match s {
        InputCalldata(bytes) => bytes.len,
        MemoryCalldata(bytes) => bytes.len,
    }

function stateless_input_slice_length

The byte length of a stateless-input slice.

function stateless_input_slice_length(s : StatelessInputSlice) -> source_length =
    s.len

let ADDRESS_BYTE_LENGTH

let ADDRESS_BYTE_LENGTH : int(20) = 20

let WORD_BYTE_LENGTH

let WORD_BYTE_LENGTH : int(32) = 32

let EIGHT_BYTE_LENGTH

let EIGHT_BYTE_LENGTH : int(8) = 8

let DOUBLE_WORD_BYTE_LENGTH

let DOUBLE_WORD_BYTE_LENGTH : int(64) = 64

function stateless_input_slice

function stateless_input_slice(off, len) =
    struct { bytes = off, len = len }

function scratch_slice

function scratch_slice(off, len) =
    struct { bytes = off, len = len }

function evm_memory_slice

function evm_memory_slice(off, len) =
    struct { bytes = off, len = len }

function code_region_slice

function code_region_slice(off, len) =
    struct { bytes = off, len = len }

function log_data_slice

function log_data_slice(off, len) =
    struct { bytes = off, len = len }

function output_slice

function output_slice(off, len) =
    struct { bytes = off, len = len }

let EMPTY_STATELESS_INPUT_SLICE

let EMPTY_STATELESS_INPUT_SLICE : StatelessInputSliceFields(0, 0) = stateless_input_slice(0, 0)

let EMPTY_SCRATCH_SLICE

let EMPTY_SCRATCH_SLICE : ScratchSliceFields(0, 0) = scratch_slice(0, 0)

let EMPTY_EVM_MEMORY_SLICE

let EMPTY_EVM_MEMORY_SLICE : EvmMemorySliceFields(0, 0) = evm_memory_slice(0, 0)

let EMPTY_CODE_REGION_SLICE

let EMPTY_CODE_REGION_SLICE : CodeRegionSliceFields(0, 0) = code_region_slice(0, 0)

let EMPTY_LOG_DATA_SLICE

let EMPTY_LOG_DATA_SLICE : LogDataSliceFields(0, 0) = log_data_slice(0, 0)

let EMPTY_OUTPUT_SLICE

let EMPTY_OUTPUT_SLICE : OutputSliceFields(0, 0) = output_slice(0, 0)

let EMPTY_CALLDATA

let EMPTY_CALLDATA : CalldataSlice = InputCalldata(EMPTY_STATELESS_INPUT_SLICE)

function stateless_input_sub_slice

function stateless_input_sub_slice(s, off, len) =
    struct { bytes = s.bytes + off, len = len }

function scratch_sub_slice

function scratch_sub_slice(s, off, len) =
    struct { bytes = s.bytes + off, len = len }

function memory_sub_slice

function memory_sub_slice(s, off, len) =
    struct { bytes = s.bytes + off, len = len }

function log_data_sub_slice

function log_data_sub_slice(s, off, len) =
    struct { bytes = s.bytes + off, len = len }

function calldata_sub_slice

function calldata_sub_slice(s, off, len) = {
    match s {
        InputCalldata(bytes) => if off + len <= bytes.len then {
            let subslice = stateless_input_sub_slice(bytes, off, len);
            InputCalldata(subslice)
        } else {
            assert(false, "calldata sub-slice bounds");
            EMPTY_CALLDATA
        },
        MemoryCalldata(bytes) => if off + len <= bytes.len then {
            let subslice = memory_sub_slice(bytes, off, len);
            MemoryCalldata(subslice)
        } else {
            assert(false, "calldata sub-slice bounds");
            EMPTY_CALLDATA
        },
    }
}

function stateless_input_slice_suffix

function stateless_input_slice_suffix(s, off) =
    struct { bytes = s.bytes + off, len = s.len - off }

function scratch_slice_suffix

function scratch_slice_suffix(s, off) =
    struct { bytes = s.bytes + off, len = s.len - off }

type LogData

A log payload retained by the host: either an existing byte slice or the canonical big-endian bytes of one EVM word used by system logs.

union LogData = {
    /* an EVM-memory payload copied into retained log storage */
    LogDataMemory : EvmMemorySlice,
    /* the canonical big-endian bytes of one EVM word */
    LogDataWord : word,
}