RFC-009a: トークンライフタイム解析——ホーア証明パイプラインに基づく

親 RFC: RFC-009: 所有権モデル設計
依存: RFC-027: コンパイル時述語と統一静的検証
前提条件: RFC-027 が受理済みであること。本 RFC の全メカニズム（証明パイプライン、SMT フォールバック、経路条件収集）は RFC-027 の実装に依存する。
本 RFC は RFC-009 §"トークン競合検出：フロー依存活性解析"（第 663-684 行）を修正し、置換する。

概要

RFC-009 第 684 行はトークン競合検出は「……NLL を必要としない」と主張している。結論は正しいが、論拠が誤っている。

「トークンは値であり、線形追跡で十分」という理由ではない。トークン活性はホーア論理の命題であり、専用のフロー依存解析ではない。 ためである。

{conflicting_tokens 全て死亡} op {WriteToken 安全取得} —— 同じ {P} op {Q} が、型検査・述語検証と RFC-027 の証明パイプラインを共有する。新しい解析フレームワークはない。一本のパイプライン、複数の命題。

動機

RFC-009 の混同

RFC-009 は二つの問題を混同している：

線形追跡（Move 後使用不可）—— {v が move されていない} use(v) {型一致}。型検査器に既に存在する。
トークンライフタイム相互作用（子トークン生存 → 親トークン停止 → 子トークン死亡 → 親トークン復活）—— {conflicting_tokens 全て死亡} write(data) {安全}。活性解析が必要であり、線形追跡ではない。

現状コードの実態

コンポーネント	状態
`BorrowChecker`	IR を線形走査し、明示的な `Borrow`/`Release` 命令に受動的に応答
`ControlFlowAnalyzer::analyze_instruction`	空実装（`control_flow.rs:145-153`）
`liveness_analysis`	存在するが Drop 挿入のみに使用され、トークン競合には未接続
Release 挿入	Call 命令の後にハードコード——純粋に語彙スコープ（`ir_gen.rs:2734-2736`）

ユーザー可視の結果：

yaoxiang

data = vec![1, 2, 3]
view = &data              # ReadToken 作成
x = view.total_count      # view の最後の使用
data.push(4)              # ❌ Release(view) が未実行、ReadToken が「生存中」

なぜ書き直すのか

旧版（009a v1）は「DAG による NLL 置換」ナラティブを用いており、不要な新概念（保守的分岐規則、ループ特殊処理）を導入した。核心的矛盾を明確にしなかった：借用検査は独立したシステムではなく、ホーア命題の一形態に過ぎない。

核心設計

全てはホーア

型検査：    { x: Int }        x + 1        { result: Int }
借用検査：  { view 死亡 }     data.push(4)  { WriteToken 取得成功 }
述語検証：  { y > 0 }         divide(x, y)  { result: Int }
逆辺切断：  { i == n }        次ループ      { cond == false }

同じ形式 {P} op {Q}。コンパイラは各操作に対して前置命題 P を生成し、証明パイプラインに投入して検証する。

借用検査とユーザー述語は同じパイプラインを共有する。 違いは命題を生成する主体と、証明失敗時の扱いのみ。

二種類の述語、一本のパイプライン

	ユーザー述語	システム述語（借用）
命題生成	プログラマー（型注釈）	コンパイラ（ブランド木 + 所有権規則）
証明提供	コンパイラ + プログラマー	コンパイラ完全自動
証明失敗時	証明関数を書くかリファクタ	コードをリファクタ（門はあるがごく稀に必要）
可視性	シグネチャ可視	暗黙的、型シグネチャを汚染しない
学習コスト	使うときだけ学習	ゼロ

システム述語の証明はプログラマーに証明関数を開かない——コンパイラが完全自動実行する。 証明失敗時はユーザーがコードをリファクタする。

三つの失敗モード、同一の検証エンジン。 型命題の証明失敗 → コンパイルエラー（回避不可）。借用命題の証明失敗 → コンパイルエラー、コードリファクタ（回避不可）。ユーザー述語の証明失敗 → コンパイルエラー、証明関数記述可能（回避可能）。失敗戦略は異なるが、検証エンジンは同一——SMT ソルバー + コンパイラインカーネル推論規則。違いは「証明失敗時に誰が証明を補うか」のみ——コンパイラはプログラマーの借用証明の代筆を拒否する（借用命題の証明戦略は構造解析 + SMT であり、プログラマー介在不要）が、ユーザー述語の証明関数は受け入れる。これはパイプラインの不整合ではなく、命題分類ごとの責任境界が異なるだけである。

これは Rust の 'a とは異なる：'a は必修科目、証明関数は選択科目——大多数のユーザーは一生選択科目の門にすら触れない。

