100%

S02 Partition infrastructure - the identity layer

Goal

The per-(ArcVarId, FieldPath) birth-site union-find exists as a typed AimsStateMap side-table (Invariant-5 avenue (c)), fully tested, with ZERO emission consumers - the identity substrate S03+ consumes.

Design constraints (verified against source this session)

  • Built ALONGSIDE compute_genuine_same_alloc_reps (aims/intraprocedural/project_aliases.rs) and ForwarderUnionFind (lower/burden_lower/ownership_scans/union_find.rs) - their deliberate phi/Select exclusions stay untouched (DE-181); the new keying makes those edges per-field-sound ONLY under the singleton-birth-site witness.
  • Integration point per reviewer consensus: a field on AimsStateMap alongside immortals, borrow_sources, project_alias_sources; populated once before Step-4b emit_burden_ops; read-only for Phase 6 eliminate_burden_ops + Phase 7 lowering; debug_assert at Phase-6 entry.
  • Sharing-view CREDIT is a ReturnContract field (avenue (b)) seeded for slice/substring/take/drop; the codegen-side +1 those producers emit becomes a typed ledger fact.

Work Items

  • Implement the per-(ArcVarId, FieldPath) birth-site union-find per T1 admission: tier-1 edges (Let{Var} alias, Project field-path composition, Construct field funding, ReturnAliasShape contract aliases); phi/Select edges ONLY under the singleton-birth-site witness; COW-mutating uses are class boundaries (DE-181 taint) - built ALONGSIDE compute_genuine_same_alloc_reps + ForwarderUnionFind, never by broadening them
  • Land the partition as an AimsStateMap side-table field (alongside immortals, borrow_sources, project_alias_sources), populated once before Step-4b emit_burden_ops, read-only for Phase 6 + Phase 7; debug_assert at Phase-6 entry that the side table is populated iff burden ops carry per-field provenance
  • Matrix tests: excluded edges stay DISTINCT (non-witnessed phi over distinct birth-sites, distinct-birth Select, COW boundary, loop back-edge invariant-vs-per-iteration allocation - the PerFieldBirthSiteUnionFind loop shapes as Rust unit tests); tier-1 subset agrees with compute_genuine_same_alloc_reps (no false unification, no missed tier-1 union)
  • Add the ReturnContract buffer-provenance sharing-view CREDIT field (Invariant-5 avenue (b)); seed sharing-view builtins (slice/substring/take/drop); IC-3/IC-4 join rules + unit tests
  • Verification: full ./test-all.sh green (zero emission change this section); cross-executor behavior, exact logical ownership/drop/unwind-event, and leak legs recorded

Governing rules (embedded per plan self-containment)

  • Calculus-first per arc.md CP-1: the governing theorem lands in compiled Lean BEFORE the consumer ships; never weaken a theorem to pass a shape; four-surface sync per CP-2 on every AIMS change.
  • Verdict surface until S08 lands: the gated burden-sole probe ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1 via compiler_repo/diagnostics/aot-guardrail.sh --floor (debug AND release), zero-new vs compiler_repo/compiler/ori_llvm/tests/aot/fixtures/corpus_under_flag_gate/baseline_failing_ids.txt. The default path is FALSE-GREEN until S08 (per arc.md STOP); never cite it as an RC verdict.
  • test-all is the compiler-state SSOT: every section-close verdict comes from a full ./test-all.sh run (background, flock-serialized; consume test-all-summary.json), never targeted runs alone.
  • Banned cures (each a carried dead-end): use-count/type-membership PROXY discriminators (DE-150/174/175); broadening compute_genuine_same_alloc_reps / ForwarderUnionFind phi edges (DE-181); relocating a release past a multi-pred merge (DE-225/243/249/250); inc-only pair splits (attempt-287 290-UAF class); broad caller-side keep-alive incs (DE-254).
  • Every retired scan/toggle records a KEPT ledger cycle with before/after teeth (collapse metric + floor).
  • Cross-executor parity over evaluator, VM, LLVM debug/release/AOT, and admitted native/direct-WASM/JIT projections, plus exact logical ownership/drop/unwind-event correspondence and leak freedom, are per-section backend legs (L9 + L10). The AOT burden probe remains a current LLVM-projection migration gate, not the definition of AIMS correctness.

Test strategy

  • Matrix: excluded edges stay distinct (non-witnessed phi over distinct births; distinct-birth Select; COW-taint boundary; loop back-edge invariant-vs-per-iteration allocation). Tier-1 subset parity with compute_genuine_same_alloc_reps (no false union, no missed union).
  • Semantic pins: the PerFieldBirthSiteUnionFind loop shapes (items invariant unified across back-edge; label per-iteration distinct) as Rust unit tests over the REAL structure.
  • Zero emission change: full ./test-all.sh green; L9 parity + L10 leak legs recorded.

Fresh intel (regenerated)

