Kernel scratch allocation

A bump cursor makes construction order and lifetime visible in the Sail semantics while the bytes themselves remain in host-backed memory.

Non-normative

This page documents the model's host interface — internal contracts of the executable specification, not protocol rules.

register scratch_arena

The active scratch arena; its length is the Sail-owned high-water mark.

register scratch_arena : ScratchSlice = EMPTY_SCRATCH_SLICE

function scratch_length_add

function scratch_length_add(left, right) =
    if right <= sizeof(scratch_region_bound) - left then {
        left + right
    } else {
        assert(false, "scratch length overflow");
        0
    }

function scratch_begin

Marks the start of a scratch construction.

function scratch_begin() -> source_pointer = {
    let arena = scratch_arena;
    arena.len
}

function scratch_reserve

function scratch_reserve(len) = {
    let arena = scratch_arena;
    let reserved = host_scratch_reserve(arena.len, len);
    assert(reserved, "scratch reserve");
    arena.len
}

function scratch_push_byte

Appends one byte without constructing a Sail list.

function scratch_push_byte(data : byte) -> unit = {
    let arena = scratch_arena;
    scratch_arena = host_scratch_store_byte(arena.len, data)
}

function stateless_input_scratch_push_slice

Appends a source-backed slice at the cursor.

function stateless_input_scratch_push_slice(data : StatelessInputSlice) -> unit = {
    if data.len != 0 then {
        let arena = scratch_arena;
        scratch_arena = host_scratch_store_stateless_input(arena.len, data)
    }
}

function scratch_scratch_push_slice

Appends an existing arena-backed slice at the cursor.

function scratch_scratch_push_slice(data : ScratchSlice) -> unit = {
    if data.len != 0 then {
        let arena = scratch_arena;
        scratch_arena = host_scratch_store_scratch(arena.len, data)
    }
}

function log_data_scratch_push_slice

Appends a retained-log-data slice at the cursor.

function log_data_scratch_push_slice(data : LogDataSlice) -> unit = {
    if data.len != 0 then {
        let arena = scratch_arena;
        scratch_arena = host_scratch_store_log_data(arena.len, data)
    }
}

function output_scratch_push_slice

Appends an output-buffer-backed slice at the cursor.

function output_scratch_push_slice(data : OutputSlice) -> unit = {
    if data.len != 0 then {
        let arena = scratch_arena;
        scratch_arena = host_scratch_store_output(arena.len, data)
    }
}

function scratch_push_address

Appends a fixed 20-byte address at the cursor.

function scratch_push_address(data : address) -> unit = {
    let arena = scratch_arena;
    scratch_arena = host_scratch_store_address(arena.len, data)
}

function scratch_push_b256

Appends a prefix of a fixed 32-byte value at the cursor.

function scratch_push_b256(data : b256, len : range(0, 32)) -> unit = {
    if len != 0 then {
        let arena = scratch_arena;
        scratch_arena = host_scratch_store_b256(arena.len, data, len)
    }
}

function scratch_push_fixed_bytes_256

Appends a decreasing fixed 256-byte vector in canonical wire order.

function scratch_push_fixed_bytes_256(data : vector(256, dec, byte)) -> unit = {
    let arena = scratch_arena;
    scratch_arena = host_scratch_store_fixed_bytes_256(arena.len, data)
}

function scratch_push_word_be

Appends the low len bytes of a word in canonical big-endian order.

function scratch_push_word_be(data : word, len : range(0, 32)) -> unit = {
    if len != 0 then {
        let arena = scratch_arena;
        scratch_arena = host_scratch_store_word(arena.len, data, len)
    }
}

function scratch_finish

The slice covering everything pushed since start.

function scratch_finish(start : source_pointer) -> ScratchSlice =
    let start_offset = start in
    let arena = scratch_arena in
    let stop_offset = arena.len in
    if start_offset <= stop_offset then {
        sub_slice(arena, start, stop_offset - start_offset)
    } else {
        assert(false, "scratch finish mark");
        EMPTY_SCRATCH_SLICE
    }

function scratch_rewind

Discards everything pushed since mark.

function scratch_rewind(mark : source_pointer) -> unit =
    let mark_offset = mark in
    let arena = scratch_arena in
    let cursor_offset = arena.len in
    if mark_offset <= cursor_offset then {
        scratch_arena = sub_slice(arena, 0, mark);
        host_scratch_truncate(mark)
    } else {
        assert(false, "scratch rewind mark")
    }

function scratch_reset

Empties the arena (per-block lifetime).

function scratch_reset() -> unit = {
    scratch_arena = EMPTY_SCRATCH_SLICE;
    host_scratch_truncate(0)
}