El propósito principal de Circom es compilar hacia un Rank 1 Constraint System (R1CS), pero su propósito secundario es poblar el witness.
Para la mayoría de los circuitos, el valor de unas pocas señales determina cuáles serán los valores del resto de las señales.
Por ejemplo, puede parecer un poco redundante proporcionar c como un input en el siguiente template porque su valor depende completamente de a y b:
template Mul() {
signal input a;
signal input b;
signal input c;
c === a * b;
}
A continuación se muestra un ejemplo más motivador.
Dividir una restricción no cuadrática
Supongamos que queremos crear un R1CS para a * b * c === d. Dado que R1CS permite una multiplicación por restricción, tenemos que crear otra señal s y una restricción adicional para dividir la multiplicación:
template Mul3() {
signal input a;
signal input b;
signal input c;
signal input d;
signal input s;
s === a * b;
d === s * c;
}
Sería extremadamente tedioso proporcionar otro input cada vez que hagamos más de una multiplicación, especialmente en circuitos más grandes con numerosas multiplicaciones. Además, el valor de s en el ejemplo anterior depende de forma determinista de a y b.
Señales intermedias y asignación
Para evitar la molestia de proporcionar s, Circom ofrece los operadores ==> y <== que asignan el valor de s para que sea calculado por Circom (recuerda que parte de la funcionalidad de Circom es generar el witness). Por lo tanto, el valor de s no necesitará ser proporcionado como un input. Los operadores ==> y <== significan (precisamente) “asignar y restringir”:
template Mul3() {
signal input a;
signal input b;
signal input c;
signal input d;
// no longer an input
signal s;
a * b ==> s;
s * c === d;
}
Circom es flexible en cuanto a la dirección de la flecha, a * b ==> s significa lo mismo que s <== a * b.
En el código anterior, s recibe el nombre de señal intermedia. Una señal intermedia es una señal definida con la palabra clave signal sin la palabra clave input. Por lo tanto, signal s es una señal intermedia, pero signal input a no lo es.
El R1CS subyacente es idéntico entre los dos templates anteriores. El ==> simplemente nos ahorra la molestia de proporcionar el valor de s como parte del input.
Suponiendo que el vector witness se representa como [1, a, b, c, d, s], el R1CS subyacente sería el siguiente:
Esto se puede pensar como pasarle a Circom el witness [1, a, b, c, d, _] y que Circom calcule el witness completo [1, a, b, c, d, s] basándose en el input.
La asignación a s ocurre fuera del R1CS. El R1CS solo verifica que el vector witness satisfaga una ecuación matricial. El R1CS espera que se proporcione el witness y no calcula ninguno de sus valores. Este enfoque simplifica el diseño de circuitos y reduce el esfuerzo manual al tiempo que mantiene inalterada la estructura del R1CS.
Los Valores de las Señales No Pueden Ser Reasignados Con <==
Una señal representa una entrada concreta en el vector witness. Por lo tanto, no puede cambiar de valor una vez que se ha establecido. Como tal, el siguiente código no compilará:
template CannotReassign() {
signal input a;
signal input b;
signal c;
c <== a * b;
// not allowed
// c already set
c <== a * a;
}
Ejemplo Real: Comprobar el Producto de un Array
Cuantas más multiplicaciones tengamos en nuestro circuito, más útil se vuelve el operador ==> porque nos ahorra tener que proporcionar señales de input adicionales.
Supongamos que quisiéramos obligar a que la señal de input k sea el resultado del producto de todas las señales en el array in[n]. En otras palabras, estamos comprobando:
Esto introduciría una cantidad significativa de señales intermedias. Para mantener el código limpio, podemos hacer que todas las señales intermedias se asignen a un array separado de la siguiente manera:
template KProd(n) {
signal input in[n];
signal input k;
// intermediate signal array
signal s[n];
s[0] <== in[0];
for (var i = 1; i < n; i++) {
s[i] <== s[i - 1] * in[i];
}
k === s[n - 1];
}
Basado en el código anterior, s[n - 1] contiene el valor
el cual luego podemos restringir para que sea igual a k.
Dividir Circom en Templates
Ahora que entendemos el operador <==, podemos comprender cómo Circom utiliza templates para hacer que el código sea más modular.
De manera similar a nuestro ejemplo Mul3, supongamos que tenemos un circuito que toma 3 inputs y obliga a que su producto sea un 4º (aquí se reproduce el código):
template Mul3() {
signal input a;
signal input b;
signal input c;
signal input d; // d === a * b * c
// no longer an input
signal s;
a * b ==> s;
s * c === d;
}
Pero supongamos que tuviéramos que hacer esto dos veces con ocho inputs. En este caso, podría ser tentador copiar y pegar el código dos veces para los inputs (a,b,c,d) y (x,y,z,u), lo cual sería feo.
template Mul3x2() {
signal input a;
signal input b;
signal input c;
signal input d; // d === a * b * c
signal input x;
signal input y;
signal input z;
signal input u; // u === x * y * z
// ugly code here
}
En su lugar, podemos poner Mul3 como un template separado de la siguiente manera:
// separate template
template Mul3() {
signal input a;
signal input b;
signal input c;
signal input d; // d === a * b * c
// no longer an input
signal s;
a * b ==> s;
s * c === d;
}
// main component
template Mul3x2() {
signal input a;
signal input b;
signal input c;
signal input d; // d === a * b * c
signal input x;
signal input y;
signal input z;
signal input u; // u === x * y * z
component m3_1 = Mul3();
m3_1.a <== a;
m3_1.b <== b;
m3_1.c <== c;
m3_1.d <== d;
component m3_2 = Mul3();
m3_2.a <== x;
m3_2.b <== y;
m3_2.c <== z;
m3_2.d <== u;
}
Cabe destacar:
- Declaramos componentes con la sintaxis
component m3_1 = Mul3();. Esta es la misma sintaxis que usamos para declarar el componente principal. - “Conectamos” las señales usando el operador
<==. - El código anterior es completamente equivalente a copiar y pegar la lógica central de
Mul3dos veces.
Devolver Resultados desde los Templates
Sería útil en algunas situaciones que un subcomponente pudiera “devolver resultados” al componente que lo creó.
Por ejemplo, el siguiente componente principal usa un subcomponente Square para asignar y restringir out para que sea el cuadrado de in.
template Square() {
signal input in;
signal output out;
out <== in * in;
}
template Main() {
signal input a;
signal input b;
signal input sumOfSquares;
component a2 = Square();
component b2 = Square();
a2.in <== a;
b2.in <== b;
// assert that a^2 + b^2 === sum of Squares
a2.out + b2.out === sumOfSquares;
}
component main = Main();
En el contexto de los subcomponentes, una señal de output es una señal a la que se espera que se le asigne un valor mediante el operador <== y que puede usarse para devolver valores al componente que la creó.
En el contexto del componente main — una señal de output significa algo completamente diferente — lo explicaremos en un capítulo posterior.
Ejemplo: De Binario a Número
La biblioteca circomlib es una biblioteca de templates de Circom para varias operaciones comunes. Una de esas operaciones es convertir un array binario en una señal. Hemos visto anteriormente que esto se puede lograr con . Aquí mostramos cómo podemos hacerlo en un componente separado. El siguiente template se puede encontrar en el archivo bitify.circom de la biblioteca Circom:
template Bits2Num(n) {
signal input in[n];
signal output out;
// lc is short for "linear combination"
// it serves as an accumulator variable
var lc1=0;
var e2 = 1;
for (var i = 0; i<n; i++) {
lc1 += in[i] * e2;
e2 = e2 + e2; // could also be e2 *= 2;
}
lc1 ==> out;
}
No necesitamos copiar y pegar código de la biblioteca; se puede “incluir” de manera similar a cómo otros lenguajes importan otros archivos:
include "circomlib/bitify.circom";
template Main(n) {
signal input in[n];
signal input v;
// instantiate the Bits2Num component
component b2n = Bits2Num(n);
// loop over each binary value
// and assign and constrain it to the
// b2n input array
for (var i = 0; i < n; i++) {
b2n.in[i] <== in[i];
}
b2n.out === v;
}
component main = Main(4);
/* INPUT = {"in": [1, 0, 0, 1], "v": 9} */
El componente anterior se puede probar en zkrepl, pero si se ejecuta localmente, la ruta de importación debe establecerse según cómo esté configurado el directorio. Normalmente, Circomlib se instala con yarn o npm.
Ejemplo de componente en una línea
En lugar de asignar las señales de input a un componente por separado, es posible proporcionarlas como un argumento. A esto se le llama un “componente anónimo”. Considera el siguiente ejemplo:
template Mul() {
signal input in[2];
signal output out;
out <== in[0] * in[1];
}
template Example() {
signal input a;
signal input b;
signal output out;
// one line instantiation
out <== Mul()([a, b]);
}
component main = Example();
Las señales de output no deben ser ignoradas
Una señal de output debe ser parte de las restricciones en el componente que la instanció. Si una señal de output se deja “flotante”, en algunas circunstancias, un prover malicioso puede asignarle cualquier valor. Se cubrirá más sobre esto en hacking underconstrained circuits.
Resumen
- Los operadores
<==y==>nos ahorran la molestia de proporcionar explícitamente el valor de una señal en el archivo input.json. - Podemos usar
<==o==>siempre que el valor de una señal esté determinado directamente por el valor de otra. <==es equivalente a==>. Los argumentos simplemente se invierten, pero el efecto es el mismo.- Los componentes pueden instanciar otros subcomponentes y enviar valores a sus señales de input usando
<==o==>. - Las señales de
outputde un subcomponente deben estar restringidas para ser iguales a otras señales en el componente que lo instanció.