Design and implementation of the Circom 1.0 compiler

The central element of the Circom project is the Circom programming language. This programming language is used for designing arithmetic circuits, which will be used in the field of cryptography. Circom programs, like most computer programs, are a set of instructions that can be executed by a computer. In this case, the execution mimics the behaviour of some arithmetic circuit. Unlike most computer programs, Circom programs are also an executable specification that, when interpreted, will produce the set of constraints of the arithmetic circuit. The Circom programming language is unique because its expressiveness allows compressing in the same code the behaviour of an arithmetic circuit and its restrictions. To take advantage of such a special programming language the Circom compiler is needed. Like Circom programs, the Circom compiler encapsulates two different behaviours. When given a Circom program the Circom compiler will translate the circuit into a target language so the circuit can be executed. The Circom compiler will also behave as an interpreter and treat the Circom program as an executable specification, by executing this specification the Circom compiler will produce the constraints of the given circuit. The Circom 1.0 compiler is a new compiler for this programming language partly developed for this thesis. The part developed for this thesis is formed by the structure and semantics analyses of Circom programs and the constraint generation. These elements of the Circom 1.0 compiler are the ones that take most advantage of the knowledge obtained in the master on formal methods. This thesis will start by providing some context to the Circom project, its history and where it is used. Following this will be an introduction to the Circom programming language and an overview of the elements that form the Circom 1.0 compiler. Most of this thesis length will be used to explain the type analysis of Circom programs, the unknown-known analysis and the constraint generation. This thesis also includes a chapter of experiments, where the perfomance and scalability of the Circom 1.0 compiler is tested. To conclude this thesis some conclusions will be given and the future work will be exposed.