% !TeX root = easycrypt.tex

\chapter{Writing Specifications\label{chap:theories}}
The definitions and lemmas one writes and proves in \EasyCrypt can be grouped
into theories.

These can then be imported, exported and reused following the
requirements of each particular proof. \EasyCrypt supports user-defined
\emph{types} and \emph{operators} (Section~\ref{sec:types}) and
\emph{distributions} (Section~\ref{sec:distributions}). These definitions can
then be used to write \emph{modules} and \emph{functors}
(Section~\ref{sec:modules}) modelling games, experiments, schemes and
adversaries. Powerful refinement mechanisms can be used to instantiate theories
with concrete parameters (constant, types or functions), allowing a certain
degree of proof reuse (Section~\ref{sec:cloning}).


\section{Defining Mathematical Functions\label{sec:types}}
At the core of any \EasyCrypt specification is a collection of types and functions
over those types. Formally, \EasyCrypt types are \emph{non-empty} sets of
values, and functions (or operators) are \emph{mathematical} functions between
them. (By mathematical, we mean total, deterministic and pure.)

The \EasyCrypt type system supports polymorphic, higher-order types: the type of
lists can be declared independently of the type of their contents, and operators
can take and return other operators. We first describe the various built-in
types and relevant operators before moving on to explaining how new definitions
can be built from them.

\warningbox{Although \EasyCrypt provides a wide variety of constructs, one may
still want to define functions axiomatically. (For example, so that they are
only partially specified.) In such a case, it is important to keep in mind that
\EasyCrypt functions are \emph{always} total, deterministic and pure. This
should \emph{never} be contradicted by user-provided axioms.}

\subsection{Built-Ins}
The language is equipped with a few built-in types:
\begin{itemize}\itemsep-.5em
\item the \rawec{unit}\index{easycrypt}{types!unit@\ec{unit}} type, which
        contains a unique element
        \rawec{tt} (or \rawec{()}) \index{easycrypt}{operators!unit_tt@\ec{tt: unit}}%
\index{easycrypt}{operators!unit_tt@\ec{():unit}}),
\item the \rawec{bool} type of booleans,
\item the \rawec{int} type of arithmetic integers (in $\mathbb{Z}$),
\item the \rawec{real} type of real numbers (in $\mathbb{R}$).
\end{itemize}

Further symbols are defined or declared in the corresponding libraries, and are
discussed further in the library documentation.

\subsubsection*{The \rawec{bool} type}
\index{easycrypt}{types!bool@\ec{bool}}
Boolean expression terms can be built from the constants
\rawec{true}\index{easycrypt}{operators!boolc_true@\ec{true: bool}} and
\rawec{false}\index{easycrypt}{operators!boolc_false@\ec{false: bool}}, in combination
with operators for logical conjunction and disjunction
(\rawec{/\\}\index{easycrypt}{operators!boolo_and@\ec{(/\\): bool -> bool -> bool}} and
\rawec{\\\/}\index{easycrypt}{operators!boolo_or@\ec{(\\/): bool -> bool -> bool}}),
short-circuiting conjunction and disjunction
(\rawec{\&\&}\index{easycrypt}{operators!boolo_anda@\ec{(&&): bool -> bool -> bool}}
and
\rawec{||}\index{easycrypt}{operators!boolo_ora@\ec{(''ora): bool -> bool -> bool}}),
and xor
(\rawec{\^\^}\index{easycrypt}{operators!boolo_xor@\ec{(\^\^): bool -> bool -> bool}}).
Basic lemmas are made available in the \rawec{Bool} theory, although we mostly
rely on \SMT solvers to discharge boolean proof obligations.

