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 12 lookup sites (BUG-04-112’s 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 per BUG-04-112/section-05-implementation.md §1.0 archive)
• 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

• 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.

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).

05.1 Lattice consumption-mode shift (emission → elimination)

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 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.

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_rc_dec_unnecessary) / DP-3 (is_rc_inc_elidable) — pure predicates; consumed ONLY by burden_elim.rs. Unchanged.
• realize/decide.rs (decide/decide_last_use/decide_annotations/decide_cow/decide_drop_hint) + realize/walk.rs — the predicate-stack RC realization path. Emits RcInc/RcDec only; walk.rs PRESERVES burden ops verbatim (new_body.push(instr.clone()) at the burden-op arm) — it constructs no burden ops. This is the retiring predicate-stack path (§09), burden-transparent. 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.

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/...).

• Cardinality + Consumption dimensions: drive DP-2 (is_rc_dec_unnecessary) + DP-3 (is_rc_inc_elidable) per-instruction at burden-op sites. Source: predicates at ori_arc/src/aims/transfer/mod.rs (fn is_rc_dec_unnecessary :405, fn is_rc_inc_elidable :413); consumer at ori_arc/src/aims/realize/burden_elim.rs (fn eliminate_burden_ops :87). VERIFIED: HEAD anchors confirmed (is_rc_dec_unnecessary :405, is_rc_inc_elidable :413, eliminate_burden_ops :87). eliminate_burden_ops is the SOLE Phase-6 burden-op consumer; it queries DP-2/DP-3 against var_state_at_block_exit and removes-only (paired-elimination preserves VF-1 balance). Burden ops are TF-N/A in both transfer directions, so block_exit_state IS the per-burden-op-site state — the dimension drives the elimination correctly over burden-emitted IR. Already pinned in realize/burden_elim/tests.rs (25-cell DP-2/DP-3 × variant matrix + §05.1 census pins).
• Uniqueness: drives COW (StaticUnique in-place vs Dynamic runtime check vs StaticShared unconditional copy) — unchanged. Source: ori_arc/src/aims/emit_rc/cow.rs (COW emission helpers) + ori_arc/src/aims/realize/decide.rs (fn decide_cow :438, DP-9 mode selection). VERIFIED: decide_cow :438 confirmed; routes Uniqueness → CowMode (DP-9): Unique (no active borrow) → StaticUnique, Shared → StaticShared, MaybeShared → Dynamic (absent disjoint-borrow proof). The consumer reads the converged Uniqueness dimension regardless of burden-op presence — burden ops carry no transfer effect, so the dimension’s meaning at the COW site is unchanged. Role survives the emission→elimination shift.
• 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: drives stack promotion (RL-14) + RC-header compression (RL-17, RL-18) — unchanged. “Unchanged” = the dimension’s ROLE, not its variant count. RL-14/RL-17/RL-18 consumption is order-based (variant-count-agnostic), so the role survives any variant-count change. Source: ori_llvm/src/codegen/abi/mod.rs (stack-promotion + header-width ABI decisions consuming Locality). VERIFIED (with source correction): the cited ori_llvm/src/codegen/abi/mod.rs RL-14/RL-17/RL-18 codegen consumer is STUBBED/target-only per repr.md §Shipped vs stubbed passes — analyze_escape (RL-14 stack promotion) + compress_arc_headers (RL-17/RL-18 header narrowing) are empty-body passes; shipped abi/mod.rs does size-based heap classification (RL-16 via abi_size), not Locality-variant-driven stack promotion. The SHIPPED order-based Locality consumer is the lattice predicate pair AimsState::is_local (DP-8, lattice/mod.rs :442 = BlockLocal | FunctionLocal) + AimsState::is_rc_skip_eligible (DP-7, :430 = is_local ∧ Owned ∧ Linear ∧ Once ∧ Unique). Both consume Locality by ORDER (≤ FunctionLocal vs ≥ HeapEscaping), so the role is variant-count-agnostic and holds identically for the shipped 4-variant Locality and the target 5-variant lattice. Not a bug — the codegen RL-14/17/18 passes are deferred per repr.md, NOT broken-over-burden; the order-based DP-7/DP-8 consumer survives the emission→elimination shift unchanged.
• 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_rc_skip_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 (the order-tail) so the predicates hold when the 5th variant (ArgEscaping, ordered between FunctionLocal and HeapEscaping) lands — ArgEscaping is ≥ HeapEscaping? No: it is > FunctionLocal, so DP-8 is_local returns false (correct: ArgEscaping is NOT local per aims-rules.md §4 DP-8), and the existing HeapEscaping/Unknown negative pins already clamp the not-local / not-skip-eligible region the new variant joins. No §05 logic change required either way.
• Effect summary: continues to inform interprocedural contracts + LLVM fact export (RL-29, RL-30, RL-31). Source: ori_llvm/src/codegen/function_compiler/purity_analysis.rs (memory(none)/memory(read) derivation, RL-30) + ori_llvm/src/codegen/ir_builder/attributes.rs (fn add_noalias_return_attribute :96, RL-29; !alias.scope/!noalias pair emission, RL-31). VERIFIED: purity_analysis.rs consumer confirmed (has_only_pure_arc_instructions + is_abi_memory_free gate memory(none)/memory(read) per RL-30, AT-3); add_noalias_return_attribute :96 confirmed (RL-29 sret path, AT-2). Per codegen-rules.md §8 AT-5 the shipped attributes derive from ARC-IR-shape + ABI analysis, NOT yet from the full RL-29/30/31 EffectSummary pipeline (RL-31 alias-metadata emission is NOT shipped — that is §05.3 scope). The RL-30 consumer (has_only_pure_arc_instructions) reads the post-lowering IR shape; burden ops are NOT in its pure-instruction allow-list, so the burden-emitted baseline cannot silently produce a spurious memory(none) — and by codegen (Phase 7) burden ops are lowered to RcInc/RcDec which also block purity, so the classification is stable across the emission→elimination→lowering shift. Role survives.
• 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):

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: elidable-state burden op removed; negative: Many ∧ Unrestricted / Many ∧ Linear / Once ∧ Affine burden op preserved).
• Uniqueness → DP-9 decide_cow, Shape + Uniqueness → DP-6 is_reuse_candidate, Locality → DP-7/DP-8 (is_rc_skip_eligible/is_local): compiler_repo/compiler/ori_arc/src/aims/realize/dimension_consumer/tests.rs (new). 13 pins: Unique→StaticUnique / Shared→StaticShared positive + MaybeShared not-StaticUnique (UAF) negative; Owned∧≠Shared∧Reusable→candidate (incl. MaybeShared RL-11a) positive + Shared / NonReusable not-candidate (alias-corruption) negatives; ≤FunctionLocal∧Unique→is_local/is_rc_skip_eligible positive + HeapEscaping / Unknown not-local / not-skip-eligible (dangling-pointer) negatives.
• Effect summary → RL-30 (has_only_pure_arc_instructions / memory(none) gate): compiler_repo/compiler/ori_llvm/src/codegen/function_compiler/purity_analysis/tests.rs (3 new §05.2 pins): pure-IR → memory(none)-eligible positive; effectful Apply not-eligible negative; residual BurdenInc not-eligible (burden-baseline non-poisoning) negative. RL-31 alias-metadata emission is §05.3 scope (not shipped), so its pins land at §05.3.

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

