Section 09: Post-Convergence Partial Retirement + PIN-1..6 Retirement

Goal: Retire the predicate-stack emission predicates and the path-sensitive class_payload_of patches; preserve non-predicate functions in post_convergence.rs per per-function audit. Remove the coexistence handshake under proven-equivalence license + record the CH-proof disposition.

Context: Per proposal §Migration / Breaking Changes + §09 + codex R5 code-graph verification (most of post_convergence.rs’s 13 functions serve non-predicate lattice-population purposes; only the path-sensitive predicate-stack-soundness patches retire — per the §09.1 per-function disposition) + R10 F4 path correction (file is in intraprocedural/, not realize/). This is a partial retirement, NOT full module deletion. The coexistence layer the handshake mediates is the predicate-stack ↔ burden-op COEXISTENCE bridge whose soundness aims-proofing-suite §11 machine-checked (CH-1..CH-comp). §09’s retirement is the proven-equivalence-licensed deletion of the now-redundant predicate_stack_path; it is NOT a re-implementation, and it does NOT invalidate the CH proofs.

Reference implementations: The proven §11 coexistence corpus at compiler_repo/aims-proof/proofs/11-coexistence/ + compiler_repo/aims-proof/lean/AimsProof/Coexistence.lean (the Handshake.proof SSOT defines burden_emission_path (Function 1), predicate_stack_path (Function 2 — the path this section retires), and the class_covered/mixed/uncovered partition the retirement licenses against).

Depends on: Section 07B — broad-shape burden self-sufficiency; frontmatter depends_on: [07B]. §07B is status: in-progress, reviewed: false, CLOSE-DEFERRED-EXTERNAL: its four WORK deliverables (07B.1 probe-gateable broad-shape self-sufficiency proof, 07B.2/07B.3 §09.2-territory residual classification, 07B.4 corpus-under-flag SET-subset gate-harness + checked-in baseline-16 failing-ID fixture) are all COMPLETE; only the 07B.R/07B.N bookkeeping subsections stay open, and the reviewed: true close is gated on a CROSS-SCOPE baseline_regression flip-gate cleared by a user-typed /commit-push --bypass (an external gate, NOT a §07B work residual). The §07B→§09.2 handoff IS complete: §07B set probe_gateable_surface_exhausted: true, drove under-flag 517→115, and delivered the classification + harness + fixture §09.2 consumes. §09’s depends_on: [07B] is therefore SATISFIED + reachable — the inv19 07B branch → {09, 13} charter-exemption (ratified §00.R.H) ratifies the parallel topology where §09 and §13 both consume §07B’s completed deliverables; this is NOT an unreachable-dependency. §09 proceeds on the COMPLETED §07B deliverables; the deferred-external reviewed: true flip on §07B does not gate §09 work because the deliverables §09.2 consumes are the WORK subsections (complete), not the bookkeeping close. §07A (status: complete, reviewed: true, closed 2026-06-04) made the burden path a standalone RC emitter for the NARROW shapes its 11-probe ORI_DISABLE_PREDICATE_STACK_RC suite covered (move-alias / dup-alias / borrow-chain / collection-buffer-last-use / closure-capture / partial-move), but the 2026-06-04 §09.2 re-measurement proved that gate TOO NARROW: under the flag the full AOT corpus regresses 2344/16 → 1784/576 (+560) on broad shapes the 11 probes never exercised (iterator-from-collection / fat-pointer-matrix / iter-RC-chain / collection-element / SSO). §07B PROVES the probe-gateable broad shapes self-sufficient (under-flag 517→115), CLASSIFIES the §09.2-territory residual, and replaces the narrow 11-probe gate with the full-corpus-under-flag SET-subset readiness signal (failing_ids_under_flag ⊆ baseline_failing_ids); the corpus-wide COMPLETION of that signal is §09.2’s own Phase-5 emission work (the ~99 JOINT residual, M-c-banned during coexistence). The proven-equivalence license precondition for §09.2/§09.3/§09.4/§09.N has TWO halves — §07’s universal class_covered (coverage, MET) AND corpus-wide burden-lowering self-sufficiency (MET for narrow shapes via §07A; the probe-gateable broad shapes proven via §07B; the corpus-wide remainder COMPLETED at §09.2 itself, NOT a §07B deliverable). §08 (rule sync + proof re-validation) is a PARALLEL branch per the 00-overview.md DAG (§08 ∥ §09, both gating §10), NOT a predecessor.

Intelligence Reconnaissance

Queries:

• scripts/intel-query.sh --human file-symbols "compiler_repo/compiler/ori_arc/src/aims/intraprocedural/post_convergence.rs" --repo ori — full function list
• scripts/intel-query.sh --human callers populate_class_payload_of_with_liveness --repo ori
• scripts/intel-query.sh --human callers populate_borrow_sources --repo ori
• scripts/intel-query.sh --human callers ssa_alias_classes --repo ori
• scripts/intel-query.sh --human callers eliminate_burden_ops --repo ori — CH-4 shipped-binding survivor set (must remain post-retirement)

Queried: 2026-05-08; 2026-06-02 (CH-proof-disposition reconciliation — eliminate_burden_ops confirmed as the CH-4 shipped anchor that survives retirement).

Results summary [ori]: post_convergence.rs holds 13 functions; populate_class_payload_of_with_liveness (line 871) + populate_borrow_sources (line 110) confirmed at edit time. Per-function audit required. eliminate_burden_ops (CH-4 shipped binding, compiler/ori_arc/src/aims/realize/burden_elim.rs:83) is consumed by the burden path and persists post-retirement.

09.1 Per-function disposition table for post_convergence.rs

File(s): plans/aims-burden-tracking/decisions/09-post-convergence-disposition.md (new)

• Inventory + tag all 13 functions resident in post_convergence.rs (inventory at edit time: populate_class_covered, populate_borrow_sources, populate_sparse_events, populate_call_result_states, populate_var_shapes, detect_trmc_candidates, populate_context_events, class_lifetime_extends_past_path_sensitive, record_payload_edge_lifetime, dst_strategy_of, container_payload_moved_out, populate_class_payload_of_with_liveness, populate_class_dec_obligations — re-confirm via scripts/intel-query.sh --human file-symbols at edit time). Tag each: RETIRE (predicate-stack patch only) / MIGRATE (relocate to lattice-input) / PERSIST (already serves lattice-input role). The lattice-population functions PERSIST; the path-sensitive predicate-stack-soundness patches RETIRE.
• Path-sensitive class_payload_of patches (introduced to plug predicate-stack soundness): RETIRE.
• Decision document authored at plans/aims-burden-tracking/decisions/09-post-convergence-disposition.md (commit lands before §09.2 retirement edits — orchestrator commit step).

Subsection close-out (09.1) per protocol.

09.2 Emission-side predicate retirement

Retirement basis (per aims-rules.md §8 RL-2/RL-4/RL-5 + CH2_single_elimination): the burden path realizes the SAME proven dec-placement without the predicate stack. The predicates being removed (class_alive_after, pin4_class_emits_dec_set, pin6_any_ancestor_will_cover, …) are the predicate-stack approximation of the dec-placement that RL-2/RL-4/RL-5 prove and Phase-5 trivial burden emission realizes directly: RL-2 (AimsProof.Realization::RL2_dec_at_last_use) dec at last use / scope exit, RL-4 (RL4_edge_dec_decision) edge-specific decs + Jump exemption, RL-5 (RL5_dead_at_entry_cleanup) dead-at-entry cleanup. With BurdenDec emitted at every transfer/last-use and DP-2/DP-3 eliminating the redundant ones (proven CH2_single_elimination), the predicate-stack predicates have no remaining consumer.

• Remove class_alive_after from realize/walk_dec.rs.

• Remove pin6_any_ancestor_will_cover from realize/walk_dec.rs.

• Remove pin4_class_emits_dec_set from emit_rc/dead_cleanup/emission_site.rs.

• Remove var_emits_dec_in_block (emit_rc/dead_cleanup/emission_site.rs:95). For canonical_rep_for: CONFIRM ABSENCE — no fn canonical_rep_for resolves under compiler/ori_arc/src/ at edit time (already removed upstream); the item is a no-op confirm-gone, not a deletion.

• Audit is_rc_managed callers; remove predicate-stack uses; preserve any non-predicate uses with rationale recorded in disposition table.

• COD-F1 — Burden* exclusion from the dead-cleanup liveness scan (relocated from §09.3 → §09.2 per routing.md §4; originally relocated from §04A.R — latent fragility, §09-coupled; its scope is dead-cleanup liveness scanning in emit_rc/dead_cleanup/mod.rs, an EMISSION-side concern, NOT ssa_alias_classes consumer simplification, so it belongs in §09.2 alongside the Phase-1.5 fallback reshape) — emit_rc/dead_cleanup/mod.rs:~596 emit_dead_invoke_dsts: the Phase-1.5 fallback used_in_succ scan counts Burden* ops as a live use via ArcInstr::used_vars() (ir/instr.rs:336-347). Latent fragility ONLY — manifest-leak-free today (a genuinely-dead Invoke result receives NO BurdenDec; last-use BurdenDecs co-occur with the real use; verified zero leaks per §04A.R COD-F1 evidence: 3 repros + ORI_CHECK_LEAKS=1). When the predicate-stack retirement above reshapes/removes the Phase-1.5 fallback sweep, exclude Burden* ops from the used_in_succ liveness scan (a Burden op is a release marker / codegen no-op, NOT a real use — mirrors §06.1 compute_live_out_owned + borrowed-alias-exclusion). Matrix tests: semantic pin (dead Invoke result with a successor BurdenDec still gets its real cleanup) + negative pin (a genuine real successor use still suppresses cleanup); VF-1 stays 0, AOT zero-new. Cite: §04A.R COD-F1 finding (full grounding evidence) + LEDGER §B.2.

• Remove the 6 BUG-04-123 surgical predicate-stack fixes (decisions/07 §2 — the patches that drove the predicate-stack model 32 -> 17; annotations the burden path supersedes, mirroring BUG-04-118’s 62): class_member_suppresses post-dominance / cross-class-uaf dedup (emit_rc/dead_cleanup/emission_site.rs:411); build_global_pin4_emits (realize/emit_unified.rs:285) + build_lineage_map (realize/walk.rs:500) + predict_retained_roots (realize/walk.rs:418) consumption-aware retained-lineage machinery; container_payload_moved_out payload-edge suppression (intraprocedural/post_convergence.rs:842); the PIN-4 defined_at_or_before reachability guard (consumed in emit_rc/edge_cleanup.rs; helper compute_defined_at_or_before in emit_rc/trampoline.rs). The four uncoordinated emission paths these patch (class_dec_should_emit realize/walk_dec.rs:466 / collect_branch_edge_decs emit_rc/edge_cleanup.rs:273 / collect_invoke_edge_decs emit_rc/edge_cleanup.rs:517 / emit_dead_at_entry_decs emit_rc/dead_cleanup/mod.rs:53) collapse to the single burden trivial-emit + DP-2/DP-3 elimination path. Re-confirm each symbol residence at edit time.

• Phase-5 broad-shape burden-emission COMPLETION (the §07B-classified §09.2 residual) — complete the ~99 under-flag-only JOINT M-c-banned shapes §07B classified as §09.2-owned (section-07B-broad-shape-burden-self-sufficiency.md 07B.1/07B.2/07B.3 CLASSIFY checkboxes; under-flag 115 at the attempt-67 probe_gateable_surface_exhausted floor = baseline-16 + ~99 JOINT). M-c-unblocked HERE because the predicate-stack retirement above removes the coexistence (no double-emit; attempt-55’s default 16→61 regression was coexistence-only). LEDGER D08 ~99-JOINT shape inventory (the under-flag-only set, inlined so §09.2 is executable without re-reading the external ledger; SSOT cross-ref: plans/aims-burden-tracking/decisions/LEDGER.md §D08 for the per-attempt provenance):

  Class	Shape cohort	Approx IDs	Cure-side	Attempt provenance
  M-a	generics forwarder transfer-through-return	~20	callee transfer-source-dec strip + caller keep-alive-inc	54/55/64
  M-a	fat_ptr_iter iterator-handle / catch-panic-edge	~15-16	iterator-handle JOINT (M-a transfer)	64/67
  M-c	narrowing / for_yield_option / elem_dec_scope per-element	~12	faithful per-element emit_dead_at_entry_decs + elem_dec_fn	9/10/11
  M-c	fat_matrix / iter_rc_matrix / rc_matrix per-path	matrix	per-CFG-path structural last-read (RL-2 LastReadBeforeScopeExit)	9/10/11
  Cure-A	rc_matrix / stress / string_sso / cow_map_set dead-vs-survives + COW-shared-survives	~29	buffer-provenance ParamContract/ReturnContract field (clone vs slice/substring/COW-push)	62/66/67

  (~20 + ~16 + ~12 + matrix + ~29 ≈ 99 JOINT; the exact count is the empirical under-flag 115 minus the baseline-16 = 99 at the attempt-67 floor — re-confirm the live count via the §07B.4 corpus-under-flag gate at edit time, the table is the cohort decomposition not a frozen tally.) Surface (per the LEDGER D08 inventory above + §07B classification):

  • M-a callee transfer-source-dec strip + caller keep-alive-inc in compiler_repo/compiler/ori_arc/src/lower/burden_lower/mod.rs + emit_burden_ops for the generics forwarder transfer-through-return (~20 IDs, attempt-54/55/64) + fat_ptr_iter iterator-handle/catch-panic-edge (~15-16 IDs, attempt-64/67) JOINTs.
  • Faithful per-element emit_dead_at_entry_decs with elem_dec_fn accounting (compiler_repo/compiler/ori_arc/src/aims/emit_rc/dead_cleanup/mod.rs) for the per-CFG-path structural last-read shapes (narrowing/for_yield_option/elem_dec_scope per-element + fat_matrix/iter_rc_matrix/rc_matrix per-path, ~12 + matrix IDs) — the exactly-one-of-N-exits dec the alloc-aware net cannot express (RL-2 LastReadBeforeScopeExit), now safe because the predicate stack no longer co-emits the over-fire (attempt-9/10/11 459→596/642 was coexistence over-fire).
  • Dead-vs-survives-after-concat + COW-shared-survives liveness verdicts for the rc_matrix/stress/string_sso/cow_map_set Phase-5-coupled shapes (~29 IDs, attempt-62/66/67); GROUND-FIRST per arc.md §CP-1 the LEDGER D08 Cure-A buffer-provenance ParamContract/ReturnContract field (clone vs slice/substring/COW-push + COW-realloc-through-borrowed-param) — prove RL-4/RL-5 cover COW-realloc-through-borrowed-param in scratch Lean if genuinely missing, THEN extend the contract field (Invariant-5 (b)).
  • Iterate-until-converged: re-run the §07B.4 corpus-under-flag gate (ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_CHECK_LEAKS=1 cargo test -p ori_llvm --test aot) after each completion step; the work is the Phase-5 emission, the gate is failing_ids_under_flag ⊆ baseline_failing_ids, the §09.4 CH-4 deletion is gated on the verdict reaching EMPTY (decisions/11 form-(b) reversible-by-non-execution — the predicate stack STAYS until then). VF-1 burden-balance 0 corpus-wide (ORI_VERIFY_ARC=1); eval+LLVM parity; debug+release.

• Per-cycle test-all VERDICT gate (user directive 2026-06-11; CLAUDE.md §Test & Doc Disciplines test-all-SSOT rule). Every grind-cycle / bug-fix close VERDICT comes from a full ./test-all.sh run (background, flock-serialized; consume build/test-all-summary.json): zero suite ERR/CRASHED + no new failures vs the prior summary. Targeted suite runs are mid-cycle iteration only. ANY test-all defect = BLOCKER routed via /fix-bug before plan work continues (current open set: BUG-04-157 mid-suite unwind SIGSEGV crashing the spec-LLVM leg, BUG-07-216 spec-LLVM in-process-JIT isolation gap, BUG-07-214 baseline-capture stale cache).

• Phase-5 grind cluster tracker (the orchestrator-trackable completion surface for the incremental burden-grind — the COMPLETION parent above is the coarse one-checkbox-for-122-cells that never flips per-serve; these per-cluster sub-items flip as each cluster’s burden cells reach guardrail-2 green, giving the per-cycle completion progress the orchestrator needs; added 2026-06-09 to resolve a /continue-roadmap route_no_completion_progress halt — the grind was healthy 130→122 but structurally invisible to the checkbox-completion orchestrator). Each cluster cleared via the proven pattern: precise structural discriminator + alloc-aware-net (compute_lineage_alloc_aware_net/compute_burden_entry_nets/same_alloc_reps), NEVER a use-count/membership proxy; guardrail-2 comm -13 (NEW vs baseline) EMPTY gate; calculus-first per arc.md §CP-1 (case-(a) impl-fix, NO Lean weakening); LEDGER §0 + §B.2 = the per-cluster derivation SSOT; sub-roots within a multi-root cluster get their own line as discovered (each its own guardrail-2 cycle).

  • fat_ptr_iter reuse-after-iter (Phase 6.66b; §B.2 241; 131→130)
  • fat_ptr_iter element-into-returned-collection (Phase 6.68b; §B.2 242; 130→129)
  • fat_ptr_iter single-borrowed-Invoke source-strip (Phase 6.66c; §B.2 243; 129→123, 6 cells)
  • fat_ptr_iter N=2-returned-scalar-list surplus-strip (Phase 6.68c; §B.2 244; 123→122)
  • fat_ptr_iter remainder (~8: conversion __index-COW-state-aware dec + yield-Some/Tuple-wrap keep-alive, unwind, control_flow, str_list, method_collect — conversion is heterogeneous per §B.2 DEAD-END, NOT a single shared root)
  • for_yield_option (cured at the attempt-73 floor=104 milestone via the Phase-5 compute_construct_fed_dead_param_lineage RL-5 dead-param release; verified terminal 2026-06-11 — zero for_yield_option cells in the gated 77-set; pins probe_construct_fed_dead_param_for_yield_option_str_no_leak + the over-fire negative green)
  • generics-forwarder transfer-through-return (~14; the hard core — model the callee ReturnContract ownership to distinguish transfer-dup from alias-spurious; attempts 54/55/64 over-fired, dedicated cycle)
  • match_alias (6 live at floor-77; attempt-98 REVERTED both cure directions — NOT a uniform burden-emission gap; decomposes into the blocked_by bug families: struct-intlist UAF = BUG-04-156, closure-env x3 + Select-branch PIN-2-EXCLUDE = BUG-04-159 territory, panic-message chars()-copy = BUG-04-160; route via /fix-bug per the both-paths-fail row, teeth at LEDGER attempt_n-150)
  • fat_matrix (~7)
  • narrowing (~6)
  • rc_matrix loop-carried (~5; the BUG-04-156 close landed the unified per-edge identity — re-measure this cluster at the 69-floor before the next cycle; the attempt-34 constraint is now the conservative back-edge decline in chain_root.rs)
  • recursive_derive (~4)
  • elem_dec_scope (~4)
  • both-paths-fail (29 cells — INDEPENDENT AIMS bugs failing on BOTH the burden AND predicate paths; route via /fix-bug separately; §09.2 burden-green is blocked_by those, NOT a burden-emission gap)
  • iterate-until-converged: re-run the §07B.4 corpus-under-flag SET-subset gate after each cluster; the grind is DONE when burden-default AOT = 0 failing cells AND the gate verdict is EMPTY

• Real-RC activation — BurdenInc → RcInc, BurdenDec → RcDec mechanical mapping (relocated from §06.1 per routing.md §4; §06 established the clean lowering SITE at realize/mod.rs, §09.2 owns the activation). Once the parallel predicate-stack RC emitters above (walk_dec.rs/emit_unified.rs) are removed AND the Phase-5 broad-shape completion above lands, the burden ops are the SOLE RC emitter — flip them from codegen no-op markers (the ArcInstr::BurdenInc { var: _ } | ArcInstr::BurdenDec { var: _ } arm at compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/instr_dispatch.rs:523) to real RcInc/RcDec (atomicity carrier per §06.3 RcAtomicity) in compiler_repo/compiler/ori_arc/src/aims/realize/mod.rs. This is now SAFE because no predicate stack co-emits → no double-emit → no double-frees (the LEDGER §B.2 hazard dissolves with the predicate-stack removal, NOT before it). The baseline-16 §09-coupled cohort (BUG-04-123 predicate-stack double-frees + BUG-04-121 VF-1 loop residuals per LEDGER §B.3) dissolves at THIS flip (class (i)); the ~99 JOINT residual (class (ii)) dissolves via the Phase-5 completion above — §09.2 owns BOTH. Verify VF-1 balance holds post-flip + zero new double-frees corpus-wide.

• §07B predicate-stack-retirement readiness verification + the ⊆16 PASS VERDICT (routed from §07B.4 per decisions/11 L57) — §07B.4 AUTHORED the gate-test harness + captured the baseline-16 SET as a checked-in fixture (the gate’s LEFT operand); §09.2 owns the RUN + the VERDICT. After the Phase-5 broad-shape completion + the BurdenInc→RcInc flip above, RE-CAPTURE the baseline failing-ID SET on §09.2’s own working tree (predicate-stack-ON cargo test -p ori_llvm --test aot, per the fixture’s re-capture protocol — predicate-stack-emission changed under §09.2, so the §07B.4-captured baseline must be refreshed before the subset assertion is trustworthy), THEN run ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_CHECK_LEAKS=1 cargo test -p ori_llvm --test aot and assert failing_ids_under_flag ⊆ baseline_failing_ids (a SET-subset, NOT a count). False-green guard (codex-F, corpus_under_flag_gate.rs:196): the gate harness MUST assert the under-flag subprocess exited with SUCCESS status (or a known test-failure exit code that still produced a parseable failing-ID list) BEFORE it computes the new_ids_over_baseline / failing_ids_under_flag ⊆ baseline_failing_ids subset comparison — an ABORTED run (ICE, panic-in-harness, signal, build failure) emits an empty or truncated failing-ID set that the naive subset check parses as “zero new failures” = a FALSE GREEN. Order the check: (1) subprocess status is a recognized completion (not abort/signal/build-fail), ELSE the gate FAILS loud (assert!/explicit error, never silently passes); (2) the failing-ID list parsed non-degenerate; (3) THEN the subset assertion. A degenerate-empty under-flag set from a crashed run is a gate-harness defect to surface, never a pass. The §09.2 execution (2026-06-04) empirically proved the §07A narrow 11-probe suite (compiler_repo/compiler/ori_llvm/tests/aot/predicate_stack_probe.rs) TOO NARROW as the readiness signal (full corpus 2344/16 → 1784/576 under the flag); §07B drove it to 115 (probe-gateable-exhausted) and §09.2’s Phase-5 completion + activation drive it to the ⊆16 EMPTY verdict (the residual 115 = baseline-16 dissolving at the flip + ~99 JOINT dissolving via the completion). The 11 probes re-run GREEN under ORI_CHECK_LEAKS=1 here as narrow-shape regression pins (they no longer SUBSTITUTE for the corpus gate). A residual comm -13 baseline⊄under-flag (any new ID outside the refreshed baseline set) or a red 11-probe is a §09.2 readiness defect cured before the flip closes, never a deferral.

• Un-ignore the corpus-under-flag SET-subset gate — remove the #[ignore] attribute on the corpus_under_flag_gate AOT test (compiler_repo/compiler/ori_llvm/tests/aot/corpus_under_flag_gate.rs:164) so normal cargo test -p ori_llvm --test aot + CI run the SET-subset readiness gate every run, NOT just under manual invocation. The #[ignore] was correct DURING coexistence (the under-flag corpus regressed, so the gate would red every CI run on the ~99 JOINT residual); it is removed HERE, AFTER the Phase-5 broad-shape completion drives failing_ids_under_flag ⊆ baseline_failing_ids to the EMPTY verdict + the BurdenInc→RcInc activation flips the burden path to the sole RC emitter, so the gate now passes and becomes a standing regression pin. Re-confirm the gate is GREEN (subset verdict holds) immediately after un-ignoring; a red gate post-un-ignore is a §09.2 activation defect cured before close, never a re-#[ignore].

• §09.2 activation close-gate (codex-F1) — after the BurdenInc→RcInc / BurdenDec→RcDec flip above, the activation is NOT closed until every §07.N §09-coupled AOT cell is GREEN post-activation: re-run the §07.5 regression corpus (the 16 BUG-04-118 originally-failing match_alias::* cells + the 17 BUG-04-123 over/under-emission cells decisions/07 maps to §07) and confirm zero regressions vs the pre-flip burden-no-op baseline. Add FileCheck pins on the emitted REAL RcInc/RcDec at each activation cell (not burden-op markers); eval + LLVM dual-execution parity per CLAUDE.md §Fix Completeness; ORI_CHECK_LEAKS=1 reports zero leaks; debug + release. A red §07.N cell here is a §09.2 activation defect cured before §09.2 close (never a deferral).

• Tests for the real-RC activation (relocated from §06.1 per routing.md §4; the FileCheck-on-RcDec pins require the no-op→real-RC flip above, so they live with the activation here, NOT at §06.1 which delivers only the lowering SITE) — per tests.md §Matrix Testing Rule. New AOT fixtures land in compiler_repo/compiler/ori_llvm/tests/aot/burden_activation.rs (new file, sibling of predicate_stack_probe.rs + corpus_under_flag_gate.rs); spec-level parity cells in compiler_repo/tests/spec/aims/burden_real_rc_activation.ori (new, use std.testing { assert, assert_eq }). Matrix dimension = element-type × transfer-scenario × expected-RC-shape:

  • Simple owned-value release (BurdenDec → RcDec at last use / scope exit, RL-2): element-type axis {str, [int], Option<str>, struct, {str: int}, Set<int>} (6 types) × scenario single-binding-dropped-at-scope-exit × expected exactly one real RcDec emitted, no BurdenDec marker survives. 6 AOT fixtures (burden_activation.rs::release_<type>_*) with FileCheck CHECK: call void @ori_rc_dec + CHECK-NOT: BurdenDec; eval+LLVM parity per CLAUDE.md §Fix Completeness; ORI_CHECK_LEAKS=1 zero-leak each.
  • Multi-transfer (BurdenInc at every transfer per §03 + last-use BurdenDec, RL-1 + RL-2): element-type axis {str, [int], struct} (3 types) × scenario value forwarded through 2 owned-param calls then dropped × expected N real RcInc at the N transfer sites + 1 real RcDec at last use, net-balanced (VF-1=0). 3 AOT fixtures (burden_activation.rs::multi_transfer_<type>_*) with semantic pin (FileCheck counts RcInc occurrences == transfer count) + NEGATIVE pin (revert the BurdenInc→RcInc mechanical mapping → fixture fails on missing RcInc / VF-1 imbalance). Eval+LLVM parity; debug + release (FastISel differs).
  • Closure last-use (ApplyIndirect / PartialApply BurdenDec lowers per aims-rules.md §8 RL-2 exempted-terminator set): capture-type axis {closure-capturing-str, closure-capturing-[int], closure-capturing-struct} (3 captures) × scenario closure built via PartialApply, invoked once via ApplyIndirect, env dropped at last use × expected env-pointer real RcDec at closure last use, no double-free of captured value. 3 AOT fixtures (burden_activation.rs::closure_lastuse_<capture>_*) with FileCheck on the env-ptr RcDec + negative pin (a second use suppresses the dec); eval+LLVM parity gate + ORI_CHECK_LEAKS=1 zero-leak each.

