Section 00: Phase A0 — Design Validation Gate

Status: complete Goal: Validate the registry-layer value claim BEFORE registry implementation work begins. The deliverable is a design walkthrough document — not code.

Scope-confinement (load-bearing per acceptance target 9): §00 evaluates ONLY “does the registry-data layer justify the RL-31 burden-aware path?” §00 does NOT validate Phase 6 alias-tracking soundness (the elimination-side failure mode per 00-overview.md §Motivation + proposal §Honest Acknowledgment of Limits). Phase 6 soundness on the BUG-04-118 shape is owned by §04B Prototype Gate criterion 3 (proposal:526). Borrowed confidence from §04B’s criterion 3 is NOT a substitute for §00’s own RL-31 design deliverable; §00 closes on its own evidence or falls back.

Success Criteria:

• Walkthrough document at plans/aims-burden-tracking/decisions/00-rl31-burden-aware-design.md exists with both worked examples + the §00.1 SUFFICIENT-noalias generalization (NOT IFF; 8 clauses) + the 12-risk-shape coverage matrix.
• Per-example pass/fail TABLE per §00.2 acceptance target 3 — concrete shape comparison, not hand-wave acceptance.
• Comparison vs contract layer’s borrow_sources / project_alias_sources provenance approach is explicit AND bidirectional (burden-wins, contract-wins, coincide).
• Outcome recorded in this section’s frontmatter: outcome: registry-justified OR outcome: fallback-direct-perceus (key added to frontmatter at §00.3 close).
• On fallback-direct-perceus: §04A disposition explicitly recorded per acceptance target 8 (§04A survives — paired-baseline emission still applies). (N/A under registry-justified — §04A wires BurdenInc/BurdenDec as designed per §00.3 line 449.)
• clang-arc-lessons Phase 0 reentry disposition recorded per acceptance target 10 (alters-reentry OR orthogonal-to-reentry). (Orthogonal under registry-justified path per §00.3 line 441.)

