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

参考:
RFC-009: 所有権モデル
RFC-010: 統一型構文 - name: type = value モデル
RFC-011: ジェネリック型システム設計
RFC-024：spawnブロックに基づく並行モデル
取代：RFC-022: ホア論理静的検証サポート（仕様コメントと仕様型） — 廃止済み

摘要

本文提出为 YaoXiang 引入コンパイル時述語作为一等市民，将所有コンパイル時静的検証统一为一条証明パイプライン。コンパイル時述語不是外挂の仕様コメント——它就是関数。返回 Type の関数，可在类型位置使用，编译器在编译期调用它并检查返回值。类型即命题，编译期求值即证明。

核心论点：型チェック在编译期的唯一工作是构造和验证证明项。型等式、トークン衝突、依存型簡約、コンパイル時述語評価、ホア論理含意——全部はコンパイル時証明パイプライン中の不同类型检查，共享同一条管道。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 同型の根本的錯誤を犯した：仕様と型を二层に分離した。コメントは型ではない。コメントは型チェックに参加しない。コメントは「外部ツール」のmental modelである。

白書には明確に述べられている：

"//! コメントはない。独立した仕様言語はない。すべては型システム内で 이루어われる。"

現在の問題

RFC-022 の //! コメントは型システムから独立した外挂構文
仕様型と普通型是两套体系，造成概念冗余
Debug Build 検証 / Release Build 忽略の分裂モード破坏了统一性
SMT 求解器在传统认知中被定位为外部工具——YaoXiang 将其作为型チェック器の加速モジュール内置
型チェック、借用にがり検証、コンパイル時述語検査、マクロ展開各自走不同的路径

正しい Mental Model

型チェック可以抽象为一个関数：

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)

ジェネリックはコンパイル時述語の特例である。

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. 経路条件伝播：実行時値のコンパイル時検証

コンパイル時述語がバインディング位置で使用されるとき、パラメータは程序员が明示的に渡す。実行時値が精製型パラメータに入ると、编译器通过経路条件収集和 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-guard：if y > 0 → true 分支に y > 0 を压入、false 分支に !(y > 0) を压入（else を使用した場合）
match パターン：if let Some(v) = opt → 分支内に opt == Some(v) を压入
論理結合：if x > 0 && y < 10 → 分支内に x > 0 と y < 10 を压入
関数前置条件：调用 divide(a, b) 时、b 必须满足 Positive の証拠要么来自当前仮定，要么来自実引数自身の精製型注釈（b が既に Positive 注釈付きならその型携带 b > 0）
代入：let z = y 时、y 上已有的精製条件传递到 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（不含意）→ コンパイルエラー：

无法证明参数 b 在 divide 调用中满足 Positive。 y 来自函数输入，无已证明的界。考虑用 if 分支守卫调用：if y > 0 { divide(x, y) }。

YaoXiang 不接受実行時値直接进入精製型パラメータ而不提供静态証拠。这不是限制——这是硬安全哲学の核心。凡编译器无法静态证明的代码，不得通过编译。

3.5 与统一パイプラインの関係

経路条件伝播不是额外的メカニズム。它はコンパイル時証明パイプライン在控制流分析上的直接延伸：

段階	职责
経路条件収集	编译器控制流分析段階、为每个基本ブロック标注仮定セット
検証条件生成	遇到需検証的类型约束时、合并経路条件 + 实引数类型情報
証明パイプライン評価	编译器内核 → SMT 加速 → 得出 Proved / Disproved / Unproven
結果	`Proved` → 通過；`Disproved` → コンパイルエラー + 反例；`Unproven` → コンパイルエラー + 未解決命题（程序员可提供証明関数）

没有新部件。没有特殊規則。経路条件就是証明パイプラインの背景知識——和类型等式、借用的约束共享同一条パイプライン、同一套予算システム。

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

すべてのコンパイル時検査共享同一条パイプライン。パイプラインの核心操作は类型检查——检查一个証明项の类型是否等于待证明の命题。一切皆类型检查。

