169 lines
4.6 KiB
Markdown
169 lines
4.6 KiB
Markdown
# PR-002 Runtime INTRINSIC Opcode, Verification, and Dispatch
|
|
|
|
## Goal
|
|
|
|
Add a dedicated runtime execution path for VM-owned intrinsics using the
|
|
metadata introduced in PR-001.
|
|
|
|
This PR should establish that intrinsic execution is a first-class VM path,
|
|
separate from host-backed syscall execution.
|
|
|
|
## Why
|
|
|
|
The runtime currently has a conceptual host-backed path centered on `SYSCALL`.
|
|
Builtin semantics cannot be layered cleanly on top of that path because:
|
|
|
|
- intrinsic ownership is VM-owned, not host-owned,
|
|
- intrinsic execution must not require host resolution,
|
|
- intrinsic execution must not depend on capabilities,
|
|
- and verifier stack effects must come from builtin layout metadata.
|
|
|
|
The runtime therefore needs its own instruction and dispatch path.
|
|
|
|
## MVP Decision
|
|
|
|
This PR should implement direct final-form execution:
|
|
|
|
```text
|
|
INTRINSIC <id>
|
|
```
|
|
|
|
Do not implement `INTRCALL` in this PR unless the runtime already has a clear
|
|
preload declaration mechanism that can be reused without coupling to `SYSC`.
|
|
|
|
The intent is:
|
|
|
|
- keep the runtime simple,
|
|
- let the frontend eventually emit final intrinsic ids for a selected VM line,
|
|
- and avoid pulling loader complexity into the first implementation.
|
|
|
|
## Scope
|
|
|
|
Add:
|
|
|
|
- runtime opcode support for `INTRINSIC <id>`,
|
|
- verifier support for intrinsic stack effects,
|
|
- execution dispatch by intrinsic id,
|
|
- trap behavior for unknown intrinsic ids,
|
|
- and tests proving separation from the syscall pipeline.
|
|
|
|
Do not add host loader changes in this PR.
|
|
|
|
## Required Changes
|
|
|
|
### 1. Bytecode/ISA support
|
|
|
|
Introduce a dedicated intrinsic opcode in the runtime bytecode interpreter.
|
|
|
|
Normative behavior:
|
|
|
|
- decode `INTRINSIC <id>`,
|
|
- lookup intrinsic metadata by numeric id,
|
|
- verify or assume verifier-proven stack shape,
|
|
- execute runtime-owned implementation,
|
|
- push results back according to intrinsic return layout.
|
|
|
|
### 2. Verifier support
|
|
|
|
The verifier must derive intrinsic stack effects from runtime intrinsic metadata.
|
|
|
|
Required behavior:
|
|
|
|
- lookup intrinsic meta by id,
|
|
- compute argument slot width from flattened `arg_layout`,
|
|
- compute result slot width from flattened `ret_layout`,
|
|
- reject underflow,
|
|
- reject invalid slot shape,
|
|
- and preserve existing verifier guarantees for control flow.
|
|
|
|
Examples:
|
|
|
|
- `vec2.dot(vec2, vec2) -> float` becomes `pop 4, push 1`
|
|
- `vec2.length(vec2) -> float` becomes `pop 2, push 1`
|
|
|
|
### 3. Trap behavior
|
|
|
|
Add deterministic failure for:
|
|
|
|
- unknown intrinsic id,
|
|
- malformed intrinsic metadata,
|
|
- verifier/runtime disagreement on intrinsic width,
|
|
- and execution-time misuse that escapes verifier guarantees.
|
|
|
|
If trap enums exist, add a runtime-specific invalid intrinsic trap rather than
|
|
reusing invalid syscall traps.
|
|
|
|
### 4. Dispatch separation
|
|
|
|
Ensure the interpreter or executor has two clearly distinct paths:
|
|
|
|
- `SYSCALL <id>` for host-backed services
|
|
- `INTRINSIC <id>` for VM-owned semantics
|
|
|
|
These paths must not share registry lookup semantics.
|
|
|
|
## Suggested Runtime Shape
|
|
|
|
Use a structure roughly like:
|
|
|
|
```text
|
|
execute_intrinsic(id, stack, runtime_ctx) -> Result<(), Trap>
|
|
```
|
|
|
|
where:
|
|
|
|
- `stack` is mutated using metadata-defined widths,
|
|
- `runtime_ctx` is VM-internal context only,
|
|
- and no host syscall registry access occurs.
|
|
|
|
If an execution table already exists for opcodes, add intrinsic dispatch as a
|
|
parallel branch rather than as a host-call subtype.
|
|
|
|
## Acceptance Criteria
|
|
|
|
1. Runtime recognizes and executes `INTRINSIC <id>`.
|
|
2. Verifier derives stack effects from intrinsic metadata rather than hardcoded arity alone.
|
|
3. Unknown intrinsic ids fail deterministically.
|
|
4. `INTRINSIC` does not route through host binding, loader syscall resolution, or capability checks.
|
|
5. `SYSCALL` behavior remains unchanged.
|
|
6. Tests demonstrate that intrinsic execution and syscall execution are distinct runtime paths.
|
|
|
|
## Test Cases
|
|
|
|
### Positive
|
|
|
|
- execute `vec2.dot` over two canonical `vec2` values and obtain one float result
|
|
- execute `vec2.length` over one canonical `vec2` value and obtain one float result
|
|
|
|
### Verification
|
|
|
|
- verifier accepts a correct stack program using `INTRINSIC <vec2.dot>`
|
|
- verifier rejects a program with insufficient stack width for `INTRINSIC <vec2.dot>`
|
|
|
|
### Separation
|
|
|
|
- `SYSCALL` still resolves and executes host-backed operations as before
|
|
- invalid intrinsic id produces intrinsic-specific failure, not syscall failure
|
|
|
|
## Out of Scope
|
|
|
|
- frontend parser/lowering changes
|
|
- preload `INTRCALL` resolution
|
|
- builtin constant source lowering
|
|
- new host bindings
|
|
|
|
## Notes for Follow-up PRs
|
|
|
|
The next PR should populate the registry and executor with the first builtin
|
|
set:
|
|
|
|
- `color`
|
|
- `vec2`
|
|
- `pixel`
|
|
|
|
and with first intrinsic implementations:
|
|
|
|
- `vec2.dot`
|
|
- `vec2.length`
|
|
- optionally `vec2.distance`
|