[Docker] Containers and how to use them

Our CI produces the following Docker containers, also usable via podman and other compatible container runtimes:

• ec-base-box (on main, release and release tags): not for use by end users
• ec-build-box (on main, release and release tags): contains all dependencies for EasyCrypt, as well as a variety of solvers:
  • Alt-Ergo: 2.4.x, 2.5.x, 2.6.x
  • Z3: 4.8.x, 4.12.x, 4.13.x, 4.14.x, 4.15.x
  • CVC5: 1.3.x
  • CVC4: 1.8
• ec-formosa-box (on main, release and release tags): the same as ec-build-box with dependencies for the current Jasmin release in addition.
• ec-test-box (on release and release tags): the same as ec-build-box with EasyCrypt installed and configured to use all installed solvers.

We aim to keep close track of the highest point version for each minor of each solver, but feel free to open a PR if we are too slow doing this.

How to use the containers

For use in interactive proof development, we recommend you use ec-build-box:main (or ec-formosa-box if you need Jasmin's eclib) and rebuild EasyCrypt from main at the start of your development session.

For use in CI, we recommend you use ec-test-box:release, rebuilding EasyCrypt only on branches that should not use the latest release. (For example, a branch set up to follow main for inclusion in EasyCyrpt's external CI.)

In both cases, we strongly recommend that you use the containers in conjunction with an easycrypt.project file constraining the set of solvers that should be used.