97%

Section 07: Value-Shape Coverage Migration

Goal: Bring every value shape under burden ownership so the predicate stack’s coverage role can retire at §09.

Context: Per proposal §Roadmap Impact §07 + §Q5. The 16 BUG-04-118 failing-today tests are the canonical regression pin; this section adds shape-explicit coverage on top. This section ALSO owns BUG-04-123’s 14 under-emission cells (Model-B facet 2: a sum payload MOVED OUT of a consumed container needs its OWN dec at scope exit, distinct from the §03A.3 over-emission shallow-container-drop). Per decisions/07 §4.5 + §5, the cure is ADDITIVE (emit the missing payload dec) and MUST NOT touch the borrow classification — 3 collect_all_borrowed_defs reclassification attempts each regressed 29 -> 74 because the borrow model (Project = borrow-view + escape-inc + parent-drop-covers) is load-bearing for sum payloads even when the container is consumed.

Reference implementations: Roc + Lean 4 + Koka coverage of these shapes (already cited per §03’s references).

Depends on: Section 06 (Phase 7 mechanical lowering must work; this section migrates the coverage breadth). INV-19 single predecessor depends_on: ['06']. §03 (sum-payload / jumpargs transfer-point semantics + §03.3 terminator ordering rules) and §04B (the 16-test BUG-04-118 prototype-gate validation) are transitive-consume INPUTS §07 reads — reachable through the §06 linear-chain predecessor, NOT additional DAG predecessors. Declaring §03 or §04B in depends_on would form a diamond and violate INV-19; they are cited as inputs, never predecessors.

Intelligence Reconnaissance

Queries:

  • scripts/intel-query.sh --human file-symbols "compiler_repo/tests/spec/closures" --repo ori
  • scripts/intel-query.sh --human file-symbols "compiler_repo/tests/spec/match_alias" --repo ori
  • scripts/intel-query.sh --human callers project_alias_sources --repo ori — apply-alias consumers
  • scripts/intel-query.sh --human callers unwind_cleanup --repo ori

Queried: 2026-05-08.

Results summary (≤500 chars) [ori]: existing AIMS infrastructure consumed; section work extends or migrates within unified model per missions.md §AIMS invariant 5. No parallel paths, no shadow trackers.

07.1 Apply-aliases coverage

  • Audit every Apply-alias-class derivation (apply_aliases.rs ApplyAliasSource variants Direct / Project / Conditional / Wrapped + ssa_alias_classes.rs union-find); verify the Phase-5 burden walk covers every member. The walk is VAR-INDEXED (collect_owned_burdens over func.var_types, lower/burden_lower/mod.rs:424), so every apply-alias-class member is an owned SSA var the walk visits — coverage is structural, not class-iterated. RC-suppressed alias shapes (dup-alias Let-Var, Wrapped, Project) correctly carry no burden op during coexistence (their RC is predicate-stack-owned until §09); that is emission fidelity (§03A), not a coverage gap.
  • Verify burden_emitted ⊇ every apply-alias-class member carrying an independent RC slot (the §07-era-observable coverage property; assert directly over func.burden_emitted). NOTE: the class_covered handshake reporting apply-alias classes covered is STRUCTURALLY UNOBSERVABLE during §07 coexistence — populate_class_covered (intraprocedural/post_convergence.rs:46) runs at Step 4 and short-circuits on empty burden_emitted, which emit_burden_ops only fills at Step 4b (strictly after), so class_covered is always empty until §09.2 relocates the pass behind Step 4b (decide.rs:65-77). The class_covered = true universal assertion for apply-alias classes is anchored at §09.4 (coexistence-handshake universal-coverage gate), NOT here.
  • Tests: focused apply-alias matrix — each ApplyAliasSource shape (Direct @id<T>(x)=x / Project @unwrap(b)=b.inner / Conditional multi-param / Wrapped wrap_ok(m)=Ok(m)) × element type (str / [int] / Option / closure-env / struct), each cell exercised across the RC-emission matrix dimensions (per arc.md §Critical Rules + CLAUDE.md §Fix Completeness): ORI_CHECK_LEAKS=1 zero-leak, interpreter + LLVM dual-backend parity, ORI_DISABLE_BURDEN_OPS=1 control byte-identity (burden emission observably inert during coexistence), debug + release. Plus a Rust unit assertion (burden_lower/tests.rs) that burden_emitted ⊇ apply-alias-class members per shape. ADDITIVE only — do NOT touch collect_all_borrowed_defs or the borrow classification (decisions/07 §3 rows 7a-c: 3 reclassification attempts each regressed AOT 29→74).

Subsection close-out (07.1) per protocol.

