GitHub

Compiler and Execution Pipeline

This is the active high-level pipeline for the current Rust bridge crate, naux-lang. It is not the final canonical architecture. The accepted target is defined by ../NAUX_ARCHITECTURE_CHARTER.md and typed_core_v0_1.md.

Canonical Semantic Path (R1-S8 and Gate B)

Alongside the bridge pipeline below, the verified lighthouse path now reaches:

Residual Core-N0
  → source-bound canonical Core SSA
  → source-bound target-independent Machine IR
  → source-bound canonical Linux x86-64/SSE2 target plan
  → checked position-independent raw bytes
  → verifier-gated W^X native execution
  → direct linker-free ELF64 + bounded syscall-only startup
  → fresh standalone process

ADR-0035 owns the Core-SSA handoff. ADR-0036 owns deterministic SSA-to-Machine-IR lowering, verification, bounded evaluation, provenance, identity, and hard limits. ADR-0037 owns the fixed lighthouse ABI, deterministic stack-home target plan, checked-array and tail-transfer templates, retained PcRel32 fixups, owned raw encoder, target-plan evaluator, source replay, and locked identities. R1-S7a itself emits but does not execute raw bytes. ADR-0038 freezes the separate R1-S7b runner/evidence boundary. S7b-a now executes the exact source-bound bytes through an owned RW→RX raw-syscall runner and passes the 51-case in-process development corpus. S7b-b seals canonical native correspondence, and S7b-c replays all 51 cases through fresh process-isolated workers with independently checked IPC, source-bound target identity, and Machine-IR observations. ADR-0039 and ADR-0040 close the finite R1-S8 direct-ELF standalone-correctness boundary and its predecessor translation roots. ADR-0041 owns the matched standalone baseline and end-to-end Gate B measurement. ADR-0042 remains the historical policy-1.3.0 tail/control-flow predecessor. ADR-0043 records the rejected greedy tail-home swap experiment. ADR-0044 migrates the complete authority chain to encoder policy 1.4.0: reachable-body DCE with one-byte label tombstones, exact unique-predecessor one-operation superblocks, typed R8/XMM2 result residency, and fail-closed substitution/copy proofs. Three local observations measure 4.822709x, 4.796549x, and 4.884944x, 16.78%–18.29% better than the policy-1.3.0 observation. Their ratios span only about 1.85%, but each is local-only, fails at least one CV check, and remains above 2.0x. ADR-0045 historically added an evaluator-observer seam, exact encoder-realization atoms, and the initial schema-1.1 post-policy-1.4 weighted profile. Its 2,927,032,491 weighted template bytes rank tail transfer first at 1,799,362,381 and selected bounded shared-join state residency as its successor proof target. ADR-0046 historically proved all five selected targets can coexist in the topological order 49, 92, 93, 121, 48: 11 prospective body replicas, 12,582,976 body executions, and 125,829,376 exact composed-ingress accesses under the sealed schema-1.2 identity 7f35655e4891bdecbe029369374dc806feb8e50d7f781836bf9f438b10be14ac. Target 48 inherits target 121 but retains distinct upstream count authorities, so overlap is neither double-owned nor double-counted. Weighted bytes and ingress accesses are deterministic structural proxies, not cycles or a performance claim. ADR-0047 historically added the per-ingress fused-compare branch-arm cross-tab under target-profile schema 1.3.0, sealed as 6031a26d6207a0e98cd8826d0cf16f7fbde3779278e27f1873e75a16232440c0. Its branch-cell data and conservation checks remain retained, while its unordered ancestor admission and schema-1.3 route authority are superseded by ADR-0048. The current implementation binds every ingress to an exact ordered sequence of logical tail edges and selected register ancestors, including zero-count preflight. It resolves the exact empty BranchRel32 bridge and requires canonical distinct successors even when one arm is dynamically unobserved. Target-profile schema 1.4.0 has historical identity ee803c9518ef891d033a0d76436667e8ad12d0d742e1d4983813fdd34c579d83. Focused raw 36/36 and profile 5/5 tests pass; self-resealed route and margin-preserving branch-cell tampering fail replay, and an explicit release-mode schema-1.4 replay passed 1/1 in 305.48 seconds. ADR-0049 now accepts the separate proof-only shadow realization under target-profile and Gate B schema 1.5.0, proof policy 1.4.0, and seal 2e7a1265e526d01697038fd7b0fac69258b9a17ce7362f063c3132551a78eb47. The 3,214-byte candidate contains 199 exactly owned atoms, 142 labels, 51 fixups, 11 replicas, and 31 shared-authority atoms; candidate and realization hashes are independently reconstructed. It is never installed, executed, packaged, timed, or selected, and the accepted encoder stays 1.4.0. Full debug/release, strict 8/8, Clippy, format, diff, Gate wrapper 1/1, and the 319.21-second release replay pass. Independent semantic decoding of cloned register/tail bytes, Gate B performance, encoder policy 1.5, general physical register allocation, and broader target coverage remain open.

Frontend

  1. Lexing (lexer.rs)
    • Tokenization with span tracking.
  2. Parsing (parser/)
    • Builds AST and reports syntax errors with source spans.
  3. Typecheck (typecheck.rs)
    • Validates core typing constraints before execution paths.

Lowering

  1. AST -> IR (vm/compiler.rs)
    • Produces stack-oriented IR instructions.
  2. IR -> Bytecode (vm/bytecode.rs)
    • Produces VM program for interpreter/JIT paths.

Refinement And SEFO Proof Loop

  1. Refinement -> ProofSlot -> E-graph -> Materialization
    • Refinement evidence is attached during IR lowering.
    • E-graph rewrites emit proof obligations as discharged, blocked, or deferred.
    • Proof-gated materialization rewrites executable IR only after the e-graph confirms the guarded equivalence.
    • naux dev refine --strict and NAUX_IR_PROOF_STRICT=1 run the current strict proof contract.

See phase1_proof_contract.md for the active Phase 1 contract.

SSA Construction (analysis/optimization path)

  1. IR -> SSA preview (vm/ssa.rs)
    • Builds CFG with explicit terminators (no implicit fallthrough).
    • Computes dominator tree and dominance frontier.
    • Runs phi placement (Cytron-style) and rename.
    • Verifies SSA invariants (def-use, dominance, phi correctness).

Execution Engines

  1. Runtime interpreter path (runtime/)
    • AST-based runtime evaluation and event emission.
  2. VM path (vm/interpreter.rs, vm/run.rs)
    • Bytecode interpreter with builtin bridge.
  3. Typed trace JIT path (vm/jit.rs, vm/typed.rs)
  • Native execution for supported hot paths with fallback behavior.

Tooling

  1. CLI/dev commands (cli/)
  • run, fmt, test, dev ir, dev disasm, dev bench.

Quality Gate

Run before commit:

cargo fmt --manifest-path naux-lang/Cargo.toml --all -- --check
cargo clippy --manifest-path naux-lang/Cargo.toml --all-targets --all-features -- -D warnings
cargo test --manifest-path naux-lang/Cargo.toml --all-features
NAUX_IR_PROOF_STRICT=1 cargo test -p naux --test refinement_closed_loop_tests