RFC-027: コンパイル時述語と統一静的検証

参考:
RFC-009: ownership モデル
RFC-010: 統一型構文 - name: type = value モデル
RFC-011: generics システム設計
RFC-024: spawn ブロックベースの並行モデル
置き換え：RFC-022: Hoare ロジック静的検証サポート（仕様コメントと仕様型） — 廃止済み

要約

本文では、YaoXiang にコンパイル時述語（compile-time predicate）を第一級市民として導入し、すべてのコンパイル時静的検証を一つの証明パイプラインに統一することを提案する。コンパイル時述語は外部仕様の注釈ではなく、それ自体が一つの関数である。Type を返す関数は型の位置で使用でき、コンパイラがコンパイル時に呼び出して戻り値をチェックする。型は命題、コンパイル時評価は証明である。

核心的な論点：コンパイル時の型検査の唯一の仕事は、証明項の構築と検証である。型等価、トークン衝突、依存型簡約、コンパイル時述語評価、Hoare 論理含意——これらすべてはコンパイル時証明パイプライン内の異なる型検査であり、同じパイプラインを共有する。SMT ソルバーは型チェッカーのアクセラレータモジュールであり、独立した信頼境界ではない。コンパイラが Unproven を返したとき、プログラマは YaoXiang 関数を証明として記述する——型チェッカーは任意の関数の戻り型を検証するのとまったく同じ方法でそれを検証する。すべてが YaoXiang コードであり、すべてが型チェッカーによって検証される。

動機

なぜ RFC-022 を廃止するのか？

RFC-022 は仕様を //! コメント形式として設計している：

yaoxiang

max: (T: Ord) -> ((arr: Array(T, n)) -> T) = {
    //! requires: NonEmpty(n) = n > 0          ← 型に独立したコメント
    //! ensures: ExistsMax(result, arr[0..n])   ← 型に独立したコメント
}

これは Curry-Howard 同型の根本的な誤りを犯している：仕様と型を二つの層に分断すること。コメントは型ではない。コメントは型検査に参加しない。コメントは「外部ツール」のメンタルモデルである。

ホワイトペーパーは明確に述べている：

"//! コメントはない。独立した仕様言語はない。すべては型システムの中にある。"

現状の問題

RFC-022 の //! コメントは型システムから独立した外部構文
仕様型と通常型は二系統であり、概念の冗長を生む
Debug Build で検証 / Release Build で無視という分断モデルが統一性を破壊する
SMT ソルバーは従来「外部ツール」として位置付けられてきた——YaoXiang では型チェッカーのアクセラレータモジュールとして内蔵する
型検査、借用検証、コンパイル時述語検査、マクロ展開がそれぞれ別々のパスを通る

正しいメンタルモデル

型検査は一つの関数として抽象化できる：

verify : Program → Proved | Disproved(Model) | Unproven

すべてのコンパイル時検査——単純な型マッチ、借用衝突検出、コンパイル時述語検証——はこの関数のサブタスクである。同じ証明パイプラインを共有し、違いはあくまで証明項の複雑さと構築戦略だけである。

コンパイラが Unproven を返したとき、プログラマは証明関数を提供する——その関数の戻り型は証明すべき命題に等しい。型チェッカーはそれを検証する。これは通常の型検査とまったく同じ操作である。

提案

1. `{}` は証明空間：型はアサーション、検証は型検査

YaoXiang の {} はコンパイル時証明空間である。内部のすべてはアサーションであり、コンパイラが各項目を True であることを保証する——自動証明されるか、プログラマが証明関数を提供することのいずれかによって。

Point: Type = { x: Float, y: Float }
#               ^^^^^^^^^^^^^^^^^^^^^  コンパイラが x が Float、y が Float であることを保証

List: (T: Type) -> Type = { data: Array(T) }
#                           ^^^^^^^^^^^^^^^  コンパイラが data が Array(T) であることを保証

generics はコンパイル時述語の特殊ケースである。

yaoxiang

Positive: (x: Int) -> Type = { x > 0 }
#          ^^^^^^              ^^^^^^
#          パラメータはシグネチャ位置      {} 内にはアサーションのみ
#          コンパイラはコンパイル時に呼び出して x > 0 を検証

List: (T: Type) -> Type = { data: Array(T) }
#      ^^^^^^^^              ^^^^^^^^^^^^^^^
#      パラメータはシグネチャ位置    コンパイラが type_of(T) == Type、type_of(data) == Array(T) を検証

同じパターン：name: (params) -> Type = { アサーション }。コンパイラは「型アサーション」と「値アサーション」を区別しない——どちらも証明パイプラインにおける評価対象である。

ループ不変条件を別途記述する必要はない。変数上の型注釈がそのまま Floyd-Hoare 不変条件である。

yaoxiang

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0   # 注釈は i を参照する——s の型が i に依存することをコンパイラに伝える
    mut i: UpTo(arr.len) = 0     # 初期化時 i=0、検証：0 == sum(arr[0..0]) → True
    while i < arr.len {
        s += arr[i]  # コンパイラが検証：s_new == sum(arr[0..i+1])
        i += 1       # i 変更→s の依存再検証をトリガ：s は SumUpTo(arr, i_new) を満たす
    }
    return s  # s: SumUpTo(arr, arr.len) = sum(arr[0..arr.len])
}

コンパイラはループ本体に対して一度だけ検証条件を生成する——帰納仮説（型注釈）→ 代入操作 → 新値が型注釈を満たすか。証明パイプラインが帰納ステップの成立を検証すれば、すべての反復が自動的にカバーされる。: decreases も : Invariant も帰納証明も不要——コンパイラは帰納を各代入の局所 VC に分解する。

2. 前置/後置条件：パラメータ型と戻り型上のコンパイル時述語

RFC-022 の //! requires///! ensures を廃止する。コンパイル時述語はパラメータまたは戻りの型注釈として記述する。

パラメータ側は関数呼び出しである。 コンパイル時述語は Type を返す関数であり、パラメータ側での使用方法はそれを呼び出すこと——factorial(5) とまったく同じである。戻り型側は新しい概念を導入する：戻り値仮パラメータ。

yaoxiang

# 前置条件：パラメータ型でコンパイル時述語を明示的に呼び出す
Positive: (x: Int) -> Type = { x > 0 }

divide: (a: Int, b: Positive(b)) -> Int = a / b
#                       ^^^^^^^^^^  b は現在の仮パラメータ名、Positive に引数として渡される
#                       コンパイラは呼び出し点で実引数値を抽出し、b に代入し、Positive(実引数) を検証
#                       例：divide(10, 2) → Positive(2) = { 2 > 0 } を検証 → True
#                       例：divide(10, 0) → Positive(0) = { 0 > 0 } を検証 → False → コンパイルエラー

# 後置条件：戻り値仮パラメータ + コンパイル時述語
IsMax: (T: Ord, arr: Array(T), result: T) -> Type = {
    forall j in 0..arr.len: result >= arr[j]
}

NonEmpty: (arr: Array(T)) -> Type = { arr.len > 0 }

max: (T: Ord) -> ((arr: NonEmpty(arr))) -> (result: IsMax(T, arr, result)) = {
#                                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
#                                            result は戻り値仮パラメータ、値は return で提供
#                                            コンパイラは return 点で戻り値を代入し、後置条件を検証
    candidate = arr[0]
    for i in 1..arr.len {
        if arr[i] > candidate { candidate = arr[i] }
    }
    return candidate
}

重要なルール：

パラメータ側：b: Positive(b) —— b は現在の仮パラメータ名であり、Positive に引数として渡される。関数呼び出し構文、ゼロ暗黙。
戻り側：-> (result: IsMax(T, arr, result)) —— result は戻り値仮パラメータ、値は return 文で提供される。result は型シグネチャ内にのみ存在し、述語によってのみ参照され、関数本体のスコープには入らず、呼び出し側にも現れない。
戻り値仮パラメータはオプション：後置条件がない場合は記述せず、シグネチャは通常関数と完全に一致する（-> Int）。
統一性：パラメータと戻り値仮パラメータは同じ概念——仮パラメータ名: 述語呼び出し(仮パラメータ名)——であり、値が呼び出し側から提供されるか return から提供されるかの違いだけである。

