以下の応募課題は、あなたの問題解決力・好奇心などを知るためのものです。
もしもまだ知らないことがあったとしても、自分でインターネット等で調べて勉強して解くことを試みてください。

リラックスして、楽しんで取り組んでいただけたら幸いです。
もし完全に解けなくても、分かった範囲で答えてくだされば大丈夫です。


[問1] 一般的なプログラム検証の理解
=============================================

## 背景

プログラム検証と一口に言っても検証したい性質は色々あります。
ここでは、一番代表的な「プログラムの計算結果が期待される条件を満たす」というタイプの性質（機能正当性）の検証に取り組みます。

## 解説

プログラム検証における基本的なアイデアである「ループ不変条件」について、ここで解説しておきます。

例えば、次の関数 to_odd を考えます（Rust で書かれています）。
```rs
fn to_odd() {
    let mut r = 1;
    while rand() {
        r += 2;
    }
    assert!(r % 2 == 1);
}
```
なお rand 関数はブール値の乱数を返すものとします。
このプログラムは、変数 r を 1 で初期化したあと、while ループで rand() が false を返すまで何度でも r を 2 増やし、最後に r が必ず奇数となっていることを assert で主張しています。
この assert が必ず成功することを検証したいとしましょう。

こうしたループを持つプログラムを検証するための基礎的な道具が「ループ不変条件 (loop invariant)」です。
ループ不変条件とは、以下の2つの性質を満たす条件 P のことです：
- ループに入る時点で P が成立している
- P が成立しているとき、ループをもう一度繰り返したあとも、必ず P が成立する
これら2つの性質より、特に、ループから抜けた直後に、ループ不変条件が成立する、ということが示せます。

上の to_odd の例の場合、以下の理由から「r が奇数である」というのが while ループの不変条件となります。
- r の初期値は 1 なので奇数である
- r が奇数のとき、r を 2 増やしても r は奇数である
したがって、ループを抜けたあとも r は奇数です。
これにより、assert が必ず成功することを検証できました。

## 問題

以下の while ループを持つプログラムを考えます（Rust で書かれています）。
```rs
fn to_square(n: u64) {
    let mut i = n;
    let mut s = 0;
    while i != 0 {
        s += 2 * i - 1;
        i -= 1;
    }
    assert!(s == n * n);
}
```
このプログラムの最後の assert が必ず成功することを、ループ不変条件を使って検証してください。
（なお、整数のオーバーフローは無視して構いません。）

### ヒント

while ループを抜けた時点では、ループ不変条件に加えて、特に i == 0 が成立しています。
これを踏まえて、assert の条件を証明できる、上手いループ不変条件を考えてみてください。

## 発展問題（任意）

もし余力があれば、ほかにも何かプログラムと仕様を記述し、その正しさを検証してください。
例えば、ユークリッドの互除法、マッカーシーの91関数、挿入ソートなどが考えられます。

## 解答作成時の注意

プログラム・仕様・検証方法は、どのようなプログラミング言語を使って書いても、また擬似コードや自然言語などで書いても良いですが、わかりやすい記述を心がけてください。
何か資料を調べて参考にしても構いませんが、その場合は出典・引用部分を必ず明記してください。


[問2] Creusot による Rust プログラム検証の理解
=============================================

## 背景: Creusot

Rust プログラムの自動検証器として最近注目されているのが Creusot です。
https://github.com/creusot-rs/creusot

Creusot は、ループ不変条件などの検証を助けるための注釈が加えられた Rust プログラムについて、機能正当性を自動で検証してくれます。

例えば、問1のプログラムを以下のように修正したものが Creusot で検証できます。
```rs
fn to_odd() {
    let mut r = 1;
    #[invariant(r@ % 2 == 1)]
    while rand() {
        if r < 0x10000000 {
            r += 2;
        }
    }
    assert!(r % 2 == 1);
}
```
while 式に r が奇数であるというループ不変条件を示す注釈 `#[invariant(r@ % 2 == 1)]` が加えられている、というのがポイントです。
（ちなみに、@ は Rust のオブジェクトをモデルの値に変換するものですが、ひとまず無視して構いません。
また、Creusot は整数のオーバーフローが起きないことも検証するので、r が十分小さいときにのみ r を増やすように処理を微修正しています。）

Creusot はこうした注釈付きの Rust プログラムを変換し、Why3 という関数型言語向けの自動検証器に投げます。
Why3 は SMT ソルバの助けを借りて、検証を自動で行います。