借用命題：コンパイラ自動生成

ユーザーが data.push(4) と書くと、コンパイラは自動的に以下の命題を生成する：

WriteToken(data, node) 取得可能
  = forall t in conflicting_tokens(data): t が node で死亡済み
  = forall t in brand_tree.children(data): forward_reachable(node) ∩ consumers(t) == ∅

三つの規則、ゼロの特殊ケース：

ブランド木（RFC-009 §2.7）が「誰と誰が競合するか」に答える：プレフィックス一致、O(depth)、深さ ≤ 3
コンシューマーリスト（DAG 構築時に自動収集）が「トークンを最後に消費したのは誰」に答える
前方到達可能性が「コンシューマーがまだ実行可能か」に答える：構造的切断 + 論理的切断

前方到達可能性：コンシューマーから逆向き

トークン T の各コンシューマー C に対して：

C から出発、DAG を逆向きに BFS。
辺は以下の場合に切断される：
  1. break 辺（構造的切断）
  2. 経路条件 ⇒ !loop_cond が SMT 証明可能（論理的切断、RFC-027 パイプライン）

切断されていない辺を全て逆向きに伝播（逆辺を含み、逆辺は活性を前イテレーションに伝播する）。
到達可能な全ノードをマーク → unsafe。

クエリ：書込操作がノード W に存在 → W ∉ unsafe → 安全。

「保守的分岐規則」の発明不要。「ループ内保守的存活」不要。一つの逆向き BFS + 二つの切断規則。

証明戦略：ファーストパス優先、SMT フォールバック

トークンを必要とする各書込操作
  │
  ├→ ファーストパス：DAG 構造解析（95%+ のケースをカバー）
  │     │
  │     ├→ ブランド木プレフィックス一致 → 競合トークン発見（O(depth)）
  │     ├→ 逆向き BFS、break が逆辺を切断
  │     └→ 穿越可能な逆辺なし → 直接 Proved / Disproved 判定
  │
  └→ スローパス：SMT 論理的切断（ファーストパスが穿越可能逆辺に遭遇した場合のみ）
        │
        ├→ 逆辺始点に経路条件あり → SMT が path_cond ⇒ !loop_cond を判定
        │     ├→ Proved → 論理的切断 → ファーストパスに降格して継続
        │     └→ Disproved / Unproven → 逆辺を穿越 → unsafe にマーク
        │
        └→ 逆辺始点に経路条件なし → 逆辺を直接穿越

ファーストパス適用範囲：線形コード、if/else、loop + break、経路条件なしの while。 スローパス適用範囲：while ループ体内、経路条件がループ終了を示唆する場合。 非適用範囲：実行時条件が静的に証明不能 → 逆辺を穿越 → unsafe → コンパイルエラー（ユーザーリファクタ）。

SMT は主力ではなく安全網である。RFC-027 のユーザー述語とは異なる：ユーザー述語は SMT を主力とする；借用システム述語は構造解析を主力とし、SMT は構造解析の届かないエッジケースのみを補完する。

SMT は精度層であり、soundness 依存ではない。 借用システム述語の健全性判定は完全にファーストパスが担う（区間 + 逆向き BFS + break 切断）；SMT 論理的切断は「ループ境界の合法プログラムを通過させるか」だけを決定する。SMT が利用不可 / タイムアウト / 未実装（RFC-027 impl: in_progress）の場合、フォールバック = 逆辺穿越 = 保守的拒否、拒否すべきものは必ず拒否される。SMT 不在時の保守度 = ループ内の借用 + 書込みを全て拒否、これは Rust NLL と同等 （Rust のプロダクション借用検査も SMT を持たない）。SMT 実装は純粋な精度向上であり、健全な本線の配信をブロックしない。

ユースケース解析

線形コード

yaoxiang

data = vec![1, 2, 3]        # ノード 1
view = &data                # ノード 2：data を消費、ReadToken(#1) を生成
x = view.total_count        # ノード 3：view を消費（= #1 の最後のコンシューマー）
data.push(4)                # ノード 4：WriteToken(data) を必要とする

逆向き BFS を view.total_count（ノード 3）から開始 → ノード 3 は #1 の最後のコンシューマー → ノード 4 > ノード 3 → ノード 4 は unsafe に含まれない → ✅

if/else：特殊規則なし

yaoxiang

view = &data
if cond {
    use(view)               # then 分岐で view を消費
} else {
    do_something_else()     # view に触れない
}
data.push(4)                # view の最後のコンシューマーは if 内 → if 後にコンシューマーなし → ✅

if/else は DAG 上の複合ノード。内部消費はこのノードに帰属する。分岐状態をマージしない。保守的多数決を取らない。後にコンシューマーがいるかどうかは整数比較。

