Machine state¶

The user-space half of the machine: per-frame registers, operand stack, gas counter, and the saved-frame stack for nested calls. World state lives in the host kernel and is reached only via k_* calls; world rollback on revert is a kernel snapshot, not saved here.

The state-passing convention¶

Hot machine state flows through handler signatures instead of registers, mirroring the Yellow Paper's state-passing transition μ′ = Ξ(μ): the remaining gas (μ_g), the program counter (μ_pc), the operand-stack cursor (μ_s), and the frame-memory height (μ_i) are carried by value from the interpreter loop into each opcode handler and returned updated. No handler reads or writes these registers: the canonical loop supplies each step's arguments from the registers and assigns the returned state back, while frame-boundary code — frame save/suspend (suspend_frame), resume (resume_frame), and the transaction wrapper — synchronizes them explicitly. The optimized interpreter carries the same values in locals and touches the registers only at those frame boundaries.

The frame registers¶

One Message per active frame (YP "message call" I = (I_a, I_o, I_s, …)); sub-calls save and restore these registers in the interpreter.

function `validated_refund_add`¶

function validated_refund_add(left, right) = {
    let total = left + right;
    if (-sizeof(gas_refund_bound) <= total) & (total <= sizeof(gas_refund_bound)) then {
        total
    } else {
        fatal_error(ExecutionInvalid)
    }
}

function `record_refund`¶

function record_refund(refund, delta) =
    validated_refund_add(refund, delta)

function `frame_code_len`¶

The frame code length in bytes (CODESIZE).

function frame_code_len(frame_code : Code) -> code_length = {
    let code = frame_code;
    let length = code.len;
    length
}

function `frame_jumpdest_valid`¶

function frame_jumpdest_valid(frame_code, dest) = {
    let code = frame_code;
    let length = code.len;
    jumpdest_ref_contains(code.jumpdests, length, dest)
}

The operand stack¶

let `STACK_LIMIT`¶

The 1024-element operand-stack limit (YP §9.1).

let STACK_LIMIT : operand_stack_height = 1024

function `conserved_gas_add`¶

function conserved_gas_add(available, credit) =
    if credit <= (2 ^ 64 - 1) - available then {
        available + credit
    } else {
        fatal_error(ExecutionInvalid)
    }

function `frame_state_gas_used`¶

Computes the signed state gas consumed by the current frame.

function frame_state_gas_used(
    state_gas_reservoir : state_gas,
    state_gas_remaining : state_gas,
    state_gas_spilled : state_gas_spill,
) -> (
    frame_state_gas_delta
) = {
    let entry = state_gas_reservoir;
    let remaining = state_gas_remaining;
    let spilled = state_gas_spilled;
    entry - remaining + spilled
}

function `exceptional_state`¶

function exceptional_state(state_gas_remaining, state_gas_spilled, state_gas_reservoir, k) = {
    let execution_profile = k_execution_profile;
    let profile = execution_profile.protocol;
    if profile.fork >= Amsterdam then {
        struct {
            state_gas_remaining = state_gas_reservoir,
            state_gas_spilled = STATE_GAS_SPILL_ZERO,
            status = Exceptional(k),
        }
    } else {
        struct {
            state_gas_remaining = state_gas_remaining,
            state_gas_spilled = state_gas_spilled,
            status = Exceptional(k),
        }
    }
}

function `stack_height`¶

The stack height below a carried cursor.

function stack_height(top : StackPointer) -> operand_stack_height = stack_top_height(top)

type `StackValidation`¶

Checks the Yellow Paper stack precondition for one instruction before it charges gas or performs side effects. inputs is the instruction's required stack height (delta) and outputs is the height it contributes after consuming those inputs (alpha). This is the single stack-bounds guard: handler bodies consume and produce operands unchecked behind it.

enum StackValidation = { StackValid, StackUnderflowFailure, StackOverflowFailure }

function `validate_stack`¶

Classifies the carried cursor against one instruction's input and output stack requirements.

function validate_stack(top, inputs, outputs) = {
    let height = stack_height(top);
    if height < inputs then {
        StackUnderflowFailure
    } else if STACK_LIMIT < height - inputs + outputs then {
        StackOverflowFailure
    } else {
        StackValid
    }
}

function `read_stack_word`¶

Reads the n=0 slot under a validated cursor.

function read_stack_word(sp : StackPointer) -> word = stack_slot_read(sp, 0)

function `write_stack_word`¶

Writes the n=0 slot under a validated cursor.

