GitHub

CoreVM0 Definitional Core Artifact Contract

Status: implemented and bounded-differential validated
Stage: Roadmap Stage 3 / pre-P1 semantic gate
Decision: ADR-0030
Construction version: 1.0.0

1. Purpose

This package defines the generic CoreVM0 interpreter as an ordinary verified Core-N0 P1V0 artifact and compares it with the Rust semantic seed.

It closes the semantic bridge from the CoreVM0 bytecode contract into Core-N0. It is a precondition for specializing the interpreter, not a Residual-Core Gate A result and not a Futamura projection.

2. Identity taxonomy

The following identities are different and must not be substituted:

Core-N0 P1V0 interpreter-semantics hash
CoreVM0 bytecode program hash
CoreVM0 full ProgramImage hash
definitional CoreVM0 artifact semantic hash

For the frozen branch_mix_kernel:

CoreVM0 program hash =
9770cd0fb20fefaebba063674e02b1881173a817b73b9f910c9ba8e025a9b2d5

legacy live-instruction image hash =
9ced2bbdcc19b5225f7e15a5d30525ffd8424794e8ccc5b40c2402a3f11856c9

full ProgramImage v1 hash =
732cc709778d757988b34b1efcf5c376b1b1443e6cebec3bb61375d1f8fa1142

definitional artifact hash for the (Array<F64>, I64) argument shape =
9ef102a420024b350e46499c83de65244ad5e1f47e006922443ab8b4d4fe3abe

The legacy image remains locked compatibility evidence. Only the full image is the Stage 3 static program value.

3. Full ProgramImage v1

The fixed ordinary Core value is:

(
  image_schema_major,
  image_schema_minor,
  image_schema_patch,
  argument_count,
  TypeSlot[8],
  local_count,
  TypeSlot[16],
  max_stack,
  instruction_count,
  InstructionSlot[64]
)
TypeSlot =
    Absent
  | Bool
  | I64
  | F64
  | ArrayF64

InstructionSlot =
    Padding
  | Present(Instruction)

Live slots form exact prefixes. Every later slot is canonical Absent or Padding. Instruction remains the exact 16-constructor Sum from the CoreVM0 nucleus contract.

corevm0_program_image accepts only VerifiedCoreVmProgram. verify_corevm0_program_image is the raw-input admission boundary: it re-verifies the bytecode, regenerates the whole image, and requires exact structural equality. A same-typed arbitrary Tuple/Sum that merely passes ordinary R0-A is not CoreVM0 evidence.

4. Opaque binding

build_definitional_corevm0:

  1. runs the CoreVM0 bytecode verifier;
  2. regenerates the canonical full image;
  3. constructs the generic artifact from the typed argument shape, not from opcode contents;
  4. seals the Core semantic hash;
  5. requires the ordinary Core verifier to accept it;
  6. binds the Core-N0 P1V0 interpreter-semantics hash and construction version;
  7. returns an opaque DefinitionalCoreVmArtifact.

The supported evaluator always supplies the package’s own image. Callers cannot replace its program, program hash, image hash, or Core runtime value. Serialized P1 admission must still use the raw-input verifier rather than trusting opacity in one Rust process.

5. Core entry and state

For the lighthouse:

execute(
  static ProgramImage,
  dynamic Array<F64>,
  dynamic I64 repetitions
) -> F64 ! Error<Bounds>

The interpreter body contains:

  • a separate dynamic pc and sp;
  • a balanced 64-slot static-projection fetch tree;
  • exhaustive InstructionSlot and 16-opcode dispatch cases;
  • a five-constructor runtime value Sum: Bool, I64, F64, ArrayF64, Uninitialized;
  • immutable 16-cell stack and local Tuples;
  • checked, balanced get/set selection helpers;
  • exact typed argument selection;
  • one proper-tail-recursive execution loop;
  • a non-returning fail-closed path for states impossible after bytecode verification.

No Core primitive, profile, schema feature, host pointer, Surface runtime, trace JIT, egg, or external compiler is added or called.

6. Genericity invariant

For verified programs P and Q with the same typed argument manifest:

hash(definitional_artifact(P))
=
hash(definitional_artifact(Q))

even when their instructions or immediates differ. Their CoreVM0 program and full-image hashes must differ.

This invariant prevents the Rust constructor from decoding branch_mix into one Core function per instruction. The generic artifact continues to fetch and dispatch at runtime.

7. Differential relation

For admitted programs and arguments that complete inside independently sufficient resource budgets:

normalize(evaluate_corevm0(seed, program, args))
=
normalize(evaluate_core(definitional_artifact, image, args))

Normalization preserves:

  • non-NaN F64 result bits, including signed zero;
  • NaN as the Core contract’s payload-unobservable NaN class;
  • typed Bounds outcome;
  • exact mapped Bounds effect trace;
  • operand and evaluation order;
  • canonical program identity.

Core-N0 Evaluation.steps counts Core terms and rvalues. Seed steps counts bytecode opcodes. They are deliberately not compared. The two external budgets must each fail closed; neither is a language input or a field in the P1 residual signature.

8. Evidence

naux-lang/tests/corevm0_program_image_v1.rs locks:

  • the full image shape, capacities, manifests, live prefixes, and padding;
  • the new image hash while preserving the legacy vector;
  • program/image mutation sensitivity;
  • raw-input re-verification and exact comparison;
  • canonical NaN-payload admission while preserving signed-zero distinction;
  • rejection of invalid bytecode and every full-image section mutation.

naux-lang/tests/corevm0_core_parity.rs locks:

  • ordinary Core verification and the definitional artifact hash;
  • all-16-opcode branch_mix smoke parity;
  • numeric/control edge cases including NaN, infinities, and signed zero;
  • a bounded exhaustive micro-domain;
  • a deterministic generated differential corpus;
  • wrapping I64 and branch-direction parity;
  • execution through instruction slot 63, argument slot 7, and stack/local slot 15;
  • typed Bounds outcome and exact effect trace;
  • deterministic repeated Core execution;
  • the genericity invariant under a valid instruction mutation;
  • structural presence of all 64 fetch projections and all 16 dispatch arms;
  • argument, artifact-hash, bytecode, and Core-budget fail-closed behavior;
  • admission of the full static image by the existing B0-D and R0-A gates.

This is bounded executable evidence, not an infinite-domain theorem or an implementation-diverse verified checker.

9. Remaining specialization gate

The generic artifact intentionally still contains bytecode fetch, opcode dispatch, tagged VM values, stack/local banks, and a dynamic program counter. Current R0 cannot erase them:

  • aggregate binding time joins dynamic payloads into their constructors;
  • dynamic control contaminates otherwise unchanged static arguments;
  • recursive call summaries are monovariant;
  • R0-B2 cannot enter a call with a dynamic result;
  • R0-C2 cannot residualize both dynamic branches.

The next ADR must jointly address partially-static aggregates, polyvariant specialization by static program counter, memoized recursive residual versions, mixed-result call unfolding, and dynamic-control residualization. Adding only one of those mechanisms is not sufficient.

10. Non-claims

This package does not erase dispatch, produce Residual Core or SSA, emit machine code, execute standalone, pass residual Gate A, satisfy performance Gates B/C, prove Futamura P1/P2, remove Rust/Cargo seed debt, establish Projection Birth, close third-party dependencies, or complete Nauxogenesis.