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 space-separated 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 annotation-like 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 module-level 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 module-level 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;, where id is the identifier of the variable and type 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.

  if (e) {
    (* ... Code of then-branch ... *)
  } else {
    (* ... Code of else-branch ... *)
  }
  The else part of the statement is optional, meaning that the following also constitutes a valid if statement.

  if (e) {
    (* ... Code of then-branch ... *)
  }
  These statements have the usual interpretation: if e evaluates to true, execute the code in the then-branch; else, if e evaluates to false, execute the code in the else-branch (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.

  while (e) {
    (* ... Code of while-loop ... *)
  }
  These statements have the usual interpretation: as long as e evaluates to true, execute the code within the while-loop (where e is (re-)evaluated before each iteration).
• Regular assignments. These are statements of the form id <- e;, where id is the identifier of a variable and e 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;, where id is the identifier of a variable and d 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);, where id is the identifier of a variable, M is the identifier of a (previously specified) module, p is the identifier of a procedure of M, and each ei is an expression written in EasyCrypt's expression language that evaluates to a value of the type of the corresponding parameter of M.p (these are ordered).
• Return statements. These are statements of the form return e, where e 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.

Higher-Order 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 higher-order 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 higher-order 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, higher-order 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)¹.

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 module-level 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 non-instantiated module parameters as parameters). Nevertheless, it is only possible to refer to the procedures of fully applied functors; otherwise, procedures may not be well-defined (e.g., calling the procedure of a non-instantiated 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 boolean-typed 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

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