moonbit-proof

MoonBit Proof-Carrying Code

検証済みの MoonBit コードを作成、拡張、またはデバッグするタスクでは、このスキルを使用してください。

よくある使用例：

• 実行可能な MoonBit コードに契約を追加する
• 抽象モデルまたは表現不変条件を定義する
• 再帰データ構造を検証する
• 具体的な表現を集合／マップモデルに結び付ける
• 信頼された証明ブリッジを補題に置き換える
• 証明の失敗、タイムアウト、またはフロントエンドの低レベル化に関する制限をデバッグする

目標

証明らしく見えるコメントではなく、証明を伴うコードを書いてください。

つまり：

• ランタイムコードは実行可能で読みやすいままにします
• 証明モデルを明示します
• 契約では、役割に一貫性のある名前付き述語／関数を使います
• 局所的な proof_assert の手順で、実装がモデルを満たす理由を示します

命名

値の証明側の意味的なビューのデフォルト名として、model(...) を優先してください。

例：

• model(set) : Fset[Int]
• model(map) : Fmap[Int, Int]
• model(tree) : Seq[Int]

より具体的な名前を使うことで明確さが大きく向上する場合に限り、その名前を使います：

• elements(node)。モデルが再帰サブツリーに格納された要素の集合そのものである場合
• domain(bitmap)。モデルが使用中のインデックス集合を示す場合
• height(tree)。主要な意味モデルではなく、構造的な尺度である場合

デフォルトのルール：

• 主要な意味的抽象には model を使います
• 補助的なビューには elements、domain、height、rank などの専用名を使います

デフォルトの構成

パッケージを 2 つのレイヤーに分けます。

• .mbtp
  • model(x) などのモデル関数
  • tree_inv(x) や sparse_array_inv(x) などの表現不変条件
  • insert_pre(...) や insert_post(...) などの名前付き証明述語
  • 再利用可能な補題
• .mbt
  • 実行可能なコード
  • 証明側の述語に対する契約
  • 構築、分岐、ループの後に置く局所的な proof_assert の手順

特別な理由がない限り、この構成をデフォルトとして使ってください。

推奨ワークフロー

1. まず抽象モデルを選びます。
2. 必要最小限の不変条件を定義します。
3. 名前付きの *_pre／*_post 述語を使って契約を記述します。
4. ランタイムコードを実装します。
5. 証明に関係するすべてのループにループ不変条件を追加します。
6. ソルバーの補助が必要な箇所に局所的な proof_assert を追加します。
7. 実際に VC の失敗を確認してから、ヘルパー補題を導入します。
8. コンストラクターから外側に向かって、信頼されたブリッジを縮小します。

最初に大量の補題を書き始めないでください。

ステップ 1：適切な抽象モデルを選ぶ

観測可能な動作に合った、最も単純なモデルを優先してください。

• メンバーシップだけを扱う構造：有限集合を使います。
• キーと値を扱う構造：有限マップを使います。
• 再帰的なツリー／トライ：model(node) を使います。より明確であれば、elements(node) を使います。
• パックされたレイアウト：ドメイン／レイアウトに関する事実と意味を分けます。

例：

fn model(set : HashSet) -> Fset[Int] {
  match set.root {
    None => @fset.fset_empty()
    Some(node) => model(node)
  }
}

再帰ヘルパーがサブツリーの要素集合を本当に表す場合は、次の形も適切です：

fn elements(node : Node) -> Fset[Int] {
  match node {
    Empty => @fset.fset_empty()
    Branch(l, x, r) => elements(l).union(elements(r)).add(x)
  }
}

すべての契約に意味全体を直接詰め込むことは避けてください。

ステップ 2：不変条件を小さく保つ

不変条件では主に、次のことを記述します：

• 形状
• 境界
• レイアウト
• 整形式性

意味上の等式は通常、*_inv の中ではなく、事後条件または補題に置きます。

良い例：

predicate sparse_ok(sa : SparseArray) {
  sa.data.length() == count_value(sa.bitmap, 0) &&
  (∀ i : Int,
    valid_idx(i) && mem_value(sa.bitmap, i) →
      0 <= rank_value(sa.bitmap, i, 0) &&
      rank_value(sa.bitmap, i, 0) < sa.data.length())
}

良くない例：

• あらゆる更新定理を不変条件に入れる
• 意味上の等式全体を *_inv にエンコードする