Subsection close-out (05.2) per protocol.

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.

• 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. 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 3/3 (execution + leak-free + dual-facet-gate-invariance). 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 (results 23/16/8, zero leaks). 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.

Subsection close-out (05.3) per protocol.

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%.

• 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 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.

Subsection close-out (05.4) per protocol.

05.R Third Party Review Findings

• None.

05.R.H Hygiene Findings

• [WASTE:Minor] compiler_repo/compiler/ori_arc/src/aims/realize/emit_unified.rs:241 — ORI_DISABLE_BURDEN_ELIM read via std::env::var on the per-function realization path; invariant value re-read + String allocated once per compiled function. Cure: cache once at pipeline-config time as bool on AimsPipelineConfig; bundle with sibling env reads (ORI_DISABLE_BURDEN_OPS, ORI_DISABLE_REDUNDANT_CLEANUP, ORI_DISABLE_RL31_NOALIAS) into an AimsDiagnosticFlags struct (litter-pickup — all four follow the same pattern). [F1][TP-CONFIRMED-both]

• [NAMING:Minor] compiler_repo/compiler/ori_arc/src/aims/realize/emit_unified.rs:244 — trace_phase_snapshot("after_phase_2_5_burden_elim", ...) labels burden elimination as “Phase 2.5” in the snapshot trace channel; arc.md §Canonical RC-Emission Path + aims-rules.md §8 name burden elimination “Phase 6”. Internal numbering (Phase 1/2/2.1/2.5/3) collides with canonical Phase 5/6/7 burden architecture. Cure: rename snapshot key to after_phase6_burden_elim OR add // INVARIANT: Phase 2.5 (local) = canonical Phase 6 (arc.md §Canonical RC-Emission Path) at emit_unified.rs:232; keep arc.md §Debugging trace-target list in sync if renamed. [F2][TP-CONFIRMED-both]