例えば、上の Rust プログラムを Creusot で変換した結果を Why3 に投げると、以下のような出力を返して検証が成功します。
```
File to_odd.mlcfg:
Goal to_odd'vc.
Prover result is: Valid (0.01s, 14456 steps).
```

なお、正確には、先ほどの Rust コードを Creusot でコンパイルするためには以下のコードを先頭に加えるなどする必要があります。
```rs
extern crate creusot_contracts;
use creusot_contracts::*;

#[trusted]
fn rand() -> bool {
    panic!()
}
```

## 解説: 預言によるメモリ更新の検証

Rust では可変参照 `&'a mut T` を通してメモリの更新が行えますが、これは従来の手法では検証が難しいものでした。
Rust の所有権型システムは強い制限を与えてくれるので、何か上手いことができそうです。

講師 松下 が提案した Rust 全自動検証器 RustHorn は、「預言 (prophecy)」という未来を先取りする仕組みを使って、可変参照をつかう更新を含む Rust プログラムを一般に効率よく検証できるようにしました。
後発の Rust 自動検証器 Creusot もこのアイデアを取り入れています。

預言を使う借用の検証の全体の流れは、簡単に説明すると、以下のようになります。

1. 預言を作る
    - 借用を始める際に、「借用中に行われる更新の最終的な結果」を未確定な形で先取りした「預言」x を作る。可変参照 `&'a mut T` は現在の値 v と預言の値 x の組 (v, x) としてモデル化される。
2. 所有権を捨てるときに預言の値を確定させる
    - 可変参照 `&'a mut T` は所有権を捨てる際に、預言の値 x をその時点の値 v' へと確定させる、すなわち、そのときのモデルが (v', x) であれば x = v' という情報を得る。
3. 借用終了後に預言の値を使う
    - 貸し手は、借用のライフタイム `'a` が終わって所有権を取り戻した際に、預言の値 x をその時点での値として使うことができる。

## 問題

可変参照、および預言を使う以下の Rust プログラム例（https://github.com/creusot-rs/creusot/blob/master/creusot/tests/should_succeed/rusthorn/inc_max.rs から引用）について、検証が上手く行く仕組みを簡単に説明してください。
```rs
#[ensures(if *ma >= *mb { *mb == ^mb && result == ma }
                   else { *ma == ^ma && result == mb })]
fn take_max<'a>(ma: &'a mut u32, mb: &'a mut u32) -> &'a mut u32 {
    if *ma >= *mb {
        ma
    } else {
        mb
    }
}

#[requires(a <= 1_000_000u32 && b <= 1_000_000u32)]
pub fn inc_max(mut a: u32, mut b: u32) {
    let mc = take_max(&mut a, &mut b);
    *mc += 1;
    assert!(a != b);
}
```
なお、Creusot の記法で `^` は可変参照の預言を表します。

また、requires は関数の実行前に入力について要求される条件を、ensures は関数の実行後に入出力について保証される条件（result は関数の出力）を表す注釈です。
ちなみに専門的には、前者を事前条件 (precondition)、後者を事後条件 (postcondition) と呼びます。

以下の講演や論文なども参照してくださって大丈夫です。

- JSSST 2020 RustHorn 講演 動画 https://www.youtube.com/watch?v=Ah_Bds6I_YI ・スライド https://shiatsumat.github.io/talks/jssst2020-esop2020-rust-horn.pdf
- RustHorn ジャーナル論文 https://dl.acm.org/doi/full/10.1145/3462205
- 講演 "Creusot: A prototype tool for verification of Rust software" 動画 https://www.youtube.com/watch?v=b8sBtmzq0FM

## 発展問題（任意）

もし余力があれば、ほかにも Rust プログラムの検証例を Creusot のテストケースなどから選んで、あるいは新たに作って、検証が上手く行く仕組みを簡単に説明してください。
預言を特に使わない例でも構いません。

## 解答作成時の注意

何か資料を調べて参考にしても構いませんが、その場合は出典・引用部分を必ず明記してください。

最新の話題で大変かもしれませんが、自分で色々調べたり考えたり手を動かしたりして取り組めば、道は開けるはずです。
皆さんの挑戦を待っています。


[問3] 自由記述
=============================================

Rust やプログラム検証についてどのようなことに興味があるか、セキュキャン2024のこのゼミでどのようなことに挑戦したいか、どのような思いがあるか、といったことについて、自由に記述してください。