path: root/tfm.tex

\documentclass[12pt,a4paper,parskip=full]{scrreprt}
%\usepackage{scrhack} % http://tex.stackexchange.com/questions/51867/koma-warning-about-toc

\usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry}

% \usepackage[spanish]{babel}
\usepackage{lmodern}
\usepackage{fontspec} \setmonofont{DejaVu Sans Mono}
\usepackage{url}
\usepackage{graphicx} \usepackage{cite} \usepackage{amsmath}
\usepackage{mathtools} \usepackage{listings} \usepackage{syntax}
% \usepackage[compact,small]{titlesec}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage[backref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref}
\usepackage{perpage} \usepackage{subcaption}

\usepackage{tikz}
\usepackage{amssymb} % arrows
\usepackage{mathpartir} % inference rules

\usepackage{minted}

\usepackage{float}
\floatstyle{boxed}
\newfloat{code}{th}{los}[chapter]
\floatname{code}{Code listing}

\usetikzlibrary{shapes,arrows}

\hypersetup{pageanchor=false}


\input{defs}
\input{ec-defs}
\input{front/front-init}

\MakePerPage{footnote}

\def\emptypage{\newpage\thispagestyle{empty}\mbox{}}

\begin{document}
\input{front/front-body}

\pagenumbering{roman}