function write_stack_word(sp : StackPointer, value : word) -> unit =
    stack_slot_write(sp, 0, value)

function `stack_set`¶

Overwrites the n-th-from-top operand (SWAP); the cursor is unchanged.

function stack_set(top : StackPointer, n : stack_index, w : word) -> unit =
    stack_slot_write(top, n, w)

function `is_running`¶

Whether the frame is still running.

function is_running(frame_status : FrameStatus) -> bool = match frame_status {
    Running() => true,
    _ => false,
}

function `calldata_install`¶

Installs the frame's calldata reference.

function calldata_install(data : CalldataSlice) -> CalldataSlice = data

function `returndata_clear`¶

Clears the returndata buffer (a new sub-call begins).

function returndata_clear() -> OutputSlice = EMPTY_OUTPUT_SLICE

function `returndata_size`¶

RETURNDATASIZE.

function returndata_size(returndata : OutputSlice) -> source_pointer = {
    let data = returndata;
    data.len
}

function `returndata_copy`¶

function returndata_copy(returndata, dst, off, len) =
    slice_copy(returndata, dst, off, len)

function `returndata_copy_prefix`¶

Copies min(want, size) returndata bytes — the CALL-family output write-back.

function returndata_copy_prefix(returndata : OutputSlice, dst : memory_base, want : memory_length) -> unit = {
    let wanted = want;
    let available = returndata_size(returndata);
    let copy_length : memory_length =
        if wanted < available then wanted else available;
    slice_copy(returndata, dst, 0, copy_length)
}

The frame memory¶

The EVM's view over frame memory, a region of the host interface. The active frame's exact byte high-water mark flows through memory-family handlers as the scalar memory_height, beside Sail's absolute arena memory_base. The host owns the arena storage and returns pointer-bearing EvmMemorySlice values only when Sail requests a derived view. Every access is guarded by gas charging against the carried cursor: an unaffordable expansion sets the halt status before expand_memory is reached, so a post-out-of-gas write to a huge offset (for example, MSTORE at 2^32) cannot grow the backing buffer. Successful expansion raises the scalar high-water mark that MSIZE and memory-expansion gas read.

function `returndata_remaining`¶

function returndata_remaining(available, offset) = available - offset

function `memory_high_water`¶

Returns the carried frame's exact byte high-water mark.

function memory_high_water(height : memory_height) -> memory_length = height

let `MEMORY_HEIGHT_ZERO`¶

The empty EVM-memory high-water mark.

let MEMORY_HEIGHT_ZERO : memory_height = 0

let `MEMORY_BASE_ZERO`¶

The top-level frame begins at the shared arena's semantic offset zero.

let MEMORY_BASE_ZERO : memory_base = 0

function `memory_absolute`¶

Converts a frame-relative coordinate to an absolute arena coordinate.

function memory_absolute(base : memory_base, relative : memory_length) -> memory_base =
    if relative <= sizeof(memory_region_bound) - base then {
        base + relative
    } else {
        fatal_error(ExecutionInvalid)
    }

function `memory_parent_base`¶

Restores the parent arena cursor from the current child cursor and the parent's frame-scoped memory height.

function memory_parent_base(child_base : memory_base, parent_height : memory_height) -> memory_base =
    if parent_height <= child_base then {
        child_base - parent_height
    } else {
        fatal_error(ExecutionInvalid)
    }

function `expand_memory`¶

Materializes an already-charged memory high-water mark and returns its updated scalar height.

function expand_memory(base : memory_base, height : memory_height, requested_height : memory_length) -> memory_height = {
    if requested_height <= sizeof(memory_region_bound) - base then {
        if height < requested_height then {
            mem_expand(base, height, requested_height);
            requested_height
        } else {
            height
        }
    } else {
        fatal_error(ExecutionInvalid)
    }
}

function `active_memory_slice`¶

function active_memory_slice(base, mem, off, len) =
    if len == 0 then {
        EMPTY_EVM_MEMORY_SLICE
    } else if mem <= sizeof(memory_region_bound) - base & off + len <= mem then {
        let window = mem_view(base, mem, off + len);
        sub_slice(window, off, len)
    } else {
        fatal_error(ExecutionInvalid)
    }

function `memory_code_slice`¶

function memory_code_slice(base, mem, off, len) =
    if len == 0 then {
        EMPTY_CODE_SLICE
    } else if mem <= sizeof(memory_region_bound) - base & off + len <= mem then {
        let window = mem_view(base, mem, off + len);
        let initcode = sub_slice(window, off, len);
        code_db_intern_memory(initcode)
    } else {
        fatal_error(ExecutionInvalid)
    }

