Skip to main content
  • Home
  • Development
  • Documentation
  • Donate
  • Operational login
  • Browse the archive

swh logo
SoftwareHeritage
Software
Heritage
Archive
Features
  • Search

  • Downloads

  • Save code now

  • Add forge now

  • Help

https://github.com/EasyCrypt/easycrypt
02 June 2025, 21:44:42 UTC
  • Code
  • Branches (169)
  • Releases (5)
  • Visits
    • Branches
    • Releases
    • HEAD
    • refs/heads/PKEROM
    • refs/heads/PolyMicro
    • refs/heads/PolynomialEncoding
    • refs/heads/aprhl
    • refs/heads/bdep
    • refs/heads/bdep_MLKEM_avx2_equivs
    • refs/heads/bdep_ecCircuitsRefactor
    • refs/heads/better-ceil
    • refs/heads/ci-external-projects-in-file
    • refs/heads/comm-algebra
    • refs/heads/csidh-group-action
    • refs/heads/deploy-annotations
    • refs/heads/deploy-axiom-clone-subcommand
    • refs/heads/deploy-better-dlet
    • refs/heads/deploy-better-int-red
    • refs/heads/deploy-better-print
    • refs/heads/deploy-better-printing
    • refs/heads/deploy-binomial-law
    • refs/heads/deploy-cdh-rsr
    • refs/heads/deploy-chachapoly
    • refs/heads/deploy-chernoff
    • refs/heads/deploy-clean-pow
    • refs/heads/deploy-codepos-fix
    • refs/heads/deploy-crt
    • refs/heads/deploy-cyclic
    • refs/heads/deploy-debug-mark
    • refs/heads/deploy-deep-match
    • refs/heads/deploy-default-nosmt
    • refs/heads/deploy-derandomize
    • refs/heads/deploy-dexcepted-sampling
    • refs/heads/deploy-djoin-dlist
    • refs/heads/deploy-docker
    • refs/heads/deploy-dword-is-dlist
    • refs/heads/deploy-eager-rp
    • refs/heads/deploy-easyPQC
    • refs/heads/deploy-eqv-quotient
    • refs/heads/deploy-extended-tests
    • refs/heads/deploy-feature-127
    • refs/heads/deploy-fingroup
    • refs/heads/deploy-fix-#154
    • refs/heads/deploy-fix-17390
    • refs/heads/deploy-fix-292
    • refs/heads/deploy-fmatch
    • refs/heads/deploy-for
    • refs/heads/deploy-general-prf-distinguisher
    • refs/heads/deploy-genhave
    • refs/heads/deploy-global-union
    • refs/heads/deploy-hybrid0
    • refs/heads/deploy-implicit-arguments
    • refs/heads/deploy-improve-matching
    • refs/heads/deploy-indexed-types
    • refs/heads/deploy-instance-adv
    • refs/heads/deploy-lamport
    • refs/heads/deploy-license
    • refs/heads/deploy-log
    • refs/heads/deploy-match
    • refs/heads/deploy-match-in-stmt
    • refs/heads/deploy-match-in=prog-logic-houra
    • refs/heads/deploy-mem
    • refs/heads/deploy-mem-in-types
    • refs/heads/deploy-minr-maxr
    • refs/heads/deploy-momemtum
    • refs/heads/deploy-multi-apply
    • refs/heads/deploy-mutual-inductives
    • refs/heads/deploy-named-goals
    • refs/heads/deploy-nested-tuples
    • refs/heads/deploy-new-cost
    • refs/heads/deploy-new-cost2
    • refs/heads/deploy-new-rom
    • refs/heads/deploy-nosmt-ops
    • refs/heads/deploy-oaep
    • refs/heads/deploy-oracle-pke
    • refs/heads/deploy-packaging
    • refs/heads/deploy-pattern-in-rewrite
    • refs/heads/deploy-poly-record
    • refs/heads/deploy-poly-reduce
    • refs/heads/deploy-polymorphic-module
    • refs/heads/deploy-ppe-with-full-path
    • refs/heads/deploy-prod-fintype
    • refs/heads/deploy-project-file
    • refs/heads/deploy-quantum
    • refs/heads/deploy-quantum-upgrade
    • refs/heads/deploy-reduce-decimal
    • refs/heads/deploy-reduction
    • refs/heads/deploy-refine-birthday
    • refs/heads/deploy-remove-cut
    • refs/heads/deploy-rewrite-patterns
    • refs/heads/deploy-rigid-auto-rewrite
    • refs/heads/deploy-rigid-opt
    • refs/heads/deploy-ring-ideal
    • refs/heads/deploy-ring-with-dfl-inv
    • refs/heads/deploy-rmap
    • refs/heads/deploy-rom-nobranching
    • refs/heads/deploy-search
    • refs/heads/deploy-sem
    • refs/heads/deploy-sigmaprotocols
    • refs/heads/deploy-simpler-rp
    • refs/heads/deploy-simpler-xpaths
    • refs/heads/deploy-solveeq
    • refs/heads/deploy-subst
    • refs/heads/deploy-subst-crush
    • refs/heads/deploy-tactic-in-rewrite
    • refs/heads/deploy-taylor
    • refs/heads/deploy-tc
    • refs/heads/deploy-theory-matrix
    • refs/heads/deploy-theory-matrix-ring
    • refs/heads/deploy-theory-monalg
    • refs/heads/deploy-theory-symmetric-group
    • refs/heads/deploy-tighter-birthday
    • refs/heads/deploy-trailing-whitespaces
    • refs/heads/deploy-transeq
    • refs/heads/deploy-trivial-in-low-api
    • refs/heads/deploy-tutorial
    • refs/heads/deploy-unit-ro
    • refs/heads/deploy-update-readme
    • refs/heads/deploy-upto
    • refs/heads/deploy-warn-on-noop-change
    • refs/heads/deploy-weak-dep-types
    • refs/heads/deploy-wf
    • refs/heads/deploy-why3-1.4
    • refs/heads/deploy-wp-kw
    • refs/heads/deploy-xreal
    • refs/heads/dilithium
    • refs/heads/distr-matrix
    • refs/heads/draft-typeclass
    • refs/heads/ellora
    • refs/heads/eval-pwhile
    • refs/heads/expr-fold
    • refs/heads/feature-lossless-while
    • refs/heads/fix-142
    • refs/heads/fix-360
    • refs/heads/fix-457
    • refs/heads/fix-729
    • refs/heads/flake-nix
    • refs/heads/fmap-fold
    • refs/heads/fun-tuple
    • refs/heads/glob-rec
    • refs/heads/hidden-theory-items
    • refs/heads/inlined-doc
    • refs/heads/latex-style
    • refs/heads/libpath
    • refs/heads/main
    • refs/heads/mayo
    • refs/heads/memory
    • refs/heads/memory-ci
    • refs/heads/ml-kem-spec-ci
    • refs/heads/mpoly
    • refs/heads/ocaml-5
    • refs/heads/ois-refactoring
    • refs/heads/opsem
    • refs/heads/poly-better-clones
    • refs/heads/polydiv
    • refs/heads/pp_form_noabbrev
    • refs/heads/proc-func-typing
    • refs/heads/r2022.04-01
    • refs/heads/remove-dump-command
    • refs/heads/remove-pinned-provers
    • refs/heads/setoidrw
    • refs/heads/simple-projects
    • refs/heads/simplify_module
    • refs/heads/softcode-memories
    • refs/heads/split-parser
    • refs/heads/sub-patterns
    • refs/heads/subtypes
    • refs/heads/theory_finite_field
    • refs/heads/trace-in-eco
    • refs/heads/unbless-alt-ergo
    • refs/heads/uptobad_warnings
    • refs/tags/r2024.09
    • r2025.03
    • r2025.02
    • r2024.01
    • r2023.09
    • r2022.04
  • 4edb6e1
  • /
  • README.md
