Extending the circom compiler

Extensiones sobre el compilador de circom Extending the circom compiler Trabajo de Fin de Grado Curso 2022–2023 Autor Juan Carlos Díaz Rodríguez Director Albert Rubio Gimeno Codirector Miguel Isabel Márquez Doble Grado en Matemáticas e Ingeniería Informática Facultad de Informática Universidad Complutense de Madrid Extensiones sobre el compilador de circom Extending the circom compiler Trabajo de Fin de Grado en Ingeniería Informática Autor Juan Carlos Díaz Rodríguez Director Albert Rubio Gimeno Codirector Miguel Isabel Márquez Convocatoria: Junio 2023 Doble Grado en Matemáticas e Ingeniería Informática Facultad de Informática Universidad Complutense de Madrid 29 de mayo de 2023 Resumen Extensiones sobre el compilador de circom En este proyecto se ha desarrollado un análisis estático para el compilador de circom, un Lenguage de Dominio Específico para el diseño de protocolos de Conocimiento Nulo. Su objetivo es detectar asignaciones de variables que no juegan ningún papel en el código generado. Bien porque la variable se sale de scope antes de ser leída o porque hay una nueva asignación de la variable antes de que el antiguo valor se haya llegado a examinar. Se propone un algoritmo y se presenta una demostración de su correción. Se han llevado a cabo tests de rendimiento tanto sobre el compilador como sobre el código que este genera. Los resultados de dichas pruebas aparecen en la sección posterior a la presentación del algoritmo. Al final del documento, se expone una discusión de los resultados y los beneficios que este análisis presenta para el compilador. Palabras clave Compilador, Circom, análisis estático, asignación, traza, Rust, seguridad del código, optimización de código. v Abstract Extending the circom compiler In this project, a static analysis is developed for the compiler of circom, a Domain Specific Language to design Zero-Knowledge protocols. It aims to detect assignments of variables that play no role in the generated code. Either because the variable is never read before going out of scope or because a new assignment occurs before the variable has ever been read. An algorithm is developed for this analysis and a correction proof is also given. Benchmarking tests have been conducted on the compiler itself and the code generated by it. The results are presented in the section following the algorithm’s explanation. A discussion of the results and the benefits this analysis brings to the compiler appears at the end of the document. Keywords Compiler, Circom, static analysis, assignment, trace, Rust, code safety, code optimization. vii Contents 1 Introduction 1 1.1 Motivation................................. 1 1.2 Objectives................................. 2 1.3 Workdescription ............................. 2 1.4 In the following chapters . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 State of Art 5 2.1 Zero-Knowledge proofs . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Arithmeticcircuits ............................ 6 2.3 Circom................................... 7 2.4 WhyRust................................. 9 2.5 Staticanalysis............................... 9 3 Assignment Analysis 11 3.1 Importance of the analysis . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Correctnessproof............................. 13 3.2.1 Previous definitions . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2.2 Single Variable approach . . . . . . . . . . . . . . . . . . . . . 16 3.2.3 Multiple Variables approach . . . . . . . . . . . . . . . . . . . 24 3.3 Bringing the analysis to real code . . . . . . . . . . . . . . . . . . . . 27 3.3.1 Implementation.......................... 27 3.3.2 Discarded improvements . . . . . . . . . . . . . . . . . . . . . 28 3.3.3 Warningsadded.......................... 28 4 Benchmarking 31 4.1 Projects .................................. 31 4.1.1 Circom ECDSA and ED25519 . . . . . . . . . . . . . . . . . 31 4.1.2 Rollups .............................. 32 4.1.3 MachineLearning......................... 33 4.1.4 Darkforest ............................ 33 4.2 Evaluationprocess ............................ 34 4.3 Performance................................ 35 ix 2Chapter 1. Introduction environment to contribute to a real-world code base. 1.2 Objectives The present project aims at developing additional features inside the circom compiler based on static analysis techniques. We can break down that end into the following specific objectives: I) Study an ongoing code repository. During the whole degree, the usual way of developing code has been building it from the ground up, using libraries if needed. We all know that is not the case in most projects. That is why it is important to get used to reading and building on top of other developers’ work. II) Read up on classic static analysis techniques and adapt them to the current code base of the compiler. III) Create a semantic preserving algorithm. It is paramount that the modifications to the code suggested by the analysis never change the semantics of our programs. IV) Improve code safety of circom circuits and help developers to find potential bugs. V) Boost the performance of the generated code by the compiler. Any minor performance improvement in the compilers output will be helpful as these programs are meant to run thousands of times when linked to a blockchain or cryptographic system. 1.3 Work description The first thing to do in this project was to get familiar with the code base. After a careful study of the parts of the compiler that were to be dealt with, a first attempt at implementation followed. To track development at the same time the compiler version was kept up to date, a fork was created from the official circom repository. Pull requests were done periodically to assure code compatibility. Because the analysis proved to have some caveats, it was decided to first complete the formal proof of the algorithm. This formal approach helped in finding proper data structures and algorithm properties that carried nicely into the existing code and fixed the existing issues. Once the main development phase was complete, we committed to a series of tests involving the circom library and additional repositories. Code bugs were fixed thanks to this testing and we made sure that no semantics were altered. Having the code sorted, there was a last phase of benchmarking to check compiler performance as well as output code improvements. The project’s code can be found in the forked repository (https://github.com/ RinconDeJC/static-circom). 1.4. In the following chapters 3 1.4 In the following chapters Once finished with the introduction, an overview of the main concepts around circom will be given. We will see what Zero-Knowledge proofs and arithmetic circuits are, the compiler’s structure and the classical literature on static analysis studied. Next up, the algorithm created will be explained, along with its correctness, completeness and termination proof. An overview of how this was translated to the code base will be given as well. In the fourth chapter, the testing chain will be discussed along with the results obtained. Finally, a discussion of the whole project will be held to round up this year’s work. Chapter 2 State of Art This chapter aims to give the reader an idea of the background behind circom and its applications. We first introduce the concept of Zero-Knowledge proofs and arithmetic circuits, followed by a description of the circom language and its compiler. At the end, there is a review of the literature on static analysis. 2.1 Zero-Knowledge proofs In the world of cryptography, a very common problem is proving you possess some information. One immediate way to prove it is by disclosing the knowledge you claim to have. However, that usually goes against the whole point of cryptography. Zero-Knowledge proofs or Zero-Knowledge protocols (ZK) are a way of assuring you have some information without having to reveal it. A classical example can be found in [1]. Here Alice and Bob have found a cave. The cave has a single entry to a circular path. On the opposite side of the entry, there is a door that requires a password. Bob claims a mysterious man has revealed the secret code to him, but has prohibited revealing it to anyone else. Alice dares him to prove his claim, and they design an experiment to do so. Bob will go into the cave first and, without Alice knowing, he will go in a random direction towards the door. Alice will stand at the entry and shout a direction she wants Bob to come out from. If Bob does not know the password and cannot cross the door, there is a 50% chance that both of them have chosen the same direction. By repeating this experiment ntimes, the chance that Bob does not know the code but always comes from the direction Alice tells him is 2−n. So after several tries, Alice is convinced Bob knows the code, although she does not know the password herself. Observe how these proofs are not a logical proof as they are understood in mathematics. They are a probability proof, where there is always a small chance that a malicious prover can convince the verifier. This probability can be made as small as we want to increase the reliability of the protocol. In the previous example, interaction between the prover Bob and the verifier Alice was also required. This aspect is avoided by Zero-Knowledge Succinct Non5 6Chapter 2. State of Art Interactive Argument of Knowledge (ZK-SNARKs) and they are the ones circom focuses on. In general, ZK-SNARKs are used to prove the correctness of a computation. These computations can be represented by an airthmetic circuit. 2.2 Arithmetic circuits One of the most recurrent languages used for ZK-SNARKs is the language of circuit satisfiability. This language is NP-complete and hence frequently appears in the field of cryptography [2, 3, 4]. An arithmetic circuit is composed of a set of gates connected just like in electronic circuits that perform arithmetic operations on their inputs to produce their output. A circuit is then said to be satisfiable if it has an assignment of its inputs that makes the output true. In our context, these circuits will be defined by circom programs, the inputs and outputs of the gates will be referred to as signals and the arithmetic operations performed will only be addition and multiplication. Signals will take values on a prime finite field Fp, where pis a very large prime [5]. Circom defines circuits by setting a set of constraints on the signals. These constraints are a set of equations of the form A∗B−C= 0, where A, B, C are linear combinations of signals over a primer field Fp, called rank-1 constraint system (R1CS). A ZK-SNARK protocol will then prove that the prover knows an assignment of the set of signals that meet the R1CS constraints, but without disclosing the values of the signals that are considered secret. To distinguish what is a secret signal and what is not, most arithmetic circuit languages have the concept of private and public signals. In general, a public signal will be known by the verifier, while the prover will have to know a correct assignment of public and private signals. In circom, signals can be considered input,intermediate or output. Intermediate signals will always be private and output signals public. Input signals can either be private or public, so the prover can hide the information that he does not want to disclose, but prove he does have it. A signal assignment in a circuit (public and private) is known as a witness. s4 s5 s3 s2 s1 s6 s7 s8s9 Figure 2.1: Graphic representation of an arithmetic circuit Cover F11 that output the expression s1×s2×s3+s4×s5mod 11 2.3. Circom 7 Example 2.2.1. Let Cbe the circuit from Fig 2.1 over F11 that given the inputs s1, s2, s3, s4and s5outputs s1×s2×s3+s4×s5. Our gates only have 2 inputs each, so we will need intermediate signals s6, s7, s8and an output signal s9. A valid witness wfor the set of signals S={si}9 i=1 could be w1={7,3,4,9,9,10,7,4,0}or w2={5,2,8,7,9,10,3,8,0}. To get the R1CS constraints, we cannot express it as s1×s2×s3+s4×s5−s9= 0 mod 11, but rather we need to split it into more constraints like          s1×s2−s6= 0 mod 11 s6×s3−s7= 0 mod 11 s4×s5−s8= 0 mod 11 s7+s8−s9= 0 mod 11 which can be further simplified into      s1×s2−s6= 0 mod 11 s6×s3−s7= 0 mod 11 s4×s5+s7−s9= 0 mod 11. 2.3 Circom Circom [6, 7] is a constraint-based Domain Specific Language to design arithmetic circuits. A much better overview of circom, its environment and usages can be found in [8], where a lot of the information in this review has been extracted from. Programming with this language is fairly low-level and the design of arithmetic circuits lands very close to the design of electronic circuits. However, circom aims to make the design of very large circuits a simpler process with a strong focus on modularity. The language allows the user to create generic circuits called templates that one can instantiate with different parameters and reuse them to create more complex systems. We will refer to a template instantiation as a component. The circom ecosystem needs two main elements to be able to work with ZeroKnowledge proofs. These are the witness and the circuit in R1CS format. The witness is generated with the assigned values of every single signal in the arithmetic circuit. The key part of these circuits is that it is almost impossible to compute the value of every signal, private and public, simply from the values of the public inputs and the outputs, which are always public. This is true given the programmer has used circom to design a robust circuit, of course, trivial circuits can be solved just from the public input. To be able to generate our witness, circom outputs 8Chapter 2. State of Art a program, either in C++ or WebAssembly that efficiently computes these values given every input of the circuit. At the same time, the set of R1CS constraints is generated from the specifications in the circom program. The compiler will output these in the format that the user asks for. These constraints are extracted by the compiler from the program by performing a symbolic execution of the code. It is symbolic because the compiler does not know the value of the signals at compile time, so the operations performed on signals are very much like the ones we would do with variables in a mathematical equation. The constraints the programmer specifies with their code must follow the R1CS structure described, or the compiler will issue an error code. Although circom is a Domain Specific Language, there is a wider variety of projects where this is used than one might think at first. Although most of them are related to cryptography in some way, there are very interesting ways to apply these techniques. Some of these projects will be reviewed in Chapter 4. The compiler has four main phases. The first part has to do with the parser. There is nothing too special about it, other than saying it is an LR(1) grammar parsed by the lalrpop tool. There is a side effect the parser has, and that is introducing initialization assignments. This will be discussed in Chapter 3 in more detail. Then, a series of static analyses are performed on the code. This is the part where this project is focused on. The circom compiler includes the usual binding and typing analysis, as well as looking for a return statement in every function’s path. Other functionalities the compiler includes are a bit more specific to circom. A list of them, although not exhaustive, is: •Signal declaration. Signals can only be declared in templates at the top scope. This means that we have to check templates to not declare signals inside an inner block and functions to not declare signals at all. •Return statements in templates. These are not allowed in a template, so much like we did in functions, we now have to check that not a single path in a template carries one of these statements. •Unknown Known analysis. In circom, every component parameter must be known at compile time. In this analysis, each expression in the program is classified as Known or Unknown at compile time. If a component parameter is Unknown or the size of an array (which is always static), an error is issued. •Constant propagation. As we have said, constant values are very important in circom. For this and performance reasons, variables detected to be constant are computed and propagated through the AST . After the static analysis phase, there is a rather special symbolic execution of the code. Here, the compiler will compute the values of the parameters of the templates, which have been checked to be known at compile time. Note that any expression involving a signal is immediately considered an unknown value. While this interpretation of the code is being done, Directed Acyclic Graph (DAG) is created. It will contain information on every component and its associated template. 2.4. Why Rust 9 This is important because each component will generate its own constraints and the DAG helps the compiler to reduce the memory space taken up by every component in the program. Note that for some circuits, the number of components can be huge, but many of them will have the same template and parameters. Once the DAG is created and the constraints extracted, they are simplified to reduce the size of the output, but without ever changing the semantics. In the final part, an intermediate representation is created from which the code that generates the witness is written to the target language. 2.4 Why Rust The circom compiler was originally written in JavaScript in versions 0.0 and 0.5 [9]. The official compiler, Circom 2.0, was rewritten in Rust [10], a general-purpose programming language focused on performance and safety. It also has strong concurrent applications, but this aspect is not exploited in this project. Safety in Rust mainly has to do with memory safety. This means making sure that all references point to valid memory. It is achieved not by a garbage collector or reference counting, which harms performance, but a concept called borrow checker. The borrow checker, ownership and lifetimes are very important concepts that shape the way one can program with Rust, but we will not go into detail. A very good guide to Rust can be found in the Rust handbook [11] or in Rust by examples [12]. All of these fancy Rust concepts do come with their drawbacks, mainly when it comes to mutable references. Some extra effort has been done to work around these issues during the programming made in this project, but once overcome, code safety is nearly assured when it comes to memory issues. 2.5 Static analysis Static analysis plays a critical role in compilers, helping to detect and prevent programming errors before the program is executed. In simple terms, static analysis refers to the process of analyzing code without executing it. This analysis can help detect a wide range of issues, from basic syntax errors to more complex issues like data flow problems and security vulnerabilities. Introductory courses on compilers start by taking a look at the classical lexical, binding and typing analysis, which are all static. However, many more things can be derived from these techniques that range from detecting mistakes from the programmer such as uninitialized variables, to a variety of code optimizations. Although these features do come together in modern compilers, back in the 1980s there was a distinction between debugging compilers and optimizing compilers, depending on whether or not they included some sort of optimization on the code generated [13]. Two of the first compilers that included a powerful optimization chain are Alpha [14] and Fortran H [15]. One of the most common applications of static analysis is in the area of code quality. For example, static analysis tools can be used to detect code smells, which 10 Chapter 2. State of Art are indicators of potential problems in the code. Some common code smells include long methods, duplicate code, and excessive branching. By identifying these issues, developers can make their code more maintainable and easier to understand. In this project, we will focus on unused assignments when it comes to error-prone details in the code. In summary, static analysis is a critical tool for ensuring the quality and security of software code. By analyzing code without executing it, static analysis tools can identify potential issues before they become significant problems. These tools can be integrated into the compiler, providing automatic analysis during the compilation process. However, the more powerful and costly analyses are usually found in external applications, so these heavier computing checkings are not run every time the code is compiled. Some of these tools can be found in [16]. Static analysis plays a central role in code optimization as well. In general, finding the optimal instruction selection and order or the optimal rewrite of the AST is an NP-complete problem [17, 18]. Static analysis can tackle some optimization techniques that, although they might not generate the absolute optimal code, can improve its efficiency at polynomial cost. The central aspect of optimization in static analysis is making semantic-preserving transformations. In [19, 20] an overview of some static analysis techniques concerning optimization is given. However, a more in-depth study can be found in [21, 22]. An approach that will come to our interest is that of Control Flow Graph and Data Flow Graph. The first takes advantage of a transformation of the AST focused on the different branches the code can follow to examine the code [19]. The latter is used at a later stage in optimizing compilers after the CFG has been created. Now the focus is on the relations that the data present when traversing the given paths. This technique dates back to the early 1960s, from Vyssotsky at Bell Labs [23]. However, this analysis usually requires that values are computed if possible, and at the moment we will apply our analysis, this information is still not computed. However, it can be interesting for the reader as similar ideas will be applied. Outside of the classical literature on compilers, there is a lot of work being done related to unused variable detection and uninitialized variable usage. In [24], a developer of RedHat describes how he is improving -Wunitialized of gcc, a specific warning [25] from the famous C compiler. More modern compilers are including these techniques as well. Solang, a compiler for the Solidity environment is implementing unused variable elimination and undefined variable detection [26]. Even data flow graph is helping to improve Psalm 4 compiler in [27]. Chapter 3 Assignment Analysis In this chapter, we will cover the static analysis developed for this project. We start by discussing why this analysis is important to the circom compiler. Afterwards, a correctness, completeness and termination proof is given making some abstractions to simplify the logic required. Finally, some aspects of the implementation are reviewed. 3.1 Importance of the analysis To generate a proper witness that can create a correct validity proof, circom programs must be deterministic. This determinism extends to the value of every single variable and signal. Programs written in other languages might be able to afford to have garbage in their memory, but in this context, this undefined behavior is very harmful. In an ideal world, no one that made a circom program would use anything with garbage in it, but because bad programming practices are everywhere, the circom compiler had to incorporate a mandatory initialization in every variable in case the programmer has not specified an initial value for a var. This is done at the parser level, so after this phase, a variable assignment introduced artificially is essentially the same as an assignment manually coded. However, a simple tag has been added to the compiler to have useful information in the analysis to come. In Listing 3.1 we can see the effect the parser has over the code given. WhatParserGets represents what the programmer would have typed. The parser will then process it, eliminating syntactic sugar and simplifying some structures. One of those simplifications is the one we have mentioned about breaking declarations into a single type, that is, a declaration without initialization followed by a mandatory independent assignment. Both possibilities of this effect can be seen in variables uninitializaed and initialized in the WhatParserGives template. This mandatory initial value came with an additional execution time cost for the code generated. We need to keep in mind that, while a language like C++ can very easily remove unnecessary initializations, that is not the case in the code generated by circom into C++. The signals and variables’ values are implemented as pointers to FieldValue objects, so the C++ compiler will not be able to detect initializations artificially added by the circom parser. There is no need to say that 11 18 Chapter 3. Assignment Analysis 39: function MergeBranches((x, id), State1, State2) 40: if State1=Useful or State2=Useful then 41: return Useful 42: end if 43: if State1=Unknown or State2=Unknown then 44: return Unknown 45: end if 46: if State1=Useless or State2=Useless then 47: return Useless 48: else 49: return NotAppeared 50: end if 51: end function 52: function IfElse((x, id),IfElseGraph, State) 53: State =analyse ((x, id),IfElseGraph.condition, State) 54: Stateif =analyse ((x, id),IfElseGraph.if, State) 55: Stateelse =analyse ((x, id),IfElseGraph.else, State) 56: return MergeBranches ((x, id), Stateif , Stateelse) 57: end function 58: function Loop((x, id),LoopGraph, State) 59: State0=analyse ((x, id),LoopGraph.condition, State) 60: 61: State1.1=analyse ((x, id),LoopGraph.body, State0) 62: State1.2=analyse ((x, id),LoopGraph.condition, State1.1) 63: 64: State2.1=analyse ((x, id),LoopGraph.body, State1.2) 65: State2.2=analyse ((x, id),LoopGraph.condition, State2.1) 66: 67: State0and1=MergeBranches ((x, id), State0, State1.2) 68: State0and1and2=MergeBranches ((x, id), State0and1, State2.2) 69: return State0and1and2 70: end function Proposition 3.2.4. analyse ((x, id),ASTGraph,NotAppeared) = Useless if and only if the assignment with this id is useless in every trace in the Call Graph. Moreover, the call always terminates, i.e. the algorithm is correct and complete. Proof. We first focus on the termination of the algorithm and later on the correctness and completeness. Termination The algorithm is following the AST with two unfolds on the loops, so it is a finite graph. For this reason, the algorithm always terminates. Correctness and completeness It is important to remark on the following when talking about scope. There is a node 3.2. Correctness proof 19 at the end of every block. A variable whose scope ends with that block is considered to be inside of scope in said node and out of scope in the next one. This detail is minor, but necessary to be able to make the next predicate mutually exclusive and always hold during the proof. Let Abe the set of assignments in the AST and Nthe set of nodes in the Call Graph. Then, we define S:A×N → {NotAppeared,Useless,Useful,Unknown}such that S((x, id), node) = NotAppeared if ∀t=t1, node, t2; (x, id)/∈t1 S((x, id), node) = Useless if ∃t=t1, node, t2: (x, id)∈t1 ∧ ∀t=t1,(x.id), t2, node, t3,                ∀node0∈t2, node0does not read x ∧xis out of scope in [node, t3] ∨ ∃(x, id0)∈((x, id), node) : ∀node0∈((x, id),(x, id0)] , node0does not read x S((x, id), node) = Useful if ∃t=t1,(x.id), t2, node, t3:∃node0∈t2:          xis read in node0 ∧ @(x, id0)∈((x, id), node0) : xis not read in (x, id0). S((x, id), node) = Unknown any other case By defining Unknown this way we make sure all cases are covered. One could develop the logic algebra of the last condition, but it ends up being too long to write here. It is enough for the reader to know that there are cases where Scan take the value Unknown. Intuitively, it means that the assignment has appeared in a trace, but we cannot say for now whether it is useless in every trace that reaches this node or if it is useful in a single trace. In particular, in the traces where that assignment has appeared it has not been read yet. It can be seen, with a little work, that all of these cases are mutually exclusive. This is very important as it allows Sto be a welldefined function. Because it is a function, we will obtain the proof of completeness for free when proving correctness. We prove by induction on the structure of the AST that, for every graph associated with a node from the AST, called Graph, we have analyse ((x, id), Graph, S((x, id), P (Graph))) = S((x, id), L (Graph)) Reading between lines, what P(Graph)and L(Graph)are doing is extending the result of Sto the next node in the AST . Note how if two instructions are consecutive in a block L(Graph1) = P(Graph2), or how P(Graphif ) = nodecondition and LGraphif/else=nodemerge in and If/Else structure. 20 Chapter 3. Assignment Analysis We now distinguish cases on the type of graph and the argument State: •Reader node. –State =NotAppeared. If the assignment has not appeared yet, then it will not have appeared after this node as it is not an assignment, so the result NotAppeared is correct. –State =Useful. Because there was already a node0where xwas read after the assignment, whether xis read here or not does not change the logic value, so the result Useful is correct. –State =Useless. There exists a trace where (x, id)appeared, so it will still be there, and in those where it appeared there is already an assignment that overwrites or it cannot be read anymore. In the first case whether xis read here or not will not change the truth value, and in the second one, we know it cannot be read here by the precondition because it is out of scope, so it would still be true. –State =Unknown. If xis read here, then we know that, because there exists a trace where (x, id)appears, that same trace will hold that ∃node0∈ t2, node:xis read in node0and @(x, id0)∈((x, id), node0) : xis not read in (x, id0). This last part we know from State 6=Useless and this node not being an assignment. Then the Useful return value is correct. If x is not read, then the State =Unknown property can be extended to this node. •Assignment node. –State =NotAppeared. If the assignment has not appeared yet and neither is this assignment the one with that id, then it will not have appeared after this node, so the result NotAppeared is correct. Now suppose we have just found the correct assignment. Then certainly the result cannot be NotAppeared anymore. It cannot be Useful, as t2is empty and it cannot be Useless because firstly, xcannot be out of scope on the next node as it has just been used and, at most, the next node could be the end of the block which we clarified counted as part of the scope of x(This is the part of the proof where that clarification was important). Secondly, the interval ((x, id), node]is empty. Then, the only valid result must be Unknown. –State =Useful or State =Useless. Same as in the previous case, no matter what happens in this node, the State =Useful or State =Useless property will extend nicely. –State =Unknown. If xis read here, this is the same case as in a Reader node, and the only valid result is Useful again. If it is not read here, but overwritten, then take t=t1,(x, id), t2,(x, id0), t3any trace where the assignment appeared and where (x, id0)is referring to this node. We know xhas not been read since, then ∃(x, id0)∈((x, id),(x, id0)] : ∀node0∈ 3.2. Correctness proof 21 ((x, id),(x, id0)] , node0does not read x. Then Useless is the correct result. If xis not read, nor overwritten, then the State =Unknown property can be extended to this node. •Block. We studied how the Induction Hypothesis simply extends correct values of Sone node further. With it, the looping we are doing over consecutive statements makes them have the proper argument and return values. Then, after the loop we have State =S((x, id), L (Graphn)). –State 6=Unknown. At the end of the block no variable can be read, overwritten or any assignment can appear, so all other values but Unknown extend perfectly to this node and would hold the definition of S. –State =Unknown. Take any trace t=t1,(x, id), t2, end_block, t3. We know xhas not been read since (x, id). Suppose xis going out of scope in this node. This means that xis in scope in end_block but not in (node, t3]. Then ∀node0∈((x, id), end_block], node0does not read x∧xis out of scope in (end_block, t3]. This means that the Useless value is holding here. If xis not going out of scope, then nothing changes about the rest of the conditions, so the Unknown value extends to this node. Before continuing with the other two nodes, let us see how State works when merging branches. Suppose there is a node where the traces can either be t=t1, t2, node, t4 or t=t1, t3, node, t4, meaning t2and t3are the supposed different branches an execution trace could have taken. We want to see what is the proper State after node, so the value of Sreturned is the one defined above. Suppose the State at the end of t2is Useful. Then, the trace that exists in t1, t2, node, t3will still exist in the set of traces made by the union, so the result at node will still be Useful. Suppose now that the State at the end of t2is Useless and the result at the end of t3is either Useless or NotAppeared. We know there is a branch where (x, id)has appeared, so we do not need to worry about the first proposition of the and. Focus on the second one. Take any trace tthat goes through node. If that trace does not contain (x, id)we have nothing to worry about. If t=t1,(x, id), t0, node, nodemerge, t3 then it comes from a branch where the State was Useless. Then for that trace the proposition ∀node0∈((x, id), node], node0does not read x ∧xis out of scope in (node, t3] ∨ ∃(x, id0)∈((x, id), node] : ∀node0∈((x, id),(x, id0)] , node0does not read x 22 Chapter 3. Assignment Analysis holds. Then, as no assignment or reading happens at a merge node the proposition ∀node0∈((x, id), nodemerge], node0does not read x ∧xis out of scope in (node, t3] ∨ ∃(x, id0)∈((x, id), nodemerge] : ∀node0∈((x, id),(x, id0)] , node0does not read x holds. By universal generalization, the State must be Useless after nodemerge. It is immediate to see that the only case where the State can be NotAppeared is when both states after t2and t3are NotAppeared. Remark that the previously described cases are the only ones where those results could hold properly. This leaves us with the only option for the remaining cases to be Unknown. This behavior is described in this rather pleasing table for the result of MergeBranches. MergeBranches Useful Unknown Useless NotAppeared Useful Useful Useful Useful Useful Unknown Useful Unknown Unknown Unknown Useless Useful Unknown Useless Useless NotAppeared Useful Unknown Useless NotAppeared Table 3.1: Result of merging branches The only thing left to do is check that the code does exactly this with the results, which is immediate too. Now that we know that calling MergeBranches allows us to keep the postconditions referring to two branches, and by induction can be extended to any number of branch merging, we continue with the proof. •If/Else node. We can see how the calling properly propagates the value of Sas in the Block case and how P(Graphif ) = P(Graphelse) = nodecondition. Then by the behavior of MergeBranches that we just saw, we prove that the value returned follows Sdefinition. •While node. Same as in If/Else case, only that we are now merging the branches with zero, one and two loops as we represented in the Call Graph. We have then proved that, given the proper value for State, the result follows S definition. Now we check that the State value of NotAppeared is the correct one in the first call and check what is the value of S((x, id), L (AST)) Because we are the beginning of the AST ,State =NotAppeared makes perfect sense. Because these states are mutually exclusive we do not need to check anything else, Sdefinition hold. Now take the result is Useless at the last node, which we will call nodeEND. This node, by the construction of the AST ends every possible 3.2. Correctness proof 23 variable’s scope. So, by substituting, and having in mind that any set of nodes after nodeEND is an empty set, we get ∃t=t1, nodeEND : (x, id)∈t1, nodeEND ∧ ∀t=t1,(x.id), t2, nodeEND,                ∀node0∈((x, id), nodeEND], node0does not read x ∧xis out of scope in (nodeEND, nodeEND] ∨ ∃(x, id0)∈((x, id), nodeEND] : ∀node0∈((x, id),(x, id0)] , node0does not read x. If we define that a scope is out of scope in the empty set, then we can just ignore that part and see how this says that there is a trace where (x, id)appears, and in those that it happens I or II hold. So (x, id)is useless in every single trace. Because a piecewise definition of a function is, essentially, a double implication, if (x, id) appears in a trace and it is useless in every single one of them, then the result will be Useless, and hence we have proved completeness as well. We have proved the correctness of the algorithm, but our call graph only covers execution traces with at maximum two unfoldings of a loop. Our analysis aims to cover every possible execution trace, so we need to show that this level of unfolding covers all possible execution traces. Proposition 3.2.5. An assignment is useless in every trace of the Call Graph iff it is useless in every execution trace. Proof. The only difference in structure between our call graph and the execution traces graph is the depth of unfolding of the loops. If we prove by induction over the number of iterations that an assignment is useless in a trace with niterations iff it is useless in a trace with n+ 1 iterations for n≥2, then we have proven by induction on the structure of the graphs that the call graph contemplates every execution traces as it reaches a fixed point on the analysis result with 2 iterations of a loop. Denote by next a trace that starts just after the loop, by body a path on the call graph that represents the body of the loop, by condition the node where the condition of the loop is evaluated and by frag a fragment of body that reaches the end (this represents an assignment that happens inside the loop). We want to prove the following: •I∨II holds on the traces condition, next and condition, body, condition, next iff it holds on the traces condition, {body, condition }∗, next. •I∨II holds on the traces frag, condition, next and frag, condition, body, condition, next iff it holds on the traces frag, condition {body, condition }∗, next. 24 Chapter 3. Assignment Analysis We prove it for the first case only, as the other is completely analogous. The rightto-left implication is obvious. Suppose I ∨II holds for the trace condition, {body, condition }n i=0, next for n≥2. If II holds, xis not read in condition,body or next, so it will not be read in condition, {body, condition }n+1 i=0 , next. If I holds, the new assignment could be in {body, condition }n i=0 or in next. If it is in body, then I still holds for {body, condition }n i=0 body, condition, and if it is in next, I implies that x is not read in {body, condition }n i=0 so neither will it be read in {body, condition }n+1 i=0 making I still hold for condition, {body, condition }n+1 i=0 , next 3.2.3 Multiple Variables approach The previous algorithm has to run the analysis for every single variable in the program. Now we will do all that processing at the same time for every assignment in the program. For that, instead of having a State, we will have sets where belonging to them means having that equivalent state. The special case of NotAppeared will be represented by not being in any of those sets. See how that works nicely for an easy initialization. In this algorithm, it will be easier to see how they are disjoint and so, the conditions that they represent are mutually exclusive. Algorithm 2 Multiple variables approach 1: function Reader(ReaderGraph,Unknown,Useful,Useless) 2: NewUseful ={(x, id)∈Unknown:x∈ReaderGraph.L} 3: Unknown =Unknown \NewUseful 4: Useful =Useful ∪NewUseful 5: end function 6: function Assignment(AssigGraph,Unknown,Useful,Useless) 7: NewUseful ={(x, id)∈Unknown:x∈AssigGraph.rhe} 8: Unknown =Unknown \NewUseful 9: Useful =Useful ∪NewUseful 10: 11: NewUseless ={(AssigGraph.y, id)∈Unknown} 12: Unknown =Unknown \NewUseless 13: Useless =Useless ∪NewUseless 14: 15: if (AssigGraph.y,AssigGraph.id)/∈Unknown ∪Useful ∪Useless then 16: Unknown =Unknown ∪ {(AssigGraph.y,AssigGraph.id)} 17: end if 18: end function 3.2. Correctness proof 25 19: function Block(BlockGraph,Unknown,Useful,Useless) 20: for each Graph ∈BlockGraph.SubGraphs do 21: analyse (Graph,Unknown,Useful,Useless) 22: end for 23: NewUseless ={(x, id)∈Unknown:x∈BlockGraph.OutingVariables} 24: Unknown =Unknown \NewUseless 25: Useless =Useless ∪NewUseless 26: end function 27: function MergeBranches(Un1, Un2, Ful1, Ful2, Less1, Less2) 28: Useful =Ful1∪Ful2 29: Unknown = (Un1∪Un2)\Useful 30: Useless = (Less1∪Less2)\(Useful ∪Unknown) 31: return Unknown,Useful,Useless 32: end function 33: function IfElse(IfElseGraph,Unknown,Useful,Useless) 34: analyse (IfElseGraph.condition,Unknown,Useful,Useless) 35: Makes copies of Unknown,Useful,Useless 36: analyse IfElseGraph.if,Unknownif ,Usefulif ,Uselessif  37: analyse (IfElseGraph.else,Unknownelse,Usefulelse,Uselesselse) 38: Unknown,Useful,Useless =MergeBranches    Unknownif ,Unknownelse, Usefulif ,Usefulelse, Uselessif ,Uselesselse    39: end function 40: function Loop(LoopGraph,Unknown,Useful,Useless) 41: analyse (LoopGraph.condition,Unknown,Useful,Useless) 42: 43: Makes copies of Unknown,Useful,Useless 44: analyse (LoopGraph.body,Unknown1,Useful1,Useless1) 45: analyse (LoopGraph.condition,Unknown1,Useful1,Useless1) 46: 47: Makes copies of Unknown1,Useful1,Useless1 48: analyse (LoopGraph.body,Unknown2,Useful2,Useless2) 49: analyse (LoopGraph.condition,Unknown2,Useful2,Useless2) 50: 51: Unknown,Useful,Useless =MergeBranches    Unknown,Unknown1, Useful,Useful1, Useless,Useless1    52: Unknown,Useful,Useless =MergeBranches    Unknown,Unknown2, Useful,Useful2, Useless,Useless2    53: end function 26 Chapter 3. Assignment Analysis Proposition 3.2.6. Let Unknown =∅,Useful =∅,Useless =∅, then the following statements are equivalent: •(x, id)∈Useless after analyse (ASTGraph,Unknown,Useful,Useless)has been executed. •(x, id)is useless in every trace of the Call Graph. Moreover, the algorithm always terminates. Proof. Termination is the same as the previous algorithm. We focus on correctness and completeness. All we have to do is check that we are keeping the same conditions on the elements (x, id)as we did in the algorithm for one assignment at a time. Suppose we are always talking about the same stage of the analysis, i.e. if we say that in the call analyse (Graph,Unknown,Useful,Useless),(x, id)∈Unknown ⇐⇒ State =Unknown in the call analyse ((x, id),Graph, State), we mean that both graphs are the same graph in the Call Graph and the same logic applies to the rest of sets, results, etc. So we want to check that •(x, id)∈Unknown ⇐⇒ State =Unknown •(x, id)∈Useful ⇐⇒ State =Useful •(x, id)∈Useless ⇐⇒ State =Useless •(x, id)/∈Unknown ∪Useful ∪Useless ⇐⇒ State =NotAppeared As we start the call with all empty sets, the first call is coherent between both algorithms. For the rest of the calls, we suppose that those properties are respected in the argument sets and show that the same is true for the value returned by the first algorithm and the changes made on these sets during the function. To lighten the proof, we will compare each function in a kind of informal way. The easiest one to compare is the MergeBranches with the Table3.1 and see that those sets created do respect the merge operation. Now we compare the different kinds of nodes function: •Reader node. The only difference between State value and returned value occurs when an Unknown assignment has its variable appearing in the read variables. That is exactly the change made in the second algorithm, making sure that both sets stay disjoint. •Assignment node. The first change happens if the State is Unknown. We take assignments in Unknown that are read and swap them to Useful set and after that swap elements in the remaining Unknown set to Useless set when the variable overwritten is the same as the assignment in Unknown. The other difference between the argument State and returned value in the first algorithm happens when State is NotAppeared. In our function that means not being in 3.3. Bringing the analysis to real code 27 any of the sets, which is the if condition. Inside here, when the ids coincide, we swap it from NotAppeared state to Unknown set. See how that is the same thing that is done in the first approach. It is easy to check how assignments that were already in Useful or Useless sets stay in them, as the first algorithm does when the argument State is any of the equivalent ones. •Block. Same as before, looping like this through statements carries nicely the properties. If we turn our attention to the OutingVariables part, we see how we are swapping elements in Unknown whose variables are going out of scope to the Useless set, whose equivalence was done in the other approach. •If/Else node. See how making a copy of these sets is the same as storing the value of the State and not touching it until the mergings occur. This also applies to the next case. After propagating the properties through the reader node of the condition and the blocks of the if and else part, MergeBranches does the same as we have seen, so properties are carried to the merging node. •While node. In the same way we have just shown, we are merging the properties of zero, one and two loop iterations. If we focus on what (x, id)∈Useless after the execution means, having in mind the analogy made before, we see how it is equivalent to having obtained Useless in the first analysis, so the same properties of correctness and completeness hold. 3.3 Bringing the analysis to real code The algorithm described needs to be adapted to the actual code. To that end, some functionalities need to be added by reusing existing code when possible. We will recover here the AST structures were left behind in the proof, discuss some improvements that were considered at the time and describe the warnings added. 3.3.1 Implementation The first thing we need to do is make sure that variables have a unique identifier. We gave this for granted when specifying the pseudocode, but in reality, we need to respect variable shadowing, which makes variable names not a unique characterization of a position of memory. To solve this we have used a circom Environment that maps variable names to an integer taking care of block logic. All we have to do is make sure we are introducing a block in the Block function and popping it at the end. This structure has been lightly modified to be able to obtain the Outing Variables set before popping the upper block. Assignments are no longer represented just by their id and their variable name, they also include information about the instruction to add a warning. This makes the analysis useful to build on top of it future functionalities that are easily derived from knowing which assignments are never used. 34 Chapter 4. Benchmarking Figure 4.1: Game event in Dark Forest. Source [37]. Gubsheep & Dark Forest © despite being a very simple game by nowadays standards, it is played by thousands of people. 4.2 Evaluation process We are interested in assessing if eliminating unnecessary assignments in the witness code improves its execution time. To evaluate these times in a significant amount of circuits some bash and Python scripts have been developed. They help us in collecting the data, offered by the compiler, measuring execution times and putting all results together in a common directory. At first, only a bash script was used to measure execution times. This means that a lot of noise from preparing the executable by the system is introduced, making the times less reliable. To reduce the noise in the executions only C++ code was assessed, leaving WebAssembly out of the question. An improvement in C++ will traduce into WebAssembly, although not in the same order given all that surrounds web programming languages. Because we were dealing only with C++ and we wanted to eliminate the time it takes to call a binary, the inside common code of every C++ output that circom generates has been modified so it measures time inside the program with a high-resolution clock and outputs that information into a file, common among different executions. We have tested the analysis against the compiler with the same version but without any modification from this project, i.e the code from the official repository, always up-to-date. Bear in mind that this project has been developed while merging every update from the parent of the fork, so the code outside this analysis is always 4.3. Performance 35 common. After compiling both versions with different names we could execute a significant amount of times the code written by each compiler, saving execution times in separate files. We accounted for a test as valid when the standard deviation of the measurements was similar and took the mean as the result. All of the previous projects have more than just circom circuits. They have unitary tests, snarkjs integration, etc. We were only interested in circuits that have a set of inputs, either as a JSON file or inside the testing code. We have also excluded the smaller circuits as their execution times tend to be a bit more unstable. The number of times each program was run varied between 40 and 2000, depending on how long it took to execute once. Some smaller circuits even appeared to be slower with the new code. To determine whether something strange was happening, we profiled the code with Valgrind and compared the output code. The only difference with the older code was the disappearance of the useless assignments. The binaries were checked to be different after g++ compiled them with O3 optimization. The conclusion was that due to compiler optimization and small execution times, unstable execution times were bound to appear, but the code was completely fine. Every test included a final bash command (diff) to see whether the witness created were the same. It is most important to remark that not a single program created by this project’s compiler created a witness different from that computed by the official version of circom. This reassures the fact that the implementation done matches that described in Chapter 3. 4.3 Performance All of the following tests were run on a Linux Mint 20.2 (5.4.0 kernel version) machine, with an Intel i5-6600K (3.9 GHz), 16GB of RAM and 32 GB of swap memory. We first start by assessing the impact on the compiler itself. We want to see whether running this analysis harms the compiler’s performance. The analysis checkings done at each node are linear in the number of variables read in the node and the amount of assignments in the whole program. This is thanks to using HashMaps and HashSets. Although these structures’ performance can decay in the worst of ways if their size is very large, we are sure that no circom program will ever reach that number of assignments to show this property. If this was ever to happen, much bigger problems would arise. Bearing in mind that the work at each node is linear, we now focus on the path followed in recursion calls. A node is traversed once unless it is part of a loop. In that case, a loop is analysed twice. That means that in the worst case, the number of nodes traversed scales as a power of 2 to the nesting level of loops. Because no program ever has a nesting level too high, this will neither harm the performance. Once the theoretical aspects are clear, we focus on some real testing. To profile the compiler, a common tool for Rust programs has been used. This is Flamegraph [40], a visual tool that creates an interactive svg file. It can be opened with a web browser to explore where the execution time was spent. It calculates these times by 36 Chapter 4. Benchmarking taking periodic samples while the code is running and assessing where it is at the moment. To illustrate how much this analysis hurt the compiler, we should say that the most difficult task with this process other than installing the tool, was to find an execution where a single sample had landed on the analysis so it could be shown in the diagrams. In other words, the analysis takes virtually no time compared to the rest of the compilation, in line with the rest of the static analysis of circom, which takes a minimal fraction of the computational effort. Figure 4.2: Flamegraph output. Purple fraction corresponds to the type analysis of the compiler In Figure 4.2, the times breakdown of the whole execution can be seen. This profiling was done by compiling an averaged size circuit from the circom ECDSA library (pubkeygen.circom). No output was asked for, so these execution times do not even include code generation and constraints output. It only takes into account parsing, static analysis, code interpretation and constraints simplification. The static analysis is highlighted in purple in Figure 4.2. In Figure 4.3, the static analysis (called type analysis in the code) has been zoomed and the assignments analysis highlighted in purple again. We can see how it takes the same effort as the rest of the static analysis previously developed. With 5 samples landing in our analysis, it means a 0.04% of the total execution time. Figure 4.3: Zoom into type analysis. Purple fraction corresponds to the implemented analysis On the performance of the witness calculators, the results are not that regular. Many factors play a part in the execution time of a program, and although eliminat- 4.3. Performance 37 ing useless instructions should decrease the computational effort, in reality, there is not a clear correlation between the number of instructions eliminated and the improvement in performance gained. It is remarkable, however, that with a virtually free-of-cost analysis, we can achieve up to a 3% improvement in the bigger witnesses. Results have been especially good in the ECDSA repository, where output programs are much bigger. In Table 4.1 there is a list of the circuits tested. Circuit Assignments Eliminated Performance Improvement Total Execution Time ECDSA-eth_addr 4.3% 1.6% 183 seconds ECDSA-groupsig 4.5% 3.0% 180 seconds ECDSA-pubkeygen 3.2% 3.1% 171 seconds ECDSA-verify 2.6% 3.4% 577 seconds ED25519-batchverify 10.5% 0.0% 115 seconds ED25519-scalarmul 9.6% 0.6% 81 seconds ED25519-verify 9.5% 0.4% 223 seconds forest-init 14.5% 0.0% 18 seconds forest-move 14.5% 0.7% 19 seconds forest-move 14.5% 0.1% 19 seconds forest-whitelist 21% -0.5% 16 seconds ML-mnist 5.7% 0.2% 160 seconds ML-mnist_precision 3.4% 0.1% 1193 seconds Rollup-16 10.8% 0.2% 99 seconds Rollup-16_1 10.8% 0.5% 117 seconds Table 4.1: Performance improvements for different circuits From the percentage of assignments eliminated, the majority of them were artificially added assignments by the circom parser. The other fraction of useless assignments were usually made useless by the constant propagation phase, so the programmer themselves had not done anything wrong. Although this seems to decrease the importance of some aspects we deemed useful, we have to keep in mind that these circuits are mostly developed by experts and their writing process is almost over. Having a feature in the compiler that points out useless assignments introduced by the programmer is much more useful during the developing stages of circuits. Chapter 5 Conclusions In this last chapter, the conclusions drawn from this project will be presented. To that end, we summarize the development done and what has been achieved with it. The first thing that was done in the project was to study an unknown code base. Given that a compiler’s code is not always the easiest to understand and the programming language it is written in was also unknown at first, the process was slow. It is clear now that one of the best approaches found with this project was an initial read on the programming language basics followed by an example-driven learning period. To achieve Objective I, active communication with the developers eased the process. It is however crucial to get a first impression of the project’s structure and begin taking notes from early impressions so one can recover those ideas later. The task of understanding a whole code repository is long, so one will inevitably forget what was deduced previously unless it is written down. A relevant aspect of the project has been learning to program in Rust. As mentioned in Chapter 2, Rust has some special features regarding memory usage. Along with its matching structures make the learning curve quite steep one. Once overcome, some other aspects of the language make it look advantageous. For instance, the compiler gives very good hints on what is wrong in the code. Pattern matching and enumerates allow for very flexible structure creation, which fits perfectly the AST components, for example. The care the compiler places over code safety comes as a nuisance at first, but it can be helpful when it comes to being sure that no undesired side effects or data races are present in the code once it compiles. In the light of present Rust uprising popularity, getting to know this programming language will hopefully come as useful in the future too. Fulfilling Objective II, it has come clear the importance of static analysis. It is a cheap way, computation wise, to detect errors in the development process. Detecting this kind of error in the compiling process helps programmers save a lot of time debugging and getting runtime errors. Static analysis also plays a huge role in code optimization. Not every optimization can be left to lower level code or CPU level dynamic optimization. Some abstractions are useful when it comes to understanding the semantics of a program, and not using this information in static analysis is neglecting a big opportunity for better code performance. Although the techniques studied in classic books in Section 2.5 were not implemented exactly in 39 40 Chapter 5. Conclusions the project, the ideas given by the most popular references in compilers can always be found in one’s approach to these problems. Semantic proving has always been an elusive aspect in Computer Science. While having wonderful mathematical properties and providing with the rigor and safety mathematical tools give, its complexity scales very rapidly with a program’s size. Not only that, even the constructions allowed by a programming language can make semantic proving a titanic task. In this project, a lighter approach was taken. The algorithm’s proof was broken down into two phases. The second one made heavy use of the properties given by the first proposition and thus showed how to carry a simpler program’s features into a more complex one that follows a similar schema. General semantic proving has not been found any easier in this project, and that is why it was not the desired approach. It has however born out useful to make a specific proof for the analysis. It not only assured the properties sought but helped to clean the code and its data structures. There is no better way of assuring we have fulfilled Objective III than a proper mathematical proof. Being more specific about circom, code safety has been improved. Not using variables which were assigned a signal is a very common error among circom developers. Although not an error itself, it is a very strong indicator of a programmer’s mistake. This analysis has proven effective in detecting this situation, and the hope is it will save developers valuable time when building their circuits. Falling back to our objectives, this clearly covers Objective IV. Although this was not an objective on its own, developing a small suite of scripts to help benchmark the compiler has proved a good way of finally learning bash. Having to test with various repositories, each with its own structure, led to the creation of these scripts. The filtering, redirection of output and easy management of directories have come in very handy to center the benchmarking results. This has made the processing and analysis of the tests’ data an easier task. It has also proven a suitable use for a scripting language like Python. Hence, an additional learning outcome of the project has been that scripting language can automate day-to-day computer tasks with little effort. On a last note, Objective V has been completed to a certain degree. It was at first thought that this additional time overhead created by the parser was significant enough to be worth getting rid of. While it has proven irregular at times, and not too worrying at others, we have been able to eliminate this overhead in every program in case there was any. The percentage of improvement might not seem much at first, but taking into account that we can reach up to a 3.5% improvement with an analysis that only costs around 0.05% of the compiler’s time, it is regarded as a worthy investment. Due to this, it is planned to include the analysis developed in the official circom repository in the near future. Therefore, this project will be part of a compiler used by thousands of developers. Bibliography [1] J.-J. Quisquater, M. Quisquater, M. Quisquater, M. Quisquater, L. Guillou, M. A. Guillou, G. Guillou, A. Guillou, G. Guillou, and S. Guillou, “How to explain zero-knowledge protocols to your children,” in Advances in Cryptology—CRYPTO’89 Proceedings, pp. 628–631, Springer, 2001. [2] B. Parno, J. Howell, C. Gentry, and M. Raykova, “Pinocchio: Nearly practical verifiable computation,” Communications of the ACM, vol. 59, no. 2, pp. 103– 112, 2016. [3] J. Bootle, A. Cerulli, P. Chaidos, J. Groth, and C. Petit, “Efficient zeroknowledge arguments for arithmetic circuits in the discrete log setting,” in Advances in Cryptology–EUROCRYPT 2016: 35th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Vienna, Austria, May 8-12, 2016, Proceedings, Part II 35, pp. 327–357, Springer, 2016. [4] E. Ben-Sasson, A. Chiesa, E. Tromer, and M. Virza, “Succinct non-interactive zero-knowledge for a von neumann architecture,” in 23rd {USENIX}Security Symposium ({USENIX}Security 14), pp. 781–796, 2014. [5] B. WhiteHat, J. Baylina, and M. Bellés, “Baby jubjub elliptic curve,” Ethereum Improvement Proposal, EIP-2494, vol. 29, 2020. [6] iden3, “Circom documentation.” Available at https://docs.circom.io/ (27/04/2023). [7] iden3, “Circom repository.” Available at https://github.com/iden3/circom (27/04/2023). [8] M. Bellés-Muñoz, M. Isabel, J. L. Muñoz-Tapia, A. Rubio, and J. Baylina, “Circom: A circuit description language for building zero-knowledge applications,” IEEE Transactions on Dependable and Secure Computing, 2022. [9] iden3, “Old circom repository.” Available at https://github.com/iden3/ circom_old (27/04/2023). [10] H. García Navarro, “Design and implementation of the circom 1.0 compiler,” UCM eprints, 2020. 41 42 BIBLIOGRAPHY [11] RustFoundation, “The rust handbook.” Available at https://doc.rust-lang. org/stable/book/ (27/04/2023). [12] RustFoundation, “Rust by examples.” Available at https://doc.rust-lang. org/rust-by-example/ (27/04/2023). [13] L. T. Keith D. Cooper, Engineering a Compiler. ACADEMIC PRESS, second ed., 2012. [14] A. P. Yershov, “Alpha—an automatic programming system of high efficiency,” Journal of the ACM (JACM), vol. 13, no. 1, pp. 17–24, 1966. [15] E. S. Lowry and C. W. Medlock, “Object code optimization,” Communications of the ACM, vol. 12, no. 1, pp. 13–22, 1969. [16] Wikipedia, “List of tools for static code analysis.” Available at https: //en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis (2/05/2023). [17] J. Bruno and R. Sethi, “Code generation for a one-register machine,” J. ACM, p. 502–510, 1976. [18] A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: principles, techniques, and tools. Addison-wesley Reading, second ed., 2007. [19] A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: principles, techniques, and tools, ch. 8 and 9. Addison-wesley Reading, second ed., 2007. [20] L. T. Keith D. Cooper, Engineering a Compiler, ch. 8 and 9. ACADEMIC PRESS, second ed., 2012. [21] K. Kennedy and J. R. Allen, Optimizing compilers for modern architectures: a dependence-based approach. Morgan Kaufmann Publishers Inc., 2001. [22] R. Morgan, Building an optimizing compiler. Digital Press, 1998. [23] V. Vyssotsky and P. Wegner, “A graph theoretical fortran source language analyzer. at & t bell laboratories, murray hill, nj,” Manuscript, 1963. [24] D. Malcolm, “The state of static analysis in the gcc 12 compiler.” Available at https://developers.redhat.com/articles/2022/04/ 12/state-static-analysis-gcc-12-compiler# (2/05/2023). [25] gcc GNU, “Options to request or suppress warnings.” Available at https:// gcc.gnu.org/onlinedocs/gcc/Warning-Options.html (2/05/2023). [26] L. Steuernagel, “Implementing unused variable elimination and undefined variable detection for the solang compiler.” Available at https://medium.com/coinmonks/implementing-unused-variable... (2/05/2023). BIBLIOGRAPHY 43 [27] M. Brown, “Better unused variable detection in psalm 4.” Available at https: //psalm.dev/articles/better-unused-variable-detection (2/05/2023). [28] A. Sankar, “Classical and quantum algorithms for isogeny-based cryptography,” Master’s thesis, University of Waterloo, 2015. [29] C. Costello, P. Longa, and M. Naehrig, “Efficient algorithms for supersingular isogeny diffie-hellman,” in Advances in Cryptology–CRYPTO 2016: 36th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2016, Proceedings, Part I 36, pp. 572–601, Springer, 2016. [30] A. J. Di Scala, A. Gangemi, G. Romeo, and G. Vernetti, “Special subsets of addresses for blockchains using the secp256k1 curve,” Mathematics, vol. 10, no. 15, p. 2746, 2022. [31] “circom-ecdsa repository.” Available at https://github.com/0xPARC/ circom-ecdsa/tree/master (18/05/2023). [32] S. Nakov, Practical Cryptography for developers, ch. Digital signatures, EdDSA and Ed25519. online, 2018. [33] E. Labs, “circom ed25519 repository.” Available at https://github.com/ Electron-Labs/ed25519-circom (20/05/2023). [34] “Hermez 1..0 documentation.” Available at https://docs.hermez.io/Hermez_ 1.0/about/scalability/ (20/05/2023). [35] H. Pan, F. Ho, and H. Palacci, “Zk machine learning.” Available at https: //0xparc.org/blog/zk-mnist (20/05/2023). [36] B. Gu, “Dark forest repository.” Available at https://github.com/ darkforest-eth/darkforest-v0.6/tree/main (20/05/2023). [37] R. Khan, “dark forest: a one-of-a-kind sci-fi blockchain game built on cutting-edge cryptography.” Available at https://www.designboom.com/technology/dark-forest-one-of-a-kind... (20/05/2023). [38] R. Das, “How to play dark forest, the zksnark powered mmo game.” Available at https://medium.com/coinmonks/how-to-play-dark-forest-the... (20/05/2023). [39] B. Gu, “Dark forest webpage.” Available at https://zkga.me/ (20/05/2023). [40] B. Gregg, “Flamegraph repository.” Available at https://github.com/ brendangregg/FlameGraph (20/05/2023).