Incorporación de la forma SSA a la máquina virtual de CIRCOM

Abstract

Este proyecto expande el compilador de CIRCOM mediante la introducción de una Representación Intermedia (IR) de la Máquina Virtual de CIRCOM (CVM), basada en un Grafo de Control del Flujo (CFG) construido directamente en forma de Asignación Única Estática (SSA). CIRCOM es un lenguaje de dominio específico para la construcción de circuitos aritméticos en sistemas de pruebas de conocimiento cero, donde la eficiencia y la corrección del compilador son aspectos críticos.

Para lograr este objetivo, se implementó para la CVM un parser, un Árbol de Sintaxis Abstracta (AST) y un verificador de tipos, todos ellos implementados en Rust. El nuevo flujo del compilador construye el CFG en forma SSA desde el inicio, evitando la necesidad de transformaciones posteriores. Sobre esta base, se implementó un algoritmo de análisis de vivacidad, lo que permite un análisis de programas más preciso y abre la puerta a optimizaciones avanzadas futuras.

La IR resultante mejora la capacidad de análisis y la eficiencia de los programas de la CVM, a la vez que proporciona una base sólida para futuras mejoras del compilador, como nuevas pasadas de optimización y técnicas de verificación formal.

This project enhances the CIRCOM compiler by introducing an Intermediate Representation of the CIRCOM Virtual Machine (CVM) based on a Control Flow Graph constructed in Static Single Assignment (SSA) form. CIRCOM is a domain-specific language for building arithmetic circuits in zero-knowledge proof systems, where compiler efficiency and correctness are critical.

To achieve this, the CVM was extended with a parser, Abstract Syntax Tree (AST) and typechecker, all implemented in Rust. The new pipeline constructs the CFG in SSA form from the start, avoiding the need for later transformations.

On top of this foundation, a liveness analysis algorithm was implemented, enabling more precise program analysis and opening the door to future advanced optimizations.

The resulting IR improves the ease of analysis and efficiency of CVM programs, while providing a solid basis for future compiler enhancements such as optimization passes and formal verification techniques.