Presentamos Achronyme — un lenguaje para pruebas zero-knowledge. Lee el anuncio arrow_right_alt

Changelog

Historial de versiones de Achronyme.

Todos los cambios relevantes de Achronyme se documentan aquí. Cada release actualiza los 10 crates del workspace a la misma versión.

0.1.0-beta.20 — No publicado

Frontend Circom: compila archivos .circom a través del pipeline de Achronyme con garantías de seguridad estructural que el compilador original no provee.

Nuevo: comando ach circom

Compilación end-to-end de archivos .circom: parse → análisis de restricciones → lowering a ProveIR → optimización → R1CS → prueba Groth16.

ach circom circuit.circom --inputs "a=3,b=7" --prove

Soporta --input-file input.toml, --prove, --r1cs, --wtns, --solidity y --prove-backend r1cs|plonkish.

Nuevo: parser Circom (sintaxis completa Circom 2.x)

Parser Pratt escrito a mano cubriendo todos los constructos de Circom: templates, funciones, señales (input/output/intermediate), declaraciones de componentes, <==, <--, -->, ==>, ===, for/while/if-else, componentes anónimos, operaciones parallel, tags, pragmas, includes.

Nuevo: WitnessHint — semántica correcta de <--

<-- en Circom es un hint de computación de testigo con cero restricciones. Nuestro CircuitNode::WitnessHint modela esto correctamente: la expresión del hint se evalúa off-circuit por el prover, y solo las restricciones === verifican el resultado. Esto previene el bug común en Circom donde los hints inflan accidentalmente el conteo de restricciones.

Un evaluador de testigos dedicado computa los valores de hints usando aritmética de enteros sobre la representación canónica de 4 limbs, soportando todas las operaciones bitwise (>>, <<, &, |, ^, ~) nativamente.

Nuevo: E100 — detección de señales sub-restringidas

Error duro cuando una señal asignada via <-- no tiene una restricción === correspondiente. Esto atrapa la fuente #1 de vulnerabilidades ZK en tiempo de compilación — <-- sin verificación.

Nuevo: W101 — warning de señales input/output sin restricciones

Warning cuando una señal input o output no participa en ninguna expresión de restricción. Un prover malicioso puede asignar valores arbitrarios a señales no verificadas. El compilador original de Circom no detecta esto.

warning: input signal `in` is not referenced in any constraint
  note: a input signal that doesn't participate in constraints cannot be verified
        — a malicious prover can set it to any value

Nuevo: operaciones bitwise via Decompose

Seis nuevas variantes de CircuitExpr (BitAnd, BitOr, BitXor, BitNot, ShiftR, ShiftL) expandidas durante la instanciación usando la infraestructura existente de Decompose. Cada operación descompone los operandos en bits, aplica la operación por bit usando aritmética de campo (AND = multiplicación, OR = a+b−ab, XOR = a+b−2ab), y recompone el resultado.

Nuevo: literales numéricos grandes

FieldConst::from_decimal_str y from_hex_str soportan constantes hasta 256 bits, cubriendo el rango completo del campo BN254. El lowering de Circom recurre a estos métodos cuando los literales exceden u64.

Nuevo: inlining de componentes y funciones

La instanciación de componentes (component c = Template(args)) inlinea el cuerpo del template con name mangling separado por . (libre de colisiones por construcción — . no puede aparecer en identificadores de Circom). Las llamadas a funciones se inlinean con sustitución de parámetros, limitadas a 64 niveles de profundidad.

Nuevo: clasificación de captures

Los parámetros de template se clasifican como StructureOnly (bounds de loops, tamaños de arrays), CircuitInput (expresiones de restricción), o Both, permitiendo que ProveIR optimice cómo se resuelven los captures durante la instanciación.

Nuevo: pruebas Groth16 E2E para 33 templates de circomlib

Pipeline completo verificado end-to-end para 33 circuitos reales de circomlib: Multiplier, compuertas lógicas (AND, OR, XOR, NOT, NAND, NOR), MultiAND, Num2Bits(8), Bits2Num(8), IsZero, IsEqual, Mux1, MultiMux1/2/4, Switcher, BinSum(4), LessThan(8), LessEqThan(8), GreaterThan(8), GreaterEqThan(8), ForceEqualIfEnabled, RangeProof(8), Min(8), AbsDiff(8), Decoder(4), DoubleMultiplier, MerkleProof(2), ParallelMul(3), FuncNbits, FuncSimple, Poseidon(2). Cada uno genera y verifica una prueba Groth16 sobre BN254.

Poseidon(2) compila la implementación real de circomlib a través de cadenas de includes (poseidon.circomposeidon_constants.circom → funciones helper) usando evaluación de arrays en tiempo de compilación para las 960+ constantes de ronda.

Nuevo: bounds dinámicos en loops de bloques prove {}

for i in 0..n y for i in 0..n+1 ahora funcionan en bloques prove cuando n se captura del scope externo. El parser acepta ForIterable::ExprRange, y el compilador ProveIR emite ForRange::WithCapture (captures simples) o ForRange::WithExpr (expresiones computadas). El loop se desenrolla en tiempo de instanciación cuando los valores de captura son conocidos.

let size = 8
prove my_proof(result: Public) {
    for i in 0..size {
        // size se auto-captura del scope externo
    }
    for i in 0..size + 1 {
        // bounds computados también funcionan
    }
}

Nuevo: argumentos de template computados en inlining de componentes

La instanciación de componentes con argumentos expresión como Num2Bits(n+1) dentro de templates (ej. LessThan) ahora funciona correctamente. La variante ForRange::WithExpr preserva la expresión del bound a través del inlining, y el instanciador la evalúa usando eval_const_expr cuando los valores de captura se resuelven.

Nuevo: evaluación de funciones en tiempo de compilación

Los cuerpos de function de Circom con lógica imperativa (var, while, for, if/else, return, ++, *=, llamadas anidadas) se evalúan completamente en tiempo de compilación. Funciones como nbits(a) que calculan tamaños de arrays o bounds de loops se resuelven a constantes durante el lowering — sin overhead en runtime.

Un pre-paso (precompute_vars) evalúa declaraciones var antes de la extracción del layout de señales, habilitando patrones como var nb = nbits(n); signal output out[nb]; donde el tamaño del array de salida depende del resultado de una función.

function nbits(a) {
    var n = 1;
    var r = 0;
    while (n - 1 < a) { r++; n *= 2; }
    return r;
}

