S06 Cutover III - protocol/loop family + tail-pass folding

Goal

Iterator-protocol, catch/unwind, and loop-carried shapes emit from contract-derived ledger events; the emit_unified 6.5-6.99 shape passes fold into the emitter core; the general net engine is the only remaining post-pass.

Family (verified)

Scans: iter_consume_dead_thread(/), lazy_iter_closure_borrow(/), catch_recover_release.rs, loop_carried_dead_param/, cow_terminal_concat.rs, ttr-iter overlap arms in dup_inc (if residual post-S05). Realize tail passes: Phase 6.5-6.99 in aims/realize/emit_unified.rs (~26 passes per the session inventory), with transfer_anchor_net already promoted (S03) and the remainder folded here.

Explicit gates (reviewer-added)

• Every ApplyToIterConsumingParam site classifies its partition entry as CONSUME/TRANSFER, never BIRTH (unit-tested).
• Closure-env release dominates captured-payload release (matrix row; the env drop cascade is the capture’s release).
• TRMC probe cells: context-hole threading + the KEPT-230 self-recursive back-edge result-dec shape stay green (T2’s model covers rewritten CFGs).

Work Items

• Cut the protocol/loop family: iter_consume_dead_thread/, lazy_iter_closure_borrow/, catch_recover_release.rs, loop_carried_dead_param/, cow_terminal_concat.rs, ttr-iter-consume overlap arms replaced by contract-derived ledger events (iter-consume transfer, keep-alive from consume-count, unwind-path accounting)
• Fold the emit_unified.rs Phase 6.5-6.99 shape passes into the emitter core (edge-cleanup = RL-4 leg; 6.66x iter passes = contract events; 6.99 transfer_anchor_net = the emitter verify core); delete folded passes
• Explicit gates: every ApplyToIterConsumingParam site classifies its partition entry as CONSUME/TRANSFER, never BIRTH (unit test); closure-env release dominates captured-payload release (matrix row); TRMC probe cells (context-hole threading + KEPT-230 back-edge result-dec shape) green
• Delete retired scans + toggles same-commit; KEPT cycles; family matrix (iterators x lazy closures x catch/unwind x loop-carried threads x for-yield)
• Gated probe zero-new (debug AND release); full ./test-all.sh green; cross-executor behavior, exact logical ownership/drop/unwind-event, and leak legs
• Abandoned empty shell from a halted mission-fit append; the retried enact re-appends the real head item
• Abandoned empty shell from a halted mission-fit append; the retried enact re-appends the real items
• Abandoned empty shell from a halted mission-fit append; the retried enact re-appends the real items
• Abandoned empty shell from a halted mission-fit append; the retried enact re-appends the real items
• Abandoned empty shell from a halted mission-fit append; the retried enact re-appends the real items

Governing rules (embedded per plan self-containment)

• Calculus-first per arc.md CP-1: the governing theorem lands in compiled Lean BEFORE the consumer ships; never weaken a theorem to pass a shape; four-surface sync per CP-2 on every AIMS change.
• Verdict surface until S08 lands: the gated burden-sole probe ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1 via compiler_repo/diagnostics/aot-guardrail.sh --floor (debug AND release), zero-new vs compiler_repo/compiler/ori_llvm/tests/aot/fixtures/corpus_under_flag_gate/baseline_failing_ids.txt. The default path is FALSE-GREEN until S08 (per arc.md STOP); never cite it as an RC verdict.
• test-all is the compiler-state SSOT: every section-close verdict comes from a full ./test-all.sh run (background, flock-serialized; consume test-all-summary.json), never targeted runs alone.
• Banned cures (each a carried dead-end): use-count/type-membership PROXY discriminators (DE-150/174/175); broadening compute_genuine_same_alloc_reps / ForwarderUnionFind phi edges (DE-181); relocating a release past a multi-pred merge (DE-225/243/249/250); inc-only pair splits (attempt-287 290-UAF class); broad caller-side keep-alive incs (DE-254).
• Every retired scan/toggle records a KEPT ledger cycle with before/after teeth (collapse metric + floor).
• Cross-executor parity over evaluator, VM, LLVM debug/release/AOT, and admitted native/direct-WASM/JIT projections, plus exact logical ownership/drop/unwind-event correspondence and leak freedom, are per-section backend legs (L9 + L10). The AOT burden probe remains a current LLVM-projection migration gate, not the definition of AIMS correctness.

Test strategy