编译期遇到 Bool 表达式需要求值（即：需要构造一个証明项）
        │
        ├── 类型等式（T1 == T2）
        │   → 编译器直接判定（结构等价）
        │
        ├── 令牌冲突条件（!conflicting(tokens)）
        │   → 流敏感活性分析（Dup/Linear 属性追踪）
        │
        ├── 依存型簡約（n + m 簡約）
        │   → 编译期项重写システム（βδι-簡約）
        │
        ├── コンパイル時述語（x > 0, forall...）
        │   → 编译器自身 + SMT 加速モジュール
        │
        └── ホア論理含意式（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。 编译器说「我证明不了」不等价于命题为假——只是超出了当前自动証明的能力。这是正直，不是缺陷。

予算硬限制は停机问题的工程解。不给 knob——给了就是在问用户「你觉得你的程序会不会停机」、用户不知道、编译器也不知道。

4.2 Unproven 之後：程序员写証明

当编译器返回 Unproven 时、程序员可以写一个証明関数——就是一个 YaoXiang 函数、其返回类型等于待证明の命题。类型检查器验证这个関数——和它验证 add(a, b): Int 是同一个メカニズム。

命题  = 类型
証明  = プログラム（该类型的一个値）
検証  = 类型检查（唯一的信任根）

SMT 求解器不是独立的信任边界——它是类型检查器の加速モジュール。SMT 帮忙找証明、但验证証明的始终是类型检查器。SMT 返回 unsat 时、编译器将其结果重构为类型检查器可验证の証明项。如果重构失败（SMT の推理步骤超出编译器内核の推理规则）、则回退到 Unproven——程序员可以手动写証明関数。

yaoxiang

# 命题：编译器无法自动証明の精製属性
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 パイプライン内の階層依存

以上の評価器共享同一接口但存在評価順序。类型等式是所有后续分析の的前提条件；所有权/令牌检查依赖类型信息；精製述語検証依赖前两层の結果。编译器按层評価、底层失败の表达式不进上层——避免在类型错误の程序上浪费求解予算。

評価順序（同一パイプライン、階層スケジューリング）
├── 第 0 層：类型等式（T1 == T2）
│   └── 结构合一 → 失敗则后续无意义、直接返回 Disproved
├── 第 1 層：所有权/令牌冲突
│   └── 流敏感活性分析 → 失敗则内存安全不成立、直接返回 Disproved
└── 第 2 層：精製述語/ホア含意
    └── 编译器自身 → 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. 终止检查

コンパイル時全自动。编译器能証明のループ通过，不能証明的直接报编译エラー——程序员必须让编译器能自动分析循环の终止性。不给半自动注釈留口子。

6.1 設計原則

编译器从两处自动提取终止証明所需の情報：

変数型注釈：精製型中の境界制約（如 UpTo(n) 给出上界 n 和下界 0）
ループ体操作：每次迭代对变量施加の操作

编译器按优先级尝试四种測度合成戦略、找到一个即停止。

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：述語違反计数——从目标型自动提取測度【実験的戦略】

⚠️ 現在状態：実験的戦略、段階 3 実装時に実際の可行性に応じて含めるかを決定する。 此戦略对相邻交換操作（バブルソート、挿入ソート）有效、对非相邻操作（クイックソート partition、ヒープソート sift-down）无法自动証明。覆盖境界见下表。如段階 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 每次交換严格递减
挿入ソート	相邻移动	✅	每次移位消除一个违反对
选择ソート	非相邻交換	❌	单次交換可能增加 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.7 再帰関数の终止检查

对需要在编译期求値の再帰関数、编译器检查パラメータ递减：

yaoxiang

factorial: (n: Int) -> Int = {
    if n <= 1 { return 1 }
    return n * factorial(n - 1)  # 编译器分析：n-1 < n → 递减 → 终止
}

# 编译期使用——编译器保证 factorial 在编译期终止
vec: Vec(factorial(5)) = Vec(120)()  # 5! = 120，编译期完成

シナリオ	動作
编译器能分析出再帰递减（如 `n-1`）	编译期求値
不递减/无法判定递减	编译エラー
実行時呼び出し（非类型位置）	不需要终止检查

