0%

Section 12: Green-Gate Red Partition + Orthogonal Routing

Goal: Bound the expanded full-green terminal gate. The 2026-05-29 reground expanded the mission to “full ./test-all.sh ZERO failures.” This section partitions the current red so that gate is honest: burden-attributable failures (this plan’s deliverable, dissolved by the migration) vs orthogonal failures (other subsystems, enumerated + routed, NOT silently swallowed). The classifier is the proven-coverage guard the whole plan already runs on — a failure is burden-attributable when its shape diverges from a PROVEN-COMPLETE AIMS rule; orthogonal when its correctness rests on a pending rule or a different subsystem. Per routing.md, unrelated bugs stay separate; “all red is a burden bug” is the banned scope error this partition prevents.

Context (live partition — 2026-05-29 ./test-all.sh): AOT test result: FAILED. 1631 passed; 671 failed; 31 ignored. The failing set carries 2873 burden imbalance (VF-1) ICE occurrences — implementation-fidelity divergences from the proven RC net-preservation invariant (AimsProof.Realization::RL3_elision_net_preserving), resident in the burden-op ↔ predicate-stack coexistence layer. The dominant failing categories are all RC-realization (fat_matrix 132, fat_ptr_iter 92, iter_rc_matrix 53, rc_matrix 30, elem_dec_scope 30, collections_ext 22, traits 21, match_alias 20, higher_order 19, generics 18, cow_map_set 18, memory_stress 17, string_sso 16, arc 16, …). The interpreter (eval) backend also reports failures (✗ Ori interpreter tests FAILED); eval does NOT go through ARC burden realization, so eval-backend failures are orthogonal to the burden migration.

Why a section (not inline bugs): the PARTITION + green-gate accounting is plan-content (it defines what “full green” means for this plan’s terminal criterion). The orthogonal FAILURES themselves route to bug-tracker per routing.md §2 (this section files/cross-references them); the burden failures are dissolved by §03A/§05/§07/§09 (no per-failure bug). The section is the accounting + routing umbrella.

Depends on: none (groundable from the current ./test-all.sh run + the aims-rules.md terminal-state table, both already present). FEEDS §10 (verification’s full-green criterion consumes this partition — section-10-verification.md depends_on: 12).

Intelligence Reconnaissance

Queries:

  • scripts/intel-query.sh --human bugs-for aims-burden-tracking — open bugs the partition cross-references
  • scripts/intel-query.sh --human hotspots — where open bugs concentrate (orthogonal-subsystem signal)
  • scripts/intel-query.sh --human symbol-plans "__cast" --repo ori — mono __cast (BUG-04-114) orthogonal-failure provenance

Queried: 2026-05-29; 2026-06-02 (proven-coverage classifier reconciliation — the aims-rules.md terminal-state table + §10.7 oracle confirmed as the authoritative within-coverage discriminator).

Results summary (≤500 chars) [ori]: the plan’s 00-overview.md orthogonal_bugs: lists 20 (BUG-04-114 mono __cast, BUG-04-039 narrowing, BUG-04-096/097/099 lattice, BUG-04-062..083 borrow-inference/IC-8/DP, BUG-04-105/108/119 codegen/nounwind/mono, BUG-04-091 mono @unwrap on Box<T>, BUG-04-092 try-lowering lower_try). This section cross-references the live ./test-all.sh orthogonal failures against that list + files /add-bug for any untracked (notably the interpreter-backend eval failures). The within-coverage discriminator is the proven-rule terminal-state table — no new subsystem ownership, extends the unified-model accounting per missions.md §AIMS invariant 5.

12.1 Partition methodology (proven-coverage classifier) + burden-attributable bulk

  • Record the partition rule (above success-criterion 1) in this section’s body as the SSOT classifier. AUTHORITATIVE rule: a failure is BURDEN-ATTRIBUTABLE iff it is an implementation-fidelity divergence from a PROVEN-COMPLETE rule — its failing shape is WITHIN the coverage of a rule whose terminal_state is proven_sound or reformulated_and_proven per the aims-rules.md HISTORY 2026-05-28 terminal-state table. This is the SAME §04B.N proven_by coverage guard the whole plan runs on (within-coverage of a proven-complete rule → impl-fidelity repair / burden; out-of-coverage / pending / unprovable_with_gap_citation → architecture review / orthogonal), NOT a new classifier. The VF-1 signature + RC-runtime double-free/leak category is the FAST first-pass signal; the proven-coverage guard is the verdict.
  • Confirm the burden bulk: grep -cE "burden imbalance \(VF-1\)" test-all.log (baseline 2873) + the RC-runtime double-free/leak failures map to §03A (emission) / §05 (elimination) / §07 (coverage) / §09 (retirement). These need NO per-failure bug — they dissolve by migration-completion. The VF-1 imbalance failures are within the coverage of RL3_elision_net_preserving (the proven RC net-preservation the burden-balance check enforces), so they are impl-fidelity divergences the migration dissolves, not orthogonal.
  • BUG-04-123 is the canonical burden-attributable cluster (absorbed to 00-overview.md absorbed_bugs[]): its 17 cells split into 3 over-emission match_alias (-> §03A.3 shallow container drop) + 14 under-emission generics / for_yield_option / higher_order / borrow_independence / aims_burden_alias / aims_interactions-h12 (-> §07 moved-out payload’s own dec). All sit within the 12.1 burden bulk categories (match_alias 20, generics 18, higher_order 19, string_sso 16, arc 16) and within the coverage of the proven RL-2 (RL2_dec_at_last_use) dec-placement rule (per 00-overview.md 2026-05-30 — over-emission cells are RL-2 BurdenDec-fidelity divergences). They dissolve when §09 retires the predicate stack; decisions/07 §5/§7 is the over/under split + cure-surface map. NO per-failure bug — BUG-04-123 IS the absorbed umbrella.
  • No semantic-pin needed here (accounting section); the regression pins live in §03A/§05/§07.