template T(maxval) {
    var nb = nbits(maxval);      // evaluado en tiempo de compilación → 8
    signal output out[nb];       // dimensión del array resuelta desde resultado de función
}
component main = T(255);

Nuevo: arrays de componentes

component muls[n] declara un array de instancias de componentes. Los cuerpos de loops que contienen operaciones de arrays de componentes (muls[i] = Template(), muls[i].signal <== expr) se desenrollan automáticamente en tiempo de lowering usando known_constants, ya que el inlining de componentes requiere nombres concretos como muls_0, muls_1.

Nuevo: soporte para arrays multi-dimensionales

Arrays de señales N-dimensionales como signal c[n][2] se linealizan usando indexación basada en strides durante el lowering. c[i][j] compila a c[i*2+j], generalizando a dimensiones arbitrarias con strides computados de derecha a izquierda.

Nuevo: asignación indexada en bloques prove {}

Arrays mutables en bloques prove de .ach soportan asignación indexada: mut arr = [0, 0, 0]; arr[i] = expr emite CircuitNode::LetIndexed. Valida que el array existe y fue declarado con mut. Funciona tanto en bloques prove {} como en archivos .ach de circuitos.

Mejorado: resolución de captures en shifts e índices de arrays

Las operaciones de shift (x >> n, 1 << n) e indexación de arrays (arr[n]) ahora resuelven captures en tiempo de instanciación via eval_const_expr, con fallback al método previo extract_const. Esto habilita patrones donde un parámetro de template se usa tanto estructuralmente (bounds de loops) como en expresiones de restricción.

Mejorado: evaluación lazy de Mux en witness hints

El evaluador de testigos ahora cortocircuita expresiones ternarias (cond ? a : b), evaluando solo la rama tomada. Esto previene errores de división por cero en patrones como in != 0 ? 1/in : 0 (usado por IsZero) cuando la condición es falsa.

Nuevo: resolución de includes con flag -l

Compilación multi-archivo con directivas include:

ach circom circuit.circom -l ./node_modules/circomlib/circuits/

La API compile_file() resuelve directivas include buscando primero en el directorio del archivo, luego en los directorios de biblioteca -l. Los includes mutuos se deduplican por path canónico. Los includes circulares se detectan y reportan.

Nuevo: funciones que retornan arrays y variables de arrays en tiempo de compilación

Funciones como POSEIDON_C(t) que retornan arrays via cadenas if-else se evalúan completamente en tiempo de compilación. EvalValue soporta tres formas: Scalar(i64), Array(Vec<EvalValue>) y Expr(Box<Expr>) para constantes demasiado grandes para i64 (elementos de campo de 256 bits).

function POSEIDON_C(t) {
    if (t == 2) { return [0x09c46e..., 0x0c19da..., ...]; }
    // ... 960+ constantes por configuración
}

template Poseidon(nInputs) {
    var t = nInputs + 1;
    var C[t] = POSEIDON_C(t);   // evaluado en tiempo de compilación
    var M[t][t] = POSEIDON_M(t); // arrays 2-D con linearización por strides
    // C[i+r] se resuelve desde known_array_values durante lowering
}

Los arrays 2-D se aplanan con indexación basada en strides: M[i][j] compila a M[i*cols+j]. Un paso unificado precompute_all procesa tanto variables escalares como de arrays en orden de declaración, permitiendo que vars posteriores referencien anteriores (ej. var nRoundsP = N_ROUNDS_P[t - 2]).

Nuevo: diagnósticos estructurados — reporte de errores estilo rustc

Los errores de Circom ahora se renderizan con snippets de código fuente, spans subrayados, códigos de error y colores ANSI — idénticos a la salida diagnóstica nativa de .ach:

error[E200]: undefined variable `amout` in circuit context
  --> circuit.circom:6:16
  |
6 |     result <== amout * 2;
  |                ^^^^^
  |
  = help: a similar name exists in scope: `amount`

Todos los tipos de error producen objetos Diagnostic estructurados:

  • E100–E102, W101–W103: Análisis de restricciones (existentes)
  • E200: Variable/señal indefinida (con “did you mean?” via distancia Levenshtein)
  • E201: Función indefinida (con sugerencia)
  • E202: Template indefinido (con sugerencia)
  • E203–E204: Errores de include (I/O, no encontrado, circular)
  • E205: Features no soportados (tipos bus, custom templates)
  • E206: Mismatch de aridad
  • E208: Violaciones de restricciones de loops
  • E209: Fallos de evaluación en tiempo de compilación
  • E210–E211: Componente main faltante o indefinido

Tres formatos de salida via --error-format: human (default, estilo rustc), json (JSON Lines para tooling), short (file:line:col: severity: message).

Mejorado: arquitectura del lowering

El pipeline de lowering se refactorizó de 3 archivos monolíticos (4,959 LOC combinados) a 21 módulos enfocados, sin ningún archivo excediendo 400 líneas de código de producción. El protocolo de la máquina de estados de component wiring está formalmente documentado. Todas las llamadas unwrap()/panic!() de producción llevan justificación // SAFETY: o fueron reemplazadas con propagación de errores.

Nuevo: evaluador BigVal de 256 bits

La evaluación de variables en compile-time migró de i64 a BigVal([u64; 4]) — un tipo de 256 bits en complemento a dos con aritmética completa (add, sub, mul, div, mod, shifts, operaciones bitwise, comparaciones). Los mapas de parámetros se actualizaron de u64 a FieldConst. Esto desbloquea circuitos como CompConstant cuyas variables computan (1 << 128) - 1, que desbordaba con i64.

Nuevo: desenrollado de loops mixtos señal+var

Los loops cuyo cuerpo tanto escribe señales como muta variables (ej., el for de CompConstant que actualiza b, a, e cada iteración mientras restringe señales) ahora se detectan y desenrollan completamente. Esto asegura que los valores de las variables son constantes concretas cuando se usan como coeficientes en expresiones de señales — requerido para R1CS válido.

Nuevo: soporte de array literals 2D en el lowering

Los array literals anidados como var BASE[10][2] = [[...], ...] (los 10 puntos base BabyJubjub de Pedersen, cada uno un par (x, y) de 254 bits) ahora se manejan correctamente. El paso de precompute los evalúa en compile-time; el lowering omite el re-procesamiento y resuelve valores desde known_array_values durante el inlining de componentes.