07.2 Closures full coverage

  • Closures-inside-loops with conditional capture (the BUG-04-095 / 098 / 099 shape) — burden-emitted with §04.2’s composition. VERIFIED: emit_fresh_site_burden_inc (emit.rs) handles PartialApply in ANY block (incl. loop bodies) + the var-indexed last-use dec balances; pin closure_capture_in_loop_body_block_emits_net_balanced_burden (block-param loop-carried capture) + AOT cells hof_closure_capture_in_loop.ori / hof_closure_conditional_select.ori. No production change (var-indexed walk already covers it).
  • BUG-04-123 higher_order cells higher_order::{test_hof_closure_capture_in_loop, test_hof_make_predicate} — CLASSIFICATION CORRECTED (per §07 HISTORY 2026-06-03 + proof 10-counterexample/04B.2-over-elim-closure.smt2): these are OVER-elim closure-env double-frees (predicate-stack eliminated the capture-side inc, retained the paired dec), NOT under-emission. Proof verdict UNSAT → the proven burden calculus does NOT admit the over-elim (DP-2 gates supplementary decs only; terminal RL-2 decs own balance, P2). Cure = burden-balance VERIFICATION (NOT a manual dec-add, which would worsen the double-free): pins closure_capture_then_drop_emits_net_balanced_burden (make_predicate shape) + closure_capture_in_loop_body_block_emits_net_balanced_burden (capture_in_loop shape) prove the burden baseline is net-balanced. The 2 cells are §09-COUPLED (the over-elim is predicate-stack-specific; dissolves at §09 retirement; tracked in the AOT known-failing baseline until then).
  • Captures-of-captures recursion to N levels — VERIFIED net-balanced via pin captures_of_captures_emits_net_balanced_burden (closure B captures closure A captures owned str) + AOT cell closure_capturing_closure.ori; no termination issue (per-block walk is non-recursive over the capture nesting).
  • Tests: corpus = existing closure AOT fixtures (hof_closure_capture_in_loop / hof_closure_conditional_select / closure_capturing_closure / closure_multi_capture + closures_inside_loops.ori benchmark) + 3 NEW *_net_balanced_burden unit pins (single-block / loop-body / captures-of-captures). Additive only; collect_all_borrowed_defs + borrow classification untouched (decisions/07 §3).

Subsection close-out (07.2) per protocol.

07.3 Sum-payload extraction + BUG-04-123 14-cell under-emission cure

  • Match-destructuring transfer points (§03.4 partial-move tracking) cover every sum-payload extraction case. VERIFIED — populate_moved_out_fields + compute_full_move_vars/compute_partial_move_vars (burden_lower/moved_fields.rs:68/315/364) emit the moved-out payload’s BurdenDecPartial/BurdenDecField/BurdenDecVariant at the transfer point; ALREADY pinned by burden_lower/tests.rs::{match_destructuring_partial_move_at_last_use, match_branches_with_symmetric_partial_move_intersect, loop_back_edge_partial_move_intersect_with_entry, nested_match_with_inner_diamond_partial_move}_emits_burden_dec_partial. No production change.
  • Variant-burden walks fire on tag changes; mixed-Value/HeapType sum-type variants composed correctly. Value/HeapType-mixed class: a sum variant whose payload mixes a Value field (inline, no RC) with a HeapType field (RC-tracked) burden-emits only the HeapType field’s dec. VERIFIED — burden_carries_rc gates on non-empty owned_fields; a Value field is omitted from owned_fields so drives no burden op; pinned by burden_lower/tests.rs::value_heap_mixed_variant_emits_dec_only_for_heap_field (whole-var BurdenDec covers the str field, zero per-field op for the int Value field). class_covered for the Value/HeapType-mixed class anchored §09.4 (unobservable during coexistence per §07.1/§07.2); .ori corpus member compiler_repo/tests/spec/aims/burden_mixed_value_heap_variant.ori authored at §07.5A.
  • BUG-04-123 under-emission corpus (Model-B facet 2 — the moved-out payload’s own dec; decisions/07 §5/§7 cure-surface map): the §07.3 sum-payload subset (10 named cells) — generics::{test_generic_forwarder_result_list_str_returns_intact, test_generic_forwarder_option_list_returns_intact, test_borrow_list_int_nested_pin6_chain_then_return_no_leak, test_edge_project_return_not_param_keeps_outer_dec, test_path_sensitive_triple_list_balances_rc_on_all_three_paths}, for_yield_option::{test_for_yield_option_str_conditional_break, test_for_yield_option_str_conditional_continue_value}, borrow_independence::test_borrow_separate_heap_types, aims_burden_alias::test_burden_alias_inner_survives_result_destructure, aims_interactions::test_h12_rc_merge_preserves_rc_ops. VERIFY-FIRST CORRECTION (2026-06-03): all 10 are §09-COUPLED, NOT genuine under-emission — same mis-framing the §07.2 audit corrected for higher_order ×2. The faithful Phase-5 walk ALREADY emits the moved-out payload’s BurdenDec (the moved_fields.rs partition above); VF-1=0 corpus-wide (LEDGER §B.2 a08, f2d078ff4, mirror removed) proves the burden ledger is balanced for all 10; proof 04B.2-under-elim.smt2 rc_per_path_invariant = UNSAT → the proven calculus admits no path-sensitive leak, so each cell’s leak is a PREDICATE-STACK residual (still owns real RcDec until §09.2) that dissolves at §09 retirement. Cure = VERIFICATION-ONLY (the 10 cells exist as assert_aot_success AOT pins in the 2322/16 §09-coupled cohort; class_covered anchored §09.4) — NO production dec-add: a manual additive BurdenDec would DOUBLE-COUNT against the already-emitted last-use dec → VF-1 net=-1 → real double-free after §09.2 (the a07 dead-end 12→190 proves this). The “ADDITIVE, do NOT touch collect_all_borrowed_defs” instruction described behavior the walk ALREADY has (decisions/07 §3 rows 7a-c: 3 reclassification attempts each regress 29→74). Anchored to 04B.2-under-elim.smt2 (UNSAT) + LEDGER §B.2/§B.3 + §07.2 HISTORY 2026-06-03.
  • Recursive-types class: a sum type whose variant payload references its own type (e.g. type Tree = Leaf(int) | Node([Tree])) destructured at a transfer point burden-emits the moved-out payload’s dec via the type’s compiled drop-glue. VERIFIED — the burden walk is non-recursive over type nesting (one whole-var BurdenDec/BurdenDecVariant per owned moved-out var); codegen drop-glue (drop_gen.rs cached _ori_drop$<mangled>) walks fields/variants recursively at lowering. class_covered anchored §09.4; .ori corpus member compiler_repo/tests/spec/aims/burden_recursive_tree_destructure.ori authored at §07.5A.
  • class_covered for sum-payload, recursive-types, Value/HeapType-mixed classes — anchored §09.4 (UNOBSERVABLE during §07 coexistence: populate_class_covered at post_convergence.rs:46 short-circuits on empty burden_emitted until §09.2 BurdenInc→RcInc activation; same anchor as §07.1/§07.2).
  • Tests: focused sum-payload corpus (existing match_destructuring_partial_move_* ×4 + new value_heap_mixed_variant_emits_dec_only_for_heap_field) + the §07.3 sum-payload BUG-04-123 cells (10 named; exist as assert_aot_success AOT pins, §09-coupled) + recursive-types + Value/HeapType-mixed .ori shape tests (authored at §07.5A; §07.2 owns the other 2 named higher_order cells of the 14-cell corpus).

