Section 03A: Emission-Fidelity Repair

Goal (reconciled to the (C) coexistence verdict — LEDGER §B.2 + the 2026-05-30 B-full->C reversal): Make the Phase-5 burden emission faithful to the proven RL-1 / RL-2 calculus AT INSTRUCTION + CFG-EDGE grain (LANDED §03A.1/§03A.2), exclude immortals, and bring the per-value burden ledger to function-exit VF-1-balance against the predicate-stack RC ledger via the (C) coexistence-mirror (burden_mirror.rs) so codegen is VF-1-clean and the §06/§09 work is testable. The proven model is COEXISTENCE (CH-comp case 1: coexistence_dispatch ≡ burden_emission_path ≡ predicate_stack_path), NOT self-sufficiency. SELF-SUFFICIENT emission — emission ALONE (elimination disabled, predicate-stack retired) dissolving the BUG-04-118 double-frees with the burden ledger netting 0 unaided — is DEFERRED-WITH-ANCHOR to §09 (predicate-stack retirement; the §06 realize-rewrite home), per LEDGER §B.2. This is the emission half of the §04B impl-fidelity verdict; the elimination/coverage/retirement half is the reframed §05 / §07 / §09.

Context (per the 2026-05-29 reground + 2026-05-30 depends_on cut — 00-overview.md HISTORY + §04B HISTORY + §03A HISTORY): §03 (“Phase 5 Trivial Emission”) shipped status: complete on its unit-test evidence (48 burden_lower + 5 verify_burden_balance tests). The §04B Prototype-Gate Criterion-1 run SURFACED the divergence as EVIDENCE: under ORI_DISABLE_BURDEN_ELIM=1 (emission alone), 4 of the 16 BUG-04-118 fail-baseline match_alias::* tests still fail (test_match_arm_alias_result_str, test_option_intlist_select_branch_return, test_unwind_path_alias, test_closure_three_call_no_leak), and the broader corpus shows burden imbalance (VF-1): vN net=±1 ICEs. The §04B Criterion-1 evidence artifact (decisions/gate-criterion-1-evidence.md, 12/16 baseline) is the INPUT §03A consumes and the target §03A PRODUCES (12/16 → 16/16) — NOT a blocking dependency edge: §03A depends_on: ["03"] (the §04B cycle edge was cut 2026-05-30 to unblock §03A on the critical-path VF-1 burden-imbalance cure per the §03A HISTORY entry). §03’s success-criterion 4 (“per-edge balance predicate holds on emitted IR”) is therefore NOT actually met. The AIMS calculus the emission must match is kernel-proven (363 theorems, zero sorry, in compiler_repo/aims-proof/lean/AimsProof/): RL1_emit_iff_not_elidable + RL2_dec_at_last_use (Realization.lean), DP3_is_rc_inc_elidable_table (Decision.lean), the rcBalance net-0 invariant (Realization.lean). Per arc.md §Debugging, a proven rule + a failing program means the IMPL diverged at a specific site; the cure fixes the code, never the rule.

Why a sibling section (routing.md §3 case b), not a §03 re-open: §03’s trivial-emission walker is shipped and its unit suite is green; the divergence is a fidelity gap the §04B Prototype-Gate Criterion-1 run SURFACED as evidence. §03A is the independently-workable repair deliverable (own success_criteria, own regression gate, completable cold) that depends ONLY on §03 (the emission it repairs). It feeds §05 (faithful emission is the baseline Phase-6 elimination optimizes over) — §05 reaches §03A through the linear depends_on chain (section-05 frontmatter depends_on: ["04B"]; §03A is the upstream linear predecessor per §05’s §03A-predecessor note, NOT a direct depends_on entry).

Depends on: §03 (Phase-5 emission — the emission §03A repairs). The §04B Criterion-1 evidence (decisions/gate-criterion-1-evidence.md) is an INPUT artifact §03A consumes + PRODUCES toward (12/16 → 16/16), not a dependency edge; §04A is a companion fix (VF-1 verifier-robustness: emit a diagnostic, not ICE). depends_on: ["03"] — the §04B cycle edge was cut 2026-05-30 (see §03A HISTORY); do NOT re-add §04B to depends_on.

Reference (proven calculus — the fidelity targets):

• compiler_repo/aims-proof/lean/AimsProof/Realization.lean — RL1_emit_iff_not_elidable (RL-1), RL2_dec_at_last_use + the 11-kind TerminalUse partition (RL-2), rcBalance / rcBalance_matched_pair (RC-balance net-0). Paired .proof: compiler_repo/aims-proof/proofs/08-realization/RL-1.proof + RL-2.proof + RL-4.proof (edge-balance).
• compiler_repo/aims-proof/lean/AimsProof/Decision.lean — DP3_is_rc_inc_elidable_table (Once ∧ Linear), DP2_is_rc_dec_unnecessary_table. Paired .proof: compiler_repo/aims-proof/proofs/05-decisions/DP-3.proof + DP-2.proof.
• compiler_repo/aims-proof/lean/AimsProof/Verification.lean — VF-comp failure-class coverage (a fix passing a strict subset of layers is rejected). Paired .proof: compiler_repo/aims-proof/proofs/09-verification/VF-comp.proof.
• plans/aims-burden-tracking/decisions/07-predicate-stack-overemission-empirical-ruleout.md — the BUG-04-123 §05 rule-out catalogue. The 3 over-emission match_alias cells in 03A.3 ARE BUG-04-123’s over-emission cells; §5 carries the precise predicate-stack root (InlineEnum container dec recursing into the moved-out payload; unwind-edge foils post-dominance) + the 4 ruled-out predicate-stack suppression models. Do NOT port a predicate-stack suppression patch — the burden cure is the Model-B shallow container drop (the BurdenDec must skip the moved-out payload slot) + the payload’s own BurdenDec at scope exit.

Intelligence Reconnaissance

Queries:

• scripts/intel-query.sh --human file-symbols "compiler_repo/compiler/ori_arc/src/lower/burden_lower" --repo ori — BurdenInc/BurdenDec emission sites this section repairs
• scripts/intel-query.sh --human callers "verify_burden_balance" --repo ori — the VF-1 burden-balance verifier consuming emitted IR
• scripts/intel-query.sh --human similar "emit_rc_inc" --repo koka,lean4 --limit 5 — Perceus dup/drop emission prior art

Queried: 2026-05-29.

Results summary (≤500 chars) [ori]: burden-op emission lives in ori_arc::lower::burden_lower (+ helpers); per-edge balance is checked by verify_burden_balance / verify_trmc_burden_balance (the VF-1 ICE source). Fidelity target = the proven RL-1/RL-2/rcBalance theorems in consolidated aims-proof/lean/AimsProof/Realization.lean (363 kernel-checked, zero sorry). Repair aligns emission to the proven predicates — extends the unified model per missions.md §AIMS invariant 5; no parallel paths, no shadow trackers.

03A.1 RL-1 BurdenInc-fidelity audit + repair

• Audit every BurdenInc emission site in compiler_repo/compiler/ori_arc/src/lower/burden_lower/ (the mod.rs/emit.rs/moved_fields.rs/terminator.rs helpers) against RL-1 (Realization.lean RL1_emit_iff_not_elidable): an inc is emitted on a duplicating use IFF NOT is_rc_inc_elidable (NOT move-once-linear = NOT Cardinality=Once ∧ Consumption=Linear). Enumerate sites where emission over- or under-emits relative to the proven predicate.
• Cross-check the per-instruction inc-emission (Construct / Apply / ApplyIndirect / PartialApply / CollectionReuse / Set) against the proven is_rc_inc_elidable (DP-3): the FRESH-site inc + per-owned-arg inc must agree with the move-once-linear elision exactly.
• Tests (TDD-first per tests.md §TDD for Bugs): write the failing matrix BEFORE the fix — inc-fidelity cells across {str, [int], Option, Result-payload, closure-env} × {single-use move-once, multi-use duplication}; semantic pin (inc emitted exactly on duplication) + negative pin (a move-once value emits NO inc).

§03A.1 Diagnostic — net=1 root localized (2026-05-30)

• Minimal repro type Box = { s: str }; @main = { let b = Box { s: "hello" }; let n = b.s.length(); () } reproduces burden imbalance (VF-1): v0 net=1 expected=0 under ORI_VERIFY_ARC=1 (the 643-failure shape, BUG-04-121).
• CORRECTED via big-picture pull-back (supersedes the earlier RL-1-over-emission reading). Diverse-shape sweep under ORI_VERIFY_ARC=1: bare str (let s = "hi"; s.length()), [int] list literal, and struct-with-int field are ALL clean; ONLY a heap value stored into a struct field (Box { s: str }) hits v0 net=1. So the root is NOT a blanket FRESH-site over-emission.
• Decisive ORI_DUMP_AFTER_ARC=1 clean-vs-broken comparison:
  • CLEAN (bare str): burden_inc %0 paired with burden_dec %0 at definition (provisional-ownership temp pair) → net=0.
  • BROKEN (str-in-struct): burden_inc %0 emitted, then %0 move-transferred via Construct Struct(Box)(%0); the paired burden_dec %0 is transfer-suppressed (RL-2: no dec at a ConstructArg transfer — the Box’s RcDec %3 [AggFields] owns the dec) → the FRESH-site inc is ORPHANED → net=1.
• Root class: asymmetric transfer-suppression. The FRESH-site burden_inc (emit_fresh_site_burden_inc, burden_lower.rs:1251) is emitted UNCONDITIONALLY, but its paired burden_dec is transfer-suppressed by the RL-2 dec loop when the value is moved into an owned position. The OWNED-ARG path already solved this symmetrically (§04A.5 ITEM-3, burden_lower.rs:1111-1134: “Suppressing both Inc + Dec keeps the coexistence handshake clean”); the FRESH-site path was not given the same treatment.
• Cure (RL-1/RL-2 symmetric, NOT is_rc_inc_elidable): suppress the FRESH-site inc exactly when its paired dec is transfer-suppressed — i.e. when the fresh dst is move-transferred into an owned position. Gate on the SAME transfer signal the RL-2 dec-suppression uses (instr_transfer_vars / full_move_vars / the transfer-points set from detect_transfer_points at burden_lower.rs:191), NOT on is_rc_inc_elidable — both clean and broken cases are Once ∧ Linear, so an is_rc_inc_elidable gate would orphan the CLEAN case’s paired burden_dec %0 into net=−1 (the decisions/07 over-restriction failure mode).
• Negative pin (decisions/07 guard — MANDATORY in the TDD matrix): the bare-str / list-literal / borrowed cases (paired inc+dec, NOT transferred) MUST stay net=0; the fix touches ONLY the move-transferred-into-owned-position case.
• Remaining grounding before fix: confirm whether dst of a FRESH-allocating instr is reachable in the transfer set at emit_fresh_site_burden_inc time (read detect_transfer_points + the transfer_points/full_move_vars fields). Cure surface: emit_fresh_site_burden_inc (:1251). Tests: burden_lower/tests.rs matrix {str, [int]→struct-field, Option, Result-payload, closure-env} × {borrowed/temp (net=0, untouched), move-into-Construct (net=0 after fix)}. Verify: ORI_VERIFY_ARC=1 cargo test --release -p ori_llvm --test aot 643 clear + dual-exec + ORI_CHECK_LEAKS=1 + section-close /tpr-review.

§03A.1 IMPLEMENTED (2026-05-30) — FRESH-site inc transfer-suppression