Fix: auto-materialización R1CS — previene OOM en circuitos grandes

El Poseidon compilado desde Circom tiene 57 rondas parciales donde los elementos de estado solo reciben operaciones lineales (MDS con coeficientes constantes). Sin materialización, los términos de LinearCombination crecen exponencialmente — f(n) ≈ 2^n — causando >12 GB de uso de memoria y OOM kills.

Tres fixes:

  1. Auto-materializar resultados de Add/Sub que excedan 8 términos en el compilador R1CS
  2. Materializar LCs fuente antes de loops de descomposición de bits (evita clonar LCs grandes 252+ veces en WitnessOps)
  3. Mismo tratamiento para instrucciones Decompose

Esto replica la optimización ya presente en el circuito nativo de Poseidon (constraints/src/poseidon/circuit.rs) pero aplicada genéricamente a todas las restricciones generadas desde IR.

Expandido: cobertura E2E R1CS de circomlib — 21 circuitos verificados

La verificación completa del sistema de restricciones (compilar → instanciar → R1CS → testigo → verificar) ahora cubre 21 circuitos reales de circomlib. Conteos post-optimizador (O1); referencia circom es --O1 salvo indicación.

CircuitoNuestro O1circomPatrón
Num2Bits(8)917Descomposición de bits
IsZero44Gadget inverso
LessThan(8)1020Composición de componentes
Poseidon(2)240243Permutación + MDS
MiMCSponge(2,220,1)1,3171,320Feistel, 220 rondas
BabyJubjub (Add+Dbl+Check)3048Curva Edwards
EscalarMulFix(253)1157 (O2: 11)Scalar mul base fija
EscalarMulAny(254)2,3102,310Scalar mul base variable
EdDSAPoseidon3,9658,086Verificación de firma completa
Pedersen(8)1389 (O2: 13)Hash EC, Window4 + Montgomery
Mux3 / Mux416 / 37Selector 8-way / 16-way
SwitcherSwap condicional

EdDSAPoseidon (verificación completa de firma EdDSA sobre BabyJubjub con hash Poseidon) se verifica end-to-end con 3,965 restricciones post-optimizador — 2.04× menos que el output --O1 de circom con 8,086. Pedersen y EscalarMulFix igualan el output --O2 de circom sin un pase O2 equivalente.

Nuevo: optimizador de restricciones R1CS (O1 + O2)

Optimizador en dos niveles que reduce el conteo de restricciones después de la compilación:

O1 — Eliminación lineal (un solo pase):

  1. Heurística de frecuencia: selecciona el wire más referenciado para sustitución, maximizando simplificaciones en cascada
  2. Eliminación lineal: sustituye wires definidos por k * LC = LC, eliminando la restricción por completo
  3. Deduplicación: remueve restricciones idénticas producidas por sustitución de variables
  4. Eliminación tautológica: descarta restricciones de producto-cero (0 = 0) que surgen después de la sustitución

O2 — Deducción algebraica (pase opcional con rollback): 5. DEDUCE: eliminación gaussiana sobre la matriz de monomios cuadráticos. Encuentra combinaciones lineales de restricciones cuadráticas que producen ecuaciones puramente lineales, introduciendo nuevas ecuaciones de wire sin agregar restricciones. Se aplica iterativamente hasta convergencia. 6. Propagación de constantes: sustituye wires probados iguales a constantes de campo, colapsando sub-expresiones enteras. Las constantes cableadas desde inlining de componentes se propagan a través de aritmética Montgomery/Edwards — toda la cadena se reduce a cero restricciones por operación de punto base. 7. Rollback: si DEDUCE + propagación constante no reduce el conteo, el pase O2 se descarta y se usa el output de O1.

Resultados en circuitos representativos (pre-opt → O1 → O2):

Circuitopre-optO1O2circom O1
Num2Bits(8)25917
Pedersen(8)30131389
EscalarMulFix(253)27111157
EscalarMulAny(254)5,3252,3102,310
Poseidon(2)491240243
MiMCSponge(2,220,1)2,5811,3171,320
EdDSAPoseidon9,7193,9658,086

Nuevo: propagación Bool e inferencia de patrones de bits

Dos nuevos pases de optimización IR:

  • Propagación Bool: detecta restricciones v * (v - 1) = 0 (verificaciones booleanas) y propaga el estado de bit probado. Permite que Decompose(v, N) omita restricciones booleanas redundantes en bits ya probados.
  • Inferencia de patrones de bits: reconoce patrones estilo Num2Bits (descomposición de bits + recombinación lineal) y marca los bits descompuestos como booleanos probados — evita doble restricción en circuitos que componen Num2Bits internamente.

Fix: signal output mapeado a wires públicos R1CS

Anteriormente, las declaraciones signal output se descartaban durante el ensamblaje del ProveIR — las señales de salida no tenían wires públicos en R1CS. DCE luego eliminaba todas las restricciones en circuitos cuyo único comportamiento observable era a través de outputs (Multiplier, AND, OR, NOT, Switcher, Bits2Num, etc. → 0 restricciones).

El fix agrega outputs a ProveIR.public_inputs e introduce instantiate_with_outputs() que asigna wires públicos para cada señal de salida. Los nodos del cuerpo (WitnessHint, Let) que asignan a señales de salida reutilizan el wire público en vez de crear wires de testigo duplicados, asegurando exactamente un wire por señal con semántica R1CS correcta.

Mejorado: constant folding en instanciación

  • ShiftL/ShiftR con operandos constantes se pliegan en tiempo de instanciación (reducción de 47× instrucciones en EscalarMulAny)
  • Decompose(Const(k), N) se expande directamente a N constantes de bits
  • Instrucciones tautológicas AssertEq(x, x) eliminadas durante DCE

Fix: emisión duplicada de restricciones en lowering de <==

<== emitía incorrectamente tanto un nodo Let como un AssertEq, con la expresión RHS clonada en ambos. Cada multiplicación en el RHS producía dos restricciones R1CS — una real, una duplicada. Los circuitos con muchos <== (esencialmente todo circomlib) producían aproximadamente 2× el conteo correcto de restricciones.

El fix: <== ahora emite solo Let. El backend R1CS deriva la restricción de las instrucciones Mul de la expresión del Let.

Mejorado: propagación de constantes a través de inlining de componentes