S02 is done, and the shipped code is a faithful — in one decisive respect STRONGER-than-demanded — Rust promotion of the S01 Lean model. Every work item is verifiable in source at HEAD: BirthSitePartition + FieldPath + BirthSiteId land in aims/intraprocedural/birth_site_partition.rs (447 lines, 8 unit tests); the population pass compute_birth_site_partition lands in birth_site_population.rs (704 lines, 12+ unit tests incl. the full w-0cf2d784 matrix — loop-invariant-vs-per-iteration back-edge, distinct-birth Select, COW boundary, tier-1 parity with compute_genuine_same_alloc_reps, AND a split_site_conditional_partition_refuses_genuine_over_approx pin proving the new partition REFUSES an over-approximation the whole-var union-find would admit); the side table is populated exactly once in pipeline/aims_pipeline/mod.rs:239-247 (after Step 4a TRMC verify, before Step 4b emit_burden_ops, with a doc comment citing PL-5 + AimsProof.Partition); the Phase-6 entry debug_assert sits at aims/realize/burden_elim.rs:180-185; and the sharing-view CREDIT ships as ReturnContract.returns_sharing_view (contract/mod.rs:693) with an AND-join (:735, the IC-4 preserves_freshness pattern) seeded on the unambiguous runtime names ori_list_slice_take/ori_list_slice_drop + the sharing_builtin_names set (builtins/mod.rs:91-101,224-229,382-400).

The strongest single fact for any downstream reader: the Rust API is structurally witness-gated. The prior pre-execution recon’s sharpest kill-criterion was “a bare public union(a, b) with the witness check left to caller discipline is a REGRESSION from the Lean model” — the shipped API forecloses this: union_phi_witnessed(merge_node, preds) -> bool (birth_site_partition.rs:149) is the ONLY phi/Select admission entry point, it internally checks the singleton-birth-site witness (every predecessor’s class carries a KNOWN site, all agree, the merge node’s own class carries no distinct one), and the raw union_roots is private. Negative pins cover unknown-site predecessors, empty predecessor lists, and distinct-site refusal (birth_site_partition.rs:373-383,336-354). The Adm inductive’s unrepresentability guarantee survived the port as an API-shape guarantee.

Second decisive fact: the “ZERO emission consumers” contract holds at HEAD. The SOLE production reader of state_map.birth_site_partition() is the Phase-6 entry debug_assert in burden_elim.rs:183 — grep-verified; S03 (in-progress) has NOT yet landed a consumer (no LedgerEvent/derive_ledger/ledger-emitter module exists in ori_arc yet). Anyone consuming this dossier for S03+ work starts from a clean, tested, unconsumed substrate.

Third: the three pre-existing union-finds (ssa_alias_classes::UnionFind — LEGACY, retiring; compute_genuine_same_alloc_reps; ForwarderUnionFind) remain untouched hazards (DE-181: widening their phi edges regressed 27 AOT cells) — the partition was built ALONGSIDE them exactly as licensed by plans/aims-burden-tracking/content/decisions/19-per-field-allocation-identity-union-find-lean-license.md. The graph now shows FOUR structurally-similar union-find shapes (§5); this is deliberate, litigated, and NOT a consolidation target until S08 deletes the predicate stack.

Decisions this package forces on the next consumer (S03 ledger-emitter-core worker, or any reviewer):

  1. Consume the partition READ-ONLY via state_map.birth_site_partition() — CH4_state_map_immutable (AimsProof/Coexistence.lean) licenses the side table as a Phase-5 pre-pass read; a Phase-6/7 mutation of it is a calculus violation, not a style issue.
  2. Route every phi/Select admission through union_phi_witnessed — never add a second admission path or expose union_roots; the witness-gated API IS the ported soundness guarantee.
  3. The debug_assert at burden_elim.rs:183 is DEBUG-ONLY; when S03 makes the partition load-bearing for elimination verdicts, decide whether the populate-iff-burden-ops contract needs a release-active check (precedent: BUG-04-240 promoted exactly such a guard to release-active assert! per IA-MF1).
  4. aims-burden-tracking#s-cba6624a (“per-field-allocation-identity-provenance-infrastructure”, still not-started) duplicates S01+S02’s delivered scope — fold it explicitly at S11 sunset; it is now OBE in substance.
  5. Do NOT touch compute_genuine_same_alloc_reps / ForwarderUnionFind / ssa_alias_classes::UnionFind to “reuse” the new per-field identity — the DE-181/DE-253 dead-ends carry verbatim teeth; the parity test (tier1_parity_with_genuine_same_alloc_reps) is the sanctioned bridge between the old and new structures.

DIG DEEPER

python -m scripts.plan_corpus.read plans/aims-provenance-ledger
grep -rn "birth_site_partition()" compiler_repo/compiler/ --include="*.rs" | grep -v tests
cat plans/aims-burden-tracking/content/decisions/19-per-field-allocation-identity-union-find-lean-license.md

(full dossier: partition-infrastructure—s-0e5fb06f.intel.md)