• Matrix: for-in / for-yield / lazy map+filter->collect / eager fold / catch(panic) / nested catch / loop-carried closure + collection threads / iter-then-return overlap.
• Pins: RL2 overlap keep-alive (B=1,T=2 -> one inc); dead-thread no-orphan-inc; lazy-env UAF negative pin.
• Resolve borrowed_invoke_lineage.rs’s ownership explicitly rather than leaving it implicit: corpus-wide grep confirms no section in this plan claims it, it is referenced only by the CLOSED BUG-04-182, and it sits thematically inside this section’s own exact territory — a borrowed-collection release treatment across a may-unwind Invoke (ORI_DISABLE_BORROWED_INVOKE_LINEAGE_RELEASE) with its own dedicated loop-exit variant (ORI_DISABLE_LOOP_BORROWED_LINEAGE_EXIT_RELEASE), i.e. borrowed-collection + may-unwind + loop-carried at once. MISSING_ABSTRACTION confirms its internal shape mirrors this section’s own loop_carried_dead_param/ at 0.929 similarity (the identical two-toggle-one-shape signature), and its borrow-only-vetting predicate is a fourth independent re-derivation of the same primitive already duplicated across catch_recover_release.rs (this section) and live_extract.rs (S05, x2). Fold borrowed_invoke_lineage.rs (both its base release treatment and its loop-exit variant) into this section’s cut family alongside iter_consume_dead_thread/, lazy_iter_closure_borrow/, catch_recover_release.rs, loop_carried_dead_param/, cow_terminal_concat.rs, and the ttr-iter-consume overlap arms, replaced by the same contract-derived ledger events. Its own test-coverage status is NOT confirmed by this section’s intel package, unlike the other five family files whose coverage was directly source-verified — verify it explicitly and, if zero-covered, apply the same walking-skeleton-pin-before-deletion discipline this section’s matrix work item requires for catch_recover_release.rs, cow_terminal_concat.rs, and loop_carried_dead_param/.
• Author and green walking-skeleton-shaped semantic pins pinning the CURRENT behavior of catch_recover_release.rs (the single largest file in this section’s family, with the richest internal call graph), cow_terminal_concat.rs, and loop_carried_dead_param/{mod,vetting}.rs (the shared skeleton backing TWO production RL-5 releases) FIRST — confirmed by direct grep across the file itself, the shared ownership_scans/tests.rs, and lower/burden_lower/tests.rs that all three carry ZERO tests anywhere today, unlike iter_consume_dead_thread.rs and lazy_iter_closure_borrow.rs which each already have a dedicated tests.rs with real coverage. Extend the same walking-skeleton discipline to borrowed_invoke_lineage.rs once its family membership is confirmed (per the sibling family-expansion item), since its own coverage status is unverified. Only once this matrix and these pins are green does deletion proceed: delete each retired scan module + its ORI_DISABLE_* toggle (this section’s remaining family plus borrowed_invoke_lineage.rs’s toggle pair) in the same commit, record each retirement as a KEPT ledger cycle with before/after teeth (collapse metric + floor), and complete the family matrix’s remaining rows (iterators x lazy closures x catch/unwind x loop-carried threads x for-yield) covering the already-tested pair — deleting before the untested trio’s pins are green removes the regression floor and bisection fallback a cutover this size needs, the same sequencing defect S04’s (w-6c58d672) and S05’s (w-5da6d021) own reviews already corrected.

Items

• Fold in BUG-04-160 (medium, in-progress, scaffolded plan dir), BUG-04-161 (high, open, no plan dir), BUG-04-184 (high, open, no plan dir), BUG-04-185 (high, open, no plan dir), BUG-04-239 (medium, in-progress, scaffolded plan dir), and BUG-05-003 (high, in-progress, scaffolded plan dir) per the plan mission’s standing directive (‘Fold-in: every failing burden/RC floor cell surfacing during this plan is worked HERE’). All six are verified open/in-progress in bug-tracker/open-bugs.json and sit squarely in this section’s own failure-mode space: BUG-04-160 (borrowed [str] collection leaks on caught-panic path) and BUG-04-185 (callee-returned template string leaks across catch/unwind) are catch_recover_release.rs’s own territory; BUG-04-161 (owned-arg-transfer into a may-unwind user-call Invoke with a live-across receiver leaks) is borrowed_invoke_lineage.rs’s territory per the sibling family-expansion item above; BUG-04-184 (loop-body str-literal lineage leaks per iteration) is loop_carried_dead_param/‘s territory; BUG-04-239 (generic Set by-value param + .iter() double-frees under LLVM/AOT) is iter_consume_dead_thread/‘s territory; BUG-05-003 (ori_iter_join direct string path leaks owned string elements from map/filter adapters) is lazy_iter_closure_borrow.rs/iter_consume_dead_thread/‘s territory. None of the six appear in S09’s 8-bug folded list (BUG-04-145/-164/-167/-175/-181/-204/-224/-238) or S04’s already-landed fold (BUG-04-180/-183/-186/-241) or S05’s already-landed fold (BUG-04-186’s S05-half) — this is NOT a duplicate of either section’s own dispositioned bugs. Read all six before finalizing the Stage-B classifier and the Phase-6.5-6.99 fold; treat each as a kill-criterion pin folded into this section’s family matrix. Verify each repro against the new class-ledger emission and close via the bug_tracker atomic flip API citing this plan once green. Separately, triage BUG-05-018 (high, open, no plan dir, runtime-arc subsystem, ‘misaligned pointer dereference’ riding an iterator-consumer trigger) BEFORE assuming it is this section’s own RC-emission scope — its symptom and subsystem tag suggest a repr/alignment issue that may belong more naturally to a different plan (e.g. repr-opt); if triage confirms a genuine RC-emission/ownership defect in this family’s territory, fold it in and close on green same as the other six; if triage confirms a repr/alignment defect outside this family, record the explicit cross-plan rescope rather than leaving it silently unrouted through the cutover.

