Rust-proofを使ってみる
概要: Rust-proofはElectrolysisと同様にRustプログラムから検証条件を抽出するが、LeanではなくSMTソルバであるZ3向けの検証条件を出力する。こちらも開発が放棄されているように見えるが現在もビルド可能である。
準備
テスト用リポジトリを準備する
$ cargo new rustproof-test $ cd rustproof-test
該当のnightlyバージョンを取得する (Electrolysisと同様、Rust-proofもコンパイラプラグインのため、特定のnightlyバージョンに強く依存している)
$ rustup override set nightly-2016-08-12
Z3をインストール
$ sudo apt install z3
使ってみる
Cargo.toml
に以下の依存関係を書く
[dependencies] rustproof = { git = "https://github.com/Rust-Proof/rustproof.git", rev = "654b004" }
src/lib.rs
に以下のように関数を書く。これはEXAMPLESに掲載されているものとほぼ同様だが、5:i32
のような型つきリテラルは5i32
に置き換えてある。
// feature(plugin) を有効化してrustproofをロード #![feature(plugin)] #![plugin(rustproof)] // #[condition] によりコンパイル時にrustproofによるチェックが走る #[condition(pre="(x:i32 <= i32::MAX - 5i32)", post="return:i32 == (x:i32 + 5i32)")] pub fn add_five(x:i32) -> i32 { assert!(x <= 2147483647-5); x+5 } #[condition(pre="(x:i32 <= i32::MAX - 4i32)", post="return:i32 == (x:i32 + 5i32)")] pub fn add_five_invalid(x:i32) -> i32 { assert!(x <= 2147483647-5); x+5 } #[condition(pre="true", post="(x:bool==true IMPLIES return:bool==false) && (x:bool==false IMPLIES return:bool==true)")] pub fn boolean_not(x:bool) -> bool { if x == true { false } else { true } }
検証を実行するには単にコンパイラを起動すればよい。
$ cargo build Compiling rustproof-test v0.1.0 fn add_five(..) Verification Condition is valid. fn boolean_not(..) Verification Condition is valid. fn add_five_invalid(..) Verification Condition is not valid. (model (define-fun x () (_ BitVec 32) #x7ffffffb) ) Finished debug [unoptimized + debuginfo] target(s) in 42.84 secs
まとめ
大変よい試みだが、古すぎるのが残念だと思う。rust-proofが開発された経緯は不明だが、documentsというディレクトリに不穏な資料が残されているので見てみると面白いかもしれない。