prometeu-runtime/docs/specs/runtime/02-vm-instruction-set.md

Prometeu Virtual Machine (PVM)

Domain: VM subsystem overview Function: normative

This chapter defines the VM as an execution subsystem inside the PROMETEU machine.

It is intentionally narrower than the broader machine specs:

• execution model;
• opcode families;
• verifier boundary;
• relationship between the VM and adjacent specs.

For the bytecode-level instruction contract, see ../virtual-machine/ISA_CORE.md.

1 Scope

The PVM is a deterministic, stack-based VM designed for a fantasy console environment with fixed frame timing and explicit hardware-facing services.

This chapter does not fully restate:

• detailed value and calling semantics;
• heap/gate/GC internals;
• coroutine scheduling internals;
• host ABI policy.

Those now live in focused companion specs:

• 02a-vm-values-and-calling-convention.md
• 02b-vm-function-values-and-closures.md
• 03-memory-stack-heap-and-allocation.md
• 09a-coroutines-and-cooperative-scheduling.md
• 16-host-abi-and-syscalls.md
• 16a-syscall-policies.md

2 Core Design Principles

The PVM is designed around the following constraints:

1. Deterministic execution: no hidden threads or asynchronous callbacks.
2. Frame-based timing: execution is bounded by frame time and explicit safepoints.
3. Safe memory model: heap access is mediated by validated handles.
4. Simple compilation target: stack-based bytecode with verified control flow.
5. Stable ABI: calls and syscalls follow fixed slot-based contracts.
6. First-class functions: user function values are represented through closures.

3 Execution Model

The PVM executes bytecode inside the PROMETEU frame loop.

Each frame:

1. firmware enters the VM;
2. the VM runs until:
   • the frame budget is consumed; or
   • a FRAME_SYNC instruction is reached;
3. at FRAME_SYNC, the VM reaches the primary safepoint for GC and cooperative scheduling;
4. control returns to firmware/runtime orchestration.

FRAME_SYNC is the primary VM synchronization point. It is the boundary where the machine can safely account for:

• GC opportunity;
• coroutine handoff;
• frame-completion semantics;
• deterministic return to firmware.

4 Instruction Families

The public VM instruction surface is documented at the bytecode level in ../virtual-machine/ISA_CORE.md. At the machine/spec level, the instruction families are:

• execution control:
  • NOP, HALT, JMP, JMP_IF_FALSE, JMP_IF_TRUE, TRAP, FRAME_SYNC
• stack manipulation:
  • PUSH_CONST, literal pushes, POP, POP_N, DUP, SWAP
• arithmetic and logic:
  • numeric, comparison, boolean, and bitwise operations
• variable access:
  • globals and locals
• function calls:
  • CALL, RET
• function values:
  • MAKE_CLOSURE, CALL_CLOSURE
• cooperative concurrency:
  • SPAWN, YIELD, SLEEP
• VM/host boundary:
  • HOSTCALL, SYSCALL, INTRINSIC

The machine-level rule is simple:

• opcodes define explicit behavior;
• there are no hidden execution paths;
• timing-sensitive behavior is exposed through frame and safepoint semantics.

5 Verifier Boundary

Before execution, bytecode must pass the verifier.

The verifier ensures, at minimum:

1. valid instruction decoding;
2. valid jump targets;
3. consistent stack depth across control-flow joins;
4. valid call/return shape;
5. closure call safety rules;
6. patched syscall and intrinsic validity.

The verifier is structural. It does not replace runtime validation of dynamic values.

6 Relationship to Adjacent Specs

• 02a-vm-values-and-calling-convention.md defines slot values, tuples, frames, and return-slot semantics.
• 02b-vm-function-values-and-closures.md defines closure representation and function-value behavior.
• 03-memory-stack-heap-and-allocation.md defines stack/heap, handles, object layout, and GC.
• 09-events-and-concurrency.md defines events, timers, and the frame boundary model.
• 09a-coroutines-and-cooperative-scheduling.md defines coroutine lifecycle and scheduling.
• 16-host-abi-and-syscalls.md defines the syscall ABI boundary.

7 Summary

The PVM is:

• stack-based;
• deterministic;
• frame-synchronized;
• verifier-gated;
• closure-capable;
• coroutine-capable;
• embedded inside the larger PROMETEU console model, not equal to it.