• Fold in the five verified-live failure-census bugs per the plan mission’s standing directive (‘Fold-in: every failing burden/RC floor cell surfacing during this plan is worked HERE’): BUG-04-160 (in-progress, medium, scaffolded plan dir — borrowed [str] collection leaks on caught-panic path; catch_recover_release.rs territory), BUG-04-161 (open, high — owned-arg-transfer into a may-unwind user-call Invoke with a live-across receiver leaks; borrowed_invoke_lineage territory per the family-expansion item), BUG-04-184 (open, high — loop-body str-literal lineage leaks per iteration; loop_carried_dead_param/ territory), BUG-04-185 (open, high — callee-returned template string leaks across catch/unwind; catch/unwind territory), and BUG-05-003 (in-progress, high, scaffolded plan dir — ori_iter_join direct string path leaks owned string elements from map/filter adapters; lazy_iter_closure_borrow/iter_consume_dead_thread territory). BUG-04-239 and BUG-05-018 are dropped from the original list as OBE-closed (verified in closed-bugs.json; BUG-05-018’s triage question is answered: routed out). None of the five appears in S09’s 8-bug folded list or S04/S05’s already-landed folds. BUG-04-160 and BUG-05-003 are in-progress with scaffolded plan dirs — check their plan dirs for a parallel session mid-fix BEFORE starting overlapping work. Read all five before finalizing the Stage-B classifier and the Phase-6.5-6.99 fold; treat each repro as a kill-criterion row of this section’s family matrix (they are the family’s real-world failure census — two catch/unwind leaks, one loop-lineage leak, one may-unwind transfer leak, one iter-adapter leak). Verify each repro against the new class-ledger emission under the gated burden-sole probe and close via the bug_tracker atomic flip API citing this plan once green.
• Fold borrowed_invoke_lineage (borrowed_invoke_lineage.rs + its borrowed_invoke_lineage/{roots,vet,death_point}.rs submodules; base release treatment ORI_DISABLE_BORROWED_INVOKE_LINEAGE_RELEASE plus loop-exit variant ORI_DISABLE_LOOP_BORROWED_LINEAGE_EXIT_RELEASE plus ORI_DISABLE_BUILTIN_INVOKE_RESULT_LINEAGE) into this section’s cut family alongside iter_consume_dead_thread/, lazy_iter_closure_borrow/, catch_recover_release.rs, loop_carried_dead_param/, cow_terminal_concat.rs, and the ttr-iter-consume overlap arms, replaced by the same contract-derived ledger events. Membership grounding: no other section in this plan claims it; it is thematically this section’s exact territory (borrowed-collection release across a may-unwind Invoke with a dedicated loop-exit variant — borrowed-collection + may-unwind + loop-carried at once); MISSING_ABSTRACTION confirms its internal shape mirrors loop_carried_dead_param/ at 0.929 similarity, and its borrow-only-vetting predicate is a fourth independent re-derivation of the primitive already duplicated across catch_recover_release.rs (this section) and live_extract.rs (S05, x2) — Stage-B event classification subsumes all four. Coverage status is RESOLVED at HEAD: a dedicated 1510-line tests.rs with 35 #[test] fns exists (verified by direct grep) — NO walking-skeleton pins are needed for this member; instead use its 35-test suite (may-unwind Invoke, loop-exit release, builtin-result-root shapes) as the pin templates for the untested trio’s walking-skeleton work item.
• Retire each cut scan with an explicit, census-gated disposition mirroring S05’s w-9d2bed53 — never a silent reinterpretation and never an unconditional same-commit deletion. Per scan module: (1) deletion is permitted ONLY when diagnostics/class-ledger-diff.sh shows zero fallback functions whose shapes exercise that scan AND the family matrix + walking-skeleton pins are green under the NEW mechanism (deleting earlier removes the ORI_DISABLE_* bisection fallback and breaks live fallback functions — the readiness gate falls back to the LEGACY walk by design); (2) when deletion lands, delete the scan module + its ORI_DISABLE_* toggle(s) in the SAME commit as recording its KEPT ledger cycle with before/after teeth (collapse metric + floor), sweeping every toggle doc home (oric/src/debug_flags.rs registration + arc.md Debugging entry; check-flag-docs.sh is the consistency gate); (3) a scan whose fallback census cannot reach zero within S06 records an explicit deferral to S08’s sole-emitter flip in the section body/HISTORY — replacement coverage + KEPT teeth are then S06’s deliverable for that scan, with file deletion recorded as S08’s. In the same doc-cure pass, fix arc.md’s verified drift: correct the two stale loop_closure_dead_param.rs path citations (arc.md:391-392; unified into loop_carried_dead_param/ at 3dee4f95d) and add the three source-live family toggles absent from arc.md (ORI_DISABLE_COW_TERMINAL_CONCAT_INC_ELISION, ORI_DISABLE_ITER_CONSUME_FOR_YIELD_TAKE_ROOT, ORI_DISABLE_ITER_CONSUME_FRESH_INVOKE_RESULT_ROOT — all three registered in debug_flags.rs; drift is arc.md-side only), coordinating with in-progress S10 (toggle-consolidation-doc-sync) before touching debug_flags.rs/arc.md. Complete the family matrix (iterators x lazy closures x catch/unwind x loop-carried threads x for-yield). The deletion-vs-coverage decision per scan is recorded, not implied.
• Author and green walking-skeleton-shaped semantic pins pinning the CURRENT behavior of exactly the untested trio FIRST: catch_recover_release.rs (673 lines, the single largest family file with the richest internal call graph), cow_terminal_concat.rs (123 lines), and loop_carried_dead_param/{mod,vetting}.rs (592 lines, the shared skeleton backing TWO production RL-5 releases) — re-verified by direct grep at HEAD that all three carry ZERO tests anywhere today (own file, the shared ownership_scans/tests.rs, and lower/burden_lower/tests.rs), unlike iter_consume_dead_thread/tests.rs (8 tests), lazy_iter_closure_borrow/tests.rs (4 tests), and borrowed_invoke_lineage/tests.rs (35 tests — now COVERED; do NOT author skeleton pins for it; use its may-unwind Invoke / loop-exit release / builtin-result-root test shapes as the trio’s pin templates). The trio is also the unchurned part of the family — nothing pins OR exercises these files, so cutting them over before pins removes the only bisection fallback (the ORI_DISABLE_* toggle A/B) a cutover this size has, the same sequencing defect S04’s (w-6c58d672) and S05’s (w-5da6d021) own reviews already corrected. Only once these pins and the family matrix rows are green does any cutover or retirement of the trio proceed; scan/toggle deletion sequencing and KEPT-cycle recording are owned by the census-gated retirement work item, not here.
• Run the class-ledger differential census FIRST and make the TRMC architectural decision against it before any Rust: (1) re-run compiler_repo/diagnostics/class-ledger-diff.sh at current HEAD (freshest verified report 2026-07-07T18:12Z: 597 functions replaced / 209 fallback / 0 divergent / 14 toggled_fixes_legacy; fallback ranking zero-classes 171 > trmc-context 23 > field-view-liveness 11 > field-decomposition-shape 3 > readiness-not-clean 1) and derive this section’s cutover worklist from the fallback populations — the 23 trmc-context hard-declines (FallbackReason::TrmcContext fires on ANY ContextHole variable) plus the zero-classes functions exercising the protocol/loop family shapes; per-function attribution via ORI_LOG=ori_arc::aims::class_ledger=debug (mode + fallback_reason). (2) Decide extend-vs-decline for TRMC: either the class ledger gains ContextHole-region support — which per CP-1 calculus-first requires naming (or proving in scratch Lean first, then landing) the governing compiled-Lean theorem for the ContextHole consume/credit shape BEFORE implementing (T2’s CFG-walk model covers back-edges; the ContextHole shape needs an explicit theorem check) — OR the TrmcContext decline-and-fallback is explicitly kept for S06 with the decision recorded in the section body; never an unproven ledger extension. (3) Ground the Stage-B classifier in the pinned surfaces verified in source: aims/intraprocedural/ledger_events/types.rs 12-kind TerminalUse grid (9 transfer + 3 non-transfer read kinds, the test-pinned mirror of AimsProof.Realization::TerminalUse) and class_ledger/events.rs EventKind (Birth/Credit/Consume/Read/Mutate/SelectCredit) — the class-ledger emitter derives its own deltas in class_ledger::events, never through the mirror table, and never from arc.md prose (independently verified stale for this family).

