Skip to content

Docs Examples Architecture Benchmarks Install Status Roadmap

Docs Examples Architecture Benchmarks Install Status Roadmap GitHub

NAUX DocsHierarchical reference

6 chapters · 85 ADRs

›01Getting started

›01.1Installation

01.2Five-minute quickstart

01.3Your first program

›02Learn NAUX

02.1Input and output

02.2Practice algorithms

02.3Diagnostics

›03Language reference

03.1Language specification

03.2Algorithm library

03.3Execution limits

›04Tooling and distribution

04.1Binary bundle

04.3Troubleshooting

›05Compiler architecture

›05.1Orientation

05.1.1Architecture Charter

05.1.2North Star

05.1.3Compiler pipeline

›05.2Semantic core

05.2.1Typed Core v0.1

05.2.2Memory model

05.2.3Region analysis

›05.3Specialization

05.3.1P1 Lighthouse

05.3.2Binding-time analysis

05.3.3Static evaluation

05.3.4Residualization

›05.4Native pipeline

05.4.1Machine IR

05.4.2x86-64 target

05.4.3Native runner

05.4.4Standalone ELF

›05.5Verification and claims

05.5.1Phase 1 proof contract

05.5.2Coq mapping

05.5.3Gate B measurement

05.5.4Performance contract

›06Architecture decisions

›06.1Semantic foundations

0001Canonical Typed Core

0002Binding Time Judgment

0003Allocation Identity Observability

0004Region Evidence Vs Placement

0005P1 Lighthouse Scope

0006Numeric Semantics

0007FFI Trust Boundary

0008Production Sovereignty

0009Rc Fallback Cycle Policy

0010Nauxogenesis

0011Surface Core T2 Boundary

0012Surface Direct Functions T2B

0013Bounded Logical Store P1V1

0014Bounded Existential Closures P1V2

0015Linear Lexical Handlers P1V3

0016Bounded Affine Unique P1V4

0017Bounded Ownership Return P1V5

0018Core Semantics Identity Stage1 Freeze

›06.2Specialization and residualization

0019B0 Request Trust Boundary

0020B0 Structural Node Identity

0021B0 Deterministic Call Fixed Point

0022B0 Sealed Evidence Independent Replay

0023R0 Specialization Value Request Boundary

0024R0B Evidence Gated Static Evaluation

0025R0B2 Continuation Machine

0026R0C1 Scalar Residual Core

0027R0C2 Folding And Opaque Evaluation Record

0028R0D Sealed Residual Evidence

0029Corevm0 Bounded Program Representation

0030Corevm0 Full Image And Definitional Boundary

0031Evidence Gated Polyvariant R1 Boundary

0032Structural Partial Values And Bounded Helper Unfolding

0033Bounds Preserving Arrays And Corevm0 Admission

0034Canonical Summaries And Corevm0 Structural Erasure

0035Gate A Translation Validation And Canonical Residual SSA

›06.3Native path and measurement

0036Canonical Machine IR Trust Boundary

0037Canonical x86 64 Target Plan And Checked Encoding

0038Verifier Gated W^X Native Runner

0039Direct ELF64 Standalone Image And Libc Free Startup

0040Sealed Predecessor Translation Correspondence Roots

0041Gate B End To End Standalone Measurement

0042Fail Closed Tail Control Flow Encoding Policy

0043Reject Greedy Tail Home Offset Swaps

0044Reachable Unique Predecessor One Op Superblocks

0045Sealed Weighted Target Profile And Shared Join Selection

0046Bounded Transitive Shared Join Composition

0047Bounded Per Ingress Fused Compare Branch Arm Cross Tabs

0048Exact Per Ingress Ordered Shared Join Lineage

0049Proof Only Shadow Prospective Shared Join Realization

0050Bounded Independent Shadow Machine Semantic Decoder

0051Sealed Non Executable Policy 15 Candidate Capsule

0052Finite Policy 15 Candidate Native Correctness Admission

0053Process Isolated Policy 15 Candidate Correspondence

0054Candidate Specific Standalone ELF Correspondence

0055Candidate Matched Gate B Measurement And Claim

0056Sovereign Candidate Cost Attribution

›06.4Sovereign execution

0057Bounded Persistent Typed Tail State Plan

0058Bounded Sovereign Physical Tail Bank Allocation

0059Bounded Physical Template Preservation Realization

0060Owned Tail Template Byte Capsule And Independent Decoder

0061Bounded Persistent Site Binding And Frontier State Proof

0062Bounded Symbolic Body Frontier Realization

0063Frontier Live Set Narrowing

0064Owned Body Frontier Byte Capsule

0065Closed Semantic Image Composition

0066Sovereign ABI Envelope Byte Capsule

0067Fully Enveloped Semantic Image Composition

0068Sovereign Enveloped Image Native Correctness

0069Sovereign Enveloped Process Containment

0070Sealed Worker Artifact Launch Attestation

›06.5Dependency and loader closure

0071Independent Worker ELF Dependency Inventory

0072Reviewed Worker Dependency Declaration Admission

0073Exact Worker Dependency Object Byte Admission

0074Sealed Object Dynamic Identity Inventory

0075Reviewed Transitive Declaration Closure Admission

0076Sealed Object GNU Version Requirement Inventory

0077Sealed Object GNU Version Definition Inventory

0078Exact GNU Version Compatibility Admission

0079Independent Dynamic Symbol Version Index Inventory

0080Sealed Root Worker GNU Version Requirement Inventory

0081Exact Root GNU Version Compatibility Admission

0082Sealed Root Dynamic Symbol Version Inventory

0083Reviewed Root Dynamic Symbol Lookup Scope Admission

0084Exact Strong Versioned Root Symbol Candidate Selection

0085Sealed Root Dynamic Relocation Inventory And Selection Join

Compiler architectureSpecialization

Compiler architecture · 05.3

Specialization

See how NAUX separates static knowledge, evaluates admitted work, and emits residual programs.

P1 Lighthouse

The bounded end-to-end Futamura P1 contract.

Binding-time analysis

The evidence that classifies static and dynamic computation.

Static evaluation

The bounded evaluator and its fail-closed rules.

Residualization

How accepted specialization becomes a residual program.