Introduction

Este capítulo muestra la relación entre el código de Circom y el Rank 1 Constraint System (R1CS) al que compila.

Entender los R1CS es crítico para comprender Circom, así que asegúrate de repasar sobre Rank 1 Constraint Systems si aún no lo has hecho.

Para explicar el funcionamiento de Circom, comenzaremos con algunos ejemplos.

Ejemplo 1: Multiplicación Simple

Supongamos que estamos intentando crear pruebas ZK para evaluar si alguien conoce el producto de dos números arbitrarios: c = a * b.

Dicho de otra manera, para ciertos a y b, buscamos verificar que el usuario ha calculado el valor correcto para c.

En pseudocódigo, la verificación sería de la siguiente manera (ten en cuenta que esto no es código de Circom):

Copy
def someVerification(a, b, c):
  res = a * b 
  assert res == c, "invalid calculation"

En consecuencia, nuestro R1CS tendría solo una restricción (constraint), a saber, la siguiente:

Copy
assert c == a * b

R1CS expresa tales restricciones en un formato matricial estructurado. Según lo que vimos en el capítulo sobre R1CS, el vector testigo (witness vector) $\mathbf{w}$ debería escribirse como [1, a, b, c], y el R1CS correspondiente puede escribirse como:

Si a = 3, b = 4 y c = 12, la operación anterior sería:

Así es como escribiríamos la restricción anterior en Circom:

Copy
template SomeCircuit() {
  // inputs
  signal input a;
  signal input b;
  signal input c;
  
  // constraints 
  c === a * b;
}

component main = SomeCircuit();

• Dados los inputs a, b, c, el circuito verifica que a * b sea de hecho igual a c.
• El circuito sirve para verificar, no para calcular. Es por esto que c (el output del cálculo) también es uno de los inputs requeridos.
• El operador === define la restricción tal como se expresó previamente en formato R1CS. === se comporta como un assertion (afirmación), por lo que el circuito no se satisfará si se proporcionan inputs inválidos. En el código anterior, c === a * b restringe a c para que tenga un valor igual al producto de a y b.

zkRepl, un IDE en línea para Circom

Para experimentos rápidos, zkRepl es una herramienta fantástica y conveniente.

Podemos probar convenientemente el código anterior en zkRepl suministrando los inputs como un comentario:

Nota: El input se suministra como un objeto JSON en un comentario al usar zkRepl. Para probar si el código compila y el input satisface el circuito, presiona shift-enter.

Las “non-linear constraints” (restricciones no lineales) equivalen a 1 (ver el cuadro rojo) porque el R1CS subyacente tiene una restricción de fila con una multiplicación entre dos señales (signals). Esto es de esperarse, ya que tenemos un solo ===.

template , component , main

• Los templates definen un plano (blueprint) para los circuitos, al igual que una clase define la estructura para los objetos en Object Oriented Programming (OOP).
• Un component es una instanciación de un template, de forma similar a como un objeto es una instancia de una clase en Object Oriented Programming.

Copy
// create template
template SomeCircuit() {
  // .... stuff
}

// instantiate template 
component main = SomeCircuit();

Se necesita component main = SomeCircuit() porque Circom requiere un solo component de nivel superior, main, para definir la estructura del circuito que se compilará.

signal input

• Los signal inputs son valores que se proporcionarán desde fuera del component. (Circom no impone que realmente se proporcione un valor — depende del desarrollador asegurarse de que los valores realmente se suministren. Si no es así, esto puede provocar una vulnerabilidad de seguridad — esto se explorará en un capítulo posterior).
• Las señales de entrada (input signals) son inmutables y no pueden ser alteradas.
• Las signals son exactamente las variables en el vector testigo (witness vector) de un Rank 1 Constraint System.

El Campo Finito de Circom

Circom realiza aritmética en un campo finito con un orden de 21888242871839275222246405745257275088548364400416034343698204186575808495617, al que simplemente llamaremos $p$. Es un número de 254 bits, correspondiente al orden de curva de la curva elíptica bn128. Esta curva es muy utilizada, en particular es la que está disponible a través de precompilados (precompiles) en la EVM. Dado que Circom fue diseñado para utilizarse en el desarrollo de aplicaciones ZK-SNARK en Ethereum, tiene sentido hacer que el tamaño del campo coincida con el orden de la curva bn128.

