Design and implementation of the Circom 1.0 compiler
dc.contributor.advisor | Rubio Gimeno, Alberto | |
dc.contributor.author | GarcĂa Navarro, Hermenegildo | |
dc.date.accessioned | 2023-06-17T10:16:27Z | |
dc.date.available | 2023-06-17T10:16:27Z | |
dc.date.issued | 2020 | |
dc.description | Trabajo 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.abstract | 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. | |
dc.description.abstract | Circom, 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.department | Depto. de Sistemas Informáticos y Computación | |
dc.description.faculty | Fac. de Informática | |
dc.description.refereed | TRUE | |
dc.description.status | unpub | |
dc.eprint.id | https://eprints.ucm.es/id/eprint/62475 | |
dc.identifier.uri | https://hdl.handle.net/20.500.14352/9079 | |
dc.language.iso | eng | |
dc.master.title | Máster en Métodos Formales | |
dc.page.total | 38 | |
dc.rights | Atribución-NoComercial 3.0 España | |
dc.rights.accessRights | open access | |
dc.rights.uri | https://creativecommons.org/licenses/by-nc/3.0/es/ | |
dc.subject.cdu | 004(043.3) | |
dc.subject.keyword | Compiler | |
dc.subject.keyword | Interpreter | |
dc.subject.keyword | Circom | |
dc.subject.keyword | Static analysis | |
dc.subject.keyword | Type analysis | |
dc.subject.keyword | Symbolic execution | |
dc.subject.keyword | Arithmetic circuits | |
dc.subject.keyword | Constraint generation | |
dc.subject.keyword | Compilador | |
dc.subject.keyword | Intérprete | |
dc.subject.keyword | Análisis estático | |
dc.subject.keyword | Análisis de tipos | |
dc.subject.keyword | EjecuciĂłn simbĂłlica | |
dc.subject.keyword | Circuitos aritméticos | |
dc.subject.keyword | GeneraciĂłn de restricciones | |
dc.subject.ucm | Informática (Informática) | |
dc.subject.unesco | 1203.17 Informática | |
dc.title | Design and implementation of the Circom 1.0 compiler | |
dc.title.alternative | Diseño e implementación del compilador de Circom 1.0 | |
dc.type | master thesis | |
dspace.entity.type | Publication | |
relation.isAdvisorOfPublication | fdfffd91-34f6-4e0a-9fce-0c38ab083383 | |
relation.isAdvisorOfPublication.latestForDiscovery | fdfffd91-34f6-4e0a-9fce-0c38ab083383 |
Download
Original bundle
1 - 1 of 1
Loading...
- Name:
- Hermenegildo_Garcia_Navarro_Memoria.pdf
- Size:
- 1.22 MB
- Format:
- Adobe Portable Document Format