EasyCrypt Installation Instructions

The official EasyCrypt installation instructions are available on the EasyCrypt GitHub. Below is a summary of these instructions that also emphasizes the connection with the Emacs text editor. EasyCrypt can be run from the shell (command line) in batch mode, to check individual .ec files. But when proofs are constructed interactively this is done within Emacs, with the generic interface Proof General mediating between Emacs and EasyCrypt, which is running as a sub-process of Emacs.

Installation on Windows via WSL2

Although the official instructions suggest it's possible to install EasyCrypt directly on Windows, the best advice I've received suggests it's better to first install a Linux VM (virtual machine) on Windows using Windows Subsystem for Linux Installation Guide for Windows 10 (WSL2), and then follow the below instructions for Linux/macOS.

Follow these instructions to install WSL2 and create a virtual machine for the Linux distribution of your choice. Ubuntu is a good option, and the following instructions assume you have made this choice.

Installing Emacs

Emacs may already be installed on Linux distributions, but here are downloading instructions. On Ubuntu Linux, you can install Emacs by running ($> represents the shell's prompt)

  $> sudo apt-get install emacs

(You may need to run

  $> sudo apt-get update

to update the Ubuntu package list, first.)

On WSL2, you'll be stuck with the terminal (non-GUI) version of Emacs.

On macOS you should install the "application" version of Emacs from https://emacsformacosx.com. This gives Emacs the look-and-feel of a typical Mac application. Emacs will then reside in /Applications/Emacs.app. (See more information about configuring Emacs, below.)

Installing EasyCrypt on Linux/macOS

To install EasyCrypt, one must first install opam, the OCaml Package Manager (EasyCrypt is implemented using the functional programming language OCaml). See this webpage for how to install opam: https://opam.ocaml.org/doc/Install.html.

Next, run the following commands ($> represents the shell's prompt):

  $> opam init # creates .opam sub-directory of your home directory
  $> eval $(opam env) # updates environment variables in current shell

Running opam init will ask you two questions about whether you shell's startup script and opam's scripts should be modified to keep your shell's environment variables up to date automatically, and you should answer "yes".

  $> opam switch create 4.10.0  # say which version of OCaml compiler to build
  $> eval $(opam env)

Next, run

  $> opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git
  $> opam install depext
  $> opam depext easycrypt
  $> opam install --deps-only easycrypt

If you get errors about ocamlbuild failing because it's already installed, the check can be skipped with the following:

  $> CHECK_IF_PREINSTALLED=false opam install --deps-only easycrypt

Next, you need to install the SMT solvers Alt-Ergo and Z3. Before installing Alt-Ergo using opam, you'll need to make sure autoconf is already installed on your system. Type which autoconf to find out. On Ubuntu Linux, you can install it by running

  $> sudo apt-get install autoconf

With MacPorts, you can run

  $> sudo port install autoconf

And on HomeBrew, you can run

  $> brew install autoconf

The following instructions assume that the current version of Why3 (which is a portal to all the installed SMT solvers) is 1.3.3. They may need to be modified otherwise. If you run why3 --version and the answer isn't 1.3.3, feel free to send me an email and I'll update these instructions.

You should install version 2.3.1 of Alt-Ergo:

  $> opam install alt-ergo.2.3.1

You need to install version 4.8.6 of Z3. There are binaries for macOS (osx) and Ubuntu Linux at this URL https://github.com/Z3Prover/z3/releases/tag/z3-4.8.6. If you need to build it from source, there are source archives available, too. Assuming you have the binary distribution, put the whole directory somewhere, and update your shell's startup script to add its bin directory to the PATH environment variable. (If you are running macOS Big Sur, you may need to go to System Preferences => Security & Privacy and allow the z3 binary to be run.) Run which z3 while not in the Z3 bin directory to verify that you have set up PATH correctly.

Next, you configure why3 by running

  $> why3 config --detect --full-config

This will create and/or update the file .why3.conf in your home directory. I was surprised that the above command reads a preexisting version of this file and includes provers that may no longer exist in the new version of the file. So deleting .why3.conf before running the above command can be helpful. Why3 should report that Alt-Ergo and Z3 are installed. The (multiple) messages should include

  Found prover Alt-Ergo version 2.3.1, OK.
  Found prover Z3 version 4.8.6, OK.

Don't worry if it says that your version of Alt-Ergo or Z3 is "not known to be supported". Then you build EasyCrypt itself by running

  $> opam install easycrypt

At this point, running

  $> which easycrypt
you should give you the response

In .opam/4.10.0/lib/easycrypt/theories you'll now find the EasyCrypt Standard Library, a collection of EasyCrypt theories that you can require to make them available for use in your own .ec files.

Finally, you should install Proof General using the instructions in https://github.com/ProofGeneral/PG, which are summarized below.

Proof General is installed using Emacs's package manager, MELPA. If you haven't already added

  (require 'package)
  (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)

to your .emacs customization file (located in your home directory (create it if it doesn't exist)), you should do so. (Everytime you update .emacs, you should then exit and restart Emacs.)

Then run the following commands within Emacs,

  M-x package-refresh-contents RET

followed by

  M-x package-install RET proof-general RET

to install and byte-compile Proof General. (In the above, M-x means hold down the meta/alt/option modifier key, and then press x. You can also type Esc and then x. And RET is the Return key.)

If you have to run the terminal (rather than the GUI) version of Emacs, you will want to add the line

  (setq overlay-arrow-string "")

to your .emacs file. Otherwise, Proof General will print an annoying => over the first two characters of the next line to be processed. This should only be an issue with WSL2.

Finally, there's an issue unique to running Emacs.app on macOS. You will need to add the following to your .emacs file so that the PATH environment variable is properly set when Proof General attempts to run easycrypt:

  (when (eq window-system 'ns)
    (setq exec-path
    (setenv "PATH"
             (getenv "PATH"))))

where: PATH-TO-HOME-DIR is the fully qualified name of your home directory; and PATH-TO-Z3-DIR is the fully qualified name of the directory in which the z3 executable has been installed (you can run which z3 to find this directory).

Checking Everything Worked

To verify that everything worked, put the following text in the file check-install.ec:

(* check-install.ec *)

(* if EasyCrypt is able to successfully check this file, then
   it and the SMT solvers Alt-Ergo and Z3 are properly installed
   and configured *)

require import AllCore.  (* load the "core" EasyCrypt theories, in
                            particular giving us the relation < on the
                            type int of integers *)

prover quorum=2 ["Alt-Ergo" "Z3"].  (* the smt tactic will only
                                       succeed if both Alt-Ergo and
                                       Z3 are able to solve the goal *)

lemma foo (x y : int) :
  x < y => x + 1 < y + 1.

First, check that running

  $> easycrypt check-install.ec

completes without reporting any errors (silence means success). (You must first cd to the directory where you stored check-install.ec.).

Second, edit this file with emacs, and verify that repeatedly stepping through the file with C-c C-n (or click Proof-General in the menu bar, and use Next Step) takes you to the point where you are told that the lemma foo has been added to list of known lemmas.

You use C-c C-u (Undo Step in the Proof-General menu) to undo an EasyCrypt step. And moving the cursor to a point in the file and then typing C-c RET (Goto Point in the Proof-Genal menu) will cause EasyCrypt to process up to that point (you can do this to undo a section of code, or to move forward to some arbitrary point).

Updating and Upgrading

You can update the list of opam packages by running

  $> opam update

This may prompt you to upgrade the installed packages to their latest verions, by running

  $> opam upgrade

But beware of doing this if it would upgrade to an overly advanced version of Alt-Ergo.

Feedback and Problems

If you run into problems, or have feedback as to how I can improve these instructions, please let me know!
Alley Stoughton (alley.stoughton@icloud.com)