GitHub

NAUX Architecture Charter

Status: accepted
Accepted: 2026-07-25
Authority: project-wide architecture and decision policy

1. Mission

NAUX turns executable typed semantics into independently checkable, performance-leading native programs through a compiler and runtime stack that NAUX owns completely.

The defining equation is:

semantic ownership
+ staged specialization
+ checked transformation
+ native sovereignty
= NAUX

Removing any term changes the identity of the project.

2. Non-negotiable invariants

INV-001 — Distinct architecture

NAUX does not become a frontend for an external optimizer or backend. Its canonical path is Typed Core interpretation, binding-time analysis, partial evaluation, residualization, checked optimization, and self-owned native emission.

INV-002 — Performance leadership

NAUX targets the performance frontier, not merely acceptable performance. Claims require fair controlled baselines and raw reproducible evidence. Fallback execution cannot be reported as native performance.

INV-003 — Total production sovereignty

A released NAUX toolchain must build and execute normal NAUX programs without LLVM, GCC, Clang, Cranelift, libc, a system assembler/linker, an external runtime, or third-party libraries. Host ISA and syscall ABIs are platform contracts; all software above that boundary is a NAUX responsibility.

INV-004 — Canonical typed semantics

Surface syntax is not the final semantic kernel. Surface programs elaborate to a small, typed, call-by-value Core with explicit evaluation order, effects, logical lifetime evidence, mutation, and identity.

INV-005 — Checkable generation

Every residual program and generated compiler carries provenance. Every behavior-changing transform is either owned and directly validated or emits evidence accepted by an independent NAUX checker.

INV-006 — Fail closed

Unsupported specialization, proof failure, exhausted budget, unknown aliasing, or unknown effects must residualize or use an explicitly declared generic path. They must never silently weaken semantics.

INV-007 — No invisible memory tax

Physical placement and reclamation are implementation choices. RC may remain a cost-visible fallback, but certified hot paths must be able to prove that they are RC-free. No hidden tracing collector is permitted.

INV-008 — Novelty must pay

NAUX deliberately takes a different and difficult path. A technique is kept only when it yields a measured performance, sovereignty, semantic, or verification advantage.

INV-009 — Nauxogenic origin

NAUX does not make an ancestral handwritten compiler its final semantic or production center. Its compiler is projected from canonical executable semantics, composed with the checked self-owned native path, and admitted only after reproducible generative and dependency closure. The physical Origin Image for a target is declared provenance, never hidden authority.

3. Authoritative architecture

Surface Source
  → Lexer / Parser
  → Elaboration + Type / Effect / Region Checking
  → Core-N0
  → Canonical Core Interpreter
  → Binding-Time Analysis
  → Partial Evaluator
  → Residual Core-N0
  → Translation Validator
  → SSA
  → Checked Optimizers
  → Machine IR
  → NAUX Encoder
  → NAUX Object / Executable Writer
  → NAUX Linker
  → NAUX Runtime and Standard Library

The current AST interpreter, bytecode VM, typed trace JIT, and Rust implementation are bridge infrastructure. They remain important for parity, performance research, and migration, but they do not define the final architecture.

4. Semantic source hierarchy

When sources disagree, use this order:

  1. this Charter;
  2. NAUX_NORTH_STAR.md;
  3. accepted records in docs/adr/;
  4. docs/typed_core_v0_1.md;
  5. PARITY_CONTRACT.md and MEMORY_MODEL.md;
  6. the canonical Typed Core interpreter for its verified admitted profiles;
  7. surface language specification;
  8. VM/JIT/backend behavior.

An implementation disagreement is a bug until an accepted ADR changes the contract.

5. Core boundaries

Core-N0 is semantic, not machine-oriented:

  • typed and call-by-value;
  • A-normal form with explicit order;
  • let, if, case, direct/closure call, tail recursion, perform, handle, and return;
  • no phi nodes, dominance, register concepts, physical addresses, or ABI details;
  • closure behavior is typed independently from its existential packed environment representation;
  • logical region evidence does not select a physical allocator;
  • binding time is a checked staging judgment over ordinary types.

SSA remains the optimization substrate below residual Core.

6. Observable behavior

Observable:

  • return value and error;
  • effect and external-call order;
  • logical identity as exposed by alias-visible mutation;
  • mutation through aliases;
  • explicit resource lifecycle;
  • numeric behavior.

Not observable:

  • physical address or placement;
  • stack versus arena versus heap;
  • RC increment/decrement traffic;
  • internal reclamation time;
  • object movement;
  • scalar replacement.

Core-N0 v0.1 has no reference-equality primitive, weak reference, implicit destructor, or finalizer. These require a future ADR because each constrains optimization and reclamation.

7. Staging policy

