Descripción General de Programación de Circuitos
Cómo Achronyme compila programas en circuitos de conocimiento cero.
Achronyme es un lenguaje de modo dual. El mismo código fuente puede ejecutarse como un programa de propósito general o compilarse en un circuito aritmético para pruebas de conocimiento cero.
¿Qué es un Circuito?
Un circuito ZK es un sistema de restricciones polinomiales sobre un campo finito. Dadas entradas públicas (conocidas por el verificador) y entradas testigo (conocidas solo por el probador), el circuito fuerza que ciertas relaciones se cumplan — sin revelar el testigo.
En Achronyme, escribes circuitos usando la misma sintaxis que los programas regulares, con algunas restricciones.
Dos Formas de Construir Circuitos
1. Archivo de circuito independiente
circuit hash_check(output: Public, secret: Witness) {
assert_eq(poseidon(secret, 0), output)
}Compila con el CLI:
ach circuit hash.ach --inputs "output=17159...,secret=42"2. Bloque prove en línea
let secret = 0p42
let hash = 0p17159...
let p = prove(hash: Public) {
assert_eq(poseidon(secret, 0), hash)
}El bloque prove captura variables del ámbito, compila el cuerpo como un circuito vía ProveIR en tiempo de compilación, y genera una prueba en tiempo de ejecución. Las variables declaradas como name: Public son entradas públicas; las demás variables del ámbito externo se infieren automáticamente como testigos privados.
Qué Funciona en Circuitos
| Característica | Comportamiento |
|---|---|
Aritmética (+, -, *, /, ^) | Se compila a operaciones de campo y restricciones |
Vinculaciones let | Alias (costo cero) |
if/else | Se compila a mux — ambas ramas se evalúan |
Bucles for (rango o array) | Desenrollado estático |
Llamadas fn | Se insertan en línea en cada punto de llamada |
| Anotaciones de tipo | Tipos opcionales Field/Bool en declaraciones y vinculaciones |
assert_eq(a, b) | Fuerza a == b (1 restricción) |
poseidon(a, b) | Hash Poseidon 2-a-1 (361 restricciones) |
range_check(x, bits) | El valor cabe en N bits |
Comparaciones (==, !=, <, <=, >, >=) | Gadgets seguros para campo |
Lógica booleana (&&, ||, !) | Con verificación booleana |
Qué No Funciona en Circuitos
| Característica | Razón |
|---|---|
Bucles while | Conteo de iteraciones desconocido — no se puede desenrollar |
break / continue | Requiere flujo de control dinámico |
print() | Efecto secundario, sin equivalente en circuito |
| Cadenas, mapas | No representables como elementos de campo |
| Recursión | Las funciones se insertan en línea, sin pila |
Estos se rechazan en tiempo de compilación con mensajes de error claros.
Pipeline de Compilación
Fuente → Parser → AST → Bajada a IR → SSA IR → Optimizar → Backend → Restricciones- Parsear — La gramática PEG produce un AST
- Bajar — El AST se convierte en instrucciones SSA planas (
Add,Mul,Mux,PoseidonHash, …) - Optimizar — Plegado de constantes, eliminación de código muerto, propagación booleana
- Compilar — El backend R1CS o Plonkish genera restricciones
- Testigo — Los valores concretos llenan el sistema de restricciones
- Exportar — Archivos binarios
.r1cs+.wtns(R1CS) o verificación en memoria (Plonkish)
Backends
Achronyme soporta dos backends de sistema de restricciones:
R1CS (predeterminado) — Sistema de Restricciones de Rango 1. Cada restricción es A * B = C donde A, B, C son combinaciones lineales de cables. Compatible con Groth16 vía snarkjs.
Plonkish — Sistema basado en puertas con puertas personalizadas, lookups y restricciones de copia. Usa compromisos polinomiales KZG. Algunas operaciones (como range_check) son más eficientes con lookups.
Selecciona el backend con --backend:
ach circuit file.ach --backend plonkish --inputs "x=42"