🛠️

Rustの形式検証ツールCreusotをWSLにインストールした記録

2025/03/27に公開

Rustの形式検証ツールCreusotをWSLにインストールした記録です。
ちょっと苦労したので一応備忘録としてひととおり書いておこうと思います。

Creusotとは何かについては公式リポジトリを見るか：
https://github.com/creusot-rs/creusot
kkobさんによる記事にある説明を読むとよいと思います：

参考資料

以下のREADMEに従いました：

`rustup` インストール

手順としてはあるので書きましたが、すでに入っていたので何もしていません。

`opam` インストール

https://opam.ocaml.org/doc/Install.html
最新版が2.3.0なところ、aptでは2.0.5しか入らないようだったので、公式スクリプトを使いました：

$ bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)"

すぐに終わりました。

リポジトリクローン

公式リポジトリをクローンします：
https://github.com/creusot-rs/creusot

インストールスクリプトの実行

インストールスクリプト1回目(失敗)

クローンしたディレクトリに入り、インストールスクリプトを実行しますが……

$ ./INSTALL

エラーが出てしまいます：

[ERROR] Opam has not been initialised, please run `opam init'
Error: Failed to create opam switch

`opam` の初期設定1回目(失敗)

言われた通りにopamの初期設定コマンドを実行しますが：

$ opam init

さらにエラーが出ます：

[ERROR] Missing dependencies -- the following commands are required for opam to operate:
  - bwrap: Sandboxing tool bwrap was not found. You should install 'bubblewrap'. See
    https://opam.ocaml.org/doc/FAQ.html#Why-does-opam-require-bwrap.

`bubblewrap` のインストール

言われたコマンドをインストールします。今度はaptに頼ってよいようです：

$ sudo apt install bubblewrap

`opam` の初期設定2回目

$ opam init

今度はうまくいきました。

`fish` 向け設定

<><> Required setup - please read <><><><><><><><><><><><><><><><><><><><><><><>

  In normal operation, opam only alters files within ~/.opam.

  However, to best integrate with your system, some environment variables
  should be set. If you allow it to, this initialisation step will update
  your fish configuration by adding the following line to ~/.config/fish/config.fish:

    test -r '/home/username/.opam/opam-init/init.fish' && source '/home/username/.opam/opam-init/init.fish' > /dev/null 2> /dev/null; or true

  Otherwise, every time you want to access your opam installation, you will
  need to run:

    eval (opam env)

  You can always re-run this setup with 'opam init' later.

fishから操作をしていたのを読み取ってか、fish向けの環境変数設定をしてくれるようです。
(なので$でプロンプトが出ているのは実は嘘です)
Configuration snippetsとして作ってくれた方がいい気がするけど……config.fishで上書きされるのが許せないのだろうか。
とりあえず従います。

Do you want opam to configure fish?
> 1. Yes, update ~/.config/fish/config.fish
  2. Yes, but don't setup any hooks. You'll have to run eval (opam env) whenever you change your current 'opam switch'
  3. Select a different shell
  4. Specify another config file to update instead
  5. No, I'll remember to run eval (opam env) when I need opam

[1/2/3/4/5] 1

インストールスクリプト2回目

$ ./INSTALL

Why3関連のインストールでかなり長い時間画面が止まりました。
たまらずCtrl-Cを押したところ、何故か正常に進んだかのような画面になり、「外部依存パッケージが足りない」というメッセージが……

The following system packages will first need to be installed:
    autoconf libcairo2-dev libgtk-3-dev libgtksourceview-3.0-dev libzmq3-dev

<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>

opam believes some required external dependencies are missing. opam can:
> 1. Run apt-get to install them (may need root/sudo access)
  2. Display the recommended apt-get command and wait while you run it manually (e.g. in another terminal)
  3. Continue anyway, and, upon success, permanently register that this external dependency is present, but not
     detectable
  4. Abort the installation

[1/2/3/4] 1

とりあえず従うと、aptで入れるべきものを入れたのち、opam側での依存関係のインストールが始まります。かなり長いです。

動作確認

以下のドキュメントのQuickstartまでは動作を確認して終わりたいと思います：

動作確認1回目(失敗)

プロジェクトを作成してみます：

$ cargo creusot new creusotinstallcheck

しかしうまくいきません。

Error: "/home/username/.local/share/creusot/bin/z3" "--version" failed: exit status: 1
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.34' not found (required by /home/username/.local/share/creusot/bin/z3)
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.32' not found (required by /home/username/.local/share/creusot/bin/z3)
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.33' not found (required by /home/username/.local/share/creusot/bin/z3)
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.30' not found (required by /home/username/.local/share/creusot/bin/z3)
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.29' not found (required by /home/username/.local/share/creusot/bin/z3)

Error: Please run 'cargo creusot setup status' to diagnostic and fix the issue(s)

従ってみます……。

$ cargo creusot setup status

同様のエラーメッセージが出ます。

Creusot installation found.
=== INSTALLATION
Why3:
- path: /home/username/.local/share/creusot/_opam/bin/why3
- check_version: true
Alt-Ergo:
- mode: builtin
- check_version: true
Z3:
- mode: builtin
- check_version: true
CVC4:
- mode: builtin
- check_version: true
CVC5:
- mode: builtin
- check_version: true
=== PATHS
config: /home/username/.config/creusot
data:   /home/username/.local/share/creusot
cache:  /home/username/.cache/creusot

Error: "/home/username/.local/share/creusot/bin/z3" "--version" failed: exit status: 1
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.34' not found (required by /home/username/.local/share/creusot/bin/z3)
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.32' not found (required by /home/username/.local/share/creusot/bin/z3)
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.33' not found (required by /home/username/.local/share/creusot/bin/z3)
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.30' not found (required by /home/username/.local/share/creusot/bin/z3)
/home/username/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.29' not found (required by /home/username/.local/share/creusot/bin/z3)

Hint: reinstall Creusot to upgrade builtin tools.

再インストールを要求されてますが、glibcってもっと基本的なものじゃありませんでしたっけ……？
怪しいので色々と調べたところ、「Ubuntuのバージョンが古すぎて必要なglibcのバージョンに達していない」ということのようです。
(後になって見つけたのですが、この件はissueとして触れられていました：)

おとなしくUbuntuのアップグレードをします。

Ubuntuアップグレード

playreeさんの記事の手順をなぞります：

22->24ではなく20->22ですが、同様でした。

動作確認2回目(失敗)

cargo creusot setup status

うまくいっていそうです：

Creusot installation found.
=== INSTALLATION
Why3:
- path: /home/username/.local/share/creusot/_opam/bin/why3
- check_version: true
Alt-Ergo:
- mode: builtin
- check_version: true
Z3:
- mode: builtin
- check_version: true
CVC4:
- mode: builtin
- check_version: true
CVC5:
- mode: builtin
- check_version: true
=== PATHS
config: /home/username/.config/creusot
data:   /home/username/.local/share/creusot
cache:  /home/username/.cache/creusot

プロジェクト作成に進みます：

$ cargo creusot new creusotinstallcheck

Warning: prover z3 not found (why3)
Warning: prover z3 not found (why3)

ないんかーい！

作ったプロジェクトディレクトリに移って証明をさせてみます：

$ cargo creusot prove

   Compiling creusot-contracts-proc v0.4.0
    Checking creusot-contracts v0.4.0
error: The `creusot_contracts` crate is loaded, but the following items are missing: ghost_new, ghost_into_inner, ghost_inner_logic, ghost_deref, ghost_deref_mut, ghost_ty. Maybe your version of `creusot-contracts` is wrong?

error: could not compile `creusot-contracts` (lib) due to 1 previous error

あれれ……

`Cargo.toml` の変更

どうやら既知の不具合のようです：

Cargo.tomlを変更し、ローカルからcreusot-contractsを読み込ませます：

[dependencies]
creusot-contracts = { path = "../../path/to/creusot-rs/creusot/creusot-contracts" }

動作確認3回目

$ cargo creusot prove

Warning: prover z3 not found (why3)
Theory verif.creusotinstallcheck_rlib.creusotinstallcheck.M_add_one.Coma: ✔ (1)
Cache 1/12
Proofs ✔ (1)
 - fixed: 1
Provers 38ms (+38ms)
Emitted 1 warning

動いた！！！

Why3 IDE 動作確認

1回目(失敗)

$ cargo creusot why3 ide

    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.09s
Fatal: loading strategy 'Creusot_Auto' failed: Prover "Z3,4.12.4" not installed or not configured
Solve this problem in your why3.conf file and retry.

Creusotの再インストール

途中で止まったのをCtrl-Cで飛ばしたのがまずかったかもしれないと思ったので、再インストール。

$ ./INSTALL

OPAM分はキャッシュが効いているのか、かなり早く終了。今度は途中で止まることもなかった。

2回目

$ cargo creusot why3 ide

GUIが出現！WSL環境でもきちんと動いてくれるみたい。

Discussion

ログインするとコメントできます