RFC-009a: 令牌生命期分析——基于霍尔证明管道

親 RFC: RFC-009: 所有権モデル設計
依存: RFC-027: コンパイル時述語と統一静的検証
前置条件: RFC-027 が既に受け入れられていること。本 RFC のすべてのメカニズム（証明パイプライン、SMT fallback、パス条件収集）は 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 から出発して、逆方向 BFS DAG。
辺が切断される場合：
  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 は構造分析が届かない角落だけを補充する。

ユースケース分析

線形コード

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 の複合ノードである。内部消費はこのノードに起因する。分岐状態をマージしない。保守的投票もしない。後に消費者がいるかどうかは、整数比較だけである。

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)                # 消費者
    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)                # 消費者
    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 にない → ✅

本質：ブランド ID は `'a` と同じ

「'a が不要」とは言わない。「#42は'42` である」と言う。

Rust	YaoXiang	等価性
`'a`	`#42`	コンパイル時ライフタイム識別子
`'a: 'b outlives 制約	`#42` は `#42.field_x` の前方一致	文字列前方一致比較 = 半順序関係
NLL 活性伝播（CFG 不動点）	逆方向 BFS（DAG）	どちらも到達可能性計算
Polonius 事実	SMT 論理的切断	どちらもパス条件推論
制約系不動点求解	ブランド樹前方一致マッチ + BFS	異なるエンコーディング、同じ問題

我々は新しい分析を発明していない。'a を型シグネチャ層から証明層に降格しただけである。 ブランド ID の仕事は 'a と完全に同じ——借用のアイデンティティをマークし、派生関係を追跡し、競合を判定する。違いは一つだけ：'a はユーザーの書いた型シグネチャにある；#42 はコンパイラー内部にある。

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

言語設計制約が何を排除したか

複雑さの来源	回避できたか	理由
変数シャドウイング	✅	言語が禁止——一つの名前は常に同じものを指す
for 跨イテレーション借用	✅	各イテレーションが新しいバインディング——イテレーション間で自然に分離
`'a` ライフタイム注釈	✅	ブランドパス = `#42.field_x`、コンパイラーが導出
名前付きライフタイム + 制約伝播	✅	ブランドパスの前方一致比較が明示的制約集合を代替
借用グラフ制約求解（Polonius）	✅	ブランド樹前方一致マッチ + DAG 消費者クエリ
ループ体内借用活性伝播	❌	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 → 競合（2つの書き込みは共存不可）
    a.source() == b.source()
        && (a.is_write() || b.is_write())
        && (a.is_prefix_of(b) || b.is_prefix_of(a))
}

O(depth) 文字列前方一致比較、深さ ≤ 3。定数レベル。

逆方向 BFS 活性分析

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

入力：
  token: チェックが必要な WriteToken
  node:  書き込み操作がある DAG ノード

出力：Proved | Disproved

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

  while queue not empty:
    cur = queue.pop()
    unsafe.add(cur)

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

      # バックエッジ → SMT fallback が必要かどうかチェック
      if pred がバックエッジ:
        path_cond = pred におけるパス条件
        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)

  # 判定
  if node ∈ unsafe:
    return Disproved
  else:
    return Proved


smt_fallback(path_cond, loop_cond):
  # バックエッジ + パス条件がある場合にのみ呼び出す
  # RFC-027 証明パイプラインを使用し、同じ SMT ソルバー、同じ予算を共有
  return smt.prove(path_cond ⇒ !loop_cond)
  # Proved → 論理的切断
  # Disproved / Unproven → 切断せず、バックエッジを横断

O(N)、ただし SMT 呼び出し回数 = バックエッジ数 × パス条件のあるバックエッジの割合。実際のコードでは SMT 呼び出しは非常に稀——while ループ体内、精化型変数のあるパス条件の場合のみトリガー。

パス条件収集

RFC-027 §3.2-3.3 の既存メカニズムが提供：

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

各 DAG ノードはパス条件セットを持つ。逆方向 BFS でバックエッジに遭遇したとき、バックエッジの起点からパス条件を取得し、SMT が次のループ入口条件を除外するかを判定する。

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

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

クエリタイプ	命題の来源	主力戦略	Fallback
型等式	型チェッカー	構造的同値	—
ユーザー述語	プログラマー型注釈	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 とイテレーション境界

令牌死亡時点 = 最後の使用点（NLL）、字句スコープ末尾ではない。

これは消費者分析の自然な帰結である：消費者の位置が令牌の最後の使用を定義する。use(v) が v の消費者である → v は use(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)                           # 消費者：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

各出口点で、そのスコープ内のすべてのアクティブ令牌の Release 命令を宣言の逆順（LIFO）で挿入する。ブランド樹の親子関係が派生存款令牌的级联解放を自動的に処理する：

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 に保持し、スコープ駆動に変更——新しいコンパイラーパスを導入しない。

操作	複雑さ	トリガー頻度
ブランド樹競合判定	O(1)	令牌が必要每次
DAG 消費者クエリ	O(1)	令牌が必要每次
逆方向 BFS（ファーストトラック）	O(N)	令牌が必要每次、N = ブロック内ノード数
SMT 論理的切断（fallback）	~1ms	極めて稀——while + パス条件のみ

SMT fallback のトリガー条件は極めて苛刻：同時に (1) while ループ (2) ループ体内書き込み操作 (3) 書き込み操作後にパス条件がありループ終了を判定できる (4) コンパイラーがその条件を必要としてバックエッジを切断する必要がある、を満たす必要がある。実際のコードでは 1% 未満を占める。それ以外の借用チェックはすべでファーストトラックで完了する。

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

線形コード → バックエッジなし → Layer 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` は冻结されており、mutable 権限を取得できない
 --> src/main.yx:5:9
2 |     view = &data
  |            ----- `data` が冻结されている（読み取り令牌はここで作成）
4 |         use(view)
  |             ---- `view` はここでまだ使用中、冻结が解除されていない
5 |         data.push(4)
  |         ^^^^ ここで mutable 権限が必要

（Rust E0499 の精度と並ぶ——変数名+行番号、ブランド ID は表示されない。）

関数間エスケープの例：

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

検討：调用元に `default_str` の宣言を提前するか、`ref default_str` を使用して共有所有に切り替える。

（Rust E0597 の精度と並ぶ。ブランドサマリーが num に2つのソースパスがあることを知っている——コンパイラー内に既にあり、エラーメッセージに使用できる。）

RFC-009 本文の修正

RFC-009 §"令牌冲突检测：流敏感活性分析"が更新された：

「不需要的东西：...NLL」を削除——結論が間違っているからではなく、理由が間違っているから（「令牌は値、線形追跡で十分」）
Layer 1/Layer 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 活性分析 + パイプライン接続（Layer 1）	Phase 2
Phase 4	パス条件収集 + SMT 論理的切断（Layer 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 本文の修正

トレードオフ

利点

欠点

代替案

実装フェーズ

開放問題

参考文献

ライフサイクルと归宿