#はじめに
vimのキーバインドを使えるEmacsであるところのSpacemacsでProofGeneralを動かすためには、coqレイヤーを追加すればよい。しかし、
- EasyCrypt公式のインストールガイドはSpacemacsを考慮していない
- Spacemacs0.200.13ではcoqレイヤーを追加するのに2通りの方法があり、片方ではEasyCryptが動作しなかった
というわけで、EasyCrypt導入からSpacemacsでEasyCryptの証明ができるまでを順に辿っていく。
なお今回の方法では、システムにEasyCryptだけではなくCoqが入る。EasyCryptはCoq/SSReflectに大きく影響を受けているようなので、使えるようになって損はしないだろう。
…と大仰に書きましたが、結局のところほとんど公式サイトへのリンク集です。
EasyCryptの導入
基本的にここを参考にすればいいです。
https://github.com/EasyCrypt/easycrypt
外部ソルバ導入
EasyCryptのインストールの際に必要なパッケージであるec-proversは、次のSMTソルバのためのメタパッケージである。
- Z3
- Alt-Ergo
EasyCryptではこれらに加えて、さらに強力なソルバであるCVC4が利用可能である。
ここから環境にあったバイナリをダウンロードし、パスの通っているところに配置すればよい。
https://cvc4.github.io/downloads.html
なお、追加後はwhy3 config --detectをもう一度実行する必要があることに注意。
Coqインストール
以下を参考に、OPAM経由でインストールする1。ここではCoqIDEは必要ない。
https://coq.inria.fr/opam-using.html
Spacemacs導入
Spacemacsインストール
ここを参考にインストール。
Spacemacsの実態は.emacs.dと設定ファイルである.spacemacsなので、.emacs.dのバックアップを忘れずに。
https://github.com/syl20bnr/spacemacs/tree/master
coqレイヤー追加
Spacemacsのcoqレイヤーを追加することで、ProofGeneralを使えるようにする。
.spacemacsのdotspacemacs/user-initに、proof-site.elへのパスを追記する。
OPAMでインストールした場合、$OPAM_SWITCH_PREFIX/share/proof-general/generic/proof-site.elになるはず。
(defun dotspacemacs/user-init ()
(setq proof-general-path "/your/local/PG/generic/proof-site"))
ここを参考に導入。
https://github.com/tchajed/spacemacs-coq
coqといいつつ、.vファイルだけではなく.ecファイルのシンタックスハイライトもしてくれるようになる2。
ちなみにこちらの方法ではProofGeneralがCoqだけしか認識せず、EasyCryptが証明できないため注意。
https://gist.github.com/mtrsk/10a03927490f9edb1f7a2cd72792b0ec
うまく動くかテストしてみる。
require import Bool DBool.
module A = {
proc main() = {
var x;
x <$ {0,1};
x <- x ^^ x;
return x;
}
}.
module B = {
proc main() = {
var y <- false;
return y;
}
}.
lemma test &m :
Pr[A.main() @ &m : res] = Pr[B.main() @ &m : res].
proof. byequiv=>//.
proc. by auto; smt.
qed.
これをSpacemacsで読み込んでProofGeneralが起動し、きちんと証明できれば勝ち。