0%

Section 03: AIMS Projection and Ownership Authority

Context

The previous section targeted a removed take_project subsystem and proposed two invalid authorities:

  • infer ownership transfer from MachineRepr::UnmanagedPtr;
  • ask physical enum layout whether projection field 0 is a tag.

Live AIMS instead uses semantic ArcInstr::Project fields, project-alias propagation, (variable, FieldPath) birth-site partitions, consume/read events, and class-ledger release placement. Annex E defines projection semantics in TF-4, TF-14, RL-33, and §12.

A physical tag is not an ARC IR field, and machine representation is not ownership provenance.

This section audits the old leak report against the current implementation and then locks the clean seam. If the report reproduces, repair the current partition/ledger path in this section before continuing.

If it does not reproduce, record an evidence-backed OBE disposition and retain the reproducer as a regression pin. Do not resurrect take_project, in_class, lineage reconciliation, or an ownership tag whitelist.

03.1 Current-Pipeline Audit and Defect Disposition

  • Query the intelligence graph for projection, alias, partition, consume-mark, release-decomposition, and cleanup consumers; then verify live source. Map the removed symbols to current owners in project_aliases, birth_site_population, birth_site_partition, class-ledger event derivation, hazard decomposition, release emission, and verification.
  • Reconstruct the old predecessor/merge leak as a production-path TDD matrix over semantic ARC IR: owned payload projection, borrowed projection, predecessor block argument, multi-predecessor merge, loop header/back edge, nested projection, path-dependent move, unwind edge, and unrelated field.
  • Run the matrix first against the kernel/checker-backed AIMS partition, ledger-event, release-site, and panic/unwind obligations. Then validate sibling physical realizations separately: use ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1 only for the current compiled-counter adapter’s RC/AOT floor, and require the VM plan’s exact event-satisfaction trace and final-live-zero result independently. Neither physical result defines the calculus.
  • If any cell leaks, double releases, or violates a verifier clause, fix the current partition/ledger algorithm with tests first. The fix must preserve per-path net zero, read floor, mutation floor, and frame-limited non-interference from Annex E §12.
  • If all cells pass, record the removed implementation and original claim as OBE in this section with current source/spec/test evidence. Keep the matrix permanently; absence of the old symbols alone is not proof of correctness.
  • Add teeth tests that deliberately corrupt a field-path class, consume mark, or release skip set and prove the partition/ledger verifier rejects the exact leak or double-release condition.
  • Verify existing iterator, Option/Result, enum projection, collection, match, and branch/loop ownership suites against the frozen logical plan, then through both the validated VM projection and the burden-sole compiled-counter adapter in debug and release. Default predicate-stack results are diagnostic only and cannot establish the compiled adapter’s floor.
  • Record a current pipeline map and dependency contract in AIMS/repr documentation after the audit. Remove stale comments or plan references that name the removed take-project lineage system.
  • Close the audit only when the original report has one of two explicit outcomes: reproduced and fixed with a semantic pin, or OBE with a passing production-path reproducer and verifier teeth.

03.2 Semantic Projection Seam

  • Define and test the invariant that ArcInstr::Project.field is a semantic source-level field identity. It never includes a physical tag, padding, payload wrapper, VM slot, or compiled aggregate element.
  • Make ownership-transfer classification consume AIMS-owned terminal-use, parameter-contract, provenance-partition, and consume-mark facts. Ban MachineRepr, pointer kind, target ABI, enum encoding, and backend type from the classification API.
  • Remove or reject any AIMS dependency on EnumLayoutInfo::field_is_tag, CompiledEnumLayout, VmEnumLayout, or physical field indices. VM and compiled-layout adapters alone translate semantic (variant, field) identity to physical storage.
  • Add layout-independence differential tests: hold canonical ARC IR constant, vary admissible compiled and VM enum encodings, and prove AIMS state maps, partition classes, and frozen logical ledger events are byte-identical. Physical action streams may differ only through separately validated satisfaction mappings.
  • Add semantic ownership matrices for unique-looking but differently owned payloads: iterator-like values, RC-managed references, opaque/FFI pointers, borrowed views, nested fields, and future unique-owned types represented through typed contracts. Representation equality must not imply ownership equality.
  • Export only the post-AIMS typed facts required by ExecutableProgram consumers. Validate stable field IDs and drop/trace obligations at the boundary; do not export AIMS internal union-find nodes or let any physical executor reclassify terminal use.

03.3 Completion Checklist

  • The old take-project leak claim is reproduced and fixed or explicitly proven OBE against the AIMS logical verifier plus independent VM and compiled-plan satisfaction gates.
  • Projection aliases, birth-site partition classes, consume marks, and release plans satisfy Annex E TF-4, TF-14, RL-33, and §12 under merge, loop, and unwind control flow.
  • Negative verifier pins reject corrupted alias, partition, consume-mark, and per-field release data.
  • Ownership classification uses typed AIMS semantic facts, never MachineRepr or pointer representation.
  • AIMS has no dependency on physical enum tag/payload positions or either physical layout plan.
  • Changing only enum physical encoding leaves AIMS facts and frozen logical event identities identical; only validated physical actions may differ.
  • Production-path tests cover predecessor merge, loop, nested projection, path-dependent move, and unwind cleanup.
  • Leak verification ends with zero live allocations across the full projection matrix.
  • Canonical test-all is green with no suite error or crash.
  • Format, lint, seam, and repository-hygiene gates are clean.
  • Third-party review is clean and all validated findings are fixed.
  • Implementation-hygiene review is clean after third-party review.
  • AIMS/spec/documentation sync is clean and names only the retained architecture.

03.R Third Party Review Findings

  • The old section is stale at the symbol and pipeline level; none of its named take-project data structures exist in live ori_arc.
  • MachineRepr::UnmanagedPtr is a storage category, not evidence of ownership transfer. Using it would couple AIMS correctness to representation selection.
  • A semantic projection field cannot be a physical enum tag. The prior field_is_tag dependency inverted the compiler seam and would make AIMS behavior target-dependent.