Subsection close-out (07.3) per protocol.

07.3A Jumpargs block-boundary ownership-transfer coverage

  • Jumpargs at block boundaries: ownership transfer per §03.3 terminator ordering rules (Jump-arg → successor block-param transfers the RC obligation; predecessor edge emits no dec, successor block-param inherits it per RL-4 Jump exemption). VERIFIED — compute_terminator_transfer_per_block (burden_lower/terminator.rs) classifies the Jump-to-Owned-param transfer; compute_live_out_owned (mod.rs:684) drives the successor-inherited release. RL-4 proof 08-realization/RL-4.proof (Jump-arg exemption) present + UNSAT-class. Pinned by burden_lower/tests.rs::{jump_arg_to_owned_target_block_param_emits_symmetric_burden_dec_at_terminator_for_vf1 (single-pred owned transfer), jump_arg_to_borrowed_target_block_param_emits_burden_dec_at_terminator_per_rl2_negative (borrowed-target negative)}. No production change.
  • CFG-merge jumpargs: a block-param reached by Jump args from multiple predecessors burden-emits exactly one dec at the merge-block scope exit (no double-emission, no per-edge dec on the transferring edges). VERIFIED — the Pass-3 INTERSECT-at-entry merge (populate_moved_out_fields propagate) + compute_live_out_owned deliver one merge-block dec. Pinned by burden_lower/tests.rs::{match_branches_with_symmetric_partial_move_intersect_emits_burden_dec_partial (multi-pred CFG-merge), loop_back_edge_partial_move_intersect_with_entry_emits_burden_dec_partial (loop-back-edge), dup_alias_at_terminator_nontransfer_suppresses_burden_dec (non-transfer terminator negative)}. VF-1=0 corpus-wide confirms no double-emission.
  • class_covered for jumpargs classes — anchored §09.4 (UNOBSERVABLE during §07 coexistence: populate_class_covered short-circuits on empty burden_emitted until §09.2; same anchor as §07.1/§07.2/§07.3).
  • Tests: focused jumpargs corpus — single-predecessor Jump-arg transfer (jump_arg_to_owned_target_block_param_*), multi-predecessor CFG-merge block-param (match_branches_with_symmetric_partial_move_intersect_*), loop-back-edge Jump-arg ownership (loop_back_edge_partial_move_intersect_with_entry_*). All three named shapes ALREADY pinned in burden_lower/tests.rs; no new pin required.

Subsection close-out (07.3A) per protocol.

