Si queremos decir que “x puede ser igual a 5 o 6”, simplemente podemos usar la siguiente restricción:

Copy
(x - 6) * (x - 5) === 0

Sin embargo, supongamos que queremos decir que “x es menor que 5 o x es mayor que 17”. En este caso, no podemos simplemente combinar ambas condiciones directamente, porque si x es menor que 5, violará la restricción de que x es mayor que 17 y viceversa.

La solución es crear señales indicadoras de las diferentes condiciones (por ejemplo, que x sea menor que 5, o sea mayor que 17), y luego aplicar restricciones a los indicadores.

Biblioteca de comparadores de Circomlib

La biblioteca de comparadores de Circomlib contiene un componente LessThan que devuelve 0 o 1 para indicar si in[0] es menor que in[1]. El funcionamiento de este componente se describe en el capítulo Arithmetic Circuit. Pero a modo de resumen, supongamos que x e y tienen como máximo 3 bits de tamaño. Si calculamos z = 2^3 + (x - y), entonces si x es menor que y, z será menor que 2^3 y viceversa (2^3 = 8). Dado que z es un número de 4 bits, podemos comprobar de manera eficiente si z es menor que 2^3 mirando solo el bit más significativo. 2^3 en binario es 1000₂. Todo número de 4 bits mayor o igual a 2^3 tiene el bit más significativo igual a 1, y todo número de 4 bits menor que 2^3 tiene el bit más significativo igual a 0.

Para números generales de n bits, podemos comprobar si x es mayor o igual a 2^n verificando si el bit más significativo está activado. Por lo tanto, podemos generalizar que si x e y son números de n-1 bits, entonces podemos detectar si x < y comprobando si el bit más significativo de 2^(n-1) + (x - y) está activado o no.

Aquí hay un ejemplo mínimo del uso de la plantilla LessThan:

Copy
include "circomlib/comparators.circom";

template Example () {
  signal input a;
  signal input b;
  signal output out;
  
  // 252 will be explained in the next section
  out <== LessThan(252)([a, b]);
}

component main = Example();

/* INPUT = {
  "a": "9",
  "b": "10"
} */

De dónde viene el 252

Los números en un campo finito (que es lo que usa Circom) no se pueden comparar entre sí como “menor que” o “mayor que” ya que las leyes algebraicas típicas de las desigualdades no se cumplen.

Por ejemplo, si $x > y$, entonces si $c$ es positivo, siempre debería ser cierto que $x+c>y+c$. Sin embargo, esto no es cierto en un campo finito. Podríamos elegir $c$ de manera que sea el inverso aditivo de $x$, es decir, $x + c=0\mod p$. Entonces terminaríamos con una afirmación sin sentido de que 0 es mayor que un número distinto de cero. Por ejemplo, si $p = 7$ y $x=2$ e $y=1$ tenemos que $x>y$. Sin embargo, si sumamos $5$ tanto a $x$ como a $y$, entonces tenemos $0>1$.

El 252 especifica el número de bits en el componente LessThan para limitar cuán grandes pueden ser x e y, de modo que se pueda hacer una comparación con sentido (la sección anterior usó 4 bits como ejemplo).

Circom puede almacenar números de hasta 253 bits de tamaño en el campo finito. Por razones de seguridad discutidas en el capítulo Alias Check, no deberíamos convertir un elemento del campo a una representación binaria que pueda codificar números más grandes que el campo. Por lo tanto, Circom no permite que las plantillas de comparación se instancien con más de 252 bits (código fuente).

Sin embargo, recordemos que para LessThan(n) necesitamos calcular z = 2^n + (x - y), y 2^n necesita ser un bit más grande que x o y. Por lo tanto, x e y necesitan ser, como máximo, de $2^{n-1}$ bits de tamaño. Dado que Circom soporta números de hasta 253 bits de tamaño, x e y deben ser como máximo de 252 bits.

x es menor que 5 o x es mayor que 17

Afortunadamente, la biblioteca Circomlib hará la mayor parte del trabajo por nosotros. Usaremos las señales de salida de los componentes LessThan y GreaterThan para indicar si x es menor que 5 o mayor que 17.

Luego, restringimos que al menos una de ellas sea 1 usando el componente OR (que bajo el capó es simplemente out <== a + b - a * b).

Copy
pragma circom 2.1.6;

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