\subsubsection*{The \rawec{int} type}
\index{easycrypt}{types!int@\ec{int}}
Integer expression terms can be built from arbitrary numerical constants, in
combination with operators for unary negation (\rawec{-}), and all arithmetic
and comparison (\rawec{+}, \rawec{-}, \rawec{*}, \rawec{/}, \rawec{\%},
\rawec{^}, \rawec{=}, \rawec{<}, \rawec{<=}, \rawec{>}, \rawec{>=} \ldots).
Since this type is identified with the \WhyThree type of integers, all \WhyThree
lemmas on it can be used by the \SMT solvers to reason about integers. The
\rawec{Int} library provides uniformly named wrappers and algebraic structures
for use in interactive proofs.

\subsubsection*{The \rawec{real} type}
\index{easycrypt}{types!real@\ec{real}}
Real expression terms can be built from integer constants suffixed with a
\rawec{\%r} (for example, \rawec{0\%r} is 0 in the \rawec{real} type), in
combination with the same operators available on integers. This type is
identified with the \WhyThree type of reals, which provides some lemmas and
tighter integration with the underlying theories, but \SMT solvers often have
very limited support for real numbers and will often fail to prove seemingly
trivial results. We are working on enriching the library of lemmas available
in this theory to allow more complex interactive proofs if (or rather, when)
automation fails.

\warningbox{\rawec{(1/2)\%r} and \rawec{1\%r/2\%r} are very different
expressions. The former evaluates to $0$ (the division is in $\mathbb{Z}$, and
the result ($0$) is interpreted in $\mathbb{R}$) whereas the latter evaluates to
$0.5$ (the operands are interpreted and the operator is applied in
$\mathbb{R}$). Eventually, we will introduce notations for scoping that should
allow less cluttered real expressions.}

\subsection{Writing functions}
From these base types and values, many more can be built. \EasyCrypt allows the
user to declare  (polymorphic) abstract types, and combine existing types into
inductive datatypes, record types, tuple types or function types, as well as to
construct typed values.