Circom permite cambiar el orden predeterminado mediante un argumento de línea de comandos.

Lo siguiente debería resultar obvio para el lector:

• p bajo mod p es congruente con 0;
• p-1 es el número entero más grande en el campo finito mod p.
• Pasar valores mayores que p-1 provocará un desbordamiento (overflow).

Ejemplo 2: BinaryXY

Veamos un segundo ejemplo para concluir esta sección.

Considera un circuito que verifica si los valores que se le pasan son binarios, es decir, 0 o 1.

Si las variables de entrada son x e y, el sistema de restricciones sería:

Copy
(1):  x * (x - 1) === 0
(2):  y * (y - 1) === 0

Recuerda que, por definición, cada restricción en un R1CS puede tener como máximo una multiplicación entre variables.

x(x-1) === 0 comprueba si x es un dígito binario*

• Solo hay 2 raíces para esta expresión polinómica.
• Es decir, x = 0 o x = 1.

Expresado en Circom

Copy
template IsBinary() {
	
  signal input x;
  signal input y;
  
  x * (x - 1) === 0;
  y * (y - 1) === 0;
}

component main = IsBinary();

Expresión Alternativa: Usando Arrays

En Circom, tenemos la opción de declarar nuestros inputs como signals separados o de declarar un array que contenga todos los inputs. Es más convencional en Circom agrupar todos los inputs en un array de signals llamado in en lugar de proporcionar los inputs x e y por separado.

Siguiendo la convención, representaremos el circuito anterior de la siguiente manera. Los arrays se indexan comenzando desde cero, como normalmente se esperaría:

Copy
template IsBinary() {

  // array of 2 input signals
  signal input in[2];
  
  in[0] * (in[0] - 1) === 0;
  in[1] * (in[1] - 1) === 0;
}

// instantiate template 
component main = IsBinary();

Solo se aceptan witnesses que satisfacen las restricciones

Circom solo puede generar una prueba (proof) para un input que realmente satisfaga el circuito. En el siguiente circuito (copiado directamente del código anterior), proporcionamos [0, 2] como un input que solo acepta {0,1} para cualquier elemento del array.

Para el 0, tenemos 0 * (0 - 1) === 0, lo cual es correcto. Sin embargo, para 2 * (2-1) === 2, tenemos una violación de la restricción (constraint violation) como se indica en el recuadro rojo de la siguiente figura.

Circom en la línea de comandos

Esta sección introduce comandos comunes de Circom. Asumimos que el lector ya ha instalado Circom y las dependencias requeridas.

Crea un nuevo directorio y añade un archivo llamado somecircuit.circom en su interior con el siguiente código:

Copy
pragma circom 2.1.8;

template SomeCircuit() {
  // inputs
  signal input a;
  signal input b;
  signal input c;
  
  // constraints 
  c  === a * b;
}

component main = SomeCircuit();

1. Compilando Circuitos

En el terminal, ejecuta el siguiente comando para compilar:

Copy
circom somecircuit.circom --r1cs --sym --wasm

• El flag --r1cs significa que se debe generar un archivo r1cs, el flag --sym le da a las variables un nombre legible para humanos (se puede encontrar más información en la documentación de sym), y --wasm sirve para generar código wasm para poblar el witness del R1CS, dado un JSON de entrada (mostrado en una sección posterior).
• Intercambia el nombre del circuito somecircuit.circom a compilar según sea necesario.

Este es el output esperado:

• Observa que las non-linear constraints (restricciones no lineales) aparecen como 1, indicativo de a * b === c.
• Wires es el número de columnas en el R1CS. En este ejemplo, tenemos una columna constante y tres signals a, b, c.

El compilador crea lo siguiente:

• Archivo somecircuit.r1cs
• Archivo somecircuit.sym
• Directorio somecircuit_js

Archivo .r1cs