Fresh intel (regenerated)

S06 is no longer “the third cutover, shaped like S04/S05” — it is the FIRST cutover to execute against a completed-precedent record, and that record REWRITES two of the section’s own work items:

1. S04 and S05 both closed with ZERO scan-file deletions. All 13 S05-family files and all 8 S04-family files still exist on disk and are still dispatcher-wired. The landed cutover model is: replacement COVERAGE (class-ledger readiness gate per function) + differential-harness zero-divergence + KEPT ledger teeth, with file deletion explicitly deferred to a fallback-census-zero gate or S08’s sole-emitter flip (S05 recorded this re-scoping in w-9d2bed53). [JOIN] S06’s w-7340b349 (“Delete retired scans + toggles same-commit”) inherits the SAME re-scoping obligation — a scan is deletable only when diagnostics/class-ledger-diff.sh shows zero fallback functions exercising its shape; otherwise the S06 deliverable is replacement coverage + teeth, deletion recorded as S08’s.
2. The emitter S06 cuts onto is LIVE and measured. Freshest differential report (build/class-ledger-diff.json, 2026-07-07T18:12Z, 242 programs): 597 functions REPLACED, 209 fallback, 0 divergent, 14 cells where the class ledger FIXES legacy. Fallback ranking: zero-classes 171 > trmc-context 23 > field-view-liveness 11 > field-decomposition-shape 3 > readiness-not-clean 1. The #1 non-trivial blocker is now TRMC-context — FallbackReason::TrmcContext hard-declines EVERY function carrying a ContextHole variable, and S06’s explicit gate (TRMC probe cells: context-hole threading + KEPT-230 back-edge result-dec stay green) sits exactly on that decline set. S06’s loop-family cutover work begins INSIDE the trmc-context + zero-classes fallback populations, not on a blank slate.
3. The prior dossier’s #1 ambiguity is DISCHARGED in source. The “nine transfer kinds vs twelve terminal-use kinds” tension is resolved at aims/intraprocedural/ledger_events/types.rs:26-46: TerminalUse is a 12-kind partition = 9 transfer (CONSUME) + 3 non-transfer (terminal READ: LastReadBeforeScopeExit, ScopeExit, ApplyToBorrowedParam), doc-commented as the test-pinned mirror of the compiled AimsProof.Realization::TerminalUse grid (terminal_use_table_matches_committed_rl2_grid). Ground the Stage-B classifier THERE, not in arc.md prose.
4. The zero-coverage trio persists; the fourth family member’s coverage question is answered. Direct grep at HEAD: catch_recover_release.rs (673 lines, shrunk from 900+ since 07-02), cow_terminal_concat.rs (123), and loop_carried_dead_param/{mod,vetting}.rs (592) still carry ZERO tests anywhere (own file, ownership_scans/tests.rs, burden_lower/tests.rs — all zero mentions). By contrast borrowed_invoke_lineage/ NOW has a dedicated 1510-line tests.rs with 35 #[test] fns (it did not at section authoring; w-0fdebaac’s “coverage NOT confirmed — verify explicitly” is answered: COVERED), joining iter_consume_dead_thread/tests.rs (8) and lazy_iter_closure_borrow/tests.rs (4). w-e2620501’s walking-skeleton-pins-BEFORE-deletion discipline now binds exactly and only the trio.
5. The bug fold-in list SHRANK from 7 to 5 live. BUG-04-239 (generic Set<T> .iter() double-free) and BUG-05-018 (iterator-consumer misalignment) are now OBE-closed. Live: BUG-04-160 (in-progress, medium — catch’d-panic borrowed-collection leak), BUG-04-161 / BUG-04-184 / BUG-04-185 (open, high), BUG-05-003 (in-progress, high). bugs-for aims-provenance-ledger still returns ZERO — none of the five is routed to this plan; the third-consecutive-dossier routing gap persists at smaller size.
6. arc.md toggle-doc drift WORSENED. The two stale loop_closure_dead_param.rs path citations survive (arc.md:391-392; the file was unified into loop_carried_dead_param/ at 3dee4f95d), and THREE source-live family toggles are now absent from arc.md entirely: ORI_DISABLE_COW_TERMINAL_CONCAT_INC_ELISION plus two NEW iter_consume_dead_thread root-family toggles (ORI_DISABLE_ITER_CONSUME_FOR_YIELD_TAKE_ROOT, ORI_DISABLE_ITER_CONSUME_FRESH_INVOKE_RESULT_ROOT) — all three ARE registered in oric/src/debug_flags.rs, so the drift is arc.md-side only. S10 (toggle-consolidation-doc-sync) is in-progress in parallel: coordinate before touching debug_flags.rs/arc.md.