template DisjointExample1() {
  signal input x;
  
  signal indicator1;
  signal indicator2;

  indicator1 <== LessThan(252)([x, 5]);
  indicator2 <== GreaterThan(252)([x, 17]);

  component or = OR();
  or.a <== indicator1;
  or.b <== indicator2;

  or.out === 1;
}

component main = DisjointExample1();

/* INPUT = {
  "x": "18"
} */

Es muy importante incluir la restricción or.out === 1;, de lo contrario el circuito aceptaría que las señales indicator1 e indicator2 sean ambas cero. Volveremos a esto con mayor detalle hacia el final de este capítulo.

Simplificando el código

El código anterior se puede simplificar usando las señales indicadoras implícitamente, como se demuestra a continuación:

Copy
pragma circom 2.1.6;

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

template DisjointExample1() {
  signal input x;

  component or = OR();
  or.a <== LessThan(252)([x, 5]);
  or.b <== GreaterThan(252)([x, 17]);
  or.out === 1;   
}

component main = DisjointExample1();

/* INPUT = {
  "x": "18"
} */

No es el caso que tanto x < 100 como y < 100

Para expresar el caso anterior donde tanto x < 100 como y < 100, podemos usar una puerta NAND. La puerta NAND devuelve 1 para todas las combinaciones excepto cuando ambas entradas son 1, lo cual tiene la siguiente tabla de verdad:

Por lo tanto, podemos crear una señal indicadora de que x es menor que 100 y una señal indicadora de que y es menor que 100, y restringir una relación NAND entre ellas.

Copy
pragma circom 2.1.6;

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

template DisjointExample2() {
  signal input x;
  signal input y;

  component nand = NAND();
  nand.a <== LessThan(252)([x, 100]);
  nand.b <== LessThan(252)([y, 100]);
  nand.out === 1;   
}

component main = DisjointExample2();

/* INPUT = {
  "x": "18",
  "y": "100"
} */

k es mayor que al menos 2 de x, y, o z

En este ejemplo, intentamos expresar que k es mayor que x e y o k es mayor que x y z, o k es mayor que y y z. k podría ser mayor que x, y, y z, pero eso no es necesario.

Dado que es verboso expresar una expresión lógica tan complicada como la anterior, es más simple sumar el número de señales de las que k es mayor, y luego comprobar que este número es 2 o más.

Copy
pragma circom 2.1.6;

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

template DisjointExample3(n) {
  signal input k;
  signal input x;
  signal input y;
  signal input z;
  
  signal totalGreaterThan;
  
  signal greaterThanX;
  signal greaterThanY;
  signal greaterThanZ;
  
  greaterThanX <== GreaterThan(252)([k, x]);
  greaterThanY <== GreaterThan(252)([k, y]);
  greaterThanZ <== GreaterThan(252)([k, z]);
  
  totalGreaterThan = greaterThanX + greaterThanY + greaterThanZ;
  
  signal atLeastTwo;
  atLeastTwo <== GreaterEqThan(252)([totalGreaterThan, 2]);
  atLeastTwo === 1;
}

component main = DisjointExample3();

/* INPUT = {
  "k": 20
  "x": 18,
  "y": 100,
  "z": 10
} */

¡No olvides restringir las salidas de los componentes!

A veces, los desarrolladores pueden olvidar restringir la salida de los componentes, ¡lo que puede provocar vulnerabilidades de seguridad graves! Por ejemplo, el siguiente código podría parecer que obliga a que x e y sean ambos iguales a 1, pero este no es el caso. x e y podrían ser cero (o cualquier otro valor arbitrario). La salida de la puerta AND será cero si x e y son cero, pero la salida no está restringida a ser nada.

Copy
template MissingConstraint1() {
  signal input x;
  signal input y;

  component and = AND();
  and.a <== x;
  and.b <== y;
  
  // and.out is not constrained, so x and y can have any values!
}

De manera similar, el siguiente circuito no obliga a que x sea menor que 100. La salida de LessThan es 1 si x es menor que 100, pero el código no restringe la salida para asegurar que esto sea de hecho cierto.

Copy
template MissingConstraint2() {
  signal input x;

  component lt = LessThan(252);
  lt.in[0] <== x;
  lt.in[1] <== 100;
  	
  // x could be ≥ 100 since lt.out is allowed to be 0 or any other arbitrary value
}