Cuando una entrada de componente se cablea a una constante en tiempo de compilación (S.in <== BASE_POINT_X), esa constante se inyecta en known_constants del sub-template antes de compilar su cuerpo. Las expresiones que dependen solo de constantes se pliegan usando aritmética modular BN254 exacta (try_fold_const).

Impacto en Pedersen(8): los 8 selectores Window4 con cableado de punto base → 2 operaciones Montgomery + 1 conversión M2E, todo plegado a constantes. Conteo de restricciones: 88 → 13 (equivalente al output --O2 de circom).

Perf: caché de cuerpos de template — 1.7× speedup en EscalarMulAny

Los sub-templates instanciados múltiples veces con los mismos parámetros ahora se compilan una sola vez y se cachean. Las instanciaciones subsecuentes reutilizan el cuerpo sin mangling, aplicando solo un pase rápido de renombrado.

EscalarMulAny(254) instancia SegmentMulAny(1) 254 veces. Con el caché, las 254 re-instanciaciones cuestan ~10 µs cada una. Tiempo de lowering end-to-end de EscalarMulAny: 1,500 ms → 880 ms (1.7×).

Fix: solidez de MiMCSponge — contaminación de la variable de loop

En loops has_mixed_signal_var (cuyo cuerpo tanto restringe señales como muta vars — ej. el loop de rondas de MiMCFeistel), las declaraciones var-only se evalúan en compile-time via try_eval_stmt_in_place. Si la evaluación tiene éxito, todos los eval_vars se escriben de vuelta a ctx.param_values.

El bug: la propia variable de loop (i) se incluía en este write-back. Para la iteración i = 0, ctx.param_values["i"] = 0 se escribía. Para i = 1, la rama else c = c_partial[i-1] fallaba en evaluación compile-time (porque c_partial es un array, no un escalar en eval_vars), por lo que el write-back no ejecutaba — y ctx.param_values["i"] permanecía en 0 de la iteración anterior.

all_constants() combina param_values y env.known_constants con or_insert (param_values gana). El env.known_constants["i"] = 1 correctamente configurado siempre era eclipsado por el param_values["i"] = 0 obsoleto. Cada ternario (i == 0) ? ... : ... evaluaba la rama i = 0 para las 220 iteraciones, colapsando todo el hash MiMC a una sola computación.

El fix: excluir la variable de loop del write-back a param_values. La variable de loop es gestionada exclusivamente por env.known_constants al inicio de cada iteración.

Impacto: MiMCSponge(2, 220, 1) — 19 restricciones (inseguro) → 2,581 pre-opt → 1,317 post-O1 — igualando las 1,320 de circom.

Breaking: operador de ruta :: para imports de módulos y namespaces de circom

El acceso calificado por módulo ahora usa el operador de ruta :: en lugar de notación de punto:

import "./math.ach" as math
import "./circomlib/poseidon.circom" as P

print(math::add(1, 2))          // antes: math.add(1, 2)
let h = P::Poseidon(2)([a, b])  // antes: P.Poseidon(2)([a, b])

El lookup se resuelve completamente en tiempo de compilación — el compilador reescribe alias::nombre al global mangled alias::nombre, reutilizando la misma ruta de dispatch que ya maneja los statics nativos como Int::MAX, Field::ZERO y BigInt::from_bits. No hay objeto alias en runtime, no hay lookup de HashMap por llamada, y la misma sintaxis funciona dentro de código VM, declaraciones circuit y bloques prove {} — cerrando el gap donde el dispatch basado en punto se rompía dentro de bloques prove.

Las formas antiguas alias.nombre / alias.func(...) producen un error de migración que apunta al spelling correcto con una sugerencia “did you mean”. Aplica tanto a alias de módulos .ach como a alias de librerías .circom.

Ve Módulos y Importando Templates de Circom para la referencia completa de sintaxis.


0.1.0-beta.19 — 2026-04-02

Arquitectura multi-prime: genéricos en tiempo de compilación sobre cualquier campo primo.

Nuevo: trait FieldBackend y FieldElement<F> genérico

La capa de campos ahora es genérica sobre el primo. FieldElement<F: FieldBackend = Bn254Fr> envuelve un tipo asociado Repr (ej. [u64; 4] para curvas de 254/255 bits, u64 para Goldilocks). Un solo match en el boundary de sesión selecciona el backend; la monomorfización lo propaga al resto — sin overhead en runtime.

Nuevo: enum PrimeId

Identifica qué campo primo está en uso en boundaries de serialización y flags CLI. Soporta 8 curvas: BN254, BLS12-381, Goldilocks, Grumpkin, Pallas, Vesta, secp256r1, BLS12-377.

Nuevo: backend BLS12-381

Bls12_381Fr — mismo algoritmo CIOS Montgomery que BN254, constantes distintas. Módulo de 255 bits, Repr = [u64; 4]. 28 tests unitarios incluyendo verificación de constantes con BigUint.

Nuevo: backend Goldilocks

GoldilocksFr — el primer backend sin Montgomery con Repr = u64. Usa la identidad de Goldilocks 2⁶⁴ ≡ 2³² − 1 (mod p) para reducción rápida sin ramas ni divisiones. 36 tests unitarios incluyendo verificación del pequeño teorema de Fermat.

Nuevo: Poseidon multi-campo

PoseidonParams<F> es ahora genérico sobre el backend con exponente S-box configurable (alpha). Constructores para BN254 (circomlibjs, α=5), BLS12-381 (LFSR, α=5) y Goldilocks (LFSR, α=7). El LFSR Grain genera constantes conformes al paper para cualquier campo. Las funciones nativas de hash (poseidon_hash, poseidon_permutation) son completamente genéricas. El sbox_circuit R1CS soporta tanto α=5 (3 restricciones) como α=7 (4 restricciones).


0.1.0-beta.18 — 2026-03-30

Infraestructura de paridad con Circom, descomposición de bits, división entera, parámetros/retornos de arrays en funciones de circuito, inspector, crate proving, WASM LSP.

Nuevo: comando ach inspect

Visualización interactiva DAG para circuitos y bloques prove. Compila el fuente, construye un grafo de restricciones con mapeo de spans de código, y sirve un frontend HTML embebido en un servidor HTTP local.

ach inspect examples/inspect_membership.ach --input-file examples/inspect_membership.toml

