Typed Core NAUX v0.1

Status: accepted architecture; bounded Stage 1 validated; Stage 2 R0-D validated; Stage 3 definitional CoreVM0 validated
Schema name: core-n0
Schema version: 0.1.0

Implementation status:

implemented: std-only Rust seed schema for the P1V0, P1V1, P1V2, P1V3, P1V4, and P1V5 profiles;
implemented: deterministic semantic encoding, SHA-256 hash, fail-closed verifier, and verified-artifact interpreter entry;
implemented: scalar/tuple/sum values, direct calls, tail calls, let, if, exhaustive case, explicit numeric modes, and read-only Array<F64>;
implemented: deterministic evaluation budgets and typed overflow/bounds outcomes;
implemented: T2A deterministic elaboration for the admitted pure scalar Assign/If Surface subset, exact typed input binding, independent Core verification, fixed semantic-hash evidence, and bridge/Core differential parity;
implemented: T2B annotated closed direct functions, forward/recursive calls, proper tail calls, exact scalar signatures, global elaboration budgets, stable-hash evidence, and bridge/Core differential parity;
implemented: P1V1 invocation-local logical store, lexical region scope, non-escaping shared scalar references, exact State<rho>/Alloc<rho> checking, stable-hash evidence, and freshness/alias/order rejection corpus;
implemented: P1V2 bounded existential closures with ordered tuple environments, exact construction/call/effect verification, live reference capture, alias-visible shared-store calls, bounded recursion, no escape, and stable-hash evidence;
implemented: P1V3 typed user operations and linear lexical handlers with explicit captures, affine implicit resumption, dynamic call/closure effect subtraction, forwarding, unhandled outcomes, and stable-hash evidence;
implemented: P1V4 direct affine Unique scalar ownership with repeated load/store borrows, single move through Use/direct call/tail call, branch-local dataflow, containment/escape rejection, and stable-hash evidence;
implemented: P1V5 one-in/one-out anchored ownership return with return-as-move, caller rebinding, branch/tail return, same-region replacement, closed-region rejection, and stable-hash evidence;
pending: escaping/general store semantics, general borrowing, aggregate ownership, escaping/general closures, first-class/multi-shot handlers, region polymorphism, and full effect rows.

The encoding contract is core_n0_semantic_encoding_v1.md, and the admitted Surface boundary is surface_core_t2_contract.md, with the direct function extension in surface_core_t2b_contract.md. The bounded logical-store profile is fixed by core_store_p1v1_contract.md, and bounded existential closures are fixed by core_closure_p1v2_contract.md, and linear handlers are fixed by core_handler_p1v3_contract.md, and bounded affine ownership is fixed by core_unique_p1v4_contract.md, and bounded ownership return is fixed by core_ownership_return_p1v5_contract.md. The bounded Stage 1 exit is accepted in stage1_exit_audit.md. The CoreVM0 seed and definitional artifact are fixed by corevm0_nucleus_contract.md and corevm0_core_artifact_contract.md. The active next boundary is the specializer extension required by p1_lighthouse_contract.md.

1. Purpose

Core-N0 is the canonical semantic language used by:

the definitional interpreter;
binding-time analysis;
partial evaluation and residualization;
translation validation;
formal models and independent checkers.

It is intentionally smaller than Surface NAUX and higher-level than SSA. Surface syntax may evolve without changing Core semantics. Machine concerns may evolve without entering the semantic kernel.

2. Design invariants

Call-by-value.
Left-to-right evaluation.
Typed before evaluation or residualization.
A-normal form: non-trivial intermediate computations are named.
Local bindings are immutable; mutation occurs only through explicit store operations.
Effects and logical lifetime regions are explicit.
No implicit fallthrough, coercion, destructor, finalizer, or physical address.
No phi nodes, dominance, registers, stack slots, ABI, or instruction encoding.
Every serialized program has a deterministic semantic hash.

3. Types

τ ::=
    Unit
  | Bool
  | I64
  | F64
  | Text
  | Bytes
  | Tuple<τ...>
  | Sum<Name { Constructor(τ...)... }>
  | Array<ρ, μ, τ>
  | Ref<ρ, μ, τ>
  | Function<(τ...), ε, τ>
  | Closure<(τ...), ε, τ>

μ ::= Read | Unique | Shared

Text and Bytes are semantic primitives with versioned operations. Higher collections such as maps, graphs, sets, and priority queues are library or opaque ADT layers, not new kernel mechanisms.

Any, host pointers, Rc, Rust enums, and host collection types do not appear in Core-N0.

4. Functions and closures

A direct function has a stable FunctionId, typed parameters, an effect row, and a result type.

The behavioral closure type is:

Closure<(Args...), Effects, Result>

After closure conversion its internal representation is:

∃Env. (
    FunctionId<(Env, Args...), Effects, Result>,
    Env
)

The verifier must prove that the packed environment type matches the selected function. The existential representation is internal; it is not required in Surface NAUX syntax.

