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

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

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

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

Depends on: Section 07B — status: in-review at edit time (broad-shape burden self-sufficiency; frontmatter depends_on: [07B]). §09 is status: blocked until §07B closes complete + reviewed: true. §07A (status: complete, reviewed: true, closed 2026-06-04) made the burden path a standalone RC emitter for the NARROW shapes its 11-probe ORI_DISABLE_PREDICATE_STACK_RC suite covered (move-alias / dup-alias / borrow-chain / collection-buffer-last-use / closure-capture / partial-move), but the 2026-06-04 §09.2 re-measurement proved that gate TOO NARROW: under the flag the full AOT corpus regresses 2344/16 → 1784/576 (+560) on broad shapes the 11 probes never exercised (iterator-from-collection / fat-pointer-matrix / iter-RC-chain / collection-element / SSO). §07B completes the remainder AND replaces the narrow 11-probe gate with the full-corpus-under-flag SET-subset readiness signal (failing_ids_under_flag ⊆ baseline_failing_ids). The proven-equivalence license precondition for §09.2/§09.3/§09.4/§09.N has TWO halves — §07’s universal class_covered (coverage, MET) AND corpus-wide burden-lowering self-sufficiency (MET for narrow shapes via §07A; PENDING for broad shapes via §07B) — so the block is RE-BLOCKED on §07B per the 2026-06-04 RE-BLOCK HISTORY, not lifted. §08 (rule sync + proof re-validation) is a PARALLEL branch per the 00-overview.md DAG (§08 ∥ §09, both gating §10), NOT a predecessor.

Intelligence Reconnaissance

Queries:

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

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

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

09.1 Per-function disposition table for post_convergence.rs

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

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

Subsection close-out (09.1) per protocol.

09.2 Emission-side predicate retirement

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

Subsection close-out (09.2) per protocol.

09.3 ssa_alias_classes.rs consumer simplification

realize/cleanup_redundant.rs, emit_rc/dead_cleanup/mod.rs, realize/walk_dec.rs, emit_rc/edge_cleanup.rs, realize/walk.rs, intraprocedural/state_map.rs continue to consume project_alias_sources / borrow_sources for lattice optimization (NOT removed — these feed Phase 6 elimination). These reside under realize/ + emit_rc/, NOT under intraprocedural/; re-confirm each path resolves at edit time.
Predicate-stack-emission integrations retired; lattice-input consumption preserved.
COD-F1 (relocated from §04A.R per routing.md §4 — latent fragility, §09-coupled) — emit_rc/dead_cleanup/mod.rs:~596 emit_dead_invoke_dsts: the Phase-1.5 fallback used_in_succ scan counts Burden* ops as a live use via ArcInstr::used_vars() (ir/instr.rs:336-347). Latent fragility ONLY — manifest-leak-free today (a genuinely-dead Invoke result receives NO BurdenDec; last-use BurdenDecs co-occur with the real use; verified zero leaks per §04A.R COD-F1 evidence: 3 repros + ORI_CHECK_LEAKS=1). When predicate-stack retirement reshapes/removes the Phase-1.5 fallback sweep, exclude Burden* ops from the used_in_succ liveness scan (a Burden op is a release marker / codegen no-op, NOT a real use — mirrors §06.1 compute_live_out_owned + borrowed-alias-exclusion). Matrix tests: semantic pin (dead Invoke result with a successor BurdenDec still gets its real cleanup) + negative pin (a genuine real successor use still suppresses cleanup); VF-1 stays 0, AOT zero-new. Cite: §04A.R COD-F1 finding (full grounding evidence) + LEDGER §B.2.
Tests: focused tests verifying lattice optimization continues to work over burden-emitted IR.

Subsection close-out (09.3) per protocol.

09.4 Coexistence handshake removal (proven-equivalence-licensed)

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

