概要: ElectrolysisはRustの検証条件をLEANに出力するプロジェクトである。これを使ってみた。

Electrolysisとは

Electrolysis (electrolysis: 電解) はSebastian Ullrich氏の修士研究で開発されたプロジェクトで、Rustプログラムの正当性や計算量に関する検証条件をLean Theorem Proverの命題として出力する機能を提供する。

なお、GitHubの様子だと、このプロジェクトは修論の日付からほぼ開発がストップしているようだ。Ullrich氏はその後、Electrolysisの成果の一部をLEANに還元するなどの活動をしているようだ。

Electrolysisの実行

以下、Ubuntu 16.04を仮定する。

ElectrolysisはRustのコンパイラプラグインとして実装されているため、Rustの特定のnightlyバージョンに強く依存している。また、libcore自体を検証ターゲットにしているため、Rustコンパイラのソースコード自体も取得する必要がある。

$ git clone https://github.com/Kha/electrolysis.git
$ cd electrolysis
$ rustup override add $(cat rust-nightly-version)
$ rustup component add rust-src
$ cargo run core
$ cargo run alloc
$ cargo run collections
$ cargo run fixedbitset

petgraphに対する検証条件の出力

petgraphに対する検証条件の出力はやや面倒である。まずpetgraphを取得してビルドする。

$ git submodule update --init
$ cd thys/petgraph/src
$ cargo build
$ cd ../../..

次に thys/petgraph/config.toml を編集して、libfixedbitsetのrlibのハッシュを適切に置き換える。例えば、

rustc_args = "thys/petgraph/src/src/lib.rs --crate-name petgraph --crate-type lib -L dependency=thys/petgraph/src/target/debug/deps --extern fixedbitset=thys/petgraph/src/target/debug/deps/libfixedbitset-0ba3fe99bd419295.rlib"

targets = [
  "algo.scc",
]

とすると以下が通る。

$ cargo run petgraph

Lean2のビルド

Leanは現在、過去の証明との互換性のために残されている0.2.0系列と、最新の3.0.0系列がある。Electrolysisに適しているのは0.2.0系列なので、そちらを使う。

また、lean2のビルドスクリプトにはninjaを取得する部分があるが、ninjaの取得先が削除されてしまっているので、以下のパッチを当てる必要がある。(以下これをlinja.patchと呼ぶ)

diff --git a/bin/linja.in b/bin/linja.in
index 926f33e..10ee37d 100755
--- a/bin/linja.in
+++ b/bin/linja.in
@@ -239,7 +239,7 @@ def show_download_progress(*data):
     log_nonewline("Download: size\t= %i kb, packet: %i/%i" % (file_size, downloaded_packets, total_packets+1))
 
 def get_ninja_url():
-    prefix = "https://leanprover.github.io/bin/"
+    prefix = "https://github.com/leanprover/leanprover.github.io/raw/8fb36e926a3c4df8b84bfafedb7f39687f24b93b/bin/"
     if platform.architecture()[0] == "64bit":
         if platform.system() == "Linux":
             return prefix + "ninja-1.5.1-linux-x86_64"

$ sudo apt install python3 git libgmp-dev libmpfr-dev
$ git clone https://github.com/leanprover/lean2.git
$ cd lean2
$ patch -p1 < path/to/linja.patch
$ mkdir -p build/release
$ cd build/release
$ cmake -DCMAKE_BUILD_TYPE=Release ../../src
$ make -j4 install DESTDIR=.

上の例ではDESTDIR=.を指定することで./usr/localにインストールしているが、これを外せば/usr/localにインストールされる。

検証条件に対するLEAN2の実行

lean2にはlean3のような--makeオプションがついていない。以下のようなMakefileをthysの直下に置くとよい。(LEANDIRを適切に変更する)

#!/usr/bin/make -f

LEANDIR = /somewhere/lean2/build/release/usr/local
LEAN = $(LEANDIR)/bin/lean

LEAN_SOURCES = $(shell find . -name '*.lean')
LEAN_BINARIES = $(LEAN_SOURCES:.lean=.olean)
LEAN_DEPFILES = $(LEAN_SOURCES:.lean=.d)

all:
  $(MAKE) deps
  $(MAKE) all2

deps: $(LEAN_DEPFILES)

all2: $(LEAN_BINARIES)

clean:
  $(RM) $(LEAN_DEPFILES) $(LEAN_BINARIES)

.PHONY: all deps all2 clean

%.d: %.lean
  (echo $<:; $(LEAN) --deps $<) | tr '\n' ' ' > $@

%.olean: %.lean
  $(LEAN) $< -o $@

-include $(LEAN_DEPFILES)

これを配置した上で thys 直下で make を実行すると、証明がコンパイルされる。

まとめと感想

Electrolysisの機能を一通り動かすことができた。

実は別のRustバージョンや別のLeanバージョンで動かせないか検討したがかなり困難であることがわかった。

Rustの検証プロジェクトではむしろRustBeltが有名で、メンバーから考えてもかなり期待が持てる。RustBeltとElectrolysisは以下のように異なる。

検証の目的: RustBeltはunsafeな動作を含むより低レベルな操作に対し、UBを踏まないなどの証明をターゲットにしている。Electrolysisはより高級な変換で、アルゴリズムの正当性や計算量の検証を目指している。
ロジック: RustBeltは高階並行分離論理フレームワークIrisに立脚している。
証明支援系: RustBeltはCoqで検証する。ElectrolysisはLeanで検証する。
検証条件の抽出: Electrolysisは実際のRustコード(MIR)からの抽出に対応している。RustBeltは今のところMIRからの抽出には対応していない(Coq側の対応するコードは手動で書かれている)が、Ralf Jung氏が最近MIRの改造に取り組んでいるところから見るに、そのうち対応すると思われる。

簡潔なQ

Electrolysisを使ってみた