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
04 July 2025, 20:56:38 UTC
  • Code
  • Branches (171)
  • 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/delayed-couplings
    • 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/softcode-memories2
    • 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
  • 79feb9a
  • /
  • 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:6900e6aee318b2659d4933ff06bcbd57ca9ed466
origin badgedirectory badge Iframe embedding
swh:1:dir:79feb9a76c3645f233982aaf4c3626852fc6a615
origin badgerevision badge
swh:1:rev:82cc4d7ad1ca93dc93773f50b053591da4d479b1
origin badgesnapshot badge
swh:1:snp:ad212edc8dbbc66dad52a850b82d297e8a05b24f
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: 82cc4d7ad1ca93dc93773f50b053591da4d479b1 authored by Pierre-Yves Strub on 09 June 2020, 19:55:20 UTC
binomial law + basic lemmas (full / support)
Tip revision: 82cc4d7
README.md
EasyCrypt: Computer-Aided Cryptographic Proofs
====================================================================

[![Build Status](https://travis-ci.org/EasyCrypt/easycrypt.svg?branch=1.0)](https://travis-ci.org/EasyCrypt/easycrypt)

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)
    - [Installing OPAM (POSIX systems)](#installing-opam-posix-systems)
    - [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)
 * [Configuring Why3](#configuring-why3)
 * [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.05)

     Available at http://caml.inria.fr/

 * OCamlbuild

 * Why3 (>= 1.0)

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


Installing OPAM (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.

To install `opam` on non-POSIX systems
[see the section below](#installing-requirements-using-opam-non-posix-systems).


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

You can 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 repository:

      ```
      $> opam repository add easycrypt git://github.com/EasyCrypt/opam.git
      $> opam update
      ```

  2. Optionally, select the EasyCrypt (git) branch you want to use:

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

     where `branch` is the branch name you want to use (e.g. `aprhl`).

     In that case, we advise you to create a dedicated opam switch
     (see first step above).

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

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

  4. Add the EasyCrypt meta-packages:

      ```
      $> opam install --deps-only easycrypt
      $> opam install ec-provers
      ```

      Provers may require external dependencies. You can install then
      directly using opam:

      ```
      $> opam install depext       # if not already done
      $> opam depext ec-provers
      ```

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

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 repository:

      ```
      $> opam repository add easycrypt git://github.com/EasyCrypt/opam.git
      $> opam update
      ```

  3. Optionally, select the EasyCrypt (git) branch you want to use:

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

     where `branch` is the branch name you want to use (e.g. `aprhl`).

  4. Use opam to install the system dependencies:

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

  5. Add the EasyCrypt meta-packages:

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

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

     * Z3: [https://github.com/Z3Prover/z3]
     * EProver: [http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html]


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

Before running EasyCrypt and after the installation/removal/update
of an SMT prover, you need to (re)configure Why3.

```
$> why3 config --detect
```

EasyCrypt is using the default Why3 location, i.e. ~/.why3.conf.
If you have several versions of Why3 installed, it may be impossible
to share the same configuration file among them. EasyCrypt via the
option -why3, allows you to load a Why3 configuration file from a
custom location. For instance:

```
$> why3 config --detect -C $WHY3CONF.conf
$> ./ec.native -why3 $WHY3CONF.conf
```

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


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.

It is possible to change the installation prefix by setting the
environment variable PREFIX:

```
$> make PREFIX=/my/prefix install
```

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


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

Installing using opam
--------------------------------------------------------------------

If you installed the EasyCrypt dependencies using opam, you can
install ProofGeneral via opam too. Running

```
$> opam install proofgeneral
```

installs ProofGeneral along with its EasyCrypt mode. You still have to
tweak your emacs configuration file (~/.emacs) to load
ProofGeneral by adding the following line to it

```
(load-file "$proof-general-home/generic/proof-site.el")
```

where `$proof-general-home` should be replaced by

```
$prefix/share/proofgeneral
```

with `$prefix` being set to the output of

```
$> opam config var prefix
```


Installing from sources
--------------------------------------------------------------------

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

back to top

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