3. パス条件伝播：ランタイム値のコンパイル時検証

コンパイル時述語が束縛位置で使用されるとき、パラメータはプログラマが明示的に渡す。ランタイム値が refined 型パラメータに入るとき、コンパイラはパス条件収集と SMT 含意判定によって検証を完了する——プログラマが明示的に証明を渡す必要はない。

3.1 明示的関数呼び出し

コンパイル時述語が束縛位置で使用されるとき、パラメータはプログラマが明示的に渡す——関数呼び出しそのもの、ゼロ暗黙。

Positive: (x: Int) -> Type = { x > 0 } はコンパイル時述語コンストラクタである。それが束縛位置（パラメータ宣言、変数宣言、戻り型）に現れるとき、プログラマは明示的に束縛済みの変数名を渡す：

yaoxiang

b: Positive(b)
// b は現在の仮パラメータとして宣言済み、Positive(b) は関数呼び出し
// 正格化後：b: { b > 0 }

コンパイラが暗黙的にパラメータを埋める必要はない——b: Positive(b) は f(5) と同じく単なる関数呼び出しである。b はパラメータ名として束縛され、その型注釈 Positive(b) は b 自身を参照している——これは依存型の標準パターンであり、暗黙の展開ルールではない。

RFC-010 の self との統一：RFC-010 は self はキーワードではなく単なるパラメータ名の慣習（"p、this、x と書いても効果はまったく同じ"）を確立している。b: Positive(b) は同じ機構を共有する——パラメータ名は型注釈内で参照可能。self は self: Point の位置に現れ、b は b: Positive(b) の位置に現れ、両者の型注釈はパラメータ自身を参照する。違いは型注釈の複雑さだけで、機構はまったく同じである——名前が束縛された後、型はその名前に依存できる。

戻り型も同様に明示的関数呼び出しを使用する：

yaoxiang

Sorted: (arr: Array(T)) -> Type = { forall i in 0..arr.len-1: arr[i] <= arr[i+1] }

sort: (arr: Array(T)) -> (result: Sorted(result)) = { ... }
//                        ^^^^^^^^^^^^^^^^^^^^^^^
//                        result は戻り値仮パラメータ、Sorted(result) は関数呼び出し
//                        コンパイラは return 点で戻り値を result に代入し、Sorted(戻り値) を検証

局所変数宣言にも同様に適用される：

yaoxiang

let x: Positive(x) = 5
// x は 5 として束縛、Positive(5) → { 5 > 0 } → True → 通過

// let y: Positive(y) = 0
// y は 0 として束縛、Positive(0) → { 0 > 0 } → False → コンパイルエラー

3.2 パス条件収集

ランタイム値が条件分岐に現れるとき、コンパイラは自動的にパス条件を収集し、現在のスコープの仮定集合を形成する。これらの仮定はコンパイル時 Bool 評価の背景知識として検証に参加する。

yaoxiang

if y > 0 {
    // コンパイラはこの分岐内で自動的に仮定を取得：{ y > 0 }
    let result = divide(x, y)
    // 検証条件：(y > 0) ⇒ (y > 0)
    // 証明パイプラインが含意成立を判定 → Proved
} else {
// この分岐の仮定：{ !(y > 0) }
// divide(x, y) を呼び出す場合、検証条件は !(y > 0) ⇒ y > 0
    // 証明パイプラインが含意不成立を判定 → Disproved
}

これはコンパイラが特定のパターンをハードコードしているのではない——コンパイル時証明パイプラインの自然な振る舞いである。型検査の呼び出しごとにパイプラインへ送信される：

{背景仮定} ⇒ {検証目標}

証明パイプラインが含意性を判定する。Proved → 通過、Disproved → コンパイルエラー + 反例、Unproven → コンパイルエラー + 未解決命題。背景仮定は現在のプログラム点のパス条件に由来する。

3.3 仮定スタック

コンパイラは制御フロー解析において、各基本ブロックに対して仮定集合を保持する：

if ガード：if y > 0 → true 分岐に y > 0 をプッシュ、false 分岐に !(y > 0) をプッシュ（else を使用する場合）
match パターン：if let Some(v) = opt → 分岐内に opt == Some(v) をプッシュ
論理結合：if x > 0 and y < 10 → 分岐内に x > 0 と y < 10 をプッシュ
関数前置条件：divide(a, b) を呼び出すとき、b が Positive の証拠を持つことは現在の仮定から来るか、実引数自身の refined 型注釈から来る（b が既に Positive として注釈されていれば、その型は b > 0 を運ぶ）
代入：let z = y のとき、y 上の既存の refined 条件が z に伝播する

すべての仮定はコンパイル時証明パイプラインに入る。SMT アクセラレーションパスに入るとき、SMT-LIB 背景アサーションに翻訳される。

3.4 静的証拠なしならコンパイルエラー

プログラマが直接以下のように書いた場合：

yaoxiang

divide_user_input: (x: Int, y: Int) -> Int = divide(x, y)

現在のプログラム点には y > 0 の仮定がなく、実引数 y 自身にも Positive 型注釈がない。検証条件は：

{} ⇒ { y > 0 }

パイプラインは Disproved（含意不成立）を返す → コンパイルエラー：

divide 呼び出しにおいてパラメータ b が Positive を満たすことを証明できない。y は関数入力に由来し、証明済みの境界を持たない。if 分岐ガードによる呼び出しを検討すること：if y > 0 { divide(x, y) }。

YaoXiang は、静的証拠を提供せずにランタイム値が直接 refined 型パラメータに入ることを許さない。これは制限ではなく、ハードセーフティ哲学の中核である。コンパイラが静的に証明できないコードは、编译を通してはならない。

3.5 統一パイプラインとの関係

パス条件伝播は追加の機構ではない。これはコンパイル時証明パイプラインの制御フロー解析における直接的な拡張である：

段階	責務
パス条件収集	コンパイラの制御フロー解析段階で、各基本ブロックに仮定集合を注釈
検証条件生成	検証が必要な型制約に遭遇したとき、パス条件 + 実引数型情報をマージ
証明パイプライン評価	コンパイラカーネル → SMT アクセラレーション → Proved / Disproved / Unproven を得る
結果	`Proved` → 通過；`Disproved` → コンパイルエラー + 反例；`Unproven` → コンパイルエラー + 未解決命題（プログラマが証明関数を提供可能）

新しい部品はない。特別なルールもない。パス条件は証明パイプラインの背景知識である——型等式、借用制約と同じパイプライン、同じ予算システムを共有する。

4. コンパイル時証明パイプライン

すべてのコンパイル時検査は同じパイプラインを共有する。パイプラインの核心操作は型検査である——ある証明項の型が証明すべき命題に等しいかを検査する。すべては型検査である。

コンパイル時に Bool 式の評価が必要（即ち、証明項の構築が必要）
        │
        ├── 型等価 (T1 == T2)
        │   → コンパイラが直接判定（構造的等価）
        │
        ├── トークン衝突条件 (!conflicting(tokens))
        │   → フロー敏感ライブ性解析 (Dup/Linear 属性追跡)
        │
        ├── 依存型簡約 (n + m 簡約)
        │   → コンパイル時項書き換えシステム (βδι-簡約)
        │
        ├── コンパイル時述語 (x > 0, forall...)
        │   → コンパイラ本体 + SMT アクセラレーションモジュール
        │
        └── Hoare 論理含意 (P ⇒ Q)
            → コンパイラ + SMT アクセラレーションモジュール
                    │
                    ▼
             ┌──────────┐
             │ Proved   │  → コンパイル通過
             │ Disproved│  → コンパイルエラー + 反例
             │ Unproven │  → コンパイルエラー + 未解決命題
             └────┬─────┘
                  │
                  ▼
         プログラマが証明関数を記述 (YaoXiang コード)
                  │
                  ▼
         型チェッカーが検証 ──→ Proved ──→ コンパイル通過
                  │
                  ▼
            検証失敗 → コンパイルエラー："証明が成立しない"