Verify BOTH preconditions of the proven-equivalence license: (1) §07 close-out confirmed class_covered is universal across the test corpus (the coverage-analysis precondition above), AND (2) §07B close-out confirmed the burden path is a complete standalone RC emitter CORPUS-WIDE (the RC-lowering self-sufficiency precondition). §07A (status: complete, reviewed: true) covered the NARROW shapes (its 11-probe ORI_DISABLE_PREDICATE_STACK_RC suite passed zero-new-vs-16-baseline + leak-free + double-free-free), but the 2026-06-04 re-measurement proved the full corpus regresses 2344/16 → 1784/576 under the flag on broad shapes — so §07B (the §09 gating dependency, depends_on: [07B]) completes the broad-shape lowering AND its full-corpus-under-flag SET-subset gate (failing_ids_under_flag ⊆ baseline_failing_ids) is the corpus-wide self-sufficiency signal §09 consumes. The handshake-removal license needs BOTH: universal coverage alone (§07) leaves VF-1=0 holding by net-zero ABSENCE of deferred ops while the predicate stack supplies the real freeing RC, so deleting the predicate stack on §07 alone would regress (the §09.2 attempt empirically measured AOT 2329/16 → 1300/1045 per §09 HISTORY 2026-06-03); §07A closed that gap. Record both confirmations in the §09.1 disposition document. NOTE (codex-F1, 2026-06-03): during coexistence class_covered is EMPTY for every function — populate_class_covered runs inside analyze_function (Step 4) and reads func.burden_emitted which emit_burden_ops only fills at Step 4b (after), so the empty-burden_emitted short-circuit always fires (see §04A.3 note). Empirically verifying “universal class_covered” therefore requires FIRST relocating populate_class_covered to run AFTER emit_burden_ops (or re-deriving coverage from the emitted IR). Since this section REMOVES the handshake outright (line below) under the proven-equivalence license (the predicate stack retires → no handshake needed), the universality check is a license-precondition recorded from §07’s coverage analysis, NOT an empirical read of the always-empty coexistence-era class_covered set. If §09 keeps a transitional handshake instead of removing it, relocate the pass behind Step 4b first.
Confirm absence of burden_mirror.rs::reconcile_burden_ledger (the coexistence-only masking balancer): neither compiler_repo/compiler/ori_arc/src/aims/realize/burden_mirror.rs nor any fn reconcile_burden_ledger resolves anywhere under compiler/ori_arc/src/ at edit time — the mirror was already removed/retired upstream (matches the §06 self-sufficient-Phase-5 lowering that SUPERSEDED it per §03A.3a forward-anchor). The literal removal is a no-op confirm-gone; the verification gate below stays LIVE. The self-sufficiency the removal relied on is proven by CH-1 (AimsProof.Coexistence::CH1_burden_emitted_is_bridge: burden_emitted IS burden_owned, a pure function of the lattice — no independent ledger) + CH-4 (CH4_state_map_immutable: BR reads the frozen state map, L does not depend on BR). Verify the burden ledger nets 0 emission-alone (ORI_VERIFY_ARC=1 ORI_DISABLE_BURDEN_ELIM=1 AOT VF-1-clean) with NO mirror present — if a reconcile_burden_ledger-shaped masking balancer has reappeared anywhere, that reappearance is a §09 defect to remove before the gate passes.
Remove class_covered: BitSet<ClassId> handshake bookkeeping (§04A.3 site). KEEP burden_emitted (func.n, compiler/ori_arc/src/ir/mod.rs:485) — it is the load-bearing burden ledger consumed by the VF-1 burden-balance verifier (compiler/ori_arc/src/aims/verify/burden_balance.rs: “For every v ∈ func.n, verify”) + Phase 6 elimination + the ORI_VERIFY_ARC=1 nets-0 gate above; ONLY the class_covered predicate-stack handshake retires, NOT burden_emitted (codex-F1, 2026-06-03).
Predicate-stack realization paths that read class_covered to skip emission — RETIRED with predicate-stack itself per §09.2.
Dead-code cleanup of AimsStateMap (compiler/ori_arc/src/aims/intraprocedural/state_map.rs) — with the class_covered handshake removed above and the class_dec_obligations-driven predicate-stack dec emission retired in §09.2, DELETE both storage maps + accessors: class_covered: FxHashSet<u32> (field at state_map.rs:493) + is_class_covered / class_covered_count / set_class_covered (state_map.rs:993/999/1008); class_dec_obligations: FxHashMap<(ArcBlockId, u32), ClassObligationEntry> (field at state_map.rs:348) + class_dec_obligations() / set_class_dec_obligations (state_map.rs:1028/1037). Re-confirm the consumer set is empty (scripts/intel-query.sh --human callers is_class_covered --repo ori + ... callers class_dec_obligations --repo ori resolve to zero live readers after §09.2/§09.4 retire populate_class_covered / populate_class_dec_obligations) before deleting; a non-empty residual is a §09 retirement-incompleteness defect to retire, never a reason to keep the storage. cargo build + cargo t green debug + release.
Coexistence-mirror-disabled correctness gate (moved here from §05.N per /review-plan §05 review 2026-06-02 — it tests the self-sufficient burden baseline §09 targets, not the §05 mirror-balanced baseline). With reconcile_burden_ledger confirmed absent above, run the existing AIMS spec + AOT corpus under ORI_DISABLE_BURDEN_OPS=0 with the coexistence mirror gone (the §09 AOT elimination path) — Phase 6 elimination over the unaided burden ledger (netting 0 WITHOUT the predicate-stack mirror) produces zero new lattice-divergence / leak / double-free failures vs the pre-retirement mirror-balanced run. Verifies the burden path’s elimination decisions are self-sufficient post-retirement (the empirical confirmation of the CH-1/CH-4 self-sufficiency proof); a failure here is a §09 emission-self-sufficiency defect cured before §09 close. Both debug + release. (Pairs with the ORI_VERIFY_ARC=1 ORI_DISABLE_BURDEN_ELIM=1 VF-1-clean check above — that proves emission nets 0; this proves elimination over that baseline is leak/double-free-free.)
Tests: cargo t green; full corpus passes via burden ownership alone.
TPR checkpoint — /tpr-review covering 09.1-09.4.