• Tests: cargo t green; debug + release.

Subsection close-out (09.2) per protocol.

09.3 ssa_alias_classes.rs consumer simplification

• realize/cleanup_redundant.rs, emit_rc/dead_cleanup/mod.rs, realize/walk_dec.rs, emit_rc/edge_cleanup.rs, realize/walk.rs, intraprocedural/state_map.rs continue to consume project_alias_sources / borrow_sources for lattice optimization (NOT removed — these feed Phase 6 elimination). These reside under realize/ + emit_rc/, NOT under intraprocedural/; re-confirm each path resolves at edit time.
• Predicate-stack-emission integrations retired; lattice-input consumption preserved.
• Tests: focused tests verifying lattice optimization continues to work over burden-emitted IR.

Subsection close-out (09.3) per protocol.

09.4 Coexistence handshake removal (proven-equivalence-licensed)

Proven-equivalence license (the precondition that makes deletion sound, NOT a re-implementation): §07 makes class_covered universal across the test corpus — every variable is in BurdenCovered(F, BR), none in MixedCoverage or Uncovered. The proven §11 partition (Handshake.proof Definition Partition; AimsProof.Coexistence::CH3_classes_disjoint + CH3_class_of_classA) is total + disjoint, so universal class_covered means CH-comp’s soundness theorem reduces to its class_covered case ALONE: coexistence_dispatch(F,L,BR,C) is observably equivalent to BOTH burden_emission_path AND predicate_stack_path (CHcomp_handshake_union + CH2_single_elimination: the burden-derived and lattice-only elimination decisions are bit-identical). Deleting predicate_stack_path (Function 2) therefore leaves coexistence_dispatch ≡ burden_emission_path — observable behavior preserved BY THE PROOF. The retirement is the proven-redundant-path deletion, never an unverified surgery.

• Verify BOTH preconditions of the proven-equivalence license: (1) §07 close-out confirmed class_covered is universal across the test corpus (the coverage-analysis precondition above), AND (2) §09.2’s own close-gate confirmed the burden path is a complete standalone RC emitter CORPUS-WIDE — the failing_ids_under_flag ⊆ baseline_failing_ids verdict RUN AFTER §09.2’s Phase-5 broad-shape emission completion (the RC-lowering self-sufficiency precondition is ACHIEVED at §09.2, NOT delivered by §07B). §07B (the §09 gating dependency, depends_on: [07B]) delivers the PRECONDITION inputs: the probe-gateable broad-shape self-sufficiency PROOF (under-flag 517→115), the §09.2-territory CLASSIFICATION of the ~99 JOINT residual, the §07B.4 corpus-under-flag SET-subset gate-HARNESS, and the baseline-16 failing-ID-SET fixture (the gate’s LEFT operand). §07A (status: complete, reviewed: true) covered the NARROW shapes (its 11-probe ORI_DISABLE_PREDICATE_STACK_RC suite passed zero-new-vs-16-baseline + leak-free + double-free-free), but the 2026-06-04 re-measurement proved the full corpus regresses 2344/16 → 1784/576 under the flag on broad shapes — so §09.2 completes the broad-shape lowering (using §07B’s classification + harness) and its corpus-wide ⊆baseline verdict is the self-sufficiency signal §09.4 consumes. The handshake-removal license needs BOTH: universal coverage alone (§07) leaves VF-1=0 holding by net-zero ABSENCE of deferred ops while the predicate stack supplies the real freeing RC, so deleting the predicate stack on §07 alone would regress (the §09.2 attempt empirically measured AOT 2329/16 → 1300/1045 per §09 HISTORY 2026-06-03); §07A closed that gap. Record both confirmations in the §09.1 disposition document. NOTE (codex-F1, 2026-06-03): during coexistence class_covered is EMPTY for every function — populate_class_covered runs inside analyze_function (Step 4) and reads func.burden_emitted which emit_burden_ops only fills at Step 4b (after), so the empty-burden_emitted short-circuit always fires (see §04A.3 note). Empirically verifying “universal class_covered” therefore requires FIRST relocating populate_class_covered to run AFTER emit_burden_ops (or re-deriving coverage from the emitted IR). Since this section REMOVES the handshake outright (line below) under the proven-equivalence license (the predicate stack retires → no handshake needed), the universality check is a license-precondition recorded from §07’s coverage analysis, NOT an empirical read of the always-empty coexistence-era class_covered set. If §09 keeps a transitional handshake instead of removing it, relocate the pass behind Step 4b first.

• Confirm absence of burden_mirror.rs::reconcile_burden_ledger (the coexistence-only masking balancer): neither compiler_repo/compiler/ori_arc/src/aims/realize/burden_mirror.rs nor any fn reconcile_burden_ledger resolves anywhere under compiler/ori_arc/src/ at edit time — the mirror was already removed/retired upstream (matches the §06 self-sufficient-Phase-5 lowering that SUPERSEDED it per §03A.3a forward-anchor). The literal removal is a no-op confirm-gone; the verification gate below stays LIVE. The self-sufficiency the removal relied on is proven by CH-1 (AimsProof.Coexistence::CH1_burden_emitted_is_bridge: burden_emitted IS burden_owned, a pure function of the lattice — no independent ledger) + CH-4 (CH4_state_map_immutable: BR reads the frozen state map, L does not depend on BR). Verify the burden ledger nets 0 emission-alone (ORI_VERIFY_ARC=1 ORI_DISABLE_BURDEN_ELIM=1 AOT VF-1-clean) with NO mirror present — if a reconcile_burden_ledger-shaped masking balancer has reappeared anywhere, that reappearance is a §09 defect to remove before the gate passes.

• Remove class_covered: BitSet<ClassId> handshake bookkeeping (§04A.3 site). KEEP burden_emitted (func.n, compiler/ori_arc/src/ir/mod.rs:485) — it is the load-bearing burden ledger consumed by the VF-1 burden-balance verifier (compiler/ori_arc/src/aims/verify/burden_balance.rs: “For every v ∈ func.n, verify”) + Phase 6 elimination + the ORI_VERIFY_ARC=1 nets-0 gate above; ONLY the class_covered predicate-stack handshake retires, NOT burden_emitted (codex-F1, 2026-06-03).

• Predicate-stack realization paths that read class_covered to skip emission — RETIRED with predicate-stack itself per §09.2.

• Dead-code cleanup of AimsStateMap (compiler/ori_arc/src/aims/intraprocedural/state_map.rs) — with the class_covered handshake removed above and the class_dec_obligations-driven predicate-stack dec emission retired in §09.2, DELETE both storage maps + accessors: class_covered: FxHashSet<u32> (field at state_map.rs:493) + is_class_covered / class_covered_count / set_class_covered (state_map.rs:993/999/1008); class_dec_obligations: FxHashMap<(ArcBlockId, u32), ClassObligationEntry> (field at state_map.rs:348) + class_dec_obligations() / set_class_dec_obligations (state_map.rs:1028/1037). Delete the ClassObligationEntry type definition + its population wiring (the predicate-stack data structures must retire ALONGSIDE the functions, not be left orphaned): the ClassObligationEntry struct itself (defined near compiler/ori_arc/src/aims/intraprocedural/state_map.rs:170) AND its population path populate_class_dec_obligations (the post_convergence.rs function tagged RETIRE in the §09.1 disposition table, which is the SOLE writer that constructs ClassObligationEntry values into the map). After populate_class_dec_obligations retires in §09.2 + the class_dec_obligations field/accessors delete here, the ClassObligationEntry struct has zero constructors and zero readers → delete the type. Re-confirm the consumer set is empty (scripts/intel-query.sh --human callers is_class_covered --repo ori + ... callers class_dec_obligations --repo ori + ... callers ClassObligationEntry --repo ori + ... callers populate_class_dec_obligations --repo ori all resolve to zero live readers after §09.2/§09.4 retire populate_class_covered / populate_class_dec_obligations) before deleting; a non-empty residual is a §09 retirement-incompleteness defect to retire, never a reason to keep the storage or the type. cargo build + cargo t green debug + release.

• Coexistence-mirror-disabled correctness gate (moved here from §05.N per /review-plan §05 review 2026-06-02 — it tests the self-sufficient burden baseline §09 targets, not the §05 mirror-balanced baseline). With reconcile_burden_ledger confirmed absent above, run the existing AIMS spec + AOT corpus under ORI_DISABLE_BURDEN_OPS=0 with the coexistence mirror gone (the §09 AOT elimination path) — Phase 6 elimination over the unaided burden ledger (netting 0 WITHOUT the predicate-stack mirror) produces zero new lattice-divergence / leak / double-free failures vs the pre-retirement mirror-balanced run. Verifies the burden path’s elimination decisions are self-sufficient post-retirement (the empirical confirmation of the CH-1/CH-4 self-sufficiency proof); a failure here is a §09 emission-self-sufficiency defect cured before §09 close. Both debug + release. (Pairs with the ORI_VERIFY_ARC=1 ORI_DISABLE_BURDEN_ELIM=1 VF-1-clean check above — that proves emission nets 0; this proves elimination over that baseline is leak/double-free-free.)

• Tests: cargo t green; full corpus passes via burden ownership alone.

• TPR checkpoint — /tpr-review covering 09.1-09.4. Route every emitted exit_reason per the global exit-reason routing table (plans/completed/scripts-first-workflow-architecture/_archive/2026-05-15-pre-fold/skill-ecosystem-coherence/decisions/31-step-6-exit-reason-table-source.md) so autopilot dispatches each /tpr-review terminal state (clean → advance to §09.5; findings → fix-and-re-run within the round cap; cap_reached_with_substantive / cap_reached_clean → record review_pipeline: round state + classify per tpr-review/SKILL.md §5.5) rather than stalling on an unrecognized exit. That global table is the SSOT for which orchestrator branch each exit_reason takes; consume it, never re-derive the routing inline.

Subsection close-out (09.4) per protocol.

09.5 CH-proof disposition + post-retirement dual-discharge confirmation

aims-proofing-suite §11 proves the coexistence layer sound but carries NO supersession clause for the case where the shipped layer retires. §09 is the consumer that retires the layer, so §09 records the proof disposition. The disposition is RETAIN, not delete — the CH proofs are over the calculus MODEL (Coexistence.lean defines burden_emission_path, predicate_stack_path, coexistence_dispatch as model functions); deleting the SHIPPED predicate_stack_path Rust code does not touch the Lean/.proof model, so the proofs stay kernel-valid and the dual-discharge gate stays green.

• Record the disposition in plans/aims-burden-tracking/decisions/09-post-convergence-disposition.md: the §11 CH-1..CH-5 + CH-comp .proof (under compiler_repo/aims-proof/proofs/11-coexistence/) + lean/AimsProof/Coexistence.lean are RETAINED unchanged — they are (a) the MS-4 published Ori-novel coexistence-handshake composition theorem and (b) the RETIREMENT-SAFETY CERTIFICATE (they prove the deletion of predicate_stack_path was observably-equivalence-preserving). The CH proofs are NOT retired with the shipped layer.
• Confirm CH-4’s shipped binding SURVIVES: eliminate_burden_ops (compiler_repo/compiler/ori_arc/src/aims/realize/burden_elim.rs, the CH4_state_map_immutable anchor per Handshake.proof Function 1) still exists and still consumes the frozen AimsStateMap read-only after retirement — the self-sufficient burden path is the surviving consumer. A retirement that deleted eliminate_burden_ops would break the CH-4 shipped conformance binding (BANNED — it is the burden eliminator, not predicate-stack machinery).
• Post-retirement dual-discharge confirmation: re-run compiler_repo/aims-proof/scripts/dual-discharge.sh (+ check-proofs.sh + lean-no-placeholder-lint.sh) — exit 0. This CONFIRMS the CH proofs (and all rule-theorems) still pass after the shipped retirement; it is a confirmation step, not a re-proof. A divergence here means the retirement perturbed something the proofs constrain (a §09 defect to cure before close), NOT a license to weaken any proof.
• Coordinate with plans/completed/aims-proofing-suite/section-11-*.md + section-17-*.md: surface the CH-proof RETAIN disposition + the surviving CH-4 eliminate_burden_ops binding so the proofing-suite’s shipped-conformance bookkeeping (§17 manifest) reflects that the CH-4 anchor persists post-retirement. aims-proofing-suite §17 (ArgEscaping shipped-conformance gate / §17 manifest) is a legitimate CROSS-PLAN reference — plans/completed/aims-proofing-suite/00-overview.md is declared in this plan’s 00-overview.md frontmatter references:[]; the coordination is informational cross-plan surfacing, NOT a local depends_on: dependency (this section’s depends_on: is intra-plan only — ["07B"], the corpus-wide burden-lowering-self-sufficiency precondition; §07B in turn depends_on §07A, which depends_on §07).

Subsection close-out (09.5) per protocol.

09.R Third Party Review Findings

• [TPR-09-001-agy][major] fresh_collection_source_apply_dst (compiler_repo/compiler/ori_arc/src/aims/realize/emit_unified.rs) recognizes self-allocating collection-source results for ArcInstr::Apply ONLY; Invoke-TERMINATOR results (whose fresh-site BurdenIncs are prepended to the normal-successor block by burden_lower/emit.rs compute_invoke_result_incs) are never recognized, so the M1 alloc-aware-net elision cannot fire for self-allocating builtins called via Invoke — an under-flag-only leak shape inside the §09.2-owned JOINT residual. Cure surface: extend the M1 recognizer AND the lineage-net walk (compute_lineage_alloc_aware_net iterates block.body only) to terminator-defined results as part of the §09.2 Phase-5 broad-shape completion. M-c-banned during coexistence per attempt-55 (default 16→61) — do NOT patch before the §09.2 retirement unblocks. Doc-side mismatch (recognizer doc promised Apply/Invoke coverage) corrected 2026-06-06.
• [TPR-09-002-opencode][major] compiler_repo/compiler/ori_arc/src/aims/realize/emit_unified.rs is 7291 lines (14.5x the 500-line compiler file cap), mixing the retiring predicate-stack walk with surviving burden passes (M1/M2/M3, Phase 6.8x relocations, strip passes). The §09.2/§09.3 retirement deletes the bulk; the post-retirement residual MUST be split into <=500-line submodules (burden elision / lineage nets / relocation / strip) as part of the §09.2 dead-code cleanup — close-gate: no aims/realize/ source file over 500 lines after §09.2 lands. Splitting BEFORE retirement would churn code §09.2 deletes; the deletion is the bulk of the cure.

09.R.H — Hygiene Findings

• [HYG2-01][critical] [GAP:dual-execution-parity-divergence] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/apply.rs:306 — float->int cast: LLVM emits raw fptosi (poison on NaN/inf/out-of-range) while eval saturates and spec mandates range check — three-way divergence with zero negative pins Cure: Per the recently-cured sibling arms: emit the range/NaN check in the (Tag::Float, Tag::Int) arm (or use LLVM llvm.fptosi.sat intrinsic + explicit NaN/range panic for eval-parity), add eval’s missing fallible range check per spec ‘truncate, range check’, add positive+negative AOT parity pins (NaN, +inf, -inf, 1e300, -1e300), and correct the apply.rs doc comment. NOT covered by BUG-05-008 (that owns the str-parse/X->str/fallible RUNTIME surface; this is the infallible __cast intercept arm emitted inline). CURED 2026-06-07: cast arm now emits llvm.fptosi.sat via new IrBuilder::fp_to_si_sat (NaN->0, MIN/MAX clamp — exact Rust-as/eval parity); 4 dual-backend saturation pins added (NaN, +/-inf, +/-1e30 clamp) in tests/spec/expressions/type_conversion.ori (23/23 both backends).
• [HYG2-17][major] [GAP:dual-execution-parity-divergence] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/builtins/primitives.rs:77 + builtins/prelude.rs:92 — .to_int() method and int() conversion fn emit raw fptosi (poison on NaN/inf) while eval’s method semantics CHECK and panic (“cannot convert NaN to int” / infinity / round-trip range check, methods/numeric.rs:405). Discovered adjacent to HYG2-01; distinct semantics target (checked-panic, NOT saturation). Cure: emit NaN/inf/range guard branches (emit_unwrap_branch pattern) matching eval’s panic messages, then fptosi; add dual-backend panic pins.
• [HYG2-02][major] [DRIFT:layout-mirror-without-sync-enforcement] compiler_repo/compiler/ori_llvm/src/codegen/abi/mod.rs:184 — abi_size/abi_alignment hand-mirror LLVM struct layout + layout_resolver + ori_repr niche/tagless lowering with comment-only coupling and no sync test Cure: Add a sync test iterating a representative type corpus (primitives, tuples, structs incl. mixed-alignment fields, explicit/niche/tagless/tagged-ptr enums, Option/Result nesting, recursive types) asserting abi_size == LLVMTypeId store size from TypeLayoutResolver::resolve and abi_alignment == LLVM ABI alignment. Longer-term: derive abi_size/abi_alignment from ReprPlan (RV-4 target) instead of re-walking TypeInfo.
• [HYG2-03][major] [LEAK:scattered-knowledge] compiler_repo/compiler/ori_llvm/src/codegen/abi/mod.rs:438 — select_call_conv’s name/is_extern params are production-dead; calling-convention policy actually applied via direct field assignment at 3 scattered sites; tests pin the dead branches Cure: Make select_call_conv the single authority: thread the real symbol/name and extern flag from callers (declare_impl_method has name_str in scope at mod.rs:378) and replace the three direct-assignment sites with select_call_conv inputs (e.g. an is_extern/is_wrapper parameter); or shrink select_call_conv’s signature to what production uses and delete the dead branches + their tests. Fix the misleading ‘caller overrides if needed’ comment either way.
• [HYG2-04][major] [DRIFT:ssot-predicate-not-consumed] compiler_repo/compiler/ori_llvm/src/verify/rc_balance.rs:231 — is_rc_dec_symbol declared SSOT for the whole-object dec ABI set, but rc_balance + rc_histogram duplicate the literal list with citation comments instead of consuming the predicate Cure: Consume the predicate via match guards (name if is_rc_dec_symbol(name) => ...) in rc_balance.rs and rc_histogram.rs, or add a test asserting the verifier match arms accept exactly the strings is_rc_dec_symbol accepts.
• [HYG2-05][major] [LEAK:lossy-fallback] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/instr_dispatch.rs:40 — Field-offset lookup falls back to offset 0 on out-of-range index at 5 codegen sites — silent wrong-address GEP if the pre-sizing invariant ever breaks Cure: Replace .unwrap_or(0) with .expect("variant field offset table pre-sized for fields") (or unreachable! citing the guard) at all 5 sites; consider a shared variant_field_offset(offsets, idx) -> u64 helper as the single loud lookup.
• [HYG2-06][major] [LEAK:lossy-fallback] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/apply_protocols.rs:195 — emit_list_slice_drop falls back to Idx::INT element type when the resolved receiver is not a List — wrong stride passed to ori_list_slice_drop Cure: Replace the fallback with unreachable!("ori_list_slice_drop receiver must resolve to Tag::List") (matching the loud-impossible-state cure pattern from the phase-0.5 sweep).
• [HYG2-07][major] [LEAK:inline-policy] compiler_repo/compiler/ori_llvm/src/codegen/runtime_decl/mod.rs:110 — noalias-out-ptr attribute policy keyed on ‘_cow’ name-suffix convention instead of being declared in the RtFn.attrs SSOT table Cure: Add an Attr::NoaliasLastParam (or per-param attr list) to the RtFn schema in types.rs, declare it on the cow_args family entries, and delete the suffix check from declare_spec.
• [HYG2-08][major] [LEAK:algorithmic-duplication] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/apply_helpers.rs:95 — apply_param_passing and apply_param_passing_with_forwarding share a ~40-line identical skeleton differing only in the borrowed-pointer forwarding branch Cure: Collapse to one function taking arc_vars: Option<&[ArcVarId]> (forwarding active when Some); plain callers pass None. Same shape as the resolve_invoke_callee -> resolve_callee dedup already landed in terminators.rs this commit range.
• [HYG2-09][major] [LEAK:algorithmic-duplication] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/apply_protocols.rs:200 — emit_list_take and emit_list_slice_drop hand-build the canonical {i64,i64,ptr} fat-pointer LLVM type inline + duplicate the alloca/call/load manual-sret skeleton Cure: Resolve the list type via self.resolve_type(list_ty) (both callers have the receiver Idx in hand) and extract a small call_manual_sret(func_id, args, llvm_ty, name) helper for the alloca/call/load pattern.
• [HYG2-10][major] [WASTE:defensive-impossible-state] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/apply.rs:523 — Dead-defensive unwrap_or_else fallbacks substitute wrong-typed zero/null values for builder.call results that cannot be None on non-void callees Cure: Replace with .expect(” is non-void; builder.call returns Some”) at all four sites (per the loud-impossible-state cure pattern).
• [HYG2-11][minor] [GAP:verifier-silent-non-convergence] compiler_repo/compiler/ori_arc/src/aims/verify/burden_delta.rs:62 — compute_burden_entry_nets exhausts its iteration cap silently — verifier consumers may run on partially-propagated entry nets (false-negative verification) Cure: After the loop: debug_assert!(!changed, "burden entry-net dataflow failed to converge within cap") plus a tracing::warn fallback in release so VF-1.1 consumers surface the non-convergence instead of silently passing.
• [HYG2-12][minor] [WASTE:defensive-impossible-state] compiler_repo/compiler/ori_llvm/src/codegen/abi/mod.rs:411 — indirect_alignment masks an impossible u32 overflow with a wrong-value 8 fallback Cure: .expect("ABI alignment fits u32").
• [HYG2-13][minor] [DRIFT:unasserted-binary-enum-assumption] compiler_repo/compiler/ori_llvm/src/codegen/abi/mod.rs:166 — niche payload-variant selection variants.get(usize::from(*niche_variant_idx == 0)) silently assumes 2-variant enums Cure: debug_assert!(variants.len() == 2, “niche payload-variant selection assumes binary enums”) at both sites, or derive the payload index as the non-niche variant explicitly.
• [HYG2-14][minor] [WASTE:defensive-impossible-state] compiler_repo/compiler/ori_llvm/src/codegen/abi/mod.rs:546 — compute_function_abi_with_ownership silently defaults to (Owned, Scalar) when annotated_sig has fewer params than sig Cure: debug_assert_eq!(annotated_sig.params.len(), sig.param_types.len(), …) alongside the existing assert; keep the default only for the genuinely-permitted None-annotated_sig path (already handled by the early return).
• [HYG2-15][minor] [LEAK:scattered-knowledge] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/apply.rs:494 — try_emit_format_call dispatches on string literals after sibling dispatchers migrated to Name-keyed / registry-keyed dispatch Cure: Mirror the ProtocolBuiltin pattern: a small FormatBuiltin enum (or entry flag in the runtime_decl format family) carrying value_is_str, with from_name as the single accessor — or fold value_is_str into the RtFn table the names already live in.
• [HYG2-16][minor] [BLOAT:file-length] compiler_repo/compiler/ori_llvm/src/codegen/abi/mod.rs:1 — abi/mod.rs (581) and arc_emitter/apply.rs (576) grew past the 500-line production cap in the reviewed commit range Cure: Split abi/mod.rs into abi/size.rs (size+alignment walkers) + abi/mod.rs (passing modes, FunctionAbi); move try_emit_cast + format/str-runtime helpers from apply.rs into a sibling (e.g. apply_cast.rs / existing apply_helpers.rs).

Plan-owned references (do NOT duplicate — already tracked)

• REFERENCE (TPR-09-002-opencode): [BLOAT:file-length] compiler_repo/compiler/ori_arc/src/aims/realize/emit_unified.rs:1 — 7,302 lines / 101 fns (14x cap); predicate-stack retirement + post-retirement split already filed as TPR-09-002-opencode above. PH3-17 is the phase-3 record; no new checklist item.
• REFERENCE (section-09 retiring surface): [LEAK:swallowed-error] compiler_repo/compiler/ori_arc/src/aims/intraprocedural/post_convergence.rs:70 — unwrap_or_default on class_payload_of (P05-ADD-2); dissolves at section-09 deletion. PH3-34 is the phase-3 record; no new checklist item.

Open — Critical