4.1 証明結果：三値代数

コンパイル時評価は三つの結果を返す——これは停止問題の必然的帰結であり、証明論の自然な区分でもある：

eval_compile_time : BoolExpr → Proved | Disproved(Model) | Unproven

Proved → 停止、証明項が構築済み、型検査通過。コンパイル続行。
Disproved(M) → 停止、反例 M が存在。コンパイルエラー + 反例 + ソース位置。
Unproven → 与えられたリソース上限内で証明が構築されなかった。コンパイルエラー + 未解決命題 + 予算消費レポート。

Unproven ≠ False。 コンパイラが「証明できない」と言うのは命題が偽であることと同義ではない——現在の自動証明能力を超えているだけである。これは正直さであり、欠陥ではない。

予算のハード制限は停止問題の工学的解である。ノブは提供しない——ノブを提供することは「あなたのプログラムは停止すると思いますか」とユーザーに尋ねることに等しく、ユーザーは知らず、コンパイラも知らない。

4.2 Unproven の後：プログラマが証明を記述する

コンパイラが Unproven を返したとき、プログラマは証明関数を記述できる——すなわち、YaoXiang 関数であり、その戻り型が証明すべき命題に等しい。型チェッカーはこの関数を検証する——add(a, b): Int を検証するのとまったく同じ機構である。

命題  = 型
証明  = プログラム（その型の値）
検証  = 型検査（唯一の信頼の根）

SMT ソルバーは独立した信頼境界ではなく、型チェッカーのアクセラレータモジュールである。SMT は証明を見つける手助けをするが、証明を検証するのは常に型チェッカーである。SMT が unsat を返したとき、コンパイラはその結果を型チェッカーが検証可能な証明項に再構成する。再構成が失敗した場合（SMT の推論ステップがコンパイラカーネルの推論規則を超える場合）、Unproven にフォールバックする——プログラマは手動で証明関数を記述できる。

yaoxiang

# 命題：コンパイラが自動証明できない refined 属性
FirstIsMin: (T: Ord, arr: Sorted(T)) -> Type = {
    forall i in 0..arr.len: arr[0] <= arr[i]
}

# 証明：プログラマが関数を記述、戻り型は上の命題
# 型チェッカーがこの関数を検証——add(a,b): Int を検証するのと完全に一致
first_is_min: (T: Ord, arr: Sorted(T)) -> FirstIsMin(T, arr) = {
    # コンパイラがここで検証：関数本体の型 = FirstIsMin(T, arr)
    ...
}

AI も不要、Coq へのエクスポートも不要、新しい概念も不要。コンパイル時に自動証明できない属性 → プログラマが YaoXiang コードで証明を記述 → 型チェッカーが検証。 プロセス全体はスムーズなグラデーションである——コンパイラが簡単な証明を引き受け、難しいものは脳に任せる。

4.3 パイプライン内の階層的依存

上記の評価器は同じインターフェースを共有するが、評価順序が存在する。型等価はすべての後続分析の前提条件であり、所有権/トークン検査は型情報に依存し、refined 述語検証は前二層の結果に依存する。コンパイラは層ごとに評価し、底层で失敗した式は上層に渡らない——型エラーを持つプログラム上で求解予算を浪費しない。

評価順序（同一パイプライン、階層的スケジューリング）
├── 第 0 層：型等価 (T1 == T2)
│   └── 構造的単一化 → 失敗なら以降は無意味、直接 Disproved を返す
├── 第 1 層：所有権/トークン衝突
│   └── フロー敏感ライブ性解析 → 失敗ならメモリ安全性が不成立、直接 Disproved を返す
└── 第 2 層：refined 述語 / Hoare 含意
    └── コンパイラ本体 → SMT アクセラレーション → Proved / Disproved / Unproven を得る

各層は依然として Proved/Disproved/Unproven を返し、同じインターフェースと同じ予算システムを共有する。

5. 三層関数の統一

階層	実行タイミング	入力	出力	例
値レベル関数	ランタイム	値	値	`add: (a: Int, b: Int) -> Int = a + b`
型コンストラクタ	コンパイル時	型/値	Type	`List: (T: Type) -> Type = { data: Array(T) }`
コンパイル時述語	コンパイル時	値	Type	`Positive: (x: Int) -> Type = { x > 0 }`

すべて同じ name: type = value 構文を使用。コンパイル時述語と型コンストラクタは同じコンパイル時証明パイプラインを通る——{} は証明空間。

6. ループ：Floyd-Hoare 検証条件生成

ループは個別の : Invariant(...) や : decreases(...) 注釈を必要としない。変数上のコンパイル時述語型注釈が Floyd-Hoare 風のアサーションを定義する——コンパイラは型注釈から検証条件を生成し、証明パイプラインが各代入が型を保持するかをチェックする。

核心機構：各代入操作は Hoare 三つ組 {P} x := e {Q} に対応し、検証条件は P ⇒ Q[e/x] である。コンパイラはループ本体に対して一度だけ検証条件を生成する——証明パイプラインが帰納ステップの成立を検証すれば、すべての反復が自動的にカバーされる。

yaoxiang

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0   # 注釈は i を参照；初期化時 i=0、検証：0 == sum(arr[0..0]) → True
    mut i: UpTo(arr.len) = 0     # 検証：0 <= 0 <= arr.len → True
    while i < arr.len {
        # コンパイラがループ本体に対して一度 VC を生成。前提：s は SumUpTo(arr, i) を満たし、i は UpTo(arr.len) を満たす。
        #
        # s += arr[i]：
        #   検証義務：s_new は SumUpTo(arr, i) を満たす（現在の i は不変）
        #   s_new = s_old + arr[i] を代入：
        #     s_old + arr[i] == sum(arr[0..i+1]) が必要
        #     帰納仮説 s_old == sum(arr[0..i]) から、両辺に arr[i] を加える：
        #     sum(arr[0..i]) + arr[i] == sum(arr[0..i+1])
        #   コンパイラ + SMT：線形算術、ミリ秒単位 → Proved
        #
        # i += 1：
        #   i 変更 → 依存図で s の型注釈が i を参照 → 再検証をトリガ
        #   新しい検証目標：s は SumUpTo(arr, i_new) を満たす
        #   即ち s == sum(arr[0..i_new])、上のステップで保証済み → Proved
        s += arr[i]
        i += 1
    }
    return s  # このとき s: SumUpTo(arr, arr.len)、即ち s == sum(arr[0..arr.len])
}

ループ不変条件は変数上の型注釈である——プログラマは型を記述し、コンパイラは帰納ステップをチェックする。コンパイラは不変条件を「発見」する必要も、「自動的に帰納を行う」必要もない——帰納証明を各代入操作の局所検証条件に分解し、証明パイプラインに分割して処理させる。

6.1 依存追跡：可変変数上の依存型

上記の機構の前提は、コンパイラが s の型注釈 SumUpTo(arr, i) が i を参照していることを知っていることである——i が変更されたとき、s の型制約もそれに従って変化する。これはコンパイラが変数間の型依存グラフを保守することを必要とする。

データ構造：

TypeDepGraph: Map<VarName, Set<VarName>>
# キーは依存される変数、値はその変数を型注釈内で参照している変数の集合
# 例：{ i: {s}, j: {s, t}, ... }

構築：型チェッカーが mut v: Pred(... x ...) = init を処理するとき、Pred(...) パラメータ内の自由変数参照を解析する。パラメータが現在のスコープ内の他の可変変数 x を参照している場合、依存グラフに x → v を記録する。

トリガ：依存される変数 x が代入されたとき、コンパイラは：

依存グラフで x に依存するすべての変数 {v₁, v₂, ...} を検索
各 v について、検証条件を生成：v の現在値が更新後の型 Pred(... x_new ...) を満たすか
VC を証明パイプラインに送る

代入順序敏感性：依存追跡は正しい代入順序を自然に強制する。SumUpTo(arr, i) を例に取る：