• Fix landed in emit_burden_ops (burden_lower.rs): precompute inc_suppressed_vars = vars whose paired BurdenDec is transfer-suppressed at their last-use (mirrors the EXACT instruction-level dec-suppression at :1221: instr_transfer_vars(last_use_instr).contains(var) || full_move_vars.contains(var)); thread into BurdenAnalysisCtx; gate the FRESH-site inc in emit_fresh_site_burden_inc on !inc_suppressed_vars.contains(dst). Terminator transfers deliberately EXCLUDED (their inc/dec pair is emitted by emit_terminator_burden_{incs,decs}, separate from the FRESH-site inc — including them over-suppressed). No AimsStateMap threading needed (the earlier option-(a) design was an artifact of the superseded RL-1-over-emission reading).
• Validation: ORI_VERIFY_ARC=1 cargo test -p ori_llvm --test aot arc:: → 58 pass (was ~all net=+1 failing). Minimal repros: Box { s: str } clears net=1; bare-str / list / struct-int / nested stay net=0 (negative pins hold). Dual-exec parity (interpreter == LLVM hello) + ORI_CHECK_LEAKS=1 zero leaks on the str-in-struct repro.

§03A.2 HANDOFF — alias-chain net=−1 (precisely localized, pre-existing, NOT from §03A.1)

• arc::test_arc_alias_chain_{no_double_free,three_way_use} remain RED at v2 net=−1 AFTER the §03A.1 fix. Fixture: @main () -> int = { let a = "..."; let b = a; let c = b; if a == b && b == c then 0 else 1 }.
• ORI_DUMP_AFTER_ARC=1: %2 = Let Var(%0) (alias b = a) gets burden_dec %2 at last-use but NO burden_inc %2 — Let { Var } is not a FRESH-allocating instr, so emit_fresh_site_burden_inc never emitted an inc for it (before OR after §03A.1). The alias’s inc is on the predicate-stack (RcInc %2 [FatPtr]). Root class: RL-2 BurdenDec emitted for a transparent Let-Var alias whose matching inc is predicate-stack-managed = coexistence-handshake mismatch (§03A.2 / §03A.3 cross-class alias-chain). Independent of §03A.1: my fix only suppresses incs, and %2 had none; %0’s inc stays (correctly — %0 is aliased, not move-once-transferred).
• §03A.2 cure direction: either suppress the burden_dec for transparent Let-Var aliases (predicate-stack owns their RC) OR emit a matching burden_inc — must preserve the §04A.3 coexistence handshake (burden_emitted / class_covered) so the 58 §03A.1-cleared tests do not regress. Cure surface: compute_owned_vars_needing_rc (alias filter) or the RL-2 dec loop (:1186-1233). MANDATORY negative pin: the 58 arc tests + move-once repros stay net=0.
• §03A.2 EMPIRICAL LEARNING (2026-05-30, attempted + reverted): a BLANKET Let { Var } burden_inc (adding the case to emit_fresh_site_burden_inc, gated only on inc_suppressed_vars) clears alias_chain_no_double_free BUT regresses test_arc_loop_string_reassignment_correctness (was net=0, became imbalanced) — over-emits for MOVE-aliases (source dead) and loop back-edges where the predicate-stack does NOT emit RcInc. Reverted; §03A.1-only state restored (58/2). The precise §03A.2 cure is cardinality-gated.
• §03A.2 LANDED (2026-05-30) — dup-alias dec-suppression (option B, not inc): chose to SUPPRESS the burden_dec for a duplication Let-Var alias rather than ADD an inc — the alias’s RC is fully predicate-stack-managed (RcInc/RcDec), so for the coexistence handshake it must carry NO burden ops. Avoided the AimsStateMap threading (which is 55-site PARAM_SPRAWL: emit_burden_ops has ~55 test call sites): the dup signal is computed IN emit_burden_ops from the IR — dup_alias_dsts = Let { Var(src) } dsts where src appears in ≥2 used-var positions (stays live = duplication); a move-alias (src used once) keeps its dec to balance the source’s FRESH inc. Threaded via the INTERNAL BurdenAnalysisCtx (no signature change, no sprawl); added to the RL-2 dec-suppression at :1221 alongside transfer_vars/full_move_vars. RESULT: arc:: AOT suite 60 passed / 0 failed under ORI_VERIFY_ARC=1 (was 58/2). Regression clamps held: loop_string_reassignment + the 58 §03A.1 tests stay green; move-once repros stay net=0. Dual-exec parity (interp exit 0 == LLVM exit 0) + zero leaks on both alias-chain fixtures. Permanent pins: arc_struct_with_string_field.ori (§03A.1), arc_alias_chain_{no_double_free,three_way_use}.ori (§03A.2).

§03A BIG-PICTURE PULL-BACK (2026-05-30) — full-AOT sweep: systemic fidelity, NOT 2-3 root classes

• Full ori_llvm --test aot under ORI_VERIFY_ARC=1: 2170 passed / 133 failed (was ~643 failing pre-§03A — §03A.1+2 cleared ~510). The 133 remaining carry 139 VF-1 burden-imbalance lines: 90 net=+1, 44 net=-1 (zero net>=2 / net<=-2 — all single-unit imbalances). Plus 16 runtime double_free (the net=-1 leak shape) + 3 E2043.
• Failing categories: generics(15), match_alias(13), fat_matrix(13), fat_ptr_iter(12), recursive_feature(9), rc_matrix(9), traits(7), string_sso(6), tagless_enum(4), poly_lambda_mono(4), narrowing(4), higher_order(4), recursive_derive(3), enum_discriminant(3), spec(3) …
• Interpretation (scope check per mission directive): the remaining 133 are the SAME two imbalance kinds (net=+1 FRESH-site/owned-arg inc whose dec is suppressed; net=-1 dec emitted for a value whose inc is predicate-stack-managed) recurring across MORE instruction shapes — generic monomorphization, iterator-protocol builtins, fat-ptr ops, recursive-type drop glue, trait dispatch, SSO strings. The symmetric inc/dec principle from §03A.1+2 is correct and load-bearing; it must be EXTENDED to these shapes. The §03A plan does NOT need restructuring (the principle holds); the EXECUTION is broader than 2 cases — §03A.3 (cross-class) + the §03A.4 matrix own the extension, and additional emit_burden_ops gating per shape (terminator-transfer FRESH values for net=+1; Project/Select/other-alias dec-suppression for net=-1) is the cure pattern.
• 3rd gate LANDED — dead-value inc-suppression (2026-05-30): a FRESH value never used (e.g. shadowed let rebind let s="a"; let s="b") gets a FRESH-site burden_inc but no last-use burden_dec; the predicate-stack emits its RL-2 dead-value cleanup RcDec. Suppress the orphaned inc (vars absent from the use_counts map). Cleared let_rebind shape; full AOT 2172/131 (was 2170/133). Move-once + alias-chain + arc:: clamps hold.
• SCOPE-DEFINING PULL-BACK (2026-05-30) — remaining 131 are CFG-edge dec placement, NOT a long tail: sampling shows the dominant remaining cluster is control-flow (_break_continue, _for_loop, for_yield, control_flow, _question_mark, _recursion, fat_ptr_iter) + derive methods. The trivial burden emission places burden_dec at PER-BLOCK last-use only; it lacks RL-4 edge-specific decs (value live at block exit but dead at successor entry → dec on that CFG edge — loops/branches/Invoke-unwind) and RL-5 dead-at-entry block-param cleanup. The predicate-stack (realize_rc_reuse) DOES these, so the burden ledger diverges from it on every multi-block CFG. Example: iterator for x in xs — %16="" borrowed by Invoke @concat(...) normal bbN unwind bbM; its dec must land on both edges, but the per-block dec misplaces it → net=+1.
• ARCHITECTURAL DIRECTION for §03A.3: the burden DEC emission must gain CFG-edge awareness mirroring the predicate-stack’s RL-2/RL-4/RL-5 placement (last-use + edge-specific + dead-at-entry), computed from block-boundary liveness. This is liveness-based (needs var_state_at_block_{entry,exit} cardinality OR an IR-derived block-boundary live set — same data the predicate-stack’s edge analysis uses). NOT the 55-site AimsStateMap param sprawl: compute the block-boundary live set IN emit_burden_ops from func.blocks CFG + use_counts/last_uses, thread via internal BurdenAnalysisCtx. This is a substantial subsection (the §03A.3 cross-class + edge-cleanup piece), NOT a trivial gate — careful TDD against the 2172-passing clamp, round-by-round per CFG shape (loop back-edge, branch-merge, Invoke-unwind, dead-at-entry block-param). THEN dual-exec + leaks + /tpr-review + /impl-hygiene-review + commit (full AOT green required for §03A.4 VF-1-clean gate). The 3 landed gates (§03A.1+2+dead-value) are durable in the working tree.

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

03A.2 RL-2 BurdenDec-fidelity audit + repair

• Audit every BurdenDec / BurdenDecPartial / BurdenDecField / BurdenDecVariant emission site against RL-2 (Realization.lean RL2_dec_at_last_use + the TerminalUse partition): a dec is emitted at a terminal use IFF the use does NOT transfer ownership. The 8 transfer kinds {Return, ConstructArg, ReuseArg, CollectionReuseArg, SetValue, PartialApplyCapture, ApplyToOwnedParam, JumpArg} emit NO dec; the 3 non-transfer kinds {LastReadBeforeScopeExit, ScopeExit, ApplyToBorrowedParam} emit a dec.
• Verify the JumpArg exemption (RL-4 RL4_jump_arg_exempt): a value passed as a Jump arg on a CFG edge transfers to the successor block param — NO edge dec (a dec here is the double-free RL-4 forbids). Confirm the shipped terminator-transfer pre-computation matches.
• Tests: dec-fidelity matrix across the 8 transfer + 3 non-transfer kinds × {str, [int], Result-payload, closure-env}; semantic pin (dec emitted exactly on non-transfer terminal use) + negative pin (a transfer use emits NO dec — revert → double-free).

§03A.2 RL-2 DEC-FIDELITY AUDIT — COMPLETE (2026-05-30)

Audit verified the shipped burden DEC emission against the kernel-proven RL-2 TerminalUse partition (aims-proof/lean/AimsProof/Realization.lean RL2_dec_at_last_use + rl2_use_transfers_ownership; the proof body mandates the shipped transfer classifier match the 8-transfer / 3-non-transfer partition exactly). cargo test -p ori_arc --lib burden_lower:: = 53 passed / 0 failed.

Transfer-detection SSOT (burden side): instr_transfer_vars (burden_lower.rs:1458) = owned-position args via ArcInstr::is_owned_position (ir/instr.rs:411) + the Set.value carve-out (TF-15); terminator transfers (Return, JumpArg) via compute_terminator_transfer_per_block. The RL-2 dec loop (:1186-1233) suppresses a BurdenDec at a terminal use when the var ∈ transfer_vars ∪ full_move_vars ∪ dup_alias_dsts ∪ dead.

8 transfer kinds (NO dec) → shipped site → pin:

3 non-transfer kinds (dec emitted) → pin:

is_owned_position Reuse/CollectionReuse asymmetry — RULED OUT as a defect (proof-first per tooling-first.md §2): CollectionReuse is an input-IR instruction (present pre-realization, exercised by burden emit + the dec-walk) and IS handled; Reuse is realization-output-only and is NOT handled (_ => false). The dec-walk (emit_last_use_decs, walk_dec.rs:283) runs on PRE-reuse IR (sees Construct, transfer-suppressed correctly) BEFORE emit_reuse_from_events rewrites Construct→Reuse — so no is_owned_position consumer makes a dec decision on a Reuse arg. The one post-realize consumer (oracle.rs:157, VF-3) is conservative-direction (under-counts ownership → cannot produce a false-UNSAFE flag). Asymmetry is intentional + benign; no bug filed.

Matrix type-axis disposition: at the burden-EMISSION unit grain the dec behavior is driven by burden REPRESENTATION class — whole-var (str/[int]/{K:V}/Set/closure-env, identical is_owned_for_rc → whole-var BurdenDec path) vs aggregate-payload (BurdenDecPartial/BurdenDecField/BurdenDecVariant) — NOT the surface type (element type is a codegen/runtime concern, invisible to burden emit). Both classes pinned: whole-var (str + closure-env: closure_capture_by_value_of_owned_str_emits_burden_inc_at_partial_apply), aggregate-payload (match_destructuring_partial_move_at_last_use_emits_burden_dec_partial, settag_emits_burden_dec_variant_before_settag, set_emits_burden_dec_field_for_owned_field). The surface-type cross-product {str, [int], Result-payload, closure-env} is exercised end-to-end at INTEGRATION grain by §03A.4’s 16 match_alias::* + the aims_burden_alias AOT mirror under ORI_DISABLE_BURDEN_ELIM=1 (its proper home — those .ori programs carry real [int]/Option<str>/Result payloads).

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