Características:

  • DAG de restricciones — grafo acíclico dirigido de instrucciones IR con aristas de flujo de variables.
  • Spans de código — cada nodo enlaza a la línea original del .ach.
  • Evaluación de testigos — evaluador tolerante que computa valores concretos para tooltips del inspector, incluso con inputs incompletos.
  • Rastreo de origen de restricciones — el backend R1CS anota cada restricción con la instrucción IR que la generó.

Construido sobre un nuevo módulo ir::inspector (~730 líneas) que genera el JSON del grafo a partir de metadatos de IrProgram (var_spans, orígenes de restricciones).

Refactor: crate proving

Los módulos de Groth16, Halo2/PlonK y generador de verificadores Solidity se han extraído de cli a un crate independiente proving. Esto permite que ach-server (y futuros consumidores) dependan de la lógica de pruebas sin incluir todo el CLI. El workspace ahora tiene 10 crates.

Nuevo: métodos Bool

let flag = true
print(flag.to_string())   // "true"
print(flag.to_int())      // 1

Nuevo: List.to_string() y mejora en formateo de valores

let xs = [1, 2, 3]
print(xs.to_string())   // "[1, 2, 3]"

Colecciones anidadas y listas de tipos mixtos se formatean recursivamente con delimitadores apropiados.

Nuevo: funciones LSP en WASM

El crate achronyme-wasm ahora expone funciones LSP (diagnósticos, hover, completions) vía ach-lsp-core, habilitando inteligencia de lenguaje en el playground del navegador sin round-trip al servidor.

Fix: plantillas de ach init

Las plantillas main.ach, circuit.ach y prove.ach generadas por ach init se han actualizado a la sintaxis actual con ejemplos funcionales que compilan y ejecutan directamente.

Propagación de spans en ProveIR

CircuitNode::Expr ahora lleva spans de código a través de la instanciación, permitiendo al inspector (y futuros mensajes de error) apuntar a la ubicación original en el código fuente para cada restricción.

Fix: parámetros y retornos de arrays en funciones de circuitos

Las funciones dentro de bloques circuit y prove ahora aceptan parámetros de tipo array y pueden retornar arrays. Anteriormente, la anotación de tipo array en parámetros de funciones era ignorada silenciosamente, causando un error “expected scalar, got array” al pasar arrays. Esto habilita un patrón de composición tipo componente donde funciones reutilizables que generan restricciones pueden componerse:

fn verify_path(leaf, siblings: Field[2], dirs: Field[2]) -> Field {
    let l1 = poseidon(mux(dirs[0] == 0, leaf, siblings[0]),
                       mux(dirs[0] == 0, siblings[0], leaf))
    let l2 = poseidon(mux(dirs[1] == 0, l1, siblings[1]),
                       mux(dirs[1] == 0, siblings[1], l1))
    l2
}

circuit main(root: Public, secret: Witness) {
    let path: Field[2] = [sibling0, sibling1]
    let dirs: Field[2] = [0, 0]
    assert_eq(verify_path(poseidon(secret, 0), path, dirs), root)
}

Esta es infraestructura fundacional para un futuro frontend de Circom: los templates de Circom mapean a funciones, la instanciación de componentes mapea a llamadas de función, y el cableado de señales mapea a parámetros/retornos de arrays.

Nuevo: decompose() — descomposición de bits accesibles

Nuevo builtin que descompone un field element en variables de bit individuales:

circuit main(x: Witness) {
    let bits = decompose(x, 8)    // 8 variables de bit con constraint booleano
    assert_eq(bits[1], 1)          // acceder bits individuales
    assert_eq(bits[0] + bits[1] * 2 + bits[2] * 4, x)  // usar en constraints
}

A diferencia de range_check, que verifica que un valor cabe en N bits pero no los expone, decompose retorna los bits como un array. Es el equivalente de Achronyme al template Num2Bits de Circom — la base para operaciones bitwise, aritmética binaria, y la mayoría de circomlib.

Costo: N+1 constraints (N checks booleanos + 1 igualdad de suma).

Nuevo: int_div() e int_mod() — aritmética entera en circuitos

Cociente y resto entero sobre field elements:

circuit main(a: Witness, b: Witness) {
    let q = int_div(a, b, 32)     // floor(a / b), range check de 32 bits
    let r = int_mod(a, b, 32)     // a - b * floor(a / b)
    assert_eq(b * q + r, a)       // siempre se cumple
}

El tercer argumento max_bits especifica el bound del range check para soundness — evita que un prover malicioso explote el wraparound del campo. El usuario elige el bound según el rango de sus valores (8 bits para bytes, 32 para contadores, 64 para valores grandes, 252 para campo completo).

Son los equivalentes de Achronyme a los operadores \ y % de Circom.

Migración de docs

El directorio docs/ y su workflow de deploy se han eliminado del repositorio principal. La documentación ahora vive en achronyme-web.


0.1.0-beta.17 — 2026-03-28

8.6x de speedup en VM, optimizador de bytecode, observabilidad ProveIR, crate WASM, unificación OuterScope, 42% reducción de restricciones.

Rendimiento: 1315ms → 303ms (8.6x con PGO)

Seis optimizaciones en el hot-path de la VM y un optimizador de bytecode de tres pasadas llevan el benchmark de 10M iteraciones de 1315ms a 303ms:

OptimizaciónSpeedupTécnica
Acceso a registros sin verificación-25%get(idx)get_unchecked(idx) en hot loop
Payloads de error en BoxfixResult<Value> de 48 → 16 bytes
Caché de dispatch-40%Cache closure→function lookup, saltar chequeo de Arena free
GC por lotes-7%Verificar cada 1024 instrucciones, no en cada una
Sentinel de budget-7%Option<u64>u64 con sentinel u64::MAX
Chequeo de int fusionado-6%as_int_unchecked() elimina doble verificación de tag
Optimizador de bytecode-8%Tres pasadas del compilador (ver abajo)
PGO-34%Profile-guided optimization vía scripts/build-pgo.sh

Tres optimizaciones intentadas fueron revertidas tras medir que no daban mejora con PGO (reorden de branches, eliminación de Result, opcodes enteros especializados), confirmando que con PGO el predictor de branches ya maneja los branches del hot-path de forma óptima — las ganancias futuras deben reducir trabajo, no branches.

Optimizador de bytecode (compiler/src/optimizer.rs)