yaoxiang

# 正しい順序
s += arr[i]   # s_new は SumUpTo(arr, i+1) を満たす
i += 1        # i 変更 → s が SumUpTo(arr, i_new) を満たすことを再検証 → True

# 誤った順序——コンパイラが拒否
i += 1        # i 変更 → s が SumUpTo(arr, i_new) を満たすことを再検証
              # s はまだ更新されていない、s_old == sum(arr[0..i_old]) ≠ sum(arr[0..i_new])
              # → コンパイルエラー：変数 s が型 SumUpTo(arr, i_new) を満たさない
s += arr[i]   # 到達不能

組み合わせ依存：一つの変数が複数の変数に依存できる。型注釈 { v: Int; v == x + y } は x と y の両方に同時に依存する——いずれの変更も再検証をトリガする。

証明パイプラインとの関係：依存追跡は VC 生成のトリガであり、独立した検証機構ではない。それは「いつ VC を生成する必要があるか」に答え、証明パイプラインは「VC が成立するか」に答える。

7. 停止性検査

適用範囲：refined 型。 停止性は独立したスイッチではなく、検証モードの一部である：型が一度 refined（Refined { base, constraint }）されると、それが注釈する計算セグメントは検証モードに入り、モード内では停止性が要求される；refined されていない通常の型は検証モードに入らず、停止義務を生成しない。

これにより二つの帰結が得られる：

ループ：生の while は検証モードに入らない；測度変数が refined 注釈（例：i: UpTo(n)）を持つ場合、検証モードに入り、停止性を証明する必要がある。
再帰：関数シグネチャが refined を持つ場合（パラメータ refined または戻り型に refined を含む）、検証モードに入り、各再帰呼び出し点の測度が厳密に減少することを証明する必要がある。

モード内では全自動が優先される：コンパイラはまず自動的に測度を探索し、証明できるものは通過する；探索できず、かつ明示的に測度が与えられていない場合はコンパイルエラー。注釈構文の逃げ道はない——測度と停止命題は型位置に書かれ、decreases のような新しい構文を導入しない。測度と明示的フォールバックの形式は §6.9 を参照。

6.1 設計原則

コンパイラは二箇所から停止証明に必要な情報を自動的に抽出する：

変数の型注釈：refined 型の境界制約（例：UpTo(n) は上界 n と下界 0 を提供）
ループ本体の操作：各反復が変数に施す操作

コンパイラは優先順位に従って四つの測度合成戦略を試し、見つかれば停止する。四つの戦略は測度探索の制限付きテンプレート列であり、入力は refined 制約（戦略 1–4 すべて「有界型の変数」を起点とする）であり、「コンパイル時に評価されるコード」ではない；これらは §6.9 の明示的測度と同じ事柄の自動と手動の二面である。

測度探索は探索であり、推論ではない。 探索はテンプレート（線形ランク、違反カウント、有界パターン、乗法スケール）のみを列挙し、解の存在を保証しない——汎用測度推論は一般に決定不能（停止問題に還元）である。したがってテンプレート外のケースはプログラマが明示的に測度を提供できる（§6.9）必要があり、そうでなければコンパイルエラー。

6.2 戦略 1：線形ランク関数の自動合成

変数が線形境界注釈を持つ場合、コンパイラは候補線形測度を列挙し SMT で検証する。

入力：
  変数 v₁: UpTo(u₁), v₂: UpTo(u₂), ...（境界を持つ変数）
  ループ条件 cond
  ループ本体内の代入集合

アルゴリズム：
  1. 型注釈から各変数の境界を抽出：[low_i, high_i]
  2. 候補測度を列挙：v_i, u_i - v_i, v_i - v_j、その他の線形結合
  3. 各候補測度 m について：
     - SMT で m ≥ 0 を検証（型境界から導出）
     - ループ本体の各実行パスについて、SMT で m' < m を検証（厳密減少）
  4. 条件を満たす線形結合を発見 → 停止性証明済み

カバー範囲：任意の変数が線形式（v = a·v + b）に代入され、有界型注釈を持つループ。i += const、i -= const、および二分探索のような区間収縮を含む：

yaoxiang

# 二分探索：low = mid + 1 または high = mid
# 測度 high - low は二つのパスで厳密に減少
binary_search: (arr: Sorted(Int, arr), key: Int) -> Option(Int) = {
    mut low: UpTo(arr.len) = 0
    mut high: UpTo(arr.len) = arr.len
    while low < high {
        let mid = (low + high) / 2
        if arr.data[mid] < key { low = mid + 1 }
        else if arr.data[mid] > key { high = mid }
        else { return Some(mid) }
    }
    return None
}

6.3 戦略 2：述語違反カウント——目標型から自動的に測度を抽出【実験的戦略】

⚠️ 現在の状態：実験的戦略。Phase 3 実装時に実際の実現可能性に応じて含めるかを決定。 この戦略は隣接交換操作（バブルソート、挿入ソート）に有効だが、非隣接操作（クイックソート partition、ヒープソート sift-down）は自動証明できない。カバー範囲の境界は以下の表を参照。Phase 3 検証が実行不可能な場合、この戦略は削除されるか将来の作業に格下げされる。

核心的洞察：ユーザーが記述した仕様はコンパイラの推論の素材である。 コンパイラは「ソートとは何か」を内蔵する必要がない——Sorted の定義を読み、定義から自動的に測度を抽出する。

入力：
  目標型：Sorted(arr) = { forall i in 0..arr.len-1: arr[i] <= arr[i+1] }
  ループ本体の操作：隣接要素の交換

アルゴリズム：
  1. 述語定義を解析：forall i in range: cond(i, arr)
  2. 自動的に測度を生成：violation_count = |{ i | ¬cond(i, arr) }|
  3. 操作の測量への影響を分析：
     - 隣接交換 arr[j], arr[j+1] = arr[j+1], arr[j]
     - インデックス j-1, j, j+1 の三対のみに影響
     - arr[j] > arr[j+1]（述語違反）なら、交換後この対は述語を満たす
     - violation_count は少なくとも 1 減少
  4. 上界：n·(n-1)/2（最大隣接逆順数）、下界：0
  → 停止性証明済み

現在のカバー範囲：

アルゴリズム	操作パターン	戦略 2 で証明可能？	理由
バブルソート	隣接交換	✅	violation_count は各交換で厳密減少
挿入ソート	隣接移動	✅	各シフトで違反対を 1 つ解消
選択ソート	非隣接交換	❌	単一交換で violation_count が増加する可能性
クイックソート	partition 分割	❌	非隣接交換、単調減少を保証しない
ヒープソート	sift-down	❌	木操作、violation_count が非単調

補完戦略：クイックソートの場合、low < high の区間収縮は戦略 1（線形ランク関数）でカバーできる——外層の partition 再帰では、各反復で区間が半分になる。戦略 1 と戦略 2 は補完的にカバーし、ほとんどの実際のアルゴリズムの停止性はどちらか一方で証明できる。しかし戦略 2 の汎用化（非隣接操作、木操作）は依然として未解決問題である。

yaoxiang

sort: (arr: Array(Int)) -> (result: Sorted(result)) = {
    mut i: UpTo(arr.len) = 0
    while i < arr.len - 1 {
        mut j: UpTo(arr.len - i - 1) = 0
        while j < arr.len - i - 1 {
            if arr.data[j] > arr.data[j+1] {
                arr.data[j], arr.data[j+1] = arr.data[j+1], arr.data[j]
            }
            j += 1
        }
        i += 1
    }
    return arr
}

6.4 戦略 3：有界増減パターン

v += const（正の定数）、変数が上界型注釈を持つ → 測度 upper_bound - v は各反復で const ずつ減少、下界 0。これは戦略 1 の縮退ケースであり、コンパイラは最初に高速処理する。

6.5 戦略 4：乗法スケール測度テンプレート

v *= const（const > 1）、変数が上下界型注釈を持つ。コンパイラは対数測度テンプレート ceil(log_const(upper/v)) を内蔵し、const 倍するごとに測度が 1 減少する。