P1V0 and P1V1 do not admit closure creation or closure calls. P1V2 admits PackClosure and CallClosure with a canonical ordered tuple environment. Closure values remain local to one function invocation; neither closure nor reference values may cross results, and closures may not cross parameters. A captured reference must be active, and its call borrows the creator’s logical store.

5. Terms

Illustrative canonical form:

program  ::= declarations entry
function ::= fn id type_params region_params (params) ! effects -> type = term

term ::=
    let x: τ = atom in term
  | let x: τ = primitive(args) in term
  | let x: τ = call function(args) in term
  | let x: τ = call_closure closure(args) in term
  | if value then term else term
  | case value of Constructor(bindings) => term ...
  | perform Effect.operation(args) as x in term
  | handle term with handler
  | tailcall function(args)
  | return value

atom ::= literal | local | tuple | constructor | function_ref | closure_pack

Surface loops elaborate to tail recursion in Core-N0. A later lowering may introduce CFG blocks and block parameters before SSA construction.

6. Evaluation

The Core interpreter evaluates:

⟨term, environment, logical_store, handlers⟩
    ⇓
⟨result, logical_store', effect_trace⟩

Evaluation order is left-to-right. A result is either:

Return(value)
Error(error_value)

Host panic, host allocation failure, or host undefined behavior is never a valid Core result.

7. Numeric semantics

I64

Core has no ambiguous integer arithmetic opcode. Operations name their mode:

i64.add.checked
i64.add.wrap
i64.add.saturating
i64.sub.checked
i64.sub.wrap
i64.mul.checked
i64.mul.wrap

Checked operations return a typed error/result rather than causing undefined behavior. Surface elaboration chooses a mode explicitly. A proof-backed pass may replace checked arithmetic with a cheaper operation only when overflow is impossible for the exact program point.

F64

IEEE-754 binary64.
Left-to-right evaluation.
No reassociation, contraction, reciprocal approximation, or fast-math by default.
NaN is unordered and unequal, including to itself.
+0.0 and -0.0 compare equal but retain their IEEE behavior in operations.
NaN payload and physical bit pattern are not observable in Core-N0 v0.1.
Relaxed numeric modes require a future explicit contract and distinct benchmark baselines.

8. Effects

An effect row is a closed or extensible set:

ε ::= Pure | { EffectName<parameters>... | effect_variable }

Initial semantic effects:

State<ρ>
Alloc<ρ>
Error<E>
IO
FFI<capability>
UnsafeMemory<capability>

A known handler may be specialized. An unknown handler or dynamic effect operation is residualized.

P1V3 implements the first bounded handler subset. Operation IDs carry exact inline signatures. Handler environments are explicit, clauses execute outside their selected boundary for forwarding, and a successful clause result resumes the structural continuation exactly once. Typed error or unhandled propagation resumes it zero times. The continuation is not yet a first-class Core value.

Static evaluation is restricted to:

pure computation;
specializer-owned internal allocation;
immutable static program reads;
bounded static control flow.

IO, FFI, time, randomness, environment access, external state, and nondeterminism are forbidden during default specialization.

9. Logical regions

ρ is logical lifetime and ownership evidence. It does not name a physical allocator.

Core-N0 v0.1 supports:

lexical region ρ in term;
simple region parameters;
alloc<ρ>;
no-escape verification;
region-contained cycles;
acyclic escaping ownership.

The implemented P1V1 subset currently covers the first four items only for non-escaping shared scalar cells. Region-contained cycles and acyclic escaping ownership remain architectural targets, not implemented claims.

The implemented P1V4 subset adds direct non-escaping unique scalar cells. Its verifier tracks whether each owner is live or moved independently of Rust ownership. Load/store borrow; Use, direct call, and tail call move. Unique owners cannot yet occur in aggregates, captures, entry parameters, or results.

The implemented P1V5 subset permits one internal direct unique result when exactly one matching direct unique parameter anchors the caller-owned region. Return moves the owner. A successful call binds the returned or fresh same-region replacement owner; error paths return none. Entry and unanchored results remain rejected.

A backend may choose registers, scalar replacement, stack, arena, region heap, or general heap when that choice preserves observable behavior.

General region polymorphism, weak references, and general shared escaping cycles are outside v0.1.

10. Identity and mutation

The logical store maps fresh, opaque locations to values. Two references alias when they carry the same logical location.

Observable:

freshness;
alias-visible mutation;
effect order;
explicit resource lifecycle.

Not observable:

numeric address;
physical placement;
RC traffic;
internal reclamation time;
object movement;
scalar replacement.

Core-N0 v0.1 has no same_identity, address-to-integer conversion, weak reference, implicit destructor, or finalizer. Identity can be observed only indirectly through behavior such as mutation through aliases.

11. Unsafe memory and FFI

Raw operations live behind typed capabilities:

Ptr<AddressSpace, Mutability, T>
raw_load(capability, ptr)
raw_store(capability, ptr, value)
raw_offset(capability, ptr, offset)
foreign_call(contract_hash, capability, args)