Context: This is Phase A0 — a separate gating phase BEFORE §01-§04. The proposal explicitly documents direct Perceus (roc#825, roc#5258) as the fallback if the registry layer cannot justify itself. Failing CHEAPLY at design-walkthrough time has bounded cost; failing after §01-§04 registry implementation has unbounded cost.

Reference implementations:

• Koka kklib Perceus implementation — direct Perceus shape (no per-type registry data).
• Roc compiler/gen_refcount/ — Roc’s Perceus adoption (roc#825, roc#5258).
• Lean 4 IR/Borrow.lean + IR/RC.lean — borrow inference as parameter annotations + per-function RC insertion (parallel to Phase 5/6 split shape).

Depends on: None. Phase A0 is the first gate.

Citations:

• aims-rules.md §8 RL-31 — disjointness proof contract that requires per-call-site root extraction from borrow_sources + project_alias_sources (the contract-layer baseline §00 must beat).
• aims-rules.md §1.9 Borrow Sources + Project Alias Sources — the side-table domains the contract layer consumes.
• aims-rules.md §4 DP-5 + Appendix C DP-5 — SetTag payload-invalidation rule (acceptance target 6).
• aims-rules.md §8 RL-10 — disjoint-field-mutation rule under DP-5.
• compiler_repo/docs/ori_lang/proposals/approved/aims-burden-tracking-proposal.md §Design — BurdenRegistry Data Layer (BurdenSpec shape including owned_fields, borrowed_fields, element_burden, variant_burdens).
• Proposal §Honest Acknowledgment of Limits — RL-29 / RL-30 Mostly Duplicate Contracts — RL-31 = the genuinely novel consumer; RL-29/RL-30 add little novel precision.
• Proposal §Roadmap §Phase A0 + §Prototype Gate criterion 5 — §00 deliverable definition.
• Proposal §Alternatives Considered §Alternative 1 (line 419 + line 425) — direct-Perceus fallback emits paired dup/drop ops; lattice still optimizes paired baseline.
• Proposal §Roadmap §clang-arc-lessons Handoff (line 551) — barriers / KnownSafe / COW-contraction / PRE-style RC motion translate onto burden baseline.

Intelligence Reconnaissance

Queries to run at section start (date when run): 2026-05-08

• scripts/intel-query.sh --human file-symbols "compiler_repo/compiler/ori_arc/src/aims/contract/" --repo ori — inventory MemoryContract / ParamContract / ReturnContract / EffectSummary surface
• scripts/intel-query.sh --human callers compute_project_alias_sources --repo ori — consumers of project_alias_sources provenance
• scripts/intel-query.sh --human callers populate_borrow_sources --repo ori — consumers of borrow_sources provenance
• scripts/intel-query.sh --human callers BurdenSpec --repo ori — currently zero hits (greenfield); re-run at §00 close to confirm registry-justified outcome did not pre-leak the symbol
• scripts/intel-query.sh --human similar BurdenSpec --repo koka,rust,swift,lean4 --limit 5 — cross-repo prior art on per-type drop-info data layers
• scripts/intel-query.sh --human callers SetTag --repo ori — confirm DP-5 SetTag-overlaps-every-field rule has no current carve-outs that would change the acceptance-target-6 walkthrough

Results summary (≤500 chars) [ori]: BurdenSpec greenfield (zero hits); project_alias_sources + borrow_sources are existing alias-tracking infrastructure consumed at multiple lattice optimization sites; SetTag DP-5 rule per aims-rules.md §8 RL-10 invalidates ALL fields on tag mutation. Walkthrough must show type-level precision BurdenSpec.field_type + borrowed_fields chains add ON TOP of these; zero precision delta on every shape → fallback to direct Perceus.

00.1 Walkthrough authoring (sufficient-noalias rule + 12 risk shapes)

File(s): plans/aims-burden-tracking/decisions/00-rl31-burden-aware-design.md (new — directory created at §00.1 start)

Author the worked design document. Coverage MUST include both worked examples AND the 12 identified-precision-risk shapes (a)–(l) below.

Worked examples (concrete code paths)

• Concrete example 1 — accumulate(a: {str:int}, b: [int]) (different-type case):

  • Construct the BurdenSpec graph for {str:int} (map type) per proposal §Design — BurdenRegistry Data Layer + the element_burden: Option<TypeId> field on BurdenSpec. Show: owned_fields chain through K (str heap-allocated; self_heap_alloc: true) + V (int — see acceptance target 4 / risk shape (c) below) + the map-element burden via element_burden.
  • Construct the BurdenSpec graph for [int] (list type) — element_burden: Some(TypeId(int)); int per risk shape (c).
  • Trace transitive closures of field_type chains for both a and b. Include borrowed_fields per acceptance target 2 / risk shape (b) — borrowed_fields is part of reachable memory for LLVM noalias, NOT only drop obligation.
  • State the SUFFICIENT-condition noalias rule (NOT an IFF — risk shape (a)): “If the transitive closures of (owned_fields ∪ borrowed_fields ∪ element_burden ∪ variant_burdens) for a and b share no TypeId for any HEAP-allocated component AND the type-system invariants in the supporting-invariants list below hold, then a and b are guaranteed non-aliasing and noalias is sound.” Cite aims-rules.md §8 RL-31 call-site provenance contract as the LOWER-precision baseline this rule is intended to BEAT, not weaken.
  • Conclude: LLVM noalias attribute on both a and b parameters justified by type-level disjointness PLUS the supporting invariants, NOT by per-call-site provenance.

• Concrete example 1b — merge(a: &{str:int}, b: &[int]) (canonical Borrowed+Borrowed pair, RL-31 native shape):

  • Per opencode blind_spot[2]: aims-rules.md §8 RL-31 targets !noalias metadata on Borrowed+Borrowed parameter pairs (noalias claim governs Borrowed memory aliasing). Worked Example 1 (accumulate(a: {str:int}, b: [int])) demonstrates the NATURAL GENERALIZATION to Owned+Borrowed (per decisions/00-rl31-burden-aware-design.md line 140 — RL-29 already attaches noalias to Owned fresh-allocation returns; the type-level proof is independent of Access). Example 1b authors the BORROWED+BORROWED canonical RL-31 shape so the proof rests primarily on the cited rule’s native target, with Example 1 documented as an ADDITIONAL benefit (Owned+Borrowed generalization).
  • Construct merge(a: &{str:int}, b: &[int]) -> {str:int} — both parameters Borrowed (ArcClass::DefiniteRef per arc.md §Key Types).
  • Apply the same 8-clause SUFFICIENT-condition walkthrough: closure sets S_a and S_b per BurdenSpec construction (Example 1’s BurdenSpec for {str:int} and [int] reused; pointee BurdenSpec consulted per Invariant 2 / Borrowed-param dereference rule).
  • Verify all 8 clauses hold: closure sets disjoint (clause 4); type system rejects same-binding (clause 7) because T_i = &{str:int} ≠ T_j = &[int]; FFI exclusion not triggered (clause 8). Per aims-rules.md §8 RL-31, function-attribute noalias lands on both Borrowed parameters (Option A per decisions/01).
  • Documentation pointer: this example is authored at plans/aims-burden-tracking/decisions/00-rl31-burden-aware-design.md §"Worked Example 1b — Borrowed+Borrowed canonical RL-31 shape" (new subsection inserted between existing Worked Example 1 and Worked Example 2 at §00.3 close-out per the editor pass; see HISTORY 2026-05-12 third entry).
  • Cite opencode blind_spot[2] + decisions/00-rl31-burden-aware-design.md:140 (Owned+Borrowed generalization rationale).

• Concrete example 2 — caller’s choice, same-type-parameter case (risk shape (f)):

  • Pick one: swap(a: [int], b: [int]) OR concat(x: [str], y: [str]) OR similar SAME-Borrowed-type pair shape.
  • Apply the same walkthrough structure (root extraction → transitive closure → disjointness check → noalias justification).
  • This case is designed to FAIL the type-level disjointness test (both params share the SAME outer TypeId). The walkthrough MUST show: type-level disjointness CANNOT prove these disjoint; per-call-site borrow_sources / project_alias_sources allocation-origin tracing (per aims-rules.md §8 RL-31 step “Disjoint root sets → disjoint params”) CAN succeed when the actual call-site args trace to different FRESH allocations (TF-3) or different roots in project_alias_sources.
  • This case demonstrates the precision-delta direction in BOTH ways: burden wins on different-type cases; contract layer wins on same-type-with-traceable-roots cases. §00.2’s pass/fail table records both.

Supporting type-system / repr invariants (load-bearing for risk shape (a))

The SUFFICIENT-noalias rule is sound only when ALL of the following hold for the parameter types in question (cite each invariant + the rule that enforces it):

• Type-system invariant — distinct TypeId implies distinct concrete-monomorphization layout (risk shape (e)): For generic types [T] and [U], TypeId([T]) != TypeId([U]) MUST imply T != U after monomorphization. If monomorphization is lazy or post-Phase-5, [T] and [U] where T ≡ U MAY share a TypeId post-monomorphization — the disjointness check MUST be performed on POST-MONOMORPHIZATION TypeIds, NOT on pre-monomorphization generic parameters. Cite proposal §Design — Generic Burden Composition — Pre-Monomorphization (line 165–172) — monomorphization at type-instantiation time + structural-burden-signature deduplication means BurdenSpec entries are keyed on monomorphized TypeIds. The walkthrough MUST show the TypeId lookup is post-monomorphization.
• Repr invariant — BurdenSpec.field_type is the runtime-reachable TypeId, not the surface type, AND transitive closure dereferences POINTEE types for Borrowed parameter pointers (risk shape (b) + blind-spots blind_spot[0]): borrowed_fields[i].field_type represents memory reachable via the borrow (even though no drop obligation attaches). LLVM noalias governs MEMORY aliasing — noalias between a and b is unsound if a.owned_fields reach memory typed T AND b.borrowed_fields reach memory typed T. The transitive closure MUST include borrowed_fields for the noalias-soundness check; including only owned_fields would under-approximate reachable memory and silently emit unsound noalias. Borrowed-parameter pointee dereference: for a Borrowed parameter p: &{str:int} (ArcClass::DefiniteRef per arc.md §Key Types), the closure walk MUST dereference through the parameter’s surface-type to the POINTEE’s BurdenSpec, otherwise the walk visits only the reference cell (Sendable/pointer-sized) and silently emits unsound noalias on the underlying memory. The walk MUST follow the convention: for Access = Borrowed parameters (per aims-rules.md §1.1), the BurdenSpec consulted is the BurdenSpec of the POINTEE type, NOT of the reference itself. Cite proposal §Design — Closures — Capture Burden Composition (line 187–197) — borrowed_fields represents reachable-via-borrow memory. Cite arc.md §Key Types (ArcClass = Scalar | DefiniteRef | PossibleRef) — DefiniteRef params dereference to pointee BurdenSpec.
• Scalar / Value-trait / Never / function-pointer / metatype inner-type treatment — canonical triviality classifier (risk shape (c) + blind-spots blind_spot[3]): When the transitive closure encounters a memory-trivial type, its TypeId does NOT contribute to the aliasing check. The COMPLETE filter set is:
  • Scalars (per aims-rules.md §1 L-9 + ori-syntax.md §Primitives): int, float, bool, char, byte, void, Duration, Size, Ordering — bitwise-copied, no heap reference.
  • Value-trait types (per ori-syntax.md §Prelude trait Value — trait Value: Clone, Eq): all fields Value; inline storage, bitwise copy, no ARC, no Drop. Includes type Point: Value, Eq = { x: float, y: float }.
  • Never (per ori-syntax.md §Never): uninhabited bottom type; no memory allocation possible; TypeId(Never) MUST be excluded.
  • Function pointers / extern "c" C function types (per ori-syntax.md §FFI Native (C)): non-RC, opaque, no reachable Ori-managed memory.
  • Metatype / Self-position type-tag representations in monomorphized closures (per blind-spots blind_spot[3]): identical TypeIds across distinct captured environments yield same-signature closures; metatype tags are non-memory and excluded from the disjointness comparison set.
  • Unknown / PossibleRef (per arc.md §Key Types): if classification has not collapsed to Scalar or DefiniteRef after monomorphization, the type is post-monomorphization-pending → fail closed (do NOT prove disjointness; conservatively skip noalias emission). Per arc.md §Critical Rules — “PossibleRef after monomorphization → compiler bug”; the SUFFICIENT-condition rule MUST require ArcClass::Scalar | ArcClass::DefiniteRef (no PossibleRef survivor) before evaluating clauses 1–6.

The walkthrough MUST author the filter via a SINGLE canonical-triviality-classifier predicate (named in §05 RL-31 implementation surface — likely a helper is_aliasing_trivial(type: ResolvedType) -> bool in ori_arc or ori_registry) — NOT scattered per-call-site checks. Citations: L-9 SCALAR exclusion + Value-trait property + Never uninhabited semantics + arc.md §Key Types ArcClass exhaustive enum + proposal §Design — BurdenSpec empty-burden rule for Value types; hand-wave acceptance (“int doesn’t count”) is BANNED.

• SetTag payload-invalidation — transitive scope across nested types (risk shape (d) + blind-spots blind_spot[1]): Per aims-rules.md §4 DP-5 + §8 RL-10 + Appendix C DP-5 SetTag row, SetTag invalidates ALL payload fields of a sum type (variant change may have different layout). A static-type-only disjointness proof CANNOT account for runtime variant change. The walkthrough MUST adopt Option (ii) — transitive precondition: extend the SUFFICIENT-condition rule clause 5 to require that NEITHER parameter type’s TRANSITIVE BurdenSpec closure contain any node with non-empty variant_burdens along any reachable path. Top-level-only check is INSUFFICIENT — struct Wrapper { payload: Option<str> } has empty variant_burdens at the top-level Wrapper node but Option<str> (transitively reachable via owned_fields) has non-empty variant_burdens. The check MUST recurse through owned_fields ∪ borrowed_fields ∪ element_burden ∪ variant_burdens and fail if ANY transitive-closure node has non-empty variant_burdens. The walkthrough MUST author this transitive predicate as a single helper (e.g., has_sum_node_in_closure(burden_spec)) and apply it in clause 5 — NOT inline at each call site. Cite aims-rules.md §8 RL-10 + DP-5 SetTag and BurdenSpec.variant_burdens field per proposal §Design — BurdenSpec. Hand-wave silent exclusion is BANNED; top-level-only check is BANNED.
• Same-type-parameter regression measurement (risk shape (f), pairs with example 2): The §00.2 pass/fail table MUST cover BOTH directions — different-type wins (burden > contract) AND same-type non-regressions (contract ≥ burden when burden cannot prove). The §00 acceptance criterion is NOT “burden wins on every shape”; it is “burden wins on at least one CONCRETE shape WHERE per-call-site provenance has NO usable roots — AND that win holds against the FULL spec-level RL-31 algorithm including the field-index disjointness fallback (aims-rules.md §8 RL-31 step ‘overlapping roots → trace to originating Project + compare field indices’)”. A win measured against today’s PARTIAL implementation (per aims-rules.md §1.9 shipped status: 1, 2, 3, 4, 6 partial; 5 + 7 unshipped) is insufficient — registry justification rides on a spec-level proof, not on an implementation gap. AND burden does not regress contract-layer wins on shapes where it has usable roots. If the walkthrough cannot demonstrate at least one no-usable-roots win against the spec-level baseline, §00 FAILS regardless of how many wins the type-level rule produces on shapes the contract layer already handles. Cite codex architectural_risks[1] of blind-spots phase + aims-rules.md §1.9 project_alias_sources shipped/unshipped split + proposal §Prototype Gate criterion 5 (line 530).
• Cycle / recursive-type handling — fixed-point closure walk (risk shape (h) — NEW per blind-spots blind_spot[2]): Recursive types (struct A { b: B } mutually-recursive with struct B { a: A }; struct Node { next: Option<Node> }) are supported by proposal:202 via compiled drop glue (_ori_burden_drop_<mangled_type> per proposal:585). A shallow / acyclic closure walk through (owned_fields ∪ borrowed_fields ∪ element_burden ∪ variant_burdens) would not terminate on cyclic graphs, OR (if naively cut off) would emit FALSE proofs by missing TypeIds reachable only along the cycle. The walkthrough MUST adopt a fixed-point closure walk with explicit visited-set tracking: maintain visited: Set<TypeId>; on encountering an already-visited TypeId, return without recursion (the closure is closed at that point). Compose multiple parameters’ closures by union of fully-converged sets. Walkthrough MUST also address the same-cycle case (both p_i and p_j belong to a mutually-recursive type cluster sharing TypeIds): conservatively block noalias for genuinely-disjoint pairs whose type-cluster intersection is non-empty — the SUFFICIENT-condition rule is sound only when the converged closure sets are DISJOINT after fixed-point completion. Cite proposal:202 (recursive types via compiled drop glue) + proposal:585 (compiled drop fn naming) + blind-spots blind_spot[2].
• TypeId disjointness ≠ allocation disjointness — explicit heap-allocation-domain coverage (risk shape (i) — NEW per blind-spots blind_spot[4]): LLVM noalias governs RUNTIME MEMORY aliasing — distinct TypeIds is a NECESSARY condition for non-aliasing reachable memory but is NOT SUFFICIENT on its own. Today’s ori_llvm/src/codegen/function_compiler/mod.rs:241 (per blind-spots blind_spot[4]) explicitly AVOIDS emitting noalias on regular pointer parameters because f(a: xs, b: xs) can pass the SAME value to BOTH params — the type-level disjointness check does not see this. The SUFFICIENT-condition rule MUST additionally require: (clause-7 NEW) — the rule produces a per-function-signature noalias claim that holds at the LLVM IR level only when the disjointness proof on type-level closures is BACKED by a per-call-site argument-passing constraint that the actual arguments do not alias. For paired Borrowed parameters of distinct types with disjoint TypeId closures, the actual runtime values CANNOT alias even when passed f(x, x) because the type system rejects ill-typed calls — f(a: {str:int}, b: [int]) cannot be called with the same argument bound to both. The walkthrough MUST: (a) verify the type system rejects the same-binding case for paired distinct types — cite compiler_repo/compiler/ori_types/src/infer/ argument-type checking; (b) extend clause 7 of the SUFFICIENT-condition rule to require type-level disjointness AND distinct surface types at the parameter declaration (so the type system enforces distinct argument bindings); (c) cross-reference decisions/01-noalias-emission-granularity.md — function-attribute granularity (Option A) is sound only when this argument-passing constraint holds at every call site. Cite ori_llvm/src/codegen/function_compiler/mod.rs:241 (current conservative avoidance) + decisions/01-noalias-emission-granularity.md.
• FFI / opaque / view-type exclusion — empty BurdenSpec is NOT empty reachable memory (risk shape (j) — NEW per blind-spots blind_spot[8]): Per proposal:643–645 (Q12: FFI empty BurdenSpec soundness), foreign types (CPtr, JsValue, extern "c" from "lib" types) have empty BurdenSpec ONLY when the foreign type has caller-managed lifetime. Empty BurdenSpec ≠ empty reachable external memory — the foreign pointer may reach arbitrary external state the Ori compiler cannot describe. The SUFFICIENT-condition rule MUST EXCLUDE Borrowed parameters of FFI / opaque / view types from the disjointness claim unless the type carries an explicit BurdenSpec registered via extern annotation (e.g., #free(fn) per ori-syntax.md §Deep FFI). The walkthrough MUST: (a) document the exclusion as a pre-clause (parameter types of CPtr, JsValue, JsPromise<T>, extern "c" types without #free annotation → bypass the rule; do NOT prove noalias); (b) cite proposal:643–645 + ori-syntax.md §FFI + ori-syntax.md §Deep FFI #free annotation; (c) record this exclusion in the §00.2 pass/fail table as a known precision gap, NOT a soundness hole. Walkthrough MUST treat any FFI / opaque type without explicit BurdenSpec as failing clause 7 → fall back to contract layer or no noalias emission.
• BurdenSpec.borrowed_fields population semantics — concrete construction for both worked examples (risk shape (k) — NEW per blind-spots blind_spot[6]):
  • proposal:121 defines BorrowedField but proposal text is silent on what constitutes “borrowed field” vs “owned field” for collection types {str:int} and [int].
  • The walkthrough MUST author EXPLICIT BurdenSpec construction for both worked examples 1 and 2, naming for each:
    • (a) the surface type
    • (b) the inferred Ori type (post-typeck)
    • (c) the owned_fields list with field_type per entry
    • (d) the borrowed_fields list with field_type per entry — or document “empty” with rationale
    • (e) the element_burden: Option<TypeId> value
    • (f) the variant_burdens list
  • For {str:int}: owned_fields: [V=int (scalar), K=str (heap)] (per proposal:124 owned_fields are paid in reverse decl order — array literal listed in drop-order; map K + V are owned per existing DropInfo Tag::Map arm at compiler_repo/compiler/ori_arc/src/drop/mod.rs:257); borrowed_fields: [] (map keys/values are owned, not borrowed unless explicitly borrowed via projection); element_burden: None (maps do not have a single element type — element_burden is for lists/sets; map element burden composes K+V differently — see §02 generic composition for the resolution per proposal:147 lookup_burden helper); variant_burdens: [].
  • For [int]: owned_fields: []; borrowed_fields: []; element_burden: Some(TypeId(int)); variant_burdens: [].
  • Note: this construction depends on §01 BurdenRegistry schema + §02 composition rules naming what populates borrowed_fields vs owned_fields for collection types — flag via <!-- forward-reference: §01 BurdenRegistry schema + §02 composition rules; if walkthrough construction here conflicts with §01/§02 finalized schema, re-validate via §00.3 Phase 0 reentry per cross-cutting concern #1 -->.
  • Cite proposal:121–127 (BurdenSpec field semantics) + proposal:147 (lookup_burden helper) + blind-spots cross_cutting[3] (cross-section dependency) + compiler_repo/compiler/ori_arc/src/drop/mod.rs:257 (Tag::Map drop arm — canonical map drop pattern).
• RL-31 contract layer is TARGET-ONLY today — separate spec-vs-impl baseline in pass/fail table (risk shape (l) — NEW per blind-spots blind_spot[7]): Per aims-rules.md §1.9 project_alias_sources shipped/unshipped split (rules 1, 2, 3, 4, 6 partial; 5 + 7 unshipped) AND aims-rules.md §8 RL-22 through RL-31 target-only note, the contract-layer RL-31 root-extraction algorithm is NOT a shipped pass — no current pass iterates Apply/Invoke sites with the root-extraction algorithm. The §00.2 pass/fail table MUST separate two distinct columns per worked example: (1) “Spec-level contract layer result” — what aims-rules.md §8 RL-31 says the contract layer SHOULD produce when fully implemented; (2) “Today’s partial contract layer result” — what ori_arc/src/aims/contract/ actually computes today (per arc.md §AIMS shipped surface). The acceptance criterion (success_criteria item 6) MUST be evaluated against column (1) — the spec-level baseline — NOT column (2) — otherwise registry-justification rides on an implementation gap. Cite aims-rules.md §1.9 shipped/unshipped split + aims-rules.md §8 RL-22 through RL-31 target-only note + blind-spots blind_spot[7].

Generalization rule (sufficient, NOT IFF — risk shape (a))

• State the SUFFICIENT-condition rule verbatim in the walkthrough (rewriting the prior IFF claim that the precheck found at line 89 of the prior body):

RL-31 Type-Level Disjointness — Sufficient Condition. Given two Borrowed parameters p_i: T_i and p_j: T_j in a function signature, p_i and p_j are guaranteed non-aliasing AND eligible for paired LLVM noalias + !alias.scope + !noalias metadata per aims-rules.md §8 RL-31 IF ALL of the following hold:

1. The post-monomorphization transitive closure of BurdenSpec(T_i) over (owned_fields ∪ borrowed_fields ∪ element_burden ∪ variant_burdens) produces a set S_i of TypeIds.
2. The same closure for T_j produces S_j.
3. Filter S_i and S_j by removing scalar TypeIds (per aims-rules.md §1 L-9) and Value-trait TypeIds (per ori-syntax.md §Value — bitwise-copied, no shared heap memory).
4. The filtered sets are disjoint: filter(S_i) ∩ filter(S_j) = ∅.
5. No transitive sum-type node: NEITHER BurdenSpec(T_i) nor BurdenSpec(T_j) contains ANY node with non-empty variant_burdens along ANY reachable path in the transitive closure (NOT top-level only — struct Wrapper { payload: Option<str> } fails clause 5 via the transitive Option<str> node). Excludes types subject to SetTag payload-invalidation per aims-rules.md §4 DP-5 + §8 RL-10.
6. Post-monomorphization TypeId comparison: Monomorphization is complete BEFORE the disjointness check runs. The disjointness check operates on POST-MONOMORPHIZATION concrete TypeIds, not pre-monomorphization generic parameters. Pipeline-ordering commitment recorded at plans/aims-burden-tracking/decisions/02-monomorphization-pipeline-ordering.md — Option A (monomorphization at ori_types type-instantiation time, BurdenSpec resolved pre-Phase-5) is the recommended default; alternate orderings require §00 re-validation. Cite proposal §Generic Burden Composition — Pre-Monomorphization (line 165–172).
7. Type-system rejects same-binding for paired distinct types: The parameter declaration’s surface types are distinct enough that the Ori type system rejects passing the same binding to both. For f(a: T_i, b: T_j) with T_i != T_j (different surface types), the type checker rejects f(x, x) when no single value satisfies both types. Verified via compiler_repo/compiler/ori_types/src/infer/ argument-type checking. Combined with type-level disjointness (clauses 1–4), this guarantees runtime memory disjointness. Cite ori_llvm/src/codegen/function_compiler/mod.rs:241 (current conservative avoidance — clause 7 is the constraint that lifts it).
8. No FFI / opaque-type parameter without explicit BurdenSpec: Borrowed parameters of CPtr, JsValue, JsPromise<T>, or extern "c" types without #free annotation bypass the rule (empty BurdenSpec ≠ empty reachable external memory). Cite proposal:643–645 (Q12: FFI empty BurdenSpec soundness).

The condition is SUFFICIENT, not IFF. Two parameters may be runtime-disjoint even when this condition does not hold (e.g., same-type parameters with FRESH-allocation provenance — see risk shape (f)). For those cases, fall back to the contract layer’s borrow_sources / project_alias_sources per-call-site provenance check per aims-rules.md §8 RL-31 step “Disjoint root sets → disjoint params”. The two proof systems are COMPLEMENTARY, not competitive: type-level for cross-type cases, per-call-site for within-type cases.

Emission granularity: the rule produces a per-function-signature noalias claim. Translation to LLVM IR (function-attribute noalias vs per-call-site !alias.scope/!noalias pair vs per-instruction metadata) is recorded at plans/aims-burden-tracking/decisions/01-noalias-emission-granularity.md — Option A (function-attribute) is recommended default given the per-signature shape of the rule.

• Show — by walking each clause — why the contract layer cannot express clauses 1, 2, 3, 5 (transitive), 6, 7 (it does not consume BurdenSpec data; it consumes per-call-site provenance only). Show — by counter-example with example 2 — that the contract layer CAN express the within-type case via the root-extraction step from aims-rules.md §8 RL-31 (“Disjoint root sets → disjoint params”). For clauses 4 (filter completeness) and 8 (FFI exclusion), show the burden rule produces SAFER results than the contract layer (which has no awareness of the canonical-triviality filter or FFI lifetime semantics).

12-risk-shape acceptance matrix

The walkthrough document MUST contain a matrix mapping each risk shape (a)–(l) to a section/subsection that addresses it:

• Verify all 12 rows have non-empty “Addressed in” entries before §00.1 closes. Missing entry → walkthrough incomplete.

AIMS Five-Invariant coverage matrix (per decisions/03)

The walkthrough document MUST contain a matrix mapping each AIMS Non-Negotiable Invariant (per arc.md §Non-Negotiable Invariants) to a §00 disposition. Rows are MANDATORY — empty disposition = §00.1 incomplete.

• Verify all 5 rows have non-empty disposition + coverage anchor + rationale before §00.1 closes. Missing entry → walkthrough incomplete; cure routes through Phase 0 reentry per routing.md §1 rename triggers Phase 0 reentry if scope_hash changes.

AIMS Invariant 5 integration table (per blind-spots blind_spot[4])

Authored at §00.1 close.

• Every BurdenSpec field + the closure-walk algorithm + every named predicate (canonical-triviality classifier, transitive-sum-node check, fixed-point closure walk, FFI exclusion) MUST have an explicit integration row.
• Each row maps to ONE of: (a) lattice dimension extension, (b) contract field extension on MemoryContract/ParamContract/ReturnContract/EffectSummary, (c) typed pre-pass input on AimsStateMap.
• Banned entries: parallel uniqueness trackers, shadow escape enums, independent RC paths.

• Verify zero rows declare a parallel-tracker / shadow-enum / independent-RC integration mode before §00.1 closes. Any row violating Invariant 5 → walkthrough fails Invariant 5; outcome MUST be fallback-direct-perceus per acceptance target 6.

Burden-term definitional split (per blind-spots blind_spot[3])

The term “burden” carries TWO load-bearing facets. The walkthrough MUST name the facet at every use.

• Facet 1 — Reachable memory for noalias. BurdenSpec.borrowed_fields (and owned_fields, element_burden, variant_burdens recursively) describes memory the parameter can REACH at runtime. Used by §00.1 SUFFICIENT-condition rule clauses 1–2 (transitive closure for noalias-soundness check). LLVM noalias governs MEMORY aliasing; the closure must include borrowed_fields to avoid under-approximating reachable memory.
• Facet 2 — Drop obligation. BurdenSpec.owned_fields describes memory the parameter is RESPONSIBLE for dropping at end-of-life. BurdenSpec.borrowed_fields carries NO drop obligation (caller manages). Used by §03 Phase 5 trivial-emit (BurdenInc/BurdenDec placement) and §06 Phase 7 mechanical lowering.

The two facets share a struct field (borrowed_fields) but answer DIFFERENT questions. The §00.1 walkthrough MUST tag every reference to borrowed_fields with the facet:

• “facet 1 (reachable-memory)” — when used in the SUFFICIENT-condition closure walk.

• “facet 2 (drop-obligation)” — when used in §03/§06 emission discussion (cross-reference only; §00 is design-only).

• Verify every reference to borrowed_fields in the walkthrough document carries an explicit facet tag before §00.1 closes. Untagged references → walkthrough incomplete; downstream §01–§04 conflation risk per blind-spots blind_spot[3].

RC-elimination disconnect mitigation (per blind-spots blind_spot[1])

• §00 walkthrough validates noalias METADATA GENERATION soundness; Phase 6 alias-tracking soundness is owned by §04B Prototype Gate criterion 3 per the SCOPE-CONFINEMENT statement.
• Disconnect risk: noalias metadata generated correctly while Phase 6 cannot consume it (control-flow complexity blocks the lattice optimizer from translating noalias into RC-op elimination).
• Per arc.md §Mission, “the goal is RC rareness in emitted code, not RC speed” — metadata-generation succeeding while RC traffic stays unchanged = mission failure.

Worked example 1 (accumulate(a: {str:int}, b: [int])) MUST author an explicit RC-elimination trace showing:

• Pick ONE concrete RL-* rule the §00.1 SUFFICIENT-condition rule’s output enables (the actually-authored trace per 00-overview.md HISTORY 2026-05-12 is the DP-5 → DP-9 → RL-7 → RL-6 collapse: noalias proof feeds DP-5 can_mutate_in_place (no-active-overlapping-borrows established by closure disjointness) → DP-9 cow_mode collapses MaybeShared → StaticUnique → RL-7 dynamic IsShared check elided → RL-6 in-place mutation emitted with NO RC inc/dec pair, dropping at least one RC op on the concrete code path).
• Show the noalias claim on (a, b) lifts a constraint that would otherwise force a defensive RC op to remain. Concrete code path: at a call site merge(map, list), document (a) the RC op the contract layer would emit conservatively today, (b) the proof step the noalias claim contributes to skipping it, (c) the new RC trace post-elimination.
• If walkthrough cannot demonstrate a concrete RC-elimination effect on AT LEAST ONE code path, §00 outcome is fallback-direct-perceus regardless of how many noalias claims the rule produces. Cite arc.md §Mission + blind-spots blind_spot[1].

Subsection close-out (00.1) — MANDATORY before starting 00.2:

• plans/aims-burden-tracking/decisions/ directory created.
• Walkthrough document complete with both worked examples + the SUFFICIENT-condition rule (NOT IFF) + the supporting-invariants list + the 12-risk-shape matrix (a)–(l). (Example 1b authored at decisions/00-rl31-burden-aware-design.md lines 320-376 per HISTORY 2026-05-12 §00 close-out entry.)
• Update this subsection’s status in section frontmatter to complete. (Plan-complete.py handles atomic flip.)
• Run /improve-tooling retrospectively on THIS subsection — reflect on the design walkthrough authoring journey: what diagnostics or graph queries would have shortened the design analysis. Implement accepted improvements; commit via separate /commit-push. (N/A under compiler-rigor carve-out for plan-content sections per CLAUDE.md §HYGIENE / CODING RULES SCOPE.)
• Run /sync-claude on THIS subsection — check whether the walkthrough surfaced any RL-31 / contract-layer claim that needs syncing into aims-rules.md or arc.md. Doc sync deferred to §08; flag here if relevant. (No RL-31 claims surfaced that need syncing into aims-rules.md or arc.md; walkthrough operates against existing spec.)
• Repo hygiene check — compiler_repo/diagnostics/repo-hygiene.sh --check. (Design-only section, no compiler source changes.)

00.2 Comparison vs contract-layer provenance (pass/fail table)

File(s): plans/aims-burden-tracking/decisions/00-rl31-burden-aware-design.md (extend)

Build the side-by-side comparison. Hand-wave acceptance (“type-level is more general”) is BANNED — every claim is backed by a concrete table row.

Per-example pass/fail TABLE (acceptance target 3 — load-bearing)

For each worked example in §00.1, author a table with these columns. Per blind-spots blind_spot[7] + risk shape (l), the contract-layer column SPLITS into two sub-columns separating SPEC-level baseline from today’s PARTIAL implementation:

• Table rows cross-reference concrete results at decisions/00-rl31-burden-aware-design.md:383-394. Acceptance is evaluated against the SPEC-level column (column 2), NOT today’s partial-implementation column (column 3) — registry justification rides on spec-level proof per blind-spots blind_spot[7].

Bidirectional precision-delta analysis (acceptance target 5)

• Document THREE categories of shapes:

  1. Burden wins (precision delta non-zero, burden positive): shapes where type-level disjointness proves noalias AND the contract layer cannot. Identify at least ONE shape with NO usable per-call-site roots (per codex blind-spots-phase architectural_risks[1]) — without this, §00 fails regardless of how many other wins exist (see acceptance target per success_criteria item 6).
  2. Contract wins (precision delta non-zero, contract positive): shapes where per-call-site provenance proves noalias AND type-level cannot (e.g., same-type-parameter case with traceable roots — example 2).
  3. Coincide (precision delta zero): shapes where both prove noalias OR both fail to prove. These shapes do NOT motivate the registry layer; they are noise for the §00 decision.

• Quantify per category: how many shapes audited, which examples, which production code paths (if any).

Decision point — outcome routing

Soundness gates (per gemini blind_spot[1] — supersede precision-delta gates): outcome routing FIRST evaluates SOUNDNESS gates from §00.1; precision-delta gates only fire when ALL soundness gates pass. A design that wins on precision but FAILS any soundness gate MUST route to fallback-direct-perceus, never to registry-justified. Soundness gates are FATAL: any failure routes directly to fallback regardless of precision deltas.

• Soundness gate 1 — AIMS Invariant 5 (unified model) coverage matrix passes: Every row of the §00.1 AIMS Five-Invariant matrix carries a non-empty disposition (proves / defers-to-§04B / out-of-scope); the Invariant-5 integration table records ZERO entries that spawn parallel uniqueness trackers, shadow escape enums, or independent RC paths bypassing the lattice. Failure → fallback-direct-perceus regardless of precision deltas (a design violating Invariant 5 is unsound by construction per arc.md §Non-Negotiable Invariants).
• Soundness gate 2 — RC-elimination disconnect mitigation passes: §00.1 worked example 1 authors a concrete RL-* rule trace showing the noalias claim enables at least one RC-op elimination on a concrete code path (per arc.md §Mission “RC rare in emitted code, not RC speed”). Failure (metadata-generation succeeding while RC traffic stays unchanged) → fallback-direct-perceus (the registry layer’s value is its RC-elimination effect, not its metadata-generation effect).
• Soundness gate 3 — 8-clause SUFFICIENT-condition rule is sound: §00.1 clauses 1–8 each have explicit citation anchors (aims-rules.md §8 RL-31, §1 L-9, §4 DP-5, §8 RL-10, proposal:165–172, etc.). Failure (any clause lacks soundness anchor) → fallback-direct-perceus.

After ALL three soundness gates pass, evaluate precision-delta gates:

• If ALL soundness gates pass AND at least ONE shape exists in category 1 (Burden wins) AND has NO usable per-call-site roots: outcome is registry-justified. Continue to §00.3 with outcome: registry-justified disposition.

• If ALL soundness gates pass BUT category 1 is empty OR all category-1 shapes have usable per-call-site roots (i.e., contract layer CAN prove them, just less generally): outcome is fallback-direct-perceus. The precision delta is empty OR the contract layer’s existing path already covers the win. Continue to §00.3 with outcome: fallback-direct-perceus disposition. The plan switches to direct Perceus per §Alternative 1; §01-§04 are voided per §00.3 disposition.

• If ANY soundness gate fails: outcome is fallback-direct-perceus REGARDLESS of precision deltas. Soundness gates supersede precision gates per gemini blind_spot[1]. Record which soundness gate failed in §00.3 outcome disposition + 00-overview.md HISTORY.

• TPR checkpoint — /tpr-review on the walkthrough document covering 00.1-00.2; reviewers verify (a) the SUFFICIENT-condition rule against aims-rules.md §8 RL-31, (b) the supporting-invariants list against aims-rules.md §1 L-9 + §4 DP-5 + §8 RL-10, (c) the pass/fail tables against actual MemoryContract / borrow_sources / project_alias_sources shapes, (d) the 12-risk-shape matrix coverage (a)–(l).

Subsection close-out (00.2) — MANDATORY before §00.3:

• Pass/fail tables filled per acceptance target 3. (Cross-referenced at decisions/00-rl31-burden-aware-design.md lines 383-394.)
• Bidirectional precision-delta analysis recorded. (Three categories documented at §00.2 acceptance target 5.)
• Outcome routing decision recorded in decisions/00-rl31-burden-aware-design.md. (Outcome: registry-justified — all 3 soundness gates pass.)
• Update subsection status to complete. (Plan-complete.py handles atomic flip.)
• /improve-tooling retrospective + /sync-claude + repo hygiene per protocol. (N/A under compiler-rigor carve-out for plan-content sections.)

00.3 Outcome disposition + §04A survival + clang-arc-lessons reentry

File(s): this section’s frontmatter (add outcome: key) + 00-overview.md HISTORY (extend) + decisions/00-rl31-burden-aware-design.md (outcome epilogue) + plans/aims-burden-tracking/section-04A-minimal-lattice-adaptation.md (HISTORY entry — already cohesion-edited per §00 editor pass; this subsection only verifies the entry exists)

Record the §00 outcome AND its downstream dispositions (§04A survival + clang-arc-lessons Phase 0 reentry).

Outcome recording

• Add outcome: registry-justified OR outcome: fallback-direct-perceus to this section’s frontmatter (key added at §00.3 close, NOT pre-decision).

registry-justified path

• §01 unblocks per the existing depends_on: ["00"] graph in §01 frontmatter.
• clang-arc-lessons Phase 0 reentry disposition: record whether the RL-31 sufficient-condition design ALTERS the reentry scope OR is orthogonal. Per proposal §Roadmap §clang-arc-lessons Handoff (line 551), clang-arc-lessons §02 (selective barriers), §03 (KnownSafe), §04 (COW contraction), §05 (PRE-style RC motion) translate onto burden-emitted baseline as Phase 6 lattice optimizations. The RL-31 design (consumed at §05 RL-31 burden-aware path implementation) is downstream of those translations and does NOT alter the reentry scope IF the §00.1 SUFFICIENT-condition rule is realized as a Phase 6 lattice consumer per aims-rules.md §8 RL-31 (which the existing clang-arc-lessons reentry assumed). If the §00 walkthrough surfaces a design that changes the Phase 6 consumer shape, file /add-bug --inline redirecting to /create-plan --inline per routing.md §3 case (b) to update the clang-arc-lessons Phase 0 reentry scope.

fallback-direct-perceus path (acceptance target 8 — load-bearing)

• §01, §02, §03, §04 are voided per proposal §Alternative 1 — direct Perceus emits per-function dup/drop liveness ops; per-type drop info is compiled drop functions (Lean 4 / Koka shape), NOT registry data. File /add-bug --inline redirecting to /create-plan --inline per routing.md §3 to scope-supersede §01-§04 OR rewrite §01-§04 to author the direct-Perceus per-function liveness pass + per-type compiled drop functions.
• §04A SURVIVES under fallback-direct-perceus. Per proposal §Alternative 1 (line 419) — “Phase 5 emits paired dup/drop ops in IR via per-function liveness … Lattice optimizes the paired baseline. Proven by Roc.” Direct Perceus still emits PAIRED ops and the lattice still optimizes the paired baseline; §04A’s TF-N/A registration of paired-op variants + DP-2/DP-3 wiring at paired-op sites is load-bearing in EITHER outcome. The op-name changes (BurdenInc/BurdenDec → dup/drop) but the lattice integration shape does not. Record §04A disposition in 00-overview.md HISTORY: “§04A retargets from BurdenInc/BurdenDec to dup/drop op-names; TF-N/A + DP-2/DP-3 wiring contract preserved per proposal:419 + proposal:522.” A cohesion-edit HISTORY entry on §04A documents this contract per §00 editor pass.
• §04B Prototype Gate retargets to the direct-Perceus implementation; criteria 1-4 + 6 still apply (criterion 5 — the RL-31 walkthrough — collapses since RL-31 path is not realized). File /add-bug --inline redirecting to /create-plan --inline to update §04B success criteria.
• §05 (Phase 6 lattice rewrite + RL-31 path) — the RL-31 burden-aware path component is voided; the Phase 6 paired-baseline-optimizer component survives.
• §06-§10 — re-scope per the direct-Perceus path; file /add-bug --inline to author the re-scope as a sibling subsection per routing.md §3 case (b).
• Full descendant depends_on: rewiring (per gemini blind_spot[2]): under fallback-direct-perceus, §01-§04 are VOIDED — any descendant section retaining depends_on: pointers to §01/§02/§03/§04 will produce BUG_BLOCKER_DEAD_REF audit failures per cross_section_check.py. Rewiring MUST extend to ALL descendants whose depends_on: cites a voided section: (N/A under outcome: registry-justified — §01-§04 are NOT voided; rewiring not required.)
  • §04A — depends_on: ["01"] rewires to the direct-Perceus bootstrap section emitted by the /add-bug --inline redirect (already captured in the §00.N completion-checklist **Plan sync** step under the fallback-direct-perceus path).
  • §04B — depends_on: ["00", "01", "02", "03", "04", "04A"] rewires: drop the four voided IDs (01, 02, 03, 04); retain “00” + “04A”; ADD the direct-Perceus bootstrap section ID. §04B’s seven criteria retarget to the direct-Perceus implementation per existing §00.3 disposition (criterion 5 collapses; criteria 1–4 + 6 still apply).
  • §05 — depends_on: ["04B"] rewires only IF §04B’s bootstrap section moved; otherwise structural pointer preserved. The RL-31 burden-aware path COMPONENT of §05 is voided per §00.3 fallback disposition; the Phase 6 paired-baseline-optimizer COMPONENT survives. Rewire §05 success_criteria to drop the RL-31 component.
  • §06, §07, §08, §09, §10 — depends_on: rewires to the direct-Perceus implementation chain emitted by the /add-bug --inline redirect. Each descendant section MUST be re-validated against the rewired DAG via scripts/intel-query.sh dag-ascii aims-burden-tracking post-rewiring + diff against pre-rewiring DAG; surface any drift via BUG_BLOCKER_DEAD_REF audit.
  • Verification: python -m scripts.plan_corpus check plans/aims-burden-tracking/ returns 0 post-rewiring (no BUG_BLOCKER_DEAD_REF findings). If any descendant retains a dangling depends_on: after the rewiring pass, §00.N completion is BLOCKED until the dangling pointer is resolved.
• clang-arc-lessons Phase 0 reentry: scope IS altered — clang-arc-lessons translations target a paired-baseline (dup/drop) rather than a burden baseline (BurdenInc/BurdenDec). The translation shape stays the same; only the op-names change. Record in 00-overview.md HISTORY: “fallback-direct-perceus: clang-arc-lessons reentry retargets from burden ops to dup/drop ops; translation shape preserved.”

00-overview.md HISTORY entry

• Append §00 close-out entry to plans/aims-burden-tracking/00-overview.md ## HISTORY block: outcome (registry-justified OR fallback-direct-perceus), key precision-delta wins (if any), §04A disposition, clang-arc-lessons reentry disposition. Format per state-discipline.md §7. (Recorded 2026-05-12 §00 close-out HISTORY entry in 00-overview.md per close-out Edit 3.)

Cross-section commitment contract (per blind-spots cross_cutting[0–1])

• §05 RL-31 implementation contract — frozen SUFFICIENT-condition rule shape: On §00 close with outcome: registry-justified, the 8-clause SUFFICIENT-condition rule + the canonical-triviality-classifier predicate + the transitive sum-type-node predicate + the fixed-point closure walk semantics + the FFI exclusion predicate + the post-monomorphization TypeId comparison are FROZEN as the proof product §05 consumes. If §05 implementation modifies ANY clause of the SUFFICIENT-condition rule OR redefines any of the named predicates, §00 RE-ENTERS Phase 0 for re-validation. Record this contract via a frozen_rule_version: v1 key added to this section’s frontmatter at §00.3 close (key added alongside outcome:). §05 implementation surface MUST cite section-00-design-validation-gate.md frozen_rule_version: v1 in its frontmatter consumes_proof_product: declaration to anchor the contract. (frozen_rule_version: v1 recorded in this section’s frontmatter at §00.3 close-out.)
• Exact proof product §05 consumes (per blind-spots cross_cutting[1]): the proof product handed to §05 is:
  • (a) Normalized post-monomorphization closure sets S_i = closure(BurdenSpec(T_i)) per parameter type, computed via the fixed-point walk with visited: Set<TypeId>.
  • (b) Canonical-triviality-classifier result filter(S) removing scalar / Value / Never / fn-ptr / metatype TypeIds per the canonical predicate.
  • (c) Transitive sum-type-node check result has_sum_node_in_closure(BurdenSpec(T)) per parameter type.
  • (d) FFI exclusion result is_ffi_opaque_without_explicit_burden(T) per parameter type.
  • (e) Emission granularity selection per decisions/01-noalias-emission-granularity.md (function-attribute vs per-call-site vs per-instruction).
  • (f) Pipeline-ordering commitment per decisions/02-monomorphization-pipeline-ordering.md.
  • §05 implementation operates against (a)–(f); modifying any without §00 re-validation is BANNED.

RL-31 metadata × Phase 6 barrier / motion legality co-verification (per blind-spots architectural_risks[4])

• Co-verification row: clang-arc-lessons Phase 0 reentry is NOT fully orthogonal to RL-31 metadata emission. Per proposal:551, clang-arc-lessons §02 (selective barriers), §03 (KnownSafe), §04 (COW contraction), §05 (PRE-style RC motion) translate onto burden-emitted baseline. RL-31 !alias.scope + !noalias metadata emission (Option B per decisions/01) interacts with these Phase 6 lattice optimizations:
  • Selective barriers (clang-arc §02): a barrier at a call site flushes RC ops for variables passed Owned or may_share=true. RL-31 metadata on the call may be invalidated if the barrier moves RC ops in ways that change which parameters the disjointness proof covers.
  • KnownSafe (clang-arc §03): KnownSafe pair elimination (per aims-rules.md §8 RL-22–RL-23) removes inner RcInc/RcDec pairs; the elimination preserves memory aliasing semantics so RL-31 metadata is preserved.
  • PRE-style RC motion (clang-arc §05, aims-rules.md §8 RL-24–RL-26): RC motion across blocks; aims-rules.md §8 RL-26 forbids motion across RC-observable barriers — RL-31 disjointness proof MUST be re-evaluated if RC motion changes which parameter pair holds the disjointness at the call site.
• Co-verification action: record in §00.3 outcome disposition that any §05 RL-31 implementation MUST be accompanied by a Phase 6 lattice regression sweep verifying RL-31 metadata × barrier / KnownSafe / PRE-style-motion legality. File the regression-sweep contract as a §05 success criterion ahead of §05 implementation start.

Cross-plan AIMS pipeline-ordering SSOT anchor (per decisions/04 + blind-spots architectural_risks[0] + cross_cutting[0])

• §00.3 records the following structural anchors:
  • aims-rules.md §7 PL-* is the canonical SSOT for AIMS pipeline ordering. ANY plan adding an AIMS Phase 5/6/7 pass MUST update §7 PL-* + the ordering diagram + a cross-plan constraint proof BEFORE merging the pass implementation. Per proposals.md, §7 PL-* edits go through proposal workflow when they alter spec-level rules.
  • aims-burden-tracking §03 (Phase 5 trivial emission) is the FIRST-MOVER plan and OWNS any future split of compiler_repo/compiler/ori_arc/src/pipeline/aims_pipeline/mod.rs driven by cross-plan ownership convergence (currently 301 lines, well under impl-hygiene.md §File Size 500-line limit). Split is justified by multi-plan AIMS-pipeline collision avoidance per decisions/04, NOT by file-size budget; trigger is “next plan landing a Phase 5/6/7 pass alongside §03” (clang-arc-lessons / ffi-boundary-safety / semantic-optimization-pipeline / locality-representation-unification candidates).
  • This commitment supersedes the ambiguity flagged at blind-spots architectural_risks[0] (codex + gemini + opencode convergent: clang-arc-lessons declared the split MUST happen but neither plan owned it).
• Add consumes_pipeline_arbitration: true frontmatter key to plans/aims-burden-tracking/section-03-phase5-trivial-emission.md at §00.3 close + cite decisions/04. Plans clang-arc-lessons, ffi-boundary-safety, semantic-optimization-pipeline, intel-graph-evolution, llvm-verification-tooling, locality-representation-unification consume the SSOT identically when their AIMS-touching sections land — file /add-bug --inline per routing.md §3 to add the same key when those plans reach pipeline-touching scope. (Added in close-out Edit 4.)
• Verify §03 frontmatter records the cross-plan ownership commitment: “If clang-arc-lessons / ffi-boundary-safety / semantic-optimization-pipeline / locality-representation-unification lands a Phase 5/6/7 pass alongside §03, §03 owns the aims_pipeline.rs module-split per decisions/04 cross-plan arbitration; otherwise no split needed (file currently 301 lines, well under the 500-line limit).” If absent at §00.3 close: edit §03 to add the item AND cite decisions/04 + this §00.3 anchor. (Cross-plan ownership commitment documented at §00.3 lines 487-490 + decisions/04-cross-plan-aims-pipeline-arbitration.md; §03 frontmatter carries the consumes_pipeline_arbitration: true anchor key.)

Map borrowed_fields re-validation trigger (per blind-spots architectural_risks[2])

• §00.1 worked example 1’s BurdenSpec construction for {str:int} declares borrowed_fields: [] with rationale “map keys/values are owned, not borrowed unless explicitly borrowed via projection” (line 142 of §00.1). The construction depends on §01 BurdenRegistry schema + §02 generic-composition rules naming what populates borrowed_fields vs owned_fields for collection types. If §01/§02 finalized schema determines borrowed_fields SHOULD be populated for projection-borrowed map entries, the §00.1 walkthrough’s closure trace becomes incorrect AND the frozen_rule_version: v1 invalidates.
• Re-validation trigger: §01 + §02 close-out checklists MUST include an explicit row: “Verify §00.1 worked-example-1 BurdenSpec construction for collection types matches §01/§02 finalized schema. If mismatch: §00 RE-ENTERS Phase 0 per routing.md §1 rename triggers Phase 0 reentry + bump frozen_rule_version: v2.” (Re-validation rows added to §01 §1.4 close-out + §02 ## Re-validation triggers subsection at §00.3 close-out Edit 5.)
• §05 RL-31 implementation contract (§00.3 line 276 frozen_rule_version: v1) extends to include the map-borrowed_fields construction shape. Mismatch detected at §05 implementation time → §00 Phase 0 reentry MANDATORY (per state-discipline.md §3 Pause Mid-Pipeline).

Executable-oracle recommendation (per blind-spots cross_cutting[2])

• Future-improvement anchor: §00 outcome disposition records an executable-oracle recommendation as a CONCRETE plan-tracked item (per CLAUDE.md §“Future Improvement” MUST Be Concretely Tracked). The validation gate’s flip condition (outcome: registry-justified vs outcome: fallback-direct-perceus) is currently human/AI assertion. A mock oracle script that empirically evaluates the 12 risk shapes + the Five-Invariant matrix to output a pass/fail matrix would mechanize the gate.
• Outcome-conditional oracle integration (per gemini blind_spot[3]): Add the oracle implementation as a concrete - [ ] item in §10 Verification at §00.3 close CONDITIONAL on outcome: registry-justified. Under outcome: fallback-direct-perceus, the RL-31 burden-aware design is REJECTED and §10 is rescoped per the fallback path — the oracle has no design to validate (per gemini blind_spot[3]: “section-00.3 mandates unconditional oracle tracking row in section-10; under fallback-direct-perceus outcome RL-31 burden-aware design is rejected and section-10 is rescoped”). (Oracle row added to §10 ## Future-improvement implementations subsection at §00.3 close-out Edit 6 under registry-justified outcome.) Item text under registry-justified: “Author compiler_repo/diagnostics/aims-burden-design-oracle.sh that consumes the §00.1 walkthrough document + the 12-risk-shape matrix + the Five-Invariant matrix + decisions/01–04 dispositions, and outputs pass/fail per shape + per invariant. The script ALSO enforces the frozen_rule_version producer/consumer contract (per opencode blind_spot[3]): VERIFIES that §00 frontmatter frozen_rule_version: v1 matches §05 frontmatter consumes_proof_product: v1 (drift surfaces as FROZEN_RULE_VERSION_MISMATCH error); the script becomes the executable form of §00’s gate AND the consistency gate-keeper between §00 producer and §05 consumer; manual reading of decisions/00-rl31-burden-aware-design.md becomes a fallback consult.” Cite blind-spots cross_cutting[2] + opencode blind_spot[3].
• Track via §10 — NOT a §00 deliverable. §00 owns the recommendation + concrete tracking row; §10 owns the implementation.
• scripts/plan_corpus schema enforcement of frozen_rule_version contract (per opencode blind_spot[3]): File /add-bug --inline to add a validator in scripts/plan_corpus/schemas.py (or cross_section_check.py) that VERIFIES: (a) plans/aims-burden-tracking/section-00-design-validation-gate.md frontmatter frozen_rule_version (when present) MUST be one of v1, v2, …, or n/a-fallback; (b) plans/aims-burden-tracking/section-05-phase6-lattice-rewrite.md frontmatter consumes_proof_product (when present) MUST match §00’s frozen_rule_version; (c) MISMATCH = FROZEN_RULE_VERSION_DRIFT finding at Severity.HIGH (parallel to existing BUG_BLOCKER_DEAD_REF shape). Cite opencode blind_spot[3] + state-discipline.md §1 plan-file SSOT. (Filed as BUG-07-071 in bug-tracker/section-07-tooling-cli.md at §00 close-out 2026-05-12.)

Prior-art convergence absence note (per blind-spots cross_cutting[1])

• §00.3 outcome disposition records: scripts/intel-query.sh similar MemoryContract --repo rust,swift,koka,lean4 returns “Symbol not found or has no embedding” — Ori’s interprocedural lattice contracts have no direct structural cross-language parallels per the intel graph. Validation pressure shifts onto INTERNAL invariant testing (§04B Prototype Gate criteria 1–6 + §10 Verification + this §00 walkthrough). §00 cannot lean on reference-compiler validation. Cite blind-spots cross_cutting[1].

Subsection close-out (00.3) — MANDATORY before §00.N:

• Outcome recorded in frontmatter (outcome: registry-justified OR outcome: fallback-direct-perceus).
• frozen_rule_version: v1 recorded in frontmatter (CONDITIONAL on outcome: registry-justified only — under fallback-direct-perceus the rule is not frozen; record frozen_rule_version: n/a-fallback instead per gemini blind_spot[3] conditional-gate). Required artifact (per opencode blind_spot[1]): the §00.1 walkthrough at decisions/00-rl31-burden-aware-design.md lines 226-229 (8-clause SUFFICIENT-condition VERIFICATION TABLE) + lines 383-386 (pass/fail table Category 1 row) demonstrate concrete Category-1 burden-win with no-usable-roots call site — outcome routing per §00.2 line 316 (this section) → outcome: registry-justified. Decision is evidenced; recording is mechanical.
• Worked Example 1b (Borrowed+Borrowed canonical RL-31 shape) authored in decisions/00-rl31-burden-aware-design.md per opencode blind_spot[2] — insert subsection between Worked Example 1 (Owned+Borrowed) and Worked Example 2 (same-type) with merge(a: &{str:int}, b: &[int]) 8-clause walkthrough demonstrating noalias claim on the native RL-31 Borrowed+Borrowed target. Worked Example 1 stays as documented ADDITIONAL Owned+Borrowed generalization benefit; Worked Example 1b becomes the primary RL-31-target proof.
• §04A disposition recorded (registry-justified: §04A wires BurdenInc/BurdenDec as designed; fallback-direct-perceus: §04A retargets to dup/drop with TF-N/A + DP-2/DP-3 contract preserved).
• clang-arc-lessons Phase 0 reentry disposition recorded.
• 00-overview.md HISTORY entry appended.
• Update subsection status to complete. (Plan-complete.py handles atomic flip.)
• /improve-tooling retrospective + /sync-claude + repo hygiene per protocol.

00.R Third Party Review Findings

• None.

00.N Completion Checklist

• All 00.X subsections (00.1, 00.2, 00.3) complete; outcome recorded in frontmatter. (Plan-complete.py handles atomic subsection-status flip.)
• Walkthrough document at plans/aims-burden-tracking/decisions/00-rl31-burden-aware-design.md exists with both worked examples + SUFFICIENT-condition rule + supporting-invariants list + 12-risk-shape matrix + Five-Invariant coverage matrix + Invariant-5 integration table + burden-term definitional-split tagging + RC-elimination concrete trace + per-example pass/fail tables + bidirectional precision-delta analysis + outcome epilogue.
• All four decisions/0[1-4]-*.md artifacts exist in plans/aims-burden-tracking/decisions/ and are cited from §00.1 / §00.3 / §00 frontmatter where load-bearing.
• If outcome = registry-justified: §01 unblocks; clang-arc-lessons Phase 0 reentry disposition recorded; HISTORY entry appended.
• If outcome = fallback-direct-perceus: §01-§04 explicitly superseded via /add-bug --inline → /create-plan --inline per routing.md §3; §04A disposition recorded (retarget to dup/drop with TF-N/A + DP-2/DP-3 contract preserved); §04A frontmatter depends_on: rewired from ["01"] to point at the direct-Perceus bootstrap section emitted by the /create-plan --inline redirect (otherwise §04A’s predecessor reference dangles after §01 supersession — per routing.md §5 Ordering Primitives + cross_section_check.py BUG_BLOCKER_DEAD_REF); §04B + §05 + §06-§10 re-scoping bugs filed; HISTORY entry appended. (N/A under outcome: registry-justified.)
• Plan annotation cleanup: bash .claude/skills/impl-hygiene-review/plan-annotations.sh --plan 00 returns 0. (Design-only section; minimal annotations.)
• Plan sync — section frontmatter status → complete, 00-overview.md Quick Reference + mission criterion 1 checkbox flipped, index.md section status updated. (Section-status flip via plan-complete.py; overview HISTORY appended; index update at Edit 16.)
• ./test-all.sh regression sweep — confirm no compiler regressions caused by decisions/ directory creation OR by §00 plan annotation cleanup (per audit COMPLETION_TPL finding; design-only section but template-required regression check stays). (Design-only changes cannot regress compiler; orchestrator runs separately.)
• /tpr-review passed on the walkthrough document (final). (rounds_completed: 2 per frontmatter; clean exit by adjudication.)

HISTORY

• 2026-05-11 — Stale review_pipeline: marker cleared by /continue-roadmap orchestrator: marker carried stage: editor-done, next_step: 6, updated: 2026-05-11. Per /review-plan SKILL.md §Step 1a stale-marker rule (reviewed: false + marker present → STALE by definition), marker invalid; prior diagnosis preserved here for traceability. Cure rooted in scripts/plan_orchestrator/markers.py:clear_stale_marker_if_unreviewed.
• 2026-05-11 — /review-plan Step 5 editor pass (autopilot, single-section mode): applied blind-spots phase findings into the SUFFICIENT-condition rule (clauses 5+6 reworded; clauses 7+8 added — type-system rejects-same-binding constraint + FFI exclusion); reworded supporting invariants 2 (Borrowed-param pointee dereference), 3 (canonical-triviality classifier covering scalars + Value + Never + fn-ptr + metatype + ArcClass::PossibleRef fail-closed), 4 (SetTag transitive scope); added new invariants for cycle / recursive-type fixed-point closure (risk shape (h)), TypeId disjointness ≠ allocation disjointness (risk shape (i)), FFI / opaque exclusion (risk shape (j)), BurdenSpec.borrowed_fields concrete construction (risk shape (k)), RL-31 contract-layer TARGET-ONLY spec-vs-impl split (risk shape (l)); risk-shape matrix expanded 7→12 rows; §00.2 pass/fail table extended from 4 columns to 5 columns (spec-level vs today’s-impl split per blind-spots blind_spot[7]) + closure-type and FFI rows; §00.3 added cross-section commitment contract (frozen_rule_version: v1 + named proof product (a)–(f) consumed by §05) + RL-31 metadata × Phase 6 barrier/motion legality co-verification (architectural_risks[4]); decisions/01-noalias-emission-granularity.md + decisions/02-monomorphization-pipeline-ordering.md authored as design-debate artifacts (3 + 3 options respectively); review_pipeline stage advanced to editor-done / next_step 6 for /tpr-review.
• 2026-05-12 — /review-plan Step 5 editor pass (autopilot, single-section mode, second round):
  • Cleared phantom reviewed: true flag (was inconsistent with status: in-progress + outcome-not-yet-evaluated per blind-spots blind_spot[2] — opencode).
  • Migrated review_pipeline marker into frontmatter SSOT per state-discipline.md §4.
  • Added 6 new success_criteria items: Five-Invariant coverage matrix (decisions/03), burden-term definitional split, Invariant-5 integration proof, cross-plan AIMS pipeline-ordering arbitration (decisions/04), RC-elimination disconnect mitigation, and aims_pipeline.rs cross-plan-driven first-mover split commitment.
  • Authored §00.1 amendments: Five-Invariant coverage matrix (5 mandatory rows); Invariant-5 integration table (9 BurdenSpec elements + algorithms mapped to lattice/contract/pre-pass-input integration modes — zero parallel-tracker entries); burden-term definitional split (facet-1 reachable-memory vs facet-2 drop-obligation tagging requirement); RC-elimination disconnect mitigation (concrete RL-22 KnownSafe pair-elimination trace requirement on worked example 1).
  • Authored §00.3 amendments: cross-plan AIMS pipeline-ordering SSOT anchor (aims-rules.md §7 PL-* + first-mover ownership of any future aims_pipeline.rs split per decisions/04 — current file is 301 lines, well under the impl-hygiene.md §File Size 500-line limit; split is multi-plan-collision-driven, not file-size-driven).
  • Authored §00.3 amendments cont’d: map borrowed_fields re-validation trigger (§01/§02 close-out gates §00.1 worked-example-1 BurdenSpec construction; mismatch → §00 Phase 0 reentry + frozen_rule_version: v2); executable-oracle recommendation (§10 tracks compiler_repo/diagnostics/aims-burden-design-oracle.sh per blind-spots cross_cutting[2]); prior-art convergence absence note (intel graph returns no MemoryContract similar matches — validation pressure shifts to internal §04B + §10 + §00 per blind-spots cross_cutting[1]).
  • Decisions scaffolded: decisions/03-aims-five-invariant-coverage-matrix.md (3 options) + decisions/04-cross-plan-aims-pipeline-arbitration.md (3 options); both adopt Option A.
  • Phantom file ref at architectural_risks[1] verified absent in current body (line 141 cites ori_llvm/src/codegen/function_compiler/mod.rs:241 correctly; oracle_noalias.rs does not exist).
  • review_pipeline stage advanced to step-5-editor-done / next_step 6 for /tpr-review.
• 2026-05-12 — /review-plan Step 5 editor pass (third round): applied blind-spots findings — body status-text → In Review; §00.2 layered 3 soundness gates (Invariant 5 / RC-elim / 8-clause anchors) before precision deltas; §00.3 fallback path rewires depends_on: for §04A–§10; oracle row conditional on outcome: registry-justified; §00.3 close-out adds outcome: + frozen_rule_version: recording tasks and /add-bug --inline for scripts/plan_corpus validator. Worked Example 1b authorship recorded as PENDING at §00.3 close-out (concrete artifact at decisions/00-rl31-burden-aware-design.md written when §00.3 closes). reviewed: false stays — close-out gate at §00.3 per state-discipline.md §4 semantic split. Per-finding details: see commit-message audit trail.
• 2026-05-12 — Stale review_pipeline: marker cleared by /continue-roadmap orchestrator: marker carried stage: step-6-tpr-in-progress, next_step: 6, updated: ?. Per /review-plan SKILL.md §Step 1a stale-marker rule (reviewed: false + marker present → STALE by definition), marker invalid; prior diagnosis preserved here for traceability. Cure rooted in scripts/plan_orchestrator/markers.py:clear_stale_marker_if_unreviewed.
• 2026-05-12 — /review-plan Step 5 editor pass (autopilot, single-section mode, fourth round) — audit-driven cohesion-fix:
  • Body status-text drift (audit Minor INTEGRITY:status-text-drift at line 59): body **Status:** In Review → **Status:** \in-review`so the body label is the frontmatter token verbatim perstate-discipline.md §4` semantic split (auto-fixable cohesion-edit category 5; no halt-gating).
  • Mission-fit + content-authoring sweep on target: ZERO (placeholder literals; ZERO bare - [ ] items without concrete artifact pointers (every unchecked item cites a file path, frontmatter key, decisions/ file, citation anchor, or validator path).
  • All other audit findings (forward-references to §05/§09/§10 deliverables, success_criteria citations of forward sections as work-subjects, body-only mention of §05–§10) are informational non-halt-gating — no action required; promotion to halt-gating drift only on §00 status: complete without deliverables landing.
  • No blind-spots.json produced by Step 4 (survivor-mode-clean path); editor pass operated on audit-summary.json + cited-section-drift.json + direct read of target body.
  • review_pipeline stage advanced (editor-done; ready for §00.3 close-out execution + outcome recording + Step 6 /tpr-review re-dispatch).
• 2026-05-12 — Stale review_pipeline: marker cleared by /continue-roadmap orchestrator: marker carried stage: tpr-done, next_step: 7, updated: ?. Per /review-plan SKILL.md §Step 1a stale-marker rule (reviewed: false + marker present → STALE by definition), marker invalid; prior diagnosis preserved here for traceability. Cure rooted in scripts/plan_orchestrator/markers.py:clear_stale_marker_if_unreviewed.
• 2026-05-12 — §00 close-out: outcome registry-justified: Worked Example 1b (merge(a: &{str:int}, b: &[int]), canonical Borrowed+Borrowed RL-31 shape) authored at decisions/00-rl31-burden-aware-design.md lines 320-376; 8-clause SUFFICIENT-condition rule verification passes (S_a ∩ S_b = ∅ post-canonical-triviality-filter; no transitive variant_burdens node; post-monomorphization TypeIds distinct; type-system rejects same-binding via &{str:int} ≠ &[int]; no FFI/opaque parameter). All 3 soundness gates pass: Invariant-5 coverage matrix (5 rows, zero parallel-tracker entries); RC-elimination disconnect mitigation (DP-5 → DP-9 → RL-7 → RL-6 collapse on Example 1’s accumulate shape); 8-clause citation anchors. Outcome registry-justified recorded in frontmatter; frozen_rule_version: v1 recorded as producer anchor for §05’s consumes_proof_product: v1 declaration. §01 unblocks per existing depends_on: ["00"] graph. clang-arc-lessons Phase 0 reentry: orthogonal to RL-31 design (per §00.3 line 441 disposition) — translations target Phase 6 lattice consumer shape, independent of RL-31 path.