明確化：「分岐状態をマージしない」は借用活性（ブランドコンシューマー逆向き BFS）にのみ適用される。 move 状態（変数所有権）は別系統の解析：CFG ノード単位の前方データフロー（NLL/Polonius スタイル）、分岐合流時に保守的 meet（いずれかの分岐で Moved → 合流点 Moved）、リテラル到達の有無（if false）は参加しない。両者は層分けされる：借用活性は「後続コンシューマーの有無」を見、move 解析は「変数が移動された可能性」を見る。

戻り値によるエスケープを伴う if/else

yaoxiang

view = &data
result = if cond {
    view                     # view が result にエスケープ
} else {
    something_else
}
use(result)                  # view を間接的に消費
data.push(4)                 # view にまだコンシューマーあり（use(result)）
                             # → push は unsafe 内 → ❌ 正しくエラー

view が戻り値経由でエスケープ → use(result) が view のコンシューマー → push から逆向きに進むと use(result) に到達可能 → unsafe。

ループ：break が逆辺を切断

yaoxiang

view = &data
loop {
    use(view)                # consumer
    if is_last {
        data.push(4)         # 書込操作
        break                # ← 構造的切断
    }
}

逆向き BFS を use(view) から開始 → 逆辺 → 前方に data.push(4) へ進む → break に遭遇 → 切断 → data.push(4) は unsafe に含まれない → ✅

break なしの場合：

yaoxiang

view = &data
loop {
    use(view)
    data.push(4)             # break 切断なし → 逆辺が穿越可能 → 次イテレーションの use(view) が到達可能
                             # → push は unsafe 内 → ❌ 正しくエラー
}

while：SMT 論理的切断

yaoxiang

view = &data
mut i: UpTo(n) = 0
while i < n {
    use(view)                # consumer
    i += 1
    if i == n {
        data.push(4)         # 経路条件：i == n
    }
}

逆向き BFS を use(view) から開始 → 逆辺 → data.push(4) に進む → 経路条件 i == n を検査 → SMT クエリ：i == n ⇒ !(i < n)？→ Proved → 論理的切断 → data.push(4) は unsafe に含まれない → ✅

判定対象が書込ノード自身の経路条件（i == n は if 分岐内の data.push(4) に属する）であることに注意、逆辺ノードの経路条件ではない。

本質：ブランド ID は `'a` そのもの

「a を必要としない」とは言わない。「#42 とは '42 のことである」と言う。

Rust	YaoXiang	等価性
`'a`	`#42`	コンパイル時ライフタイム識別子
`'a: 'b` outlives 制約	`#42` は `#42.field_x` のプレフィックス	文字列プレフィックス比較 = 半順序関係
NLL 活性伝播（CFG 不動点）	逆向き BFS（DAG）	共に到達可能性計算
Polonius fact	SMT 論理的切断	共に経路条件推論
制約システム不動点求解	ブランド木プレフィックス一致 + BFS	異なるエンコード、同一の問題

新しい解析を発明したのではなく、'a を型シグネチャ層から証明層に降ろしただけである。 ブランド ID が行うことは 'a と完全に同じ——借用の識別、派生関係の追跡、競合の判定。違いは一つ：'a はユーザー記述の型シグネチャに含まれる；#42 はコンパイラ内部にある。

これは恥ずべきことではない。Curry-Howard は型は命題、プログラムは証明と説く。'a は命題の一部ではなく、証明戦略の一部である。Rust は証明戦略を命題シグネチャに書き込む。我々はそれを本来あるべき場所に戻す。

言語設計制約が排除したもの

複雑性の源泉	回避したか	理由
変数シャドーイング	✅	言語で禁止——同じ名前が常に同じものを指す
for の反復間借用	✅	各反復で新しいバインディング——反復間が自然に分離
`'a` ライフタイム注釈	✅	ブランドパス = `#42.field_x`、コンパイラ推導
名前付きライフタイム + 制約伝播	✅	ブランドパスのプレフィックス比較で明示的制約集合を置換
借用グラフ制約求解（Polonius）	❌	ブランド木プレフィックス一致 + DAG コンシューマークエリ（誤記。原文では ✅ だが、§核心設計 1 では「`#42` は `#42.field_x` のプレフィックス」でプレフィックス比較採用とあり、Polonius 回避が論旨。原文ママ）
ループ体内借用活性伝播	❌	Rust と同様に処理が必要——逆向き BFS + 論理的切断で対処
条件分岐の保守性	❌	Rust と同様——SMT が証明可能な範囲をカバー、残り保守的拒否

なぜ DAG が実現可能か

