Reference
This page contains detailed explanations of several core concepts/features of EasyCrypt.
Loading and Importing Libraries
Loading and importing libraries from the standard library (or from the folder EasyCrypt
is being executed in) is done with the require
and import
keywords. The require
keyword loads the content of a library; the import
keyword makes all the symbols in
the theory (defined by the library) available without qualification. Conveniently,
require
and import
can be combined (as require import
) to achieve both of the
above at once. Moreover, it is possible to require
and import
multiple libraries
in a single command by providing them in a spaceseparated manner. So, for example,
importing the libraries that contain the definitions and properties for lists
(List.ec
) and distributions (Distr.ec
) can be done as follows.
require import List Distr.
Usually, these type of commands are issued at the beginning of a file, but inserting them just before they are needed works as well.
Oftentimes, it is convenient (if not necessary) to have basic definitions and
properties at your disposal, e.g., concerning the integers and real numbers. Several
of these are contained in the fundamental library AllCore.ec
. As such, it is often
useful to load and import this library by default, as follows.
require import AllCore.
Finally, successful loading and importing can be checked by printing known symbols
from the imported library; this is achieved using the print
keyword. (This is useful
in interactive mode, but could—and likely should—be removed from committed code.) The
following snippet exemplifies this, assuming the List.ec
and Distr.ec
libraries
were loaded and imported.
print list.
print distr.
Distributions
In the analysis and verification of probabilistic programs as in EasyCrypt,
subdistributions are used to model the output distribution of programs that
potentially may not terminate. Loosely speaking, subdistributions are the same as
regular probability distributions, except that the sum of probabilities may be less
than or equal to 1 (instead of being exactly equal to 1). So, in a sense,
subdistributions are an extension of (regular) distributions by being less
restrictive regarding the sum of probabilities. We implement these subdistributions
for any type by defining an operator and using the type constructor distr
as shown
below.
op [lossless full uniform] dctxt : ctxt distr.
The preceding annotationlike syntax for specifying the assumed properties of a
distribution is syntactic sugar that currently only works for the lossless
, full
,
and uniform
properties. Naturally, it is possible to specify any combination (or
none) of these properties for a distribution. For completeness, we provide equivalent
code for the preceding dctxt
definition without any syntactic sugar.
op dctxt : ctxt distr.
axiom dctxt_ll : is_lossless dctxt.
axiom dctxt_fu : is_full dctxt.
axiom dctxt_uni : is_uniform dctxt.
Here, is_lossless
, is_full
, and is_uniform
are predicates (defined in Distr.ec
)
that each capture the property suggested by their name.
Module Types, Modules, and Procedures
In EasyCrypt, algorithms are specified as procedures, which are contained in modules.
Modules provide name spacing, but are also used to define global memories as well as group together procedures and global variables in (somewhat) meaningful ways. Intuitively, modules can be viewed as (potentially stateful) entities that implement a number of algorithms. EasyCrypt also allows for the definitions of module types which, as the name suggests, are types for modules. In essence, module types simply define a set of procedure signatures that a module must implement in order to be of that module type. Ignoring the possibility of specifying module parameters (which we will get to later), the definition of a module type takes the following form.
module type MT = {
proc p(id1 : t1, id2 : t2, ..., idn : tn) : tout
(* ... Other procedure signatures ... *)
}.
In the above snippet, MT
is a module type identifier and proc p(id1 : t1, id2 : t2, ..., idn : tn) : tout
is a procedure signature. In this signature, p
is a procedure identifier; idi
and ti
in idi : ti
are a parameter identifier and type, respectively; and tout
is the type of the
value that the procedure outputs. A module type may contain an unlimited number of procedure signatures.
Then, ignoring the possibility for defining submodules and module parameters, the definition of a module typically looks as follows.
module M : MT = {
var id : t
(* ... Other modulelevel variable declarations ... *)
proc p(id1 : t1, id2 : t2, ..., idn : tn) : tout = {
(* ... Implementation of procedure p ... *)
}
(* ... Other procedure implementations ... *)
}.
Here, M
is a module identifier, and var id : t
denotes a modulelevel variable declaration where id
and t
are a variable identifier and a variable type; the remainder is the same as before. Note that a module of a certain module type
is free to implement any procedure it wants, as long as it also implements the procedures specified by the module type.
In case a module is not given a specific module type, there are no obligations concerning the procedures it implements:
it may even implement no procedures at all.
Finally, procedures contain imperative code written in EasyCrypt's $\texttt{pWhile}$ language. This language is relatively simple, merely allowing for the following kinds of statements inside procedures.
 Local variable declarations. These are statements of the form
