GitHub

CoreVM0 Semantic Nucleus Contract

Status: Rust seed model implemented and validated; definitional successor implemented under ADR-0030
Stage: Roadmap Stage 3 / P1 lighthouse preparation
Decision: ADR-0029

1. Purpose

This package freezes the typed bytecode, verifier, canonical identity, and reference execution semantics that the definitional CoreVM0 artifact must implement.

It is a bridge semantic seed, not the P1 interpreter artifact and not a projection.

2. Bytecode v1

The exact opcode set is:

ConstI64(i64)
ConstF64(f64)
LoadArg(index)
LoadLocal(index)
StoreLocal(index)
AddI64
SubI64
AddF64
SubF64
CmpLtI64
CmpGeI64
ArrayLenF64
ArrayGetF64
Jump(target)
JumpIfFalse(target)
ReturnF64

CoreVM0 v1 uses wrapping I64 Add/Sub, strict Core binary64 Add/Sub, exact I64 comparisons, left-to-right stack effects, and typed Bounds failure for ArrayGetF64.

Hard caps:

instructions <= 64
arguments    <= 8
locals       <= 16
stack slots  <= 16

3. Verified programs

verify_corevm0_program performs deterministic CFG dataflow and rejects:

  • unknown schema or empty/oversized envelopes;
  • invalid argument, local, or branch indexes;
  • stack underflow or opcode type mismatch;
  • unequal stack types at a CFG join;
  • local reads without definite initialization on every predecessor;
  • invalid ReturnF64 stack shape;
  • reachable fallthrough beyond the image;
  • missing reachable return;
  • unreachable instruction;
  • a declared max stack different from the computed exact maximum.

Only VerifiedCoreVmProgram enters the evaluator.

4. Reference evaluation

evaluate_corevm0:

  • checks exact argument arity and types;
  • executes one deterministic step per opcode;
  • fails closed on exact step-budget exhaustion;
  • preserves read-only array identity semantically;
  • returns only ReturnF64 or typed Bounds;
  • records Bounds in the effect trace;
  • never invokes the Surface VM, trace JIT, or a host compiler.

The evaluator is written with Rust/Cargo as seed infrastructure. It is an oracle for the upcoming Core-N0 interpreter, not final semantic authority.

5. Canonical program identity

The program encoding domain is:

NAUX:corevm0:program:v1\0

It covers schema, ordered argument/local types, exact max stack, instruction order, every immediate, branch target, and canonical F64 bits.

The frozen branch_mix_kernel vector is:

program_hash =
9770cd0fb20fefaebba063674e02b1881173a817b73b9f910c9ba8e025a9b2d5

6. Ordinary Core static image

A verified program maps to the existing P1V0 static domain as:

Tuple<Instruction Sum, ...>

The Instruction Sum has exactly 16 constructors in opcode order. Index and target immediates use exact I64 fields. No host pointer or Rust layout enters the value.

The frozen branch-mix Core specialization-value hash is:

core_image_hash =
9ced2bbdcc19b5225f7e15a5d30525ffd8424794e8ccc5b40c2402a3f11856c9

The image passes the ordinary B0 and R0-A Tuple/Sum static-slot admission boundary alongside dynamic Array<F64> and I64 repetition inputs.

7. Evidence

naux-lang/tests/corevm0_nucleus.rs covers:

  • every required opcode in the canonical branch-mix image;
  • locked program and Core-image hashes;
  • direct-oracle parity for empty input, zero/negative repetitions, signed zero, NaN, infinities, and non-vector lengths;
  • bounded exhaustive arrays of length zero through three;
  • a deterministic 256-vector generated corpus;
  • typed array-bounds outcomes and effect traces;
  • exact argument and step-budget rejection;
  • instruction/order/immediate/layout/numeric-bit hash mutation;
  • control, stack, local-initialization, reachability, and max-stack verifier mutations.

8. Successor gate

ADR-0030 closes the next package with a complete fixed-capacity ProgramImage, raw-input admission verifier, generic verified Core-N0 artifact, and bounded CoreVM0-vs-seed differential parity. Its normative contract is corevm0_core_artifact_contract.md.

The current R0 evaluator still cannot preserve partially-static aggregate constructors, build polyvariant static-PC loop versions, enter a call whose result is dynamic, or specialize both sides of dynamic control. A new ADR must address that complete set before dispatch erasure can be attempted.

9. Non-claims

This seed package by itself does not implement the definitional CoreVM0 interpreter. Its ADR-0030 successor does, but neither package implements Residual Core erasure, SSA/native lowering, standalone execution, Futamura P1/P2, Projection Birth, dependency closure, or Nauxogenesis.