• [GAP:cross-backend-divergence — Critical] compiler_repo/compiler/ori_llvm/src/codegen/function_compiler/impls.rs:252 — ImplDef.self_path consumed via .first() in ori_llvm but .last() in ori_eval — multi-segment impl paths diverge between backends. Parser permits multi-segment type paths; typeck keys on last segment. For impl mod.Point { ... }, LLVM mangles under mod while eval registers under Point: dual-execution parity violation. Cure: add self_type_name() accessor returning self_path.last() on ori_ir::ImplDef; route both backends through it. Validate or reject multi-segment impl subjects at parse. CURED 2026-06-07: ImplDef::type_name() accessor landed (self_path.last, doc-pinned to the parser’s ParsedType::Named { name: path.last() } invariant); all five raw consumers (ori_llvm impls.rs, ori_eval module_registration, ori_canon lower, oric arc_lowering + repr_setup) routed through it; 3 semantic pins in ori_ir/ast/tests.rs incl. qualified-path last-vs-first negative pin. Gates: 16/115/libs green.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Critical] compiler_repo/compiler/ori_arc/src/aims/realize/walk_dec.rs:6 — BUG-04-104 is CLOSED; 24 comment sites cite it across walk_dec.rs, emission_site.rs, intraprocedural, plus ori_llvm/tests/aot/match_alias.rs:4. Strip ID; preserve architectural rationale as // INVARIANT: / // Why: content.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Critical] compiler_repo/compiler/ori_arc/src/aims/realize/walk_dec.rs:253 — BUG-04-118 is CLOSED; 53 comment sites cite it across ori_arc realize/emit_rc/intraprocedural and ori_llvm tests. Largest single closed-bug leak cluster in scope. Strip ID; preserve architectural rationale.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Critical] compiler_repo/compiler/ori_arc/src/aims/intraprocedural/state_map.rs:1 — BUG-04-106 is CLOSED; 25 comment sites cite it (state_map.rs and siblings). Strip ID, keep invariant content.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Critical] compiler_repo/compiler/ori_arc/src/aims/emit_rc/edge_cleanup.rs:1 — BUG-04-043 is CLOSED; 23 comment sites cite it. Aggregate of 13 additional closed/unknown IDs (~60 further sites: BUG-02-002 x7, BUG-04-013 x7, BUG-04-024 x6, BUG-04-077 x4, BUG-04-021/035/022/071, BUG-02-013, BUG-04-065, BUG-05-001, BUG-04-003, BUG-04-076) in prose-lint.json. Strip IDs; preserve invariant content.
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Critical] compiler_repo/compiler/ori_arc/src/aims/realize/walk_dec.rs:70 — InstrEmitState doc claims emitted_classes is an active PIN-5 suppression set but it is dead: class_dec_should_emit discards it (let _ = emitted_classes_this_instr; at :494); PIN-5 suppression is lineage-based via emitted_vars only. Cure: fix underlying code (remove dead field or restore the usage).
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Critical] compiler_repo/compiler/ori_arc/src/aims/realize/walk_dec.rs:87 — Fn doc on emit_post_instr_decs_unified describes per-class dedup via emitted_classes_this_instr; implementation performs lineage-based suppression (:483-498) and the class set is unread. Cure: rewrite to invariant (lineage-granularity dedup only).
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Critical] compiler_repo/compiler/ori_arc/src/aims/realize/walk_dec.rs:101 — “PIN-5: per-instruction class-id set” describes class-granularity dedup the code no longer performs; companion :493 “emitted_classes_this_instr is retained for PIN-6” also wrong (PIN-6 consumes classes_dying_here, never the streaming set). Cure: rewrite to invariant.
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Critical] compiler_repo/compiler/ori_arc/src/aims/emit_rc/dead_cleanup/emission_site.rs:92 — Variant doc claims BodyWalkLastUse/DefinedDead/DeferredParent/MergeEdgeRouted land “in subsequent step commits” — contradicted 15 lines below where var_emits_dec_in_block dispatches check_body_walk_last_use returning BodyWalkLastUse and DeferredParent. Cure: rewrite to invariant.
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Critical] compiler_repo/compiler/ori_arc/src/aims/emit_rc/dead_cleanup/emission_site.rs:78 — “forthcoming, pin4_class_emits_dec_set” — exists in same file (:324); “subsequent Steps 3-5” is stale plan-step narration. Cure: rewrite to invariant.
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Critical] compiler_repo/compiler/ori_arc/src/aims/emit_rc/dead_cleanup/emission_site.rs:116 — cites emit_last_use_decs at “lines 180-246” but it is at walk_dec.rs:290-347; stale line range. Cure: cite function name only.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Critical] compiler_repo/compiler/ori_llvm/tests/aot/fixtures/generics/path_sensitive_select_list.ori:2 — “CRITICAL Plan TPR Round-0 refinement (codex + gemini)” — reviewer names + review-round IDs in public fixtures. Sibling fixtures: borrow_list_int_bypass_safe_interaction_then_return.ori, borrow_list_int_nested_pin6_chain_then_return.ori, edge_branch_merge_two_params.ori, path_sensitive_select_negative_pin.ori. Cure: keep semantic-pin description, strip reviewer/round IDs.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Critical] compiler_repo/compiler/ori_arc/src/aims/intraprocedural/ssa_alias_classes.rs:32 — cites “Codex F4 + Gemini F2 PIN material”, “per PIN-2 / Codex F3”, “per Codex F4 +” — reviewer-name + finding-ID provenance in compiler source. Strip reviewer attribution; keep PIN-N labels and invariant statements.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Critical] compiler_repo/compiler/ori_llvm/tests/aot/fixtures/coalesce/coalesce_option_chain_bare_none.ori:1 — “Regression: TPR-02-003” — review-cycle finding ID as regression anchor; 40 TPR-XX-NNN sites in scope. Cure: keep behavioral regression description, strip TPR ID.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Critical] compiler_repo/compiler/ori_arc/tests/aims/coexistence/ch4_behavioral_conformance.rs:3 — module doc cites wrapper plan paths plans/aims-proofing-suite/section-11-coexistence-handshake-proofs.md and plans/aims-burden-tracking/section-04A-minimal-lattice-adaptation.md. Plan paths leak wrapper layout to public repo. Cure: cite public proof artifacts (aims-proof/proofs/11-coexistence/CH-4.proof / AimsProof/Coexistence.lean) instead.
• [COMMENT_HYGIENE_DRIFT:llm-verbose — Critical] compiler_repo/compiler/ori_arc/src/lower/calls/lambda.rs:38 — five S1 step-narration comments in one function (“Step 1: Capture analysis”, “Step 2: Get actual param types”, “Step 3: Build the lambda function body”, “Step 4: Assign globally unique name”, “Step 5: Emit PartialApply”); >=3 escalates to Critical. Same shape at ori_llvm/src/codegen/ir_builder/cfg_simplify/mod.rs:178 and ori_llvm/src/aot/object.rs:322. Cure: delete step-narration comments.

Open — Major (phase-3)

• [LEAK:lossy-fallback — Major] compiler_repo/compiler/ori_llvm/src/codegen/function_compiler/impls.rs:255 — self_path cannot legitimately be empty (parser E1002 guarantee); silent unwrap_or_default() produces colliding _ori_$method symbols on corrupted IR. ori_eval/src/module_registration/mod.rs:213-215 has same silent-continue guard. Cure: replace with expect("ImplDef.self_path non-empty per parser E1002 guarantee") / unreachable! in both backends. CURED 2026-06-07: both sites now unreachable! with the E1002 invariant named (impls.rs mangling fallback + module_registration silent-continue). Gates: 16/115/libs green.
• [LEAK:scattered-knowledge — Major] compiler_repo/compiler/ori_arc/src/lower/collections/mod.rs:328 — __cast protocol marker bypasses ProtocolBuiltin registry; raw literal interned at :328 and strcmp’d at ori_llvm/src/codegen/arc_emitter/apply.rs:185. Rename desync risk; borrow-inference unknown-callee fallthrough applies to __cast (the __index RC-leak failure mode). Cure: add Cast variant to ProtocolBuiltin; route apply.rs intercept through try_emit_protocol from_name dispatch.
• [GAP:lowering-completeness — Major] compiler_repo/compiler/ori_arc/src/lower/collections/mod.rs:323 — lower_cast discards the fallible flag; as and as? both lower to identical Apply __cast. LLVM cannot emit fallible/range-checked/parse casts; falls through to “unresolved function __cast” codegen error. Zero as? fixtures under tests/aot/fixtures/. Cure: thread fallible through ARC lowering; implement LLVM emission for range-checked + parse + Option-wrapped pairs; add parity matrix. Route via /add-bug (relate to open __cast mono-resolution bug).
• [LEAK:inline-policy — Major] compiler_repo/compiler/ori_arc/src/lower/burden_lower/mod.rs:558 — raw “iter” literals interned at 8+ canonical-path sites while ProtocolBuiltin::Iter.name() is the registry accessor. Sites: burden_lower/mod.rs:558,614; aims/emit_rc/borrowed_defs.rs:512; aims/emit_rc/unwind_cleanup/mod.rs:31; lower/control_flow/loops.rs:175; lower/control_flow/for_yield.rs:47,58. Cure: route every canonical-path site through ProtocolBuiltin::Iter.name() (emit_unified.rs sites dissolve at section-09 — do not churn).
• [LEAK:algorithmic-duplication — Major] compiler_repo/compiler/ori_arc/src/aims/normalize/verify.rs:679 — terminal-zero check + per-var driver skeleton duplicated between VF-1 (aims/verify/burden_balance.rs:135) and TRMC burden-balance verifiers (:679). Dataflow kernel shared at burden_delta.rs; verdict-extraction layer not. Cure: extend aims/verify/burden_delta.rs with a verdict kernel; both verifiers map to respective error types.
• [LEAK:algorithmic-duplication — Major] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/apply.rs:278 — narrowed elem-size override block verbatim duplicated between apply.rs:278-295 and terminators.rs:748-762; ori_list_push/new arg-policy inlined at 3 consumers. Cure: extract fn override_for_yield_elem_size + shared coercion helper; validate against 16/115 AOT baselines.
• [LEAK:algorithmic-duplication — Major] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/apply.rs:214 — 5-step callee-resolution chain inlined in emit_apply, duplicating resolve_invoke_callee in terminators.rs:636-657. Cure: make emit_apply consume resolve_invoke_callee (rename resolve_callee; project ABI tuple shape each caller needs).
• [GAP:emission-asymmetry — Major] compiler_repo/compiler/ori_llvm/src/codegen/arc_emitter/terminators.rs:731 — borrowed-param forwarding on Apply runtime path (apply.rs:256-270) but NOT on Invoke runtime path (terminators.rs:731-745 coerces unconditionally). Divergent pointer identity for same call shape; potential COW-uniqueness observation difference. Cure: forward borrowed params on Invoke path or document with IR pin test why Invoke must copy.
• [LEAK:algorithmic-duplication — Major] compiler_repo/compiler/ori_arc/src/lower/control_flow/type_layout.rs:20 — three parallel layout computers (ori_arc pool_type_store_size / ori_llvm type_store_size / ori_repr compute_field_layout) with manual must-stay-in-sync contract, no enforcement test, DEAD deferral anchor (TODO points at completed plan with no layout-extraction item). Cure: extract shared kernel to ori_repr; both consumers query it; add exhaustive Tag-matrix test until extraction lands.
• [GAP:re-derived-layout — Major] compiler_repo/compiler/ori_llvm/src/codegen/abi/mod.rs:187 — abi_size_inner sums field sizes WITHOUT alignment padding; Direct/Indirect misclassification admitted in code; abi/tests.rs:103 asserts WRONG classification with “Acceptable for now”. Violates ori_repr mission. Cure: query ReprPlan/shared layout kernel; flip abi/tests.rs:103 to Indirect; validate against 16/115 AOT baselines.
• [LEAK:scattered-knowledge — Major] compiler_repo/compiler/ori_llvm/src/codegen/abi/mod.rs:129 — enum_repr_for SSOT helper not consumed by 6 direct get_enum_repr sites in abi/mod.rs:129,139,155, type_info/enum_layout.rs:37, type_info/layout_resolver.rs:213,244. Variable-residue type yields Some(repr) inside arc_emitter and None in abi/type_info — divergent size/classification. Cure: move enum_repr_for to type_info module or ReprPlan method; route all 6 sites through it.
• [LEAK:algorithmic-duplication — Major] compiler_repo/compiler/oric/src/commands/repr_setup.rs:320 — verbatim duplicate of ori_llvm::collect_unconstrained_fn_names; canonical copy at ori_llvm/src/unconstrained_fns.rs. Cure: consume ori_llvm::collect_unconstrained_fn_names directly (oric always builds with llvm feature) or move to ori_repr.
• [WASTE:dead-infrastructure — Major] compiler_repo/compiler/ori_llvm/src/aot/incremental/parallel/mod.rs:1 — entire parallel-compilation module has zero production callers; execute_parallel, CompilationPlan::from_graph, and deprecated compile_parallel are test-only or dead. Cure: Chesterton check then decide: wire into AOT multi-file driver under a plan item, or delete (compile_parallel is unconditionally deletable).
• [GAP:latent-deadlock — Major] compiler_repo/compiler/ori_llvm/src/aot/incremental/parallel/mod.rs:99 — cyclic dependency graph deadlocks executor; topological_order().unwrap_or_default() degrades priorities but items in a cycle never reach unsatisfied_deps==0. Cure: make from_graph return Result and error on cycle; or add is_deadlocked() detection. Resolve with PH3-14.
• [GAP:test-harness — Major] compiler_repo/compiler/ori_llvm/tests/aot/util/binary.rs:1 — AOT harness ensure-step ran against stale binary this session (2377 spurious failures); explicit cargo build restored the 16-failure baseline. Cure: verify ensure-step blocks on build completion + covers ori_rt; add binary-fingerprint assertion (BUILD_NUMBER/git SHA) that fails loudly on stale binary. File via /add-bug (tooling/test-harness).
• [BLOAT:file-length — Major] compiler_repo/compiler/ori_llvm/src/codegen/runtime_decl/runtime_functions.rs:1 — 1,751 lines (cap 500); pure data table monolith. Cure: split per family (rc/list/map/set/str/print/eh) into submodules concatenated into RT_FUNCTIONS via const slices, preserving single-table SSOT semantics and jit_allowed enforcement test.
• [BLOAT:file-length — Major] compiler_repo/compiler/ori_arc/src/aims/intraprocedural/state_map.rs:1 — 1,341 lines (cap 500). Map itself survives section-09; specific predicate-stack fields retire. Cure: sequence decomposition after section-09 removes retiring fields; add - [ ] decomposition item to post-09 follow-up.
• [BLOAT:file-length — Major] compiler_repo/compiler/ori_arc/src/aims/interprocedural/extract.rs:1 — 1,261 lines (cap 500); extract_contract fn 208 lines with nesting to depth 8. Cure: decompose by contract facet (param contracts / return contracts / effect summaries / iter-consume detection) into submodules.
• [BLOAT:file-length — Major] compiler_repo/compiler/ori_arc/src/lower/burden_lower/mod.rs:1 — 1,127 lines (cap 500); canonical burden-emission entry (emit_burden_ops, in-degree 75). Cure: split (burden-op emission core / COW-method classification tables / per-instruction walk); COW classification sets pair with PH3-05 cure.
• [BLOAT:fn-length — Major] compiler_repo/compiler/ori_arc/src/aims/intraprocedural/mod.rs:143 — 123 functions exceed 100-line cap. Top canonical-path offenders: analyze_function (:143, 258 lines), compute_invoke_edge_dead_set (emit_rc/edge_cleanup.rs:553, 226 lines, depth 8), emit_dead_at_entry_decs (emit_rc/dead_cleanup/mod.rs:53, 222 lines), cleanup_redundant_project_alias_decs (realize/cleanup_redundant.rs:71, 224 lines), walk_body_unified (realize/walk.rs:53, 215 lines), extract_contract (extract.rs:37, 208 lines), fmt_instr (ir/format/instr.rs:27, 243 lines). Cure: extract phase-helpers at touch-time; fmt_instr is mechanical per-variant split.
• [BLOAT:nesting-depth — Major] compiler_repo/compiler/ori_arc/src/aims/emit_rc/edge_cleanup.rs:227 — 163 sites exceed nesting depth 4; four reach depth 8. Cure: cure alongside PH3-23 extractions (let-else early-exits + extracted per-edge/per-var helpers).
• [LEAK:lossy-fallback — Major] compiler_repo/compiler/ori_arc/src/lower/collections/mod.rs:369 — resolve_field_index miss returns field index 0 with only tracing::debug! — silently projects the WRONG FIELD in release builds. PC-2 guarantees typeck resolved the field; miss is an internal invariant violation. Cure: unreachable!/ICE citing PC-2; add a negative pin test asserting the panic.
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Major] compiler_repo/compiler/ori_arc/src/aims/emit_rc/dead_cleanup/emission_site.rs:26 — Variant docs cite “Source 1 in dead_cleanup/mod.rs:80-241” and “Source 2 in dead_cleanup/mod.rs:265-426” — stale cross-file line ranges. Cure: rewrite to invariant.
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Major] compiler_repo/compiler/ori_arc/src/aims/emit_rc/dead_cleanup/emission_site.rs:21 — #[expect(dead_code)] reason cites “BodyWalkLastUse/DefinedDead/DeferredParent/MergeEdgeRouted land in subsequent step commits”; BodyWalkLastUse + DeferredParent are constructed (:131+). Cure: fix underlying code (remove expect or narrow to truly-dead variants).
• [COMMENT_HYGIENE_DRIFT:inaccurate-comment — Major] compiler_repo/compiler/ori_arc/src/aims/emit_rc/dead_cleanup/emission_site.rs:7 — module doc: “the SSOT predicate that all four PIN-4 gate sites consult” — only 2 call sites exist; “four” count unverifiable. Cure: rewrite to invariant.
• [COMMENT_HYGIENE_DRIFT:self-referential-narration — Major] compiler_repo/compiler/ori_arc/src/aims/emit_rc/dead_cleanup/emission_site.rs:4 — “The companion var_emits_dec_in_block helper (added incrementally in subsequent steps)” — C-B15 S10 edit-sequence narration. Cure: delete; state purpose only.
• [COMMENT_HYGIENE_DRIFT:self-referential-narration — Major] compiler_repo/compiler/ori_arc/src/aims/realize/walk.rs:7 — “Replaces emit_rc/forward_walk::emit_body_forward_walk() with a walk…” plus :42 repeat — S10 refactor-provenance narration (x2). Cure: delete; state what the walk IS.
• [COMMENT_HYGIENE_DRIFT:self-referential-narration — Major] compiler_repo/compiler/ori_arc/src/aims/intraprocedural/post_convergence.rs:620 — “Replaces the unsound population at step 4 (compute_ssa_alias_classes)” — S10 refactor narration + pipeline-step provenance. Cure: rewrite to current population invariant.
• [COMMENT_HYGIENE_DRIFT:self-referential-narration — Major] compiler_repo/compiler/ori_arc/src/aims/emit_rc/borrowed_defs.rs:7 — “Extracted from helpers.rs to respect the 500-line file size limit.” Same shape at ori_llvm/src/evaluator/compile.rs:3, ori_llvm/src/codegen/derive_codegen/clone_rc.rs:3, ori_llvm/src/codegen/type_info/enum_layout.rs:3, ori_llvm/src/codegen/arc_emitter/builtins/debug_helpers.rs:3, ori_llvm/src/codegen/arc_emitter/builtins/iterators_guard.rs:3, ori_llvm/src/codegen/arc_emitter/emit_function_setup.rs:3, ori_llvm/src/codegen/function_compiler/impls.rs:291 (7 sites). Cure: delete all; state module purpose, never split provenance.
• [COMMENT_HYGIENE_DRIFT:self-referential-narration — Major] compiler_repo/compiler/ori_arc/src/pipeline/aims_pipeline/mod.rs:3 — “Replaces the sequential analysis passes…” plus batch.rs:260 and ori_llvm/src/codegen/type_registration/mod.rs:8 with same “Replaces X” pattern. Cure: delete; old pipeline no longer exists.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Major] compiler_repo/compiler/ori_llvm/tests/aot/closure_drop.rs:2 — cites plans/aims-burden-tracking/section-04-recursive-closures-drop-value.md; same at value_empty_burden.rs:2. Wrapper plan-path references in public test module docs. Cure: delete plan path; keep behavioral description.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Major] compiler_repo/compiler/ori_llvm/tests/aot/recursive_drop.rs:142 — cites bug-tracker/plans/BUG-02-032/ (plan-dir path — BUG-02-032 ID is open/permitted, the PATH is not); tagless_enum.rs:9 cites bug-tracker/plans/completed/BUG-04-122/. Cure: strip paths; keep bare open-bug IDs only.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Major] compiler_repo/compiler/ori_arc/src/lower/burden_lower/mod.rs:1066 — cites codegen-rules.md (:1066, :1104) — wrapper-private rule-file reference (C-B13). Cure: replace with Spec: Annex E citation or concept-only statement of the dual-consuming runtime contract.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Major] compiler_repo/compiler/ori_arc/src/aims/realize/walk_dec.rs:115 — “Per the STRENGTHENED GATE annotation” and “(BUG-04-104 STRENGTHENED GATE)” (:775) — cites review/plan annotation as authority for load-bearing invariant. Cure: rewrite as // INVARIANT: statement; drop annotation pointer.
• [COMMENT_HYGIENE_DRIFT:non-spec-pointer — Major] compiler_repo/compiler/ori_llvm/tests/aot/higher_order.rs:738 — “Plan TPR Round 1 dropped the parallel cell because…” — ephemeral review-round reference. Cure: state current matrix rationale or delete.
• [COMMENT_HYGIENE_DRIFT:self-referential-narration — Major] compiler_repo/compiler/ori_arc/src/aims/realize/walk_dec.rs:105 — “Kept alongside the class set so PIN-6 + non-inc PIN-5 are unchanged.” — edit-decision narration; stale alongside dead emitted_classes findings. Cure: delete.
• [COMMENT_HYGIENE_DRIFT:ai-vocabulary — Major] compiler_repo/compiler/ori_llvm/src/aot/linker/wasm/mod.rs:140 — “Apply comprehensive WASM configuration.” — S8 puffery; “comprehensive” carries no technical content. Cure: state WHICH configuration knobs are set, or delete.
• [COMMENT_HYGIENE_DRIFT:llm-verbose — Major] compiler_repo/compiler/ori_llvm/src/verify/tests.rs:152 — ”// let’s use a module where the function itself has the wrong signature.” — S7 chatbot-filler opener. Cure: delete.

Open — Minor (phase-3)