Raw File Download
Take a new snapshot of a software origin

If the archived software origin currently browsed is not synchronized with its upstream version (for instance when new commits have been issued), you can explicitly request Software Heritage to take a new snapshot of it.

Use the form below to proceed. Once a request has been submitted and accepted, it will be processed as soon as possible. You can then check its processing state by visiting this dedicated page.
swh spinner

Processing "take a new snapshot" request ...

Permalinks

To reference or cite the objects present in the Software Heritage archive, permalinks based on SoftWare Hash IDentifiers (SWHIDs) must be used.
Select below a type of object currently browsed in order to display its associated SWHID and permalink.

  • content
  • directory
  • revision
  • snapshot
origin badgecontent badge Iframe embedding
swh:1:cnt:7dbbd61c71373fb5f1826280262462e87c5e71db
origin badgedirectory badge Iframe embedding
swh:1:dir:4edb6e1cfb2ff9f7b2f0b5c31b8fb353b26da2e7
origin badgerevision badge
swh:1:rev:dc50f44bff4c40022c08e46832a16b676b3db0da
origin badgesnapshot badge
swh:1:snp:1daf49d44cfdbe57fd4e94361450fbdc0c873593
Citations

This interface enables to generate software citations, provided that the root directory of browsed objects contains a citation.cff or codemeta.json file.
Select below a type of object currently browsed in order to generate citations for them.

  • content
  • directory
  • revision
  • snapshot
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Generate software citation in BibTex format (requires biblatex-software package)
Generating citation ...
Tip revision: dc50f44bff4c40022c08e46832a16b676b3db0da authored by Pierre-Yves Strub on 26 May 2023, 09:54:58 UTC
Forbid the usage of [declare] for concrete modules.
Tip revision: dc50f44
README.md
EasyCrypt: Computer-Aided Cryptographic Proofs
====================================================================