YaoXiang の三つの言語設計制約が DAG 解析を可能にする：

変数シャドーイング禁止——同じ名前が常に同じものを指し、再バインディング間の追跡不要
for は反復ごとに新バインディング——反復間が自然に分離し、反復間借用が存在しない
構造化並行性——タスク境界が明確、タスク間活性伝播不要

これらの制約が Rust CFG 不動点反復の主要複雑性源泉を排除する。DAG が CFG より「高度」なのではなく、より単純な言語設計がより単純な解析を可能にする。

詳細設計

システム述語一覧

コンパイラは以下の命題を自動生成し、RFC-027 証明パイプラインに投入する：

システム述語	発動タイミング	命題形式
`borrow_conflict`	WriteToken(v) を必要とする時	`forall t ∈ conflicting(v): dead_at(t, node)`
`use_after_move`	変数 v を使用する時	`¬moved(v)`
`use_after_drop`	変数 v を使用する時	`¬dropped(v)`
`double_drop`	Drop(v)	`¬dropped(v)`
`mut_violation`	不変変数 v への書込	`is_mut(v)`

既存の BorrowChecker、MoveChecker、DropChecker、MutCheckerは命題生成器になる——消えるのではなく、役割を変える。命題を生成し、パイプラインが検証する。

ブランド木

RFC-009 §2.7 のブランド機構をブランド木として形式化する。

トークンセマンティクス——凍結優先、コピー非優先：

&T と &mut T の本質的違いは「コピー可能かどうか」ではなく、「同時書込を許すかどうか」である：

ReadToken(T)：読取専用権限を付与し、ソースデータ T を凍結する——この期間中は
              WriteToken(T) は一切取得不可。凍結が ReadToken の第一義セマンティクス。
              Dup（コピー可能）は凍結の帰結：データが既に凍結されている（変異不可）
              ため、複数の読取専用ビューが自然に安全になる。

WriteToken(T)：排他的な読書き権限を付与する。書込みが存在するため、他のトークン
              （読取・書取問わず）は共存不可。Dup を実装しない（線形型）のは
              排他性の帰結。

因果関係：

ReadToken 存在 → ソースデータ凍結 → 複数読取専用が安全 → Dup
                      ↓
              WriteToken 拒否（borrow_conflict システム述語が強制）

ではなく：

ReadToken が Dup を持つ → 複数可能 → ついでに競合検査  ← 因果が逆

BrandTree:
  nodes: Map<BrandId, BrandNode>

BrandNode:
  id: BrandId               # "#42"、"#42.field_x"
  kind: ReadToken | WriteToken
  source_var: Operand
  parent: Option<BrandId>   # 派生関係の親ノード
  children: Set<BrandId>    # 派生子トークン
  consumers: Set<NodeId>    # 当該トークンを消費する DAG ノード
  ref_count: usize          # ReadToken 凍結期間中の安全コピー数

競合判定——凍結保証による実行メカニズム：

rust

fn conflicts(a: &BrandId, b: &BrandId) -> bool {
    // 競合条件：同ソース + 少なくとも一方が書込み + ブランドパス重複
    // これは以下を意味する：
    //   1. ReadToken vs ReadToken → 競合なし（共に読取専用、変異なし）
    //   2. WriteToken vs ReadToken → 競合（書込みが読取りの凍結保証を破壊）
    //   3. WriteToken vs WriteToken → 競合（二つの書込みは共存不可）
    a.source() == b.source()
        && (a.is_write() || b.is_write())
        && (a.is_prefix_of(b) || b.is_prefix_of(a))
}

O(depth) 文字列プレフィックス比較、深さ ≤ 3。定数級。

逆向き BFS 活性解析

本アルゴリズムは「トークン生成時刻」次元を導入する。トークン活性は区間 [created_at, last_use] であり、逆向き到達可能集合ではない；書込操作はトークンの活性区間内でのみ競合を構成する——これは「書込み先、借用後」の合法順序（§2.4 セマンティクス：引数トークンは呼出終了時に解放）をカバーし、誤検知を防ぐ。

アルゴリズム：check_borrow(token, node, dag, brand_tree)

入力：
  token: 検査対象の WriteToken
  node:  書込操作の DAG ノード

出力：Proved | Disproved

