176 lines
5.4 KiB
Markdown
176 lines
5.4 KiB
Markdown
# Runtime Traps v0 — Prometeu VM Specification
|
|
|
|
> **Status:** Proposed (requires explicit owner approval)
|
|
>
|
|
> **Scope:** Prometeu VM / PBS v0 execution model
|
|
|
|
---
|
|
|
|
## 1. Motivation
|
|
|
|
Prometeu aims to be a **deterministic, industrial-grade virtual machine**.
|
|
To achieve this, execution errors that are:
|
|
|
|
* caused by **user programs**,
|
|
* predictable by the execution model,
|
|
* and recoverable at the tooling / host level,
|
|
|
|
must be **explicitly represented** and **ABI-stable**.
|
|
|
|
This specification introduces **Runtime Traps** as a *formal concept*, consolidating behavior that already existed implicitly in the VM.
|
|
|
|
---
|
|
|
|
## 2. Definition
|
|
|
|
A **Runtime Trap** is a **controlled interruption of program execution** caused by a semantic violation detected at runtime.
|
|
|
|
A trap:
|
|
|
|
* **terminates the current execution frame** (or program, depending on host policy)
|
|
* **does not corrupt VM state**
|
|
* **returns structured diagnostic information** (`TrapInfo`)
|
|
* **is deterministic** for a given bytecode + state
|
|
|
|
A trap is **not**:
|
|
|
|
* a debugger breakpoint
|
|
* undefined behavior
|
|
* a VM panic
|
|
* a verifier/load-time error
|
|
|
|
---
|
|
|
|
## 3. Trap vs Other Failure Modes
|
|
|
|
| Category | When | Recoverable | ABI-stable | Example |
|
|
| ------------------ | ---------------------- | ----------- | ---------- | -------------------------------- |
|
|
| **Verifier error** | Load-time | ❌ | ❌ | Stack underflow, bad CFG join |
|
|
| **Runtime trap** | Execution | ✅ | ✅ | OOB access, invalid local |
|
|
| **VM panic** | VM invariant violation | ❌ | ❌ | Handler returns wrong slot count |
|
|
| **Breakpoint** | Debug only | ✅ | ❌ | Developer inspection |
|
|
|
|
---
|
|
|
|
## 4. Trap Information (`TrapInfo`)
|
|
|
|
All runtime traps must produce a `TrapInfo` structure with the following fields:
|
|
|
|
```text
|
|
TrapInfo {
|
|
code: u32, // ABI-stable trap code
|
|
opcode: u16, // opcode that triggered the trap
|
|
pc: u32, // program counter (relative to module)
|
|
message: String, // human-readable explanation (non-ABI)
|
|
}
|
|
```
|
|
|
|
### ABI Guarantees
|
|
|
|
* `code`, `opcode`, and `pc` are ABI-relevant and stable
|
|
* `message` is diagnostic only and may change
|
|
|
|
---
|
|
|
|
## 5. Standard Trap Codes (v0)
|
|
|
|
### 5.1 Memory & Bounds
|
|
|
|
| Code | Name | Meaning |
|
|
| -------------------- | ------------- | ------------------------------ |
|
|
| `TRAP_OOB` | Out of bounds | Access beyond allowed bounds |
|
|
| `TRAP_INVALID_LOCAL` | Invalid local | Local slot index out of bounds |
|
|
|
|
### 5.2 Execution & Types
|
|
|
|
| Code | Name | Meaning |
|
|
| ------------------------- | -------------------- | ------------------------------------------------------ |
|
|
| `TRAP_ILLEGAL_INSTRUCTION`| Illegal instruction | Unknown/invalid opcode encountered |
|
|
| `TRAP_TYPE` | Type violation | Type mismatch for operation or syscall argument types |
|
|
| `TRAP_DIV_ZERO` | Divide by zero | Division/modulo by zero |
|
|
| `TRAP_INVALID_FUNC` | Invalid function | Function index not present in function table |
|
|
| `TRAP_BAD_RET_SLOTS` | Bad return slots | Stack height mismatch at return |
|
|
|
|
### 5.3 System
|
|
|
|
| Code | Name | Meaning |
|
|
| ---------------------- | --------------- | --------------------------------------- |
|
|
| `TRAP_INVALID_SYSCALL` | Invalid syscall | Unknown syscall ID |
|
|
| `TRAP_STACK_UNDERFLOW` | Stack underflow | Missing arguments for syscall or opcode |
|
|
|
|
> This list is **closed for PBS v0** unless explicitly extended.
|
|
|
|
---
|
|
|
|
## 6. Trap Semantics
|
|
|
|
### 6.1 Execution
|
|
|
|
When a trap occurs:
|
|
|
|
1. The current instruction **does not complete**
|
|
2. No partial side effects are committed
|
|
3. Execution stops and returns `TrapInfo` to the host
|
|
|
|
### 6.2 Stack & Frames
|
|
|
|
* Operand stack is left in a **valid but unspecified** state
|
|
* Call frames above the trapping frame are not resumed
|
|
|
|
### 6.3 Host Policy
|
|
|
|
The host decides:
|
|
|
|
* whether the trap terminates the whole program
|
|
* whether execution may be restarted
|
|
* how the trap is surfaced to the user (error, log, UI, etc.)
|
|
|
|
---
|
|
|
|
## 7. Verifier Interaction
|
|
|
|
The verifier **must prevent** traps that are statically provable, including:
|
|
|
|
* stack underflow
|
|
* invalid control-flow joins
|
|
* invalid syscall IDs
|
|
* incorrect return slot counts
|
|
|
|
If a verifier rejects a module, **no runtime traps should occur for those causes**.
|
|
|
|
---
|
|
|
|
## 8. What Is *Not* a Trap
|
|
|
|
The following are **VM bugs or tooling errors**, not traps:
|
|
|
|
* handler returns wrong number of slots
|
|
* opcode implementation violates `OpcodeSpec`
|
|
* verifier and runtime disagree on stack effects
|
|
|
|
These must result in **VM panic**, not a trap.
|
|
|
|
---
|
|
|
|
## 9. Versioning Policy
|
|
|
|
* Trap codes are **ABI-stable within a major version** (v0)
|
|
* New trap codes may only be added in a **new major ABI version** (v1)
|
|
* Removing or reinterpreting trap codes is forbidden
|
|
|
|
---
|
|
|
|
## 10. Summary
|
|
|
|
Runtime traps are:
|
|
|
|
* an explicit part of the Prometeu execution model
|
|
* deterministic and ABI-stable
|
|
* reserved for **user-program semantic errors**
|
|
|
|
They are **not** debugging tools and **not** VM panics.
|
|
|
|
This spec formalizes existing behavior and freezes it for PBS v0.
|
|
|
|
---
|