Tres pasadas peephole ejecutadas sobre el bytecode de cada función tras la compilación:

  1. Eliminación de cargas redundantesSetGlobal Ra, idx; GetGlobal Rb, idxMove Rb, Ra. Los targets de salto actúan como barreras.
  2. Elevación de constantes (LICM)LoadConst invariantes al loop movidos antes del loop. Se re-ejecuta tras la promoción de registros para capturar nuevas constantes elevables.
  3. Promoción de registros — Globals en loops internos sin llamadas promovidos a registros locales. GET_GLOBAL/SET_GLOBAL se convierten en Move, con carga única antes del loop y escritura al salir.

26 tests unitarios. El optimizador maneja correctamente continue (back-edges colapsados), loops anidados (solo el más interno) y globals de solo lectura (sin write-back para let).

ProveIR Display

ach disassemble examples/proof_of_membership.ach
  -- ProveIR block 1 (instruction 0134) --
  Captures:
    key_5                (witness)
    proof_path_0..2      (witness)
    proof_indices_0..2   (witness)
  Public inputs:
    merkle_root: Field
  Body:
    let my_commitment = poseidon($key_5, 0)
    merkle_verify(merkle_root, my_commitment, proof_path, proof_indices)

Representación legible de plantillas de circuito pre-compiladas. Variables capturadas con prefijo $ para distinguirlas de nombres locales al circuito. Muestra capturas con roles de uso (witness/structure/ambos), inputs tipados y cuerpo completo del circuito con indentación.

Reescritura del desensamblador

El comando ach disassemble ahora trabaja desde artefactos compilados en vez de re-parsear el fuente:

  • Bloques prove — Deserializados del constant pool del bytecode vía ProveIR::from_bytes(). Antes fallaba con “expected expression, found ..”.
  • Declaraciones circuitcircuit name(params) { body } extraídas del AST con slicing basado en spans. Antes fallaba con “circuit declarations not supported inside circuits”.

Nuevo: crate achronyme-wasm

7 de 9 crates core compilan a wasm32-unknown-unknown (parser, compiler, vm, ir, memory, constraints, std). El crate wasm/ provee una API lista para el navegador para el playground planificado (0.3.0).

Nuevas anotaciones de tipo: Int y String

let count: Int = 42
let name: String = "hello"

Anotaciones de tipo en modo VM para documentación y futuro type checking. Se suman a las existentes Field, Bool, Public, Witness.

Unificación de OuterScope

Las funciones definidas antes de bloques prove {} y circuit {} inline ahora son accesibles dentro de ellos — el mismo comportamiento que los archivos ach circuit ya tenían, ahora unificado en todos los caminos de compilación.

fn double(x) { x * 2 }

prove(expected: Public) {
    assert_eq(double(val), expected)   // ✓ funciona ahora
}

El nuevo struct OuterScope reemplaza el hack ad-hoc de prepend de preámbulo en compile_circuit(). Los ASTs de FnDecl se registran en la fn_table del compilador ProveIR antes de compilar el bloque, por lo que las funciones externas se inlinean de forma idéntica a las definidas localmente.

Optimización ZK: 2,539 → 1,461 restricciones (-42.4%)

Tres optimizaciones reducen el conteo de restricciones del proof of membership (Merkle depth-3):

OptimizaciónAntesDespuésΔ
Swap condicional en merkle_verify2,5391,464-42.3%
Dedup de enforcement booleano1,4641,461-0.2%
Total2,5391,461-42.4%

Swap condicional — El builtin merkle_verify ahora usa 2 Mux + 1 Poseidon por nivel Merkle (365 restricciones) en vez de 2 Poseidon + 1 Mux (724 restricciones). Esto coincide con el patrón estándar de Tornado Cash y Semaphore.

Dedup de enforcement booleano — El backend R1CS ahora rastrea qué variables ya tienen v * (1-v) = 0 enforzado. Cuando la misma condición se usa en múltiples instrucciones Mux/And/Or, el chequeo se emite solo una primera vez.

Nueva pasada: CSE (Common Sub-expression Elimination)

Nueva pasada de optimización IR que identifica computaciones puras duplicadas y remapea sus resultados a la primera ocurrencia. Cubre todas las instrucciones puras: aritmética, Poseidon, Mux, operaciones booleanas, comparaciones. Las instrucciones con efectos secundarios (AssertEq, Assert, RangeCheck) nunca se deduplican. Maneja sustituciones encadenadas.

El pipeline de optimización ahora es: constant folding → bound inference → CSE → dead code elimination.

Nuevo ejemplo: proof of membership

examples/proof_of_membership.ach — Árbol Merkle depth-3 con 8 miembros. Dos miembros prueban membresía vía commitments Poseidon y merkle_verify sin revelar identidad. 1,461 restricciones por prueba (Groth16, ~855 bytes).

Fix: BigInt.to_string() y BigInt.to_hex()

Los valores BigInt ahora soportan conversión a string:

let b = bigint256(42)
print(b.to_string())   // "42"
print(b.to_hex())      // "0x2a"

Suite de tests: 2,705 tests

2,543 tests unitarios/integración (cargo test —workspace) + 162 tests E2E (run_tests.sh). Subió desde 2,125 en beta.16.

Script PGO

./scripts/build-pgo.sh

Construye un binario optimizado usando profile-guided optimization. Recolecta perfiles del benchmark de hot-loop y la suite de tests de la VM, luego reconstruye con LLVM PGO. Integrado en CI (release.yml) para targets nativos.


0.1.0-beta.16 — 2026-03-25

Hardening, imports en circuitos, mensajes en assert, inputs TOML.

Hardening

  • Panics → Result: Arena::alloc() retorna Result, unreachable!() reemplazado con Err(InvalidOpcode), ~35 conversiones defensivas de unwrap.
  • Errores genéricos eliminados: RuntimeError::Unknown y SystemError reemplazados con variantes específicas (StaleHeapHandle, StaleUpvalue, IoError, etc.).
  • Robustez del lexer: from_utf8().unwrap() reemplazado con propagación de errores.
  • Formato flat de circuito eliminado: Declaraciones public/witness a nivel top son error de compilación. Usar circuit name(param: Type, ...) { body }.
  • Validación de keyword arguments: Errores tipográficos en llamadas a circuitos producen sugerencias “did you mean?”.

assert_eq / assert con mensajes personalizados

assert_eq(computed, expected, "commitment mismatch")
assert(is_valid, "eligibility check failed")

Tercer argumento opcional (literal string) mostrado cuando la evaluación del testigo falla. Usa nombres de variables + valores cuando no se proporciona mensaje.