• [BLOAT:file-length — Minor] compiler_repo/compiler/ori_arc/src/aims/contract/mod.rs:1 — 48 additional files over 500-line cap (53 total in scope): contract/mod.rs 769, post_convergence.rs 1,130 (partially plan-owned — class_payload_of/disposition surface retires at section-09), and 46 others. Cure: work down by size after section-09 retirement; per-file split decisions at touch-time.
• [NAMING:weak-test-descriptor — Minor] compiler_repo/compiler/ori_llvm/tests/aot/spec.rs:21 — 53 test names carry banned weak descriptors (_basic, _default, _ok, _correct, _works). ~15 are domain-word candidates (Default-trait, Result-Ok-variant) requiring per-name behavioral judgment. Cure: rename to <subject>_<scenario>_<expected> using compiler_repo/scripts/fn-rename.py; manually adjudicate domain-word candidates.
• [NAMING:ephemeral-test-id — Minor] compiler_repo/compiler/ori_llvm/tests/aot/narrowing.rs:342 — 18 test names embed plan-phase tokens (phase_b/phase_c from repr-opt section-04), meaningless after plan archives. Cure: rename to behavioral names; move phase provenance to doc comments.
• [NOTE:lint-false-positive — Minor] compiler_repo/compiler/ori_llvm/tests/aot/rc_matrix.rs:127 — hygiene-lint commented-code check false-positives on matrix-cell label comments and doc-pseudocode (11 sites; zero genuine commented-out code in scope). Cure: /improve-tooling: teach hygiene-lint to skip matrix-label (// <type> x <scenario>) and fenced doc-pseudocode shapes.
• [NOTE:tooling-ssot — Minor] compiler_repo/scripts/test-naming-lint.py:1 — test-naming-lint.py exits clean while hygiene-lint test-weak/test-ephemeral flags 71 sites on the same tree. Two linters claim same responsibility with divergent verdicts — SRP/SSOT violation at tooling layer. Cure: /improve-tooling: designate one detector canonical; test-naming-lint delegates or narrows to disjoint responsibility.
• [NOTE:phase-3c-anchor — Minor] compiler_repo/compiler/ori_llvm/tests/aot/higher_order.rs:1 — review-cycle-token / C-B11-class comment debris in sibling AOT test files (higher_order.rs 24, arc.rs 18, stress.rs 14, conversions.rs 12, cow_map_set.rs 11, error_handling.rs 11, structs.rs 11, operators.rs 10, string_sso.rs 10, strings.rs 10, mutations.rs 9 — 434 total). Same class phase-0.5 purged from generics.rs. Cure: apply generics.rs treatment (behavior-descriptive rewording, keep OPEN BUG-XX refs, strip review-cycle tokens). Phase 3C anchor.
• [DRIFT:unanchored-deferral — Minor] compiler_repo/compiler/ori_arc/src/aims/verify/burden_balance.rs:21 — module doc defers full VF-1 (per-edge dataflow + SCC net-zero obligation) with no plan item or bug ID cited. Cure: verify plans/aims-burden-tracking carries a full-VF-1 item (sections 03A/07B likely owners); if present, cite it; if absent, /add-bug or add the plan item.
• [PLAN_DELIVERY_DRIFT:missing-propagation — Minor] bug-tracker/closed-bugs.json:1 — 17 closed bugs missing delivered_to_roadmap field (Phase 5 Step 9.5 skipped): BUG-01-006, BUG-02-033, BUG-02-034, BUG-04-043, BUG-04-120, BUG-07-078, BUG-07-086, BUG-07-088, BUG-07-089 + 8 others. Cure: backfill via bug_tracker api.py write path; /improve-tooling candidate: make /fix-bug Phase 9 refuse when field absent.
• [WASTE:defensive-impossible-state — Minor] compiler_repo/compiler/ori_arc/src/lower/collections/mod.rs:307 — lower_try other => arm warns and returns scrutinee on non-Option/Result tag; typeck E2xxx rejects that program (PC-2). Cure: convert to unreachable! citing typeck guarantee.
• [BLOAT:bare-todo — Minor] compiler_repo/compiler/ori_llvm/src/evaluator/runtime_mappings.rs:65 — bare TODO proposing mechanical JIT address table generation; drift doubly contained by catch-all panic and jit_symbol_mappings_match_jit_allowed enforcement test. The mapping cannot be mechanically generated (requires literal Rust fn pointers). Cure: replace with fact-comment citing the two enforcement mechanisms; no structural change needed.
• [GAP:catch-all-arm — Minor] compiler_repo/compiler/ori_llvm/src/codegen/derive_codegen/field_ops/thunks.rs:705 — bare _ => unreachable!() without message; sibling sites carry messages. block_merge/single_pred_phi.rs:56-65 double-matches same terminator. Cure: thunks.rs:705 add message; single_pred_phi.rs collapse into one if-let destructure.

09.N Completion Checklist

• Per-function disposition table committed.
• Phase-5 broad-shape burden-emission COMPLETION landed (§09.2) — the ~99 under-flag-only JOINT shapes §07B classified as §09.2-owned (M-a callee transfer-source-dec strip + caller keep-alive-inc; faithful per-element emit_dead_at_entry_decs with elem_dec_fn accounting; dead-vs-survives-after-concat + COW-shared-survives liveness; the LEDGER D08 Cure-A buffer-provenance contract field GROUND-FIRST per arc.md §CP-1) are completed; iterate-until-converged drove the under-flag failing set to the baseline-16 cohort alone.
• §07B predicate-stack-retirement readiness VERDICT verified — the full-corpus-under-flag gate harness §07B.4 authored, RE-CAPTURED on §09.2’s working tree (predicate-stack-emission changed under §09.2 per the fixture re-capture protocol), asserts failing_ids_under_flag ⊆ baseline_failing_ids EMPTY-of-new-IDs (comm -13 baseline⊆under-flag EMPTY) after the Phase-5 completion + real-RC flip; the §07A 11-probe suite (compiler/ori_llvm/tests/aot/predicate_stack_probe.rs) re-runs green as narrow-shape regression pins but no longer SUBSTITUTES for the corpus gate. §07B.4 owns the LEFT operand (the fixture) + the harness; §09.2 owns this VERDICT.
• Emission-side predicates removed; non-emission predicates preserved per audit.
• Coexistence handshake removed; class_covered no longer referenced; removal recorded as proven-equivalence-licensed (§07 universal class_covered + §09.2 corpus-wide standalone-burden-ledger self-sufficiency [the §09.2 Phase-5 emission completion + the ⊆baseline verdict, with §07B’s probe-gateable proof + §09.2-territory classification + baseline-16 fixture as the precondition inputs] → CH-comp class_covered case → predicate_stack_path redundant).
• Dead-code cleanup landed — class_covered + class_dec_obligations storage maps + accessors deleted from AimsStateMap (state_map.rs); consumer set confirmed empty before deletion; cargo build + cargo t green debug + release.
• Coexistence-mirror-disabled correctness gate (§09.4, moved from §05.N) PASSES — Phase 6 elimination over the unaided self-sufficient burden baseline produces zero new lattice-divergence / leak / double-free failures; debug + release.
• CH-proof disposition (§09.5) recorded: CH .proof + lean/AimsProof/Coexistence.lean RETAINED; CH-4 eliminate_burden_ops binding survives; post-retirement dual-discharge.sh exit 0.
• cargo t green; debug + release.
• Plan annotation cleanup.
• Plan sync per protocol; mission criteria 13 + 16 (00-overview.md) checkboxes flipped.
• /tpr-review passed (final); /impl-hygiene-review passed.

HISTORY

• 2026-06-12 — Linear-execution rule #1/#4 auto-reversal: plan-cleanup detected out-of-order subsection completion (09.R.H marked complete while a predecessor was not). Reverted those subsections + completion checklist to not-started; flipped section reviewed: true → false. Re-run /review-plan to determine next steps.

• 2026-06-11 — test-all promoted to the per-cycle VERDICT surface (user directive). All §09.2 grind-cycle + bug-close verdicts now come from full ./test-all.sh runs (summary JSON), not targeted suites; test-all defects are blockers via /fix-bug. CLAUDE.md §Test & Doc Disciplines carries the durable rule; §Fix Completeness gains the test-all gate. Filed at directive time: BUG-07-216 (spec-LLVM in-process JIT isolation — one SIGSEGV kills the runner, the leg’s CRASHED cause alongside open BUG-04-157).

• 2026-06-11 — Linear-execution rule #1/#4 auto-reversal: plan-cleanup detected out-of-order subsection completion (09.R.H marked complete while a predecessor was not). Reverted those subsections + completion checklist to not-started; flipped section reviewed: true → false. Re-run /review-plan to determine next steps.

• 2026-06-10 — Linear-execution rule #1/#4 auto-reversal: plan-cleanup detected out-of-order subsection completion (09.R.H marked complete while a predecessor was not). Reverted those subsections + completion checklist to not-started; flipped section reviewed: true → false. Re-run /review-plan to determine next steps.

• 2026-06-09 (METRIC REDEFINITION — the floor is the test-all metric; bare-cargo floors were under-counts blind to every VF-1 verification failure). USER DIRECTIVE: the plan targets the number test-all.sh reports, not a private metric. Root cause of the divergence: every floor/guardrail capture ran bare cargo test -p ori_llvm --test aot WITHOUT ORI_VERIFY_ARC=1 + ORI_VERIFY_EACH=1, while test-all.sh and CI export both — so the floor counted only behavioral failures (leaks/double-frees/wrong output) and excluded every VF-1 burden-imbalance verification failure (compilation aborts under the gate). Proof cell: traits::test_aot_option_is_some_true PASSES bare, FAILS gated (VF-1: v2 net=-1 ICE). Same tree, same day: bare floor = 97 (attempt-79) vs gated test-all AOT row = 2099 passed / 522 failed / 29 ignored — 97 behavioral + 425 verification-only. The 2026-06-08 USER DECISION goal anchor (“ABSOLUTE green on the burden default = green test-all = green nightly CI”) was already metric-correct; only the measurement tooling lagged. CURES SHIPPED (same session, in-tree): (1) compiler_repo/diagnostics/aot-guardrail.sh now ALWAYS exports ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1 (METRIC CONTRACT header; --env "ORI_VERIFY_ARC=0" override reserved for diagnostic bisection); (2) corpus_under_flag_gate.rs live gate sets both env vars on its subprocess + module-doc METRIC CONTRACT; (3) baseline_failing_ids.txt RE-CAPTURED as the gated burden-default failing-ID SET (522 IDs from today’s test-all run; shrink-only zero-regression guard, terminal target EMPTY) — the prior 16-ID stack-ON-era baseline measured a different metric and is superseded. PROTOCOL FORWARD: every floor capture, guardrail-2 comm run, and LEDGER floor entry uses diagnostics/aot-guardrail.sh (or exports both gates explicitly); a bare-cargo count is NOT a floor and MUST NOT be compared against gated sets. The behavioral sub-count (97) stays useful as a severity partition (runtime misbehavior vs accounting imbalance) but is never the headline. Floor under the canonical metric as of this entry: 522.

• 2026-06-09 — Linear-execution rule #1/#4 auto-reversal: plan-cleanup detected out-of-order subsection completion (09.R.H marked complete while a predecessor was not). Reverted those subsections + completion checklist to not-started; flipped section reviewed: true → false. Re-run /review-plan to determine next steps.

• 2026-06-08 (ROUTING CONSOLIDATION — supersedes the BUG-04-142 AND BUG-04-145 routing pointers above; the alias-chain over-dec is the §09.2 TRANSFER-THROUGH-RETURN JOINT broadened to ==, owned HERE, NOT a separate bug). Read BUG-04-145’s plan state (bug-tracker/plans/BUG-04-145/00-overview.md HISTORY). Three corrections to the entries below: (1) NO parallel session — cargo build -p ori_types -p ori_arc -p ori_llvm finishes clean; the large staged changeset is THIS session’s ONE mixed work-stream (the §09.2 burden work + the ori_types monomorphization), so the “frankenstate / in-flight surface” caveat below OVERSTATES the hazard — edits are safe (the E2003 len symptom that suggested a parallel typeck break was a standalone-ori check no-prelude artifact, not a break). (2) BUG-04-145 is implementation-COMPLETE + fully reviewed (cell-1 compute_borrowed_arg_let_aliases shipped; Plan TPR + Code TPR + hygiene all clean; no-regressions MET; AOT 202→196). Its close-gates are blocked ONLY on the commit landing, which waits on §09.2 green. So the alias-chain is NOT a BUG-04-145 gap and NOT a fresh /fix-bug — /fix-bug BUG-04-145 was a MISROUTE (it has nothing left to implement). (3) The real owner is the §09.2 transfer-through-return JOINT: per BUG-04-145’s HISTORY the genuine test-all-green blocker is an RL-2 over-dec on returned-buffer dup-alias chains (cohort borrow_list_int_*_then_return_no_leak ×9 / generic_forwarder_* / path_sensitive_*; exit 134/139), characterized in decisions/LEDGER.md attempts 54/55 (M-a/M-b/M-c). MY CONTRIBUTION — BROADEN THE JOINT: the alias-chain let b=a; let c=b; a==b proves the SAME dup-alias-chain RL-2 over-dec ALSO manifests on == COMPARISON operands, not only on RETURN. Phase-5 evidence (this fire): dup-aliases get asymmetric burden ops (%2=b gets burden_inc, %4=c gets none) and the borrowed == operands %6,%7,%9,%10 get owned burden_inc/burden_dec pairs; Phase-6 elim strips incs (DP-3) but not paired decs (DP-2 needs Absent/Dead) → net −2 → double-free. So the JOINT’s fix must cure the dup-alias-chain over-dec GENERALLY (return + ==-borrow + likely other borrow terminals), not return-specifically. CONVERGENCE OWNER: /continue-roadmap plans/aims-burden-tracking §09.2 (LEDGER 54/55 M-a/M-b/M-c) — the dup-alias-chain RL-2 over-dec is the single root behind the bulk of the 156 burden-default reds; fix it once (calculus-first, ground in Realization.lean RL-2 + the §1.9 project_alias_sources dup-alias model + Coexistence CH-2 net-preservation) and the return cohort + the ==/alias cohort clear together. The alias-chain fixture is a NEW matrix cell for the JOINT (== / comparison-borrow axis). The BUG-04-142 and BUG-04-145 pointers in the entries below are SUPERSEDED by this JOINT routing.

• 2026-06-08 (PRECISE RCA — the alias-chain over-dec root is BORROWED ==-OPERAND MISCLASSIFICATION in the burden ownership scan; it is BUG-04-145 territory, NOT BUG-04-142’s __index/COW; the fix is precisely targeted). [Routing SUPERSEDED by the CONSOLIDATION entry above — it is the §09.2 JOINT (dup-alias-chain over-dec), not a BUG-04-145 gap; the RCA mechanism below stands.] Calculus-first RCA via ORI_DUMP_AFTER_BURDEN (faithful Phase-5) + the VF-1 burden-balance warn (EMPTY → Phase-5 is per-path net-balanced, so the over-dec is post-Phase-5). Phase-5 burden IR for let a="s"; let b=a; let c=b; a==b && b==c:

  • bb0: %6=%0; burden_inc %6; %7=%2; burden_inc %7; %8=%6==%7; burden_dec %6; burden_dec %7 (a==b operands)
  • bb1: %9=%2; burden_inc %9; burden_dec %2; %10=%4; %11=%9==%10; burden_dec %9; burden_dec %10 (b==c operands)
  • Phase-5 total: 5 burden_inc (%0,%2,%6,%7,%9) + 5 burden_dec (%6,%7,%2,%9,%10). %0 has an inc with no dec (+1); %10 has a dec with no inc (−1) — asymmetric, but same allocation (all alias %0), so net +1 (a LEAK at Phase 5; matches the ORI_DISABLE_BURDEN_OPS=1 predicate-stack leak).
  • MECHANISM: the == operands %6,%7,%9,%10 are BORROWS (Eq::equals takes Borrowed params per arc.md §Protocol Builtins; RL-2: borrowed ⇒ NO caller dec). The burden ownership scan misclassifies them as OWNED → emits owned inc/dec. Then Phase-6 eliminate_burden_ops elides 3 incs via DP-3 (Once ∧ (Linear∨Affine)) but does NOT elide the paired decs (DP-2 fires only on Absent/Dead, NOT Once): final ARC = 2 RcInc, 5 RcDec → net −2 → DOUBLE-FREE. (Counts confirmed: Phase-5 5/5 → final 2/5; the missing 3 incs are the DP-3-elided single-use borrow incs whose decs survived.)
  • §CP-1 verdict: COVERED shape (RL-2 + DP-3 + CH-2 net-preservation are PROVEN) → IMPLEMENTATION divergence, fix the Rust, NOT the calculus. The ownership scan must classify == (Eq::equals) operands AND their Let-aliases as Borrowed on the burden path → emit NEITHER burden_inc NOR burden_dec on them (then there is nothing for DP-3 to half-eliminate). Fix surface: compiler/ori_arc/src/lower/burden_lower/ownership_scans/ (move_alias.rs/live_out.rs — the in-flight restructure) + burden_lower/emit.rs. This is BUG-04-145 class (its compute_borrowed_arg_let_aliases + ownership_scans restructure is the IN-FLIGHT fix for exactly this borrowed-==-operand ownership gap; the alias-chain is its BURDEN-path manifestation — BUG-04-145’s tracker repro is the predicate-stack LEAK face of the same root, made moot for that path by retirement but LIVE on the burden path). NOT BUG-04-142 (whose __index self-inc + receiver-dec-before-COW are distinct mechanisms — those cover OTHER cells of the 156). CONVERGENCE = complete the in-flight BUG-04-145 ownership-scan restructure so ==-operand borrows + their Let-aliases emit no burden ops — then this cell + likely several arc::*alias*/*eq* cells of the 156 clear together. Secondary cure (defense-in-depth, only if ownership-scan can’t catch every borrow shape): make Phase-6 elim CH-2-faithful (eliding an inc MUST elide its paired dec, never half a pair) — but the ownership-scan fix is the root.

• 2026-06-08 (CRITICAL SURFACE CAVEAT — the burden emission is a LARGE IN-FLIGHT staged changeset, NOT a clean surface; do NOT pile a fresh /fix-bug on it). git status at this point shows a large mostly-STAGED changeset: the AIMS calculus (aims-proof/lean/AimsProof/Decision.lean + proofs/05-decisions/DP-3.proof + checker decision_predicates.rs/realization_rules.rs/coexistence_handshake.rs) STAGED; the burden emission (ori_arc/src/aims/realize/{burden_elim,emit_unified}.rs) STAGED; a burden_lower RESTRUCTURE STAGED (lower/burden_lower/ctx.rs NEW, ownership_scans.rs → ownership_scans/{mod,live_out,move_alias}.rs split); monomorphization (ori_llvm/monomorphize/mod.rs, ori_types/def_impls.rs) STAGED; this session’s BUG-04-145 artifacts (inline_aggregate_borrow_leak.rs, predicate_stack_probe.rs) STAGED. This is the accumulated in-flight burden-emission + calculus work (this session’s BUG-04-145 + the §09.2 burden attempts + a DP-3/Decision.lean calculus change), guardrail-clean (no NEW failures vs baseline per prior fires) but NOT converged (156 burden-default failures remain). The alias-chain double-free I measured this fire is the CURRENT STATE of this in-flight changeset (a pre-existing BUG-04-142-class burden failure among the 156, intermittently visible as the changeset is partially-rewritten) — NOT a newly-discovered stable bug. IMPLICATION for the prior CORRECTION entry’s “NEXT: /fix-bug BUG-04-142” pointer: do NOT dispatch a fresh /fix-bug that starts re-editing ori_arc burden emission on top of this large in-flight changeset — it would compound the WIP + risk frankenstate (CLAUDE.md §Stabilization concurrent-ori_arc-edit hazard) AND the staged calculus change means any burden RC fix is calculus-first territory (§CP-1: prove in the compiled Lean FIRST, never weaken, the impl is almost always the bug). The correct path is to CONVERGE the existing in-flight burden-emission changeset to green (the 156 → 0 burden-default failures), carefully + calculus-grounded, NOT to layer a new fix. The 156 ARE the BUG-04-142-class burden-emission bugs (__index self-inc double-inc, receiver-dec-before-COW, Let-alias+==-borrow over-dec). Endgame ordering: converge burden emission (this changeset) → burden-default green → THEN §09.2 Step-2 predicate-stack deletion (D09-gated). The predicate-stack 409 is the retiring path; never gated retirement.

• 2026-06-08 (CORRECTION — retract the prior entry’s “both-paths-fundamental” framing; it is a BURDEN-FLIP REGRESSION = BUG-04-142 class, NOT a pre-existing fundamental bug). Three-way disambiguation on arc::test_arc_alias_chain_no_double_free: burden-default (production now) → DOUBLE-FREE; ORI_DISABLE_BURDEN_OPS=1 (predicate-stack only, the RETIRING path) → LEAK (1 alloc); ORI_DISABLE_PREDICATE_STACK_RC=0 (BOTH enabled — the OLD pre-§09.2-flip production path) → CLEAN. So the fixture is clean on the pre-flip path; the double-free is a regression INTRODUCED by the §09.2 burden-default flip (burden RC-emission over-decs alias chains when sole emitter). This MATCHES BUG-04-142 [critical]’s signature verbatim (“burden-only-default RC emission regresses heap-element RC … exit 0 under ORI_DISABLE_PREDICATE_STACK_RC=0”). The prior entry’s “97 both-paths-fail are FUNDAMENTAL” conclusion was a measurement artifact — comm -12 intersected /tmp/cur_fail.txt (burden-default) with /tmp/pred_fail.txt (the RETIRING ORI_DISABLE_BURDEN_OPS=1 path); both “fail” but the predicate-stack failures are IRRELEVANT to the endgame (that path is being deleted). The real endgame number is the 156 burden-default failures, not 97. They are burden-emission bugs (BUG-04-142 class — __index double-inc, premature receiver-dec-before-COW, AND the Let-Var-alias + ==-borrow over-dec this fixture exhibits). The predicate-stack 409 is the retiring path; its count never gated retirement. ROUTING (per arc.md §CP-1 + routing.md don’t-duplicate): the alias-chain double-free is NOT a new bug — it is a BUG-04-142-class burden-default RC-emission regression (covered shape RL-1/RL-2 + CH-* burden family → IMPLEMENTATION divergence in emit_burden_ops/eliminate_burden_ops/Phase-7 lowering, fix the Rust against the proven theorem; the Let-alias+==-borrow over-dec may be a THIRD mechanism within BUG-04-142’s broad-fallout claim OR a sibling — BUG-04-142’s RCA decides). NEXT: /fix-bug BUG-04-142 (critical, tracked, the dominant burden-emission blocker) — its fix surfaces (do NOT emit BurdenInc on self-incrementing protocol-builtin results; do NOT schedule receiver RcDec before a consuming COW/borrow; AND the alias-chain over-dec) are the §09.2 burden-green path. Tail (the 59 burden-only delta tail e.g. for_yield_str_identity’s jt_reps net-attribution) is secondary to BUG-04-142. BUG-04-145 (==-borrow LEAK on the retiring ORI_DISABLE_BURDEN_OPS=1 path) is the SAME fixture’s predicate-stack manifestation, made moot by retirement. Big-picture pull-back: §09 is “retirement”, but the WORK gating it is “make burden RC-emission correct (BUG-04-142 + the 156)” — the plan must own burden-green, not just the deletion step.

• 2026-06-08 (PIVOTAL — the 97 both-paths-fail are led by a FUNDAMENTAL alias-chain RC over-dec; the compiler is currently BADLY broken on basic aliasing, BOTH paths). [SUPERSEDED by the CORRECTION entry above — the both-paths framing was a measurement artifact; the bug is a burden-flip regression, BUG-04-142 class.] Ground-truthed the first both-paths-fail (arc::test_arc_alias_chain_no_double_free). Fixture is TRIVIAL: let a = "<heap str>"; let b = a; let c = b; if a == b && b == c then 0 else 1. RESULT: DOUBLE-FREE on the burden default (and predicate-stack — it’s in the 97 intersection). ORI_DUMP_AFTER_ARC shows the imbalance: the str allocation gets 3 incs (alloc + RcInc %0 + RcInc %2) vs 5 RcDec (%6,%7,%2,%9,%10) → net −2 → double-free. Basic let b = a aliasing of a heap value is broken — the Let-Var alias chain + the == comparison borrows emit UNBALANCED RC (over-dec). This is NOT a burden-emission edge case (fails on ORI_DISABLE_BURDEN_OPS=1 too) — it is a CORE AIMS/RC realization bug, almost certainly the monomorphization regression (the recent feat(typeck,arc): monomorphization + burden follow-on commits broke fundamental alias/lineage RC handling; both baselines blew up — predicate-stack 16→409, burden 48→156). STRATEGIC IMPACT: this explains the large 97-count (any heap aliasing hits it) and means the dominant blocker is FUNDAMENTAL AIMS correctness, not the §09.2 burden-emission tail. The arc::alias cluster (test_arc_alias_chain_no_double_free/test_rc_alias_chain_compare_heap_string/test_rc_project_merge_two_distinct_parents/test_rc_alias_owned_call_then_root_use/apply_alias_coverage) likely shares this root; the other both-paths clusters (cow/unwind/fat_matrix-generics) need separate root-analysis but are the same class (monomorphization-regression core-AIMS bugs). NEXT (high-leverage, urgent): /fix-bug the alias-chain RC over-dec — full rigor (RCA on the Let-Var-alias + comparison-borrow RC emission, TDD matrix across str/[int]/Option/struct × alias-depth × comparison, dual-execution + leak parity, ground in Realization.lean RL-1/RL-2 + TF-2 transparent-alias + same_alloc_reps merging). This is independent of the burden migration (fix once, helps both paths) and likely clears a large fraction of the 97. The §09.2 burden-only delta tail (59) is secondary to this fundamental regression. CAUTION on scope: do NOT git-archaeology the monomorphization commit (banned per CLAUDE.md §NEVER Investigate Pre-Existing); the question is “is it fixed”, investigate the FAILURE + fix the RC-emission root.

• 2026-06-08 (MAJOR STRATEGIC PULL-BACK — the burden path is the BETTER path; the dominant blocker is 97 BOTH-PATHS-FAIL independent AIMS bugs (monomorphization regression), NOT burden-emission gaps). Measured both compiler configurations on the full AOT corpus: predicate-stack path (ORI_DISABLE_BURDEN_OPS=1) = 409 FAILURES; burden path (default) = 156; both-paths-fail intersection = 97; burden-only gaps = 59 (156−97). DECISIVE REFRAME: (1) the burden path (156) is DRAMATICALLY less broken than the predicate stack (409) — the user’s “keep burden default” is strongly confirmed; the burden path is WINNING. (2) Both baselines blew up vs the LEDGER’s documented figures (predicate-stack 16→409, burden 48→156) = the recent monomorphization commits (2785086a4/f9d1304f6/473878019 “monomorphization + burden follow-on”/etc.) REGRESSED the core AIMS/RC handling on BOTH paths. (3) The 156 burden failures are DOMINATED by the 97 both-paths-fail (independent AIMS bugs failing regardless of burden ops — alias-chains arc::*alias*, COW cow_map_set/cow, unwind fat_ptr_iter::unwind, generics/matrix fat_matrix::*, control-flow for_yield_option, aims_interactions, cli::main_args, elem_dec_scope), with only 59 being burden-emission-specific. I’VE BEEN MIS-SCOPED: grinding the 59 burden-only delta edge cases (for_yield_str_identity etc., 1 fix per several fires, over-fire wall) while the 97 independent core-AIMS bugs are the LARGER, higher-leverage blocker. STRATEGIC PIVOT (recommended path to green nightly CI): the 97 both-paths-fail are core AIMS/RC correctness bugs (NOT burden-migration-specific) — route via /fix-bug, investigate for the SHARED monomorphization-regression root (one root may clear many: the alias-chain cluster, the unwind cluster, the fat_matrix/generics cluster each likely share a root). This is independent of the §09.2 burden grind and clears the bigger chunk. The 59 burden-only gaps (the delta/lineage-rep edge cases) remain the §09.2 tail, fixed after (or alongside) the core-AIMS regression. Captured sets: /tmp/pred_fail.txt (409), /tmp/cur_fail.txt (156 burden), intersection (97). NEXT: pick a both-paths-fail cluster (e.g. arc::*alias* or fat_matrix::*generic*), ground-truth its root via ORI_TRACE_RC + ORI_DUMP_AFTER_ARC (both paths agree it’s broken → it’s realization/lattice/lowering, NOT emission-path), confirm the monomorphization-IR linkage, /fix-bug the shared root.

• 2026-06-08 (for_yield_str_identity root LOCALIZED to a lineage-rep net-attribution gap; + honest SCOPE pull-back). ROOT: compute_burden_entry_nets (aims/verify/burden_delta.rs:49) DOES count BurdenDec/BurdenDecPartial/BurdenDecVariant per-var (forward-dataflow Σ BurdenInc − Σ BurdenDec*), and compute_lineage_alloc_aware_net (emit_unified.rs:5895) adds the alloc +1. For %20: alloc(+1) + 1 inc − 2 decs = net 0 (balanced) → 6.8’s net-gate SHOULD skip. It emits anyway ⇒ the miscompute is lineage-rep attribution: %20’s 2 decs are not counted under the jt_reps (jump-threaded) rep that 6.8’s net keys on — the index-consumed for-yield’s take-result %20 and its decs resolve to DIFFERENT reps, so the net for the queried rep omits %20’s decs and reads +1 (leaked) instead of 0. NEXT-FIRE FIX (focused, fresh context): trace compute_jump_threaded_reps’s rep for %20 vs the rep its decs are attributed to at the 6.8 release-selection; align them so the net counts %20’s decs (a rep-merging-completeness fix; guardrail-2 against the 22 RC≥2 shapes 6.8 correctly serves). SCOPE PULL-BACK (per the directive): for_yield_str_identity (1 of 156) has consumed several fires — it IS too-narrowly-scoped. The §09.2 residual (156) is the post-attempt-67 HARD edge-case set (the easy shapes were cleared 517→48 by attempts 13-67; the remaining are deep net-coordination/lineage-rep/over-fire-wall cases, each needing a focused pass). REALISTIC PATH: each shape = one focused session with the now-established toolchain (predicate-stack oracle ORI_DISABLE_BURDEN_OPS=1 ORI_DUMP_AFTER_ARC=1 + per-(phase,block) realize=trace bisection + alloc-aware-net root + guardrail-2). The autopilot continues with periodic context refresh. Verified in-tree progress stands: iter-source-split (fat_ptr_iter 25→24). Both-paths-fail independent bugs (per the user “both red” decision) remain a SEPARATE workstream (/fix-bug) orthogonal to the burden grind, also needed for absolute-green.

• 2026-06-08 (S2 root REFINED — phase 6.8 is ALREADY net-aware; the bug is a net MIScomputation, NOT a missing gate; corrected next-fire approach). Read compute_dead_owned_collection_releases (3898): it ALREADY consults the alloc-aware net + exclusions (its own comments: “the alloc-aware net fires ONE scope-exit dec when the chain nets +1 [leaked] and leaves it when nets 0 [already released]”; excludes compute_fresh_owned_collection_reps / compute_iter_drop_handle_lineages / compute_owned_consumed_lineages). So last fire’s “add a net-gate” framing is WRONG — the gate EXISTS. The bug is the net MISCOMPUTING %20 for the index-consumed for-yield: %20 (copied [str]) = alloc(+1) + 1 inc (block 3) − 2 CORRECT decs (blocks 5+6 — RC=2 from the alloc+inc legitimately needs 2 decs) = net 0 (already balanced), yet 6.8 emits a 3rd dec → its alloc-aware net for %20’s lineage is NOT counting the 2 existing BurdenDecs (a lineage-rep / dec-attribution gap — likely %20’s decs are attributed to a different jt_reps rep than the one the net keys on, OR compute_burden_entry_nets counts incs+alloc but undercounts the pre-6.8 decs). NEXT-FIRE DEBUG (fresh context): trace the alloc-aware net VALUE 6.8 computes for %20’s lineage rep (add a targeted tracing::trace! of compute_burden_entry_nets’s per-rep net at the 6.8 release-selection site, or read compute_burden_entry_nets + compute_jump_threaded_reps to see why %20’s 2 decs aren’t subtracted) — the fix is to make the net correctly count the pre-6.8 decs so the net-gate sees 0 and skips, NOT to add a new gate. This is a net-COMPUTATION-completeness fix on the existing M3 foundation (the same compute_burden_entry_nets Cure B extended for conversion-sources), low-blast-radius if scoped to the dec-counting. The S1 framing (last fire’s “pre-6.8 %20 over-dec”) was ALSO wrong — the 2 pre-6.8 decs are CORRECT (RC=2); only 6.8’s 3rd is the over. So for_yield_str_identity is SINGLE-source after all (6.8’s net-miscompute), plus the separate S3 @__index late-double — re-examine S3 too (it may be the same net-miscompute on the view lineages).

• 2026-06-08 (S2 fix attempt — naive 6.8 same-block idempotency guard REGRESSED +22 → REVERTED clean; DEAD-END + the correct net-aware approach recorded). Attempted the S2 gate on phase 6.8 emit_burden_dead_owned_collection_decs: a block_has_burden_dec(block, var) guard skipping a same-block same-var second BurdenDec. REGRESSED under-flag 156→178 (+22 NEW, comm -13 non-empty): sets::{set_union,set_intersection,set_difference,set_to_list}, narrowing::test_narrowed_list_sort, index_set_updated::{updated_list_str_elements,updated_list_unique_replaces,updated_map_replaces}, arc::test_arc_borrowed_param_cow_push_str_list, trmc::test_trmc_list_map_increment, generics::test_edge_for_yield_return_preserves_unwind_decs, poly_lambda_mono, traits::map_debug_int_keys, + 6 predicate_stack_probe. REVERTED clean (compile clean, baseline 156 restored; git diff back to the iter-source-split-only delta). ROOT (the over-fire wall, AGAIN): a same-block same-var double-dec is NOT always an over-release — a collection inc’d to RC≥2 (COW/dup result — set union/intersection/difference, list sort, index-set-updated, COW push) LEGITIMATELY needs 2 decs; the naive guard skips the NEEDED second dec → leak. The for_yield_str_identity %20 block-6 double IS a true over-release (RC=1), but the gate CANNOT use a proxy (idempotency / use-count / “already has a dec”) — those over-fire on the RC≥2 collection-result shapes. CORRECT S2 fix (next fire): key the 6.8 dec-emission on the ALLOC-AWARE NET (compute_lineage_alloc_aware_net / compute_burden_entry_nets, the M3 foundation) — emit/skip the dec per whether the lineage’s per-path alloc-aware net is already balanced WITHOUT it (RC=1 already-released → skip) vs needs it (RC≥2 → keep). This is the LEDGER M3 + attempt-6 “net-keyed elision, NOT def-block-uniqueness/use-count/type proxy” discipline applied to the dead-owned-collection DEC side (attempts 6-8 applied it to the fresh-INC-elision side). Re-confirms: for the §09.2 over-emission residual, the alloc-aware net is the ONLY non-proxy discriminator; every naive proxy over-fires.

• 2026-06-08 (for_yield_str_identity double-dec — over-emitting phases PINPOINTED via per-phase trace; precise gated-fix targets for the next fire). Continued the realize=trace per-(phase,block) bdec bisection PAST 6.65 (ANSI-stripped, grep block 3/5/6). DECISIVE: phase 6.8 emit_burden_dead_owned_collection_decs ADDS the redundant decs — block 5 [20,29,32]→[20,29,32,29] (+%29), block 6 [20]→[20,20] (+%20). The @__index views (%27/%32) stay SINGLE through 6.85 → they double even LATER (post-6.85 phase OR Phase-7 lowering). And %20 ALREADY had 2 decs (blocks 5+6) BEFORE 6.8 vs the predicate-stack oracle’s 1 — so genuinely MULTI-SOURCE: (S1) a pre-6.8 %20 over-dec (one of blocks-5/6 is redundant), (S2) phase-6.8 doubling of %20+%29, (S3) a late @__index-view double. Three independent over-emission sources, each needs its own gate (last fire’s single-pass hypothesis confirmed insufficient). NEXT-FIRE FIX (fresh context, per source): (S2) gate emit_burden_dead_owned_collection_decs (6.8) OFF for a collection lineage already carrying its scope-exit dec from an earlier phase (the index-consumed for-yield case) — likely high-leverage (6.8 may over-emit for many collection-result shapes; guardrail-2 against shapes where its dec IS needed); (S1) trace WHY %20 gets decs in BOTH block 5 and block 6 (the two index-consume exit paths) — one is redundant; (S3) extend the trace past 6.85 / into Phase-7 lowering for the @__index double. Acceptance: per-op burden dec-count == predicate-stack oracle (ORI_DISABLE_BURDEN_OPS=1 ORI_DUMP_AFTER_ARC=1); guardrail-2 (comm -13 EMPTY). TOOLING NOTE: the realize=trace per-(phase,block) binc/bdec snapshot is the canonical bisection tool for burden over/under-emission — it named the exact phase (emit_burden_dead_owned_collection_decs) in one run.

• 2026-06-08 (for_yield_str_identity double-dec BISECTED via per-phase trace — multi-source + shape-specific, NOT a single redundant pass). Used ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_LOG=ori_arc::aims::realize=trace (the per-(phase,block) binc/bdec snapshot per arc.md) to bisect the systematic double-dec. Findings: (a) %2 (words [str]) carries binc=[2,2]/bdec=[2,2] (DOUBLED, net 0) from the EARLIEST snapshot after_phase_2_5_burden_elim — present pre-probe-tail, in the general emission; (b) %20 (copied buffer) has 1 inc (block 3) + 2 decs (block 5 + block 6) = over-dec, ALSO present by after_phase_6_65_borrowed_terminator_arg_edge; (c) the @__index views (%27/%32) carry ONE bdec through phase 6.65 but TWO in the final ORI_DUMP_AFTER_ARC IR → a LATE probe-tail phase (after 6.65: 6.7 dead-collection-source / 6.8 dead-owned-collection / etc., OR Phase-7 lowering) adds the second. So the over-emission is MULTI-SOURCE (general-emission doubling on %2 + over-dec on %20 by 6.65 + a late probe-tail double on the @__index views), NOT a single redundant pass — last fire’s “gate the probe-tail index-dec” hypothesis is INSUFFICIENT (it only addresses the @__index-view half). And it is SHAPE-SPECIFIC: the iter-consumed yield_identity_str_list (this session’s fix) PASSES, so this is NOT a global double-processing — it is the INDEX-CONSUMED for-yield shape specifically that multiple passes over-emit for. NEXT-FIRE DEBUG (fresh context): continue the per-phase realize=trace bisection PAST phase 6.65 (grep the later-phase block-3/5 bdec snapshots) to identify the exact late doubling phase for the @__index views; separately trace WHY %2 carries 2 incs+2 decs (general-emission double-count) and WHY %20 gets a 2nd dec (blocks 5+6) — each over-emission source needs its own gate; per-op burden dec-count == predicate-stack oracle is the acceptance check; guardrail-2.

• 2026-06-08 (for_yield_str_identity + for_yield_option GROUND-TRUTHED — both burden-only gaps; precise next-fire targets + a load-bearing TRACING insight). TRACING INSIGHT (improves the diagnostic loop): ORI_DUMP_AFTER_BURDEN dumps PRE-probe-tail (after Step 4b emit_burden_ops, BEFORE emit_burden_path_probe_tail), so it does NOT show the probe-tail passes’ ops (the for-yield element RC, conversion-source, dead-collection-source passes all run in the probe tail) — it MISLED me into thinking the yield-element-inc was missing. Use ORI_DUMP_AFTER_ARC under-flag for the FINAL burden IR (post-probe-tail, post-Phase-7-lowering = RcInc/RcDec) when diagnosing probe-tail-emitted RC; pair with ORI_DISABLE_BURDEN_OPS=1 ORI_DUMP_AFTER_ARC=1 as the predicate-stack ORACLE (the correct per-op RC to match) + ORI_CHECK_LEAKS. (1) for_yield_str_identity (index-consumed for-yield let copied = for w in words yield w; copied[0].length()…): PREDICATE STACK PASSES (exit 0 — burden-only gap, NOT a both-paths bug). Oracle: RcInc %17 (yield-element-inc, ONCE) + RcDec %27/%32 (the @__index views, ONCE each). BURDEN final IR: the yield-element-inc is CORRECT (RcInc %17 once — this session’s index-consumed eligible path works), but EVERY dec is emitted TWICE — %27/%32 (@__index views), %29 (copied alias), %20 (copied buffer) — a SYSTEMATIC DOUBLE-DEC → double-free. Root hypothesis: the probe-tail emit_for_yield_index_consumed_element_rc index-result-element-dec is REDUNDANT with the general burden emission for this shape (both emit the @__index-view + copied decs). Pre-existing (NOT from this session’s iter-consumed inc, which is correct and untouched here). FIX (next fire): coordinate probe-tail vs general emission for index-consumed for-yields — gate the probe-tail index-dec OFF when the general emission already covers it; verify burden dec-count == predicate-stack per-op via ORI_DUMP_AFTER_ARC; guardrail-2 (over-fire-prone — the index-dec was added for shapes the general emission may NOT cover). (2) for_yield_option (7 failing): NOT the wrapped-yield I assumed — it is for-yield over an OPTION with break/continue-value control flow (for x in opt yield { continue 42 }); a control-flow-coupled str-element shape, distinct mechanism (separate next-leaf). NEXT-CLUSTER priority by size+tractability per the 156-landscape: the index-consumed double-dec (above, adjacent to this session’s pass) > for_yield_option (control-flow) > the larger generics-forwarder (21, Cure-A/cross-procedural) + match_alias (13) + iter_rc_matrix (12).

• 2026-06-08 (USER DECISION — KEEP THE BURDEN-ONLY DEFAULT FLIPPED; both RC paths are red, so there is NO green predicate-stack baseline to preserve). State confirmed: PREDICATE_STACK_RC_DISABLED defaults TRUE in COMMITTED HEAD (pipeline/aims_pipeline/mod.rs:69 — std::env::var("ORI_DISABLE_PREDICATE_STACK_RC").as_deref() != Ok("0"); unset ⇒ predicate-stack DISABLED ⇒ burden-only is the DEFAULT compiler path), and the corpus_under_flag_gate live run is #[ignore]-gated, so the default AOT suite runs the burden path and is red (156 under-flag failures this session). Both configurations are red: the predicate-stack path (ORI_DISABLE_BURDEN_OPS=1) ALSO has failing AOT tests (independent compiler bugs failing on BOTH paths) AND the burden path has its own gaps. DECISION (user): keep the burden-only default flipped — do NOT revert the default to the predicate stack. Rationale: reverting would NOT restore a green nightly-CI baseline (the predicate stack is red too — there is no green baseline to fall back to), and the burden path is the long-term-correct architecture this whole plan (§09 predicate-stack retirement) drives toward, so it is the right default. IMPLICATION (plan framing updated) — distinguish the two activation steps: Step 1 = flip the DEFAULT to burden-only (committed; user decision = KEEP it). Step 2 = DELETE the predicate-stack fallback (CH-4) — STILL GATED by D09 (“never delete CH-4 with an uncovered shape — irrecoverable-safety, BANNED per Invariant-5”), so the predicate stack is RETAINED as the ORI_DISABLE_PREDICATE_STACK_RC=0 opt-in fallback (NOT deleted) until the burden path is green. What the user decision settles is ONLY the default choice (Step 1): since both paths are red, no green predicate-stack baseline gates the default, so the burden path (the §09 retirement target) is the right default. D09’s deletion-ban is untouched and still holds. The §09.2 goal is therefore ABSOLUTE green on the burden default (= green test-all = green nightly CI), NOT parity with a red predicate stack. The corpus_under_flag_gate baseline_failing_ids.txt (the §07B.4-captured 48-ID burden residual) is a zero-regression floor, NOT the terminal target — the terminal target is 0 failures on the burden default. Two failure classes to drive to 0: (i) burden-only gaps (the §09.2 grind — for-yield/iterator/generics-forwarder/per-element/matrix clusters per this session’s 156-failure landscape characterization); (ii) both-paths-fail tests = independent compiler bugs (fix alongside, file via /fix-bug as surfaced). Mission-aligned: per CLAUDE.md §The One Rule + the directive “clean all-green nightly CI is the ultimate requirement,” the burden default + absolute-green endgame IS the path — no predicate-stack fallback to maintain.

• 2026-06-08 (ITER-SOURCE-SPLIT for_yield fix LANDED — yield_identity_str_list FIXED, fat_ptr_iter 25→24 [+1, ZERO new]; KEPT in-tree, guardrail-clean). Executed the prior-fire next-leaf. Ground-truth discovered the fix locus is the EXISTING emit_for_yield_index_consumed_element_rc pass (emit_unified.rs), whose docstring already documents the exact shape (“yield-element-inc RL-1: ori_list_push(scratch, w [own]) DUPLICATES the borrowed iter-element view → needs +1; without it the source IterState::Drop AND the result elem_dec_fn both free the element → double-free”) — but the pass GATED it on !for_yield_result_transferred_out, excluding BOTH iter-consumed AND returned results, so the iter-consumed identity-yield (let copy = for w in words yield w; for w in copy do …) got no inc → double-free. FIX (additive, 3 edits in emit_for_yield_index_consumed_element_rc): (1) new for_yield_result_iter_consumed_not_returned helper (passed OWNED to @iter AND NOT Return-value); (2) collect those results’ scratch args into iter_consumed_scratch_to_result; (3) the yield-element-inc fires for them too, GATED on w ∈ collect_iter_element_defs (the borrowed Project(__iter_next.1) view, TF-4) — never an owned-fresh Construct push. The index-result-element-dec stays gated on non-transferred-out (no @__index on an iter-consumed result). DISCRIMINATOR — the over-fire wall navigated by RC-ownership LOCUS: in-function iter-consume releases via local IterState::Drop → inc belongs in-function (FIXED now); the RETURNED case (@clone_list returns the for-yield result — borrowed_param/two_calls) releases in the CALLER → an inc in the callee LEAKS (the broad version that included returned leaked two_calls) → correctly EXCLUDED, left at baseline. GUARDRAILS: fat_ptr_iter under-flag 25→24 (only yield_identity_str_list removed; the 3 residual for_yield failures = str_identity[index-consumed, separate gap] + borrowed_param+two_calls[returned, excluded] — ALL baseline-failing, ZERO new for_yield); ori_arc 1642/0; build clean; rename behavior-neutral (yield_identity_str_list still ok post-rename). Over-fire impossible by construction: the inc is gated EXCLUSIVELY on the ori_list_take for-yield finalizer + iter-consumed-not-returned + ori_list_push + iter_element_defs — cannot touch non-for-yield tests; the inc is RL-1-REQUIRED for exactly this shape. CALCULUS: Realization.lean RL-1 (RL1_emits_inc = !incElidable, a duplicating push) — impl-conformance, NO .lean edit. Semantic pin: the existing test_yield_identity_str_list AOT test (fails reverted, passes fixed, under-flag). BASELINE NOTE (important state discovery): my session’s tree has 156 under-flag failures vs the checked-in corpus_under_flag_gate/baseline_failing_ids.txt = 48 — my session is on a LESS-advanced base than the §07B.4 foundation (the recent monomorphization commits 2785086a4/f9d1304f6/etc. changed the IR, opening burden-foundation coverage gaps; the foundation FUNCTIONS exist in-tree but don’t achieve 48 on this base). So baseline_failing_ids.txt is NOT the comm-13 reference for this session; net-positive confirmed via fat_ptr_iter 25→24 + the additive narrow gate. NEXT: (a) the RETURNED for-yield case (borrowed_param/two_calls — inc in callee, release in caller) needs cross-procedural / joint-multi-borrow accounting (LEDGER attempt-18 part-2 + §09.2 territory); (b) for_yield_str_identity (index-consumed) still fails — the EXISTING index path has a SEPARATE gap (exit 134, not touched by this fix); (c) the wrapped-yield (option_list/tuple_list: yield Some(p) — the borrowed p is INSIDE a fresh Construct, so w is the Construct, NOT in iter_element_defs) is a distinct sub-shape (inc on the inner p at the Construct, not the push). Follow-up rigor: dedicated probe pin in predicate_stack_probe.rs; full-corpus comm-13 vs a clean captured baseline; LEDGER attempt entry.

• 2026-06-08 (for_yield/cow OVER-ELIM ROOT-CAUSED + LEDGER-GROUNDED: it is the §09.2 ITER-SOURCE-SPLIT next-leaf, NOT a move-alias point-fix; the move-alias-chain-break is RULED-OUT — do NOT apply). Ground-truthed the remaining fat_ptr_iter (25 post-Cure-B) via ORI_CHECK_LEAKS (leak vs double-free classification) + ORI_DUMP_AFTER_BURDEN (element Access). FINDING — the remaining cluster splits by failure-mode into TWO mechanisms: (1) slice-provenance (str_split_on_substring: a substring seamless-slice split) = Cure A (buffer-provenance ParamContract/ReturnContract field, calculus-first — LEDGER attempt-10 NEXT-LEAF-A, contract extension NOT settled by current Lean, ground RL-4/RL-5-vs-COW-realloc-through-borrowed-param in scratch Lean FIRST); (2) borrowed-element-into-collection OVER-ELIMINATION (for_yield ×4 + wrapped-yield option_list/tuple_list + cow ×2 — DOUBLE-FREE) = the §09.2 ITER-SOURCE-SPLIT shape. EXACT IR (yield_identity_str_list, for w in words yield w): %16: str [FatVal] = Project %12.1 (the yielded element — Borrowed per TF-4) → %17 = %16 (Let-Var) → Apply @ori_list_push(%8 [borrow], %17 [own], …) with NO burden_inc %17 — the borrowed element pushed [own] into the surviving result list needs a promotion-inc that the burden path elides → double-free. CRITICAL LEDGER GROUNDING (this fire’s deep read of decisions/LEDGER.md attempts 1-20 + frontier line 202): my initial move-alias-chain-break plan (break compute_transfer_via_move_alias at a non-scalar Project source) is DOUBLY RULED-OUT: (a) LEDGER B.1 (for_yield borrow-model relaxations, 3 variants → each 29→74; the under-emission cure must be ADDITIVE only — never touch the borrow classification); (b) LEDGER attempts-7/8 (compute_transfer_via_move_alias IS a LANDED fix; a blanket Project-dst exclusion is UNSAFE — project-escape RL-15a may legitimately add an inc). The correct shape is attempt-18’s flagged DISTINCT next-leaf: “a burden_inc/dec net-0 pair that should split inc-bb0/dec-postloop, NOT the borrowed-terminator-arg shape” — the iter-SOURCE split-inc/dec, per-element-aware. §09.2 ACTIVATION STATE confirmed (reconciles Cure B’s gating note with LEDGER line 202): the predicate stack is now burden-only by DEFAULT (predicate_stack_rc_disabled defaults TRUE), so the LEDGER’s “M-c-banned during coexistence (default 16→61)” caveat on this residual is LIFTED (no coexistence default to protect); the probe-tail cure (emit_unified.rs) is valid, guardrail = comm -13 EMPTY under-flag (== default now). CORRECT CURE (next fire): extend the established in-tree A’+B’+M1/M2/M3+iter-consume foundation (LEDGER attempts 13-20 — all uncommitted, guardrail-clean, 459→380) with the iter-source split-inc/dec: emit the promotion-BurdenInc at the yield-into-collection owned position (bb0) + the freeing BurdenDec at the post-loop dead sink (RL-4/RL-5), per-element-aware (the str element’s local dec coordinated with the result list’s elem_dec_fn per attempt-16’s COPY-not-move element-ownership contract), escape-gated, guardrail-2 per step. PRESERVE validated building blocks: compute_cow_inc_borrowed_aliases (attempt-13 step-1, COW-mutator+owned-position+RcPtr discriminator), compute_lineage_alloc_aware_net/compute_jump_threaded_reps (M3 alloc-aware net = the SOLE non-proxy leak discriminator), ApplyToIterConsumingParam (attempt-19 committed-Lean transfer kind) + EdgeRelease::Suppress (attempt-20), compute_conversion_source_reps (Cure B). CALCULUS: Realization.lean rcBalance+RL-2/RL-4/RL-5 already model the iter-source-split (impl-conformance, case a per arc.md §CP-1) — NO .lean edit. Diagnostic-question log (per tooling-first §3 fallback): leak-vs-double-free via ORI_CHECK_LEAKS, element-Access via ORI_DUMP_AFTER_BURDEN — existing tools sufficed, no new diagnostic gap. The LEDGER read this fire prevented a ruled-out fix — validates the “READ LEDGER every fire” directive.

• 2026-06-08 (CURE B IMPLEMENTED + GUARDRAIL-2 PASSED — CLEAN WIN, 21 FIXED / 0 NEW; KEPT in-tree). FIRST committed-quality §09.2 progress. Executed the verified Cure B recipe. CHANGE (5 edits, aims/realize/emit_unified.rs + burden_lowering_tests.rs): (1) compute_conversion_source_reps(func, pool, same_alloc_reps, interner) computed in emit_burden_path_probe_tail (where pool is available) before the fresh-inc-elision call; (2) passed the resulting &FxHashSet<ArcVarId> through compute_elidable_fresh_self_alloc_incs → compute_lineage_alloc_aware_net (SET-param, NOT pool — avoids threading pool through 6 direct unit-test call sites; tests pass &FxHashSet::default() = pre-change behaviour); (3) in compute_lineage_alloc_aware_net, group conversion_source_reps by phi_rep_of, keep single-source phi classes into conv_eligible, set use_phi_for = phi.eligible ∪ conv_eligible. GATING CONFIRMED: emit_burden_path_probe_tail runs under if predicate_stack_rc_disabled which DEFAULTS TRUE (burden is the default emitter), so the fix runs on the DEFAULT path (the LEDGER’s “probe-tail M-c-banned” caveat predates the default flip to burden-only; Decision 10 same-date treats compute_lineage_alloc_aware_net as the legit Cure B locus). RESULTS: str_split/map_keys_str/set_to_list_str runtime BALANCED; ori_arc --lib 1642 pass / 0 fail; under-flag full AOT corpus 179→158 (21 FIXED), comm -13 EMPTY (ZERO new). The 21 = 12 fat_ptr_iter::conversion (str_split{,_auto_iter,_clone,function_param}, map_keys_str, map_values_str, set_to_list_str, derive_clone{result_str_int,result_str_str,slice_str_option,slice_str_struct,slice_str_tuple}) + 9 predicate_stack_probe (the parity probes for those shapes). NOTE: a VF-1 static verify_burden_balance WARN (net=1 expected=0) persists — the PRE-elision burden ops net +1; the Phase-7 LOWERING elides it (elidable_fresh_incs), so RUNTIME balanced + tests pass. Decision-10 M3 “VF-1 alloc-aware net” follow-on (static verifier should consult the alloc-aware net) — verifier-noise, NOT a correctness gap; track as §09.2 cleanup. DISPOSITION: KEPT in-tree (net-positive, zero-new; add Attempt-70 to decisions/LEDGER.md). COMMIT deferred: the tree co-stages parts 1+2 (net-vs-HEAD unestablished) — a clean /commit-push needs parts-1+2 disposition resolved, OR commit ONLY emit_unified.rs + the test file as an isolated Cure-B commit. NEXT: extend the SAME lattice-liveness-grounded eligibility-discriminator pattern to the rest per LEDGER attempt-67 — Cure A (box_list M-a forwarder, buffer-provenance contract field, calculus-first) for generics-21; Phase-5-coupled concat/loop/COW (rc_matrix/stress/cow_map_set) via dead-vs-survives-from-lattice-liveness; per-element dead-after-last-read (narrowing/for_yield_option/elem_dec_scope). Cure B VALIDATES the method: precise lattice-grounded eligibility + guardrail-2 per step → no over-fire (contrast box_list’s naive proxy, 16× over-fire).

• 2026-06-08 (CURE B TRACED TO A TARGETED, ACTIONABLE FIX — extend the phi-threading ELIGIBILITY in compute_lineage_alloc_aware_net to conversion-source reps). Read the machinery in aims/realize/emit_unified.rs (6000+ lines, extensive compute_jump_threaded_reps discriminators). KEY: the dead-source dec pass emit_burden_dead_collection_source_decs (line 2241, doc “frees a borrowed-then-dead CONVERSION SOURCE m.keys()/s.split() at a dead-block-param loop-exit sink”) IS wired in (line 523) AND IS FIRING for str_split (RcDec %15 at bb5 confirmed). So the dead-source dec is NOT the gap. The leak persists because the fresh-site inc on the str-source is NOT ELIDED: the single dead-source dec frees the alloc but the surplus fresh-inc adds an unreleased ref (s-buffer rc=2 at sink, one dec → rc=1 leak). Fresh-inc elision = compute_lineage_alloc_aware_net (line 5875). It ALREADY phi-threads via compute_list_take_phi_attribution BUT scoped to ori_list_take for_yield results ONLY (lines 5896-5907 SCOPE GUARD — broad phi-threading breaks the loop-INVARIANT closure-env case hof_closure_capture_in_loop/coll_map_index_in_loop: a PartialApply threaded unchanged through a loop has net-0 keep-alive inc/dec pairs on SEPARATE unthreaded reps; folding them leaves the alloc’s +1 spuriously unbalanced → leak). str_split’s str-source is NOT ori_list_take → UNTHREADED → net mis-computed across the %0→%11→%15 phi → surplus fresh-inc not elided → leak. THE TARGETED FIX: compute_conversion_source_reps (consumed by the dead-source pass at line 4294) ALREADY identifies the @keys/@values/@split/@to_list conversion sources. Extend compute_lineage_alloc_aware_net’s use_phi_for eligibility (line 5914) to ALSO phi-thread conversion-source reps (reuse compute_conversion_source_reps), so str_split/map_keys/set str-sources get the phi-threaded net → surplus fresh-inc elided. OVER-FIRE GUARD HOLDS NATURALLY: a conversion-source (borrowed by @split/@keys, dies at loop-exit) is categorically NOT a loop-invariant closure-env (threaded-unchanged PartialApply) — the two predicates are disjoint, so extending eligibility to conversion-sources does NOT re-enable the closure-env over-fire the scope guard prevents. Calculus: impl-only (within proven rcBalance, no Lean change) per Decision 10. IMPLEMENTATION RECIPE (next fire / continue): (1) re-establish under-flag cohort baseline; (2) in compute_lineage_alloc_aware_net, compute conversion_source_reps = compute_conversion_source_reps(func, pool, &same_alloc_reps-or-jt, interner) once, and OR it into the use_phi eligibility (the lineage takes phi-threaded attribution iff ori_list_take-eligible OR a conversion-source rep); thread the conversion-source phi the same way compute_list_take_phi_attribution threads the for_yield result (the Jump-arg→block-param positional rename union); (3) build, then guardrail-2 (ORI_DISABLE_PREDICATE_STACK_RC=1 full AOT corpus, comm -13 vs baseline EMPTY — revert clean on ANY new failure per the box_list discipline). Expect it to green the ~15 fat_ptr_iter conversion leaks (str_split/map_keys_str/map_values_str/set_to_list_str + str_list iterations) at once. This is the precise, settled, impl-only Cure B — far more tractable than a “systematic emission rewrite”; the machinery exists, only the eligibility predicate is too narrow. EXECUTION-SHARPENING FACTS (verified this fire): (a) compute_phi_threaded_alloc_reps (emit_unified.rs:6295) is ALREADY GENERIC — unions ALL forward Jump-arg→block-param positional renames (forward-only, back-edges dominator-skipped) — so str_split’s %0→%11→%15 lineage is ALREADY in the threaded map; ONLY compute_list_take_phi_attribution.eligible (line 6269) is list_take-specific → change THAT eligibility only (group compute_conversion_source_reps by phi class, keep single-source classes, mirroring the line-6270 single-alloc guard); (b) NET MATH HAND-VERIFIED (str_split threaded class): alloc(+1)+fresh-inc(+1)+[keep-alive pairs 0]−dec@bb5(−1)=+1 → net==1 → fresh-inc redundant → elide → +1−1=0 balanced; (c) POOL-THREADING: compute_lineage_alloc_aware_net (5875) + enclosing fn (5793) take func,same_alloc_reps,interner only — thread pool:&Pool through both to REUSE compute_conversion_source_reps (never re-implement pool-free = LEAK:algorithmic-duplication). Design COMPLETE + verified; mechanical impl (pool-thread + ~15-line eligibility extension) + guardrail-2 = a FRESH-session task, NOT a 20+-fire session-tail edit (box_list’s 16-test over-fire is the precedent for not rushing emission edits).

• 2026-06-08 (DECISION 10 = the settled architecture; str_split maps to the documented CURE B blocker with a PRECISE impl-only fix locus). Read decisions/10-broad-shape-burdenspec-model-adequacy.md (ESTABLISHED) — the settled §09.2 architecture. VERDICT: the burden DATA MODEL IS ADEQUATE (BurdenSpec expresses every residual obligation); the residual is burden-LOWERING + VF-1-accounting impl-fidelity, NOT a model gap. The cure surface is ENUMERATED + SHARED: Phase-7 lowering (emit_unified.rs:lower_burden_ops_to_rc), the alloc-aware VF-1 net (aims/verify/burden_delta.rs:compute_burden_entry_nets), + 2 contract provenance fields. Three settled mechanisms: M1 spurious fresh-site BurdenInc on non-dup FRESH self-alloc → leak (Phase-7 lowering conformance); M2 borrowed-Invoke-terminator-arg BurdenDec on the WRONG CFG edge (inline vs successor per RL-4/RL-5) (emission-placement); M3 compute_burden_entry_nets allocation-blind (VF-1 alloc-aware net). MY str_split FINDING IS DECISION-10’s “CURE B blocker” VERBATIM: “Per-path alloc-aware net across the Jump-arg → block-param SSA rename — compute_lineage_alloc_aware_net excludes the phi boundary BY DESIGN; threading it is a VF-1 extension SHARED with §07B.2 nested-buffer freeing. Calculus status: within Realization.lean rcBalance (no Lean change; impl-only).” — exactly the %0→%11→%15 loop-carried s-lineage crossing block-param renames I traced (str_split fresh-site inc’s net not propagated across the phi to loop-exit → mis-placed dec → leak). PRECISE FIX LOCUS = compute_lineage_alloc_aware_net (aims/realize/emit_unified.rs:151) — thread the per-path alloc-aware net ACROSS the Jump-arg→block-param phi boundary (currently excluded). IMPL-ONLY (no calculus change — within proven rcBalance). OVER-FIRE CONSTRAINT (load-bearing — the exclusion exists for a REASON): emit_unified.rs:508-620 guards heavily — “a dead-block-param dec there double-frees the iterator-owned buffer”; SEED-not-reuse excludes transferred / iterator-managed / borrowed / return-view-aliasing lineages. Cure B must thread the net across the phi WHILE PRESERVING these guards (iterator-managed/transferred-lineage exclusions) — NOT “delete the exclusion”. This is the deep, over-fire-prone work the box_list 16-test over-fire proved cannot be rushed at a session-tail. box_list (M-a forwarder) = Decision-10 Cure A (buffer-provenance contract field: distinguish fresh-copy / clone from buffer-sharing / slice / COW-push; calculus-first per §CP-1 — ground whether RL-4/RL-5 model COW-realloc-through-borrowed-param, prove in scratch Lean if missing, THEN extend the contract). Decision-10 bounding rule (the 4-case bug-fix-vs-model-extension test): every residual is case 1-3 (impl-fidelity / placement / contract-provenance) — NONE is case 4 (model extension) through attempt-10. NEXT FIRE — execute Cure B: read compute_lineage_alloc_aware_net + build_global_pin4_emits + the lineage_roots/SSA-alias-class machinery FULLY; thread the net across the Jump-arg→block-param phi preserving the SEED-not-reuse over-fire guards; re-establish cohort baselines (scratch/leaf*/base_underflag.txt) first; guardrail-2 under-flag comm -13 empty. This is the architecturally-correct, settled, impl-only path — NO model extension, NO calculus change.

