GitHub

Nauxogenesis Contract

Status: accepted target, not yet achieved
Architecture decision: ADR-0010

1. Definition

Nauxogenesis is NAUX’s semantics-derived lifecycle:

Canonical Core-N0 Semantics
             +
NAUX Specialization Kernel
             ↓ Futamura P2
Generated Semantic Compiler
             +
Checked NAUX Native Path
             ↓
Native NAUX Compiler
             ↓ regeneration
Nauxogenic Fixed Point

It is not a synonym for conventional self-hosting. The handwritten compiler is not the semantic authority and compiler ancestry is not the release architecture.

2. Named artifacts

  • Canonical Interpreter (I) — executable Core-N0 semantics.
  • Specialization Kernel (S) — binding-time analysis, partial evaluation, residualization, budgets, and provenance.
  • Projected Compiler (C) — compiler produced by P2 from S and I.
  • NAUX Origin Image — declared native artifact used for the first execution on a target architecture.
  • Architecture Genesis — establishment of a verified Origin Image on a new target.
  • Generative Closure — ability of the generated toolchain to rebuild I and S and project its next compiler generation.
  • Nauxogenic Fixed Point — accepted stable generation satisfying every gate in this contract.

3. Authority

The authority order remains:

Charter and accepted ADRs
→ Core-N0 contract
→ canonical interpreter
→ independent checkers
→ projected compiler
→ backend implementation

A generated compiler that disagrees with the canonical interpreter is wrong. Reproducible compiler bytes do not excuse semantic disagreement.

4. Admission gates

Gate N0 — Semantic origin

  • Core-N0 schema and observable behavior are versioned.
  • The canonical interpreter accepts only verified Core.
  • Schema, semantics, and numeric contracts have deterministic hashes.

Gate N1 — Projection birth

  • C = P2(S, I) is demonstrated with complete provenance.
  • C is generated from I; it is not a manually written compiler relabeled as a projection.
  • The generated compiler agrees with I on the admitted corpus.

Gate N2 — Native closure

  • C is composed with the checked, NAUX-owned encoder, object/executable writer, linker, runtime, and standard library.
  • Ordinary output has no interpreter, trace-JIT, or generic-handler fallback unless explicitly declared by the source contract.

Gate N3 — Regenerative closure

  • Generation Cₙ rebuilds the canonical Iₙ₊₁ and Sₙ₊₁.
  • P2(Sₙ₊₁, Iₙ₊₁) produces Cₙ₊₁.
  • Repeating the operation reaches a stable artifact for identical declared inputs and target.
  • All differing generations and all equivalence exceptions fail closed.

Gate N4 — Dependency closure

  • Rust, Cargo, egg, external compilers, system assemblers/linkers, foreign runtimes, and third-party libraries are absent from the normal release graph.
  • A machine-readable dependency report confirms the boundary.
  • Optional comparison and research tools can be deleted without changing semantics or breaking an ordinary release build.

Gate N5 — Independent acceptance

  • Semantic parity, translation validation, provenance, dependency closure, and artifact hashes are checked independently from the pass that produced them.
  • The complete evidence bundle verifies offline.

Only N0 through N5 together permit a release to claim Nauxogenesis.

5. Origin honesty

An Origin Image is unavoidable physical input, like any executable loaded by a processor. Its hash, target contract, generator provenance, and validation results must be published.

The Origin Image:

  • does not define language semantics;
  • cannot silently approve a transformation;
  • is replaceable by a later verified NAUX generation;
  • is excluded from the next generation’s software dependency graph once closure is established.

6. Current status

NAUX has not achieved Nauxogenesis:

  • the current seed is built by Rust and Cargo;
  • equality saturation currently uses egg;
  • bounded P1V0/P1V1/P1V2/P1V3/P1V4/P1V5 Core profiles, a verified canonical interpreter, bounded logical-store, existential-closure, linear-handler, affine-ownership, and ownership-return semantics, and T2A/T2B elaborators now exist as Rust/Cargo seed evidence toward semantic origin; broader Core semantics remain open;
  • P1, P2, complete native sovereignty, and regenerative closure remain open.

These are development facts, not exceptions to the gates.