§15 TRMC Cross-Block Admission + Must-Fire Activation

§15.0 Discovered Work Context

§15.1 Mission

The rewrite machinery (detection, soundness verification, rollback, 90 IR-level unit tests across aims/normalize/tests.rs + tail_call/tests.rs) is built and proven (PL-7..PL-11 proven_sound); the v1 same-block admission means it never fires on real lowered source, so no TRMC loop conversion reaches any emitted binary. Deliverable: the admission lift + the verification layer that pins “fired” — not just “behaviorally correct”.

• Lowered match arms split the recursive Apply and the wrapping Construct into different blocks (overflow-checked arithmetic emits jo-guarded branches; calls lower as Invoke with normal/unwind edges) — the same-block shape the v1 gate requires does not occur in lowered real programs.
• The IR-level unit tests exercise synthetic same-block shapes; the AOT fixtures are behavioral-only (assert_aot_success passes whether or not the rewrite fires). Nothing currently pins end-to-end firing — that pin is a §15 deliverable, not an incidental.

§15.2 Calculus + Evidence Anchors

§15.3 Implementation Sketch

§15.4 Implementation Items

• §15.3.0 Calculus coverage check: scratch-Lean discharge attempt for the cross-block rewrite obligation; record verdict (case (a) covered / case (b) extended) + artifact paths in this section’s HISTORY block. Case (b) lands the Lean extension + four-surface sync BEFORE any Rust edit per arc.md §CP-1.
• §15.3.1 Cross-block admission lift in check_admission consuming ContextRegion.open_block/close_block; all non-block admission checks preserved; PL-10 five structural checks pass on rewritten IR; rollback negative test (an inadmissible region rolls back + Steps 3-4 re-run per PL-5).
• §15.3.2 Must-fire pins: deep-recursion fixture at loop-conversion-required depth (stack-overflows when the rewrite does not fire); IR-shape pin on the rewritten loop (context-hole threading present, self-recursive Apply absent); negative must-NOT-fire pin on a branching non-TRMC shape.
• §15.3.3 Hole-position matrix: hole=0 both-holes mirror fixture; interior-hole multi-field fixture; the 5 shape-less fixtures reconciled with their claimed Matrix G cells (content matches claim, or cell re-homed + program retained under a non-TRMC name).
• §15.3.4 verify_trmc_burden_balance zero errors over rewritten regions; ORI_CHECK_LEAKS=1 zero leaks on every TRMC fixture; eval + LLVM parity.
• §15.3.5 Assembly pin: -O3 --emit=asm of the canonical list-map — no self-call in the fn body; loop + hole-plugging store shape present.
• §15.3.6 Snapshot re-bless under §11 proven-antecedent discipline: classify each drifted pass output against the proven PL-9/PL-10 shape; ORI_BLESS=1 only on classified intended-drift.
• §15.3.7 Cross-coverage: timeout 150 ./test-all.sh debug + release clean; zero new failures vs the §12-partitioned terminal baseline.
• §15.3.R /tpr-review on §15 diff returns clean. Route every emitted /tpr-review exit_reason per the global exit-reason routing table (plans/completed/scripts-first-workflow-architecture/_archive/2026-05-15-pre-fold/skill-ecosystem-coherence/decisions/31-step-6-exit-reason-table-source.md) so autopilot dispatches each terminal state (clean → advance to §15.3.N; findings → fix-and-re-run within the round cap; cap_reached_with_substantive / cap_reached_clean → record review_pipeline: round state + classify per tpr-review/SKILL.md §5.5) rather than stalling on a non-clean exit. That global table is the SSOT for the routing; consume it, never re-derive it inline.
• §15.3.N /impl-hygiene-review on §15 diff returns clean after TPR.
• §15.3.Close flip status: → complete via the atomic-flip API per state-discipline.md §4.
• §15.4.P0 Nightly CI full-run monitor (hardened 2026-06-10 — the LAST verification gate before plan close): trigger/await the next full Nightly CI cycle over the terminal substrate; monitor every scheduled workflow to completion (gh run list + gh run watch in compiler_repo); ALL jobs green on the post-§14 surface (aims-proofs.yml + the nightly dev→master merge ci.yml run + any other live scheduled workflow) — zero failures, zero cancelled. Record run IDs + date in this section’s HISTORY. A red job routes per CLAUDE.md §Failing Tests Mid-Work (fix, then monitor a fresh full cycle); plan close is BLOCKED until a fully-green monitored cycle exists.
• §15.4.P1 All mission success criteria (00-overview.md) checked off — every section 00-15 is status: complete (§15 is the terminal section; plan-level all-MSC gate relocated from §10.N per the §15-terminal-tail topology). Includes the 2026-06-10 hardened criteria: unconditional test-all green (zero failures/warnings/skips/build-failures/LLVM-crashes), zero #[ignore]/#skip remaining, trace modes clean, and the §15.4.P0 monitored Nightly CI green run.
• §15.4.P2 Plan annotation cleanup (full-plan): bash .claude/skills/impl-hygiene-review/plan-annotations.sh --plan aims-burden-tracking returns 0.
• §15.4.P3 Plan close: 00-overview.md + index.md status → complete; HISTORY block records §10 PASS + §11 rebake + §15 TRMC activation + spec propagation date.
• §15.4.P4 Plan move: python -m scripts.plan_corpus.move_completed_plans move-plan-if-terminal --plan plans/aims-burden-tracking --apply once spec propagation lands (idempotent terminal-plan move to plans/completed/).

§15.5 Banned Approaches

