ADR-0030: CoreVM0 Full Program Image and Definitional Boundary

Status: accepted
Date: 2026-07-28
Supersedes: the instruction-only admission interpretation of ADR-0029

Context

ADR-0029 established a bounded Tuple/Sum representation for CoreVM0 instructions. The first Rust seed maps only the program’s live instruction sequence into the ordinary specialization-value domain. Its schema version, argument and local type manifests, exact stack bound, and instruction count remain bound by corevm0_program_hash, but are not themselves present in that static Core value.

That split is adequate for checking that instructions can be represented, but it is not a sufficient Stage 3 admission boundary. A static value could retain the same instruction Tuple while losing or replacing part of the verified manifest. The generic definitional interpreter must also be independent of the instruction contents; generating one decoded Core function per bytecode instruction would manually perform the specialization that P1 is meant to demonstrate.

The frozen P1V0 profile has no recursive data type, dynamic tuple projection, mutable array, or untyped value. It does have fixed Tuple/Sum values, direct and proper tail calls, typed numeric primitives, read-only Array<F64>, and typed Bounds effects.

Options considered

Decision

Introduce CoreVM0 ProgramImage v1, one fixed-shape ordinary P1V0 value:

(
  schema_major,
  schema_minor,
  schema_patch,
  argument_count,
  argument_type_slots[8],
  local_count,
  local_type_slots[16],
  max_stack,
  instruction_count,
  instruction_slots[64]
)

Each type slot is a canonical Sum with Absent, Bool, I64, F64, and ArrayF64 constructors. Each instruction slot is Padding or Present(Instruction), preserving the exact 16-constructor Instruction Sum. Slots below the declared counts are present and exact; later slots are canonical padding. The full image is generated only from a verified CoreVmProgram. Both its ordinary specialization-value hash and the existing canonical CoreVM0 program hash are retained as evidence.

Keep the previous live-length instruction Tuple API as compatibility evidence, but it is no longer the complete Stage 3 program admission value.

Build one deterministic P1V0 Core artifact whose shape and semantic hash do not depend on bytecode contents. Its entry receives the full image followed by the exact typed argument manifest. For the lighthouse shape:

ProgramImage v1     // static for P1
Array<F64> input    // dynamic
I64 repetitions     // dynamic

The artifact uses:

• a dynamic program counter kept separate from state;
• a generated bounded selection tree over the 64-instruction Tuple;
• a canonical Instruction Sum case for opcode dispatch;
• a RuntimeValue Sum for Bool, I64, F64, ArrayF64, and an internal Uninitialized sentinel;
• exact typed entry arguments and a generated checked argument selector;
• immutable 16-cell Tuple banks for stack and locals;
• generated checked get/set helpers rather than host indexing;
• proper tail recursion for the VM loop;
• wrapping I64 arithmetic and strict F64 primitives already frozen in P1V0;
• the ordinary Bounds effect for ArrayGetF64;
• a non-returning fail-closed Core path for a verified-program invariant failure.

An opaque bound package owns the verified source program, full image, program/image identities, and generic Core artifact. The public definitional evaluation path supplies the package’s own image; it does not accept a caller-provided replacement. The generic Core artifact remains inspectable for B0/R0, but using an arbitrary same-typed value does not constitute CoreVM0 evidence or a P1 claim.

CoreVM0 execution steps and Core-N0 interpreter steps are different counters. The Rust seed’s max_steps and Core-N0’s EvaluationBudget are external resource envelopes, not language inputs and not observable successful-result semantics. Parity compares completed executions under sufficient independent budgets. Exhaustion must fail closed on each side, but the two counters are not equated or inserted into the P1 residual signature.

Rationale

1. The static P1 input now carries every field that the bytecode verifier and canonical program identity depend on.
2. One artifact for all admitted programs proves that its opcode dispatch is generic rather than decoded from branch_mix.
3. Generated selection trees use only already frozen P1V0 semantics and keep the dynamic program counter visible for the later residual-control ADR.
4. The opaque binding prevents an accidental same-type image substitution in the supported parity path.
5. Keeping resource budgets outside the Core term avoids adding a dynamic counter and branch that are absent from the intended residual program.

Trade-offs

• The full image and three fixed state banks are larger than the live lighthouse state.
• Tuple updates copy a bounded logical bank in the seed interpreter.
• Invalid same-typed images remain representable as ordinary Core values; only the verified binding makes them CoreVM0-admitted inputs.
• The generic artifact is an intentionally slow semantic definition, not a performance implementation.
• Adding the internal Uninitialized constructor makes impossible verified states explicit but increases dispatch structure.

These costs are accepted because this package establishes semantics and provenance. P1 must later erase the static dispatch and state scaffolding rather than benchmarking the generic artifact.

Consequences

Positive:

• manifest, capacity, live length, and every instruction are one static value;
• the definitional artifact can be structurally identical across different verified programs with the same typed argument shape;
• bounded selectors and state transitions are dependency-free Core-N0;
• budget, Bounds, numeric, and opcode parity can be tested independently.

Negative:

• the old instruction-image hash remains a compatibility vector while the new full-image hash becomes the Stage 3 vector;
• Core evaluation is much more expensive than direct Rust seed execution;
• future mixed-call and dynamic-control residualization must understand the generated helper calls and terminal branch structure.

Mitigation:

• lock both identities and test every image field mutation;
• cap all banks at existing CoreVM0 limits;
• use bounded differential corpora before running the larger lighthouse corpus;
• defer every dispatch-erasure change to a separate ADR after parity is green.

Non-claims

This decision and its generic artifact do not implement residual dispatch erasure, native lowering, standalone execution, Gate A against Residual Core, Futamura P1/P2, Projection Birth, dependency closure, performance leadership, or Nauxogenesis.

Revisit trigger

Changing an image field, tag, padding rule, capacity, RuntimeValue constructor, external-budget rule, or selection/state representation requires a new image version and ADR. Mixed-call unfolding or residualizing both sides of dynamic control requires a separate ADR and cannot silently amend this decision.