VM de Testigos Artik

VM basada en registros para cómputo de testigos: bytecode, superficie de lift, y despacho R1CS.

Artik es una VM dedicada, basada en registros, para cómputo de testigos en circuitos de Achronyme. Cierra la brecha E212 — la clase de funciones Circom (con var, for, if/else, llamadas anidadas, y argumentos de señal en tiempo de ejecución) que antes no podían inlinearse en un circuito.

Artik está emparejado con Akron, la VM de bytecode de propósito general. A diferencia de Akron, Artik no tiene heap, ni GC, ni valores etiquetados en tiempo de ejecución, ni estado compartido con la VM principal. Es un intérprete de un solo uso: señales entran, slots de testigo salen.

Por qué existe Artik

Antes de Artik, cualquier cuerpo de función no trivial con argumentos de señal surgía como E212 — function body not inlineable with runtime signal arguments. Circom resuelve el mismo problema con calculadoras de testigos ejecutadas en tiempo de prueba; SHA-256, Pedersen y primitivas de la familia EdDSA lo necesitan.

Artik compila esos cuerpos de función a un bytecode compacto, emite una Instruction::WitnessCall en el IR, y ejecuta el bytecode en tiempo de generación de testigos R1CS contra el vector de testigos vivo. La carga de trabajo más exigente que ahora lleva end-to-end es ECDSAVerify(64,4) — el circuito de referencia de circomlib más pesado (ECDSA secp256k1) — que se liftea, genera un testigo, y prueba a través de Groth16 con el testigo verificando (R1CS optimizado ~1.49M restricciones, por debajo del propio conteo de circom para el mismo circuito).

Arquitectura

.circom de Circom
    |
    v
circom::lowering (ProveIR)
    |
    +-- expresion pura?     --> CircuitExpr (inline)
    |
    +-- cuerpo complejo?    --> artik_lift --> Bytecode Artik
                                                |
                                                v
                                      Instruction::WitnessCall { program_bytes }
                                                |
                                                v
                              Backend R1CS: WitnessOp::ArtikCall
                                                |
                                                v
                              WitnessGenerator::execute_op --> artik::execute

Layout del Crate

artik/
  src/
    lib.rs        // re-exports, superficie publica
    header.rs     // header de 16 bytes + FieldFamily
    ir.rs         // Instr, IntW, IntBinOp, RegType, OpTag
    program.rs    // Program + FieldConstEntry
    bytecode/
      encode.rs   // Program -> bytes
      decode.rs   // bytes -> Program (corre validador)
    validate.rs   // invariantes estructurales
    executor.rs   // execute / execute_with_budget
    builder.rs    // API ProgramBuilder (usada por el lift)
    error.rs      // ArtikError

Formato de Bytecode

Cada programa .artik está precedido por un header de 16 bytes:

0..4   magic "ARTK"
4..6   version (u16 LE)           // actual: 1
6      field_family (u8)          // 0=BnLike256, 1=Goldilocks64, 2=M31_32
7      flags (u8)
8..12  const_pool_len (u32 LE)
12..16 body_len (u32 LE)

El cuerpo comienza con un prelude frame_size de 4 bytes, luego una secuencia de instrucciones codificadas. El validador revisa cada programa decodificado antes de que el ejecutor lo toque.

FieldFamily

Un mismo blob .artik puede ejecutarse contra cualquier primo de su familia declarada — el runtime toma F del llamador.

Registros y Tipos

Artik es estilo SSA: cada registro se asigna como máximo una vez por función (impuesto en tiempo de emisión). Cada registro carga una categoría de tipo, rastreada por el validador:

enum RegType {
    Field,
    Int(IntW),          // U8 | U32 | U64 | I64
    Array(ElemT),       // Field | IntU8 | IntU32 | IntU64 | IntI64
}

Las operaciones enteras son bit-exactas con semántica de wrapping; se aplica una máscara específica de ancho a cada salida aritmética. Registros de field e int no pueden mezclarse sin una conversión explícita IntFromField / FieldFromInt.

Opcodes

32 opcodes, agrupados por categoría. La codificación es <opcode tag>(1 byte) + operandos.

Flujo de Control

Call invoca otro subprograma por func_id: los registros de argumento se copian celda por celda en los registros de parámetro del callee y los valores de retorno regresan a los rets del llamador. Las celdas de array cargan un handle hacia el almacén global de arrays del programa, así que los argumentos y retornos de array cruzan los frames sin copia de respaldo. Esto es lo que hace a Artik una VM multi-subprograma — un cuerpo Circom lifteado puede llamar a funciones hermanas en vez de forzar que todo se inlinee.

Constantes y Señales

Las señales son de solo lectura; los slots de testigo son el único canal de salida.

Operaciones de Field

FIDiv, FIRem, FShr, FAnd y FPow2 operan a precisión completa de field en vez de demotar a un ancho entero fijo, así que la aritmética de limbs estilo bignum se mantiene exacta. FCmpLt es la comparación ordenada sin signo a nivel de field de la que dependen los cuerpos de división larga y reducción modular de secp256k1 — un < ordenado que se sostiene sobre el valor de field completo de 256 bits, no una comparación truncada a U64.

Operaciones Enteras

IntBinOp cubre Add, Sub, Mul, And, Or, Xor, Shl, Shr, CmpLt, CmpEq. Los Rotl32 / Rotr32 / Rotl8 de la familia SHA son opcodes de primera clase para que el lowering de hashes de bits se mantenga compacto.

