Section 07B: Broad-Shape Burden-Lowering RC-Ledger Self-Sufficiency

Goal: PROVE the burden path’s PROBE-GATEABLE self-sufficiency for the broad value shapes §07A did not cover — iterator-from-collection, fat-pointer / nested-collection (matrix), iter-RC-chain, collection-element, SSO strings — driving the under-ORI_DISABLE_PREDICATE_STACK_RC=1 AOT corpus 517→115 via the shared Phase-7 alloc-aware-net foundation (LEDGER D08 M1/M2/M3), CLASSIFY the §09.2-territory residual (each remaining cluster → its §09.2-owned Phase-5 emission mechanism), and AUTHOR the §07B.4 corpus-under-flag SET-subset gate-harness + capture the baseline-16 failing-ID SET as a checked-in fixture. §07B does NOT complete the broad-shape ledger corpus-wide and does NOT assert the ⊆16 PASS: the COMPLETE standalone ledger (the ~99 under-flag-only JOINT residual) + the corpus-wide ⊆baseline VERDICT are §09.2’s — the M-a callee-strip / per-element emit_dead_at_entry_decs / COW-loop-liveness Phase-5 emission is M-c-banned while the predicate stack coexists (attempt-55 broke default 16→61), inseparable from §09.2 predicate-stack retirement. §07B is the probe-gateable-proof + classification + gate-authoring precondition for §09.2 (per decisions/11 L57 gate split + LEDGER D08/D09 + attempt-67 probe_gateable_surface_exhausted: true).

Context: §07A closed the standalone-ledger gap for NARROW shapes (move-alias / dup-alias / borrow-chain / collection-buffer-last-use / closure-capture / partial-move) and certified them green via an 11-probe ORI_DISABLE_PREDICATE_STACK_RC suite. The §09.2 execution (2026-06-04) empirically proved that gate is too narrow: under ORI_DISABLE_PREDICATE_STACK_RC=1 the FULL AOT corpus regresses 2344 pass / 16 fail → 1784 pass / 576 fail (+560) — the SAME failure shape as the 2026-06-03 attempt (2329/16 → 1300/1045). lower/burden_lower tracks only the whole-var collection result (burden_inc/dec %result) and DEFERS per-element / iterator-source / collection-element / matrix / SSO RC to the predicate stack. 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). The 11-probe suite never exercised these shapes, so the CH-comp proven-equivalence license (class_covered universal → coexistence_dispatch ≡ burden_emission_path ≡ predicate_stack_path) is FALSE for them: the predicate stack is NOT redundant on these shapes. This section completes the burden path so it IS. Cross-ref: decisions/LEDGER.md §B.2 + §B.3 2026-06-04 re-block lines; section-09-post-convergence-partial-retirement.md HISTORY 2026-06-04.

Downstream consumers: §09.2 is the direct consumer (its predicate-stack-retirement readiness gate consumes §07B’s strengthened corpus-under-flag SET-subset gate). §13 (Burden Verification Suite) is a SECOND downstream consumer: §13’s AST-probe conformance, burden SMT counterexample shapes, and dual-discharge proof-lean-map rows must absorb the broad-shape iterator / matrix / collection-element / SSO / generic burden-emission semantics — the burden path must be the sole RC emitter corpus-wide (§09.2’s deliverable, NOT §07B’s; §07B proves the probe-gateable subset self-sufficient + classifies the §09.2-territory residual + authors the gate-harness) before §13’s corpus-wide conformance cross-walk + VF-1 corpus gate assert against it. §13’s TOOLING-BUILD half depends_on §07B (the probe-gateable shape + classification + frozen-shape contract); its CORPUS-ASSERTION half depends_on §09 (the §09.2-activation that makes the burden path the corpus-wide sole emitter) per the 00-overview DAG.

Cross-plan coordination — plans/iterator-element-ownership: §07B’s custom iterator / collection-element burden lowering in burden_lower/mod.rs emits element-RC for collection elements. plans/iterator-element-ownership introduces owned-value tracking for iterator/collection elements; §07B’s element-RC emission MUST be forward-compatible with that plan’s owned-value model — the broad-shape element burden lowering is a temporary surface that owned-value tracking SUPERSEDES when elements become owned, NOT a parallel element-RC path that plans/iterator-element-ownership later has to unwind. §07B emits element decs through the standard burden ledger (BurdenDec at element last-use per RL-2), so the owned-value model replaces the lowering decision (which vars are owned) without forking the emission path.

Reference implementations: §07A (section-07A-burden-lowering-self-sufficiency.md) is the direct predecessor + the narrow-shape exemplar — its burden_lower move-alias / collection-buffer-last-use fixes are the pattern this section extends to the per-element / iterator / matrix / SSO surface. The proven calculus SSOT: RL-1/RL-2/RL-4/RL-5 + RL-comp (compiler_repo/aims-proof/proofs/08-realization/ + lean/AimsProof/Realization.lean), CH-1 (lean/AimsProof/Coexistence.lean). The protocol-builtin ownership table (arc.md §Protocol Builtins: Iter/IterNext/IterDrop/CollectSet) governs the iterator-lineage RC the burden path must emit.

Depends on: Section 07A — status: complete, reviewed: true (closed 2026-06-04). §07A delivered the narrow-shape standalone ledger; §07B extends it to the broad shapes. §07A in turn depends_on §07 (universal class_covered coverage-analysis).

Intelligence Reconnaissance

Queries (run at execution time — re-confirm residences before editing):

scripts/intel-query.sh --human file-symbols "compiler/ori_arc/src/lower/burden_lower/mod.rs" --repo ori — burden-lower emission entry points (graph-form repo-relative path; the compiler_repo/-prefixed form returns 0 from file-symbols)
scripts/intel-query.sh --human callers emit_burden_ops --repo ori
scripts/intel-query.sh --human similar elem_dec_fn --repo ori — the predicate-stack element-dec walk the burden path must replace for these shapes
scripts/intel-query.sh --human callers lower_burden_ops_to_rc --repo ori — the Phase-7 mechanical-flip site (emit_unified.rs:357)

Results summary [ori] (2026-06-04; grounded against current source via the §09.2 execution measurement + ORI_DUMP_AFTER_BURDEN):

Dominant deferral: [ori:compiler/ori_arc/src/lower/burden_lower/mod.rs] tracks only the whole-var collection result; per-element / iterator-source / nested-buffer / SSO-heap RC carries no burden ops.
Evidence: ORI_DUMP_AFTER_BURDEN=1 on a s.split(sep:",") repro shows burden_inc %result / burden_dec %result only — no per-element ops.
Predicate-stack element-dec walk currently supplying them: [ori:compiler/ori_arc/src/aims/emit_rc/dead_cleanup/mod.rs] (elem_dec_fn path).
Phase-7 mechanical-flip site the standalone ledger lowers through: [ori:compiler/ori_arc/src/aims/realize/emit_unified.rs] lower_burden_ops_to_rc.
Provenance: graph queries above are the at-execution recon protocol; this summary is the at-authoring grounding from the live §09.2 measurement.

07B.1 Iterator-from-collection + collection-element standalone burden ledger

The burden path must emit the iterator-lineage + per-element RC that the predicate stack’s elem_dec_fn walk currently supplies for iter() / __iter_next / collect-back chains and element-scope ops.

Localize the deferral: identify where lower/burden_lower emits the whole-var collection-result burden ops but omits the iterator-source / per-element lineage (the fat_ptr_iter / elem_dec_scope / collections_ext double-free path under the flag). DONE 2026-06-04: root cause = the burden walk emitted spurious last-use BurdenDec on BORROWED __iter_next.1 element views (RL-2 — borrowed values receive no dec); cure landed = exclude the collect_iter_element_defs SSOT set from owned_vars_needing_rc in emit_burden_ops (gated so default-path predicate-stack-ON stays byte-identical). Empirical: fat_ptr_iter 21/115 → 48/88 under the flag (+27); full corpus 1784/576 → 1843/517 (+59); zero new failing IDs vs the 16-baseline; ori_arc 1565/0 debug + 1561/0 release; §07A 11-probe 11/0 leak-clean; VF-1=0 on the for x in xs repro.
Emit the probe-gateable collection-SOURCE freeing RC via the M1 alloc-aware-net foundation: elide the self-allocating builtin collection-source Apply fresh-inc over-count (fresh_collection_source_apply_dst unioned into fresh_rc_alloc_dst → the M1 elision + alloc-aware net drops the spurious fresh inc when net==1 ∧ !cow_mutated; second fix: compute_cow_mutated_lineage_reps exempts read-only builtins from the callee_may_cow flag). DONE attempt-66 (compiler_repo/compiler/ori_arc/src/lower/burden_lower/emit.rs fresh_site_burden_inc_dst + compute_elidable_fresh_self_alloc_incs): under-flag 119→115 (4 FIXED, ZERO new); default-16 byte-identical; probe-gated. Calculus: pure case-(a) — Realization.lean RL1_emit_iff_not_elidable:122 + rcBalance already govern (Lean CORRECT, impl diverged; git diff aims-proof/ EMPTY).
CLASSIFY (§09.2-owned, NOT closed here): the iterator-HANDLE freeing BurdenDec (Iter Borrowed source / IterNext Owned iterator + Borrowed marker / IterDrop Owned / CollectSet Owned per arc.md §Protocol Builtins) + the fat_ptr_iter catch-block panic-edge JOINT (attempt-64/67, ~15-16 IDs) dissolve via §09.2 emit_burden_ops M-a callee transfer-source-dec strip — M-c-BANNED while the predicate stack coexists (attempt-55 broke default 16→61). Recorded in section-09-post-convergence-partial-retirement.md §09.2; verified at §09.2’s close-gate, not here. DONE 2026-06-06 (verify-first): the classification IS recorded in section-09 §09.2 checkbox-block (the “M-a callee transfer-source-dec strip + caller keep-alive-inc … for the generics forwarder transfer-through-return … + fat_ptr_iter iterator-handle/catch-panic-edge JOINTs” item) AND in the §09.N readiness verdict; this CLASSIFY checkbox’s deliverable (recording the residual as §09.2-owned with the §09.2 anchor) is satisfied.
CLASSIFY (§09.2-owned, NOT closed here): per-element freeing RC for collection-element scope lineages (the elem_dec_fn equivalent — elem_dec_scope/narrowing/for_yield_option per-element non-block-param dead-after-last-read, attempt-9/10/11 + attempt-67, ~12 IDs) is an IRREDUCIBLE per-CFG-path structural last-read (emit_dead_at_entry_decs, RL-2 LastReadBeforeScopeExit) with NO alloc-aware-net expression — a whole-var BurdenDec fires on ALL paths (double-free) or NONE (leak), never exactly-one-of-N-exits (the over-fire surface 459→596/642). Per the OVER-FIRE CAUTION the structural proxy is NOT built here; §09.2 Phase-5 faithful emit_dead_at_entry_decs with elem_dec_fn accounting owns it (M-c-coupled). DONE 2026-06-06 (verify-first): the classification IS recorded in section-09 §09.2 (“faithful per-element emit_dead_at_entry_decs with elem_dec_fn accounting … for the per-CFG-path structural last-read shapes (narrowing/for_yield_option/elem_dec_scope per-element …)”) AND in the §09.N readiness verdict; this CLASSIFY checkbox’s deliverable (recording the residual as §09.2-owned with the §09.2 anchor) is satisfied.
Tests (tests.md §Matrix Testing Rule): iterator-from-collection (for x in xs, .iter().map().collect()), collection-element scope — semantic pin (standalone ledger nets correct under the flag) + negative pin (revert → double-free under the flag); ORI_CHECK_LEAKS=1 zero-leak; eval+LLVM parity. Residences (per the §07A precedent): Rust unit pins for the iterator-handle / per-element burden-op emission shape in compiler_repo/compiler/ori_arc/src/lower/burden_lower/tests.rs; Ori spec behavioral pins under compiler_repo/tests/spec/ (iterator + collection-element shapes). DONE 2026-06-06 (verify-first, PROBE-GATEABLE SUBSET ONLY): the landed probe-gateable pins exist + cover the LANDED fixes — burden_lower/tests.rs carries iter_next_element_projection_gets_no_burden_dec + iter_next_element_let_alias_gets_no_burden_dec (attempt-66, the element-view exclusion shape, negative-direction verified); predicate_stack_probe.rs carries the iterator-from-collection / collection-element behavioral pins (probe_collection_buffer_last_use_*, the for_yield_* / nested-for keep-alive pins, the dead-collection-source freeing pins) + the attempt-66 probe_collect_* collection-source M1 pins. The §09.2-territory JOINT shapes’ behavioral pins (iterator-HANDLE / matrix / generic / per-element non-block-param) are NOT marked here — they land at §09.2 with the Phase-5 completion (they cannot pass on the burden path alone until §09).

Subsection close-out (07B.1) per protocol.

07B.2 Fat-pointer / nested-collection (matrix) + generic-instantiated standalone ledger

Land the probe-gateable nested-buffer freeing via the SHARED M2/M3 successor-edge-dec + per-path alloc-aware-net foundation (LEDGER D08): thread compute_lineage_alloc_aware_net across the Jump-arg → block-param SSA rename (the Cure-B phi-boundary the net currently excludes by design) for the nesting levels whose freeing dec IS alloc-aware-net-expressible. Calculus status: within Realization.lean rcBalance (impl-only, no Lean change). Concrete pin: a [[int]] outer-buffer + inner-element repro whose per-path net the threaded compute_lineage_alloc_aware_net balances, with comm -13 baseline⊆under-flag staying EMPTY. RECLASSIFIED 2026-06-06 (verify-first, NOT a fix-claim): the attempt-66/67 survey ground-truthed that NO probe-gateable nested-buffer freeing surface remains — the fat_matrix / iter_rc_matrix / rc_matrix nested clusters are per-CFG-path structural last-read JOINTs (the over-fire surface — whole-var BurdenDec all-paths/none, never exactly-one-of-N) with NO alloc-aware-net expression, i.e. §09-territory (Phase-5-coupled, M-c-banned). The one probe-gateable nested-source cure in that family (the rc_matrix loop-carried-CONSUME source, attempt-35) ALREADY landed via the shared emit_unified.rs consume-vs-borrow discriminator. Attempt-67 records probe_gateable_surface_exhausted: true: the M3 alloc-aware-net Jump-arg→block-param thread is NOT alloc-aware-net-expressible for the remaining nesting levels, so the threaded-net cure is NOT built here — the residual is the §09.2 Phase-5 faithful emit_dead_at_entry_decs work (cb2 below).
CLASSIFY (§09.2-owned, NOT closed here): the fat_matrix / iter_rc_matrix / rc_matrix per-CFG-path structural last-read JOINT (the over-fire surface — whole-var BurdenDec all-paths/none, never exactly-one-of-N) + the generics forwarder transfer-through-return JOINT (attempt-54/55/64, ~20 IDs — M-a callee transfer-source-dec strip, Phase-5/M-c-banned) + the recursive-aggregate-in-variant JOINT (recursive_feature/derive, ~5 IDs, attempt-65) dissolve via §09.2 Phase-5 burden-emission completion, NOT a §07B probe-tail change. The buffer-provenance distinction (fresh-copy clone vs buffer-sharing slice/substring/COW-push) is a ParamContract/ReturnContract field extension (LEDGER D08 Cure-A, Invariant-5 (b)) GROUND-FIRST per arc.md §CP-1 — recorded for §09.2, not patched here. DONE 2026-06-06 (verify-first): the classification IS recorded in section-09 §09.2 — the M-a callee-strip item (generics forwarder + fat_ptr_iter), the faithful per-element emit_dead_at_entry_decs item (fat_matrix/iter_rc_matrix/rc_matrix per-path), and the dead-vs-survives + buffer-provenance ParamContract/ReturnContract field item (GROUND-FIRST per arc.md §CP-1) — plus the §09.N readiness verdict. This CLASSIFY checkbox’s deliverable (recording each residual cluster → its §09.2-owned Phase-5 mechanism with the §09.2 anchor) is satisfied.
Tests (probe-gateable subset only): the nested-buffer alloc-aware-net repro above — Rust unit pin for the per-path-net emission shape in compiler_repo/compiler/ori_arc/src/lower/burden_lower/tests.rs (semantic pin: threaded net balances; negative pin: revert the SSA-rename threading → leak re-appears under the flag); ORI_CHECK_LEAKS=1 zero-leak; eval+LLVM parity. The matrix / generic-instantiation JOINT shapes’ behavioral pins land at §09.2 with the Phase-5 completion (they cannot pass on the burden path alone until then). DONE 2026-06-06 (verify-first, follows cb1’s exhaustion reclassification): cb1 ground-truthed that NO probe-gateable nested-buffer alloc-aware-net repro remains (the threaded-net cure is NOT alloc-aware-net-expressible for the residual levels → not built), so there is no new threaded-net pin to author here. The ONE probe-gateable nested-source cure that landed in this family (the rc_matrix loop-carried-CONSUME source, attempt-35) carries its pins in predicate_stack_probe.rs — 6 positive (probe_loop_carried_{push_list_int,push_list_str,insert_map,concat_str,push_while,push_break}_source_no_double_free) + 2 NEGATIVE clamps (probe_loop_invariant_{closure_borrow,map_index_borrow}_no_premature_free_negative, the consume-vs-borrow over-fire guard). The matrix / generic / recursive-aggregate JOINT shapes’ behavioral pins land at §09.2 with the Phase-5 completion (not passable on the burden path alone until §09).

Subsection close-out (07B.2) per protocol.

07B.3 SSO-string standalone burden ledger

