Publication:
Design and implementation of the Circom 1.0 compiler

dc.contributor.advisorRubio Gimeno, Alberto
dc.contributor.authorGarcía Navarro, Hermenegildo
dc.date.accessioned2023-06-17T10:16:27Z
dc.date.available2023-06-17T10:16:27Z
dc.date.issued2020
dc.descriptionTrabajo de Fin de Máster en Métodos Formales, Facultad de Informática UCM, Departamento de Sistemas Informáticos y Computación, Curso 2019/2020
dc.description.abstractThe 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.
dc.description.abstractCircom, como proyecto, tiene de elemento central el lenguaje de programación Circom. Este lenguaje de programación es usado para diseñar circuitos aritméticos, que serán usados en el campo de la criptografía. Al igual que los programas escritos en otros lenguajes, los programas escritos en Circom son un conjunto de instrucciones que pueden ser ejecutadas por un computador. La diferencia de los programas escritos en Circom es que estos también son una especificación ejecutable que, al ser interpretada, produce el conjunto de restricciones del circuito aritmético. Para aprovechar todo el potencial de este lenguaje de programación se necesita el compilador de Circom. Al igual que los programas escritos en Circom, este compilador agrupa dos comportamientos distintos. Cuando este compilador recibe un programa escrito en Circom este será traducido a un lenguaje destino. Por otro lado, el compilador de Circom se comportará como un intérprete del programa recibido y producirá el conjunto de restricciones del circuito. Para este trabajo de fin de máster se ha desarrollado parte de la versión 1 del compilador de Circom. Las partes elegidas para este trabajo de fin de máster son los análisis semánticos y estructurales de los circuitos y la generación de restricciones. Estos elementos son los que mejor representan como la versión 1 del compilador de Circom aprovecha el conocimiento adquirido en el máster de métodos formales para mejorar las versiones anteriores. Esta memoria comenzará aportando un contexto al proyecto Circom, contando su historia y donde es usado. A continuación se dará una introducción al lenguaje de programación y un resumen de los elementos que forman parte de esta nueva versión del compilador. La mayor parte de esta memoria está dedicada al análisis de tipos, al análisis unknown-known y a la generación de restricciones. Esta memoria también incluye un apartado de experimentos, donde se ha puesto a prueba la escalabilidad y eficiencia de esta nueva versión del compilador. Esta memoria terminará exponiendo las conclusiones obtenidas de este trabajo y los avances que se harán en el futuro.
dc.description.departmentDepto. de Sistemas Informáticos y Computación
dc.description.facultyFac. de Informática
dc.description.refereedTRUE
dc.description.statusunpub
dc.eprint.idhttps://eprints.ucm.es/id/eprint/62475
dc.identifier.urihttps://hdl.handle.net/20.500.14352/9079
dc.language.isoeng
dc.master.titleMáster en Métodos Formales
dc.page.total38
dc.rightsAtribución-NoComercial 3.0 España
dc.rights.accessRightsopen access
dc.rights.urihttps://creativecommons.org/licenses/by-nc/3.0/es/
dc.subject.cdu004(043.3)
dc.subject.keywordCompiler
dc.subject.keywordInterpreter
dc.subject.keywordCircom
dc.subject.keywordStatic analysis
dc.subject.keywordType analysis
dc.subject.keywordSymbolic execution
dc.subject.keywordArithmetic circuits
dc.subject.keywordConstraint generation
dc.subject.keywordCompilador
dc.subject.keywordIntérprete
dc.subject.keywordAnálisis estático
dc.subject.keywordAnálisis de tipos
dc.subject.keywordEjecución simbólica
dc.subject.keywordCircuitos aritméticos
dc.subject.keywordGeneración de restricciones
dc.subject.ucmInformática (Informática)
dc.subject.unesco1203.17 Informática
dc.titleDesign and implementation of the Circom 1.0 compiler
dc.title.alternativeDiseño e implementación del compilador de Circom 1.0
dc.typemaster thesis
dspace.entity.typePublication
relation.isAdvisorOfPublicationfdfffd91-34f6-4e0a-9fce-0c38ab083383
relation.isAdvisorOfPublication.latestForDiscoveryfdfffd91-34f6-4e0a-9fce-0c38ab083383
Files
Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Hermenegildo_Garcia_Navarro_Memoria.pdf
Size:
1.22 MB
Format:
Adobe Portable Document Format