Imports de circuitos en ProveIR

import "./hash_lib.ach" as h

circuit main(out: Public, a: Witness, b: Witness) {
    assert_eq(h.my_hash(a, b), out)
}

Los circuitos ahora pueden importar funciones de otros módulos. Las funciones importadas se inlinean durante la compilación ProveIR. Soporta import ... as alias e imports selectivos. Detección de imports circulares incluida.

--input-file para inputs TOML de circuitos

ach circuit merkle.ach --input-file inputs.toml
root = "7853200120375982..."
leaf = "1"
path = ["2", "3"]
indices = ["0", "1"]

Reemplaza la convención --inputs "path_0=2,path_1=3" con arrays TOML nativos. Soporta valores string, enteros, hex ("0xFF") y valores negativos. Mutuamente exclusivo con --inputs.

Interno

  • ModuleLoader movido de compiler a crate ir (compartido entre compilador de bytecode y ProveIR).
  • Versión del formato ProveIR bumpeada a v3 (campo de mensaje de assert en CircuitNode::AssertEq/Assert).
  • Factibilidad WASM verificada: 7/9 crates core compilan a wasm32-unknown-unknown.

0.1.0-beta.15 — 2026-03-23

Unificación de sintaxis, metadatos de tipo global, ejemplo Tornado Cash.

Breaking: Sintaxis unificada

Seis patrones de sintaxis inconsistentes consolidados en un diseño coherente:

// Definiciones de circuito — parámetros con tipos de visibilidad
circuit eligibility(root: Public, secret: Witness, path: Witness Field[3]) {
    merkle_verify(root, poseidon(secret, 0), path, indices)
}

// Bloques prove — solo parámetros públicos, witnesses auto-capturados
prove withdrawal(root: Public, nullifier_hash: Public) {
    merkle_verify(root, commitment, path, indices)
}

// Keyword arguments para todos los callables
eligibility(root: root_val, secret: my_secret, path: my_path)
  • TypeAnnotation refactorizado de enum a struct con campos visibility, base, array_size.
  • Public/Witness son keywords de tipo contextuales: root: Public, path: Witness Field[3].
  • Call/CircuitCall unificados — nodo único Call con Vec<CallArg> soporta keyword args para todos los callables.
  • CircuitParam, CircuitVisibility eliminados del AST.
  • Sintaxis anterior eliminadaprove(public: [...]), circuit(public x, witness y) ya no parsean.

Keyword circuit — definiciones de circuito reutilizables

circuit eligibility(root: Public, secret: Witness, path: Witness Field[3], indices: Witness Field[3]) {
    let commitment = poseidon(secret, 0)
    merkle_verify(root, commitment, path, indices)
}
  • ach circuit file.ach requiere el formato de declaración circuit name(...).
  • import circuit "./path.ach" as name importa archivos de circuito independientes.
  • Llamadas a circuitos con keyword arguments: eligibility(root: val, secret: s).

Bloques prove con nombre

prove vote(hash: Public) {
    assert_eq(poseidon(secret, 0), hash)
}
  • prove name(...) a nivel statement se desugarea a let name = prove name(...)
  • Las pruebas son valores de primera clase (TAG_PROOF)

--circuit-stats — profiler de restricciones

ach circuit merkle.ach --circuit-stats
ach run program.ach --circuit-stats
  • 7 categorías: Aritmética, Aserciones, Range checks, Hashes, Comparaciones, Ops booleanas, Selecciones
  • ach run --circuit-stats recolecta stats de todos los bloques prove en runtime
  • El modelo de costo estático coincide exactamente con los conteos reales de restricciones R1CS

Metadatos de tipo global (GlobalEntry)

Las variables globales ahora llevan anotaciones de tipo a través del pipeline del compilador:

let path: Field[2] = [voter1, n1]   // type_ann preservado en GlobalEntry
prove(root: Public) {
    merkle_verify(root, leaf, path, idx)  // path capturado correctamente como array
}
  • global_symbols actualizado de HashMap<String, u16> a HashMap<String, GlobalEntry> con campos index, type_ann, is_mutable.
  • compile_prove lee GlobalEntry.type_ann para construir OuterScopeEntry enriquecido para globals.
  • find_array_size busca en locals, upvalues Y globals.
  • Los imports selectivos propagan type_ann del módulo fuente.

Captura de arrays en bloques prove

Variables array del scope VM se capturan automáticamente por bloques prove:

let path = [voter1, n1]           // inferido como Field[2]
prove(merkle_root: Public) {
    merkle_verify(merkle_root, commitment, path, indices)
}
  • Inferencia de tipo arraylet x = [a, b, c] infiere Field[3] en bindings inmutables.
  • Rastreo de capturas extract_array_ident — merkle_verify y constructos que consumen arrays ahora marcan correctamente las capturas de elementos array para instanciación.
  • El handler prove de la VM auto-expande capturas TAG_LIST en entradas escalares.

Warnings de anotación de tipo

let x: Bool = 0p42          // W006: type mismatch
let a: Field[3] = [1, 2]    // W007: array size mismatch

Ejemplos

  • tornado_mixer.ach — Mixer privado estilo Tornado Cash completo: árbol de 4 depósitos, pruebas de membresía Merkle, prevención de doble gasto con nullifiers, binding de receptor. 3 pruebas Groth16 generadas end-to-end.
  • credential_proof.ach — Actualizado para usar arrays reales en vez de convención _N.
  • prove_secret_vote.ach — Modernizado a nueva sintaxis prove(x: Public).

Editor

  • Gramática TextMate actualizada: Public/Witness como modificadores de visibilidad, Field/Bool como tipos, definiciones con nombre circuit/prove, import circuit, builtins ZK separados.
  • Gramática sincronizada al sitio de docs para highlighting Shiki.

Documentación

  • 21 páginas actualizadas (EN + ES) a nueva sintaxis en tutoriales, getting-started, circuitos y conceptos ZK.

0.1.0-beta.14 — 2026-03-21

Pipeline ProveIR completo (Fases A-H). Los bloques prove ahora se compilan en tiempo de compilación y se serializan en bytecode, eliminando el re-parseo en runtime.

Nueva sintaxis

  • prove(public: [...]) — Sintaxis de bloque prove con auto-inferencia de witnesses (reemplazada por prove(name: Public) en beta.15).
let secret = 0p42
let hash = poseidon(secret, 0)

let p = prove(public: [hash]) {
    assert_eq(poseidon(secret, 0), hash)
}

Pipeline ProveIR

  • Fase A: Compilador ProveIR — AST a plantillas de circuito pre-compiladas con desugaring SSA, inlining de funciones y lowering de métodos.
  • Fase B: Instanciación — desenrolla loops, resuelve capturas, emite IR SSA plano. Incluye MAX_INSTANTIATE_ITERATIONS (1M) y enforcement de consistencia AssertEq para capturas usadas en estructura y restricciones.
  • Fase C: Serialización — bincode con header mágico ACHP, byte de versión, límite de 64 MB y validación post-deserialización.
  • Fase D: ach circuit usa ProveIR en vez de IrLowering (fallback IrLowering retenido para circuitos con imports).
  • Fase E: compile_prove() compila bloques prove a ProveIR en tiempo de compilación y almacena bytes serializados en el constant pool del bytecode vía TAG_BYTES.
  • Fase F: handle_prove() de la VM lee bytes ProveIR del constant pool, el handler deserializa e instancia con valores capturados del scope.
  • Fase G: El parser soporta sintaxis prove(name: Public). El compilador sintetiza statements PublicDecl y valida que no haya sintaxis mixta.
  • Fase H: Documentación actualizada (18 páginas, EN + ES).

Hardening

  • Variante de error explícita ImportsNotSupported (reemplaza matching frágil de strings para detección de fallback IrLowering).
  • Validación de referencias de captura en ProveIR::validate() — rechaza ArraySize::Capture y ForRange::WithCapture que referencien nombres de captura desconocidos.
  • Contrato de rango con signo documentado en Instruction::IsLt / IsLe.
  • Validación de inputs en execute_prove_ir() — errores en vez de saltar silenciosamente valores faltantes del scope.
  • Fix de scope de upvalues — compile_prove() incluye locals del scope padre para que bloques prove dentro de funciones anidadas puedan referenciar variables accesibles por upvalue.

Infraestructura

  • TAG_BYTES = 14 — nuevo tag de valor para constantes blob binarias (mark, sweep, recount del GC integrados).
  • BytesInterner — interner append-only del compilador para ProveIR serializado.
  • SER_TAG_BYTES — soporte del serializador/loader de bytecode para constantes bytes en archivos .achb.
  • Eliminado source: String del AST Expr::Prove y parámetro source no usado de Parser::new().

Ejemplos

Tres nuevos ejemplos en examples/:

  • private_auction.ach — Subasta con oferta sellada con commitments Poseidon, range checks y gadgets de comparación.
  • credential_proof.ach — Verificación anónima de credenciales con membresía Merkle y pruebas de umbral de edad.
  • hash_chain_proof.ach — Hashing Poseidon iterado con funciones dentro de bloques prove.

Editor

  • Gramática TextMate: regla prove-block para highlighting de sintaxis prove(name: Public).
  • LSP: snippet de completion provep, hover docs actualizados.

0.1.0-beta.13 — 2026-03-19

Dispatch de métodos, namespaces estáticos, reorganización de namespaces.

Features

  • Dispatch de métodos (.method()) — 50 métodos prototype en 8 tipos (Int, Field, String, List, Map, BigInt, Bool, Proof). Resueltos en tiempo de compilación vía opcode MethodCall (161).
  • Namespaces estáticos (Type::MEMBER) — Int::MAX, Int::MIN, Field::ZERO, Field::ONE, Field::ORDER, BigInt::from_bits. Compilados a LoadConst o GetGlobal.
  • Reorganización de namespaces — Funciones globales reducidas de 43 a 14 builtins + 2 std. Funciones como abs, len, min, max, pow, to_string migradas a métodos.

Documentación

  • 83 páginas de documentación (EN + ES) en docs.achrony.me.
  • Referencia de métodos Map, guía de migración de métodos, referencia de namespaces estáticos.

0.1.0-beta.12 — 2026-03-18

NativeModule trait, librería estándar, proc-macros.

Features

  • NativeModule trait — Registro modular de funciones nativas. Cada grupo de stdlib implementa NativeModule.
  • Crate achronyme-std — 16 nuevas funciones nativas: conversión de tipos, utilidades matemáticas, strings extendidos, I/O (feature-gated).
  • Proc-macros #[ach_native] / #[ach_module] — Generación automática de wrappers NativeFn con verificación de aridad y extracción de argumentos type-safe.
  • Traits FromValue / IntoValue — Conversión type-safe entre Value de la VM y tipos Rust.

0.1.0-beta.11 — 2026-03-16

Manifiesto de proyecto, comando ach init.

Features

  • achronyme.toml — Configuración de proyecto con búsqueda walk-up de directorio. Soporta secciones [project], [circuit] y [output].
  • ach init — Scaffolding interactivo de proyectos.
  • Resolución de config — Flags CLI > TOML > defaults.

0.1.0-beta.10 — 2026-03-16

Fix de lookup Plonkish, warning W003.

Bug Fix

  • Los range_check e IsLtBounded de Plonkish ahora generan pruebas KZG reales. Migrado de meta.selector() a meta.fixed_column() + meta.lookup_any().

Features

  • Warning W003 — Advierte cuando comparaciones quedan sin acotar (~761 restricciones) con sugerencia de range_check.

0.1.0-beta.9 — 2026-03-15

Fix de export R1CS, optimización IsLtBounded.

Fix de Seguridad

  • Export R1CS: write_lc() simplifica LinearCombinations antes de serialización (arregla fallos de wtns check en snarkjs).

Features

  • Optimización IsLtBounded — La pasada bound_inference reescribe comparaciones cuando los operandos tienen bitwidth probado. 761 restricciones bajan a 66 para comparaciones de 64 bits.

Benchmark

PrimitivaAchronymeCircomNotas
Poseidon(t=3)36251730% más eficiente
IsLt (64-bit)6667Paridad

0.1.0-beta.3 — 2026-03-04

Hardening zero-panic, refactorización de arquitectura.

Seguridad (16 fixes)

Todos los paths .unwrap() y panic! reemplazados con propagación de Result en compilador, VM, memoria y backends de restricciones.

Arquitectura (13 refactors)

Archivos monolíticos divididos en submódulos enfocados: vm.rs, field.rs, parser.rs, poseidon.rs, plonkish_backend.rs, lower.rs, eval.rs, Arena<T>.

Navigation