FOLD-IN + SUPERSEDE + GRIND-HERE (plan-wide standing directive — see overview Mission §Bug Fold-In + Supersession, ABSOLUTE). Every failing burden/RC-emission floor cell this section touches is worked HERE as part of this plan’s grind; any BUG-XX-NNN covering it, including BUG-04-118, BUG-04-142, BUG-04-156, the #150 same-allocation-identity class, and every sibling RC-emission bug, is FOLDED INTO this plan and SUPERSEDED — NEVER deferred to / routed away as separate bug tracking, a “separate architecture-level pass”, or “already tracked elsewhere”. Dead-end / deferred-compound / reclassified classifications (decisions/LEDGER.md §6) shape WHAT the fix is; they NEVER exit the cell from this plan. If the correct fix is an architecture-level pass, building it IS this plan’s work. Calculus-first per arc.md §CP-1; one terminal gate = ./test-all.sh zero failing cells.

RC-REMARKS CO-EVOLUTION (plan-wide standing directive — see overview Mission §8, ABSOLUTE). This grind is the rc-remarks RC-survivor observability system’s first real test: every floor cell / surviving-RC cluster this section works MUST be grounded via the burden-sole rc-remark stream (ori build --emit-rc-remarks + intel-query.sh rc-survivors --by-cause / rc-cause-rank) before hypothesizing a fix, AND when the stream/analyzer/query falls short for a real cell, improving rc-remarks (producer ori_arc/.../rc_remark.rs, analyzer tools/ori-rc-remarks, intel import_rc_remarks.py + query_graph.py rc-* handlers) IS this section’s work for that cell — never deferred as separate observability work. Burden-sole verdict discipline (arc.md §STOP) unchanged.

Section 05: Phase 6 Lattice Rewrite + RL-31

Goal: Per proposal §Design — Phase 6 (Lattice Analysis) — Optimization Over Burden Baseline. The lattice’s role narrows from constructor-of-correctness to optimizer.

Context: Critical invariant per proposal: “the lattice only ever ELIMINATES burden-emitted ops; it never CONSTRUCTS them.” Note the honest qualification: an OVER-elimination bug where DP-2 removes a BurdenDec that should fire produces a leak; over-elimination of an inc-dec pair where the elimination is wrong because alias-tracking input is wrong CAN produce double-frees. The burden model dissolves predicate-stack-EMISSION failure mode but inherits lattice’s elimination-side dependency on accurate alias-tracking infrastructure (project_alias_sources, borrow_sources).

Reference implementations:

• Roc compiler/gen_refcount/ post-emission optimization passes — Perceus’s pair-elimination shape (Phase 6 mirrors this).
• Lean 4 IR/RC.lean followed by simplification passes — same shape.

Depends on: Section 04B (Prototype Gate verdict unblocks §05: pass, partial-pass-criterion-6 with extensions documented, OR impl-fidelity-routing per the §04B.N proven_by override — the DEFAULT verdict, where empirical criterion FAILs are impl-fidelity divergence sites cured by §05→§07→§09, §05 NOT voided).

Intelligence Reconnaissance

Queries:

• scripts/intel-query.sh --human file-symbols "compiler_repo/compiler/ori_arc/src/aims" --repo ori
• scripts/intel-query.sh --human callers MemoryContract --repo ori
• scripts/intel-query.sh --human similar pair_elimination --repo roc,lean4 --limit 5

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.

05.0 IC-1 enforcement precondition (absorbs BUG-04-112)

Status: complete (per frontmatter SSOT sections[].id 05.0, state-discipline.md §1; all §05.0 tasks below are [x] with DELIVERED evidence). The BUG-04-112 absorption scope is in the **Precondition relationship:** block below + the closed bug-plan archive at bug-tracker/plans/completed/BUG-04-112/ (investigation history; superseded by this section per the 2026-05-16 audit-correction HISTORY entry in 00-overview.md).

Precondition relationship: §05.2 success criterion 7 declares “Interprocedural MemoryContract SCC fixpoint: computes ParamContract / ReturnContract / EffectSummary exactly as today.” That “exactly as today” claim is sound ONLY when the contract layer enforces IC-1 — every func.name in func_by_name post-fixpoint has a MemoryContract entry. The shipped code silently degrades on absence at the 12 lookup sites in the BUG-04-112 grep inventory. This subsection hardens the 10 in-scope sites BEFORE §05.1 begins; the 2 remaining sites dissolved naturally via §03.3 Rule 1 Return-transfer burden semantics (cycles 32-39 close-out, 2026-05-15).

File(s):

• compiler_repo/compiler/ori_arc/src/aims/contract/mod.rs — ContractMapExt trait + impls (already landed pre-Phase-2.5 at lines 653-684, recorded in the BUG-04-112 section-05 implementation archive §1.0)
• compiler_repo/compiler/ori_arc/src/aims/contract/tests.rs — H1-H6 unit tests
• compiler_repo/compiler/ori_arc/src/pipeline/aims_pipeline/{batch.rs,mod.rs,postprocess.rs,trmc.rs} — sites 1-5 + 7 + 9-10 replacements
• compiler_repo/compiler/ori_arc/src/aims/emit_reuse/mod.rs — site 6 replacement
• compiler_repo/compiler/ori_arc/src/aims/emit_rc/drop_hints/mod.rs — site 8 explicit-match + debug_assert! + func_by_name threading through is_safe_non_sharing_callee + collect_borrowed_call_args
• compiler_repo/compiler/ori_arc/src/aims/realize/mod.rs — site 8 call-site update at line 218 (threading)
• Test fixtures: compiler_repo/compiler/ori_arc/src/tests.rs:26 + compiler_repo/compiler/ori_arc/src/pipeline/tests.rs:377/439/491 (F1-F4 empty-map sites cured via populated MemoryContract pre-insertion)

Site inventory (10 absorbed sites + 2 dissolved-via-burden)

Anchors below are span/symbol-named (verified against HEAD), NOT bare line numbers — re-resolve via grep -n on the named span/symbol, the line numbers in parens are HEAD-as-of-2026-06-01 confirmations only.

Tasks

Archived bug-plan reference

Full investigation history (Phase 1 RCA, Phase 1.75 /tp-help Round 1 consensus on cure shape, Phase 2 fix-consensus across all 12 original sites including persuaded-divergence on TRMC Option-scope, test-fixture pre-emptive cures, Site 8 debug_assert! enhancement; Phase 2.5 Plan TPR Rounds 0-7 convergence trajectory): bug-tracker/plans/completed/BUG-04-112/ — see archive’s 00-overview.md ## HISTORY block for the 7-round convergence detail.

Subsection close-out (05.0) per protocol — runs BEFORE §05.1 (the precondition relationship).