Subsection close-out (09.4) per protocol.

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

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

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

Subsection close-out (09.5) per protocol.

09.R Third Party Review Findings

None.

09.N Completion Checklist

HISTORY

2026-06-02 — Real-RC activation relocated IN from §06.1 (routing.md §4 cure for §06.1 linear-execution block): §06.1 established the clean mechanical-lowering SITE (realize/mod.rs thin dispatcher, zero predicate-stack queries, faithful Phase-5 emission VF-1=0, mirror removed) but its two real-RC [ ] items (BurdenInc→RcInc / BurdenDec→RcDec mechanical-mapping flip + real-RC FileCheck-on-RcDec test pins) were §09-coupled and carried banned  annotations. Per routing.md §4, the items MOVED here: §09.2 retires the parallel predicate-stack RC emitters (walk_dec.rs/emit_unified.rs), so the burden ops become the SOLE RC emitter — the no-op→real-RC flip is safe HERE (the LEDGER §B.2 double-emit/double-free hazard dissolves WITH the predicate-stack removal, never before it). Added: §09.2 checkboxes for the BurdenInc→RcInc/BurdenDec→RcDec activation + its 3 real-RC FileCheck pins; a success_criterion for the activation; realize/mod.rs to touches:. §09 is the natural home — its predicate-stack retirement IS the precondition the activation needs.
2026-06-02 — Reworked §09 to ground the coexistence retirement in the proven §11 CH- theorems + added §09.5 CH-proof disposition.* The retirement of predicate_stack_path + the coexistence handshake was reframed from a mechanical deletion to a PROVEN-EQUIVALENCE-LICENSED deletion: §07’s universal class_covered collapses the proven CH-comp soundness partition (CHcomp_handshake_union + CH2_single_elimination + CH3_classes_disjoint) to its class_covered case, where coexistence_dispatch ≡ burden_emission_path ≡ predicate_stack_path — so deleting the redundant predicate path preserves observable behavior by the proof. The reconcile_burden_ledger mirror removal is grounded in CH-1 (burden_emitted = burden_owned, no independent ledger) + CH-4 (CH4_state_map_immutable, BR reads L read-only). Added §09.5 to fill the gap the research surfaced — aims-proofing-suite §11 has no supersession clause, so §09 (the consumer) records the disposition: the CH .proof + lean/AimsProof/Coexistence.lean are RETAINED as the MS-4 published theorem + the retirement-safety certificate (the proofs are over the model, not the shipped Rust, so the shipped deletion leaves them kernel-valid); CH-4’s shipped eliminate_burden_ops binding SURVIVES; dual-discharge.sh re-runs clean post-retirement as a confirmation step. mission criteria 13 + 16 noted as the §09 close-out flips.
2026-06-02 — Coexistence-mirror-disabled correctness gate moved in from §05.N (per /review-plan §05 review, 3-reviewer Critical STRUCTURE:section-not-independent). The gate tests Phase-6 elimination over the SELF-SUFFICIENT burden baseline with the reconcile_burden_ledger coexistence mirror OFF — the post-convergence elimination state §09 targets, not §05’s mirror-balanced baseline. Self-sufficient burden emission is not implemented until §09 retires the predicate stack + mirror, so gating §05 close on it would either block on downstream §09 work or be unverifiable at §05 close. Landed as a §09.4 checkbox (alongside the existing reconcile_burden_ledger removal + emission-nets-0 VF-1 check) + a §09.N completion-checklist item. §05’s success_criteria stay scoped to mirror-balanced DP-2/DP-3 elimination correctness.
2026-05-30 — Recorded the 6 BUG-04-123 surgical fixes as predicate-stack annotations §09 strips (plan reframe per user directive). BUG-04-123’s §05 landed 6 narrow predicate-stack patches (32 -> 17): container_payload_moved_out (post_convergence.rs), the PIN-4 defined_at_or_before guard (edge_cleanup.rs), class_member_suppresses post-dominance dedup (emission_site.rs), and build_global_pin4_emits / build_lineage_map / predict_retained_roots consumption-aware lineage machinery (emit_unified.rs + walk.rs). These are annotations the completed burden path supersedes — 09.2 retires them alongside class_alive_after / pin4_class_emits_dec_set / pin6_any_ancestor_will_cover, mirroring BUG-04-118’s 62. The four uncoordinated emission paths they patch collapse to one burden trivial-emit + DP-2/DP-3 elimination path; decisions/07 §4.1 + §8 carries the rationale + the empirical proof (10 ruled-out broad approaches). BUG-04-123 absorbed to 00-overview.md absorbed_bugs[]; realize/emit_unified.rs added to §09 touches.
2026-05-29 — §09 reframed as the GREEN-CRITICAL coexistence retirement (per 00-overview.md 2026-05-29 reground). The ~671 ./test-all.sh VF-1 burden-imbalance failures are impl-fidelity divergences resident in the burden-op ↔ predicate-stack COEXISTENCE layer — a TRANSITIONAL migration bridge whose soundness the proven CH-1..CH-comp certify (CH-1 reformulated_and_proven, CH-2..CH-comp proven_sound per the aims-rules.md HISTORY 2026-05-28 terminal-state table; .proof at compiler_repo/aims-proof/proofs/11-coexistence/CH-*.proof + Lean mirror AimsProof/Coexistence.lean), alongside the core calculus (DP/RL/VF/IC/PL) of the kernel-checked corpus. §09’s retirement of the emission-side predicate stack (class_alive_after / pin4_class_emits_dec_set / pin6_any_ancestor_will_cover / canonical_rep_for / var_emits_dec_in_block) + the class_covered coexistence handshake is therefore the load-bearing path to full green: it DELETES the coexistence machinery — which the completed burden path SUPERSEDES — so the compiler runs on the proven burden calculus alone, dissolving the 671 by construction rather than hand-fixing each. The proven CH coexistence proofs certify the §07→§09 bridge during the migration window; the layer is superseded, NOT a permanent dependency of the end state. Precondition unchanged: §07 class_covered universal before the handshake removes itself.
2026-06-03 — Stale review_pipeline: marker cleared by /continue-roadmap orchestrator: marker carried stage: ?, next_step: ?, updated: ?. Per /review-plan SKILL.md §Step 1a stale-marker rule (reviewed: false + marker present → STALE by definition), marker invalid; prior diagnosis preserved here for traceability. Cure rooted in scripts/plan_orchestrator/markers.py:clear_stale_marker_if_unreviewed.
2026-06-04 — §07A closed → §09.2/§09.3/§09.4/§09.N block LIFTED. §07A (Burden-Lowering RC-Ledger Self-Sufficiency) reached status: complete + reviewed: true (its HISTORY 2026-06-04 + §07A.N checklist): the burden path is now a complete standalone RC emitter — the ORI_DISABLE_PREDICATE_STACK_RC self-sufficiency probe (11 probes, compiler/ori_llvm/tests/aot/predicate_stack_probe.rs) passed zero-new-vs-16-baseline + leak-free + double-free-free under ORI_CHECK_LEAKS=1, with the move-alias / duplication-alias / borrow-flow / collection-buffer RC the overlay had deferred to the predicate stack now emitted by the burden path itself. The §09.2-readiness gate (the §07A.3 corpus gate) is MET. The structured blocker is the section-level depends_on: [07A] (already in frontmatter, schema-supported), now SATISFIED by §07A’s completion — the SubsectionEntry schema carries no per-subsection blocked_by field, so the §09.2/§09.3/§09.4/§09.N block is recorded by the satisfied section-level depends_on plus this HISTORY note (per state-discipline.md §3 + routing.md §2 — the block is no longer §05-prose-only). The 2026-06-03 BLOCKED entry below is the at-block diagnosis, now resolved. §09.2 reverts to not-started (the 2026-06-03 attempt reverted cleanly to baseline with no §09.2 checkboxes flipped, so no in-progress work persists; §09.2 is ready-to-start). §09.4’s first checkbox now gates on BOTH §07 (coverage) AND §07A (lowering self-sufficiency). Added: §07A predicate-stack-retirement readiness verification (re-run the 11-probe suite) to the §09.2 activation close-gate; a dead-code-cleanup success criterion + §09.4 checkbox + §09.N item deleting the class_covered + class_dec_obligations storage maps + accessors from AimsStateMap (state_map.rs); realize/{tests,decide}.rs, realize/burden_elim/tests.rs, intraprocedural/mod.rs, interprocedural/extract.rs to touches: (handshake-removal compilation surface).
2026-06-03 — §09.2 BLOCKED: burden path is NOT a complete standalone RC emitter (empirically discovered + verified-with-facts). §09.1 disposition done (decisions/09-post-convergence-disposition.md, commit 41e7b1dc). §09.2 execution attempted the lockstep predicate-stack-retirement + real-RC-activation, measured the corpus, reverted cleanly (compiler tree at baseline AOT 2329 pass / 16 fail). Discovery: lower/burden_lower/mod.rs:261 states verbatim a Let { Var(src) } duplication-alias whose source stays live “carries NO burden ops” because “the predicate-stack emits the alias’s real RcInc/RcDec” — burden_lower is a duplication-tracking OVERLAY that deliberately DEFERS move-alias / Let-Var-alias / borrow-flow RC to the predicate stack. Removing the predicate stack with burden-as-sole-emitter regressed AOT 2329/16 → 1300 pass / 1045 fail (+1029 systemic) across every RC category (fat_matrix, fat_ptr_iter, collections_ext, rc_matrix, string_sso, cow_map_set, …): move-alias chains double-free (pre-elim) or LEAK (post-DP-2-elim collapses the freeing dec); collections emit NO RcDec. ROOT: §07’s class_covered-universal + VF-1=0 claim is true for coverage ANALYSIS but FALSE at the RC-LOWERING level — VF-1=0 holds precisely BECAUSE the deferred ops carry no burden ops (net-zero by absence) while the predicate stack supplies the real freeing RC. The proven calculus (RL-2 dec-at-last-use, CH-1 burden_emitted = burden_owned) is the spec; the burden_lower IMPLEMENTATION diverges by deferring move/alias/borrow RC. CURE (architecturally-correct, soundness-load-bearing per the standing directive): a NEW prerequisite work item makes emit_burden_ops/burden_lower emit a COMPLETE standalone RC ledger — (a) NO BurdenInc for move-aliases (Let { Var(src) } where src is consumed), (b) a BurdenDec at the true final last-use of each allocation lineage that SURVIVES DP-2 elimination (not elided as move-through-Dead), (c) the duplication-alias RcInc/RcDec the overlay currently defers — BEFORE §09.2 predicate-stack retirement is sound. §09.2 / §09.3 / §09.4 / §09.N are now blocked-by that prerequisite (inserted via /create-plan —inline as a sibling sequenced after §07, before §09). No §09 checkboxes flipped beyond §09.1.
2026-06-04 — §09.2 RE-BLOCKED: §07A self-sufficiency INCOMPLETE corpus-wide; §07B prerequisite required (empirically re-measured). §07A closed complete/reviewed:true on the strength of its 11-probe ORI_DISABLE_PREDICATE_STACK_RC gate, but that gate is TOO NARROW. The §09.2 execution (validated end-state behavior before editing, zero code edits, no LEDGER §B.2 dead-end re-tried) measured: AOT baseline (predicate stack ON) 2344/16; under ORI_DISABLE_PREDICATE_STACK_RC=1 (the §09.2 end-state) 1784/576 — +560 NEW failures, the SAME shape as the 2026-06-03 attempt. Scoped confirm: fat_ptr_iter 136/0 → 21/115. Newly-failing clusters: fat_ptr_iter (115), fat_matrix (59), iter_rc_matrix (52), generics (38), rc_matrix (31), elem_dec_scope (26), collections_ext (26), string_sso (16). ROOT: lower/burden_lower/ tracks only the whole-var collection result and DEFERS per-element / iterator-source / collection-element / matrix / SSO RC to the predicate stack — the 11 probes (move-alias / dup-alias / borrow-chain / collection-buffer-last-use / closure-capture / partial-move) never exercised these shapes, so the CH-comp proven-equivalence license (class_covered universal) is FALSE for them. CURE (per standing directive — plan-expansion territory, /create-plan —inline, choose-recommended-not-ask): a §07A-class prerequisite §07B (broad-shape burden self-sufficiency: iterator-from-collection / fat-pointer-matrix / iter-RC-chain / collection-element / SSO) that ALSO replaces the narrow 11-probe readiness gate with the FULL AOT corpus under ORI_DISABLE_PREDICATE_STACK_RC=1 = zero-new-vs-baseline (the corpus IS the probe). §07A stays complete for the shapes it covered; §07B completes the remainder. §09.2/§09.3/§09.4/§09.N gate on §07B. No §09 checkboxes flipped. Cross-ref: LEDGER §B.2 + §B.3 2026-06-04 re-block lines.