• 2026-06-08 (RE-GROUNDING ON LEDGER attempt-67 + §09 PLAN BODY — my ~18 fires of box_list/fat_ptr_iter diagnosis RE-DERIVED what the LEDGER already definitively established; DISCIPLINE CORRECTION + §09.2 execution strategy). Read the §09 plan body + LEDGER attempt-67 (most recent, 2026-06-06). The LEDGER already has the complete answer: default-path baseline = 16 (§09-coupled cohort), under-flag (ORI_DISABLE_PREDICATE_STACK_RC=1) = 115 floor, probe_gateable_surface_exhausted: true. The 104 under-flag-only residual is FULLY CATEGORIZED: ~45 §09-territory JOINTs (generics 20 + fat_ptr_iter 15 + recursive_feature/derive + match_alias + higher_order = forwarder transfer-through-return / iterator-handle+catch / aggregate-in-variant — “M-a callee-side source-dec strip + caller keep-alive-inc, Phase-5 lower/burden_lower/**+emit_burden_ops, M-c-banned in probe-gating, §09.2-burden-emission-activation must dissolve”); ~29 Phase-5-coupled concat/loop/COW-fork liveness (rc_matrix/stress/cow_map_set/string_sso/collections_ext/arc — M-c-banned, the dead-vs-survives-after-concat + COW-shared-survives + loop-carried-reassign verdicts the predicate stack provides); ~12 per-element NON-block-param dead-after-last-read (narrowing/for_yield_option/elem_dec_scope — needs faithful Phase-5 emit_dead_at_entry_decs at true per-path last-read with elem_dec_fn accounting; the attempt-9/10/11 OVER-FIRE catastrophe surface 459→596/642); 3 environment-coupled (cli, not a burden bug). MY DIAGNOSIS RE-CONFIRMED THE LEDGER, did not advance it: box_list = the M-a forwarder JOINT (attempt-67’s generics-20); my 16-test over-fire = attempt-62’s documented killing clause (the cow_mutated / transfer-vs-survives distinction whose fix re-breaks an identical-signature survives-guard coll_list_cow_concat_shared); fat_ptr_iter str_split = the loop-carried per-element/slice surface. DISCIPLINE FIX (the directive’s standing imperative I under-applied): READ decisions/LEDGER.md THOROUGHLY FIRST every fire — it is the SSOT for the attempt history + the killing clauses + the categorized residual. Re-diagnosing individual leaks re-treads documented ground. §09.2 EXECUTION STRATEGY (the actual work, all routes through ONE thing): the residual dissolves via §09.2 burden-emission-ACTIVATION = make the burden Phase-5 emission (emit_burden_ops) own the path-sensitive dead-vs-survives / dead-at-entry / M-a-strip verdicts the predicate stack currently provides, THEN remove the 4 predicate-stack emission paths (class_dec_should_emit, collect_branch_edge_decs, collect_invoke_edge_decs, emit_dead_at_entry_decs) + 5 helpers per the §09 success criteria. The OVER-FIRE WALL (documented across attempts 9/10/11/62/box_list): the dead-vs-survives verdict MUST come from the lattice’s actual per-path liveness (Cardinality/Consumption + the path-sensitive dead-determination), NEVER a proxy (cow_mutated, return_alias==Project, alloc-net alone) — every proxy conflates transfer-with-survives and over-fires. This is a SYSTEMATIC path-sensitive emission rewrite (not per-shape patches), behaviorally validated against the predicate-stack realize phase (aims/emit_rc/{edge_cleanup,dead_cleanup}.rs + aims/realize/walk_dec.rs) as the SSOT, with guardrail-2 (under-flag comm -13 empty) per step. This is large + high-effort — the architecturally-correct path the directive mandates; it is the §09 plan’s existing success-criteria, now with the over-fire discriminator (lattice-liveness-not-proxy) made explicit. Numbers note: my full-corpus measurement (178) ≠ the LEDGER §09-cohort metrics (16 default / 115 under-flag) — re-establish the cohort baselines (scratch/leaf67/base_{default,underflag}.txt) before any §09.2 edit, and gate on under-flag comm -13 (the LEDGER’s metric), not the full corpus.

• 2026-06-08 (fat_ptr_iter DEFINITIVELY = PATH-SENSITIVE dec-placement for a LOOP-CARRIED slice-source; corrects the “slice-sharing / spurious source-inc” framing below). Exhaustive max-rigor isolation on str_split: (Case 1) str literal + len, NO split/loop → BALANCED; (Case 2) split + parts.len(), NO loop → BALANCED; (str_split) split + for p in parts loop → LEAK. So NEITHER the string-literal fresh-site inc NOR split-slices alone leak — the LOOP is required. Allocation-level balance (lineage-independent, the authoritative metric): burden s-buffer inc=3 dec=3 net=+1; predicate inc=2 dec=3 net=0. Burden has exactly ONE extra inc = the fresh-site RcInc %0 on the string literal. BUT removing it would fix str_split AND double-free Case 1 (where it IS correctly balanced) — so the inc is NOT the bug. Full op-by-op ORI_DUMP_AFTER_ARC diff (burden vs ORI_DISABLE_BURDEN_OPS=1): the s source flows %0→%11→%15 through the loop via block-param renaming (Jump bb3(%0) keeps s alive so its buffer survives for the slices the loop iterates); the burden path’s 3 decs on the s-lineage are SCATTERED ACROSS DIFFERENT CFG PATHS — RcDec %0 at bb2 (unwind), RcDec %15 at bb5 (loop-exit), RcDec %0 at bb7 (loop-body) — so on the NORMAL execution path s receives fewer decs than its 4 refs (alloc + fresh-inc + 2 slice-incs), leaving the fresh-site inc unbalanced → +1 leak. TRUE ROOT = PATH-SENSITIVE RL-4/RL-5 dec-placement gap for a LOOP-CARRIED owned slice-source (the value is kept alive across the loop for slice-keepalive, then dies at loop-exit; the burden path does not place a correct per-path dec at every normal-path exit). The predicate-stack realize phase places these correctly. META-CONCLUSION (forced by this + the box_list arc — the genuine §09 big-picture): BOTH dominant clusters (fat_ptr_iter loop-carried-slice + generics/box_list liveness-transfer) are PATH-SENSITIVE burden-EMISSION gaps where the spec-driven emit_burden_ops + lattice-elimination does not reproduce the predicate-stack realize phase’s path-sensitive dec/inc placement. Patching individual leaks is INTRACTABLE — each fix is path-sensitive and over-fires when attempted naively (box_list: 16-test over-fire; the str-inc removal would double-free Case 1). The retirement cannot complete by leak-patching; emit_burden_ops’s per-path dec/inc placement must be brought to parity with the predicate-stack aims/emit_rc/ realize phase (RL-2/RL-4/RL-5 path-sensitive emission). STRUCTURAL RECOMMENDATION: §09 needs a dedicated emit-model-parity subsection (not 178 leak-patches) — systematically port / verify the predicate-stack realize phase’s RL-4 (edge-specific decs) + RL-5 (dead-at-entry block-param decs) + slice-keepalive dec placement into emit_burden_ops, with the predicate-stack aims/emit_rc/{edge_cleanup,dead_cleanup,forward_walk}.rs as the SSOT. This is the high-effort-but-correct architectural path the directive mandates. Diagnostic SSOT for this class: allocation-level balance awk (per-alloc inc/dec net) + ORI_DISABLE_BURDEN_OPS=1 baseline diff + minimal-case isolation — wire these first.

• 2026-06-08 (fat_ptr_iter ROOT CAUSE = PHASE-5 SLICE-SHARING MODEL GAP, NOT Phase-6 — corrects the “Phase 6 coalescing gap” locus in the entry below). Read eliminate_burden_ops (burden_elim.rs:105+): Phase 6 is ALL-OR-NOTHING PER VAR (lines 196-198 — elide a var’s incs+decs only when DP-3 fires on EVERY inc AND DP-2 on EVERY dec, else RETAIN ALL so Σ Inc − Σ Dec stays at its PRE-elimination value). So Phase 6 CANNOT introduce an imbalance — it preserves whatever Phase 5 emitted. Therefore the +1 leak ORIGINATES IN PHASE 5. CONFIRMED: ORI_DUMP_AFTER_BURDEN (Phase-5 output) for str_split main → %0 (str source s): 2 inc, 1 dec — IMBALANCED +1 (inc bb0, inc bb1, dec bb1); %4 (split result): 2 inc 2 dec (balanced). The predicate stack emits 0 inc for %0 + frees s’s buffer via the SLICE dec (its 2 decs are %3 sep + %15 slice, never %0). DEEP ROOT: s.split(sep) returns parts whose elements are zero-copy SLICES sharing s’s buffer (seamless-slice model). The predicate stack correctly models the SHARING — s needs NO independent inc; the slices’ decs release the shared buffer. The burden Phase-5 emission incs/decs s INDEPENDENTLY of its slices (treats s as a separate RC entity) → double-counts the shared buffer → +1 leak. This is a SLICE-BUFFER-SHARING MODEL GAP in the burden Phase-5 emission (emit_burden_ops) — the burden spec-driven emission lacks the slice-source-sharing awareness the predicate-stack lattice-driven emission has. BIG-PICTURE REFRAME (the §09 endgame structure): the 178 burden-residual failures stem from the burden Phase-5 emission lacking ≥2 models the retired predicate stack had — (1) slice-buffer-sharing (fat_ptr_iter 37 + iter_rc_matrix/fat_matrix — str/map/set slice sources), (2) liveness-gated field-transfer (generics/box_list — the forwarder shape). Retiring the predicate stack requires PORTING these models to emit_burden_ops, not patching individual leaks. This is plan-expansion territory: §09 likely needs dedicated subsections per missing model (slice-sharing-port, liveness-transfer-port). NEXT FIRE (slice-sharing port): read emit_burden_ops (burden_lower/emit.rs) inc-emission — find WHY %0 (a str source borrowed by a slice-producing op) gets the bb0 + bb1 incs; the predicate-stack model (aims/emit_rc/ + the slice-aware realize) is the SSOT to mirror. The cure: emit_burden_ops must recognize a fat-pointer source whose slices share its buffer + NOT emit the independent source-inc (the slices carry the shared-buffer RC). Calculus-ground against §1.9 project_alias_sources + RL-2 (slice = borrow of the source buffer; borrows get no source-inc). Guardrail-2. This is a model port, not a one-line fix — expect it to green the bulk of the 37+ slice-cluster leaks at once. The “Phase 6 / per-var coalescing gap” + “DP-3 elimination not firing” framings in the entry below are RETRACTED — Phase 6 is balance-preserving; the imbalance is Phase-5 slice-model gap.

• 2026-06-08 (fat_ptr_iter PRECISELY LOCALIZED — burden OVER-EMITS spurious incs the lattice fails to eliminate; CORRECTS the “missing dec” framing in the entry below). Confirmed shared mechanism across 4 fat_ptr_iter leaks (str_split, map_keys_str, set_to_list_str, str_list_slice_iteration — all live>0 at exit). DEFINITIVE localization via ORI_DISABLE_BURDEN_OPS=1 (predicate-stack baseline) vs default (burden): str_split BURDEN path alloc=2 free=1 LEAK=1; PREDICATE-STACK alloc=2 free=2 LEAK=0. So the predicate stack is CORRECT; the burden path diverges → §CP-1 case (a) impl divergence, gap is in BURDEN EMISSION (the §09 target). ORI_DUMP_AFTER_ARC RcInc/RcDec diff in main: BURDEN = 2 inc (RcInc %0 str-source s, RcInc %4 split-result parts) + 6 dec; PREDICATE-STACK = 0 inc + 2 dec. The framing is NOT “missing dec” — it is SPURIOUS INCS: the burden path incs %0 (s, consumed once: borrowed by split then the iteration) and %4 (split result, consumed once by iter(%8 [own])), both Once+Linear → DP-3 is_rc_inc_elidable (Cardinality=Once ∧ Consumption∈{Linear,Affine}) should ELIDE both, but eliminate_burden_ops (Phase 6) does NOT, so they survive to RcInc + imbalance the dec accounting → leak by 1. The predicate stack never emits these (lattice-driven emission elides at source). FIX LOCUS (next fire): Phase 6 eliminate_burden_ops / DP-3 application is not firing for fat-pointer FatVal(str) / RcPtr([str]) results+sources whose lattice state is Once+Linear. Investigate WHY: (a) is the lattice state for %0/%4 actually Once+Linear at the inc site, or mis-derived as Many/Unrestricted (→ DP-3 correctly declines)? Dump the AimsState via ORI_LOG=ori_arc::aims::pipeline=info / the realize snapshot; (b) does eliminate_burden_ops even VISIT these BurdenInc sites, or skip FatVal/RcPtr-result incs? (c) is the burden EMISSION (Phase 5) placing the inc where the lattice can’t match it to a var-state? CALCULUS: DP-3 is proven (RL1_emit_iff_not_elidable + proofs/05-decisions/DP-3.proof); a Once+Linear value’s inc IS elidable — so a surviving inc on a proven-Once+Linear var is an impl bug in the elimination, NOT a calculus gap. Fix the elimination to elide it; guardrail-2 (the over-emission affects ~37 fat_ptr_iter + likely iter_rc_matrix/fat_matrix). Diagnostic tools that nailed this: ORI_DISABLE_BURDEN_OPS=1 baseline-vs-burden + ORI_DUMP_AFTER_ARC RcInc/RcDec diff — wire these FIRST for every burden-parity leak. The “missing slice-source dec” hypothesis in the entry below is RETRACTED — it is spurious-inc over-emission, opposite direction. SHARPENED FIX LOCUS: aims/realize/burden_elim.rs (eliminate_burden_ops) — its own module doc (lines 42-58) describes EXACTLY this Σ Inc − Σ Dec = +1 leak: a var whose lattice state is BOTTOM/Dead/Absent passes DP-2 is_rc_dec_unnecessary (Absent ∨ Dead) → BurdenDec elided, but FAILS DP-3 is_rc_inc_elidable (needs Cardinality=Once; Dead/BOTTOM ≠ Once) → BurdenInc RETAINED → +1 leak. The doc claims a per-VAR pass prevents it (“check DP-2/DP-3 against the var’s exit state once, and elide ALL [ops]; when DP-2 elides a BurdenDec, the corresponding BurdenInc is also elided in the same pass”). str_split’s +1 leak proves the per-var coalescing has a GAP for the fat-pointer source/result vars (%0 str-source, %4 split-result). NEXT FIRE: read eliminate_burden_ops fully + dump the AimsState for %0/%4 (are they Dead/Absent at exit → the BOTTOM case the per-var pass must catch?); the cure is making the per-var pass also elide the orphaned BurdenInc when DP-2 elided its paired BurdenDec (the doc’s stated invariant — verify it actually fires for these vars). inc_elidable_at_realization (burden_elim.rs:88) currently = pure is_rc_inc_elidable (no added restriction). Guardrail-2: this likely greens many of the 37 fat_ptr_iter + iter_rc_matrix/fat_matrix leaks (shared over-emission).

• 2026-06-08 (fat_ptr_iter GROUND-TRUTH — str_split is a LEAK via missing str-slice dec; seeds the pivot cluster’s fix). Dumped + traced fixtures/fat_ptr_iter/conversion/str_split.ori (let s = "<91-byte SSO-exceeding>"; let parts = s.split(sep: ","); for p in parts do total += p.len()). ORI_TRACE_RC: source string s (91-byte alloc) reaches rc=4 (alloc + 3 incs) but only 3 decs → ends rc=1, live=1 — NEVER FREED (one missing dec). EXIT=0 (output correct) but assert_aot_success fails on the residual live allocation (leak). Mechanism: s.split(sep) produces parts whose elements are zero-copy SLICES into s’s buffer (seamless-slice model per memory slice_encoding / SLICE_FLAG); each slice incs s; dropping parts + the per-element p should dec s once per slice, but the burden path emits ONE FEWER dec than slice-incs → s leaks by 1. Distinct from box_list (double-free) — this is a MISSING-DEC LEAK on a slice-source fat pointer. Likely the SHARED fat_ptr_iter mechanism: str/map/set conversions (split/keys/values/to_list) produce buffer-sharing slices whose source-dec the burden path under-emits. NEXT-FIRE FIX PATH: ground-truth 2-3 MORE fat_ptr_iter failures (map_keys_str, set_to_list_str, str_list_slice_iteration) to confirm the shared missing-slice-source-dec mechanism; locate where the burden path emits slice-source decs (memory: ori_rt slice-aware ori_buffer_rc_dec + propagate_*_header slice-resolution; the burden EMISSION side is in burden_lower — find where slice-elem decs are emitted/under-emitted); calculus-ground against RL-2 (every slice’s source-inc needs a matched dec at the slice’s last use) — this is a STRAIGHTFORWARD missing-dec (RL-2 dec-at-last-use under-emission), almost certainly §CP-1 case (a) impl divergence, NOT a calculus gap. Fix + guardrail-2. This shape is far more tractable than box_list’s liveness-gated transfer.

• 2026-06-08 (BIG-PICTURE PULL-BACK — DATA-GROUNDED STRATEGIC PIVOT off the narrow generics/box_list cluster). Measured the ACTUAL §09 residual: timeout 150 cargo test -p ori_llvm --test aot → 178 failed / 2425 passed (47-71s). Grouped all 178 by module: fat_ptr_iter 37, predicate_stack_probe 27, generics 21, match_alias 13, iter_rc_matrix 12, narrowing 7, for_yield_option 7, fat_matrix 7, rc_matrix 5, arc 5, recursive_derive 4, higher_order 4, elem_dec_scope 4, + long singleton tail. (baseline_failing_ids.txt tracks only 16 of these as corpus-gate expected-fails; the 178 is the broader default-path burden-residual.) DECISIVE INSIGHT: the ITERATOR-family clusters dominate — fat_ptr_iter (37) + iter_rc_matrix (12) + fat_matrix (7) + for_yield_option (7) = 63 failures, far exceeding the generics-forwarder cluster (21) I had spent ~13 fires grinding. The plan WAS too narrowly scoped (the directive’s pull-back mandate vindicated). box_list / value-copy-aggregate is the HARDEST cluster (needs a liveness-gated RL-2 transfer-kind calculus extension + transitive contract forwarding — last fire over-fired 16× on the naive version); it is now a DEFERRED dedicated unit (the corrected fix direction is fully recorded below — author the calculus extension when returning to it). PIVOT TARGET = fat_ptr_iter (37, largest single cluster): failures cluster in conversion (str_split, str_split_clone, map_keys_str/map_values_str, set_to_list_str, derive_clone_{slice_str_option,result_str_int,result_str_str}) + control_flow (str_list_slice_iteration, str_list_iteration_in_match, matrix_str_nested_unwind) — heavily str/fat-pointer RC during conversions + clones + iterations, likely a SHARED burden-path mechanism (one fix could green many). predicate_stack_probe (27) are the burden-vs-predicate-stack parity probes — fixing the underlying mechanism clusters (fat_ptr_iter etc.) likely greens the corresponding probes too. NEXT: ground-truth a representative fat_ptr_iter failure (test_str_split) via the proven ORI_DUMP_AFTER_BURDEN + ORI_TRACE_RC diagnostic FIRST (per tooling-first.md — never reason about RC from the lattice), identify the shared mechanism, fix, guardrail-2. This is higher-leverage broader-corpus progress than continuing the narrow box_list grind. box_list returns as a dedicated calculus-extension unit later.

• 2026-06-08 (IMPLEMENTED + GUARDRAIL-2 REVERTED — the naive return_alias==Project pair-suppression OVER-FIRES; the relation is necessary but NOT sufficient). Implemented the pair-suppression from the entry below (4 edits: compute_transfer_through_return_results admits Project return_alias; moved_fields::populate_moved_out_fields Pass 2b marks the arg’s projected field moved; threaded contracts). Built clean. box_list UNCHANGED (still SIGSEGV) because main calls unbox (a FORWARDER: b.unwrap() via Invoke), and find_return_alias_shapes (alias_flow.rs) detects only a DIRECT Project off the param, NOT a transitively Apply/Invoke-forwarded one — so unbox’s b.return_alias is NOT Project and the detection never fires for box_list. WORSE: guardrail-2 (generics AOT suite) showed 16 NEW regressions (vs 5 baseline expected-fails) — borrow_list_int_* (bypass/determinism/for-yield/let-alias/multi-let-alias), generic_forwarder_{box_list,set_int,struct_with_list}, inherent_method_forwarder_self, path_sensitive_{match_dispatch,select_*}, edge_*. ALL clean-reverted (re-edit, no destructive git; git diff empty; ori_arc builds 8.83s; work-stream back to corpus 178). ROOT INSIGHT (decisive): return_alias == Some(Project) conflates TWO verdicts — (1) the field genuinely TRANSFERS OUT (move; box_list intent → suppress field-dec + elide inc) vs (2) a BORROW-READ where the callee returns a projection but the ARG SURVIVES and decs its own field (borrow_list_int_* shape → KEEP field-dec, KEEP inc). The naive fix treated ALL Project-returns as transfers → suppressed needed decs (leak) + elided needed incs (double-free) across the 16 borrow-read/forwarder cases. This is EXACTLY the RL-2 ApplyToBorrowedParam (borrow-read → caller decs) vs ApplyToIterConsumingParam (transfer → no dec) split (Realization.lean:166/183 + RL2_borrowed_param_emits_caller_dec / RL2_iter_consuming_no_caller_dec): one signal cannot express two verdicts → a NEW distinguishing signal is required. The distinguisher is LIVENESS — does the arg’s lineage genuinely END at the call (transfer) or SURVIVE past the result’s uses (borrow-read)? return_alias==Project alone lacks this. CORRECTED FIX DIRECTION (this is now a genuine §CP-1 case b — the contract is insufficient): the Project-return must split into a TRANSFER variant vs a BORROW-READ variant, distinguished by whether the arg is dead-after-call (transfer) vs live-after-call (borrow-read) — PLUS the transitive-forwarding gap (find_return_alias_shapes must propagate a callee’s Project return_alias through an Apply/Invoke-forwarder like unbox, currently direct-Project-only). Author the RL-2 ApplyToProjectReturnTransfer transfer kind (mirroring ApplyToIterConsumingParam) in lean/AimsProof/Realization.lean + sync 4 surfaces per §CP-2 BEFORE re-implementing; the burden detection must gate on the arg being dead-after-call (liveness), and the contract extraction must be made transitive. The predicate-stack path got this right via union-find + the liveness-aware realize phase (apply_aliases.rs) — that liveness-awareness is the missing ingredient the burden path needs. The pair-suppression mechanism below is CORRECT in shape but must be GATED by liveness (transfer-not-borrow-read) + fed a transitive contract; ungated it over-fires 16×. Parts 1+2+edge remain staged (178); this fire’s 4 fix-edits fully reverted.

• 2026-06-08 (DEFINITIVE IR + RC-TRACE GROUND TRUTH — instrumentation broke the cycle of 3 wrong reasoned hypotheses; THIS supersedes the field-dec-only recipe below). Dumped box_list via ORI_DUMP_AFTER_BURDEN=1 + ran with ORI_TRACE_RC=1. The failure is a USE-AFTER-FREE → double-free from dec/inc MISORDERING, net-balanced but wrongly-ordered. main burden IR: %3=[int] alloc; %4=Box(%3); %6=%4; burden_dec %6; %7=Invoke @unbox(%6 [borrow]); [bb1] burden_inc %7; ...uses of %7 via %9/%13/%21.... RC trace: alloc %3 rc=1 → dec(burden_dec %6, Box drop decs %3) rc=0 FREE → free → inc(burden_inc %7) rc=1 ON FREED MEM (UAF) → ... → second FREE. Root: burden_dec %6 (Box’s whole-aggregate drop, which decs its sole owned field %3) is emitted at bb0 BEFORE the unbox(%6 [borrow]) call, paired with a compensating burden_inc %7 at bb1 AFTER the call. Net on %3 = 0 (dec%6 + inc%7 cancel), but the ORDER frees %3 before the inc resurrects it. WHY the result-inc is NOT elided: unbox’s b param has return_alias = Some(Project{value}), and the invariant transfers_through_return == true IFF return_alias == Some(Direct) (extract/mod.rs:213) makes transfers_through_return == false for Project → callee_transfers_through_return(unbox) == false in compute_transfer_through_return_results → %7 NOT admitted → result-inc KEPT (the misordered compensating inc). DEFINITIVE FIX = suppress the {aggregate field-dec, compensating result-inc} PAIR together (suppressing either alone breaks balance: field-dec-only-suppress → LEAK net +1; result-inc-only-elide → double-free net −1; verified by hand against the IR). Both keyed on the SAME relation: an Apply/Invoke result %r = call(%agg [borrow], ...) whose callee has return_alias == Some(Project{field}) on the %agg param, where field is %agg’s transferred owned field. THEN: (a) suppress %agg’s burden field-dec for that field (field-granular for multi-field aggregates; whole-%agg exclusion suffices when it is the sole owned field, as Box<[int]>); (b) admit %r to the result-inc elision set (%r owns the MOVED field, not a duplicate — RL-1 move-once-no-inc). Post-fix expected emission: NO burden_dec %6, NO burden_inc %7; %3 lineage = alloc(+1) + dup inc/dec pairs (net 0) − final dec(−1) = 0, freed ONCE at the terminal dec, correct order, no UAF (hand-verified). CALCULUS-FIRST: the pair-suppression = RL-2 Return transfer-kind (no parent dec on the transferred field) + RL-1 move-once (no inc on a move) at FIELD granularity. Ground both in lean/AimsProof/Realization.lean (RL-2 transfer partition + RL1_emit_iff_not_elidable move-once) BEFORE the Rust edit; if the field-granular Project-return-transfer composition is uncovered, author the theorem per §CP-1 case b. IMPLEMENTATION: extend compute_transfer_through_return_results’s callee_transfers_through_return to ALSO return true for a Project return_alias (admits %r, eliding burden_inc %7) AND add a sibling caller-side exclusion suppressing %agg’s transferred-field burden_dec (suppresses burden_dec %6) — both consuming the SAME return_alias == Some(Project) contract relation (factor the relation into one helper, avoid LEAK:algorithmic-duplication). Then guardrail-2 (build + full AOT corpus, comm -13 empty vs baseline incl. baseline_failing_ids.txt). Diagnostic note: ORI_DUMP_AFTER_BURDEN + ORI_TRACE_RC are the definitive tools for this class — wire any new burden-RC investigation through them FIRST (per tooling-first.md), never reason about RC balance from the lattice alone. The field-dec-only recipe below is RETRACTED (it would LEAK; the pair-suppression above is correct).

• 2026-06-08 (GAP CONFIRMED + precise fix recipe — completes the ROOT-CAUSE CORRECTION below). Traced the existing mechanism: the interprocedural contract ALREADY models field-level Project-returns. ParamContract.return_alias: Option<ReturnAliasShape> where ReturnAliasShape ∈ {Direct, Project} (contract/mod.rs:300+; extract/mod.rs:303-307 find_return_alias_shapes — “Project entries detect Return { value } whose definition is a Project off the param’s var” = exactly unwrap(self)=self.value). The PREDICATE-STACK path consumes the Project shape via aims/intraprocedural/apply_aliases.rs (install_alias_entry reading ParamContract.return_alias) + project_aliases.rs + the apply_result_aliases side-table — that is the caller-side field-dec-suppression for Project-returns. THE GAP: the BURDEN path (ownership_scans/mod.rs:269 compute_transfer_through_return_param_vars) keys ONLY on return_alias == Some(Direct) (whole-value, @id-shape); it does NOT handle Some(Project). Since the predicate stack is retired (burden is sole emitter), the Project-return field-dec-suppression is LOST → box_list double-frees. PRECISE FIX: extend the burden path to consume return_alias == Some(Project) at field granularity — when a param’s .value field transfers out via a Project-return, suppress exactly that owned_fields[k] field-dec in the consuming caller’s burden (xs’s drop frees the Box header but skips the transferred .value), mirroring apply_aliases.rs::install_alias_entry’s predicate-stack handling. STUDY apply_aliases.rs + project_aliases.rs as the SSOT model to mirror (avoid LEAK:algorithmic-duplication — factor the shared Project-shape suppression decision if both paths need it during coexistence). The fix is NOT a NEW transfers_through_return field-path extension (the shape is already tracked as return_alias: Project); it is making the burden path HONOR the already-tracked Project shape. CALCULUS-FIRST: ground field-level Project-return transfer against RL-2 transfer-kind partition in lean/AimsProof/Realization.lean BEFORE the Rust edit; author the theorem if uncovered (§CP-1 case b). Then guardrail-2 (re-verify comm -13 set against baseline_failing_ids.txt per the corpus-gate note below). This is a bounded, well-understood fix — the next fire implements it with the apply_aliases.rs model in hand.

• 2026-06-08 (ROOT-CAUSE CORRECTION — calculus-first + tooling-first grounding SUPERSEDES the prior “part-3 EXECUTABLE SPEC” entry below, which had the WRONG root cause). Ground-truthed the actual box_list fixture (generic_method_box_list_int_unwrap.ori): it is NOT the @id<T>(x:T)->T=x whole-value forwarder the prior spec assumed. It is type Box<T> = { value: T }; impl<T> Box<T> { @unwrap (self) -> T = self.value }; @unbox (b: Box<[int]>) -> [int] = b.unwrap(); main: let xs = Box{value:[1,2,3]}; let out = unbox(b: xs); use out. TRUE root cause = FIELD-LEVEL transfer-through-return, NOT a result-inc leak. unwrap returns self.value — a Project (Borrowed per TF-4) that is RETURNED → IA-6 widens the returned value to Owned + HeapEscaping. The [int] is SIMULTANEOUSLY (a) the Box’s owned field (part-2 burden decs it via whole-var drop of xs) AND (b) the returned out value (IA-6-Owned → out also decs it). TWO decs on one allocation → DOUBLE-FREE. The prior spec treated this as a spurious result-INC (a LEAK, net +1 per RL1_duplication_balanced + the doc at ownership_scans/mod.rs:283-287); box_list is a DOUBLE-FREE (too many DECs), so eliding an inc would make it WORSE. Calculus governing it: TF-4 (Project → Borrowed, parent owns + decs the field via whole-var drop-glue) vs IA-6 (return → Owned, returned value decs) CONFLICT. Resolution per spec + RL-2 transfer kinds: unwrap/unbox return self.value BY VALUE = a MOVE of the field OUT of the parent. The field .value TRANSFERS THROUGH the return → the parent (xs) must SKIP the .value field-dec; out owns + decs it once. This is transfers_through_return at FIELD granularity (interprocedural: unbox’s b param transfers its .value field through the return; the contract must record field-level return-flow, and the burden suppression must skip exactly the transferred field while keeping the rest of xs’s burden — the Box header still drops). FIX DIRECTION (next fire, NOT yet implemented): extend the interprocedural contract’s transfers_through_return from param-level to FIELD-PATH level (facts.return_flow in interprocedural/extract already traces Return-flow — check whether it carries the projected field path), then make the burden field-dec suppression (compute_transfer_through_return_param_vars consumer in emit.rs) skip the specific transferred owned_fields[k] rather than the whole param. CALCULUS-FIRST: ground against RL-2 transfer-kind partition (Return = transfer use, no parent dec) at FIELD granularity in lean/AimsProof/Realization.lean; if no theorem covers field-level transfer-through-return, author it per §CP-1 case (b) BEFORE the Rust edit. CORPUS-GATE NOTE: 2 of the prior-claimed “3 new failures” (test_edge_project_return_not_param_keeps_outer_dec, test_generic_forwarder_result_list_str_returns_intact) ARE in corpus_under_flag_gate/baseline_failing_ids.txt — pre-existing tracked expected-fails, NOT regressions from parts 1+2. box_list_int_unwrap is the genuine new failure. Re-verify the exact guardrail-2 comm -13 set against baseline before acting. The prior spec’s alias-traced-aggregate-result-inc fix is RETRACTED (wrong root cause); the field-level-transfer-through-return fix above replaces it.

• 2026-06-08 (part-3 EXECUTABLE SPEC — grounded in the actual gate at ownership_scans/mod.rs:303-340). The box_list double-free fix is a precisely-bounded condition on compute_transfer_through_return_results’s result_repr_admits closure (line 313). CURRENT gate admits Invoke/Apply TTR result dsts whose var_repr ∈ {RcPointer, FatValue}; EXCLUDES Aggregate. The exclusion’s doc rationale (lines 292-302): an aggregate’s inner heap fields are Projected and each projection lineage carries its own RcDec, so the result-inc keeps the inner buffer RC ≥ projection-dec count. THIS RATIONALE IS VOIDED BY PART-1: compute_borrowed_projection_dsts now removes exactly those projection decs (pure borrows get NO dec). When an aggregate result’s projections are ALL borrow-excluded there are no projection decs to balance → the result-inc is spurious (double-counts the transferred-in alloc) → eliding it is sound (identical to RcPointer/FatValue). This is WHY part-2 exposed box_list: burden now active, but the blanket-Aggregate-exclude keeps the spurious result-inc. EXECUTABLE FIX: (1) thread borrowed_projection_dsts (computed in mod.rs ~line 27) into compute_transfer_through_return_results as a new param; (2) extend result_repr_admits to ALSO admit an Aggregate dst WHEN every Project whose value traces (through the move/dup Let{Var} edges + the new invoke_ttr_edges) to the result dst has its projection-dst ∈ borrowed_projection_dsts (no owned projection of the aggregate’s lineage exists). The alias-trace reuses the move-edge build in move_alias.rs:111-131 — factor it into a shared helper to avoid LEAK:algorithmic-duplication. (3) The RcPointer | FatValue unconditional admit STAYS; the Aggregate admit is GATED on all-borrow-projected — any owned projection keeps the aggregate excluded (this is the part-3a 178→1943 over-fire boundary, now made precise instead of blanket-exclude). CALCULUS-FIRST PRECONDITION (arc.md §CP-1): BEFORE the Rust edit, ground the forwarded-aggregate rcBalance in the compiled Lean — box_list (path-sensitive forwarder + aggregate field projection across bb-merge) maps to aims-proof/proofs/10-counterexample/ shapes 04B.2-under-elim (rc_per_path_invariant) + bug-04-118. Read lean/AimsProof/Realization.lean RL1_emit_iff_not_elidable + RL3_elision_net_preserving; confirm the all-borrow-projected aggregate-forward satisfies net-zero-per-path. If the Lean does not cover the shape, author the theorem FIRST (scratch Lean per §CP-4 → land into kernel-checked corpus + sync all four surfaces per §CP-2), THEN implement + immediate guardrail-2 (comm -13 empty). Over-fire fallback: admit Aggregate only when it has ZERO projections (provably safe, but does NOT fix box_list — partial step only). STATE: parts 1+2+invoke-ttr-edge staged in work-stream (corpus 178, net +6/−3 vs 181 baseline). Part-2 (generic-user-struct burden) is architecturally correct + exposes the real box_list forwarder over-release — NOT to be reverted (re-masks a latent leak per the directive). Parts 2+3 are a JOINT: part-2 alone regresses the metric (latent-leak → exposed-double-free); they land together. Next fire executes this spec with fresh context (alias-trace + Lean grounding must not be rushed at accumulated depth). The 5m cron was re-armed this fire (043e0c5d).

• 2026-06-08 (later) — OPERATIONAL CLARIFICATION: this is a large multi-session STAGED work-stream (~38 files), NOT a per-session clean tree; parts 1+2 + Invoke-TTR edge are CORRECT contributions confirmed present (grep-verified) + STAGED. A parallel session co-works the burden-path files (system reminders + active modifications). Per CLAUDE.md parallel-session safety, REVERT is OFF THE TABLE (no clean baseline exists; reverting could clobber concurrent work). Keep contributions; the work-stream commits collectively when the corpus greens. git status: all burden_lower + ori_types + aims-proof changes are M (staged); HEAD 2785086a4 unchanged. Part-3 blocker now PRECISE: the cross-block TTR result %7. transfer_via_move_alias (with the new Invoke-TTR edge) suppresses %4/%6 (the arg + its move-source) but NOT %7: %7 is the Invoke result used in TWO blocks (bb1 via %9, bb5 via %14), so no move-edge makes it a transfer-SOURCE (is_global_last_use needs 1 last_use entry; %7 has 2), and the unified exclusion approach (exclude transfer_via_move_alias from owned_vars) reaches %4/%6 but not %7. So %7’s RESULT inc (compute_invoke_result_incs) + its cross-block last-use dec survive. The value-copy-aggregate JOINT needs %7-specific handling: a TTR-forwarded Invoke/Apply result whose lineage is consumed by copies (%9 dup + %14 move) should itself emit NO ops (result-inc suppressed + last-use-dec suppressed) — the copies carry the inc/dec. This requires recognizing the TTR result as a pass-through owned by its copies, distinct from a fresh result. STRATEGIC: given the parallel session co-works the burden path, the next fire should either (a) coordinate / continue the %7-pass-through handling, or (b) confirm whether the parallel session is already addressing the generics-forwarder cluster before further investment (avoid duplicate effort). Tree: large staged work-stream at 178 (parts 1+2 contributions correct + present).

• 2026-06-08 (later) — Invoke-TTR move-edge IMPLEMENTED (correct building block, NEUTRAL 178) + DEEP part-3 reality corrected: part-2 (aggregate carries RC) makes EVERY emission mechanism over-fire for value-copy aggregate chains — the prior unified recipe mis-identified the mechanism. Implemented compute_transfer_via_move_alias gaining invoke_ttr_edges: &[(result,arg)] (computed in mod.rs from transfers_through_return contracts, integrated into move_edges before the fixpoint). Builds clean, corpus UNCHANGED at 178 — INERT on box_list because the over-emission is NOT last-use decs (which the move-alias suppresses): @main IR shows burden_inc %6/burden_dec %6 = TERMINATOR keep-alive inc + edge dec (owned-arg passing, not last-use); burden_inc %7 = RESULT inc (compute_invoke_result_incs); burden_dec %7 = %7’s last-use dec that the move-alias CANNOT collapse because %7 is CROSS-BLOCK (used bb1 via %9 + bb5 via %14 → is_global_last_use requires exactly 1 last_use_points entry, %7 has 2 → the %14←%7 move-edge is rejected); burden_inc %14 = move-inc. Only %9’s dup pair + %14’s dec are correct. CORRECTED part-3: the value-copy aggregate forwarder over-fires across FIVE mechanisms (terminator-inc, result-inc, cross-block last-use-dec, move-inc, edge-dec) — this is the coherent VALUE-COPY-AGGREGATE EMISSION RECONCILIATION (the JOINT redesign), NOT a point-fix. The Invoke-TTR edge is a correct building block (KEPT) but insufficient alone; the full fix must suppress the terminator inc/dec + result inc + handle the cross-block result dec for the value-copy-aggregate-through-TTR chain so it nets to %9 dup-pair + %14 final-dec = 1 inc + 2 dec. STRATEGIC: this is a genuine JOINT redesign (plan-expansion territory) of how RC-carrying value-copy aggregates emit through forwarders. parts 1+2 (correct, +3) + the edge are the foundation. Given ~175 OTHER corpus failures + this being the single hardest cluster (50+ historical reverts), the next fire SHOULD pivot to a tractable cluster (fat_ptr_iter / match_alias / iter_rc_matrix) for broader progress, returning to this value-copy-aggregate JOINT redesign as a dedicated focused unit (possibly /create-plan —inline §09.2 subsection). Tree: parts 1+2 + Invoke-TTR edge UNCOMMITTED (red 178).

• 2026-06-08 (later) — PART-3 REFINED to a UNIFIED part-1-shaped formulation (supersedes the 4-separate-mechanism framing below). compute_transfer_via_move_alias (move_alias.rs:47) builds move-edges from Let{Var(src)} ONLY — it does not span the Invoke @id (%6 moves in at an owned arg; %7 is a fresh result, not a Let-alias), so the chain %4→%6→%7→%14 never collapses. UNIFIED fix: extend the move-alias chain with an Invoke-transfer-through-return edge (%7 result ← %6 owned-arg) when the callee MemoryContract has transfers_through_return (result IS the forwarded arg = a move across the call). The EXISTING collapse (dec + FRESH-inc suppression, mod.rs:342) then makes %4/%6/%7 transferred (ops suppressed), %14 keeps its single terminal dec, %9 keeps its dup pair. Two NON-FRESH incs must also consult the extended set: %6’s TERMINATOR keep-alive inc (terminator_inc_vars) + %7’s RESULT inc (compute_invoke_result_incs) — exclude members of transfer_via_move_alias. So ONE set (transfer_via_move_alias + Invoke-TTR edges) consumed at 3 emission sites (= part-1’s single-set-multi-consumer shape). GATE: narrow to transfers_through_return callees (NOT part-3a’s broad ValueRepr gate that exploded 178→1943). THREADING: compute_transfer_via_move_alias gains invoke_ttr_edges: &[(result,arg)] computed in mod.rs (has contracts) integrated into move_edges BEFORE the fixpoint. ATOMIC — implement + ORI_TRACE_RC-verify box_list single-free + guardrail-2 comm -13 EMPTY in ONE pass (partial states are unbalanced). Tree: parts 1+2 UNCOMMITTED (red 178). Next fire: implement this unified recipe atomically.

• 2026-06-08 (later) — PART-3 FIX SURFACE FULLY LOCALIZED: the value-copy aggregate transfer-through-return is a COHERENT 4-MECHANISM fix (the M-a/M-b/M-c JOINT applied to the RC-carrying aggregate), NOT a point-fix. parts 1+2 KEPT (178). Traced the @main over-emission to its sources: burden_inc %6 is a TERMINATOR keep-alive inc (terminator.rs:terminator_inc_vars emits one per owned Invoke arg in owned_vars_needing_rc; with part-2 the Box %6 qualifies) + a paired edge dec — both SPURIOUS because @id is a transfers_through_return callee (it forwards %6 back as %7, does NOT consume it), but terminator_inc_vars has no contract access to know this. %7’s dec + %14’s inc are the result move-chain. The 4 mechanisms (must land together; point-fixes over-fire — cf. part-3a’s 178→1943): (1) suppress the terminator keep-alive inc + edge dec for an owned arg passed to a transfers_through_return callee (%6); (2) suppress the result’s last-use dec (%7, carried by move-target %14); (3) suppress the move-target’s spurious FRESH/dup inc (%14 — a move inherits the ref, no new inc); (4) keep %9’s dup inc+dec pair + %14’s move dec (= 1 inc + 2 dec, freed once). Requires threading the transfers_through_return contract into compute_terminator_inc_per_block + the edge-cleanup dec + the move-alias suppression — a coordinated change across the terminator-inc/move-alias/result machinery. This is precisely the LEDGER attempts-54/55 M-a/M-b/M-c JOINT, now cleanly set up by parts 1+2 (the aggregate carries RC). STRATEGIC PULL-BACK (per directive): I have been narrowly focused on this single HARDEST cluster (transfer-through-return, 50+ historical reverts) for several fires while ~175 other corpus failures remain. parts 1+2 (the generic-user-struct burden composition + borrow-projection exclusion) are a CORRECT, net-positive (+3) foundation that EXPOSES the latent value-copy-aggregate bug (CLAUDE.md: keep, never re-hide). Next fire OPTIONS: (a) implement the part-3 4-mechanism JOINT from this exact substrate; OR (b) keep parts 1+2 and PIVOT to a more tractable cluster (fat_ptr_iter / match_alias / iter_rc_matrix per the LEDGER cluster list) for broader corpus progress, returning to the part-3 JOINT with the foundation in place — the generics-forwarder JOINT need not block the other clusters. Tree: parts 1+2 UNCOMMITTED (red 178; do NOT commit until a cluster greens).

• 2026-06-08 (later) — part-3a (admit Aggregate in transfer-through-return result-inc elision) CATASTROPHIC over-fire 178→1943, REVERTED clean; KEY NEGATIVE RESULT: the result-inc-elision Aggregate-exclusion is LOAD-BEARING for the broad corpus. parts 1+2 KEPT (178, net +3). Part-3a tried extending compute_transfer_through_return_results result_repr_admits to admit ValueRepr::Aggregate (to elide the forwarder-result Box<[int]>’s spurious burden_inc %7). On-target it removed the %7 inc, but the full corpus EXPLODED to 1943 failed (660 pass) — eliding aggregate result-incs broadly double-frees every aggregate-returning forwarder whose inner fields ARE independently projected+dec’d (the doc’s original reasoning holds across the corpus). REVERTED clean (gate back to RcPointer | FatValue; build clean; corpus back to 178). PART-3 PRECISELY BOUNDED: the 3 new failures (box_list_int_unwrap, edge_project_return_not_param_keeps_outer_dec, forwarder_result_list_str) are the value-copy aggregate SPECIFICALLY through the Invoke @id transfer-through-return. parts-1+2’s whole-var-drop aggregate RC COEXISTS fine elsewhere (the move/dup-alias suppression collapses non-forwarder aggregate copies — that’s why part-2 is net-POSITIVE, fixing the derived_clone cluster); only the Invoke-result move-chain breaks: @main IR over-emits burden_inc %6/burden_dec %6 (the Box moving INTO @id) + burden_dec %7 (the result, move-aliased to %14) because the move-alias suppression (compute_transfer_via_move_alias) does NOT span the Invoke-result transfer-through-return (%6 moves in, %7 is a fresh result, not a Let-alias of %6). PART-3 FIX SURFACE (narrow, must NOT touch the broad result-inc gate): make the callee transfer_through_return_param_vars (M-a) + caller-side move-chain suppression span the Invoke @id result for the RC-carrying aggregate, so %6/%7’s spurious aggregate inc/dec are suppressed (the value-copy aggregate shares the [int] buffer; only %9’s dup inc/dec + %14’s move dec should survive = 1 inc + 2 dec, freed once). This is the M-a/M-b/M-c transfer-through-return JOINT (LEDGER attempts 54/55) now applied to the RC-carrying aggregate — needs the narrow Invoke-result move-chain suppression, NOT the broad gate. Tree: parts 1+2 UNCOMMITTED (red 178; do NOT commit until part-3 greens). Next fire: implement the narrow Invoke-result aggregate move-chain suppression, ORI_TRACE_RC-verify box_list single-free, guardrail-2 comm -13 EMPTY.

• 2026-06-08 (later) — BREAKTHROUGH: part-2 (generic-user-struct burden composition) IMPLEMENTED + WORKING + KEPT in-tree; part-1 KEPT; the forwarded-aggregate JOINT is now 3-PART (part-3 = value-copy-aggregate inc/dec, a LATENT bug part-2 exposed). PART-2 (3 edits, ori_types): (a) compute_struct_burden_from_field_types(&[Idx], pool) added to burden_compute.rs (per-instantiation analogue of compute_struct_burden, classifies substituted field types); (b) compose_for_idx (monomorphization.rs:440) extended with a user-struct branch — for an Idx resolving to Tag::Struct, composes the burden from pool.struct_fields(resolved) types + record_composed_burden(idx, …) (the builtin templates covered Option/Result/[T]/etc. ONLY; user structs _ => return’d); (c) re-applied resolve_applied_type for the free-function-mono path’s concrete param/return types (sets Box<[int]>→Struct{value:[int]} resolution so (b)‘s resolve_fully sees concrete fields). VERIFIED via burden-probe: Box<[int]> now enters owned_vars_needing_rc (@main owned [3,10,15]→[3,4,6,7,9,14] — aggregate vars 4/6/7/9/14 now carry RC; projections 10/15 excluded by part-1). PART-1 (ori_arc): compute_borrowed_projection_dsts re-applied + wired. Full AOT corpus 181→178 (net +3); guardrail-2 SET: 6 FIXED (same derived-clone cluster) but 3 NEW — generics::{test_box_list_int_unwrap, test_edge_project_return_not_param_keeps_outer_dec, test_generic_forwarder_result_list_str_returns_intact} — ALL the value-copy-aggregate over-release class. PART-3 (the exposed latent bug): with the aggregate now carrying RC, Box value-copies (%4→%6→%7→%9/%14, sharing the SAME [int] buffer — fat-ptr copied, not buffer) each get dup/move-alias burden_inc/burden_dec pairs that over-release the shared [int] (@main IR: burden_inc %6;burden_dec %6 BEFORE Invoke @id, burden_inc %7;…;burden_dec %7, plus %9/%14 pairs → trace alloc rc=1; dec rc=1; dec rc=0 FREE; dec DOUBLE-FREE). The move/dup-alias machinery doesn’t collapse aggregate value-copies that share a heap field — the move-chain breaks at the Invoke @id transfer-through-return (%6 moves in, %7 is a fresh result, not a Let-alias of %6). PART-2 KEPT (not reverted): it is the correct, missing architectural path + net-positive; reverting would RE-HIDE the latent value-copy-aggregate bug (CLAUDE.md never-hide-bugs). The 3 new failures ARE part-3, found by part-2. Next fire: implement part-3 on the kept parts-1+2 tree — collapse aggregate value-copy inc/dec so a shared heap field is released exactly once (the move/dup-alias suppression must span the Invoke-result transfer-through-return; likely the M-a/M-b/M-c transfer-through-return mechanisms now applying to the RC-carrying aggregate). Build, ORI_TRACE_RC-verify single-free on box_list, then guardrail-2 comm -13 EMPTY for the full JOINT (projected ≥ +8). Tree state: parts 1+2 UNCOMMITTED (red 178, do NOT commit until part-3 greens).

• 2026-06-08 (later) — PART-2 FULLY CHARACTERIZED: generic-user-struct burden composition is ENTIRELY MISSING (architectural gap, not a point-fix). resolve_applied_type mirror ATTEMPTED + REVERTED (insufficient). Tried the bounded fix — mirror the method-mono path’s resolve_applied_type(receiver) (monomorphization.rs:279) in the FREE-FUNCTION path maybe_record_mono_instance (added resolve_applied_type for concrete_param_types/concrete_return_type). Built clean; BURDEN-PROBE (re-added, removed clean, git diff EMPTY) showed @main owned=[3,10,15] UNCHANGED — Box<[int]> still empty owned_fields, fixture still double-frees. ROOT: resolve_applied_type registers the Applied→Struct type RESOLUTION (pool.set_resolution, monomorphization.rs:747-748) but does NOT compose the BURDEN. Decisive: compose_user_burden (burden_compose/mod.rs:75) takes a BuiltinBurdenSpec TEMPLATE — take_composed_burdens (infer/mod.rs:551) composes per-instantiation burdens for generic-BUILTINS ONLY (Option/Result/[T]/{K:V}/Set per infer/mod.rs:212). Generic-USER-structs (Box<T>) have NO per-instantiation burden-composition path — only the declaration-time generic burden (compute_struct_burden with the unresolved T field ⇒ empty owned_fields). PART-2 FIX (mirror the builtin path for user structs): at struct instantiation, compute compute_struct_burden(concrete_field_defs, pool) (burden_compute.rs:92, signature confirmed: classifies [int]→FieldClass::Owned) and REGISTER it PER-INSTANTIATION so ori_arc lookup_burden(Box<[int]>) resolves owned_fields=[value@0] (distinct from the generic Box<T>, exactly as builtins distinguish Option<str> from Option<T>). Location: infer/expr/calls/monomorphization.rs (instantiation site) + the per-instantiation registration surface (mirror take_composed_burdens). This is the §09.2 burden-path completion for user-struct instantiations — fits within §09.2, no new plan. Once part-2 lands (Box<[int]> carries RC ⇒ aggregate whole-var dec via drop-glue), re-apply part-1 (borrow-projection exclusion, code recorded above) ⇒ JOINT: [int] freed once, projected net +8 (box_list + result_list_str + the 6), guardrail-2 comm -13 EMPTY. Baseline pristine (all attempts reverted clean).

• 2026-06-08 (later) — PART-2 ROOT-CAUSED + LOCATED via burden-walk probe; the forwarded-aggregate JOINT is CROSS-CRATE (ori_arc part-1 + ori_types part-2). A same-build-cycle eprintln probe in burden_lower/mod.rs (dumping owned_vars_needing_rc + dec-sites; removed clean, git diff empty — the ori_arc::aims::realize trace does NOT fire for ori build/check/run, a separate tooling gap) showed for generic_forwarder_box_list @main: owned=[3,10,15] dec_sites=[3,10,15] — i.e. the [int] %3 + the two borrowed Projects %10/%15, but the Box aggregate lineage %4/%6/%7/%9/%14 is ABSENT from owned_vars_needing_rc. So the Box<[int]> burden spec has EMPTY owned_fields (burden_carries_rc false) — the aggregate never carries RC, never gets a whole-var dec, and the [int] drop is (wrongly) delegated to the borrowed projections (the double-free; %3’s own dec is transfer-suppressed into the Construct Box(%3)). GENERIC-SPECIFIC: part-1 FIXED the 6 non-generic fat_matrix::f20_derived_clone struct-with-heap-field cases (their aggregate burden DID carry RC), but the GENERIC Box<T>→Box<[int]> instantiation’s burden is missing the [int] owned field — matching the value_heap_mixed_variant UNIT test (which manually registers owned_fields=[str@1] and passes). Part-2 fix location: ori_types/src/check/registration/burden_compute.rs + infer/expr/calls/monomorphization.rs (D02 monomorphization ordering + D06 TypeEntry.burden: UserBurdenSpec storage) — a generic struct instantiated with a heap type-arg must propagate the field’s heap-ness into the instantiated owned_fields. The JOINT (lands together, both affect only the burden path post-retirement): part-1 ori_arc compute_borrowed_projection_dsts borrow-projection exclusion (code recorded above) + part-2 ori_types generic-struct-instantiation owned_fields registration. Next fire: implement part-2 (populate generic-instantiation owned_fields), verify Box<[int]> enters owned_vars_needing_rc (whole-var dec fires, drop-glue frees [int] once), then re-apply part-1, ORI_TRACE_RC-verify single-free on box_list+result_list_str, guardrail-2 full AOT (comm -13 EMPTY) — projected net +8.

• 2026-06-08 (later) — ATTEMPT (borrow-projection exclusion / part-1 of the forwarded-aggregate JOINT) IMPLEMENTED + validated-on-target + REVERTED clean (guardrail-2 over-fire by 1). Built compute_borrowed_projection_dsts (ownership_scans/mod.rs): a Project dst whose EVERY use is a borrow position (gated against owned-position transfer + Return escape per RL-15a) excluded from owned_vars_needing_rc — RL-2/TF-4 (a borrowed field-read owns no allocation; the parent aggregate drops the field). Wired as a retain exclusion in mod.rs. Result: eliminated the generic_forwarder_box_list double-free (the spurious burden_dec %10/burden_dec %15 on the two borrowed Project b2.0 reads gone). Full AOT corpus 181→176 (cargo test -p ori_llvm --test aot); guardrail-2 SET (comm vs the 181 baseline): 6 FIXED (arc::test_rc_project_merge_edge_scoped_cleanup, fat_matrix::f20_derived_clone::{map_field,struct_list_fat,struct_list_scalar,struct_str_heap}, predicate_stack_probe::probe_derived_clone_used_struct_str_field_no_leak) but 1 NEW (generics::test_generic_forwarder_result_list_str_returns_intact) → guardrail-2 comm -13 NON-EMPTY ⇒ REVERTED clean (re-Edit, no git ops; git diff --stat EMPTY both files; fixture back to baseline double-free; oric builds clean). DECISIVE part-2 localization (ORI_DUMP_AFTER_BURDEN full @main post-part-1): the value-copy Box aggregate lineage %4 Construct → %6 → %7 Invoke@id → %9/%14 copies has ZERO burden ops — no whole-var dec, no partial. The [int] was freed ONLY via the (over-firing, 1-per-borrowed-read) projection decs; excluding them ⇒ LEAK. So the forwarded-aggregate shape is a LOCKSTEP JOINT: part-1 (borrow-projection exclusion, code-ready, RL-2/TF-4) + part-2 (the value-copy aggregate must emit a WHOLE-VAR dec — drop-glue covers the heap field once, per the value_heap_mixed_variant param-aggregate contract). Part-2 root cause to localize next: %9=%7/%14=%7 are dup/move-aliases of an owned aggregate whose sole use is a borrowed Project, and the dup/move-alias emission produces NO inc/dec for them (NOT excluded by compute_borrowed_alias_vars — source-gated on borrowed PARAMS, and %7 is an owned Invoke-result). JOINT (part-1+part-2) projected: fixes box_list + result_list_str + the 6 = net +8, 0 broken. Predicate stack retired (mod.rs:69), so both halves affect only the burden path.

• 2026-06-08 (later) — GROUND-TRUTH on generic_forwarder_box_list REFINES the generics-cluster bug shape: it is BORROW-PROJECTION OVER-DEC, NOT the M-a/M-b transfer-through-return inc-JOINT. Rebuilt dev oric+ori_rt (libori_rt.a present); ORI_TRACE_RC burden vs predicate-stack oracle: burden = alloc rc=1 → dec rc=0 FREE → dec → DOUBLE-FREE (0 inc, 2 dec); oracle = alloc → inc → dec → dec rc=0 (1 inc, 2 dec, freed once). ORI_DUMP_AFTER_BURDEN on @main: the [int] buffer %3 is wrapped in Box %4; b2=%7 (forwarded Box); bb1: %10=Project %9.0; burden_dec %10 then bb5: %15=Project %14.0; burden_dec %15 — BOTH %10/%15 are Project of the owned Box’s RcPtr field (the SAME [int]), used PURELY at borrow positions (@len [borrow], @__index [borrow]). Per TF-4 a Project is Borrowed; per RL-2 borrowed values get NO dec — the burden path wrongly emits a burden_dec on EACH borrowed projection (2 decs / 1 alloc / 0 inc / no %7 aggregate-drop) ⇒ −1 double-free. @id itself is correct (Return %1, no dec). CURE (project-escape-aware, the LEDGER’s flagged-but-untried secondary residual): exclude a Project-dst of an owned aggregate’s RcPtr field from owned_vars_needing_rc WHEN it is used ONLY at borrow arg positions (NOT a blanket Project-dst exclusion — RL-15a project-escape may add an inc), AND ensure the owning aggregate (%7/Box) gets its single scope-exit field-drop so the [int] frees exactly once (alloc+1, 1 dec, net 0; no inc needed — simpler than the oracle’s 1-inc-2-dec model). Predicate stack is RETIRED (aims_pipeline/mod.rs:69 defaults predicate_stack_rc_disabled=true) so the fix affects ONLY the burden path — no coexistence double-emit. Next fire: implement the project-escape-aware borrow-projection exclusion + aggregate-field-drop in LOCKSTEP (burden_lower/ownership_scans + emit.rs), ORI_TRACE_RC-verify the fixture frees %3 exactly once, then guardrail-2 full AOT (rebuild ori_rt, 0-staticlib-abort, default==baseline before keep).

• 2026-06-08 (later, same day) — SUPERSEDES the M-a-PARTIAL entry’s “cross-session baseline instability / parallel monomorphization” blocker: that diagnosis was FALSE. Rebuilt-from-disk: cargo build -p ori_types -p ori_arc -p ori_llvm Finishes clean (zero errors) — there is NO parallel-session compile break, and the 18 uncommitted ori_types monomorphization files are part of THIS work-stream’s tree, not an external session adding reds. The len-unresolved symptom that fed the “baseline instability” claim was an artifact of standalone ori check not auto-loading the prelude (no regression; len resolves in the prelude-loaded AOT path). The real state per decisions/LEDGER.md (attempts 54/55/57, SSOT, predates this drift): default-path baseline = 16, under-flag floor = 141 (attempts 56+57 KEPT — str + list borrowed-read carve-outs, uncommitted). The generics 27 cluster IS the transfer-through-return JOINT (NOT probe-gateable) needing THREE coordinated mechanisms: (M-a) callee transfer-source-dec strip gated by per-lineage alloc-aware net (unconditional strip over-fires single-call-safe callees — the current uncommitted compute_transfer_through_return_param_vars is the UNGATED form the attempt-55 killing clause rejected); (M-b) caller RL-1 keep-alive-inc per may-unwind borrowed read (missing-inc count = #reads − 1; N≥3 threshold); (M-c) keep-alive-inc emitted before edge-cleanup dec. Attempt-55 KILLING CLAUSE governs the resume: the JOINT broke default 16→61 despite probe-gating — root-cause the default-path regression FIRST (re-confirm whether default==16 reproduces, or the uncommitted ungated M-a leaked to the default path causing the borrow_list_int_*_then_return double-frees/UAFs now observed on the default emitter) BEFORE the next coordinated attempt. §09.2 is resumable NOW by this /continue-roadmap run — it does NOT gate on any external session. Concrete default-path baseline (rebuilt-from-disk cargo test -p ori_llvm --test aot, 47s): 181 failed / 2422 passed / 29 ignored. The “16” baseline above is the §09-COUPLED COHORT subset, NOT the full corpus — the full default-path AOT corpus carries 181 RC failures, the genuine ./test-all.sh-green / nightly-CI blocker. Cluster breakdown (resume substrate; pick a NON-&&-branchy single-mechanism cluster ground-truthed on its ACTUAL fixtures per the LEDGER next-leaf discipline): fat_ptr_iter 37 (iter-consume, distinct mechanism), predicate_stack_probe 28 (under-flag burden-self-sufficiency pins), generics 18 (transfer-through-return JOINT M-a/M-b/M-c), match_alias 13, iter_rc_matrix 12, fat_matrix 11, narrowing 7, for_yield_option 7, arc 6, rc_matrix 5, recursive_derive 4, higher_order 4, elem_dec_scope 4, string_sso 3, recursive_feature 3, cli 3, aims_interactions 3, + ~13 singleton/pair clusters. SCOPE PULL-BACK — RESOLVED (LEDGER read in entirety via head + grep-inventory + frontier extraction; retirement state confirmed in code). Plan is CORRECTLY SCOPED — no /create-plan --inline expansion needed. The §09.2 activation flip is DONE (uncommitted): aims_pipeline/mod.rs:69 makes predicate_stack_rc_disabled TRUE by default (ORI_DISABLE_PREDICATE_STACK_RC unset ⇒ disabled), so the predicate stack is RETIRED and the burden path is the sole default emitter. The “default-path = 181” IS the burden path’s residual now exposed on default/CI by the flip (the old “default 16” was the pre-flip predicate-stack cohort). Drive 181 → ⊆16 cluster-by-cluster per the LEDGER latest next-leaf, dominant-first: (1) generics-forwarder transfer-through-return (~20) ← START, (2) fat_ptr_iter iterator-handle/catch (~15), (3) per-element emit_dead_at_entry_decs/elem_dec_fn + concat/COW liveness. Each = one guardrail-2 cycle (revert on ANY new failure outside baseline), 0-staticlib-abort CLEAN AOT run (rebuild ori_rt, confirm target/debug/libori_rt.a pre-run). Generics-forwarder bug (ground-truthed generic_forwarder_box_list.ori: @id<T>(x:T)->T=x forwards Box<[int]>, result’s inner list borrowed twice): the M-a transfer_through_return_param_vars callee dec-strip is now ACTIVE on the default path (gated on predicate_stack_rc_disabled=true) but INSUFFICIENT ALONE — a JOINT per attempt-55 (callee over-dec M-a strips + caller keep-alive-inc M-b per may-unwind borrowed read, missing-inc = #reads−1 = 1 here + M-c ordering). Governed by RL-2 (Return = ownership-transfer ⇒ no callee dec) + RL-1 (caller keep-alive on may-unwind borrow); UNSAT counterexample shapes ⇒ implementation-conformance fix per arc.md §CP-1, NEVER a calculus change. 50+ prior arm-by-arm attempts REVERTED (guardrail-2); the LEDGER’s recurring verdict is “JOINT redesign, not arm-by-arm” — next attempt builds M-a+M-b+M-c IN LOCKSTEP, ORI_TRACE_RC-ground-truthed to the freed address BEFORE editing, re-measure default==baseline before keep.**

• 2026-06-08 — §09.2 Phase-1 M-a cohort PARTIAL (generics transfer-through-return strip); under-flag gate BLOCKED on cross-session baseline instability. Resumed §09.2 Phase-1 broad-shape burden-emission completion (predicate stack STAYS as default emitter per LEDGER D09 reversible-by-non-execution; burden emission extended + measured under ORI_DISABLE_PREDICATE_STACK_RC=1, NO predicate-stack removal, NO activation flip — correctly deferred to post-convergence). M-a generics forwarder transfer-through-return cohort: callee transfer-source-dec strip — consumes the function’s own MemoryContract.params[i].transfers_through_return (proven Return-flow fact) to suppress a param’s last-use BurdenDec when it flows to a Return terminal use. CONFORMANCE completion (RL-2 RL2_transfer_kinds_no_dec, Realization.lean:174-206 — a Return is an ownership-transferring TerminalUse, callee emits no dec), NOT a calculus change; no calculus gap. Probe-gated so the default path is byte-identical-inert. Result: 14 M-a IDs fixed under-flag (under-flag generics 32→19); ori_arc lib 1642/0; 5 new probe pins in predicate_stack_probe.rs (4 positive + 1 negative over-strip pin) green under-flag, leak-free, VF-1 net 0. Files: ownership_scans/mod.rs (compute_transfer_through_return_param_vars), burden_lower/{mod.rs,emit.rs}, predicate_stack_probe.rs. **BLOCKER (cross-scope, out of reach): the §09.2 under-flag SET-subset gate (failing_ids_under_flag ⊆ baseline_failing_ids) is UN-TRUSTABLE while the default-path baseline is unstable — it moved from 2026-06-04 2344/16 to 19+ generics fails now, because the parallel session’s in-progress generics-MONOMORPHIZATION (recent committed feat(typeck): monomorphization commits + uncommitted state; the pre-existing generics/BUG-04-119 cohort) is actively adding/reds generics AOT cells. Per Git Safety the parallel monomorphization is untouched. §09.2’s remaining cohorts (M-a fat_ptr_iter ~37, M-c ~12+matrix, Cure-A ~29) + the §07B.4 baseline RE-CAPTURE + the coupled removal+activation all gate on a STABLE default-path baseline. Autopilot disposition: M-a progress retained (probe-gated, default-inert, additive); §09.2 resumes when the parallel monomorphization lands + the baseline stabilizes (the /continue-roadmap loop re-attempts on re-fire).

• 2026-06-08 — Linear-execution rule #1/#4 auto-reversal: plan-cleanup detected out-of-order subsection completion (09.R.H marked complete while a predecessor was not). Reverted those subsections + completion checklist to not-started; flipped section reviewed: true → false. Re-run /review-plan to determine next steps.

• 2026-06-07 — Linear-execution rule #1/#4 auto-reversal: plan-cleanup detected out-of-order subsection completion (09.R.H marked complete while a predecessor was not). Reverted those subsections + completion checklist to not-started; flipped section reviewed: true → false. Re-run /review-plan to determine next steps.

• 2026-06-02 — Real-RC activation relocated IN from §06.1 (routing.md §4 cure for §06.1 linear-execution block): §06.1 established the clean mechanical-lowering SITE (realize/mod.rs thin dispatcher, zero predicate-stack queries, faithful Phase-5 emission VF-1=0, mirror removed) but its two real-RC [ ] items (BurdenInc→RcInc / BurdenDec→RcDec mechanical-mapping flip + real-RC FileCheck-on-RcDec test pins) were §09-coupled and carried banned <!-- blocked-by: §09 --> annotations. Per routing.md §4, the items MOVED here: §09.2 retires the parallel predicate-stack RC emitters (walk_dec.rs/emit_unified.rs), so the burden ops become the SOLE RC emitter — the no-op→real-RC flip is safe HERE (the LEDGER §B.2 double-emit/double-free hazard dissolves WITH the predicate-stack removal, never before it). Added: §09.2 checkboxes for the BurdenInc→RcInc/BurdenDec→RcDec activation + its 3 real-RC FileCheck pins; a success_criterion for the activation; realize/mod.rs to touches:. §09 is the natural home — its predicate-stack retirement IS the precondition the activation needs.

• 2026-06-02 — Reworked §09 to ground the coexistence retirement in the proven §11 CH- theorems + added §09.5 CH-proof disposition.* The retirement of predicate_stack_path + the coexistence handshake was reframed from a mechanical deletion to a PROVEN-EQUIVALENCE-LICENSED deletion: §07’s universal class_covered collapses the proven CH-comp soundness partition (CHcomp_handshake_union + CH2_single_elimination + CH3_classes_disjoint) to its class_covered case, where coexistence_dispatch ≡ burden_emission_path ≡ predicate_stack_path — so deleting the redundant predicate path preserves observable behavior by the proof. The reconcile_burden_ledger mirror removal is grounded in CH-1 (burden_emitted = burden_owned, no independent ledger) + CH-4 (CH4_state_map_immutable, BR reads L read-only). Added §09.5 to fill the gap the research surfaced — aims-proofing-suite §11 has no supersession clause, so §09 (the consumer) records the disposition: the CH .proof + lean/AimsProof/Coexistence.lean are RETAINED as the MS-4 published theorem + the retirement-safety certificate (the proofs are over the model, not the shipped Rust, so the shipped deletion leaves them kernel-valid); CH-4’s shipped eliminate_burden_ops binding SURVIVES; dual-discharge.sh re-runs clean post-retirement as a confirmation step. mission criteria 13 + 16 noted as the §09 close-out flips.

• 2026-06-02 — Coexistence-mirror-disabled correctness gate moved in from §05.N (per /review-plan §05 review, 3-reviewer Critical STRUCTURE:section-not-independent). The gate tests Phase-6 elimination over the SELF-SUFFICIENT burden baseline with the reconcile_burden_ledger coexistence mirror OFF — the post-convergence elimination state §09 targets, not §05’s mirror-balanced baseline. Self-sufficient burden emission is not implemented until §09 retires the predicate stack + mirror, so gating §05 close on it would either block on downstream §09 work or be unverifiable at §05 close. Landed as a §09.4 checkbox (alongside the existing reconcile_burden_ledger removal + emission-nets-0 VF-1 check) + a §09.N completion-checklist item. §05’s success_criteria stay scoped to mirror-balanced DP-2/DP-3 elimination correctness.

• 2026-05-30 — Recorded the 6 BUG-04-123 surgical fixes as predicate-stack annotations §09 strips (plan reframe per user directive). BUG-04-123’s §05 landed 6 narrow predicate-stack patches (32 -> 17): container_payload_moved_out (post_convergence.rs), the PIN-4 defined_at_or_before guard (edge_cleanup.rs), class_member_suppresses post-dominance dedup (emission_site.rs), and build_global_pin4_emits / build_lineage_map / predict_retained_roots consumption-aware lineage machinery (emit_unified.rs + walk.rs). These are annotations the completed burden path supersedes — 09.2 retires them alongside class_alive_after / pin4_class_emits_dec_set / pin6_any_ancestor_will_cover, mirroring BUG-04-118’s 62. The four uncoordinated emission paths they patch collapse to one burden trivial-emit + DP-2/DP-3 elimination path; decisions/07 §4.1 + §8 carries the rationale + the empirical proof (10 ruled-out broad approaches). BUG-04-123 absorbed to 00-overview.md absorbed_bugs[]; realize/emit_unified.rs added to §09 touches.

• 2026-05-29 — §09 reframed as the GREEN-CRITICAL coexistence retirement (per 00-overview.md 2026-05-29 reground). The ~671 ./test-all.sh VF-1 burden-imbalance failures are impl-fidelity divergences resident in the burden-op ↔ predicate-stack COEXISTENCE layer — a TRANSITIONAL migration bridge whose soundness the proven CH-1..CH-comp certify (CH-1 reformulated_and_proven, CH-2..CH-comp proven_sound per the aims-rules.md HISTORY 2026-05-28 terminal-state table; .proof at compiler_repo/aims-proof/proofs/11-coexistence/CH-*.proof + Lean mirror AimsProof/Coexistence.lean), alongside the core calculus (DP/RL/VF/IC/PL) of the kernel-checked corpus. §09’s retirement of the emission-side predicate stack (class_alive_after / pin4_class_emits_dec_set / pin6_any_ancestor_will_cover / canonical_rep_for / var_emits_dec_in_block) + the class_covered coexistence handshake is therefore the load-bearing path to full green: it DELETES the coexistence machinery — which the completed burden path SUPERSEDES — so the compiler runs on the proven burden calculus alone, dissolving the 671 by construction rather than hand-fixing each. The proven CH coexistence proofs certify the §07→§09 bridge during the migration window; the layer is superseded, NOT a permanent dependency of the end state. Precondition unchanged: §07 class_covered universal before the handshake removes itself.

• 2026-06-03 — Stale review_pipeline: marker cleared by /continue-roadmap orchestrator: marker carried stage: ?, next_step: ?, updated: ?. Per /review-plan SKILL.md §Step 1a stale-marker rule (reviewed: false + marker present → STALE by definition), marker invalid; prior diagnosis preserved here for traceability. Cure rooted in scripts/plan_orchestrator/markers.py:clear_stale_marker_if_unreviewed.

• 2026-06-04 — §07A closed → §09.2/§09.3/§09.4/§09.N block LIFTED. §07A (Burden-Lowering RC-Ledger Self-Sufficiency) reached status: complete + reviewed: true (its HISTORY 2026-06-04 + §07A.N checklist): the burden path is now a complete standalone RC emitter — the ORI_DISABLE_PREDICATE_STACK_RC self-sufficiency probe (11 probes, compiler/ori_llvm/tests/aot/predicate_stack_probe.rs) passed zero-new-vs-16-baseline + leak-free + double-free-free under ORI_CHECK_LEAKS=1, with the move-alias / duplication-alias / borrow-flow / collection-buffer RC the overlay had deferred to the predicate stack now emitted by the burden path itself. The §09.2-readiness gate (the §07A.3 corpus gate) is MET. The structured blocker is the section-level depends_on: [07A] (already in frontmatter, schema-supported), now SATISFIED by §07A’s completion — the SubsectionEntry schema carries no per-subsection blocked_by field, so the §09.2/§09.3/§09.4/§09.N block is recorded by the satisfied section-level depends_on plus this HISTORY note (per state-discipline.md §3 + routing.md §2 — the block is no longer §05-prose-only). The 2026-06-03 BLOCKED entry below is the at-block diagnosis, now resolved. §09.2 reverts to not-started (the 2026-06-03 attempt reverted cleanly to baseline with no §09.2 checkboxes flipped, so no in-progress work persists; §09.2 is ready-to-start). §09.4’s first checkbox now gates on BOTH §07 (coverage) AND §07A (lowering self-sufficiency). Added: §07A predicate-stack-retirement readiness verification (re-run the 11-probe suite) to the §09.2 activation close-gate; a dead-code-cleanup success criterion + §09.4 checkbox + §09.N item deleting the class_covered + class_dec_obligations storage maps + accessors from AimsStateMap (state_map.rs); realize/{tests,decide}.rs, realize/burden_elim/tests.rs, intraprocedural/mod.rs, interprocedural/extract.rs to touches: (handshake-removal compilation surface).

• 2026-06-03 — §09.2 BLOCKED: burden path is NOT a complete standalone RC emitter (empirically discovered + verified-with-facts). §09.1 disposition done (decisions/09-post-convergence-disposition.md, commit 41e7b1dc). §09.2 execution attempted the lockstep predicate-stack-retirement + real-RC-activation, measured the corpus, reverted cleanly (compiler tree at baseline AOT 2329 pass / 16 fail). Discovery: lower/burden_lower/mod.rs:261 states verbatim a Let { Var(src) } duplication-alias whose source stays live “carries NO burden ops” because “the predicate-stack emits the alias’s real RcInc/RcDec” — burden_lower is a duplication-tracking OVERLAY that deliberately DEFERS move-alias / Let-Var-alias / borrow-flow RC to the predicate stack. Removing the predicate stack with burden-as-sole-emitter regressed AOT 2329/16 → 1300 pass / 1045 fail (+1029 systemic) across every RC category (fat_matrix, fat_ptr_iter, collections_ext, rc_matrix, string_sso, cow_map_set, …): move-alias chains double-free (pre-elim) or LEAK (post-DP-2-elim collapses the freeing dec); collections emit NO RcDec. ROOT: §07’s class_covered-universal + VF-1=0 claim is true for coverage ANALYSIS but FALSE at the RC-LOWERING level — VF-1=0 holds precisely BECAUSE the deferred ops carry no burden ops (net-zero by absence) while the predicate stack supplies the real freeing RC. The proven calculus (RL-2 dec-at-last-use, CH-1 burden_emitted = burden_owned) is the spec; the burden_lower IMPLEMENTATION diverges by deferring move/alias/borrow RC. CURE (architecturally-correct, soundness-load-bearing per the standing directive): a NEW prerequisite work item makes emit_burden_ops/burden_lower emit a COMPLETE standalone RC ledger — (a) NO BurdenInc for move-aliases (Let { Var(src) } where src is consumed), (b) a BurdenDec at the true final last-use of each allocation lineage that SURVIVES DP-2 elimination (not elided as move-through-Dead), (c) the duplication-alias RcInc/RcDec the overlay currently defers — BEFORE §09.2 predicate-stack retirement is sound. §09.2 / §09.3 / §09.4 / §09.N are now blocked-by that prerequisite (inserted via /create-plan —inline as a sibling sequenced after §07, before §09). No §09 checkboxes flipped beyond §09.1.

• 2026-06-04 — §09.2 RE-BLOCKED: §07A self-sufficiency INCOMPLETE corpus-wide; §07B prerequisite required (empirically re-measured). §07A closed complete/reviewed:true on the strength of its 11-probe ORI_DISABLE_PREDICATE_STACK_RC gate, but that gate is TOO NARROW. The §09.2 execution (validated end-state behavior before editing, zero code edits, no LEDGER §B.2 dead-end re-tried) measured: AOT baseline (predicate stack ON) 2344/16; under ORI_DISABLE_PREDICATE_STACK_RC=1 (the §09.2 end-state) 1784/576 — +560 NEW failures, the SAME shape as the 2026-06-03 attempt. Scoped confirm: fat_ptr_iter 136/0 → 21/115. Newly-failing clusters: fat_ptr_iter (115), fat_matrix (59), iter_rc_matrix (52), generics (38), rc_matrix (31), elem_dec_scope (26), collections_ext (26), string_sso (16). ROOT: lower/burden_lower/ tracks only the whole-var collection result and DEFERS per-element / iterator-source / collection-element / matrix / SSO RC to the predicate stack — the 11 probes (move-alias / dup-alias / borrow-chain / collection-buffer-last-use / closure-capture / partial-move) never exercised these shapes, so the CH-comp proven-equivalence license (class_covered universal) is FALSE for them. CURE (per standing directive — plan-expansion territory, /create-plan —inline, choose-recommended-not-ask): a §07A-class prerequisite §07B (broad-shape burden self-sufficiency: iterator-from-collection / fat-pointer-matrix / iter-RC-chain / collection-element / SSO) that ALSO replaces the narrow 11-probe readiness gate with the FULL AOT corpus under ORI_DISABLE_PREDICATE_STACK_RC=1 = zero-new-vs-baseline (the corpus IS the probe). §07A stays complete for the shapes it covered; §07B completes the remainder. §09.2/§09.3/§09.4/§09.N gate on §07B. No §09 checkboxes flipped. Cross-ref: LEDGER §B.2 + §B.3 2026-06-04 re-block lines.