var id : type;
, whereid
is the identifier of the variable andtype
is the type of the variable. Moreover, these statements are only allowed in the beginning of a procedure, and, hence, must occur before any other kind of statement.  If statements. These are statements of the following form, where
e
is a boolean expression written in EasyCrypt's expression language.Theif (e) {
(* ... Code of thenbranch ... *)
} else {
(* ... Code of elsebranch ... *)
}else
part of the statement is optional, meaning that the following also constitutes a valid if statement.These statements have the usual interpretation: ifif (e) {
(* ... Code of thenbranch ... *)
}e
evaluates totrue
, execute the code in the thenbranch; else, ife
evaluates tofalse
, execute the code in the elsebranch (if this branch is present, otherwise simply continue).  While statements. These are statements of the following form, where
e
is a boolean expression written in EasyCrypt's expression language.These statements have the usual interpretation: as long aswhile (e) {
(* ... Code of whileloop ... *)
}e
evaluates totrue
, execute the code within the whileloop (wheree
is (re)evaluated before each iteration).  Regular assignments. These are statements of the form
id < e;
, whereid
is the identifier of a variable ande
is an expression written in EasyCrypt's expression language that must evaluate to a value of the variable's type.  Sampling assignments. These are statements of the form
id <$ d;
, whereid
is the identifier of a variable andd
is a (sub)distribution over values of the variable's type.  Procedure call assignments. These are statements of the form
id <@ M.p(e1, e2, ..., en);
, whereid
is the identifier of a variable,M
is the identifier of a (previously specified) module,p
is the identifier of a procedure ofM
, and eachei
is an expression written in EasyCrypt's expression language that evaluates to a value of the type of the corresponding parameter ofM.p
(these are ordered).  Return statements. These are statements of the form
return e
, wheree
is an expression writing in EasyCrypt's expression language that must evaluate to the procedure's output type. A procedure can only have a single return statement; this statement must be the last statement of the procedure.
That's it. Those are all the different kinds of statements EasyCrypt's $\texttt{pWhile}$ language allows inside procedures.
HigherOrder Modules and Module Types
As alluded to before, EasyCrypt allows modules and module types to be parameterized on other modules; such a module (type) is called higherorder module (type) or functor (type), respectively. A module of such a functor type must be instantiated with modules of the type of the parameters indicated by in the functor type definition. A technicality with this is that the module parameters themselves cannot be of functor types; i.e., the module parameters cannot themselves have module parameters that still need to be instantiated.
The procedures of higherorder modules may refer to the exposed procedures of their module parameters; in principle, the available procedures of a module parameter are the ones defined in its module type. Otherwise, higherorder modules are nearly identical to regular modules; this is reflected in the typical form of their definitions, as depicted in the following snippet (compare this to the typical form of the definitions of regular modules and their types)^{1}.
module type HOMT(M1 : MT1, M2 : MT2, ..., Mn : MTn) = {
proc p(id1 : t1, id2 : t2, ..., idn : tn) : tout
(* ... Other procedure signatures ... *)
}.
module (HOM : HOMT) (M1 : MT1, M2 : MT2, ..., Mn : MTn) = {
var id : t
(* ... Other modulelevel variable declarations ... *)
proc p(id1 : t1, id2 : t2, ..., idn : tn) : tout = {
(* ... Implementation of procedure p (may call procedures of M1, ..., Mn) ... *)
}
(* ... Other procedure implementations (may call procedures of M1, ..., Mn) ... *)
}.
Here, notice the type denotation for HOM: it is given before the declaration of the module parameters. Intuitively, this is because, for the typing of modules, we consider the module parameters as "given" or "instantiated". Thus, HOM is only of type HOMT before the declaration of the module parameters, but not after; in fact, after the declaration of the module parameters, each of the parameters is considered "instantiated" (in terms of typing), and HOM is not of a functor type anymore. The following snippet attempts to illustrate this further.
module type HOMT(M1 : MT1, M2 : MT2, ..., Mn : MTn) = {
proc p(id1 : t1, id2 : t2, ..., idn : tn) : tout
}.
module type MT = {
proc p(id1 : t1, id2 : t2, ..., idn : tn) : tout
}.
module (HOM : HOMT) (M1 : MT1, M2 : MT2, ..., Mn : MTn) : MT = {
proc p(id1 : t1, id2 : t2, ..., idn : tn) : tout = {
(* ... Implementation of procedure p (may call procedures of M1, ..., Mn) ... *)
}
}.
Lastly, it is possible to partially apply functors from left to right—that is, only instantiate the first couple of parameters, but not all—producing a new functor (with the remaining noninstantiated module parameters as parameters). Nevertheless, it is only possible to refer to the procedures of fully applied functors; otherwise, procedures may not be welldefined (e.g., calling the procedure of a noninstantiated module parameter). The following snippet provides an example of partial functor application.
module (HOM : HOMT) (M1 : MT1, M2 : MT2, ..., Mn : MTn) = {
(* ... *)
}.
module M1 : MT1 = {
(* ... *)
}.
(* HON is a functor parameterized on modules of type MT2, ..., MTn, in that order. *)
module HON = HOM(M1).
Using this allows us, for example, to exactly capture the concept of a class of adversaries that expect access to an oracle(s) or to define reductions.
Probability Statements
Generically, a probability statement in EasyCrypt takes the form
Pr[M(N1, ..., Nl).p(e1, ..., en) @ &m : er]
, where M
is a module, Ni
(for i
in the range [1, l]
) is a module instantiating the i
th module parameter of M
(and so must be of the correct type), p
is a procedure defined in M
, ei
(for i
in the range [1, n]
) instantiates the i
th parameter of p
(and so must be of the
correct type), &m
is a memory (variable), and er
is a booleantyped expression that
may refer to the return value of M(N1, ..., Nn).p(e1, ..., en)
through the keyword
res
. Intuitively, such a probability statement denotes "the probability that after
executing M(N1, ..., Nn).p(e1, ..., en)
, starting from memory &m
, er
evaluates to
true".
Footnotes

As you can see, the syntactical differences between a functor type and a (nonfunctor) module type are analogous to those between a functor and a (nonfunctor) module: A functor type is written down as a (nonfunctor) module type with additional typed module parameters between the name and the
=
symbol. ↩