アルゴリズム：
  # ファーストパス：逆向き BFS
  unsafe = empty_set
  queue = brand_tree.consumers(token)

  while queue が空でない:
    cur = queue.pop()
    unsafe.add(cur)

    for each pred in dag.predecessors(cur):
      # 構造的切断：break は穿越しない
      if pred が break 辺:
        continue

      # 逆辺 → SMT フォールバックの要否を判定
      if pred が逆辺:
        path_cond = 書込ノード node の経路条件   # 判定対象は書込ノード自身の条件
        loop_cond = ループ条件
        # まず構造的に切断可能か確認（対応する break が既に経路を切断 → ここには来ない）
        # 次に経路条件を確認
        if path_cond が非空:
          result = smt_fallback(path_cond, loop_cond)   # ← スローパス
          if result == Proved:
            continue                    # 論理的切断
        # 経路条件なし、または SMT 証明失敗 → 逆辺を穿越
        # fall through

      if pred ∉ unsafe:
        queue.push(pred)

  # 判定（書込み先・借用後）
  # node < created_at(token) → 書込時点でトークン未存在 → Safe
  if node ∈ unsafe かつ created_at(token) ≤ node:
    return Disproved
  else:
    return Proved


smt_fallback(path_cond, loop_cond):
  # 逆辺 + 経路条件ありの場合のみ呼び出し
  # RFC-027 証明パイプラインを使用、同一 SMT ソルバー、同一予算を共有
  return smt.prove(path_cond ⇒ !loop_cond)
  # Proved → 論理的切断
  # Disproved / Unproven → 切断しない、逆辺を穿越（保守的拒否）
  # SMT 利用不可/タイムアウト/未実装 = Disproved 分岐——
  # SMT は精度にのみ影響（合法プログラムの通過可否）、soundness には影響しない
  # （拒否すべきものは必ず拒否）；SMT 不在時の保守度 = ループ内借用+書込みの
  # 全拒否、これは Rust NLL と同等。

BrandNode にフィールド追加：

BrandNode:
  ...
  created_at: NodeId         # トークン生成ノード（借用区間の左端点）

O(N)、SMT 呼び出し回数 = 逆辺数 × 経路条件付き逆辺の割合。実コードでは SMT 呼び出しは極めて稀——while ループ体内、精化型変数の経路条件がある場合にのみ発動する。

経路条件収集

RFC-027 §3.2-3.3 の既存機構により提供される：

if ガード：if y > 0 → true 分岐に y > 0 をプッシュ
match パターン：if let Some(v) = opt → 分岐内に opt == Some(v) をプッシュ
代入：i += 1、コンパイラが変数の値域情報を保守
while cond：ループ体内に cond == true をプッシュ

各 DAG ノードは経路条件集合を保持する。逆向き BFS が逆辺に遭遇した時、逆辺始点の経路条件を取得し、SMT が次ループ入口条件の排除を判定する。

経路条件の伝播規則：

経路条件は書込ノード自身に付与される：分岐内書込操作 W はその分岐条件を保持する（if i == n { W } → path_cond(W) = i == n）。逆向き BFS が逆辺を穿越する際、SMT が判定するのは path_cond(W) ⇒ !loop_cond（W 到達経路はループを抜ける → 次イテレーションの consumer は到達不能 → 切断）であり、逆辺ノードの経路条件ではない。
合流点で保守的にクリア：if/else 合流点は分岐内経路条件を保持しない（両分岐条件の選言は通常判定不能のため直接クリア）。合流点後の書込操作の path_cond は空 → 逆辺を穿越。
経路条件のセマンティック化：path_cond は ConstExpr（RFC-027 §3.2 セマンティクス）であり、ソースコードテキストではない；smt_cut がこれを SMT 制約に翻訳して求解する。
経路条件なし → 逆辺を直接穿越（unsafe）、SMT は呼び出さない。

RFC-027 とのインタフェース

借用システム述語とユーザー述語は同じ証明パイプラインを共有する——違いは主力証明戦略のみ：

クエリ種別	命題ソース	主力戦略	フォールバック
型等式	型検査器	構造等価	—
ユーザー述語	プログラマー型注釈	SMT	プログラマー証明関数
借用競合	コンパイラ自動生成	DAG 構造解析（ファーストパス）	SMT 論理的切断

借用検査における SMT ソルバーの役割：主力ではなく、安全網。 while 逆辺の論理的切断が必要な場合にのみ呼び出される。借用検査の大多数はファーストパスで完結——O(N) 逆向き BFS、SMT オーバーヘッドゼロ。

既存コードとの関係

既存コンポーネント	取り扱い
`BorrowChecker`	`BorrowPredicateEmitter` に変身——借用ホーア命題を生成
`MoveChecker`	`MovePredicateEmitter` に変身——`¬moved(v)` 命題を生成
`DropChecker`	同上——Drop 関連命題を生成
`MutChecker`	同上——`is_mut(v)` 命題を生成
`ControlFlowAnalyzer`	不要——パイプラインが統一処理
`liveness_analysis`	保持——Drop 挿入は依然として変数活性情報を必要とする
`ir_gen.rs` Release ハードコード	削除——Release 位置は DAG コンシューマー解析駆動

NLL とイテレーション境界

トークン活性は区間 [created_at, last_use] であり、逆向き到達可能集合ではない。created_at = トークン生成ノード； last_use = コンシューマー解析が得る最大消費ノード。書込操作 W とトークン T の競合の必要十分条件： conflicts(T, W) ∧ created_at(T) ≤ node(W) ∧ node(W) は last_use(T) に前方到達可能（逆向き BFS で判定）。「書込み先、借用後」の合法順序（§2.4：引数トークンは呼出終了時に解放）は created_at(T) ≤ node(W) で直接排除され、特殊規則は一切不要。本モデルにより §トレードオフ利点 5「アルゴリズムが保守的でない」という宣言が全順序下で成立する。

トークン死亡時刻 = 最後の使用点（NLL）、語彙スコープ末尾ではない。

これはコンシューマー解析の自然な帰結：コンシューマーの位置がトークンの最終使用を定義する。use(v) は v のコンシューマー → use(v) の直後に v は死亡。トークンライフタイムを早期終了させるための追加の {} や drop() は不要。

ループ反復境界はトークンコピーの死亡線である。 三つの規則：

規則 1：ループ内で宣言された変数は反復終了時に自動死亡する。
        for の各反復は新バインディング（言語設計保証）、loop も同様。

規則 2：ブランド木の ref_count はループ頭でループ外生成のコピーのみを計上する。
        ループ内 Dup による新コピーは、ref_count が反復境界でゼロクリアされる。

規則 3：逆向き BFS が逆辺を穿越する際、現在の反復の活性情報を持ち越さない。
        ループ頭での ref_count のみを持ち越す（すなわち：ループ外のコピー）。

実例：

yaoxiang

view = &data                          # ループ頭：ref_count = 1、consumer = use(view)
loop {
    v2: &Point = view                 # ループ内 Dup → ref_count = 2
    use(v2)                           # consumer：v2 の最終使用 → v2 死亡 → ref_count = 1
    data.push(4)                      # ✅ 安全！v2 は死亡、view のみ残存（ref_count = 1、書込み競合なし）
    # 反復境界：規則 3——v2 を次反復に持ち越さない。次反復開始時 v2 は新バインディングで再生成される。
}

この設計には追加の「ループ内保守的存活」規則は不要。逆向き BFS はコンシューマーから出発し、コンシューマーがループ体内にある → 活性が現在の反復内に限定される → 逆辺は穿越しない。RFC-009a §ユースケース解析のループ例と完全一致。

`?` エラー伝播とスコープ駆動 Release

? は早期リターン——スコープの正常出口に加えてもう一つの脱出経路が存在する。トークンもこの経路で解放される必要があり、解放順序を誤れば UB となる。

Release 命令はスコープ解析により生成され、Call の後にハードコードされるのではない。

コンパイラは各スコープの出口点リストを保守する：

}（スコープ正常終了）
?（エラー伝播、早期 return）
明示的 return

各出口点で、宣言の逆順（LIFO）で当該スコープ内の全アクティブトークンの Release 命令を挿入する。ブランド木の親子関係が派生トークンのカスケード解放を自動処理する：

yaoxiang

Point.get_x: (self: &Point) -> (&Float, &Point) = {
    return (&self.x, self)    # 子トークン &Float + 親トークン &Point を返す
}

fn use_case(p: Point) -> Result<(), Error> = {
    (x_ref, p_ref) = p.get_x()?   # ? で伝播する場合：
    # ブランド木は x_ref が p_ref の派生（#42.field_x は #42 のプレフィックス）であることを知っている
    # 解放順序：x_ref（子）→ p_ref（親）→ LIFO で自動充足
    p.modify()                     # WriteToken——全 ReadToken 解放済み
    Ok(())
}

実装位置：ir_gen.rs に保持、スコープ駆動に変更——新しいコンパイラパスを導入しない。

上表の複雑度は設計見積もりであり、実測未実施；「~1ms」「極めて稀」は量級期待値であり測定値ではない、実装後に可観測性データで校正すべき。

SMT フォールバックの発動条件は極めて限定的：同時に (1) while ループ (2) ループ体内に書込操作 (3) 書込操作後にループ終了を示唆する経路条件 (4) コンパイラがその条件に依存して逆辺を切断する必要、を満たす場合。実コードでの比率は 1% を遥かに下回る。残りの借用検査は全てファーストパスで完結する。

RFC-027 ユーザー述語との関係：ユーザー述語は SMT を主力とし、借用システム述語は構造解析を主力とする。両者は同一 SMT ソルバーと予算上限（RFC-027 §8）を共有するが、借用システム述語は SMT 予算をほぼ消費しない。

線形コード → 逆辺なし → 層 1 O(N) で即座に結果。ループ + 経路条件 → SMT 呼び出し、線形算術でミリ秒級（RFC-027 予算 100ms）。一回 BFS 結果は同一トークンの複数クエリ向けにキャッシュ可能。

エラーメッセージ設計

核心原則：エラーメッセージはユーザーが書いたシンボルだけを含む。

Rust の借用関連エラーは二分類：

変数レベルエラー：E0597（生存期間不足）、E0502（可変 + 不変の同時借用）、E0499（複数回可変借用）。Rust は既に模範——変数名 + 行番号、'a は出現しない。YaoXiang は精度同等。情報は全てブランド木に含まれる：トークン生成点、コンシューマー位置、要求点。

シグネチャレベルエラー：E0623（lifetime mismatch）、E0106（missing lifetime specifier）、E0477（required lifetime 不充足）。'a を巡るもの。YaoXiang には此类のエラーが存在しない——シグネチャに 'a が含まれない。「報告できない」のではなく、ユーザーが書いていないものを報告しない。

関数内競合の例：

エラー：`data` は凍結されており、可変権限を取得できません
 --> src/main.yx:5:9
2 |     view = &data
  |            ----- `data` は凍結されています（読取専用トークンがここで生成）
4 |         use(view)
  |             ---- `view` はここでまだ使用中、凍結未解除
5 |         data.push(4)
  |         ^^^^ ここで可変権限が必要

（Rust E0499 と精度同等——変数名 + 行番号、ブランド ID は出現しない。）

関数間エスケープの例：

エラー：`num`（第 4 行）が保持するデータソースの一つは `default_str`（第 3 行）ですが、
`default_str` は第 6 行で失効し、`num` は第 5 行でまだ使用中です。

検討：`default_str` の宣言を呼び出し側に前倒すか、`ref default_str` で共有保持を使用してください。

（Rust E0597 と精度同等。ブランド要約は num に二つのソースパスがあることを知っている——コンパイラ内に既存、誤り措辞で利用可能。）

RFC-009 本文修正

RFC-009 §「トークン競合検出：フロー依存活性解析」を更新：

「不要なもの：……NLL」を削除——結論が誤っているためではなく、理由が誤っているため（「トークンは値であり、線形追跡で十分」）
層 1/層 2 移行案を保持、完全版は本 RFC を参照
明確化：ブランド ID（#42）とは 'a のこと——情報は完全同一、エンコードが異なる。新しい解析を発明したのではなく、ライフタイムを型層から証明層に降ろした

トレードオフ

利点

型シグネチャにライフタイムを含まない：#42 とは '42 のこと——同じ情報、ブランド木内にエンコードされ、型シグネチャに露出しない。本点は反証不可：Rust で 3 つの参照引数を持つジェネリック型が必要な 'a パラメータの数を数え、YaoXiang で必要な数を数える。答えは 3 vs 0。
概念統一：借用検査とユーザー述語は同じ証明パイプラインを共有——{P} op {Q}、パイプラインが P を検証。Curry-Howard 一貫。
新規解析フレームワークゼロ：新しい解析フレームワークを導入しない。ユーザーは「借用検査器」の存在を認識しない——「型検査器」の実装詳細を認識しないのと同様。
エラーメッセージはユーザーが書いたシンボルのみ：エラー分類の一つの次元を削除（E0623、E0106、E0477——全て 'a 関連）。変数レベルエラーは Rust と精度同等。
アルゴリズムが保守的でない：逆向き BFS + break 切断 + SMT 論理的切断。「ループ内保守的存活」不要。「分岐保守的マージ」不要。

欠点

新規発明ではない：ブランド ID が行うことは 'a と完全に同じ——コンパイラ内部の制約求解複雑度は消えておらず、エンコードが「変数名 + 制約集合」から「ブランドパス + プレフィックス一致」に変わっただけ。エンドユーザーへの違いはシグネチャに 'a を書かない点のみ。
全新実装：ブランド木はコード中に概念のみ存在し、ゼロから実装が必要。BorrowChecker、ControlFlowAnalyzer は置換される。
SMT 依存：論理的切断は Z3 に依存（RFC-027 で既に導入、新規依存なし）。ただし借用検査の発動は極めて稀——while + 経路条件時のみ。
極めて稀なパターンにリファクタが必要：コンパイラ自動証明でカバーできない分岐間借用は、ユーザーがコードをリファクタする必要がある。Rust 'a のフォールバックとは異なる：Rust には 'a という筆がある（注釈すれば通る）；YaoXiang のフォールバック（証明関数）は MVP ではない。

代替案

