Instruction Set

This chapter is the bytecode reference. It lists every instruction the Keleusma virtual machine executes, so the disassembly shown in the playground bytecode view has a place to be looked up. It reproduces the authoritative docs/spec/INSTRUCTION_SET.md from the repository.

The Keleusma VM executes a stack-based bytecode using block-structured control flow. All instructions operate on a value stack. This document lists every instruction with its operands, behavior, and cost contribution to the WCET (worst-case execution time) and WCMU (worst-case memory usage) analyses.

Each instruction carries a relative integer cost. Costs are unitless relative weights, not cycle counts. Higher values indicate more expensive operations. The cost table is consulted by wcet_stream_iteration(); the per-instruction stack and heap effects are consulted by wcmu_stream_iteration().

For details on how bytecode is generated from source, see Chapter 25, From Source to Bytecode. For the bytecode wire format including the framing header, opcode-stream encoding, and operand pool, see EXECUTION_MODEL.md. For the structural ISA specification including block hierarchy and verification rules, see STRUCTURAL_ISA.md.

Constants

PushImmediate encoding

Sixteen small-integer literals (Int(0) through Int(15)) are encoded inline. Larger or non-immediate literals continue to use Const referencing the constant pool. The extraction rule is predictable: operand values 0..3 select sentinels; values 4..19 select Int(value - 4); values 20..255 signal corruption.

Local Variables

Data Segment

The unified slot index space partitions into shared slots [0, shared_count) and private slots [shared_count, shared_count + private_count). Shared slots live in the host-owned buffer borrowed at each call and are reached by the host through Vm::get_shared/Vm::set_shared (B28 item 2); private slots are script-only and live in the arena’s persistent region. The opcodes below admit both partitions; the runtime dispatches by comparing the slot index against the cached shared_slot_count, sending a shared slot to the borrowed buffer by byte offset and a private slot to the arena. Const data fields do not consume a slot; field reads compile to Const and writes are compile errors.

Arithmetic

Integer arithmetic uses the checked-arithmetic family. Each CheckedAdd, CheckedSub, CheckedMul, and CheckedNeg opcode pops Value::Int operands (two for the binary forms, one for CheckedNeg), computes the true result in i128, and pushes three slots: the low half, the high half, and an outcome flag (Int(0) ok, Int(1) overflow, Int(2) underflow). The push order places low at the bottom and flag on top so that surface-level wrapping expressions, such as a + b on Int operands, compile to the checked opcode followed by PopN(2) and leave the wrapping result on the stack. Source-level pattern-arm matching destructures the three outputs.

The wrapping arithmetic opcodes Add, Sub, Mul, and Neg remain in the instruction set but no longer accept Value::Int operands. Their permitted operand types are Byte, Fixed, and Float. The V0.2.0 Consolidation B pass narrowed these opcodes by routing all Int arithmetic through the checked family; the compiler emits CheckedXxx; PopN(2) for every Int operand position. Operands whose type the compiler cannot statically infer fall through to the Int path as well, because Word is the default numeric type.

Op::Div and Op::Mod remain polymorphic over Int, Byte, and Float. Their checked counterparts CheckedDiv and CheckedMod expose the corner cases of signed division.

CheckedMul and CheckedDiv carry a u8 fraction-bit count that selects integer or Q-format arithmetic, where 0 is integer and a positive count is Fixed. This is the only place the integer and fixed-point datapaths differ, namely a shift by the fraction-bit count around the multiply or divide, so a single parameterized opcode serves both rather than separate opcodes. CheckedAdd, CheckedSub, CheckedMod, and CheckedNeg need no such parameter because their Fixed forms involve no shift, and they dispatch on the operand type alone.

Comparisons

Logic

Short-circuit AND and OR are encoded as If-branching at the bytecode level; there are no LogicalAnd or LogicalOr opcodes.

Bitwise

Control Flow

Block-structured control flow opcodes carry u16 jump targets. A chunk’s opcode count is therefore bounded at 65,535 (CHUNK_SIZE_HARD_LIMIT). The compiler emits a CompileWarning when a single chunk crosses 80% of the limit (52,428 ops, CHUNK_SIZE_SOFT_WARN_THRESHOLD), prompting decomposition into helper functions; the bytecode at the limit remains valid. Chunks exceeding CHUNK_SIZE_HARD_LIMIT are rejected at compile time as a CompileError. The host invokes keleusma::compiler::compile_with_warnings(program, target) to receive the warning vector alongside the module; compile_with_target and compile discard the warnings for callers that do not need them.

Function Calls

Native function calls partition into two classes distinguished by the source-level use declaration and a matching host-side registration ABI:

• Verified natives. Imported with use module::name. Host registers through Vm::register_verified_native(name, fn, wcet_bound, wcmu_bound). The host-attested cost folds into the iteration’s WCET and WCMU budget. Compiler emits CallVerifiedNative.
• External natives. Imported with use external module::name. Host registers through Vm::register_external_native(name, fn, max_invocations_per_iteration). The host attests an upper bound on per-iteration invocation count rather than per-call cost. Compiler emits CallExternalNative.