\subsubsection*{Tuple types}
Given two types \ec{'t} and \ec{'t'},
\ec{('t * 't')}\index{easycrypt}{types!prod@\ec{'a * 'b}}
(or \ec{'t *'t'}, whenever possible) denotes the type of pairs of elements of
\ec{'t} and \ec{'t'}. More generally, the product can be iterated to produce
tuple types of arbitrary arity. For example, Listing~\ref{lst:tuples} declares
two abstract types, \ec{pkey} and \ec{skey}, and then defines the type
\ec{keypairs} as the type of pairs of elements of \ec{pkey} and \ec{skey}.

\warningbox{Types \ec{'t * 't' * 't''}, \ec{('t * 't') * 't''} and
\ec{'t * ('t' * 't'')} are distinct (but isomorphic). This may cause confusing
error messages.}

\begin{easycrypt}[label={lst:tuples}]{A simple tuple type.}
type pkey.
type skey.

type keypair = pkey * skey.
\end{easycrypt}

Values of tuple types are constructed using a comma. For example, given two
values \ec{pk:pkey} and \ec{sk:skey}, one can simply define the key pair
\ec{kp:keypair = (pk,sk)}.

\subsubsection*{Inductive datatypes}
The following type definition defines a polymorphic type for lists: for any
base type \ec{'a}, one can build a list over \ec{'a} from the constant
constructor \ec{Nil}, and the binary constructor \ec{Cons} that prepends a
value of type \ec{'a} to a list over \ec{'a}.

\begin{easycrypt}[label={lst:inductive}]{A simple inductive type.}
type 'a list = [
  | Nil
  | Cons of 'a & 'a list ].
\end{easycrypt}

Defining an inductive datatype $\tau$ automatically generates a recursor
$\tau$\ec{_rect}, an induction principle $\tau$\ec{_ind} and a case distinction
lemma $\tau$\ec{_case} for use in further definitions and proofs. For example,
Listing~\ref{lst:derived_ind} displays these three generated definitions for the
type of lists defined in Listing~\ref{lst:inductive}.

\begin{easycrypt}[label={lst:derived_ind}]{Generated entities for polymorphic lists.}
fun list_rect (v:'b) (f:'a -> 'a list -> 'b -> 'b) (xs:'a list) =
  with xs = Nil        => v
  with xs = Cons x xs => f x xs (list_rect v f xs).

lemma list_ind (p:'a list -> bool):
  p Nil =>
  (forall x xs, p xs => p (Cons x xs)) =>
  (forall xs, p xs).

lemma list_case (p:'a list -> bool):
  p Nil =>
  (forall x xs, p (Cons x xs)) =>
  (forall xs, p xs).
\end{easycrypt}

Keep in mind that all types must be inhabited, and some type definitions may be
rejected by \EasyCrypt when \WhyThree fails to prove that they are not empty. In
general, any inductive definition that has at least one non-recursive
constructor will be accepted. Constructors can be applied partially.

Function \ec{list_rect} in Listing~\ref{lst:derived_ind} illustrates the
definition of a fixpoint (inductive function) by simple pattern-matching and
induction. Pattern-matching can be applied to tuples as well, but must be
exhaustive. In addition to the exhaustivity check, \WhyThree checks that the
fixpoint exists by requiring that all inductive calls are made on strict
subterms of the argument.

\subsubsection*{Record types}
Record types (or structure types) can be defined by listing the field names and
their types, as illustrated in Listing~\ref{lst:records}.

\begin{easycrypt}[label={lst:records}]{A simple record type.}
type intpoint = { x:int; y:int; }.
\end{easycrypt}

Record values can be constructed by assigning all fields, as illustrated in
Listing~\ref{lst:recordvalues}, and fields can be accessed using the
illustrated notation.

\begin{easycrypt}[label={lst:recordvalues}]{Simple record values.}
op origin = {| x = 0; y = 0; |}.

op x_coord (p:intpoint) = p.`x.
\end{easycrypt}

\subsubsection*{Function types}
\index{easycrypt}{types!function@\ec{'a -> 'b}}

\subsubsection*{On currying}
It is standard practice to write functions of several arguments in curried form,
where applying the function symbol to the first argument returns a function that
takes the second argument, and so on. This very easily allows the user to
partially apply functions to fix some of their arguments. This does not restrict
or increase the expressivity of the language in any way, although it may
initially cause some syntax issues for users unfamiliar with the concept. When
applying a curried function to several arguments, the arguments should be
separated by spaces rather than the more standard commas.
Listing~\ref{lst:currying} illustrates this.

\begin{easycrypt}[label={lst:currying}]{Currying and partial function application.}
fun log: int -> int -> int.
fun log2: int-> int = log 2.

fun log_pair: (int * int) -> int.
fun log2_pair (n:int): int = log (2,n).
\end{easycrypt}

The \rawec{log} is declared as an integer function of two (curried) integer
arguments, and the log base 2, \rawec{log2}, is defined as its partial
application to 2. This definition could have been equivalently written as
\begin{easycrypt}[frame=none]{}
op log2 (n:int): int = log 2 n.
\end{easycrypt}
or
\begin{easycrypt}[frame=none]{}
op log2: int = fun (n:int), log 2 n.
\end{easycrypt}
Contrasting with the curried form described above, \rawec{log_pair} is declared
as an integer function of a single argument (whose type is a pair type).
Partial application is slightly more verbose, but the syntax of application may
look more familiar to imperative programmers.

\subsubsection*{Infix\index{easycrypt}{infix} and mixfix\index{easycrypt}{mixfix} operators}
Binary operators can be declared in infix form by parenthesizing their name when
the desired infix symbol starts with \ec{+}, \ec{:}, \ec{^}, \ec{@} or \ec{*}. (In the
latter case, spaces may be needed to avoid parsing part of the operator
declaration as a comment separator.) Once the infix symbols are declared, they
can simply be used as desired. However, the priorities and associativity of
user-defined infix operators are fixed by the syntax. In the absence of a
reference manual detailing these priorities, we recommend parenthesizing when
in doubt. Infix operators can be used in prefix form by wrapping them in
parentheses.

In addition, \EasyCrypt supports some built-in mixfix notations. They can be
used by replacing the \ec{_} symbols with parameters, or in prefix form by
wrapping them in double quotes. We list the available mixfix notations below.
\begin{itemize}\itemsep-.5em
\item \rawec{[]}, can represent, say, empty collections;
\item \rawec{[_]}, can represent, for example, singleton collections;
\item \rawec{_.[_]}, can be used to denote getting an element from an indexed
  collection (it expects at least a binary definition);
\item \rawec{_.[_ <- _]}, can be used to denote updating one element of an
  indexed collection (it expects at least a ternary definition).
\end{itemize}

\section{Probabilistic Expressions\label{sec:distributions}}

\EasyCrypt features a polymorphic type
\rawec{'a distr}\index{easycrypt}{types!distr@\ec{'a distr}} of
\emph{discrete sub-distributions} over a base type \rawec{'a}. The primary
operation over sub-distributions is the function
\rawec{op mu (d:'a distr) (E:'a -> bool): real.}%
\index{easycrypt}{operators!mu@\ec{mu: 'a distr -> ('a -> bool) -> real}},
which measures the probability of event \ec{E} in distribution \ec{d}.
Function \rawec{mu} is assumed to satisfy the following axioms:
\begin{itemize}\itemsep-.5em
\item probabilities lie in the unit interval;\\
  \ec{axiom mu_unit d E: 0\%r <= mu d E <= 1\%r.}
\item the probability of the constantly false predicate \ec{False} is null;\\
  \ec{axiom mu_false d: mu d False <= 0\%r.}
\item probabilities are monotonic with respect to event inclusion;\\
  \ec{axiom mu_leq d E E': E <= E' => mu d E <= mu d E'.}
\item any event whose probability is that of the constantly true event
  \ec{True} contains the distribution's support;\\
  \ec{axiom mu_supp d E: mu d E = mu d True => support d <= E.}
\item the probability of a union of events is equal to the sum of
  their probabilities, minus the probability of their intersection;\\
  \ec{axiom mu_or d E E': mu d (E \\/ E') = mu d E + mu d E' - mu d (E /\\ E').}
\item two sub-distributions are equal if and only if they are pointwise equal;
  \ec{axiom mu_pw d d': d == d' <=> d = d'.}
\end{itemize}

where the standard library \ec{Distr} defines, among other auxiliary operators,
\begin{easycrypt}[frame=none]{}
pred (==) (d d':'a distr) = forall x, mu d ((=) x) = mu d' ((=) x).

op support (d:'a distr) x = mu d ((=) x) <> 0%r.
\end{easycrypt}

Sub-distributions can be user-defined axiomatically, and no well-formedness
checks are performed. For example, the uniform distribution on booleans is
defined, in the standard library, as displayed in Listing~\ref{lst:dbool}, where
\rawec{charfun P x} is the characteristic function of \rawec{P} evaluated in
\rawec{x} (that is, \rawec{1\%r} if \rawec{P} holds on \rawec{x} and
\rawec{0\%r} otherwise).

\begin{easycrypt}[label={lst:dbool}]{[Uniform Boolean distribution]Defining the uniform distribution on booleans}
op dbool: bool distr.

axiom mu_def (p:bool -> bool):
  mu dbool p =
    (1%r/2%r) * charfun p true +
    (1%r/2%r) * charfun p false.
\end{easycrypt}

It is in fact fairly easy to check that the simple axiom from
Listing~\ref{lst:dbool} does indeed define a distribution, by proving the
following lemma, which can be discharged automatically.

\begin{easycrypt}[]{}
lemma lossless : mu dbool True = 1%r by smt.
\end{easycrypt}

However, the consistency of such axiomatic definitions needs to be carefully
checked and justified, just like any user-provided axiom. Once good axiomatics
definitions are given to a sufficient collection of primitive distributions, it
should be possible to define further distributions by applying distribution
transformers, properly defined as operators, to the core distributions.

For example, the standard library \ec{Pair} provides a distribution transformer
\rawec{(*): 'a distr -> 'b distr -> ('a * 'b) distr} that can be used to define
the uniform distribution on pairs of booleans, without adding any axioms to
\EasyCrypt. We also display a direct consequence of this definition.

\begin{easycrypt}[]{}
op dbpair = {0,1} * {0,1}.

lemma dbpair_x b b': mu dbpair ((=) (b,b')) = 1%r/4%r.
\end{easycrypt}

\section{\pWHILE, Modules and Functors\label{sec:modules}}
Although the languages for expressions and probabilistic expressions are quite
powerful, they fail to properly capture the kind of objects cryptographers
manipulate. \EasyCrypt uses the same language, \pWHILE, to describe
cryptographic schemes, oracles, and experiments, all represented as
\emph{modules}\index{easycrypt}{modules}.
Modules are wrappers that declare a collection of typed global variables and
define a set of imperative \emph{procedures} that may read and write
(amongst other things) the module's global state. We first briefly describe the
\pWHILE language before giving an overview of the two main mechanisms for
module composition: direct usage and functor application.

\subsection{The \pWHILE language}
\pWHILE procedures are composed of a set of typed local variables and a
sequence of statements that include:
\begin{itemize}\itemsep-.5em
\item assignment of an expression to a local or global variable,
\item assignment of the result of a function call (on expressions) to a local
  or global variable,
\item assignment of a freshly sampled random value to a local or global
  variable,
\item conditional branching,
\item looping (only in the form of \rawec{while} loops),
\item return statements.
% missing things?
\end{itemize}
Unless the return type of the function is \rawec{unit}, the final statement in
the function's body needs to be a \rawec{return} (and a \rawec{return}
statement can only be the last statement in a procedure's body).

Listing~\ref{lst:pWhile} shows a module implementing a random oracle where the
number of queries is bounded and the responses are sampled (but not assigned to
any particular queries) during initialization. In this display, we use the type
\rawec{word} to model bitstrings of an arbitrary but fixed length, and
\rawec{dword} to model the uniform distribution on words. Random sampling is
denoted by preceding a distribution with the \textsf{\$} symbol. Note that
complex update statements are available for any type for which a mixfix set
operator is defined. In this example, the map \ec{mG} is updated at location
\ec{x} using a statement of the form \ec{mG.[x] = v}.

\begin{easycrypt}[label={lst:pWhile}]{Example of a module}
module RO_E = {
  var tape: word list
  var mG: (word,word) map

  fun init():unit = {
    var r:word;
    tape = [];
    mG = empty;
    while (`|tape| < qG)
    {
      r = $dword;
      tape = r :: tape;
    }
  }

  fun h(x:word): word = {
    var r:word;
    var res:word;
    if (`|tape| <> 0)
    {
      if (!in_dom x mG)
        mG.[x] = hd tape;
      res = mG.[x];
      tape = tl tape;
    }
    else
      res = zeros;
    return res;
  }
}.
\end{easycrypt}

The return type for procedures, as well as the types of local variables can be
inferred automatically by \EasyCrypt.

%
%\subsection{Module Signatures}
%We first formally define the functionalities a random oracle is expected to
%provide, as a \emph{module type}, or \emph{signature}
%(Listing~\ref{lst:modulesig}). Any module implementation \rawec{M} that provides
%\emph{at least} the functions from a module type \rawec{Mt} is said to be of
%type \rawec{Mt} (denoted \rawec{M :> Mt}). Module types cannot specify state
%directly. Instead, if a global variable of the module should be exposed to the
%outside, getter and setter functions can be added to the module signature.
%
%\begin{easycrypt}[label={lst:modulesig}]{[A signature for random oracles]A signature for random oracles from bitstrings to bitstrings}
%module type RO = {
%  fun init():unit
%  fun h(x:bitstring):bitstring }.
%\end{easycrypt}
%
%Such a module signature can then be given various realizations. For example, Listing~\ref{lst:modules} shows two possible realizations of a random oracle, both of which assume a positive integer constant \rawec{qH}, used to bound the number of calls to the oracle, and two positive integer constants \rawec{inLen} and \rawec{outLen} representing the input and output lengths of the random oracles.
%
%%% The following is probably the single most disgusting thing I've ever typeset in Latex... and I've done ugly things.
%\begin{minipage}{\textwidth}
%\hrule
%\begin{multicols}{2}
%\begin{easycrypt}[frame=none,xleftmargin=0pt,xrightmargin=0pt]{}
%module RO_L: RO = {
%  var cG: int
%  var mG: (bitstring,bitstring) map
%
%  fun init() = {
%    mG = empty;
%    cG = 0;
%  }
%
%  fun h(x:bitstring) = {
%    var r:bitstring;
%    var res:bitstring = empty;
%    if (length x = inLen && cG < qG)
%    {
%      cG = cG + 1;
%      r = $dbitstring(outLen);
%      if (!mem(x,dom mG)) mG[x] = r;
%      res = mG[x];
%    }
%    return res;
%  }
%}.
%\end{easycrypt}
%\columnbreak
%\begin{easycrypt}[frame=none,xleftmargin=0pt,xrightmargin=0pt]{}
%module RO_E: RO = {
%  var tape: bitstring list
%  var mG: (bitstring,bitstring) map
%
%  fun init() = {
%    var r:bitstring;
%    tape = [];
%    mG = empty;
%    while (length tape < qG)
%    {
%      r = $dbitstring(outLen);
%      tape = r :: tape;
%    }
%  }
%
%  fun h(x:bitstring) = {
%    var r:bitstring;
%    var res:bitstring = empty;
%    if (length x = inLen &&
%       length tape <> 0)
%    {
%      r = hd tape;
%      if (!mem(x,dom mG))
%        mG[x] = r;
%      res = mG[x];
%      tape = tl tape;
%    }
%    return res;
%  }
%}.
%\end{easycrypt}
%\end{multicols}
%\hrule
%\begin{easycrypt}[frame=non,xleftmargin=0pt,xrightmargin=0pt,label={lst:modules}]{[Two random oracles]Two possible implementations of module type \rawec{RO}}
%\end{easycrypt}
%\end{minipage}
%
%\subsection{Functors and Oracle Annotations}
%Modules can in fact be specified as functors, parameterized by other modules
%whose functions can be accessed as oracles. For example, the signature shown in
%Listing~\ref{lst:functorsig} describes a class of modules that are given access
%to a random oracle but whose unique function can in fact only call the \rawec{h}
%function provided by the parameter.
%
%\begin{easycrypt}[label={lst:functorsig}]{[A functor signature]A functor signature}
%module type RO_adv(O:RO) = {
%  fun a(): bool { O.h }
%}.
%\end{easycrypt}

\subsection{Module types}
Modules can be abstracted as module types, that hide details of the module's
internal state and implementation, and listing only some of the procedures the
module provides. For example, the \rawec{RO_E} module from
Listing~\ref{lst:pWhile} can be typed with both of the signatures given in
Listing~\ref{lst:signatures}. In the first signature, which could for example
be used by an experiment, the \rawec{\{*\}}  annotation on \rawec{init}
indicates that this function serves as initialization function and may be called
(in relational proofs) in desynchronized states.

\begin{easycrypt}[label={lst:signatures}]{Examples of module signatures.}
module type RO = {
  fun init(): unit {*}
  fun h(x:word): word
}.

module type ARO = {
  fun h(x:word): word
}.
\end{easycrypt}

For a module to provide a signature, it needs to provide an implementation of
all the listed functions \emph{with the same names, types, and formal
parameters}.

\warningbox{Error messaging for module typing may still be a bit obscure, and
some of the typing constraints---in particular the one concerning the naming of
formal parameters---can easily be overseen. These constraints will hopefully
make sense by the end of this Chapter, after discussions on module
quantification.}

Module type information, although it can be listed after a module's name in the
manner of a type annotation (for example,
\rawec{module RO_E: RO, ARO = \{...\}}.) is not attached to the module itself.
Instead, it is checked whenever a module is instantiated that it provides the
expected interface.

\subsection{Accessing module state}
A module can directly access the state of any other module that is currently in
scope. For example, the definitions listed in Listing~\ref{lst:dependencies} is
perfectly valid, and can in fact be used to model memory sharing and simplify
definitions.

\begin{easycrypt}[label={lst:dependencies}]{Memory accesses}
module Mem = {
  var c: int
}.

module Counter = {
  fun get(): int = {
    return Mem.c;
  }

  fun incr(): unit = {
    Mem.c = Mem.c + 1;
  }
}.
\end{easycrypt}

When such access exists, we say that a module \emph{depends} on another module.
(In Listing~\ref{lst:dependencies}, \rawec{Counter} depends on \rawec{Mem}.)

\subsection{Modelling oracle access}

\begin{itemize}
\item Functors
\item Functor signatures, oracle access restrictions
\end{itemize}

\section{Writing Axioms and Lemmas}
We now know how to define mathematical functions and types, and how to describe
schemes, oracles, experiments and games. We now briefly present the language of
formulas on those objects. The tools to prove such lemmas are presented in
Chapter~\ref{chap:tactics}.

\subsection{Simple Lemmas\label{sec:ec-specifics}}
Using these symbols, and since functions are values, one can express complex
logical formulas in higher-order logic, that can then be wrapped into
predicates, lemmas or axioms. We call this fragment of our logic that only
deals with operators the \emph{ambient logic}. Listing~\ref{lst:formulas}
displays a possible definition for a commutativity predicate on internal
operators, and expresses the fact that integer addition is commutative by
applying it. We also display a simple proof using the \rawec{smt} tactic, which
simply asks the SMT solvers to discharge the lemma.

\begin{easycrypt}[label={lst:formulas}]{Examples of ambient formulas: predicates and lemmas}
pred commutative (ope: 'a -> 'a -> 'b) =
  forall x y, ope x y = ope y x.

lemma addiC: commutative Int.(+) by smt.
\end{easycrypt}

Any lemma or axiom that starts with universal quantifiers can instead be
parameterized by those quantified variables. This does not change the semantics,
but may make proofs slightly more elegant. For example, the two lemmas below
are strictly equivalent.\footnote{To as lesser extent, this trick also works on
predicate definitions, although it changes the predicate's type. The reader
familiar with \Coq may not see this as a problem.}
\begin{easycrypt}[label={lst:formulas}]{Examples of ambient formulas: predicates and lemmas}
lemma xorbC: forall (b b' : bool), b ^^ b' = b' ^^ b.

lemma xorbC' (b b' : bool): b ^^ b' = b' ^^ b.
\end{easycrypt}

\subsection{Lemmas on Procedures}
We are interested in three kinds of judgements about programs:
\begin{itemize}\itemsep-.5em
\item Standard Hoare logic judgements, consisting of two predicates over
  memories: a precondition and a postcondition;
\item Probabilistic Hoare logic judgements, consisting of two predicates over
  memories, a relation on reals, and a real bound lying in the unit interval;
\item Probabilistic relational Hoare logic judgements, consisting of two
  relations on memories.
\end{itemize}
This section informally describes their syntax and semantic interpretations.
We leave formal definitions to a future reference manual. They can also be
found in \CertiCrypt-related documents.

\warningbox{In the following, note the distinct implication symbols.
$\Rightarrow$ is implication in the ambient logic (corresponding to the
\rawec{=>} predicate), whereas $\Longrightarrow$ is used to express contracts on
functions (corresponding to \rawec{==>} in raw \EasyCrypt code).}

\subsubsection*{(Possibilistic) Hoare Judgements}
Given a statement $\mathsf{c}$ and two predicates $\pre$ and $\post$ on
memories, judgement \[\Hoare{c}{\pre}{\post}\] means that for any memory
$\mathsf{m}$ such that $\pre\ \mathsf{m}$ and any memory $\mathsf{m'}$ that may
be obtained by executing $\mathsf{c}$ in $\mathsf{m}$, $\post\ \mathsf{m'}$.

In \EasyCrypt, such judgments are written as follows:
\begin{easycrypt}[frame=none]{}
hoare [c: pre ==> post]
\end{easycrypt}

\subsubsection*{Probabilistic Hoare Judgements}
Given a statement $\mathsf{c}$, two predicates $\pre$ and $\post$ on
memories, a relation $\mathfrak{R} \in \left\{=,\leq,\geq\right\}$ and a real bound $\delta$,
judgement \[\Hoare{c}{\pre}{\post} \mathrel{\mathfrak{R}} \delta\] means that for
any memory $\mathsf{m}$ such that $\pre\ \mathsf{m}$ the probability that
$\post$ holds after executing $\mathsf{c}$ in $\mathsf{m}$ is related to
$\delta$ by $\mathfrak{R}$.

In \EasyCrypt, such judgments are written as follows:
\begin{easycrypt}[frame=none]{}
phoare [c: pre ==> post] R d
\end{easycrypt}

\subsubsection*{Relational Hoare Judgements}
Given two statements $c_1$ and $c_2$ and two relations $\pre$
and $\post$ on pairs of memories, judgment
\[\Equiv{c_1}{c_2}{\pre}{\post}\]
means that for any memories $\mathsf{m_1}$ and $\mathsf{m_2}$ such that
$\pre\ \mathsf{m_1}\ \mathsf{m_2}$, then $c_1$ terminates on $\mathsf{m_1}$
exactly when $c_2$ terminates on $\mathsf{m_2}$, and for any resulting pair of
memories $\mathsf{m_1'}$ and $\mathsf{m_2'}$, we have
$\post\ \mathsf{m_1'}\ \mathsf{m_2'}$.

In \EasyCrypt, such judgments are written as follows:
\begin{easycrypt}[frame=none]{}
equiv [c1 ~ c2: pre ==> post]
\end{easycrypt}

\subsubsection*{Probabilities of Events}
Given a procedure $\mathsf{f}$, well-typed inputs x to $\mathsf{f}$, a memory
$\mathsf{m}$ and a boolean formula $\mathsf{E}$ that may refer to the global
state of any module in scope or to the special variable \ec{res},
the \EasyCrypt expression \ec{Pr[f(x) \@ \&m: E]} is the probability of event
$\mathsf{E}$ after executing $\mathsf{f}$ on $\mathsf{x}$ in initial memory
$\mathsf{m}$.

\subsubsection*{Simplified Notations for Lemmas on Procedures}
The \ec{hoare}, \ec{phoare} and \ec{equiv} keywords can be used in place of
\ec{lemma}, whenever the lemma is an unconditional judgment of the appropriate
form. In such a case, the square brackets are omitted, as illustrated in the
following listing, showing two equivalent notations for a \pRHL lemma.
(Note that universal quantifications can still be made.)

\begin{easycrypt}{}
lemma G0_G1_E (A <: Adv):
  equiv [G0(A).main ~ G1(A).main: true==> ={res}].

equiv G0_G1_E' (A <: Adv):
  G0(A).main ~ G1(A).main: true ==> ={res}.
\end{easycrypt}

\section{The Ambient Logic}
As an important step towards writing modular proofs, all the logical judgments
described above can be interpreted as valid expressions in an all-encompassing
\emph{ambient logic}. In particular, equivalences, probability bounds and Hoare
judgments can be used as premises in theorems, making it possible to express
complex abstract results that can then be applied to concrete schemes.
In addition, probability expressions using \ec{Pr} can be used as real-valued
expressions in other formulas.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "easycrypt"
%%% End: