Achronyme 0.1.2 publicado: la verificacion separada conserva errores operativos y salida JSON global arrow_right_alt

Introducción

Qué es Achronyme, cómo encajan sus rutas de host y circuitos, y cuáles versiones están publicadas.

Achronyme es un lenguaje de programación para programas de host con capacidades acotadas y circuitos zero-knowledge.

Escribe código normal, haz explícitos los efectos concurrentes y externos, y decide qué afirmaciones deterministas se convierten en pruebas. El mismo lenguaje alimenta máquinas separadas de ejecución, witness y constraints en lugar de fingir que los tres trabajos tienen los mismos requisitos de runtime.

Versiones actuales

SuperficieEstable publicadoRecibo del source
Compilador y CLI0.1.2cd7a6e66
Editor y LSP0.3.1Compatible; LSP construido desde core b1774e88
Paquete web y servidor0.1.2Fijado al core cd7a6e66

El CLI, el paquete WASM y el servicio web desplegado usan la revision del core cd7a6e66e133bebd8e2026e321a4c85023c311f7. Editor 0.3.1 permanece compatible porque 0.1.2 no cambia los contratos del lenguaje ni del LSP. Consulta las notas de 0.1.2 para los fixes de verificacion separada y la declaracion de compatibilidad.

Ejecución del host

Los programas generales soportan closures, colecciones, concurrencia estructurada, recursos de archivo y TCP con propietario, y límites explícitos:

fn work(value) {
    await yield_now()
    return value * 2
}

let total = concurrent {
    let left = spawn work(10)
    let right = spawn work(11)
    await left + await right
}

El intérprete es portable. LLVM 21 ORC JIT acelera el código soportado y ach aot crea ejecutables nativos. El acceso a filesystem y red permanece denegado hasta que el operador entrega grants exactos.

Compilación de circuitos

circuit multiply(product: Public, a: Witness, b: Witness) {
    assert_eq(a * b, product)
}
ach circuit multiply.ach --inputs "product=42,a=6,b=7"

La ruta R1CS emite artefactos .r1cs y .wtns compatibles con snarkjs. Achronyme también importa templates Circom, calcula witnesses complejos con Artik y escalona la expansión repetida mediante Lysis.

Pruebas inline

let secret = 0p42
let commitment = poseidon(secret, 0p7)

let proof = prove(commitment: Public) {
    assert_eq(poseidon(secret, 0p7), commitment)
}

La generación de pruebas falla de forma cerrada si no se selecciona una fuente de llave:

# Solo desarrollo local
ach --insecure-dev-setup run proof.ach

# Store de producción derivado de ceremonia
ach --trusted-key-dir ./trusted-keys run proof.ach

La verificacion separada usa ach verify y no requiere configuracion de proyecto ni proving key. Los errores operativos de los artefactos permanecen separados de una prueba criptograficamente invalida.

Las tres máquinas

  • Akron ejecuta programas de host, tareas estructuradas, recursos con propietario y proof values mediante intérprete, JIT o AOT.
  • Artik ejecuta programas deterministas de witness, incluyendo operaciones bigint nativas usadas por circuitos Circom a escala ECDSA.
  • Lysis escalona la instanciación y emite cuerpos compartidos de constraints sin expansión eager de memoria.
Flowchart diagram10 nodes, 10 edgesach runach circuiten líneaFuente (.ach)Parser → ASTPratt + descenso recursivobloque prove { }compilar + testigo + verificar (en línea)Bytecode → VMmodo ejecuciónSSA IR + Optimizarmodo circuitoR1CSGroth16PlonkishKZG-PlonK.r1cs + .wtnscompatible con snarkjsGates + Lookupscopy constraintsPrueba nativa

Dónde continuar

Navigation