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 5.1.1 of the OCaml compiler;
• version 1.7.2 of why3;
• version 2.5.2 of alt-ergo.

(EasyCrypt is implemented in OCaml, why3 is the interface to SMT solvers used by EasyCrypt, and alt-ergo is one of SMT solvers you will need.) If you run into problems, or have feedback as to how I can improve these instructions, please let me know!

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.

To be able to run the GUI version of Emacs, you should install GWSL, the Windows X server.

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, the default is having to work with the terminal (non-GUI) version of Emacs. Install GWSL (see above) to be able to run the GUI version, which gives a much better user experience when using EasyCrypt.

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.

  $> sudo apt-get install autoconf

With MacPorts, you can run

  $> sudo port install autoconf

And on HomeBrew, you can run

  $> brew install autoconf

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 5.1.1  # 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 --deps-only easycrypt
  $> eval $(opam env)

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

You should ensure opam won't install newer versions of Why3:

  $> opam pin why3 1.7.2

Next, you need to install the SMT solvers Alt-Ergo and Z3.

You should install Alt-Ergo:

  $> opam pin alt-ergo 2.5.2

You need to install version 4.12.4 of Z3. On HomeBrew, you can run

  $> brew install z3

There are binaries for macOS (OSX) and Ubuntu Linux at this URL https://github.com/Z3Prover/z3/releases/tag/z3-4.12.4. 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 or later, 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 build EasyCrypt itself by running

  $> opam install easycrypt
  $> eval $(opam env)

At this point, running

  $> which easycrypt

  PATH-TO-HOME-DIR/.opam/5.1.1/bin/easycrypt

In .opam/5.1.1/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.

Next, you use easycrypt to configure why3, by running

  $> easycrypt why3config

This will first delete and then create the file .config/easycrypt/why3.conf in your home directory. Why3 should report that Alt-Ergo and Z3 are installed. The (multiple) messages should include

  Found prover Alt-Ergo version 2.5.2, OK.
  Found prover Z3 version 4.12.4, OK.

Don't worry about the warning about why3.conf not existing; it's because EasyCrypt first deleted the old version.

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/5.1.1/bin")
           exec-path))
    (setenv "PATH"
            (concat
             "PATH-TO-HOME-DIR/.opam/5.1.1/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

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 main branch (which is called main). 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 5.1.1
  $> 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 --deps-only easycrypt
  $> eval $(opam env)
  $> opam pin why3 1.7.2
  $> opam pin alt-ergo 2.5.2
  $> eval $(opam env)
  $> opam install easycrypt
  $> eval $(opam env)
  $> easycrypt why3config

At this point, running

  $> which easycrypt

  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 5.1.1 in these settings of your .emacs file:

  (when (eq window-system 'ns)
    (setq exec-path
          (append
           '("PATH-TO-HOME-DIR/.opam/5.1.1/bin")
           exec-path))
    (setenv "PATH"
            (concat
             "PATH-TO-HOME-DIR/.opam/5.1.1/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 5.1.1
  $> eval $(opam env)
  $> easycrypt why3config

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)
  $> easycrypt why3config

(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