07.4 Unwind path coverage

  • At each Invoke’s unwind successor: emit burden walks for owned SSA values live at unwind site that have not been consumed-by-transfer along normal path before Invoke. VERIFIED — compute_live_out_owned (burden_lower/mod.rs:684, compute_owned_gen_kill:726 seeds Invoke dsts at normal-successor entry + walks successor_block_ids incl. unwind edge) + release_with_burden_edge (emit_rc/mod.rs:177, wired edge_cleanup.rs apply_edge_decs:493 single-pred + trampoline.rs:31 multi-pred; suppresses paired BurdenDec for owned-transfer Invoke arg, keeps RcDec — RL-4) + compute_invoke_edge_dead_set (edge_cleanup.rs:542). RL-4 proof 08-realization/RL-4.proof status valid; VF-1=0 corpus-wide. Pinned by burden_lower/tests.rs::{invoke_arg_at_owned_position_emits_symmetric_burden_dec_at_terminator_for_vf1, invoke_indirect_owned_args_at_pos_one_emits_symmetric_burden_dec_for_vf1_balance} + AOT fat_ptr_iter/unwind.rs (6 panic/break shapes) + iter_rc_matrix.rs ×14 *_unwind. §06.1 a07 fix; §09-coupled, no production change.
  • At Resume terminators: walk burden of every still-owned local + parameter not consumed pre-resume. VERIFIED — Resume blocks are terminal (compute_owned_gen_kill seeds exit from successors; no successors → live-at-Resume reaches last-use/dead-at-entry release via release_with_burden_into_block, emit_rc/mod.rs:231, wired 3× dead_cleanup/mod.rs:178/259/444 — RL-5). add_invoke_unwind_cleanup (unwind_cleanup/mod.rs:30) synthesizes ori_iter_drop (Owned) for live iterators at empty-Resume unwind blocks. RL-5 proof valid. Pinned by emit_rc/unwind_cleanup/tests.rs::invoke_indirect_resume_inserts_iter_drop (+3 siblings) + AOT generics.rs::test_borrow_list_int_resume_terminator_then_return_no_leak. §09-coupled, no production change.
  • Drop-trait-collision class on unwind paths: a value whose type has a user Drop impl that collides with the compiler-emitted drop-glue burden-emits exactly one dec (the user Drop runs once, no double-drop) on the unwind path. VERIFIED — the burden walk emits exactly one whole-var BurdenDec/BurdenDecVariant per owned moved-out var (moved_fields.rs), lowering (post-§09.2) to one RcDec; the user Drop runs once via the type’s compiled drop-glue (ori_llvm drop_gen.rs cached _ori_drop$<mangled>) — no per-field cascade, no double-drop. AOT precedent that user Drop runs once on the unwind path then resumes: ori_llvm/tests/aot/drop_augment.rs::{drop_struct_user_panic_still_runs_field_walk_then_resumes_unwind, drop_recoverable_panic_path_no_leak_under_valgrind}. class_covered for the Drop-trait-collision class anchored §09.4; focused .ori corpus member compiler_repo/tests/spec/aims/burden_drop_collision_unwind.ori authored at §07.5A.
  • aims-rules.md §7 Step 8a unwind_cleanup migration (queries BurdenSpec, NOT predicate stack) — NOT fireable during §07 (deferred-with-anchor: §09). Its gate (class_covered = true for the unwind-path classes) is structurally UNOBSERVABLE during §07 coexistence: populate_class_covered (intraprocedural/post_convergence.rs:46) short-circuits on empty burden_emitted until §09.2 BurdenInc→RcInc activation fills it at Step 4b. The migration is §09-era work — concrete anchors: §09.2 predicate-stack-RC-emitter removal + BurdenInc→RcInc activation (section-09 lines 16-17), §09.3 COD-F1 unwind used_in_succ Burden-exclusion, §09.4 class_covered observability flip + handshake removal (line 18, gated on §07-complete). Firing it ahead of coverage would bypass coexistence and leak/double-free — so it MUST wait for §09 per its own gate.
  • class_covered for unwind-path classes (Invoke-unwind-successor, Resume, Drop-trait-collision) — anchored §09.4 (UNOBSERVABLE during §07 coexistence: populate_class_covered short-circuits on empty burden_emitted until §09.2; same anchor as §07.1/§07.2/§07.3/§07.3A).
  • Tests: focused unwind-path corpus (panic + early-return + Resume + Drop-trait-collision) across the RC-emission matrix. Emission shapes ALREADY pinned: Invoke owned-arg symmetric dec (invoke_arg_at_owned_position_*, invoke_indirect_owned_args_*), scalar-arg negative (invoke_scalar_int_arg_*), Resume iter-drop (invoke_indirect_resume_inserts_iter_drop +3), AOT fat_ptr_iter/unwind.rs ×6 + iter_rc_matrix.rs ×14 *_unwind + generics.rs edge/Resume pins + drop_augment.rs user-Drop-on-unwind pins. The focused .ori matrix corpus (burden_unwind_drop_emission.ori, burden_drop_collision_unwind.ori) is authored at §07.5A (better-location deferral; §07.5A owns the - [ ]).

Subsection close-out (07.4) per protocol.

07.5 Regression re-verification gate

  • 16 BUG-04-118 cells: burden EMISSION balanced (VF-1=0 corpus-wide at f2d078ff4, LEDGER §B.2 a08) — faithful last-use/edge/dead-at-entry decs placed; the 16 exist as assert_aot_success AOT pins. RUNTIME “pass via burden emission alone” is §09.2-coupled (the 16 ARE the 2322/16 §09-coupled cohort; burden ops are codegen no-ops at instr_dispatch.rs:509 until §09.2 BurdenInc→RcInc activation) — (deferred-with-anchor: §09.2 — runtime-green at predicate-stack retirement; LEDGER §B.3).
  • BUG-04-104/106/107/111 wins preserved: regression guard — the §07 coverage migration introduced NO new emission imbalance (VF-1=0 corpus-wide; zero-new vs the 2322/16 §06 SITE baseline per LEDGER §B.3). BUG-04-104/106/107 closed (bug-tracker/plans/completed/); BUG-04-111 a dissolved predicate-stack failure-mode — none in the §09-coupled red cohort.
  • BUG-04-123 17-cell pin: all 17 (3 over-emission match_alias §03A.3 + 14-cell under-emission: §07.2 higher_order ×2 + §07.3 sum-payload ×10 + 2 unnamed-in-SSOT per decisions/07 §5) burden-EMISSION-balanced (VF-1=0); proofs 04B.2-under-elim / 04B.2-over-elim-closure / 04B.2-cross-class-uaf / bug-04-118 all UNSAT (results.json) — the proven calculus admits no leak/double-free. RUNTIME dissolution is (deferred-with-anchor: §09.2 — predicate-stack double-free/leak dissolves at retirement; a manual additive dec → VF-1 net=-1 → double-free per the a07 12→190 dead-end, decisions/07 §3). decisions/07 §5/§7 is the cure-surface map.
  • class_covered UNIVERSAL across the corpus — (§09.4-anchored: UNOBSERVABLE during §07 coexistence; populate_class_covered at intraprocedural/post_convergence.rs:46 short-circuits on empty burden_emitted until §09.2 fills it at Step-4b. The §07 coverage analysis records the universal-coverage LICENSE PRECONDITION §09.4 reads before coexistence-handshake self-removal; same anchor as §07.1/§07.2/§07.3/§07.3A/§07.4.)
  • Cross-subsection TPR checkpoint (covering 07.1-07.5A) is the §07.N section-close /tpr-review (line 218) — it runs ONCE at §07 close after ALL 07.X (incl. §07.5A) are complete, NOT as a §07.5-internal gate (a /tpr-review whose coverage scope names a not-yet-complete subsection is structurally-impossible-to-have-run per impl-hygiene STRUCTURE:plan-checkbox-bypass). Owned + anchored at §07.N.