The initial binding-time lattice is:

Static ≤ Dynamic

join is an operation, not a third binding-time value. A static expression may depend only on static inputs. Reproducible specialization-time evaluation is limited to pure work, specializer-owned allocation, immutable static program reads, and bounded static control flow.

IO, FFI, clocks, randomness, environment variables, external state, and nondeterminism cannot execute at specialization time by default. A future compile-time capability must be explicit and hashed into provenance.

8. Native and dependency policy

The current seed and normal development build use rustc and Cargo, while the bridge e-graph path uses egg. They are acknowledged dependency debt, not approved final dependencies.

External proof assistants, fuzzers, compilers, and benchmark tools may provide optional independent comparison during migration. They cannot:

  • be required to build a normal release;
  • be linked into release artifacts;
  • define canonical behavior;
  • make an unchecked semantic decision;
  • become the only implementation of an essential pass.

Every external dependency must have an owner, a removal milestone, and a NAUX-owned replacement path.

9. Performance policy

Each performance claim compares:

  1. a generic C or Rust engine;
  2. a hand-specialized C or Rust implementation;
  3. a NAUX-generated residual implementation.

The claim artifact includes sources, compiler versions and flags, numeric contract, input hashes, hardware fingerprint, raw samples, distribution statistics, execution provenance, and a verifier.

The lighthouse differentiation target is satisfied when NAUX either:

  • exceeds the generic engine by at least 1.25x; or
  • comes within 10% of the hand-specialized implementation while being generated from the generic interpreter.

The long-term target requires both on suitable domains.

10. Memory and cycles

Logical region evidence proves lifetime and ownership; it never mandates stack, arena, or heap placement.

Core-N0 v0.1 permits:

  • lexical regions;
  • simple region parameters;
  • no-escape checking;
  • region-contained cycles;
  • acyclic escaping ownership.

General shared escaping cycles and weak references are outside v0.1. RC fallback may support unresolved acyclic shared escape while its traffic remains visible.

11. Futamura milestones

  • P1 produces standalone residual code from MIX(CoreVM0, fixed_program).
  • P2a generates the semantic compiler through Residual Core/SSA.
  • P2b composes P2a with the checked self-owned native path.
  • Generative closure rebuilds the interpreter and specialization kernel and projects the next compiler generation.
  • Nauxogenesis is reached only when semantic, native, regenerative, dependency, and independent-acceptance gates all pass.
  • P3 begins only after reproducible P2 utility and Nauxogenic closure are proven.

The trace JIT may donate tests, profiles, and encoder components. It cannot be renamed P1 because P1 requires specializer provenance.

The complete terminology and evidence gates are defined in docs/nauxogenesis_contract.md and ADR-0010.

12. Governance

A significant architectural change requires:

  1. an ADR with context, alternatives, trade-offs, and consequences;
  2. updated semantic or performance contract;
  3. parity/proof evidence;
  4. a migration plan that does not weaken sovereignty;
  5. a clear revisit trigger.

Historical plans and status narratives live in Git history, not beside active specifications. ROADMAP.md is the only active execution roadmap.

13. Current reality

