0%

AIMS Rust aligned to the calculus

The implementation is audited against the calculus the previous section made pristine, under full impl-hygiene. The coherence path is IN scope: excluding it to keep a later section non-empty would preserve the root defect in order to reserve work.

END STATE, structural: ONE frozen calculus artifact CONSUMED by each admitted production executor. Documenting a divergence is NOT completion — a shared artifact no production path consumes is not a seam, and “record why the seam differs” would let the mission (“implementation matches the calculus”) close while no production consumer exists.

Measured at authoring: ori_arc = 322 files / 123,754 LOC. aims/class_ledger/ = 27 files / 13,655 LOC, of which tests.rs is 6,725 lines against the project’s 500-line file limit. realize_closed_program (pipeline/mod.rs:92) has 5 call expressions, every one in test or oric driver code — no production ori_llvm / ori_vm call site. Satisfies / VmLayoutPlan / CompiledLayoutPlan / LayoutCapabilities exist as Rust types ONLY in aims-proof/checker/src/engine/realization_rules.rs; inside compiler/ they appear solely in doc comments.

Deliverables

  • Split class_ledger/tests.rs (6,725 lines) under the 500-line cap by responsibility, not by line count. Coverage must not shrink.
  • Thread realize_closed_program through the REAL production path, naming each production caller and each admitted executor that consumes it. Recording why the seam differs is NOT an accepted outcome; if the seam genuinely cannot be threaded, the MISSION is rewritten to what is true, never closed over a documented gap.
  • Audit the coherence path against the calculus; every divergence is a defect to fix, never a documented difference.
  • Per missions.md §AIMS conflict rule, prove no parallel ownership calculus was introduced: a MECHANICAL enumerator over shadow uniqueness trackers, independent escape enums, and backend-local ownership classification — the enumerator must find its own known sites, so a green run cannot mean it enumerated nothing.
  • Full impl-hygiene pass over every file this section touches, with findings fixed inline rather than filed.
  • TDD matrix BEFORE the fix, dimensions named explicitly: type x pattern x executor over the changed ownership path. Missing cells are future regressions.
  • Production-path semantic pin exercising the REAL entry point on a REAL target and asserting the real deliverable, PLUS a negative pin that rejects the broken behavior. A seam-injected unit the production caller never threads is NOT coverage (INVERTED-TDD:seam-injected-only-coverage).
  • Debug AND release across every affected admitted executor, with observably identical output / drop / unwind behavior, plus zero leaked owners under ORI_CHECK_LEAKS=1 on every memory-touching projection.
  • Required performance comparator evidence per CLAUDE.md §Performance North Star, on output-checked workloads — ALL THREE, none optional: (a) compiled Ori vs equivalent pinned optimized C; (b) strict-interpreted Ori vs pinned CPython 3; (c) strict-interpreted Ori vs pinned LuaJIT with JIT DISABLED (-joff) — the strict-interpreter completion target. Clearing the Python floor alone is NOT mission completion. A missing, inconclusive, bypassed, or non-work-equivalent comparator — including a missed LuaJIT -joff floor — is PERFORMANCE:required-comparator-gap / PERFORMANCE:interpreter-luajit-north-star-miss Critical UNFINISHED work at this gate, never a pass.