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というディレクトリに不穏な資料が残されているので見てみると面白いかもしれない。