Emulación de 32 bits en ZK

Last updated on Aug 20, 2025

El tipo de datos predeterminado en ZK es el elemento de campo (field element), donde toda la aritmética se realiza módulo un número primo grande. Sin embargo, la mayoría de los cálculos “reales” se realizan utilizando números de 32, 64 o 256 bits, dependiendo de la máquina virtual o del entorno de ejecución.

¿Por qué necesitamos la emulación de 32 bits?

Muchas funciones hash criptográficas operan sobre palabras de 32 bits ya que, históricamente, 32 bits era el tamaño de palabra predeterminado de muchas CPUs. Esto posteriormente aumentó a 64 bits. La EVM utiliza 256 bits para poder acomodar fácilmente el hash keccak256.

Si queremos usar ZK para probar la ejecución correcta de una función hash tradicional o de alguna máquina virtual que no utilice campos finitos (la mayoría no lo hace), entonces necesitamos “modelar” los tipos de datos tradicionales con un elemento de campo. Por lo tanto, usamos un elemento de campo (signal) en Circom para almacenar un número que no puede exceder lo que puede contener un número de 32 bits, aunque la signal pueda contener valores mucho mayores que 32 bits.

Palabras de 32 bits vs elementos de campo finito

La diferencia clave entre una palabra de 32 bits y un elemento de campo finito es el punto en el que se desbordan (overflow). En Circom, o en cualquier lenguaje que utilice la curva bn128, el desbordamiento ocurre en $p$ donde $p$ = 21888242871839275222246405745257275088548364400416034343698204186575808495617. En una máquina de 32 bits, el desbordamiento ocurre en 4294967296 o, en general, en $2^n$ donde $n$ es el número de bits en la máquina virtual.

Se puede pensar en una máquina virtual de 32 bits realizando toda la aritmética módulo $2^{32}$ . Una máquina virtual normal se desborda en ese número por defecto. Sin embargo, al hacer aritmética modular en un campo finito, calcular el módulo $2^{32}$ añadiría bastantes restricciones (constraints), como veremos más adelante, pero afortunadamente, existe un truco matemático útil para hacerlo de manera eficiente.

Las dos funciones siguientes son equivalentes al calcular el módulo $2^{32}$ :

contract DemoMod32 {
  function mod32(uint256 x) public pure returns (uint256) {
    return x % (2**32);
  }

  function mod32e(uint256 x) public pure returns (uint256) {
    // only keep the 32 least significant bits
    return uint256(uint32(x)); 
  }
}

Podemos calcular $\mod 2^{32}$ simplemente conservando solo los 32 bits menos significativos. En el apéndice se encuentra una verificación formal de esto. Antes de realizar cualquier aritmética en una signal que contenga un número de 32 bits, primero debemos estar completamente seguros de que el número almacenado en la signal, de hecho, cabe en 32 bits.

La comprobación de rango (range check) de 32 bits

Si estamos creando un circuito ZK que simula un cálculo usando palabras de 32 bits, entonces necesitamos asegurarnos de que ninguna de las signals contenga un valor mayor o igual a $2^{32}$ . Algo intuitivo sería usar la plantilla (template) LessThan de la siguiente manera:

signal safe;
safe <== LessThan(252)([x, 2**32]);
safe === 1;

Sin embargo, este circuito crea más restricciones de las necesarias.

Un enfoque más eficiente sería aprovechar la representación binaria. La idea clave es codificar un número con 32 bits, y si cabe en 32 bits, el circuito se ejecuta normalmente. Por el contrario, si el número no cabe en 32 bits, entonces las restricciones no se pueden satisfacer. Por lo tanto, el circuito a continuación garantiza que in es $2^{32}-1$ o menos.

include "circomlib/comparators.circom";

// 8 bit range check
template RangeCheck() {
  signal input in;
  component n2b = Num2Bits(32);
  n2b.in <== in;
}

component main = RangeCheck();

// if in = 2**32 - 1, it will accept
// if in = 2**32 it will reject

No es necesario restringir las salidas de Num2Bits como con LessThan, porque internamente, ya restringe out para que sea cero o uno, y también restringe la representación binaria para que sea igual a la entrada (a través de lc1 === in) como se puede ver en el template Num2Bits a continuación:

template Num2Bits(n) {
    signal input in;
    signal output out[n];
    var lc1=0;

    var e2=1;
    for (var i = 0; i<n; i++) {
        out[i] <-- (in >> i) & 1;
        out[i] * (out[i] -1 ) === 0; // CONSTRAINT HAPPENS HERE
        lc1 += out[i] * e2;
        e2 = e2+e2;
    }

    lc1 === in;
}

Suma de 32 bits

Supongamos que queremos sumar dos elementos de campo x e y, que representan números de 32 bits.

La implementación ingenua de la suma de 32 bits es convertir el elemento de campo a 32 bits, y luego construir un “circuito de suma” que sume cada bit y arrastre el desbordamiento (carry the overflow). Sin embargo, esto crea un circuito más grande de lo necesario.

En su lugar, podemos hacer lo siguiente:

Comprobar el rango (range check) de x e y utilizando la estrategia descrita anteriormente.
Sumar x e y como elementos de campo, es decir, z <== x + y.
Convertir z en un número de 33 bits.
Convertir los 32 bits menos significativos del número de 33 bits en un elemento de campo.

Esto se puede visualizar de la siguiente manera:

Lo máximo que x + y puede desbordar es a un número de 33 bits. Considere que el valor máximo que x e y pueden contener es $2^{32}-1$ . Si sumamos ese valor a sí mismo, obtenemos

\begin{align*} &(2^{32}-1)+(2^{32}-1)\\ &=2\cdot(2^{32}-1)\\ &=2^{33}-2 \end{align*}

El número final necesita 33 bits para ser almacenado. (Recuerde que el número máximo que 33 bits pueden contener es $2^{33} - 1$ . Por lo tanto, el número anterior es el segundo número más grande que 33 bits pueden contener.) Por lo tanto, solo necesitamos 33 bits para almacenar la suma antes de eliminar el bit 33.

A continuación se muestra el código para emular y verificar la suma de 32 bits utilizando Circom:

include "circomlib/comparators.circom";
include "circomlib/bitify.circom";

template Add32(n) {
  signal input x;
  signal input y;
  signal output out;

  // range check x and y
  component rCheckX = Num2Bits(32);
  component rCheckY = Num2Bits(32);
  rCheckX.in <== x;
  rCheckY.in <== y;
  
  // convert the sum to 33 bits
  component n2b33 = Num2Bits(33);
  n2b33.in <== x + y;

  // convert the least significant 32 bits
  // to the final result
  component b2n = Bits2Num(32);
  for (var i = 0; i < 32; i++) {
    b2n.in[i] <== n2b33.out[i];
  }

  b2n.out ==> out;
}

Multiplicación de 32 bits

La lógica para la multiplicación de 32 bits es extremadamente similar a la suma de 32 bits, excepto que necesitamos permitir que la multiplicación de 32 bits requiera temporalmente hasta 64 bits antes de guardar solo los 32 bits finales:

\begin{align*} &=(2^{32}-1)(2^{32}-1)\\ &=2^{64}-2^{32}-2^{32}+2\\ &=2^{64}-2^{33}+2 \end{align*}

El número final necesita 64 bits para ser almacenado.

La implementación de este circuito se deja como ejercicio para el lector.

División y módulo de 32 bits

La división de enteros es uno de los errores (bugs) más problemáticos en ZK, ya que restringirla adecuadamente es mucho más difícil que en los ejemplos de suma y multiplicación. Aquí hay algunos ejemplos en la vida real de divisiones con restricciones insuficientes (underconstrained):

En la división de enteros, la relación entre el numerador, denominador, cociente y resto (remainder) es:

\text{numerator}=\text{denominator}\times\text{quotient}+\text{remainder}

Sin embargo, esa restricción por sí sola no es suficiente para garantizar que la división se haya realizado correctamente.

Por ejemplo, supongamos que estamos intentando probar que calculamos 12 / 7 = 1. Nuestro circuito tendría los valores

12 = 7 \times 1 +5

Sin embargo, el siguiente witness también satisface la restricción:

12 = 7 \times 0 + 12

Podemos protegernos contra esto añadiendo una restricción de que el resto (remainder) sea estrictamente menor que el denominador.

Además, debemos ser conscientes de los siguientes posibles bugs:

Esto no es una preocupación para 32 bits en un campo de 254 bits (que es el predeterminado que usa Circom), pero queremos estar seguros de que el cálculo $\text{denominator}\times\text{quotient}$ no puede desbordar el campo finito subyacente.
De manera más general, no queremos que el cálculo $\text{denominator}\times\text{quotient}+\text{remainder}$ se desborde. Si a denominator y quotient se les comprueba el rango a 32 bits, entonces la mayor cantidad de bits que el producto $\text{denominator}\times\text{quotient}$ puede contener es 64 bits, y si a remainder se le comprueba el rango a 32 bits, la mayor cantidad de bits que $\text{denominator}\times\text{quotient}+\text{remainder}$ puede requerir es 65 bits. Por lo tanto, trabajar con un tamaño de bits de VM de 32 bits no es una preocupación para el campo predeterminado de Circom, pero para otros tamaños de bits de VM, como 128 bits, un desbordamiento es posible.
La división por cero puede tener un comportamiento inesperado dependiendo de qué ZKVM se esté considerando. La EVM, por ejemplo, no entra en pánico (panic) cuando ocurre una división por cero, sino que devuelve cero. En la arquitectura RISC-V, la división por cero devuelve una palabra con todos los bits establecidos en 1.

Es poco práctico calcular directamente la división de enteros utilizando solo la suma y la multiplicación (los algoritmos eficientes como el método de Karatsuba para la multiplicación o la división eficiente de enteros utilizan bucles for o recursividad, que no se adaptan bien a la suma y la multiplicación), por lo que es mejor calcular el resultado de la división de enteros fuera de las restricciones.

En Circom, el operador / se refiere a la división modular (multiplicación por el inverso multiplicativo) y el operador \ se refiere a la división de enteros. El siguiente código muestra cómo probar que calculamos el cociente y el resto correctamente. Incluimos el cálculo del resto (remainder) ya que lo obtenemos gratis al probar que calculamos la división de enteros correctamente.

include "circomlib/comparators.circom";
include "circomlib/bitify.circom";

template DivMod(wordSize) {
  // a wordSize over this could overflow 252
  assert(wordSize < 125);

  signal input numerator;
  signal input denominator;

  signal output quotient;
  signal output remainder;

  quotient <-- numerator \ denominator;
  remainder <-- numerator % denominator;
  
  // quotient and remainder still need
  // to be range checked because the
  // prover can supply any value
  
  // range check all the signals
  component n2bN = Num2Bits(wordSize);
  component n2bD = Num2Bits(wordSize);
  component n2bQ = Num2Bits(wordSize);
  component n2bR = Num2Bits(wordSize);
  n2bN.in <== numerator;
  n2bD.in <== denominator;
  n2bQ.in <== quotient;
  n2bR.in <== remainder;

  // core constraint
  numerator === quotient * denominator  + remainder;

  // remainder must be less than the denominator
  signal remLtDen;
  
  // depending on the application, we might be able
  // to use fewer than 252 bits
  remLtDen <== LessThan(wordSize)([remainder, denominator]);
  remLtDen === 1;

  // denominator is not zero
  signal isZero;
  isZero <== IsZero()(denominator);
  isZero === 0;
}

component main = DivMod(32);

Desplazamiento de bits (Bitshift) de 32 bits

