“Compute then constrain” (calcular y luego restringir) es un patrón de diseño en circuitos ZK donde la salida correcta de un algoritmo se calcula primero sin restricciones. La exactitud de la solución se verifica luego haciendo cumplir las invariantes relacionadas con el algoritmo.
Motivación para calcular y luego restringir
Si uno estuviera limitado a usar solo suma, multiplicación y asignar-luego-restringir (==>), entonces muchos cálculos serían extremadamente difíciles de modelar y requerirían un número extremadamente grande de sumas y multiplicaciones.
Por ejemplo, calcular la raíz cuadrada de un número requiere varias estimaciones iterativas. Esto haría que el tamaño del circuito fuera considerablemente mayor.
Por lo tanto, a menudo es más práctico ejecutar el cálculo fuera del circuito — es decir, no generar ninguna restricción mientras se calcula la respuesta — y luego configurar restricciones que se satisfacen si y solo si la respuesta calculada es correcta.
Mostraremos muchos ejemplos de las bibliotecas Bitify y Comparator en Circomlib, las cuales usan este patrón de manera intensiva.
El operador de “flecha delgada” <-- en Circom y cómo difiere de <==
El operador <== asigna un valor a una señal y crea una restricción. Debido a que las restricciones deben ser cuadráticas, no podemos llevar a cabo operaciones como la siguiente:
template InputEqualsZero() {
signal input in;
signal output out;
// out = 1 if in == 0
out <== in == 0 ? 1 : 0;
}
component main = InputEqualsZero();
Compilar el circuito anterior resultará en un error de restricciones no cuadráticas, ya que el operador ternario no puede expresarse directamente como una sola multiplicación entre señales. De hecho, Circom rechaza directamente cualquier operación sobre señales que no sea multiplicación o suma.
Al principio, puede parecer que Circom no puede calcular out por nosotros y requiere que se proporcione como una entrada pública en su lugar. Sin embargo, esto sería muy inconveniente si hubiera muchas señales involucradas.
Necesitamos un mecanismo para decirle a Circom “calcula y asigna el valor para esta señal en función de otras señales, pero no crees una restricción”. La sintaxis para esa operación es el operador <--:
template InputEqualsZero() {
signal input in;
signal output out;
// out = 1 if in == 0
out <-- in == 0 ? 1 : 0;
}
component main = InputEqualsZero();
La operación in == 0 ? 1 : 0; a veces se denomina “cálculo fuera del circuito” (out-of-circuit computation) o una “pista” (hint).
El código anterior compilará, pero no se han aplicado restricciones a out ni a in.
El operador <-- es muy conveniente porque nos permite calcular valores sin generar restricciones, lo que elimina la necesidad de suministrar manualmente ciertos valores de señales. Sin embargo, también ha sido una fuente de errores de seguridad.
Circom no obliga a los desarrolladores a crear las restricciones apropiadas después de usar <-- y esto ha sido una fuente común de vulnerabilidades críticas y altas en Circom. Incluso si el desarrollador no añade restricciones, creando así un código muy peligroso, el compilador ni siquiera emitirá una advertencia o un aviso. Las señales sin restricciones pueden tomar cualquier valor, permitiendo así que el circuito produzca pruebas ZK para afirmaciones sin sentido.
Enseñaremos en un tutorial posterior, explotación de circuitos subrestringidos, cómo explotar el código de Circom que hace un mal uso del operador <--. Por ahora, piensa en ello como una operación que nos ahorra la molestia de suministrar un determinado valor de señal nosotros mismos, aunque sigue requiriendo que restrinjamos esa señal más adelante.
El cálculo y la restricción se entienden mejor con ejemplos, los cuales se proporcionan en el resto de este capítulo.
Ejemplo 1: Raíz Cuadrada Modular
Una raíz cuadrada modular de un número es un número tal que . Sin embargo, no todos los elementos del campo tienen una raíz cuadrada modular. La restricción que modela el cálculo correcto de una raíz cuadrada es sencilla (aunque calcular la raíz cuadrada no lo es).
Considera el siguiente código, que prueba que out es la raíz cuadrada modular de in:
function sqrt(n) {
// do some magic (see the next code block)
return r;
}
template ValidSqrt() {
signal input in;
signal output out; // sqrt(in)
out <-- sqrt(in);
out * out === in; // ensure sqrt was correct
// the `*` is implicity done modulo p
}
Aquí, out <-- sqrt(in) asigna la raíz cuadrada a out sin añadir restricciones.
El archivo pointbits en Circomlib proporciona la función para calcular la raíz cuadrada modular. Ten en cuenta que las funciones deben declararse fuera de un template de Circom. Una “función” en Circom es simplemente una conveniencia para agrupar código relacionado en un bloque contenido.
function sqrt(n) {
if (n == 0) {
return 0;
}
// Test that have solution
var res = n ** ((-1) >> 1);
// if (res!=1) assert(false, "SQRT does not exists");
if (res!=1) return 0;
var m = 28;
var c = 19103219067921713944291392827692070036145651957329286315305642004821462161904;
var t = n ** 81540058820840996586704275553141814055101440848469862132140264610111;
var r = n ** ((81540058820840996586704275553141814055101440848469862132140264610111+1)>>1);
var sq;
var i;
var b;
var j;
while ((r != 0)&&(t != 1)) {
sq = t*t;
i = 1;
while (sq!=1) {
i++;
sq = sq*sq;
}
// b = c ^ m-i-1
b = c;
for (j=0; j< m-i-1; j ++) b = b*b;
m = i;
c = b*b;
t = t*c;
r = r*b;
}
if (r < 0 ) {
r = -r;
}
return r;
}
Las raíces cuadradas modulares tienen dos soluciones: la raíz cuadrada en sí y su inverso aditivo. Por lo tanto, podemos generar ambas soluciones de la siguiente manera:
template ValidSqrt() {
signal input in;
signal output out1; // sqrt(in)
signal output out2; // -sqrt(in)
out1 <-- sqrt(in);
out2 <-- out1 * -1; // Computation Step (Unconstrained)
out1 * out1 === in; // Verification Step (Constraint-Based):
out2 * out2 === in; // Verification Step
}
ADVERTENCIA: El código presentado aquí está codificado de forma rígida (hardcoded) para el tamaño de campo predeterminado de Circom. Si configuras Circom para usar algún otro campo, ¡podría producir una respuesta incorrecta!
El ejemplo anterior demuestra que calcular la raíz cuadrada es mucho más simple cuando las restricciones no son una preocupación; si intentáramos calcular la raíz cuadrada usando solo multiplicaciones y sumas, el circuito sería irrazonablemente grande. La exactitud del resultado se puede asegurar posteriormente mediante restricciones.
Esto ilustra cómo Circom puede ser tanto un lenguaje de programación tradicional como un DSL para la generación de restricciones. La porción de código de la función sqrt(n) es programación tradicional, pero la restricción in === out * out genera la restricción.
Ejemplo 2: Sudoku
Si un cálculo es demasiado difícil o computacionalmente costoso de modelar mediante restricciones — es decir, si requiere muchas puertas y señales intermedias — simplemente se puede proporcionar como una entrada y asumir que el probador obtuvo la respuesta por otros medios.
Para resolver realmente un rompecabezas de Sudoku, se debe ejecutar un algoritmo de búsqueda de posibles soluciones, probablemente utilizando una búsqueda en profundidad. Sin embargo, no necesitamos probar directamente que ejecutamos un algoritmo de búsqueda; producir una solución válida es suficiente para probar que lo ejecutamos. Debido a que ya existen numerosos tutoriales de Sudoku para Circom en internet, no producimos un ejemplo aquí.
Ejemplo 3: Inverso Modular
Supongamos que queremos calcular el inverso multiplicativo de la señal in, es decir, encontrar una señal out tal que out * in === 1.
Una forma de calcular inversos multiplicativos es usar el Pequeño Teorema de Fermat:
Sin embargo, usar un exponente tan grande (el valor predeterminado de Circom es ) resultará en muchas multiplicaciones y en un circuito muy grande. En su lugar, sería mejor calcular el inverso multiplicativo fuera del circuito y luego probar que tenemos el inverso multiplicativo correcto. Por ejemplo:
template MulInv() {
signal input in;
signal output out;
// Fermat's little theorem
// compute:
// note that -2 = p - 2 mod p
var inv = in ** (-2);
out <-- inv;
// then constrain
out * in === 1;
}
component main = MulInv();
Aquí, solo tenemos una restricción: out * in === 1, por lo que esto es muy eficiente.
División modular en Circom
Circom interpreta el operador / como una división modular, por lo que el inverso de un valor n puede calcularse como:
inv <-- 1 / n;
El template anterior podría escribirse un poco más limpio de la siguiente manera:
template MulInv() {
signal input in;
signal output out;
// compute
out <-- 1 / in;
// then constrain
out * in === 1;
}
component main = MulInv();
La división modular es una operación no cuadrática, por lo que debe usarse solo con variables o con la asignación de flecha delgada — es decir, necesita ser calculada fuera del circuito.
Ejemplo 4: IsZero
Motivación
El circuito IsZero es muy útil para componerse en cálculos más grandes. Supongamos, por ejemplo, que queremos probar que x es menor que 16 o que x es igual a 42.
El siguiente conjunto de restricciones no funcionará:
// equal 42
x === 42
// less than 16
x === b_0 + 2*b_1 + 4*b_2 + 8*b_3
0 === b_0 * (b_0 - 1)
0 === b_1 * (b_1 - 1)
0 === b_2 * (b_2 - 1)
0 === b_3 * (b_3 - 1)
Si x es 42, violará las restricciones inferiores, y si es menor que 16, violará x === 42.
Por lo tanto, lo que realmente queremos son subcircuitos que indiquen que se cumple una determinada condición (es decir, que x sea igual a 42 o menor que 16) sin imponer que esa condición se cumpla. Luego podemos aplicar restricciones sobre estos indicadores. Por ejemplo, supongamos que tenemos los indicadores x_eq_42 y x_lt_16. Podemos restringir que al menos uno de ellos sea verdadero con lo siguiente:
// at least one of the two signals is not zero
x_eq_42 * x_lt_16 === 1;
Para crear un indicador de que x es igual a 42, queremos saber si el valor x - 42 es precisamente cero o no.
Diseñando un circuito para indicar que un valor es cero
Aquí, diseñamos un circuito que devuelve 1 si la entrada es 0 y 0 en caso contrario (Para los curiosos, el nombre de esta función es la función Delta de Kronecker).
Si escribiéramos tal función usando puramente suma y multiplicación, nuestra función sería un polinomio, lo cual está limitado en la cantidad de lugares donde puede ser 0. En otras palabras, si quisiéramos que nuestra función fuera cero en todas partes de nuestro campo finito, entonces nuestro polinomio tendría un grado casi tan grande como el orden del campo finito, lo cual es poco práctico.
En su lugar, diseñamos un conjunto de restricciones donde in y out tienen las siguientes propiedades:
| in | out | restricción |
|---|---|---|
| 0 | 0 | violada |
| 0 | 1 | aceptada |
| no 0 | 0 | aceptada |
| no 0 | 1 | violada |
Necesitamos un conjunto de restricciones que requieran que out sea 1 si in es 0, y que out sea 0 si in no es cero. Otra forma de pensar en esta relación es “al menos uno de in u out debe ser no cero, pero no pueden ser ambos cero ni ambos no cero”.
Decir que al menos uno de in u out debe ser cero puede modelarse con la restricción in * out === 0.
En la tabla a continuación, podemos ver que in * out === 0 acepta la situación “exactamente uno entre in y out es cero”, y rechaza correctamente la situación donde tanto in como out no son cero:
| in | out | restricción | in * out === 0 |
|---|---|---|---|
| 0 | 0 | violada | acepta |
| 0 | 1 | aceptada | acepta |
| no 0 | 0 | acepta | acepta |
| no 0 | 1 | violada | viola |
El problema con la restricción in * out === 0 es que no previene el caso donde in y out son ambos 0 (como se marca en la tabla anterior).
La propiedad faltante que estamos intentando capturar es que in y out no pueden ser cero simultáneamente.
Ingenuamente, podríamos lograr esto con in + out === 1. Esto significaría que si in es 1, entonces out debe ser 0 y viceversa. Sin embargo, las especificaciones dicen que in podría ser cualquier valor distinto de cero, por ejemplo, 100, y 100 + out no puede ser 1.
Sin embargo, si podemos “convertir el 100 en un 1”, entonces podemos hacer que la restricción funcione. Esto se puede lograr calculando el inverso multiplicativo de in fuera del circuito y aplicando posteriormente la restricción in * inv + out === 1. Si in es cero, entonces hacemos que inv sea cero porque cero no tiene un inverso multiplicativo. Ahora tenemos las siguientes restricciones:
in * inv + out === 1;
in * out === 0;
Ten en cuenta que inv no está restringido en sí mismo, pero esto no tiene consecuencias en este caso.
La primera restricción, in * inv + out === 1;, solo sirve para el propósito de no permitir que tanto in como out sean cero. Si tanto in como out son cero, entonces la restricción será violada independientemente del valor de inv.
Para resumir los cálculos realizados fuera del circuito:
- Si
ines cero o no. - El inverso multiplicativo de
in.
El componente IsZero en Circomlib cumple con las restricciones descritas en esta sección:
template IsZero() {
signal input in;
signal output out;
signal inv;
inv <-- in!=0 ? 1/in : 0;
out <== -in*inv +1;
in*out === 0;
}
Primero calcula inv fuera del circuito, luego restringe que out sea 1 si in es cero y asigna 0 a out en caso contrario.
Entradas no deterministas
Los valores calculados fuera del circuito que nos permiten usar restricciones más concisas se llaman “entradas de consejo” (advice inputs) o “entradas no deterministas” (non-deterministic inputs). La señal inv en el circuito anterior es un ejemplo de una entrada de consejo o entrada no determinista.
Ejemplo 5: IsEqual
El componente IsEqual en Circomlib está estrechamente relacionado con IsZero — comprueba si la diferencia entre las entradas es cero (de ser así, entonces deben ser iguales entre sí):
template IsEqual() {
signal input in[2];
signal output out;
component isz = IsZero();
in[1] - in[0] ==> isz.in;
isz.out ==> out;
}
Ejemplo 6: Num2Bits
El template Num2Bits en Circomlib descompone una señal en n bits según lo especificado por el parámetro del template:
template Num2Bits(n) {
signal input in; // number
signal output out[n]; // binary output
var lc1=0;
var e2=1;
for (var i = 0; i<n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0;
lc1 += out[i] * e2;
e2 = e2+e2;
}
lc1 === in;
}
Ten en cuenta que para n en el código anterior, si es mayor que el campo finito, podemos tener un error de alias (alias bug). Esto se explica con más detalle en ese capítulo.
Esencialmente, el código itera a través de cada bit en la representación binaria, comenzando desde el bit menos significativo. En cada iteración del bucle, almacenamos el valor [1,2,4,8,…,2^i] en una variable e2, que es el valor que representa ese bit. Si ese bit es 1 (out[i] <-- (in >> i) & 1;), sumamos ese valor al acumulador lc1. En cada iteración del bucle, restringimos que el bit leído sea realmente 0 o 1 (con out[i] * (out[i] -1 ) === 0;). Al final, restringimos que el valor binario calculado coincida con el valor original (lc1 === in;).
La forma en que calcula el array binario se muestra mejor con una animación, la cual mostramos aquí:
Comparable a los ejemplos anteriores, el cálculo del valor binario se realiza fuera del circuito, pero luego restringimos para asegurar que el array binario sea correcto.
El template Num2Bits es un componente central en el template LessThan y otros templates para comparar el valor relativo de las señales.
Los elementos del campo (números en un campo finito) no pueden compararse directamente entre sí — primero necesitan ser convertidos a números binarios.
Para entender cómo comparar eficientemente el tamaño de los números binarios en un circuito, por favor revisa la sección relevante en nuestro capítulo sobre Circuitos Aritméticos y luego compara la discusión allí con el template LessThan en Circomlib.
Ejemplo 7: IsMax
Para probar que un elemento es el máximo en una lista, debemos demostrar que 1) es mayor o igual a cada elemento y 2) que también está presente en la lista. Para entender el segundo requisito, considera que 100 no es el máximo de la lista [4,5,6] aunque 100 sea mayor o igual a todos los elementos en la lista.
El siguiente circuito calcula el máximo fuera del circuito usando un bucle for tradicional, luego usa el componente GreaterEqThan para asegurar que out es mayor o igual a todos los demás elementos de la lista.
Para asegurar que out sea igual a al menos uno de los elementos de la lista, suma una comparación IsEqual con todas las demás señales. Si la suma es cero, entonces sabemos que out no está en la lista. Por lo tanto, restringimos que esa suma no sea cero:
template IsMax() {
signal input in[3];
signal output out;
// compute the max as usual
var maxx = in[0];
for (var i = 1; i < 3; i++) {
if (in[i] > maxx) {
maxx = in[i];
}
}
// propose the max, but do not constrained it yet
out <-- maxx;
// max must be ≥ every other element
signal gte0;
signal gte1;
signal gte2;
// gte0 <== GreaterEqThan(252)([out, in[0]]);
// is shorthand for
// component gte0 = GreaterEqThan(252);
// gte0[0] <== out;
// gte0[1] <== in[0];
// 252 is to ensure we don't have enough
// bits to encode numbers larger than what
// fits in the default finite field, which
// would lead to aliasing issues
gte0 <== GreaterEqThan(252)([out, in[0]]);
gte1 <== GreaterEqThan(252)([out, in[1]]);
gte2 <== GreaterEqThan(252)([out, in[2]]);
gte0 === 1;
gte1 === 1;
gte2 === 1;
// max must be equal to at least one element
signal eq0;
signal eq1;
signal eq2;
eq0 <== IsEqual()([out, in[0]]);
eq1 <== IsEqual()([out, in[1]]);
eq2 <== IsEqual()([out, in[2]]);
signal iz;
iz <== IsZero()(eq0 + eq1 + eq2);
// if IsZero is 1, we have a violation
iz === 0;
}
En su forma actual, nuestro circuito está codificado de forma rígida (hardcoded) para soportar solo un array de longitud 3. Sin embargo, sería bueno poder tener un template para una entrada de longitud arbitraria. Este es el tema de un próximo capítulo.
Problemas de práctica
Escribe una función en Circom que encuentre la raíz de un polinomio de grado 2 usando la fórmula cuadrática. Recuerda, todo se hace sobre un campo finito, así que necesitas usar la raíz cuadrada modular del primer ejemplo.
Luego, escribe las restricciones para que las dos raíces (si existen) satisfagan el polinomio. Pasa el polinomio al template de Circom como un array de tres coeficientes.