Subsection close-out (12.1) per protocol.

12.2 Orthogonal enumeration + routing

  • Enumerate the ORTHOGONAL failures from the live partition: narrowing::* (BUG-04-039), poly_lambda_mono::* + any __cast/E5001 (BUG-04-114), inherent-method-on-generic missing-mono-instance (BUG-04-091 @unwrap on Box<T>), try-lowering lower_try E5001-on-non-struct (BUG-04-092), the interpreter-backend (eval) spec::test_aot_* failures, and the per-failure-classified enum_zero_payload / error_handling::test_catch_* (read each fixture + error mode; classify burden-runtime vs orthogonal-codegen — do NOT assume). Orthogonal = its correctness rests on a rule that is NOT proven-complete (pending/unprovable_with_gap_citation) OR a subsystem upstream of / parallel to AIMS RC-realization (monomorphization dispatch, try-lowering canonicalization, the eval backend).
  • Burden-ops-disabled verification gate (agy-F2 cure — prevents the category heuristic hiding a genuine non-burden double-free), reframed as proven-baseline reproduction: the first-pass signal classifies a runtime double-free/leak/UAF in an RC-realization category as BURDEN-ATTRIBUTABLE on category alone. Before accepting that label for ANY such failure, RE-CHECK it under ORI_DISABLE_BURDEN_OPS=1 (the proven predicate_stack_path baseline — emit_burden_ops skipped at Step 4b per arc.md §Debugging; this IS Function 2 of Handshake.proof, the pre-burden lattice-only path the §11 CH proofs prove equivalent on covered classes). If the double-free/leak DISSOLVES with burden ops disabled, it is genuinely burden-attributable (kept in the burden bucket, dissolved by §03A/§05/§07/§09). If it PERSISTS with burden ops disabled, the proven predicate-stack baseline has the SAME defect — burden emission did not cause it, so it is ORTHOGONAL; reclassify it out of the burden bucket and route it per the orthogonal mapping below (/add-bug if untracked). A category-based label is provisional until this proven-baseline re-check confirms it.
  • Cross-reference each against 00-overview.md orthogonal_bugs: (20 entries, incl. BUG-04-091 + BUG-04-092). Covered → cite the bug. Untracked → /add-bug (routing.md §2: orthogonal bugs route to bug-tracker, NOT inline). The interpreter-backend eval failures specifically: verify coverage; /add-bug if missing.
  • Record the orthogonal→bug mapping table in this section’s body.

Subsection close-out (12.2) per protocol.

12.3 ir_checks / ir_quality_attributes → §11 rebake

  • Classify ir_checks (1) + ir_quality_attributes (12) FileCheck IR-assertion failures: these pin EXACT emitted IR, which burden landings change. They are NOT orthogonal-subsystem failures — they are RE-BLESS-after-§09 candidates, the same discipline as §11 (AIMS snapshot rebake). Route them to §11’s rebake scope.
  • Banned: ORI_BLESS=1 re-bless WITHOUT the §11 proven-antecedent gate confirming the drift satisfies the proven calculus (CLAUDE.md §INVERTED-TDD positive-test-modification). The rebake happens at §11 AFTER §09, gated on the §11.3.0 proven-antecedent check (the new IR shape must satisfy the proven DP/RL/CH antecedents per the §10.7 oracle).

Subsection close-out (12.3) per protocol.

12.4 Green-gate accounting for §10

  • Author the green-gate accounting (consumed by §10 verification’s terminal full-green criterion; hardened 2026-06-10): full ./test-all.sh ZERO failures ⟺ (burden set → 0 via §03A/§05/§07/§09 migration-completion) AND (orthogonal set → each failure FIXED-and-verified via /fix-bug — tracked-but-failing and gate-scope exclusion are interim routing states, NOT close-enabling) AND (ir_checks/ir_quality re-blessed at §11 under the proven-antecedent gate) AND (zero warnings + zero ignored + zero build failures incl. wasm + zero LLVM crashes per the hardened 00-overview.md terminal criteria).
  • DAG confirmation (no cycle): section-10-verification.md depends_on lists 12 (wired at the 2026-06-02 rework — §10 consumes this partition), and this section’s depends_on is [] (groundable from the test run; it FEEDS §10). Confirm the DAG is acyclic — topological order 08, 09, 12 → 10 → 11 — via python -m scripts.plan_corpus check plans/aims-burden-tracking/. Do NOT add 11 (or any successor of §10) to this section’s depends_on — that would create the 12 → 10 → 11 → 12 cycle the prior depends_on: ["11"] risked.
  • Confirm 00-overview.md Mission criterion “orthogonal non-burden red enumerated + routed per routing.md” is satisfied by 12.2’s mapping table.
  • TPR checkpoint — /tpr-review covering 12.1-12.4.