The runtime cross-checks each declared native against its host registration at the entry of Vm::call_function and at every explicit invocation of Vm::verify_native_classifications. The check walks every native call site in the module and rejects a mismatch (e.g., a bytecode importing use math::sqrt but a host registering sqrt through register_external_native) as VmError::VerifyError. The result is cached after the first successful walk; any register_* call or replace_module invocation invalidates the cache. Hosts that prefer to surface mismatches at a deployment-validation step rather than at first call may invoke verify_native_classifications explicitly after registration.

V0.2.0 Phase 5 introduced the verified-versus-external split. The legacy Op::CallNative opcode was retired; every native call site compiles to either Op::CallVerifiedNative or Op::CallExternalNative. Hosts that previously called Vm::register_native continue to register verified natives because that method ascribes the verified classification.

The max_invocations_per_iteration attestation on external natives is recorded at registration but is not yet folded into the WCMU bound. The verifier treats external natives as contributing zero to the script’s per-iteration WCMU budget; the host accepts that external natives are outside the script’s resource contract and has separately verified their resource use. The chunk-level integration (which would bound external-native cost as max_invocations_per_iteration * per_call_wcmu per chunk rather than per static call site) is forward-looking work tracked under B20.

The closure-construction and indirect-dispatch opcodes (PushFunc, MakeClosure, MakeRecursiveClosure, CallIndirect) are not present in the ISA. Closure-shaped surface expressions are rejected at the type-checker stage with a diagnostic that names the construct; first-class function values are likewise rejected. The Value::Func runtime variant was retired alongside the opcodes in V0.2.0 Phase 4. Surface programs that previously used closures must be rewritten as top-level fn definitions or trait methods.

Coroutine and Streaming

Stack

Type Construction

A tuple is an anonymous struct, an array a homogeneous struct, and a flat enum a struct whose first packed value is the discriminant, so flat construction is one operation across all four kinds. The operand carries the composite kind, the operand-stack pop count, and either the exact flat allocation size in bytes (flat form) or a struct-template index (boxed form). The flat byte size is the precise worst-case-memory-usage contribution the verifier sums; see the Heap allocation table below.

The Option::None sentinel and Option::Some wrap are handled through PushImmediate(3) and the natural representation of the wrapped value, respectively; there are no dedicated PushNone or WrapSome opcodes.

Field Access

Type Testing

Casting and Fixed-Point Arithmetic

Faults

Opcode count and operand-shape inventory

The instruction set contains 66 opcodes. The B28 consolidation retired the four V0.2.0 construct opcodes (NewStruct, NewEnum, NewArray, NewTuple, wire ids 34-37) in favour of the single NewComposite opcode (wire id 69). The retired ids are reserved and not reused; the maximum live wire id is 69. Operand shapes:

The shapes below are the Op-variant operand types as defined in src/bytecode.rs, which differ from the flattened inline wire encodings documented in WIRE_FORMAT.md. In particular the four baked field-and-element access opcodes carry bespoke operand structs rather than a plain integer.

The wire encoding flattens these Op-level shapes: 62 of the 66 opcodes always carry their operand inline in the 4-byte opcode record. Three opcodes (GetDataIndexed, SetDataIndexed, and IsEnum) always reference an entry in the operand pool by index. NewComposite carries its operand inline in the common small flat form and references a (u16, u16, u8) operand-pool entry only for the boxed form or a flat field count above 62. The (u16, u8) opcodes (Call, CallVerifiedNative, CallExternalNative) fit inline because the u8 lands in byte 3 of the record. The four baked access opcodes fit their compiler-selected operand form inline. See EXECUTION_MODEL.md and WIRE_FORMAT.md for the wire format that encodes these shapes.

Cost Summary

The cost groupings reproduce bytecode::nominal_op_cycles. Hosts that need wall-clock WCET supply a custom CostModel calibrated to the target.

WCMU contributions

WCMU costs are reported separately as stack slot growth, stack slot shrink, and heap allocation in bytes. The constant VALUE_SLOT_SIZE_BYTES converts slot counts to bytes; the parametric Vm<W, A, F> shape uses size_of::<GenericValue<W, F>>() directly. Computed by wcmu_stream_iteration() in src/verify.rs.

Stack growth (peak net delta during execution)

The values reproduce Op::stack_growth in src/bytecode.rs. For multi-output opcodes the value is the net peak delta against the starting depth, not the raw push count: e.g. CheckedAdd pops two and pushes three, so the peak depth relative to the start is +1. IsEnum and IsStruct peek the scrutinee (no pop) and push a Bool, so their net delta is +1.

Stack shrink (slots popped during execution)

The values reproduce Op::stack_shrink. For opcodes whose net delta is non-negative (e.g. CheckedAdd, CheckedNeg) the shrink reads zero because the verifier accounts for the peak through stack_growth and there is no net pop.

Heap allocation (bytes)