Decisions this package forces before any Rust is written:

1. Record the deletion-vs-coverage re-scoping decision for w-7340b349 UP FRONT, mirroring S05’s w-9d2bed53: per scan, deletion gated on class-ledger-diff fallback census zero for its shapes + matrix green, else explicit S08 deferral (§6).
2. Pull the CURRENT per-function fallback census (diagnostics/class-ledger-diff.sh; ORI_LOG=ori_arc::aims::class_ledger=debug for per-function mode/fallback_reason) and treat the 23 trmc-context + relevant zero-classes functions as the cutover worklist — the leverage is extending events//emit//verify.rs (and deciding whether TrmcContext stays a hard decline or gains ledger support) BEFORE touching the six old scans (§3D).
3. Author the walking-skeleton pins for the untested trio FIRST (catch_recover_release.rs, cow_terminal_concat.rs, loop_carried_dead_param/) — unchanged from the section body, re-verified zero-covered at HEAD (§3.6).
4. Ground the Stage-B classifier in ledger_events/types.rs’s pinned 12-kind grid + class_ledger/events.rs’s 6-kind EventKind (Birth/Credit/Consume/Read/Mutate/SelectCredit); the class-ledger emitter derives its own deltas in class_ledger::events, NEVER through the mirror table (the doc-comment says so explicitly) (§2).
5. Re-read the FIVE live fold-in bugs (04-160, 04-161, 04-184, 04-185, 05-003) before finalizing the classifier; drop 04-239/05-018 from the section’s w-c3132d6b list as OBE-verified (§4).
6. Fix arc.md’s 2 stale paths + 3 missing toggle entries in the SAME commit as any toggle retirement, coordinating with in-progress S10 (§3D, §6).
7. The carried dead-ends bind unchanged — never broaden compute_genuine_same_alloc_reps / ForwarderUnionFind / ssa_alias_classes::UnionFind; never re-derive the rejected per-field designs (§Constrained symbols).

DIG DEEPER

python -m scripts.plan_corpus.read plans/aims-provenance-ledger
python3 -c "import json; print(json.load(open('compiler_repo/build/class-ledger-diff.json'))['summary'])"
sed -n '26,78p' compiler_repo/compiler/ori_arc/src/aims/intraprocedural/ledger_events/types.rs

(full dossier: cutover-protocol-loop—s-d0d5b08a.intel.md)

TRMC architectural decision (w-51795e5c) - DECLINE for S06; theorem-first extension anchored at S08 w-d450dfd4