They carry UnsafeMemory or FFI effects. The contract defines ABI, ownership, lifetime, mutation, errors, threading, callbacks, and hidden-state dependencies.

FFI is opaque to specialization unless its contract proves the relevant property. A pure foreign operation must also be independent of time, randomness, locale, thread-local state, and hidden mutable state.

12. Binding-time judgment

Binding time is not a runtime type:

Γs ; Γd ⊢ expression : τ @ b ! ε
b ::= Static | Dynamic
Static ≤ Dynamic

Join:

join(Static, Static)   = Static
join(Static, Dynamic)  = Dynamic
join(Dynamic, Static)  = Dynamic
join(Dynamic, Dynamic) = Dynamic

Soundness requirements:

a static expression has no free dynamic dependency;
a default static expression performs no observable effect;
a dynamic condition makes the selected computation dynamic unless both residual branches can be emitted safely;
recursion and static unfolding obey declared budgets.

Annotations constrain inference:

static
dynamic
specialize
no_specialize
specialization_budget

Budget and policy do not change program semantics.

13. Verification

Before interpretation, specialization, or lowering, the verifier checks:

unique IDs and deterministic ordering;
type correctness;
constructor and pattern exhaustiveness;
function and closure signature compatibility;
effect-row correctness;
region lifetime and no-escape rules;
capability use;
ANF binding and scope;
binding-time evidence when present;
schema version and semantic hash.

Malformed Core fails closed.

Artifact identity and interpreter-semantics identity are separate:

semantic_hash(program)
interpreter_semantics_hash(profile)

Semantic Identity Encoding v1 locks P1V0–P1V5 independently of Rust source layout. The accepted bounded Stage 1 evidence matrix is stage1_exit_audit.md. Binding-time evidence is not part of the runtime type system. B0-A now validates the exact P1V0 request, policy, entry manifest, provenance hashes, and budgets. B0-B assigns stable intraprocedural node judgments with conservative control contamination and effect eligibility. B0-C adds direct/tail-call summaries, incoming-control flow, deterministic recursive convergence, and cumulative budgets. B0-D seals canonical evidence and independently replays it against the verified source and request. Complete B0 is validated; R0-A static-value/request identity is implemented and validated. R0-B1/R0-B2 effect-safe bounded static evaluation, R0-C1/R0-C2 verified residual generation, and R0-D sealed regenerative validation are implemented and validated. The generic CoreVM0 P1V0 artifact and its full static ProgramImage are also bounded-differential validated. Dispatch erasure remains closed pending partially-static aggregates, polyvariant loop specialization, mixed-result unfolding, and dynamic-control residualization.

14. P1 admitted subsets

P1 v0 admits only:

Unit, Bool, I64, F64;
read-only Array<ρ, Read, F64>;
direct first-order functions;
tuples and the opcode ADT;
let, if, case, tail recursion, and return;
explicit checked bounds behavior;
pure computation and typed errors.

Excluded:

closures;
general heap mutation;
user algebraic handlers;
IO and FFI;
weak references and shared cycles;
concurrency;
general maps/text processing;
region polymorphism;
dynamic code loading.

The exclusion is a specializer scope limit, not a claim that the full language will never support these constructs.

P1V1 is a verifier-profile extension, not an implemented Futamura projection. It adds lexical Region plus RefAlloc, RefLoad, and RefStore for non-escaping Shared scalar references. It does not silently add those operations to the P1 lighthouse workload.

P1V2 is another verifier-profile extension, not an implemented Futamura projection. It adds bounded existential closure construction and calls without admitting escaping closures or changing the P1 lighthouse workload.

P1V3 is another verifier-profile extension, not an implemented Futamura projection. It adds typed operations and affine implicit lexical handlers without adding handlers to the P1 lighthouse workload.

P1V4 is another verifier-profile extension, not an implemented Futamura projection. It adds bounded affine direct ownership without adding mutation or ownership to the P1 lighthouse workload.

P1V5 is another verifier-profile extension, not an implemented Futamura projection. It adds bounded ownership return without adding ownership to the P1 lighthouse workload.

15. Evolution rule

Any change to an existing Core tag, field order, normalization rule, or semantic meaning requires:

an accepted ADR;
schema version change;
interpreter and verifier update;
semantic-hash policy update;
migration or explicit rejection of older artifacts;
parity and residualization regressions.

An append-only profile extension may allocate previously unused tags under the existing encoding domain only through an ADR, with strict unknown-profile rejection and locked proof vectors. ADR-0013 applies that rule to P1V1; ADR-0014 applies it to P1V2; existing P1V0 and P1V1 bytes and hashes remain unchanged. ADR-0015 applies it to P1V3; all older profile vectors remain unchanged. ADR-0016 applies it to P1V4; all older profile vectors remain unchanged. ADR-0017 applies it to P1V5; all older profile vectors remain unchanged. ADR-0018 freezes the profiled interpreter-semantics identity and exact P1V0 semantic input to B0; future profile append operations cannot change an older identity vector.