Confirm the burden path emits the standard String burden ledger for ALL probe-gateable String lineages (string_sso) at lowering with NO SSO-state-dependent suppression — burden_lower emits BurdenInc/BurdenDec for every String var the same way regardless of SSO state (it cannot statically know inline vs heap-backed; the inline-SSO no-RC behavior is a RUNTIME dynamic-bypass property of the RcInc/RcDec helpers, which no-op on inline ≤23-byte strings, NOT a compile-time omission). Verify via ORI_DUMP_AFTER_BURDEN on a heap-backed SSO multi-ref repro that the freeing BurdenDec is emitted at last-use (RL-2 lowered to a real RcDec); inline SSO reaches the same RcDec which dynamically no-ops. Probe-gateable subset only — no leak / double-free under burden-as-sole-emitter for the non-JOINT case. DONE 2026-06-06 (verify-first, CONFIRM — no fix, the burden path already emits it): ORI_DUMP_AFTER_BURDEN on a heap-backed (>23-byte) SSO multi-ref repro (let s = "<heap>"; let a = s; a.length() + s.length()) emits the standard String ledger burden_inc %0 (RL-1 dup of the live-source alias) + burden_dec %0 (RL-2 release at last-use), and the IDENTICAL shape on an inline (≤23-byte) string — no SSO-state-dependent suppression at lowering. The heap repro runs leak-free (exit 0) under ORI_DISABLE_PREDICATE_STACK_RC=1 (burden path as sole emitter). The behavioral pin is the §07A probe_dup_alias_live_source_str (the heap-str dup-alias-live-source shape, green in the 11-probe suite).
CLASSIFY (§09.2-owned, NOT closed here): the string_sso heap-clone buffer-provenance (a.clone() distinct buffer) + COW-concat JOINT residual (attempt-66/67, confirmed JOINT/Phase-5-coupled by source — the load-bearing inc a COW-shared value needs vs a fresh-copy result, the LEDGER D08 Cure-A buffer-provenance class) dissolves via §09.2 Phase-5 completion + the ParamContract/ReturnContract buffer-provenance field (GROUND-FIRST per arc.md §CP-1), NOT a §07B probe-tail change. DONE 2026-06-06 (verify-first): the classification IS recorded in section-09 §09.2 — the dead-vs-survives-after-concat + COW-shared-survives liveness item names string_sso among the Phase-5-coupled shapes and ties the cure to the LEDGER D08 Cure-A buffer-provenance ParamContract/ReturnContract field (clone vs slice/substring/COW-push, GROUND-FIRST per arc.md §CP-1) — plus the §09.N readiness verdict. This CLASSIFY checkbox’s deliverable (recording the heap-clone / COW-concat residual as §09.2-owned with the §09.2 anchor) is satisfied.
Tests (probe-gateable subset only): SSO heap multi-ref (non-clone, non-COW-concat) — semantic pin (standard String ledger emitted, freeing BurdenDec at last-use) + negative pin (assert no SSO-state-dependent suppression at lowering); leak-free; parity. Residence: Rust unit pin for the standard-String-ledger burden-op emission shape in compiler_repo/compiler/ori_arc/src/lower/burden_lower/tests.rs. The clone / COW-concat JOINT behavioral pins land at §09.2 with the Phase-5 completion. DONE 2026-06-06 (verify-first; cb1 is a CONFIRM-no-fix, so the probe-gateable SSO heap multi-ref behavioral pin is the standing probe_dup_alias_live_source_str (§07A 11-probe suite, green) which exercises the exact heap-str dup-alias-live-source standard-String-ledger shape under the flag, plus probe_heap_str_same_root_multi_compare_no_double_free_negative as the multi-ref clamp. Because cb1 lands NO new lowering change (the burden path already emits the standard ledger uniformly), no NEW burden_lower/tests.rs unit pin is required — the cb1 ORI_DUMP_AFTER_BURDEN confirmation + the green behavioral probe are the verification. The clone / COW-concat JOINT behavioral pins land at §09.2 with the Phase-5 completion.

Subsection close-out (07B.3) per protocol.

07B.4 Strengthened readiness gate (full-corpus-under-flag) + matrix tests

The §07A narrow 11-probe gate is the recurring under-coverage root cause. This subsection REPLACES the §09.2-readiness signal with the full AOT corpus under the flag and lands the cross-shape matrix.

Baseline failing-ID SET — SSOT is the checked-in fixture compiler_repo/compiler/ori_llvm/tests/aot/fixtures/corpus_under_flag_gate/baseline_failing_ids.txt (RE-CAPTURED to the gated burden-default failing-ID set per the §09.2 2026-06-09 metric redefinition; the gate asserts failing_ids_under_flag ⊆ fixture). The enumeration below is the HISTORICAL 2026-06-04 16-ID capture (predicate stack ON, no-valgrind) retained for the §09-coupled-cohort identification only — the live fixture wins on any divergence: aims_burden_alias::test_burden_alias_inner_survives_result_destructure, aims_interactions::test_h12_rc_merge_preserves_rc_ops, borrow_independence::test_borrow_separate_heap_types, for_yield_option::test_for_yield_option_str_conditional_break, for_yield_option::test_for_yield_option_str_conditional_continue_value, generics::test_borrow_list_int_nested_pin6_chain_then_return_no_leak, generics::test_edge_project_return_not_param_keeps_outer_dec, generics::test_generic_forwarder_option_list_returns_intact, generics::test_generic_forwarder_result_list_str_returns_intact, generics::test_path_sensitive_triple_list_balances_rc_on_all_three_paths, higher_order::test_hof_closure_capture_in_loop, higher_order::test_hof_make_predicate, match_alias::test_match_arm_alias_result_str, match_alias::test_option_intlist_select_branch_return, match_alias::test_unwind_path_alias, tagless_enum::tagless_enum_list_payload_reads_and_drops. These are the §09-coupled cohort (BUG-04-118 + BUG-04-123 predicate-stack residuals) that dissolve at §09 retirement — they stay IN the baseline set (§09/§12-owned); the §07B.4 gate forbids only ADDITIONS. The §07B.4 close-out codifies this list as a checked-in fixture the gate test reads. (Note: a valgrind-present environment surfaces 2 additional flaky names — drop_augment::drop_recoverable_panic_path_no_leak_under_valgrind, the generics::test_generic_forwarder_result_list_str valgrind variant — NOT in this canonical no-valgrind baseline.)

Author the gate-test harness + capture the baseline-16 as a checked-in fixture: REPLACE the §09.2-readiness signal (from the narrow 11-probe suite to the FULL AOT corpus under ORI_DISABLE_PREDICATE_STACK_RC=1, asserted as a failing-test-ID-SET subset failing_ids_under_flag ⊆ baseline_failing_ids, NOT a count). Add a concrete checked-in gate test (a #[test] in a corpus-under-flag harness file alongside compiler_repo/compiler/ori_llvm/tests/aot/predicate_stack_probe.rs, at least as concrete as that probe file) that: (a) reads the baseline failing-ID SET from a checked-in fixture file under compiler_repo/compiler/ori_llvm/tests/aot/ (the 16 canonical no-valgrind names enumerated in the §07B.4 prose below — codified AS the fixture, NOT left in plan-prose), (b) runs the corpus under ORI_DISABLE_PREDICATE_STACK_RC=1, (c) asserts the under-flag failing-ID set adds no ID outside the baseline set. Include a re-capture protocol comment in the fixture: any predicate-stack-emission change re-captures the baseline (predicate-stack-ON cargo test -p ori_llvm --test aot) before trusting the subset assertion. The 11 probes stay as narrow-shape regression pins but no longer SUBSTITUTE for the corpus gate. §07B.4 owns the LEFT operand (the fixture) + the harness; the PASS VERDICT is §09.2’s. DONE 2026-06-06: authored compiler_repo/compiler/ori_llvm/tests/aot/fixtures/corpus_under_flag_gate/baseline_failing_ids.txt (the 16 canonical no-valgrind names codified AS the fixture, with the re-capture-protocol comment) + compiler_repo/compiler/ori_llvm/tests/aot/corpus_under_flag_gate.rs (wired into aot/main.rs). The harness has (i) the live-corpus SET-subset gate test #[ignore = "Spec: Annex E §AIMS — ... PASS after predicate-stack retirement + BurdenInc→RcInc activation"] (ignored, not red-by-default, since under-flag 115 ⊄ 16 today; re-execs the aot binary under the flag, parses ... FAILED IDs, asserts ⊆ baseline) AND (ii) 4 NON-ignored harness-logic unit tests that green-test the fixture parser + the SET-subset helper on synthetic inputs (including the swapped-in-failure-at-equal-count case the count-only check would mask) + the libtest-output FAILED-ID parser. Verified: cargo test -p ori_llvm --test aot -- corpus_under_flag_gate:: → 4 passed, 1 ignored, 0 failed; clippy clean; prose-lint clean; no wrapper-private leak.
Confirm the existing §07A 11 probes stay GREEN under ORI_CHECK_LEAKS=1 (no narrow-shape regression). DONE 2026-06-06: cargo test -p ori_llvm --test aot over the 11 §07A narrow probes (probe_move_alias_chain_str / probe_dup_alias_live_source_str / probe_collection_buffer_last_use_{list,map,set} / probe_borrow_chain_project_of_projection / probe_closure_capture_last_use_str / probe_result_str_partial_move_via_try_codegen_clean / probe_result_scalar_only_no_partial_move_codegen_clean / probe_coalesce_discards_heap_err_payload / probe_default_path_unaffected_str) → 11 passed; 0 failed (leak-clean under the run-step ORI_CHECK_LEAKS=1).
Probe-gateable under-flag progress pin: confirm the under-flag corpus is at 115 failing via the landed alloc-aware-net foundation with comm -13 baseline⊆under-flag EMPTY (zero new IDs vs the 16-baseline at the attempt-67 floor); probe_gateable_surface_exhausted: true recorded (HISTORY). The strict failing_ids_under_flag ⊆ baseline_failing_ids PASS VERDICT over the FULL corpus + VF-1=0 corpus-wide is DEFERRED to §09.2’s close-gate (section-09-post-convergence-partial-retirement.md §09.2 — §09.2 re-captures predicate-stack-ON on its own working tree, then asserts the subset after the BurdenInc→RcInc activation + Phase-5 completion dissolve the residual 115); it is unreachable at §07B (the residual is M-c-coupled until §09 retires the predicate stack). NOT a §07B deliverable, NOT a deferral-without-anchor: the verdict’s owning checkbox is section-09 §09.2 “§09.2 activation close-gate”. DONE 2026-06-06 (verify-first): the under-flag floor 115 + comm -13 baseline⊆under-flag EMPTY (zero new IDs vs the 16-baseline) + probe_gateable_surface_exhausted: true are recorded in the §07B HISTORY (attempt-66 drove 119→115 with ZERO new; attempt-67 re-scan ground-truthed the genuinely-clean M1-collection-source surface EXHAUSTED, NO clean alloc-aware-net-expressible probe-gateable leaf remaining, and recorded the probe_gateable_surface_exhausted boundary). The strict ⊆16 PASS VERDICT stays §09.2’s close-gate per cb anchor (section-09 §09.2).
Tests (probe-gateable subset only): the cross-shape matrix for the LANDED probe-gateable fixes (collection-source M1 elision + nested-buffer alloc-aware-net) lands with semantic + negative pins per tests.md §Matrix Testing Rule in compiler_repo/compiler/ori_arc/src/lower/burden_lower/tests.rs. The JOINT iterator-handle / matrix / generic / per-element / SSO-clone shapes’ behavioral pins land at §09.2 with the Phase-5 completion (classified above, not passable on the burden path alone until §09). DONE 2026-06-06 (verify-first, LANDED probe-gateable subset): the collection-source M1 elision (attempt-66) carries its matrix pins in predicate_stack_probe.rs — probe_collect_set_result_multibranch_dead_freed + probe_collect_list_result_multibranch_dead_freed (POSITIVE, leaked pre-cure) + probe_collect_result_duplicated_not_double_freed_negative (CRITICAL NEGATIVE clamp — a duplicated .collect() result’s fresh inc is load-bearing, the net != 1 gate keeps it) + probe_collect_result_straightline_dead_already_balanced_sibling. The other LANDED probe-gateable fix in this family (the rc_matrix loop-carried-CONSUME source, attempt-35) carries its 6 positive + 2 negative pins (cited in 07B.2 cb3). The nested-buffer alloc-aware-net cure was NOT landed (07B.2 cb1 reclassified the nested-buffer surface as §09-territory / exhausted), so no nested-buffer threaded-net pin exists. The JOINT iterator-handle / matrix / generic / per-element / SSO-clone shapes’ behavioral pins land at §09.2.
TPR checkpoint — /tpr-review covering 07B.1-07B.4. DONE 2026-06-06: ran as part of the §07B RE-SCOPE /review-plan (verdict SIGNIFICANT REWORK APPLIED) — /tpr-review converged in-cap over 2 rounds (round 1: 5 actionable residual-COMPLETE-ledger-language findings cured; round 2: 4 actionable residual cured; 9 resolved, 0 deferred; post-cure grep zero residual mis-attributions; plan_corpus check clean apart from pre-existing decisions-path warnings). Cross-ref: the §07B HISTORY 2026-06-06 RE-SCOPED entry + the /review-plan verdict.

Subsection close-out (07B.4) per protocol.

07B.R Third Party Review Findings

None.

07B.N Completion Checklist

Probe-gateable iterator-from-collection + collection-source self-sufficiency PROVEN via the M1 alloc-aware-net foundation (07B.1); the iterator-handle / catch / per-element JOINT residual CLASSIFIED as §09.2-owned. (07B.1 cb1/cb2 landed; cb3/cb4 CLASSIFY recorded in section-09 §09.2; cb5 probe-gateable pins exist.)
Probe-gateable nested-buffer freeing landed via the M2/M3 successor-edge-dec + per-path alloc-aware-net (07B.2); the matrix / generics-forwarder / recursive-aggregate JOINT residual CLASSIFIED as §09.2-owned. (07B.2 cb1 RECLASSIFIED 2026-06-06 verify-first: NO probe-gateable nested-buffer freeing surface remains — the fat_matrix/iter_rc_matrix/rc_matrix nested clusters are per-CFG-path structural last-read JOINTs with no alloc-aware-net expression, i.e. §09-territory; the one probe-gateable nested-source cure that landed is the rc_matrix loop-carried-CONSUME source via the shared emit_unified.rs discriminator; cb2 CLASSIFY recorded in section-09 §09.2.)
SSO-string standard-ledger emission confirmed for the probe-gateable case (07B.3); the heap-clone / COW-concat buffer-provenance JOINT residual CLASSIFIED as §09.2-owned. (07B.3 cb1 confirmed via ORI_DUMP_AFTER_BURDEN — heap + inline emit the identical burden_inc/burden_dec ledger, no SSO-state suppression, heap repro leak-free under the flag; cb2 CLASSIFY recorded in section-09 §09.2.)
Readiness gate HARNESS authored + baseline-16 captured as a checked-in fixture (07B.4): full-corpus-under-ORI_DISABLE_PREDICATE_STACK_RC=1 failing-ID-SET-subset gate test alongside predicate_stack_probe.rs replaces the narrow 11-probe gate; the 11 probes stay green as narrow-shape regression pins. The PASS VERDICT is routed to §09.2. (Authored corpus_under_flag_gate.rs + fixtures/corpus_under_flag_gate/baseline_failing_ids.txt; 4 harness-logic unit tests pass + 1 §-anchored ignored live-corpus gate test; 11 probes green.)
Probe-gateable under-flag floor confirmed at 115 with comm -13 baseline⊆under-flag EMPTY (zero new IDs); probe_gateable_surface_exhausted: true recorded. The strict ⊆16 PASS VERDICT + VF-1=0 corpus-wide + ORI_CHECK_LEAKS=1 zero-leak over the FULL corpus is §09.2’s close-gate (section-09 §09.2), NOT a §07B item. (Recorded in the §07B HISTORY attempt-66/67; the ⊆16 PASS VERDICT routed to §09.2 per anchor.)
§07B-achievable test gate — landed probe-gateable work passes its pins (corpus_under_flag_gate harness units 4 green + 1 anchored-ignored live gate; 11 probes green under ORI_CHECK_LEAKS=1; attempt-66/35/37 pins green; comm -13 baseline⊆under-flag EMPTY at the under-flag-115 floor; ori_arc green debug+release). Residual = a known-state cache refresh ONLY (state.sh refresh against committed HEAD per state-discipline.md §6) + the reviewed:true flip — full derivation in HISTORY 2026-06-11 (test-gate residual). Full-corpus-green is owned by section-09 §09.2 + 00-overview.md → §10/§12 (anchored, not deferred).
OBE — frozen-shape versioning superseded by §09.2’s metric redefinition. The attempt-67 frozen probe-gateable shape this item would version (under-flag-115 floor, baseline-16 fixture at HEAD 9e53362ea) was overtaken by the §09.2 2026-06-08/09 burden-default flip + canonical-metric redefinition (section-09 §09.2 HISTORY 2026-06-09): the compiler_repo/compiler/ori_llvm/tests/aot/fixtures/corpus_under_flag_gate/baseline_failing_ids.txt fixture was RE-CAPTURED to the gated burden-default failing-ID SET, so the under-flag-115 / baseline-16 identity no longer exists in-tree to freeze. The §07B→§13 TOOLING-BUILD contract binds the CURRENT fixture (the artifact §13’s tooling-build half reads); the binding edge is section-13 depends_on: [07B, 09] per the 00-overview DAG, with §09 owning the live fixture’s frozen identity at activation.
Plan annotation cleanup.
Plan sync per protocol.

HISTORY

2026-06-11 — test-gate residual derivation (lifted from the §07B.N checkbox per STRUCTURE:matrix-as-checklist). The cross-scope compiler cures the gate awaited (attempt-66 element-view exclusion + collection-source M1 elision, attempt-35 consume-vs-borrow split, attempt-37 forwarder alloc-aware-net) are COMMITTED (HEAD advanced past 9e53362ea via the §09.2 burden-default flip + 2026-06-09 metric recapture), so the 2026-06-06 “uncommitted cures await cache_refresh” premise is OBE. Body conditions are empirically GREEN at the attempt-67 floor; the unchecked state reflects ONLY the stale known-state cache. The FULL-corpus zero-failures VERDICT is unreachable at §07B by construction (the 16-baseline §09-coupled cohort — BUG-04-118/123/121 predicate-stack residuals — dissolves only at the §09.2 activation) and is owned by §09.2 + overview → §10/§12.
2026-06-04 — §07B created (via /create-plan —inline; routing.md §3 case c) as the TRUE §09.2 predicate-stack-retirement precondition. The §09.2 execution empirically proved §07A’s self-sufficiency is INCOMPLETE corpus-wide: under ORI_DISABLE_PREDICATE_STACK_RC=1 the FULL AOT corpus regresses 2344/16 → 1784/576 (+560), because lower/burden_lower defers iterator-from-collection / fat-pointer-matrix / iter-RC-chain / collection-element / SSO RC to the predicate stack — shapes the §07A 11-probe gate never covered (scoped confirm: fat_ptr_iter 136/0 → 21/115). §07A stays complete for its narrow shapes; §07B completes the broad-shape remainder AND replaces the narrow-probe readiness gate with the full-corpus-under-flag gate (narrow-probe certification is the recurring under-coverage root cause). Sequenced §07A → §07B → §09 (§07B depends_on: [07A]); §09 + §13 re-home their dependency onto §07B (the burden path is the sole RC emitter only after §07B). Cross-ref: decisions/LEDGER.md §B.2 + §B.3 2026-06-04 re-block lines; §09 HISTORY 2026-06-04.
2026-06-04 — §07B.1 checkbox 1 (localize + element-view fix) LANDED; checkboxes 2/3 collection-source freeing characterized + anchored. The borrowed iterator-element-view double-free is cured: emit_burden_ops excludes collect_iter_element_defs (the predicate-stack SSOT) from owned_vars_needing_rc, gated so default-path (predicate-stack-ON) AOT codegen is byte-identical. Empirical under ORI_DISABLE_PREDICATE_STACK_RC=1: fat_ptr_iter 21/115 → 48/88 (+27); full corpus 1784/576 → 1843/517 (+59); zero new failing IDs vs the 16-baseline; ori_arc 1565/0 debug + 1561/0 release; §07A 11-probe 11/0 leak-clean. Files: burden_lower/mod.rs (interner thread + exclusion), pipeline/aims_pipeline/mod.rs + burden_lattice_smoke.rs (call-site interner), burden_lower/tests.rs (2 TDD pins: iter_next_element_projection_gets_no_burden_dec + iter_next_element_let_alias_gets_no_burden_dec, negative-direction verified). REMAINING (checkboxes 2/3, the residual 88 fat_ptr_iter + 26 elem_dec_scope + 26 collections_ext = 140 under the flag). CORRECTED CHARACTERIZATION (2026-06-04, empirically re-measured via ORI_TRACE_RC on the scope clusters — SUPERSEDES the VF-1-Jump-arg-rename characterization, which was empirically refuted): the dominant residual is TWO mechanisms, NEITHER a VF-1 compute_burden_entry_nets extension (VF-1 reports net=0 / exit 0 on the leaking + double-freeing repros — these are RC-net-on-the-allocation defects INVISIBLE to per-ArcVarId VF-1). (M1) FRESH-allocation BurdenInc over-count under Phase-7 mechanical lowering (dominant collections_ext/fat_ptr_iter LEAK): a self-allocating Construct List/Map (rc=1 at alloc) that is dup-aliased N times (used ≥2×, e.g. [10,20,30] indexed at [0] and [2] across two blocks) emits 1 FRESH inc + N dup-alias incs vs N dup decs + 1 self dec, plus the alloc’s +1 = net +1 leak of the container (ORI_TRACE_RC: alloc rc=1 → final rc=1, “1 RC allocation not freed”). Single-use/move-alias values net 0 (the FRESH inc balances the move-alias extra dec) — why §07A’s narrow probes passed (never exercised multi-dup-alias collection-source). (M2) Borrowed-Invoke-terminator-arg BurdenDec misplacement (the map_keys/map_values/set_to_list DOUBLE-FREE): a collection borrowed into an Invoke @keys/@len/@values terminator whose last-use IS that terminator gets its BurdenDec emitted INLINE before the terminator (emit_terminator_burden_decs, because under the probe invoke_terminator_borrowed_args is forced empty at emit.rs:122-127) → the map is freed (running elem_dec_fn on key strings) BEFORE @keys borrows it → ori_map_keys_to_list resurrects freed strings → keys-list drop double-frees (ORI_TRACE_RC: dec→0 FREE, then inc on freed ptr, then dec→0 FREE again → tcache double-free). The dec belongs on the NORMAL SUCCESSOR EDGE, via the completeness pass emit_burden_scope_exit_decs REFERENCED at emit.rs:616 but NEVER IMPLEMENTED (zero definitions; a dead reference defect). HARD CONSTRAINTS for the cure (both empirically runnable now, NOT §07B.4-gated): default-path (predicate-stack-ON) AOT corpus byte-identical + §06 corpus-wide VF-1 net=0 intact. PREREQUISITE discovered: §07B.4’s baseline failing-ID SET is unrecorded (only count “16”; live default count is 19 — 2 valgrind-flaky drop_augment::drop_recoverable_panic_path_no_leak_under_valgrind + generics::test_generic_forwarder_result_list_str_returns_intact absent under the flag); the SET must be captured before the subset assertion (M1/M2 cure validation + §07B.4 gate) can be authored. Cross-ref: decisions/LEDGER.md §B.2 2026-06-04 §07B.1 lines.
2026-06-04 — Attempt 9: checkbox-2/3 residual PRECISELY split into TWO sub-shapes (UAF + leak) with DIFFERENT roots; both fixes built, validated-on-target, REVERTED (guardrail-2). Ground-truthed via ORI_TRACE_RC/ORI_DUMP_AFTER_BURDEN on the real failing repros under the flag. (A) USE-AFTER-FREE (coll_list_clone_int SIGSEGV; collections_ext clone/length/index/contains): a self-alloc list move-aliased then passed at a BORROWED Invoke @clone([borrow]) terminator gets its freeing BurdenDec emitted INLINE before the terminator (emit.rs:128-133 forces terminator_borrowed_args empty under the probe) → buffer freed before the callee borrows it. (B) LEAK (map_keys_str/str_split/map_values conversion; elem_dec_scope map-iteration): the collection receiver flows as a loop Jump-arg into a dead-at-entry post-loop block param never freed — default path frees it via emit_dead_at_entry_decs (RL-5), the probe tail runs only edge cleanup (catches multi-succ dying edges, NOT single-succ dead-block-params). FIX-A (relocate borrowed-arg dec to successor edge via compute_invoke_edge_dead_set cat-2 + carries_burden seed): fixed coll_list_clone_int, REGRESSED 459→454 with 32 NEW IDs (slices/wrapper_rc_retain/match_alias/structs) — over-fires where the borrowed value’s payload escapes into the call result (the inline dec was correct there; relocation NOT universally sound — confirms the §06.1 M2 hazard). FIX-B (BlockCtx.burden_only flag + probe-tail emit_burden_dead_at_entry reusing emit_dead_at_entry_decs): fixed map_keys_str/str_split, REGRESSED 459→596 with ~137 NEW IDs (entire iter_rc_matrix/fat_ptr_iter for-loop/ir_quality_attributes clusters) — the predicate-stack dead-cleanup double-frees for-loop iterator/element block params the burden walk already handles via iter-element-view exclusion + ori_iter_drop. BOTH reverted by re-Editing to the EXACT attempts-7+8 foundation (verified: under-flag comm -13+comm -23 vs 459 BOTH empty; default-path comm vs 16 BOTH empty; ori_arc 1570/0; no Lean/test/gate weakened; no git checkout/restore/reset). Checkboxes 2/3 stay UNCHECKED (PARTIAL). NEXT LEAF: (A) the edge-relocation needs an ESCAPE discriminator — relocate ONLY when the borrowed value’s payload does NOT escape into the call result (clone/len/contains safe; unwrap/slice/take/match-alias keep inline); (B) the dead-block-param leak needs a SEED-not-reuse approach — emit the RL-5 dead-block-param BurdenDec ONLY for an owned, non-iter-element, non-ori_iter_drop-managed collection block param dead at entry, excluding collect_iter_element_defs + iterator handles, so it does not double-free the for-loop clusters. Both must re-prove comm -13 EMPTY before keeping. Cross-ref: decisions/LEDGER.md §B.2 attempt-9 line.
2026-06-04 — M1+M2 cure implemented + empirically validated on-target, but BOTH revert (guardrail-2 regressions); triple-confirmed PLAN-RESTRUCTURE signal. Three deep implementation passes engaged checkbox-2/3. The third implemented both mechanisms (no parallel emission path — extended the burden path per arc.md Invariant 5), confirmed each FIXES its target (M1: coll_list_index/coll_map_contains_key leak→clean; M2: map_keys/map_values/set_str_union/closure-capture double-free→clean, under-flag 517→471 −46, collections_ext 26→21, elem_dec_scope 26→22), but each introduced a NEW failure outside the 16-baseline → reverted to the clean checkbox-1 baseline (guardrail-2: zero new failing IDs). M1 BLOCKER: the “spurious FRESH-inc” condition is NOT capturable by the self-alloc ∧ ¬move-alias-source heuristic — splicing the FRESH-site BurdenInc (so the allocation’s own rc=1 isn’t double-counted under Phase-7 lowering) LEAKS cow/concat/sort patterns (coll_list_cow_concat_shared: a load-bearing FRESH inc on a CollectionReuse/concat result gets wrongly spliced). The SOUND condition needs per-allocation runtime-RC-net reasoning — thread VF-1 burden_delta per-var nets into the Phase-7 lower_burden_ops_to_rc splice decision (does the lowered ledger net 0 against the allocation’s implicit +1?) — a Phase-7-accounting rework, NOT iterator-specific. M2 BLOCKER: the successor-edge dec relocation (the now-implemented emit_burden_scope_exit_decs pass) cured the pure scope-drop shapes but moved fat_ptr_iter 88→89 — the compound iterator-conversion CFG shapes (fat_ptr_iter::conversion::{map_keys_str,map_values_str,set_to_list_str}) straddle §07B.1 (collection-element) AND §07B.2 (fat-pointer-conversion); M2 only cures the simple scope-drop shapes. PLAN-RESTRUCTURE SIGNAL (triple-confirmed): §07B’s subsection decomposition (07B.1 iterator/element ∥ 07B.2 matrix/generic) does NOT partition the cure surface — the collection-source FRESH-inc-net accounting (M1) is a SHARED Phase-7 foundation all broad shapes need, and the iterator-conversion shapes straddle 07B.1/07B.2. The architecturally-correct next move (per the standing directive’s “/create-plan —inline to expand/restructure as needed”): extract a SHARED foundational subsection — Phase-7 standalone-ledger per-allocation-net accounting (VF-1 burden_delta → lower_burden_ops_to_rc thread) — that 07B.1/07B.2/07B.3 depend on, rather than each re-deriving it. No code landed beyond checkbox-1 (clean revert verified: cargo check clean, ori_arc 1565/0 debug + 1561/0 release, default-path = exactly the 16-baseline). Cross-ref: decisions/LEDGER.md §B.2 2026-06-04 M1/M2-revert line.
2026-06-05 — Attempt 34: rc_matrix loop-carried-reassignment SOURCE double-free root-caused (fresh-inc elision-split on the back-edge-split lineage net); pair-elide cure built + REVERTED (over-fired on loop-invariant Jump-transferred values). Ground-truthed ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN/ORI_DUMP_AFTER_BURDEN_ELIM + ORI_TRACE_RC + per-(phase,block) binc/bdec on matrix_list_int_for_loop. ROOT: the loop-carried source (xs = xs.push(i) / s = s + "x" / m = m.insert(..)) is a FRESH self-alloc in the loop-init block (bb0) with a same-site net-0 [burden_inc %X, burden_dec %X] pair, transferred into the loop via the loop-entry Jump bb1(.., %X) arg (RL-4). compute_same_alloc_reps excludes the Jump-arg→block-param rename (back-edge split), so compute_lineage_alloc_aware_net for %X’s rep mis-computes +1 → compute_elidable_fresh_self_alloc_incs mis-elides the fresh inc → Phase-7 lower_burden_ops_to_rc lowers burden_inc %X to a no-op MARKER but lowers the paired burden_dec %X to a real RcDec %X, stranding [dec] (net −1) → the source frees before the loop reads it (double-free; struct/str leak). Confirmed identical bb0 split across list_int/list_str/map/str × {for/while/break}; oracle jumps %X in with ZERO bb0 RC. CALCULUS: pure case-(a) impl-conformance — Realization.lean RL1_duplication_balanced + RL3_elision_net_preserving ALREADY mandate atomic-pair elision ([inc,dec] OR [], never [dec]); the impl diverges; NO .lean/.proof/rule edit. The pair-elide cure (elide the paired same-block dec when its var is Jump-arg-transferred out) fixed list_int/list_str/map but OVER-FIRED: under-flag 251→243 with 3 NEW failures (hof_closure_capture_in_loop + coll_map_index_in_loop + phase_c_push_corruption_guard) — a loop-INVARIANT closure-env / read-only map is ALSO Jump-arg-transferred with the IDENTICAL bb0 shape but its bb0 dec is its GENUINE scope-exit release (borrowed-read-only, never consumed in-loop). The bb0-shape + Jump-transfer discriminator cannot separate loop-carried-CONSUME from loop-invariant-BORROW; only the whole-chain consume-vs-borrow net distinguishes them. REVERTED clean by re-Editing (no git checkout/restore/reset/stash); post-revert: default SET = base16 EXACT, under-flag SET = base251 EXACT (both comm EMPTY), ori_arc 1610/0 debug, predicate_stack_probe 96/96 (concurrent attempt-33’s pins intact), git diff carries zero attempt-34 markers, calculus untouched. NEXT LEAF: CONSUME-AWARE net correction — extend compute_phi_threaded_alloc_reps (currently ori_list_take-only eligible) to the loop-carried fresh source so its whole-chain net counts the in-loop [own]-consume as the release (net 0 → both bb0 halves lower to a harmless net-0 pair) while the loop-invariant value stays net +1 (inc elided, bb0 dec genuine); the str concat-loop old-string release is a sibling sub-leaf. The recurring loop-carried / JOINT keep-alive class (attempts 9/11/12/13/22/25/27/30 + concurrent-33 coll_list_push_loop_1000). §07B.1 checkbox 2 stays UNCHECKED (PARTIAL). Cross-ref: decisions/LEDGER.md §B.2 attempt-34 line.
2026-06-05 — Attempt 35: rc_matrix loop-carried-reassignment SOURCE double-free CURED + KEPT (the attempt-34 NEXT LEAF, guardrail-clean); 11 fixed, ZERO new, under-flag 251→240. A NEW permanent diagnostic (ORI_LOG=ori_arc::aims::realize=trace “fresh-self-alloc inc-elision decision” in compute_elidable_fresh_self_alloc_incs, emitting per-fresh-alloc dst / rep / lineage_net / cow_mutated / elidable) PROVED the attempt-34 net-framing cannot discriminate: the double-freeing rc_matrix %3 and the correctly-passing loop-invariant hof_closure %2 both emit the IDENTICAL lineage_net=1 cow_mutated=false elidable=true verdict. The actual discriminator is the COW-flag. CURE: split compute_cow_mutated_lineage_reps’s consume detection into consumed_owned (owned-position value-mutation + Add-concat — a GENUINE in-loop CONSUME, resolved to same-alloc reps THROUGH compute_phi_threaded_alloc_reps’s FORWARD Jump-arg→block-param union, mapping each phi-rep to its own same-alloc rep so a bb0 construct source that is the union-find ROOT — and thus not a phi_reps KEY — is reachable; a loop-body owned-consume of a back-edge-renamed alias then flags the SOURCE’s rep → fresh inc kept → bb0 lowers to a harmless [RcInc, RcDec] pair) vs consumed_maycow (the conservative may-COW-user-call over-approximation — stays REP-LOCAL, no phi-propagation, preserving the arc_borrowed_param_cow_push_use_after behavior AND fixing the over-fire: a loop-INVARIANT closure-env passed apply(scale [borrow]) is ONLY in consumed_maycow, never consumed_owned → stays unflagged → fresh inc elided → bb0 dec is its genuine release). The discriminator is in-loop owned-CONSUME vs BORROW, NOT the bb0 Jump-transfer shape (attempt-34 proved that indistinguishable). Probe-gated (emit_burden_path_probe_tail behind predicate_stack_rc_disabled) → default codegen byte-identical (confirmed bb0 IR %3=Construct List; Jump bb1(%15,%3) with ZERO burden/RcDec). CALCULUS: pure case-(a) impl-conformance — Realization.lean RL1_duplication_balanced + RL3_elision_net_preserving already mandate [inc,dec]-OR-[]-never-[dec]; NO .lean/.proof/rule edit. FIXED (11, ZERO new): rc_matrix list_int/list_str/map × {for/break/while} (9) + matrix_list_of_strings_in_loop + journey_guard::test_journey_20_cow_patterns. GUARDRAILS: default SET = base16 EXACT (comm -13+comm -23 both EMPTY, probe-gated byte-identical); under-flag comm -13 EMPTY, 251→240; cargo check --workspace --tests 0; ori_arc 1610/0 debug + 1606/0 release; predicate_stack_probe 104/104; clippy -D warnings clean (ori_arc + ori_llvm tests); §06 VF-1=0 default (burden-balance.sh 0 distinct); lake build green (13 jobs) + git diff --stat aims-proof/ EMPTY; eval+LLVM parity (probe-gated; cured rc_matrix programs exit 0 on BOTH backends default path); prose-lint clean; public-repo hygiene scrubbed (Spec: Annex E §AIMS form only). 8 TDD pins matrix-first in predicate_stack_probe.rs (6 loop-carried-CONSUME positives probe_loop_carried_{push_list_int,push_list_str,insert_map,concat_str,push_while,push_break}_source — 5 FAILED pre-cure → all PASS; 2 loop-invariant-BORROW NEGATIVE clamps probe_loop_invariant_{closure_borrow,map_index_borrow} — PASS pre AND post, the explicit attempt-34 over-fire guard). Files: aims/realize/emit_unified.rs (consume-class split + phi-threaded rep resolution + permanent inc-elision diagnostic), ori_llvm/tests/aot/predicate_stack_probe.rs (8 pins). Checkbox 2 stays UNCHECKED — this fixes the rc_matrix loop-carried-source SUBSET; the iterator-handle / per-element / nested-collection / generic broad-shape remainder (net 240: fat_matrix 37 / generics 35 / fat_ptr_iter 26 + iter_rc_matrix) is the recurring JOINT keep-alive multi-mechanism class still open. The phi-threaded CONSUME-vs-BORROW discriminator landed here is reusable foundation for it. Cross-ref: decisions/LEDGER.md §B.2 attempt-35 line.
2026-06-05 — Attempt 36: generics transfer-through-return forwarder-RESULT leak root-caused; contract-recognizer cure built + REVERTED (over-fired on multi-borrow-then-return forwarders the burden path already releases). Ground-truthed ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN + ORI_TRACE_RC+ORI_CHECK_LEAKS on generic_forwarder_hop1_list_int. ROOT: @id<T>(x:T)->T = x returns its [own] arg unchanged, so in @main the result %4 = Apply @id(%3 [own]) IS the same allocation as the fresh %3 = Construct List (the burden walk emits a net-0 [burden_inc %3, burden_dec %3] pair at the construct; the forwarder result is borrowed-read @len/@__index then dead but carries ZERO burden ops → 1 RC allocation not freed, exit 2). @id itself is byte-identical oracle-vs-flag (the attempt-19 transfers_through_return callee-dec elision holds); the leak is the CALLER’s missing scope-exit release of the transferred fresh allocation. CALCULUS: pure case-(a) impl-conformance — Realization.lean RL2_release_exactly_once + rl2_emits_dec(.ScopeExit) already mandate the fresh-owned result’s single release; NO .lean/.proof/rule edit; no case-(b). The cure recognized a forwarder result (callee param transfers_through_return ∧ ReturnAliasShape::Direct, the proven BUG-04-090 carrier) whose Direct-transfer arg is fresh-owned as itself fresh-owned (a fixpoint in compute_fresh_owned_collection_reps + the matching +1 in compute_owned_collection_delta, threading contracts). On-target the 5 forwarder positives went leak-free + the 2 negatives held, but the FULL corpus OVER-FIRED: under-flag 240→238 with 10 NEW (generics::test_borrow_list_int_{use_twice,use_thrice,one_borrow_apply,two_borrow_applies,multi_let_alias_chain,mixed_apply,project_consumer,resume_terminator,bypass_safe_interaction}_then_return + test_edge_param_returned_and_used). OVER-FIRE ROOT (borrow_list_int_use_twice_then_return SIGSEGV-139 under flag with the cure): a forwarder that BORROW-USES its param then returns it is contract-INDISTINGUISHABLE from @id (both transfers_through_return ∧ Direct) but the burden path ALREADY releases its result (these PASSED at base240); the added dec is a SECOND release → double-free. Same recurring contract-discriminator-too-broad failure as attempt-9/10 (clone-vs-slice) and attempt-34 (bb0-shape). DEFAULT-path guardrail HELD (probe-gated; comm vs base16 both EMPTY). REVERTED clean by re-Editing (no git checkout/restore/reset/stash): recognizer fixpoint + forwarder_direct_transfer_arg helper + delta +1 + threaded contracts all removed; signatures restored. Post-revert: default SET = base16 EXACT, under-flag SET = base240 EXACT (both comm EMPTY, net 240 unchanged), cargo check --workspace --tests 0, ori_arc 1610/0 debug + 1606/0 release (identical to attempt-35), clippy clean, lake build green + git diff --stat aims-proof/ EMPTY, prose-lint clean, zero attempt-36 residual tokens. 7 TDD pins authored + verified pre-cure (5 forwarder positives FAILED = leak, 2 negatives PASSED) then REMOVED on revert (no orphan red pins in the shared probe binary). Files-touched THEN-REVERTED: aims/realize/emit_unified.rs + ori_llvm/tests/aot/predicate_stack_probe.rs. Session: NO net change (characterization-only). Checkbox 2 stays UNCHECKED. NEXT LEAF: NOT a contract-level transfers_through_return recognizer (too broad) — fire the forwarder-result scope-exit dec ONLY when the burden path does NOT already release it, via the per-allocation alloc-aware NET threaded THROUGH the apply-Direct transfer edge (extend compute_jump_threaded_reps/compute_phi_threaded_alloc_reps to union the Apply @fwd(arg)->dst Direct-transfer edge so the result rep merges with the source rep; the trivial @id chain nets +1 → dec, the multi-borrow @use_twice chain already nets 0 via its existing release → no dec). This extends attempt-35’s compute_phi_threaded_alloc_reps foundation. Cross-ref: decisions/LEDGER.md §B.2 attempt-36 line.
2026-06-05 — Attempt 37: forwarder-RESULT leak CURED + KEPT (the attempt-36 NEXT LEAF — alloc-aware net through the apply-Direct transfer edge, NOT a contract recognizer); 12 fixed, ZERO new, under-flag 240→228. FRESH baseline captured this session (warm binary stale; rebuilt oric+ori_rt+aot): default 16/2453 (§09-coupled cohort EXACT), under-flag 240/2453. CURE (3 parts, burden-path, Invariant-5-clean): (1) compute_jump_threaded_reps gains an OPTIONAL apply-Direct seed (SORTED-key for codegen determinism) wired ONLY by the dead-owned-collection pass — the forwarder result %4 merges with %3’s lineage (the merge already lives in same_alloc_reps via populate_apply_result_aliases ApplyAliasSource::Direct); the other 7 callers pass None (byte-identical). (2) compute_owned_consumed_lineages + compute_user_call_arg_lineages gain a Direct-PASS-THROUGH skip (an owned/user-call arg whose same-alloc rep == the call result rep is the forwarder passing the allocation forward, NOT consumed → stays eligible). (3) a forwarder single-sink gate (compute_forwarder_result_reps + sinks.len() != 1) — fire the freeing dec only on the straight-line single-dead-sink shape; a branchy &&-short-circuit result whose own binc/bdec pairs release per-branch is left to joint accounting (firing per-branch double-frees, the @use_twice SIGSEGV-139 attempt-36 reproduced). CALCULUS: pure case-(a) impl-conformance — Realization.lean rcBalance+RL2_release_exactly_once+rl2_emits_dec(.ScopeExit) already mandate the trivial @id result’s single scope-exit release; NO .lean/.proof/rule edit (lake build 13 jobs green + git diff --stat aims-proof/ EMPTY + no .lean mtime-touched). FIXED 12 (verbatim, ZERO new): apply_alias_coverage::test_apply_alias_direct_intlist + fat_matrix::f10_generics::{list_fat,list_scalar,map,multi_instantiation,str_heap} + generics::{chain_list_element,generic_forwarder_hop1,hop2,hop4,list_str,map_int_str}-returns_intact. GUARDRAILS: default SET = base16 EXACT (comm -13+comm -23 both EMPTY, 16/2453 — probe-gated byte-identical); under-flag comm -13 EMPTY, 240→228; cargo check --workspace --tests 0; ori_arc 1612/0 debug + 1608/0 release (+4 unit pins); clippy -D warnings clean; §06 VF-1=0 default (burden-balance.sh 0); eval+LLVM parity (forwarder fixture exit 0 both backends); prose-lint clean; public-repo hygiene scrubbed (Spec: Annex E §AIMS only; litter-pickup scrubbed 2 pre-existing attempt-9 test-file leaks). 6 TDD pins matrix-first (4 AOT probe_forwarder_result_freed_{id_list_int,multi_hop_list,non_generic_list} positives FAILED pre-cure + probe_multi_borrow_then_return_no_double_free_negative PASSED pre-cure = the over-fire boundary; 2 ori_arc unit dead_owned_collection_{frees,skips}_forwarder_result_{with,without}_apply_direct_seed — the negative proving the seed is load-bearing). Files: aims/realize/emit_unified.rs + its test sibling + predicate_stack_probe.rs. Checkbox 2 stays UNCHECKED — this fixes the SIMPLE straight-line forwarder subset; 7 directive targets remain (generics::generic_forwarder_{box_list,closure_capturing_list,nested_list,set_int,struct_with_list}-returns_intact + non_generic_forwarder_list + fat_matrix::f10_generics::test_fm_generic_with_operation) = the BRANCHY/compound forwarder shapes needing post-dominating single-dec placement + joint result-element accounting (the recurring JOINT keep-alive class per attempts 9/11/12/13/22/25/27/30/34/36). The apply-Direct-seeded reps + Direct-pass-through-skip foundation landed here is what that builds on. Cross-ref: decisions/LEDGER.md §B.2 attempt-37 line.
2026-06-05 — Attempt 38: fat_matrix::f13_derived_eq (derived-Eq on struct-with-heap-field, 14 under-flag) CHARACTERIZED as a JOINT 3-mechanism shape; two over-inc sub-mechanisms BUILT + validated-on-IR + REVERTED net-zero; zero new, zero fixed. FRESH baseline rebuilt from disk (warm binary showed 2292 default fast-fails from a concurrent-build collision; rebuild restored default 16/2453 EXACT, under-flag 228/2453 floor). LEAF = fat_matrix::f13_derived_eq (largest coherent single-sub-cluster of fat_matrix 32, all test_fm_eq_*). Ground-truth (ORI_TRACE_RC/ORI_DUMP_AFTER_BURDEN/ORI_LOG=ori_arc::aims::realize=trace inc-elision diagnostic on fm_eq_heap_str): THREE mechanisms. (M1) DEAD-owned-Aggregate-with-heap-field NO scope-exit dec = DOMINANT root — a minimal let a = Doc { content: "…" }; 0 (struct never used) LEAKS: the Doc Aggregate %1 / its content string %0 carry ZERO burden ops → the heap string is never freed (oracle frees via RcDec [AggFields] walking the field). The struct is var_repr = Aggregate (inline struct holding a heap str), so compute_fresh_owned_collection_reps (the attempt-30 dead-owned recognizer, RcPtr List/Map/Set only) never sees it — THIS is attempt-30’s verbatim next-leaf (compute_dead_no_use_aggregate_reps, field-walk net, “larger over-fire surface, every Option/Result/struct/enum”). (M2) Aggregate Construct fresh-site inc spurious for a borrow-only-used struct — burden_inc %1 propagates to the field string; compute_elidable_fresh_self_alloc_incs (emit_unified.rs:3627) deliberately restricts elision to RcPtr/FatValue dsts, never the Aggregate. (M3) dup-alias incs on borrow-read comparison operands — %9=%1/%12=%1 aliases into a==b/a!=c flagged dup_alias_dsts (%1 use-count ≥2) but the operand is a PrimOp Binary(Eq/NotEq) (is_owned_position false, the derived Eq::equals(self,other) borrow-reads) → RL-1 no inc on a non-duplicating use. BUILT M2 (skip aggregate builders in the cow-mutated owned-position scan — a struct-field STORE is a transfer, not a COW) + M3 (a dst_uses_are_all_borrowed_reads non-Add-PrimOp-operand predicate excluding such aliases from BOTH dup_alias_dsts (inc) AND owned_vars_needing_rc (dec) in LOCKSTEP — suppressing only the inc strands the dec → double-free), validated on the burden IR (binc 3→1 on the content string). KILLING CLAUSE: full under-flag corpus with M2+M3 = 228 EXACT, comm -13=0 AND comm -23=0 — NET ZERO. M2+M3 are sound (zero regressions) but INERT — M1 (the dead-Aggregate dec) is the load-bearing root; the field leaks regardless of inc count. REVERTED CLEAN (both production files back to in-tree A’+B’+15-37; 4 authored TDD pins REMOVED — no orphan red pins; verified residual-token grep 0, burden_lower/mod.rs numstat-vs-HEAD EMPTY, default 16 + under-flag 228 both comm directions EXACT, ori_arc 1612/0 debug, git diff --stat aims-proof/ EMPTY, no git checkout/restore/reset/stash, no Lean/test/gate weakened). CALCULUS: pure case-(a) impl-conformance — Realization.lean rl2_emits_dec(.ScopeExit) (M1) + RL1_emit_iff_not_elidable/RL1_duplication_balanced (M2/M3) already mandate all three; NO .lean/.proof/rule edit; no case-(b) scratch theorem. Checkbox 2 stays UNCHECKED. NEXT LEAF: (a) build M1 (dead-no-use-Aggregate field-walk dec — the dominant root, attempt-30’s next-leaf) FIRST, then layer M2+M3 in lockstep; OR (b) pick a NON-Aggregate single-mechanism cluster (fat_ptr_iter 26 non-iter-element, string_sso 6, iter_rc_matrix non-nested, collections_ext/elem_dec_scope non-per-element). PRESERVE the validated M3 borrow-read predicate + M2 aggregate-builder-is-transfer insight. Cross-ref: decisions/LEDGER.md §B.2 attempt-38 line.
2026-06-05 — Attempt 39: M1 dead-no-use INLINE-AGGREGATE scope-exit dec CURED + KEPT (attempt-38’s DOMINANT-root next-leaf + attempt-30’s verbatim compute_dead_no_use_aggregate_reps leaf, M1 ALONE as the load-bearing fix); 3 fixed, ZERO new, under-flag 228→225. Fresh baseline rebuilt from disk: default 16/2441 (§09-coupled EXACT), under-flag 228/2229 floor. ROOT (ground-truthed ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN + ORI_TRACE_RC+ORI_CHECK_LEAKS on let c = Link(a: Logged{tag:"outer-a"}, b:.., next: Link(.., next: Nil)) + minimal let a = Doc{content: Logged{..}}; 0 + tuple repros): a bare let-bound INLINE aggregate (var_repr = Aggregate: struct/tuple/Option/Result/user-enum holding a heap field), dead with ZERO uses, carries ZERO burden ops in the Phase-5 walk → the heap field’s alloc +1 is never released (the user @drop silently does not run); the oracle emits ONE scope-exit RcDec [InlineEnum]/[AggFields] walking the field drop-glue. CURE (KEPT, burden-path, Invariant-5-clean — extends the dead-owned recognizer family, no parallel emitter): new probe-tail Phase 6.85 emit_burden_dead_no_use_aggregate_decs + compute_dead_no_use_aggregate_releases + the gate is_burden_carrying_aggregate (var_repr == Aggregate AND ori_types::classify_triviality == NonTrivial — the SSOT both ArcClassifier and burden synthesis consume). Emits ONE whole-var BurdenDec at the defining block’s scope exit; Phase-7 lowers through RcStrategy::from_var(Aggregate, ..) to RcDec [AggFields]/[InlineEnum] = byte-identical to oracle. FIELD-WALK net: the inline aggregate has NO self-buffer +1 and carries ZERO burden ops, so the emission is exactly the missing dec balancing the heap FIELD’s +1. SEED-not-reuse exclusions (same set as the dead-owned-collection pass + ONE ADDED): compute_dead_iterator_handle_candidates (Phase 6.9’s domain — an iterator-bearing aggregate would double-free without this; cured the iterator_handle_in_struct/tuple over-fire) + owned-consumed (the nested Link(.., next: Link(..)) inner node is excluded → only the OUTERMOST let c fires, its single dec walks the whole tree) + returned + primop-operand + user-call-arg + owned-moved + iter-element/borrowed-defs + the lineage_has_any_use no-use gate. Probe-gated → default codegen byte-identical. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean rl2_emits_dec(.ScopeExit)=true + RL2_release_exactly_once + RL5_cleanup_balanced ALREADY mandate the single scope-exit release; the impl emitted [] = leak; NO .lean/.proof/rule edit, no case-(b) scratch theorem (lake build 13 jobs green + git diff --stat aims-proof/ EMPTY). FIXED 3 (verbatim, ZERO new): drop_augment::drop_boxed_recursive_enum_runs_every_node_payload_drop_in_reverse_order (attempt-30’s documented M1 next-leaf) + recursive_feature::recursive_feature_mutual_enum_cycle + recursive_feature::recursive_feature_mutual_struct_enum_cycle. GUARDRAILS: default SET = base16 EXACT (comm -13+comm -23 both EMPTY, 16/2450 — probe-gated byte-identical); under-flag comm -13 EMPTY, 228→225; cargo check --workspace --tests 0; ori_arc 1615/0 debug + 1611/0 release; predicate_stack_probe 117/117; clippy -D warnings clean (ori_arc + ori_llvm tests); §06 VF-1=0 default (0 imbalances on cured struct/tuple/enum); lake build green + git diff --stat aims-proof/ EMPTY; eval+LLVM parity (probe-gated → eval cargo st 4629/45 baseline; cured fixtures exit 0 both backends — the top-level-let-no-use drop-print eval/AOT-default divergence is PRE-EXISTING + orthogonal per attempt-30); prose-lint clean; public-repo hygiene scrubbed (Spec: Annex E §AIMS RL-2 only). 12 TDD pins matrix-first (9 AOT: 6 type×repr positives probe_dead_no_use_{struct_str_field,tuple_str_fields,option_struct,result_struct,user_enum_payload,nested_struct_field} FAILED pre-cure → PASS + heap_str_field_freed leak positive FAILED pre-cure + 2 NEGATIVES {returned_aggregate_no_double_free,scalar_only_struct_no_dec} pass pre+post; 3 ori_arc unit dead_no_use_aggregate_{frees_struct_with_str,skips_scalar_only_struct,skips_returned_struct}). A’+B’+15-37 PRESERVED (the attempt-31 iterator_handle_in_struct/tuple pins restored after the over-fire exclusion). Files: aims/realize/emit_unified.rs (Phase 6.85 + compute_dead_no_use_aggregate_releases + is_burden_carrying_aggregate + the iterator-bearing exclusion), its test sibling (3 unit pins + 3 builders), predicate_stack_probe.rs (9 pins + 1 helper). No parallel-session files touched; no Lean/test/gate weakened; no git checkout/restore/reset/stash. M2+M3 NOT layered (M1 ALONE is the load-bearing fix; M2+M3 stay attempt-38-preserved for the f13_derived_eq JOINT attempt). Checkbox 2 stays UNCHECKED — M1 fixes the bare no-use shape; fat_matrix::f13_derived_eq (14, USED-and-compared a==b struct) STILL needs M1+M2+M3 in lockstep. NEXT LEAF: the f13_derived_eq JOINT M1+M2+M3 attempt (M1 foundation now reusable) OR a NON-Aggregate single-mechanism cluster (fat_ptr_iter 26 / string_sso 6 / iter_rc_matrix non-nested / collections_ext+elem_dec_scope non-per-element). Cross-ref: decisions/LEDGER.md §B.2 attempt-39 line.
2026-06-05 — Attempt 40: PROJECT-BORROWED-VIEW alias spurious-release suppression CHARACTERIZED; the membership-strip cure built + REVERTED (over-fired on RcPtr-collection-field / sum-payload / last-owner borrow-views it also stripped); zero net fixed, zero net regression. Fresh baseline rebuilt from disk: default 16/2466 EXACT, under-flag 225/2466 floor (attempt-39 kept; the 4 default-path-only IDs generics::generic_forwarder_{option,result}_list* + higher_order::hof_closure_capture_in_loop + tagless_enum::tagless_enum_list_payload_reads_and_drops fail predicate-stack-ON but PASS under the flag — orthogonal). LEAF = the str-field BORROW-VIEW double-free (borrow_independence::test_borrow_then_let_alias + inc_symmetry::test_inc_symmetry_borrow_then_let_alias; the clean single-mechanism residual after ground-truthing that string_sso multi-ref is &&-branchy per-path JOINT, concat/rc_matrix::matrix_str_* is str + str PrimOp-Add buffer-aliasing INVISIBLE to same_alloc_reps, and fat_ptr_iter::cow/derive_clone are loop+COW multi-mechanism). ROOT (ground-truthed ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN/ORI_DUMP_AFTER_BURDEN_ELIM/ORI_DUMP_AFTER_ARC + ORI_TRACE_RC+ORI_CHECK_LEAKS on type Wrapper = { s: str }; let w = Wrapper{s:"…"}; let borrowed = w.s; let chained = borrowed; chained == "…"): %4 = Project %3.0 is a TF-4 borrow-view of the LOCAL owned struct %3; its move-alias chain %6 = %4, %8 = %6 is borrowed too. The struct’s own RcDec %3 [AggFields] frees the field string %0. The Phase-5 emit_burden_ops (burden_lower/) emits a spurious burden_dec %8 (lowered RcDec %8 [FatPtr]) → frees %0 AGAIN → DOUBLE-FREE. KILLING ROOT of the spurious dec: the base compute_borrowed_alias_vars (burden_lower/mod.rs:499) seeds ONLY from borrowed PARAMS + borrowed.is_empty() early-return, so for @main (no borrowed params) it never marks the LOCAL borrow-view chain borrowed; the probe tail’s collect_project_borrowed_defs (emit_rc/borrowed_defs.rs:350 — non-take Project dsts + alias closure, take-projects EXCLUDED) DOES include %4/%6/%8 but NO pass strips the base’s already-emitted dec. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL4_borrowed_no_edge_dec (.Borrowed ⟹ no edge dec) + RL2_release_exactly_once (the aggregate’s single [AggFields] drop IS the field’s one release) ALREADY mandate a borrow-view emits no release; the impl emits a second [dec]; NO .lean/.proof/rule edit (lake build 13 jobs green + git diff --stat aims-proof/ EMPTY); no case-(b). CURE ATTEMPTED (REVERTED): probe-tail Phase 6.96 suppress_project_borrowed_view_decs — strip every whole-var BurdenDec { var } where var ∈ collect_project_borrowed_defs AND var ∉ inc_vars (UNPAIRED-only — a paired [BurdenInc, BurdenDec] index-retain unit nets 0; stripping only its dec orphans the inc → the discriminator added after the first formulation (strip ALL) turned the [int]-list-field case from double-free into LEAK). On-target the str-field shape went leak-free + the owned-literal negative held. KILLING CLAUSE: full under-flag corpus = comm -13 NON-EMPTY, 10 NEW: fat_matrix::f11_struct_field::test_fm_struct_field_map + fat_matrix::f12_sum_payload::{test_fm_sum_list_fat_payload,test_fm_sum_list_scalar_payload,test_fm_sum_str_heap_payload} + for_yield_option::test_for_yield_option_break_semantic_pin + generics::{test_generic_forwarder_option_list_returns_intact,test_generic_forwarder_result_list_str_returns_intact} + match_alias::test_let_alias_filter_protected + string_sso::test_heap_in_struct + structs::test_struct_list_field; FIXED 9: borrow_independence::test_borrow_then_let_alias + inc_symmetry::test_inc_symmetry_borrow_then_let_alias + fat_matrix::f11_struct_field::{test_fm_struct_field_list_fat,test_fm_struct_field_list_scalar,test_fm_struct_field_str_heap} + match_alias::test_set_value_alias + rc_matrix::test_matrix_struct_scope + recursive_codegen::recursive_codegen_read_through_back_edge_returns_value + spec::test_aot_struct_with_list_field. NET −9 +10. OVER-FIRE ROOT: collect_project_borrowed_defs marks EVERY non-take Project dst borrowed, but a Project of an RcPtr-COLLECTION field / sum-payload / last-owner struct-list-field that is the buffer’s LAST owner is NOT a pure borrow-view — under the flag its dec IS the buffer’s genuine release (the aggregate [AggFields] drop does NOT free a moved-out / last-owner collection on those paths), so stripping it LEAKS (the unpaired guard does not exclude these — a last-owner view carries an unpaired dec too). Same recurring classifier-too-broad failure as attempt-9 Fix-A (clone-vs-slice), attempt-34 (bb0-shape), attempt-36 (transfers_through_return-Direct), attempt-38 (M2 RcPtr-only-guard). DEFAULT-path guardrail HELD (probe-gated; comm vs base16 both EMPTY). REVERTED clean by re-Editing (Phase-6.96 call + project_borrowed_defs param thread + suppress_project_borrowed_view_decs fn all removed; signature back to 9-param; no git checkout/restore/reset/stash). Post-revert: default SET = base16 EXACT (comm -13+comm -23 both EMPTY); under-flag SET = base225 EXACT (comm -13+comm -23 both EMPTY, byte-clean to the attempt-39 floor); cargo check --workspace --tests 0; ori_arc 1615/0 debug + 1611/0 release (identical to attempt-39); predicate_stack_probe 117/117 (attempt-39’s pins intact, my 4 removed — no orphan red pins); clippy -D warnings clean (ori_arc + ori_llvm tests); §06 VF-1=0 default; lake build green (13 jobs) + git diff --stat aims-proof/ EMPTY; prose-lint clean (2 touched files); zero attempt-40 residual tokens. 4 TDD pins authored + verified pre-cure (3 str-field positives probe_project_borrowed_view_{alias_str_field,direct_use,alias_deeper_chain} FAILED = double-free + 1 negative probe_owned_literal_release_not_suppressed_negative PASSED) then REMOVED on revert (no orphan red pins in the shared probe binary). Files-touched THEN-REVERTED: aims/realize/emit_unified.rs + predicate_stack_probe.rs. Session: NO net change (225 floor unchanged; the 9 fixed exactly cancel the over-fire on revert). A parallel session concurrently edited emit_unified.rs during this attempt (file git-added-line count drifted 1038→942 between baseline-capture and revert, owned by that session — untouched by me beyond my reverted additions). No other parallel-session files touched; no Lean/test/gate weakened. Checkbox 2 stays UNCHECKED. NEXT LEAF: NOT a collect_project_borrowed_defs-membership recognizer (too broad) — strip the borrow-view dec ONLY when the burden path does NOT already need it as the buffer’s last-owner release, via the per-allocation alloc-aware NET (compute_lineage_alloc_aware_net/compute_same_alloc_reps): a FatValue str-field view whose field is freed by the aggregate [AggFields] drop nets +1 (surplus → strip), an RcPtr collection-field / sum-payload last-owner view nets 0 (genuine release → keep). Extend the alloc-aware net to attribute the aggregate’s [AggFields]/[InlineEnum] field-drop as the field’s release so the str-field view’s lineage shows the surplus; pair with M3 borrow-read-alias inc-suppression (attempt-38-preserved) for the co-occurring %9-class comparison-literal over-inc. This is the reusable alloc-aware-net foundation (attempts 35/37/39), NOT a single-pass membership strip. SECONDARY non-Aggregate residuals: fat_ptr_iter 26 non-iter-element; string_sso heap-multi-ref only via per-path JOINT (&&-branchy heap_multiple_references); concat/rc_matrix::matrix_str_* only via a str + str PrimOp-Add buffer-provenance recognizer (same_alloc_reps Let-Var-only — the empty/concat operand-buffer reuse is invisible, needs a contract/recognizer extension flagged risky). Cross-ref: decisions/LEDGER.md §B.2 attempt-40 line.
2026-06-05 — Attempt 41: PROJECT-BORROWED-VIEW redundant scope-exit dec CURED + KEPT (attempt-40’s NEXT LEAF — the alloc-aware aggregate-field-drop NET, NOT the collect_project_borrowed_defs membership attempt-40 over-fired on); 9 fixed, ZERO new, under-flag 225→216. Fresh baseline rebuilt from disk (the warm aot binary showed 2301/2494 default fast-fails from a stale dashmap --check-cfg artifact left by a concurrent build — cargo build -p oric cleared it): default 16/2494 (§09-coupled EXACT), under-flag 225/2494 floor. ROOT (ground-truthed ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN/ORI_DUMP_AFTER_ARC + ORI_TRACE_RC+ORI_CHECK_LEAKS on Wrapper{s:str}/Container{items:[str]|[int]}/Option<Wrapper>/Result<Wrapper,int> match-extract): a %view = Project %src.field borrow-view of a LOCAL owned aggregate (%src var_repr=Aggregate, heap-bearing field) gets a spurious last-use burden_dec %view from the Phase-5 walk; the aggregate’s own burden_dec %src (lowered RcDec %src [AggFields]/[InlineEnum]) ALREADY frees the field → burden_dec %view (lowered RcDec %view [FatPtr]/[HeapPtr]) double-frees it (exit 134). %src SINGLE-REF (no burden_inc) → rc=1 field, the two decs collide. The KEEP shape Config{settings,name} (two projected fields) is paired-inc shared (burden_inc %6/%9 raise the field rc≥2, the projection dec releases the extra ref, net 0); the sum-payload KEEPs (Text(content)/Numbers(items)) are enum-keep-alive-balanced. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL4_borrowed_no_edge_dec (borrow-view emits no release) + RL2_release_exactly_once (the aggregate [AggFields]/[InlineEnum] drop IS the field’s one release) ALREADY mandate it; the impl emitted a second [dec]; NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY, lake build 13 jobs green); no case-(b). CURE (KEPT, burden-path, Invariant-5-clean, no parallel emitter): probe-tail Phase 6.96 strip_redundant_project_borrowed_view_decs + the testable compute_redundant_project_borrowed_view_dec_strips, gated behind predicate_stack_rc_disabled. STRIP a burden_dec %view iff (1) %view ∈ collect_project_borrowed_defs; (2) it traces (resolve_root) to Project %src.field; (3) %src is ValueRepr::Aggregate + is_burden_carrying_aggregate; (4) AGGREGATE-DROP-FIRES — %src carries a freeing BurdenDec (its drop releases the field; no agg dec → KEEP, the no-agg-dec tuple shape); (5) the NET discriminator — %src SINGLE-REF (no BurdenInc on any same-root alias; paired inc → shared rc≥2 → the projection dec is the genuine extra-ref release → KEEP). This executes attempt-40’s verbatim alloc-aware-net prescription AS a net (single-ref + aggregate-drop-fires), NOT a membership strip (the over-fire root). FIXED 9 (verbatim, ZERO new): borrow_independence::test_borrow_then_let_alias + inc_symmetry::test_inc_symmetry_borrow_then_let_alias + fat_matrix::f11_struct_field::{test_fm_struct_field_list_fat,test_fm_struct_field_list_scalar,test_fm_struct_field_str_heap} + match_alias::test_set_value_alias + rc_matrix::test_matrix_struct_scope + recursive_codegen::recursive_codegen_read_through_back_edge_returns_value + spec::test_aot_struct_with_list_field — the SAME 9 attempt-40 fixed, but the net KEEPS all 10 attempt-40 broke (the f11_struct_field::map + f12_sum_payload list/str payloads + string_sso::test_heap_in_struct + structs::test_struct_list_field + match_alias::test_let_alias_filter_protected + the option/result forwarders stay passing). GUARDRAILS: default SET = base16 EXACT (comm -13+comm -23 vs /tmp/a41_default.txt BOTH EMPTY, 16/2494 — probe-gated byte-identical); under-flag comm -13 vs /tmp/a41_underflag.txt EMPTY, 225→216; cargo check --workspace --tests 0; ori_arc 1618/0 debug + 1614/0 release (+3 unit pins); predicate_stack_probe 127/127 (117 + 10 new); rc_matrix 135/0; clippy -D warnings clean (fixed 2 doc-backtick warnings); §06 VF-1=0 default (burden-balance.sh 0 + 0 on cured fixtures); lake build green (13 jobs) + git diff --stat aims-proof/ EMPTY; eval+LLVM parity (cured fixtures exit 0 both backends; eval cargo st 4629/45 EXACT attempt-39 baseline); prose-lint clean (3 touched files); public-repo hygiene scrubbed (Spec: Annex E §AIMS only; a LEDGER §B.2 doc-comment ref I introduced was scrubbed to self-contained prose). 13 TDD pins matrix-first (10 AOT: 6 positives probe_project_borrowed_view_{struct_str_field,struct_list_str_field,struct_list_int_field,option_struct_str_field,result_struct_str_field,disjoint_field} — 5 FAILED pre-cure → all PASS; 4 NEGATIVES {paired_inc_collection_field,sum_str_payload,sum_list_int_payload,owned_literal_release} PASS pre AND post = the attempt-40 over-fire guards; 3 ori_arc unit project_borrowed_view_{strips_single_ref_str_field_dec,keeps_paired_inc_shared_aggregate_dec,keeps_view_dec_when_no_aggregate_dec}). Files: aims/realize/emit_unified.rs (Phase 6.96 + 2 fns), its test sibling (3 unit pins + 1 builder), predicate_stack_probe.rs (10 pins). A PARALLEL SESSION concurrently edits emit_unified.rs (my additions grep-confirmed intact); no parallel-session files touched; no Lean/test/gate weakened; no git checkout/restore/reset/stash. NEXT LEAF: the fat_matrix::f13_derived_eq JOINT M1+M2+M3 (attempt-39 M1 + this view-strip are foundations) OR a NON-Aggregate single-mechanism cluster (fat_ptr_iter 26 / string_sso &&-branchy / concat-PrimOp-Add). Cross-ref: decisions/LEDGER.md §B.2 attempt-41 line.
2026-06-05 — Attempt 42: fat_matrix::f13_derived_eq USED-and-compared derived-Eq struct cluster — M3 borrow-read comparison-operand keep-alive-inc strip BUILT + REVERTED (over-fired LEAK→DOUBLE-FREE); a FOURTH mechanism (M4) isolated; byte-clean revert. Fresh baseline rebuilt from disk: default 16/2457 (§09-coupled EXACT; comm both EMPTY; tagless_enum_list_payload_reads_and_drops flakes under concurrent binary contention, deterministic-FAIL in isolation, in baseline, not my scope), under-flag 216/2457 floor (attempt-41 kept). LEAF = f13_derived_eq (20/29 fat_matrix residuals — derived-Eq a==b/a!=c on aggregate-with-heap-field; inline-SSO test_fm_eq_struct_str passes, only heap-backed/list/map/option/result leak). ROOT (ground-truthed ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN/_ELIM/ORI_DUMP_AFTER_ARC + ORI_TRACE_RC+ORI_CHECK_LEAKS on #derive(Eq) type Doc={content:str}; a==b; a!=c): the multi-use struct %1(a) gets ONE keep-alive burden_inc %1 (RL-1 duplication); each comparison move-alias %9=%1(==), %12=%1(!=) ALSO gets a paired burden_inc/dec (use-count≥2 → dup_alias_dst), but they flow ONLY into PrimOp Binary(Eq/NotEq) (is_owned_position false, borrow-read) — NOT a duplicating use; the operand inc/dec self-cancel, leaving the burden_inc %1 bump never released → heap content LEAKS (exit 2, size=30). /calc ledger: buggy net +1 (leak), oracle net -1 (freed once). CALCULUS: case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL1_emit_iff_not_elidable + RL1_duplication_balanced mandate [inc,dec] OR [], never a spurious extra [inc] on a borrow-read; impl diverges; NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY, no .lean mtime-touched); no case-(b). CURE ATTEMPTED (REVERTED): probe-tail Phase 6.97 strip_redundant_compare_operand_incs + testable compute_redundant_compare_operand_inc_strips, gated behind predicate_stack_rc_disabled — STRIP burden_inc %op iff (1) %op sole-non-RC-use is a PrimOp Binary(Eq/NotEq/Lt/LtEq/Gt/GtEq) operand; (2) %op is Let{Var(src)} move-alias; (3) paired BurdenDec %op; (4) src-root carries a keep-alive bump. KILLING CLAUSE: on fm_eq_heap_str the cure turned the LEAK into FATAL — ori_rc_dec called on already-freed DOUBLE-FREE (exit 134). M4 root (NEW, not in attempt-38 M1+M2+M3): the ORACLE puts RcDec %1 ONLY on bb2 (the a==b-FALSE else-branch) and frees %1 on the TRUE then-branch via operand decs %9(bb0)+%12(bb1) ALONE; the BURDEN path puts burden_dec %1 on bb1 (the THEN-branch) → 3 decs on %1 on the then-path (%9+%12+%1) vs oracle’s 2. Stripping the operand incs nets the then-path 1+1-1-1-1 = -1 (/calc) → double-free. M3 alone CANNOT land: the burden %1 scope-exit dec lands on the WRONG (then) branch vs the oracle’s complement (else) branch. REVERTED CLEAN (Phase-6.97 + 2 fns + import + builder + 3 unit pins + 7 AOT pins removed; grep 0; default 16 EXACT both comm; under-flag 216 EXACT both comm; cargo check --workspace --tests 0; ori_arc 1618/0 debug; predicate_stack_probe 127/127 attempt-41 floor; git diff --stat aims-proof/ EMPTY; no .lean touched; no git checkout/restore/reset/stash; no Lean/test/gate weakened). 7 AOT TDD pins (5 positives FAILED=leak pre-cure, 2 negatives PASSED) + 3 ori_arc unit pins authored matrix-first then removed on revert (no orphan red pins). NOTE: a flawed 8th negative on let held=[a,a] FAILED pre-cure for an ORTHOGONAL reason → surfaced + filed BUG-04-139 (let held=[a,a] duplicate-owned-list-literal-element LEAKS on the DEFAULT path; orthogonal to §07B burden-path); replaced with a clean comparison_in_callee negative before the attempt. VERDICT: f13_derived_eq is a JOINT 4-mechanism shape — M3 (operand-inc strip, BUILT + validated on bare-block ledger) + M4 (the burden-path %1 scope-exit dec must move to the oracle’s complement-branch placement, OR the operand decs must ALSO be stripped so %1’s dec is the SOLE release) in LOCKSTEP. PRESERVE: the M3 discriminator + the M4 then-vs-else dec-placement diagnosis. NEXT LEAF: (a) build M4 FIRST (reconcile the burden multi-use-aggregate scope-exit dec CFG placement to the oracle per-branch shape), then layer M3; OR (b) a NON-Aggregate NON-branchy single-mechanism cluster (fat_ptr_iter 26 / arc 14 / rc_matrix 11 non-str+str / trmc 8 / narrowing 9 / recursive_derive 5). Cross-ref: decisions/LEDGER.md §B.2 attempt-42 line.
2026-06-05 — Attempt 43: sets set-algebra RESULT leak CURED + KEPT (clean single-mechanism cluster — a.union(b)/a.difference(b)/a.intersection(b) return a FRESH owned {T} Set, borrowed-read by @len then dead at scope exit; the fresh-owned-collection recognizer omitted set-algebra producers so the result buffer leaked). Extended compute_fresh_owned_collection_reps + compute_owned_collection_delta allocates with a new collection_set_algebra_names SSOT (union/difference/intersection) — a direct extension of the landed conversion / iter-consumer recognizer family (attempts 30/33), the alloc-aware net fires ONE scope-exit dec per result. Pure case-(a) impl-conformance (arc.md §CP-1): Realization.lean RL2_release_exactly_once + rl2_emits_dec(.ScopeExit) ALREADY mandate the single release; impl diverged (omitted the freeing dec); NO .lean/.proof/rule edit (lake build 13 jobs green, git diff --stat aims-proof/ EMPTY). Under-flag net 216→213, ZERO new; FIXED 3 verbatim: sets::test_aot_set_union + sets::test_aot_set_difference + sets::test_aot_set_intersection. Guardrails all clean (default-16 byte-identical both comm; ori_arc 1620/0 debug + 1616/0 release; clippy -D warnings 0; §06 VF-1=0 default+under-flag; eval+LLVM parity exit-0 both backends; prose-lint 0; hygiene Spec: Annex E §AIMS RL-2 form only). TDD: 4 AOT pins in predicate_stack_probe.rs (3 positives FAILED pre-cure / union/difference/intersection + 1 returned NEGATIVE PASSED pre/post) + 2 ori_arc unit pins (fresh_owned_collection_reps_includes_set_union_result + set_algebra_names_covers_union_difference_intersection). NEXT LEAF: a NON-Aggregate, NON-branchy single-mechanism cluster — cow_map_set 3 / slices 2 / realize_rc_reuse 3; AVOID recursive_feature 4 (the dead-Jump-arg-aggregate-block-param net is 0 on the inline-aggregate self-rep — needs the field-walk net + keep-alive accounting reconciliation, closer to JOINT) + the f13_derived_eq/comparison-on-branch shape (M4 unisolated, attempt-42) + the concat/rc_matrix::matrix_str_* str+str PrimOp-Add buffer-provenance recognizer (flagged risky). Cross-ref: decisions/LEDGER.md §B.2 attempt-43 line.
2026-06-05 — Attempt 44: slices seamless-slice RECEIVER-dec-before-Apply UAF/double-free — the Both-edge relocation cure (extend Phase-6.65 borrowed_arg_release_verdict with a sharing_view escape-safe class for slice/take/drop/substring) BUILT + REVERTED (over-fired on the &&-branchy slice/take/drop variants); the M4-CFG-dec-placement class re-surfaced; byte-clean revert. Fresh baseline rebuilt from disk (oric+ori_rt+aot): default 16/2514 (§06-coupled EXACT, comm both EMPTY), under-flag 213/2514 floor (attempt-43 kept). LEAF = the seamless-slice receiver-dec shape (the CLEAN single-mechanism cluster after ground-truthing the attempt-43 NEXT-LEAF suggestions are all risky: cow_map_set 3 = loop-carried + &&-branchy; slices::test_list_slice_preserves_original = &&-branchy JOINT; realize_rc_reuse::multi_use_let_var_eq_chain_* = the f13_derived_eq EqChain M4 family). ROOT (ground-truthed ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_ARC/ORI_DUMP_AFTER_BURDEN + ORI_TRACE_RC+ORI_CHECK_LEAKS on let xs=[1..10]; let ys=xs.slice(start:2,end:8); if ys.length()==6 then 0 else 1): %12 = %10 (move-alias of the parent buffer, rc=1) flows into %15 = Invoke @slice(%12 [borrow]) normal bb1 unwind bb2; the seamless slice %15/%17 SHARES %12’s buffer (SLICE_FLAG cap) and @slice rc-INCs it (1->2). The Phase-5 walk places burden_dec %12 INLINE in bb0 BEFORE the @slice Invoke -> under sole-emitter lowering the dec frees the buffer (dec->0 FREE) BEFORE @slice reads+incs it -> UAF (inc->1 (live=0) on freed mem) + the slice’s RcDec %17 double-frees. slice_then_length SIGSEGVs (exit -139); take/drop/substring are the IDENTICAL latent UAF passing by luck. The ORACLE places RcDec %12 AFTER @slice (bb1 normal + bb2 unwind), then RcDec %17 (slice) 1->0. Phase-6.65 relocate_borrowed_terminator_arg_dec_to_edges is EXACTLY the surface but DECLINES @slice (the !dst_scalar gate catches the non-scalar slice result). CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) - Realization.lean RL2_borrowed_param_emits_caller_dec (line 220) + RL2_release_exactly_once (line 239) + RL4_borrowed_no_edge_dec (line 302) ALREADY mandate the borrowed receiver’s single caller dec at its TRUE last use (after the borrow reads); the impl placed it BEFORE; NO .lean/.proof/rule edit (lake build 13 jobs green, git diff --stat aims-proof/ EMPTY, no .lean mtime-touched); no case-(b). CURE ATTEMPTED (REVERTED): a sharing_view field on EscapeSafeBorrowedNames (from crate::borrow::sharing_builtin_names SSOT ∪ take/drop), checked in borrowed_arg_release_verdict BEFORE the !dst_scalar gate returning EdgeRelease::Both (the slice result holds its own rc-inc’d ref keeping the buffer live past the relocated dec - same shape as clone) + the recv_has_freeable_dec gate widened to FatValue (str substring); + 2 clippy-driven refactors (recv_has_freeable_dec/apply_borrowed_arg_relocations/sharing_view_builtin_names helpers) to hold the 100-line cap. On-target the receiver-dead shapes went clean (slice_then_length/matrix_slice_in_scope: alloc rc=1, inc->2, dec->1, dec->0 FREE balanced). KILLING CLAUSE: full under-flag corpus comm -13 NON-EMPTY = 11 NEW: fat_ptr_iter::str_list::test_substring_repeat_one + slices::{test_list_drop_basic,test_list_drop_zero,test_list_slice_basic,test_list_slice_from_start,test_list_slice_full,test_list_slice_single_element,test_list_slice_to_end,test_list_take_all,test_list_take_basic,test_list_take_then_drop}; FIXED 3: fat_ptr_iter::str_list::test_substring_to_uppercase + rc_matrix::test_matrix_slice_in_scope + slices::test_list_slice_then_length. NET -3 +11. OVER-FIRE ROOT (list_slice_basic POST-CURE under flag - let ys=xs.slice(..); if ys.length()==3 && ys.first().unwrap()==20 && ys.last().unwrap()==40 then 0 else 1): the &&-branchy slice shapes read the slice result MULTIPLE times across &&-short-circuit branches, so the Both-edge receiver-dec relocation interacts with the slice result’s per-branch decs and nets a LEAK (rc=1 (live=1)). The Both-edge relocation is correct ONLY for the non-branchy single-use slice; the &&-branchy variants need per-path SINGLE-dominating-edge dec placement - the SAME M4-class CFG-dec-placement attempt-42 hit on f13_derived_eq. REVERTED clean by re-Editing (the sharing_view field + verdict + FatValue gate-widening + all 3 helpers removed; EscapeSafeBorrowedNames back to 4 fields; relocate fn body re-inlined; no git checkout/restore/reset/stash). Post-revert: default SET = base16 EXACT (comm -13+comm -23 both EMPTY, 16/2514); under-flag SET = base213 EXACT (comm -13+comm -23 both EMPTY, byte-clean to the attempt-43 floor); cargo check --workspace --tests 0; ori_arc 1620/0 debug + 1616/0 release (IDENTICAL to attempt-43); predicate_stack_probe 131/131 (attempt-43 floor, my 6 pins removed - no orphan red pins); clippy -D warnings clean (ori_arc + ori_llvm tests); §06 VF-1=0 default; lake build green (13 jobs) + git diff --stat aims-proof/ EMPTY; eval+LLVM parity untouched (probe-gated); prose-lint clean (3 touched files); public-repo hygiene clean (Spec: Annex E §AIMS RL-2 + RL-4 only; the EscapeSafeBorrowedNames + recv_has_freeable_dec inline local are PRE-EXISTING parallel-session code restored, not mine). 6 TDD pins authored + verified pre-cure (5 positives probe_slice_view_{list_slice,list_take,list_drop,str_substring,list_slice_then_fold}_receiver_dead_no_uaf FAILED = UAF/SIGSEGV + 1 negative probe_slice_view_non_sharing_borrowed_read_keep_negative [@length scalar borrow-read]; note: an earlier negative on the preserves_original xs-live-after-slice shape ALSO failed pre-cure - that shape is itself currently-broken &&-branchy, NOT a valid clamp, replaced before the attempt) then REMOVED on revert (no orphan red pins in the shared probe binary). Files-touched THEN-REVERTED: aims/realize/emit_unified.rs + its test sibling (borrow_survives_transform_names_* unit test) + predicate_stack_probe.rs. Session: NO net change (213 floor unchanged; the 3 fixed exactly cancel the 11 new on revert). A PARALLEL SESSION concurrently edits emit_unified.rs; my additions grep-confirmed removed. No parallel-session files touched; no Lean/test/gate weakened. Checkbox 2 stays UNCHECKED. NEXT LEAF: the seamless-slice cluster needs the SAME per-path SINGLE-dominating-edge dec placement (M4-class) the f13_derived_eq cluster needs - place ONE BurdenDec recv at the post-dominating dead block covering all paths the slice result is read on, NOT on BOTH the normal AND unwind successor edges (the non-branchy slice_then_length happens to have post-dominator == normal successor so Both works; the &&-branchy variants do not). This is the recurring M4 CFG-dec-placement class (attempt-42); the seamless-slice cluster is its second instance. The sharing_view-class recognizer (slice/take/drop/substring) BUILT here is the reusable name-set foundation the M4 placement would consume. AVOID the Both-edge path for any sharing-view callee until M4 lands. SECONDARY non-slice residuals to ground-truth next: apply_alias_coverage::test_apply_alias_conditional_intlist (1) / enum_discriminant::test_enum_rc_payload_narrowed_tag (1) / poly_lambda_mono 2 (multifile imported-generic + assert_eq confounder). Cross-ref: decisions/LEDGER.md §B.2 attempt-44 line.
2026-06-06 — Attempt 45: slices/fat_ptr_iter seamless-slice RECEIVER-dec M4 post-dominating single-edge placement CURED + KEPT (the attempt-44 NEXT-LEAF — EdgeRelease::PostDominator for sharing-view receivers, NOT the over-firing Both; scoped to the single-read non-branchy + single-read take/drop/substring subset via a result-spread guard + a chained-slice guard); 3 FIXED, ZERO new, under-flag 213→210. Fresh baseline rebuilt from disk (oric+ori_rt+aot-302aa53194d0e118, both baselines reproduced): default 16/2473 (§09-coupled EXACT, comm both EMPTY), under-flag 213/2473 floor (attempt-43 kept). ROOT (ground-truthed permanent surfaces ONLY — ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN + ORI_LOG=ori_arc::aims::realize=trace per-phase snapshot + ORI_TRACE_RC+ORI_CHECK_LEAKS on slice_then_length/slice_basic/preserves_original/take_then_drop): the misplaced burden_dec %recv is a Phase-5 op present in block 0 from after_phase_2_5_burden_elim on; PRE-merge @slice is an Invoke TERMINATOR so the dec lands in the block BODY before it (ORI_DUMP_AFTER_BURDEN showed no body dec because that dump precedes Step-9 merge_blocks, which runs AFTER the probe tail and folds the bb1-edge dec inline). Phase-6.65 relocate_borrowed_terminator_arg_dec_to_edges IS the surface (attempt-44 right); its Both over-fires not on the RECEIVER (its decs balance — oracle: bb1 normal + bb2 unwind) but by UNMASKING a latent slice-RESULT keep-alive leak: fixing the receiver UAF reveals the &&-branchy slice RESULT carries a RcInc multi-use keep-alive (RL-1) that nets +1 on the success path (slice rc=1, bb1 inc→2, recv-dec→1, result keep-alive inc/dec leaves rc 1 → LEAK size 40). The non-branchy single-read result has no keep-alive, so the receiver fix is the SOLE missing op. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL2_borrowed_param_emits_caller_dec (:220) + RL2_release_exactly_once (:239) + RL4_edge_release_balanced (:309) mandate the borrowed receiver’s single caller dec at its TRUE last use; the impl placed it before the read; NO .lean/.proof/rule edit (lake build 13 jobs green, git diff --stat aims-proof/ EMPTY, no .lean mtime-touched); no case-(b). CURE LANDED (KEPT, probe-gated → default byte-identical): sharing_view_relocation_names SSOT (crate::borrow::sharing_builtin_names ∪ take/drop) + EdgeRelease::PostDominator variant + sharing_view field on EscapeSafeBorrowedNames + verdict returns PostDominator for sharing-view callees before the !dst_scalar gate + NEW reusable PostDominatorTree::immediate_post_dominator accessor consumed by post_dominating_dead_block (walks the ipdom chain from the slice’s normal successor to the receiver’s dead-on-entry block; degenerates to the normal-successor for the dead-after-slice subset) + the PostDominator apply-arm places ONE dec at that post-dominating block PLUS the unwind edge (slice did not inc on the panic path) + recv_has_freeable_dec widened to non-Scalar FatValue (str substring) + SCOPE GUARDS that prevent the attempt-44 over-fire (lineage_reader_block_count(dst) > 1 declines the &&-branchy multi-read-result; sharing_view_result_feeds_sharing_view(dst) declines chained slices take().drop()) + clippy-driven extraction borrowed_terminator_arg_relocation_for_block. FIXED 3 verbatim (213→210, ZERO new): fat_ptr_iter::str_list::test_substring_to_uppercase + rc_matrix::test_matrix_slice_in_scope + slices::test_list_slice_then_length. Guardrails all clean (default-16 byte-identical both comm; ori_arc 1621/0 debug + 1617/0 release; predicate_stack_probe 137/137 [131 floor + 6 new]; rc_matrix 135/0; clippy -D warnings 0; §06 VF-1=0 default+under-flag; eval+LLVM parity exit-0 both backends; lake build 13 jobs; prose-lint 0; hygiene Spec: Annex E §AIMS RL-2 + RL-4 form only, M4 mechanism labels stripped from source; cargo fmt 0). 6 TDD pins matrix-first (4 positives FAILED=UAF pre-cure / PASS post: probe_sharing_view_{list_slice_then_length,list_take_dead_receiver,list_drop_dead_receiver,str_substring_then_transform}_no_uaf + 1 over-fire regression guard probe_sharing_view_list_slice_branchy_multi_read_no_uaf PASS pre/post [the slice_basic shape attempt-44’s Both broke; the result-spread guard keeps it correct] + 1 negative probe_sharing_view_non_sharing_borrowed_read_keep_negative PASS pre/post) + 2 ori_arc unit pins (sharing_view_relocation_names_covers_slice_substring_take_drop + the verdict assertion expecting PostDominator). Files-touched (all ori_arc/ori_llvm probe + graph): aims/realize/emit_unified.rs + graph/post_dominator.rs (immediate_post_dominator) + the test sibling emit_unified/burden_lowering_tests.rs + predicate_stack_probe.rs. A PARALLEL SESSION concurrently edits emit_unified.rs/burden_lowering_tests.rs; my additions grep-confirmed intact; cargo fmt mechanically fixed one pre-existing concurrent-session fmt violation adjacent to my import (benign). No parallel-session-owned files touched; no Lean/test/gate weakened; no git checkout/restore/reset/stash. NEXT LEAF: the &&-branchy multi-use-slice-RESULT keep-alive subset (slices::test_list_slice_preserves_original [also receiver live-out] + fat_ptr_iter::conversion::test_str_split_on_substring + the chained take().drop() family the guards decline) — the residual is the slice RESULT’s RL-1 multi-use keep-alive RcInc netting +1 on the success path, NOT the receiver placement (now fixed); needs a slice-result-lineage keep-alive accounting balancing the dup inc with ONE post-dominating release of the shared buffer where the result + every alias jointly die. The sharing_view_relocation_names recognizer + immediate_post_dominator/post_dominating_dead_block primitives BUILT here are the reusable foundation. Cross-ref: decisions/LEDGER.md §B.2 attempt-45 line.
2026-06-06 — Attempt 46: USER-function-call FRESH-owned-collection RESULT leak CURED + KEPT (clean single-mechanism cluster — a user fn builds + returns a fresh [T]/{K:V} [@to_array(list) -> [int] = [h, ...]], the caller dup-reads it [.len() + index] then it dies; the fresh-site burden_inc %result is SURPLUS over the alloc-aware net [alloc(+1)+inc(+1)−dec(−1)=+1] → result buffer leaks); 11 FIXED, ZERO new, under-flag 210→199. Fresh baseline rebuilt from disk (oric+ori_rt+aot-302aa53194d0e118, both baselines reproduced): default 16/2470 (§09-coupled EXACT, comm both EMPTY), under-flag 210/2470 floor (attempt-45 kept). LEAF picked after ground-truthing 6 candidates (realize_rc_reuse/narrowing derived-Eq = JOINT 3-mech per attempt-38, declined; cow_map_set/trmc &&-branchy mixed, declined; the TRMC size-32 [int]-result subset = clean). ROOT (ground-truthed permanent surfaces ONLY — ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN + ORI_TRACE_RC+ORI_CHECK_LEAKS on trmc_list_map_increment): the user-call collection result carries a surplus fresh-site inc; single-use nets 0 (why §07A passed). CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean rcBalance + RL2_release_exactly_once (:239) + rl2_emits_dec(.ScopeExit) (:185) ALREADY mandate the fresh-owned user-call result’s single scope-exit release; impl diverged (no candidate recognition for user-call results); NO .lean/.proof/rule edit (lake build 13 jobs green, git diff --stat aims-proof/ EMPTY, no .lean mtime-touched); no case-(b). CURE LANDED (KEPT, probe-gated → default byte-identical; extends the attempt-15/33/37 foundation, Invariant-5-clean): compute_fresh_owned_collection_reps gains a user_call_fresh_result(callee, args, dst) arm — a non-builtin (BuiltinOwnershipSets::is_builtin false) Apply/Invoke returning a collection (is_collection_dst) whose result does NOT same-alloc-merge any arg (the Direct-transfer-forwarder discriminator, the apply-Direct merge from attempt-37 inverted); compute_owned_collection_delta gains the matching user_call_allocates +1 for the same non-Direct user-call result (a forwarder returns an EXISTING alloc → no +1); same_alloc_reps threaded into both. The existing alloc-aware-net gate + ALL exclusions (returned/owned_consumed/user_call_args/forwarder_result single-sink/conversion-source/iter-element/borrowed) gate which actually leak so the net never fires on a double-free; a buffer-sharing-view result (@head(xs)=xs.slice(..)) carries no fresh-alloc +1 of its own → NOT over-freed (the slice-view NEGATIVE pin passes pre+post). FIXED 11 verbatim (210→199, ZERO new): arc::test_arc_borrowed_param_cow_push_str_list, drop_augment::drop_value_inside_for_yield_drops_on_collection_teardown, fat_ptr_iter::for_yield::test_for_yield_break_value, fat_ptr_iter::for_yield::test_for_yield_continue_value, generics::test_edge_for_yield_return_preserves_unwind_decs, generics::test_edge_project_return_not_param_keeps_outer_dec, narrowing::test_for_yield_str_with_narrowed_int_list, poly_lambda_mono::test_imported_generic_fn_struct, trmc::test_trmc_list_map_increment, trmc::test_trmc_list_map_two_args, trmc::test_trmc_reuse_pattern (the 3 targeted TRMC [int]-result fixtures + 8 cross-cluster IDs sharing the SAME user-call-fresh-collection-result mechanism — the for_yield::break_value/continue_value scalar-yield-result next-leaf from attempt-25/26, here a [int] from the for-yield ori_list_take flowing as a user-call-equivalent result). Guardrails all clean (default-16 byte-identical both comm; ori_arc 1622/0 debug + 1618/0 release; predicate_stack_probe 141/141 [137 floor + 4 new]; rc_matrix 135/0 + realize_rc_reuse 7/0; cargo check --workspace --tests 0; clippy -D warnings 0; §06 VF-1=0 default [burden-balance.sh 0 distinct]; eval+LLVM parity exit-0 both backends; lake build 13 jobs; prose-lint 0; hygiene Spec: Annex E §AIMS RL-2 form only). 6 TDD pins matrix-first (4 AOT: positives probe_user_call_fresh_{list,map}_result_dup_read_freed FAILED=leak pre-cure/PASS post + probe_user_call_fresh_list_result_single_read_freed single-use-no-leak clamp PASS pre/post + NEGATIVE probe_user_call_returns_borrowed_slice_view_no_double_free_negative PASS pre/post; 2 ori_arc unit: fresh_owned_collection_reps_classifies_user_call_result_and_excludes_direct_transfer + the reframed dead_owned_collection_frees_user_call_result_without_apply_direct_seed [the attempt-37 _skips_forwarder_result_without_apply_direct_seed pin reframed — my cure adds a second recognition path so the forwarder result is freed once via the user-call path even without the seed; both paths converge on exactly one release, never double-fire; the _with_apply_direct_seed companion still asserts 1 release with the seed; NOT a weakening]). Files-touched (all ori_arc/ori_llvm probe): aims/realize/emit_unified.rs + the test sibling emit_unified/burden_lowering_tests.rs + predicate_stack_probe.rs. A PARALLEL SESSION concurrently edits emit_unified.rs/burden_lowering_tests.rs; my additions intact. No parallel-session-owned files touched; no Lean/test/gate weakened; no git checkout/restore/reset/stash. Checkbox 2 stays UNCHECKED (PARTIAL — the recursive-Cons-InlineEnum-chain leak [size-24×N, trmc_deep_recursion/tree_mirror/shared_structure/multi_field_ctor] is the same user-call-fresh-RESULT mechanism for an [InlineEnum]/[AggFields] recursive aggregate not a collection — needs the user-call arm extended to the attempt-39 is_burden_carrying_aggregate candidate class with the field-walk net, the precise next leaf). Cross-ref: decisions/LEDGER.md §B.2 attempt-46 line.
2026-06-06 — Attempt 47: recursive-boxed-AGGREGATE RESULT + inline-Construct leak CURED + KEPT (attempt-46’s NEXT-LEAF, RECURSION-GATED — a fresh recursive boxed enum [@build_list -> List user-call result OR inline Construct Cons(.., Cons(..))], ValueRepr::Aggregate RcStrategy [InlineEnum], dup-read then dead; each Cons node is heap-boxed [alloc → rc=1], the dup-alias burden_inc/burden_dec pairs net the explicit ops to 0 leaving the node +1 unreleased → the [InlineEnum]-walked chain leaks size-24×N); 12 FIXED, ZERO new, under-flag 199→187. Fresh baseline rebuilt from disk (HEAD moved to 1fb0b424 — parallel-session commits past attempt-46’s 3266d4080; both baselines reproduced): default 16 (§09-coupled EXACT, comm both EMPTY vs scratch/leaf47/base_default.txt), under-flag 199 floor (attempt-46 kept). CALCULUS-vs-LEAF CORRECTION (decisive): attempt-46’s NEXT-LEAF “aggregates carry no self-buffer +1; the dec balances via the AggFields/InlineEnum drop-glue” is WRONG for a RECURSIVE enum — a boxed Cons node DOES self-allocate (alloc → rc=1), so its lineage +1 IS the node’s own buffer (same as a collection), NOT a field-walk-only balance; the no-self-buffer field-walk model applies ONLY to INLINE NON-RECURSIVE aggregates (Doc{content:str}, Config{settings,name}). CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean rcBalance + RL2_release_exactly_once (:239) + rl2_emits_dec(.ScopeExit) (:185) ALREADY mandate the boxed node’s single scope-exit release; impl diverged (no candidate recognition for Aggregate results); NO .lean/.proof/rule edit (lake build 13 jobs green, git diff --stat aims-proof/ EMPTY, no .lean mtime-touched); no case-(b). CURE LANDED (KEPT, probe-gated → default byte-identical; extends the attempt-15/33/37/46 dead-owned-collection foundation, Invariant-5-clean): new Pool::aggregate_type_is_recursive(idx) SSOT (ori_types nominal accessors — self-reference detection following nominal resolution with cycle detection) + new is_self_allocating_aggregate(var) = is_burden_carrying_aggregate ∧ aggregate_type_is_recursive; compute_fresh_owned_collection_reps (body-Construct insert-gate + user-call arm + Invoke gate) and compute_owned_collection_delta (3 arms) extended is_collection_dst → (is_collection_dst ∨ is_self_allocating_aggregate); compute_dead_owned_collection_releases no-use path GATED to skip ALL is_burden_carrying_aggregate reps (Phase-6.85 owns no-use aggregates → no double-fire; the two passes partition: 6.85 = no-use aggregates, 6.8 = USED aggregates + collections). OVER-FIRE CAUGHT + CURED (the RECURSION GATE, empirically forced): the FIRST cut gated on is_burden_carrying_aggregate ALONE → DOUBLE-FREE on Config{settings:{str:int}, name:str} (the attempt-41 probe_project_borrowed_view_paired_inc_collection_field_keep negative, exit 134) — an INLINE NON-RECURSIVE struct (no self-alloc; fields projected+freed in main) counted the Construct as +1 → spurious RcDec [AggFields] → double-free; gating on RECURSION excludes it (DEAD-END: is_burden_carrying_aggregate-alone, reverted before keeping; DO NOT RE-TRY). FIXED 12 verbatim (199→187, ZERO new): trmc::test_trmc_deep_recursion, trmc::test_trmc_multi_field_ctor, trmc::test_trmc_shared_structure, trmc::test_trmc_tree_mirror (the 4 leaf targets) + aims_interactions::test_h13_reuse_priority_over_drop_hint, aims_interactions::test_h18_drop_trmc_context_root_hint, aims_interactions::test_h20_trmc_tailcall_no_double_loop, aims_interactions::test_h4_fip_certified_recursive_rebuild, aims_interactions::test_h5_intra_trmc_reconvergence, recursive_derive::recursive_derive_eq_equal_chains_true_differing_false, recursive_derive::recursive_derive_eq_result_boxed_ok_compares_through_box, recursive_feature::recursive_feature_generic_box_two_instantiations (8 cross-cluster recursive-aggregate shapes — both user-call-result @build_list AND inline-Construct tree_mirror/shared_structure). trmc::test_trmc_nested_recursion correctly STAYS failing (the DISTINCT double-free, 134, scoped OUT — over-release, not a leak). Guardrails all clean (default-16 byte-identical both comm; ori_arc 1622/0 debug + 1618/0 release; ori_types 1054/0 lib; predicate_stack_probe 147/147 [141 floor + 6 new]; cargo check --workspace --tests 0; clippy -D warnings 0; §06 VF-1=0 default; eval+LLVM parity exit-0 both backends; lake build 13 jobs + aims-proof untouched; prose-lint 5 files 0; hygiene Spec: Annex E §AIMS RL-2 form only). 8 TDD pins matrix-first (6 AOT: 3 positives probe_user_call_fresh_recursive_enum_result_dup_read + probe_inline_construct_recursive_enum_dup_read + probe_recursive_struct_payload_enum_dup_read FAILED=leak pre-cure/PASS post + 3 NEGATIVES probe_user_call_returns_recursive_enum_no_double_free + probe_scalar_only_struct_dup_read + probe_inline_struct_multi_heap_field_projected [the Config over-fire boundary] PASS pre/post; 2 ori_types unit: recursive_enum_aggregate_is_recursive + inline_struct_with_heap_field_is_not_recursive). Files-touched: ori_types/src/pool/accessors/nominal.rs + ori_arc/src/aims/realize/emit_unified.rs + ori_llvm/tests/aot/predicate_stack_probe.rs + ori_types/src/triviality/tests.rs. A PARALLEL SESSION concurrently edits emit_unified.rs; my additions intact. No parallel-session-owned files touched; no Lean/test/gate weakened; no git checkout/restore/reset/stash. Checkbox 2 stays UNCHECKED (PARTIAL — the INLINE NON-RECURSIVE aggregate dup-read field-walk leak [Doc{content:str} dup-read, string_sso heap-in-struct] is the precise next leaf: a non-recursive aggregate USED-and-dead whose heap FIELD leaks; needs per-field release-state accounting [the Doc-fires-vs-Config-keeps discriminator], distinct from this leaf’s self-allocating-node +1 model). Cross-ref: decisions/LEDGER.md §B.2 attempt-47 line.
2026-06-06 — Attempt 48: FRESH-owned-str method-RESULT leak CURED + KEPT (clean single-mechanism cluster — a fresh-str-producing method [@debug() derived #[derive(Debug)] / @to_str() Printable] returns a fresh owned str, the caller dup-reads it across && short-circuit [let s = p.debug(); s.contains(..) && s.contains(..)] then it dies; the multi-use keep-alive RcInc %result is SURPLUS over the alloc-aware net [net +1] → the result fat-pointer buffer leaks); 4 FIXED, ZERO new, under-flag 187→183. Fresh baseline rebuilt from disk (oric+ori_rt+aot-302aa53194d0e118, both baselines reproduced): default 16 (§09-coupled EXACT, comm -13+comm -23 both EMPTY vs scratch/leaf48/base_default.txt), under-flag 187 floor (attempt-47 kept). LEAF picked after ground-truthing candidates: the generics::borrow_list_int_* cluster = &&-branchy multi-read-of-returned-list JOINT (inc → rc=3 (live=0) UAF-on-freed-address, declined); string_sso heap-multi-ref = &&-branchy str-LITERAL multi-ref JOINT (the a==b && a==".." heap-str-literal aliased 4× + heap_clone b=a.clone() where the literal a is the leak, declined); realize_rc_reuse/narrowing derived-Eq + cow_map_set &&-branchy = JOINT (declined). The fresh-str method-result is the clean single mechanism: single-read = exit 0 (clean, confirmed — the struct field-walk is NOT the leak), only the dup-read s leaks; the alloc-aware net handles the && dup-read (attempt-46 mechanism, NOT M4 CFG-dec-placement). ROOT (ground-truthed permanent surfaces ONLY — ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_ARC + ORI_TRACE_RC+ORI_CHECK_LEAKS on #[derive(Debug)] type Pair={first:str,second:str}; let s=p.debug(); s.contains(aaa) && s.contains(bbb) + a bare @make_label -> str): %5 = Apply/Invoke @debug(%4 [borrow]) is a fresh owned str; the dup-use marks it dup_alias_dst → keep-alive RcInc %5 (+1); the ORACLE emits RcDec %5 on both &&-branch sinks (freed), the BURDEN path’s freeing dec count does not match the keep-alive +1 so on every through-path %5 ends rc=1 (LEAK size 82). The bare @make_label user-fn str result was fixed FIRST by extending the attempt-46 user_call_fresh_result arm to str via is_collection_or_str_dst; the derived @debug()/@to_str() results stayed leaking because their interned method names are REGISTERED builtin borrowing methods (ori_registry::borrowing_method_names — debug/to_str exist for primitive/collection types) so BuiltinOwnershipSets::is_builtin returns true → the !is_builtin discriminator excluded them. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean rcBalance + RL2_release_exactly_once (:239) + rl2_emits_dec(.ScopeExit)=true (:185) ALREADY mandate the fresh-owned str result’s single scope-exit release; impl diverged (no candidate recognition for str method-results); NO .lean/.proof/rule edit (lake build 13 jobs green, git diff --stat aims-proof/ EMPTY, no .lean mtime-touched); no case-(b) scratch theorem (the shape is governed + proven — a @debug() result is a standard fresh owned str, RL-2 covers it). CURE LANDED (KEPT, probe-gated → default byte-identical; extends the attempt-15/33/37/46/47 dead-owned-collection foundation, no parallel emitter/shadow tracker — Invariant-5-clean): (1) the attempt-46 user_call_fresh_result recognizer arm + user_call_allocates delta arm + their Invoke-terminator dst_is_freeable gates extended is_collection_dst → is_collection_or_str_dst so a fresh str returned from a non-builtin USER fn (@make_label) joins the candidate set + alloc-aware net; (2) NEW fresh_str_producing_method_names SSOT (debug/to_str — pure-synthesis fresh-str builtin/derived methods, the str analogue of collection_conversion_names) wired into BOTH compute_fresh_owned_collection_reps (a body-Apply arm + the Invoke-terminator is_fresh branch) AND compute_owned_collection_delta’s allocates() predicate — these names ARE builtins (so the user_call_fresh_result !is_builtin arm excludes them) but their result genuinely allocates a fresh str, so they get their own name-set arm. The existing exclusions (returned/owned_consumed/user_call_args [already considers FatValue str args]/primop_operands [str + str concat is a PrimOp Binary(Add), structurally excluded]/conversion-source/iter-element/borrowed) gate which actually leak; the alloc-aware net guards double-free. EXCLUDES sharing-view str methods (slice/substring, in sharing_view_relocation_names — share the receiver buffer) and str + str concat (PrimOp, not an Apply to a named method). FIXED 4 verbatim (187→183, ZERO new): derives::test_aot_derive_debug_mixed_str_int_no_leak, derives::test_aot_derive_debug_multi_str_no_leak, narrowing::test_float_narrowed_derive_debug, narrowing::test_narrowed_derive_debug_negative_values (the 2 derives @debug() str-result targets + 2 narrowing derive(Debug) str-result leaks on narrowed-int structs — same fresh-str-method-result mechanism). Guardrails all clean (—test-threads 8, fresh-rebuilt binary): default-path SET = base16 EXACT (comm -13+comm -23 vs scratch/leaf48/base_default.txt BOTH EMPTY — probe-gated byte-identical); under-flag SET comm -13 vs scratch/leaf48/base_underflag_noprobe.txt EMPTY (ZERO new), net 187→183; cargo check --workspace --tests 0; ori_arc 1623/0 debug + 1619/0 release (+1 unit pin); predicate_stack_probe 152/152 (146 attempt-47 floor + 6 new str pins); rc_matrix 135/0 + realize_rc_reuse 7/0 (prior pins intact); clippy -D warnings 0 (ori_arc + ori_llvm tests); §06 VF-1=0 default (postprocess=warn 0 imbalances on cured Pair + mixed fixtures); lake build 13 jobs green + committed Lean/.proof/rule-files UNTOUCHED (git diff --stat aims-proof/ EMPTY, no .lean mtime-touched); eval+LLVM parity (cured Pair + mixed fixtures exit 0 on BOTH backends default path; probe-gated → eval untouched); prose-lint clean; public-repo hygiene clean (no attempt-N/§07B/BUG-XX-NNN/.claude/wrapper-path/LEDGER/M4 refs in MY added source — Spec: Annex E §AIMS RL-2 form only); cargo fmt 0. 6 TDD pins matrix-first (verified pre-cure): 5 AOT in predicate_stack_probe.rs — positives probe_user_call_fresh_str_result_dup_read_freed (bare @make_label) + probe_derive_debug_str_result_dup_read_freed (the Pair.debug() derived-method shape) FAILED=leak pre-cure / PASS post + probe_user_call_fresh_str_result_single_read_freed (single-read no-leak must-not-regress clamp — PASS pre AND post, net stays 0) + 2 NEGATIVES probe_user_call_returns_str_no_double_free_negative (a fresh str RETURNED onward, RL-2 transfer — must not be over-freed) + probe_str_arg_to_user_call_no_double_free_negative (a fresh str passed as an OWNED arg — compute_user_call_arg_lineages excludes FatValue args) PASS pre AND post + 1 ori_arc unit pin in emit_unified/burden_lowering_tests.rs — fresh_owned_collection_reps_includes_user_call_str_result (the %2 = @make_label(..) fresh str result is a candidate post-cure; FAILED pre-cure). Files-touched (2 production + 2 test, all ori_arc+ori_llvm probe): compiler/ori_arc/src/aims/realize/emit_unified.rs (fresh_str_producing_method_names + recognizer arm + Invoke is_fresh branch + delta allocates arm + the 4 is_collection_dst → is_collection_or_str_dst user-call-path gate widenings) + its test sibling emit_unified/burden_lowering_tests.rs (user_call_str_result_func builder + 1 unit pin) + compiler/ori_llvm/tests/aot/predicate_stack_probe.rs (6 pins). A PARALLEL SESSION concurrently edits emit_unified.rs/burden_lowering_tests.rs; my additions grep-confirmed intact. No parallel-session-owned files touched (lexer/parse/types-inference/eval/llvm-incremental/context/monomorphize/repr/rt/oric/docs untouched by me); no Lean/test/gate weakened; no git checkout/restore/reset/stash. Checkbox 2 stays UNCHECKED (PARTIAL — 183 under-flag failures remain). NEXT LEAF: the INLINE NON-RECURSIVE aggregate dup-read field-walk leak (Doc{content:str} dup-read — a non-recursive struct USED-and-dead whose heap FIELD leaks, the attempt-47 next-leaf still open; needs per-field release-state accounting, the Doc-fires-vs-Config-keeps discriminator) OR the concat/rc_matrix::matrix_str_* str + str PrimOp-Add buffer-provenance recognizer (flagged risky — same_alloc_reps Let-Var-only, operand-buffer reuse invisible). The fresh_str_producing_method_names recognizer extension landed here is reusable for any builtin/derived method returning a fresh owned str not yet in the set. Cross-ref: decisions/LEDGER.md §B.2 attempt-48 line.
2026-06-06 — Attempt 49: USED-and-compared aggregate-with-heap-field a == b leak CHARACTERIZED (no edit, ZERO source change, 183 floor preserved). The fat_matrix::f13_derived_eq (14 IDs) + f20_derived_clone (4 IDs) = 18-ID cluster is ONE mechanism, ground-truthed uniform (gt.sh all 1 RC allocation(s) not freed). Fresh baselines rebuilt-binary-confirmed: default 16/2473 EXACT (comm both EMPTY vs scratch/leaf_inline/base_default.txt), under-flag 183/2473 (attempt-48 floor reproduced). ROOT (ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 + ORI_TRACE_RC+ORI_CHECK_LEAKS on #derive(Eq) type Doc={content:str}; if a==b then (if a!=c then 0 else 1) else 2 + the f20 a.clone() sibling): the leaked alloc is %1’s 30-byte str field. The oracle emits ONE keep-alive RcInc %1 net-0 (3 aggregates freed); the BURDEN path emits THREE incs — %9 = %1/%12 = %1 aliases are classified dup_alias_dst (use_counts(%1) >= 2 at compute_use_counts_and_dup_aliases burden_lower/mod.rs:943) so each gets a SPURIOUS keep-alive BurdenInc even though %9/%12 are consumed ONLY at the ==/!= PrimOp{Binary(Eq|NotEq)} (a BORROW-READ, RL-1 incElidable) → bb1 net +1 → %1 field LEAKS. The attempt-47/48 “inline-non-recursive field-walk” framing was RE-CHARACTERIZED: ground-truth proved the SINGLE-call Doc dup-read is CLEAN under-flag (exit 0), so the leak is the MULTI-use keep-alive net imbalance, IDENTICAL to f13/f20 — NOT a no-use field-walk. KILLING CLAUSE (CHARACTERIZED, not KEPT): the cure is JOINT M2+M3+M4 in LOCKSTEP and the dominant M3 (suppress comparison-operand keep-alive inc) lives in dup_alias_dsts (burden_lower), which runs in BOTH default AND under-flag → NOT probe-gateable (default would not stay byte-identical, which the mission requires); M3-alone is net-unsound (orphans the M2 construct-site RcInc %1 or double-frees bb1); the matched inc+dec pair (net-0 per RL1_duplication_balanced) must be coordinated with M4 then-vs-else dec placement (immediate_post_dominator). CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL1_emit_iff_not_elidable (:122) + RL1_duplication_balanced (:129) + RL2_release_exactly_once (:239) ALREADY govern; the dup_alias_dsts classifier is the bug (a borrow-read comparison operand is not a duplication); NO .lean/.proof/rule edit (zero edits made), no case-(b). No TDD pins authored (CHARACTERIZED — orphan red pins would break default byte-identity). NEXT LEAF: the M3+M2+M4 LOCKSTEP for the ==/!= comparison-operand keep-alive, implemented IN emit_burden_path_probe_tail (NOT burden_lower): identify each Let{dst, value:Var(src)} whose sole consumer is a Binary(Eq|NotEq) operand; strip the spurious BurdenInc dst + its paired last-use BurdenDec dst together; re-place the construct-site keep-alive BurdenInc src to pair with the lineage TRUE last-use via immediate_post_dominator; GATED by the alloc-aware field-net extended to the inline-non-recursive is_burden_carrying_aggregate ∧ ¬is_self_allocating_aggregate class so Config{settings,name} (fields projected+freed, net 0) does NOT fire (the attempt-41 inline-struct negative pin + Config boundary MUST hold). Composes the landed alloc-aware foundation (attempts 15/33/37/46/47/48) + immediate_post_dominator (attempt-45) + recursion-gate (attempt-47). Cross-ref: decisions/LEDGER.md §B.2 attempt-49 line.
2026-06-06 — Attempt 50: the attempt-49 comparison-operand keep-alive cure LANDED + RECURSION-GATED + KEPT — 23 FIXED (the full f13(14)+f20(4)=18 cluster + 5 cross-cluster), ZERO new, under-flag 183→160. Ground-truth (ORI_DUMP_AFTER_ARC oracle-vs-flag on #derive(Eq) type Doc={content:str}; if a==b then (if a!=c then 0 else 1) else 2): the burden path emits spurious operand-alias incs RcInc %9(bb0)+RcInc %12(bb1) (the %9=%1/%12=%1 dup_alias_dst aliases consumed only at ==/!=, RL-1 borrow-read = incElidable) PLUS a misplaced RcDec %1 on bb1(then); /calc then=+1, else=+1 LEAK. ATTEMPT-49 M2-PRESCRIPTION CORRECTED: the construct keep-alive RcInc %1 is ALREADY correctly placed (byte-matches oracle) — NO immediate_post_dominator re-placement needed; the cure is M3 (strip operand INCS, KEEP their paired DECS — the operand dec balances the construct keep-alive) + M4 (strip the misplaced then-branch whole-var RcDec %1 only); /calc cured then=0 / else=0, byte-matches oracle. This supersedes the attempt-42 killing clause (strip operand incs ALONE → then −1 double-free) — the M4 then-dec-strip is what makes it net 0. CURE: probe-tail Phase 6.97 strip_comparison_operand_keepalive (+ split compute_comparison_operand_keepalive_strips/compute_comparison_operand_aliases/compute_comparison_operand_dec_strips/whole_var_dec_or_inc), gated behind predicate_stack_rc_disabled after Phase 6.96 before Phase-7 lowering, Invariant-5-clean. OVER-FIRE caught + cured: the no-recursion-gate first cut BROKE 2 NEW (recursive_derive::recursive_derive_eq_{equal_chains_true_differing_false,result_boxed_ok_compares_through_box} — a recursive Node{value, next:Option<Node>} multi-node alloc chain whose operand decs + whole-var decs target distinct allocations resolve_root collapses → RcDec %7/%30 emitted TWICE, double-free exit 134); CURE = gate M3+M4 by !is_self_allocating_aggregate(root) (pool.aggregate_type_is_recursive, the attempt-47 recursion-gate). DEAD-END (DO NOT RE-TRY): the no-recursion-gate cut → 2 NEW recursive-derive double-frees. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL1_emit_iff_not_elidable (:122) + RL1_duplication_balanced (:129) + RL2_release_exactly_once (:239) ALREADY govern; the dup_alias_dsts classifier is the bug; NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY, lake build 13 jobs green, no .lean mtime-touched), no case-(b). Guardrails all clean (fresh-rebuilt aot-302aa53194d0e118, —test-threads 8): default 16 EXACT (comm -13+comm -23 BOTH EMPTY — probe-gated byte-identical); under-flag comm -13 EMPTY (ZERO new), 183→160; cargo check --workspace --tests 0; ori_arc 1626/0 debug + 1622/0 release (+3 unit pins); predicate_stack_probe 159/159 (+7 comparison-operand pins); rc_matrix 135/0; clippy -D warnings 0 (refactored the compute fn into 3 helpers to clear cognitive-complexity-25 + 100-line caps); §06 VF-1=0 default + under-flag; eval+LLVM parity (cargo st 4629/45 EXACT — probe-gated, eval untouched); prose-lint clean; public-repo hygiene clean. 10 TDD pins matrix-first (7 AOT in predicate_stack_probe.rs — 5 positives + probe_config_projected_fields_compared_keep_negative + probe_derived_eq_single_comparison_keep_negative; 3 ori_arc unit in burden_lowering_tests.rs). Files-touched: compiler/ori_arc/src/aims/realize/emit_unified.rs (Phase 6.97 + 4 split fns) + its test sibling + compiler/ori_llvm/tests/aot/predicate_stack_probe.rs. UNCOMMITTED in-tree (cross-scope dirty-tree, DID NOT COMMIT); no Lean/test/gate weakened; no git checkout/restore/reset/stash. Checkbox 2/3 stays PARTIAL (160 under-flag failures remain). NEXT LEAF: the a.clone(); a == b clone-borrow-alias UNDER-emission (an ADJACENT shape NOT in the 18-cluster — when a is borrowed by BOTH @clone(%3 [borrow]) AND a == operand, the construct keep-alive bumps for two borrowed reads but only the == operand dec balances; the oracle emits RcDec %3 on BOTH clone-normal + clone-unwind edges, the burden path is MISSING it — an under-emission, distinct from the over-emission M3/M4 cures). The compute_comparison_operand_aliases/compute_comparison_operand_dec_strips + recursion-gate foundation is reusable. Cross-ref: decisions/LEDGER.md §B.2 attempt-50 line.
2026-06-06 — Attempt 51: the attempt-50 NEXT-LEAF a.clone(); a == b clone-borrow-alias UNDER-emission — Phase-6.98 clone-borrow edge-release CURE BUILT + correct + guardrail-clean, but CORPUS-ABSENT (net 160→160, ZERO corpus drop): REVERTED byte-clean, CHARACTERIZATION-ONLY. Fresh baselines rebuilt-binary-confirmed (oric+ori_rt+aot-302aa53194d0e118, —test-threads 8): default 16 (§09-coupled EXACT, comm both EMPTY vs scratch/leaf51/base_default.txt), under-flag 160 floor (attempt-50 reproduced exactly). GROUND-TRUTH (ORI_DUMP_AFTER_ARC oracle-vs-flag + ORI_DUMP_AFTER_BURDEN Phase-5 + ORI_CHECK_LEAKS on synthetic #derive(Eq,Clone) type Doc={content:str}; let b=a.clone(); if a==b then 0 else 1): %1.content (size 30) leaks. Oracle bb1(clone-normal) RcDec %3+RcDec %6+RcDec %7 (%3=%6=%1 aliases, TWO %1-lineage releases); burden bb1 has ONLY RcDec %6+RcDec %7 — MISSING RcDec %3 (the @clone(%3 [borrow]) clone-borrow alias). The construct keep-alive RcInc %1 covers TWO borrowed reads (%3 clone + %6 compare) but the burden path releases %1 once; /calc bb1 net oracle 0 vs burden +1 LEAK. ROOT-CAUSE (ORI_DUMP_AFTER_BURDEN): Phase-5 emits %3’s burden_inc/burden_dec SAME-BLOCK pair in bb0 (before the clone borrow); Phase-7 elidable_fresh_incs eliminates the net-0 pair → keep-alive unbalanced for the clone-borrow read. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL1_emit_iff_not_elidable (:122) + RL2_borrowed_param_emits_caller_dec (:220) + RL4_borrowed_no_edge_dec/RL4_edge_release_balanced (:302/:309) + RL2_release_exactly_once (:239) MANDATE the missing edge dec; NO .lean/.proof/rule edit, no case-(b). CURE BUILT (probe-tail Phase 6.98 emit_clone_borrow_alias_edge_release gated behind predicate_stack_rc_disabled, after Phase 6.97 before Phase-7): fires when a clone-borrow alias %a=%src (Aggregate, sole non-RC leaf use = a Borrowed Invoke arg) whose %src root is used as BOTH a borrowed-Invoke read AND a ==/!= operand (exactly 2 root leaf uses), carries a construct keep-alive inc, !is_self_allocating_aggregate, AND the clone RESULT is COMPARED-ONLY (no re-read) → emit BurdenDec %a on the clone Invoke’s normal + unwind successor heads. VERIFIED: clone_eq/b==a → exit 0 FIXED; the result-re-read shape (real f20 fixture) STAYS exit 0 (compared-only gate skips — the %4 re-read frees the shared str field via an extended lifecycle; adding a dec would double-free); pure double-comparison STAYS exit 0. KILLING CLAUSE (CHARACTERIZED, not KEPT): the inline-aggregate clone-borrow-compared-only shape is CORPUS-ABSENT — under-flag 160→160 (comm -13+comm -23 BOTH EMPTY = zero new, zero fixed). The actual AOT-corpus clone-borrow failures are ALL str-FatVal &&-branchy (string_sso::{test_heap_clone[a==b && a==lit],test_heap_clone_independence,test_heap_multiple_references[a aliased 3×+&&],test_heap_iteration[for-loop]} — the mission-declined string_sso &&-branchy cluster) OR a DISTINCT dec-before-borrow double-free; the f13/f20 corpus fixtures all re-read b and are already attempt-50-fixed. REVERTED byte-clean (default 16 + under-flag 160 BOTH re-confirmed EXACT post-revert on rebuilt aot-302aa53194d0e118, comm -3 EMPTY both; ori_arc 1626/0 debug intact); the 5 built TDD pins removed with the cure (orphan red pins break default byte-identity per mission). DEAD-END (DO NOT RE-TRY): the inline-aggregate clone-borrow-compared-only Phase-6.98 cure — correct + guardrail-clean but corpus-absent. NEXT LEAF: the DISTINCT clone-borrow dec-before-borrow DOUBLE-FREE (let b=a.clone(); if b==b/b==c, clone-only, a NOT compared — %3’s RcDec placed BEFORE the @clone borrow read → exit 134, a dec-PLACEMENT bug; needs relocation not addition) + @dup(d:a) owned-callee leak (neg4); SECONDARY the residual 160 NON-&& clusters (fat_ptr_iter 23 / generics 25 / arc 13 / rc_matrix 10). REQUIRED before any clone-borrow re-attempt: ground-truth the chosen shape is IN the corpus (run the actual failing fixture under flag) BEFORE building — attempt-51’s lesson is a correct cure on a corpus-absent shape lands zero drop. Cross-ref: decisions/LEDGER.md §B.2 attempt-51 line.
2026-06-06 — Attempt 52: the fat_ptr_iter::conversion::test_derive_clone_* (5) derived-Clone-of-aggregate borrowed-clone-arg DEC-PLACEMENT cure — Phase-6.65 clone_heap_aggregate relocation arm BUILT + correct + guardrail-clean on the ISOLATED no-loop shape, but CORPUS-ABSENT-as-isolated (net 160→160, ZERO corpus drop): REVERTED byte-clean, CHARACTERIZATION-ONLY. Fresh baselines rebuilt-binary-confirmed (oric+ori_rt+aot-302aa53194d0e118, —test-threads 8): default 16 (§09-coupled EXACT, comm both EMPTY vs scratch/leaf52/base_default.txt), under-flag 160 floor (attempt-50 reproduced exactly). LEAF = the only coherent single-mechanism sub-cluster of the fresh under-flag set (fat_ptr_iter::conversion::test_derive_clone_{result_str_int,result_str_str,slice_str_option,slice_str_struct,slice_str_tuple}, 5; all burden-path-only, all #derive(Clone) of an inline heap-bearing struct). GROUND-TRUTH (ORI_DUMP_AFTER_BURDEN+ORI_DUMP_AFTER_ARC+ORI_TRACE_RC+ORI_CHECK_LEAKS on a MINIMAL no-loop synthetic let w=Wrapper{s:p,n:p.len()}; let copy=w.clone()): no-loop reproduced exit-134 double-free under flag, default clean. ROOT (no-loop): lower/burden_lower/emit.rs::emit_terminator_burden_decs places BurdenDec %w [AggFields] INLINE in the block BODY before the Invoke @clone(%w [borrow]) normal/unwind terminator (the borrowed-Invoke-arg suppression is empty under the probe per emit.rs:160), freeing %w’s str field BEFORE the clone deep-copies it → the copy reads freed memory + double-free. ORACLE: RcDec %w [AggFields] on BOTH clone successor edges (RL-4), AFTER the borrow read. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL4_borrowed_no_edge_dec/RL4_edge_release_balanced (:302/:309) + RL2_borrowed_param_emits_caller_dec (:220) + RL2_release_exactly_once (:239); NO .lean/.proof/rule edit, no case-(b). CURE BUILT (probe-tail Phase-6.65 extension): added a clone_heap_aggregate arm to borrowed_terminator_arg_relocation_for_block’s recv_has_freeable_dec gate (emit_unified.rs) — survives_transform.contains(callee) ∧ is_burden_carrying_aggregate(recv) ∧ !is_self_allocating_aggregate(recv); threaded pool through the relocate fn + the per-block fn (probe-tail caller + 8 existing unit-test call sites in lockstep); the existing EdgeRelease::Both machinery strips the inline body dec + inserts BurdenDec %w at both successor heads (byte-matched the oracle on no-loop). VERIFIED: no-loop synthetic → exit 0 FIXED under flag, default still exit 0. KILLING CLAUSE (CHARACTERIZED, not KEPT): the 5 CORPUS fixtures STILL double-free under flag post-cure — corpus drop ZERO (comm -23 excl. own pin EMPTY). The corpus derive_clone_* fixtures are JOINT: each wraps the clone in for p in text.split(sep:",") do { let w=Struct{field:p,...}; w.clone() }, so the str field p is an ITER-ELEMENT SEAMLESS-SLICE sharing the text source backing — the corpus double-free is a SECOND mechanism (the Wrapper’s RcDec [AggFields] over-decs the size-90 SHARED text backing across loop iterations; ORI_TRACE_RC: 0x..2c0 size=90 rc=0 FREE then a later dec double-frees it, confirmed identical on struct+option fixtures). My clone-borrow-dec-placement cure fixes the ISOLATED no-loop shape, but that shape is CORPUS-ABSENT (every corpus clone fixture has the loop+slice-share joint). REVERTED byte-clean (default 16 + under-flag 160 re-confirmed EXACT post-revert on rebuilt aot-302aa53194d0e118, comm -13+comm -23 EMPTY both directions; ori_arc 1626/0 debug + 1622/0 release intact); the 7 AOT pins + 2 ori_arc unit pins + the clone_borrowed_aggregate_func builder removed with the cure. DEAD-END (DO NOT RE-TRY): the isolated derived-Clone-of-aggregate borrowed-clone-arg dec-placement relocation — correct + guardrail-clean but CORPUS-ABSENT-as-isolated. NEXT LEAF: the ITER-ELEMENT SEAMLESS-SLICE-into-AGGREGATE over-dec (the actual corpus mechanism) — the loop element p is a slice (SLICE_FLAG cap) sharing the source text backing; the burden path’s aggregate-field drop DECS the shared backing once per iteration → N decs double-free the single text allocation; needs the aggregate-field drop to recognize a slice-cap field as a SHARED borrow (no per-field dec). TWICE-CONFIRMED LESSON (51+52): ground-truth the EXACT corpus-fixture leak (run the ACTUAL loop fixture under flag + ORI_TRACE_RC to the double-freed ADDRESS+SIZE) BEFORE isolating a synthetic — a no-loop synthetic that removes the loop’s slice-sharing reproduces a DIFFERENT (real but corpus-absent) bug. Checkbox stays PARTIAL (160 under-flag failures remain). Cross-ref: decisions/LEDGER.md §B.2 attempt-52 line.
2026-06-06 — Attempt 53: ITER-ELEMENT SEAMLESS-SLICE-into-AGGREGATE-FIELD under-emission (the 5 fat_ptr_iter::conversion::test_derive_clone_* actual corpus mechanism, attempt-52’s NEXT LEAF) CURED + KEPT. Ground-truthed the ACTUAL corpus fixture (derive_clone_slice_str_struct, NOT a synthetic) under ORI_DISABLE_PREDICATE_STACK_RC=1 + ORI_TRACE_RC+ORI_CHECK_LEAKS: double-freed alloc = the %text backing 0x..2c0 size=90 (exit 134). The loop slice element p (Project @__iter_next.1, a Borrowed view in collect_iter_element_defs, excluded from owned_vars_needing_rc) is stored as a heap field of a #derive(Clone) aggregate; the aggregate’s RcDec [AggFields]/[InlineEnum] walks the field + decs the shared backing once per iter, but the burden path omits the RL-1 keep-alive inc on the slice -> per-iter %text-net 0−1=−1 (oracle +1−1=0) -> rc 0 early -> double-free. ORACLE (ORI_DUMP_AFTER_ARC default): RcInc %23 [FatPtr] before Construct Struct(Wrapper)(%23,%25), balanced by Wrapper RcDec %28 [AggFields] + clone RcDec %32 (clone dec balanced by clone-internal deep-copy inc). ROOT = a MISSING RL-1 keep-alive inc (the directive’s SUPPRESS framing and ADD-INC both balance, but the oracle uses ADD-INC -> CP-1 case-(a) mandates conforming to it). CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL1_emit_iff_not_elidable (:122) + RL2_release_exactly_once (:239) + RL4_edge_release_balanced (:309); NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY, Realization.lean untouched, lake build 13 jobs GREEN); no case-(b). CURE (probe-tail Phase 6.68 emit_slice_element_aggregate_field_keepalive_inc + recursive aggregate_transferred_out, gated behind predicate_stack_rc_disabled, after Phase 6.67): a Construct/Reuse whose dst is_burden_carrying_aggregate AND is DROPPED IN-SCOPE (!aggregate_transferred_out — the gate FOLLOWS parent-Construct/Reuse consumption to the OUTERMOST aggregate, so a NESTED MaybeNamed { name: Some(p) } fires on the inner Some(p) while a moved-into-collection for p in parts yield Some(p) / returned / user-call-arg aggregate is skipped) with a collect_iter_element_defs RcPointer|FatValue field arg -> emit one keep-alive BurdenInc <slice> before the Construct (byte-matches oracle RcInc %23). OVER-FIRE caught + cured mid-leaf: the first gate (no transfer-out check) ADDED 2 new test_str_split_in_{option,tuple}_list leaks (for p in parts yield Some(p) pushes the aggregate [own] into a collected list via @ori_list_push, field-drop runs LATER via the list elem_dec_fn -> orphaned +1, 0x..2c0 size=75 unfreed); the second gate (immediate-Construct transfer-out only) regressed the nested option/tuple/result corpus; the recursive-to-outermost gate cures both. GUARDRAILS CLEAN (freshly-rebuilt binary): default-path SET base16 EXACT both directions; under-flag 160->155 (comm -13 EMPTY = zero new; the 5 test_derive_clone_{result_str_int,result_str_str,slice_str_option,slice_str_struct,slice_str_tuple} FIXED); cargo check --workspace --tests 0; ori_arc 1626/0 debug + 1622/0 release; lake build 13 jobs GREEN + aims-proof diff EMPTY; clippy -D warnings clean (ori_arc + ori_llvm, merged identical match arms); prose-lint + test-weakening + test-naming + sprawl-lint clean; predicate_stack_probe 165/0 (159 prior + 6 new) + rc_matrix 135/0 all prior pins GREEN. TDD-matrix-first: 4 AOT positives (probe_slice_element_into_{struct,option,tuple,result}_field_no_double_free, FAILED=double-free pre-cure -> PASS post) + 2 negatives (probe_owned_collection_field_into_struct_negative [owned [int] field already has its own inc] + probe_slice_element_scalar_use_only_negative [slice p.len()-only, no aggregate store], PASS pre AND post). UNCOMMITTED in-tree. NEXT LEAF: the moved-out-aggregate element accounting (the collected-list elem_dec_fn element-release for for p in parts yield Some(p)/(p,..) — the distinct under-emission this leaf’s transfer-out gate DEFERS, net-0-by-both-missing pre-cure so corpus-passing today, NOT in scope here) + the corpus-ABSENT-as-isolated owned-FRESH-literal-aggregate-field clone shape (Tag { label: <str-literal> }; .clone(), 0x..2c0 size=56 double-free, missing FRESH-literal Construct-arg inc — a DIFFERENT site than the Borrowed-slice-view). SECONDARY: residual 155 clusters (generics 27 / fat_ptr_iter 18-remaining / arc 13 / fat_matrix 11 / rc_matrix 10 — NON-&&-branchy single-mechanism, ground-truthed on ACTUAL fixtures). Checkbox 2 stays PARTIAL (155 under-flag remain). Cross-ref: decisions/LEDGER.md §B.2 attempt-53 line.
2026-06-06 — Attempt 54: generics::test_borrow_list_int_*_then_return TRANSFER-THROUGH-RETURN dup-alias-SOURCE over-dec CHARACTERIZED; the callee-only Phase-6.99 strip BUILT + correct-in-isolation + REVERTED (guardrail-1 corpus over-fire — JOINT shape, 9 regressions). FRESH baselines rebuilt-binary-confirmed: default-path 16 EXACT + under-flag 155 EXACT (attempt-53 floor; both comm directions vs scratch/leaf54/base_*.txt EMPTY). LEAF = largest residual cluster generics (27), dominant sub-shape test_borrow_list_int_*_then_return_no_leak (9). GROUND-TRUTH on ACTUAL corpus fixtures (borrow_list_int_determinism_then_return UAF exit 134 0x..2c0 size=24; borrow_list_int_if_arm_use_then_return leak exit 1) under flag + ORI_TRACE_RC+ORI_DUMP_AFTER_BURDEN/ORI_DUMP_AFTER_ARC: the CALLEE returns its [int] param; the burden walk emits a terminal burden_dec %3 on the Let-alias SOURCE %3 of the Return value %8=%3 (a dup_alias_dst, %3 used >= 2), freeing the returned buffer before the caller reads it. ROOT: %8’s dup keep-alive inc is transfer-suppressed (terminator-transfer seed into compute_transfer_via_move_alias → inc_suppressed_vars) but compute_transfer_via_move_alias (mod.rs:818) only follows MOVE-alias edges (use_counts(src)==1, :845), so %3 (used twice) keeps its orphaned last-use dec (emit.rs:475). The completeness dec is GATED predicate_stack_rc_disabled (default emits none). CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean rl2_use_transfers_ownership(.Return)=true (:175) + RL2_transfer_kinds_no_dec (:199) + RL2_release_exactly_once (:239) + RL4_jump_arg_exempt (:297); the Lean is CORRECT, the impl over-emits. NO .lean/.proof/rule edit (aims-proof diff EMPTY, Realization.lean untouched). CURE (probe-tail Phase 6.99 strip_transfer_through_return_source_decs, gated predicate_stack_rc_disabled, after Phase 6.97): strip BurdenDec src where Let{dst,Var(src)} has rep_of(dst)∈compute_returned_lineages (jump-threaded: direct Return + Jump-arg→Owned-param→Return) ∧ src used >= 2 ∧ dst has no surviving BurdenInc. The cure CORRECTLY fixed the callee in isolation (callee RcDec %3 removed, returns rc=1; det symptom flipped UAF→3-allocation leak). KILLING CLAUSE (REVERTED, guardrail-1): the shape is JOINT — @main emits keep-alive RcInc %6/%14/%22 (protecting each user-call result across the next Invoke, an extra inc the oracle lacks) whose final balancing dec the prior (buggy) callee over-free supplied; stripping ONLY the callee half orphaned the caller incs → 9 GENUINE corpus regressions (8 generics::* IDs that were PASSING under the flag + probe_multi_borrow_then_return_no_double_free_negative; ORI_CHECK_LEAKS=1 exit 2, 3-allocation leak per fixture). REVERTED CLEAN (re-Edit removed wiring + both fns + 6 TDD pins; byte-state == fresh baseline: under-flag 155 + default 16 both comm directions EMPTY; ori_arc 1626/0 debug; cargo check --workspace --tests 0; aims-proof diff EMPTY). TDD-matrix-first (verified pre-cure, removed on revert): 4 AOT positives + 2 negatives. NEXT LEAF: land the JOINT AS A JOINT — the callee transfer-through-return source-dec strip (Phase 6.99) TOGETHER with the caller-side keep-alive-inc balance (the @main RcInc %6 keep-alive needs a matching final RcDec per result, an alloc-aware-net release at the borrowed-read scope-exit sink; the %6 aliases are len/__index borrow-args, NOT Binary(Eq|NotEq) operands → distinct from the Phase-6.97 comparison-operand strip). Both halves net the lineage to 0; either alone unbalances. SECONDARY: residual 155 clusters (fat_ptr_iter 18 / arc 13 / fat_matrix 11 / rc_matrix 10). DO NOT re-try the isolated callee-only strip. UNCOMMITTED in-tree (REVERTED — zero net source change). Checkbox 2 stays PARTIAL (155 under-flag remain). Cross-ref: decisions/LEDGER.md §B.2 attempt-54 line.
2026-06-06 — Attempt 55: the transfer-through-return JOINT (callee source-dec strip Phase-6.98 + caller keep-alive-inc Phase-6.99) BUILT TOGETHER + REVERTED (guardrail-1 over-fire); attempt-54’s caller-half framing CORRECTED. FRESH baselines rebuilt-binary-confirmed (oric+ori_rt+aot-302aa53194d0e118, —test-threads 8): default-path 16 + under-flag 155 EXACT (comm both directions vs scratch/leaf54j/base_*.txt EMPTY). DECISIVE GROUND-TRUTH (permanent tools): the JOINT is TWO INDEPENDENT bugs. (1) CALLEE over-dec (attempt-54’s, two sub-shapes: Let-alias-chain a2=a1=xs AND phi-block-param if_arm_use). (2) CALLER bug INDEPENDENT of callee — ISOLATED via a synthetic CLEAN callee (@clean_borrow returns param directly) with N-call dup-read @main: 1-call PASS, 2-call PASS, 3-call SEGV — ORI_DUMP_AFTER_ARC oracle-vs-flag per result: oracle RcInc=2/RcDec=4, under-flag RcInc=1/RcDec=9 — the burden path UNDER-emits the RL-1 keep-alive inc (1 vs 2) per may-unwind borrowed read while the edge-cleanup decs correctly on each dying edge → normal-path over-free. SUPERSEDES attempt-54’s “add one final dec” caller framing: the caller MISSES keep-alive INCS per-path (one per may-unwind borrowed read of the result), NOT a final dec. ORI_DUMP_AFTER_BURDEN shows emit_burden_ops emits ZERO ops for the user-call result — its RC is DEFERRED to emit_edge_cleanup(burden_only=true) (Phase 6.5, blocks 4+13 via realize=trace per-block multiset), same class as the §09.2 deferral finding. CALCULUS: pure case-(a) impl-conformance — Realization.lean RL1_emit_iff_not_elidable(:122) + rl2_use_transfers_ownership(.Return)/RL2_transfer_kinds_no_dec(:175/:199) + RL2_release_exactly_once(:239) + RL4_edge_release_balanced(:309); NO .lean/.proof/rule edit (aims-proof diff EMPTY). JOINT BUILT (probe-tail, both gated predicate_stack_rc_disabled): Phase 6.98 strip_transfer_through_return_source_decs (callee) + Phase 6.99 emit_invoke_result_borrowed_read_keepalive_inc (caller); cargo check -p ori_arc clean. KILLING CLAUSE (REVERTED, guardrail-1 OVER-FIRE — verbatim): under-flag 155→363 (+209 NEW), default-path 16→61 (+45 NEW — the JOINT BROKE THE DEFAULT PATH despite both phases being probe-gated, anomalous; +209 under-flag is the reproducible kill). Broke the SAME borrow_list_int equilibrium cluster attempt-54 broke (callee strip too broad — flipped use_twice/multi_let_alias_chain/one_borrow_apply/two_borrow_applies/project_consumer/use_thrice/bypass_safe_interaction then_return + clean_callee_1call PASS→leak-exit-2) AND caller keep-alive-inc did NOT fix N>=3 (determinism stayed exit-2). REVERTED CLEAN (re-Edit removed both phases + 7 helper fns, grep-confirmed 0 matches; byte-state == fresh baseline: default 16 + under-flag 155 both comm EMPTY; ori_arc 1626/0 debug + 1622/0 release; cargo check --workspace --tests 0; aims-proof diff EMPTY; no Lean/test/gate weakened; no git checkout/restore/reset/stash). NO TDD pins authored (REVERTED — orphan red pins break default byte-identity in shared probe binary). NEXT LEAF: the JOINT needs THREE mechanisms — (M-a) callee source-dec strip GATED by per-lineage ALLOC-AWARE NET (the unconditional strip over-fires single-call-safe callees; a structural gate cannot separate transfer-source from equilibrium-source — the net is the direct measure per LEDGER line-75/attempt-6 lesson), (M-b) caller RL-1 keep-alive-inc per may-unwind borrowed read of the result (missing-inc count = N-borrowed-reads − 1; this REMOVES the equilibrium’s dependency on the callee over-free so M-a becomes safe), (M-c) root-cause the default-path 16→61 break FIRST (a probe-tail-only change must NOT move default — re-confirm default==16 before/after each next attempt). DO NOT re-try: unconditional callee strip, callee-only strip, def-block-uniqueness discriminator, “add one final dec” caller framing. UNCOMMITTED in-tree (REVERTED — zero net source change). Checkbox 2 stays PARTIAL (155 under-flag remain). Cross-ref: decisions/LEDGER.md §B.2 attempt-55 line.
2026-06-06 — Attempt 56: BORROWED-STR-arg-to-user-call dup-read RESULT leak CURED + KEPT — un-exclude a FatValue str at an EXPLICITLY Borrowed user-call arg position from the dead-owned compute_user_call_arg_lineages exclusion. FRESH baselines rebuilt-binary-confirmed (oric+ori_rt+aot-302aa53194d0e118, —test-threads 8): default-path 16 + under-flag 155 EXACT (comm both directions vs scratch/leaf56/base_*.txt EMPTY). LEAF = fat_matrix::f02_function_param::test_fm_param_str_heap_reuse shape (let s = "…"; get_len(s: s); get_len(s: s) — local str literal borrowed-read TWICE, dead, NOT returned) — the CLEAN single-mechanism NON-&&-branchy NON-JOINT target after rejecting generics (BANNED transfer-through-return JOINT), fat_ptr_iter (loop/&&-heavy, not single-mechanism), rc_matrix (loop-carried concat). GROUND-TRUTH (ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN + ORI_TRACE_RC+ORI_CHECK_LEAKS on the ACTUAL fixture): oracle trace alloc rc=1, inc rc=2, dec rc=1, dec rc=0 FREE; under-flag trace alloc rc=1, inc rc=2, dec rc=1, STOP → rc=1 unfreed (exit 2 leak — ONE dec where oracle has TWO; /calc %0-lineage burden net +1). ROOT: %0 IS a fresh-owned candidate (compute_fresh_owned_collection_reps admits Let{Literal(String)}) but the Phase-6.8 dead-owned pass EXCLUDES its lineage via compute_user_call_arg_lineages (inserts EVERY FatValue/RcPointer arg to a non-builtin call); the exclusion is over-broad for an immutable str at a BORROWED position (survives the call, caller retains ownership → RL-2 caller release). CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL2_borrowed_param_emits_caller_dec(:220) + RL2_release_exactly_once(:239) + rl2_emits_dec(.ScopeExit)(:185); NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY, lake build 13 jobs GREEN); no case-(b). CURE (probe-gated → default byte-identical; M-c-safe — compute_user_call_arg_lineages consumed ONLY by Phase 6.8 + 6.85, both inside emit_burden_path_probe_tail): new is_str_dst helper + the consider closure threads arg_ownership+pool and SKIPS excluding an arg when arg_ownership[pos]==Borrowed ∧ is_str_dst(arg) → the str lineage stays eligible for the alloc-aware net (the §B.2 line-75 working discriminator), which fires ONE RL-2 release iff net +1; scoped to str (collections stay excluded per the A’ COW-through-borrow blocker; Owned-position str stays excluded as transfer). FIXED 4 (verbatim, under-flag 155→151, ZERO new): fat_matrix::f02_function_param::test_fm_param_str_heap_reuse, fat_matrix::f03_function_return::test_fm_return_chained, fat_matrix::f17_higher_order::test_fm_higher_order_called_twice, traits::test_aot_map_debug_int_keys_str_values. GUARDRAILS ALL HOLD: default-path SET base16 EXACT (comm -13+comm -23 vs scratch/leaf56/base_default.txt BOTH EMPTY — the M-c byte-identity guardrail a probe-tail-only cure must satisfy, and did, unlike attempt-55’s anomalous 16→61); under-flag comm -13 EMPTY (ZERO new) 155→151; cured fixture under-flag trace now alloc rc=1, inc rc=2, dec rc=1, dec rc=0 FREE (byte-matches oracle, exit 0); cargo check --workspace --tests 0; ori_arc 1626/0 debug + 1622/0 release; predicate_stack_probe 170/0 (165 attempt-53 floor + 5 new) + rc_matrix 135/0; lake build 13 jobs GREEN + aims-proof diff EMPTY; clippy -D warnings clean; §06 VF-1=0 default; eval+LLVM parity (cured fixture exit 0 both backends default; probe-gated → eval untouched); prose-lint + test-weakening + test-naming + sprawl clean; public-repo hygiene clean (Spec: Annex E §AIMS RL-2 form only). TDD-matrix-first (pre-cure FAIL/negatives-PASS, post-cure all PASS): 2 positives (probe_str_local_dup_read_borrowed_user_call_freed, probe_str_local_dup_read_via_higher_order_freed) + 3 negatives (probe_str_single_read_borrowed_user_call_no_double_free_negative, probe_str_returned_from_user_call_chain_no_double_free_negative, probe_collection_borrowed_to_user_call_single_read_no_double_free_negative). NO burden_lower/emit_burden_ops touched (M-c). UNCOMMITTED in-tree (cross-scope dirty-tree; DID NOT COMMIT). Checkbox 2 stays PARTIAL (151 under-flag remain). NEXT LEAF: the COLLECTION analogue ([int]/{K:V}/Set borrowed-dup-read at user-call — UNSAFE without a ParamContract-precision non-COW gate per the A’ blocker); SECONDARY: residual 151 (generics 27 BANNED-JOINT; fat_ptr_iter 18 / arc 13 / fat_matrix 8 / rc_matrix 10). Cross-ref: decisions/LEDGER.md §B.2 attempt-56 line.
2026-06-06 — Attempt 57: COLLECTION analogue of the str carve-out CURED + KEPT — un-exclude a fresh-local [T] LIST at a Borrowed user-call arg, GATED by a NEW per-param ParamContract.borrowed_read_only fact proving the callee does not COW-mutate / transfer / iter-consume the borrowed collection. FRESH baselines rebuilt-binary-confirmed (oric+ori_rt+aot-302aa53194d0e118, —test-threads 8): default-path 16 + under-flag 151 EXACT (comm both directions vs /tmp/leaf57/base_*.txt EMPTY). MAKE-OR-BREAK (b) RESOLVED: the ParamContract precision IS derivable + the COW negative is cleanly separated. GROUND-TRUTH (ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 + ORI_TRACE_RC+ORI_CHECK_LEAKS): (1) corpus fixture fat_matrix::f16_recursion::test_fm_recursion_list_param (@sum_recursive(xs:[int],idx) reads xs.length()/xs[idx], recursive borrow-read; main passes an INLINE list literal) under flag = alloc rc=1, inc rc=2, dec rc=1, STOP rc=1 unfreed size=24 (exit 2 leak — ONE dec where oracle has TWO, same single-missing-RL-2 release as the str case); (2) the callee param %0:[int] [borrow] flows ONLY to @len/@__index [borrow] (no owned position) while the call-site passes [own] — IDENTICAL to the str fixture, so the carve-out keys off the PROBE-TAIL arg_ownership (Borrowed), not the post-realize [own] dump; (3) the COW negative @push_one(xs:[int])={xs.push(99);..} ALREADY double-frees under flag pre-cure (exit 134 — the existing borrowed_param_then_cow_mutation residual), its param flows to @push(%1 [own]) (OWNED) — borrow inference leaves a COW receiver param Borrowed (apply_consuming_overrides runs in rc_insert, AFTER extraction), so arg_ownership==Borrowed alone does NOT prove non-COW + a blanket un-exclusion would WORSEN it → the per-param borrowed_read_only flow fact is the SOLE sound discriminator (get_len→true, push_one→false). CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL2_borrowed_param_emits_caller_dec(:220, NON-transfer, type-AGNOSTIC over str/collection) + RL2_release_exactly_once(:239) + rl2_emits_dec(.ScopeExit)(:185); a COW-mutated param is a transfer (RL2_transfer_kinds_no_dec:199); the Lean is CORRECT+COMPLETE, the impl contract precision was the gap. NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY, lake build 13 jobs GREEN); borrowed_read_only is an impl-internal ParamContract precision field (NOT a calculus rule, §CP-2 four-surface sync N/A — mirrors the existing iter_consumes/return_alias precision fields); no case-(b). CURE (probe-gated → default byte-identical; M-c-safe — the un-exclusion is consumed ONLY by Phase 6.8 + 6.85 inside emit_burden_path_probe_tail): (1) NEW ParamContract.borrowed_read_only: bool (CONSERVATIVE=false, OPTIMISTIC=true, join=AND); (2) NEW find_borrowed_read_only_params + borrowed_ro_arg_is_owned_position + borrowed_ro_arg_forward_safe in extract.rs (mirrors the proven find_iter_consume_params alias-to-param + body-scan + SCC-forwarding; owned-position authority = the COW-builtin sets + protocol table + user-fn access==Owned, matching compute_arg_ownership; builtins constructed locally — NO signature threading through extract_contract/analyze_program); (3) the attempt-56 compute_user_call_arg_lineages carve-out widened from str-only to ALSO un-exclude is_collection_dst at a Borrowed position when the callee ParamContract[pos].borrowed_read_only is true (threaded contracts into the dead-owned + dead-no-use-aggregate + user-call-lineage passes). The alloc-aware net (§B.2 line-75) + ALL existing exclusions gate which actually leak; COW / iter-consume / indirect-unknown / Owned-position args stay EXCLUDED. Invariant-5-clean. FIXED 10 (verbatim, under-flag 151→141, ZERO new): arc::test_arc_aliased_list_params, fat_matrix::f16_recursion::test_fm_recursion_list_param, fat_matrix::f16_recursion::test_fm_recursion_option_return, generics::test_generic_debug_list, generics::test_generic_iterator_item_only_positional, journey_guard::test_journey_10_lists, poly_lambda_mono::test_imported_generic_fn_list_int, recursion::test_tail_rec_with_list_param, rl31_co_verification::rl31_pre_motion_barrier_blocked, rl31_co_verification::rl31_selective_barrier_flush. GUARDRAILS ALL HOLD: default-path SET base16 EXACT (comm -13+comm -23 vs /tmp/leaf57/base_default.txt BOTH EMPTY — the M-c byte-identity guardrail; borrowed_read_only is computed on both paths but consumed only by the probe-tail gate, so default codegen cannot move, and did not); under-flag comm -13 EMPTY (ZERO new) 151→141; the COW double-free fixture borrowed_param_then_cow_mutation stays in BOTH sets UNCHANGED + NOT in the fixed set (the gate correctly EXCLUDES it — empirical over-fire-guard confirmation on the real corpus); cargo check --workspace --tests 0; ori_arc 1628/0 debug (+2 unit pins) + 1622/0 release; predicate_stack_probe 173/0 (170 attempt-56 floor + 3 new) + rc_matrix 135/0; lake build 13 jobs GREEN + aims-proof diff EMPTY; clippy -D warnings clean (2 module-level helpers extracted to clear complexity/100-line; local builtins construction avoided 8-arg threading); §06 VF-1=0 default; eval+LLVM parity (cargo st 4629/45 EXACT baseline — probe-gated → eval untouched); prose-lint 0 violations + test-weakening + test-naming + sprawl clean; public-repo hygiene clean (Spec: Annex E §AIMS RL-2 form only). TDD-matrix-first (pre-cure FAIL/negatives-PASS, post-cure all PASS): 3 AOT (2 positives probe_list_borrowed_to_user_call_dup_read_freed + probe_list_borrowed_recursive_borrow_read_dup_read_freed; 1 negative probe_collection_borrowed_to_user_call_single_read_no_double_free_negative) + 2 ori_arc unit pins (borrowed_read_only_true_for_param_at_borrowed_user_call_position, borrowed_read_only_false_for_param_at_owned_consumer_position — the COW over-fire guard). NO burden_lower/emit_burden_ops touched (M-c). UNCOMMITTED in-tree (cross-scope dirty-tree; DID NOT COMMIT). Checkbox 2 stays PARTIAL (141 under-flag remain). NEXT LEAF: map/set borrowed-dup-read is ALREADY-BALANCED (the leak is [T]-list-specific; the gate covers map/set but the net never fires); remaining residual-141 (generics 27 BANNED-JOINT; fat_ptr_iter 18 iter-consume/&&; arc 13; fat_matrix ~9; rc_matrix 10 loop-concat); the borrowed_param_iterate_then_index/borrowed_str_list_called_in_loop candidates are ITER-CONSUME (a DISTINCT mechanism, not borrow-read). Cross-ref: decisions/LEDGER.md §B.2 attempt-57 line.
2026-06-06 — Attempt 58: owned closure-VALUE scope-exit-dec leak CURED + KEPT (the attempt-57 NEXT-LEAF pivot to the arc/higher_order/generics/journey_guard closure cluster); 10 fixed, ZERO new, under-flag 144->131 (same-toolchain isolated-cure baseline). A curried / closure-returning-call closure VALUE that is an ANONYMOUS chained intermediate (fst("hello")(0) -> the PartialApply result + each closure-returning ApplyIndirect/Invoke result, never let-bound, falling outside owned_vars_needing_rc) leaks its env under the burden path; the base Phase-5 walk decs a let-BOUND closure but not the anonymous intermediates. New probe-tail Phase 6.69 emit_owned_closure_scope_exit_dec (+ is_owned_closure_value = FatValue+Tag::Function, + closure_lineage_transferred_out RL-2 transfer-out gate) emits the missing scope-exit RcDec [Closure] at the closure value’s non-transfer last use, gated predicate_stack_rc_disabled so default codegen is byte-identical. Over-fire caught + cured mid-leaf: the FIRST gate fired on the @__iter_next args[1] elem_ty_marker (FatValue+Function literal-zero) -> E5001 extract_value on non-struct on a [closure] list; the collect_iter_element_defs exclusion cures it. CALCULUS: pure case-(a) impl-conformance — Realization.lean RL2_dec_at_last_use + rl2_emits_dec(.LastReadBeforeScopeExit)/(.ScopeExit) (invoking a closure is a non-transfer read -> release its env), RL2_transfer_kinds_no_dec (a transferred closure’s env is freed by the consumer); the Lean is correct + complete, the impl under-emitted. NO .lean/.proof/rule edit (lake build 13 jobs GREEN, git diff --stat aims-proof/ EMPTY). TOOLCHAIN NOTE: the rustup default reverted 1.96.0->1.93.1 mid-session (pinned rust-toolchain.toml); cargo clean + full rebuild under 1.93.1 settled the stale-rmeta cache (the 800+/2277/all-fail snapshots were stale-1.96.0-artifacts, NOT the code). GUARDRAILS ALL HOLD (clean-rebuilt 1.93.1, —test-threads 8): default SET=base16 EXACT (M-c byte-identity, probe-gated); under-flag comm -13 EMPTY (ZERO new) vs same-toolchain no-cure baseline, 144->131 (10 corpus + 3 new positive pins fixed); ori_arc 1628/0 debug + 1624/0 release; predicate_stack_probe 177/0 (172 floor + 5 new) + rc_matrix 135/0; lake build green; clippy + prose-lint + test-weakening/naming + sprawl + public-hygiene clean; §06 VF-1=0 default; cargo st 4629/45 EXACT (eval parity, probe-gated). The &&-branchy double-dec hof_make_predicate + the iterator-map-capture Name(shard=..) codegen-bug cases stay UNCHANGED in both sets (excluded — distinct mechanisms). TDD-matrix-first: 5 AOT pins (3 positives probe_chained_curried_closure_{str,list}_capture_freed + probe_call_returned_closure_invoked_freed FAILED pre -> PASS; 2 negatives probe_closure_transferred_into_struct_no_double_free_negative + probe_let_bound_closure_single_invoke_no_double_free_negative PASS pre+post = the transfer-out + existing-burden over-fire guards). Files: aims/realize/emit_unified.rs (Phase 6.69 + 3 fns), ori_llvm/tests/aot/predicate_stack_probe.rs (5 pins). NO burden_lower/emit_burden_ops touched (M-c). NEXT LEAF: the &&-branchy closure double-dec class (hof_make_predicate — branch-merge dec-dedup, distinct from this missing-dec leaf), or the iterator-map-capture codegen bug. Cross-ref: decisions/LEDGER.md §B.2 attempt-58 line.
2026-06-06 — Attempt 59: heap-str @clone-receiver fresh-inc over-retention CHARACTERIZED + REVERTED net-zero (the leaf grounds out JOINT); byte-clean, default 16 / under-flag 131 reproduce EXACTLY post-revert. The attempt-58 PRIMARY-NEXT-LEAF (hof_make_predicate &&-branchy closure double-dec) ground-truthed as DEFAULT-coupled §09 territory — ORACLE plain run exits 134 double-free, make_predicate is in the default-16 set, so the over-emission is burden_lower/predicate-stack Phase-5 (M-c-BANNED, not probe-gateable). Pivoted to the under-flag-ONLY residual (comm -23 underflag\default = 120 probe-gateable). LEAF = string_sso/heap_clone.ori (let a="<heap str>"; let b=a.clone(); if a==b && a=="..."): the heap-str receiver %0 flows into Invoke @clone(%2 [borrow]) (deep-copy/share borrow-read, never reads receiver rc to COW-mutate) + == comparisons; the conservative compute_cow_mutated_lineage_reps callee_may_cow (non-__ user/stdlib call) wrongly classed the @clone borrow arg COW-mutation -> cow_mutated=true kept the redundant fresh inc -> lineage_net=1 -> a’s buffer leaks (the inc-elision decision permanent trace pinned dst=0 net=1 cow=true elidable=false). compute_cow_mutated_lineage_reps is called ONLY from compute_elidable_fresh_self_alloc_incs -> ONLY from emit_burden_path_probe_tail (fully probe-gated). CURE (excluding @clone from callee_may_cow) flipped %0 cow=false + freed a’s buffer, BUT the SAME test then leaked the @clone RESULT b (separate fresh alloc, the heap-str clone deep-copies) -> the leak MOVED a->b = JOINT (the a-inc-elision and the b-vs-a shared-refcount release through clone+a==b are coupled). Full-corpus under-flag 131->131 NET-ZERO (comm -13+comm -23 both EMPTY) -> count did not drop -> REVERTED CLEAN (re-Edit removed the callee != clone_name clause + let clone_name def + 3 TDD pins; git diff --stat EMPTY). CALCULUS: pure case-(a) impl-conformance — Realization.lean RL1_emit_iff_not_elidable (clone borrow-read is not a duplicating/COW use -> incElidable); no .lean/.proof/rule edit. TDD-matrix-first (authored + verified, reverted with cure): POSITIVE probe_heap_str_clone_then_compare_freed FAILED=leak pre-cure; NEGATIVE probe_heap_str_clone_receiver_consumed_keeps_inc_negative (clone receiver ALSO +-concatenated -> + keeps cow=true, over-fire boundary) PASS pre+post; STAYS-GREEN probe_sso_str_clone_then_compare_no_change ok. NEXT LEAF: the @clone-result b missing-scope-exit-dec HALF PAIRED with the @clone-receiver callee_may_cow exclusion (ground-truth BOTH receiver-net AND clone-result-net under flag BEFORE building — the JOINT must net a AND b to 0 per path). SECONDARY (distinct mechanism): heap_clone_independence leaks via the a + " extended" concat path (%0 cow=true via consumed_owned Add arm, independent of clone) — a concat-result fresh-alloc release leaf. DE-PRIORITIZE: match_alias::test_closure_env_alias/test_closure_option_str_capture_two_call_no_leak = codegen drop-glue completeness sub-leaf (closure RC ops IDENTICAL to the PASSING str-capture; the divergence is inline-aggregate-capture env drop-glue, shared codegen — NOT a probe-tail RC-balance issue). NO burden_lower/emit_burden_ops touched. Cross-ref: decisions/LEDGER.md §B.2 attempt-59 line.
2026-06-06 — Attempt 60: the attempt-59 NEXT-LEAF re-ground-truthed — leaf PREMISE CORRECTED + the architecturally-correct cure surface identified + built + REVERTED on a same-root multi-compare over-fire; byte-clean, default 16 / under-flag 131 reproduce EXACTLY post-revert. Re-ground-truth (ORI_TRACE_RC=verbose+ORI_CHECK_LEAKS+/calc per-path nets on heap_clone.ori) CORRECTS attempt-59: the leak is NOT the bb0 fresh-self-alloc inc (a’s burden_inc %0 is balanced — attempt-59 targeted the wrong inc). The REAL mechanism is the str == COMPARISON-OPERAND keep-alive incs — each Let{Var}/Let{Literal(String)} whose sole non-RC use is a Binary(Eq|NotEq) operand gets a spurious burden_inc though a == operand is an RL-1 borrow-read (incElidable); the spurious incs net the compared alloc +1 (/calc: a bb3-path +1, bb4-complement +2). KEY: emit_rc_inc_clone (arc_emitter/builtins/collections/mod.rs:19) makes heap-str clone an rc-INC of the SAME buffer (NOT a deep copy) so a/b share one alloc; the 2nd leaked alloc is the bb3 ==-literal %9. This IS attempt-50’s PROVEN compute_comparison_operand_keepalive_strips M3/M4 shape — but attempt-50 scoped compute_comparison_operand_aliases to ValueRepr::Aggregate only (emit_unified.rs:2644), uncovering str/FatValue/Literal. CURE BUILT (probe-gated, M-c-safe — Phase 6.97 inside emit_burden_path_probe_tail): widened the gate to Aggregate|FatValue|RcPointer + added a Let{Literal(String)}->self-root operand branch. On-target heap_clone under flag exit 0 leak-free (ORACLE-matched); default exit 0. KILLING CLAUSE (comm -13 NON-EMPTY): full corpus 131->126 (FIXED 8 incl. test_heap_clone/test_catch_returns_heap_string/test_generic_str_compound/3 arc::*/2 fat_ptr_iter::unwind) BUT REGRESSED 2 baseline-GREEN under-flag tests to DOUBLE-FREE: arc::test_arc_alias_chain_no_double_free (a==b && b==c) + arc::test_rc_alias_chain_compare_heap_string (r1=a==b;r2=b==c;r3=a==c). ROOT: the SAME-ROOT multi-compare (operands aliasing ONE allocation) yields >1 operand-alias dec of the same root per block; M3 strips both incs, keeps both decs -> over-release -1 double-free. attempt-50’s M3/M4 net reasoning holds only for DISTINCT-root comparisons. Per KEEP-or-REVERT (comm -13 MUST be EMPTY) REVERTED CLEAN (re-Edit restored the Aggregate-only gate + removed the Literal branch + 4 TDD pins; git diff --stat emit_unified.rs predicate_stack_probe.rs EMPTY; baselines reproduce 16/131; cargo check --workspace --tests exit 0; ori_arc 1628/0). CALCULUS: pure case-(a) impl-conformance — Realization.lean RL1_emit_iff_not_elidable:122 + RL2_release_exactly_once:239 + rl2_emits_dec(.LastReadBeforeScopeExit):185; no .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY). TDD-matrix-first (reverted with cure): POSITIVE probe_heap_str_clone_then_double_compare_freed FAILED pre -> PASS post-v2; POSITIVE probe_heap_str_multi_ref_double_compare_freed (same-root, the over-fire) FAILED pre AND post; NEGATIVES probe_heap_str_single_compare_no_double_free_negative + probe_sso_str_clone_then_double_compare_no_change_negative PASS pre+post. NEXT LEAF: re-attempt the FatValue/RcPointer/Literal comparison-operand widening WITH a same-root guard — either exclude a root with >1 operand-alias live across the same branch-merge (leaves same-root shapes as their original leak, net-positive if the 8 distinct-root fixes hold), OR (correct full fix) thread compute_lineage_alloc_aware_net into the strip so M3 strips incs only down to the per-path release count (the alloc-aware NET discriminates; the structural operand-alias proxy over-fires on same-root per LEDGER §B.2 line 75). Ground-truth arc/arc_alias_chain_no_double_free.ori + arc/rc_alias_chain_compare_heap_string.ori under flag BEFORE re-building. SECONDARY: heap_clone_independence still leaks 1 via the +-concat-result path (distinct). NO burden_lower/emit_burden_ops touched. Cross-ref: decisions/LEDGER.md §B.2 attempt-60 line.
2026-06-06 — Attempt 61: attempt-60’s characterized full fix LANDED + KEPT — FatValue/RcPointer/Literal(String) comparison-operand widening WITH the alloc-aware-net same-root guard; 8 FIXED, ZERO new, under-flag 131->123. Re-built attempt-60’s cure (widen compute_comparison_operand_aliases repr gate to Aggregate|FatValue|RcPointer + Let{Literal(String)}->self-root branch) PLUS the SAME-ROOT GUARD curing its killing clause: a Binary(Eq|NotEq) whose two operands satisfy same_alloc(same_alloc_reps, args[0], args[1]) excludes BOTH operands from the strip (the same-root comparison’s incs/decs stay at the balanced baseline). Discriminator = compute_same_alloc_reps (the union-find over Let-Var + apply-result Direct/Conditional alias edges, the alloc-class SSOT emit_edge_cleanup consumes) threaded through strip_comparison_operand_keepalive -> compute_comparison_operand_keepalive_strips -> compute_comparison_operand_aliases — the alloc-aware measure the line-75 thesis demands (the structural operand-alias proxy over-fired on same-root EXACTLY as line-75 predicts). Ground-truthed: in heap_clone (a==b && a=="lit") the @clone RESULT is an Invoke result = DISTINCT same_alloc rep from a -> each == DISTINCT-root -> strip sound (8 fixes); in arc_alias_chain (a==b && b==c, b/c Let-Var aliases) all operands = ONE rep -> SAME-root -> guard excludes -> the attempt-60 double-free prevented (/calc then-path without the guard 1+2−2+0−2=−1). FIXED 8 (the EXACT attempt-60 targets): arc::test_rc_alias_borrowed_call_then_root_use, arc::test_rc_catch_heap_alias_scalar_project, arc::test_rc_project_merge_edge_two_fields_escape, fat_ptr_iter::unwind::test_unwind_list_reusable_after_catch, fat_ptr_iter::unwind::test_unwind_multiple_invokes_with_panic, generics::test_generic_str_compound, string_sso::test_catch_returns_heap_string, string_sso::test_heap_clone; the 2 same-root regressions STAYED GREEN. CALCULUS: pure case-(a) impl-conformance — Realization.lean RL1_emit_iff_not_elidable:122 (== operand borrow-read is incElidable) + RL2_release_exactly_once:239 (one alloc released once per path = the same-root guard’s basis); no .lean/.proof/rule edit (lake build 13 jobs GREEN, git diff --stat aims-proof/ EMPTY). GUARDRAILS ALL HOLD (fresh clean-rebuilt 1.93.1, —test-threads 8): default SET=base16 EXACT (M-c byte-identity, probe-gated — both comm EMPTY); under-flag comm -13 EMPTY (ZERO new), 131->123; cargo check --workspace --tests exit 0; ori_arc 1629/0 debug + 1625/0 release (+1 unit pin); predicate_stack_probe 181/0 (177 floor + 4 new) + rc_matrix 135/0; lake build green; clippy + prose-lint + test-weakening/naming + sprawl + public-hygiene clean; cargo st 4629/45 EXACT (eval parity, probe-gated). VF-1: §06 VF-1=0 default for this change (default byte-identical); a PRE-EXISTING same-root alias-chain dead-else-path VF-1 imbalance (v2 net=1 at exit block 3 on arc_alias_chain_no_double_free) shows on BOTH default AND under-flag (present on the DEFAULT path = NOT this change; the executed then-path nets 0 so the test passes) — see NEXT LEAF. TDD-matrix-first: 4 AOT pins (POSITIVE probe_heap_str_clone_then_double_compare_freed FAILED pre -> PASS; CRITICAL NEGATIVE probe_heap_str_same_root_multi_compare_no_double_free_negative + NEGATIVES probe_heap_str_same_root_three_compare_no_double_free_negative + probe_heap_str_single_compare_no_double_free_negative PASS pre+post = the over-strip boundary) + 1 ori_arc unit pin comparison_operand_same_root_excluded_no_strip. Files: aims/realize/emit_unified.rs (widened gate + Literal branch + same-root same_alloc guard + same_alloc_reps threading), emit_unified/burden_lowering_tests.rs (unit pin + thread 3 existing), ori_llvm/tests/aot/predicate_stack_probe.rs (4 pins). NO burden_lower/emit_burden_ops touched (M-c). NEXT LEAF: the PRE-EXISTING same-root alias-chain dead-else-path VF-1 imbalance (arc_alias_chain_no_double_free a==b && b==c shows v2 net=1 at exit block 3 on the DEFAULT path = §09-territory Phase-5/predicate-stack burden-balance asymmetry, NOT probe-tail-curable); OR the SECONDARY heap_clone_independence +-concat-result fresh-alloc release leaf. Residual 123: generics 25 = BANNED transfer-through-return JOINT; fat_ptr_iter/arc-remaining/rc_matrix per attempt-56/60 char. Cross-ref: decisions/LEDGER.md §B.2 attempt-61 line.
2026-06-06 — Attempt 62: FRESH-heap-str dead-on-early-?/branch RL-4 edge release LANDED + KEPT — new probe-tail Phase 6.86 emit_burden_branch_dead_value_decs; 1 FIXED, ZERO new, under-flag 123->122. The briefing LEAD (heap_clone_independence +-concat-result release) GROUNDED OUT JOINT — ruled NOT single-mechanism: /calc + ORI_DUMP_AFTER_BURDEN showed the leak is heap-str a(%0) net=+1 blocked from fresh-inc elision by cow_mutated=true, but the over-fire GUARD coll_list_cow_concat_shared (xs SURVIVES the concat) has the IDENTICAL net=1 cow_mutated=true signature — the alloc-aware net CANNOT distinguish dead-after-concat from survives-after-concat (attempt-67 M1 killing clause re-confirmed; that needs a Phase-5 liveness change = M-c-coupled). PIVOTED to fat_matrix::f15_question_mark::test_fm_question_cleanup_fat_scope (@process(opt)={ let name="…30"; let v=opt?; Some(v+name.length()) }): ground-truth — ORACLE name freed; UNDER-FLAG alloc rc=1 STOP unfreed size=30 LEAK. ROOT (Phase-5 dump): name(%1) fresh Let{Literal(String)} in bb0, branch bb1:bb2; bb1->bb3 reads+releases name; bb2 (the ?-None early-return) is name-DEAD with NO release — the base walk releases only on the survives branch (RL-4 edge-cleanup gap). NOT covered by Phase 6.8/6.85/6.69. CURE (probe-gated Phase 6.86, M-c-safe): compute_branch_dead_value_releases + emit_burden_branch_dead_value_decs — STR-ONLY candidates (is_str_dst; collections/aggregates EXCLUDED = RL-2 transfer-into-struct over-fire), emit ONE BurdenDec at the dead successor’s FRONT iff Branch/Switch split ∧ NOT unwind-reachable ∧ def_block DOMINATES S ∧ single-pred S ∧ dead-in-S-subtree ∧ live-out-of-B; SEED-not-reuse exclusions (returned/owned-consumed/PrimOp/user-call/owned-moved/iter/borrowed). OVER-FIRE CAUGHT+CURED across 3 narrowings (isolation-proven via Phase-6.86-disable: the 8 regressed pins were MY over-fire): str-only candidate gate (cured 6 slice-element-into-field pins), compute_unwind_reachable_blocks exclusion + Branch/Switch-only (cured the @debug-Invoke-unwind-block E5001), DominatorTree.dominates guard (cured the derive_debug %11 sibling-branch-literal double-free). CALCULUS: pure case-(a) impl-conformance — Realization.lean RL4_edge_dec_decision:289 + RL4_edge_release_balanced:309 + RL4_jump_arg_exempt:297 (the Lean mandates the edge release; the impl under-emitted); no .lean/.proof/rule edit (lake build 13 jobs GREEN, git diff --stat aims-proof/ EMPTY). FIXED 1 (verbatim, under-flag 123->122): fat_matrix::f15_question_mark::test_fm_question_cleanup_fat_scope. GUARDRAILS ALL HOLD (fresh clean-rebuilt 1.93.1, —test-threads 8; stale-binary 1010-fail measurement was a no-op cargo build artifact, corrected via touch-forced rebuild): default SET=base16 EXACT (M-c byte-identity, probe-gated — both comm EMPTY); under-flag comm -13 EMPTY (ZERO new), 123->122; cargo check --workspace --tests exit 0; ori_arc 1631/0 debug + 1627/0 release (+2 unit pins); predicate_stack_probe 184/0 (181 floor + 3 new) + rc_matrix 135/0; lake build green; clippy -D warnings clean (4 missing-backtick doc warnings cured) + prose-lint + test-weakening/naming + sprawl + public-hygiene clean; cargo st 4629/45 EXACT (eval parity, probe-gated; cured fixture exits 0 BOTH backends default); §06 VF-1=0 default on cured fixture. TDD-matrix-first: 3 AOT pins (POSITIVES probe_fresh_heap_str_dead_on_question_early_exit_freed + probe_fresh_heap_str_dead_on_explicit_branch_freed FAILED=leak pre -> PASS; CRITICAL NEGATIVE probe_fresh_heap_str_returned_on_early_exit_no_double_free_negative — str RETURNED on the dead branch = RL-2 transfer, compute_returned_lineages excludes — PASS pre+post) + 2 ori_arc unit pins (branch_dead_value_frees_str_on_early_exit_branch + branch_dead_value_skips_str_returned_on_dead_branch). Files: aims/realize/emit_unified.rs (Phase 6.86 + 2 fns), emit_unified/burden_lowering_tests.rs (helper + 2 unit pins + import), ori_llvm/tests/aot/predicate_stack_probe.rs (3 pins). NO burden_lower/emit_burden_ops touched (M-c). NEXT LEAF: the construct-heap-field-into-aggregate-variant leak — f06_pattern_matching::test_fm_match_heap_str_multi_field + f12_sum_payload::test_fm_sum_multi_fat_variant (heap str/list moved into an inline sum variant; the BurdenDec [InlineEnum] drop-glue does not free the moved-in field under flag — distinct mechanism, excluded here by the str-only gate); ground-truth WHY BEFORE building. SECONDARY (still JOINT, DE-PRIORITIZE): heap_clone_independence +-concat-result (needs the dead-after-concat liveness discriminator the alloc-aware net lacks, Phase-5-coupled). Cross-ref: decisions/LEDGER.md §B.2 attempt-62 line.
2026-06-06 — Attempt 63: attempt-62’s NEXT-LEAF construct-heap-field-into-inline-aggregate-variant leak CURED + KEPT — new probe-tail Phase 6.87 relocate_borrowed_terminator_aggregate_dec; 3 FIXED, ZERO new, under-flag 122->119. A heap value (str/[T]) moved into an INLINE SUM VARIANT or struct (ConstructArg transfer INTO the aggregate), where the fresh aggregate is passed BORROWED to a borrow-read callee and DEAD afterward, leaks the moved-in heap field under sole-emitter lowering. GROUND-TRUTH (permanent tools — ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN/ORI_DUMP_AFTER_LLVM + ORI_TRACE_RC+ORI_CHECK_LEAKS + ORI_LOG=ori_arc::aims::realize=trace per-phase + /calc per-path nets): on f06 (Named(description: heap51, count) borrow-read by desc_len) ORACLE LLVM @main emits ori_str_rc_dec(@_ori_drop$3) AFTER the call (the predicate-stack path’s direct field-dec; name alloc rc=1 -> dec rc=0 FREE), UNDER-FLAG LLVM @main emits NEITHER ori_str_rc_dec NOR an InlineEnum drop call -> alloc rc=1 STOP unfreed size=51 LEAK (zero dec events). ROOT (NOT codegen — emit_rc_dec_inline_enum correctly tag-switches per-variant field drop; NOT M-c-banned Phase-5 — emit_burden_ops emits a matched burden_inc %4; burden_dec %4 PAIR on the aggregate pre-call): the realize-phase per-block trace pinned binc=[4] bdec=[4] UNCHANGED through every probe-tail phase (6.5-6.97) + lowered correctly at after_phase_7_burden_lowering to inc=[4] dec=[4], then the Phase-3 coalesce peephole (coalesce/mod.rs:179 “Net zero: both cancelled — emit nothing”) CANCELS the adjacent RcInc %4; RcDec %4 (the Invoke terminator is not a coalesce barrier) -> no scope-exit RcDec [InlineEnum] survives -> the moved-in str field never freed. The single burden_dec %4 is the spurious-paired Phase-5 mis-emission; on the DEFAULT path the predicate stack co-emits the real ori_str_rc_dec, on the under-flag path only the coalesce-cancelled burden pair remains. The moved-in field is an RL2_transfer_kinds_no_dec ConstructArg transfer INTO the aggregate so the aggregate’s own scope-exit drop is the field’s sole release; the aggregate’s last use is a borrowed call (rl2_emits_dec(.LastReadBeforeScopeExit) non-transfer) whose release relocates to the dead successor edges. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL2_release_exactly_once:239 + RL2_transfer_kinds_no_dec:199 (ConstructArg) + rl2_emits_dec(.LastReadBeforeScopeExit):185 + RL4_edge_release_balanced:309 (released once per concrete path); the Lean ALREADY mandates the single field release, the impl under-emitted (coalesce-cancelled). NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY, lake build 13 jobs GREEN); no case-(b) gap. CURE LANDED (KEPT, probe-gated -> default byte-identical; the new Phase 6.87 runs ONLY inside emit_burden_path_probe_tail behind predicate_stack_rc_disabled — M-c-safe, NOT a burden_lower/emit_burden_ops change): relocate_borrowed_terminator_aggregate_dec + compute_borrowed_terminator_aggregate_relocations + aggregate_borrow_read_relocatable. Per call block whose terminator is Invoke @callee(recv [borrow]) where recv is_burden_carrying_aggregate (heap-bearing struct/tuple/Option/Result/sum-variant — Value-variants EXCLUDED, no heap field) ∧ carries the coalesce-doomed BurdenInc+BurdenDec PAIR ∧ the callee borrow-reads without return-view aliasing (aggregate_borrow_read_relocatable reuses the proven borrowed_arg_release_verdict for escape-safe builtins + adds the user-fn borrow-read case: ParamContract return_alias==None ∧ !return_payload_contains_param ∧ !iter_consumes ∧ access==Borrowed) ∧ recv DEAD after (!lineage_live_out) ∧ NOT returned/owned-consumed/owned-moved-into-collection: STRIP both the spurious BurdenInc recv + BurdenDec recv from the call block + emit ONE BurdenDec recv at the FRONT of BOTH successor edges (RL-4 Both, RL4_edge_release_balanced). Reuses attempt-41’s aggregate-field-drop attribution (is_burden_carrying_aggregate -> RcDec [AggFields]/[InlineEnum] field-walk) + the SEED-not-reuse exclusion set + borrowed_arg_release_verdict from attempt-18’s borrowed-terminator-relocation foundation; no structural-proxy over-fire (the per-callee return-view-aliasing gate + the Borrowed-position gate + dead-after gate are the discriminators). FIXED 3 (verbatim, under-flag 122->119, ZERO new): fat_matrix::f06_pattern_matching::test_fm_match_heap_str_multi_field, fat_matrix::f12_sum_payload::test_fm_sum_multi_fat_variant, enum_discriminant::test_enum_rc_payload_narrowed_tag (the third a bonus same-mechanism heap-payload-into-variant case). GUARDRAILS ALL HOLD (fresh clean-rebuilt-from-disk 1.93.1 oric+ori_rt+aot-302aa53194d0e118, —test-threads 8; a mixed-1.96/1.93.1 dep-cache E0514 mid-session was cleared via rm -rf target/debug/{deps,.fingerprint,build,incremental} + single-resolution rebuild, BOTH baselines re-confirmed 16/122 before measurement): default SET=base16 EXACT (comm -13+comm -23 vs scratch/leaf_inlinevar/base_default.txt BOTH EMPTY — the M-c byte-identity guardrail; the Phase 6.87 pass runs ONLY under the flag, so default codegen cannot move, and it did not); under-flag SET comm -13 vs scratch/leaf_inlinevar/base_underflag.txt EMPTY (ZERO new), 122->119; cargo check --workspace --tests EXIT 0 (Finished); ori_arc 1633/0 debug + 1629/0 release (+2 unit pins; the 4-test debug/release gap is pre-existing debug-only tests); predicate_stack_probe 189/0 (184 attempt-62 floor + 5 new) + rc_matrix 135/0 all prior pins GREEN; lake build 13 jobs GREEN + git diff --stat aims-proof/ EMPTY; clippy -D warnings clean (ori_arc + ori_llvm tests; 3 doc-list-indentation warnings cured); §06 VF-1=0 default (postprocess=warn 0 imbalances on cured f06+f12); eval+LLVM parity (cargo st 4629/45 EXACT attempt-56/57/58/61/62 baseline — probe-gated -> eval untouched; cured fixtures exit 0 BOTH backends default path); prose-lint clean (3 touched files, 0 violations); test-weakening-lint + test-naming-lint + sprawl-lint clean; public-repo hygiene clean (no attempt-N/§07B/BUG-XX-NNN/.claude/LEDGER/rule-file refs in MY added source — Spec: Annex E §AIMS RL-2 + RL-4 form only). NO burden_lower/emit_burden_ops touched (M-c). TDD-matrix-first (authored + verified pre-cure FAIL/negatives-PASS, post-cure all PASS): 5 AOT pins in predicate_stack_probe.rs — 2 positives probe_heap_str_into_sum_variant_borrow_read_freed (f06 shape) + probe_heap_list_into_sum_variant_borrow_read_freed (f12 shape) FAILED=leak pre-cure -> PASS + 3 NEGATIVES probe_call_result_variant_borrow_read_no_double_free_negative (a make()-result variant borrow-read, already-balanced under flag — the alloc-aware/returned exclusion must not double-free) + probe_value_variant_into_sum_no_spurious_dec_negative (a scalar-only Both(a,b) Value-variant — is_burden_carrying_aggregate excludes, no field to free) + probe_heap_str_into_sum_variant_already_balanced_sibling (a str borrow-read NOT wrapped in a variant — the cure must not touch it) all PASS pre AND post + 2 ori_arc unit pins in burden_lowering_tests.rs (borrowed_terminator_aggregate_relocates_dec_to_edges positive [relocation = (block 0, recv %1, normal bb1, unwind bb2)] + borrowed_terminator_aggregate_skips_owned_transfer negative [owned-position aggregate transfer -> no relocation, the double-free over-fire guard]). Files-touched (1 production-region + 2 test): compiler/ori_arc/src/aims/realize/emit_unified.rs (Phase 6.87 call + relocate_borrowed_terminator_aggregate_dec + compute_borrowed_terminator_aggregate_relocations + aggregate_borrow_read_relocatable) + its test sibling emit_unified/burden_lowering_tests.rs (borrowed_terminator_aggregate_func + borrow_read_contracts helpers + 2 unit pins + import) + compiler/ori_llvm/tests/aot/predicate_stack_probe.rs (5 pins) — no parallel emission path (Invariant-5-clean; an RL-2/RL-4 burden-op edge-placement refinement, NOT a calculus change). A PARALLEL SESSION concurrently edits the §07B files; my additions grep-confirmed intact (HEAD c0d7bb711 unchanged). No parallel-session-OWNED logic touched; no Lean/test/gate/contract weakened; no git checkout/restore/reset/stash; DID NOT COMMIT (cross-scope dirty-tree). NEXT LEAF: the owned-transfer-CHAIN heap-field leak — take_owned(i) = consume(i: i) forwards a fresh variant [own] through a chain where the str field is not freed under flag (a transfer-through-call shape, DISTINCT from this borrow-read mechanism; the verdict’s UnwindOnly/Owned arm or the generics transfer-through-return JOINT territory). SECONDARY (still JOINT, DE-PRIORITIZE): heap_clone_independence +-concat-result (needs the dead-after-concat liveness discriminator the alloc-aware net lacks, Phase-5-coupled). The compute_borrowed_terminator_aggregate_relocations borrow-read-aggregate RL-4 foundation landed here is reusable for any fresh-aggregate-into-borrowed-call residual. Cross-ref: decisions/LEDGER.md §B.2 attempt-63 line.
2026-06-06 — Attempt 64: attempt-63’s NEXT-LEAF owned-transfer-CHAIN heap-field leak — HARD GROUND-TRUTH GATE applied, decided mechanism-class B (BANNED generics transfer-through-return JOINT), CHARACTERIZED-ONLY, NO cure built, byte-clean. Fresh clean-rebuild-from-EMPTY-target 1.93.1 (oric+ori_rt 21.79s + aot-302aa53194d0e118 20.95s, —test-threads 8): default 16 / under-flag 119 reproduce EXACTLY (both comm directions vs scratch/leaf_chain/base_*.txt EMPTY); HEAD 9e53362ea unchanged; ZERO compiler-source changes (only scratch). HARD-GATE (decide A-vs-B from trace BEFORE writing any cure): the owned-transfer-CHAIN cohort is the generics forwarder cluster (@id<T>(x:T)->T=x / @just_return_it(x:[int])->[int]=x — callee returns its [own] param). GROUND-TRUTH (ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN/ORI_DUMP_AFTER_BURDEN_ELIM + ORI_TRACE_RC+ORI_CHECK_LEAKS + /calc): non_generic_forwarder_list ORACLE net 0 FREE vs UNDER-FLAG net +1 LEAK (rc=1 unfreed size=24; /calc TRUE-path 1+1−1+1+1−1+1−1−1=+1, FALSE-path =+2); callee emits ZERO burden ops (Return %1 [own] — correct, RL2_transfer_kinds_no_dec(.Return)), imbalance ENTIRELY caller-side, eliminate_burden_ops UNCHANGED. The cluster is BIDIRECTIONAL: nested_list/set_int/non_generic_forwarder_list net=+1 LEAK; box_list/struct_with_list/inherent_method_forwarder_self exit 134 double-free (on struct_with_list @main emits two projected-inner-list burden_dec with NO keep-alive incs the oracle has). B-DETERMINATION: this leak/double-free bidirectional signature = caller-keep-alive-inc-deficit interplaying with the callee transfer = the IDENTICAL JOINT attempts 54/55 isolated (THREE coordinated mechanisms: M-a callee transfer-source-dec strip GATED by alloc-aware net = Phase-5 emit_burden_ops = M-c-BANNED; M-b caller RL-1 keep-alive incs; M-c inc-before-edge-cleanup), whose isolated build over-fired under-flag 155->363 (+209) AND broke default 16->61 (+45). Per directive: B -> STOP, do NOT build the isolated callee strip, characterize as §09 territory. CALCULUS: pure case-(a) impl-conformance (arc.md §CP-1) — Realization.lean RL1_emit_iff_not_elidable:122 + rl2_use_transfers_ownership(.Return):175 + RL2_transfer_kinds_no_dec:199 + RL2_release_exactly_once:239 + RL4_edge_release_balanced:309; Lean CORRECT, impl caller-side under-emits; NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY). PIVOT SURVEY (all DE-PRIORITIZED): arc::test_arc_loop_string_reassignment_no_leak (loop+concat liveness = Phase-5-coupled); elem_dec_scope::test_str_list_explicit_last_owner (loop + use-after-loop double-free = Phase-5-coupled); fat_ptr_iter::unwind::test_unwind_callee_local_heap_value (catch-block TWO sub-leaks: callee panic-edge concat-result + caller post-catch block-param = catch-completeness JOINT); recursive_feature::recursive_feature_option_some_holds_recursive_node (Some(n1) matched, dead; net=+1 LEAK on n1 — CLEANEST (A) single-buffer BUT the match-merge block-param carries n2-moved-into-n1 + n1 + Some-wrapping-n1, so emitting the outermost-owner dec WITHOUT double-freeing n2 needs the alloc-aware-net + move-alias discriminator = over-fire-risky; bare-str-in-variant analogue ALREADY balanced under flag). NEXT LEAF: the recursive_feature_option_some_holds_recursive_node nested-aggregate-in-variant matched-and-dead leaf IF paired with the alloc-aware-net OUTERMOST-OWNER discriminator (a probe-tail Phase-6.x emitting ONE scope-exit BurdenDec for the outermost fresh aggregate carried into a match-merge block-param, GATED by lineage_net==+1 + the move-alias set so nested ConstructArg-moved fields AND the borrow_list_int transfer-through-return siblings are EXCLUDED; ground-truth every block-param aggregate’s per-path net BEFORE building + author the nested-moved-in-no-double-free + transfer-through-returned-no-dec NEGATIVES). SECONDARY: the forwarder transfer-through-return JOINT stays §09 territory (M-a callee strip is Phase-5 = M-c-banned); the fat_ptr_iter catch-block panic-edge + post-catch JOINT is a distinct catch-completeness leaf. NO burden_lower/emit_burden_ops touched; no Lean/test/gate weakened; no git checkout/restore/reset/stash; DID NOT COMMIT (cross-scope dirty-tree). Cross-ref: decisions/LEDGER.md §B.2 attempt-64 line.
2026-06-06 — Attempt 65: attempt-64 NEXT-LEAF recursive-aggregate-in-variant matched-and-dead OUTERMOST-owner missing scope-exit release — BUILT probe-tail Phase-6.855 (emit_burden_match_merge_dead_aggregate_decs + alloc-aware-net OUTERMOST-owner discriminator via compute_burden_entry_nets/compute_jump_threaded_reps/is_lineage_dead_sink), REVERTED-CLEAN — JOINT 2-mechanism over-fire, byte-identical. Fresh 1.93.1 baselines reproduce default 16 / under-flag 119 EXACT (both comm EMPTY). GROUND-TRUTH (ORI_DUMP_AFTER_ARC oracle vs flag ORI_DUMP_AFTER_BURDEN/_ELIM + ORI_TRACE_RC=verbose+ORI_CHECK_LEAKS + /calc): Option niche-encoded (Some(n1)==n1 ptr), 2 allocs n2(0x..2c0)/n1(0x..3c0); burden walk threads n2/n1/outer-Some into match-merge bb1 block-param with ZERO scope-exit decs, bb2 frees n2 via projected RcDec %19 [AggFields] (walks n1.next), n1 LEAKS (rc 1->2->1). The discriminator WORKED (only outermost %10 fired; n2+n1 owned-consumed EXCLUDED) but the emitted RcDec %10 [InlineEnum] recursive drop re-walks n1.next -> re-frees already-freed n2 -> FATAL DOUBLE-FREE at 0x..2c0 (target NOT fixed). KILLING NUMBERS (verbatim): default 16->20 (+4, ALL predicate_stack_probe::probe_project_borrowed_view_*), under-flag 119->126 comm -13=14 NEW / comm -23=7 FIXED (an unrelated for_yield_option-str cohort) — candidate set (every fresh burden-carrying Construct aggregate at a dead-sink net>0) too broad, double-frees fat_matrix::f12_sum_payload/tagless_enum/predicate_stack_probe::probe_project_borrowed_view_* wherever the burden walk already split the nested release via a projected field-dec. The leak (outermost missing) + double-free (recursive drop re-frees separately-freed nested field) = SAME recursive-drop mechanism = NOT a clean single-mechanism (A) leaf (attempt-64 (A) classification REFUTED). CALCULUS: case-(a) impl-conformance — Realization.lean RL2_release_exactly_once:239 + rl2_emits_dec(.ScopeExit):185 + RL2_transfer_kinds_no_dec:199; NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY); no scratch theorem. REVERTED by re-Editing (both fns + wiring deleted; git diff HEAD --stat compiler/ docs/ library/ EMPTY = byte-identical to HEAD 9e53362ea; ori_arc 1633/0 debug + 1629/0 release; predicate_stack_probe 189/0 + rc_matrix 135/0 — 4 over-fired probe pins back GREEN; ZERO TDD pins authored; no git checkout/restore/reset/stash; DID NOT COMMIT — cross-scope dirty-tree). NEXT LEAF: recnode JOINT needs M1 (Phase-6.855 outermost dead-sink dec — built, discriminator validated) + M2 (suppress the split nested-field release so the outermost recursive drop is sole nested free — either strip the projected RcDec %19 when the outermost recursive drop covers the same field, OR compensating nested BurdenInc mirroring the oracle bb0 RcInc %2) in LOCKSTEP + a narrowed candidate sub-class (recursive-aggregate-IN-VARIANT with a back-edge Option/Result field + a projected-nested-field-dec presence check, not blanket is_burden_carrying_aggregate). Cross-ref: decisions/LEDGER.md §B.2 attempt-65 line.
2026-06-06 — Attempt 66: KEPT — collection-source-result fresh-inc over-count (M1) on self-allocating builtin collection-result Apply callees; under-flag 119->115 (4 FIXED, ZERO new); default 16 byte-identical; probe-gated. SURVEY (fresh 1.93.1 baselines: default 16 / under-flag 119, both comm EMPTY): the 119 under-flag set has 11 IDs ALSO in the default-16 set (§09-coupled / independent, not §07B-fixable), leaving 108 under-flag-only candidates. Cluster classification: generics(20)=forwarder transfer-through-return JOINT (§09, attempts 54/55/64 M-a callee strip = Phase-5/M-c-banned); fat_ptr_iter(16)=iterator-handle/conversion + catch-block panic-edge JOINT (§09, attempt-64); rc_matrix(10)+stress(7)+string_sso(4 partial)+arc(5)=str-concat / loop-reassign liveness Phase-5-coupled (attempt-62 dead-vs-survives-after-concat needs Phase-5 liveness=M-c-banned); match_alias(5)=alias-chain/payload-escape (§09, attempt-9/61); cow_map_set(3 partial)=COW-shared-survives load-bearing-inc JOINT (attempt-5/6); cli(3)=main-args env-coupled (passes standalone); recursive_feature/derive(5)=recursive-aggregate-in-variant JOINT (§09, attempt-65); narrowing(5)=collection-source-result M1 over-count = THE clean (A) candidate. GROUND-TRUTH (ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN + ORI_TRACE_RC+ORI_CHECK_LEAKS + /calc + ORI_LOG=ori_arc::aims::realize=trace elision-decision trace) on narrowing::test_set_int_operations_canonical ([10,20,30].iter().collect() into Set<int>, multi-branch @contains/@len borrow-read, dead-after): ORACLE %5 (the @__collect_set result) alloc(+1) dec(−1) FREE; UNDER-FLAG burden_inc %5 (Phase-5 fresh-site inc) + burden_dec %5 -> alloc(+1)+RcInc−RcDec = net +1 LEAK (size=72 unfreed). ROOT (case-a impl-conformance): Phase-5 fresh_site_burden_inc_dst (burden_lower/emit.rs:587) emits a fresh-site BurdenInc for EVERY Apply result with Unique/MaybeShared/no-contract return (caller-acquires-owned-reference); for a SELF-allocating builtin collection result (@__collect_set/@collect/@union/@keys, rc=1 fresh buffer distinct from operands) that inc is the M1 over-count under Phase-7 sole-emitter lowering. The landed M1 alloc-aware-net elision (compute_elidable_fresh_self_alloc_incs) NEVER considered them because fresh_self_alloc_dst excludes Apply results (deliberate — general Apply results inherit a callee reference). CALCULUS: pure case-(a) — Realization.lean RL1_emit_iff_not_elidable:122 (a non-duplicated FRESH value’s single use is move-once-linear -> inc elidable -> NO fresh inc) + rcBalance (the alloc IS the +1; one dec frees) ALREADY govern; the Lean is CORRECT, the impl diverged. NO .lean/.proof/rule edit (git diff --stat aims-proof/ EMPTY; lake build 13 jobs GREEN). CURE (KEPT, probe-gated -> default byte-identical): new fresh_collection_source_apply_dst recognizes self-allocating BUILTIN collection-source Apply results (the __collect_set protocol builtin + the allocates-predicate name sets: cow / conversion / iterator-consumer / set-algebra / fresh-str), unioned with fresh_self_alloc_dst via fresh_rc_alloc_dst into the M1 elision + alloc-aware-net — so the landed alloc-aware net drops the spurious fresh inc when net==1 ∧ !cow_mutated. SECOND fix (required): compute_cow_mutated_lineage_reps callee_may_cow exempted KNOWN builtins (!builtins.is_builtin(callee)) — a borrowed-position read-only builtin method (@contains/@len/@get) was spuriously flagging the collection cow_mutated=true (blocking elision), while genuine builtin COW-mutators (push/set/insert) take the receiver OWNED and are already caught by the owned-position consumed_owned check; only NON-builtin user calls are the interprocedural-COW-through-borrowed-param risk. GUARDRAILS ALL HOLD (fresh 1.93.1, --test-threads 8): default-path SET 16 EXACT (comm -13+comm -23 vs scratch/leaf66/base_default.txt BOTH EMPTY — M-c byte-identity); under-flag SET comm -13 vs base_underflag.txt EMPTY (ZERO new), 119->115; 4 FIXED: cow_map_set::test_cow_set_union_shared, fat_ptr_iter::generalize::test_generalize_string_iteration, narrowing::test_set_int_operations_canonical, string_sso::test_heap_iteration. cargo check --workspace --tests EXIT 0; ori_arc 1633/0 debug + 1629/0 release; predicate_stack_probe 193/0 (189 floor + 4 new) + rc_matrix 135/0; lake build 13 jobs GREEN + aims-proof diff EMPTY; clippy -D warnings clean (cognitive-complexity + let-else cured via the fresh_rc_alloc_dst extraction); §06 VF-1=0 default on cured fixtures; eval+LLVM parity cargo st 4629/45 EXACT; prose-lint + test-weakening-lint + test-naming-lint + sprawl-lint clean; public-repo hygiene clean (Spec: Annex E §AIMS RL-1/RL-2 form; M1/M3 established public vocab). CRITICAL NEGATIVE arc::test_arc_borrowed_param_cow_push_use_after/_diamond/_str_list STAY GREEN (the cow-flag exemption does NOT over-elide the load-bearing COW-through-borrowed-param inc). TDD-matrix-first: 4 AOT pins in predicate_stack_probe.rs — 2 POSITIVE (probe_collect_set_result_multibranch_dead_freed FAILED=leak pre-cure -> PASS; probe_collect_list_result_multibranch_dead_freed) + 1 CRITICAL NEGATIVE (probe_collect_result_duplicated_not_double_freed_negative — a duplicated .collect() result’s fresh inc is load-bearing, net != 1 gate keeps it, PASS pre+post) + 1 ALREADY-BALANCED SIBLING (probe_collect_result_straightline_dead_already_balanced_sibling). Files-touched (1 production + 1 test): compiler/ori_arc/src/aims/realize/emit_unified.rs (fresh_collection_source_apply_dst + fresh_rc_alloc_dst + callee_may_cow builtin exemption + 2 M1-consumer wirings) + compiler/ori_llvm/tests/aot/predicate_stack_probe.rs (4 pins). No burden_lower/emit_burden_ops touched (M-c). No Lean/test/gate/contract weakened; no git checkout/restore/reset/stash; DID NOT COMMIT (cross-scope dirty-tree). NEXT LEAF: the remaining narrowing per-element (test_iter_map_on_narrowed_int_list 3-collected-lists, test_phase_c_push_large_values) + rc_matrix/stress concat-liveness clusters are Phase-5-coupled (dead-vs-survives-after-concat = M-c-banned, attempt-62); the genuinely-clean M1-collection-source surface is now near-exhausted — the residual is dominated by the §09-territory JOINTs (generics forwarder, fat_ptr_iter catch/iterator-handle, recursive-aggregate-in-variant) + Phase-5-loop/concat-coupled shapes that the probe tail structurally cannot fix. Cross-ref: decisions/LEDGER.md §B.2 attempt-66 line.
2026-06-06 — Attempt 67: DUAL-goal probe-gateable-surface re-scan on attempt-66 floor — CHARACTERIZED, probe_gateable_surface_exhausted: true; ZERO code edits. FRESH 1.93.1 baselines reproduce attempt-66 EXACT: default 16 / under-flag 115 (both comm directions vs scratch/leaf67/base_*.txt EMPTY); cargo check --workspace --tests EXIT 0. The 104 under-flag-only IDs survey to: §09-territory JOINTs (generics 20 forwarder transfer-through-return + fat_ptr_iter 15 iterator-handle/catch + recursive_feature/derive 5 aggregate-in-variant + match_alias 5 + higher_order 3 = ~48); Phase-5-coupled liveness/COW (rc_matrix 10 + stress 7 + cow_map_set 2 + string_sso 3 + collections_ext 2 + arc 5 = 29, M-c-banned); per-element NON-block-param dead-after-last-read collection (narrowing 4 + for_yield_option 4 + elem_dec_scope 4 = 12, the attempt-9/10/11 over-fire surface); cli 3 environment-coupled. DECISIVE GROUND-TRUTH (ORI_CHECK_LEAKS + ORI_DUMP_AFTER_ARC oracle vs ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_DUMP_AFTER_BURDEN + /calc) on the survey-named clean (A) candidate narrowing::test_iter_map_on_narrowed_int_list (3 .collect() [int] results read via result[i] __index [borrow], dead-after, inside a deeply-nested if-else): under-flag 3 leaks size=64 / oracle 0 leaks (exit 0 BOTH = pure LEAK). Burden lineage %11/%57/%89: Apply @collect(alloc) -> move-alias -> __index [borrow] -> ZERO decs (net +1 LEAK, /calc 1-0=1); oracle frees via MULTIPLE per-CFG-path dead-value decs (static-text 9/6/2, one per if-else exit path so exactly ONE fires per run). IRREDUCIBLE: the dead-determination of a body-SSA-var collection across a nested if-else is a per-CFG-path structural last-read liveness (emit_dead_at_entry_decs, RL-2 LastReadBeforeScopeExit) with NO alloc-aware-net expression — a whole-var BurdenDec fires on ALL paths (double-free) or NONE (leak), never “exactly one of N exits”; the attempt-9/10/11 over-fire catastrophe surface (459->596/642). Per the OVER-FIRE CAUTION: STOP, do NOT build the structural proxy. cow_map_set::test_cow_map_multiple_forks (COW-fork shared-survives) + string_sso::test_heap_clone_independence (a.clone() buffer-provenance + COW-concat) confirmed JOINT/Phase-5-coupled by source. VERDICT: the genuinely-clean M1-collection-source surface was EXHAUSTED by attempt-66 (its 4 fixes); NO clean alloc-aware-net-expressible probe-gateable leaf remains. §09.2 HANDOFF: the dominant residual dissolves only via §09.2 burden-emission-ACTIVATION (Phase-5 lower/burden_lower/** + emit_burden_ops M-a callee-strip + faithful emit_dead_at_entry_decs with elem_dec_fn accounting + dead-vs-survives-after-concat/COW-shared-survives verdicts) dissolving the predicate stack — NOT the §07B probe tail. GUARDRAILS (no-cure path): default 16 / under-flag 115 EXACT; git status = attempt-66’s 2 files + pre-existing untracked, ZERO new edits; aims-proof diff EMPTY; no git checkout/restore/reset/stash; DID NOT COMMIT. CALCULUS: pure case-(a) READ-only — Realization.lean RL2_dec_at_last_use:194 + rcBalance:83 ALREADY mandate freeing the dead collection (Lean CORRECT); cure is §09.2 Phase-5 (M-c), NOT a probe-tail change; NO .lean/probe-tail edit. Cross-ref: decisions/LEDGER.md §B.2 attempt-67 line.
2026-06-06 — §07B RE-SCOPED to probe-gateable-proof deliverable (the attempt-67 probe_gateable_surface_exhausted inflection actioned via /review-plan; verdict SIGNIFICANT REWORK APPLIED). Big-picture pull-back per the standing directive recognized §07B was mis-scoped: its goal/success_criteria/checkboxes claimed the COMPLETE broad-shape burden ledger + ⊆16 PASS, which attempts 54/55/62/64/65/67 + decisions/11’s ESTABLISHED gate split + the §B.3 anchor establish is §09.2’s (the Phase-5 emission completion is M-c-banned while the predicate stack coexists, attempt-55 broke default 16→61; inseparable from §09.2 predicate-stack retirement). /review-plan (cold audit + 3-reviewer blind-spots + Opus editor + 2-round /tpr-review) re-scoped §07B to its ACHIEVABLE deliverable — probe-gateable self-sufficiency PROOF (under-flag 517→115 via the LEDGER-D08 alloc-aware-net foundation) + §09.2-territory CLASSIFICATION + §07B.4 baseline-16 checked-in fixture + corpus-under-flag gate-test HARNESS — and routed the COMPLETE ledger + ⊆16 PASS VERDICT to §09.2. Four cross-section cohesion-edits landed: §09.2 gained explicit Phase-5 broad-shape emission-completion ownership (curing the 3-reviewer-convergent ownership-orphan); §13 depends_on split to [07B, 09] (tooling-build §07B-gated / corpus-assertion §09-gated); decisions/11 form-(a) now distinguishes the baseline-16 activation-dissolve class from the ~99 JOINT Phase-5-completion class (§09.2 owns BOTH; §09.4 CH-4-deletion gated on FULL-set ⊆baseline verdict); 00-overview node-13 INV-19 exemption + DAG diagrams + BROAD-shapes MSC re-attributed; index roster re-scoped. /tpr-review converged in-cap (round 1: 5 actionable residual-COMPLETE-ledger-language cured; round 2: 4 actionable residual cured; 9 resolved, 0 deferred; post-cure grep zero residual mis-attributions; plan_corpus check clean apart from pre-existing decisions-path warnings). DISPOSITION: the reviewed: true flip is GATED baseline_regression (flip_result.action: gated) — the known-state test baseline b9939de7d (“feat(while)”) is a PRE-SESSION ANCESTOR of HEAD 9e53362ea, so the gate flags the entire session’s burden-work delta (19 §09-territory under-flag predicate_stack_probe::* pins “newly-failing” vs the stale ancestor, +2 fixed, totals +70/+17) as a “regression”; this is a STALE-BASELINE artifact over the cross-scope uncommitted compiler state (attempt-66’s emit_unified.rs cure + 193 probe pins), NOT caused by the plan-content re-scope (plan edits do not change compiler tests). Per skill-control-contract.md §Autopilot Mode hook-failure/cross-scope clause: NOT bypassed, NOT halted; reviewed: true awaits the cross-scope /commit-push cache refresh (state-discipline.md §6 — owned by the parallel session / future user-typed /commit-push --bypass). ALL re-scope edits (§07B + §09 + §13 + decisions/11 + 00-overview + index) uncommitted per the cross-scope dirty-tree charter. Cross-ref: decisions/LEDGER.md §B.2 attempt-67 + the /review-plan verdict.
2026-06-06 — §07B.N two close-gates re-scoped to §07B-achievable form (linear-execution-cure, amend_structure); residual blocker is the cross-scope reviewed: true stale-baseline gate alone. The LINEAR EXECUTION INVARIANT pinned §07B (in-progress, reviewed:false, has_actionable_work:false — 07B.1-07B.4 all [x], 5/9 §07B.N items [x]). Two of the four unchecked §07B.N close gates were MIS-SCOPED as §07B-close gates, mirroring the same §06-SITE/§09.2-ACTIVATION split the RE-SCOPE established: (1) cargo t green; debug + release re-scoped to the §07B-achievable “LANDED probe-gateable pins green + ZERO-new-vs-16-baseline (comm -13 EMPTY at under-flag 115)” — the FULL-corpus cargo t/./test-all.sh ZERO-failures VERDICT is unreachable at §07B by construction (the 16-baseline §09-coupled BUG-04-118/123/121 cohort dissolves ONLY at the §09.2 BurdenInc→RcInc activation per 00-overview L132/L140/L145 + §09 §09.2 L227-228 + LEDGER D09), routed to section-09 §09.2 + 00-overview.md → §10/§12; (2) /tpr-review passed (final); /impl-hygiene-review passed re-scoped to acknowledge the §07B RE-SCOPE /tpr-review already converged in-cap, and routed the FINAL compiler-code-TPR + /impl-hygiene-review of §07B’s cross-scope-uncommitted compiler cures (attempt-66 emit_unified.rs etc.) to section-09 §09.2 where those cures are committed/activated. The other two (Plan annotation cleanup, Plan sync per protocol) remain — genuine §07B-local close-out housekeeping. NOT faking completion, NOT a status:complete edit, NO checkbox flipped to [x] — two mis-scoped close criteria corrected to their achievable form per routing.md §4. RESIDUAL: after this amendment the only blocker to §07B reviewed: true is the cross-scope stale-baseline gate (flip_result.action: gated, baseline b9939de7d is a pre-session ancestor of HEAD — flags the session’s burden-work delta as a “regression”) — NO plan-content cure possible; it awaits the /commit-push cache refresh (state-discipline.md §6, cross-scope, charter forbids Claude-initiated commit). Cross-ref: the 2026-06-06 RE-SCOPED entry above + section-09 §09.2 + 00-overview.md Mission Success Criteria → §10/§12.
2026-06-11 — §07B.N §09.2-owned items MIGRATED OUT + OBE item retired (linear-execution-cure, migrate_items per routing.md §4); §07B.N now carries only §07B-achievable close-out. The LINEAR EXECUTION INVARIANT re-pinned §07B (in-progress, reviewed:false, has_actionable_work:false — 07B.1-07B.4 all [x], §07B.N 5/12). Root cause of the perpetual has_actionable_work:false: four §07B.N unchecked items duplicated trackers that already live as live section-09 §09.2 checkboxes — the blocked-by-annotation-as-cure anti-pattern (routing.md §4: items belonging to a different section are MOVED, not left annotated in place). Removed (work tracked at the existing §09.2 checkboxes, no information loss): (1) the libtest-completeness guard (codex-F1 — §09.2 line 290 false-green guard + line 291 un-ignore own it); (2) the per-ID classification references/attempt-67-classification.csv (opencode-F2 — §09.2 activation owns the per-ID source + the CSV); (3) the FINAL compiler-code-/tpr-review + /impl-hygiene-review of §07B’s compiler cures (§09.2 activation close-gate code-review owns it). One item retired as OBE: the attempt-67 frozen-shape versioning (under-flag-115 / baseline-16) was superseded by §09.2’s 2026-06-08/09 burden-default flip + canonical-metric redefinition (baseline_failing_ids.txt RE-CAPTURED to the gated SET; the under-flag-115/baseline-16 identity no longer exists in-tree to freeze) — the §07B→§13 contract binds the CURRENT fixture; §09 owns its frozen identity at activation. The §07B-achievable test-gate item’s (blocked-by: ...) clause CORRECTED: the cross-scope compiler cures it awaited are now COMMITTED (compiler_repo working tree clean), so the 2026-06-06 “uncommitted cures await /commit-push cache_refresh” premise is OBE — the residual is a state.sh refresh reconciling the stale known-state baseline against committed HEAD per state-discipline.md §6 + the subsequent reviewed:true flip. §07B.N now carries: 5 [x] + the §07B-achievable test gate (body GREEN) + the OBE note + Plan annotation cleanup + Plan sync — all §07B-achievable. NOT faking completion, NO checkbox flipped to [x], NO status:complete edit — duplicated cross-section trackers migrated to their owning §09.2 checkboxes + one OBE item retired per routing.md §4. Cross-ref: section-09 §09.2 (lines 290-292 owning checkboxes) + the 2026-06-06 entries above.
2026-06-11 — /review-plan Step 5 cohesion audit: COHESION-CLEAN at both tiers; no sibling contradiction, no plan-content blocker. Tier-1 (depends_on reachability): depends_on: [07A] is accurate and reachable — section-07A is status: complete + reviewed: true (its narrow-shape standalone-ledger deliverable closed, the §07B precondition met). The 2026-06-06 re-scope cross-section edits form one coherent convergence DAG: section-09 declares depends_on: [07B] (consuming §07B’s completed probe-gateable WORK deliverables — the strengthened corpus-under-flag SET-subset gate + the classification handoff), and section-13 declares depends_on: ["07B", "09"] (the inv19-ratified split-predecessor edge — §13’s TOOLING-BUILD half gates on §07B’s frozen probe-gateable shape, its CORPUS-ASSERTION half on §09’s activation). The 00-overview inv19 node_id: 07B, branch, members: [09, 13] exemption matches the live sibling depends_on topology; no fabricated edge, no linearization violation. Tier-2 (close-out state, non-halt-gating): the section is status: in-review, reviewed: false; 07B.R not-started (no findings — body records “None”), 07B.N in-progress with 3 unchecked items (the §07B-achievable test-gate body-GREEN line, Plan annotation cleanup, Plan sync). The HISTORY documents the reviewed: true flip is gated solely on a cross-scope known-state cache reconciliation (state.sh refresh against committed HEAD per state-discipline.md §6), NOT on any unmet plan-content body condition — the LANDED probe-gateable conditions are empirically GREEN at the attempt-67 floor. This is a close-out-housekeeping residual tracked at the section’s own §07B.N checkboxes, not a Step 5 editor blocker. Anchors the umbrella mission (aims-burden-tracking — burden-path RC-ledger self-sufficiency as the §09.2 predicate-stack-retirement precondition): §07B’s probe-gateable proof + classification + gate-harness IS the precondition §09 + §13 consume. NO checkbox flipped to [x], NO status: / reviewed: edit — cohesion verification recorded only. Cross-ref: section-07A + section-09 §09.2 + section-13 frontmatter depends_on + 00-overview.md inv19_exemptions node_id: 07B.