• Este archivo contiene el sistema de restricciones R1CS del circuito en formato binario.
• Puede utilizarse con diferentes stacks de herramientas para construir declaraciones (statements) de prueba/verificación (ej. snarkjs, libsnark).

Ten en cuenta que los archivos R1CS son algo así como binarios, en el sentido de que ejecutar cat <file> te mostrará texto ininteligible (gibberish).

Ejecutando snarkjs r1cs print somecircuit.r1cs, obtenemos el siguiente output legible para humanos:

Copy
[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.a ] * [ main.b ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.c ] = 0

En Circom, las operaciones aritméticas se llevan a cabo dentro de un campo finito, por lo que 21888242871839275222246405745257275088548364400416034343698204186575808495616 en realidad es representativo de -1. En el archivo R1CS, sin embargo, el operador de restricción es = en lugar de == o ===.

Podemos confirmar esto verificando -1 mod p, (en Python: -1 % p), donde p es el orden del campo finito de Circom. Si traducimos los grandes valores que imprimió snarkjs r1cs print somecircuit.r1cs a números negativos, obtenemos:

Copy
[-1 * main.a] * [main.b] - [-1 * main.c] = 0

Ahora convertiremos la expresión anterior en la forma más familiar a * b === c. El álgebra se muestra a continuación:

Copy
[-1 * main.a] * [main.b] - [-1 * main.c] = 0

    [-main.a] * [main.b] - [-main.c] = 0 // distribute -1
   
     [main.a] * [main.b] + [-main.c] = 0 // multiply both sides by -1
    
     [main.a] * [main.b] = [main.c] // move -main.c to the other side

Nuevamente, observa que esto coincide con la restricción (a * b === c) descrita en somecircuit.circom.

Archivo .sym

El archivo somecircuit.sym es un archivo de símbolos generado durante la compilación. Este archivo es esencial porque:

• Mapea los nombres legibles de las variables a sus posiciones correspondientes en el R1CS para la depuración (debugging).
• Ayuda a imprimir el sistema de restricciones en un formato más comprensible, facilitando la verificación y depuración de tu circuito.

Directorio somecircuit_js

El directorio somecircuit_js contiene artefactos para la generación del witness:

• somecircuit.wasm
• generate_witness.js
• witness_calculator.js

El archivo generate_witness.js es lo que usaremos en la siguiente sección, los otros dos archivos son ayudantes (helpers) para generate_witness.js.

Al suministrar valores de entrada para el circuito, estos artefactos calcularán los valores intermedios necesarios y crearán un witness que podrá utilizarse para generar una prueba ZK (ZK proof).

2. Calculando el Witness

Para generar el witness, debemos suministrar los valores de input públicos para el circuito. Hacemos esto creando un archivo inputs.json en el directorio somecircuit_js.

Supongamos que queremos crear un witness para los valores de entrada a=1, b=2, c=2. El archivo JSON sería así:

Copy
{"a": "1","b": "2","c": "2"}

Circom espera strings en lugar de números porque JavaScript no funciona de manera precisa con enteros mayores a $2^{53}$ (fuente).

Ejecuta este comando en el directorio somecircuit_js:

Copy
node generate_witness.js **somecircuit.wasm** inputs.json witness.wtns

El output es el witness calculado como un archivo witness.wtns.

Examinar el Witness Calculado: witness.wtns

Si ejecutas cat witness.wtns, el output es texto ininteligible.

Esto se debe a que witness.wtns es un archivo binario en un formato aceptado por snarkjs.

Para obtener la forma legible para humanos, lo exportamos a JSON mediante: snarkjs wtns export json witness.wtns. Luego vemos el JSON usando cat witness.json:

• El primer 1 es la porción constante del witness, la cual siempre es 1. Tenemos que a = 1, b = 2 y c = 2 ya que nuestro JSON de entrada era {"a": "1","b": "2","c": "2"}.
• snarkjs ingiere el archivo witness.wtns para emitir witness.json.
• El witness calculado se adhiere a la disposición R1CS del vector testigo (witness vector): [1, a, b, c] = [1, 1, 2, 2]