function `suspend_frame`¶

Captures parent execution state and enters child stack and memory frames. The caller has published its carried machine state to the frame registers: this checkpoint reads them at the one authoritative boundary. The host operand-frame cursor mirrors call_depth: push the empty child operand stack before installing the child's semantic depth, and pop it before restoring the parent's semantic depth.

function suspend_frame(
    pc : code_pointer,
    gas_remaining : gas,
    stack_top : StackPointer,
    memory_base : memory_base,
    memory_height : memory_height,
    state_gas_remaining : state_gas,
    state_gas_spilled : state_gas_spill,
    frame_refund : gas_refund,
    frame_status : FrameStatus,
    message : Message,
    frame_code : Code,
    calldata : CalldataSlice,
) -> (
    (FrameCheckpoint, StackPointer, memory_base, memory_height)
) = {
    k_journal_checkpoint();
    let child_stack = operand_stack_push_empty_frame();
    let child_memory_base = memory_absolute(memory_base, memory_height);
    let child_memory_height = MEMORY_HEIGHT_ZERO;
    let checkpoint : FrameCheckpoint = struct {
            pc = pc,
            gas_remaining = gas_remaining,
            stack_top = stack_top,
            state_gas_remaining = state_gas_remaining,
            state_gas_spilled = state_gas_spilled,
            refund = frame_refund,
            status = frame_status,
            message = message,
            code = frame_code,
            calldata = calldata,
            memory_height = memory_height,
        };
    (checkpoint, child_stack, child_memory_base, child_memory_height)
}

function `mem_set_byte`¶

Writes one memory byte and raises the high-water mark.

function mem_set_byte(base : memory_base, off : memory_base, v : byte) -> unit = {
    let absolute_offset = memory_absolute(base, off);
    mem_write_byte(absolute_offset, v)
}

function `mem_load`¶

MLOAD: the big-endian word at off.

function mem_load(base : memory_base, off : memory_base) -> word = {
    let absolute_offset = memory_absolute(base, off);
    mem_load_word(absolute_offset)
}

function `mem_store`¶

MSTORE: writes the big-endian word at off and raises the high-water mark.

function mem_store(base : memory_base, off : memory_base, w : word) -> unit = {
    let absolute_offset = memory_absolute(base, off);
    mem_store_word(absolute_offset, w)
}

function `mem_store_byte`¶

MSTORE8: writes the low byte of w.

function mem_store_byte(base : memory_base, off : memory_base, w : word) -> unit = {
    let value = word_low_byte(w);
    mem_set_byte(base, off, value)
}

function `mem_mcopy`¶

MCOPY (EIP-5656): overlapping-safe memory-to-memory copy.

function mem_mcopy(base : memory_base, dst : memory_base, src : memory_base, len : memory_length) -> unit =
    if len != 0 then {
        let absolute_dst = memory_absolute(base, dst);
        let absolute_src = memory_absolute(base, src);
        mem_move(absolute_dst, absolute_src, len)
    }

function `mem_keccak`¶

KECCAK256 over the already-expanded memory range [off, off+len).

function mem_keccak(base : memory_base, mem : memory_height, range : MemoryRange) -> word = {
    let bytes = active_memory_slice(base, mem, range.off, range.len);
    let digest = keccak256(bytes);
    hash_to_word(digest)
}

Machine state¶

The state-passing convention¶

The frame registers¶

function validated_refund_add¶

function record_refund¶

function frame_code_len¶

function frame_jumpdest_valid¶

The operand stack¶

let STACK_LIMIT¶

function conserved_gas_add¶

function frame_state_gas_used¶

function exceptional_state¶

function stack_height¶

type StackValidation¶

function validate_stack¶

function read_stack_word¶

function write_stack_word¶

function stack_set¶

function is_running¶

function calldata_install¶

function returndata_clear¶

function returndata_size¶

function returndata_copy¶

function returndata_copy_prefix¶

The frame memory¶

function returndata_remaining¶

function memory_high_water¶

let MEMORY_HEIGHT_ZERO¶

let MEMORY_BASE_ZERO¶

function memory_absolute¶

function memory_parent_base¶

function expand_memory¶

function active_memory_slice¶

function memory_code_slice¶

function suspend_frame¶

function mem_set_byte¶

function mem_load¶

function mem_store¶

function mem_store_byte¶

function mem_mcopy¶

function mem_keccak¶