这里的EasyCrypt指的是那个密码学的辅助证明工具.

其实他的github上说明已经挺详细的了，但还是会有一点坑，记录一下.

PS：据说里面有个script目录里有安装脚本的（不过我没试过，逃）

首先安装包管理工具opam：

1
2
3
4
5
6
7
# e.g. ubuntu 18.04
sudo add-apt-repository ppa:avsm/ppa
sudo apt-get update
sudo apt-get install ocaml ocaml-native-compilers camlp4-extra opam

opam init
eval `opam config env`

克隆github上的仓库：

1
2
git clone https://github.com/EasyCrypt/easycrypt.git
cd easycrypt

指定编译器（ocaml?）版本，就是仓库的README的“Via OPAM”对应的第0点，但上面指定的版本是个变量$OVERSION，这里应该换成跟他一样的4.07.0，不然会有奇怪的错误（不过其实4.07.0以上的好像也行，像我如果还要编EasyUC的话就需要4.08.0）；然后后面第1点没啥问题，就一起写了：

1
2
opam switch create easycrypt 4.08.0
opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git

第2点的话据说在opam=2.1.0及以上的版本已经不需要depext了，所以可以忽略；第三点的话需要注意alt-ergo的版本要跟他的2.4.0一样（在“Note on Prover Versions”里有说- -）：

1
2
opam install --deps-only easycrypt
opam pin alt-ergo 2.4.0

然后第4点的z3=4.8.10和cvc4=1.8其实是要自己安装的，对应的github上都有release，注意版本就好，然后加到path中（这里我直接放bin里了）：

1
2
3
4
5
6
7
8
9
# z3
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip
# unzip and cd ...
ln -s /path/to/z3-4.8.10-x64-ubuntu-18.04/bin/z3 /path/to/bin

# cvc4
wget https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt
chmod +x ./cvc4-1.8-x86_64-linux-opt
ln -s /path/to/cvc4-1.8-x86_64-linux-opt /path/to/bin

然后why3 config一下，没报错的话就没啥问题了：

1
why3 config detect

接着就可以愉快地make了，在make的时候会报两个错，都是跟Option相关的，根据这里的说法，Option改名为BatOption了，打开报错的文件把“Option”改成“BatOption”就好（比如我编的版本是src/ecHiGoal.ml: 695和src/ecTheoryReplay.ml: 839），都改完后再make就没啥问题了；

然后make install是可以指定目录的，比如我装在~/.local里（已经加到path里的）就不用sudo了：

1
2
3
4
5
6
7
# change Option to BatOption
make
make check
make examples

make PREFIX=~/.local install
easycrypt --help

如果能运行的话就是安装成功了；

另外说一下easycrypt后面接文件运行时有时会没有输出的（特别是如果证明是对的话），所以需要获取它的返回值，用echo $?，或者：

1
if easycrypt path/to/xxx.ec; then echo yes; else echo no; fi

Links：

  • https://github.com/EasyCrypt/easycrypt
  • https://github.com/alleystoughton/EasyTeach
  • https://github.com/easyuc/EasyUC/
  • https://tover.xyz/p/easy-crypt-tex/