yaoxiang

mut i: Positive(i) = 1
while i < n {
    # コンパイラが自動推論：測度 ceil(log₂(n/i))、2 倍するごとに測度が 1 減少
    i *= 2
}

6.6 停止性と正当性の分離

停止性証明と正当性証明は独立である：

停止性：上記四つの戦略がループが有限ステップで終了することを自動証明；探索できない場合はプログラマが型位置に測度を提供（§6.9）
正当性：ループ本体が目標型に向かって進むかは、コンパイル時証明パイプラインが検証条件を通じてチェック

両方が通過 → コンパイル通過。停止性証明済みだが正当性が失敗 → コンパイルエラー + 反例。正当性証明済みだが停止性を証明できない → コンパイルエラー、分析不能な変数または操作を指す。両方失敗 → コンパイルエラーが二つの失敗理由を別々に報告。

6.7 再帰関数の停止性検査

refined シグネチャを持つ再帰関数について、コンパイラは各再帰呼び出し点の仮パラメータ減少をチェックする：

yaoxiang

gcd: (a: Int, b: NonNegative(b)) -> Int = {
    if b == 0 { return a }
    return gcd(b, a % b)  // コンパイラが探索：(b, a % b) の整列順序測度が減少 → 停止
}

仮パラメータ減少は最強の自動パス（構造的再帰）である。探索できない場合、プログラマは型位置に明示的に測度を提供できる（§6.9）。

6.8 ハード境界

i = f(i) で f が可逆ではなく、閉じておらず、単調性を保持しない場合——数学的には自動停止証明は不可能。コンパイルエラー：

このループは自動停止証明できない。ループ変数が分析不能な関数 f に依存する。コンパイラが分析可能な反復パターンを使用するか、そのループに名前を付けて型位置に測度を提供（§6.9）すること。

これはコンパイラの失敗ではない。静的に安全を証明できないコードは、编译を通してはならない。明示的な測度が与えられても、SMT によって真と判定されなければ通過しない——測度を誤って記述すれば反例で差し戻され、人は証明できないだけで、誤った証明をすることはできない。

6.9 明示的測度：`Terminates`

自動探索が測度を見つけられない場合、プログラマは測度を型位置に記述する——Positive(b)、IsMax(T, arr, result) と同じ機構（述語適用）、ゼロ新構文：

yaoxiang

// 測度：通常関数、ユニットテスト可能、再利用可能、ランタイムに参加しない
gcd_measure: (a: Int, b: Int) -> Int = { b }

// 停止コンポーネントは関数自身の型位置に配置される
gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

// ループ：バインド名がアンカー、測度は名前でスコープ内の量を取得
loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n {
        i = i + 1
    }
    return acc
}

ループでの根拠：Terminates(m) が精化するのはループ本体の末尾式の値の型であり、アンカーはバインド名 acc が提供する——これによりループが指称可能になり、「匿名構造は指称不能」という死角がなくなる。

Terminates は組み込み述語であり、Int、Never と同じくコアプリミティブの一部。これはコンパイラが関数本体を代書する唯一の述語である——そのアサーション（「各再帰呼び出し点/ループバックエッジの測度が厳密に減少する」）は計算構造の中に存在し、ユーザーが記述する述語は関数本体やループ本体を参照できないため、「構文」節の述語定義構文で表現できない。組み込み面はこの名前に収束する。

アリティ。Terminates(FnType, m) と Terminates(m) は同じ述語の二つのアリティであり、二つの構造ではない：

形態	アンカー	用途
`Terminates(m)`	所在バインディングの名前	自己再帰関数、ループ——デフォルト形態
`Terminates(FnType, m)`	明示的関数型	相互再帰などアンカーが一意でないシナリオ

両者は本質的に同一：停止義務は常に「精化が位置する型位置に注釈される計算セグメント」に落ちる。

測度は戻り型を制限しない。 測度は任意の型の式であり得る（自然数を強制しない）；その上の「厳密減少」は当該型で利用可能な整列順序によって与えられる。測度が well-founded であるか（例：Int を返すときに >= 0 であるか）は独立した義務であり、減少義務と同様に refined 推論または SMT に委ねられる；どちらも推論できない場合、診断は直接拒否せず、確認の方向性を提案する（測度の下界が成立するか、再帰パラメータが本当にその方向に進むか）。

自動探索との関係：明示的測度は別のパイプラインではなく、探索失敗後の入力である。測度を提供した後でも、同じ SMT が減少性と well-founded 性を検証するために走る；不成立ならエラーが反例とともに報告される。

義務生成、判定パイプライン、診断方向、相互再帰の測度共有（SCC）などの実装メカニズムは RFC-027a: 停止性検査の明示的測度を参照。

8. SMT ソルバー：型チェッカーのアクセラレータモジュール

SMT ソルバーは従来の言語では外部ツール（F* が Z3 を呼ぶ、Dafny が Z3 を呼ぶ）である。YaoXiang では、型チェッカーのアクセラレータモジュールである——コンパイラカーネル自体が直接判定できない場合にのみ呼び出される。SMT は証明を見つける手助けをするが、証明を検証するのは型チェッカーである。

信頼モデル：型チェッカーは唯一の信頼の根である。SMT ソルバーはアクセラレータモジュールである——証明を見つける手助けをするが、SMT は独立した信頼境界ではない。コンパイラは Z3 の unsat 結果を信頼する（F*/Dafny 路線と一致——Z3 が誤る確率はコンパイラ自身のバグ率より低く、これは工学的な実用的選択である）。真の信頼性制御は SMT 翻訳層にある——翻訳にバグがあれば、コンパイラは他のテストで露呈する。

インターフェース：コンパイラ内部は SMT-LIB 2.6 標準形式に翻訳し、特定のソルバー API に束縛しない。SMT-LIB は ISO 標準であり、Z3、CVC5、MathSAT、Yices すべてがネイティブサポートする。

デフォルトバックエンド：Z3（MIT ライセンス、最も広範なドキュメントとコミュニティ検証）。CVC5 は SMT-LIB 互換の代替として、ユーザーはコンパイル時にコンパイラフラグで切り替え可能。

「汎用ソルバー抽象層」は作らない——SMT-LIB が抽象層である。将来 CVC5 が特定理論でブレークスルーを達成した場合、バイナリを交換するだけでよく、コンパイラコードの変更は不要。

コンパイル時 Bool 式
        │
        ├── コンパイラカーネルが直接判定可能（構造的等価、単純算術、
        │   定数畳み込み後の自明な式）
        │   → 直接 Proved / Disproved を返す
        │
        └── コンパイラカーネルが直接判定不能（量化子、記号変数）
            → 依存型事前簡約（factorial(5) → 120）
            → SMT-LIB 形式に翻訳
            → Z3/CVC5 に送信（予算制限付き）
            → 戻り値：unsat → Proved  │  sat + モデル → Disproved  │  unknown → Unproven

求解予算——スタック深度のようなハードリミット：

予算次元	デフォルト値	説明
求解ステップ数	10,000	Z3 は線形算術に対して通常 100 ステップ以内。10,000 ステップで実用述語の 99% をカバー。
時間	100ms	単一述語が 100ms を超える = ユーザーがコンパイル時プログラムを書いているのではなく型注釈を書いている。100ms × 50 述語 = 5 秒のコンパイル時間上限。
量化子インスタンス化深度	3	三層ネスト量化子が実際のパターンをカバー。三層を超える場合は論理学の問題を書いている可能性が高い。

予算超過は Unproven を返し、コンパイルエラー + 述語位置 + 消費量。降格なし、ランタイムチェックなし、サイレントパスなし。

なぜこれが実用的か：工学的に実用述語の 95% は線形算術である——x > 0、arr.len > 0、0 <= idx < arr.len——すべて決定可能フラグメント内にあり、SMT ソルバーはこれらの問題に対してミリ秒単位で返す。予算を超える複雑な述詞の稀なケースでは、プログラマが証明関数を記述すればよい。

