Presentamos Achronyme — un lenguaje para pruebas zero-knowledge. Lee el anuncio →
achronyme
en

Pruebas en Línea

Usando bloques prove para generación de pruebas en línea.

El bloque prove te permite generar pruebas de conocimiento cero en línea, sin salir de la VM. Compila su cuerpo como un circuito en tiempo de compilación vía ProveIR, genera un testigo a partir de variables capturadas y devuelve una prueba criptográfica.

Ejemplo Básico

let x: Field = 0p6
let y: Field = 0p7
let product: Field = 0p42

let p = prove(product: Public) {
    assert_eq(x * y, product)
}

print(proof_json(p))

El bloque prove:

  1. Compila assert_eq(x * y, product) como un circuito en tiempo de compilación
  2. Captura x e y del ámbito externo como entradas testigo (inferidas automáticamente)
  3. Marca product como entrada pública (declarada como product: Public)
  4. Genera una prueba Groth16 en tiempo de ejecución
  5. Devuelve un ProofObject

Auto-Inferencia de Testigos

Con la sintaxis prove(name: Public), solo declaras qué variables son públicas — todo lo demás se infiere automáticamente como testigo:

let secret: Field = 0p42
let hash: Field = 0p17159...

let p = prove(hash: Public) {
    assert_eq(poseidon(secret, 0), hash)
}
  • hash se declara como hash: Public → entrada pública (visible para el verificador)
  • secret se referencia en el cuerpo pero no está en la lista pública → testigo (privado, inferido automáticamente)

El verificador aprende solo que algún valor hashea a hash, sin conocer secret.

Declaraciones Explícitas (Sintaxis Clásica)

La sintaxis explícita witness/public también está soportada:

let secret: Field = 0p42
let hash: Field = 0p17159...

let p = prove {
    witness secret    // privado — el probador lo conoce
    public hash       // público — el verificador lo ve
    assert_eq(poseidon(secret, 0), hash)
}

Ambas sintaxis producen circuitos idénticos. La forma prove(name: Public) es más concisa; la forma explícita da control total. No se pueden mezclar ambas en el mismo bloque.

Auto-Conversión de Enteros

Los enteros capturados por bloques prove se convierten automáticamente a elementos de campo. Este es el único lugar donde la conversión Int→Field ocurre implícitamente:

let a = 10
let b = 20
let sum = 30

prove(sum: Public) {
    assert_eq(a + b, sum)
}

Fuera de los bloques prove, mezclar Int y Field genera un error TypeMismatch. Usa literales de campo 0p para conversión explícita.

Acceder a Componentes de la Prueba

Un ProofObject contiene tres componentes JSON:

let p = prove(y: Public) {
    assert_eq(x, y)
}

// Datos de prueba Groth16 (pi_a, pi_b, pi_c)
let proof = proof_json(p)

// Entradas públicas como array de cadenas decimales
let inputs = proof_public(p)

// Clave de verificación (para verificación on-chain)
let vkey = proof_vkey(p)

print(proof)
print(inputs)
print(vkey)

Verificar Pruebas

Usa verify_proof() para verificar una prueba dentro de la VM:

let p = prove(hash: Public) {
    assert_eq(poseidon(secret, 0), hash)
}

let ok = verify_proof(p)
print(ok)  // true

Arrays y Funciones

Los bloques prove soportan arrays, funciones y todas las características del modo circuito:

let v0: Field = 0p10
let v1: Field = 0p20
let v2: Field = 0p30
let total: Field = 0p60

prove(total: Public) {
    let vals: Field[3] = [v0, v1, v2]
    let acc: Field = vals[0] + vals[1] + vals[2]
    assert_eq(acc, total)
    assert_eq(len(vals), 3)
}

Poseidon en Bloques Prove

Las funciones criptográficas integradas funcionan dentro de bloques prove:

let a: Field = 0p1
let b: Field = 0p2
let h: Field = 0p7853200120776062878684798364095072458815029376092732009249414926327459813530

prove(h: Public) {
    assert_eq(poseidon(a, b), h)
}

Verificaciones de Rango

Fuerza que un valor quepa dentro de cierto número de bits:

let val: Field = 0p200

prove() {
    range_check(val, 8)   // 0 ≤ val < 256
}

Múltiples Bloques Prove

Puedes usar múltiples bloques prove en secuencia:

let a: Field = 0p3
let b: Field = 0p4
let sum: Field = 0p7
let product: Field = 0p12

prove(sum: Public) {
    assert_eq(a + b, sum)
}

prove(product: Public) {
    assert_eq(a * b, product)
}

Cada bloque prove compila y prueba independientemente.

Ejecutar con Generación de Pruebas

Para generar pruebas Groth16 reales, proporciona un archivo Powers of Tau:

ach run my_program.ach --ptau pot12_final.ptau

Sin --ptau, los bloques prove aún verifican restricciones pero devuelven VerifiedOnly (no se genera prueba criptográfica).

La zkey se cachea en ~/.achronyme/cache/ para ejecuciones posteriores más rápidas.

Selección de Backend

Por defecto, los bloques prove usan el backend R1CS/Groth16. Para usar Plonkish/KZG-PlonK:

ach run my_program.ach --prove-backend plonkish
Navigation