# 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`](../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`](02a-vm-values-and-calling-convention.md)
- [`02b-vm-function-values-and-closures.md`](02b-vm-function-values-and-closures.md)
- [`03-memory-stack-heap-and-allocation.md`](03-memory-stack-heap-and-allocation.md)
- [`09a-coroutines-and-cooperative-scheduling.md`](09a-coroutines-and-cooperative-scheduling.md)
- [`16-host-abi-and-syscalls.md`](16-host-abi-and-syscalls.md)
- [`16a-syscall-policies.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`](../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`](02a-vm-values-and-calling-convention.md) defines slot values, tuples, frames, and return-slot semantics.
- [`02b-vm-function-values-and-closures.md`](02b-vm-function-values-and-closures.md) defines closure representation and function-value behavior.
- [`03-memory-stack-heap-and-allocation.md`](03-memory-stack-heap-and-allocation.md) defines stack/heap, handles, object layout, and GC.
- [`09-events-and-concurrency.md`](09-events-and-concurrency.md) defines events, timers, and the frame boundary model.
- [`09a-coroutines-and-cooperative-scheduling.md`](09a-coroutines-and-cooperative-scheduling.md) defines coroutine lifecycle and scheduling.
- [`16-host-abi-and-syscalls.md`](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.