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

Declaraciones

Declaraciones de entradas publicas y de testigo en definiciones de circuitos.

Cada circuito declara sus entradas en la firma del circuit. Cada parametro especifica una visibilidadPublic (visible para el verificador) o Witness (conocida solo por el probador).

Sintaxis Basica

Una declaracion de circuito nombra el circuito y lista sus parametros con su visibilidad:

circuit multiplicar(output: Public, a: Witness, b: Witness) {
    assert_eq(a * b, output)
}

Las entradas publicas se convierten en parte de la declaracion publica de la prueba — cualquiera que verifique la prueba puede ver sus valores. Las entradas testigo permanecen privadas para el probador.

Parametros de Array

Declara un array de entradas de tamano fijo con sintaxis de corchetes despues del tipo:

circuit verificar_merkle(root: Public, path: Witness Field[3], indices: Witness Bool[3]) {
    // path e indices tienen 3 elementos cada uno
    // accede con indexacion estandar: path[0], path[1], path[2]
}

Los parametros de array crean variables indexadas a las que accedes con indexacion estandar. Funcionan tanto para entradas publicas como de testigo:

circuit verificar_compromisos(commitments: Public Field[4], secrets: Witness Field[4]) {
    for i in 0..4 {
        assert_eq(poseidon(secrets[i], 0), commitments[i])
    }
}

Anotaciones de Tipo

Los parametros pueden incluir anotaciones de tipo opcionales (Field o Bool) entre la visibilidad y el nombre del parametro (o los corchetes del array):

circuit ejemplo_tipado(root: Public Field, flag: Witness Bool) {
    if flag {
        assert_eq(root, poseidon(root, 0))
    }
}

Para parametros de array, el tipo va entre la visibilidad y los corchetes:

circuit camino_merkle(root: Public Field, path: Witness Field[3], indices: Witness Bool[3]) {
    // indices son de tipo booleano, ahorrando 1 restriccion cada uno
}

Anotar un testigo como Bool ahorra 1 restriccion al omitir la verificacion booleana. Consulta Anotaciones de Tipo para detalles completos.

Uso de Entradas Declaradas

Dentro del cuerpo del circuito, los parametros son variables ordinarias. Usalas en expresiones, pasalas a funciones integradas e indexa arrays:

circuit verificar_producto(output: Public, a: Witness, b: Witness) {
    let product = a * b
    assert_eq(product, output)

    let sum = a + b
    assert_eq(sum, a + b)
}

Los elementos de array se acceden por indice:

circuit verificar_suma(expected_sum: Public, vals: Witness Field[3]) {
    let acc = vals[0]
    let acc = acc + vals[1]
    let acc = acc + vals[2]
    assert_eq(acc, expected_sum)
}

Uso por CLI

Pasa valores concretos para las entradas del circuito con la bandera --inputs:

ach circuit program.ach --inputs "a=3,b=5,output=15"

Las entradas de array se pasan con nombres indexados:

ach circuit merkle.ach --inputs "root=123,leaf=42,path_0=99,path_1=77,indices_0=0,indices_1=1"

Errores

ErrorCausa
DuplicateInputMismo nombre declarado dos veces en la lista de parametros
UndeclaredVariableUsar una variable dentro del cuerpo del circuito que no es un parametro
AnnotationMismatchTipo declarado no coincide con el tipo inferido
Navigation