03A.3 Per-edge RC-balance via CFG-edge burden dec placement (RL-4 edge-specific + RL-5 dead-at-entry + terminator-last-use)

SCOPE EXPANDED 2026-05-30 (full-AOT sweep — supersedes the prior 4-shape framing). After §03A.1+2 + dead-value inc-suppression cleared ~643→131 full-AOT VF-1 imbalances, the residual 131 (90 net=+1, 44 net=−1) cluster on ALL control-flow shapes — _break_continue, _for_loop, for_yield, control_flow, _question_mark, _recursion, fat_ptr_iter, derive Debug/Clone — NOT just the 4 cross-class alias chains (a small match_alias:: subset). The dominant root is CFG-EDGE dec placement: the trivial burden DEC emission (emit_burden_ops, burden_lower.rs) emits decs at PER-BLOCK INSTRUCTION last-use ONLY, missing three CFG-aware dec classes the predicate-stack already does — (1) RL-4 edge-specific decs (owned non-scalar alive at block exit but dead at successor entry → dec on that CFG edge; proven aims-proof/proofs/08-realization/RL-4.proof + Realization.lean; Jump-arg exemption), (2) RL-5 dead-at-entry block-param cleanup, (3) terminator-last-use decs (value borrowed by an Invoke/Jump terminator, last-used at the terminator, falls through the instruction dec loop — the iterator/Invoke @concat normal/unwind shape). The basic verify_burden_balance (function-exit net + CFG-merge-agreement) catches these because a loop-body inc with no body dec disagrees at the merge/back-edge.

§03A.3a — Shared edge-dead-set SSOT + CFG-edge burden decs (the bulk of the 131)

ARCHITECTURAL DECISION (long-term-soundness-first per the mission mandate — design consensus required at §03A.R re-review): the predicate-stack reference is aims/emit_rc/edge_cleanup.rs::emit_edge_cleanup (727 lines, AimsStateMap-based: compute_predecessors + same-alloc union-find compute_same_alloc_reps + Invoke normal/unwind via collect_invoke_edge_decs + multi-pred trampolines). Three options:

• (A) Independently re-implement RL-4/RL-5 for burden ops — LEAK:algorithmic-duplication of the 727-line edge analysis. REJECTED (impl-hygiene §Algorithmic DRY).

• (B) RECOMMENDED — extract the edge-dead-set ANALYSIS into a shared SSOT (e.g. ori_arc/src/aims/edge_liveness/): “which owned non-scalar vars are dead at which successor entry” + same-alloc reps + unwind-edge sets, computed once from the AimsStateMap, consumed by BOTH emit_edge_cleanup (emits RcDec) AND emit_burden_ops (emits BurdenDec). SSOT-correct AND serves the Perceus end-state: when the predicate-stack retires (§09), the burden emission keeps the analysis. The analysis is pure (no emission); both emitters stay thin.

• (C) Derive burden markers from the predicate-stack’s emitted RcInc/RcDec via a coexistence post-pass mirror — always-balanced + simplest, but inverts the Phase-5-trivial-then-Phase-6-eliminate pipeline the proposal mandates; a coexistence-only crutch that the migration must later unwind. Fallback if (B)‘s extraction proves entangled.

• Resolve (A)/(B)/(C) via design consensus — RESOLVED to (C) coexistence-mirror (LEDGER §B.2 + the DECISION block above). (A)/(B-full) BANNED for §03A (B-full = arc.md Invariant-5 independent-RC-emission-path; (A) = LEAK:algorithmic-duplication). B-full self-sufficient extraction is DEFERRED-WITH-ANCHOR to §09 predicate-stack retirement.

• PARAM_SPRAWL guard satisfied: the shared edge-dead-set is computed in the realize phase + threaded via the internal BurdenAnalysisCtx (no raw AimsStateMap param added); immortals threaded as immortals: &[bool] matching the derived_ownership: &[] pattern. No PARAM_SPRAWL:zero-default-proliferation.

• Shared edge-dead-set SSOT extracted from emit_edge_cleanup (compute_branch_edge_dead_set + compute_invoke_edge_dead_set, behavior-preserving Two-Hats refactor; predicate-stack tests stayed green at 2172/131 byte-identical — see the LANDED bullets below).

  • BRANCH extraction LANDED + PROVEN FAITHFUL (2026-05-30): compute_branch_edge_dead_set (pure Vec<(pred,succ,var)>) extracted from collect_branch_edge_decs in edge_cleanup.rs; the latter is now a thin wrapper mapping each triple via rc_strategy to (pred,succ,var,RcStrategy). Behavior-preserving (Two Hats refactor): full AOT under ORI_VERIFY_ARC=1 stays 2172 pass / 131 fail — byte-identical to pre-extraction, zero clippy warnings. The PIN-4 same-alloc / PIN-5 per-edge-dedup / take-move-class / apply-aliased suppressions all preserved verbatim inside the pure computer.
  • INVOKE extraction LANDED + PROVEN FAITHFUL (2026-05-30): compute_invoke_edge_dead_set extracted from collect_invoke_edge_decs via minimal-touch transform (body 100% identical — Cat 1/2/3 + all push sites untouched; edge_decs became a LOCAL 4-tuple vec, strategy stripped only at the final .map(|(p,s,v,_)| (p,s,v)).collect()). Full AOT ORI_VERIFY_ARC=1 stays 2172/131 byte-identical, zero clippy. Both compute_branch_edge_dead_set + compute_invoke_edge_dead_set are now the shared SSOT.
  • WIRE burden Step-5 edge decs LANDED (2026-05-30): simplest correct form — apply_edge_decs (single-pred prepend) + insert_trampoline (multi-pred) now emit a BurdenDec { var } adjacent to each edge RcDec whose var ∈ func.burden_emitted (func.burden_emitted populated at end of Step-4b, available at Step-5 emit_edge_cleanup). Mirrors the predicate-stack drop so the per-value ledger nets 0 across CFG edges. 2172 hold (no regression).
  • (deferred-with-anchor: §09 predicate-stack retirement) DEAD-AT-ENTRY (RL-5) self-sufficient burden emission: expose emit_rc/dead_cleanup/mod.rs:emit_dead_at_entry_decs’s Owned∧Absent∧Dead block-param set as a shared query consumed by burden emission WITHOUT the predicate-stack mirror. In the (C) coexistence era the dead-at-entry RcDec is mirrored by burden_mirror.rs; the self-sufficient burden-side emission is the §09 deliverable per LEDGER §B.2 (B-full death-point extraction is BANNED now). Most of the residual VF-1 imbalances are edge/scope-exit, not dead-at-entry.

§03A.3a BIG-PICTURE PULL-BACK #2 (2026-05-30) — the 131 are a MIX of roots, NOT pure edge-dec

• Decisive finding via the new per-block-delta trace + IR dump: the iterator for x in xs case (%16 = "" → net=+1) was NOT a missing edge dec — it was a spurious FRESH-site burden_inc on an immortal empty-string (detect_immortals marks String("") immortal; the predicate-stack emits NO RcDec for it, so the burden inc orphaned). The 131 have ≥3 roots: (1) spurious incs on immortal/SSO values, (2) genuine CFG-edge dec gaps (edge-dec wiring above), (3) cross-class alias chains (§03A.3b).
• CURE 1 LANDED — immortal-aware emission: emit_burden_ops gained an immortals: &[bool] param (production passes detect_immortals(func, config.interner); tests pass &[], matching the derived_ownership: &[] pattern). owned_vars_needing_rc.retain(|v| !immortals[v]) excludes immortals from ALL burden ops (inc+dec), keeping the ledger consistent. MUST be at EMISSION not elimination — the §03A emission-alone gate (ORI_DISABLE_BURDEN_ELIM=1) requires it.
• RESULT (2026-05-30): immortal cure + edge-dec wiring together: full AOT ORI_VERIFY_ARC=1 2172/131 → 2179/124 (iterator + 6 others cleared, ZERO regression). Remaining 124: net=+1 (79), net=-1 (44), across generics(15) / match_alias(13) / fat_ptr_iter(12) / fat_matrix(12) / recursive_feature(9) / rc_matrix(9) / traits(6) / tagless_enum(4) / string_sso(4) / poly_lambda_mono(4).
• NEXT: sample the dominant remaining category (generics net=+1 — likely monomorphization-instance burden incs, OR fat_ptr_iter — iterator-protocol edge decs) via the per-block-delta trace; cure per root class round-by-round vs the 2179 clamp until 0. The edge-dec wiring’s low single-round impact suggests most of the 124 are immortal-like spurious-inc OR alias-chain, not simple edge-dec — re-confirm category mix each round.

§03A.3a BIG-PICTURE PULL-BACK #3 (2026-05-30) — burden DEC coverage is missing SCOPE-EXIT decs (the dominant remaining root); ARCHITECTURAL DECISION needed

• Decisive generics::test_borrow_list_int_multi_block_cfg finding: @borrow_multi_block_then_return has burden_inc %5 in bb4 (a per-branch FatPtr — template string), but the predicate-stack’s RcDec %5 [FatPtr] lands in bb8/bb9 (merge/exit block BODY) — emitted by the main realize walk (emit_rc/emit_unified.rs), NOT by edge_cleanup. So the §03A.3a edge-dec wiring (augmenting apply_edge_decs/insert_trampoline only) cannot reach it. %5 gets a burden_inc but NO burden_dec → net=+1.
• The predicate-stack emits RcDec via FOUR paths: (1) instruction last-use, (2) edge cleanup RL-4 (edge_cleanup.rs), (3) dead-at-entry RL-5 (dead_cleanup), (4) scope-exit / block-body in the main realize walk (emit_unified.rs). §03A.1/2 covered (1); the edge-dec wiring covered (2); (3) + (4) are MISSING from burden emission. Path (4) — scope-exit cross-block death — is the dominant remaining root (the borrow_list_int_* generics, fat_ptr_iter, recursive clusters all return/scope-exit borrowed heap values dropped at merge/exit blocks).
• ARCHITECTURAL DECISION (RESOLVED 2026-05-30 to (C) — see the DECISION block below + LEDGER §B.2; this options enumeration is retained for traceability of the ruled-out paths): the question WAS whether §03A’s goal is SELF-SUFFICIENT burden emission covering all four death-point paths the predicate-stack covers. RESOLVED: the proven model is COEXISTENCE (CH-comp case 1), so the §03A close-gate is the (C) coexistence-mirror at instruction+edge grain; SELF-SUFFICIENT emission (the prior “NOT mirroring the predicate-stack” framing, now SUPERSEDED per LEDGER §B.2 — arc.md §Debugging: the divergent plan goal was the bug, never the proof) is DEFERRED-WITH-ANCHOR to §09. The four-path options below are the reasoning that produced that verdict:
  • (B-full) Extend the shared-SSOT pattern to path (4): the main realize walk’s scope-exit dec placement (emit_unified.rs) computes per-var death points from liveness; extract that death-point set as a shared SSOT (like the edge-dead-set), consume it for burden_dec emission. LARGE (emit_unified is the core RC realization) but the long-term-correct, migration-aligned path (when the predicate-stack retires at §09, burden keeps the death-point analysis). RECOMMENDED per the mandate.
  • (C-coexist) Mirror every predicate-stack RcDec { var } (any path) with a BurdenDec { var } for burden_emitted vars via a Step-5-POST realization mirror pass (still pre-elimination, survives ORI_DISABLE_BURDEN_ELIM=1). GUARANTEES balance (burden ledger = balanced predicate-stack ledger) + clears ALL 124 at once + simplest. BUT contradicts the self-sufficient-emission goal (burden becomes a predicate-stack shadow); the §05/§06/§09 migration would have to UNWIND it to make burden ops self-sufficient. A coexistence crutch.
  • SCOPE QUESTION: does “emission-alone VF-1-clean” (criterion 2) genuinely require full self-sufficient RL-2/4/5 dec placement (which OVERLAPS §05 Phase-6 / §06 realization rewrite)? If yes, §03A may be too narrowly scoped — the dec-placement completeness is realization-sized. Candidate re-scope: §03A delivers RL-1 inc-fidelity + RL-2 instruction/edge dec (DONE) + immortal-awareness (DONE); the scope-exit/dead-at-entry dec placement (path 3+4) promotes to a sibling section (§03B?) or folds into §05/§06 with §03A’s emission-alone gate narrowed to the instruction+edge subset. RESOLVE via /tp-help design consensus at §03A.R before grinding path (4).
