59%

FOLD-IN + SUPERSEDE + GRIND-HERE (plan-wide standing directive — see overview Mission §Bug Fold-In + Supersession, ABSOLUTE). Every failing burden/RC-emission floor cell this section touches is worked HERE as part of this plan’s grind; any BUG-XX-NNN covering it (BUG-04-118 / 142 / 156, the #150 same-allocation-identity class, every sibling RC-emission bug) is FOLDED INTO this plan and SUPERSEDED — NEVER deferred to / routed away as separate bug tracking, a “separate architecture-level pass”, or “already tracked elsewhere”. Dead-end / deferred-compound / reclassified classifications (decisions/LEDGER.md §6) shape WHAT the fix is; they NEVER exit the cell from this plan. If the correct fix is an architecture-level pass, building it IS this plan’s work. Calculus-first per arc.md §CP-1; one terminal gate = ./test-all.sh zero failing cells.

RC-REMARKS CO-EVOLUTION (plan-wide standing directive — see overview Mission §8, ABSOLUTE). This grind is the rc-remarks RC-survivor observability system’s first real test: every floor cell / surviving-RC cluster this section works MUST be grounded via the burden-sole rc-remark stream (ori build --emit-rc-remarks + intel-query.sh rc-survivors --by-cause / rc-cause-rank) before hypothesizing a fix, AND when the stream/analyzer/query falls short for a real cell, improving rc-remarks (producer ori_arc/.../rc_remark.rs, analyzer tools/ori-rc-remarks, intel import_rc_remarks.py + query_graph.py rc-* handlers) IS this section’s work for that cell — never deferred as separate observability work. Burden-sole verdict discipline (arc.md §STOP) unchanged.

§07A Burden-Lowering RC-Ledger Self-Sufficiency

Predicate-stack-retirement precondition discovered during the §09.2 execution attempt. Full diagnosis + empirical evidence: section-09-post-convergence-partial-retirement.md HISTORY 2026-06-03. §09.2 / §09.3 / §09.4 / §09.N are blocked-by this section.

Mission

Close the gap between §07’s COVERAGE-ANALYSIS completeness (class_covered universal, VF-1=0) and RC-LOWERING completeness (a standalone burden ledger that frees every allocation lineage at its true last-use without the predicate stack). The burden path must become a COMPLETE standalone RC emitter — emitting the move-alias / duplication-alias / borrow-flow / collection-buffer RC it currently defers — so that §09.2 can delete the predicate stack + activate real-RC safely.

The proven calculus is the spec, the implementation is the bug: RL-2 (RL2_dec_at_last_use), RL-4, RL-5, CH-1 (CH1_burden_emitted_is_bridge) prove the correct dec placement; lower::burden_lower diverges by deferring to the predicate stack. This section makes the implementation match the proof.

Intelligence Reconnaissance

Queries run 2026-06-03 (scripts/intel-query.sh --human): file-symbols compiler/ori_arc/src/lower/burden_lower; callers emit_burden_ops.

Summary (citation: [ori:compiler/ori_arc/src/lower/burden_lower/emit.rs]):

  • Burden-lowering surface: lower/burden_lower/{mod,emit,terminator,moved_fields}.rs (30 symbols).
  • Dec/inc emission functions to extend: emit.rs::emit_last_use_decs:292 (BurdenDec-at-last-use — must emit the TRUE freeing dec, not defer); emit_fresh_site_burden_inc:361 + emit_owned_position_incs:208 (BurdenInc sites — must suppress move-alias incs); emit_terminator_burden_decs:477 (transfer-point exemptions).
  • Move-alias deferral logic: inc_suppressed_vars / compute_use_counts_and_dup_aliases in mod.rs around the documented mod.rs:261 deferral.
  • Driver: emit_burden_ops runs from drive_steps_4_and_4b (Step 4b slot per aims-rules.md §7 Burden Phases).
  • DP-2 interaction: Phase-6 eliminate_burden_ops currently elides the freeing dec on move-through-Dead lineages; the fix keeps the freeing dec out of DP-2’s elision set by emitting it at the true survivor last-use.

07A.1 Move-alias inc-suppression + true-last-use dec emission in burden_lower

File(s): compiler_repo/compiler/ori_arc/src/lower/burden_lower/mod.rs + emit.rs

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

  • Re-ground at edit time: read lower/burden_lower/mod.rs:261 + the surrounding inc_suppressed_vars / compute_use_counts_and_dup_aliases / transitive-transfer-suppression logic; confirm the verbatim deferral (“the predicate-stack emits the alias’s real RcInc/RcDec, so the alias carries NO burden ops”) still resides there and map the exact deferral surface.

  • Move-alias inc-suppression: a Let { Var(src) } alias where src is consumed at/after the alias is a MOVE — emit NO BurdenInc (no duplication, no inc owed per RL-1). Already partially handled by inc_suppressed_vars; confirm + extend so the move-alias chain (%0→%2→%4) nets correctly WITHOUT the predicate stack.

  • True-last-use dec: emit a BurdenDec at the final last-use of each allocation lineage that SURVIVES DP-2 elimination — NOT elided as move-through-Dead. The freeing dec (RL-2 dec-at-last-use / scope exit) must be in the standalone burden ledger. The bug: DP-2 collapses the move-alias hops as Dead/Absent and elides the very dec that frees the rc=1 allocation.

  • Duplication-alias RcInc/RcDec: when a Let { Var(src) } alias’s source genuinely stays live (duplication, the mod.rs:261 path), the burden path itself emits the inc + matching dec (currently deferred to the predicate stack).

  • Move-vs-duplication classifier as an executable table (the load-bearing decision in 07A.1; specify BEFORE editing burden_lower). For each Let { Var(src) } alias %d = %s, the classifier decides MOVE (no inc owed; the alias forwards the source’s reference) vs DUPLICATION (inc + matching dec owed; source and alias both stay live). Define every case as a table row so the implementation is mechanical, not ad-hoc:

    CaseConditionClassificationBurden emission
    same-block%s used exactly once (at %d’s defining Let) within the same block; no later use of %sMOVENo BurdenInc for %d; %d carries the source’s freeing dec at its true last-use
    cross-block%s used only at %d’s alias and %d flows across a block boundary (Jump arg / block param); %s dead after the aliasMOVENo BurdenInc; freeing dec at %d’s true last-use, RL-4 edge-dec rules apply
    terminator-transfer%s (or %d reached through a move-alias chain) transfers ownership at a terminator transfer point (Return, owned Apply/Invoke arg, owned Jump arg)MOVE (transfer-via-move-alias)No BurdenInc; NO last-use dec on the source — discharged at the transfer point (RL-2 ownership-transferring-use exception; matches compute_transfer_via_move_alias)
    ambiguous post-alias-source-use%s appears in >= 2 used-var positions (the alias use PLUS at least one more downstream use of %s) — source genuinely stays liveDUPLICATIONBurden path emits the alias’s BurdenInc + matching last-use BurdenDec (the mod.rs:261 path the overlay currently defers)

    Ground the table against compute_use_counts_and_dup_aliases (use-count + dup-alias detection) and compute_transfer_via_move_alias (transfer-via-move-alias fixpoint) in mod.rs before editing; the four rows MUST partition every Let { Var(src) } alias (WBS 100% — no overlap, no gap).

07A.2 Collection-buffer + borrow-flow standalone-ledger completeness

File(s): compiler_repo/compiler/ori_arc/src/lower/burden_lower/mod.rs + terminator.rs + moved_fields.rs

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

  • Collection-buffer last-use: let $xs=[1,2,3]; xs.len() must emit a freeing BurdenDec for the list buffer at last-use (today burden-as-sole-emitter emits NO RcDec → leak). Confirm the CollectionBuffer-shape lineage gets its dec in the standalone ledger for ALL three collection backing buffers — list ([T]), Map ({K: V}), and Set (Set<T>) — not list-buffer alone. Map (let $m = {1: 2}; m.len()) and Set (let $s = Set<int>{1, 2}; s.len()) backing buffers share the list-buffer’s CollectionBuffer shape (per the AIMS Shape dimension) and the same deferred-dec gap; each must free its buffer at last-use.
  • Borrow-flow correctness: values flowing through Project borrow chains produce no leak / double-free / UAF in the standalone burden ledger (the borrow paths the predicate stack currently covers). Ground against the proven borrow rules (RL-32/33 borrow inference + the project_alias_sources side-table consumers) before editing.
  • Propagate borrow status through Project in compute_borrowed_alias_vars (compiler_repo/compiler/ori_arc/src/lower/burden_lower/mod.rs:388): today the borrowed-set is seeded from Ownership::Borrowed params and propagated forward only through Let { Var(src) } alias edges, NOT through Project — so a var derived from a borrowed value via Project is not recognized as borrowed and can receive a BurdenDec it does not own (double-free in the standalone ledger). Extend the forward fixpoint to also mark Project { dst, value: borrowed_src, .. } destinations borrowed (per TF-4 borrow propagation), so borrow-derived vars are excluded from BurdenDec.
  • Transfer-point dec exemption parity: confirm the burden path honors the RL-2 ownership-transferring last-use exemptions (Return, Construct/Reuse/CollectionReuse arg, Set value, PartialApply capture, owned Apply/Invoke param, Jump arg per RL-4) in the standalone ledger — a dec at a transfer point would double-free.

07A.3 Self-sufficiency probe + matrix tests (predicate-stack-disabled corpus green)

File(s): test corpus + a predicate-stack-disable probe (NOT shipped activation — §09.2 owns the shipped flip)

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

  • Self-sufficiency probe — ONE mechanism, an env flag mirroring §03A’s ORI_DISABLE_BURDEN_OPS: add a compile-time env-gated ORI_DISABLE_PREDICATE_STACK_RC-style flag (the symmetric twin of ORI_DISABLE_BURDEN_OPS — same gating point at the AIMS pipeline, opposite emitter) under which the predicate-stack RC emitters are suppressed and the burden path is the SOLE RC emitter. NOT an ad-hoc local disable (a local disable cannot be re-run deterministically across the corpus); NOT shipped activation (§09.2 owns the shipped predicate-stack deletion + real-RC activation). The probe MUST assert BOTH: (a) ZERO predicate-stack RcInc/RcDec emission (the predicate stack is genuinely off — guards against a miswired disable still emitting via the predicate path), AND (b) NONZERO burden-originated real RC (BurdenInc → RcInc / BurdenDec → RcDec actually fired — guards against a miswired disable passing only because some fallback RC path covered the gap). Confirm the burden path alone produces a VF-1-balanced ledger.
  • Matrix tests per tests.md §Matrix Testing Rule: move-alias chain (FatVal %0→%2→%4); Let-Var-alias with live source (duplication); collection-buffer last-use; borrow-chain (Project of a projection); closure-capture last-use. Each: semantic pin (standalone ledger nets correct) + negative pin (revert the burden-lowering fix → leak/double-free re-appears). Debug + release; eval + LLVM dual-execution parity.
  • Corpus gate: with the predicate stack disabled, the burden path alone produces an AOT corpus with zero NEW failures vs the predicate-stack baseline (start-of-section baseline AOT 2329/16); ORI_CHECK_LEAKS=1 zero leaks; zero double-frees. This IS the §09.2-readiness gate — §09.2 cannot ship until this passes. (BUG-04-134 field-grain struct_gep blocker RESOLVED — var_field_base_ptr spill-to-alloca landed; corpus gate met: default AOT 16-baseline zero-new, 11 probes green under ORI_CHECK_LEAKS=1.)
  • Tests: cargo t green; debug + release.

07A.R — Third Party Review Findings

Code TPR (/tpr-review work mode, 3 rounds, exit_reason=clean): converged clean. Round 1 — 1 actionable (PUBLIC_LEAK Critical, 3-reviewer agreement): wrapper-private bug-tracker/plans/BUG-04-136 path + BUG-04-136 IDs in collections_ext.rs doc comments + 1 assert message; cured (stripped, prose left self-contained). Round 2 — 1 actionable (COMMENT_HYGIENE_DRIFT decorative-banner Major): Unicode box-drawing banner; cured + litter-pickup of all 21 banners in collections_ext.rs. Round 3 — 0 actionable (clean; prior cures confirmed). Refuted across rounds: codex INVERTED-TDD claim (probe-gating transfer-suppression is the intended burden-path deliverable per RL-2, NOT test-weakening); emit_unified.rs:936 leak (line out of range). Substantive axes verified clean: RC-balance, default-path neutrality, calculus-correctness (var_field_base_ptr/compute_scalar_literal_vars/collect_auto_iter_result/BurdenDecPartial-enum-arm/burden-only-edge-cleanup), phase-boundary integrity.

Hygiene (/impl-hygiene-review, plan context): mandatory lint-fix-to-green gates GREEN (cargo fmt, clippy/clippy-all, enum-drift, sprawl-lint, test-naming). No arc-introduced defects. function_compiler/mod.rs:401 swallowed-error = pre-existing intentional best-effort DWARF attachment (non-arc). Additive findings below are anchored-deferred (pre-existing structural debt / lint-FP / out-of-scope parallel-session — NONE arc-introduced correctness defects; do NOT force-refactor mid-arc — RC-emission-function splits are own correctness-bearing work). Each carries a concrete implementation anchor per CLAUDE.md §ALL Deferrals; they do NOT gate the §07A burden-self-sufficiency close (the §09.2 critical-path precondition):

  • HYG-1 (BLOAT/file-length) — anchored-deferred: 8 file-length + 16 fn-length violations in large emit files (emit_instr 527 lines, edge_cleanup depth-8) — pre-existing, exceed the 500-line compiler limit per compiler-ops.md. Anchor: structural-refactor follow-up via /create-plan (RC-emission split has correctness surface; its own deliverable, not litter-pickup).
  • HYG-2 (tooling-gap, hygiene-lint FP) — anchored-deferred: hygiene-lint counts 89 assert_aot_success(include_str!(...)) AOT tests in collections_ext.rs as “ghost-tests” (no inline assert! macro recognized). False-positive class, not an arc defect. Anchor: /improve-tooling on compiler_repo/scripts/hygiene-lint.py to recognize helper-based assertions.
  • HYG-3 (out-of-scope, informational): loops.ori test-weakening (2) = parallel-session ori_fmt work, not this arc; delivery-drift (17 MISSING_PROPAGATION) = pre-existing corpus. No arc action.

07A.N Completion Checklist

  • Move-alias inc-suppression + true-last-use dec emission landed (07A.1).
  • Collection-buffer + borrow-flow standalone-ledger completeness landed (07A.2).
  • Self-sufficiency probe + matrix tests green; predicate-stack-disabled corpus zero-new-failures + leak-free + double-free-free (07A.3).
  • cargo t green; debug + release; eval + LLVM parity.
  • /tpr-review passed; /impl-hygiene-review passed. /tpr-review work-mode 3 rounds exit_reason=clean (R3 0-actionable); /impl-hygiene-review plan-context lint-fix-to-green gates GREEN, no arc-introduced defects (§07A.R)
  • Plan sync per protocol: §09 unblocked (the §09.2-readiness gate passes); record §07A completion in 00-overview HISTORY.

HISTORY

  • 2026-06-04 — §07A.3 burden-path self-sufficiency landed + reviewed; close-out commit DEFERRED on user-authority /commit-push --bypass. Burden-emission codegen-lowering self-sufficiency chain complete: BUG-04-133 (live TypeRegistry::from_typed_exports threading through FunctionCompiler, probe-gated so default path byte-identical) → 134 (var_field_base_ptr spill-to-alloca before field-grain struct_gep, AB-5/FastISel; struct_gep crashes 332→0) → 135 (compute_scalar_literal_vars excludes scalar-Literal markers from BurdenDec over-collection, AIMS:L-9/TF-1; extract_value 66→0, ~22 default failures cured) → 136 (collect_auto_iter_result collects lazy iter handle into declared collection; iter-handle crashes→0) → 137 (BurdenDecPartial DropKind::Enum arm + populate_moved_out_fields scalar-projection gate; 15→1 crash) → 138 (emit_burden_path_probe_tail burden-only edge cleanup, Phase-6.5; heap-Err leak→0). Probe = ORI_DISABLE_PREDICATE_STACK_RC (twin of ORI_DISABLE_BURDEN_OPS; arc.md §Debugging). Default AOT held at 16-failure baseline (zero-new); ~25 default failures cured; 11 probes green under ORI_CHECK_LEAKS=1. Code-TPR clean (3 rounds, §07A.R) + hygiene-lint green (§07A.R). Working tree (~40 files across ori_arc/ori_llvm/ori_types/oric + §07A plan) UNCOMMITTED: /commit-push gate is baseline-red (the 16 §09.2/§12-owned predicate-stack AOT failures), so per skill-control-contract.md §Autopilot Mode the autopilot proceeds WITHOUT committing — the commit lands via user-typed /commit-push --bypass (Claude never initiates). The §09.2-readiness gate (07A.3 corpus gate) is MET; §09.2 (predicate-stack retirement → the 16 baseline failures dissolve → green test-all) unblocks once this section’s work is committed + closed. BUG-04-133..138 deliverables verified; tracker close-out flips with the commit.
  • 2026-06-03 — §07A created (discovered prerequisite, routing.md §3 case c). §09.2 execution empirically proved the burden path is not a complete standalone RC emitter — lower::burden_lower defers move/duplication/borrow-alias RC to the predicate stack (mod.rs:261 verbatim), so burden-as-sole-emitter regressed AOT 2329/16 → 1300/1045. §07’s class_covered-universality + VF-1=0 is coverage-analysis completeness, not RC-lowering completeness. §07A closes the gap (standalone burden ledger frees every lineage at true last-use) as the §09.2 predicate-stack-retirement precondition. Full diagnosis: section-09 HISTORY 2026-06-03. depends_on §07; §09.2/09.3/09.4/09.N blocked-by §07A.

Work Items

  • ITEM-2 — class_covered: BitSet<ClassId> in AimsStateMap. Compute in aims/intraprocedural/post_convergence.rs adjacent to existing detect_trmc_candidates (line 445). Algorithm: walk per-class membership (class_members[C] per existing ssa_alias_classes infrastructure consumed at aims/intraprocedural/) + transitive payload obligations (class_payload_of[C]). class_covered[C] = (∀ v ∈ class_members[C]: burden_emitted[v]) ∧ (∀ payload_class P transitively reachable from C via class_payload_of: class_covered[P]). Fixed-point computation: iterate until no new classes covered (termination by finite class set per aims-rules.md §1.8 L-5).
  • ITEM-3 — Predicate-stack realization defers to burden walk on covered classes. Existing aims/realize/emit_unified.rs::realize_rc_reuse walks per-block; at each RcInc/RcDec emission decision site, consult state_map.class_covered[class_of(var)]. If true, SKIP the emission (burden walk owns those decs). If false, proceed with existing predicate-stack emission. Mixed-coverage classes (NOT yet fully covered) fall through to predicate stack — no partial-class skipping. Decision site: decide.rs::decide() (line 179) — add class_covered parameter to DecisionContext; the function returns RcDecision::None when class_covered is true for the target var’s class. Existing call sites pass state_map.class_covered slice.
  • ITEM-4 — Positive pin: class fully burden-owned → predicate stack skips. Fixture in aims/realize/burden_elim/tests.rs::class_fully_covered_predicate_stack_skips — synthetic ArcFunction where every var in class C has burden_emitted = true and class_covered[C] = true; predicate-stack realization emits ZERO RcInc/RcDec for class-C vars (only burden ops survive elimination).
  • ITEM-5 — Negative pin: mixed-coverage class → predicate stack runs as today. Fixture aims/realize/burden_elim/tests.rs::mixed_coverage_predicate_stack_runs — synthetic ArcFunction where ONE var in class C lacks burden_emitted; class_covered[C] = false; predicate stack emits RC ops for the entire class (no partial-class skipping). Asserts via count_rc_ops helper at aims/realize/emit_unified.rs:383.
  • Tests: class fully burden-owned → predicate stack skips dec emission; mixed-coverage class → predicate stack runs as pre-§04A.
  • Coexistence handshake landed: burden_emitted on ArcFunction + class_covered in AimsStateMap + predicate-stack realization defers on covered classes (§04A.3 ITEMs 1-3); positive pin (§04A.3 ITEM-4) + negative pin (§04A.3 ITEM-5) green.

Items

  • Re-ground at edit time against the CURRENT mission (content/overview/mission.md, not the stale section-body Intelligence Reconnaissance): read ownership_scans/dup_inc.rs::compute_use_counts_and_dup_aliases + compute_genuine_dup_move_aliases (the actual move-vs-duplication classifier, already implemented) and the surrounding ~30-file ownership_scans/ family. Confirm which of this section’s remaining work_items describe work already shipped there vs a genuine residual gap, before authoring any new classifier code — a new per-shape scan/table here is the named anti-pattern (mission §6.1 “the per-shape-surgical trap”).
  • Verify (do not re-implement) that compute_use_counts_and_dup_aliases’s existing MOVE classification (dup_inc.rs) correctly nets a move-alias chain (%0->%2->%4) without the predicate stack: no BurdenInc for a use_counts<2 alias, no double-suppression when forwarder_transparent_aliases also applies. Add a matrix test for the multi-hop chain case if none exists; do not add new classifier logic — the classifier already exists and is proof-cited.
  • Fold in and complete BUG-04-145 (bug-tracker/plans/BUG-04-145/) HERE per the section’s FOLD-IN directive: burden_elim.rs::mark_whole_var_removals queries var_state_at_block_exit for a fresh single-use Construct consumed at a borrowing operand, which returns Dead/BOTTOM instead of the TF-11 converged backward-demand state at the definition, so DP-3 is_additional_credit_elidable never fires and the fresh-site logical additional-credit event survives without its matching RL-2 release — a leak. The observed BurdenInc/BurdenDec pair is transitional Phase-6 carrier evidence. Fix: query the converged backward-demand state at the var’s definition (§CP-1 case (a), already Lean-verified per BUG-04-145 §05 — no calculus change needed). Land BUG-04-145’s implementation + its own matrix as this item’s deliverable.
  • Verify (not author) that the duplication-alias path (dup_alias_dsts from compute_use_counts_and_dup_aliases, paired through the Phase-6 pair-atomic elision in burden_elim.rs) emits its inc + matching dec correctly in the standalone burden ledger with the predicate stack disabled — add a matrix case if a genuine gap is found; do not re-implement the classifier.
  • Run the EXISTING self-sufficiency probe (ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1, already implemented and documented in arc.md; drives compiler_repo/compiler/ori_llvm/tests/aot/predicate_stack_probe.rs) against the current corpus. Confirm BOTH: (a) zero predicate-stack RcInc/RcDec emission is genuinely achieved (not just the flag being set), and (b) nonzero burden-originated real RC actually fires. Ground the current pass/fail state via compiler_repo/diagnostics/aot-guardrail.sh --floor (the mission’s §4 collapse-metric probe) rather than assuming the probe needs to be built.
  • Corpus gate: with the predicate stack disabled (the gated burden-sole probe), the burden path alone produces an AOT corpus with zero NEW failures vs the CURRENT baseline (re-derive via compiler_repo/diagnostics/aot-guardrail.sh --floor at execution time — do not trust the section’s 2026-06-04 HISTORY figure of 16, which the dossier’s fresh recon shows has since moved); ORI_CHECK_LEAKS=1 zero leaks; zero double-frees. This is the §09.2-readiness gate — §09.2 cannot ship until this passes.
  • 07A.1 landed: BUG-04-145’s DP-3 converged-at-def-demand fix folded in and shipped; move-alias inc-suppression and duplication-alias RcInc/RcDec paths in ownership_scans/dup_inc.rs verified correct against the standalone burden ledger (no new classifier table authored — existing logic confirmed sufficient).
  • Resolve the Attack-B open question from the intel dossier (§7.1) before landing any (var,field) partition work touched by this section: does the mission’s §2.2 per-field allocation-identity partition subsume, extend, or duplicate the existing, separately-proven IA-MF1 moved-out-fields fixpoint (moved_fields/dataflow.rs, propagate_moved_out_fields, arc.md HISTORY 2026-07-02 / BUG-04-240)? If this section’s Project-propagation fix (w-d4472adb) or any downstream work touches per-field allocation identity, ground it against this open question first — landing a parallel per-field analysis without resolving it risks a LEAK:aims-ad-hoc-emission finding per Invariant 5.
  • Check for an active parallel session before touching union_find.rs, same_alloc_reps, cleanup_redundant.rs, or live_extract.rs — the ledger repeatedly (attempts 271/273/274/275, and the most recent KEPT attempt 289, 2026-06-30) records these as parallel-session domain with a collision ban. Attempt-289’s DO-NOT-RE-TRY is directly relevant to any locality-blocked BurdenInc work this section’s items touch: sound keep-alive elision on a locality-blocked survivor must be WHOLE-PAIR via a same_alloc_reps MERGE, never a per-var inc-only split (the per-var split causes premature free / the attempt-287 mass-UAF class).

Fresh intel (regenerated)

This section is not a routine implementation task — it is live, contested, and mid-supersession. Three facts change what “doing this section” means:

  1. The section’s own approach is the thing the plan’s current mission wants to retire. §07A’s Intelligence Reconnaissance cites a “move-vs-duplication classifier as an executable table” at mod.rs:261 — but that logic has evolved into a ~971-symbol, 30-file ownership_scans/ subsystem of independently-toggled per-shape scans (ORI_DISABLE_* × ~50), and the plan’s regrounded mission (content/overview/mission.md, superseded 2026-06-19) explicitly names this exact family — move_alias, dup_inc, call_arg_dup, store_dup, construct_fed, sibling_union, same_alloc_reps — as the target of a generalization the mission wants to COLLAPSE into two inferred, Lean-proven properties (§2.1 frame-limited ownership, §2.2 per-field allocation-identity partition). Treating §07A as “add another scan” is now explicitly the dead-end the mission’s §6.1 calls “the per-shape-surgical trap.”
  2. The section’s cited source lines are stale. mod.rs:261 — the exact citation in the section body’s Intelligence Reconnaissance — no longer contains the deferral logic it describes; mod.rs is now 612 lines of ONLY ORI_DISABLE_* LazyLock definitions. The classifier the section prescribes now lives in ownership_scans/dup_inc.rs::compute_use_counts_and_dup_aliases, already implemented, already far more elaborate than the section’s 4-row table, and untested by direct unit calls (0 test-caller edges).
  3. A live, open, high-severity bug (BUG-04-145) reproduces exactly the coverage gap §07A exists to close — a heap payload inside an inline aggregate leaks on the borrow-terminal path of ==, on BOTH ORI_DISABLE_BURDEN_OPS=1 and ORI_DISABLE_PREDICATE_STACK_RC=1 (burden-sole) — i.e. the burden path is STILL not self-sufficient for this shape, in-progress at BUG-04-145 §03, unresolved since 2026-06-07.

Decisions this package forces before any code is written:

  1. Read the mission reground FIRST (content/overview/mission.md, all of it) — it supersedes the method §07A’s body prescribes, though it retains calculus-first + predicate-stack-legacy + burden-path-of-record unchanged.
  2. Do not add a 31st ownership_scans/*.rs file or a new ORI_DISABLE_* toggle to close a residual leak — that is the explicitly-named dead-end (§6.1 “the per-shape-surgical trap”); route toward the frame-limited-ownership / per-field-partition generalization instead, or coordinate with whichever session is developing compute_same_alloc_reps/union_find.rs (per the ledger’s own repeated “parallel-session domain, collision-banned” verdicts).
  3. The RC-remarks stream says locality (70 survivors) dominates cardinality (32 survivors) as the proof-failure cause — that is the leverage-ranked worklist, not a scan-by-scan floor hunt.
  4. Coordinate with BUG-04-145 (open, high, in-progress at §03) before treating any inline-aggregate-borrow-leak as a fresh discovery — it is the SAME failure family this section’s Fold-In directive already requires folding in.
  5. The Ledger’s attempt-289 (KEPT, 2026-06-30, most recent) is the current live thread: a Lean-discharged “keep-alive redundancy” theorem proving sound elision must be WHOLE-PAIR via a same_alloc_reps MERGE, never a per-var inc-only split — read it before hypothesizing any locality-blocked survivor fix.

[JOIN]: the mission’s own §1.2 combination table cites phase-6...--s-09a822f6.intel.md as documenting eliminate_burden_ops hotspot 1580 — the graph’s current churn query returns emit_burden_ops (a sibling function in scan_orchestration.rs) at hotspot 1658.6, the single highest-churn symbol in the entire 971-symbol burden_lower subsystem — confirming the mission’s claim that this Phase-5/6 boundary is “the single substrate under the hottest, most-reverted code on the burden surface” is current, not stale.

DIG DEEPER

python -m scripts.plan_corpus.read plans/aims-burden-tracking --completion
scripts/intel-query.sh plan-status aims-burden-tracking --human

(full dossier: burden-lowering-rc-ledger-self-sufficiency-predicate-stack—s-b14a3bfd.intel.md)