• Census at HEAD 8d5239a6b (diagnostics/class-ledger-diff.sh, tests/ corpus, 226 programs, build/class-ledger-diff-full.json 2026-07-07T20:13Z): 597 functions replaced / 209 fallback / 0 semantic divergences / 14 toggled_fixes_legacy. Ranking: zero-classes 171 > trmc-context 23 > field-view-liveness 14 > readiness-not-clean 1. The single “divergent” row (benchmarks/aims_burden/doors_toggle.ori) re-probed identical at —timeout 180 (the LEGACY leg alone exceeded the 30s default; ledger leg finished) - a timing artifact, not a divergence.
• DECISION: FallbackReason::TrmcContext stays the hard decline through S06. Grounds:
  • CP-1: the T2 CFG model (AimsProof/Ledger.lean) covers TRMC-marked back-edge regions (trmcBlocks; K2 proves the walk for every iteration count and rejects a release placed after the tail-call transfer), but its LedgerInstr alphabet (construct / dup / projRead / cowMutate / escapeUse / jumpArg / burdenDec) has NO hole-fill instruction kind - the ContextHole fill-at-recursive-call consume/credit obligation (replace.rs TrmcContext arm doc) is unmodeled. Ledger support is a genuine calculus extension (new event kind + credit semantics + kill criteria) proven BEFORE Rust; an unproven extension is banned (EVIDENCE:calculus-first-violation).
  • Leverage: zero-classes (171) dominates trmc-context (23) 7.4x; S06’s cutover worklist lives in the zero-classes protocol/loop population (12 family-shape programs, 32 functions: cow_iterator_collect 10, tail_call_test 8, closure_capture 3, try-tailless-empty 2, f04_closure_capture 2, + 7 single-function programs).
  • Safety: the 23 trmc-context declines (8 programs: aims_h_trmc 7, aims_h_fip_reuse 6, aims_fip_interprocedural 3, aims_drop_reuse 2, trmc_list_map 2, recursive_tree 1, tail_call_test 1, trmc_chain_lifecycle 1) fall back to the legacy burden walk unchanged - 0 semantic divergences corpus-wide, so w-b33bab90’s TRMC gate (context-hole threading + KEPT-230 back-edge result-dec probe cells stay green) holds by construction through S06.
• Deferral anchor: ContextHole ledger support is mission-required (the north-star gate deletes ownership_scans/, and trmc-context fallbacks route through the legacy Phase-5 walk) - anchored as S08 work item w-d450dfd4 (theorem-first sequencing, before the sole-emitter flip completes).
• Stage-B grounding verified in source: ledger_events/types.rs:26-39 TerminalUse 12-kind grid (9 transfer + 3 terminal-read; test-pinned mirror of AimsProof.Realization::TerminalUse via terminal_use_table_matches_committed_rl2_grid) + class_ledger/events.rs:25-34 EventKind (Birth / Credit / Consume / Read / Mutate / SelectCredit); the emitter derives its deltas in class_ledger::events, never through the mirror table.

Bug fold-in census (w-f01ee5f7) - five live bugs verified against class-ledger emission at HEAD 8d5239a6b

Per-repro kill-criterion matrix. legacy = gated burden-sole probe (ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1); ledger = same + ORI_CLASS_LEDGER_EMITTER=1; ORI_CHECK_LEAKS=1 runs, debug-compiler direct builds (release cargo cells re-confirm the two closures):

Kill-criterion rows for the family cut (w-34a8f486) - empirical ledger-leg regressions the cut MUST fix, both with all-classes-clean readiness (the gate reads clean on unmodeled family shapes - fail-closed hole):

• CATCH/UNWIND COEXISTENCE (b160 shape): main + partial_iter REPLACED all-clean, panicking_func fallback (readiness-not-clean); caught-panic path leaks 4. The borrowed-collection unwind release arrangement (catch_recover_release territory) is unmodeled in Stage-B events while verify reads Clean.
• LAZY-ITER CLOSURE RETENTION (b003 shape): main + __lambda_main_0 BOTH replaced all-clean; ledger leg leaks 3 vs legacy 1 (+2 emission-side). The lazy-iterator adapter retains the closure env as a borrowed raw pointer across the chain (lazy_iter_closure_borrow territory) - a retention/credit fact invisible to the per-class walk.
• CENSUS BLIND SPOT: the aot fixtures corpus (compiler/ori_llvm/tests/aot/fixtures/) is NOT in the tests/ census sweep - the b160 exit-0-vs-exit-2 divergence never surfaces in class-ledger-diff.sh. The w-34a8f486 differential gate MUST also sweep the fixtures corpus (or the family-shape subset of it).

Parallel-session check: no mtime activity since 2026-07-06 in either scaffolded dir (BUG-04-160, BUG-05-003) before this fold-in; BUG-04-160’s dir archived to completed/ by the close.

Family-cut progress (w-34a8f486) - both kill-criterion rows cured at 98eba601e

