100%

§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

  • 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).

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

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

  • 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.

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

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)

  • 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.

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

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.