案	採用しない理由
完全な Rust NLL を実装	YaoXiang の設計制約（シャドーイング禁止、for 新バインディング）が NLL の主要複雑性源泉を既に排除、CFG 不動点は不要
現状維持（Release ハードコード）	不十分——ユーザーが手動でトークンスコープを管理する必要がある
spawn ブロック内のみ解析	不十分——非 spawn コード内のトークン使用が大多数
借用検査の代わりに GC	言語設計原則に違反——YaoXiang は GC なし

実装フェーズ

フェーズ	内容	依存
Phase 1	ブランド木データ構造実装	—
Phase 2	システム述語生成器（Borrow/Move/Drop/Mut → 命題）	Phase 1
Phase 3	逆向き BFS 活性解析 + パイプライン接続（層 1）	Phase 2
Phase 4	経路条件収集 + SMT 論理的切断（層 2）	Phase 3 + RFC-027 Phase 2
Phase 5	Release 命令を DAG コンシューマー駆動に変更	Phase 3
Phase 6	ControlFlowAnalyzer 削除、BorrowChecker 再構築	Phase 4

オープン問題

[x] ループ展開時の ref_count ブランド木の反復間セマンティクス——NLL 採用：トークンは最終使用後に死亡。ループ内バインディングのコピーは反復境界で死亡し、逆向き BFS は反復間活性を持たない。詳細 §NLL とイテレーション境界。
[x] ? エラー伝播経路上のトークン解放順序——Release はスコープ解析駆動（ir_gen.rs に保持）。各スコープ出口点（}、?、明示的 return）で LIFO によりアクティブトークン解放。ブランド木の親子関係がカスケード解放を自動処理。詳細 §? エラー伝播とスコープ駆動 Release。
[ ] 証明関数構文（遠期、MVP 外——どの Phase もブロックしない）

参考文献

RFC-009: 所有権モデル設計 — 親 RFC
RFC-027: コンパイル時述語と統一静的検証 — 証明パイプライン
RFC-010: 統一型構文 — {} セマンティクス
RFC-024: spawn ブロックベースの並行モデル — spawn DAG

ライフサイクルと帰趣

状態	位置	説明
受理済み	`docs/design/rfc/accepted/`	正式設計文書となる

RFC-009a: トークンライフタイム解析——ホーア証明パイプラインに基づく ​

概要 ​

動機 ​

RFC-009 の混同 ​

現状コードの実態 ​

なぜ書き直すのか ​

核心設計 ​

全てはホーア ​

二種類の述語、一本のパイプライン ​

借用命題：コンパイラ自動生成 ​

前方到達可能性：コンシューマーから逆向き ​

証明戦略：ファーストパス優先、SMT フォールバック ​

ユースケース解析 ​

線形コード ​

if/else：特殊規則なし ​

戻り値によるエスケープを伴う if/else ​

ループ：break が逆辺を切断 ​

while：SMT 論理的切断 ​

本質：ブランド ID は 'a そのもの ​

言語設計制約が排除したもの ​

なぜ DAG が実現可能か ​

詳細設計 ​

システム述語一覧 ​

ブランド木 ​

逆向き BFS 活性解析 ​

経路条件収集 ​

RFC-027 とのインタフェース ​

既存コードとの関係 ​

NLL とイテレーション境界 ​

? エラー伝播とスコープ駆動 Release ​

エラーメッセージ設計 ​

RFC-009 本文修正 ​

トレードオフ ​

利点 ​

欠点 ​

代替案 ​

実装フェーズ ​

オープン問題 ​

参考文献 ​

ライフサイクルと帰趣 ​

RFC-009a: トークンライフタイム解析——ホーア証明パイプラインに基づく

概要

動機

RFC-009 の混同

現状コードの実態

なぜ書き直すのか

核心設計

全てはホーア

二種類の述語、一本のパイプライン

借用命題：コンパイラ自動生成

前方到達可能性：コンシューマーから逆向き

証明戦略：ファーストパス優先、SMT フォールバック

ユースケース解析

線形コード

if/else：特殊規則なし

戻り値によるエスケープを伴う if/else

ループ：break が逆辺を切断

while：SMT 論理的切断

本質：ブランド ID は `'a` そのもの

言語設計制約が排除したもの

なぜ DAG が実現可能か

詳細設計

システム述語一覧

ブランド木

逆向き BFS 活性解析

経路条件収集

RFC-027 とのインタフェース

既存コードとの関係

NLL とイテレーション境界

`?` エラー伝播とスコープ駆動 Release

エラーメッセージ設計

RFC-009 本文修正

トレードオフ

利点

欠点

代替案

実装フェーズ

オープン問題

参考文献

ライフサイクルと帰趣