Ejemplo: isbinary.circom

Repasemos un ejemplo menos trivial: isbinary.circom. La forma de las restricciones debería resultarle familiar al lector (recuerda el ejemplo 2).

Copy
template IsBinary() {

  // array of 2 input signals
  signal input in[2];
  
  in[0] * (in[0] - 1) === 0;
  in[1] * (in[1] - 1) === 0;
}

// instantiate template 
component main = IsBinary();

Compilar Circuito

• circom isbinary.circom --r1cs --sym --wasm
• Comprobación rápida (sanity check) en el output del terminal: non-linear constraints: 2

Esto tiene sentido, ya que nuestro circuito contiene dos aserciones (assertions), cada una involucrando una multiplicación de signals.

A continuación, examinamos el archivo R1CS: El comando snarkjs r1cs print isbinary.r1cs resulta en el siguiente output:

Copy
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[0] ] * [ main.in[0] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[1] ] * [ main.in[1] ] - [  ] = 0

Nota que este gran número es ligeramente diferente del coeficiente -1 mod p destacado anteriormente (Ej.: 21888242871839275222246405745257275088548364400416034343698204186575808495616)

Observa el dígito adicional, 1, al final:

• 21888242871839275222246405745257275088548364400416034343698204186575808495616
• 21888242871839275222246405745257275088548364400416034343698204186575808495616(1)

La razón por la que hay un 1 al final se debe a un defecto en cómo snarkjs formatea el output. Está “intentando” decir -1 * 1 pero no tiene espacio entre ellos.

Ahora transformaremos algebraicamente el output de snarkjs a las restricciones originales de:

Copy
(in[0] - 1) * in[0] === 0
(in[1] - 1) * in[0] === 0

La derivación es la siguiente:

Copy
// original circom output
[ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[0] ] * [ main.in[0] ] - [  ] = 0
[ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[1] ] * [ main.in[1] ] - [  ] = 0

// remove empty terms
[ (21888242871839275222246405745257275088548364400416034343698204186575808495616)1 +main.in[0] ] * [ main.in[0] ] = 0
[ (21888242871839275222246405745257275088548364400416034343698204186575808495616)1 +main.in[1] ] * [ main.in[1] ] = 0

// rewrite p - 1 as -1
[ (-1)1 +main.in[0] ] * [ main.in[0] ] = 0
[ (-1)1 +main.in[1] ] * [ main.in[1] ] = 0

// simplify
[ main.in[0] - 1] * [ main.in[0] ] = 0
[ main.in[1] - 1] * [ main.in[1] ] = 0

Generando el Witness

• Crea un archivo inputs.json en el directorio ./isbinary_js.
• Optaremos por pasar los valores in[0] = 1, in[1] = 0.
• Usaremos lo siguiente para inputs.json.

Copy
{"in": ["1","0"]}

• Genera witness.wtns: node generate_witness.js isbinary.wasm inputs.json witness.wtns (en el directorio isbinary_js)
• Ahora que se ha creado witness.wtns, expórtalo a JSON para que podamos examinarlo:
  snarkjs wtns export json witness.wtns
• Obtendríamos el siguiente output al ejecutar cat witness.json:

Copy
[
 "1",  // 1
 "1",  // in[0] 
 "0"   // in[1] 
]

• La signal calculada coincide con la disposición R1CS del vector testigo (witness vector), [1, in[0], in[1]], al igual que sus respectivos valores.

Generando una Prueba ZK

Una vez creado el R1CS, el lector puede seguir los pasos en la documentación de Circom para generar la Prueba ZK (ZK Proof) y un smart contract verificador acompañante.

Problemas de Práctica

Pon a prueba tu comprensión/aprendizaje de este capítulo resolviendo estos puzzles de nuestro repositorio ZK Puzzles. Cada puzzle requiere que completes la lógica faltante. Puedes verificar tus respuestas simplemente ejecutando las pruebas unitarias (unit tests).

• https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/BinaryXY/BinaryXY.circom
• https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/MultiplyNoOut/MultiplyNoOut.circom
• https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/FourBitBinary/FourBitBinary.circom