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.

These instructions are current for version 4.12.0 of the OCaml compiler, and version 1.4.0 of why3.

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.12.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.4.0. They may need to be modified otherwise. If you run why3 --version and the answer isn't 1.4.0, feel free to send me an email and I'll update these instructions.

You should install Alt-Ergo:

  $> opam install alt-ergo

If you need to install a particular version of Alt-Ergo, you can run, e.g.:

  $> opam pin alt-ergo.2.4.0

You need to install version 4.8.10 of Z3. There are binaries for macOS (OSX) and Ubuntu Linux at this URL https://github.com/Z3Prover/z3/releases/tag/z3-4.8.10. 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

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.4.0, OK.
  Found prover Z3 version 4.8.10, 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
  PATH-TO-HOME-DIR/.opam/4.12.0/bin/easycrypt

In .opam/4.12.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)
  (package-initialize)

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.)

You will probably want to add

  (setq electric-indent-mode nil)

to your .emacs file, because the built-in indentation rules for editing EasyCrypt definitions and proofs may seem nonoptimal. Then format manually, using explicit spaces.

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
          (append
           '("PATH-TO-HOME-DIR/.opam/4.12.0/bin")
           exec-path))
    (setenv "PATH"
            (concat
             "PATH-TO-HOME-DIR/.opam/4.12.0/bin:PATH-TO-Z3-DIR:"
             (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.
proof.
smt().
qed.

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.

Using a Development Branch of EasyCrypt

It is also possible to work with a development branch of EasyCrypt (see the branches on GitHub), switching back and forth between that branch and the master branch (which is called 1.0). Here are instructions in terms of the aprhl branch. You can repeat these instructions for as many branches as you wish.

First create a new opam "switch" (which you can call whatever you like (here, easycrypt-aprhl)), specifying which version of the OCaml compiler to use:

  $> opam switch create easycrypt-aprhl 4.12.0
  $> eval $(opam env)

Next, run the following commands (note the occurrence of the branch, aprhl, in the first command), repeating steps from the above instructions, but for this new switch:

  $> opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git#aprhl
  $> opam install depext
  $> opam depext easycrypt
  $> opam install --deps-only easycrypt
  $> opam install alt-ergo
  $> why3 config detect
  $> opam install easycrypt

At this point, running

  $> which easycrypt
you should give you the response
  PATH-TO-HOME-DIR/.opam/easycrypt-aprhl/bin/easycrypt

If you are running Emacs.app on macOS, you'll need to substitute the name of your branch (easycrypt-aprhl in our example) for 4.12.0 in these settings of your .emacs file:

  (when (eq window-system 'ns)
    (setq exec-path
          (append
           '("PATH-TO-HOME-DIR/.opam/4.12.0/bin")
           exec-path))
    (setenv "PATH"
            (concat
             "PATH-TO-HOME-DIR/.opam/4.12.0/bin:PATH-TO-Z3-DIR:"
             (getenv "PATH"))))

(PATH-TO-HOME-DIR is still the fully qualified name of your home directory; and PATH-TO-Z3-DIR is still the fully qualified name of the directory in which the z3 executable has been installed.)

To switch back to the master branch, you run:

  $> opam switch set 4.12.0
  $> eval $(opam env)
  $> why3 config detect

If you are running Emacs.app on macOS, you'll need to revert the above changes to your .emacs file.

And then to switch back to easycrypt-aprhl, you run:

  $> opam switch set easycrypt-aprhl
  $> eval $(opam env)
  $> why3 config detect

(also updating your .emacs file if running Emacs.app on macOS). And so on.

You can find out which branch you are on by running

  $> opam switch

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)