依存型は SMT 呼び出し前に事前簡約レイヤを経る：factorial(5) は直接コンパイル時評価で 120 になり、append([1,2], [3]) は直接 [1,2,3] になる。これらの決定論的値計算は SMT 予算を消費しない。

プログラマは SMT の存在を知る必要がない。メンタルモデルは：コンパイラが証明できれば通過、できなければエラー——コンパイラができない場合、関数で証明して見せることもできる。

9. コンパイル時述語の組み合わせ

コンパイル時述語は Type を返す関数であり、組み合わせは関数組み合わせによって自然に実現される：

yaoxiang

SortedNonEmpty: (T: Ord, arr: Array(T)) -> Type = {
    Sorted(T, arr) and NonEmpty(arr)
}

10. コード例

9.1 除算安全性

yaoxiang

Positive: (x: Int) -> Type = { x > 0 }

divide: (a: Int, b: Positive(b)) -> Int = a / b

result = divide(10, 2)   # ✅ コンパイラが Positive(2) = { 2 > 0 } を検証 → True
# result = divide(10, 0)  # ❌ コンパイラが Positive(0) = { 0 > 0 } を検証 → False

9.2 配列アクセス安全性

yaoxiang

InBounds: (idx: Int, arr: Array(T)) -> Type = { 0 <= idx and idx < arr.len }

get: (arr: Array(T), idx: InBounds(idx, arr)) -> T = arr.data[idx]

arr = Array(Int)(1, 2, 3)
x = get(arr, 1)   # ✅ コンパイラが InBounds(1, arr) = { 0 <= 1 and 1 < 3 } を検証 → True
# y = get(arr, 5)  # ❌ コンパイラが InBounds(5, arr) = { 0 <= 5 and 5 < 3 } を検証 → False

9.3 ソート正当性

yaoxiang

Sorted: (T: Ord, arr: Array(T)) -> Type = {
    forall i in 0..arr.len-1: arr[i] <= arr[i+1]
}

sort: (T: Ord) -> ((arr: Array(T))) -> (result: Sorted(T, result)) = {
    result = arr.clone()
    # ... ソートアルゴリズム実装 ...
    return result
}

9.4 ループ：コンパイラによる VC 生成

yaoxiang

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0
    mut i: UpTo(arr.len) = 0
    while i < arr.len {
        s += arr[i]
        i += 1
    }
    return s
}

11. dispatch 分派パイプライン：コンパイル時とランタイムの統一分派

assert と Assert は同じ refined 型プリミティブの二面である。分派パイプライン dispatch は述語の自由変数がコンパイル時にアクセス可能かに応じてコンパイル時証明とランタイムチェックを自動的に決定する：

判定基準	モード	振る舞い
すべての自由変数がコンパイル時既知（generics パラメータ、コンパイル時定数）	CompileTime	証明パイプラインへ：Proved → 消去、Disproved → コンパイルエラー、Unknown → 証明を要求
自由変数がランタイムに由来（関数パラメータ、外部入力、mut 変数）	Runtime	ランタイム check を挿入し、フロー敏感仮定集合 Γ に refined 事実を注入

重要：「判定不能」≠「反証」。CompileTime モードの Unknown は証明を要求し（静かに降格しない）、Runtime モードでは命題はコンパイル時には真偽を持たない——「ユーザーが負数を入力したかもしれない」に対する恒真証明は prover がどれほど強くても書けず、ランタイム check が唯一の sound な選択である。これは prover が十分強くないからではなく、理論的必然である。

12. フロー敏感仮定集合 Γ：最強後置条件伝播

コンパイラはフロー敏感（flow-sensitive）仮定集合 Γ を保守し、各制御フロー点で成立が知られている命題を追跡する。

SP（最強後置条件）伝播：

yaoxiang

assert(x > 0)       // Γ = {x > 0}
y = x + 1           // Γ = {x > 0, y > 1}  ← SP 伝播

mut 変数の kill set：mut 変数が再代入された後、当該変数に関するすべての仮定が Γ から削除される：

yaoxiang

assert(x > 0)       // Γ = {x > 0}
mut x = x - 5       // Γ = {}  ← x > 0 が kill される

これは soundness のハード要求である——変数の値が変われば、旧仮定は無効になる。

分岐合流：IF/ELSE または match 分岐が合流するとき、Γ は各分岐の仮定の交差集合を取る。すべてのパスで成立する命題のみが分岐外に伝播する。

13. 消去モデル明確化：witness 消去 ≠ check 消去

RFC-027 の「refined 型はランタイムで完全に消去される」という主張は proof witness（証明トークン）を指している——コンパイル時に検証済みの証明項はランタイムコードを生成しない。しかし Runtime モードで dispatch が挿入するランタイム check は保持される——これは値レイヤで実行される Bool チェックであり、型レイヤの witness ではない。

要約：witness 消去、check 保持。二つの事は矛盾せず、RFC-027 の元の主張は変わらない。

詳細設計

構文変更

以前 (RFC-022)	以降 (本 RFC)
`//! requires: NonEmpty(n) = n > 0`	コンパイル時述語をパラメータ型として `(b: Positive(b))`
`//! ensures: ExistsMax(result, arr)`	戻り型に戻り値仮パラメータを使用 `-> (result: IsMax(T, arr, result))`
`/! invariant: ... !/`	変数上のコンパイル時述語型注釈——Floyd-Hoare 不変条件
`//! decreases: n`	測度を refined 型位置に記述（`Terminates`）；コンパイラがまず自動探索、探索失敗時のみ明示提供を要求
仕様はコメント	仕様は型システム

構文

コンパイル時述語に新しいキーワードはない。 {} は証明空間であり、既存の型定義構文と完全に一致する。コンパイル時述語は Type を返す関数そのものである——name: (params) -> Type = { アサーション }。使用時は関数呼び出しそのものである——Positive(b)、IsMax(T, arr, result)。

bnf

# コンパイル時述語 = Type を返す関数、{} 内はコンパイラが検証するアサーション
# 既存関数/型構文を使用し、新しい BNF 規則は不要
predicate ::= identifier ':' params '->' 'Type' '=' '{' assertions '}'

述語適用の実引数はコンパイル時定数形式でなければならない——リテラル、変数（名前による束縛）、型適用（再帰的抽出）、またはコンパイル時指称可能な関数参照（関数名）。実引数形式が定数式に変換できない場合は E1092 を報告し、実引数の個数が述語宣言の仮パラメータ個数と一致しない場合は E1093 を報告する。実引数は位置で仮パラメータリストに束縛され、述語のアリティは宣言によって決定される——Positive(x) は 1 項、IsMax(T, arr, result) は 3 項、Terminates(m) と Terminates(FnType, m) は 1 項と 2 項——refined 制約は決して静かに破棄されない（以前、変換不能な実引数が制約を無音で消失させ、制約違反のバインディングが静かに通過していた）。

新しい構文概念：戻り値仮パラメータ——-> (name: Type) の name は戻り値仮パラメータ。

戻り値仮パラメータは YaoXiang が既存関数構文に導入する唯一の構文概念。その意味論：

name の値は return 文で提供される
name は型シグネチャ内にのみ存在し、後置条件述語によって参照される（例：-> (result: IsMax(T, arr, result))）
name は関数本体のスコープに入らず、呼び出し側にも現れない
戻り値仮パラメータはオプション——後置条件がない場合、シグネチャは通常関数と完全に一致し（-> Int）、追加負担を導入しない

導入の根拠：後置条件は「関数が返そうとしている値」を参照する必要がある。戻り値仮パラメータがない場合、コンパイラは述語が戻り値を参照できるように、特殊なルール（暗黙変数 $result や __retval__ など）を通すしかない。戻り値仮パラメータはこの参照を明示化する——それは一つの仮パラメータであり、値が呼び出し側ではなく return から提供される点が異なるだけである。

証明関数は新しい概念ではない——それは一つの YaoXiang 関数であり、その戻り型がアサートされる命題である。コンパイラが Unproven を返したとき、プログラマは証明関数を提供し、型チェッカーは任意の関数の戻り型を検証するのとまったく同じ方法でそれを検証する。新しい構文、新しいキーワード、新しいルールは不要。

