ADR-0029: CoreVM0 Bounded Typed Program Representation

Status: accepted; instruction-only admission superseded by ADR-0030
Date: 2026-07-27

Context

The P1 lighthouse requires a definitional stack-bytecode interpreter in the frozen Core-N0 P1V0 semantics. P1V0 has read-only Array<F64>, Tuple, and Sum, but no general byte array, recursive data type, dynamic tuple projection, or untyped value.

The representation must support real opcode dispatch and static-program specialization without adding a host pointer, Rust object, external runtime, or manually replacing the interpreter with the expected loop.

Options considered

Option	Benefit	Cost
Host-side bytecode object	Easy seed implementation	Not a Core value; invalid P1 provenance
Encode opcodes as `Array<F64>`	Existing aggregate	No exact typed instruction fields; `ArrayGetF64` is effectful and denied at specialization time
Recursive instruction list	Natural interpreter data	Core-N0 v0.1 has no recursive type
One Core function per decoded instruction	Simple control flow	Program is already manually decoded; weak dispatch-erasure evidence
Fixed-capacity Tuple of Instruction Sum values	Uses existing typed Core values; every projection index is static in the interpreter	Interpreter shape and capacity are versioned; fetch is a bounded decision tree

Decision

CoreVM0 v0 uses a fixed-capacity typed program image:

ProgramImage<N> = Tuple<Instruction, ... N times>

Instruction is one canonical Sum with exactly the opcode variants in the P1 lighthouse contract. Immediate fields are typed I64/F64; indexes and branch targets are non-negative I64 values admitted by the bytecode verifier.

The first frozen capacity is 64 instructions, enough for the canonical branch_mix_kernel image. Capacity, instruction schema, numeric modes, stack/local limits, and program encoding are versioned and hashed.

The generic Core interpreter uses:

a bounded static projection/selection tree to fetch one instruction from the program tuple;
a tagged VmValue Sum for Bool, I64, F64, and read-only Array<F64>;
fixed bounded stack and local state threaded through tail recursion;
an explicit program counter and step budget;
wrapping I64 Add/Sub for CoreVM0 v0;
strict Core binary64 Add/Sub and comparisons;
typed bounds failure for ArrayGetF64.

Before Core elaboration or execution, a deterministic verifier proves:

instruction/immediate validity
branch-target validity
exact stack type at every CFG entry
equal stack shape at joins
definite local initialization
ReturnF64 result shape
no reachable fallthrough
declared max-stack exactness
canonical reachability

The initial Rust seed implements the bytecode schema, verifier, canonical hash, evaluator, and differential corpus first. The next slice constructs the same interpreter as a verified Core-N0 artifact. Seed execution alone is not CoreVM0 completion and cannot satisfy P1.

Rationale

Tuple/Sum values stay inside the already hashed P1V0 semantic domain.
A generic bounded fetch/dispatch path exists and can later be certified absent from Residual Core.
Static program identity includes instruction order, immediates, layout, and capacity without relying on host memory layout.
A typed CFG verifier prevents runtime “wrong stack tag” behavior from becoming part of the valid-program semantics.

Trade-offs

The first interpreter has a fixed maximum program and state size.
Core generation is verbose because P1V0 has no dynamic tuple projection.
The current R0-B2 evaluator halts at dynamic control and does not yet residualize both dynamic branches. CoreVM0 construction therefore does not imply dispatch erasure; a later evidence-gated residual-control extension is required.

Consequences

Positive: the lighthouse gains an exact typed bytecode and state contract that can be represented in frozen Core-N0 without an external dependency.

Negative: extending capacity or instruction/value variants changes the interpreter identity and requires new locked vectors.

Non-claims

The Rust seed model, generic CoreVM0 artifact, or first residual fragment is not Futamura P1. P1 remains closed until dynamic-control specialization, structural erasure, standalone native emission, Gate A, Gate B, and Gate C all pass.

Revisit trigger

Changing program capacity, instruction variants, numeric mode, stack/local limits, fetch representation, or adding a recursive/static-data Core feature requires a new ADR and identity version.