Este tutorial presenta el lenguaje Circom y cómo usarlo, junto con los errores comunes. También explicaremos una parte importante de la biblioteca circomlib para introducir patrones de diseño comunes.
Una nota sobre su uso en producción
Circom es una herramienta fantástica para aprender ZK-SNARKS. Sin embargo, debido a que es de bastante bajo nivel, existen más oportunidades de agregar accidentalmente errores sutiles. En aplicaciones reales, los programadores deberían considerar el uso de lenguajes de programación de conocimiento cero de alto nivel. Siempre debes obtener una auditoría antes de implementar un contrato inteligente que contenga fondos de los usuarios, pero esto es especialmente cierto para los circuitos ZK, ya que los vectores de ataque son menos conocidos.
Requisitos previos
Aunque es posible programar en Circom sin entender qué es un Rank 1 Constraint System, te resultará mucho más fácil desarrollar un modelo mental del lenguaje si lo haces. Circom es esencialmente una interfaz ergonómica para crear Rank 1 Constraint Systems.
Instalación
Sigue los pasos aquí para instalar circom
También necesitarás instalar snarkjs
npm install -g snarkjs@latest
Hola Mundo
El hola mundo de los circuitos ZK es realizar una multiplicación, así que comencemos con eso.
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal output out;
out <== a * b;
}
component main = Multiply();
Guarda el código anterior como multiply.circom y en la terminal ejecuta
circom multiply.circom
template instances: 1
Everything went okay, circom safe
para asegurarte de que compile.
Generación de un archivo R1CS
Para convertir el circuito a un R1CS, ejecuta el siguiente comando en la terminal:
circom multiply.circom --r1cs --sym
El indicador --r1cs le dice a circom que genere un archivo R1CS y el indicador --sym significa “guardar los nombres de las variables”. Esto quedará claro en breve.
Se crean dos archivos nuevos:
multiply.r1cs
multiply.sym
Si abres multiply.r1cs, verás un montón de datos binarios, pero dentro del archivo .sym, verás los nombres de las variables.
Para leer el archivo R1CS, usamos snarkjs de la siguiente manera:
snarkjs r1cs print multiply.r1cs
y obtendremos la siguiente salida:
[INFO] snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.a ] * [ main.b ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out ] = 0
Recuerda que todo se hace en un campo finito cuando se trata de circuitos aritméticos, por lo que el número masivo que ves es esencialmente -1. La ecuación R1CS es equivalente a
-1 * a * b - (-1*out) = 0;
Con un poco de álgebra, podemos ver que esto es equivalente a a * b = out, que es nuestro circuito original.
Los pasos algebraicos son los siguientes:
-1 * a * b - (-1*out) = 0;
-1 * a * b = -1*out;
a * b = out;
¡No se permiten restricciones no cuadráticas!
Un R1CS válido debe tener exactamente una multiplicación por restricción (una restricción es una fila en R1CS, y <== o === en Circom). Si intentamos hacer dos (o más) multiplicaciones, esto fallará. Todas las restricciones con más de una multiplicación deben dividirse en dos restricciones. Considera el siguiente ejemplo (que no compila):
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal input c;
signal output out;
out <== a * b * c;
}
component main = Multiply();
Cuando ejecutamos circom multiply.circom obtendremos el siguiente error:
error[T3001]: Non quadratic constraints are not allowed!
┌─ "multiply.circom":9:3
│
9 │ out <== a * b * c;
│ ^^^^^^^^^^^^^^^^^ found here
│
= call trace:
->Multiply
previous errors were found
Una restricción en Circom se representa mediante el operador <==. Para esta restricción en particular, tenemos dos multiplicaciones para una sola restricción. Para resolver esto, necesitamos crear una restricción separada para que cada restricción tenga solo una multiplicación.
Desglose de restricciones no cuadráticas
Solucionar el problema anterior es sencillo. Introducimos una señal intermedia s1 e indicamos que restrinja la primera multiplicación, luego combinamos la salida de s1 con la tercera entrada. Ahora tenemos dos restricciones y dos multiplicaciones, tal como lo espera Circom.
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal input c;
signal s1;
signal output out;
s1 <== a * b;
out <== s1 * c;
}
component main = Multiply();
Cuando regeneramos e imprimimos el R1CS, obtenemos lo siguiente:
[INFO] snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.s1 ] * [ main.c ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out ] = 0
Con un poco de álgebra, esto se traduce en:
a * b = s1
s1 * c = out
Y podemos ver que esto codifica el mismo cálculo de nuestro circuito.
Calculando el witness
Ejecuta el siguiente comando para crear el código que generará el vector witness:
circom multiply.circom --r1cs --sym --wasm
Esto regenerará el archivo R1CS y el de símbolos, pero también creará una carpeta llamada multiply_js/. Usa cd para entrar a esa carpeta.
A continuación, necesitamos crear un archivo input.json en esa carpeta. Este es un mapa desde los nombres de las señales designadas como entrada hacia el valor que el probador (prover) les suministrará. Vamos a configurar nuestro input.json para que tenga los siguientes valores:
{"a": "2","b": "3","c": "5"}
Si no hubiéramos creado el archivo .sym anteriormente, no sería posible para Circom saber a qué señales de entrada estábamos intentando mapear. Debido a que s1 y out no son señales de entrada, no creamos pares clave-valor para ellas. Aquí, a, b y c corresponden a los nombres de las señales de entrada.
signal input a;
signal input b;
signal input c;
Ahora calculamos y exportamos el witness con el siguiente comando:
node generate_witness.js multiply.wasm input.json witness.wtns
snarkjs wtns export json witness.wtns
cat witness.json
[
"1",
"30",
"2",
"3",
"5",
"6"
]
El witness calculado tiene los valores [1, 30, 2, 3, 5, 6]. 2, 3 y 5 son las entradas, y 6 es la señal intermedia s1, que es el producto de 2 y 3.
Esto sigue la disposición esperada de las variables R1CS en la forma [1, out, a, b, c, s1].
Entradas públicas
¿Qué pasa si queremos hacer públicas algunas de las entradas? En los esquemas nullifier (nullifier schemes), por ejemplo, aplicamos hash a la concatenación de dos números y revelamos uno de ellos más adelante.
Motivación: esquemas nullifier
Como un breve paréntesis, un esquema nullifier funciona concatenando dos números y luego aplicándoles un hash. Se utilizan en el contexto donde tenemos un conjunto de hashes y queremos demostrar que conocemos la preimagen de uno de ellos sin revelar de cuál se trata.
Si los hashes fueran simplemente el hash de un solo número, revelar ese número revelaría de qué hash conocemos la preimagen. Sin embargo, si no revelamos ninguna información, podríamos repetir la acción de demostrar que conocemos la preimagen de uno de los hashes varias veces. ¡Esto sería muy problemático si esta acción involucrara retirar dinero de un contrato inteligente!
Al revelar uno de los dos números procesados por el hash, no podemos reutilizar la preimagen, pero tampoco revelamos de qué hash conocemos la preimagen, ya que revelar solo uno de los dos números no es suficiente.
Así es como Circom maneja las entradas públicas:
template SomePublic() {
signal input a;
signal input b;
signal input c;
signal v;
signal output out;
v <== a * b;
out <== c * v;
}
component main {public [a, c]} = SomePublic();
En el ejemplo anterior, a y c son entradas públicas, pero b permanece oculta. Nota la palabra clave public cuando se instancia el componente main.
Arrays en Circom
Vamos a crear un componente que calculará n potencias de la entrada.
Sería bastante molesto tener que escribir manualmente signal input n veces, por lo que Circom proporciona un tipo de array de señales para hacer esto. Aquí está el código:
pragma circom 2.1.6;
template Powers(n) {
signal input a;
signal output powers[n];
powers[0] <== a;
for (var i = 1; i < n; i++) {
powers[i] <== powers[i - 1] * a;
}
}
component main = Powers(6);
Con este ejemplo se introducen algunas características sintácticas nuevas: argumentos de template y variables.
Argumentos de Template
En el ejemplo anterior, vemos que el template está parametrizado con n, es decir, Powers(n).
Un Rank 1 Constraint System debe ser fijo e inmutable, lo que significa que no podemos cambiar el número de filas o columnas una vez definidas, y no podemos cambiar los valores de las matrices o del witness. Es por eso que la línea final tiene el argumento codificado de forma rígida (hard-coded) Powers(6); este tamaño debe ser fijo.
Sin embargo, si quisiéramos reutilizar este código más adelante para soportar un circuito de diferente tamaño, sería más ergonómico que el template pudiera cambiar su tamaño sobre la marcha. Por lo tanto, los componentes pueden recibir argumentos para parametrizar flujos de control y estructuras de datos, pero esto debe fijarse por circuito.
Variables en Circom
El ejemplo anterior es equivalente a lo siguiente:
pragma circom 2.1.6;
template Powers() {
signal input a;
signal output powers[6];
powers[0] <== a;
powers[1] <== powers[0] * a;
powers[2] <== powers[1] * a;
powers[3] <== powers[2] * a;
powers[4] <== powers[3] * a;
powers[5] <== powers[4] * a;
}
component main = Powers();
Aunque obtenemos un R1CS idéntico, ese código es feo. Sin embargo, este ejemplo ilustra de manera útil que cualquier circuito que use variables en su cálculo puede reescribirse para no incluir variables.
Las variables construyen código auxiliar que existe fuera del R1CS. Ayudan a definir el circuito, pero no forman parte de él.
La variable var i era simplemente un registro interno para rastrear la iteración del bucle mientras se construía el circuito; no forma parte de las restricciones.
Signal vs variable
Una señal (signal) es inmutable y está destinada a ser una de las columnas del R1CS. Una variable no forma parte del R1CS. Está destinada a calcular valores fuera del R1CS para ayudar a definir el R1CS.
No sería exacto pensar en las señales como “variables inmutables” y en las variables como “variables mutables” de la manera en que algunos lenguajes las asignan. La razón por la que las señales son inmutables es porque las entradas del witness en un R1CS tienen un valor fijo. Un vector de solución en un R1CS que cambie de valor no tiene sentido, ya que no se puede crear una prueba (proof) para él.
Los operadores <--, <== y === se usan con señales, no con variables. Explicaremos los operadores menos familiares en breve.
Al trabajar con variables, Circom se comporta como un lenguaje normal tipo C. Los operadores =, ==, >=, <=, !=, ++ y -- se comportan como cabría esperar. Es por esto que el ejemplo del bucle parece familiar.
Los siguientes ejemplos no están permitidos:
signal a;
a = 2; // using a variable assignment for a signal
var v;
v <-- a + b; // using a signal assignment for a variable is not allowed
=== vs <==
Los siguientes circuitos son equivalentes:
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal output c;
c <-- a * b;
c === a * b;
}
template MultiplySame() {
signal input a;
signal input b;
signal output c;
c <== a * b;
}
El operador <== calcula, luego asigna y después agrega una restricción. Si solo quieres restringir, usa ===.
Por lo general, usarás el operador === cuando intentes forzar que el <-- asigne el valor correcto. Verás esto en acción cuando veamos el template IsZero.
Pero antes de llegar a eso, veamos un ejemplo real. Supongamos que queremos que el probador proporcione tanto las entradas como la salida. Así es como lo haríamos usando el operador ===.
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal input c;
c === a * b;
}
component main {public [c]} = Multiply();
Circom no requiere que exista una señal de salida (output), ya que esto es simplemente azúcar sintáctico para una entrada pública. Recuerda, una “entrada” es simplemente un elemento en el vector witness, por lo que todo es una entrada desde la perspectiva de una prueba de conocimiento cero. En el ejemplo anterior, no hay señal de salida, pero este es un circuito perfectamente válido con las restricciones adecuadas.
Conectando templates entre sí
Los templates de Circom son reutilizables y componibles, como ilustra el siguiente ejemplo. Aquí, Square es un template utilizado por SumOfSquares. Observa cómo las entradas a y b están “conectadas” al componente Square().
pragma circom 2.1.6;
template Square() {
signal input in;
signal output out;
out <== in * in;
}
template SumOfSquares() {
signal input a;
signal input b;
signal output out;
component sq1 = Square();
component sq2 = Square();
// wiring the components together
sq1.in <== a;
sq2.in <== b;
out <== sq1.out + sq2.out;
}
component main = SumOfSquares();
Puedes pensar en el operador <== como una forma de “conectar” los componentes al hacer referencia a sus entradas o salidas.
Múltiples entradas a un componente
El ejemplo Square anterior toma una sola señal como entrada, pero si un componente toma múltiples entradas, lo convencional es especificarlo como un array in[n]. El siguiente componente toma dos números y devuelve su producto:
template Mul {
signal input in[2]; // takes two inputs
signal output out; // single output
out <== in[0] * in[1];
}
Saber cómo conectar templates entre sí es un requisito previo para cuando incorporemos una biblioteca de circuitos, lo cual mostraremos en una próxima sección.
Convenciones de nomenclatura de señales
Es convencional nombrar a las señales de entrada in o como un array in[] y a las señales de output como out o out[].
Potencias inseguras, cuidado con <--
Al encontrarse con el problema de las restricciones cuadráticas, puede ser tentador usar el operador <-- para silenciar al compilador. El siguiente código compila y parece lograr lo mismo que nuestro ejemplo anterior de potencias.
pragma circom 2.1.6;
template Powers {
signal input a;
signal output powers[6];
powers[0] <== a;
powers[1] <== a * a;
powers[2] <-- a ** 3;
powers[3] <-- a ** 4;
powers[4] <-- a ** 5;
powers[5] <-- a ** 6;
}
component main = Powers();
Sin embargo, cuando creamos el R1CS, ¡solo tenemos una restricción!
(base) ➜ hello-circom circom bad-powers.circom --r1cs
template instances: 1
non-linear constraints: 1 ### only one constraint ###
linear constraints: 0
public inputs: 0
public outputs: 6
private inputs: 1
private outputs: 0
wires: 7
labels: 8
Written successfully: ./powers.r1cs
Everything went okay, circom safe
Con solo una restricción, el probador solo tiene que establecer correctamente el primer elemento en el array, ¡pero puede poner el valor que quiera para los otros 5! ¡No puedes confiar en las pruebas que salen de un circuito como este!
Las sub-restricciones (underconstraints) son una fuente importante de errores de seguridad en aplicaciones de conocimiento cero, ¡así que revisa tres veces que las restricciones realmente se generen en el R1CS de la forma que esperas!
Es por esto que enfatizamos en la comprensión de los Rank 1 Constraint Systems antes de aprender el lenguaje Circom; de lo contrario, ¡hay toda una categoría de errores que te resultará difícil detectar!
Puedes aprender en nuestro otro tutorial sobre cómo explotar circuitos ZK sub-restringidos (underconstrained).
Cuándo usar <--
Si el <-- conduce a sub-restricciones, ¿por qué el lenguaje incluiría un arma de doble filo (foot gun) como esta?
Al describir algoritmos utilizando circuitos en lugar de código natural, la mentalidad a adoptar es “calcular, luego restringir”. Algunas operaciones son extremadamente difíciles de modelar únicamente con restricciones puras. Un ejemplo de esto se muestra en la próxima sección.
Circomlib
Iden3 mantiene un repositorio de templates útiles de Circom llamado circomlib. En este punto, tenemos los conocimientos previos suficientes de Circom para comenzar a estudiar estos templates, y ahora es un buen momento para introducir un template simple pero útil que demuestra el uso de <--.
IsZero
El template IsZero devuelve 1 si la señal de entrada es cero, y cero si la señal de entrada no es cero.
Si pasas algún tiempo pensando en cómo comprobar si un número es cero usando solo multiplicaciones, te encontrarás atascado; resultará ser un problema endiabladamente difícil.
Veamos cómo el componente IsZero de circomlib logra esto.
template IsZero() {
signal input in;
signal output out;
signal inv;
inv <-- in!=0 ? 1/in : 0;
out <== -in*inv +1;
in*out === 0;
}
En el ejemplo anterior, inv es una señal de entrada auxiliar para facilitar la creación de un circuito válido. Calculamos que inv sea cero o el inverso de in fuera del R1CS y luego forzamos que inv sea correcto como parte de las restricciones. Esto sigue el patrón de “calcular, luego restringir”.
La señal inv aún está restringida a ser cero o el inverso modular de in.
Como ejercicio para el lector, dibuja una tabla de verdad que muestre las siguientes combinaciones posibles:
out:
inv:
in:
Verás que solo es posible satisfacer las restricciones estableciendo out en 1 cuando in es 0, y out en 0 cuando in no es cero. No puedes hacer trampas con inv, debe seguir las reglas. Esto ilustra el patrón de “calcular, luego restringir”.
La flecha crea una restricción y también asigna un valor. En el código anterior, out está restringido a ser igual a -in*inv + 1. Sin embargo, la línea final no está asignando cero a in*out. En cambio, está imponiendo que in*out sea de hecho igual a cero.
Aunque normalmente usarías el operador ternario (o elementos tipo C en general) con variables, puedes usar la sintaxis de programación tradicional con señales si usas el operador <--.
Ejercicio para el lector: ¿puedes crear un template que haga lo opuesto a IsZero, sin usar el template IsZero?
=== y <== no crearán una restricción si la operación no es cuadrática y el optimizador está activado
Aquí hay una peculiaridad del compilador con la que debes tener cuidado:
template FactorOfFiveFootgun() {
signal input in;
signal output out;
out <== in * 5;
}
component main = FactorOfFiveFootgun();
Aquí estamos diciendo que conocemos x, tal que 5x = out, donde out es pública. Así que si out es 100, esperamos que x sea 20, ¿verdad? Si miramos el R1CS, vemos que de hecho está vacío, ¡no se crea ninguna restricción!
Esto se debe a que, aunque <== es una restricción, el optimizador del compilador elimina las restricciones que no tienen una multiplicación en ellas.
Cuando compilamos el circuito a R1CS, vemos que está vacío.
(base) ➜ hello-circom circom footgun.circom --r1cs
template instances: 1
non-linear constraints: 0 ### no constraints ###
linear constraints: 0
public inputs: 0
public outputs: 1
private inputs: 1
private outputs: 0
wires: 2
labels: 3
Written successfully: ./footgun.r1cs
Everything went okay, circom safe
Sin embargo, si compilamos el circuito con el optimizador desactivado a través de
circom footgun.circom --r1cs --O0
entonces vemos que se crea una restricción:
template instances: 1
non-linear constraints: 0
linear constraints: 1 ### Constraint created here
public inputs: 0
private inputs: 1
public outputs: 1
wires: 3
labels: 3
Written successfully: ./footgun.r1cs
Everything went okay
Siempre haz una comprobación de cordura (sanity check) del número de restricciones que crea el compilador.
Funciones en Circom
Una cosa que hace que Circom sea un poco confuso es que es a la vez un lenguaje para crear restricciones aritméticas, y también un lenguaje para crear restricciones de forma programática, además de un lenguaje para hacer cálculos regulares.
Aquí hay un ejemplo de cómo separar el cálculo en una función. Ten en cuenta que el promedio (“average”) aquí se calcula utilizando aritmética modular, por lo que no corresponderá a la media aritmética tradicional.
pragma circom 2.1.6;
include "node_modules/circomlib/circuits/comparators.circom";
function invert(x) {
return 1 / x;
}
template Average(n) {
signal input in[n];
signal denominator;
signal output out;
var sum;
for (var i = 0; i < n; i++) {
sum += in[i];
}
denominator <-- invert(n);
component eq = IsEqual();
eq.in[0] <== denominator;
eq.in[1] <== n;
0 === eq.out;
out <== sum * denominator;
}
component main = Average(5);
Existen restricciones que dependen del valor de la condición y este puede ser desconocido durante la fase de generación de restricciones
Aquí hay otro error fácil de cometer al escribir código en circom: la señal no puede ser una entrada para una declaración if o un bucle.
template IsOver21() {
signal input age;
signal output oldEnough;
if (age >= 21) {
oldEnough <== 1;
} else {
oldEnough <== 0;
}
}
Si intentas compilar el código anterior, obtendrás el error que aparece en el encabezado de esta sección. Obtendrás un error similar si usas una señal para determinar el número de veces que se debe ejecutar un bucle (¡inténtalo!). La razón por la que esto no está permitido es porque estaríamos haciendo que el número de restricciones en el R1CS sea función de una de las entradas del R1CS, pero esto no tiene sentido.
Entonces, ¿cómo verificamos si alguien es mayor de 21 años?
En realidad, esto es más difícil de lo que parece, ya que comparar números en un campo finito es bastante complicado.
Los peligros de comparar números en Circom
Si , entonces, ¿ese número enorme es realmente mayor que 1 o menor que 1?
No puedes comparar números en un campo finito, ya que no tiene sentido decir que un número es mayor que otro.
Sin embargo, ¡aún nos gustaría poder comparar números!
El primer requisito antes de hacer cualquier comparación, es que deben ser menores que el tamaño del campo, y trataremos cualquier número en el campo como un entero positivo, protegiéndonos cuidadosamente contra el desbordamiento inferior (underflow) y superior (overflow).
Si piensas por un momento en cómo representar la siguiente declaración:
usando una representación puramente R1CS, te quedarás atascado. Es imposible hacer eso.
Siempre y cuando forcemos a los números a mantenerse dentro del orden del campo, podremos compararlos de manera significativa. No es posible traducir el operador > a un conjunto de restricciones cuadráticas.
Sin embargo, si convertimos un elemento del campo a una representación binaria del número, entonces es posible hacer una comparación.
Ahora podemos introducir dos templates más de circomlib: Num2Bits y LessThan, con el propósito de comparar enteros.
Num2Bits
El siguiente template Num2Bits de Circomlib muestra cómo circom transforma una señal en un array de señales que contienen la representación binaria.
template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;
// this serves as an accumulator to "recompute" in bit-by-bit
var e2=1;
for (var i = 0; i<n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0; // force out[i] to be 1 or 0
lc1 += out[i] * e2; //add to the accumulator if the bit is 1
e2 = e2+e2; // takes on values 1,2,4,8,...
}
lc1 === in;
}
Restringir un número para que sea representable con bits es equivalente a decir que es menor que .
LessThan
¿Cómo podríamos comparar dos números que son 9,999 o menos sin usar los operadores normales < y > y usando solo una conversión binaria? Si se nos permiten dos conversiones binarias, esto es fácil, pero resulta en un circuito más grande.
Es un problema complicado, pero así es como lo hace circomlib.
Digamos que estamos comparando e .
Dado que 9,999 es el mayor valor que pueden tomar nuestras entradas, sumamos 10,000 a la y restamos la de la suma de e .
Pase lo que pase, será positivo, incluso si es 9,999 y es 0. Como estamos tratando con elementos de campo aquí, no queremos que ocurran desbordamientos inferiores (underflows), y en este caso, no puede ocurrir un underflow.
Aquí está la parte clave. Si , entonces estará entre 10,000 y 19,999 y si , estará en el rango .
Para saber si un número está en el rango , solo necesitamos mirar el dígito en la posición de las decenas de millar, es decir, 1x,xxx. Si tenemos un allí, entonces sabemos que está en el rango y si tenemos algo de la forma 0x,xxx, entonces debe haber sido originalmente mayor que .
Circom simplemente hace lo mismo en representación binaria en lugar de decimal.
En la analogía decimal, sumamos 10,000 a un número del que se garantiza que no será mayor que 9,999. En el caso binario, sumamos el número binario
a un número que se garantiza que tiene como máximo bits de tamaño. Nota que 1 desplazado a la izquierda (left-shifted) bits, es decir, 1 << n es:
Para ver por qué es este el caso, considera en qué se convierte cuando calculamos 1 << 0 y 1 << 1.
Aquí está el template LessThan en Circom:
template LessThan(n) {
assert(n <= 252);
signal input in[2];
signal output out;
component n2b = Num2Bits(n+1);
// add 1 << n then subtract the number we are comparing
n2b.in <== in[0] + (1<<n) - in[1];
// check if the n-th bit is 1 or 0
out <== 1-n2b.out[n];
}
El código está parametrizado por , que es el tamaño máximo de los números en bits, aunque existe un límite superior impuesto de 252 bits para mantenerse por debajo del límite del tamaño del campo y evitar el alias bug.
Los números no pueden ser mayores que , por lo que sumar 1<<n asegura que el término in[0] + (1<<n) siempre será mayor que in[1]. La diferencia se convierte a binario, y si el bit más alto sigue siendo 1, entonces in[0] es mayor que in[1]. El término final es 1 menos ese bit, por lo que esto invierte si el bit está presente o no.
Por lo tanto, el componente restringe la salida (out) para que sea 1 si in[0] es menor que in[1] y 0 de lo contrario.
Ejemplo funcional Over21
Ahora que tenemos la caja de herramientas necesaria, hagamos un verificador de edad que realmente funcione.
Circomlib proporciona un comparador llamado GreaterThan que es como LessThan con un pequeño giro, por lo que no lo explicaremos aquí. El lector interesado puede consultar el código fuente directamente.
Para usar el template de circomlib, crea un directorio node_modules/ vacío y luego ejecuta:
npm install circomlib
Luego crea el siguiente circuito:
pragma circom 2.1.6;
include "node_modules/circomlib/circuits/comparators.circom";
template Over21() {
signal input age;
signal input ageLimit;
signal output oldEnough;
// 8 bits is plenty to store age
component gt = GreaterThan(8);
gt.in[0] <== age;
gt.in[1] <== 21;
0 === gt.out;
oldEnough <== gt.out;
}
component main = Over21();
Esta es la forma segura de verificar que la edad es realmente superior a 21 (aunque en una aplicación real, necesitarías una autoridad que certifique la edad).
Comparators.circom
Los comparadores proporcionados en este archivo son:
IsZeroIsEqual(resta las dos entradas y pasa el resultado a IsZero)LessThanLessEqThan(derivado de LessThan)GreaterThan(derivado de LessThan)GreaterEqThan(derivado de LessThan)ForceEqualIfEnabled
¿Qué hace el último?
ForceEqualIfEnabled
El código para el template ForceEqualIfEnabled se muestra a continuación:
template ForceEqualIfEnabled() {
signal input enabled;
signal input in[2];
component isz = IsZero();
in[1] - in[0] ==> isz.in;
(1 - isz.out)*enabled === 0;
}
ForceEqualIfEnabled nos permite “activar y desactivar restricciones”. Se comporta como una restricción condicional o una declaración if. Si enabled es 0, entonces no importa si in[0] es igual a in[1] o no; la restricción es efectivamente ignorada porque la restricción final será 0 === 0. Por otro lado, si enabled no es cero, entonces 1 - isz.out debe ser cero (es decir, in[1] es igual a in[0]) para que la restricción se cumpla.
Assert en Circom
Curiosamente y de manera confusa, Circom tiene una declaración assert que no hace exactamente lo que uno esperaría.
La declaración assert no añade ninguna restricción.
Es simplemente una comprobación de seguridad para que el desarrollador no cree circuitos con propiedades indeseables.
Por ejemplo, podríamos usarla para asegurar que los templates no se inicialicen con arrays de longitud cero si eso conduce a la posibilidad de una división por cero.
Siempre debes asumir que un probador malicioso puede simplemente copiar el código del circuito, borrar la declaración assert y crear una prueba (proof). Esa prueba será compatible con el circuito, porque el circuito no incorpora la declaración assert.
Operadores booleanos
A estas alturas ya deberías saber que no puedes usar los operadores destinados a las variables en las señales. El siguiente código no compilará:
template And() {
signal input in[2];
signal output c;
c <== in[0] && in[1];
}
Recuerda, las señales son elementos de campo, y && no es un operador válido para los elementos de campo.
Sin embargo, si restringes a y b para que sean 0 y 1, puedes restringir c, a y b para que sigan el comportamiento de una compuerta AND.
template And() {
signal input in[2];
signal output c;
// force inputs to be zero or one
in[0] === in[0] * in[0];
in[1] === in[1] * in[1];
// c will be 1 iff in[0] and in[1] are 1
c <== in[0] * in[1];
}
Es un ejercicio útil para el lector pensar en cómo lograr las otras operaciones booleanas: NOT, OR, NAND, NOR, XOR y XNOR. Aunque cada compuerta booleana se puede construir a partir de una compuerta NAND, esto hará que el circuito sea más grande de lo necesario, así que no exageres con la reutilización de compuertas.
Las soluciones se encuentran en el archivo gates.circom de circomlib. Ten en cuenta que no restringen la entrada a cero o uno; es responsabilidad del diseñador del circuito hacer eso.
Funciones hash compatibles con ZK (ZK-Friendly)
Puedes imaginar que construir una función hash usando el método que producen los circuitos será inmenso. Veamos qué tan grande será un generador de hash sha256 que toma 256 bits:
pragma circom 2.0.0;
include "node_modules/circomlib/circuits/sha256/sha256.circom";
component main = Sha256(256);
Este pequeño e inofensivo circuito producirá casi 30,000 restricciones:
(base) ➜ hello-circom circom Sha256-example.circom --r1cs
template instances: 99
non-linear constraints: 29380 ### WOW! ###
linear constraints: 0
public inputs: 0
public outputs: 256
private inputs: 256
private outputs: 0
wires: 29325
labels: 204521
Written successfully: ./Sha256-example.r1cs
Everything went okay, circom safe
La razón por la que las funciones hash criptográficas tradicionales tienen tantas restricciones es que operan con números de 32 bits, por lo que los elementos de campo deben restringirse para “simular” números de 32 bits.
Esto crea una cantidad de trabajo significativa para el probador. Como respuesta, la comunidad de investigación ha producido funciones hash optimizadas para la representación de circuitos. Además de sha256, encontrarás:
- Mimc
- Pedersen
- Poseidon
Las funciones hash ZK-Friendly (amigables con ZK), por otro lado, usan directamente elementos de campo y evitan operaciones que añaden muchas restricciones, como el desplazamiento de bits (bit-shifting) o las operaciones XOR.
Es un ejercicio para el lector comparar el tamaño de la salida R1CS de las funciones hash. Ten en cuenta que algunas de las funciones toman el número de “rondas” como parámetro, lo que naturalmente aumentará el tamaño del circuito.
Las funciones hash ZK-friendly son un tema considerable que es mejor tratar en su propia discusión, por lo que posponemos esto para un artículo futuro.
¿Qué pasa con el resto?
El resto de los templates son lo suficientemente pequeños como para explicarse por sí mismos, o están relacionados con esquemas de firmas digitales de conocimiento cero y el cálculo de curvas elípticas.
La motivación para calcular curvas elípticas dentro de un circuito ZK es que algunas funciones hash ZK-friendly se basan en curvas elípticas como primitiva central.
Este es otro gran tema que posponemos para otro artículo.
Aprender Circom con ejemplos del mundo real
Dos de los circuitos clásicos pero accesibles para estudiar son Tornado Cash y Semaphore.
Aprende más con RareSkills
La mejor manera de aprender circom es usándolo. Nuestros Zero Knowledge Puzzles ofrecen pequeños retos de complejidad creciente para que aprendas el lenguaje. Se proporciona un entorno de desarrollo con pruebas unitarias (unit tests) para informarte si has completado el puzzle con éxito. Ten en cuenta que es posible pasar las pruebas con circuitos sub-restringidos, ya que probar si existen sub-restricciones es extremadamente difícil de hacer en general. Como mínimo, debes verificar el número de restricciones generadas y asegurarte de que la cantidad tenga sentido.
Este material es parte de nuestro curso de conocimiento cero (zero knowledge). Consulta el programa para obtener más información.
Publicado originalmente el 26 de septiembre de 2023