二つの領域の境界。 正当性領域（述語 Unproven）は本体で証明を補う：戻り型が証明すべき命題である関数を記述する。停止性領域（§6.9）は型位置で測度を補う：Terminates(測度) をバインディングまたは関数シグネチャの型として記述する。前者は「証明できない命題は証明を記述する」であり、後者は「探索できない測度は明示的に宣言する」——機構は同じ（いずれも refined 型適用）であり、配置が異なる。停止性領域は _proof 関数の記述を必要としない。

型システムへの影響

型宇宙：コンパイル時述語は Type₂ 層に位置する——値を受け取り Type を返す関数は、型コンストラクタと同じ階層
generics との相互作用：コンパイル時述語は generics パラメータを持てる、例：NonEmpty: (T: Type) -> (arr: Array(T)) -> Type
所有権との相互作用：コンパイル時述語内の式は所有権ルールに従い、読み取りのみ可能、書き込み不可
型推論：コンパイル時述語のパラメータは HM 型推論に参加する

ランタイム表現

コンパイル時述語はランタイムでdispatch 分派結果に従って処理される：

CompileTime モード（すべての自由変数がコンパイル時既知）：証明が通過した後、witness トークンは完全に消去される。Positive: (x: Int) -> Type = { x > 0 }——パラメータ b: Positive(5) のランタイム表現は Int である。refined 条件 { 5 > 0 } は通過済み、消去される。
Runtime モード（ランタイム自由変数が存在）：ランタイム check を保持——値レイヤで Bool チェックを実行し、フロー敏感仮定集合 Γ に注入。詳細は §11 dispatch 分派パイプラインと §13 消去モデル明確化を参照。

コンパイル時述語を型の位置に配置する（例：f(x: Positive(x))）ことはラッパー型を生成せず、追加メモリを割り当てない。ただし x がランタイム入力に由来する場合、ランタイム Bool チェックが挿入される。

ref との相互作用制約：コンパイル時述語は不変借用または所有権が既に移動した値のみを参照できる。可変借用を参照するコンパイル時述語は、コンパイラがコンパイル時の検証結果がランタイムでも成立することを保証できない——このような使用法は直接コンパイルエラーを報告する。

コンパイラの変更

パーサ：コンパイル時述語は標準関数構文を使用し、追加解析ルール不要
コンパイル時証明パイプライン：Proved/Disproved/Unproven 戻りインターフェースを統一、自動戦略選択
SMT アクセラレーションモジュール：SMT-LIB 2.6 翻訳層、デフォルトバックエンド Z3、CVC5 は代替
型チェッカーカーネル：推論規則の実装——構造的等価、βδι-簡約、全称量化子の導入/除去。これが唯一の信頼の根であり、SMT とプログラマの証明はどちらもこれを介して検証される
検証条件生成：WP/SP 計算 + ループ不変条件証明義務
エラー報告：反例フォーマット化 + 未解決命題レポート + ソース位置関連付け

後方互換性

✅ コンパイル時述語を使用しないコードは完全に不変
✅ コンパイル時述語は CompileTime モードでランタイムコストゼロ、Runtime モードでは必要な Bool チェックのみ保持
⚠️ RFC-022 の //! 構文はサポートされない——ただし 022 は一度も実装されておらず、移行負担なし

トレードオフ

利点

Curry-Howard 同型の完全実現：型は命題、プログラムは証明、name: Proposition = Proof
統一性：コンパイル時述語と通常関数は完全に同じ構文を使用し、概念分裂なし
SMT 透明性：プログラマは SMT の存在を知る必要がなく、メンタルモデルは型検査と一致
段階的採用：一つのコンパイル時述語から開始し、徐々にカバレッジを拡大可能
最小ランタイムオーバーヘッド：CompileTime モードはゼロコスト、Runtime モードは必要な Bool チェックのみ保持

欠点

コンパイル時間：SMT 求解がコンパイル時間を増加させるが、予算ハード制限により上限は制御可能
自動証明の境界：一階線形算術を超える複雑な述語はプログラマの証明関数を必要とする可能性がある。これは言語の欠陥ではなく、停止問題の必然的帰結である。コンパイラは True/False を偽って報告するのではなく、Unproven を正直に報告する
学習曲線：効果的なコンパイル時述語と証明関数の記述には Curry-Howard 同型の基本直感の理解が必要
実装複雑性：コンパイル時証明パイプラインの統一は慎重な設計が必要

リスク緩和

SMT 求解予算のハード制限（ステップ数 10,000 / 時間 100ms / インスタンス化深度 3）、予算超過は Unproven を返す
依存型事前簡約：決定論的な値計算が先に消費され、SMT は非決定的部分のみを処理
Unproven は行き止まりではない：正当性領域では証明関数を記述（戻り型が命題）、停止性領域では型位置に測度を提供（§6.9）——どちらも型チェッカーによって検証される
増分検証：変更モジュールのみを検証
明確なエラーメッセージ + 反例表示 + 予算消費レポート + 未解決命題 + 提案（可能な場合）

代替案

案	選択しない理由
RFC-022：`//!` コメント式仕様	仕様と型が分裂、Curry-Howard 同型に違反
独立仕様ファイル（例：CVL）	仕様とコードが分離、保守コスト増
ランタイムアサーションのみ	静的に正当性を保証できない
外部証明アシスタント（例：Coq）	コンパイラから分離、独立した証明言語と信頼境界が必要。YaoXiang の選択：証明は YaoXiang コード、型チェッカーが唯一の信頼の根
本案：コンパイル時述語を第一級市民として	✅

実装戦略

フェーズ区分

フェーズ	内容
フェーズ 1	コンパイラカーネル：構造的等価 + βδι-簡約 + 全称量化子の導入/除去。単純算術述語（`x > 0`、`arr.len > 0`）をサポート
フェーズ 2	SMT-LIB 翻訳層 + Z3/CVC5 統合。パイプラインは Proved/Disproved/Unproven を返す。Unproven 時にプログラマの証明関数をサポート
フェーズ 3	ループ不変条件 VC 生成 + 停止性検査（測度探索四戦略 + `Terminates` 明示的測度、§6、§6.9）
フェーズ 4	増分検証 + キャッシュ + IDE サポート

依存関係

RFC-010: 統一型構文 — コンパイル時述語は name: type = value に基づく
RFC-011: generics システム — コンパイル時述語は generics パラメータを持てる
RFC-009: ownership モデル — コンパイル時述語内の式は所有権ルールに従う

オープン問題

