RustのcoreおよびallocクレートをCoqに翻訳して形式検証
(formal.land)Rustのcoreおよびallocクレートの翻訳
初回実行 🐥
coq-of-rustを使って Rust のallocおよびcoreクレートを初回実行した結果、数十万行の Coq コードファイルが2つ生成された。- これはツールが大規模なコードベースでも動作することを意味するが、生成された Coq コードはコンパイルできない。エラーの発生頻度は低い（数千行に1回程度）。
入力 Rust コードの規模（cloc コマンド基準）
-
alloc: 26,299 行の Rust コード -
core: 54,192 行の Rust コード -
マクロを展開して翻訳する必要があるため、実際に翻訳すべき規模はさらに大きい。
生成されたコードの分割 🪓
- 主な変更点は、
coq-of-rustが生成した出力を、各入力 Rust ファイルごとに1つのファイルへ分割したこと。 - これは定義順序に依存せず翻訳できるため可能である。Rust ファイル間の循環依存は Coq では禁止されるが、それでも分割は可能。
出力規模
alloc: 54 個の Coq ファイル、171,783 行の Coq コードcore: 190 個の Coq ファイル、592,065 行の Coq コード
コード分割の利点
- 生成されたコードを読みやすく、探索しやすい
- 並列コンパイルが可能になり、コンパイルしやすい
- 1つのファイルに集中してデバッグしやすい
- コンパイルできないファイルを無視しやすい
- 単一ファイルの変更追跡がしやすく、保守しやすい
いくつかのバグ修正 🐞
- モジュール名同士の衝突によるバグがあった。これは
implブロックのモジュール名を選ぶ際に発生していた。 - モジュール名により多くの情報を追加して一意性を高めた。たとえば
where句を追加した。
例
-
DefaultトレイトのMapping型実装:#[derive(Default)] struct Mapping<K, V> { // ... } -
以前の Coq コード:
Module Impl_core_default_Default_for_dns_Mapping_K_V. (* ...trait implementation ... *) End Impl_core_default_Default_for_dns_Mapping_K_V. -
修正後の Coq コード:
Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V. (* ... *)
コンパイルできないファイル一覧
-
alloc/boxed.v -
core/any.v -
core/array/mod.v -
core/cmp/bytewise.v -
core/error.v -
core/escape.v -
core/iter/adapters/flatten.v -
core/net/ip_addr.v -
これは全ファイルの 4% を占める。コンパイルできるファイルにも未処理の Rust 構造が存在する可能性がある。
例 🔎
Option 型の unwrap_or_default メソッドの元コード
pub fn unwrap_or_default(self) -> T
where
T: Default,
{
match self {
Some(x) => x,
None => T::default(),
}
}
翻訳された Coq コード
Definition unwrap_or_default (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
let Self : Ty.t := Self T in
match τ, α with
| [], [ self ] =>
ltac:(M.monadic
(let self := M.alloc (| self |) in
M.read (|
M.match_operator (|
self,
[
fun γ =>
ltac:(M.monadic
(let γ0_0 :=
M.get_struct_tuple_field_or_break_match (|
γ,
"core::option::Option::Some",
0
|) in
let x := M.copy (| γ0_0 |) in
x));
fun γ =>
ltac:(M.monadic
(M.alloc (|
M.call_closure (|
M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
[]
|)
|)))
]
|)
|)))
| _, _ => M.impossible
end.
単純化した関数コード
Definition unwrap_or_default {T : Set}
{_ : core.simulations.default.Default.Trait T}
(self : Self T) :
T :=
match self with
| None => core.simulations.default.Default.default (Self := T)
| Some x => x
end.
- この単純化された定義はコード検証時に使用される。同値性の証明は
CoqOfRust/core/proofs/option.vにある。
結論
-
標準ライブラリを形式化することで、Rust プログラムの検証作業を信頼できるものにできる。
-
次の目標は、依然として煩雑な証明プロセスを単純化すること。特に、シミュレーションが元の Rust コードと同値であることを示す過程で、名前解決、高度な型の導入、副作用の除去といった段階を分離したい。
-
Rust プロジェクトの形式検証に関心がある場合は、contact@formal.land まで連絡してほしい。形式検証は、与えられた仕様に対してバグがないことを数学的に保証する、最高水準の安全性を提供する。
タグ:
- coq-of-rust
- Rust
- Coq
- 翻訳
- core
- alloc
GN⁺の意見
- Rust と Coq の統合: Rust と Coq の統合は、Rust プログラムの安定性向上に大きく役立つ。Rust の安全性と Coq の形式検証を組み合わせれば、特に重要なアプリケーションで非常に有用である。
- 自動化の重要性:
coq-of-rustツールを用いた自動翻訳は、手作業よりも信頼性が高い。しかし、検証過程では依然としてエラーが発生しうるため注意が必要。 - 複雑なコードベース管理: 大規模コードベースを扱ううえで、コード分割は保守やデバッグに大いに役立つ。これは特にチーム開発で重要な要素である。
- 形式検証の必要性: 形式検証は、特に金融、医療、航空などの重要分野で不可欠である。Rust と Coq の組み合わせは、これらの分野で大きな価値を提供しうる。
- 技術導入時の考慮事項: 新しい技術を導入する際は、学習コストと既存システムとの互換性を考慮すべきである。Coq のような形式検証ツールは学習コストが高い可能性があるため、十分な教育と準備が必要。
1件のコメント
Hacker Newsの意見
Hacker Newsコメントまとめ要約
自動翻訳ツールの信頼性
プログラム規模と検証
翻訳プロセスにおけるエラーの可能性
暗号資産関連の投稿
形式検証の限界
Rustの形式検証
形式検証仕様の作成
他のアプローチとの比較
Rustのカーネル採用
F*へのRustバックエンド追加