\tikzstyle{block} = [rectangle, draw, fill=blue!20,
text width=5em, text centered, rounded corners, minimum height=4em]
\tikzstyle{invisbl} = [text width=5em, text centered, minimum height=4em]
\tikzstyle{line} = [draw, -latex']
\tikzstyle{cloud} = [draw, ellipse,fill=blue!10, node distance=3cm,
minimum height=2em]


\emptypage
\chapter*{Resumen}

La sociedad depende hoy más que nunca de la tecnología, pero la inversión en
seguridad es escasa y los sistemas informáticos siguen estando muy lejos de ser
seguros. La criptografía es una de las piedras angulares de la seguridad en este
ámbito, por lo que recientemente se ha dedicado una cantidad considerable de
recursos al desarrollo de herramientas que ayuden en la evaluación y mejora de
los algoritmos criptográficos. EasyCrypt es uno de estos sistemas, desarrollado
recientemente en el Instituto IMDEA Software en respuesta a la creciente
necesidad de disponer de herramientas fiables de verificación formal de
criptografía.

En este trabajo se abordará la implementación de una mejora en el reductor de
términos de EasyCrypt, sustituyéndolo por una máquina abstracta simbólica. Para
ello se estudiarán e implementarán previamente dos máquinas abstractas muy
conocidas, la Máquina de Krivine y la ZAM, introduciendo variaciones sobre ellas
y estudiando sus diferencias desde un punto de vista práctico.

\chapter*{Abstract}

Today, society depends more than ever on technology, but the investment in
security is still scarce and using computer systems are still far from safe to
use. Cryptography is one of the cornerstones of security, so there has been a
considerable amount of effort devoted recently to the development of tools
oriented to the evaluation and improvement of cryptographic algorithms. One of
these tools is EasyCrypt, developed recently at IMDEA Software Institute in
response to the increasing need of reliable formal verification tools for
cryptography.

This work will focus on the improvement of the EasyCrypt's term rewriting
system, replacing it with a symbolic abstract machine. In order to do that, we
will previously study and implement two widely known abstract machines, the
Krivine Machine and the ZAM, introducing some variations and studying their
differences from a practical point of view.

\emptypage
\tableofcontents

%% Content begins here
%
%% Level    | Spaces before | '%'s after
%  ---------+---------------+-----------
%  part     | 5             | until EOL
%  chapter  | 4             | 10
%  section  | 3             | 2
%  subs.    | 2             |
%  subsubs. | 1             |




\emptypage
\chapter{INTRODUCTION} %%%%%%%%%%

\pagenumbering{arabic}
\setcounter{page}{1}

In the last years, society is becoming ever more dependent on computer
systems. People manage their bank accounts via web, are constantly in touch with
their contacts thanks to instant messaging applications, and have huge amounts
of personal data stored in the \textit{cloud}. All this personal information
flowing through computer networks need to be protected by correctly implementing
adequate security measures regarding both information transmission and
storage. Building strong security systems is not an easy task, because there are
lots of parts that must be studied in order to assure the system as a whole
behaves as intended.




\section{Cryptography}

One of the most fundamental tools used to build security computer systems is
\textbf{cryptography}. As a relatively low-level layer in the security stack, it
is often the cornerstone over which all the system relies in order to keep being
safe. Due to its heavy mathematical roots, cryptography today is a mature
science that, when correctly implemented, can provide strong security guarantees
to the systems using it.

At this point, one could be tempted of just ``using strong, NIST-approved
cryptography'' and focusing on the security of other parts of the system. The
problem is that correctly implementing cryptography is a pretty difficult task
on its own, mainly because there is not a one-size-fits-all construction that
covers all security requirements. Every cryptographic primitive has its own
security assumptions and guarantees, so one must be exceptionally cautious when
combining them in order to build larger systems. A given cryptographic
construction is usually well suited for some kind of scenarios, and offers
little to no security otherwise. In turn, this can produce a false sense of
security, potentially worse that not having any security at all.




\section{Formal Methods} %%

In order to have the best guarantee that some cryptographic construction meets
its security requirements, we can use use formal methods to prove that the
requirements follow from the assumptions (scenario).

While mathematical proofs greatly enhance the confidence we have in that a given
cryptosystem behaves as expected, with the recent increase in complexity it has
become more and more difficult to write and verify the proofs by hand, to the
point of being practically non-viable. In the recent years there has been an
increasing effort in having computers help us write and verify this proofs.

There are various methods and tools for doing this, but one of the most
versatile and powerful are the \textbf{proof assistants}, which are tools
designed to help users develop formal proofs interactively. A proof assistant
usually follows the rules of one or more \textbf{logics} to derive theorems from
previous facts, and the user helps it by giving ``hints'' on how to
proceed. This is in contrast to some other theorem provers that use little or no
help from the user, making them easier to use but fundamentally more limited.
Coq\footnote{\url{http://coq.inria.fr/}} and
Isabelle\footnote{\url{http://isabelle.in.tum.de/}} are examples of widely used
proof assistants.

One downside of proof assistants is that they require a considerable amount of
knowledge from the user, making them difficult to use for people that is not
somewhat fluent with theoretical computer science and logic. This is a
significant obstacle to the application of this technologies to other scientific
fields that could benefit from adopting the formal methods approach to
verification.


\section{EasyCrypt}
\label{sec:easycrypt}

EasyCrypt \cite{BartheGHB11} is a toolset conceived to help cryptographers
construct and verify cryptographic proofs. It is an open source
project\footnote{\url{https://www.easycrypt.info}} being developed
currently at IMDEA Software Institute and Inria. It is the evolution of the
previous CertiCrypt system \cite{BartheGB09}.

EasyCrypt's works as an interpreter of its own \textbf{programming language}, in
which the programmer can express all that's needed in order to develop the
proofs. At every step of the evaluation, EasyCrypt can output some information
regarding the state of the system so that external tools can parse and show it
to the user. Together with the fact that the evaluation steps can be reversed,
this forms the basis of the interactivity of the EasyCrypt system: the user can
evaluate the program step by step, and if needed, undo it and re-evaluate in the
fly.

\begin{figure}[H]
  \centering
  \includegraphics[width=1\textwidth]{img/easycrypt.png}
  \caption{EasyCrypt}
  \label{fig:easycrypt}
\end{figure}

The preferred way of working with EasyCrypt is using the
\textbf{Emacs}\footnote{\url{http://www.gnu.org/software/emacs/}} text editor,
with the \textbf{Proof
  General}\footnote{\url{http://proofgeneral.inf.ed.ac.uk/}} interface to proof
assistants (figure \ref{fig:easycrypt}). This interface shows both the source
code and the EasyCrypt output at the point of evaluation (the already evaluated
code is displayed in a different color), and offers standard key combinations
for forward/backward code stepping.

As we'll see later (section \ref{sec:verif-easycrypt}), EasyCrypt has different
sub-languages for working with different things, e.g., representing games,
developing the proofs, etc. One of them is specially relevant in this thesis:
the \textbf{expression language}. It is the language EasyCrypt uses to define
typed values, like quantified formulas, arithmetic expressions, functions,
function application and such, and developing proofs relies heavily on the
manipulation of this expressions.



\section{Contributions} %%

In this work we will study and implement some well-known abstract machines to
improve the EasyCrypt's current term rewriting engine. As we will see in the
corresponding section (~\ref{cha:reduction-easycrypt}), the current
implementation is an ad-hoc solution that works well, but is monolithic,
difficult to extend and somewhat inefficient. Before that, we will introduce
some theory to the field of term rewriting and implement both the Krivine
Machine and the ZAM, as a way to understand their differences and which is the
best reference to improve the EasyCrypt's engine.





\part{STATE OF THE ART} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\chapter{CRYPTOGRAPHY} %%%%%%%%%%

In this chapter we will review some concepts related to how cryptographic proofs
are built, in order to understand how EasyCrypt works and how proofs are written
in it.

\section{Public-key Encryption} %%

Here we will introduce some basic concepts in asymmetric
cryptography, as they will be useful to understand the next sections on
EasyCrypt's proof system and sequences of games (section
\ref{sec:sequences-games}).

\textbf{Asymmetric cryptography} (also called \textbf{Public Key cryptography}),
refers to cryptographic algorithms that make use of two different keys, $pk$
(public key) and $sk$ (secret key). There must be some mathematical relationship
that allows a specific pair of keys to perform dual operations, e.g., $pk$ to
encrypt and $sk$ to decrypt, $pk$ to verify a signature and $sk$ to create it,
and so on. A pair of (public, secret) keys can be generated using a procedure
called \textbf{key generation} ($\KG$).

The encryption ($\Enc$) and decryption ($\Dec$) functions work in the
following way:

$$\Enc(pk,M) = C$$
$$\Dec(sk,C) = M$$

That is, a message ($M$) can be encrypted using a public key to obtain a
ciphertext ($C$). In turn, a ciphertext ($C$) can be decrypted using a private
key to obtain a message ($M$). Any \textbf{complete} encryption algorithm must
satisfy the following property, given that $pk$ and $sk$ were obtained by a call
to $\KG$:

$$\Dec(sk, \Enc(pk,M)) = M$$

\section{Proofs by reduction} %%
\label{sec:proofs-reduction}

In cryptography it is usually not possible to prove \textbf{perfect security},
as the only possible way to archieve it would be using keys as long as the
message (Shannon's theory of information). So, the usual approach is to prove
that some cryptographic protocol's security can be \textbf{reduced} to the
security of some well-known primitive that is believed to be
\textbf{computationally untractable}. That is, the security relies on the
unability of any human being to solve some computationally hard problem.  The
overall structure of this proofs is represented in the figure \ref{fig:proofs}.

\begin{figure}[ht]
  \centering
  \begin{tikzpicture}[node distance = 6cm, auto]
    % Nodes
    \node [block, fill=blue!40] (primitive) {Primitive};
    \node [block, below of=primitive, fill=blue!40] (scheme) {Scheme};
    \node [block, right of=primitive, fill=red!60] (attack1) {Attack};
    \node [block, right of=scheme, fill=red!60] (attack2) {Attack};
    % Edges
    \path [line,dashed] (attack1) -- (primitive);
    \path [line,dashed] (attack2) -- (scheme);
    \path [line]
    (primitive) edge node[left] {\textbf{Construction}} (scheme)
    (attack2) edge node[right] {\textbf{Reduction}} (attack1);
  \end{tikzpicture}
  \caption{Proofs by reduction}
  \label{fig:proofs}
\end{figure}

One of the most famous hard problems in cryptography is \textbf{integer
  factorization}. It can be proven that the computational power needed to factor
the product of two big primes grows exponentially on the size of the primes,
making it a practically impossible task to archieve for sufficiently big prime
numbers. The RSA cryptosystem, for example, can be proven secure because it can
be reduced to the integer factorization problem.

\section{Sequences of games} %%
\label{sec:sequences-games}

In 2004 \cite{Shoup04}, Victor Shoup introduced the concept of \textbf{sequences
  of games} as a method of taming the complexity of cryptography related
proofs. A \textbf{game} is like a program written in a well-defined,
probabilistic programming language, and a sequence of games is the result of
applying transformations over the initial one. Every game represents the
interaction between a \textbf{challenger} and an \textbf{adversary}, with the
last one being usually encoded as a function (probabilistic program). In the
end, we will want the sequence of games to form a proof by reduction (see
section \ref{sec:proofs-reduction}), where the transition of games proves that
our system can be reduced, under certain conditions, to some well-known
cryptographic primitive. We say that the adversary \textbf{wins} when certain
event takes place. It generally has to do with his capacity to extract some
information or correctly guess some data.

We can define the following game in order to see a practical example of how
sequences of games work:

\begin{game}[caption=IND-CPA game (from \cite{BartheGB09}),
  label={lst:indcpa}]{}
  $(pk,sk) \leftarrow \KG();$
  $(m_0,m_1) \leftarrow A_1(pk);$
  $b \overset{\$}{\leftarrow} \{0,1\};$
  $c \leftarrow \Enc(pk,m_b);\\$
  $\tilde{b} \leftarrow A_2(c)$
\end{game}

The game \ref{lst:indcpa}\footnote{$\KG$
  and $\Enc$
  are the key generation and encryption functions provided by the encryption
  algorithm, respectively, and $A_1$
  is the encoding of the adversary} can be used to define the IND-CPA property
of public key encryption schemes. \textbf{IND-CPA} (Indistinguishability Under
Chosen Ciphertext Attacks) means that the adversary is unable to distinguish
between pairs of ciphertexts. The IND-CPA game encodes this fact by letting the
adversary chose two messages, encrypting one of them, and making him guess which
one was encrypted. In this case, the event that makes the adversary win is that he
correctly guesses which of his plaintexts was encrypted. In a full sequence of
games, we would start with this game and apply transformations over it trying to
preserve the probability of that event (the adversary winning) constant. The
final game would hopefully be one in which the calls 






\section{Verification: EasyCrypt} %%
\label{sec:verif-easycrypt}

EasyCrypt allows the encoding and verification of game-based proofs, but it has
different languages to perform different tasks:


\subsection{Specification languages}

This are the languages EasyCrypt uses to declare and define types, functions,
axioms, games, oracles, adversaries and other entities involved in the proofs.

\subsubsection{Expressions}
\label{sec:expressions}

The main specification language of EasyCrypt is the expression language, in
which \textbf{types} are defined together with \textbf{operators} that can be
applied to them (or be constant). EasyCrypt follows the usual semicolon
notation\cite{Church40} to denote the typing relationship: <<$a : T$>> means
``$a$ has type $T$''. EasyCrypt has a type system supporting parametric
polymorphism: \rawec{int list} represents a list of integers.

The operators are functions over types, defined with the keyword \rawec{op}
(e.g., \\ \rawec{op even : nat -> bool}). An operator can be applied to some
argument by putting them separated by a space: \rawec{even 4}. Operators can be
abstract, i.e., defined without any actual implementation; with semantics given
by the definition of axioms and lemmas that describe its observational
behavior. Operators are also \textit{curried}, so they support multiple
arguments by returning new functions that consume the next one. For example,
$f : (A \times B\times C) \rightarrow D$ would be encoded as
$f : A \rightarrow (B \rightarrow (C \rightarrow D))$, or, by associativity,
$f : A \rightarrow B \rightarrow C \rightarrow D$.

In this example (from the current EasyCrypt library) we can see the how actual
types and operators are defined in the EasyCrypt's expression language:

\begin{easycrypt}[caption=Lists (expression language), label={lst:exprlang}]{}
type 'a list = [
  | "[]"
  | (::) of 'a & 'a list ].

op hd: 'a list -> 'a.
axiom hd_cons (x:'a) xs: hd (x::xs) = x.

op map (f:'a -> 'b) (xs:'a list) =
  with xs = "[]"      => []
  with xs = (::) x xs => (f x)::(map f xs).
\end{easycrypt}

The first line defines the \rawec{list} type as a sum type with two constructors
(cases): the \textit{empty list} and the \textit{construction} of a new list
from an existing one and an element that will appear at its head position. The
rest of the code defines operators working with lists.

The next line abstractly defines the operator \rawec{hd}, together with its
type. The axiom following it partially specifies the behavior of the \rawec{hd} when
applied to some list: if the list has the form \rawec{x::xs} (element \rawec{x}
followed by \rawec{xs}), the return value is \rawec{x}. The other case (empty
list) is left unspecified.

The last line defines the \rawec{map} operator directly, using pattern
matching. This operator receives a function and a list, and returns the list
consisting of the results of evaluating the function over each element of the
list, preserving its order.

\paragraph{Probabilistic expressions}

Additionally, EasyCrypt defines some standard types and operators to work with
probabilistic expressions. The type \rawec{'a distr} represents discrete
sub-distributions over types. The operator \rawec{mu} represents the probability
of some event in a sub-distribution:

\begin{easycrypt}[]{}
op mu : 'a distr -> ('a -> bool) -> real
\end{easycrypt}

For example, the uniform distribution over booleans is defined in the
EasyCrypt's standard library as follows:

\begin{easycrypt}[caption=Uniform distribution over bool,
  label={lst:booldistr}]{}
op dbool : bool distr.
axiom mu_def : forall (p : bool -> bool),
  mu dbool p =
    (1/2) * charfun p true +
    (1/2) * charfun p false.
\end{easycrypt}

\subsubsection{pWhile language}

Expression languages are usually not adequate to define games and other data
structures as cryptographic schemes and oracles, due to the stateful nature of
sequential algorithms. That's why EasyCrypt uses a different language
called \textbf{pWhile} \cite{BartheGB12} (probabilistic while) to define them:

\begin{bnf}[caption=pWhile language, label={lst:pwhile}]{}
  $\mathcal{C} ::=$ skip
    | $\mathcal{V \leftarrow E}$
    | $\mathcal{V \overset{\$}{\leftarrow} DE}$
    | if $\mathcal{E}$ then $\mathcal{C}$ else $\mathcal{C}$
    | while $\mathcal{E}$ do $\mathcal{C}$
    | $\mathcal{V} \leftarrow \mathcal{P}(\mathcal{E}, ..., \mathcal{E})$
    | $\mathcal{C}$; $\mathcal{C}$
\end{bnf}


\subsection{Proof languages}

% These are the languages used to write and prove theorems:

\subsubsection{Judgments}

Whenever there is some statement that we want to prove, it must be written as a
judgment in some \textbf{logic}. Apart from the first order logic expressions,
EasyCrypt supports judgments in some logics derived from Hoare logic:

\begin{itemize}
\item Hoare Logic (\textit{HL}). These judgments have the following shape:

  $$c : P \Longrightarrow Q$$

  where $P$ and $Q$ are assertions (predicates) and $c$ is a statement or
  program. $P$ is the \textbf{precondition} and $Q$ is the
  \textbf{postcondition}. The validity of this kind of Hoare judgment implies
  that if $P$ holds before the execution of $c$ and it terminates, then $Q$ must
  also hold.

\item Probabilistic Hoare Logic (\textit{pHL}). This is the logic resulting from
  assigning some probability to the validity of the previously seen Hoare
  judgments. The probability can be a number or an upper/lower bound:

  $$[c : P \Longrightarrow Q] \leq \delta$$
  $$[c : P \Longrightarrow Q] = \delta$$
  $$[c : P \Longrightarrow Q] \geq \delta$$

\item Probabilistic Relational Hoare Logic (\textit{pRHL}). These have the
  following shape:

  $$c_1 \sim c_2 : \Psi \Longrightarrow \Phi$$

  In this case, the pre and postconditions are not standalone predicates, but
  \textbf{relationships} between the memories of the two programs $c_1$ and
  $c_2$. This judgment means that if the precondition $\Psi$ holds before the
  execution of $c_1$ and $c_2$, the postcondition $\Phi$ will also hold after
  finishing its execution.

  This logic is the most complete and useful when developing game-based
  reduction proofs, because it allows to encode each game transition as a
  judgment. Twe two games are $c_1$ and $c_2$ respectively, and the
  pre/postconditions refer to the probability of the adversary winning the
  games.

\end{itemize}

\subsubsection{Tactics}

If the judgment is declared as an axiom, it is taken as a fact and does not need
to be proven. Lemmas, however, will make EasyCrypt enter in ``proof mode'',
where it stops reading declarations, takes the current judgment as a goal and
and starts accepting \textbf{tactics} until the current goal is trivially
true. Tactics are indications on what rules EasyCrypt must apply to transform
the current goal.

This is a simplified example of proof from the EasyCrypt's library, where we can
see the tactics applied between the \rawec{proof} and \rawec{qed} keywords:

\begin{easycrypt}[caption=Tactics usage, label={lst:tactics}]{}
lemma cons_hd_tl :
  forall (xs:'a list),
    xs <> [] => (hd xs)::(tl xs) = xs.
proof.
  intros xs.
  elim / list_ind xs.
  simplify.
  intros x xs' IH h {h}.
  rewrite hd_cons.
  rewrite tl_cons.
  reflexivity.
qed.
\end{easycrypt}





\chapter{TERM REWRITING} %%%%%%%%%%



\section{Introduction} %%

In computing and programming languages it is common to encounter scenarios where
objects (e.g., code) get transformed gradually for simplification, to perform a
computation, etc. The transformations must obey some rules that relate ``input''
and ``output'' objects, that is, how to make the transition from one object to
the other. When we take both the objects and the rules and study them as a
whole, the result is an \textbf{abstract reduction system} \cite{Baader98}.

This is a very general framework, but for what this work is concerned, we are
specially interested in reasoning about rewriting of ($\lambda$-)terms. In the
end we will want to improve how EasyCrypt is able to reduce terms in its
expression language, so we will start by understanding Lambda Calculus and how
it is reduced, because it is very similar to how EasyCrypt represents its own
terms.



\section{Lambda Calculus} %%

The \textbf{Lambda Calculus} \cite{Church36} is a formal system developed by
Alonzo Church in the decade of 1930 as part of his research on the foundations
of mathematics and computation (it was later proven to be equivalent to the
Turing Machine). In its essence, the Lambda Calculus is a simple term rewriting
system that represents computation through \textbf{function application}.

Following is the grammar representing \textbf{$\lambda$-terms} (lambda-terms,
$\mathcal{T}$):

\begin{bnf}[caption=Lambda Calculus, label={lst:lambda}]{}
  $\mathcal{T} ::= x$               variable
    | $(\lambda x . \mathcal{T})$           abstraction
    | $(\mathcal{T}_1 \: \mathcal{T}_2)$           application
  $x ::= v_1, v_2, v_3, ...$               (infinite variables available)
\end{bnf}

Intuitively, the \textbf{abstraction} rule represents function creation: take an
existing term ($\mathcal{T}$) and parameterize it with an argument ($x$). The
variable $x$ binds every instance of the same variable on the body, which we say
are \textbf{bound} instances. The \textbf{application} rule represents function
evaluation ($\mathcal{T}_1$) with an actual argument ($\mathcal{T}_2)$.

Seen as a term rewriting system, the Lambda Calculus has some reduction rules
that can be applied over terms in order to perform the computation.


\subsection{Reduction rules}

The most prominent reduction rule in Lambda Calculus is the \textbf{beta
  reduction}, or $\beta$-reduction. This rule represents function evaluation,
and can be outlined in the following way:

\[
  \inferrule* [left=$\beta$-red]
  { }
  {((\lambda x . \mathcal{T}_1) \: \mathcal{T}_2) \Betared \mathcal{T}_1[x :=
    \mathcal{T}_2]}
\]


An application with an abstraction in the left-hand side is called a
\textbf{redex}, short for ``reducible expression'', because it can be
$\beta$-reduced following the rule\footnote{The <<$\rightsquigarrow$>> symbol
  means ``reduces to'', and <<$\overset{\star}{\rightsquigarrow}$>> is its
  symmetric and transitive closure (``reduces in 0 or more steps to'')} . The
semantics of the rule match with the intuition of function application: the
result is the body of the function with the formal parameter replaced by the
actual argument. It has to be noted that even when a term is \textit{not} a
redex, it can contain some other sub-expression that indeed is; the problem of
knowing where to apply each reduction will be addressed in section
\ref{sec:reduction-strategies}.

The \textbf{substitution operation} $\mathcal{T}_1[x := \mathcal{T}_2]$ replaces
$x$ by $\mathcal{T}_2$ in the body of $\mathcal{T}_1$, but we have to be careful
in its definition, because the ``obvious/naïve'' substitution process can lead
to unexpected results. For example, $(\lambda x . y)[y := x]$ would
$\beta$-reduce to $(\lambda x . x)$, which is not the expected result: the new
$x$ in the body has been \textbf{captured} by the argument and the function
behavior is now different.

The solution to this problem comes from the intuitive idea that ``the exact
choice of names for bound variables is not really important''. The functions
$(\lambda x . x)$ and $(\lambda y . y)$ behave in the same way and thus should
be considered equal. The \textbf{alpha equivalence} ($\alpha$-equivalence) is
the equivalence relationship that expresses this idea through another rule: the
\textbf{alpha conversion} ($\alpha$-conversion). The basic definition of this
rule is the following:

\[
  \inferrule* [left=$\alpha$-conv]
  {y \notin \mathcal{T}}
  {(\lambda x . \mathcal{T}) \Alphared (\lambda y . \mathcal{T}[x := y])}
\]

So, to correctly apply a $\beta$-reduction, we will do \textbf{capture-avoiding
  substitutions}: if there is the danger of capturing variables during a
substitution, we will first apply $\alpha$-conversions to change the problematic
variables by fresh ones.

Another equivalence relation over lambda terms is the one defined by the
\textbf{eta conversion} ($\eta$-conversion), and follows by the extensional
equivalence of functions in the calculus:

\[
  \inferrule* [left=$\eta$-conv]
  {x \notin FV(\mathcal{T})}
  {(\lambda x . \mathcal{T} \: x) \Etabired \mathcal{T}}
\]


In general, we will treat $\alpha$-equivalent and $\eta$-equivalent functions as
interchangeable.


% \subsection{Types}

% Until now, we have been discussing the \textbf{untyped} Lambda Calculus, where
% there are no restrictions to the kind of terms we can build. Every formula
% resulting from the grammar (\ref{lst:lambda}) is a valid term. There are
% alternative interpretations of the Lambda Calculus, the \textbf{Typed Lambda
%   Calculi} \cite{Church40}, which give \textbf{typing rules} to construct
% ``well-typed terms'' (terms that have a \textbf{type} associated to it). The
% point is being unable to construct terms that ``make no sense'', like the ones
% that encode logical paradoxes or whose evaluation does not finish.




\section{Normal forms}

In abstract rewriting systems, a term $a$ is in \textbf{normal form} whenever it can
not be reduced any further. That is, there does not exist any other term $b$
such that $a \rightsquigarrow b$.

When a $\lambda$-term has no subexpressions that can be reduced, it is already
in normal form. There are also three additional notions of normal form in Lambda
Calculus:

\begin{itemize}
\item \textbf{Weak normal form}: $\lambda$-terms with form
  $(\lambda x . \mathcal{T})$ are not reduced
\item \textbf{Head normal form}: $\lambda$-terms with form $(x \: \mathcal{T})$
  are not reduced
\item \textbf{Weak head normal form}: neither $\lambda$-terms in weak or head
  normal form are not reduced
\end{itemize}

The Lambda Calculus is \textbf{not normalising}, so there is not any guarantee
that any normal form exists for a given term.



\section{Reduction Strategies} %%
\label{sec:reduction-strategies}

When reducing $\lambda$-terms, a \textbf{reduction strategy} \cite{Sestoft02} is
also needed to remove the ambiguity about which sub-expression on a given term
should be reduced next.  This is usually an algorithm that given some reducible
term (redex), points to the redex inside it that sould be reduced next.

Each reduction strategy knows when to stop searching based on some normal form
(of the four we've already seen).

Two of the most common reduction strategies, and the ones we will be more
concerned with in this work, are the following:

\begin{itemize}
\item \textbf{Call-by-name} reduces the leftmost outermost redex, unless it is
  in weak head normal form. Due to the head normal form, the evaluation is
  non-strict.
\item \textbf{Call-by-value} reduces the leftmost innermost redex, unless it is
  in weak normal form. The evaluation is strict.
\item \textbf{Applicative order} reduces the leftmost innermost redex, unless it is
  in normal form. The evaluation is strict.
\end{itemize}

The Lambda Calculus has an interesting property called \textbf{confluence}, that
means that whenever some term has more than one possible reduction, there exists
another term to which both branches will converge in the end:

\[
  \inferrule* [left=Confluence]
  {a \overset{\star}{\rightsquigarrow} b_1 \\ a \overset{\star}{\rightsquigarrow} b_2}
  {\exists c . (b_1 \overset{\star}{\rightsquigarrow} c \wedge
    b_2 \overset{\star}{\rightsquigarrow} c)}
\]

What this means is that the reduction order does not really matter unless one of
them leads to non-termination (an infinite chain). Non-strict strategies, such
as call-by-name, helps avoiding non-terminating reductions thanks to its head
normal form (which does not evaluate function arguments until needed).



\newpage
\section{Abstract Machines} %%

In order to actually implement the reduction over $\lambda$-terms, there are
some different ways with different advantages and drawbacks, the most
``extreme'' being direct interpretation of source code and compilation to native
instructions of a real machine.

An intermediate point is simulating an \textbf{abstract machine} to which we can
feed a sequence of instructions (requiring a previous compilation process) or
the original language itself if it is simple enough. This approach is useful
because it is more portable than native code generation while being more
efficient than plain interpretation.

There can be different abstracts machine for the same language, differing not
only in their implementation details but in the reduction strategies they
implement, so the output can also be different, with some machines implementing
\textbf{stronger} reductions than others (i.e., to normal form).

In the next part of the thesis we will study and implement two widely-known
abstract machines to reduce $\lambda$-terms, and improve the EasyCrypt current
reduction machinery by applying the same concepts.



\part{IMPLEMENTATION} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\chapter{KRIVINE MACHINE} %%%%%%%%%%

To begin our study of the implementation of abstract machines, we will start
with the Krivine Machine. It is a relatively simple and well-known model that
will help us see the steps that we need to take in order to implement a real
abstract machine. We will be using the OCaml language from now on (not only in
this section but also in the next ones), and while snippets of code will be
presented to illustrate the concepts, the full code is available in the
annex \ref{sec:kriv-mach-source} for reference.

The Krivine Machine \cite{Krivine07} is an implementation of the weak-head
call-by-name reduction strategy for pure lambda terms. What that means is that:

\begin{itemize}
\item The Krivine Machine reduces pure (untyped) terms in the Lambda Calculus
\item The reduction strategy it implements is call-by-name, reducing first the
  leftmost outermost term in the formula
\item It stops reducing whenever the formula is in weak-head normal form, that
  is:
  \begin{itemize}
  \item does not further reduce abstractions: $(\lambda x . \mathcal{T})$
  \item does not reduce arguments before substitution $(x \: \mathcal{T})$
  \end{itemize}
\end{itemize}



\section{Target language}
\label{sec:krivine-target-language}

The first thing we need to have is an encoding of the language we will be
reducing, in this case the Lambda Calculus. We will define a module,
\textbf{Lambda}, containing the data structure and basic operations over it:

\newpage
\begin{code}
  \begin{minted}[fontsize=\footnotesize]{ocaml}
type symbol = string * int
let show_symbol (s, _) = s

module Lambda = struct
    type t = Var of symbol | App of t * t | Abs of symbol * t
    let rec show = match m with
      | Var x -> show_symbol x
      | App (m1, m2) -> "(" ^ show m1 ^ " " ^ show m2 ^ ")"
      | Abs (x, m) -> "(λ" ^ show_symbol x ^ "." ^ show m ^ ")"
end
  \end{minted}
\end{code}

(From now on, the auxiliar (e.g., pretty-printing) functions will be ommited for
brevity.)

The module Lambda encodes the pure Lambda Calculus with its main type <<t>>
\footnote{Naming the main type of a module <<t>> is an idiom when using modules
  in OCaml}. Variables are just symbols (strings tagged with an integer so that
they're unique), Applications are pairs of terms and Abstractions are pairs of
symbols (the binding variable) and terms (the body). As the Krivine Machine
usually works with expressions in \textbf{de Bruijn} notation\footnote{The de
  Bruijn's notation gets rid of variable names by replacing them by the number
  of ``lambdas'' between it and the lambda that is binding the variable. For
  example, $(\lambda x . (\lambda y . (x \: y)))$ will be written in de Bruijn
  notation as $(\lambda . (\lambda . (1 \: 0)))$}, we'll need to write an
algorithm to do the conversion of variables. To be sure we do not accidentally
build terms mixing the two notatios, we'll create another module,
\textbf{DBILambda}, with a different data type to represent them:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
let rec find_idx_exn x = function
  | [] -> raise Not_found
  | (y::ys) -> if x = y then 0 else 1 + find_idx_exn x ys

module DBILambda = struct
    type dbi_symbol = int * symbol
    type t = Var of dbi_symbol | App of t * t | Abs of symbol * t

    let dbi dbis x = (find_idx_exn x dbis, x)

    let of_lambda =
      let rec of_lambda dbis = function
        | Lambda.Var x -> let (n, x) = dbi dbis x in Var (n, x)
        | Lambda.App (m1, m2) -> App (of_lambda dbis m1, of_lambda dbis m2)
        | Lambda.Abs (x, m) -> Abs (x, of_lambda (x :: dbis) m)
      in of_lambda []
end
  \end{minted}
\end{code}

The new variables, of type <<dbi_symbol>>, store the de Bruijn number together
with the previous value of the symbol, to help debugging and
pretty-printing. The function <<of_lambda>> accepts traditional lambda terms
(Lambda.t) and returns its representation as a term using de Bruijn notation
(DBILambda.t). Now we are ready to implement the actual reduction.



\section{Reduction}

The Krivine Machine has a state $(C, S, E)$ consisting on the \textbf{code} it
is evaluating ($C$), an auxiliar \textbf{stack} ($S$) and the current
\textbf{environment} ($E$). The code is just the current Lambda expression, the
stack holds \textbf{closures} (not yet evaluated code + the environment at the
time the closure was created), and an environment that associates variables (de
Bruijn indices) to values (closures).

The typical description of the Krivine Machine \cite{Douence07} is given by the
following set of rules:

\begin{center}
\line(1,0){250}
\end{center}
\begin{table}[H]
\centering
\begin{tabular}{lllll}
$(M N, S, E)$ & \rightsquigarrow & $(M, (N,E) :: S, E)$ \\ \\
$(\lambda M, N :: S, E)$ & \rightsquigarrow & $(M, S, N :: E)$ \\ \\
$(i+1, S, N :: E)$ & \rightsquigarrow & $(i, S, E)$ \\ \\
$(0, S, (M,E_1) :: E_2)$ & \rightsquigarrow & $(M, S, E_1)$
\end{tabular}
\end{table}
\begin{center}
\line(1,0){250}
\end{center}

In the previous diagram, $S$ and $E$ are both described as \textbf{lists}, with
the syntax (H :: T) meaning ``list whose head is H and tail is T''. The stack
$S$ is a list of closures that implements the push/pop operations over its
head. The environment is a list whose $i$-th position stores the variable with
de Bruijn index $i$.

\begin{itemize}
\item In the first rule, to evaluate an application $M N$, the machine builds a
  closure from the argument $N$ and the current environment $E$, pushes it into
  the stack, and keeps on reducing the function $M$.
\item To reduce an abstraction $\lambda M$, the top of the stack is moved to the
  environment and proceeds with the reduction of the body $M$. What this means
  is that the last closure in the stack (the function argument) is now going to
  be the variable in position (de Bruijn index) 0.
\item The last two rules rearch through the environment to find the closure
  corresponding to the current variable. Once it is found, the closure's code
  $M$ and environment $E_1$ replace the current ones.
\end{itemize}

From this specification we can write a third module, \textbf{KM}, to define the
data structures (state, closure, stack) and implement the symbolic reduction
rules of the Krivine Machine:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
module KM = struct
    open DBILambda

    type st_elm = Clos of DBILambda.t * stack
    and stack = st_elm list

    type state = DBILambda.t * stack * stack

    let reduce m =
      let rec reduce (st : state) : DBILambda.t =
        match st with
        (* Pure lambda calculus *)
        | (Var (0, _), s, Clos (m, e') :: e) -> reduce (m, s, e')
        | (Var (n, x), s, _ :: e) -> reduce (Var (n-1, x), s, e)
        | (App (m1, m2), s, e) -> reduce (m1, Clos (m2, e) :: s, e)
        | (Abs (_, m), c :: s, e) -> reduce (m, s, c :: e)
        (* Termination checks *)
        | (m, [], []) -> m
        | (_, _, _) -> m in
      reduce (m, [], [])
end
  \end{minted}
\end{code}

At this point, we have a working implementation of the Krivine Machine and can
execute some tests to see that everything works as expected. We'll write some
example $\lambda$-terms:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
let ex_m1 =      (* (λx.((λy.y) x)) *)
  let x = symbol "x" in
  let y = symbol "y" in
  Abs (x, App (Abs (y, Var y), Var x))

let ex_m2 =      (* (((λx.(λy.(y x))) (λz.z)) (λy.y)) *)
  let x = symbol "x" in
  let y = symbol "y" in
  let z = symbol "z" in
  App (App (Abs (x, Abs (y, App (Var y, Var x))), Abs (z, Var z)), Abs (y, Var y))
  \end{minted}
\end{code}

And lastly, a helper function that accepts a $\lambda$-term, translates it to de
Bruijn notation and reduces it, outputting the results:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
let dbi_and_red m =
  let dbi_m = DBILambda.of_lambda m in
  print_endline ("# Lambda term:\n    " ^ DBILambda.show dbi_m);
  let red_m = KM.reduce dbi_m in
  print_endline ("# Reduced term:\n    " ^ DBILambda.show red_m);
  print_endline "-----------------------------------------------\n"
  \end{minted}
\end{code}

\newpage
The results:

\begin{code}
\begin{verbatim}
ocaml> List.iter dbi_and_red [ex_m1; ex_m2];;

# Lambda term:
    (λx.((λy.y) x))
# Reduced term:
    (λx.((λy.y) x))
----------------------------------------------------------

# Lambda term:
    (((λx.(λy.(y x))) (λz.z)) (λy.y))
# Reduced term:
    (λz.z)
----------------------------------------------------------
\end{verbatim}
\end{code}

As we can see, the first term is not reduced because it is already in weak head
normal form (abstraction). The second term reduces as we would expect. As a
sidenote, we can easily tweak the DBILambda module to show the real de Bruijn
variables:

\begin{code}
\begin{verbatim}
ocaml> List.iter dbi_and_red [ex_m1; ex_m2];;

# Lambda term:
    (λ.((λ.0) 0))
# Reduced term:
    (λ.((λ.0) 0))
----------------------------------------------------------

# Lambda term:
    (((λ.(λ.(0 1))) (λ.0)) (λ.0))
# Reduced term:
    (λ.0)
----------------------------------------------------------
\end{verbatim}
\end{code}



\section{Extended version} %%

Now that we have a working Krivine Machine over basic Lambda Terms, we want to
extend it to work with some extensions: \textbf{case expressions} and
\textbf{fixpoints}.


\subsection{Case expressions}

First, we will need to extend our definition of the Lambda Calculus to support
constructors and case expressions, both in Lambda and DBILambda. Constructors
are just atomic symbols, optionally parameterized by some arguments, used to
encode arbitrary data. Case expressions are used to ``destructure'' constructors
and extract the value of their parameters:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
module Lambda = struct
    type t = Var of symbol | App of t * t | Abs of symbol * t
             (* constructors / case expressions *)
             | Constr of t constr
             | Case of t * (symbol constr * t) list
    and 'a constr = symbol * 'a list

    (* ... *)
end

module DBILambda = struct
    type t = Var of dbi_symbol | App of t * t | Abs of symbol * t
             (* constructors / case expressions *)
             | Constr of t constr
             | Case of t * (symbol constr * t) list
    and 'a constr = symbol * 'a list

    let of_lambda =
      let rec of_lambda dbis = function
        (* ... *)
        | Lambda.Constr (x, ms) -> Constr (x, List.map (of_lambda dbis) ms)
        | Lambda.Case (m, bs) -> Case (of_lambda dbis m,
                                      List.map (trans_br dbis) bs)
      in of_lambda []

    (* ... *)
end
  \end{minted}
\end{code}

The basic approach to implement the reduction will be the same as when reducing
applications in $\lambda$-terms: when encountering a case expression, create a
custom closure ``CaseCont'' containing the branches and push it into the
stack. When a constructor is encountered, if there is a CaseCont closure in the
stack, the machine will iterate over the branches in the closure until it finds
one whose symbol matches with the constructor, and evaluate the body:

\newpage
\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
module KM = struct
    (* ... *)
    type st_elm = Clos of DBILambda.t * stack
                (* Specific closure for case expressions *)
                | CaseCont of (symbol DBILambda.constr * DBILambda.t) list * stack

    let reduce m =
      let rec reduce (st : state) : DBILambda.t =
        match st with
        (* ... *)
        (* Case expressions (+ constructors) *)
        | (Case (m, bs), s, e) -> reduce (m, CaseCont (bs, e) :: s, e)
        | (Constr (x, ms), CaseCont (((x', args), m) :: bs, e') :: s, e)
             when x == x' && List.length ms == List.length args ->
           reduce (List.fold_left (fun m x -> Abs (x, m)) m args,
                   map_rev (fun m -> Clos (m, e)) ms @ s, e')
        | (Constr (x, ms), CaseCont (_ :: bs, e') :: s, e) ->
           reduce (Constr (x, ms), CaseCont (bs, e') :: s, e)
        | (Constr (x, ms), s, e) ->
           Constr (x, List.map (fun m -> reduce (m, s, e)) ms)
      reduce (m, [], [])
end
  \end{minted}
\end{code}

Note that te last rule reduces the terms inside a constructor even when it is
not being pattern matched. It can be deleted to more closely resemble a
weak-head normal form behavior.

With this new functionality we can encode Peano arithmetic by using the
constructors <<z>> and <<s>>, and try some examples of pattern matching:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
(* Peano arithmetic helpers *)
let z = symbol "z"
let s = symbol "s"

let rec peano_add n x =
  if n == 0 then x else peano_add (n-1) (Constr (s, [x]))

let peano_of_int ?(base=Constr (z, [])) n = peano_add n base
  \end{minted}
\end{code}

\newpage
\begin{code}
\begin{verbatim}
# Lambda term:
    ((λc.(case c of (Some(x) → x)
                    (None() → c)))
     Some(s(z())))
# Reduced term:
    s(z())
----------------------------------------------------------

# Lambda term:
    ((λc.(case c of (triple(x,y,z) → y)))
     triple(s(z()), s(s(z())), s(s(s(z())))))
# Reduced term:
    s(s(z()))
----------------------------------------------------------
\end{verbatim}
\end{code}


\subsection{Fixpoints}

The second extension we are going to implement in our Krivine Machine is the
ability to support fixpoints, that is, recursion. Again, we extend the data
structures of the Lambda Calculus. As the extension to DBILambda follows
trivially, we will omit it here:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
module Lambda = struct
    type t = Var of symbol | App of t * t | Abs of symbol * t
             | Constr of t constr
             | Case of t * (symbol constr * t) list
             (* fixpoints *)
             | Fix of symbol * t
    (* ... *)
end
  \end{minted}
\end{code}

The ``Fix'' constructor is parameterized by a symbol and another lambda
term. The symbol is the name of the fixpoint, and will expand to itself when
referenced inside the term. Let's see an example:

\begin{code}
\begin{verbatim}
fix(λf.λc. case c of (s(x) → s(s(f x)))
                     (z → z))
    s(s(s(z)))
\end{verbatim}
\end{code}

Here, the name of the fixpoint is <<f>>, and is an implicitly-passed argument
that references to the term itself (<<fix(...)>>). So, in this case, <<f>> will be
bound to <<fix($\lambda$f. $\lambda$c. case c of ... )>> and <<c>> will be bound
to <<s(s(s(z)))>> initially.

The reduction itself is simpler than the previous case:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
module KM = struct
    (* ... *)
    type st_elm = Clos of DBILambda.t * stack
                | CaseCont of (symbol DBILambda.constr * DBILambda.t) list * stack
                (* Specific closure for fixpoints *)
                | FixClos of symbol * DBILambda.t * stack

    let reduce m =
      let rec reduce (st : state) : DBILambda.t =
        match st with
        (* ... *)
        (* Fixpoints *)
        | (Var (0, _), s, FixClos (f, m, e') :: e) ->
           reduce (m, s, FixClos (f, m, e') :: e')
        | (Fix (x, m), s, e) -> reduce (m, s, FixClos (x, m, e) :: e)
      reduce (m, [], [])
end
  \end{minted}
\end{code}

Again, here we create a new closure when reducing the Fix constructor. Then,
whenever some variable refers to a fixpoint closure, the result is its body,
with the side effect of keeping the closure it in the environment (so that it is
automatically bound to the first argument <<f>> of itself).

The fixpoint tests:

\begin{code}
\begin{verbatim}
# Lambda term:
    (fix(λf.(λc.(case c of (s(x) → s(s((f x))))
                           (z() → z()))))
     s(s(s(z()))))
# Reduced term:
    s(s(s(s(s(s(z()))))))
----------------------------------------------------------

# Lambda term:
    ((fix(λf.(λg.(λc.(case c of (s(x) → (g ((f g) x)))
                                (z() → z())))))
         (λy.s(s(s(y)))))
     s(s(s(z()))))
# Reduced term:
    s(s(s(s(s(s(s(s(s(z())))))))))
----------------------------------------------------------
\end{verbatim}
\end{code}

The first test is the example we have previously seen; the fixpoint receives a
number in Peano notation and multiplies it by two by iterating over its
structure. The second one generalizes it by accepting a function <<g>> that is
applied once for each iteration over the number: in this case, <<g>> adds 3 to
its argument, so the whole term is a ``by 3'' multiplier.




\chapter{ZAM} %%%%%%%%%%

The ZAM (ZINC Abstract Machine) \cite{Leroy90} is a call-by-value variant of the
Krivine Machine, and currently powers the bytecode interpreter of the Caml Light
and OCaml languages. We will implement the version introduced in
\cite{LeroyG02} as a previous step before tackling the implementation of
EasyCrypt's new reduction machinery. Again, the full code is available in the
annex \ref{sec:zam-source-code}.

As with the Krivine Machine before, it will be able to handle extended
$\lambda$-terms with case expressions and fixpoints, but this time the machine
will interpret actual abstract code instead of implementing symbolic reduction,
so we will need an extra step to compile the the $\lambda$-terms to machine
code. Also, we will skip the progressive exposition of the basic and extended
machine, as it has already been done in the previous section, and just implement
the final version. To finish, we will show how to use it to archieve
\textbf{strong reduction}.



\section{Target language}

As the reference work \cite{LeroyG02} aimed to improve the performance of strong
reduction in proof assistants, this version of the ZAM works over type-erased
terms of the Calculus of Constructions \cite{Coquand88}, adding
\textbf{inductive types} (for our purposes, equivalent to the previously
implemented algebraic data types) and \textbf{fixpoints}.

For this task, we will define a module called \textbf{CCLambda} with a type
encoding the terms of our language:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
module CCLambda = struct
    type t = Var of symbol | App of t * t | Abs of symbol * t
             | Constr of t constr | Case of t * (symbol constr * t) list
             | Fix of symbol * symbol list * symbol * t
    and 'a constr = symbol * 'a list

    (* ... *)
end
  \end{minted}
\end{code}

The only difference we can see here with respect to the encoding of terms in the
K-Machine (section \ref{sec:krivine-target-language}) is the more elaborate
fixpoints. Even though our $\lambda$-terms are not typed, the Calculus of
Constructions' fixpoints need an argument (``guard'') to structurally to the
recursion and prevent infinite unrolling. We will represent fixpoints as <<Fix
(f, xs, c, m)>>, where <<f>> is the symbol (bound in <<m>>) referring to the
fixpoint itself, <<xs>> is the argument list, <<c>> is the guard (a
constructor), and <<m>> is the $\lambda$-term.



\section{Compilation}

Unlike the previous implementation, in this case we are going to implement a
more efficient version. Instead of symbolically evaluating the $\lambda$-terms
we need an extra step to compile them to some intermediate code Now we need to
be able to compile $\lambda$-terms to instructions targeting the ZAM runtime,
which will do the actual reduction.

This is the type encoding the machine instructions:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
module WeakRed = struct
    open CCLambda

    type dbi = symbol * int
    type instr =
      | ACCESS of dbi
      | CLOSURE of instrs
      | ACCLOSURE of symbol
      | PUSHRETADDR of instrs
      | APPLY of int
      | GRAB of symbol
      | RETURN
      | MAKEBLOCK of symbol * int
      | SWITCH of (symbol constr * instrs) list
      | CLOSUREREC of (symbol * symbol list * symbol) * instrs
      | GRABREC of symbol
    and instrs = instr list
    and mval =
      | Cons of mval constr
      | Clos of instrs * env
      | Ret of instrs * env * int
    and env = mval list
    and stack = mval list
    and state = {
        st_c : instrs;
        st_e : env;
        st_s : stack;
        st_n : int;
    }

    (* ... *)
end
  \end{minted}
\end{code}

The <<WeakRed.compile>> function in the code does the actual work of translating
$\lambda$-terms to a sequence of instructions.

\section{Reduction}

The figure \ref{fig:zam-rules} details the reduction rules. The implementation
is straightforward (although contrived) and follows the same structure as the
Krivine Machine. I refer the reader to the annex in order to see how this rules
are actually encoded in our program.

\begin{figure}[h]
  \centering
  \includegraphics[width=1\textwidth]{img/zamrules.png}
  \caption{ZAM reduction rules (from \cite{LeroyG02})}
  \label{fig:zam-rules}
\end{figure}

\newpage
At this point, we can try some code examples to see the results:

\begin{code}
\begin{verbatim}
WEAK REDUCTION TEST
Lambda term:
    ((λx.x) (λy.(((λz.z) y) (λt.t))))
Reduced term:
    (λy.(((λz.z) y) (λt.t)))
----------------------------------------------------------

WEAK REDUCTION TEST
Lambda term:
    (((λf.(λx.(f (f x)))) (λy.y)) (λz.z))
Reduced term:
    (λz.z)
----------------------------------------------------------

WEAK REDUCTION TEST
Lambda term:
    ((λc.(case c of (Cons(x,xs) → x)
                    (Nil() → Nil())))
     Cons((λm.m), Nil()))
Reduced term:
    (λm.m)
----------------------------------------------------------

WEAK REDUCTION TEST
Lambda term:
    (fix_0(λf.λc. (case c of (s(x) → s(s((f x))))
                  (z() → z())))
     s(s(s(z()))))
Reduced term:
    s(s(s(s(s(s(z()))))))
----------------------------------------------------------
\end{verbatim}
\end{code}



\newpage
\section{Strong reduction}

Once we have the machinery to perform call-by-value reduction (that is, until it
reaches a weak normal form) we can use a callback procedure to apply it
repeatedly and archieve strong normalization. The actual implementation is in
the module <<StrongRed>> (annex \ref{sec:zam-source-code}).

The most interesting detail about using the readback procedure is the need to
support \textbf{accumulators} as another case of $\lambda$-terms. Accumulators
are just terms that cannot get reduced, and are self-propagating: whenever a
function is applied to an accumulator, the result is an accumulator containing
the application of the function to the previous accumulator. The callback
procedure needs it in order to reach the previously-unreachable terms inside an
abstraction. Here are the modifications to the data structures:

\newpage
\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
module CCLambda = struct
    type t = Var of symbol | App of t * t | Abs of symbol * t
             | Constr of t constr | Case of t * (symbol constr * t) list
             | Fix of symbol * symbol list * symbol * t
             | Acc of t    (* Accumulators *)
    and 'a constr = symbol * 'a list

    (* ... *)
end

module WeakRed = struct
    open CCLambda

    type dbi = symbol * int
    type instr =
      | ACCESS of dbi
      | CLOSURE of instrs
      | ACCLOSURE of symbol
      | PUSHRETADDR of instrs
      | APPLY of int
      | GRAB of symbol
      | RETURN
      | MAKEBLOCK of symbol * int
      | SWITCH of (symbol constr * instrs) list
      | CLOSUREREC of (symbol * symbol list * symbol) * instrs
      | GRABREC of symbol
    and instrs = instr list
    and accum =
      | NoVar of symbol
      | NoApp of accum * mval list
      | NoCase of accum * instrs * env
      | NoFix of accum * instrs * env
    and mval =
      | Accu of accum
      | Cons of mval constr
      | Clos of instrs * env
      | Ret of instrs * env * int
    and env = mval list
    and stack = mval list
    and state = {
        st_c : instrs;
        st_e : env;
        st_s : stack;
        st_n : int;
    }

    (* ... *)
end
  \end{minted}
\end{code}

\newpage

And we pass the tests again:

\begin{code}
\begin{verbatim}
STRONG REDUCTION TEST
Lambda term:
    ((λx.x) (λy.(((λz.z) y) (λt.t))))
Reduced term:
    (λy.(y (λt.t)))
----------------------------------------------------------

STRONG REDUCTION TEST
Lambda term:
    (((λf.(λx.(f (f x)))) (λy.y)) (λz.z))
Reduced term:
    (λz.z)
----------------------------------------------------------

STRONG REDUCTION TEST
Lambda term:
    ((λc.(case c of (Cons(x,xs) → x)
                    (Nil() → Nil())))
     Cons((λm.m), Nil()))
Reduced term:
    (λm.m)
----------------------------------------------------------

STRONG REDUCTION TEST
Lambda term:
    (fix_0(λf.λc. (case c of (s(x) → s(s((f x))))
                             (z() → z())))
     s(s(s(z()))))
Reduced term:
    s(s(s(s(s(s(z()))))))
----------------------------------------------------------
\end{verbatim}
\end{code}

As we were expecting, the first term is now \textbf{strongly reduced} to
normal form.



\chapter{REDUCTION IN EASYCRYPT} %%%%%%%%%%
\label{cha:reduction-easycrypt}

The current approach that EasyCrypt uses to reduce terms is the iteration over
the formula and application of ad-hoc transformations based on the information
provided by its type and global state.

To archieve strong reduction, EasyCrypt uses a similar ``read-back'' protocol to
the one we've already seen in the ZAM: repeatedly application of a function that
iterates the current formula and tries to reduce it in a call-by-value
fashion. When there is no other expression to be reduced, the read-back
procedure stops and the normalized formula is returned.



\section{Target language} %%

Each formula is composed by some metadata (type, free variables, unique tag)
together with a \textbf{node} that holds the actual structure of the term:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
type f_node =
  | Fquant  of quantif * bindings * form
  | Fif     of form * form * form
  | Flet    of lpattern * form * form
  | Fint    of BI.zint
  | Flocal  of EcIdent.t
  | Fpvar   of EcTypes.prog_var * memory
  | Fglob   of EcPath.mpath     * memory
  | Fop     of EcPath.path * ty list
  | Fapp    of form * form list
  | Ftuple  of form list
  | Fproj   of form * int
  | FhoareF of hoareF
  | FhoareS of hoareS
  | FbdHoareF of bdHoareF
  | FbdHoareS of bdHoareS
  | FequivF of equivF
  | FequivS of equivS
  | FeagerF of eagerF
  | Fpr of pr
  \end{minted}
\end{code}

As there are so much types and corner cases, we will briefly explain what are
the most important constructors and what are they for:

\begin{itemize}
\item \textbf{FQuant}: They serve both as universal/existential quantifiers
  (forall / exists) and lambda abstractions, depending on the value of the
  <<quantif>> parameter (Lforall, Lexists, Llambda, respectively).
\item \textbf{Fif}: Conditionals.
\item \textbf{Fint}: Literal integers.
\item \textbf{Flocal}: Local variables.
\item \textbf{Fop}: Operators: as explained in the introduction (section
  \ref{sec:expressions}). The actual code must be obtained by resolving its path.
\item \textbf{Fapp}: Function application (to multiple arguments).
\end{itemize}

\section{Reduction rules}

As the term language of EasyCrypt is more complex than standard Lambda
Calculus, it has some reduction rules we have not seen befone:

\begin{itemize}
\item $\delta$-reduction (\textbf{delta}): used to unfold global
  definitions. Affects operators (<<Fop>>).
\item $\zeta$-reduction (\textbf{zeta}): used to unfold a let expression in its
  body. Affects let expressions (<<Flet>>).
\item $\iota$-reduction (\textbf{iota}): used to unfold a case
  expression. Affects conditionals (<<Fif>>), operators (<<Fop>>).
\item Logical reduction: used to evaluate logic expressions (And, Or,
  ...). Affects operators (<<Fop>>).
\end{itemize}

A structure containing information about which of this reductions must be done
is passed to every reduction procedure:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
type reduction_info = {
  beta    : bool;
  delta_p : (path  -> bool);
  delta_h : (ident -> bool);
  zeta    : bool;
  iota    : bool;
  logic   : bool;
}
  \end{minted}
\end{code}



\section{Reduction}

The reduction machinery is implemented in an EasyCrypt module called
\textbf{EcReduction}. The main entry point is the function <<\textbf{h_red}>>,
which accepts the target formula and a <<reduction_info>> structure (see
previous section) and returns the reduced formula according to it. An important
point is that <<h_red>> only reduces until \textbf{weak normal form}, and there
is another callback procedure that calls it repeatedly as we've already seen
with the ZAM machine. So, we need to take that function and replace it with a
ZAM-like machine to do only the weak reduction.

This is a short fragment of the <<h_red>> function:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
let rec h_red_old ri env hyps f =
  match f.f_node with
    (* β-reduction *)
  | Fapp ({ f_node = Fquant (Llambda, _, _)}, _) when ri.beta ->
      f_betared f

    (* ζ-reduction *)
  | Flocal x -> reduce_local ri hyps x

    (* ζ-reduction *)
  | Fapp ({ f_node = Flocal x }, args) ->
      f_app_simpl (reduce_local ri hyps x) args f.f_ty

  (* ... *)
  \end{minted}
\end{code}

Although it is actually a pretty long function (around 220 lines of code), the
structure is simple: a pattern matching over the structure of the current
formula. We will start by defining the state of the new abstract machine and
replacing the pattern matching by a recursive function over an initial state:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
type st_elm =
  | Clos of form * menv
  | ClosCont of bindings
  | IfCont of form * form
and stack = st_elm list
and menv = (EcIdent.t, form) Hashtbl.t

let rec h_red ri env hyps f =
  let iter st =
    match (st : EcFol.form * stack * menv) with

    (* β-red *)
    | ({ f_node = Fapp (f, fs) }, s, e) when ri.beta ->
       iter (f, List.map (fun f -> Clos (f, e)) fs @ s, e)

  in
  iter (f, [], Hashtbl.create 100)
  \end{minted}
\end{code}

As we can see, the first block is very similar to what we did with the ZAM:
define a stack, the types of the closures and an environment (for efficiency,
this time it is implemented as a hash map from variables <<EcIdent.t>> to
formulas).

The new <<h_red>> function creates an initial state composed by the formula to
be reduced, an empty stack and an empty environment, and begins the reduction by
evaluating the auxiliar <<iter>> function in a tail-recursive manner. In this
example it is included the evaluation of an application: iterate over the
arguments, putting in the stack a new closure for every one of them.

Here we have the new code that performs the full $\beta$-reduction:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
let rec h_red ri env hyps f =
  let iter st =
    match (st : EcFol.form * stack * menv) with

    (* β-red *)
    | ({ f_node = Fapp (f, fs) }, s, e) when ri.beta ->
       iter (f, List.map (fun f -> Clos (f, e)) fs @ s, e)
    | ({ f_node = Fquant (Llambda, [], f) }, s, e) ->
       iter (f, s, e)
    | ({ f_node = Fquant (Llambda, (x,_)::bds, f) }, Clos (cf, _) :: s, e) ->
       let e' = Hashtbl.copy e in
       Hashtbl.add e' x cf;
       iter (f_quant Llambda bds f, s, e')

    (* ... *)
  \end{minted}
\end{code}

The second and third cases handle the evaluation of a $\lambda$-abstraction: if
it has no arguments, just keep going with the function body; if there are
arguments and a function closure is present in the stack, bind the function to
the closure in the environment and evaluate the function body with one parameter
less. (The <<f_quant>> and <<f_lambda>> functions are just helpers to build
formulas)

In order to do some of the other reductions, as they have nothing to do with the
abstract machine but with global state, we simply have to call standard
EasyCrypt's functions. For example, to $\delta$-reduce operators and resolve
local variables:

\begin{code}
  \begin{minted}[fontsize=\scriptsize]{ocaml}
let rec h_red ri env hyps f =
  let iter st =
    match (st : EcFol.form * stack * menv) with
    (* ... *)

    | ({ f_node = Fop (p, tys) }, s, e) when ri.delta_p p ->
       iter (reduce_op ri env p tys, s, e)

    | ({ f_node = Flocal x }, s, e) -> let f' = if Hashtbl.mem e x
                                              then Hashtbl.find e x
                                              else reduce_local ri hyps x in
                                      iter (f', s, e)

    (* ... *)
  \end{minted}
\end{code}

\newpage
Once we are done replacing one by one the standard EasyCrypt operations by
transitions in the abstract machine, we can see that it works (the formula being
reduced appears in the upper right of the screen):

\begin{figure}[h]
  \centering
  \includegraphics[width=0.8\textwidth]{img/ec1.png}
  \caption{After entering proof mode}
\end{figure}

\begin{figure}[h]
  \centering
  \includegraphics[width=0.8\textwidth]{img/ec2.png}
  \caption{Reduced $((\lambda x . x + x) \: 5) \Betared 10$}
\end{figure}

\begin{figure}[h]
  \centering
  \includegraphics[width=1\textwidth]{img/ec3.png}
  \caption{The proof is finished (``no more goals'' at bottom right)}
\end{figure}



\part{EPILOGUE} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\chapter{CONCLUSIONS} %%%%%%%%%%

In this work we began by exposing the need to verify cryptographic protocols and
the role that the EasyCrypt framework plays in the field. Then we moved on to
abstract rewriting systems and how the current machinery that EasyCrypt uses to
reduce its formulas could be improved. In order to do that, we implemented two
abstract machines with multiple variations (extended lambda terms, strong
reduction) and exposed the differences between them: evaluation strategies,
symbolic evaluation, bytecode compilation, and so on. Lastly, we continued to
the source language and current inner workings of EasyCrypt and proceeded to
replace it in a way that closely resembles the work previously done with the
abstract machines.

In my opinion, the development of this thesis has resulted in two main
contributions belonging to different scopes.

The first one is, obviously, the technical improvement of an existing
tool. Although it is not a contribution on features, but the replacing of an
existing module for an improved one, we believe it is an important step that had
to be taken in order to be able to further expand the system in the future.

The second contribution is the insight given by the actual implementation of two
different abstract machines. While none of these by itself was really needed for
the task of replacing the EasyCrypt's engine, the research needed to understand
the concepts of the abstract machines and correctly implement them has proven
crucial when facing a complex system such as EasyCrypt. It might prove to be
valuable to some of the interested readers as well, as having the source code of
both the abstract machines is a nice way to experiment and compare their
behaviors.

Of course, this work can be improved in many ways. The engine is still
evaluating code symbolically, which is slower than producing instructions
(bytecode) for the machine to evaluate. Some EasyCrypt features make this a
feature not trivial to implement (i.e., it would need to decompile bytecode to
recover the original terms), but worth keeping it in mind as a possibility for
future work.




\chapter{ANNEX} %%%%%%%%%%



\section{Krivine Machine source code} %%
\label{sec:kriv-mach-source}

\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml}

%\newpage
\section{ZAM source code} %%
\label{sec:zam-source-code}

\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/zam.ml}

\pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}

\end{document}