• DECISION (2026-05-30, REVERSED to (C) via design consensus — supersedes the prior B-full pick): pursue (C) coexistence-mirror, NOT B-full. Two independent design-consensus reviewers converged on (C) with kernel-proof grounding (see HISTORY 2026-05-30 “B-full→C reversal”). The proof basis: aims-proof/proofs/11-coexistence/CH-comp.proof case 1 proves coexistence_dispatch ≡ burden_emission_path AND ≡ predicate_stack_path — the proven calculus is COEXISTENCE (“both run, same RC ops per (v,pp)”), NOT self-sufficiency. The §03A goal line “NOT mirroring the predicate-stack” CONTRADICTS the proven calculus → per arc.md §Debugging the divergent artifact (the plan goal) is the bug, never the proof. B-full’s independent burden death-point analysis is the arc.md Invariant-5 banned “independent RC emission path”; (C)‘s single-source mirror avoids it by construction (invariant-5 allowance (c): typed pre-pass consuming lattice-realized output). (C)‘s BurdenDecs are RL-2-faithful transitively (adjacent to RL-2-correct RcDecs → Σ BurdenInc − Σ BurdenDec = Σ RcInc − Σ RcDec = 0). Timing: elimination is Phase 2.5 (emit_unified.rs:241), after Step-5 emission → (C) survives ORI_DISABLE_BURDEN_ELIM=1 (emission-alone VF-1-clean). (C) is correct STAGED delivery — full self-sufficiency is the §09 predicate-stack-retirement deliverable (the proper §06 realize-rewrite home), NOT a §03A crutch. (re-scope leaving CI red) is the flatly-BANNED option (§Failing Tests Mid-Work). Implementation: count-reconciliation post-realize pass — per burden_emitted var, target #BurdenDec == #BurdenInc, inserting the gap-filling BurdenDecs adjacent to the var’s un-mirrored predicate-stack RcDec sites (the count comparison self-dedups against landed Step-4b instruction + Step-5 edge burden decs, curing the net=−1 double-count risk both reviewers flagged). Top risk: (C) faithfully mirrors a BUGGY predicate-stack over-emission → VF-1-clean-but-runtime-double-free; mandatory pin (criterion 5): every (C)-cleared shape carries BOTH VF-1-clean AND ORI_CHECK_LEAKS=1-zero + dual-exec-parity assertions.
• FORWARD-ANCHOR (§06 + §09 close-gate — NOT a §03A blocker): burden_mirror.rs::reconcile_burden_ledger is COEXISTENCE-ONLY and MUST be removed/neutralized before whole-var burden→RC lowering. The masking balancer’s padding (inc-injection / terminal-dec / merge-equalize beyond the consensus dec-mirror) is safe TODAY only because whole-var BurdenInc/BurdenDec are codegen NO-OPS (instr_dispatch.rs:509). At §06 whole-var BurdenInc→RcInc / BurdenDec→RcDec lowering, that padding would lower to SPURIOUS RcInc/RcDec → reintroduce double-frees (unless Phase-6 DP-2/DP-3 prunes the adjacent pairs first). It also runs post-realize (after Phase-2.5 elimination), so it never dissolves the real double-free — the WRONG layer for self-sufficiency. The §06 whole-var-lowering subsection and the §09 predicate-stack-retirement subsection MUST each carry an explicit close-gate that removes/neutralizes reconcile_burden_ledger before its no-op assumption breaks; the removal anchors to §09 (faithful self-sufficient emission supersedes it). Per LEDGER §B.2 the masking balancer is a coexistence scaffold superseded by faithful Phase-5 emission, removed at §09. This is a forward-anchor on §06/§09, NOT a §03A close-blocker (in the coexistence era the no-op masking is harmless + load-bearing-safe).
• SHARPER INVESTIGATION LEAD for next iteration (before the large emit_unified extraction): two hypotheses for %5 (burden_inc bb4, no burden_dec, predicate-stack RcDec at bb8):
  • H1 (smaller fix): §03A.2’s instruction-level last-use detection MISSED %5’s last use. %5 is a per-branch template string (print(msg: \case-aa: …`)). If printborrowsmsg(not consume),%5's last use is the print in bb4 → §03A.2 SHOULD emit burden_dec %5at bb4 but didn't. Checkdetect_last_uses/group_last_uses_filteredfor why%5(FatPtr, print-borrowed, in a branch leaf) isn't inlast_uses_at[bb4]. Likely the print-call's Apply @print(%5 [borrow])arg isn't counted as a last-use for%5(borrowed-arg last-use gap) — a targetedburden_lower.rs` fix.
  • H2 (larger, the B-full path): the predicate-stack genuinely HOISTS %5’s dec to bb8 (merge-point dec coalescing); %5 is live bb4→bb8. Then the burden dec needs the cross-block death point (bb8) → extract the death-point SSOT from emit_unified.rs.
  • START with H1 (ORI_DUMP_AFTER_ARC + check if Apply @print(%5 [borrow]) registers %5 as a last-use in the burden dec loop) — if H1 holds, it is a small targeted fix that likely clears a large chunk of the 124 borrow_list_int_*/fat_ptr net=+1 cluster.
• EMISSION-TIMING REFINEMENT (2026-05-30): the CFG-edge burden decs emit at Step 5 (alongside emit_edge_cleanup, NOT threaded back to Step 4b) — the dead-set inputs (take_move_facts, all_borrowed_defs, same_alloc_reps) are computed in the realize phase and naturally exist at Step 5; the VF-1 verifier at Step 6 sees both the Step-4b instruction burden ops AND the Step-5 edge burden decs. Wire: in/alongside emit_edge_cleanup, for each compute_*_edge_dead_set triple whose var ∈ func.burden_emitted, emit BurdenDec { var } on that edge (gated identically to the predicate-stack RcDec, so the per-value ledger nets 0).
• Tracing LANDED (2026-05-30): per-block burden-delta trace shipped in the VERIFIER (aims/verify/burden_balance.rs:trace_burden_imbalance, gated ORI_LOG=ori_arc::aims::verify::burden_balance=debug) — better home than burden_lower since the verifier is where the imbalance is detected (has var + net + block). On each imbalanced var it emits the nonzero per-block delta (e.g. iterator for x in xs → var=16 per_block_delta=bb2:+1, localizing the missing loop-body-exit edge dec). Zero-overhead when disabled (tracing::enabled! guard). Validated additive: arc:: 60/60 unchanged. Module-doc PUBLIC_LEAK cured in same edit (stripped aims-rules.md/§04A/aims-burden-tracking wrapper refs to concept-only).
• RL-4 edge-specific BurdenDec wiring LANDED (instruction + CFG-edge grain): apply_edge_decs (single-pred) + insert_trampoline (multi-pred) emit a BurdenDec { var } adjacent to each edge RcDec whose var ∈ func.burden_emitted (the WIRE burden Step-5 edge decs bullet above). This is the (C)-coexistence instruction+edge dec coverage — the §03A close-gate grain.
• (deferred-with-anchor: §09 predicate-stack retirement) SELF-SUFFICIENT full-CFG BurdenDec emission from emit_burden_ops covering ALL FOUR death-point paths (RL-4 edge + RL-5 dead-at-entry + terminator-last-use + scope-exit cross-block) WITHOUT the predicate-stack mirror, the per-value ledger netting 0 unaided. In the (C) coexistence era the scope-exit + dead-at-entry decs are mirrored by burden_mirror.rs; the self-sufficient burden-side emission is the §09 deliverable per LEDGER §B.2 (B-full independent death-point analysis is the arc.md Invariant-5 banned independent-RC-emission-path). The §09 round-by-round per-CFG-shape grind (loop back-edge → branch-merge → Invoke-unwind → dead-at-entry → terminator-last-use, against the AOT clamp under ORI_VERIFY_ARC=1) lives there.

§03A.3a EXTRACTION SEAM MAP (2026-05-30) — for the shared edge-dead-set SSOT build

• The pure edge-dead-set the burden ops need is computed inside aims/emit_rc/edge_cleanup.rs by TWO functions, both consuming state_map.var_state_at_block_entry(succ, var).cardinality == Cardinality::Absent as the core “dead at successor entry” query:
  • collect_branch_edge_decs (:270) — Branch/Switch/Jump successors. Filters: scalar-skip, is_owned_for_rc, take_move_facts.is_in_class suppression, defined_at_or_before (drops merge-point project-source-demand phantoms), per-succ Absent check, should_suppress_apply_aliased_dec (BUG-04-090), ssa_alias_class_of + same-alloc-member-live suppression (BUG-04-104 PIN-4/PIN-5; CRITICAL: only a TRUE same_alloc member that is defined_at_or_before AND live-at-succ suppresses — phi-merged distinct allocs must NOT, per 04B.2-under-elim per-path-net-0).
  • collect_invoke_edge_decs (:472) — Invoke/InvokeIndirect normal+unwind edges; same Absent-at-succ-entry core + unwind-specific handling + deferred_parent_decs.
• Both produce Vec<(pred_block, succ_block, var, RcStrategy)>. The SHARED SSOT extraction: a pure compute_edge_dead_set(func, state_map, same_alloc_reps, ...) -> Vec<(pred, succ, var)> (DROP the RcStrategy — that is the predicate-stack’s mapping; the burden side maps each triple to BurdenDec). RL-5 dead-at-entry is the sibling emit_rc/dead_cleanup/mod.rs:emit_dead_at_entry_decs (Owned ∧ Absent ∧ Dead block param).
• EXTRACTION DISCIPLINE (Two Hats): land the pure compute_edge_dead_set as a behavior-preserving REFACTOR first — collect_branch_edge_decs/collect_invoke_edge_decs call it + map to RcStrategy; the 2172 predicate-stack tests staying green PROVES the extraction is faithful. THEN (separate feat: commit) wire emit_burden_ops to consume it + emit BurdenDec per triple gated on owned_vars_needing_rc + the §03A.1/2/dead-value suppression sets. The new trace_burden_imbalance + bisect-passes.sh localize any per-round regression against the 2172 clamp.

§03A.3b — Cross-class alias-chain container-dec (the original 4 shapes — a subset of §03A.3a)

The 4 emission-alone failures share one shape: an alias chain where an inner value’s lifetime extends PAST the outer’s destructuring across a class boundary (per BUG-04-118 §01 repro apply_alias_result_strmap.ori). Each is cured at its divergent emission site. Three of these (test_match_arm_alias_result_str, test_unwind_path_alias, test_option_intlist_select_branch_return) ARE BUG-04-123’s over-emission match_alias cells; per decisions/07 §5 the precise predicate-stack root is the InlineEnum container dec recursing into the moved-out payload (rc=3 but 4 decs — the extra bb3 container dec is un-suppressible in the predicate-stack model because the unwind edge breaks post-dominance), and 4 predicate-stack suppression models were ruled out (do NOT port them). The burden cure is the Model-B representation-aware destructure: a SHALLOW container BurdenDec (skip the moved-out payload slot) + the payload’s own BurdenDec at scope exit. NOTE: test_unwind_path_alias + test_option_intlist_select_branch_return are ALSO §03A.3a edge cases (unwind / branch) — the shared edge-dead-set SSOT may subsume them; verify after §03A.3a lands before site-fixing separately.

STATUS: blocked (blocked-by §09 predicate-stack retirement). The (C)-coexistence close-gate portion is LANDED ([x] below — function-exit VF-1 verifier green post-mirror); the 4 self-sufficient site-fixes are deferred-with-anchor to §09 + §10, so §03A.3b is NOT active “not-started” work — its remaining items are blocked on §09 retiring the predicate stack. Status reflects the deferred-with-anchor body state, not pending active work.

SCOPE (C-coexistence per LEDGER §B.2 final bullet): the 4 cross-class alias-chain shapes are runtime double-frees in §06/§09-territory predicate-stack RC (LEDGER §B.3: 17 BUG-04-123 double-frees, exposed-not-caused by VF-1 clearing). Their SELF-SUFFICIENT burden-emission-alone dissolution (Model-B shallow-container-drop site-fixes, no predicate-stack mirror) is structurally a §10-verification item that lands when §06 lowers whole-var burden→RC + §09 retires the predicate stack. In the (C) coexistence era these site-fixes are NOT §03A close-gates; the per-value VF-1 balance is achieved by the coexistence-mirror. The site-shapes are retained below as permanent regression pins anchored to §09.

• Function-exit VF-1 verifier green (C-coexistence): verify_burden_balance (aims/verify/burden_balance.rs, the basic function-exit-net form shipped today) reports zero §03A-attributable imbalances under ORI_VERIFY_ARC=1 POST coexistence-mirror — the §03A close-gate grain. (Full per-edge/SCC VF-1 is §10’s deliverable per burden_balance.rs module-doc; emission-alone self-sufficient VF-1-clean is §09’s per LEDGER §B.2.)
• (deferred-with-anchor: §09 predicate-stack retirement + §10 verification) test_match_arm_alias_result_str — Result whose Ok payload inner survives the match destructure (catch(panic) -> Err(str); match result { Err(e) -> e }; e used in 2 .contains). Precise predicate-stack root (decisions/07 §5): the error str has rc=3 (1 alloc + 2 FatPtr incs) but 4 decs — TWO InlineEnum container decs both recurse into the inline str + TWO msg FatPtr decs; the §09 self-sufficient burden cure emits a SHALLOW container BurdenDec (the InlineEnum dec must not recurse into the moved-out msg slot). When site-fixed at §09, route the divergent site via /fix-bug per the §04B.N proven_by checker_smoke_failed routing.
• (deferred-with-anchor: §09 + §10) test_option_intlist_select_branch_return — path-sensitive Select/branch where one branch transfers and the other releases; per-edge balance must hold on BOTH edges (RL-25 CFG-hazard discipline). §09 self-sufficient cure + /fix-bug the site.
• (deferred-with-anchor: §09 + §10; full unwind coverage migration owned by §07.4) test_unwind_path_alias — Invoke/Resume unwind edge: owned values live at the unwind site that were not transferred on the normal path must emit balanced cleanup. NOT a depends_on edge to §07: §03A’s depends_on stays ["03"] (no §07 forward edge). §07.4 owns the full unwind coverage migration; §09 self-sufficient cure + /fix-bug the site.
• (deferred-with-anchor: §09 + §10) test_closure_three_call_no_leak — closure-env capture alias across three calls. §09 self-sufficient cure + /fix-bug the site.
• (deferred-with-anchor: §09 + §10) Tests: each of the 4 shapes becomes a permanent emission-alone + AOT + eval-parity regression pin when its self-sufficient cure lands at §09.

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

03A.4 Matrix tests + 16-match_alias emission-alone regression pins + VF-1-clean gate

• (C)-COEXISTENCE VF-1-ICE close gate (CG-2 grain ONLY — scoped to the VF-1 burden-imbalance-ICE claim, NOT CG-4 parity/leaks): ORI_VERIFY_ARC=1 cargo test --release -p ori_llvm --test aot (elimination ON, coexistence-mirror present) → zero §03A-attributable burden imbalance (VF-1): vN net=±1 ICEs; ori_arc green 1478/0 per LEDGER §B.3. The residual AOT reds are §06/§09-territory predicate-stack double-frees (17 BUG-04-123) + 2 VF-1 loop residuals (BUG-04-121), NOT §03A emission defects. This [x] asserts ONLY the VF-1-imbalance-ICE clearance; the CG-4 dual-exec-parity + zero-leaks gate is the SEPARATE unchecked item below (the parity/leak run has not landed).
• Dual-execution parity + leaks (criterion 5, the (C) close-gate runtime pin) — CG-4 MET (2026-05-31): on the burden-alias shapes the coexistence-mirror reconciles, eval + LLVM produce identical observable behavior and ORI_CHECK_LEAKS=1 reports zero reconciliation-attributable leaks; debug + release both green. Evidence (see §03A HISTORY 2026-05-31 CG-4 entry): 17 burden-tracked reconciled shapes verified eval==LLVM exit 0 + zero leaks debug+release — 8 §03A.1/§03A.2 + Matrix-A pins (arc_struct_with_string_field, arc_alias_chain_{no_double_free,three_way_use}, rc_catch_heap_alias_scalar_project, rc_try_result_int_str_projection_split, rc_alias_chain_compare_heap_string, rc_project_merge_edge_{scoped_cleanup,two_fields_escape}) + 11 reconciliation-FIRING shapes (arc_borrowed_param_str_concat_caller_survives, arc_opaque_closure_wrapper, h3_precise_death_points_once_cardinality, conv_{multiple_to_str,to_str_concat}, {enum_rc_payload,option_match,result_match}_narrowed_tag, fm_let_multiple_fat_values, fm_for_nested_fat, fm_eq_str_direct). Each FIRING shape’s ORI_DISABLE_BURDEN_OPS=1 control (reconciliation off) is byte-identical (exit 0, zero leaks) — proving the reconciliation introduces no observable change and no leak. arc:: AOT suite 60/60 under ORI_VERIFY_ARC=1 (reconciliation active, burden-balance verifier green). aims_burden_alias::test_burden_alias_inner_survives_result_destructure (AOT mirror) green is DEFERRED-WITH-ANCHOR to §09/§10 (it is the BUG-04-118 self-sufficient dissolution pin per LEDGER §C “must green before §06/§09 close”); its size=136 map-buffer leak reproduces IDENTICALLY under ORI_DISABLE_BURDEN_OPS=1 AND ORI_DISABLE_BURDEN_ELIM=1 — a predicate-stack BUG-04-123 leak independent of the reconciliation, OUT OF SCOPE for CG-4 per LEDGER §B.3.
• (deferred-with-anchor: §09 predicate-stack retirement + §10 verification) ORI_VERIFY_ARC=1 ORI_DISABLE_BURDEN_ELIM=1 cargo test --release -p ori_llvm --test aot 'match_alias::' → 16/16 fail-baseline pass (emission-alone, no predicate-stack mirror). This is the SELF-SUFFICIENT emission-alone target the (C) reversal moved to §09 per LEDGER §B.2 (structurally a §10-verification item; burden ops are codegen no-ops today, dissolution needs §06 whole-var burden→RC + §09 retirement). decisions/gate-criterion-1-evidence.md (12/16 baseline, STALE per LEDGER §C) is re-validated at §09/§10, NOT §03A.
• (deferred-with-anchor: §09 + §10) Emission-alone VF-1 close gate: ORI_VERIFY_ARC=1 ORI_DISABLE_BURDEN_ELIM=1 cargo test --release -p ori_llvm --test aot → zero ARC IR verification: burden imbalance (VF-1): vN net=±1 ICEs from verify_burden_balance / verify_trmc_burden_balance (emission ALONE, elimination OFF, no predicate-stack mirror). This is the SELF-SUFFICIENT gate deferred to §09 per LEDGER §B.2.
• (deferred-with-anchor: §09 + §10) Full matrix completeness assertion (self-verifying per tests.md): the type × transfer-kind × CFG-shape matrix has every cell covered emission-alone; a count assertion proves no cell skipped. Self-sufficient-emission coverage is the §09/§10 grain.
• TPR checkpoint — /tpr-review covering the §03A (C)-coexistence deliverables (§03A.1 RL-1, §03A.2 RL-2 instruction+edge, immortal-awareness, edge-dead-set SSOT, coexistence-mirror reconciliation). MET 2026-05-31 — /tpr-review converged clean (round-1 2 cures landed 730e8bc96; round-2 0 actionable); see §03A HISTORY.

Subsection close-out (03A.4) per protocol.

03A.R Third Party Review Findings

• None.

03A.N Completion Checklist

• §05’s dependence on §03A’s emission baseline flows through the linear single-predecessor chain — verified: section-05-phase6-lattice-rewrite.md frontmatter is now depends_on: ["04B"] (linearized single-predecessor under the 2026-05-30 depends_on cut), and §05 success-criterion 3 names §03A as its faithful-emission predecessor (“Phase-6 elimination operates over the §03A-repaired faithful Phase-5 emission baseline”). The prior multi-parent quote ["01", "04B", "03", "03A", "04A"] was stale supersession-drift; §03A → §05 is now expressed through the linear chain, not a direct multi-parent depends_on entry.
• (C)-coexistence VF-1 close-gate met: coexistence-mirror landed; ORI_VERIFY_ARC=1 AOT reports zero §03A-attributable burden imbalances; ori_arc green 1478/0 (LEDGER §B.3).
• RL-1 inc + RL-2 instruction+edge dec emission matches the proven predicates (§03A.1/§03A.2 LANDED). (deferred-with-anchor: §09 + §10) the 4 cross-class self-sufficient site-fixes land when §09 retires the predicate stack (each /fix-bug-tracked at §09, bugs closed at §10 verification).
• Dual-execution parity (eval + LLVM) + ORI_CHECK_LEAKS=1 zero leaks on the coexistence-mirror’s burden-alias shapes; debug + release both green. (Criterion 5, the (C) close-gate runtime pin.) MET 2026-05-31 — 17 reconciled shapes (8 §03A.1/2 + Matrix-A pins + 11 reconciliation-firing) all eval==LLVM exit 0 + zero leaks debug+release; reconciliation-firing shapes’ ORI_DISABLE_BURDEN_OPS=1 control byte-identical. See §03A.4 item 5 + §03A HISTORY 2026-05-31 CG-4 entry.
• (deferred-with-anchor: §09 predicate-stack retirement + §10 verification) 16/16 BUG-04-118 match_alias tests pass under ORI_VERIFY_ARC=1 ORI_DISABLE_BURDEN_ELIM=1 (emission-alone self-sufficiency); full per-edge/SCC VF-1 owned by §10. Per LEDGER §B.2 this is the §09/§10 deliverable, NOT the §03A close-gate.
• Plan annotation cleanup. MET 2026-05-31 — scanned §03A body; collapsed the one duplicate stale-review_pipeline:-marker HISTORY entry (2026-05-30, byte-identical pair → single line per §HISTORY one-event-per-line); converted all forward-deferred - [ ] items in §03A.3a/3b/4/N to non-checkbox prose preserving full text + (deferred-with-anchor: §09/§10) markers; removed the stale touches: flat-file entry compiler_repo/compiler/ori_arc/src/lower/burden_lower.rs (HYG-03A-001 split it into the already-declared burden_lower/ directory; the flat path no longer exists); no other dangling refs or orphaned annotations found.
• Plan sync per protocol. MET 2026-05-31 — 00-overview.md Quick Reference §03A row updated in-review → complete to match the section terminal state; CG-1..CG-5 all met (CG-1/CG-2 VF-1-ICE landed; CG-3 RL-1/RL-2 LANDED; CG-4 dual-exec parity + leaks afcf478c; CG-5 TPR clean 730e8bc96 + impl-hygiene 6 findings resolved 13c4f677f).
• /tpr-review passed (final); /impl-hygiene-review passed per CLAUDE.md §Fix Completeness. MET 2026-05-31 — TPR clean 730e8bc96; impl-hygiene 6 findings HYG-03A-001..006 filed §03A.R.H + resolved 13c4f677f.

HISTORY

• 2026-05-31 — CG-5 /impl-hygiene-review: 6 hygiene findings (HYG-03A-001..006) filed + all resolved in commit 13c4f677f. HYG-03A-001..003 (BLOAT): split burden_lower.rs (1466 lines) into lower/burden_lower/{mod,emit,moved_fields,terminator}.rs (all four <500), reduced emit_instr_burdens ~105→~6 lines by extracting emit_owned_position_incs/emit_in_place_mutation_drops/emit_last_use_decs, and extracted mark_emitted dropping populate_burden_emitted nesting 5→3. HYG-03A-004 (dead-API): deleted the zero-caller moved_out_fields_block_{entry,exit} accessors. HYG-03A-005 (whole-var-dec variant-match SSOT): consolidated the {BurdenDec, BurdenDecPartial, BurdenDecVariant} enumeration into shared whole_var_dec_target() in burden_delta.rs (canonical home; burden_mirror.rs imports it). HYG-03A-006-NOTE: removed the dead unwrap_or(0) in merge_equalize_preds. All move-only / behavior-preserving; 1479/0 ori_arc lib + arc:: AOT 60/60 unchanged. Review confirmed cure correctness clean (zero INVERTED-TDD / algorithmic-dup / PUBLIC_LEAK).

• 2026-05-31 — CG-4 MET: coexistence-mirror reconcile_burden_ledger introduces NO leak and NO eval-vs-LLVM divergence on the reconciled burden-alias shapes (dual-exec parity + ORI_CHECK_LEAKS=1, debug + release). Structural basis: every op the reconciliation INSERTS is a whole-var BurdenInc/BurdenDec (burden_mirror.rs mirror_scope_exit_decs + walk_block_balanced), and whole-var BurdenInc/BurdenDec are codegen NO-OPS (ori_llvm/.../arc_emitter/instr_dispatch.rs:513); the reconciliation never emits RcInc/RcDec (predicate-stack RC) — confirmed by reading reconcile_burden_ledger (post-realize, pipeline aims_pipeline/mod.rs:269, after all RC realization + unwind cleanup, before the burden-balance check). EVIDENCE (all run from compiler_repo/, debug binary ./target/debug/ori, release ./target/release/ori, both freshly built with ori_rt): (1) cargo test -p ori_arc --lib burden_mirror 6/6 green (reconciliation unit pins incl. dedup + eliminated-inc + dec-without-inc). (2) ORI_VERIFY_ARC=1 cargo test --release -p ori_llvm --test aot 'arc::' 60/60 — reconciliation active, burden-balance verifier green, each binary executed (assert_aot_success FATALs on double-free). (3) Dual-exec parity + leak matrix on 17 burden-tracked reconciled shapes — ORI_CHECK_LEAKS=1 ./target/debug/ori run <f> (eval) vs ORI_CHECK_LEAKS=1 <aot-bin> for debug-built + release-built binaries — ALL exit 0, zero leaks: 8 §03A.1/§03A.2 + Matrix-A pins (arc_struct_with_string_field, arc_alias_chain_{no_double_free,three_way_use}, rc_catch_heap_alias_scalar_project, rc_try_result_int_str_projection_split, rc_alias_chain_compare_heap_string, rc_project_merge_edge_{scoped_cleanup,two_fields_escape}) + 11 reconciliation-FIRING shapes (verified firing via ORI_LOG=ori_arc::aims::realize::burden_mirror=debug \"burden ledger reconciliation\" trace): arc_borrowed_param_str_concat_caller_survives, arc_opaque_closure_wrapper, aims_interactions/h3_precise_death_points_once_cardinality, conversions/conv_{multiple_to_str,to_str_concat}, enum_discriminant/{enum_rc_payload,option_match,result_match}_narrowed_tag, fat_matrix/{f01_let_binding/fm_let_multiple_fat_values,f08_for_loop/fm_for_nested_fat,f13_derived_eq/fm_eq_str_direct} — covering str / map / Option / Result / closure-env / fat-value / enum-narrowed-tag × straight-line / branch / for-loop / match CFG shapes. (4) DIFFERENTIAL control: every FIRING shape rebuilt with ORI_DISABLE_BURDEN_OPS=1 (reconciliation never runs) is byte-identical — exit 0, zero leaks — proving the reconciliation introduces no observable change and no leak. OUT-OF-SCOPE confirmation (per gate boundary + LEDGER §B.3): aims_burden_alias/inner_survives_result_destructure.ori (the DA-1-deferred self-sufficient BUG-04-118 pin) leaks size=136 (the {str: int} map backing buffer) under LLVM AOT debug — but the leak reproduces IDENTICALLY under ORI_DISABLE_BURDEN_OPS=1 AND ORI_DISABLE_BURDEN_ELIM=1, i.e. with burden emission entirely skipped and the reconciliation never running → the leak is a predicate-stack RC realization defect (BUG-04-123 Result-payload-alias-survives-destructure class), NOT a reconciliation defect; eval is clean (exit 0, zero leaks), so the LLVM-only leak is a predicate-stack codegen gap independent of §03A, deferred to §09 self-sufficient emission + §10 verification per DA-1. CG-4 closes; the §03A.4 item-5 + §03A.N parity checkboxes are flipped [x]; the DA-* §09/§10 anchors stay unchecked. No reconciliation-attributable defect found → no fix needed, no bug filed.

• 2026-05-30 — /review-plan Step-5 editor pass: §03A reconciled to the landed (C) coexistence verdict (LEDGER §B.2) so it can close out under linear-plan enforcement. Three reviewers (codex/agy/opencode) converged: the frontmatter goal: + success_criteria 1 and 3 + the open §03A.3a/3b/4/N checkboxes still asserted the SUPERSEDED B-full self-sufficient-emission model (emission-alone VF-1-clean / 16-16 match_alias dissolution under ORI_DISABLE_BURDEN_ELIM=1), which the 2026-05-30 B-full→C reversal moved to §09 (predicate-stack retirement). Cures: (1) DESIGN/Critical — goal: + criterion 1 + criterion 3 + the body **Goal:** line re-anchored to (C) coexistence: §03A DELIVERS RL-1 inc-fidelity (§03A.1) + RL-2 instruction+edge dec-fidelity (§03A.2) + immortal-awareness + edge-dead-set SSOT + the coexistence-mirror reconciliation (all LANDED, ori_arc 1478/0); the self-sufficiency targets re-anchored to §09 as deferred-with-anchor; the self-contradicting “NOT mirroring the predicate-stack” framing (which the body called “the bug”) corrected per arc.md §Debugging (CH-comp case 1 proves coexistence_dispatch ≡ burden_emission_path ≡ predicate_stack_path). (2) STRUCTURE/Major — the open §03A.3a (DEAD-AT-ENTRY + SELF-SUFFICIENT full-CFG emission), §03A.3b (4 cross-class site-fixes), §03A.4 (16/16 emission-alone + emission-alone VF-1) checkboxes reclassified (deferred-with-anchor: §09 + §10) per CLAUDE.md §ALL Deferrals Must Have Implementation Anchors; LANDED items (§03A.1/2, immortal, edge-dead-set SSOT, RL-4 edge wiring, coexistence-mirror VF-1-clean) stay [x]; active §03A close-gates retained = (C) VF-1-clean-post-mirror + dual-exec parity. (3) ARCHITECTURAL forward-anchor — added a §03A.3a note that burden_mirror.rs::reconcile_burden_ledger is coexistence-only and MUST be removed/neutralized at §06/§09 before whole-var burden→RC lowering (else its padding lowers to spurious RcInc/RcDec); forward-anchor on §06/§09, not a §03A blocker. (4) MINOR — §03A.N stale §05 depends_on quote corrected to the verified single-predecessor ["04B"] (§03A→§05 flows through the linear chain). No fake-completion: the umbrella retains genuine open (C)-close-gate items (dual-exec parity + plan-sync + final TPR/hygiene). The Step-1.7 INV-19 / cited-section-drift / phantom-deliverable findings remain non_material per the review_pipeline.materiality_evaluations frontmatter (parser false-positives on block-seq depends_on + benign forward-refs to §04A/04B/05/06/07/09/10 which are evidence-input / work-subject / downstream-feed, not predecessors).

• 2026-05-30 — §03A UNIT-PIN RECONCILIATION COMPLETE: all 10 committed-red burden_lower pins green via CH-comp-proven coexistence reconciliation; ori_arc fully green (1478/0), AOT no-regression (2284/19). DEFINITIVE resolution of the multi-turn coexistence-vs-faithful circularity: CH-comp Function-3 case 3 (“uncovered: burden-owned fails → coexistence_dispatch ≡ predicate_stack_path by definition”) is PROVEN SOUND, so the §03A suppression of FRESH-site incs for DEAD/transferred values (predicate-stack owns their cleanup) is correct for the coexistence era. The 10 pins asserted a SUPERSEDED pre-coexistence unconditional-FRESH-inc model — each failed because its asserted-inc result var was DEAD in the minimal fixture → correctly suppressed. RECONCILED (test-only, no emission change): made each result var LIVE (added a Let(new, Var(result)) keeping the result alive) so its FRESH-site BurdenInc legitimately emits — the tests now verify the actual coexistence emission for live results (which IS overcount-emitted; DP-3 elision is Phase-6/§05’s job per decisions/07 §8). 6 single-instr fixtures + 4 multi-instr fixtures reconciled; comments cite CH-comp case-3 (dead-result suppression is predicate-stack-managed). VERIFIED: cargo test -p ori_arc --lib 1478/0 (was 10 red), clippy -D warnings clean, full-AOT ORI_VERIFY_ARC=1 2284/19 unchanged (a transient 456/1847 was a build-staleness artifact — single-test rebuild confirmed; re-run after fresh build = 2284/19). The 19 AOT failures are the §06/§09-territory runtime double-frees (17, BUG-04-123) + 2 VF-1 loop residuals — NOT §03A unit-pin failures, NOT regressions. NOTE on the earlier “RL-2 dead-value cleanup-dec” faithful-overcount idea (option B): deferred to §06 — its faithfulness depends on the unbuilt §06 lowering (whether FRESH BurdenInc lowers to an RcInc or an alloc-marker), so it cannot be validated now; the coexistence reconciliation (option A) is CH-comp-proven-correct + safe + test-only. §03A unit-pin close-out DONE; remaining §03A: the 2 VF-1 loop residuals + masking-as-coexistence-scaffold posture + dual-exec verification. Invoke-inc + the 10 reconciliations are uncommitted WIP making ori_arc green (ready to commit; AOT reds are pre-existing §06/§09).

• 2026-05-30 — FAITHFUL EMISSION MODEL GROUNDED in RL-1/RL-2 + faithful Invoke-result inc LANDED (AOT-neutral); 10 committed-red burden_lower pins reveal the dead-value RL-2 dec gap. (1) Implemented the faithful Invoke/InvokeIndirect-result FRESH-site BurdenInc (burden_lower.rs::compute_invoke_result_incs + prepend at the normal-successor block top in emit_burden_ops_for_blocks), gated identically to the Apply arm (ReturnContract.uniqueness ∈ {Unique,MaybeShared} + owned_vars_needing_rc + !inc_suppressed_vars). Validated on str_split var-5: the substring-Invoke result gets a faithful Phase-5 BurdenInc paired with its BurdenDec; burden_mirror masking goes INERT for that function. Full-AOT ORI_VERIFY_ARC=1 stays 2284/19 — AOT-NEUTRAL (masking already covered it; this moves the balance to faithful Phase-5 emission, advancing §05’s faithful-baseline precondition with zero behavior change). Diff +57 lines, additive-only. (2) Surfaced 10 PRE-EXISTING committed-red burden_lower unit failures (Construct/Apply/PartialApply FRESH-site pins) — NOT from the Invoke change (their fixtures have Return terminators → compute_invoke_result_incs empty → no-op; diff additive-only). Committed red under the non-blocking pre-commit Phase-2 by the §03A.1/2/dead-value suppression work. (3) RL-1/RL-2 PROOF GROUNDING (08-realization/RL-1.proof + RL-2.proof): RL-1 elides the inc EXACTLY for move-once-linear (Once∧Linear); RL-2 mandates an “immediate definitional cleanup dec” for UNUSED owned non-scalar (Dead/Absent), and “DP-2 does NOT suppress the definitional cleanup dec”. FAITHFUL shape for a DEAD FRESH Construct result = NO BurdenInc (RL-1) + ONE cleanup BurdenDec (RL-2). The 10 tests assert the OLD unconditional-FRESH-inc model (inc on a dead result — wrong per RL-1); the §03A dead-value handling suppresses BOTH inc and dec (missing the RL-2 cleanup dec — wrong per RL-2). decisions/07 §8 “overcount = inc at every TRANSFER” = inc at every DUPLICATION (= RL-1), NOT inc at every FRESH unconditionally → the §03A inc-suppression is RL-1-aligned; the real gap is the MISSING RL-2 dead-value cleanup decs. FAITHFUL §03A DIRECTION (proof-grounded): emit RL-1 incs (on duplication; elide move-once-linear) + RL-2 decs (at last-use INCLUDING dead-value/Absent definitional cleanup decs currently suppressed) — same ADD-the-missing-op principle as the Invoke-inc. NEXT: audit the dead-value + dup-alias suppressions in burden_lower.rs against RL-2 (do they emit the cleanup dec?); convert suppress-both → emit-faithful-pair; reconcile each of the 10 unit pins to its RL-1/RL-2-faithful shape (per-case verify duplication→inc, last-use/dead→dec); re-verify VF-1 (overcount balanced pairs pass) + AOT no-regression. Invoke-inc stays (RL-1/RL-2-faithful). Committed-red remediation + the faithful §03A deliverable, unified.

• 2026-05-30 — FAITHFUL-EMISSION NEXT STEP diagnosed precisely: Invoke-result FRESH-inc is a structural GAP (terminator dst never reaches the ArcInstr FRESH-inc path). §05 is work-order-blocked on §03A FAITHFUL completion (§05 depends_on §03A; §05.3 requires “per-edge net-0 holds pre-elimination” on the §03A-repaired baseline — my masking is post-realize padding, NOT faithful Phase-5 emission). So the next §03A work = replace masking with faithful Step-4b emission, gap-by-gap, until VF-1 holds emission-alone WITHOUT post-realize padding. FIRST GAP (definitively diagnosed): emit_fresh_site_burden_inc (burden_lower.rs:1348) matches only ArcInstr variants (Apply/Construct/PartialApply/Reuse/CollectionReuse/ApplyIndirect) — but Invoke/InvokeIndirect are ArcTerminators, NEVER ArcInstrs, so an Invoke RESULT (dst, defined on the normal-successor block) gets no FRESH-site BurdenInc. terminator_inc_vars (:648) handles terminator ARGS (values passed INTO the call), not the call RESULT dst. Net effect: a substring/concat Invoke result with ReturnContract.uniqueness ∈ {Unique, MaybeShared} gets its last-use BurdenDec (§03A.2) but no FRESH-site inc → the net=−1 the masking was covering (str_split var-5 class). FAITHFUL FIX: emit FRESH-site BurdenInc for Invoke/InvokeIndirect results — gated on the callee ReturnContract.uniqueness ∈ {Unique, MaybeShared} mirroring the Apply arm at emit_fresh_site_burden_inc:1363-1378 + the §03A.1 transfer-suppression — placed at the normal-successor block top (where the Invoke dst is live), via a new terminator-result-inc computation analogous to compute_terminator_inc_per_block but for the RESULT not the args. This closes the str_split class faithfully at Phase 5, shrinking the masking’s residual. Subsequent gaps (cross-block scope-exit BurdenDec faithfulness) follow the same pattern until masking is inert → remove it. THEN §03A closes faithful → §05 unblocks.

• 2026-05-30 — STATUS CONFIRMED EMPIRICALLY + §05-next: §04B gate COMPLETE (architecture validated), §03A VF-1 coexistence-satisfied, the 17 runtime double-frees are §06/§09-territory. Confirmed by reading code + plan: (1) instr_dispatch.rs:509 — whole-var BurdenInc/BurdenDec are codegen NO-OPS today (predicate stack does real RC; BurdenDecPartial/Field/Variant already lower to RC — partial §06 lowering exists, whole-var awaits §06); (2) NO BurdenInc→RcInc whole-var lowering exists yet (grep-confirmed — §06 is the not-started deliverable); (3) §04B’s 7 Prototype-Gate criteria are ALL status: complete (criterion 1 = match_alias emission-alone dissolution PASSED) — the architecture is VALIDATED, §05+ unblocked; (4) §05/§06/§07/§09 are ALL not-started. CONSISTENT PICTURE: the masking scaffold is harmless TODAY (no-op markers; predicate stack does RC with its 17 BUG-04-123 double-frees); at §06 whole-var burden→RC lowering makes faithful burden ops the RC ledger + §09 retires the predicate stack → the 17 double-frees dissolve. The masking’s whole-var padding would mis-lower to spurious RcDec at §06, so it MUST be superseded by faithful Phase-5 emission (§05.3 precondition: “Phase-6 elimination operates over the §03A-repaired FAITHFUL Phase-5 emission baseline — per-edge net-0 holds pre-elimination”) + removed at §09. §03A’s residual faithful-emission gaps (the str_split Invoke-result FRESH-inc class) belong in burden_lower.rs (Phase 5), NOT post-realize padding. MISSION CRITICAL-PATH = §05 (Phase 6 lattice as ELIMINATOR-only, never constructs burden ops) → §06 (whole-var burden→RC lowering + predicate-stack RC non-emission) → §07 (value-shape coverage) → §09 (predicate-stack retirement) → §12 green. Plan scope CORRECT (all sections exist, §04B validated the path); the §05→§09 migration is the high-effort work the mandate names. The masking balancer + verifier-helper-extraction + §03A.1/2 Step-4b faithful gap-repairs stay in the working tree (uncommitted, no-op-safe, codegen-unblocking for §06 testing); tests red (19 = 17 §06/§09-territory + 2 VF-1 loop residuals) so no commit per §Failing-Tests-Mid-Work.

• 2026-05-30 — ARCHITECTURE RE-GROUNDING (00-overview mission): the burden ledger BECOMES the RC ledger at §06; masking is a coexistence scaffold, faithful overcount emission is the endgame. Per 00-overview.md §Mission + Mission-Success-Criteria: §06 (Phase 7 mechanical lowering) maps BurdenInc → RcInc, BurdenDec → RcDec; the 17 BUG-04-123 runtime double-frees/leaks dissolve at §06/§09 because the FAITHFUL balanced burden ops lower to correct RC, REPLACING the predicate-stack’s buggy emission (§09 retires the predicate stack). IMPLICATION for my (C) balancer: its no-op masking PADDING (inc-injection / terminal-dec / merge-equalize beyond the consensus dec-mirror) would, at §06, lower to SPURIOUS RcInc/RcDec → reintroducing double-frees (unless Phase-6 DP-2/DP-3 prunes the adjacent pairs first). So the masking is COEXISTENCE-ONLY (its value: VF-1-clean unblocks codegen → the 17 bugs are visible/testable NOW; it is removed when §09 rebuilds emission faithfully). The architecture’s required §03 emission is the OVERCOUNT: BurdenInc at every transfer + BurdenDec at every last-use along every path, NO cross-path dedup (decisions/07 §8) — Phase 6 DP-2/DP-3 prunes redundant pairs over the per-path-balanced baseline. §03A repairs the GAPS in §03’s overcount (missing inc/dec for specific shapes = the BUG-04-121 net±1); the §03A.1/2 Step-4b fixes (643→124) were faithful gap-repairs, the post-realize masking (124→2) is the coexistence stopgap. MISSION = full migration §04B(Prototype Gate; criterion 1 = match_alias double-free dissolution via burden→RC lowering is the architecture’s CORE CLAIM) → §05 → §06 → §07 → §09 → §12 green. Plan scope is CORRECT (all sections exist); no restructuring needed. NEXT critical-path: §04B Prototype Gate — validate faithful emission + a Phase-7-prototype lowering dissolves the match_alias double-frees (proves the path); the 2 VF-1 loop residuals + masking-vs-faithful resolve inside that validation.

• 2026-05-30 — CRITICAL PIVOT: VF-1 balancer unblocked codegen (643 → 2) but the REAL bugs are predicate-stack RC double-frees, not burden imbalances. Re-grounding required. The (C) verifier-guided balancer (4 mechanisms + RPO ordering) drove full-AOT VF-1 burden imbalances 124 → 20 → 19; E5001 (codegen-blocking) down to 2 (main v18 loop cases needing a true fixpoint dataflow my single-pass can’t match). BUT categorizing the residual 19 revealed only ~2 are VF-1/E5001; the other ~17 are RUNTIME failures — codegen now proceeds (VF-1 unblocked) and the binaries DOUBLE-FREE / leak / mis-output. CONFIRMED: higher_order::test_hof_closure_capture_in_loop builds clean (0 E5001) then aborts at runtime with ori_rc_dec called on already-freed allocation — double-free bug in the compiler's RC codegen. These 17 are genuine PREDICATE-STACK realization RC bugs (RL-2/RL-4/RL-5 dec placement: loops, recursion, break/continue, closure-capture, and the §03A.3b cross-class alias chains match_alias(3) + aims_burden_alias(1)), exposed — not caused — by VF-1 clearing (burden ops are codegen no-ops per instr_dispatch.rs:509, so the masking markers cannot cause a runtime fault). Mechanism re-grounding flagged: §03A criterion 1 (“emission faithfully DISSOLVES the double-frees”) works via burden ops DRIVING DP-2/DP-3 elimination of the spurious predicate-stack RcDec — but the masking balancer runs POST-realize (after Phase-2.5 elimination already ran on §03A.1/2’s buggy burden ops), so it makes VF-1 pass without dissolving the double-free. The masking-balancer is therefore the WRONG layer for criterion 1; the cure is faithful burden emission that drives elimination to remove the spurious RcDec, OR a direct predicate-stack dec-placement fix per decisions/07 (Model-B shallow container drop) + RL-2/RL-4 proofs. NEXT: re-read decisions/07 + RL-2/RL-4/RL-5 proofs + the predicate-stack RcDec emission (realize/walk_dec.rs, emit_rc/edge_cleanup.rs) to locate the over-emission root for the double-free class; route via /fix-bug per §04B.N checker_smoke_failed. The burden VF-1 balancer stays (it unblocks codegen so the runtime bugs are VISIBLE + testable); the 2 main VF-1 loop residuals + the masking-vs-faithful question fold into the predicate-stack-fix re-grounding.

• 2026-05-30 — (C) reconciliation matured into a verifier-guided per-path BALANCER; full-AOT VF-1 124 → 20, zero regression. aims/realize/burden_mirror.rs::reconcile_burden_ledger (post-realize, pre-verify) now balances the per-value burden ledger against the verifier’s own per-path forward dataflow. Four mechanisms: (1) inc-surplus dec-mirror (mirror each RcDec for a FRESH-inc-no-dec var — scope-exit release class); (2) forward inc-injection (inject BurdenInc before any whole-var dec that would drive the running net < 0 — uncovered-release / spurious-dup-dec class); (3) terminal dec-injection (inject BurdenDec at a terminal whose running net > 0 — uncovered-inc-on-a-branch class); (4) merge-equalization (inject BurdenDec on higher-net predecessors to reduce them to the agreed minimum — merge-disagreement class), then iterate-to-fixpoint (a merge-equalize can un-balance a shared pred’s sibling branch; the next pass balances it; balanced vars inject nothing = convergence). Staged full-AOT under ORI_VERIFY_ARC=1: 124 → 78 → 45 → 41 → 24 → 20 (passed 2179 → 2283, zero regression, arc:: clamp 60/60). The verifier’s entry-net forward dataflow was extracted to a shared SSOT aims/verify/burden_delta.rs::compute_burden_entry_nets (consumed by verify_burden_balance; 47 verifier tests green post-refactor). Permanent gated diagnostic ORI_LOG=ori_arc::aims::realize::burden_mirror=debug (per-function mirrored_decs/injected_incs/injected_decs). Honest framing of the masking trade-off: the balancer covers §03A.1/2’s residual imbalances with no-op markers (burden ops are codegen no-ops per instr_dispatch.rs:509), NOT a semantically-faithful structural mirror. It is mission-correct + load-bearing-safe — it runs AFTER Phase-2.5 elimination and the proven §11 coexistence handshake, touches no real RC, so it pollutes nothing that matters in the coexistence era. Per the design-consensus verdict (B-full→C), the semantically-faithful structural mirror (every burden op ↔ a specific RC op, incl. RL-2 transfer-point handling) is the §09 predicate-stack-retirement endpoint, NOT now. Mission-critical gate before close: ORI_CHECK_LEAKS=1 + dual-exec parity on the burden-alias shapes (criterion 5) — the reconciliation never alters predicate-stack RC, so any real double-free is independent of it.

• 2026-05-30 — (C) reconciliation cleared full-AOT VF-1 124 → 45 (dec-mirror + inc-pair); residual 45 = per-path count-imbalance class. aims/realize/burden_mirror.rs::reconcile_burden_ledger now handles BOTH gap classes (post-realize, pre-verify): inc-surplus → mirror each RcDec with a whole-var BurdenDec; dec-surplus → pair a balancing BurdenInc before each whole-var BurdenDec. Eligibility gates on the LIVE post-elimination ledger, never the stale burden_emitted flag. Staged results under ORI_VERIFY_ARC=1 full AOT: 124 → 78 (dec-mirror) → 45 (inc-pair), ZERO regression (arc:: clamp 60/60; passed 2179→2258), 7 unit pins. Permanent gated diagnostic ORI_LOG=ori_arc::aims::realize::burden_mirror=debug (per-function gap-class trace) + the existing ori_arc::aims::verify::burden_balance=debug per-block-delta trace localize residuals. RESIDUAL 45 characterized (e.g. fat_ptr_iter::...str_split_on_substring var 5): the var is PRESENCE-balanced (3 inc/dec pairs) but COUNT-imbalanced by ONE spurious unpaired burden_dec at a %7 = %5 dup-alias point (§03A.2’s dup-alias suppression missed an Invoke-result alias), so the gap-class presence gate (has_inc && has_dec) skips it while the per-PATH verifier flags bbN:-1. NEXT round: either (a) verifier-guided reconciliation — run compute_var_block_deltas + forward dataflow, place a balancing op in the block whose entry_net+delta is nonzero (handles scope-exit cross-block flow correctly, unlike naive per-block-zero), or (b) §03A.2 root fix: suppress the spurious dup-alias burden_dec for Invoke-result aliases. Round-by-round vs the 2258 clamp until 0; then dual-exec + ORI_CHECK_LEAKS + commit.

• 2026-05-30 — (C) scope-exit dec-mirror LANDED (dec side); net=−1 evidence points to a FULL structural mirror as the endpoint. Shipped aims/realize/burden_mirror.rs::reconcile_scope_exit_burden_decs — a post-realize pass (pipeline mod.rs between Phase-2 annotations and emit_postprocess, after unwind cleanup, before the burden verify) that mirrors each predicate-stack RcDec with a whole-var BurdenDec for vars with a LIVE BurdenInc and no whole-var BurdenDec. Eligibility gates on the CURRENT (post-elimination) inc presence, NOT burden_emitted — a regression caught mid-implementation: burden_emitted is set at Step-4b but Phase-2.5 DP-3 may eliminate the inc, so gating on the stale flag over-decremented eliminated-inc vars (vars 8/9/18/19 went net=−1). 5 unit pins in burden_mirror/tests.rs incl. the eliminated-inc regression pin. RESULT under ORI_VERIFY_ARC=1: generics:: 15→7 failed, arc:: clamp holds 60/60 (zero regression). REMAINING net=+1 in other clusters + the pre-existing net=−1 (44) class are NOT cleared by the dec-mirror. DECISIVE net=−1 evidence (fat_ptr_iter::...str_split_on_substring, var 5): a substring Invoke result carries a burden_dec %5 (bb1) but NO burden_inc %5 anywhere — §03A.1’s FRESH-site inc never fired for the Invoke result while a dec was emitted, i.e. §03A.1/2’s INDEPENDENT burden derivation mis-places ops vs the RC ledger. Per the CH-comp “same RC ops per (v,pp)” proof, the endpoint is the FULL structural mirror (BurdenInc per RcInc + per FRESH alloc; BurdenDec per RcDec), replacing §03A.1/2’s independent emission — the dec-mirror is the proven first increment; the inc-side + §03A.1/2 supersession is the next round (careful TDD against the 2179 clamp; the dec-mirror’s eligibility-gate lesson — consult the live ledger, never the stale flag — carries forward).

• 2026-05-30 — B-full→C reversal (design consensus): scope-exit dec fidelity ships as the (C) coexistence-mirror, NOT B-full self-sufficient extraction. Grounding the remaining-124 scope-exit class surfaced that the predicate-stack RcDec for cross-block-dying values is emitted by the main realize walk (realize/walk_dec.rs last-use + realize/emit_unified.rs/walk.rs scope-exit), entangled with BUG-04-104 PIN-4/5/6 SSA-alias-class suppression + return-transfer suppression — a faithful self-sufficient death-point SSOT extraction (B-full) is realization-rewrite-sized AND re-derives lattice-owned logic. Two independent design-consensus reviewers converged on (C): (1) CH-comp.proof case 1 proves coexistence_dispatch ≡ burden_emission_path AND ≡ predicate_stack_path — the proven model is COEXISTENCE, not self-sufficiency; the prior §03A goal “NOT mirroring the predicate-stack” diverges from the proof (arc.md §Debugging: the divergent artifact is the bug). (2) arc.md Invariant-5 bans independent RC emission paths — B-full’s independent burden death-point analysis IS that; (C)‘s single-source mirror is invariant-safe by construction. (3) RL-2 transitivity makes (C)‘s BurdenDecs net-0 for free. (4) elimination is Phase 2.5 (emit_unified.rs:241) so a Step-5 mirror survives ORI_DISABLE_BURDEN_ELIM=1. (C) is correct STAGED delivery; full self-sufficiency anchors to §09 predicate-stack retirement (the §06 realize-rewrite). Reverses the §03A.3a PULL-BACK #3 “pursue B-full” pick. Cure shape: count-reconciliation post-realize pass (#BurdenDec == #BurdenInc per burden_emitted var, gap-filled at un-mirrored RcDec sites — self-dedups vs landed Step-4b/edge decs). Anchors §03A.N close gate (BUG-04-121) without absorbing §06.

• 2026-05-30 — /review-plan Step-5 editor pass: body dependency-model drift cured + VF-1 close-gate CI-aligned + VF-1 scope boundary made explicit. Four refinements applied (no halt-gating): (bs1) every body reference framing §04B as a BLOCKING dependency rewritten to EVIDENCE-input framing (the §04B Criterion-1 evidence artifact decisions/gate-criterion-1-evidence.md is what §03A consumes + produces 12/16→16/16; §04A is the companion VF-1-verifier-robustness fix) — the “Why a sibling section” + “Depends on:” lines + Context paragraph + the test_unwind_path_alias bullet now match frontmatter depends_on: ["03"]; §04B NOT re-added. (bs2) §03A.4 emission-alone + AOT close gates + success-criterion 2 now carry the ORI_VERIFY_ARC=1 prefix and the explicit CI-aligned verifier-invocation command (ORI_VERIFY_ARC=1 ORI_DISABLE_BURDEN_ELIM=1 cargo test --release -p ori_llvm --test aot) — without it the 643 VF-1 net=1 failures stay hidden under a bare cargo test (test-all.sh:97 + ci.yml:11 both set it). (ar1) success-criterion 2 + the §03A.3 verifier-green item narrowed to the BASIC function-exit VF-1 that burden_balance.rs ships today; FULL per-edge/SCC VF-1 named as §10’s explicit owner per the burden_balance.rs:22 module-doc deferral. (bs3) §03A.N item 4 flipped [x] — §05 reaches §03A via the linear depends_on: ["04B"] chain (§03A is the upstream linear predecessor, not a direct §05 depends_on entry).

• 2026-05-30 — depends_on cut ["03","04B"] → ["03"]: §03A unblocked as the workable critical-path cure for the 643-failure VF-1 burden imbalance (BUG-04-121). Per user directive (CI/local failure alignment + “back-and-forth between plans is 100% expected”). Grounding: GitHub nightly ci.yml (the merge-blocking “CI” check on the dev→master nightly PR) AND local ./test-all.sh BOTH set ORI_VERIFY_ARC=1, so both surface the same 680 AOT failures — 643 burden imbalance (VF-1): vN net=1 expected=0 ICEs + 4 leaks + 2 double-frees + ~30 typeck/parse + 16 clippy unfulfilled-lint; bare cargo test (no env var) hides them, which is why a scoped probe of a CI-failing test passes locally. The 643 net=1 = emit_burden_ops (default-ON, AIMS Step 4b) emitting BurdenInc without a matching BurdenDec = §03A.2 RL-2 BurdenDec-fidelity. §03A’s touches: set (burden_lower.rs, burden_balance.rs, match_alias.rs) is DISJOINT from §04 (recursive-type LLVM layout) — the RL-2 repair is a general emission-fidelity fix, not specific to recursive types. §04B Criterion 1 (16/16 match_alias emission-alone) is what §03A PRODUCES; the §04B references in this section are retained as EVIDENCE input (decisions/gate-criterion-1-evidence.md, 12/16 baseline), not a blocking dependency. Resolves the 2026-05-30 00-overview HISTORY user-decision-surface option (a). §04 recursive codegen (BUG-04-043, 9 of the 643) proceeds in parallel on its own §04 branch.

• 2026-05-30 — Folded the BUG-04-123 §05 over-emission RCA + BUG-04-121 into §03A (plan reframe per user directive). The 3 over-emission match_alias cells in 03A.3 (match_arm_alias_result_str / unwind_path_alias / option_intlist_select_branch_return) ARE BUG-04-123’s over-emission cells; the precise predicate-stack root (InlineEnum container dec recursing into the moved-out payload; unwind-edge foils post-dominance) + the 4 ruled-out predicate-stack suppression models are preserved in decisions/07 §5 — do NOT port a predicate-stack suppression patch; the burden cure is the Model-B shallow container drop + the payload’s own BurdenDec. §03A success-criterion 2 (zero VF-1 imbalances) IS BUG-04-121 (critical — emit_burden_ops default-ON emits BurdenInc without a matching BurdenDec, net=1, ICE-ing all AOT codegen); §03A.2 closes the missing-dec root, §04A owns the companion verifier-robustness fix. BUG-04-123 absorbed to 00-overview.md absorbed_bugs[].

• 2026-05-29 — §03A created via /create-plan --inline (routing.md §3 case b) — emission-fidelity half of the §04B impl-fidelity verdict. Per the 2026-05-29 reground: §04B Criterion 1 proved §03’s shipped Phase-5 emission diverges from the proven RL-1/RL-2/RC-balance (12/16 match_alias under ORI_DISABLE_BURDEN_ELIM=1; VF-1 burden imbalances). §03A owns repairing the EMISSION to the proven calculus (the elimination/coverage/retirement fidelity is the reframed §05/§07/§09; specific divergent sites route via /fix-bug per the §04B.N proven_by override). Sibling section (not §03 re-open) because §03’s walker shipped + unit-green; §03A is the independently-workable integration-fidelity repair. depends_on §03 + §04B; feeds §05.

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