• CURE 1 (concat-operand split): the Stage-B classifier modeled EVERY heap PrimOp concat operand as CONSUME; ori_str_concat BORROWS (fresh result, caller-side dec is the operand’s release) while ori_list_concat_cow is dual-consuming. Split by repr mirroring the legacy discriminator: RcPointer consumes, FatValue reads. Cured the lazy-iter lambda +2 (b003 toggled leg 3->1, legacy-identical; residual = the ori_rt BUG-05-003 runtime bug, out of emission reach).
• CURE 2 (iter-consume param origin): a BORROWED param whose own contract is iter-consuming births FOREIGN (PV-4: the caller’s ApplyToIterConsumingParam transfer hands the reference in) instead of Borrowed-origin self-funding - the double-funding leaked the caller’s transferred whole-collection reference. Cured b160 (toggled leg 4->0 leaks).
• Both cures are event-classification corrections within the proven alphabet (PrimOp operands are not call boundaries or 12-kind terminal uses; PV-4 already assigns the transferred reference callee-side) - no new theorem per CP-1 case (a). Fail-first pins: str_concat_operand_reads_not_consumes, list_concat_operand_consumes, borrowed_iter_consuming_param_births_foreign, heap-primop pin re-scoped to RcPointer. ori_arc lib 2050 green, clippy clean, aot ledger_green 2/2. Ledger cycle attempt 6 (KEPT, BETTER).
• Remaining for this item: valid full-census re-verification (two sweep runs invalidated by parallel binary churn mid-run), fixtures-corpus differential coverage (the census blind spot recorded in the fold-in block), and the leak-dimension gap: class-ledger-diff.sh compares exit/stdout only - leaks are invisible to it; the item’s completion evidence must include leak-checked family probes (done for the four fold-in repros) and SHOULD extend the harness with an ORI_CHECK_LEAKS leg.
• CURE 3 (indirect-arg fail-closed gate): the fixtures-corpus differential sweep (495 programs - the census blind spot, now covered) surfaced 2 REAL divergences: curried-closure captures (arc_curried_closure_capture_{list,nested}.ori) DOUBLE-FREED under the ledger. Root: call-site arg_ownership is populated during realization, AFTER Stage-B classifies, and an indirect callee is unresolved - the blanket READ guess plans a release for a reference a consuming callee’s capture already owns. Cure: a non-excluded heap arg through ApplyIndirect/InvokeIndirect poisons the classification (indirect_arg_handoff) and the readiness gate declines with the new FallbackReason::IndirectArgOwnership - fail-closed fallback, never a guess in either direction (READ double-frees a consumer; CONSUME leaks a borrower). Closure-receiver-only indirect calls (the lambda invocation shape) stay replaceable. Pins: indirect_heap_arg_sets_handoff_flag + indirect_receiver_only_does_not_set_handoff_flag (fail-first); both divergent cells now exit 0; repro matrix intact; lib 2052 green.
• HARNESS LEAK LEG (tooling): class-ledger-diff.sh gains —leaks - both legs run under ORI_CHECK_LEAKS=1 so leak counts land in the compared output and a leg-vs-leg leak difference reports as a divergence (leaks were invisible to the exit/stdout comparison; the b003 +2 and b160 +4 regressions were census-invisible pre-cure). Verified: b003 reads identical under —leaks (both legs leak the runtime residual equally); b184 reads toggled-fixes-legacy (ledger clean, legacy leaks 3).
• COMPLETION EVIDENCE (w-34a8f486, HEAD c394d6d3f): leak-legged main census (tests/, 226 programs, —leaks): ZERO ledger regressions - 30 toggled-fixes-legacy (the leak leg reveals 16 more cells the ledger fixes beyond the 14 exit-visible ones), 2 leak-count differences BOTH ledger-better (recursive_tree 36->20, trmc_tree_ops 61->30; TRMC-territory partial-replacement mixes), 1 benchmark timeout artifact (doors_toggle, proven identical at —timeout 180). Fixtures census (495 programs): 0 divergent. Family per-shape probes: all six members ledger-correct; ttr-overlap and template-loop shapes FIX legacy outright. Fallback ranking at HEAD: zero-classes 171 > trmc-context 23 (S08 w-d450dfd4) > field-view-liveness 14 > indirect-arg-ownership 14 (fail-closed by design) > readiness-not-clean 2. Scan retirement dispositions stay with w-37af1b54; explicit gates with w-b33bab90.

Phase 6.5-6.99 fold inventory (w-bf88b828) - subsumption-by-replacement; deletion anchored at S08 w-6589cdda

The 26 tail passes (all 27 markers at HEAD minus 6.99) are LEGACY-walk repairs operating on the legacy Phase-5 walk’s burden ops. A ledger-REPLACED function bypasses the ENTIRE Phase-6 repair pipeline (the plan is applied instead) - the fold into the emitter core is subsumption-by-replacement, verified per-shape by the paired census (fixtures 495 programs 0 divergent; leak-legged main census 0 ledger regressions, 30 toggled-fixes-legacy). Hydra mapping (each pass -> the general ledger-core rule that subsumes it):

Deletion disposition (per the S05 w-9d2bed53 re-scoping precedent): the passes stay LOAD-BEARING for the 224 fallback functions routing the legacy walk; deleting any of them today regresses live fallback cells. Deletion lands with the legacy-walk retirement at fallback-census-zero - anchored as S08 w-6589cdda (explicit: the passes die with the walk they repair; 6.99 survives). No pass is deleted in this section.

