\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 <> \footnote{Naming the main type of a module <> 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 <>, store the de Bruijn number together with the previous value of the symbol, to help debugging and pretty-printing. The function <> 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 <> and <>, 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 <>, and is an implicitly-passed argument that references to the term itself (<>). So, in this case, <> will be bound to <> and <> will be bound to <> 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 <> 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 <> that is applied once for each iteration over the number: in this case, <> 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 <>, where <> is the symbol (bound in <>) referring to the fixpoint itself, <> is the argument list, <> is the guard (a constructor), and <> 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 <> 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 <> (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 <> 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 (<>). \item $\zeta$-reduction (\textbf{zeta}): used to unfold a let expression in its body. Affects let expressions (<>). \item $\iota$-reduction (\textbf{iota}): used to unfold a case expression. Affects conditionals (<>), operators (<>). \item Logical reduction: used to evaluate logic expressions (And, Or, ...). Affects operators (<>). \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 <> structure (see previous section) and returns the reduced formula according to it. An important point is that <> 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 <> 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 <> to formulas). The new <> 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 <> 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 <> and <> 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}