ステップ 3：名前付きの事後条件を使う

大きな数式を繰り返すのではなく、名前付き述語を優先してください。デフォルトの命名規則として、*_inv、*_pre、*_post を使います。

良い例：

predicate singleton_post(res : SparseArray, idx : Int, value : Int) {
  sparse_ok(res) &&
  model(res).eq(@fmap.fmap_empty().add(idx, value))
}

pub fn singleton(idx : Int, value : Int) -> SparseArray where {
  proof_require: valid_idx(idx),
  proof_ensure: result => singleton_post(result, idx, value),
} {
  ...
}

こうすることで契約が短くなり、ソルバーが再利用できる目標を用意できます。

ステップ 4：数学的な内容を .mbtp に記述する

証明側の内容は .mbtp に記述します。

例：

fn model(t : Tree) -> Fset[Int] {
  match t {
    Empty => @fset.fset_empty()
    Node(l, x, r, _) => model(l).union(model(r)).add(x)
  }
}

predicate avl(t : Tree) {
  match t {
    Empty => true
    Node(l, x, r, h) =>
      avl(l) &&
      avl(r) &&
      all_lt(model(l), x) &&
      all_gt(x, model(r)) &&
      h == 1 + max2(height(l), height(r))
  }
}

.mbtp は次の内容に絞ります。

• 論理定義
• 述語
• 補題

.mbtp にランタイムの実装詳細を詰め込まないようにします。

特に役立つ、よく使われるヘルパーパターンは次の 2 つです。

1. 抽象構造に対する外延的等価性の仮定。

例：

predicate fmap_eq_hyp(m1 : Fmap[Int, Int], m2 : Fmap[Int, Int]) {
  (∀ k : Int, m1.mem(k) == m2.mem(k)) &&
  (∀ k : Int, m1.mem(k) → m1.find(k) == m2.find(k))
}

lemma fmap_eq_intro(m1 : Fmap[Int, Int], m2 : Fmap[Int, Int]) where {
  proof_require: fmap_eq_hyp(m1, m2),
  proof_ensure: m1.eq(m2),
} {
}

これは、マップの精緻化の証明を完了する際に、多くの場合もっとも簡潔な方法です。

2. 更新に対する小さな移送補題。

例：

• 自身および他のキーでの mem の追加／削除
• 自身および他のキーでの find の追加／削除
• 要素の追加／削除後の基数（対象の要素が存在する場合／しない場合）

「すべてが正しく変更された」という巨大な定理を 1 つ作るより、小さな移送補題を複数使うことを優先します。

ステップ 5：.mbt でソルバーを導く

データを構築した後、ソルバーが見落とす可能性のある具体的な事実をアサートします。

例：

let data = FixedArray::make(1, value)
proof_assert data.length() == 1
proof_assert data[0] == value
let result = { bitmap, data }
proof_assert sparse_ok(result)
proof_assert singleton_post(result, idx, value)
result

proof_assert は次の箇所で使用します。

• レコードの構築後
• 配列への書き込み後
• 場合分けの後
• ループ本体でより強い関係が確立された後

呼び出し可能な、信頼済みラッパー関数を導入するより、この方法を優先します。

ステップ 6：ループ不変条件を早い段階で記述する

証明に関係するループには、ループの形が安定したらすぐに不変条件を設定します。

実際には、証明を伴う MoonBit コードでは、次のような処理にループを使うことがよくあります。

• 配列の先頭部分または末尾部分のコピー
• カウントや順位の累積
• 結果の構造の段階的な構築
• サブツリーまたはパック表現の反復処理

プローバーが失敗するまで、明らかな不変条件を記述するのを待たないでください。

よくある不変条件：

• インデックスの境界
• アキュムレーターと、これまでの抽象モデルとの関係
• 先頭部分／末尾部分のコピーに関する事実
• 変更されないフィールドの保持

例：

for j = 0, acc = 0; j < idx; {
  let next_acc = if bitmap_mem(bitmap, j) { acc + 1 } else { acc }
  proof_assert next_acc == rank_value(bitmap, j + 1, 0)
  continue j + 1, next_acc
} nobreak {
  acc
} where {
  proof_invariant: 0 <= j,
  proof_invariant: j <= idx,
  proof_invariant: acc == rank_value(bitmap, j, 0),
}

配列の更新では、証明の形に合った段階的な不変条件を使います。

