prometeu-runtime/docs/pull-requests/PR-002-runtime-intrinsic-opcode-verification-and-dispatch.md

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:

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:

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