Supongamos que deseamos emular el siguiente código:

uint32 x;
uint32 s;
x << s;

Un desplazamiento a la izquierda por s es equivalente a multiplicar por $2^s$ donde $s$ es el tamaño del desplazamiento, y un desplazamiento a la derecha por s es equivalente a la división por $2^s$ . Como se vio en el capítulo anterior, el cálculo de potencias puede crear un conjunto bastante grande de restricciones. Por lo tanto, generalmente es más eficiente precalcular cada potencia de 2 hasta el tamaño de la palabra menos 1. Así, para un desplazamiento a la izquierda de un número de 32 bits, precalculamos cada potencia de 2 hasta 31 (tamaño de la palabra (32) - 1): 1, 2, 4, 8, …, $2^{31}$ y multiplicamos x por la selección adecuada utilizando las técnicas de selección condicional discutidas anteriormente. Si la cantidad de desplazamiento es 32 o mayor, multiplicamos por cero.

La implementación se deja como ejercicio para el lector.

AND, NOT, OR, XOR y NOT de 32 bits

La biblioteca de puertas (gates) de Circomlib tiene implementaciones para cada uno de estos circuitos y se explican por sí mismos, por lo que animamos al lector a que simplemente lea el código allí. A continuación mostramos las plantillas (templates) sobre cómo emular la operación para lo siguiente:

AND a nivel de bits (Bitwise AND)

uint32 a;
uint32 b;
a & b;

NOT a nivel de bits (Bitwise NOT)

uint32 x;
~x; // flip all the bits

A continuación se muestra el código para calcular y restringir el AND a nivel de bits de a y b.

include "circomlib/gates.circom";
include "circomlib/bitify.circom";

template BitwiseAnd32() {
  signal input a;
  signal input b;
  signal output out;

  // range check
  component n2ba = Num2Bits(32);
  component n2bb = Num2Bits(32);
  n2ba.in <== a;
  n2bb.in <== b;

  component b2n = Bits2Num(32);
  component Ands[32];
  for (var i = 0; i < 32; i++) {
    Ands[i] = AND();
    Ands[i].a <== n2ba.out[i];
    Ands[i].b <== n2bb.out[i];
    Ands[i].out ==> b2n.in[i];
  }

  b2n.out ==> out;
}

component main = BitwiseAnd32();

Las operaciones restantes para NOT, OR y XOR se dejan como ejercicio para el lector.

Cómo manejan las ZK EVM los números de 256 bits

El campo predeterminado de Circom no puede contener números de 256 bits. En su lugar, cada palabra en la EVM debe ser modelada con una lista de tamaños de palabra más pequeños, similar a cómo una computadora de 64 bits puede emular la EVM.

Por ejemplo, un número de 256 bits se puede modelar con cuatro palabras de 64 bits. Al sumar, llevamos el desbordamiento (overflow) de las palabras menos significativas a la siguiente palabra significativa. Si la palabra más significativa se desborda, simplemente descartamos el desbordamiento.

Apéndice A: Pruebas de Equivalencia

Usamos el probador (prover) Certora para demostrar la equivalencia de las siguientes funciones:

contract DemoMod32 {
    function mod32(uint256 x) public pure returns (uint256) {
        return x % (2**32);
    }

    function mod32e(uint256 x) public pure returns (uint256) {
        // only keep the 32 least significant bits
        return uint256(uint32(x)); 
    }
}

Aquí está la regla del lenguaje de verificación de Certora:

methods {
  function mod32(uint256) external returns (uint256) envfree;
  function mod32e(uint256) external returns (uint256) envfree;
}

rule test_Mod32AndMod32E_Equivalence() {
  uint256 x;
  assert mod32(x) == mod32e(x);
}

Aquí está el informe de Certora:

https://prover.certora.com/output/541734/6cd3303cb5f5441e8773adb5c79787d7?anonymousKey=0b945ee1440cd67efed3efba3162b0f924e8cf8f