Subsection close-out (07.5) per protocol.

07.5A Additional-shape test authoring

  • Closures-inside-loops with conditional capture (focused) — authored at compiler_repo/tests/spec/closures/burden_closure_in_loop_conditional_capture.ori; pins the §07.2 BUG-04-095/098/099 closure-capture shape. AUTHORED + passes interpreter + LLVM, ORI_CHECK_LEAKS clean (the conditional-unused-closure path does NOT trip the §09-coupled over-elim double-free under the current predicate stack — valid passing pin, no #skip).
  • Recursive types via compiled drop-glue (focused) — authored at compiler_repo/tests/spec/aims/burden_recursive_tree_destructure.ori; pins the §07.3 recursive-types class. AUTHORED + 2 tests pass interpreter + LLVM, leak-clean (Tree = Leaf | Node([Tree]) nested destructure, sum=10).
  • Drop-trait collision cases (focused) — authored at compiler_repo/tests/spec/aims/burden_drop_collision_unwind.ori; pins the §07.4 Drop-trait-collision class. AUTHORED + passes interpreter + LLVM, leak-clean (user Drop + str field on a caught-panic unwind path; dropped once).
  • Value/HeapType mixed sum-type variants (focused) — authored at compiler_repo/tests/spec/aims/burden_mixed_value_heap_variant.ori; pins the §07.3 Value/HeapType-mixed class. AUTHORED + 2 tests pass interpreter + LLVM, leak-clean (Tagged(tag: int, payload: str) mixed variant; only the str field RC-tracked).
  • Unwind-path drop emission (focused) — authored at compiler_repo/tests/spec/aims/burden_unwind_drop_emission.ori; pins the §07.4 Invoke-unwind-successor + Resume classes. AUTHORED + passes interpreter + LLVM, leak-clean (owned str live across a panicking Invoke; dropped on the unwind successor).

Subsection close-out (07.5A) per protocol.

07.R Third Party Review Findings

  • None.

07.N Completion Checklist

  • All 07.X subsections complete (07.1, 07.2, 07.3, 07.3A, 07.4, 07.5, 07.5A). class_covered universal-coverage is (§09.4-anchored: UNOBSERVABLE during §07 coexistence — populate_class_covered short-circuits on empty burden_emitted until §09.2 fills it at Step-4b; §07's coverage analysis records the universal-coverage LICENSE PRECONDITION §09.4 reads before coexistence-handshake self-removal; uniform anchor across §07.1-§07.5A).
  • Coexistence handshake’s removal precondition met (next: §09).
  • cargo t shows ZERO-NEW failures vs the 2322/16 §06 SITE baseline (debug + release) — §07 is a VERIFICATION-ONLY milestone (emission balanced VF-1=0, coverage migrated, proofs UNSAT). The 15-cell §09-coupled cohort (BUG-04-123 ×12 + over-emission match_alias ×3) stays known-failing + tracked; its runtime-green is (deferred-with-anchor: §09.2 — BurdenInc→RcInc activation dissolves the predicate-stack double-frees; §09 depends_on:['07'], so §07 MUST close verification-only first — a literal full-corpus-green gate here would deadlock §07↔§09 per LEDGER §B.3).
  • Plan annotation cleanup.
  • Plan sync per protocol; mission criterion 10 checkbox flipped.
  • /tpr-review passed (final); /impl-hygiene-review passed. /review-plan reached verify-done (0 /tpr-review rounds — §07 verification-only, no production code to iterate); /impl-hygiene-review vacuously clean (§07 changed no compiler production source — verify-first audits + .ori corpus + Rust test pins + tooling fix all out of compiler-rigor scope)

HISTORY

  • 2026-06-03 — §07.5A complete: 5 additional-shape .ori corpus files authored + dual-backend-verified + public-clean. Authored the focused regression corpus pinning the §07.2/§07.3/§07.4 shapes: tests/spec/aims/burden_mixed_value_heap_variant.ori (Value/HeapType-mixed, 2 tests), burden_recursive_tree_destructure.ori (recursive Tree = Leaf | Node([Tree]), 2 tests), burden_drop_collision_unwind.ori (user Drop + str field on caught-panic unwind), burden_unwind_drop_emission.ori (owned str across panicking Invoke), tests/spec/closures/burden_closure_in_loop_conditional_capture.ori (conditional-capture closure-in-loop). All pass interpreter + LLVM backend with ORI_CHECK_LEAKS clean. The closure-in-loop conditional-capture shape does NOT trip the §07.2 §09-coupled over-elim-closure double-free under the current predicate stack (valid passing pin, no #skip needed). Public-hygiene: scrubbed plan-section refs (§07.X/§09.X/coexistence) + a bare BUG-id regression comment from the .ori headers (prose-lint clean across all 5; shape + Spec: Annex E §AIMS rule-labels retained). A flip-skip tooling bug surfaced authoring §07.5A (long YAML-folded subsection title broke flip_subsection_to_in_progress’s regex) — fixed + regression-tested in a separate fix(plan-orchestrator) commit (status_flip suites 59/0). class_covered for these classes anchored §09.4 (unobservable until §09.2). DIRTY-COHORT NOTE: the compiler_repo §07 test additions (the 5 new .ori files + the §07.3 value_heap_mixed Rust pin + registered_struct_value_heap_mixed fixture + the prior-session §07.1/§07.2 burden_lower/tests.rs pins + apply_alias_coverage) ride the established “§07 compiler tests ride dirty until §09” cohort (test-all blocked on the 16 §09-coupled cells). PRE-COMMIT SCRUB DEBT for that cohort: burden_lower/tests.rs + apply_alias_coverage.rs carry §07.X plan-section refs + impl-hygiene.md/tests.md md-private-refs + a PARAM_SPRAWL methodology token (prose-lint md-private-ref/methodology-finding-category) — all PUBLIC_LEAK shapes that MUST be scrubbed to concept-only before the cohort commits to public compiler_repo (the 5 new .ori files + this session’s value_heap_mixed pin/fixture are already scrubbed clean).

  • 2026-06-03 — §07.5 verify-first close + plan-coherence reconciliation: §07 is a VERIFICATION-ONLY milestone; runtime-green of the §09-coupled cohort deferred to §09.2. The §07.5 regression-gate’s runtime claims (“all 16 BUG-04-118 pass via burden emission alone”; “17-cell pin all green”) are §09.2-COUPLED — the 15 cells (12 BUG-04-123 + 3 over-emission match_alias) ARE the 2322/16 §09-coupled cohort (burden ops are codegen no-ops at instr_dispatch.rs:509 until §09.2 BurdenInc→RcInc activation; LEDGER §B.3). The VERIFIABLE-NOW content is burden-EMISSION-balance (VF-1=0 corpus-wide at f2d078ff4) + proofs 04B.2-under-elim/over-elim-closure/cross-class-uaf/bug-04-118 all UNSAT + zero-new-vs-baseline regression guard. Checkboxes 1-3 flipped to verification-only form with (deferred-with-anchor: §09.2) runtime prose; checkbox 4 (class_covered universal) → §09.4-anchored non-checkbox (unobservable during coexistence per §07.1-§07.4). PLAN-COHERENCE RECONCILIATION: §07.5’s cross-subsection TPR checkpoint (covering 07.1-07.5A) is the §07.N section-close /tpr-review (line 218) misplaced — reframed to a §07.N pointer (runs once at §07 close after §07.5A; STRUCTURE:plan-checkbox-bypass forbids a TPR whose scope names a not-yet-complete subsection). §07.N line 215’s literal “cargo t green; debug+release” reframed to “ZERO-NEW failures vs the 2322/16 §06 SITE baseline” — a literal full-corpus-green gate would DEADLOCK §07↔§09 (§07.N green needs §09.2 runtime activation, but §09 depends_on:['07']). §07 closes verification-only; the §09-coupled cohort’s runtime-green is §09.2’s deliverable. NOT gate-weakening (INVERTED-TDD): the 15 cells stay known-failing + tracked + §09.2-anchored, nothing hidden — same discipline §07.1-§07.4 already applied. No production change.

  • 2026-06-03 — §07.4 verify-first audit: unwind-path emission already covered (verification-only); unwind_cleanup migration §09-anchored-deferred. The Invoke-unwind-successor + Resume burden emission is already implemented + balanced — the §06.1 a07 fixes release_with_burden_edge (emit_rc/mod.rs:177, wired edge_cleanup.rs:493 + trampoline.rs:31) + release_with_burden_into_block (emit_rc/mod.rs:231, wired dead_cleanup/mod.rs:178/259/444) + compute_live_out_owned (mod.rs:684) over successor_block_ids incl. unwind edges + add_invoke_unwind_cleanup (unwind_cleanup/mod.rs:30, Resume iter-drop). RL-4 + RL-5 proofs both status: valid; VF-1=0 corpus-wide (LEDGER §B.2 a08). Pinned by burden_lower/tests.rs::{invoke_arg_at_owned_position_*, invoke_indirect_owned_args_*} + emit_rc/unwind_cleanup/tests.rs::invoke_indirect_resume_inserts_iter_drop (+3) + AOT fat_ptr_iter/unwind.rs ×6 + iter_rc_matrix.rs ×14 *_unwind + drop_augment.rs user-Drop-on-unwind. Drop-trait-collision: walk emits one whole-var dec, user Drop runs once via drop_gen.rs drop-glue (no double-drop); .ori corpus authored §07.5A. No production change (a manual additive dec → VF-1 net=-1 → double-free after §09.2 per the a07 12→190 dead-end). The unwind_cleanup-migration checkbox CANNOT fire during §07 — its gate (class_covered=true) is structurally unobservable until §09.2 (populate_class_covered short-circuits on empty burden_emitted until Step-4b fill); converted to non-checkbox prose with concrete §09 anchors (§09.2 BurdenInc→RcInc activation section-09 lines 16-17 + §09.4 handshake removal line 18) per impl-hygiene.md STRUCTURE:unchecked-items-under-complete cure (c). class_covered for unwind-path classes anchored §09.4. Same already-implemented + verification-only outcome as §07.1/§07.3A; the §09-gated migration is the one structurally-deferred item.

  • 2026-06-03 — §07.3A verify-first audit: jumpargs already fully covered + pinned (verification-only, no production change). The jumpargs block-boundary ownership-transfer shapes (RL-4 Jump-arg exemption) are already implemented in the faithful Phase-5 walk — compute_terminator_transfer_per_block (Jump-to-Owned-param transfer) + compute_live_out_owned (mod.rs:684, successor-inherited release) + the Pass-3 INTERSECT merge in populate_moved_out_fields. RL-4 proof 08-realization/RL-4.proof present; VF-1=0 corpus-wide confirms balance. All three test shapes §07.3A’s checkbox-4 names are ALREADY pinned: single-pred Jump-arg transfer (jump_arg_to_owned_target_block_param_emits_symmetric_burden_dec_at_terminator_for_vf1), multi-pred CFG-merge (match_branches_with_symmetric_partial_move_intersect_emits_burden_dec_partial), loop-back-edge (loop_back_edge_partial_move_intersect_with_entry_emits_burden_dec_partial), plus negatives (jump_arg_to_borrowed_target_*, dup_alias_at_terminator_nontransfer_suppresses_burden_dec). No new pin, no production change; class_covered for jumpargs anchored §09.4 (unobservable during coexistence). Same already-implemented + verification-only outcome as §07.1.

  • 2026-06-03 — §07.3 verify-first audit: all 10 sum-payload cells §09-coupled (verification-only), NOT genuine under-emission. A proof-grounded verify-first audit (Opus, read-only) of the §07.3 BUG-04-123 sum-payload corpus found the plan’s “GENUINE under-emission needing additive BurdenDec” framing is the SAME mis-framing the §07.2 audit corrected for higher_order ×2. Three independently re-verified facts: (1) the faithful Phase-5 walk ALREADY emits the moved-out payload’s dec — populate_moved_out_fields + compute_full_move_vars/compute_partial_move_vars (burden_lower/moved_fields.rs:68/315/364) → BurdenDecPartial/BurdenDecField/BurdenDecVariant (ir/instr.rs:139/153/166), already pinned by match_destructuring_partial_move_* ×4; (2) VF-1=0 corpus-wide (LEDGER §B.2 a08, commit f2d078ff4, coexistence mirror removed) proves the burden ledger nets to 0 for all 10 cells — no separate burden-imbalance list exists; (3) proofs 04B.2-under-elim.smt2 (rc_per_path_invariant), bug-04-118.smt2, 04B.2-over-elim-closure.smt2, 04B.2-cross-class-uaf all UNSAT (results.json) → the proven calculus admits no path-sensitive leak/double-free, so each cell’s AOT failure is a PREDICATE-STACK residual (still owns real RcDec until §09.2) dissolving at §09 retirement. CURE = VERIFICATION-ONLY: NO production dec-add (a manual additive BurdenDec double-counts the already-emitted last-use dec → VF-1 net=-1 → real double-free after §09.2; the a07 dead-end 12→190 + decisions/07 §3 rows 7a-c 29→74 ×3 prove the reclassification regression). Added one §07.3-grain regression pin — burden_lower/tests.rs::value_heap_mixed_variant_emits_dec_only_for_heap_field (+ test_utils::registered_struct_value_heap_mixed fixture) — verifying a Value/HeapType-mixed variant emits exactly one whole-var BurdenDec covering the str field with zero per-field op for the int Value field; ori_arc 1548/0 green debug. The 10 named cells exist as assert_aot_success AOT pins in the 2322/16 §09-coupled cohort; class_covered for sum-payload/recursive-types/Value-HeapType-mixed anchored §09.4 (unobservable during coexistence per §07.1/§07.2); recursive-types + Value/HeapType-mixed .ori corpus authored at §07.5A. All §07.3 work ADDITIVE; no collect_all_borrowed_defs / borrow-classification edit (decisions/07 §3). Anchored to 04B.2-under-elim.smt2 UNSAT + LEDGER §B.2/§B.3 + §07.2 HISTORY 2026-06-03.

  • 2026-06-03 — §07.2 verify-first audit: higher_order ×2 classification corrected (over-elim, not under-emission). The §07.2 task #2 + decisions/07 §5 line 94 bucket higher_order::{test_hof_closure_capture_in_loop, test_hof_make_predicate} as UNDER-emission (Model-B facet 2 — “burden-emit the captured value’s own dec at scope exit”). The precise SMT counterexample compiler_repo/aims-proof/proofs/10-counterexample/04B.2-over-elim-closure.smt2 classifies the SAME 2 cells as OVER-elim closure-env double-free (ori_rc_dec called on already-freed): PartialApply captures v (TF-7/TF-13) → RcInc + scope-exit RcDec; the predicate-stack elimination drops the capture-side inc but NOT the paired dec → unbalanced → double-free. Proof verdict UNSAT (per arc.md §Debugging, proof = realization-semantics SSOT): the PROVEN burden calculus does NOT admit this — DP-2 gates SUPPLEMENTARY decs only, terminal RL-2 decs own balance (P2), so the burden trivial-emit baseline (balanced BurdenInc+BurdenDec for the capture) + DP-2/DP-3 elimination over the balanced baseline is correct by construction. CURE CORRECTION: §07.2’s higher_order ×2 cure is NOT a manual under-emission dec-add (would worsen the double-free) — it is the burden-migration VERIFICATION that closure-capture emission stays balanced (the §07.1 verify-first-additive pattern: no production dec-add; additive matrix tests + class_covered anchored §09.4). These cells are §09-COUPLED (the over-elim is a predicate-stack bug dissolving at §09 retirement). Anchored to 04B.2-over-elim-closure.smt2 + decisions/07 §5. Does NOT touch the borrow classification (decisions/07 §3).

  • 2026-06-03 — §07.1 verify-first audit + scope correction (autopilot execution). A verify-first audit (Opus, read-only) of §07.1 established: (1) checkbox 1 is ALREADY-SATISFIED at the implementation level — the Phase-5 burden walk (emit_burden_ops → collect_owned_burdens, lower/burden_lower/mod.rs:424) is VAR-INDEXED over func.var_types, so every apply-alias-class member is structurally visited; no production code change needed. (2) checkbox 2 was mis-scoped — class_covered reporting apply-alias classes covered is UNOBSERVABLE during §07 coexistence (populate_class_covered at post_convergence.rs:46 runs Step 4 and short-circuits on empty burden_emitted, which emit_burden_ops fills at Step 4b strictly after; decide.rs:65-77 confirms the set stays empty until §09.2). Restated checkbox 2 to the §07-era-observable property (burden_emitted ⊇ apply-alias members) and anchored the class_covered = true assertion at §09.4. (3) checkbox 3 scoped to the ApplyAliasSource shape × element-type matrix (Direct / Project / Conditional / Wrapped × str / [int] / Option / closure / struct) with dual-backend parity + ORI_CHECK_LEAKS + ORI_DISABLE_BURDEN_OPS control dimensions. All §07.1 work is ADDITIVE (verification test + fixtures); no collect_all_borrowed_defs / borrow-classification edits (decisions/07 §3). The audit independently re-confirmed the round-2 codex-F1 cure (class_covered measured post-Step-4b).

  • 2026-05-30 — Folded BUG-04-123’s 14 under-emission cells into §07 (plan reframe per user directive). The under-emission half of BUG-04-123 (Model-B facet 2 — a sum payload moved out of a consumed container needs its own dec at scope exit) lands in 07.3 (sum-payload: generics forwarders + for_yield_option + borrow_independence + aims_burden_alias + aims_interactions-h12) + 07.2 (higher_order closure-capture). The cure is ADDITIVE (emit the missing payload dec) and MUST NOT touch the borrow classification — 3 collect_all_borrowed_defs reclassification attempts each regressed 29 -> 74 (decisions/07 §3 rows 7a-c, §4.5). decisions/07 is the SSOT for the rule-out catalogue. BUG-04-123 absorbed to 00-overview.md absorbed_bugs[]; the over-emission half is §03A.3.

  • 2026-06-03 — Autopilot auto-cure: review_plan_redispatch_loop reset_lost_dispatch (autopilot_run_id=0bd4550edc3c4ced9d32e21b9c04a43c); chain log recorded a phantom /review-plan dispatch but section frontmatter showed zero review evidence; chain counter reset and /review-plan re-dispatched (per state-discipline.md §4 Hard-abort terminal-state semantics + skill-control-contract.md §Autopilot Mode unified hook-failure continuation clause).

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

  • 2026-06-03 — /review-plan Step 5 editor split co-bundled subsections (in-place re-scope, no new sibling sections). Per the reviewer blind-spots workplan + the design_decision (splits stay within §07’s bounded value-shape-coverage scope; none independently-workable as a sibling per routing.md §4): §07.3 “Sum-payload extraction + jumpargs coverage” split into §07.3 (sum-payload extraction + BUG-04-123 14-cell under-emission cure) + §07.3A (jumpargs block-boundary ownership-transfer coverage); §07.5 “Regression test corpus + additional shape coverage” split into §07.5 (regression re-verification gate) + §07.5A (additional-shape test authoring). Added explicit class_covered tasks for recursive-types (§07.3), Value/HeapType-mixed (§07.3), Drop-trait-collision (§07.4) classes; declared the BUG-04-123 14-cell under-emission cure cells in success_criteria. Gated the §07.4 unwind_cleanup migration on the class_covered handshake for the unwind-path classes. Moved the INV-19 transitive-consume justification out of success_criteria into the body Depends on: note (transitive-consume meaning preserved: §03/§04B are transitive INPUTS reachable through the §06 linear-chain predecessor, NOT additional DAG predecessors; depends_on: ['06'] single-predecessor intact).