6.8 硬边界

i = f(i) 且 f 不可逆、不封闭、不保持任何单调性——数学上不可能自动証明终止。编译エラー：

此循环无法自动証明终止。循环变量依赖于不可分析の関数 f。请使用可被编译器分析の迭代パターン。

这不是编译器の失敗。凡无法静态証明安全の代码、不得通过编译。

8. SMT 求解器：类型检查器の加速モジュール

SMT 求解器在传统语言中是外部ツール（如 F* 调用 Z3、Dafny 调用 Z3）。在 YaoXiang 中，它是类型检查器の一个加速モジュール——仅当编译器内核自身无法直接判定时才被调用。SMT 帮忙找証明、但验证証明的是类型检查器。

信任モデル：类型检查器是唯一的信任根。SMT 求解器是加速モジュール——它帮忙找証明、但 SMT 不是独立的信任边界。编译器信任 Z3 の unsat 结果（与 F*/Dafny 路线一致——Z3 出错の概率低于编译器自身の bug 率、是工程上の务实选择）。真正的不可靠性控制在 SMT 翻訳層——如果翻訳有 bug、编译器会在其他测试中暴露。

接口：编译器内部翻訳为 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 对線形算術通常在百步以内。10,000 步覆盖 99% の实际述語。
时间	100ms	单述语超过 100ms = 用户在写编译期程序而非类型注釈。100ms × 50 个述语 = 5 秒编译时间上限。
量词实例化深度	3	三层嵌套量词覆盖实际パターン。超过三层大概率在写論理练习题。

超予算返回 Unproven、编译エラー + 述语位置 + 消费量。没有降级、没有実行時检查、没有 silent pass。

为什么这实际可行：工程中 95% の实际述语是線形算術——x > 0、arr.len > 0、0 <= idx < arr.len——全在可判定片段内、SMT 求解器对这类问题ミリ秒级返回。遇到极少数超予算の复杂述语、程序员写証明関数即可。

依存型在 SMT 调用前做了一层预簡約：factorial(5) 直接编译期求值得 120、append([1,2], [3]) 直接求值得 [1,2,3]。这些确定性の値計算不消耗 SMT 予算。

程序员不需要知道 SMT の存在。Mental modelは：编译器能証明就通过、不能就报错——如果编译器不会，你可以写个関数証明给它看。

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

コンパイル時述語は Type を返す関数、組み合わせは関数組み合わせ自然实现：

yaoxiang

SortedNonEmpty: (T: Ord, arr: Array(T)) -> Type = {
    Sorted(T, arr) && 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 && 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 && 1 < 3 } → True
# y = get(arr, 5)  # ❌ 编译器検証 InBounds(5, arr) = { 0 <= 5 && 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 は同一个精製型原语の両面である。分派パイプライン dispatch は述語の自由变量在编译期是否可及により自动决定走编译期証明还是実行時检查：

判据	モード	動作
所有自由变量编译期已知（ジェネリックパラメータ、编译期常量）	CompileTime	进証明パイプライン：Proved → 擦除、Disproved → 编译エラー、Unknown → 要求証明
存在自由变量来自実行時（函数パラメータ、外部入力、mut 变量）	Runtime	插入実行時 check，并向流敏感仮定セット Γ に注入精製事实

