Visión General del Pipeline

El pipeline de compilación desde el código fuente hasta las pruebas.

Achronyme compila código fuente a través de cuatro caminos distintos: Modo VM para ejecución general, Modo circuito para generación de restricciones vía ach circuit, Modo prove para generación de pruebas en línea vía bloques prove {}, y Modo Circom para compilar archivos .circom a través del mismo pipeline de backend.

Diagrama del Pipeline

Etapa 1: Parseo

Punto de entrada: achronyme_parser::parse_program(source)

Parser de descenso recursivo escrito a mano con parseo de expresiones Pratt. Produce un AST con nodos Program, Stmt, Expr y Block. Maneja declaraciones public/witness, anotaciones de tipo, bloques prove {}, llamadas a métodos y acceso a namespaces estáticos (Type::MEMBER).

Precedencia de operadores (de mayor a menor):

1. ^ (potencia)
2. *, /, % (multiplicativos)
3. +, - (aditivos)
4. ==, !=, <, <=, >, >= (comparación)
5. && (AND lógico)
6. || (OR lógico)

Etapa 2a: Compilación a Bytecode (Modo VM)

Punto de entrada: compiler::FunctionCompiler::compile()

Para ach run, el AST se compila a bytecode para la VM basada en registros (37 opcodes). Un optimizador de bytecode de 3 pases se ejecuta después de la compilación:

• Peephole — fusiona secuencias de instrucciones comunes
• Plegado de constantes — evalúa aritmética sobre constantes conocidas
• Eliminación de stores muertos — elimina escrituras a registros que nunca se leen

Los bloques prove {} se manejan especialmente: el cuerpo se compila a ProveIR en tiempo de compilación (no en runtime), se serializa como bytes en el constant pool (TAG_BYTES), y se deserializa + instancia cuando la VM llega a la expresión prove.

Etapa 2b: Bajada a IR (Modo Circuito)

Punto de entrada: IrLowering::lower_circuit(source, pub_vars, wit_vars)

Para ach circuit, el AST se baja directamente a SSA IR. Comportamientos clave:

• Las vinculaciones let son alias — no se emite instrucción
• if/else se compila a Mux(cond, then_val, else_val) — ambas ramas se evalúan
• Los bucles for se desenrollan estáticamente (máximo 10,000 iteraciones)
• Las llamadas a funciones se insertan en línea; recursión detectada vía guardia de pila
• Los arrays soportan indexación en tiempo de compilación: a[i] donde i debe ser constante

Etapa 2c: Pipeline ProveIR (Modo Prove)

Punto de entrada: ProveIrCompiler::compile_prove_block()

Los bloques prove {} pasan por un pipeline de 8 fases:

Este diseño significa que los bloques prove se pre-compilan en tiempo de compilación — no hay re-parseo en runtime. El formato ProveIR lleva información de tipos, spans de código y referencias a funciones a través de la serialización.

Etapa 2d: Frontend Circom

Crate: circom — Punto de entrada: circom::parser::parse_circom(source)

Compila archivos .circom a través del mismo pipeline ProveIR → IR → Backend. El frontend Circom agrega seguridad estructural: <-- (asignación de signal sin constraint) sin un === correspondiente produce un error duro en tiempo de compilación (E100), capturando signals sub-restringidos que son la fuente #1 de vulnerabilidades ZK.

El ProveIR resultante alimenta el mismo pipeline de instanciación → optimización → backend que los bloques prove {} y ach circuit. Los templates Circom también pueden importarse y llamarse desde archivos .ach tanto en modo circuito como en modo VM — ve el capítulo Interoperabilidad con Circom para la sintaxis y semántica orientada al usuario.

Etapa 3: Optimización

Punto de entrada: ir::passes::optimize(&mut program)

Cinco pases se ejecutan secuencialmente sobre el IR:

Plegado de Constantes (const_fold)

Pase hacia adelante que evalúa operaciones sobre constantes conocidas. Pliega aritmética (Const(3) + Const(5) → Const(8)), simplifica identidades (x * 0 → 0, x - x → 0, x / x → 1) y lógica booleana.

Inferencia de Límites (bound_inference)

Reescribe comparaciones IsLt/IsLe sin límites a variantes acotadas cuando los operandos tienen anchos de bits probados desde RangeCheck. Comparaciones sin límites cuestan ~761 restricciones; acotadas cuestan ~(n+3) donde n es el ancho de bits.

Eliminación de Sub-expresiones Comunes (cse)

Pase O(n) que identifica computaciones puras duplicadas y remapea al primer resultado. Cubre aritmética, Poseidon, Mux, operaciones booleanas, comparaciones. Particularmente efectivo en bucles desenrollados.

Eliminación de Código Muerto (dce)

Pase de punto fijo iterativo que elimina instrucciones cuyos resultados nunca se usan. Instrucciones con efectos secundarios (AssertEq, Assert, Input, RangeCheck) nunca se eliminan.

Propagación Booleana (bool_prop)

Calcula el conjunto de variables SSA probadas como booleanas. Semillas desde comparaciones, RangeCheck(x, 1), operandos de Assert y anotaciones Bool. Se propaga a través de Not, And, Or, Mux. El backend R1CS lo usa para omitir enforcement booleano redundante.

Análisis de Taint (taint)

Advierte sobre entradas testigo sub-restringidas o no usadas. Rastrea el flujo de datos desde testigos hasta assertions — un testigo que no influencia ninguna restricción se marca con un warning.

Etapa 4: Compilación de Backend

Backend R1CS (predeterminado)

Punto de entrada: R1CSCompiler::compile_ir(program)

Mapea cada SsaVar a una LinearCombination. Add/Sub/Neg son gratis (aritmética de LC). Mul/Div/Mux/Poseidon emiten restricciones R1CS (A × B = C).

Disposición de cables: [ONE, pub₁..pubₙ, wit₁..witₘ, intermedios...]

Backend Plonkish

Punto de entrada: PlonkishCompiler::compile_ir(program)

Evaluación perezosa con PlonkVal — difiere add/sub/neg hasta que una multiplicación fuerza materialización. Puerta estándar: s_arith · (a·b + c − d) = 0. Verificaciones de rango usan tabla de lookup (1 fila vs n+1 restricciones en R1CS).

Etapa 5: Generación de Pruebas

Crate: proving

Generación de pruebas nativa en proceso — no requiere herramientas externas.

También genera contratos verificadores Solidity para verificación on-chain de pruebas Groth16.

Las exportaciones binarias .r1cs y .wtns siguen siendo compatibles con snarkjs para usuarios que prefieren herramientas externas.

Soporte Multi-Prime

El pipeline es genérico sobre el campo primo vía FieldElement<F: FieldBackend>. Tres backends implementados:

La selección de campo se resuelve una vez en el boundary de sesión; la monomorfización elimina todo overhead en runtime.

Archivos Fuente