Bounded Stage 1 Exit Audit
Status: accepted and validated
Date: 2026-07-25
Decision: ADR-0018
1. Decision scope
This audit evaluates Roadmap Stage 1 for the implemented, versioned Core-N0 profiles P1V0–P1V5 and the admitted Surface T2A/T2B subsets.
The fixed Stage 2 lighthouse input is P1V0. P1V1–P1V5 are append-only semantic evidence; they do not widen the P1 lighthouse. General escaping stores and closures, aggregate borrowing, first-class or multi-shot handlers, FFI, concurrency, and every future Core profile remain outside this bounded exit.
2. Required-artifact audit
| Stage 1 requirement | Executable or normative evidence | Result |
|---|---|---|
| Versioned schema and verifier | core/schema.rs, core/verify.rs, core_n0.rs negative corpus | Satisfied |
| Typed call-by-value ANF | Typed Operand/RValue/Term, verifier scope checks, left-to-right T2A/T2B tests | Satisfied |
| Numeric modes and errors | Strict I64 modes, binary64 canonical NaN policy, typed overflow/bounds tests | Satisfied |
| Effects, regions, mutation, identity | P1V1 lexical logical-store contract and positive/negative alias/lifetime corpus | Satisfied in admitted profile |
| Typed and existential closures | Typed closure signatures plus P1V2 ordered existential environments and no-escape corpus | Satisfied in admitted profile |
| Surface subset to Core | Deterministic fail-closed T2A/T2B elaborators with exact type manifests and budgets | Satisfied in admitted subsets |
| Canonical interpreter | core::evaluate verifies before evaluation and has no unchecked public entry | Satisfied |
| Surface/Core parity | T2A/T2B scalar, branch, direct-call, recursive, tail-call, error, and budget differential tests | Satisfied in admitted subsets |
| Deterministic serialization and hash | Semantic Encoding v1, domain-separated SHA-256, P1V0–P1V5 artifact vectors | Satisfied |
| Independent interpreter-semantics identity | Semantic Identity Encoding v1 and six per-profile locked vectors | Satisfied |
Profile contracts and their evidence suites:
| Profile/work package | Contract | Executable suite |
|---|---|---|
| P1V0 | typed_core_v0_1.md and core_n0_semantic_encoding_v1.md | naux-lang/tests/core_n0.rs |
| T2A | surface_core_t2_contract.md | naux-lang/tests/surface_core_t2.rs |
| T2B | surface_core_t2b_contract.md | naux-lang/tests/surface_core_t2b.rs |
| P1V1 | core_store_p1v1_contract.md | naux-lang/tests/core_store_p1v1.rs |
| P1V2 | core_closure_p1v2_contract.md | naux-lang/tests/core_closure_p1v2.rs |
| P1V3 | core_handler_p1v3_contract.md | naux-lang/tests/core_handler_p1v3.rs |
| P1V4 | core_unique_p1v4_contract.md | naux-lang/tests/core_unique_p1v4.rs |
| P1V5 | core_ownership_return_p1v5_contract.md | naux-lang/tests/core_ownership_return_p1v5.rs |
| Semantics identity | core_n0_interpreter_semantics_identity_v1.md | naux-lang/tests/core_semantics_identity.rs |
3. Exit-evidence audit
| Exit condition | Evidence | Result |
|---|---|---|
| Verify before evaluation | evaluate(CoreArtifact, ...) calls verify and converts rejection into InvalidArtifact; no unchecked public evaluator exists | Satisfied |
| Positive and negative elaboration goldens | T2A/T2B parity, exact-manifest, rejection, budget, determinism, and locked-vector tests | Satisfied |
| Bounded differential corpus clean | T2A/T2B compare normalized Surface and Core observations, including numeric edges and recursion | Satisfied |
| Schema/artifact hashes stable | Semantic Encoding v1 plus locked P1V0–P1V5 and T2A/T2B hashes | Satisfied |
| Interpreter semantics hashes stable | Semantic Identity Encoding v1 locked for P1V0–P1V5 | Satisfied |
| Core isolated from bridge semantics | Source-isolation regression rejects Surface AST, bridge Value, VM, JIT, and egg imports | Satisfied |
| Repository gates | 98 focused semantic tests; 422 workspace tests; strict Clippy; format; 22 governance tests; 9 shell syntax checks; 54 Markdown files/107 local links; diff hygiene | Satisfied |
4. Freeze boundary
The repository gates are green. Therefore:
- P1V0 schema
core-n0@0.1.0, artifact encoding v1, and interpreter semantics identity v1 are the frozen semantic input to Stage 2; - changes to an existing P1V0 meaning require a new ADR, version/domain, migration policy, vector replacement, and parity evidence;
- append-only later profiles remain permitted under their own ADRs;
- Stage 2 opens only for binding-time analysis and its independent evidence verifier.
5. Non-claims
This audit does not implement or claim a binding-time analyzer, residualizer, CoreVM0, Futamura P1/P2/P3, native backend closure, performance leadership, dependency closure, seed retirement, Projection Birth, or Nauxogenesis.
The current evidence is still produced by the Rust/Cargo seed. The owner-controlled clean revision/tag remains required before a public reproducibility or release claim.