[x] SMT ソルバーの選択：デフォルト Z3（MIT ライセンス、最も広範に検証済み）。CVC5 は SMT-LIB 互換の代替としてコンパイラフラグで切り替え。コンパイラ内部は SMT-LIB 2.6 標準形式に翻訳——SMT-LIB が抽象層であり、カスタム汎用ソルバーインターフェースは作らない。
[x] 求解予算の具体値：ステップ数 10,000 / 時間 100ms / 量化子インスタンス化深度 3。コンパイラ内部で固定、ノブは提供しない。実際の使用で本物のユースケースが証明不十分と示す場合（「ユーザーが書き間違えた」ではなく）、調整する。
[x] 量化子のサポート範囲：言語レベルでは量化子の階数を制限しない。コンパイル時述語は Type パラメータを受け入れる——Type は関数型を含む——したがって高階量化子は型システムの自然な帰結であり、特殊構文は不要。SMT ソルバーは一階量化子を自動判定できる（forall/exists、交差ネストをサポート、予算深度 3 による制限）。高階量化子：SMT は Unproven を返し、コンパイラは「この述語は自動証明範囲外です、証明関数を提供してください」と促す。プログラマは戻り型がその命題に等しい YaoXiang 関数を記述する——型チェッカーがその関数を検証する。外部エクスポート不要、AI 不要、対話的証明モード不要。すべてが YaoXiang コード、すべてが型チェッカーによって検証される。
[x] 反例フォーマット化：ソース変数名を直接 SMT 変数名として使用（モジュールプレフィックス付きで衝突回避）。Z3 モデルが返されたとき、変数名で逆引き。出力フォーマット：変数名 = 具体値 + ソース位置 + 述語定義位置。複雑なマッピング層は作らない。
[x] ~~ref スマートポインタとのコンパイル時述語の相互作用？~~ → 決定済み：コンパイル時述語は不変借用または既に所有権が移動した値のみを許可する。可変借用される値はコンパイル時述語に現れない。
[x] forall 述語違反カウント測度の非隣接操作への拡張？ → 拡張しない。現在のカバー範囲（隣接交換、隣接移動）は戦略 1（線形ランク関数）で補完的にカバーされる——クイックソートの外層区間収縮は戦略 1 がフォールバック、ヒープソートは戦略 1（配列インデックスパターン）がフォールバック。どの戦略でも停止性を証明できないループは、コンパイラが直接エラーを報告する——これはハードセーフティ哲学であり、欠陥ではない。未来に本物のシナリオ（学術的構成ではなく）のアルゴリズムが四つの戦略すべてでカバーできない場合、再検討する。→ 再検討がトリガされた（2026-09-14、#318）：非構造的再帰（gcd 類の非直接減少、相互再帰、マージ分割）は本条項が予期した本物のシナリオである——測度探索のテンプレート列はこれらを自動的に取得できず、可読性を損なうことなく分析可能な反復パターンに書き換えることもできない。結論：ハードセーフティ哲学は不変（測度の記述が誤っていれば SMT の反例で差し戻され、人は証明できないだけで、誤った証明はできない）が、「探索失敗は即拒否」は「探索失敗はプログラマが型位置に明示的に測度を提供できる」に緩和される——§6.9 を参照。
[x] 線形ランク関数の列挙組み合わせ爆発：候補列挙上限は 3 つの有界変数。≤3 の場合、すべての線形結合を列挙し SMT で逐一検証。>3 の場合、単一変数測度（v_i、u_i - v_i）のみを試行し、失敗すれば直接コンパイルエラーを報告——「ループが 3 つを超える有界変数を持ち、コンパイラが多変数測度を自動合成できない」とプログラマに通知する。これは工学的妥協ではなく、プログラマによりシンプルなループを書くことを強制する。

参考文献

RFC-010: 統一型構文
RFC-011: generics システム設計
RFC-009: ownership モデル
Howard, W. A. (1969). The Formulae-as-Types Notion of Construction.
Swamy, N. et al. (2016). Dependent Types and Multi-Monadic Effects in F*. POPL 2016.
Vazou, N. et al. (2014). Refinement Types for Haskell. ICFP 2014.
Leino, K. R. M. (2010). Dafny: An Automatic Program Verifier for Functional Correctness. LPAR 2010.
De Moura, L. & Bjørner, N. (2008). Z3: An Efficient SMT Solver. TACAS 2008.

ライフサイクルと帰結

┌─────────────┐
│   ドラフト   │  ← 著者作成
└──────┬──────┘
       │
       ▼
┌─────────────┐
│  レビュー中  │  ← 現在の状態：コミュニティ議論
└──────┬──────┘
       │
       ├──────────────────┐
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│   承認済み   │    │   拒否済み   │
└──────┬──────┘    └──────┬──────┘
       │                  │
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│ accepted/   │    │  rejected/  │
│ (正式設計)  │    │ (元の位置)   │
└─────────────┘    └─────────────┘

RFC-027: コンパイル時述語と統一静的検証 ​

要約 ​

動機 ​

なぜ RFC-022 を廃止するのか？ ​

現状の問題 ​

正しいメンタルモデル ​

提案 ​

1. {} は証明空間：型はアサーション、検証は型検査 ​

2. 前置/後置条件：パラメータ型と戻り型上のコンパイル時述語 ​

3. パス条件伝播：ランタイム値のコンパイル時検証 ​

3.1 明示的関数呼び出し ​

3.2 パス条件収集 ​

3.3 仮定スタック ​

3.4 静的証拠なしならコンパイルエラー ​

3.5 統一パイプラインとの関係 ​

4. コンパイル時証明パイプライン ​

4.1 証明結果：三値代数 ​

4.2 Unproven の後：プログラマが証明を記述する ​

4.3 パイプライン内の階層的依存 ​

5. 三層関数の統一 ​

6. ループ：Floyd-Hoare 検証条件生成 ​

6.1 依存追跡：可変変数上の依存型 ​

7. 停止性検査 ​

6.1 設計原則 ​

6.2 戦略 1：線形ランク関数の自動合成 ​

6.3 戦略 2：述語違反カウント——目標型から自動的に測度を抽出 【実験的戦略】 ​

6.4 戦略 3：有界増減パターン ​

6.5 戦略 4：乗法スケール測度テンプレート ​

6.6 停止性と正当性の分離 ​

6.7 再帰関数の停止性検査 ​

6.8 ハード境界 ​

6.9 明示的測度：Terminates ​

8. SMT ソルバー：型チェッカーのアクセラレータモジュール ​

9. コンパイル時述語の組み合わせ ​

10. コード例 ​

9.1 除算安全性 ​

9.2 配列アクセス安全性 ​

9.3 ソート正当性 ​

9.4 ループ：コンパイラによる VC 生成 ​

11. dispatch 分派パイプライン：コンパイル時とランタイムの統一分派 ​

12. フロー敏感仮定集合 Γ：最強後置条件伝播 ​

13. 消去モデル明確化：witness 消去 ≠ check 消去 ​

詳細設計 ​

構文変更 ​

構文 ​

型システムへの影響 ​

ランタイム表現 ​

コンパイラの変更 ​

後方互換性 ​

トレードオフ ​

利点 ​

欠点 ​

リスク緩和 ​

代替案 ​

実装戦略 ​

フェーズ区分 ​

依存関係 ​

オープン問題 ​

参考文献 ​

ライフサイクルと帰結 ​

RFC-027: コンパイル時述語と統一静的検証

要約

動機

なぜ RFC-022 を廃止するのか？

現状の問題

正しいメンタルモデル

提案

1. `{}` は証明空間：型はアサーション、検証は型検査

2. 前置/後置条件：パラメータ型と戻り型上のコンパイル時述語

3. パス条件伝播：ランタイム値のコンパイル時検証

3.1 明示的関数呼び出し

3.2 パス条件収集

3.3 仮定スタック

3.4 静的証拠なしならコンパイルエラー

3.5 統一パイプラインとの関係

4. コンパイル時証明パイプライン

4.1 証明結果：三値代数

4.2 Unproven の後：プログラマが証明を記述する

4.3 パイプライン内の階層的依存

5. 三層関数の統一

6. ループ：Floyd-Hoare 検証条件生成

6.1 依存追跡：可変変数上の依存型

7. 停止性検査

6.1 設計原則

6.2 戦略 1：線形ランク関数の自動合成

6.3 戦略 2：述語違反カウント——目標型から自動的に測度を抽出【実験的戦略】

6.4 戦略 3：有界増減パターン

6.5 戦略 4：乗法スケール測度テンプレート

6.6 停止性と正当性の分離

6.7 再帰関数の停止性検査

6.8 ハード境界

6.9 明示的測度：`Terminates`

8. SMT ソルバー：型チェッカーのアクセラレータモジュール

9. コンパイル時述語の組み合わせ

10. コード例

9.1 除算安全性

9.2 配列アクセス安全性

9.3 ソート正当性

9.4 ループ：コンパイラによる VC 生成

11. dispatch 分派パイプライン：コンパイル時とランタイムの統一分派

12. フロー敏感仮定集合 Γ：最強後置条件伝播

13. 消去モデル明確化：witness 消去 ≠ check 消去

詳細設計

構文変更

構文

型システムへの影響

ランタイム表現

コンパイラの変更

後方互換性

トレードオフ

利点

欠点

リスク緩和

代替案

実装戦略

フェーズ区分

依存関係

オープン問題

参考文献

ライフサイクルと帰結