例：

for i = 0; i < pos; {
  new_data[i] = old_data[i]
  continue i + 1
} where {
  proof_invariant: 0 <= i,
  proof_invariant: i <= pos,
  proof_invariant: add_prefix_ok(old_data, new_data, pos, i),
}

次に、挿入／削除した要素を処理した後で、2 つ目の不変条件を追加します。

基本ルール：

• ループが事後条件に関係する場合は、その不変条件で証明側の進捗を明示します
• ループが具体的な状態を変更するだけの場合でも、次の抽象化補題に必要な具体的な関係を不変条件で示します
• ループの最終的に返される値が意味的に重要な場合は、proof_yield を追加して、返される結果が満たす性質をプローバーに知らせます

例：

for i = 0, acc = 0; i < xs.length(); {
  continue i + 1, acc + xs[i]
} nobreak {
  acc
} where {
  proof_invariant: 0 <= i,
  proof_invariant: i <= xs.length(),
  proof_invariant: acc == prefix_sum(xs, i),
  proof_yield: res => res == prefix_sum(xs, xs.length()),
}

反復中に維持される状態だけでなく、ループ式全体が生成する値に関する事実が必要な場合は、proof_yield を使います。

ステップ 7：自然な API の形を検証する

公開 API がメソッド指向の場合は、メソッドを直接検証します。

例：

pub fn HashSet::contains(self : HashSet, key : Int) -> Bool where {
  proof_require: set_inv(self),
  proof_ensure: result => result == model(self).mem(key),
} {
  ...
}

トップレベルの検証済みヘルパー関数は、構造や再利用性を向上させる場合にのみ使用し、メソッドのコントラクトを回避するために使わないでください。

ステップ 8：再帰コードには構造に沿った証明の形を使う

再帰データ構造の場合：

• model(node) や elements(node) のような意味論的ビューを定義する
• node_ok(node, level) のような形状不変条件を定義する
• 構造に沿って再帰する
• proof_decrease を追加する

例：

fn contains_at(node : Node, key : Int, level : Int) -> Bool where {
  proof_decrease: node,
  proof_require: node_ok(node, level),
  proof_ensure: result => result == model(node).mem(key),
} {
  match node {
    Flat(k) => key == k
    Branch(children) => ...
  }
}

コントラクト付き関数内の末尾再帰ループにソルバーが対応しない場合は、まず構造的再帰のコードを試してください。

ステップ 9：パック形式またはインデックス形式の表現では、意味論的な意味を示す前に具体的な更新を証明する

表現がパック形式、インデックス形式、または段階的に再構築される場合は、低レベルの変更から最終的な意味論的定理へ直接進まないでください。

まず、実装の構造に対応する具体的な更新の事実を証明してから、それらを抽象モデルに結び付けます。

一般的な進め方は次のとおりです。

1. 基本的なドメインまたはインデックスの事実
2. 局所的な境界または位置の事実
3. 変更されない領域と変更された領域についての具体的な更新の事実
4. 完全な具体的更新述語
5. 最終的な意味論的な *_post 定理

正確な中間述語は実装によって異なります。コード内の実際の段階を反映する名前を選んでください。

典型的な段階は次のとおりです。

• 変更されない領域
• 更新された領域
• シフトまたは再構築された領域
• 完全な具体的更新述語
• 最終的な事後条件

パターンの例：

predicate update_prefix_ok(before_data, after_data, upto) { ... }
predicate update_middle_ok(before_data, after_data, pos, value, upto) { ... }
predicate update_data_ok(before, key, value, after) { ... }

lemma update_model_lemma(...) where {
  proof_require: update_data_ok(...),
  proof_ensure: update_post(...),
} {
  ...
}

スパース配列や密配列のコードでは、*_prefix_ok、*_fill_ok、*_data_ok のような、より具体的な段階付けが効果的なことがよくあります。ただし、これは一般的な手法の有用な適用例のひとつとして扱い、万能のテンプレートとは考えないでください。

ステップ 10：共有シムパッケージは小さく保つ

再利用可能な証明インポートや理論がある場合は、シムパッケージにまとめてください。

典型的な例：

• 有限集合のラッパー
• 有限マップのラッパー
• ビットマップのドメイン／ランク／カウント用ヘルパー

次のようなメリットがあります。

• クライアントパッケージに集中できます
• インポートの重複を避けられます
• 回帰テスト用の共有推論をより簡単に行えます

ただし、共有シムは最小限に保ってください。共有補題が多すぎると、無関係な証明に影響することがあります。

また、次のような低レベル化の癖も考慮してください。

• メソッドはコントラクト内で使えても、静的コンストラクターは使えない場合があります
• Fmap::mk(...) が解析できても、fmap_mk(...) のような自由関数のラッパーが依然として必要な場合があります
• こうしたラッパーは、各クライアントに重複して配置せず、シムパッケージにまとめてください

ヘルパーがひとつのパッケージでしか必要ない場合は、共有シムからエクスポートするのではなく、そのパッケージ内のローカル補題を優先してください。

ステップ 11：信頼指定は一時的なものとして扱う

信頼指定されたヘルパーは、限定的な橋渡しとしては許容できますが、設計の最終形にしてはいけません。

信頼指定が避けられない場合：

• 事前条件は具体的に保ちます
• 名前を付けたひとつの述語を対象にします
• 数学的な記述は .mbtp に保ちます

適切な一時的な橋渡し：

fn singleton_bridge(res : SparseArray, idx : Int, value : Int) -> Unit where {
  proof_axiomatized: true,
  proof_require: valid_idx(idx),
  proof_require: res.data.length() == 1,
  proof_require: res.data[0] == value,
  proof_ensure: singleton_ok(res, idx, value),
} {
  ()
}

次の順序で、信頼指定された橋渡しを取り除きます。

1. コンストラクター
2. オブザーバー
3. 更新関数
4. プリミティブな機械語ブリッジ

デバッグルール：まず実際の失敗を調べる

証明に失敗した後：

• moon prove <pkg> を実行します
• _build/verif/<pkg>/<pkg>.proof.json を調べます

編集する前に問題を分類します。

• 算術またはインデックスの事実が不足している
• 意味論的な橋渡しが不足している
• 量化子のインスタンス化が不適切
• 新しい補題によってソルバーに影響が出ている
• フロントエンド／低レベル化の制限

原因によって必要な修正は異なります。

例：

• インデックスの事実が不足 → ローカルな proof_assert を追加する
• モデルへの橋渡しが不足 → ヘルパー補題または述語を追加する
• ソルバーへの影響 → 補題を共有シムから移動する
• 低レベル化の制限 → 証明の対象を簡略化するか、より小さな再現例で調査する

一般的な再現例の作成方法：

• 構文を小さなプローブパッケージに切り出す
• moon check が失敗するのか、moon prove がクラッシュするのか、VC が単にタイムアウトするのかを確認する
• その後で初めて、問題がモデル化、ソルバーへの誘導、コンパイラーの低レベル化のいずれにあるかを判断する

回帰テストの規律

証明を編集するたびに：

moon check <pkg>
moon prove <pkg>
moon test <pkg>   # if runtime code changed

共有証明レイヤーを編集した後は、依存するパッケージも再実行してください。

ローカルな修正が全体でも安全だと決めつけないでください。

反パターン

次のことは避けてください。

• 各クライアントパッケージで生の #proof_import を繰り返す
• 名前付き述語を使わず、コントラクトの式を長々とインラインで記述する
• 抽象化の設計変更とソルバーへの誘導を一度に行う
• まず証明レポートを確認せずに、多数のヘルパー補題を追加する
• 意味論的な定理を信頼指定された .mbt 関数にだけ保存する
• トップレベル関数のほうが簡単な場合に、メソッドを優先して検証する
• 単相的な最初の段階のほうが早く証明できる場合に、汎用の抽象化を早々に導入する

最小チェックリスト

検証済みの MoonBit の変更を引き渡す前に、次の点を確認してください。

• 意味を表す model(...) が存在するか、または elements(...) のようなより具体的な名前を使う明確な理由がある
• *_inv 述語が存在する
• 適切な場合、コントラクトで名前付きの *_pre ／ *_post 述語に言及している
• 抽象モデルがセット／マップの場合、外延的等価性が明示的に扱われている
• 証明固有のロジックの大部分が .mbtp にある
• 必要に応じて、実行時コードにローカルな proof_assert がある
• 証明に関係するループに明示的な proof_invariant がある
• 信頼する範囲が明示され、可能な限り小さい
• moon check、moon prove、および必要な moon test コマンドを実行済みである