The accepted destination is not yet implemented:

  • the current seed, including Core-N0, T2A/T2B, P1V1 logical store, P1V2 existential closures, P1V3 linear handlers, P1V4 affine ownership, and P1V5 ownership return, is written in Rust and built through Cargo/rustc;
  • the e-graph path depends on egg;
  • the general runtime uses shared RC;
  • the bridge native path remains an x86-64 JIT subset; the canonical path now owns a bounded Linux x86-64/SSE2 target plan, encoder, and verifier-gated in-memory runner. ADR-0039 freezes a direct ELF64/syscall-only standalone boundary, but its authority-bound writer, independent verifier, and direct execution evidence are not yet complete;
  • Core-N0 T1 provides the P1V0 schema, artifact and interpreter-semantics hashes, verifier, and definitional interpreter; T2A/T2B provide narrow deterministic typed scalar/control/direct-function elaboration and differential corpora; P1V1 provides bounded lexical-region, non-escaping shared-scalar store semantics, P1V2 provides bounded non-escaping existential closure semantics, and P1V3 provides typed operations plus affine implicit lexical handlers; P1V4 provides bounded direct non-escaping affine Unique ownership; P1V5 provides bounded anchored ownership return; the bounded Stage 1 audit is accepted while escaping/general mutation, general borrowing, aggregate ownership, escaping/general closures, first-class/multi-shot handlers, and future Core semantics remain;
  • the complete B0-A/B/C/D boundary provides hash-bound requests, structural judgments, deterministic interprocedural summaries, sealed certificates, and independent replay; R0-A provides canonical typed static values, exact dynamic holes, B0-bound request identity, hard-capped budgets, and mutation evidence; R0-B1/R0-B2 provide evidence-gated intraprocedural and continuation-machine static evaluation; R0-C1/R0-C2 emit verified scalar and aggregate Residual Core with static control/call folding and pruning; R0-D seals and regeneratively validates the complete residual chain;
  • CoreVM0 v1 now has a verified Rust seed, canonical full ProgramImage, opaque raw-input admission boundary, and a generic P1V0 definitional Core artifact with bounded seed-vs-Core differential evidence. The generic artifact deliberately retains dispatch; the frozen R1-S4 residual erases it. R1-S5 now supplies finite Residual-Core Gate A evidence and the source-bound canonical Core SSA handoff; R1-S6 supplies the verified, target-independent Machine IR handoff; R1-S7a supplies canonical target planning and checked raw encoding; R1-S7b-a/b/c supply source-bound W^X execution, canonical native correspondence identities, and process-isolated acceptance over the exact 51-case corpus. Standalone native output and P1 do not exist yet;
  • ADR-0031 R1-S1 now provides a bounded, pure-scalar P1V0 polyvariant specializer slice: ordered known/dynamic parameter patterns, mixed direct and tail calls, both residual branches of dynamic If, memoized exact-key recursion, canonical key-byte residual function ordering, four exact specialization budgets, distinct R1 policy/request identity, and ordinary verifier-accepted Residual Core;
  • ADR-0032 R1-S2 is implemented and bounded-differential validated: recursively pure Tuple/Sum partial values, known/unknown Sum control, alias-normalized flattened signatures, structural version keys, and zero-residual acyclic helper result propagation on an explicit bounded frame machine. Eight exact budgets and a locked policy/request/residual vector bind the accepted 16-test slice;
  • ADR-0033 R1-S3 is implemented and bounded-differential validated: dynamic read-only Array, exact Error and region/effect signature preservation, known-control pure helper unfolding, two recursive components, and a concrete identity-bound CoreVM0 package. A locked nine-test corpus covers the generic and CoreVM0 binding vectors;
  • ADR-0034 R1-S4 is implemented and bounded-differential validated: hash-checked static interning, alias-parameterized helper summaries, explicit recursive control pins, a deterministic widening state quotient, frozen branch-mix specialization, structural dispatch erasure, and raw-input regenerative replay. Locked generic and branch-mix vectors bind the accepted five-test slice without raising S3 hard caps;
  • full node-origin R1-D, Gate B performance, and P1 remain unfinished; the fixed finite Gate A, canonical SSA, Machine IR, checked x86-64 encoding, in-process native identity, and process-isolated native acceptance boundaries are implemented and locally validated. R1-S8 now has a frozen contract, canonical I/O codec, opaque authority, typed and raw syscall-only startup, NAUX-owned direct ELF64 writer/parser, verifier-owned full-byte startup oracle, adversarial artifact verification, and an accepted ordered 51-case direct-process result. This completes only the declared finite standalone-correctness boundary;
  • general object writing and linking are not end-to-end NAUX-owned; only the exact R1-S8 direct ELF64 image grammar is currently owned;
  • the Stage 0 validation matrix is green, while the clean baseline commit/tag remains an owner action.

These are explicit debts. Documentation must not describe them as completed North Star properties.

T2A/T2B, logical-store P1V1, existential-closure P1V2, linear-handler P1V3, affine-ownership P1V4, and ownership-return P1V5 are Rust-seed evidence for bounded Stage 1 work packages. They are not P1, P2, Projection Birth, Nauxogenesis, or a reduction of the Rust/Cargo/egg dependency debt. The accepted freeze and completed B0/R0-D chain authorize only verified, evidence-bound residualization. The CoreVM0 definitional artifact authorizes the R1 line; R1-S1 authorizes its bounded pure-scalar control slice, R1-S2 its structural Tuple/Sum slice, and R1-S3 only its bounds-preserving array and concrete CoreVM0 admission slice. R1-S4 authorizes only its canonical-summary, frozen-program structural-erasure, and regenerative-replay subgate. R1-S5 authorizes only its fixed finite Gate A evidence and source-bound canonical Core SSA handoff. R1-S6 authorizes only its closed target-independent Machine IR, deterministic source replay, bounded evaluator relation, and locked 51-case finite evidence. R1-S7a authorizes only canonical target planning and checked bytes; R1-S7b-a/b/c authorize only verifier-gated execution, canonical native identity evidence, and finite process-isolated containment. ADR-0039 and ADR-0040 authorize only the exact finite R1-S8 direct-ELF standalone-correctness subgate and its sealed predecessor translation roots. The active successor is the separately frozen Gate B measurement and performance boundary; none of these gates authorize a projection, complete Gate B, or a performance claim.