Anotaciones de Tipo

Anotaciones de tipo opcionales para variables de circuito, funciones y vinculaciones.

Achronyme soporta tipado gradual en circuitos. Puedes agregar anotaciones de tipo opcionales a declaraciones, vinculaciones y funciones. El código sin anotar funciona exactamente como antes — las anotaciones son estrictamente opcionales.

Universo de Tipos

Cuatro tipos están disponibles en contexto de circuito:

Bool es un subtipo de Field — un valor booleano puede usarse donde se espera un elemento de campo. Lo inverso es un error a menos que el valor sea un booleano probado (ej., un resultado de comparación o la constante 0/1).

Field y Bool no son palabras clave. Son identificadores contextuales reconocidos solo después de : o ->. Puedes seguir usando Field y Bool como nombres de variables en código regular.

Declaraciones de Entrada

Agrega : Type después del nombre del parametro en la firma del circuito. Usa Public o Witness como visibilidad antes del tipo:

circuit entradas_tipadas(root: Public Field, flag: Witness Bool, secret: Witness Field, path: Witness Field[3], indices: Witness Bool[3]) {
    // cuerpo del circuito
}

Sin anotaciones, las entradas son no tipadas por defecto — mismo comportamiento que antes:

circuit entradas_sin_tipo(root: Public, secret: Witness) {
    // cuerpo del circuito
}

Ambas formas pueden coexistir en el mismo circuito:

circuit entradas_mixtas(root: Public Field, leaf: Witness, path: Witness Field[3], indices: Witness) {
    // cuerpo del circuito
}

Vinculaciones Let

Anota vinculaciones locales con : Type después del nombre, antes de =:

circuit vinculaciones_let(a: Witness Field, b: Witness Field) {
    let product: Field = a * b
    let is_equal: Bool = a == b
}

El compilador maneja las anotaciones dependiendo del tipo inferido de la expresión:

• Expresión tipada coincide con la anotación: Sin costo extra. let eq: Bool = a == b es gratis porque == ya produce Bool.
• Expresión tipada conflicta: Error. let x: Bool = a + 1 falla porque + produce Field, que es incompatible con Bool.
• Expresión no tipada con : Bool: El compilador emite una restricción RangeCheck(v, 1) para forzar v * (1 - v) = 0, costando 1 restricción extra. Esto es necesario para la solidez — sin verificación, un probador malicioso podría asignar cualquier valor.
• Expresión no tipada con : Field: No se necesita verificación. Field es el predeterminado y no restringe el espacio de valores.

circuit ejemplo_incompatible(a: Witness Field) {
    // Error: incompatibilidad de anotación de tipo para `x`: declarado como Bool,
    //        pero la expresión tiene tipo Field
    let x: Bool = a + 1
}

circuit bool_verificado(w: Witness) {
    // Verificado: emite RangeCheck(w, 1) — cuesta 1 restricción
    let b: Bool = w
}

Las operaciones aritméticas (+, -, *, /, ^) producen Field. Las comparaciones y operaciones lógicas (==, !=, <, <=, >, >=, &&, ||, !) producen Bool.

Vinculaciones de Array

Para anotaciones de array, el compilador valida que la longitud del array coincida con el tamaño declarado:

circuit error_longitud_array(x: Witness, y: Witness) {
    // Error: incompatibilidad de longitud de array: se esperaban 3, se obtuvieron 2
    let a: Field[3] = [x, y]
}

Las anotaciones Bool[N] verifican cada elemento no tipado individualmente (1 restricción por elemento):

circuit verificacion_array_bool(x: Witness, y: Witness) {
    // Verificado: emite RangeCheck para cada elemento no tipado — cuesta 2 restricciones
    let flags: Bool[2] = [x, y]
}

Funciones

Anota parámetros con : Type y tipos de retorno con -> Type:

circuit con_funciones(a: Witness Field, b: Witness Field) {
    fn hash_pair(a: Field, b: Field) -> Field {
        poseidon(a, b)
    }

    fn is_valid(x: Field, y: Field) -> Bool {
        x == y
    }

    let h = hash_pair(a, b)
    let valid = is_valid(a, b)
}

Se permite mezclar parámetros tipados y no tipados:

circuit parametros_mixtos(a: Witness Field, b: Witness) {
    fn scale(x: Field, factor) {
        x * factor
    }

    let result = scale(a, b)
}

El compilador verifica que los argumentos coincidan con los tipos de parámetro declarados en cada punto de llamada:

circuit verificacion_llamada(a: Witness Field) {
    fn double(x: Field) -> Field { x + x }

    let result: Field = double(a)    // ok
}

Verificación Bool en Parámetros y Tipos de Retorno

Cuando un parámetro : Bool recibe un argumento no tipado, el compilador emite un RangeCheck para forzar la restricción booleana (1 restricción extra por argumento no tipado):

circuit verificacion_param_bool(w: Witness) {
    fn check(b: Bool) { assert(b) }
    check(w)     // emite RangeCheck(w, 1) — 1 restricción extra
}

De manera similar, cuando una función con tipo de retorno -> Bool produce un resultado no tipado en el cuerpo, el compilador fuerza el booleano en el valor de retorno:

circuit verificacion_retorno_bool(w: Witness) {
    fn to_flag(x: Field) -> Bool { x }
    let f = to_flag(w)    // emite RangeCheck en el valor de retorno — 1 restricción extra
}

Si el argumento o valor de retorno ya tiene un tipo probado (ej., de una comparación), no se emite restricción extra.

Subtipado: Bool como Field

Los valores Bool pueden usarse en contexto aritmético (de campo). Esto es seguro porque los booleanos son 0 o 1 en el campo:

circuit subtipado_bool(flag: Witness Bool) {
    // Bool usado en aritmética — permitido (Bool es subtipo de Field)
    let as_field: Field = flag + flag
}

Lo inverso depende del tipo del valor fuente:

• Tipado como Field: Error. Un valor explícitamente tipado como Field no puede estrecharse a Bool:

  circuit error_field_a_bool(x: Witness Field) {
      // Error: x es Field, no se puede anotar como Bool
      let b: Bool = x
  }

• No tipado: Verificación. El compilador emite RangeCheck(x, 1) para forzar x * (1 - x) = 0 (1 restricción):

  circuit verificacion_no_tipado(x: Witness) {
      // Verificado: emite RangeCheck — 1 restricción extra
      let b: Bool = x
  }

• Ya probado como booleano: Gratis. No se emite restricción extra:

  circuit booleano_probado(a: Witness Field, b: Witness Field) {
      // El resultado de comparación es un booleano probado — la anotación es gratis
      let eq: Bool = a == b
  }

Ahorro de Restricciones

Anotar una entrada como : Bool emite una restricción de verificación RangeCheck única (v * (1-v) = 0) en el sitio de declaración. Este estado booleano verificado se propaga a través de bool_prop, permitiendo que todos los usos posteriores omitan la verificación booleana redundante. El efecto neto es un ahorro cuando la variable se usa múltiples veces en contexto booleano.

// Sin anotación: cada mux agrega 1 verificación booleana para cond
circuit sin_anotacion(cond: Witness, a: Witness, b: Witness, c: Witness, d: Witness) {
    let r1 = mux(cond, a, b)   // 2 restricciones (1 verificación + 1 selección)
    let r2 = mux(cond, c, d)   // 2 restricciones (1 verificación + 1 selección)
    // Total: 4 restricciones
}

// Con anotación: 1 verificación en la declaración, usos posteriores omiten
circuit con_anotacion(cond: Witness Bool, a: Witness, b: Witness, c: Witness, d: Witness) {
    // cond declarado como Bool — 1 restricción (verificación RangeCheck)
    let r1 = mux(cond, a, b)   // 1 restricción (solo selección, verificación omitida)
    let r2 = mux(cond, c, d)   // 1 restricción (solo selección, verificación omitida)
    // Total: 3 restricciones (se ahorró 1)
}

Esta optimización es aplicada por el pase bool_prop, que rastrea variables probadas como booleanas a través del programa. El pase reconoce estas fuentes como booleanas probadas:

• Constantes 0 y 1
• Resultados de comparación (==, !=, <, <=, >, >=)
• Resultados de RangeCheck(x, 1) (incluyendo los emitidos por verificación : Bool en declaraciones, vinculaciones let, parámetros de función y tipos de retorno)
• Operandos y resultados de Assert
• Not/And/Or/Mux de operandos booleanos probados

Verificación vs. Ahorro

Todas las anotaciones : Bool emiten restricciones de verificación por solidez. El costo es único por variable; los usos posteriores se benefician del ahorro de bool_prop.

El costo de verificación es una garantía de solidez única. Los usos posteriores de la variable verificada se benefician del ahorro de bool_prop.

Ejemplo Completo

Una prueba de membresía Merkle completamente tipada:

circuit prueba_merkle(root: Public Field, leaf: Witness Field, path: Witness Field[3], indices: Witness Bool[3]) {
    merkle_verify(root, leaf, path, indices)
}

El mismo circuito con funciones auxiliares tipadas:

circuit verificar_cadena_hash(expected: Public Field, a: Witness Field, b: Witness Field, c: Witness Field) {
    fn hash_chain(x: Field, y: Field, z: Field) -> Field {
        let h: Field = poseidon(x, y)
        poseidon(h, z)
    }

    let result: Field = hash_chain(a, b, c)
    assert_eq(result, expected)
}

Referencia Rápida

Errores

Modo VM

Las anotaciones de tipo funcionan en ambos modos: circuito y VM. En modo circuito generan restricciones (como se describe arriba). En modo VM producen advertencias en tiempo de compilación cuando la anotación no coincide con el valor:

W006: Tipo Incompatible

Se emite cuando el tipo de un valor literal no coincide con la anotación:

let x: Bool = 0p42    // W006: type annotation `Bool` on `x` does not match value type `Field`
let y: Field = "hello" // W006: type annotation `Field` on `y` does not match value type `String`

El código sigue ejecutándose — la VM es dinámicamente tipada y las anotaciones son informativas. Pero la advertencia detecta errores potenciales temprano.

W007: Tamaño de Array Incompatible

Se emite cuando un literal de array tiene una longitud diferente a la anotación:

let a: Field[3] = [1, 2]  // W007: type `Field[3]` expects 3 elements, but array has 2

Lo Que No Se Verifica

Las advertencias solo se emiten para valores literales que pueden analizarse estáticamente. Las expresiones dinámicas (llamadas a funciones, referencias a variables, operaciones binarias) no se verifican:

let x: Bool = f()   // Sin advertencia — el tipo de retorno de f() es desconocido en tiempo de compilación
let y: Field = a + b // Sin advertencia — el tipo de la expresión depende de valores en tiempo de ejecución

Recomendación

Usa anotaciones de tipo en código VM para:

• Documentar intención — deja claro que una variable contiene un elemento de campo vs un booleano
• Detectar errores — asignar un string a un binding : Field se señala inmediatamente
• Preparar para circuitos — el código VM anotado transiciona a modo circuito sin cambios
• Ayudar a bloques prove — las anotaciones de array como Field[N] habilitan la captura automática de arrays en bloques prove(name: Public)