Explicit gates (w-b33bab90) - all three green at HEAD

• GATE 1 (ApplyToIterConsumingParam classifies CONSUME, never BIRTH): unit-pinned on BOTH boundary sides - caller: iter_consume_fact_overrides_borrowed_to_consume (the arg’s derived ledger is exactly [Birth(own construct), Consume(call)] - an extra site-birth would break the exact-match); callee: borrowed_iter_consuming_param_births_foreign + borrowed_non_iter_consuming_param_stays_borrowed (the transferred reference arrives owned; plain borrows stay borrowed-origin).
• GATE 2 (closure-env release dominates captured-payload release): skeleton_closure_env_release_dominates_capture_ledger_green (class_ledger_skeleton.rs) - closure captures a heap payload, invoked twice, dead; the helper asserts ledger-toggled exit 0 + leak-free + interpreter parity. Legacy leaks the env allocation (BUG-04-254 territory; the cell pins the ledger-side dominance, the legacy face stays with that bug’s cutover cure anchor). A raw valgrind matrix cell was NOT added (it would red test-all’s default-path leg on the tracked legacy defect).
• GATE 3 (TRMC probe cells green): all 25 aot trmc cells (context-hole threading: list_map/tree_mirror/multi_field_ctor/enum_with_tag_change/deep_recursion…; back-edge result-dec: trmc_rc_balance et al.) pass under the gated burden-sole probe on BOTH legs (with the ledger toggle, the TrmcContext decline keeps them on the legacy walk - green by construction through the cutover; census confirms the trmc programs identical, with the two leak-count differences both ledger-better).

Census-gated retirement dispositions (w-37af1b54) - all six scans: explicit S08 deferral

Per-scan disposition at HEAD (census: 226-program main + 495-program fixtures; fallback populations non-zero in every family territory - readiness-not-clean in catch territory, zero-classes across corpora, indirect-arg-ownership fail-closed set):

• No scan module or toggle is deleted in this section (deleting while any fallback function exercises the shape breaks live fallback emission - the readiness gate falls back to the LEGACY walk by design). Every scan’s walking-skeleton/dedicated pins are green (100/100 ownership_scans suite) and the replacement mechanism is census-verified; deletion + toggle sweep + KEPT-cycle-per-scan land with the S08 legacy-walk retirement (anchors: w-e3f5a409 + w-6589cdda; scan-module deletion is part of the legacy Phase-5 walk retirement the sole-emitter flip performs).
• arc.md doc drift CURED in this pass (S10 coordination: arc.md clean in the parallel session’s working set at edit time): the two stale loop_closure_dead_param.rs path citations now point at loop_carried_dead_param/mod.rs, and the three source-live family toggles absent from arc.md are documented (ORI_DISABLE_COW_TERMINAL_CONCAT_INC_ELISION, ORI_DISABLE_ITER_CONSUME_FOR_YIELD_TAKE_ROOT, ORI_DISABLE_ITER_CONSUME_FRESH_INVOKE_RESULT_ROOT). check-debug-flags.sh: 111 flags, 0 stale, 0 orphan.

Family matrix (iterators x lazy closures x catch/unwind x loop-carried x for-yield), gated burden-sole probe, ORI_CHECK_LEAKS=1, both legs:

Section gate state (w-f8519c69) - all three blocker bugs RESOLVED; gate legs re-verifying at HEAD a16be6e1e

The gated floor at c11ac53e6 reads 14 failing = 11 baseline + 3 NEW (guardrail-2 regression): drop_augment::drop_map_key_panic_two_channel_cleanup_frees_values (default-path AND gated; the recoverable @drop-panic teardown not engaging) = BUG-04-258; mono_cross_facet::test_import_x_complex_generic_cast (exit -1) = BUG-04-259; predicate_stack_probe::probe_generic_set_str_param_named_iter_count_no_double_free (exit -134) = BUG-04-260. All three deterministic in isolation; the 334f7d930 sweep-restore experiment refuted the swept-refactor hypothesis; historical window snapshots are churn-contaminated (attribution by fixing, never archaeology). 259/260 appear in the section pre-work baseline failure list; 258 does not. The gate item completes only when the gated probe reads zero-new — the three bugs are fix_now work in this loop per the mission’s standing fold-in directive. test-all at c11ac53e6: coexistence-surface red as expected (arc.md STOP); the gated probe is the verdict surface.

Gate re-verification (2026-07-09, HEAD a16be6e1e)

• BUG-04-258 (drop_augment two-channel teardown), BUG-04-259 (complex generic cast exit -1), and BUG-04-260 (Set named-iter-count double-free) are ALL resolved in closed-bugs.json; 259+260 fixed via full /fix-bug cycles this loop (260: __collect_set fresh-lineage-root admission + RL-2 CONSUME tightening; commits 9fbef3c5b/308ee1554/94bf4e71f + hygiene a16be6e1e).
• RELEASE gated leg: 11 failed = EXACT baseline_failing_ids.txt match (zero new), verified post-fix, post-TPR-cures, and post-hygiene.
• Remaining legs in flight: DEBUG gated leg (aot-guardrail —floor) + full ./test-all.sh at HEAD (background, flock-serialized) + per-node parity/leak engine-read.