Conversión

Arrays

Los arrays viven en un Vec bump-allocated gestionado por el ejecutor — sin GC. ArrayId / ArrayFromId pasan handles de array a través de registros escalares, que es como los arrays viajan entre frames de Call y como se direccionan slices de fila 2D sin copiar las celdas de respaldo.

Intrínsecos Nativos de Bignum

Un puñado de rutinas bignum multi-limb (el inverso modular estilo Fermat de secp256k1, la exponenciación modular, el producto escolar y la división larga) son demasiado lentas para interpretar limb por limb. El lift toma una huella (fingerprint) de estos cuerpos de función y, al coincidir, los ejecuta nativamente como ModInv, ModExp, Prod o LongDiv en vez de recorrer el bytecode interpretado:

Cada cuerpo reconocido aún recae en el camino interpretado si su huella no coincide exactamente, así que la solidez no cambia. El camino nativo es lo que bajó el recorrido de testigos de ECDSAVerify(64,4) de aproximadamente 226 s a 64 s end-to-end — la inversión de Fermat interpretada era el 98.6% del recorrido — con conteo de restricciones y verificación idénticos.

Límites Estáticos y de Runtime

El validador rechaza bytecode adversarial antes de que alcance al ejecutor:

Las constantes mayores a family.max_const_bytes() son rechazadas. Todos los traps emergen como variantes tipadas de ArtikError.

Superficie de Lift

circom::lowering::artik_lift compila cuerpos de función a bytecode Artik. Qué acepta actualmente el lift:

Sentencias

• VarDecl escalar y array 1D
• Substitution escalar e indexado (arr[i] = expr) con índices de runtime
• Asignaciones compuestas (+=, *=, etc.), con const-fold en variables de loop
• For con bounds de tiempo de compilación (desenrollado, máx 4096 iteraciones)
• IfElse — folded en tiempo de compilación y runtime vía mux de aritmética de field
• Return — escalar o array
• ++ / -- solos sobre variables de loop

Expresiones

• Ident, Number, HexNumber
• BinOp — Add/Sub/Mul/Div + bitwise And/Or/Xor/ShiftL/ShiftR vía int-promotion U32
• UnaryOp::Neg y ::BitNot
• Index con índice folded o de runtime
• Call — inlineado, retorno escalar o array
• Ternary

Mux if/else en Runtime

Ambos brazos se liftean; locales escalares se fusionan vía el patrón estándar cond * then + (1 - cond) * else. cond se normaliza vía FEq(cond, 0) -> FieldFromInt U8 -> 1 - is_zero. Los brazos deben ser libres de efectos (sin escrituras a array, sin return).

Llamadas anidadas son admisibles dentro de brazos mux — los returns anidados capturan a nested_result sin emitir WriteWitness.

Despacho en Runtime

ir::eval::evaluate + evaluate_lenient despachan a artik::execute en cada Instruction::WitnessCall:

Instruction::WitnessCall {
    outputs: Vec<Variable>,        // slots de testigo a llenar
    inputs: Vec<LinearCombination>, // senales, materializadas en cables LC
    program_bytes: Vec<u8>,        // el blob .artik
}

El backend R1CS materializa cada LC de entrada en un cable de testigo fresco, aloca cables para cada salida, y emite un WitnessOp::ArtikCall en el trace. En tiempo de generación de testigos, WitnessGenerator::execute_op decodifica el bytecode y corre Artik contra el vector de testigos vivo.

Ver Generación de Testigos para el modelo completo de replay del trace.

Decisiones de Diseño

• Canal lateral vía Instruction::WitnessCall, no una tabla lateral separada en IrProgram. Mantiene los programas de testigo en orden de instrucción para que el loop de witness-gen del prover naturalmente los intercale entre otros replays de WitnessOp. Costo: ~8 sitios de match exhaustivo extendidos en ir + zkc.
• Salida primaria = outputs[0], extras vía extra_result_vars. Los lifts que retornan array exponen slots de testigo secundarios así. Invariante no-vacío impuesto por el lift.
• Salidas públicas ganan sobre cables de testigo frescos. Instantiate reutiliza output_pub_vars[name] cuando el nombre de binding coincide con una señal de salida pública, así Artik escribe directamente en el cable de salida pública.
• Chequeo de familia BN vía F::PRIME_ID, no type_name. Más limpio y captura Goldilocks como no soportado en vez de aceptarlo silenciosamente.
• Sin heap, sin GC. Los arrays son bump-allocated en un solo Vec poseído por el ejecutor. Un programa es de un solo uso: corre una vez por prueba, luego se descarta.

Gaps recientemente cerrados

Los tres gaps históricos más grandes del lift están todos cerrados — son exactamente lo que habilitó el cierre del testigo de ECDSA secp256k1:

• Parámetros array — los cuerpos de función con params array (sha256compression(hin[256], inp[512]), helpers de secp256k1) se liftean vía inferencia de dimensión del call-site + binding de array, ya no bailan a E212.
• Arrays multidimensionales — los slices de fila 2D (var M[t][t], pubkey[2][k]) se direccionan y pasan mediante handles de array, no solo 1D.
• Bounds de loop en runtime — los loops con un end dependiente de señal o descendente se liftean usando el JumpIf de Artik en vez de requerir un desenrollado en tiempo de compilación.

Límites Restantes

• Backend Plonkish — retorna error limpio en WitnessCall. R1CS es el único camino de prueba para Artik en este release.

Cobertura E2E

Archivos Fuente