EasyCrypt is a toolset for reasoning about relational properties of
probabilistic computations with adversarial code. Its main application
is the construction and verification of game-based cryptographic
proofs.

Table of Contents
--------------------------------------------------------------------

 * [EasyCrypt: Computer-Aided Cryptographic Proofs](#easycrypt-computer-aided-cryptographic-proofs)
    - [Installation requirements](#installation-requirements)
    - [Via OPAM](#via-opam)
      - [Installing requirements using OPAM (POSIX systems)](#installing-requirements-using-opam-posix-systems)
      - [Installing requirements using OPAM (non-POSIX systems)](#installing-requirements-using-opam-non-posix-systems)
    - [Via NIX](#via-nix)
 * [Configuring Why3](#configuring-why3)
    - [Note on prover versions](#note-on-prover-versions)
 * [Installing/Compiling EasyCrypt](#installingcompiling-easycrypt)
 * [Proof General Front-End](#proof-general-front-end)
    - [Installing using opam](#installing-using-opam)
    - [Installing from sources](#installing-from-sources)


Installation requirements
--------------------------------------------------------------------

EasyCrypt uses the following third-party tools/libraries:

 * OCaml (>= 4.08)

     Available at https://ocaml.org/

 * OCamlbuild

 * Why3 (= 1.6.x)

     Available at <http://why3.lri.fr/>

     Why3 must be installed with a set a provers.
     See <http://why3.lri.fr/#provers>

     Why3 libraries must be installed (make byte && make install-lib)

 * Menhir <http://gallium.inria.fr/~fpottier/menhir/>

 * OCaml Batteries Included <http://batteries.forge.ocamlcore.org/>

 * OCaml PCRE (>= 7) <https://github.com/mmottl/pcre-ocaml>

 * OCaml Zarith <https://forge.ocamlcore.org/projects/zarith>

 * OCaml ini-files <http://archive.ubuntu.com/ubuntu/pool/universe/o/ocaml-inifiles/>

On POSIX/Win32 systems (GNU/Linux, *BSD, OS-X), we recommend that users
install EasyCrypt and all its dependencies via `opam`.

Via OPAM
--------------------------------------------------------------------

### Installing requirements using OPAM 2 (POSIX systems)

Opam can be easily installed from source or via your packages manager:

  * On Ubuntu and derivatives:

      ```
      $> add-apt-repository ppa:avsm/ppa
      $> apt-get update
      $> apt-get install ocaml ocaml-native-compilers camlp4-extra opam
      ```

  * On Fedora/OpenSUSE:

      ```
      $> sudo dnf update
      $> sudo dnf install ocaml ocaml-docs ocaml-camlp4-devel opam
      ```

  * On MacOSX using brew:

      ```
      $> brew install ocaml opam
      ```

Once `opam` and `ocaml` has been successfully installed run the following:

```
$> opam init
$> eval $(opam env)
```

For any issues encountered installing `opam` see:

  * [https://opam.ocaml.org/doc/Install.html] for detailed opam installation instructions.

  * [https://opam.ocaml.org/doc/Usage.html] for how to initialize opam.

You can then install all the needed dependencies via the opam OCaml
packages manager.

  0. Optionally, switch to a dedicated compiler for EasyCrypt:

      ```
      $> opam switch create easycrypt $OVERSION
      ```

      where `$OVERSION` is a valid OCaml version (e.g. ocaml-base-compiler.4.07.0)

  1. Add the EasyCrypt package from repository:

      ```
      $> opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git
      ```

  2. Optionally, use opam to install the system dependencies:

      ```
      $> opam install opam-depext
      $> opam depext easycrypt
      ```

  3. Install EasyCrypt's dependencies:

      ```
      $> opam install --deps-only easycrypt
      $> opam install alt-ergo
      ```

     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
      ```

  4. You can download extra provers at the following URLs:

     * Z3: [https://github.com/Z3Prover/z3]
     * CVC4: [https://cvc4.github.io/]

### Installing requirements using OPAM (non-POSIX systems)

You can install all the needed dependencies via the opam OCaml packages manager.

  1. Install the opam Ocaml packages manager, following the instructions at:

     https://fdopen.github.io/opam-repository-mingw/installation/

  2. Add the EasyCrypt package from repository:

      ```
      $> opam pin -yn add easycrypt https://github.com/EasyCrypt/easycrypt.git
      ```

  3. Use opam to install the system dependencies:

      ```
      $> opam install depext depext-cygwinports
      $> opam depext easycrypt
      ```

  4. Install EasyCrypt's dependencies:

      ```
      $> opam install --deps-only easycrypt
      $> opam install alt-ergo
      ```

  5. You can download extra provers at the following URLs:

     * Z3: [https://github.com/Z3Prover/z3]
     * CVC4: [https://cvc4.github.io/]


Via NIX
--------------------------------------------------------------------

First, install the [Nix package manager](https://nixos.org/) by
following [these instructions](https://nixos.org/manual/nix/stable/#chap-installation).

Then, at the root of the EasyCrypt source tree, type:

    ```
    $> nix-shell
    ```
    
These should install all the required dependencies. From there, simply
run:

    ```
    $> make
    ```
    
to compile EasyCrypt.

Note on Prover Versions
--------------------------------------------------------------------

Why3 and SMT solvers are independent pieces of software with their
own version-specific interactions. Obtaining a working SMT setup may
require installing specific versions of some of the provers.

At the time of writing, we depend on Why3 1.6.x, which supports the
following prover versions:

 * Alt-Ergo 2.4.2
 * CVC4 1.8
 * Z3 4.12.1

`alt-ergo` can be installed using opam, if you do you can use pins to
select a specific version (e.g, `opam pin alt-ergo 2.4.1`).

Development branches use `dune-3.x` and which is incompatible with
`alt-ergo-2.4.1`. In this case, you can use `alt-ergo-2.4.2`. The
warning "Prover Alt-Ergo version 2.4.2 is not recognized." upon
configuration (see below) can be [safely ignored](https://gitlab.inria.fr/why3/why3/-/commit/f2863d84f65824f21afd75546117becbf453efcc).

Installing/Compiling EasyCrypt
====================================================================

If installing from source, running

```
$> make
$> make install
```

builds and install EasyCrypt (under the binary named `easycrypt`),
assuming that all dependencies have been successfully installed. If
you choose not to install EasyCrypt system wide, you can use the
binary `ec.native` that is located at the root of the source tree.

EasyCrypt comes also with an opam package. Running

```
$> opam install easycrypt
```

installs EasyCrypt and its dependencies via opam. In that case, the
EasyCrypt binary is named `easycrypt`.

Configuring Why3
====================================================================

Initially, and after the installation/removal/update of SMT provers,
you need to (re)configure Why3 via the following `easycrypt` command:

```
$> easycrypt why3config
```

EasyCrypt stores the Why3 configuration file under

```
$XDG_CONFIG_HOME/easycrypt/why3.conf
```

EasyCrypt allows you, via the option -why3, to load a Why3
configuration file from a custom location. For instance:

```
$> easycrypt why3config -why3 $WHY3CONF.conf
$> easycrypt -why3 $WHY3CONF.conf
```

where `$WHY3CONF` must be replaced by some custom location.

Proof General Front-End
====================================================================

EasyCrypt mode has been integrated upstream. Please, go
to <https://github.com/ProofGeneral/PG> and follow the instructions.

Examples
====================================================================

Examples of how to use EasyCrypt are in the `examples` directory. You
will find basic examples at the root of this directory, as well as a
more advanced example in the `MEE-CBC` sub-directory and a tutorial on
how to use the complexity system in `cost` sub-directory.

Software Heritage — Copyright (C) 2015–2025, The Software Heritage developers. License: GNU AGPLv3+.
The source code of Software Heritage itself is available on our development forge.
The source code files archived by Software Heritage are available under their own copyright and licenses.
Terms of use: Archive access, API— Contact— JavaScript license information— Web API

back to top