本課題は、このゼミの受講生を選抜するにあたって、皆さんの問題解決力や探究心などを知るためにあります。

もし知らないことがあれば、インターネットなどで調べてくださっても構いません。仮に完全に解けなくても、ぜひ分かる範囲で、考察を書いてみてください。

皆さんの挑戦を待っています！！

[問1] ビット演算の理解
==============================

コンピュータの中では、整数は2進数の0/1のビット列で表現されています。こうしたビット列に対するビット毎の AND や XOR、ビットシフトといった「ビット演算」は効率よく実行できるため、広く活用されています。

例えば、次の関数 `mod4` は、整数 `n` を 4 で割ったときの非負の余り (0～3) を返します。
```rust
fn mod4(n: i64) -> i64 { n & 3 }
```
なお、`i64` は64ビット符号付き整数型で、`&` はビット毎の AND です。`3` は2進数表現では `0b11` なので、この関数は `n` の下位2ビットを返しますが、これは2進数で考えると、`n` を 4 で割った非負の余り (0～3) に対応します。

それでは問題です。次の関数 `skim` を考えてみましょう。
```rust
fn skim(n: i64) -> i64 { n & -n }
```

この関数 `skim` は、端的に言うとどのような値を返す関数でしょうか。また、そのような動作をするのはなぜでしょうか。簡単に説明してください。

ヒント: 様々な値を `skim` に入れて、どういう動作をするか確かめてみると、様子がわかります。例えば、`7`, `8`, `-8`, `12` を入れるとどうなるでしょうか。負の数をビット列で表現するための「2の補数表現」についてもぜひ調べてみてください。

狙い: 入り組んだビット演算は、人間には一見分かりづらくバグの原因となる一方で、論理的には割と扱いやすいため、形式検証の良いテーマとなります。このゼミで扱う可能性も高いので、出題しました。

[問2] 複雑な再帰関数の理解
==============================

以下の関数 `seven` を考えてみましょう。
```rust
fn seven(n: i64) {
    if n <= 4 { n + 3 } else { seven (seven (n - 4)) }
}
```

不思議なことに、この関数 `seven(n)` は、n ≥ 4 で常に 7 を、n ≤ 3 で n + 3 を返します。これがなぜか、説明してください。

ヒント: 一見複雑ですが、小さい `n` から順に動作を追ってみると、様子が見えてきます。例えば、`seven(7)` はどういう動作になるでしょうか。次に、`seven(11)` はどういう動作になるでしょうか。さらに、`seven(15)` はどういう動作になるでしょうか。

狙い: 複雑な問題に取り組む胆力、論理的な思考力を見ています。また、検証器の実装では再帰をしばしば使うので、再帰への習熟も確認しています。

[問3] RustHorn 流の預言の理解
==============================

## 解説

Rust では「借用」という機能により「可変参照」`&'a mut T` を作り、これを通して安全にメモリ上のデータを更新できます。しかし、これは従来の手法では検証が難しいものでした。Rust の所有権型システムは非常に強い制限を与えてくれるので、何か上手いことができそうです。

講師 松下 の研究「RustHorn」は、「預言 (prophecy)」という未来を先取りする技術で Rust プログラムをモデル化する手法を提案し、可変参照を使う Rust プログラムを一般に効率よく検証できるようにしました。Rust 半自動検証器 Creusot もこのアイデアを取り入れています。

RustHorn 流の預言による借用のモデル化を簡単に説明すると、以下のようになります。

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

## 問題

それでは問題です。可変借用を扱う以下の Rust 関数を考えましょう。
```rust
fn take_max<'a>(ma: &'a mut i32, mb: &'a mut i32) -> &'a mut i32 {
    if *ma >= *mb { ma } else { mb }
}
fn inc_max(mut a: i32, mut b: i32) {
    { let mc = take_max(&mut a, &mut b); *mc += 7; }
    assert!((a - b).abs() >= 7);
}
```
なお、`abs` は絶対値を計算する関数です。

関数 `inc_max` は任意の入力 `a`, `b` について、`assert!` によるアサーションが成功して終了します (ただし、整数のオーバーフローは無視します)。これがなぜか、RustHorn 流の預言によるモデルを通して説明してください。

ヒント: 上の解説に加えて、以下の講演や論文などを参考にしてくださって構いません。
- RustHorn JSSST 2020 トップカンファレンス特別講演
    + 動画 https://www.youtube.com/watch?v=Ah_Bds6I_YI
    + スライド https://shiatsumat.github.io/talks/jssst2020-esop2020-rust-horn-talk.pdf
- RustHorn ACM TOPLAS 2021 論文 https://dl.acm.org/doi/full/10.1145/3462205
- Creusot RW 2021 講演 動画 https://www.youtube.com/watch?v=b8sBtmzq0FM

狙い: このゼミで自作する Rust 検証器で RustHorn 流の預言を扱う可能性が高いので、これを機にこの考え方を理解してもらいたい、という思いで出題しました。プログラムの動作を追って、落ち着いて考えていけば、きっとわかると思います。

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

セキュリティ・キャンプ 2025 のこのゼミで挑戦したいこと、参加にあたっての思い、自身の強みなどについて、自由に書いてください。