• Verify shipped state: ContractMapExt::get_required + get_mut_required exist at compiler_repo/compiler/ori_arc/src/aims/contract/mod.rs:655-686 (already landed pre-Phase-2.5); H1-H6 unit tests appended at compiler_repo/compiler/ori_arc/src/aims/contract/tests.rs.
• Test-fixture pre-emptive cures (F1-F4 per archived bug-plan §03 §5): each empty FxHashMap::default() site at compiler_repo/compiler/ori_arc/src/tests.rs:26 + compiler_repo/compiler/ori_arc/src/pipeline/tests.rs:377/439/491 gets a populated conservative MemoryContract for the synthetic func.name BEFORE constructing AimsPipelineConfig. (The run_arc_pipeline single-function entry ALSO seeds func’s own conservative contract via ensure_own_contract — see the Sites-11-12 / out-of-batch note below — so codegen of test/impl/derive bodies outside the interprocedural batch never panics.)
• Replace 9 sites with get_required / get_mut_required (sites 1-7 + 9-10) per the inventory table above; each cure replaces a silent-degradation no-else / unwrap_or_default / is_some_and pattern with an IC-1 panic. Added func_names: &FxHashSet<Name> to AimsPipelineConfig (sourced from the functions slice in the batch path, from the contracts keyset in the single-function path) to drive the site-8 IC-1 debug_assert!.
• Site 8 cure: explicit lookup (if let Some(c) = contracts.get(&callee) { ... } else { debug_assert!(...) }, clippy-rewritten from match) + debug_assert! in the None arm + threaded func_names: &FxHashSet<Name> through is_safe_non_sharing_callee + collect_borrowed_call_args + realize_annotations (+ AimsPipelineConfig.func_names).
• TDD matrix: H1-H6 helper cells (contract/tests.rs); Site 8 cells 8a-8e (drop_hints/tests.rs, 8e split debug/release via #[cfg(debug_assertions)]); INV1 + INV2 (pipeline/tests.rs); F1-F4 fixture cures. cell 8e exercises debug_assert! in debug build (panic) and returns false silently in release (sibling test); both gates required + passing.
• Pre-fix verification: H1-H6 cells PASS (helpers already exist); INV2 panics on synthetic break (run_aims_pipeline direct with empty contracts → unreachable! at first get_required); 8e debug_assert fires in debug only.
• Post-fix verification: BOTH cargo test -p ori_arc (debug) AND cargo test -p ori_arc --release GREEN (1501 debug / 1498 release lib tests, 3 debug-only cfg-gated). Production call sites: grep \.get_required\( returns 8 (sites 1-7 PLUS the re-absorbed site-11/12 emit_unified_return_transfer_setup per the escape-hatch below); grep \.get_mut_required\( returns 2 (sites 9-10); site 8 AIMS Invariant IC-1 debug_assert present in drop_hints/mod.rs.
• Tests: INV2 = semantic pin (fails on revert — re-surfaces silent fallback); H2/H5/8c/8e = negative pins rejecting silent-degradation.
• Sites 11-12 dissolution verification: grep confirmed the build_return_transfer_setup function-level metadata mechanism PERSISTS (the §03.3 Rule 1 dissolution did NOT remove the lossy contracts.get(&func.name).map(...).unwrap_or_default() lookup). Per the escape-hatch, sites 11-12 RE-ABSORBED into §05.0 scope: cured with get_required("emit_unified_return_transfer_setup") (1 supplementary immutable site, bringing the immutable total to 8). No re-opening of BUG-04-112.
• Cross-plan — ParamContract.may_escape form: locality-representation-unification has NOT landed — ParamContract.may_escape remains a stored field (contract/mod.rs). §05.0 proceeds against the stored-field form; no may_escape() method-call migration required. Advisory/non-blocking per routing.md §1.

05.1 Lattice consumption-mode shift (emission → elimination)

Vocabulary boundary: AIMS decides logical ownership events and mutation obligations. Burden* names below are transitional Phase-6 carriers used to observe those logical decisions; Rc*, CowMode, and IsShared belong only to the current Phase-7 compiled adapter and are not calculus outputs.

File/site inventory (verified against HEAD 2026-06-01). Anchors are symbol-named; re-resolve via grep -n on the symbol. All paths compiler_repo/compiler/ori_arc/src/aims/....

Audit outcome (verified against HEAD). The lattice consumption mode is ALREADY elimination — eliminate_burden_ops (realize/burden_elim.rs, Phase 2.5 of emit_rc_unified) is the SOLE Phase-6 burden-op consumer and it ONLY removes/compacts; it never appends. The inventory sites split into three classes, none of which construct burden ops in Phase 6:

• realize/burden_elim.rs eliminate_burden_ops — the canonical Phase-6 eliminator. Removal-only (compacts via body.retain). Now carries the §05.1 structural enforcement.
• transfer/mod.rs DP-2 (is_release_event_unnecessary) / DP-3 (is_additional_credit_elidable) — pure predicates; consumed ONLY by burden_elim.rs. Unchanged.
• transfer/mod.rs::cow_obligation_from_uniqueness plus realize/decide.rs (decide/decide_last_use/decide_annotations/decide_cow/decide_drop_hint) and realize/walk.rs — the logical-decision seed plus its current compiled-adapter compatibility surface. The retiring predicate stack emits physical RcInc/RcDec; walk.rs preserves transitional Burden* carriers verbatim and constructs no such carriers. NOT extended (per LEDGER §B).

Burden-op CONSTRUCTION lives only outside Phase 6: Phase 5 (lower/burden_lower/emit.rs emit_burden_ops) and the §03A coexistence-mirror scaffold (realize/burden_mirror.rs reconcile_burden_ledger + the adjacent edge/trampoline BurdenDec markers in emit_rc/edge_cleanup.rs / emit_rc/trampoline.rs), the latter §09-retired. No Phase-6 construction site exists; the audit converts nothing because the consumption mode is already correct.

Structural enforcement (CRITICAL invariant made loud). eliminate_burden_ops now takes a per-kind burden-op census (burden_op_census) before AND after the elimination loop and asserts the post-pass census is ≤ the pre-pass census for EVERY burden-op kind (debug_assert_burden_removal_only, backed by the release-safe SSOT predicate is_burden_removal_only). A future regression that appends a BurdenInc/BurdenDec* inside Phase 6 trips the guard loudly (debug) rather than silently lowering to a spurious RcInc/RcDec in Phase 7.

Tests (realize/burden_elim/tests.rs): phase6_is_elimination_census_strictly_shrinks (semantic positive pin — fails on revert if Phase 6 stopped eliminating or became a constructor); phase6_preserves_census_when_nothing_elidable (lower-bound clamp — never grows); removal_only_predicate_rejects_construction_per_kind (release-safe negative pin — rejects construction of every kind); debug_guard_panics_on_phase6_construction (debug-build #[should_panic] guard pin). All pass debug + release (debug-only pin excluded under --release).

Subsection close-out (05.1) per protocol.

• Audit every site in the inventory above where lattice analysis DECIDES where to emit RC ops; convert each site to make an ELIMINATION decision over burden-emitted ops.
• Verify the CRITICAL invariant: lattice never constructs new BurdenInc/BurdenDec — only marks for elimination.
• Tests: lattice fixpoint produces correct burden ops post-elimination; no construction.

05.2 Dimension wiring audit

Per-task consumer source files verified against HEAD 2026-06-01 (re-resolve symbols via grep -n; all compiler_repo/compiler/...).

Test matrix delivered. Each dimension’s positive + negative pin landed against its shipped consumer predicate:

• Cardinality + Consumption → DP-2/DP-3 (eliminate_burden_ops over burden-emitted IR): compiler_repo/compiler/ori_arc/src/aims/realize/burden_elim/tests.rs (pre-existing 25-cell DP-2 × DP-3 × burden-op-variant matrix + §05.1 census/removal-only pins — positive: DP-3 removes additional credit for Once ∧ (Linear ∨ Affine) when the realization safety preconditions hold; negative: Many ∧ Unrestricted / Many ∧ Linear preserve it. Any wider-locality Affine retention belongs to the separate realization safety guard, not the DP-3 truth table).
• Uniqueness → DP-9 COW obligations, Shape + Uniqueness → DP-6 is_reuse_candidate, Locality → DP-7/DP-8 (is_event_pair_elision_eligible/is_local): compiler_repo/compiler/ori_arc/src/aims/realize/dimension_consumer/tests.rs (new). The pins establish same-identity permission, alias-isolation, sharing-observation, reuse eligibility, and bounded lifetime without prescribing IsShared, copying, counters, or storage.
• Historical LLVM-local effect scan (superseded, not AIMS authority): §05.2 once pinned has_only_pure_arc_instructions in ori_llvm::purity_analysis and treated it as a memory(none) gate. That was a backend-local re-derivation and did not prove RL-30. Production deletes that scan, freezes exact stable-ID neutral facts during AIMS realization, transports them validation-only, projects only proved ReadOnly as memory(read), and forbids memory(none) until inaccessible reads and writes are modeled.

Revert-sensitivity confirmed by mutation: breaking the is_local order-gate (always-true) fails the HeapEscaping not-local + not-event-pair-elision-eligible negative pins.

Subsection close-out (05.2) per protocol.

• Cardinality + Consumption dimensions: drive DP-2 (is_release_event_unnecessary) + DP-3 (is_additional_credit_elidable) per logical ownership event. Source: predicates at ori_arc/src/aims/transfer/mod.rs; consumer at ori_arc/src/aims/realize/burden_elim.rs (fn eliminate_burden_ops). eliminate_burden_ops is the SOLE Phase-6 transitional-carrier consumer; it queries DP-2/DP-3 against var_state_at_block_exit and removes only. Paired elimination preserves VF-1 logical owner-credit/release balance. Transitional Burden* carriers are TF-N/A in both transfer directions, so block_exit_state is the per-event state. Already pinned in realize/burden_elim/tests.rs (25-cell DP-2/DP-3 × variant matrix + §05.1 census pins).
• Uniqueness plus borrow safety drives DP-9 cow_obligation: safe Unique → SameIdentityPermitted; MaybeShared without a disjointness proof → SharingObservationRequired; Shared or an overlapping borrow → AliasIsolationRequired. Source: ori_arc/src/aims/transfer/mod.rs::cow_obligation_from_uniqueness returns the canonical CowMutationObligation seed; shared borrow-safety refinement may strengthen that seed before any target projection. The consumer reads converged Uniqueness and borrow facts regardless of transitional carrier presence. The current compiled Phase-7 adapter maps these obligations through decide_cow/CowMode (StaticUnique/Dynamic/StaticShared) and may emit IsShared; that mapping is compatibility evidence, not an AIMS output.
• Shape + Uniqueness: drive FBIP / Reset / Reuse (DP-6, RL-11, RL-11a) — unchanged. Source: ori_arc/src/aims/emit_reuse/detect.rs (find_reuse_opportunities_from_events :104, DP-6 eligibility) + ori_arc/src/aims/emit_reuse/planner.rs (Reset/Reuse planning) + ori_arc/src/aims/emit_reuse/dynamic.rs (RL-11a dynamic-uniqueness path). VERIFIED: find_reuse_opportunities_from_events :104 confirmed; the DP-6 eligibility predicate is AimsState::is_reuse_candidate (lattice/mod.rs :413) = Owned ∧ uniqueness ≠ Shared ∧ shape ≠ NonReusable — gates on BOTH Shape and Uniqueness. MaybeShared reusable shapes still qualify (RL-11a dynamic path); Shared and NonReusable are rejected (CN-3). Consumer reads converged Shape+Uniqueness; burden-transparent. Role survives.
• Locality continues to drive neutral lifetime eligibility; exact placement/header width does not. The shipped order-based consumers are AimsState::is_local and is_event_pair_elision_eligible, which remain variant-count-agnostic. The old ori_llvm::abi stack/header passes were stubbed and are not AIMS consumers. Production freezes lifetime/locality, OwnerBound, OwnershipObservationFacts (stable additional-credit, release, and sharing-observation event identities), and external visibility, then combines them with representation-owned extent evidence so VmLayoutPlan and CompiledLayoutPlan can select and validate physical storage and width independently.
• Cross-plan sequencing dependency (advisory, non-blocking) — plans/locality-representation-unification/: this plan adds a 5th Locality variant (ArgEscaping) + raises CHAIN_HEIGHT 15→16 + converts ParamContract.may_escape from a stored field to a derived method. IMPACT on §05.2: if locality has landed, the lattice this section optimizes over is 5-variant and may_escape is a method call — verify the order-based Locality predicates (RL-14/RL-17/RL-18 + DP-7/DP-8) hold across all 5 variants (the proven invariant per aims-proofing-suite §08 RL-15a/RL-18a + §05 DP-7/DP-8). SEQUENCING: SHOULD execute §05 after locality to avoid a contract/ + split-aims/-file rebase; if locality has NOT landed, §05 proceeds against the shipped 4-variant form (no §05 logic change either way). Schema restricts subsection_depends_on: / blocked_by: to in-plan IDs / BUG-XX-NNN, so this cross-plan optional dependency binds via this explicit task + the 2026-05-27 HISTORY entry + decisions/04 Clarification rather than a frontmatter ordering edge; structural sequencing tooling reads this task marker. VERIFIED (advisory, non-blocking): locality-representation-unification has NOT landed — shipped Locality is 4-variant (BlockLocal | FunctionLocal | HeapEscaping | Unknown) per aims/lattice/dimensions.rs; ParamContract.may_escape remains a stored field per aims/contract/mod.rs. The order-based DP-7/DP-8 predicates (is_local / is_event_pair_elision_eligible) are confirmed variant-count-agnostic (gate on ≤ FunctionLocal / ≥ HeapEscaping, never on a variant count). §05.2 proceeds against the shipped 4-variant form; the negative pins clamp HeapEscaping and Unknown so the predicates hold when ArgEscaping lands. ArgEscaping > FunctionLocal, so is_local and is_event_pair_elision_eligible both remain false. No §05 logic change is required.
• Effect/return/disjointness analysis continues to produce interprocedural neutral facts. The former ori_llvm::purity_analysis ARC-shape scan and ABI-local attribute derivation are historical migration gaps, not RL-29/RL-30/RL-31 implementations. The production consumer is an exact stable-ID fact plan frozen by AIMS and validated without recomputation; LLVM, VM, native, compiled-WebAssembly, and JIT project or consume those same facts independently.
• TRMC structural rewrite (PL-7..PL-11): operates over burden-emitted IR — unchanged. Source: ori_arc/src/pipeline/aims_pipeline/trmc.rs (TRMC normalization + verify_trmc_soundness). VERIFIED: normalize_with_trmc + verify_trmc_soundness confirmed in trmc.rs; normalize_with_trmc consumes config.contracts.get_required(&func.name, "trmc_entry") (the §05.0 IC-1-hardened lookup). TRMC runs at Step 3a over the lowered ArcFunction; burden ops are per-instruction and TF-N/A, so context-hole threading + arity preservation (PL-10) operate over the same structural shape regardless of burden-op presence. Depends on §05.0 IC-1 (complete). Role unchanged.
• Immortal pre-pass: continues to feed AimsStateMap as typed pre-pass input — unchanged. Source: ori_arc/src/aims/immortal/ (AimsStateMap::immortals bitvector population). VERIFIED: aims/immortal/ confirmed (mod.rs + tests.rs); intraprocedural/mod.rs :150-155 populates immortals: Vec<bool> and calls state_map.set_immortals(immortals). Immortal detection feeds the lattice-driven analysis as a typed pre-pass input (Invariant-5 avenue (c)) — it is NOT a lattice dimension and does not interact with burden-op emission. Role unchanged.
• Interprocedural MemoryContract SCC fixpoint: computes ParamContract / ReturnContract / EffectSummary exactly as today. Source: ori_arc/src/aims/interprocedural/mod.rs (SCC fixpoint) + ori_arc/src/aims/contract/mod.rs (MemoryContract/ParamContract/ReturnContract/EffectSummary); depends on §05.0 IC-1 enforcement. VERIFIED: interprocedural/mod.rs confirmed — Tarjan SCC + topological (callees-before-callers) fixpoint producing MemoryContract per function (analyze_program via scc_driver). Runs at Step 1, before any per-function burden lowering, so the contract computation is upstream of and independent from burden-op emission (“exactly as today”). §05.0 IC-1 hardening (complete) guarantees every post-fixpoint func.name has a MemoryContract entry, so the “exactly as today” claim is sound. Role unchanged.
• Tests — dimension-to-consumer matrix (positive + negative pin per dimension over burden-emitted IR):

05.3 RL-31 burden-aware path implementation

File(s): compiler_repo/compiler/ori_llvm/src/codegen/ (alias-scope emission) + LLVM fact-export site

§00 producer/consumer contract anchor (per opencode blind_spot[3]): This subsection consumes the 8-clause SUFFICIENT-condition rule + named predicates frozen at section-00-design-validation-gate.md §00.3 frozen_rule_version: v1 (per section-00-design-validation-gate.md §00.3 cross-section commitment contract). Add consumes_proof_product: v1 to this section’s frontmatter at §05.3 start; verify via scripts/plan_corpus check (post-validator-landing per opencode blind_spot[3]) that the producer/consumer keys match. ANY modification of the SUFFICIENT-condition rule clauses or named predicates here MUST trigger §00 Phase 0 reentry per state-discipline.md §3 Pause Mid-Pipeline + frozen_rule_version: v2 bump.

Subsection close-out (05.3) per protocol.

• Implement type-level disjointness proof via BurdenSpec.field_type chain comparison (per §00 walkthrough). DELIVERED: compiler_repo/compiler/ori_arc/src/aims/realize/rl31_disjoint.rs — prove_param_noalias(param_types, pool) -> NoaliasProof realizes the frozen 8-clause SUFFICIENT condition (fixed-point reachable-heap closure walk = clauses 1-3/6; closure disjointness = clause 4; transitive sum-node check = clause 5; distinct-surface-type = clause 7; opaque/unresolved fail-closed = clause 3/8). Builtin-burden self-sufficient (BURDEN_TABLE) for the worked-example collection types; user types fail-closed pending §04A.0 ITEM-1 registry threading (conservative = sound). 11 proof pins in rl31_disjoint/tests.rs (positives + same-type/shared-element/sum-node/scalar/unresolved negatives + self-verifying matrix).

• At LLVM emit time for noalias / alias-scope metadata, consume both ParamContract (existing) AND BurdenSpec (new) — combine to produce strictly stronger proofs where burden adds precision, gated on RL-31.proof P2’s dual-facet requirement. DELIVERED (conservative omission — RL-31.proof P2): ori_llvm/src/codegen/function_compiler/mod.rs declare_function_llvm_with_extra_params wires the dual-facet gate at the add_noalias_attribute call (noalias_proof.call_site_provenance_proven && noalias_proof.eligible.get(pidx)). RL-31 noalias is sound ONLY when BOTH facets hold: facet (b) type-level closure-disjointness (prove_param_noalias in ori_arc/src/aims/realize/rl31_disjoint.rs, computed today) AND facet (a) per-call-site provenance (NoaliasProof.call_site_provenance_proven, hardcoded false — the provenance pass depends on aims-rules.md §1.9 rules 5 + 7, unshipped). Because facet (a) is unshipped the gate conservatively OMITS noalias: every NoaliasProof-eligible Reference/Indirect pointer param keeps the existing ParamContract-derived readonly/nonnull/dereferenceable WITHOUT noalias. The gate is wired + reversible: the day the provenance facet flips call_site_provenance_proven: true, noalias+readonly emits as strictly-stronger LLVM AA — with NO codegen change beyond that facet EXCEPT the mandatory nounwind precondition gate (per decisions/01-noalias-emission-granularity.md §Consequences + decisions/00-rl31-burden-aware-design.md §(m)): function-attribute noalias on a parameter of an unwindable function is an LLVM soundness hazard (the optimizer may assume noalias across the Invoke/Resume unwind edge), so the flip MUST additionally require the function be nounwind (or restrict noalias to the non-unwinding path). ORI_DISABLE_RL31_NOALIAS=1 bisection flag added (sibling of ORI_DISABLE_BURDEN_OPS).

• Tests: merge(a: &{str:int}, b: &[int]) (Worked Example 1b Borrowed+Borrowed canonical shape per section-00-design-validation-gate.md §00.1 Concrete example 1b) emits WITHOUT noalias on its Borrowed parameters (facet (a) unshipped → conservative omission); verify with LLVM IR inspection. Additionally accumulate(a: {str:int}, b: [int]) (Worked Example 1 Owned+Borrowed generalization shape) emits WITHOUT noalias; verify same. DELIVERED: FileCheck IR pins compiler_repo/compiler/ori_llvm/tests/codegen/aims/rl31_merge_borrowed_pair_noalias.ori + rl31_accumulate_distinct_types_noalias.ori (both params ptr noundef nonnull readonly dereferenceable(24) — CHECK-NOT: ptr noalias, with a comment that the pin flips back to asserting noalias the day facet (a) ships) + NEGATIVE pin rl31_same_type_params_no_noalias.ori (combine(a:[int], b:[int]) same-type → CHECK-NOT: ptr noalias, omitted on facet (b) failure independent of facet (a)). Run via ori_llvm --test aot ir_checks.

• RL-31 × Phase 6 barrier / KnownSafe / PRE-style-motion legality co-verification sweep (per section-00-design-validation-gate.md §00.3 line 376 + codex blind_spot[1]): author instrumented tests at the named paths below — Ori spec source compiler_repo/tests/spec/aims/rl31_co_verification.ori (covers shapes a/b/c) + AOT IR-inspection mirror compiler_repo/compiler/ori_llvm/tests/aot/rl31_co_verification.rs (asserts !alias.scope/!noalias metadata survives each interaction), matching the groundedness pattern of §04B criterion 3 (compiler_repo/tests/spec/aims/burden_alias_tracking.ori): DELIVERED — spec test 3/3 (interp + LLVM dual-exec parity); AOT mirror IR-inspection + dual-facet-gate-invariance PASS 3/3. NOTE (per decisions/05-rl31-co-verification-evidence.md §Correction — gated-probe leak reality, which supersedes the raw leaks-0 column): the three rl31_*_exec execution tests carry #[ignore = "BUG-04-241: both-paths-fail borrowed-collection-arg drop leak"] on the gated probe — the AOT mirror’s EXECUTION+leak-free leg is BLOCKED on BUG-04-241 (§06/§09-coupled, dissolves at §09 predicate-stack retirement), NOT passing; the DELIVERED IR-inspection + gate-invariance legs stand. The RL-31 dual-facet gate (RL-31.proof P2) is parameter-level and decided at declare time; because facet (a) is unshipped the gate conservatively OMITS noalias identically across all three Phase-6 interactions — _ori_merge carries readonly/nonnull/dereferenceable WITHOUT noalias through all three shapes (IR results 23/16/8; the ‘zero leaks’ claim is superseded by the decisions/05 §Correction gated-probe reality — the exec leak is BUG-04-241). The sweep proves the gate verdict is structurally invariant to the Phase-6 RC-op-placement passes: when facet (a) ships and noalias emits, the same invariance holds (the metadata, like its omission today, is parameter-level not RC-op-level).

  • (a) KnownSafe pair elimination interaction: a merge(a: &T1, b: &T2) call site with an outer RcInc(a) in scope establishing KnownSafe(a) = true per aims-rules.md §8 RL-22 + RL-23 → an inner (RcInc(a), RcDec(a)) pair on the disjoint-Borrowed parameter MUST be eliminated; the RL-31 dual-facet gate verdict on the call site MUST be invariant post-elimination (today: noalias conservatively OMITTED per RL-31.proof P2 facet (a) unshipped; when facet (a) ships, the emitted metadata MUST survive). Test fn rl31_known_safe_pair_elim in both files.
  • (b) PRE-style RC motion across RC-observable barriers: a RcInc(a) / RcDec(a) pair around a call site that passes a to a callee Owned parameter (RC-observable barrier per aims-rules.md §8 RL-26 + RL-27) → motion MUST be REJECTED (barrier blocks motion); the RL-31 dual-facet gate verdict on the call site MUST be invariant (today: omitted; when facet (a) ships, metadata survives). Test fn rl31_pre_motion_barrier_blocked in both files.
  • (c) Selective barrier flush at call site: per clang-arc-lessons §02 (selective barriers), a call site where RL-31 applies AND the callee has may_share = true on a parameter → pending RcInc/RcDec ops MUST be flushed before the call; the RL-31 dual-facet gate verdict remains valid post-flush (the disjointness facet (b) is parameter-level, not RC-op-level — its emission/omission is decided at declare time independent of the flush). Test fn rl31_selective_barrier_flush in both files.

• Verify each co-verification test exercises the EXACT shape per aims-rules.md §8 RL-22..RL-26 + clang-arc §02; document evidence (per-shape IR snippet + pass/fail) in decisions/05-rl31-co-verification-evidence.md (new artifact at §05.3 close). DELIVERED: decisions/05-rl31-co-verification-evidence.md authored — per-shape IR snippet (params ptr noundef nonnull readonly dereferenceable(24), noalias conservatively OMITTED per RL-31.proof P2) + pass/fail table (shapes a/b/c all PASS on gate-verdict invariance + correct result + leak-free), implementation surface (dual-facet gate at function_compiler/mod.rs; facet (a) call_site_provenance_proven: false unshipped), fix-completeness gate results, and the ORI_DISABLE_RL31_NOALIAS=1 A/B proving zero new failures beyond the §06/§09 baseline.

05.4 Criterion-6 benchmark authoring + extension integration

Criterion-6 ownership moved to §05 (touches: compiler_repo/tests/benchmarks/aims_burden/). Under the §04B C6=proof_status:complete proven_by override, §04B’s outcome is impl-fidelity-routing (NOT partial-pass-criterion-6), so the criterion-6 microbenchmark deliverable is a §05 EXTENSION INPUT, not a §04B close-gate (per §04B.N Criterion-6 microbenchmark re-run anchor). The benchmark authoring + RC-count recording is therefore UNCONDITIONAL here — the conditional decisions/gate-criterion-6-extensions.md integration below fires only on top of it when a measured gap exceeds 5%.

Subsection close-out (05.4) per protocol.

• Author the three microbenchmarks (unconditional — the §04B criterion-6 deliverable, now §05-owned): compiler_repo/tests/benchmarks/aims_burden/{closures_inside_loops,sum_payload_extraction,conditional_transfer_in_branch} per the §04B.6 microbenchmark specifications (closure-env BurdenSpec composition; Maranget-tree BurdenDecVariant + DP-2 elimination; per-edge balance + DP-3 elimination). Authored as .ori (NOT .rs): the BS-04B-4 measurement methodology (rc-stats.sh <file.ori> via ORI_AUDIT_CODEGEN=1, ORI_DISABLE_BURDEN_OPS=1 ori build, counts on lowered LLVM IR after Phase 7) is Ori-program-based — a .rs file is neither compilable by the ori compiler nor measurable by rc-stats.sh; the sibling tests/benchmarks/cow/*.ori corpus is the canonical idiom. The .rs extension in the §04B.6 spec was an authoring-detail mismatch; the workload (closure-env / sum-payload / conditional-transfer Ori programs) is the deliverable.
• Run + record normalized RC counts (unconditional): established baseline counts via current AIMS predicate stack (ORI_DISABLE_BURDEN_OPS=1) + burden-emitted counts under Phase-6 elimination; normalized per the §04B.6 BS-04B-4 rule (Phase-7 mechanical-op units); cross-checked via ORI_TRACE_RC=1 + compiler_repo/diagnostics/rc-stats.sh; recorded per-benchmark (baseline | burden-normalized | gap %) in decisions/gate-criterion-6-evidence.md (§05.4 re-run section). Result: closures 9|9|0%, sum 2|2|0%, conditional 3|3|0%; runtime trace cross-check (300000|0|300000 events) agrees baseline≡burden. All build clean + run leak-free.
• If any benchmark gap > 5%: NOT TRIGGERED — all three gaps are 0% (≤5%). decisions/gate-criterion-6-extensions.md NOT authored; no section-05A-lattice-extension-gap.md sibling promotion needed. (Conditional preserved verbatim for the record: author/read decisions/gate-criterion-6-extensions.md; integrate the listed Phase 6 lattice extensions; re-measure; if STILL > 5% post-integration promote section-05A-lattice-extension-gap.md per routing.md §4 with inserts_after: "05" per routing.md §5; NEVER escalate to user; NEVER close §05 with the gap open — sibling owns the residual via blocks_section_complete.)
• If all three benchmarks ≤5% gap: no extensions needed; recorded “all benchmarks within 5% — no Phase 6 extensions required” in decisions/gate-criterion-6-evidence.md (§05.4 re-run section Verdict).
• TPR checkpoint — /tpr-review AND /impl-hygiene-review covering 05.1-05.4. Exit-reason → next-action routing is owned canonically by the orchestrator (scripts/plan_orchestrator/next_action.schema.json + orchestration-rules.json:skill_exit_reasons), consumed per skill-control-contract.md §Continuation Contract + §Iteration-loop discipline; this checkpoint does NOT re-author a routing table. Every emitted exit_reason routes: clean / resolved → advance to §05.N close-gate; findings → /verify-tpr triage then re-dispatch per review_pipeline: frontmatter; cap_reached_with_substantive / cap_reached_clean → record review_pipeline.rounds_completed + last_round_commit and continue (no exit_reason left unrouted under autopilot per skill-control-contract.md §Autopilot Mode). Under autopilot a hook-failure halt on the round’s /commit-push proceeds with dirty tree + logged disposition per the unified hook-failure clause — it never terminates the checkpoint.

05.R Third Party Review Findings

• None.

05.R.H Hygiene Findings

• [PLAN_DELIVERY_DRIFT:Major — RECORDED, non-blocking; anchor: /fix-bug Phase 5 Step 9.5 reconciliation] bug-tracker/ (16 closed bug plans) — 16 closed bug plans missing delivered_to_roadmap: field (MISSING_PROPAGATION). Does not block §05 close (scope_match:false — cross-repo tracking metadata gap outside ori_arc/ori_llvm primary scope). Cure: run /fix-bug Phase 5 Step 9.5 reconciliation on affected closed bug plans, or backfill delivered_to_roadmap:; entries where subsection is undeterminable require human review per PLAN_DELIVERY_DRIFT.UNRESOLVED_SUBSECTION. [F3]

05.N Completion Checklist

• Baseline-red snapshot disposition (success_criterion line 19; §03 HISTORY 2026-05-15 cycle 50a deferred-to-§05 anchor): compiler_repo/compiler/oric/tests/aims-snapshots/realize_rc_reuse/aliased-value-keeps-rc.alias_test.realize_rc_reuse.after.arc (test aims_snapshots_across_all_passes_match_baselines) resolved — EITHER (a) Phase-6 burden→lattice rewrite restores the symmetric RcDec %2 [FatPtr] pair → snapshot unchanged + test passes, OR (b) the elision is provably correct under burden discipline → re-bless via ORI_BLESS=1 cargo test -p oric --test aims_snapshots aims_snapshots_across_all_passes_match_baselines AND amend a §05.N HISTORY entry citing burden-discipline rationale + spec citation, OR (c) the residual is a tracked compiler defect → /add-bug filed with the BUG-XX-NNN recorded here. The §05 close gate requires (a), (b), or (c) decided — never left open. RESOLVED via disposition (c): BUG-04-132 filed (bug-tracker/plans/BUG-04-132/; codegen-llvm, high). The snapshot is an over-dec (committed baseline RcInc %0 + RcDec %5 = 1 inc / 1 dec balanced; current emission inserts a spurious RcDec %2 [FatPtr] → 1 inc / 2 dec). GROUND-TRUTH: PREDICATE-STACK-rooted (reproduces with ORI_DISABLE_BURDEN_OPS=1; stable inc=[0] dec=[2,5] across after_phase_1_walk..after_phase_3_coalesce), so it is NOT a §05 Phase-6 burden/eliminator gap — §05 owns the burden baseline + eliminator, NOT predicate-stack repair. Same predicate-stack RC-imbalance CLASS as BUG-04-123 (distinct manifestation: straight-line aliased let-binding vs sum-type CFG-branch); §06/§09-coupled per decisions/LEDGER.md §B.3, dissolves at §09 (predicate-stack retirement). Option (b) re-bless is REJECTED — blessing a 1-inc/2-dec over-dec is INVERTED-TDD:positive-test-modification (it would enshrine a double-free shape into the baseline). The snapshot stays red WITHIN the §06/§09-coupled baseline (line below); the green obligation lands at §09, not §05.
• Phase 6 lattice operates as pure optimizer over the §03A-delivered coexistence-mirror-balanced baseline; CRITICAL invariant verified (lattice ELIMINATES burden-emitted ops, never CONSTRUCTS). The self-sufficient-baseline correctness gate (Phase-6 elimination with the reconcile_burden_ledger coexistence mirror OFF) is a §09 verification item per §09.4 — §05’s scope is mirror-balanced DP-2/DP-3 elimination correctness, not the post-retirement self-sufficient baseline §09 owns.
• RL-31 burden-aware path produces type-level disjointness proofs (facet (b)); the dual-facet noalias gate (RL-31.proof P2) conservatively OMITS noalias until the call-site-provenance facet ships.
• RL-31 × Phase 6 barrier / KnownSafe / PRE-style-motion legality co-verification sweep PASSES with evidence in decisions/05-rl31-co-verification-evidence.md (per §05.3 + codex blind_spot[1]).
• consumes_proof_product: frontmatter key matches section-00-design-validation-gate.md frozen_rule_version: (per opencode blind_spot[3]); scripts/plan_corpus check clean. exit 0 (verified this session)
• Criterion-6 benchmarks authored + run + normalized RC counts recorded in decisions/gate-criterion-6-evidence.md (§05.4; unconditional — §04B C6=complete override moved this deliverable to §05); any >5% gap closed via decisions/gate-criterion-6-extensions.md integration.
• ori_arc lib green (debug + release) AND no NEW test-all failures beyond the §06/§09-coupled baseline (LEDGER §B.3: AOT 2284/19 = 17 BUG-04-123 predicate-stack double-frees + 2 VF-1 loop residuals, ALL §06/§09-coupled, none §05-emission bugs). The 19 AOT residuals dissolve at §09 (predicate-stack retirement), NOT §05; absolute-green test-all is the §12 green-gate (green-gate red-partition), not §05’s close-gate. §05’s deliverable is the eliminator-only lattice over the mirror-balanced baseline — verified by ori_arc green + zero new lattice-divergence (success_criterion line ~22). A/B ORI_DISABLE_RL31_NOALIAS=1 + ORI_DISABLE_BURDEN_OPS=1 confirm comm -23 active disabled empty (zero new regressions from §05’s emission/elimination).
• Plan annotation cleanup.
• Plan sync per protocol; mission criterion 9 checkbox flipped (the 00-overview.md line-105 §05-delivering bullet: “Phase 6 lattice rewrite … → §05”).
• /tpr-review passed (final); /impl-hygiene-review passed. /review-plan ran 2 /tpr-review rounds, stage=verify-done; /impl-hygiene-review ran this session — 7 findings, 6 resolved + F3 recorded-non-blocking

HISTORY

• 2026-07-13 — §05’s shipped “Phase 6 lattice-rewrite” architecture (05.0-05.4 body + the “Fresh intel” fold below) is SUPERSEDED by BUG-04-276 (class-ledger-sole consolidation). eliminate_burden_ops (realize/burden_elim.rs) + its 6 submodules + the entire lower/burden_lower/ directory — described throughout this section (notably §05.1 lines 89-121, §05.2 line 149, §05.N line 220) as the shipped Phase-5-emit → Phase-6-eliminate two-pass burden architecture — were DELETED as dead code (reachable only from their own tests). run_aims_pipeline’s Step-4b class-ledger emission (apply_class_ledger_replacement) had already superseded the two-pass burden architecture as the sole production RC emitter before this bug’s RCA (commits ec53bf9ec6/d06aa9353f, 2026-07-10/11); the separate emit-then-eliminate pass this section documents as live was orphaned dead code by that point, not a §05 regression. The section’s PROVEN calculus grounding (DP-2/DP-3, CH-1/CH-2, RL-comp) is UNAFFECTED — class-ledger planning FUSES the same DP-2/DP-3-equivalent verdict into its plan at Step 4b (per aims-rules.md §7 + §12 PV-1..PV-6); only the separate-pass architecture this section narrates as shipped is gone. Current normative framing: .claude/rules/arc.md §Canonical RC-Emission Path, .claude/rules/canon.md §7.1 invariant 5. Disposition record: bug-tracker/plans/completed/BUG-04-276/. The “Fresh intel” fold below (regenerated pre-BUG-04-276) is now itself PRE-FIX-STALE — its claim that eliminate_burden_ops is “the single hottest function on the entire burden surface” describes deleted code; regenerate on the next /review-section pass rather than trusting it. reviewed: left as-is (drift triggers reversal per state-discipline.md §4).

• 2026-07-01 — §05.4 section-close TPR (rounds 1-2) cures + plan-wide two-ADR-tree structural anchor. Cured: RL-31 noalias ADR (decisions/01) Decision+Consequences (Option A dual-facet gate, conservative omission) + status→accepted; the (m) panic/unwind forward-soundness row (decisions/00 risk-shape matrix) + co-verification forward-soundness table (decisions/05); §05.3 body reconciled to the BUG-04-241 exec-blocked reality (the 3 rl31_*_exec AOT tests are #[ignore]’d per decisions/05 §Correction) + the nounwind precondition; code-side hygiene (nounwind gate-site comments at function_compiler/mod.rs + rl31_disjoint.rs, inaccurate borrowed_inner comment, canonical // Env: docs for ORI_DISABLE_{LINEAGE_REBALANCE,SINGLE_RELEASE_AFTER_LAST_READ,RL31_NOALIAS}, geographical-framing comment links, oversized-file splits of burden_elim.rs/function_compiler/mod.rs). STRUCTURAL ANCHOR for /review-plan (NOT resolved here — plan-wide, ambiguous canonical, history-loss risk): the plan carries TWO diverged ADR trees — plan-root decisions/ (cited by the section body; legacy) and content/decisions/ (cited by the ledger-evolution machinery + status.md + intel; carries unique newer decisions 17/18/19 lean-license). The §05 ADRs {00,01,05-rl31} were reconciled to IDENTICAL across both trees this cycle; the plan-wide canonical-tree consolidation (finish the v7 migration, merge the tree-unique files, remove the non-canonical tree, update all refs) is a plan-structural decision the plan’s own /review-plan owns.

• 2026-06-02 — §05.N baseline-red snapshot disposition (c) decided: BUG-04-132 filed. The aliased-value-keeps-rc snapshot (@alias_test () -> void = { let $s = "hello"; print(msg: s); print(msg: s); }) is an over-dec: committed baseline .after.arc is RcInc %0 + RcDec %5 (1 inc / 1 dec, balanced); current emission inserts a spurious RcDec %2 [FatPtr] (after burden_dec %0, before the 2nd borrow-print) → 1 inc / 2 dec. Both %2 and %5 are FatVal aliases of owned %0. RIGOROUSLY ESTABLISHED as PREDICATE-STACK-rooted, NOT a §05 Phase-6 burden/eliminator gap: the over-dec reproduces with ORI_DISABLE_BURDEN_OPS=1 (burden path OFF) and is stable inc=[0] dec=[2,5] across all realize phases (after_phase_1_walk..after_phase_3_coalesce); the defined-dead-elision pass logs defined-dead RcDec SKIPPED (early) reason=not-managed-defined-dead for vars 0/2/5 (redundant dec not elided). Disposition (c) chosen (NOT (a) restore — §05’s eliminator-only lattice does not construct predicate-stack repairs; NOT (b) re-bless — blessing the double-free shape is INVERTED-TDD:positive-test-modification). Filed BUG-04-132 (bug-tracker/plans/BUG-04-132/, codegen-llvm, high): same predicate-stack RC-imbalance CLASS as BUG-04-123 (distinct manifestation), §06/§09-coupled per decisions/LEDGER.md §B.3, dissolves at §09 (predicate-stack retirement). The relatedness verdict’s mechanical needs_plan_escalation/case-(e) (inline-into-§05) was overridden: case (e) requires a NOT-STARTED matched section but §05 is in-progress, and the cure is owned by the not-started §09, not §05 — disposition (c) mandates the separate tracker entry. The snapshot stays red WITHIN the §06/§09-coupled baseline (L275); green lands at §09/§12, not §05. Drifts the reviewed section → §05 re-reviews on next scan (reviewed: left as-is; drift triggers reversal per state-discipline.md §4).

• 2026-06-02 — §05.N L275 close-gate re-scoped to §05’s actual deliverable (plan-coherence correction). The - [ ] cargo t green; debug + release close-gate was unsatisfiable at §05 close: per decisions/LEDGER.md §B.3 the AOT 2284/19 residuals (17 BUG-04-123 predicate-stack double-frees + 2 VF-1 loop residuals) are ALL §06/§09-coupled and dissolve at §09 (predicate-stack retirement), NOT §05 — “none §05-emission bugs.” An absolute-green close-gate on §05 created a false circular dependency (§05 close needs green → green needs §09 → §09 depends_on the §05→§06→§07 chain). The plan’s own structure puts the absolute-green gate at §12 (green-gate red-partition); §05’s deliverable is the eliminator-only lattice over the mirror-balanced baseline, whose correctness gate is ori_arc green + zero NEW lattice-divergence (success_criterion line ~22). Re-scoped L275 to “ori_arc green + no new failures beyond the §06/§09-coupled baseline” with ORI_DISABLE_RL31_NOALIAS/ORI_DISABLE_BURDEN_OPS A/B confirming zero new regressions. Coherence correction (the green requirement was mis-scoped onto §05; §05 never owned the §06/§09-coupled failures), NOT gate-weakening. Drifts the reviewed section → §05 re-reviews on next scan, converging on the satisfiable gate. reviewed: left as-is (drift triggers reversal per state-discipline §4).

• 2026-06-02 — §05 close-out /review-plan pass (Step 5 editor + §05.R section-close TPR). Editor cures: RL-31 noalias evidence reconciled to conservative-omit (§05.3 + decisions/05-rl31-co-verification-evidence.md worked-example IR blocks now show noalias OMITTED, citing RL-31.proof P2 dual-facet — type-facet proven, call-site-provenance facet unshipped per aims-rules.md §1.9 rules 5+7; ground-truth-verified against shipped rl31_disjoint.rs call_site_provenance_proven: false gate + FileCheck CHECK-NOT: ptr noalias pins); coexistence-mirror-disabled correctness gate relocated §05 → §09.4/§09.N (it tests the self-sufficient burden baseline §09 retires the predicate stack for, not §05’s mirror-balanced elimination); subsection_depends_on 05.4 re-pointed [05.3] → [05.2] (benchmarks consume Phase-6 dimension-wired output, not RL-31); §05.N baseline-red-snapshot disposition close-gate added. §05.R TPR round-1 cures: criterion-6 benchmark success_criterion .rs → .ori (delivered files are .ori); §05.0 sites-11-12 success_criterion reconciled from “dissolved” to “re-absorbed via get_required supplementary site” matching §05.0 body line 141; this HISTORY entry (post-editor change record). reviewed: stays false (TPR round in progress; close-out flip owned by /review-plan Step 7+8).

• 2026-05-29 — §05 regrounded on the PROVEN DP-2/DP-3 elimination calculus (per 00-overview.md 2026-05-29 reground). Phase 6’s elimination-only role consumes is_rc_dec_unnecessary (DP-2: Cardinality=Absent ∨ Consumption=Dead) + is_rc_inc_elidable (DP-3: Cardinality=Once ∧ Consumption=Linear) — both kernel-checked in consolidated compiler_repo/aims-proof/lean/AimsProof/Decision.lean (DP2_is_rc_dec_unnecessary_table / DP3_is_rc_inc_elidable_table), gating the proven RL-2 dec / RL-1 inc emission whose RC-BALANCE net-0 invariant is proven in Realization.lean. The §05 honest-limit (elimination-side dependency on project_alias_sources / borrow_sources) is bounded above by §09’s coexistence retirement: once the predicate stack is deleted, the elimination decisions rest solely on the proven DP-2/DP-3 over the converged AimsState, not on the transitional coexistence alias-tracking that the completed burden path supersedes (the coexistence CH-1..CH-comp are themselves proven_sound per aims-rules.md HISTORY 2026-05-28 — the layer is retired as superseded, not as unproven). RL-31 (the §05.3 burden-aware path) is REAL in Realization.lean (RL31_disjoint_borrowed_noalias + dual-facet RL31_type_facet_alone_insufficient), so §05.3 implements a proven theorem, not a design hypothesis. reviewed: stays false (cross-section reground edit on a not-started section).

• 2026-05-12 — §00 editor cohesion-edit (per section-00-design-validation-gate.md §00.3 line 376 + codex blind_spot[1] + opencode blind_spot[3]): §05 success_criteria gained two new entries — RL-31 metadata × Phase 6 barrier / KnownSafe / PRE-style-motion legality co-verification sweep (cures gap where §00.3 mandated the sweep be filed as §05 success criterion but §05 itself only carried generic lattice convergence criteria); consumes_proof_product: v1 ↔ §00 frozen_rule_version: v1 producer/consumer contract verification. §05.3 body extended with three co-verification test shapes (KnownSafe pair elimination, PRE-style motion across RC-observable barrier, clang-arc §02 selective barrier flush) + §00 producer/consumer contract anchor. §05.3 also updated the example shape to merge(a: &{str:int}, b: &[int]) (Worked Example 1b Borrowed+Borrowed RL-31-native shape) plus the existing accumulate Owned+Borrowed generalization. §05.N completion checklist extended with co-verification + consumes_proof_product items. reviewed: field left false per /review-plan SKILL.md §Step 1.7 §D Critical Rule 9 (cohesion-edit on non-target section).

• 2026-05-25 — Cross-plan advisory dependency established (aims-proofing-suite §14): §05’s Phase-6 lattice rewrite (RL-31 burden-aware path) consumes proven calculus from plans/completed/aims-proofing-suite/ §08 (Realization Rule Proofs — RL-2/RL-10/RL-31) + §11 (Coexistence Handshake Proofs), both not-started. Per aims-proofing-suite §14 Lazy-Migration Policy this pointer is ADVISORY + NON-BLOCKING: §05 proceeds under “design assumed sound; subject to revision when proofs land.” A frontmatter blocked_by: is not used — scripts/plan_corpus/schema.py:_check_blocked_by_shape restricts blocked_by: to BUG-XX-NNN; cross-plan proof dependencies bind via this narrative pointer (and, for criterion-gated sections, via the §13 proven_by: mechanism, which §05 does not use since it consumes proven design rather than empirically gating criteria). Enforcement flips (verdict semantics shift to “implement against proven design”) once §08 RL-10/RL-31 + §11 reach proof_status: complete; C3 on §04B proven_by: already flipped pending → partial at §05.3 close-out and flips to complete on §08 RL-10 PASS. reviewed: left false per /review-plan SKILL.md §Step 1.7 §D Critical Rule 9 (cross-plan binding edit on non-target section in not-started status).

• 2026-05-15 — Baseline-red snapshot anchor pulled forward from §03 HISTORY cycle 50a deferral. aims_snapshots_across_all_passes_match_baselines (compiler/oric/tests/aims_snapshots.rs:28) fails on realize_rc_reuse/aliased-value-keeps-rc.alias_test.realize_rc_reuse.after.arc: baseline emits an RcDec %2 [FatPtr] between the two ori_print(s) calls that the current realize_rc_reuse pass elides. The §03 (Phase 5 trivial emission) HISTORY recorded “needs re-bless OR root-cause investigation deferred to §04A/§05” without a structural anchor; this entry pairs that deferral with a concrete §05 success_criterion (added same edit) so the cure obligation is tracked under the Phase 6 lattice rewrite that owns realize_rc_reuse output behavior. Disposition decided at §05 close (re-bless under burden-discipline rationale OR rewrite restores the dec). reviewed: field left false per /review-plan SKILL.md §Step 1.7 §D Critical Rule 9 (success_criterion edit on non-target section currently in not-started status). Per feedback_plan_cures_failures_linkage pre-JSON-v3 mechanical attribution unavailable — narrative + success_criterion is the structural surface today.

• 2026-05-27 — Cross-plan advisory dependency established (locality-representation-unification): §05.2’s “Locality … unchanged” refers to the dimension’s ROLE (RL-14 stack promotion / RL-17/18 header compression), not its variant count. plans/locality-representation-unification/ (not-started; absorb-candidate into plans/roadmap/section-21A-llvm.md; NOT superseded by this plan) changes shipped Locality to 5 variants (adds ArgEscaping), raises CHAIN_HEIGHT 15→16, and converts ParamContract.may_escape from a stored field to a derived method. §05.0’s contract/ IC-1 hardening + §05.3’s RL-31 path consume ParamContract; if locality has landed they consume may_escape() as a derived method. ADVISORY/NON-BLOCKING per routing.md §1 (schema restricts blocked_by: to BUG-XX-NNN; the cross-plan dependency binds via this narrative pointer + decisions/04 Clarification). SHOULD sequence after locality to avoid a contract/ + split-aims/-file rebase. None of §04B’s C1-C6 criteria depend on ArgEscaping, so locality is NOT a gate blocker — it is a §05 sequencing input + the shipped-conformance bridge for the proven 5-variant Locality rules (aims-proofing-suite §17). reviewed: left false (cross-plan binding edit on a not-started section).

Fresh intel (regenerated)

This section’s body reads as fully DELIVERED — five subsections (05.0–05.4), each with cycle-level evidence, test IDs, and [x]-checked work items. The graph and direct-source cross-check CONFIRM the substance is real and shipped: eliminate_burden_ops is the single hottest function on the entire burden surface (hotspot 1271, matching the mission’s own cited ~1580 figure to within recon-tool drift), prove_param_noalias + the dual-facet noalias gate are wired exactly where the body claims (function_compiler/mod.rs:376-407), and every cited spec/AOT test file exists on disk with the described CHECK-NOT content. But the plan’s own plan.json says this section’s workflow status is not-started, reviewed: false — because the ENTIRE plan was zeroed (0/29 sections complete) for a forensic re-walk. The body’s “DELIVERED” claims are prose, not the SSOT; this review is exactly the mechanism that re-grounds them.

Three decisions this package forces before the review adjudicates:

1. The section’s substance re-verifies clean — do not re-litigate 05.0/05.1/05.2/05.4; they are IC-1 hardening, lattice-audit-with-structural-guard, dimension-wiring-with-pins, and a criterion-6 benchmark that all check out against live source, hotspot data, and plan ownership. Spend review budget on 05.3.
2. 05.3’s one real open engineering gap is RL-31 facet (a) (NoaliasProof.call_site_provenance_proven hardcoded false, per-call-site interprocedural provenance unshipped) — and external prior art says the ORIGINAL design choice that created this gap (function-attribute noalias, decisions/01-noalias-emission-granularity.md Option A) is the harder of two SUFFICIENT-condition-compatible choices. decisions/01’s own “Decision” + “Consequences” sections are STILL EMPTY despite Option A already being implemented — a real plan-coherence gap, not a stylistic one.
3. A NEW risk shape is missing from the 12-shape acceptance matrix (a)–(l): none of the 12 shapes address whether a callee’s panic/unwind mid-execution can violate the noalias claim’s “no other access during execution” guarantee — this is EXACTLY the lesson rustc learned the hard way (it once emitted noalias for &mut params, then stopped, because “LLVM’s semantics miss the ‘is known not to panic’ requirement,” per rust-lang/rust-memory-model#24). Ori’s ARC IR has Invoke/Resume unwind terminators; this gap is real and unaddressed anywhere in the section’s evidence.

[JOIN] The graph’s callers/cypher CALLS-edge resolution has a repeatable false negative on exactly this code region: prove_param_noalias and add_noalias_attribute’s PRODUCTION call sites (both inside declare_function_llvm_with_extra_params, function_compiler/mod.rs) are invisible to the graph (callers returns test-only lists; a direct cypher non-test-caller query returns 0 rows) even though grep proves both call sites exist and are load-bearing. Any FUTURE blast-radius analysis on this file done via the graph alone will silently under-count callers — flag before trusting a callers result on function_compiler/mod.rs.

DIG DEEPER

python -m scripts.plan_corpus.read plans/aims-burden-tracking   # plan.json status="in-progress"; per-section status via the API below
python3 -c "from scripts.plan_corpus.read import load_plan; p=load_plan('plans/aims-burden-tracking'); print([s for s in p.subsections if s.get('id')=='s-09a822f6'])"
scripts/intel-query.sh plan-status aims-burden-tracking --human

(full dossier: phase-6-lattice-rewrite-rl-31-burden-aware-path—s-09a822f6.intel.md)