重要：「判不了」≠「証伪」。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 の「精製型在実行時完全擦除」论断指的是 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`	编译器全自动推导測度関数
仕様はコメント	仕様は型システム

構文

コンパイル時述語没有新关键字。 {} は証明空間、和现有类型定义構文完全一致。コンパイル時述語就是返回 Type の関数——name: (params) -> Type = { 表明 }。使用时就是関数呼び出し——Positive(b)、IsMax(T, arr, result)。

bnf

# コンパイル時述語 = 返回 Type の関数、{} 内为编译器検証の表明
# 使用现有関数/类型構文、无需新增 BNF 規則
predicate ::= identifier ':' params '->' 'Type' '=' '{' assertions '}'

新增構文概念：返回值パラメータ——-> (name: Type) 中 name は返回值パラメータ。

返回值パラメータは YaoXiang 在现有関数構文上引入の唯一一个構文概念。它的语义：

name の値由 return 文から提供される
name 仅存在于型シグネチャ中、被後置条件述語参照（如 -> (result: IsMax(T, arr, result))）
name 不进入関数体スコープ、不出现在呼び出し方
返回値パラメータ任意——无後置条件时签名与普通関数完全一致（-> Int）、不引入任何额外负担

引入它的理由：後置条件需要参照「関数将要返回の値」。在没有返回值パラメータ的情况下、编译器只能通过特殊規則（如暗黙変数 $result 或 __retval__）来让述語参照返回值。返回值パラメータ将这种参照显式化——它就是一个パラメータ、只是値由 return 而非呼び出し方から提供される。

証明関数不是新概念——它就是一个 YaoXiang 関数、其返回类型是被表明の命题。当编译器返回 Unproven 时、程序员提供証明関数、类型检查器以与验证任何関数返回类型完全相同的方式验证它。不需要新構文、新关键字、新規則。

型システム影響

型宇宙：コンパイル時述語位于 Type₂ 層——接受値返回 Type の関数、与类型コンストラクタ层级相同
ジェネリック相互作用：コンパイル時述語可带ジェネリックパラメータ、如 NonEmpty: (T: Type) -> (arr: Array(T)) -> Type
所有権相互作用：コンパイル時述語中の表达式遵守所有権規則、只能读不能写
型推导：コンパイル時述語のパラメータ参与 HM 型推导

実行時表現

コンパイル時述語在実行時按 dispatch 分派結果处理：

CompileTime モード（所有自由变量编译期已知）：証明通过後见证トークン（witness）完全擦除。Positive: (x: Int) -> Type = { x > 0 }——パラメータ b: Positive(5) 在実行時の表现就是 Int。精製条件 { 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 の存在、mental model 与类型检查一致
渐进式采用：可从一个コンパイル時述語开始、逐步增加覆盖
最小実行時开销：CompileTime モード零开销、Runtime モード仅保留必要の Bool 检查

缺点

编译时间：SMT 求解增加编译时间、但予算硬限制保证上限可控
自动証明边界：超越一階線形算術の复杂述语可能需要程序员写証明関数。这不是语言缺陷——这是停机问题的必然结论。编译器正直报告 Unproven 而非伪报 True/False
学習曲线：编写有效のコンパイル時述語和証明関数需要理解 Curry-Howard 同型の基本直觉
実装复杂度：コンパイル時証明パイプラインの统一需要精心設計

リスク缓解

SMT 求解予算硬限制（步数 10,000 / 时间 100ms / 实例化深度 3）、超予算返回 Unproven
依存型预簡約：确定性の値計算先吃掉、SMT 只啃非确定部分
Unproven 不是死路：程序员可以写証明関数、类型检查器验证——和验证任何関数返回类型一致
增量検証：仅検証変更モジュール
清晰の錯誤信息 + 反例展示 + 予算消費レポート + 未解決命题 + 提案（如果编译器能给出）

替代方案

方案	为什么不选择
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 生成 + 终止检查（線形ランク関数 + 述語違反计数 + 有界パターン + 组合爆発控制）
段階 4	增量検証 + 缓存 + IDE 支持

依存関係

RFC-010: 统一型構文 — コンパイル時述語基于 name: type = value
RFC-011: ジェネリック型システム — コンパイル時述語可带ジェネリックパラメータ
RFC-009: 所有権モデル — コンパイル時述語表达式遵守所有権規則

開放問題

[x] SMT 求解器選択：默认 Z3（MIT プロトコル、最广泛検証）。CVC5 作为 SMT-LIB 兼容备选、编译器标志切换。编译器内部翻訳目标为 SMT-LIB 2.6 标准格式——SMT-LIB 就是抽象層、不做自定义通用求解器接口。
[x] 求解予算の具体数値：步数 10,000 / 时间 100ms / 量词实例化深度 3。编译器内部固定、不给 knob。实际使用中如有真实用例证明不够（非「用户写错了」）、再调整。
[x] 量词支持範囲：语言层面不限制量词阶数。コンパイル時述語接受 Type 参数——Type 包括関数类型——因此高階量词是型システムの自然推论、不需要特殊構文。SMT 求解器可自动判定一階量词（forall/exists、支持交错嵌套、由予算深度 3 限制）。高階量词：SMT 返回 Unproven、编译器提示「此述语超出自动証明範囲、请提供証明関数」。程序员写一个返回类型等于该命题の YaoXiang 関数——类型检查器验证该関数。不需要外部导出、不需要 AI、不需要対話式証明モード。一切都是 YaoXiang 代码、一切由类型检查器验证。
[x] 反例格式化：源码变量名直接用作 SMT 变量名（加上模块前缀避免冲突）。Z3 模型返回时按变量名反查。出力格式：変数名 = 具体値 + ソースコード位置 + 述語定义位置。不做复杂映射層。
[x] ~~与 ref スマートポインタのコンパイル時述語相互作用？~~ → 已决策：コンパイル時述語只允许不可変借用或已转移所有権の値。可变借用の値不可出现在コンパイル時述語中。
[x] forall 述語違反计数測度对非相邻操作の扩展？ → 不扩展。当前覆盖範囲（相邻交換、相邻移动）由戦略 1（線形ランク関数）互补覆盖——クイックソート外層区间收缩由戦略 1 兜底、ヒープソート由戦略 1（配列インデックスパターン）兜底。不能由任何戦略証明终止のループ、编译器直接报错——这是硬安全哲学、不是缺陷。如果未来有真实场景（非学術構造）の算法四种戦略都无法覆盖、再重新讨论。
[x] 線形ランク関数枚举组合爆発：候选枚举上限为 3 个有界变量。≤3 时枚举所有線形結合并 SMT 逐一検証。>3 时只尝试单变量測度（v_i、u_i - v_i）、失敗直接报编译エラー——提示程序员「ループ有 >3 个有界变量、编译器无法自动合成多变量測度」。这不是工程妥协——是迫使程序员写更简单のループ。

参考文献

RFC-010: 统一型構文
RFC-011: ジェネリック型システム設計
RFC-009: 所有権モデル
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 を廃止するのか？ ​

現在の問題 ​

正しい Mental Model ​

提案 ​

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 硬边界 ​

8. SMT 求解器：类型检查器の加速モジュール ​

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

10. コード例 ​

9.1 除法安全 ​

9.2 配列アクセス安全 ​

9.3 ソート正確性 ​

9.4 ループ：编译器 VC 生成 ​

11. dispatch ディスパッチパイプライン：编译期と実行時の统一分派 ​

12. 流敏感仮定セット Γ ：最强後置条件伝播 ​

13. 擦除モデル澄清：witness 擦除 ≠ check 擦除 ​

詳細設計 ​

構文変化 ​

構文 ​

型システム影響 ​

実行時表現 ​

编译器改动 ​

後方互換性 ​

权衡 ​

优点 ​

缺点 ​

リスク缓解 ​

替代方案 ​

実装戦略 ​

段階划分 ​

依存関係 ​

開放問題 ​

参考文献 ​

ライフサイクルと归宿 ​

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

摘要

動機

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

現在の問題

正しい Mental Model

提案

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 硬边界

8. SMT 求解器：类型检查器の加速モジュール

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

10. コード例

9.1 除法安全

9.2 配列アクセス安全

9.3 ソート正確性

9.4 ループ：编译器 VC 生成

11. dispatch ディスパッチパイプライン：编译期と実行時の统一分派

12. 流敏感仮定セット Γ ：最强後置条件伝播

13. 擦除モデル澄清：witness 擦除 ≠ check 擦除

詳細設計

構文変化

構文

型システム影響

実行時表現

编译器改动

後方互換性

权衡

优点

缺点

リスク缓解

替代方案

実装戦略

段階划分

依存関係

開放問題

参考文献

ライフサイクルと归宿