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

Funciones en Circuitos

Cómo funcionan las funciones dentro de la compilación de circuitos.

Las funciones en circuitos usan la misma sintaxis fn que el código regular de Achronyme, pero se comportan de manera diferente internamente — cada llamada se inserta en línea.

Sintaxis

Define funciones de la misma manera que en modo regular:

fn double(x) {
    x + x
}

Las funciones pueden incluir anotaciones de tipo en parámetros y tipos de retorno:

fn double(x: Field) -> Field {
    x + x
}

Llámalas como de costumbre:

circuit double_demo(vals: Witness[3]) {
    fn double(x) { x + x }
    assert_eq(double(vals[0]), vals[0] + vals[0])
}

Inserción en Línea

No hay pila de llamadas a funciones en circuitos. Cada punto de llamada expande el cuerpo de la función con los argumentos sustituidos. Si llamas a una función 5 veces, su cuerpo se compila 5 veces.

circuit square_demo(vals: Witness[3]) {
    fn square(x) { x * x }

    // Cada llamada se inserta independientemente — 1 restricción cada una
    let a = square(vals[0])
    let b = square(vals[1])
    let c = square(vals[2])
}

Esto significa que las funciones son una conveniencia para organizar código, no un mecanismo para reducir el conteo de restricciones.

Costo de Restricciones

El costo de una llamada a función es igual a la suma de las restricciones de su cuerpo, más cualquier costo de verificación de tipo. Una función con dos multiplicaciones cuesta 2 restricciones por llamada.

fn dot(a0, a1, b0, b1) {
    a0 * b0 + a1 * b1      // 2 restricciones (dos multiplicaciones de variables)
}

Llamar a dot tres veces produce 6 restricciones.

Costos de Verificación de Tipo

Cuando una función tiene parámetros tipados o un tipo de retorno, el compilador puede emitir restricciones adicionales:

  • Parámetro : Bool con argumento no tipado: +1 restricción por parámetro (emite RangeCheck(arg, 1))
  • Retorno -> Bool con resultado no tipado en el cuerpo: +1 restricción (emite RangeCheck(result, 1))
  • Argumentos/resultados ya tipados que coinciden: Sin costo extra
circuit type_cost_demo(w: Witness, b: Witness Bool) {
    fn check(b: Bool) { assert(b) }    // cuerpo: 2 restricciones (assert)

    check(w)                            // total: 2 + 1 = 3 restricciones (1 por verificación de param)
    check(b)                            // total: 2 restricciones (sin verificación necesaria)
}

Restricciones

RestricciónErrorRazón
Sin recursiónRecursiveFunctionLas funciones se insertan en línea — la recursión haría un bucle infinito
Sin closures—Sin entorno en tiempo de ejecución para capturar
Sin funciones de orden superior—No se pueden pasar funciones como valores de circuito
Sin funciones anónimas—Solo se soportan definiciones fn con nombre
Incompatibilidad de tipoAnnotationMismatchTipo de argumento no coincide con parámetro tipado (ej., arg Field para param Bool)
Verificación Bool—Arg no tipado para param : Bool emite RangeCheck (+1 restricción)

Las funciones en circuitos son puramente un mecanismo de tiempo de compilación. No pueden capturar variables de ámbitos externos (excepto entradas declaradas), no pueden pasarse como valores y no pueden llamarse a sí mismas.

Ejemplo

Un circuito completo usando una función auxiliar:

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

    let n = len(vals)
    assert_eq(n, 3)

    fn double(x) { x + x }
    assert_eq(double(vals[0]), vals[0] + vals[0])
}
Navigation