Subsection close-out (12.4) per protocol.

12.R Third Party Review Findings

  • None.

12.N Completion Checklist

  • Partition methodology recorded (proven-coverage classifier) + burden bulk confirmed (12.1).
  • Orthogonal set enumerated + every failure mapped to a tracked bug (existing or /add-bug), each confirmed via the proven-baseline (ORI_DISABLE_BURDEN_OPS=1) re-check (12.2).
  • ir_checks/ir_quality routed to §11 rebake under the proven-antecedent gate (12.3).
  • Green-gate accounting authored; §10 depends_on: 12 confirmed; DAG acyclic via plan_corpus check (12.4).
  • Plan annotation cleanup.
  • Plan sync per protocol.
  • /tpr-review passed (final); /impl-hygiene-review passed.

HISTORY

  • 2026-06-10 — Green-gate accounting HARDENED per user directive (plan-level Mission Success Criteria hardening, 00-overview.md HISTORY 2026-06-10). The orthogonal set’s terminal disposition collapses from closed-OR-tracked to FIXED-and-verified: tracking (existing orthogonal_bugs: entry or new /add-bug) remains the mandatory mid-plan routing form, but every tracked orthogonal failure is driven to fixed via /fix-bug (per §10.4 still-open handling) before the terminal gate reads green; gate-scope exclusions are likewise interim-only. The accounting equation gains the hardened terms: zero warnings + zero ignored + zero build failures incl. wasm + zero LLVM crashes. The partition methodology (proven-coverage classifier, §12.1-§12.3) is unchanged — only the terminal accounting (§12.4 + success criteria 4-5) hardened.
  • 2026-06-02 — Reworked §12 to a proven-coverage classifier + DAG fix. The burden-vs-orthogonal partition was reframed from a category heuristic (VF-1 signature OR RC-realization category = burden) to the PROVEN-COVERAGE guard the whole plan already runs on: a failure is burden-attributable iff it is an impl-fidelity divergence from a PROVEN-COMPLETE rule (within the coverage of a proven_sound/reformulated_and_proven rule per the aims-rules.md terminal-state table — the SAME §04B.N proven_by coverage guard, SSOT not duplicated); orthogonal iff its correctness rests on a pending/unprovable_with_gap_citation rule or a different subsystem. The VF-1 / RC-category signal is retained as the fast first-pass; the proven-coverage guard is the verdict. The agy-F2 ORI_DISABLE_BURDEN_OPS=1 re-check was reframed as proven-baseline reproduction: that flag IS Handshake.proof Function 2 (predicate_stack_path), so a defect that persists with burden off is in the proven pre-burden baseline → orthogonal. DAG fix: depends_on corrected from ["11"] to [] — aligns the frontmatter with this section’s own body (“Depends on: none … FEEDS §10”) and breaks the latent 12 → 10 → 11 → 12 cycle that ["11"] plus §10-consumes-§12 would have formed; §12.4’s prior “Add 12 to §10 depends_on” action (cycle-creating if §12 still depended on §11) was corrected to a DAG-acyclicity confirmation (§10 now lists 12; §12 depends on nothing).
  • 2026-05-30 — Cross-referenced BUG-04-123’s 17 cells into the burden-attributable partition (plan reframe per user directive). BUG-04-123 (absorbed to absorbed_bugs[]) is the canonical burden-attributable cluster: 3 over-emission match_alias (§03A.3) + 14 under-emission generics/for_yield/etc (§07), dissolved by §09 retirement. The cells already sit within 12.1’s burden bulk (match_alias 20, generics 18, higher_order 19, string_sso 16, arc 16 categories) and within the proven RL-2 coverage; decisions/07 §5/§7 is the over/under split + cure-surface map. No new partition logic — BUG-04-123 IS an absorbed umbrella, not a per-failure bug.
  • 2026-05-29 — §12 created via /create-plan --inline (routing.md §3 case b) — the green-gate red partition for the expanded full-green mission. Per the 2026-05-29 reground, the mission expanded to full ./test-all.sh zero-failures; this section bounds that gate by partitioning the live red (671 AOT failures, 2873 VF-1 ICE occurrences) into burden-attributable (~650, dissolved by §03A/§05/§07/§09) vs orthogonal (narrowing/mono/eval-backend/codegen — enumerated + routed to bug-tracker, mostly already in orthogonal_bugs:). Prevents the banned ‘all red is a burden bug’ scope error; feeds §10’s terminal green criterion. Grounded in the 2026-05-29 partition run.