• [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]

• [NAMING:Minor] compiler_repo/tests/spec/traits/traceable/definition.ori:64 — test named @test_ok; weak descriptor communicates nothing about subject/scenario/expected. Per impl-hygiene.md §Test Function Naming, NAMING violations are renamed inline, never deferred. Cure: rename to <subject>_<scenario>_<expected> (e.g., traceable_with_trace_attaches_entry); move provenance to a // doc comment above the test. Rename is local to the spec file (no callers). (scope_match:false; additive per plan-context disposition.) [F4]

• [COMMENT_HYGIENE_DRIFT:Major] compiler_repo/compiler/ori_arc/src/aims/realize/cleanup_redundant.rs:264 — eprintln!("[CLEANUP] func={:?} removing {:?}", func.name, removals); bare eprintln! in a production library crate. Per impl-hygiene.md §Tracing & Logging, library crates use tracing macros only. Cure: replace with tracing::debug!(func = ?func.name, removals = ?removals, "[CLEANUP] removing") or remove if diagnostic-only. [F5][TP-SURFACED-codex]

• [PUBLIC_LEAK:Critical] compiler_repo/compiler/ori_arc/src/aims/realize/cleanup_redundant.rs:3 — module doc //! Synthesized from /tp-help R1 codex consensus (2026-05-08): the over-emission … embeds internal wrapper-skill (/tp-help) and a dated session citation in compiler_repo (public OSS). Per CLAUDE.md §Public Repo Hygiene + impl-hygiene.md §PUBLIC_LEAK:wrapper-skill-reference, compiler_repo MUST NOT reference internal dev-workflow slash commands. Blocks §05 close-out. Cure: replace module doc with self-contained technical rationale; move provenance to commit message or wrapper-side plan HISTORY block. [F6][TP-SURFACED-codex]

• [WASTE:Minor] compiler_repo/compiler/ori_llvm/src/codegen/function_compiler/mod.rs:278 — let rl31_disabled = std::env::var_os("ORI_DISABLE_RL31_NOALIAS").is_some(); called per-function on the declare_function path. Same pattern as F1 (ORI_DISABLE_BURDEN_ELIM at emit_unified.rs:241). Cure: bundle into the AimsDiagnosticFlags config proposed for F1; cache once at pipeline-config time. [F7][TP-SURFACED-agy]

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-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).