• Implementing the cross-block lift BEFORE the §15.3.0 calculus coverage verdict — banned per arc.md §CP-1 (calculus-first; prove THEN implement). A bare “the unit tests pass” is not coverage evidence.
• WEAKENING the compiled Lean (hypothesis narrowing, sorry, vacuous discharge) to admit the cross-block shape — banned per arc.md §CP-1 BANNED clause; extension is by genuine kernel-checked theorem only.
• ORI_BLESS=1 snapshot rebake without the §11 proven-antecedent classification — banned per CLAUDE.md §INVERTED-TDD (positive-test-modification).
• Starting §15 while §07B/§09/§10/§11 are in flight — the depends_on: ["11"] gate is load-bearing: a new CFG rewrite firing mid-migration churns §07B’s under-flag baseline SET comparisons and §11’s re-blessed snapshots. The 5 shape-less trmc fixtures are LIVE §07B RC-corpus cells (per §07B HISTORY attempts 46-47); their content is NOT rewritten before §15’s turn.
• A parallel rewrite path beside normalize_function (a second TRMC implementation for cross-block while same-block keeps the old path) — banned per missions.md §AIMS invariant 5; one admission gate, one rewrite.
• Citing behavioral assert_aot_success green as rewrite-fired evidence — the must-fire pins are the evidence; behavioral green is necessary, not sufficient.

Intelligence Reconnaissance

Date: 2026-06-06 (discovery session). Direct-source grounding (graph file-symbols on ori_arc/src/trmc returned empty; symbols verified by Read):

• [ori:compiler/ori_arc/src/aims/normalize/rewrite.rs] check_admission v1 same-block gate at lines 122-127 (the lift target).
• [ori:compiler/ori_arc/src/aims/normalize/detect.rs] detect_context_regions at line 27 (Construct-with-recursive-field detection; no change expected).
• [ori:compiler/ori_arc/src/pipeline/aims_pipeline/trmc.rs] normalize_with_trmc (idempotent ≤2-iteration loop, pre-TRMC rollback save) + verify_trmc_soundness (Step 4a).
• [ori:compiler/ori_llvm/tests/aot/trmc.rs] Matrix G behavioral suite (12 fixtures; 7 genuine TRMC shapes all hole=last; 5 shape-less).
• [ori] Re-run at execution time: scripts/intel-query.sh callers check_admission --repo ori + callers detect_context_regions --repo ori for blast radius before editing.

§15.6 References

• compiler_repo/compiler/ori_arc/src/aims/normalize/{rewrite,detect,verify,lift}.rs — the rewrite pipeline
• compiler_repo/compiler/ori_arc/src/aims/normalize/tests.rs (58 tests) + compiler_repo/compiler/ori_arc/src/tail_call/tests.rs (32 tests) — IR-level rewrite coverage
• compiler_repo/compiler/ori_llvm/tests/aot/trmc.rs + fixtures/trmc/ — AOT behavioral layer (must-fire pins land here)
• compiler_repo/aims-proof/proofs/07-pipeline/PL-{7,8,9,10,11}.proof + Lean mirrors — the proven TRMC calculus (aims-rules.md §7 PL-7..PL-11)
• .claude/rules/arc.md §AIMS Change Protocol §CP-1..§CP-4 — calculus-first protocol governing §15.3.0
• .claude/rules/aims-rules.md §7 PL-7..PL-11 — TRMC pipeline rules (four-surface sync target on case (b))
• section-11-snapshot-baseline-rebake.md — proven-antecedent re-bless discipline §15.3.6 consumes
• section-09-post-convergence-partial-retirement.md §09.1 — detect_trmc_candidates PERSIST disposition
• tests.md §Negative Testing Protocol item 4 — must-optimize / must-NOT-optimize pairing (Swift arcsequenceopts precedent)
• OCaml 4.14 TRMC + Koka TRMC (Leijen & Lorenzen, “Tail Recursion Modulo Context”, POPL 2023) — prior art for cross-block constructor contexts

HISTORY

• 2026-06-10 — §15.4.P0 Nightly-CI full-run monitor ADDED as the LAST plan-close gate (plan-level Mission Success Criteria hardening, 00-overview.md HISTORY 2026-06-10). Per user directive the plan is not successful until one full Nightly CI cycle is monitored end-to-end with every scheduled workflow green (post-§14 surface: aims-proofs.yml + the nightly dev→master merge ci.yml run + any other live scheduled workflow). New success criterion + new §15.4.P0 item ahead of the P1-P4 plan-close chain; a red job routes per CLAUDE.md §Failing Tests Mid-Work (fix, then monitor a fresh full cycle). §15.4.P1 amended to name the hardened all-MSC set (unconditional test-all green, zero skips, trace-clean, monitored nightly run).
• 2026-06-06 — Section created via /create-plan --inline inline-insertion (routing.md §3 case (b)): Assembly-level verification session established that the TRMC rewrite never fires on real lowered source — check_admission’s v1 same-block gate (rewrite.rs:125) rejects every genuine fixture + canonical scratch shape under both the default path and ORI_DISABLE_PREDICATE_STACK_RC=1; -O3 assembly of map_inc retains callq _ori_map_inc@PLT. Detection (both hole positions), soundness verification, rollback, and the PL-7..PL-11 proofs are all in place; the admission lift is the single gap. Inserted as terminal tail depends_on: ["11"] — activating a CFG rewrite mid-migration would churn §07B under-flag baseline sets and §11 re-blessed snapshots; the 5 shape-less trmc fixtures are live §07B RC-corpus cells (attempts 46-47) and are not touched before §15’s turn. Must-fire pins (deep-recursion overflow + IR-shape) are a §15 deliverable: the AOT layer is currently behavioral-only and pins nothing about firing.