🦀

CreusotによるRustプログラムの形式検証: 事前条件・事後条件・ループ不変条件

2023/02/14に公開

Rust

この記事は下記の記事の続きであり、Creusotでの基本的な条件の記述方法について解説します。

事前・事後条件

引数を足すだけの関数を考えます。

pub fn add(i : u32, j : u32) -> u32 {
    i + j
}

この関数の仕様は「返り値が二つの引数iとjの和になっていること」ことです。
関数終了時の状態や返り値に対して保証する条件を事後条件(postcondition)といい、Creusotでは#[ensures(..)]を用いて記述できます。また、返り値はresultという名前の変数で参照できます。

+#[ensures(result == i + j)]
pub fn add(i : u32, j : u32) -> u32 {
    i + j
}

ここから cargo creusotでmlcfgファイルを生成し、Why3のIDEで開いてAuto level 0の自動証明を試みます。

失敗してしまいました。自動証明コマンドを実行しても、Statusは？マークのままです。何がいけないのでしょうか？
このようなときは、ひとまず現在表示されている複雑なゴールを簡単な形に変換するとよいでしょう。

メニューからSplit VCコマンドを選びます。すると、左のペインに表示されているツリーに新たなノードsplit_vcと、その子タスク0および1が追加されます。追加されたsplit_vcノードに対してAuto level 0を実行すると、以下のようになりました。

子タスクのうち"1[postcondition]"と名づけられている方は証明が完了しています。一方"0[integer overflow]"は証明ができていません。どのような内容かは名前から想像がつくと思いますが、具体的なゴールは右ペインに表示されています。iとjの和ががuint32の範囲に収まっていなければならないということですね。

Rustでは整数演算のオーバーフローはdebugモードではpanicするエラー扱いになります。Creusotでの検証でも、全ての計算でオーバーフローが起きないことを証明する必要があります。
今回はこの問題に、iとjが十分小さいという制約を追加することで対処します。
関数呼び出し時の状態や引数に対して要求する条件を事前条件(precondition)といい、Creusotでは#[requires(..)]を用いて記述できます。

+#[requires(i <= 1000u32 && j <= 1000u32)]
#[ensures(result == i + j)]
pub fn add(i : u32, j : u32) -> u32 {
    i + j
}

ここでは厳しめに、両方の引数が1000以下という条件を設定しました。

事前条件を追加したことで、全てのタスクが証明できました。
ちなみに、画像では以前の試行で失敗した自動証明器のノード(一番下の三つ)が痕跡として残ってしまっていますが、"add'vc [VC for add]"に緑のチェックマークがついているので、add関数についての検証は全て完了しています。

次は、add関数を使って別の関数を定義してみます。

#[requires(i <= 1000u32 && j <= 1000u32)]
#[ensures(result == i + j)]
pub fn add(i : u32, j : u32) -> u32 {
    i + j
}

+#[ensures(result == i + 1u32)]
+pub fn inc(i : u32) -> u32 {
+    add(1, i)
+}

この検証は成功するでしょうか？

残念ながら失敗します。先ほど同様Split VCして詳細を見てみると、"0 [precondition]"が失敗しています。
右ペインから内容を確認すると、「1とiがともに1000以下」であることの証明を要求されています。これは先ほどadd関数に対して設定した事前条件です。関数を呼び出す際は、事前条件が満たされていることを呼び出し側で保証しなければなりません。

add関数の事前条件を満たすため、inc関数にも事前条件を設定します

#[requires(i <= 1000u32 && j <= 1000u32)]
#[ensures(result == i + j)]
pub fn add(i : u32, j : u32) -> u32 {
    i + j
}

+#[requires(i <= 1000u32)]
#[ensures(result == i + 1u32)]
pub fn inc(i : u32) -> u32 {
    add(1, i)
}

これでinc関数についても検証ができました。

ループ不変条件

引数に対してループを用いて割り算を行い、商と余りを返す関数を考えます

#[requires(m != 0u32)]
#[ensures(result.0 * m + result.1 == n)]
#[ensures(result.1 < m)]
pub fn div_mod(n: u32, m: u32) -> (u32, u32) {
    let mut div = 0;
    let mut rem = n;
    while rem >= m {
        rem -= m;
        div += 1;
    }
    (div, rem)
}

事前条件は割る数が0でないこと、事後条件は返り値が商と余りとしての条件を満たしていることになります。
プログラムに間違いはなさそうですが、証明には失敗してしまいます。

右のペインに表示される情報を見てみます。Local Contextの部分に表示されている情報を使ってGoal以下の主張が示せればよいのですが、どうやら無理そうです。Local Contextにはいくつかの値の存在やそれらに関する条件が示されていますが、nとdiv_6が満たす条件は何一つ書かれていません。しかしnとdiv_6はGoalの等式に登場しており、任意のnとdiv_6に対してこの等式が成立するわけでもありません。これでは証明は不可能です。

ループを含むプログラムを検証する場合は、ループ不変条件(loop invariant)を記述する必要があります。Creusotではループ不変条件に名前をつける必要があり、#[invariant(名前,条件)]と記述します

#[requires(m != 0u32)]
#[ensures(result.0 * m + result.1 == n)]
#[ensures(result.1 < m)]
pub fn div_mod(n: u32, m: u32) -> (u32, u32) {
    let mut div = 0;
    let mut rem = n;
+   #[invariant(inv, div * m + rem == n)]
    while rem >= m {
        rem -= m;
        div += 1;
    }
    (div, rem)
}

これは、以下の2箇所のassertが全て成功することを主張しています

    assert!(div * m + rem == n) // 開始時に成立
    while rem >= m {
        rem -= m;
        div += 1;
        assert!(div * m + rem == n)　// 反復時に成立
    }

すなわち、ループ不変条件とは以下の二つを満たす条件のことをいいます。

ループ開始時に成立する
ループの中身を（ループの継続条件が真である限り）反復して実行しても、そのたびに成立し続ける（保存される）

ループ不変条件を追加して、検証を成功させることができました。

[loop invariant init]と[loop invariant preservation]という二つのタスクが存在しており、それぞれ開始時と反復時それぞれにおけるループ不変条件の成立を意味しています。

事前・事後条件

ループ不変条件

Discussion