63%

S08 Predicate-stack deletion - compiled-counter adapter cutover

Goal

With the gated floor at ZERO (entry gate), the predicate-stack counter-emission system is deleted whole; the class ledger becomes the sole logical event-placement authority and sole input to the current compiled-counter adapter; the default build IS the former gated build. This cutover does not make that adapter AIMS’s sole physical realization.

Entry gate - ABSOLUTE

aot-guardrail.sh --floor under the gated env reads 0 failing (debug AND release) BEFORE any deletion lands. ADR decisions/01-cutover-ordering.md records deletion-after-cutovers (locked per three-reviewer consensus; arc.md STOP + attempt-287 as evidence).

Deletion inventory (verified surfaces)

aims/realize/walk.rs + walk_dec.rs predicate emitters; decide.rs Phase-1 surface; cleanup_redundant.rs; populate_class_covered + class_payload_of residue (relocate the load-bearing ensure_singleton_class materialization FIRST per the superseded plan’s w-8044d21f Option-2 grounded design - ledger attempt 281’s coupling lesson); ssa_alias_classes predicate integrations; predicate_stack_rc_disabled flag + ORI_DISABLE_PREDICATE_STACK_RC env var; predicate_stack_probe test artifacts; aims_snapshots re-blessed to ledger output.

Work Items

  • Extend the class ledger to TRMC ContextHole regions THEOREM-FIRST per arc.md CP-1, then lift FallbackReason::TrmcContext: the T2 model (AimsProof/Ledger.lean) proves the TRMC-marked back-edge region walk (trmcBlocks; K2 kill criterion) but its LedgerInstr alphabet carries NO hole-fill instruction kind - the ContextHole fill-at-recursive-call consume/credit obligation is unmodeled (class_ledger/replace.rs TrmcContext doc). Sequence: (1) scratch-Lean prove the hole-fill event shape (new LedgerInstr kind + credit semantics + a release-after-fill kill criterion), (2) land the additive theorem four-surface-synced per CP-2, (3) implement Stage-B/C support, (4) verify the trmc-context fallback census reads ZERO (diagnostics/class-ledger-diff.sh; 23 functions across 8 programs at the S06 w-51795e5c census) - prerequisite of the single-logical-planner/current-compiled-adapter end state (ownership_scans/ deletion requires zero legacy-walk fallback populations).
  • ENTRY GATE (verified FIRST, recorded in the section body): gated burden-sole probe floor == 0 across the full AOT corpus (debug AND release) - all families cut over; author ADR decisions/01-cutover-ordering.md locking deletion-after-cutovers (arc.md PREDICATE STACK IS LEGACY + attempt-287 lesson as tradeoff evidence)
  • Re-derive the deletion inventory via grep against HEAD as this item’s FIRST step — never trust a frozen file list. aims/realize/walk.rs, walk_dec.rs, dead_cleanup.rs no longer exist (consolidated into aims/realize/emit_unified.rs); populate_class_covered/class_payload_of are not literal identifiers anywhere in compiler_repo — prose shorthand only, zero grep hits. The verified live deletion surface: (1) THE 7-SITE COLLAPSE — grep -rn predicate_stack_rc_disabled compiler/ori_arc/src/lower/burden_lower/*.rs locates the 7 conditional branches across 3 files in the Phase-5 burden-lowering module (as of HEAD: emit.rs x5, cow_aliases.rs x1, scan_orchestration.rs x1) plus 2 pass-through param-threading sites and 3 field declarations. Collapse each site to its predicate_stack_rc_disabled == true (probe) arm becoming unconditional, delete the else/default arm, one file at a time (cow_aliases.rs -> scan_orchestration.rs -> emit.rs), running the ori-rc-remarks --diff two-build comparison (ori build <fixture>.ori --emit-rc-remarks pre.jsonl before, post.jsonl after each file, then cargo run --manifest-path compiler_repo/tools/ori-rc-remarks/Cargo.toml -- --diff pre.jsonl post.jsonl) after EACH file per CLAUDE.md narrow-the-front — a non-empty diff after a collapse is a correctness bug in the collapse, not a floor regression; do not proceed to the next file until it is empty. Delete the predicate_stack_rc_disabled field + ORI_DISABLE_PREDICATE_STACK_RC env-var read only AFTER all 7 sites collapse. (2) THE decide.rs DEAD-CODE ISLAND — delete decide(), decide_last_use(), decide_reuse() + their supporting types (DecisionContext/DecisionSite/InstructionDecisions/RcDecision/ReuseContext/ReuseDecision/UseSemantics) — confirmed 0 production callers — together with ALL their direct tests (grep-count at execution time; as of HEAD: 27 in aims/realize/tests.rs + 2 in aims/realize/burden_elim/tests.rs, 29 total) in the SAME change — never leave a test dangling against a removed function. PRESERVE-LIST (SAME FILE, DO NOT TOUCH): decide_annotations(), decide_cow(), decide_drop_hint(), AnnotationSiteContext — LIVE, called unconditionally from annotate_block (aims/realize/mod.rs:277) inside Phase-2 realize_annotations() on every function, every build; deleting decide.rs wholesale breaks COW-mode and drop-hint decisions crate-wide. ALSO PRESERVE (shared substrate, NOT predicate-stack-specific, confirmed by source grep + similar embedding to be structurally isolated from anything deletable): ssa_alias_classes/compute_ssa_alias_classes (aims/intraprocedural/ssa_alias_classes.rs) and ensure_singleton_class/materialize_payload_edge_classes (aims/intraprocedural/post_convergence.rs) — both LIVE, unconditional, single production callers feeding the surviving burden path’s same-alloc-rep machinery; there is no separate ‘predicate integration’ inside them to remove. Verify at execution time whether ensure_singleton_class’s relocation (the superseded plan’s w-8044d21f Option-2 design, ledger attempt-281’s coupling lesson) is already satisfied by this plan’s own earlier DAG-ordered sections (S02 partition-infrastructure, S07 phase6-class-grain-elision both precede S08) before treating it as open work here — do not re-do work an earlier section already did. (3) GATED SUB-DECISION — cleanup_redundant_project_alias_decs (aims/realize/cleanup_redundant.rs:71, called unconditionally from pipeline/aims_pipeline/mod.rs:414): do NOT bundle its fate into this same commit set. Its own module doc cites 4 producers, 2 of which (walk_dec::emit_post_instr_decs_unified, dead_cleanup::emit_dead_at_entry_decs) no longer exist as modules (a stale doc comment, drifted from the same consolidation that erased walk.rs) — whether it is still load-bearing post-collapse is UNRESOLVED by static reading. Empirically resolve it via ORI_DISABLE_REDUNDANT_CLEANUP=1 vs unset under the gated burden-sole probe (ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1) per arc.md §Debugging bisection, AFTER the 7-site collapse lands — only then decide deletable / reduced / already-vestigial (LLVM legacy-PM-deprecation precedent: scope removal to what is proven ready, gate the unready sub-surface separately). (4) REPR-OPT COORDINATION — before landing ANY edit to aims/realize/emit_unified.rs, run scripts/intel-query.sh plan-status repr-opt --human and confirm repr-opt#section-07-enum-repr’s (Enum Representation Optimization) current state; confirmed as of HEAD it is in-progress with 76 unchecked items and edits touching emit_unified.rs directly (threads take_move_facts through emit_block_rc/BlockCtx) — per CLAUDE.md §Stabilization ‘plan boundaries = impl boundaries’, coordinate with that section’s owner rather than silently absorbing or colliding with its in-flight changes. Only once (1)+(2)+(3) collapse cleanly does ‘the ledger is the sole unconditional RC emitter’ become true for the Phase-5 emission surface.
  • Delete the legacy burden Phase-5 walk’s emit_unified.rs Phase 6.5-6.98 repair passes together with the walk they repair, once the fallback census reads ZERO (every function ledger-replaced; the passes operate on legacy-walk burden ops and are dead code the moment no function routes legacy). Phase 6.99 (transfer_anchor_net) survives as the general net engine per the S06 goal. The Hydra subsumption inventory mapping each pass to its ledger-core leg (edge-cleanup family -> RL-4 planner releases; 6.66x iter family -> Stage-B contract events; dead-value family -> births-only planner releases; 6.96/6.97 strips -> unneeded, the ledger never emits the spurious ops; 6.98 -> uniform unwind edges) is recorded in the S06 body (w-bf88b828); the paired census (fixtures 495 programs 0 divergent + leak-legged main census 0 ledger regressions) is the subsumption verifier.
  • Re-bless aims_snapshots baselines to ledger output (ORI_BLESS=1, verifying RC balance per snapshot). For compiler/ori_llvm/tests/aot/predicate_stack_probe.rs: do NOT blanket-delete on the claim ‘(they assert the deleted path)’ — verified false for the bulk of the file. Grep-verify the exact test population at execution time (grep -c '^#\[test\]' compiler/ori_llvm/tests/aot/predicate_stack_probe.rs; grep -c 'assert_burden_path_self_sufficient(' <same file>; grep -c 'assert_default_path_leak_free(' <same file>) — as of HEAD: 212 of 231 #[test] fns call assert_burden_path_self_sufficient (compiles WITH the probe flag set, i.e. burden-ALONE) — these assert the SURVIVING path’s own correctness across the historically highest-churn shapes (move-alias chain, dup-alias-live-source, collection-buffer last-use list/map/set, borrow-chain project-of-projection, closure-capture last-use — the exact shapes the BUG-04-132/133/134/135/136/137/142/157 bring-up sequence fixed). Once the 7-site flag/branch collapse lands (this section’s own deletion work item), these become unconditional regression pins with only their build-env boilerplate simplified (no flag left to set) — RETAIN them, do not delete. Only the 5 probe_default_path_unaffected_{str,list_int,map_str_int,set_int,closure_env} tests (calling assert_default_path_leak_free, compiled WITHOUT the flag) specifically pin a comparison axis — is the predicate-stack-as-default path unperturbed by burden-bring-up plumbing — that becomes vacuous once there is only one path; fold their underlying leak-free program shapes (str round-trip, list_int, map_str_int, set_int, closure_env) into the now-unconditional regression suite (dropping the ‘default_path_unaffected’ framing/naming — there is no second path left to compare against) rather than deleting them outright, so that basic-shape coverage is not silently lost. Counts here are as of the current HEAD and will drift — re-derive by grep, never assume.
  • Delete the predicate stack: aims/realize/walk.rs + walk_dec.rs emitters, decide.rs Phase-1 surface, cleanup_redundant.rs, populate_class_covered + class_payload_of residue (relocating the load-bearing ensure_singleton_class materialization first per the superseded plan’s w-8044d21f Option-2 design), ssa_alias_classes predicate integrations, the predicate_stack_rc_disabled flag + ORI_DISABLE_PREDICATE_STACK_RC env var; the ledger is the sole logical event-placement authority and sole input to the current compiled-counter adapter
  • Re-bless aims_snapshots baselines to ledger output (ORI_BLESS=1, verifying RC balance per snapshot); delete predicate_stack_probe test artifacts (they assert the deleted path)
  • Default path == former gated path: compiler_repo/diagnostics/aot-guardrail.sh —floor green on the DEFAULT build; full ./test-all.sh green debug AND release; cross-executor behavior, exact logical ownership/drop/unwind-event, and leak legs

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

  • Post-deletion: DEFAULT aot-guardrail.sh --floor green; full ./test-all.sh debug AND release; snapshot suite re-blessed with RC-balance verified per snapshot; VF-1.1 zero corpus-wide.

Entry-gate reading (w-06f7a675, 2026-07-09 at 87d7a2154; gate MET 2026-07-10 at b79c1880a)

  • 2026-07-09 at 87d7a2154: 10 failing cells — gate NOT met; ADR authored, ordering locked, cells folded in.
  • Dominant family: borrowed-param + COW mutation (5 cells: push_element_borrowed_param_two_calls, borrowed_param_then_cow_mutation, borrowed_str_list_called_in_loop, arc_borrowed_param_cow_push_diamond, split_first_to_lowercase); generics forwarder (2); callee-returns-unique reuse (1); journey_guard lifecycle (1); narrowing coexistence (1).
  • The 10 cells drained across ledger cycles 12-20 (one cure per cell: guardrail zero-NEW verification, baseline prune, toggle + negative pins where a new pass landed; per-cycle teeth in the plan ledger).
  • 2026-07-10 at b79c1880a: aot-guardrail.sh --floor reads FAIL COUNT: 0 (2979 passed / 0 failed, zero NEW vs baseline, full AOT corpus under the gated burden-sole probe). Gate MET.
  • Open-bug reconciliation at floor-zero (detail in decisions/01-cutover-ordering.md): BUG-04-253 + BUG-04-255 repro shapes now PASS (cured incidentally; flagged for closure re-triage); BUG-04-256 still double-frees but on ALL paths (path-independent — does not discriminate the cutover; stays on its own fix route); BUG-07-286 is a tooling bug mooted for clean runs by the zero-cell floor.

Diagnostic-question log

  • 2026-07-09 arc/class-ledger: why is a registered user @drop invisible at the ledger gate (UserDropGlue never fires for a Drop-impl type)? — answered: the mono sweep’s write_spec_to_idx recomposed the burden with user_drop: None, clobbering the Drop-impl overlay; cured by inheriting user_drop/compiled_drop from the existing burden when incoming fields are None (registry pin recomposed_burden_preserves_drop_impl_overlay); temporary probes removed same build cycle, no recurring diagnostic gap (the registry pin is the permanent guard).

Full-corpus census reading (2026-07-10, post-flip at ec8640e59)

  • class-ledger-diff.sh DEFAULTS TO --limit 100; the earlier zero-fallback readings were 100-program SAMPLES. The w-6589cdda gate is the FULL corpus: re-derive with --limit 2500.
  • Full fixtures corpus (2256 compared): 2253 identical, 0 ledger regressions, 3 cells where the LEDGER FIXES a legacy double-free (borrowed_invoke_leak/mutation_in_closure_decline, borrowed_invoke_leak/non_scalar_result_carrier, ir_quality_attributes/iter_next_no_wrapper_struct — the last shows as divergent only because the correct exit code is non-zero), 48 fallback functions.
  • Fallback drain inventory: field-view-liveness 38 (struct_self_rebuild loop-carried rebuilds 17, iterator_drop take-projects 7, generics/derive_clone two-heap-field pairs 10, rc_matrix struct loops 4); zero-classes 7 (all immortal-empty-string shapes); readiness-not-clean 2; absent-owned-param 1 (might_panic Absent-cardinality gate, VF-2).
  • Main corpus (62, leak-legged): 62/62 identical, 0 fallbacks.
  • Concurrent cargo builds corrupt census legs (1799 build_fail_both + 1 phantom divergent observed while the commit agent’s clippy gate ran) — run the census with the build lock free.

Fallback-drain progress (2026-07-10, post zero-classes drain)

  • zero-classes (7) DRAINED: the classifier records its own effective all-excluded verdict (LedgerClassification.all_vars_excluded — state-map exclusion UNION the placeholder alias-closure); the gate’s retired per-var state-map-only helper missed Let Var aliases of immortal literals. Empty-plan admission now covers the immortal-empty-string family; pins all_vars_excluded_covers_immortal_alias_closure + the zero-classes decline trace (ORI_LOG=ori_arc::aims::class_ledger=trace lists the non-excluded vars).
  • field-view-liveness (38) diagnosis on the simplest cell (struct_self_rebuild/single_field_loop_negative): the loop-carried container (r = Box { values: r.values.push(i) }) has MULTIPLE birth sites (initial + per-iteration rebuild), so PV-1 refuses the phi admission and the loop block-param class is CONSTRUCTLESS — field-decomposition declines (view not skip-derivable, the consume is not at the container’s own Construct) and extraction-funding declines MergeDisagree (loop-header owed counts differ entry-edge vs back-edge). The cure surface is a loop-aware arrangement for multi-birth-site rebuild chains (the ledger analog of the legacy sibling-union + rebuild-lineage scans); sub-families: struct_self_rebuild 17, iterator_drop take-projects 7, generics/derive_clone two-heap-field pairs 10, rc_matrix struct loops 4.
  • absent-owned-param (1, might_panic) + readiness-not-clean (2) remain; the absent-param gate is the VF-2-honest disposition until the dead-live-path shape is modeled.

Field-view-liveness cure design (loop-carried rebuild; next implementation step)

  • Root shape: a Jump-arg into a phi-REFUSED block-param (multi-birth-site loop thread) books NO event today — the funded field class’s back-edge Jump consume gets a successor-front release at the loop header, whose owed count then disagrees entry-edge (0) vs back-edge (+1) → MergeDisagree; field-decomposition separately declines because the loop block-param class is constructless.
  • CORRECTION (verified against dispatch.rs): the cross-class Jump-arg transfer bookkeeping ALREADY EXISTS (classify_terminator Jump arm books Consume(arg class) + Credit(param class); an excluded immortal hand-off still credits). The real defect is in the EXTRACTION-FUNDING cure’s seed arrangement for a LOOP-SPANNING view class: the endangered view (ArcVarId(30), path [0]) unions the per-iteration extraction views (%21 consumed at the bb2 back-edge Jump, %31 read at the bb4 Invoke) into ONE class, and the cure seeds incs at both sites with front decs at blocks 7/8/9 — the completed plan’s owed counts then disagree at merge block 1 (entry edge vs back edge, disagree=[(1,1)]). The cure surface is the seed/release arrangement for a class whose funded sites sit on OPPOSITE sides of a loop back-edge (per-iteration pairing: each seed’s release must land within its own iteration’s edge cone, not on shared successor fronts).
  • Verify against struct_self_rebuild/single_field_loop_negative.ori first (simplest cell), then the 17-cell struct_self_rebuild family, then iterator_drop take-projects (7) + generics/derive_clone pairs (10) + rc_matrix (4); full census target: field-view-liveness 38 -> 0.
  • Calculus anchor: PV-2 three-clause placement over the per-class CFG ledger already models per-edge credits (T4 boundary composition consumes contract-classified events); the intra-function Jump-transfer is the same event algebra — verify whether AimsProof.Ledger needs an additive theorem for the refused-phi edge kind BEFORE implementing (arc.md CP-1; scratch-Lean the shape when in doubt).

Fallback drain progress 2 (2026-07-10, post per-reference pricing at commit 48a6502dc+)

  • field-view-liveness 38 -> 20: the loop-carried rebuild family (struct_self_rebuild 14 + rc_matrix 4) drained by per-REFERENCE consume pricing (emit/incs.rs: a consume OF a seeded member prices against the seed var’s own alias closure, forward-only; the class-wide full surface double-funded back-edge hand-offs -> MergeDisagree). Census-snapshot tooling fix: class-ledger-diff.sh copies the resolved binary into its workdir (parallel builds corrupted two full-census runs into ~1800 phantom build-fail-both records).
  • Remaining 20 field-view-liveness sub-families:
    • generics pairs (5: swap/duplicate/pair/chain/permuted_layout): the returned TUPLE (Invoke result, constructless) has endangered str field views; extraction-funding declines “seed type carries no burden” — the Project dst’s var_type is the monomorphized-generic Idx and lookup_burden(idx_to_type_ref(ty)) fails to resolve it (concretely str). Cure surface: resolve the mono’d type (or fall back to the partition/repr’s heap-ness) before declaring un-fundable.
    • derive_clone (4) + iterator_drop take-projects (7) + struct_self_rebuild residue (3: cross_variant_projection_loop, late_use_alias_loop, sum_payload_match_rebuild) + memory_stress (1): un-diagnosed.
  • readiness-not-clean 2 (branch_exclusive_rebuild + might_panic second fn); absent-owned-param 1.

Fallback drain progress 3 (2026-07-10, post FatValue-seed admission)

  • Census-verdict discipline: NEVER count readiness modes with a bare grep on ori’s stderr — tracing wraps mode= in ANSI codes even when piped, so grep -c 'mode="fallback"' returns FALSE ZEROS. The census script (which strips ANSI) is the sole mode-count verdict; pin ORI_BIN to a session-owned snapshot when parallel worktree sessions share target/.
  • field-view-liveness 20 -> 15 (fallback total 18): the FatValue-seed admission (a str/closure fat value is always refcount-managed; the burden lookup cannot resolve monomorphized-generic pool aliases of str) drained the generics-pairs family (5). Pin fat_value_seed_fundable_without_burden_entry (revert-checked).
  • Remaining 18: iterator_drop take-projects (7) — the endangered payload IS an iterator handle (Holds(it: Iterator<int>)): extraction-funding correctly declines (no RC burden, an inc lowers to nothing) and field-decomposition declines arm-safety (“sum release site neither extraction-dominated nor tag-excluded”, the bypass path never extracts). Cure surface: an iterator-payload disposition for take-project source enums (the ledger analog of the legacy take_project bypass-entry release scan). derive_clone (4), struct_self_rebuild residue (3), memory_stress (1) un-diagnosed; readiness-not-clean (2); absent-owned-param (1).

derive_clone family diagnosis (next cure)

  • Shape (derive_clone_result_str_str): the loop element p is extracted once (one Project seed) but handed off TWICE per iteration (Ok(p) store + Err(p) store, each followed by a p.len() read). The cure seeds ONE inc; the completed plan’s owed count goes -1 at the merge (disagree [(3,-1)]) because the second consume is unfunded.
  • CORRECTED (IR verified): %22 = Project %18.1 is the single seed and %23/%25/%32/%34 are ALL plain Let Var(%22) aliases — the closure covers every consume/read, yet plan_incs emitted ZERO duplication incs despite each consume having a same-block suffix read of a closure var (bb4: Consume %23 then Read %25 at the terminator; bb9: Consume %32 then Read %34). The completed plan is [seed inc only] and the owed count goes -1 at the merge. The hole is INSIDE plan_incs’ seeded-consume branch (or the funded event stream feeding it) — reproduce with a focused unit test (one Project seed, two Let-alias consume+read pairs in successive blocks) and step the pricing predicates.
  • Likely shared with struct_self_rebuild residue (cross_variant_projection_loop, late_use_alias_loop, sum_payload_match_rebuild) + memory_stress (multi-hand-off per extraction).

Fallback drain progress 4 (2026-07-10, owning-seed closures + cycle-seed discriminator)

  • field-view-liveness 15 -> 9 (fallback total 12): the derive-Clone / cross-variant / late-use multi-hand-off family drained by (1) pricing a seeded consume against the OWNING SEED’s Let-alias closure (an alias-rooted closure is a singleton - the closure grows downstream only - so demand read empty and no duplication inc landed) and (2) counting IN-CYCLE SEED ops as per-iteration instance creators in the full-closure discriminator (has_cycle_seeds; the funded stream has no positive-delta events so the class read loop-invariant and no per-iteration release placed). Probe seeded_view_with_two_handoffs_funds_both drives plan_class directly.
  • One ablation negative pin (test_rebuild_lineage_release_toggle_restores_leak) pinned to the legacy leg (the drained shape made the legacy toggle inert under replacement) - the same treatment as the flip’s ~30 ablation-env pins; expect the SAME cure for any toggle pin whose bisected shape drains later.
  • Remaining 12: field-view-liveness 9 (iterator-payload take-projects ~7 + memory_stress 1 + 1 TBD), readiness-not-clean 2, absent-owned-param 1. The iterator-payload family needs its own disposition (funding cannot apply - no RC burden on handles; decomposition fails arm-safety on the bypass path).

Iterator-payload take-project disposition (CP-1 grounding, next cycle)

  • The FD calculus (AimsProof/FieldDecomposition.lean §T6) models a field’s moved mark as PATH-INDEPENDENT (FD_skipset_sound: skip == marked per field, one verdict for all release sites). The take-project shape is path-DEPENDENT: the payload moves out on the take path (skip the payload at that path’s release) and stays on the bypass path (whole-var release must drop the iterator).
  • Step (1) DISCHARGED (2026-07-10): the scratch-Lean per-site theorems (FD_per_site_skipset_sound pathwise iff + FD_site_uniform_projection site-verdict projection under the arm-safety uniformity hypothesis) both prove clean under the kernel against the committed payloadEvents/FD_cell_balanced_iff model (scratch source preserved at the session scratchpad scratch_per_site.lean; re-run via cp into aims-proof/lean/scratch/ + lake env lean). Proceed to (2) landing four-surface-synced.
  • Cure sequence per arc.md CP-1/CP-4: (1) scratch-Lean an additive per-SITE theorem — over a path universe where each path p carries moved_p and each release site s serves paths P(s): with skip(s) <-> (all p in P(s) moved), and one release site per path, every path’s payload stream balances per the committed pathwise FD_cell_balanced_iff; (2) land it four-surface-synced (Lean + .proof T6 extension + aims-rules PV-6 + Annex E prose); (3) implement per-site skip verdicts in derive_sum_skip / dec_partial planning (arm-safety then becomes the per-site condition itself); (4) drain the 7 iterator_drop cells + memory_stress via the census.
  • Current honest state: those cells run leak-free via the legacy fallback; the toggle-pin cure precedent (legacy-leg env) applies to any of their ablation pins that drain later.

Per-site decomposition implementation design (calculus landed; step 3 in flight)

  • Calculus LANDED four-surface-synced: FD_per_site_skipset_sound + FD_site_uniform_projection in AimsProof/FieldDecomposition.lean (lake build clean; check-proofs 0 regressions; dual-discharge 129 agree; sync-aims-spec clean; T6 .proof + proof-lean-map row + aims-rules PV-6 per-site clause + Annex E prose all updated).
  • Implementation (in cure_view_with_field_decomposition / sum_skip_sites_arm_safe): per-SITE classification instead of the all-sites gate — a container release site EXTRACTION-DOMINATED gets the skip (DecPartial/DecVariant); a site NOT forward-reachable FROM any extraction (the bypass edge; tag-excluded arms) keeps the whole-var Dec; a MIXED site (reachable both with and without extraction) declines.
  • Booking insight (expressible in the EXISTING event algebra, no per-path streams needed): KEEP the view’s move-in store consume; book each extraction as a CREDIT (+1 re-acquisition of the reference the store gave the container). Take path: birth +1, store -1, extraction credit +1, move-out consume -1 = 0. Bypass path: birth +1, store -1 = 0 (the whole-var release recursively pays it). The per-path verifier validates both.
  • Target family: iterator_drop take-projects (7) + memory_stress (1); the iterator payload needs NO funding (the credit is the extraction itself, and the extracted handle’s own consume is its release).

Fallback drain progress 5 (2026-07-10, per-site consumer + constructless variant + funded-move-in)

  • field-view-liveness 9 -> 0 (pending full-census confirmation). Three cures, all pinned + ori_arc lib 2062 green + clippy 0:
    1. Per-site decomposition consumer (step 3 of the plan above): SiteVerdict Skip/Whole per container release site (SumArmContext dominance + tag-exclusion + forward-reachability), extraction credits booked via extract_class_events_with_extraction_credits, preceding_credit_funds hoisted above the borrowed-gate in emit/incs.rs. Pin bypassable_extraction_sum_cures_per_site (rewritten from the fail-closed decline pin - behavior change kernel-proven by FD_site_uniform_projection). Drained 4 of the 7 take-projects + vacuity (all_payloadless) drained enum_tagged_ptr_match_empty.
    2. CONSTRUCTLESS sum containers (enum arrives as callee Invoke result / merge param - sum_container=false constructless=true): variant identity derives from the TYPE’s burden table via derive_constructless_enum_variant - self_heap_alloc required (excludes Option/Result niche wrappers structurally: their builtin templates carry self_heap_alloc: false), EXACTLY ONE payload-bearing variant with ONE payload slot, ordinal = variant_id.get()-1 (VariantId is 1-indexed). Gate relaxed: constructless admitted ONLY with a type-derived skip. Scratch-Lean discharge scratch_constructless_variant.lean (uniqueness premise composes with committed FD_per_site_skipset_sound; CP-1 case (a) - covered, no calculus extension needed). Pin constructless_invoke_result_sum_decomposes_container_release + test-util registered_tagged_enum_with_unique_payload_variant (compute-shape burden). Drained enum_tagged_ptr_match_consume_dynamic + per_source_lineage; both exit 0 under ORI_CHECK_LEAKS=1 on the burden-sole probe.
    3. FUNDED-MOVE-IN refinement (memory_stress/mem_shared_inner_multiple_containers - one Core shared by TWO Wrapper containers, no extraction): a consume at ANOTHER released container’s Construct is a funded hand-off when the view’s own plan carries the funding (facts_consume_marked: all extra consumes at released construct sites AND consume_sites.len() <= 1 + planned_inc_count). NOT gated on self_funded_clean (a Clean verdict does NOT prove funding - the extract-then-restore pin caught that first attempt; the planned-Inc count does). Pins: shared_inner_two_released_containers_funded_no_hazard (new) + extract_then_move_out_via_second_container_funds_itself_at_extraction (updated: the base plan’s dup inc at BeforeBody funds the second hand-off - no cure re-book needed; both placements RC-sound, the base one is now recognized).
  • Remaining fallbacks (expected 3): readiness-not-clean 2 (branch_exclusive_rebuild + might_panic second fn), absent-owned-param 1 (might_panic, VF-2-honest). Full census + guardrail floor in flight.

Readiness-not-clean diagnoses (next cycle; read-only scoping 2026-07-10)

  • struct_self_rebuild/branch_exclusive_rebuild (main): merge-origin class (ArcVarId(12) whole-var) verdict Unprovable declined MergeDisagree. Loop-carried Pair rebuilt on the even arm / read on the odd arm; the class books Credits (+1) on TWO predecessor terminators feeding the merge, reads across the loop body, ONE terminator consume. The per-path owed counts disagree at a merge - the branch-exclusive variant the per-reference pricing cure did not reach.
  • ir_quality_attributes/generic_call_with_builtin_arg_not_treated_as_intercepted (main): fresh str-literal class (“hello”, var 0) verdict LeakOnly declined UnplaceableRelease. Books Birth +1 (owned literal into the ttr call) then Credit +1 (RL-34 result re-acquisition, var 1) with borrow reads only - NO consume anywhere, so no release placement site verifies. Coupled to the SAME fixture’s might_panic$m$3_str absent-owned-param fallback (the callee always panics; if true then panic; x - the surviving-path x is dead, the transfer path is the unwind). Treat the two as ONE cure surface.

branch_exclusive_rebuild cure design (readiness-not-clean cell 1; IR)

  • IR shape (main): loop header bb1(%11, %12: Pair[Aggregate]); even arm bb6 extracts BOTH fields (%26 = Project %25.0, %28 = Project %27.1, aliases of %12) into a NEW Construct %29 and hands %30 to the bb8 merge; odd arm bb7/bb9 borrow-reads both fields then hands %12 ITSELF to bb8 via bb15 (Consume at b15 terminator). bb8(%51) -> bb3(%13) -> back-edge into %12.
  • The %12 merge-origin class books: Credit +1 at bb0 + bb3 terminators (per-edge hand-ins), borrow Reads on both arms, ONE Consume (odd arm only). Completed-plan nets: even path arrives at bb8 owing 1 (no consume - the field extractions are booked as Reads), odd path owing 0 -> disagree=[(8, 0)] -> MergeDisagree -> Unprovable.
  • Cure surface: the even arm is a FULL MOVE of the aggregate (every owned field of the Aggregate-repr Pair projected and consumed at the same arm’s Construct args - the ledger analog of the legacy sibling-moved-field-union full_move_vars suppression). Book the arm’s LAST field extraction as a Consume of the AGGREGATE class (delta -1): even path then nets 1-1=0 at bb8, agreeing with the odd path. Booking lives in the events extraction (or a hazard-style rebook pass): detect “all owned fields of an aggregate class projected on one arm, each projection consumed at a Construct arg on that arm” -> rebook the final projection Read as the aggregate’s move-out Consume. CP-1: check whether the T3/T6 committed calculus covers arm-local full-move rebooking (likely FD_skipset_sound with the whole-field-set marked = full skip = the vacuous release); scratch-Lean first.
  • CP-1 step 1 DISCHARGED (scratch_full_move_rebook.lean, kernel-clean; copy at session scratchpad): the full-skip cell (every field marked+skipped) balances per committed FD_cell_balanced_iff; the rebooked consume is the committed RL-2 ConstructArg transfer (FD_moveout_is_committed_transfer); per-path parent streams [Credit +1, Consume -1] net 0 on both arms. CP-1 case (a) - covered, no calculus extension; proceed straight to the events-rebook implementation next cycle.

Fallback drain progress 6 (2026-07-10, arm-local full-move rebook)

  • readiness-not-clean branch_exclusive_rebuild DRAINED (fallbacks 4 -> 3 pending census): the arm-local FULL-MOVE rebook. Three pieces in events.rs + wiring in analyze_class_ledger:
    1. detect_full_move_arms (pure-IR pre-pass): per block, ONE Construct consuming projection dsts; all Projects off ONE aggregate class; each dst used exactly once; moved field set == the burden’s owned top-level field set; no other member-var use in the block (Let aliases + the moves permitted). Fail-closed.
    2. Aggregate side (apply_full_move_rebook): the arm’s Reads rebook to ONE move-out Consume at the Construct site - per-path owed counts then agree at the downstream merge (was disagree=[(8,0)] MergeDisagree/Unprovable).
    3. Field-view side (full_move_credit_sites + extract_class_events_with_extraction_credits gaining a force_owned param): the extraction books a CREDIT (bookkeeping, NOT a runtime inc) - the field’s reference rides the aggregate’s transfer.
  • TWO wrong attempts recorded en route (both caught by ORI_CHECK_LEAKS on the fixture, 2 leaked allocations each): (a) rebook alone: the field classes’ plan-time dup incs (+1 per even iteration) lost their balancing release when the old aggregate’s per-iteration drop disappeared; (b) rebook + credits in the INITIAL extraction only: the initial plans read Planned([]) correctly, but the hazard cure ladder re-fired (container-held demand endangerment) and REPLACED them with seeded runtime incs at the full-move extractions - same surplus. Cure: cure_view_with_extraction_funding takes full_move_arms, seeds every OTHER Project but books full-move projections as credits (force_owned re-extraction with credits); full-move construct sites also join the hazard funded-union.
  • Key distinction learned: a SEED is a planned runtime Inc (+1 at execution); a CREDIT is pure bookkeeping (the reference already exists via the transfer). Full-move extractions need credits, never seeds - a seed there bumps the count once per arm execution with no matching release (the moved-out aggregate is never dropped).
  • CP-1: covered calculus (scratch_full_move_rebook.lean discharged against committed FD_cell_balanced_iff + FD_moveout_is_committed_transfer; no extension landed). Pin branch_exclusive_full_move_rebooks_aggregate_consume + the aot fixture leak-clean e2e. ori_arc lib 2063 green, clippy 0; 4 cured fixtures regression-verified exit 0.
  • Remaining (census in flight): readiness-not-clean 1 (generic_call_with_builtin_arg… main UnplaceableRelease) + absent-owned-param 1 (its might_panic twin) - ONE cure surface (the panic-always ttr callee).
  • might_panic pair IR-scoped (final 2 cells, one surface): callee might_panic$m$3_str(%0: str [own]) panics unconditionally - the if true FOLDED, so the Return %0 fallthrough bb3 is predecessor-less and %0 is genuinely Absent. Call site passes %0 [borrow] (caller retains + decs on BOTH edges - the legacy plan is coherent). Cures next cycle: (a) callee absent-owned-param admission - an Absent param whose effective call-site ABI is BORROWED owes the callee nothing (no release to plan; the decline is pure conservatism); genuinely-owned Absent params plan the RL-5 entry dec instead. (b) main’s UnplaceableRelease - the {literal, ttr-credited result} class owes 2 on the normal path (birth + credit) and 1 on the unwind path; the release placement walk fails on the asymmetric owed counts (normal: dec %0 + dec %1; unwind: dec %0 with Resume terminator). Extend placement for per-path owed asymmetry funded by a normal-edge-only credit.
  • OVER-FIRE caught by guardrail-2 (NEW failure test_loop_header_init_vs_back_edge_keeps_per_edge_identity, exit 139 UAF): in loop_header_merge_read.ori the loop threads TWO Pair params (%16 iteration value + %18 init value) that alias ONE runtime allocation on the ENTRY edge (Jump bb1(.., %6, .., %4) - both args alias the same birth %4). The full move through %16’s lineage stranded %18’s reads. Per-source partition splits them (correctly, per-edge identity) so partition membership + block-local alias closure both missed it. CURE: moved_class_shares_edge_source - decline the arm when ANY Jump edge feeds a moved-class param AND a different-class param from same-class args (the statically-visible aliasing witness). All 6 struct_self_rebuild fixtures now exit 0 (incl. the regression cell); pins shared_edge_source_declines_full_move_arm (unit negative) + the aot fixture (e2e). ori_arc lib 2064 green, clippy 0. Guardrail + census re-running against the gated build.

Fallback drain progress 7 (2026-07-10, might_panic pair drained - CENSUS TARGET: ZERO fallbacks)

  • absent-owned-param DRAINED: an Absent param books NO events regardless of declared ownership - every call site passes it BORROWED (the contract_to_params convention maps Cardinality::Absent/Consumption::Dead to Ownership::Borrowed, verified at aims/emit_rc/arg_ownership/mod.rs), so the caller retains+releases and the callee owes nothing (the borrowed-boundary discipline, RL2_borrowed_param_emits_caller_dec). The FallbackReason::AbsentOwnedParam decline + classification flag REMOVED (dead machinery); pin rewritten absent_owned_param_books_no_events (asserts no Birth for the absent param; live param keeps its birth).
  • readiness-not-clean (main, UnplaceableRelease) DRAINED: a class may owe SEVERAL references to ONE allocation (birth + RL-34 result re-acquisition credit); the release planner refused any owed count != 1. Cure: push_front_decs(count) - one front dec per owed reference at each dead successor (same resolved subject var; each lowers to one refcount decrement) - wired into the RL-4 edge-release path AND the terminator-read residue path (plan_block_release). Pin multi_owed_class_places_one_dec_per_reference (drives plan_class with the credited stream; asserts 2 front decs on the normal successor + Clean verify). might_panic fixture: BOTH functions replaced, output + exit byte-identical to legacy (“ori panic: boom”, exit 1).
  • ori_arc lib 2065 green, clippy 0; all 5 previously-cured fixtures regression-verified exit 0. Final sweep in flight: guardrail floor + full aot census + spec census (fresh snapshot) - EXPECTED: 0 fallback functions across the corpus (the w-6589cdda deletion precondition).

Multi-owed placement REVERTED (2026-07-10; leak-check masking lesson)

  • Guardrail-2 caught TWO regressions from the multi-owed release placement: no_loop_rebuild_negative (SIGSEGV 139, plain run) + probe_dup_alias_store_into_struct_pair_coupling_disabled_double_frees_negative CONTROL leg (exit 134 double-free on stash_and_return).
  • VERIFICATION-PROTOCOL LESSON - ABSOLUTE for this grind: ORI_CHECK_LEAKS=1 runs MASK use-after-free/double-free (the leak-check allocator defers reuse); every fixture verdict now requires BOTH a plain run AND a leak-check run. Several earlier “exit 0” verdicts this session were leak-check-only.
  • no_loop root cause (KEPT, gated): the full-move arm fired where the aggregate BIRTHS in the arm block - the rebook precondition (all-Read events) fails there so the aggregate keeps its release, while the field credits still injected -> half-applied booking double-funds the store. Cure: class_uses_confined_to_moves declines when any non-Let instruction DEFINES a tracked member in the block (birth-in-block witness). Detection and application are now structurally coupled.
  • stash root cause (REVERTED): the one-dec-per-owed-book placement trusted the BOOKS’ residue as the runtime count; cure/force-owned re-extractions deliberately inflate books past the runtime count (floor discipline), so residue-N placement over-released. releases.rs restored byte-identical to 212ae19de; might_panic’s main returns to the honest readiness-not-clean fallback (the ONE remaining fallback cell). A future multi-owed cure must prove each positive book entry is a REAL runtime acquisition before counting it.
  • Pin multi_owed_class_declines_fail_closed (rewritten from the 2-dec assertion): a books-owe-two class DECLINES UnplaceableRelease. absent-param admission KEPT (callee replaced; absent_params joins the classifier exclusion set so param-only functions admit via zero-classes/all-vars-excluded - spec census 62/62, 276 replaced, 0 fallbacks).
  • ori_arc lib 2065 green, clippy 0; ALL cured fixtures re-verified plain+leak (stash 0, no_loop 0/0, branch_exclusive 0/0, loop_header 0/0, iterator_drop pair 0/0, mem_shared 0/0, might_panic 1/1 = designed panic, legacy-identical).

Runtime-grounded multi-owed design (next cycle; the ONE remaining fallback cell)

  • The might_panic main books were actually runtime-true PER PATH: normal path birth(+1 real) + RL-34 credit(+1 real, pending_entry routes it to the normal successor only), unwind path 1. The dead-end teeth (attempt 42) bite the GENERALIZED placement because OTHER classes reach the same code path with cure-inflated books (force_owned re-extractions, seeded re-plans).
  • Sound scoping: carry a books_runtime_grounded: bool on ClassEvents - TRUE only from the PLAIN extract_class_events path (every positive entry a classifier-booked Birth/Credit); FALSE for force_owned / rebooked / credited / seeded cure extractions. plan_block_release + plan_edge_releases permit residue-N placement (N front decs via a count-aware push that preserves the front dedup) ONLY when the flag is true; cure books keep the fail-closed != 1 decline. This satisfies the attempt-42 generalizes_to clause: the flag IS the proof each entry is a real acquisition.
  • Then re-verify against BOTH teeth: stash_and_return (cure books -> still declines) and no_loop (arm gated) - plain + leak runs.

Fallback drain progress 8 (2026-07-10, runtime-grounded multi-owed - LAST cell drained)

  • The books_runtime_grounded flag (designed above) implemented: TRUE only from the PLAIN extract_class_events_inner path (!force_owned && skip_consume_sites.is_empty()); cleared by the credits variant AND apply_full_move_rebook. push_front_decs(count) restored with the front-dedup preserved; multi-owed placement (edge releases with exit > 1; terminator-read residue > 1) fires ONLY on grounded books - cure-inflated books keep the fail-closed != 1 decline (the attempt-42 generalizes_to satisfied: the flag IS the per-entry real-acquisition proof).
  • Verified against BOTH attempt-42 teeth: stash_and_return plain=0 leak=0 (cure books ungrounded -> the cure plans exactly as at 212ae19de); no_loop_rebuild plain=0 leak=0 (arm gated). Target drained: might_panic fixture 0 fallbacks, plain=1 leak=1 (designed panic, legacy-identical). branch_exclusive + loop_header re-verified 0/0.
  • Pins: multi_owed_grounded_books_place_one_dec_per_reference (positive: Planned + Clean + 2 front decs on the normal successor) + multi_owed_ungrounded_books_decline_fail_closed (negative: UnplaceableRelease) - the positive/negative pair over the same builder. ori_arc lib 2066 green, clippy 0. Guardrail + spec census for this increment in flight; commit 0ac14df32 carried the prior increment.

Deletion-unit scoping notes (post-drain; census confirmation in flight)

  • Commits this campaign: 212ae19de (field-view-liveness drain: per-site + constructless + funded move-in), 0ac14df32 (full-move rebook + gates + absent-param admission + multi-owed fail-closed pin), c531a2a45 (runtime-grounded multi-owed placement - LAST cell). Spec census 0 fallbacks x3 runs; guardrail floor 2979/0 NEW 0 x3; definitive full-aot census (2256 programs, ori-census-v2 snapshot @ c531a2a45) in flight - its ZERO-fallback verdict is the w-6589cdda deletion precondition.
  • Gate-site inventory so far (deletion targets): ORI_DISABLE_PREDICATE_STACK_RC read via rc_remark.rs:on_burden_sole_path (env read) + LazyLock consumers in emit_rc/mod.rs (release_burden_only_edge), emit_rc/edge_cleanup.rs (burden_only paths), emit_unified.rs (probe-path realization tail ~line 353), lower/burden_lower/ownership_scans/reassign_release.rs; oric surfaces: debug_flags.rs entry + commands/build/mod.rs remarks-bridge auto-set. burden_emitted coexistence-handshake refs: 54 in ori_arc (the marker driving predicate-stack suppression per-shape on the default path).
  • PRESERVE-LIST reminder (from prior scoping): decide_annotations/decide_cow/decide_drop_hint/AnnotationSiteContext/ssa_alias_classes/ensure_singleton_class/materialize_payload_edge_classes. decide.rs dead island + 29 tests; cleanup_redundant empirical resolution via ORI_DISABLE_REDUNDANT_CLEANUP bisection; repr-opt coordination before emit_unified.rs edits; per-file ori-rc-remarks —diff during the 7-site collapse.

Fallback drain progress 9 (2026-07-10, tuple burden composition - the ACTUAL last cell)

  • The definitive full-aot census @ c531a2a45 read 1 fallback (field-view-liveness), not zero: fat_ptr_iter/conversion/derive_clone_slice_str_tuple.ori (parallel-hunt across all 2276 fixtures with an 8-way split of per-file mode="fallback" traces). Shape: derived-Clone Pair holding a TUPLE (str, int); the clone result’s tuple field view (33,[0]) is demand-endangered (read after the pair’s release); extraction funding declined “seed type carries no burden” - the seed var is the TUPLE-typed projection (Aggregate repr, so the FatValue escape does not apply) and compose_burden_for_idx had NO Tag::Tuple arm (Struct/Enum + builtin templates only) -> lookup_burden(tuple_idx) = None.
  • ROOT-CAUSE fix in ori_types (monomorphization/burden.rs): Tag::Tuple composes the anonymous-struct burden from pool.tuple_elems via compute_struct_burden_from_field_types - a standalone tuple Idx now resolves the same owned-field burden a named struct with those fields would. Cell drains: 0 fallbacks, plain=0 leak=0.
  • Pins: tuple_with_heap_element_composes_owned_field_burden ((str,int) -> owned_fields [[0]] typed str) + all_scalar_tuple_composes_no_burden ((int,bool) -> None), sibling burden/tests.rs. ori_types 1202 green, ori_arc 2066 green, clippy 0 both crates.
  • Blast-radius note: the tuple arm also feeds the codegen pool-walking gap-fill pass, so tuple Idxs may now REGISTER burdens where they previously resolved None - guardrail + both censuses (v3 snapshot) re-running to catch any tuple-wide RC emission shift.

CAMPAIGN CLOSE: fallback census reads ZERO (2026-07-10, @ 73593ddae)

  • Definitive full-aot census (2256 programs, v3 snapshot): 0 fallback functions, 3739 replaced, 2253 identical. Spec census: 62/62 identical, 276 replaced, 0 fallbacks. Guardrail floor 2979/0, NEW 0, STALE 0.
  • The 3 non-identical cells are ALL legacy-leg failures the ledger FIXES (iter_next_no_wrapper_struct DIVERGENT: legacy double-free 134 vs ledger correct exit 14; mutation_in_closure_decline + non_scalar_result_carrier: legacy 134 vs ledger 0) - the retiring path is the broken one; non-blockers.
  • Campaign commits: 212ae19de, 0ac14df32, c531a2a45, 73593ddae. Full drain 48 -> 0 across: zero-classes vacuity, per-reference pricing, FatValue seeds, owning-seed closures + cycle seeds, per-site decomposition + extraction credits, constructless type-derived variant skip, funded move-in, full-move rebook + 3 gates, absent-param admission, runtime-grounded multi-owed placement, tuple burden composition.
  • w-6589cdda precondition MET: every function in the corpus is ledger-replaced under ORI_CLASS_LEDGER_EMITTER=1 (the default). The deletion unit (emit_unified Phase 6.5-6.98 repair passes + the legacy walk, per the deletion-unit scoping notes above + PRESERVE-LIST) is now unblocked.

Deletion-unit anatomy (verified from emit_unified dispatch, 2026-07-10)

  • emit_unified’s main entry is ALREADY burden-sole: func.class_ledger_emission -> mechanical Phase-7 lowering + coalesce + finalize ONLY (no probe tail, no repairs); the non-ledger branch (take_move_facts, same_alloc_reps, Phase 2.5 elimination, emit_burden_path_probe_tail with the 6.5-6.99 repair chain) is reached ONLY when the readiness gate declines (now ZERO functions corpus-wide) or under ORI_CLASS_LEDGER_EMITTER=0.
  • Deletion sequence (w-6589cdda):
    1. Remove the ORI_CLASS_LEDGER_EMITTER opt-out (ledger unconditional; keep a release-active assert or fallback_reason trace for any future readiness decline - fail-closed becomes fail-LOUD, never silent legacy).
    2. Delete emit_unified’s non-ledger branch: Phase 2.5 eliminate_burden_ops_phase, emit_burden_path_probe_tail + the whole 6.5->6.99 repair chain, their helpers.
    3. Audit burden_lower Phase-5: the ownership scans exist to shape the LEGACY op stream that replaced functions DISCARD - verify what the ledger path actually consumes (the classification + partition, not the legacy ops), then delete scan-only machinery + its ~40 ORI_DISABLE_* bisection toggles + their doc rows in arc.md/compiler-ops.md (CP-2 sync).
    4. Verify whether Phase-5’s emit_burden_ops even needs to run for replaced functions (the replacement may overwrite its output wholesale - if so, skip it entirely and delete the walk).
    5. decide.rs dead island + 29 tests; cleanup_redundant empirical resolution (ORI_DISABLE_REDUNDANT_CLEANUP bisection); repr-opt coordination; PRESERVE-LIST (decide_annotations/decide_cow/decide_drop_hint/AnnotationSiteContext/ssa_alias_classes/ensure_singleton_class/materialize_payload_edge_classes).
    6. Per-increment: guardrail floor + both censuses (the differential harness DIES with the legacy leg - its A-leg is the deletion target; retire class-ledger-diff.sh in the same increment that removes the toggle, or repoint leg A at a pinned pre-deletion binary).
  • Each deletion increment is its own cure cycle: full sweep + ledger entry + commit via the agent.
  • Step-4 ANSWERED (pipeline mod.rs Step 4b): apply_class_ledger_replacement analyzes the PRE-BURDEN IR; a replaced function SKIPS emit_burden_ops_step (the legacy Phase-5 walk) entirely - “never both emitters”. With 0 fallbacks corpus-wide, the legacy walk + its ~40 ownership scans + emit_unified’s non-ledger branch execute ONLY under ORI_CLASS_LEDGER_EMITTER=0 / legacy_emission_enabled(). The deletion is toggle-removal-then-dead-code-sweep.
  • Increment 1 (next): remove the ORI_CLASS_LEDGER_EMITTER opt-out + legacy_emission_enabled + make a readiness decline fail-LOUD (release assert / hard error, never silent legacy); retire class-ledger-diff.sh in the SAME increment (its A-leg IS the deleted toggle) - or repoint leg A at a pinned pre-deletion binary for one transition census. Then increment 2+: dead-code sweep per the sequence above.
  • Increment-1 blast radius (inventoried): 34 test sites across ~14 aot files pin the LEGACY leg via ("ORI_CLASS_LEDGER_EMITTER", "0") (ablation-toggle negative pins whose subject IS the deleted walk) - they are deleted WITH the legacy walk, in the same increment as the toggle they ride (never orphaned as silent no-ops: a stale =0 env in a test becomes a false-green ledger run). legacy_emission_enabled = !ORI_DISABLE_BURDEN_OPS (a DIFFERENT toggle - the pre-flip empty-harness baseline; dies in the same sweep). Toggle definition sites: class_ledger/mod.rs LazyLock + oric/debug_flags.rs entry + compiler-ops.md / arc.md doc rows (CP-2 sync applies to the doc removals).
  • NOTE for the deletion decision record: the readiness gate remains per-function on ARBITRARY user programs - corpus-zero is the w-6589cdda criterion, not a universality proof. Post-deletion a decline FAILS COMPILATION LOUDLY (internal error naming the declined class + reason) and every such report is a ledger bug to fix (the drain discipline, forever forward). This is the plan-recorded trade; never soften it to silent wrong-code.

UDG scalar admission: drop obligations enter the books (cycle 56, 7d5c43b07) (2026-07-11)

  • RCA correction (the destructure-discharge theory is a DEAD END): the ORI_DUMP_AFTER_BURDEN dump of sum_nested shows the legacy walk EMITS burden_dec %1 on the SCALAR-repr user-drop var even on the full-destructure shape - @drop runs at the death point (RL-DROP). The ledger could not replace because the L-9 scalar exclusion kept these vars out of the books entirely, so no Dec was ever planned and gate (b) declined.
  • Cure (admission core): compute_birth_site_partition_with_admitted + classify_function_with_admitted thread a user_drop_admitted set (scalar non-immortal vars whose type carries user_drop, computed at analyze_from_state_map); the books book their births/reads; the plan places the whole-var Dec; Phase-7 lowers it with the shipped scalar UserDrop strategy. Wrapper variants keep every existing caller unchanged (the un-admitted classify_function wrapper is now #[cfg(test)]).
  • Gate (final hybrid): an ADMITTED scalar’s drop obligation is verified by its class verdict (Clean = every path discharges by planned Dec or transfer-consume); every OTHER user-drop var keeps the conservative coverage requirement (own whole-var planned Dec, or borrowed param whose release the caller owns).
  • REGRESSION TEETH (in-cycle, caught by the aot guardrail before commit): the intermediate aggressive gate reduction - decline only on excluded && (!scalar || immortal) - drained heap map-insert user-drop structs WITHOUT books (classes=0, planned_ops=0, no release emitted) and broke drop_augment::drop_map_both_channels_let_bound_structs + drop_map_value_let_bound_released_after_insert under the gated probe (FAIL COUNT 2). DO-NOT-RE-TRY: never widen user-drop admission past the booked admitted set; a class verdict verifies nothing for an UN-booked var.
  • Pins: replacement_admits_scalar_user_drop_value_with_planned_release (red -> green; asserts Replaced + planned whole-var BurdenDec), replacement_admits_returned_scalar_user_drop_value (flipped from the prior decline pin), replacement_admits_borrowed_user_drop_param_without_own_dec, credited_call_result_payload_view_books_stay_clean.
  • Drains: t, sum_fields, drop_impl_type_checks, test_whole_value_destructure_accepted (UDG family FULLY drained). Remaining sub-shapes shifted honestly to their true reasons (each the next iterative target): sum_nested -> field-view-liveness (destructure Projects create views on the admitted scalar container; the cure ladder must run for scalar containers), newtype_drop_impl_type_checks -> zero-classes (newtype construction births nothing in the books; population gap).
  • Results: census13 fallbacks 7 -> 3 (UDG 6 -> 0; remaining sum_nested=FVL, newtype_drop_impl_type_checks=zero-classes, while_closure_by_value=RNC); replaced 10136; FAIL name-set identical 67/67 (0 new, 0 gone; +2 failed/+2 llvm-compile-fail counts attributed to 3 new traceable fixtures from a parallel session); skip count 77 identical, zero skip-set movement (skips-are-failures mandate gate); aot guardrail FAIL COUNT 0 / 2958 passed under the gated probe; drop-family 16/16 gated+leak both backends; ori_arc 2073 passed; clippy clean

Newtype zero-classes drain: unbooked-admitted empty-surface forgiveness (cycle 57, e20b9f1b6) (2026-07-11)

  • RCA: the cycle-56 admission makes a scalar user-drop var NON-excluded, but a scalar-NEWTYPE lineage mints no ledger event (the admitted var is only ever an alias DST of a non-admitted excluded scalar - %1: Handle = %0(int) - and is read only through a non-admitted int alias), so all_vars_excluded=false with classes=0 -> ZeroClasses decline, even though the empty plan is byte-identical to the legacy walk (ORI_DUMP_AFTER_BURDEN: zero ops for the shape).
  • Correctness grounding (empirical, gated env, both backends): @drop does NOT fire for scalar-repr newtype values on ANY path today (probe fixture prints nothing on interp or llvm) - an RL-DROP violation filed as BUG-04-275 (independent, deferred per routing §4: own deliverable spanning ori_eval + burden registration + booking + side-effect spec pins). The forgiveness is self-correcting: once 04-275’s fix books the shape, its class carries events and the forgiveness stops applying.
  • Cure: classify_function_with_admitted tail - an ADMITTED user-drop scalar whose partition class carries NO event counts excluded-equivalent for all_vars_excluded (evented-reps set over the classified streams x nodes_snapshot); a NON-admitted live var with zero events still declines (classifier coverage gap stays with the legacy walk).
  • Pin: replacement_admits_unbooked_scalar_user_drop_newtype_lineage (faithful 3-var alias-DST shape; revert-proof verified - RED with the forgiveness disabled; asserts Replaced + empty plan). Prior pin iteration with the admitted var as a direct Let-literal was NOT faithful (the direct literal births and self-discharges through the return) - the alias-DST shape is load-bearing.
  • Results: census14 fallbacks 3 -> 2 (newtype_drop_impl_type_checks drained; remaining sum_nested=FVL, while_closure_by_value=RNC); replaced 10137; FAIL name-set identical (0 new, 0 gone); summary byte-identical 4167/200/77/133; skip count 77 identical (skips-are-failures mandate gate); aot guardrail FAIL COUNT 0 / 2958 passed under the gated probe; drop-family 12/12 gated+leak both backends; ori_arc 2074 passed; clippy clean

sum_nested FVL drain: scalar user-drop containers skip the field-view hazard (cycle 58, b30d2c7eb) (2026-07-11)

  • RCA: sum_nested’s container (Outer, all-int fields + user @drop) is SCALAR-repr and admitted (cycle 56); its planned whole-var release lowers to the balance-neutral @drop call (RLDROP_user_drop_balance_neutral) - nothing is freed. The field-view-liveness hazard is a heap-UAF guard: it fired on the two Inner views read astride the release, though the read-after-release ordering is exactly what the legacy walk emits (burden_dec %1 between the nested Project reads in the ORI_DUMP_AFTER_BURDEN stream). The cure ladder could not help (field-decomposition: constructless param-rooted container derives no skips; extraction-funding: UnplaceableRelease).
  • Cure: field_view_hazard_classes skips a container whose whole-var members include an ADMITTED user-drop scalar (is_admitted_scalar_container); the admitted set rides LedgerClassification.user_drop_admitted (populated by classify_function_with_admitted). Heap containers keep the full hazard + cure ladder unchanged.
  • Pin: replacement_admits_scalar_user_drop_container_with_post_release_view - the faithful nested-destructure shape (alias + TWO Inner views of field 0 + nested int reads straddling the release; Inner itself user-drop). Two earlier under-faithful shapes passed vacuously (single view read before the release; direct Let-literal admitted var) - the two-view straddle is load-bearing.
  • Results: census15 fallbacks 2 -> 1 (sum_nested drained; sole remaining while_closure_by_value=readiness-not-clean MergeDisagree); replaced 10138; FAIL name-set identical (0 new, 0 gone); summary byte-identical 4167/200/77/133; skip count 77 identical; aot guardrail FAIL COUNT 0 / 2958 passed gated; drop-family 12/12 gated+leak both backends; ori_arc 2075 passed; clippy clean

while_closure RNC drain: per-edge merge equalization (cycle 59, 415adc296) (2026-07-11)

  • RCA: the loop-carried closure param’s reference dies UNPASSED on the reassignment arm (stash = () -> snapshot overwrites the binding; the arm’s jump passes the FRESH closure, not the old one) while the passthrough arm hands the old reference off at its Terminator (cross-class jump-arg Consume). The two predecessor edges exit the if-merge with divergent owed counts (the corpus trace: disagree (8,0) then the derived (1,2) at the loop header); the death-frontier walk cannot place the missing RL-4 release (every loop block stays activity-live), so the completed-plan merge gate declined MergeDisagree.
  • Cure: pre-release per-edge merge equalization in plan_class (equalize_disagreeing_merges -> equalize_one_merge): for each disagreeing merge, release the surplus (exit - min-exit) on each owing predecessor edge at BeforeTerminator, releasing the member a min-exit sibling edge hands off at its Terminator (the merge-feeding member dying unpassed). One merge per round + recompute (downstream disagreements are DERIVED from upstream frozen nets - the loop header’s (1,2) vanished once the if-merge equalized). Guards: CYCLE-INTERIOR single-successor owing preds only; candidate never passed by the owing pred itself; unresolvable residue falls to the final MergeDisagree gate.
  • REGRESSION TEETH (in-cycle, caught by the suite before commit): the first UNRESTRICTED equalizer double-released two acyclic pins (branch_exclusive_death_places_edge_dec_and_verifies_clean, dead_cross_class_merge_credit_releases_at_receiving_front) - plan_releases’ own dead-arm RL-4 already owns acyclic merges. The cycle-interior restriction (regions.is_in_cycle on the owing pred) is load-bearing; DO-NOT-RE-TRY widening the equalizer to acyclic edges.
  • Pin: merge_disagree_equalizes_with_per_edge_release (the faithful 7-block loop CFG: birth into the loop header, reassignment arm passing a fresh construct, passthrough arm handing off, back edge; asserts Clean + the equalizing Dec on the reassignment arm; RED Unprovable pre-cure). Behavior: tests/spec/expressions/while.ori 28/28 both backends gated + zero leaks (stash()==2 capture-by-value semantics pinned).
  • Results: census16 fallbacks 1 -> 0 - THE tests/spec CLASS-LEDGER FALLBACK SURFACE READS ZERO (replaced 10139); FAIL name-set identical (0 new, 0 gone); summary byte-identical 4167/200/77/133; skip count 77 identical; aot guardrail FAIL COUNT 0 / 2958 passed gated; expressions/while corpus 28/28 both backends gated + zero leaks; ori_arc 2076 passed; clippy clean; pin revert-proof verified

Increment-1 fail-loud attempt REVERTED: the aot corpus is not zero (cycle 60, in-tree revert) (2026-07-11)

  • Attempt: with tests/spec + tests/aims + tests/run-pass reading ZERO fallbacks, the fail-LOUD landed (apply_class_ledger_replacement asserting Replaced; pipeline pin retargeted to should_panic).
  • TEETH: guardrail 60 returned FAIL COUNT 38 - the ENTIRE drop_augment aot family (boxed recursive enums, closure-env teardown, panic-path cleanup, map two-channel drops) still DECLINES and was silently falling back. The sibling workstream’s aot census-zero was taken at 73593ddae, BEFORE the cycle-56 user-drop admission changed the decline profile. census17 (tests/spec) stayed clean: 0 fallbacks, 0 ICEs, name-sets identical.
  • DO-NOT-RE-TRY (extends cycle-47): never land fail-loud off a census taken at an older SHA or on a subset of surfaces - re-measure EVERY surface (tests/spec, tests/aims, tests/run-pass, the FULL aot fixture corpus, snapshots) under the CURRENT tree in the SAME cycle.
  • Revert: assert + should_panic pin backed out; silent-fallback pin restored; ori_arc 2076 green; guardrail re-run pending.
  • Next: drain the drop_augment aot decline family (38 fixture ids preserved in the session worklist) - these are the heavier RL-DROP shapes (heap user-drop containers, panic-path cleanup) the cycle-56..58 scalar admissions do not cover; then re-measure all surfaces and re-land fail-loud.

Cycle 61 — borrowed-ROOTED alias exemption drains the @drop/eq/hash impl-method decline family

  • Target sub-shape: 19/21 extracted drop_augment fixtures declined on function="drop" / "eq" / "hash" / "scoped" — UserDropGlue.
  • RCA (DBG-ICE probe + ORI_DUMP_AFTER_BURDEN IR): fn @drop(%0: Logged [borrow]) bodies carry %2 = %0 (a Let { Var } alias of the borrowed self). The cycle-55 exemption borrowed_param(var) matched only the param VAR; the alias — the SAME caller-released allocation — tripped the gate.
  • Cure (replace.rs): borrowed_rooted = close_over_let_aliases(func, borrowed params); gate checks !borrowed_rooted.contains(&var) instead of the bare param test.
  • Pin: replacement_admits_borrowed_user_drop_param_alias (borrowed Guarded param + Let-Var alias + is_shared read → Replaced). RED pre-cure (left: Fallback / right: Replaced); GREEN post-cure; revert-proof RED when the closure is neutered to an empty seed.
  • Gates: ori_arc lib 2077 green; clippy 0; drop_augment aot 32 pass under the gated probe; guardrail 61 FAIL COUNT 0; census 18 tests/spec 10139 replaced / 0 fallbacks, FAIL-name-set + 77-skip set byte-identical to census 16.
  • Post-cure family census: drop/eq/hash/scoped self-alias declines DRAINED (drop_dead_heap_field_struct_still_runs_user_drop fully CLEAN). Remaining: 18 main fns with heap user-drop LOCALS, 1 recursive-drop drop, 1 eq, 1 scoped try-operator.
  • Cycle-62 target (RCA grounded): main-fn heap user-drop locals show all_classes_clean=true, planned_ops=1 — the collection root gets the whole-var Dec while the user-drop locals are CONSUMED INTO it (Construct args, ownership transferred; PV-4 CONSUME events). Gate demands per-var own Dec; cure = admit a user-drop var whose class carries a covering EventKind::Consume discharge (owner’s release chain runs the drop glue recursively).

Cycle 62 — consume-covered exemption drains the main-fn heap-user-drop-local family

  • Target sub-shape: 18/21 drop_augment fixtures declining on function="main" — heap user-drop locals in main-like fns.
  • RCA (DBG trace + ORI_DUMP_AFTER_BURDEN): the locals’ classes discharge via Consume events (ownership transfers into an owning Construct chain — struct/list roots carrying the whole-var planned Dec); all_classes_clean=true, planned_ops=1. The gate demanded a per-var own Dec the transfer discipline never owes — the owner’s recursive drop glue runs each consumed value’s @drop.
  • Cure: consume_covered var set threaded classification → ClassLedgerAnalysis → gate (ledger_events/{types,mod}.rs, class_ledger/{mod,replace}.rs). A var whose WHOLE-VAR node’s class carries a Consume event is exempt; field-path views excluded via is_whole_var() (a consumed field view must not cover its container); class-level rep matching is PV-1-sound (same class = same allocation).
  • Pin: replacement_admits_heap_user_drop_locals_consumed_into_owner (Logged→Resource→List Construct chain, scalar return). RED pre-cure (fallback user-drop-glue — probed via fallback_reason); GREEN post-cure; revert-proof RED when the exemption is neutered.
  • Gates: ori_arc lib 2078 green; clippy 0; drop_augment aot 32 pass gated; guardrail 62 FAIL COUNT 0; census 19 tests/spec 10139 replaced / 0 fallbacks, FAIL-name-set + 77-skip set byte-identical.
  • Post-cure family census: 18/21 fully CLEAN (was 1/21). Remaining 3 decliners: recursive owned-self @drop (boxed enum), map-eq (eq+main), map-insert (main: Boom local aliased and passed [borrow] to @insert — borrowed-store RL-1 duplication, Read not Consume; own-release path is the next RCA).

Cycle 63 — REVERTED: class-rep Dec coverage admitted a booking-gap shape

  • Attempt: replace the gate’s per-var var_has_own_dec with class-rep Dec coverage (an alias-placed release frees the same allocation) to drain the 2 map-fixture declines.
  • Teeth: drop_augment gated 30/32 with the cure (was 32/32) — drop_map_value_let_bound_released_after_insert + drop_map_both_channels_let_bound_structs regressed: @drop fired BEFORE the post-insert marker and the unwind skipped it.
  • RCA: the classification books the borrowed @insert value arg as plain Read — the local is [Aggregate] repr, VALUE-copied into the map. Legacy emits RcDec %7 [AggFields] at the SAME slot: field-walk-only, NO user @drop (the obligation moves to the STORED copy at teardown). The replacement’s whole-var Dec ran drop glue — wrong STRATEGY, not wrong placement.
  • DO-NOT-RE-TRY: never admit a user-drop var via class-release coverage while the class books a borrowed-store arg as Read. Real cure surface: the plan must express an AggFields-only release for a copied-out aggregate (the PV-6 consume-mark re-booking applied to borrowed-store value copies). Reverted to c693b450d blobs; 32/32 restored.

Cycle 64 — borrow-view closure drains the recursive-@drop decline

  • Target: drop_enum_boxed_recursive_drop_panic_recoverable_frees_payload (fn drop declining). RCA: the @drop body’s match arms bind user-drop-typed FIELD VIEWS (%12 = Project %1.2, the next: payload) — TF-4 borrows of the caller-owned allocation tree; the legacy walk emits zero ops for them; the class model plans nothing. Pure gate conservatism (the cycle-61 closure followed Let aliases only).
  • Cure (emit.rs + replace.rs): close_over_borrow_views — the borrowed-rooted closure follows Let aliases AND Project hops; seeds unchanged (Borrowed params).
  • Pin: replacement_admits_borrowed_self_user_drop_field_view (borrowed self + alias + user-drop field view + read). RED pre-cure (user-drop-glue); GREEN post-cure; revert-proof RED via empty-seed neuter.
  • Gates: ori_arc 2079 green; clippy 0; drop_augment 32/32 gated; guardrail 64 FAIL COUNT 0; census 20 tests/spec 10139 replaced / 0 fallbacks (byte-identical name-sets). Commit c86fe8072.
  • Family: FULL 38-id re-census under the current tree — 36/38 CLEAN (all 12 predicate_stack_probe dead-no-use shapes, recursive_drop, tagless_enum, template_str_chain, the ir_quality_loops while-continue single, and 19/21 drop_augment). Remaining 2: the map-fixture AggFields shapes (correctly declining per the cycle-63 dead-end). Fail-loud re-land stays blocked until a same-cycle all-surface ZERO census.

Cycle 65 — RL-DROP §8.1.1 copy-out calculus (f05cbbaf7)

  • The 2 remaining map-fixture declines needed a calculus extension first (§CP-1): a drop-glue aggregate VALUE-copied into a still-live container has its death point at the CONTAINER’s teardown. LLVM forensics: legacy’s local dec is coalesce-absorbed into the teardown walk; the sole _ori_Boom$drop invoke sits in the cleanup region; the dead-local control proved direct [AggFields] decs DO run @drop — the distinguisher is copy-out, not emitter order.
  • Scratch Lean (§CP-4) discharged, landed as AimsProof.Realization §8.1.1: RLDROP_copyout_exactly_once, RLDROP_copyout_local_death_double_drops (the cycle-63 regression as a rejected witness), RLDROP_copyout_balanced. RL-DROP.proof P4 + aims-rules.md copy-out clause synced; lake build + check-proofs + sync-aims-spec clean.

Cycle 66 — copy-out booking drains the LAST declines; census ZERO everywhere

  • Cure (class_ledger/{mod,replace,tests}.rs): copy_out_store_args (borrowed insert arg + MapLiteral/SetLiteral receiver-definer + user-drop arg type; list.insert MOVES so name-only marking would UAF) → apply_copy_out_rewrite (class-rep whole-var Decs → fields-only DecPartial{skip:[]}) → gate + shape-check admission scoped to copy_out_covered.
  • Pin replacement_admits_map_insert_copy_out_user_drop_local (asserts Replaced + the empty-skip partial in the applied body); revert-proof RED.
  • Gates: ori_arc 2080 green; clippy 0; drop_augment 32/32 gated (both map fixtures REPLACE with the correct observable order); guardrail 66 FAIL 0; census 21 tests/spec 10139/0 (identical name-sets), tests/aims 0, tests/run-pass 0; the 38-fixture family reads ZERO decliners.
  • Measurement lesson (third recurrence): grep -c on raw colored build output produced 3 phantom decliners; every census now strips ANSI before grepping.
  • The cycle-60 DO-NOT-RE-TRY precondition is now MET (same-cycle all-surface zero census). Next: cycle 67 re-lands fail-loud (the assert becomes the standing census), unblocking increment 2 (legacy-walk deletion).

Cycle 67 — fail-loud re-land, scoped to the burden-sole path

  • With the cycle-66 all-surface zero census, fail-loud re-landed: apply_class_ledger_replacement asserts Replaced when Step-4b emission is live AND the compile is on the burden-sole path (on_burden_sole_path()), naming the function + failed gate. The unscoped form ICEd the DEFAULT (coexistence) leg — the retiring predicate-stack path changes upstream IR shapes and declines shapes the sole path replaces; it retires with the walk, so the assert gates the path of record only.
  • The silent-fallback pin retargeted: class_ledger_declined_function_falls_back_on_default_path (default leg); the sole-path ICE is pinned end-to-end by the gated aot corpus (every compile runs the assert).
  • The assert immediately EARNED ITS KEEP: 5 real decliners surfaced that the CLI-probe censuses had been mismeasuring (stale-binary/stale-context reads) — the CLI census methodology is DEPRECATED; the assert is the only census.

Cycle 68 — assert-driven drain of the last 5 shapes; corpus at ZERO

  • Tagless payload views (tagless_enum ×2): pure-seed extraction-funding books are runtime-grounded BY CONSTRUCTION (every owed entry = an emitted seed Inc) — multi-owed dead edges release one front dec per funded reference.
  • @eq(self [own], other [own]) impl methods (both map fixtures): owned-param alias-dec coverage — the param’s Let-alias closure member carrying the whole-var planned Dec covers the param. Structural lineage only; DISTINCT from the reverted rep-level surface (no store-booked classes).
  • while (continue) diverging fn: vacuous-unreachable verdict — a class whose every walk item sits in entry-unreachable code is Clean (no_terminal_verdict).
  • catch-arm dead extracts (template_str_chain): a seed funds only a LIVE extract — Err(e) arms that never read e stay unseeded; liveness follows Let aliases AND Jump-arg → block-param hand-offs (live_seeds).
  • Verdict: gated aot suite 2958/0 UNDER THE LIVE ASSERT — the class-ledger fallback census reads zero with the census now structural, not sampled. ori_arc 2080 green; clippy 0.
  • Unblocked next: increment 2 — delete the legacy burden walk (emit_unified Phase 6.5–6.98 repairs + burden_lower ownership scans + ~40 ORI_DISABLE_* toggles + decide.rs island), each deletion its own cure cycle.

Cycle 69 — legacy walk + repair passes DELETED (increment 2 landed)

  • Fail-loud gate UN-SCOPED (both paths): cycle 68’s suite-vs-CLI divergence was a stale-measurement artifact; the 5 default-leg decliners drained, so the burden-sole scoping came off and any decline ICEs everywhere. The declined-fixture pin retargeted to #[should_panic(expected = "class-ledger replacement declined")] (no env dependence — the assert is unconditional).
  • Deleted (d06aa9353, 58 files, +393/-24295): the emit_unified fallback branch (12065 → 1243 lines; unreachable! guard at the seam), module trees realize/transfer_anchor_net{,.rs} + emit_rc/{edge_cleanup,take_project,trampoline}, 286 dead lib items + ~3700 dead test lines (iterative cargo-json dead_code fixpoint purge), 16 stale ORI_DISABLE_* registrations (118 → 102; check-debug-flags.sh clean), and the consumer-less return_payload_contains_param_all_paths ParamContract plumbing (sole consumer was the deleted 6.99 wrapped-anchor admission).
  • Phase 6.99 survivorship honored: the shared compute_burden_entry_nets net engine survives (verify_class consumer); the apply_transfer_anchor_credit_net REPAIR was the deleted part. cleanup_redundant survives pipeline-called (its empirical keep/delete decision belongs to the 7-site collapse sibling).
  • Coexistence pins retargeted: the 7 apply_alias_coverage ORI_DISABLE_BURDEN_OPS=1 byte-identical/baseline-leaks pins now assert FAIL-LOUD (disabling Step-4b logical event placement leaves the current compiled-counter adapter without its validated input; the toggle is a negative-pin probe, never a build mode). Registration + arc.md docs synced.
  • Tooling cure shipped same commit: check-debug-flags.sh died at its first stale flag (set -euo pipefail + zero-match grep exits 1 inside $( | wc -l)); || true on the two count pipelines makes stale flags reportable.
  • Comment hygiene: all attributions to the deleted passes (Category-2/deadAtSucc conjunct, edge_cleanup.rs, transfer_anchor_net) rewritten to the class-ledger per-edge placement; the four-producer narrative in cleanup_redundant.rs corrected; emit_rc module list synced.
  • Verdicts: gated aot 2958/0 (byte-identical to the cycle-68 baseline with 24k lines deleted); ori_arc 1939/0 (post-purge count; dead tests removed); clippy 0; full test-all failure set BYTE-IDENTICAL to baseline (rust_workspace 4 known independents, interp 24 / llvm 223+147lc standing floor).
  • Remaining for the section: w-fbd52b50 (the Default==former-gated contract-phase checkpoint) is the sole live item; the 7-site collapse landed earlier at 5740ac9a8 (w-7f90818e done) and w-e3f5a409/w-36a7f205/w-86d3b2a0 are abandoned-as-superseded. Checkpoint legs in flight: guardrail —floor DEFAULT green (FAIL 0, no baseline delta); rc-remarks two-build diff pre=f15ba1298 vs post=d06aa9353 over the 2276-fixture aot corpus (worktree-reconstructed pre binary + explicit ori_rt staticlib build - E5005 lesson: cargo build -p oric alone omits libori_rt.a).

Checkpoint w-fbd52b50 — legs 1+4 GREEN; pushed forward on the floor legs

  • Leg 1 (guardrail —floor, default build == gated build since ori build auto-composes burden-sole): FAIL COUNT 0, E5005-aborts 0, NEW vs baseline empty, STALE empty.
  • Leg 4 (rc-remarks two-build diff, pre=f15ba1298 vs post=d06aa9353 over ALL 2276 aot fixtures): exit-code sets byte-identical; remark file sets identical; 487 remark lines per side; ori-rc-remarks --diff = 0 regressions, 0 improvements, 128 persisted survivors. The cycle-69 mass deletion is per-op inert — the strongest available proof it was pure dead-code removal. Methodology: worktree-reconstructed pre binary (explicit cargo build --release -p ori_rt — oric alone omits libori_rt.a, E5005), both sides emitted under ORI_DISABLE_PREDICATE_STACK_RC=1 with per-fixture JSONL then sorted concatenation. Streams preserved at scratchpad pre.jsonl/post.jsonl for the session.
  • Legs 2-3 (full test-all green debug+release; parity/leak legs): BLOCKED BY NAME on the standing spec floor — ori_interp 24 fails + ori_llvm 223 fails + 147 lcfail + 4 filed independent rust_workspace bugs (BUG-02-090/091, BUG-03-014/015 family). Folding/fixing that floor IS the next section’s charter (s-42f7f01f floor-closure-bug-fold), so the checkpoint relocates there per the verify-first push-forward route (INV-5 relocate-past-blocker) — its aggregate legs become meaningful exactly when the fold completes.

Close-out reviews — TPR clean; hygiene round 1 + confirmation sweep both test-gate-clean

  • Code TPR: exit_clean (round summaries recorded at the section’s review pipeline; adjudicated over the cycle-69 arc).
  • Hygiene round 1: 92 fixes committed at 106a7b89e.
  • Hygiene confirmation sweep (rails run 1783812076-d9be9257 over d06aa9353^..106a7b89e, committed after cd50ba5b5): lint 33 wrapper-py prose fixes; B2 9 stale-”legacy” mislabels renamed to burden-op vocabulary (burden_ops_enabled, BurdenEmissionDisabled) incl. a factually-stale panic message; B3 deleted the dead uniqueness-summary chain end-to-end (run_uniqueness_analysis, UniquenessSummary/UniquenessMap, to_uniqueness_summary, the threaded-unused pipeline params) across ori_arc/ori_llvm/oric; B4 2 module-org fixes (pipeline mod-decl order; debug_flags index purified); B5 10 stale deleted-symbol citations corrected (aot probes, methods.rs docs, aims-proof checker + RL-4 proof “shipped site” pointers re-aimed at class_ledger emit); md-prose 2 (arc.md mission-restatement + rationale tail); B6 14 (12 more stale proof-checker citations + project_aliases rewrite + a debug_assert_eq! making the class-ledger-sole-emitter dispatch invariant explicit); critic 8 (class_ledger 500-line-cap splits: mod->copy_out, replace->placement, emit->merge_equalize, events->full_move, hazard 5-way; intern_name_set SSOT collapse of 8 duplicate accessors; 3 fused doc-comments re-homed). CONVERGENCE: converging; close test-gate regressed: false (full run 2026-07-11T23:24Z: aot 2958/0, doctest passed, floor byte-stable).
  • Known residual surfaced honestly by the sweep (pre-existing over-cap files the arc SHRANK but did not bring under 500 lines): contract/mod.rs, alias_flow.rs, state_map.rs, post_convergence.rs, project_aliases.rs, emit_unified.rs, ir/mod.rs, burden_lower/mod.rs, borrowed_invoke_lineage.rs, scan_helpers.rs, scan_orchestration.rs — owned by the recurring hygiene-sweep cadence (learning-ledger §14) as the arc’s follow-on splitting tail.

Fresh intel (regenerated)

S08 is no longer a prospective deletion. The current graph and plan state show that the cutover landed: predicate_stack_rc_disabled has no indexed symbol, the old decide/decide_last_use/decide_reuse API is absent, and the live production emission chain is now realize_rc_reuse -> emit_rc_unified -> {lower_burden_ops_to_rc, finalize_rc_emission}. The section body records the corresponding deletion commit and a pre/post RC-remark stream with identical remark sets and zero regressions.

The important result is architectural, not textual. [JOIN] The absence of the legacy symbols, the single production caller of emit_rc_unified, the empty targeted MISSING_ABSTRACTION tier, and the completed section state jointly support one canonical emitter. They do not authorize further broad deletion: the graph still shows live annotation, alias-class, cleanup, and ownership-analysis callers around the canonical path.

Decisions this dossier forces:

  1. Treat emit_rc_unified, lower_burden_ops_to_rc, finalize_rc_emission, the Phase-2 annotation functions, alias-class materialization, and cleanup_redundant_project_alias_decs as surviving architecture, not predicate-stack residue.
  2. Judge future RC changes against the default path and the --emit-rc-remarks stream. Do not recreate a fallback emitter or a shadow scan path. This is required by SSOT-01, SSOT-18, SSOT-19, and DESIGN:mission-misalignment.
  3. Keep the cutover fail-loud. A future class-ledger decline must be a compilation failure naming the reason, never a silent route to a second emitter. This is required by SSOT-13, PHASE-30, PHASE-33, PHASE-37, and FLOW-32.
  4. Preserve production-path coverage. Direct test-call edges are sparse for the orchestration symbols, so AOT, default-build, leak, parity, and RC-remark checks remain the meaningful pins under TEST-14 and COVER-02.
  5. Use the current survivor causes as the next optimization worklist, not as evidence against the cutover: 112 ingested survivors are attributed only to burden_inc_kept_by_whole_var_disposition, split across locality (76) and cardinality (36).
["emit_rc_unified", "lower_burden_ops_to_rc", "finalize_rc_emission", "compute_ssa_alias_classes", "ensure_singleton_class", "materialize_payload_edge_classes", "decide_annotations", "decide_cow", "decide_drop_hint", "AnnotationSiteContext", "cleanup_redundant_project_alias_decs"]

VERDICT: S08 achieved its single-logical-planner/current-compiled-adapter cutover contract. The downstream risk is no longer incomplete deletion; it is accidentally classifying retained class-ledger support as legacy residue, reintroducing an alternate ownership calculus, or letting a physical adapter infer policy. Multiple validated physical emitters remain required. Any design on this terrain must satisfy SSOT-19, PHASE-33, PHASE-62, FLOW-32, TEST-14, and COVER-02.

DIG DEEPER

scripts/intel-query.sh status
scripts/intel-query.sh plan-status aims-provenance-ledger
scripts/intel-query.sh symbols predicate_stack_rc_disabled --repo ori
scripts/intel-query.sh callers emit_rc_unified --repo ori
scripts/intel-query.sh callees emit_rc_unified --repo ori

(full dossier: predicate-stack-deletion—s-ee6e96e4.intel.md)