Este capítulo cubre la sintaxis esencial, la cual verás en la mayoría de los programas de Circom. Con Circom, somos capaces de definir un Rank 1 Constraint System (R1CS) usando código en lugar de definir explícitamente cada restricción. Exploraremos esas herramientas en este capítulo.

Parámetros de plantilla

Anteriormente, vimos un circuito (IsBinary) que verificaba si las entradas proporcionadas eran efectivamente binarias. Ese circuito estaba codificado de forma estática (hardcoded) para aceptar solo 2 entradas.

Copy
template IsBinary() {

  signal input in[2];

  in[0] * (in[0] - 1) === 0;
  in[1] * (in[1] - 1) === 0;
}

component main = IsBinary();

Aunque el código anterior funciona para dos entradas, modificarlo para soportar un número grande de n entradas requeriría agregar restricciones manualmente, lo cual es una mala experiencia para el desarrollador.

Por lo tanto, Circom nos permite restringir un número arbitrario de señales usando el siguiente patrón para generar las restricciones automáticamente:

Copy
template IsBinary(n) {

  // array of n inputs
  signal input in[n];
    
  // n loops: n constraints
  for (var i = 0; i < n; i++) {
    in[i] * (in[i] - 1) === 0;
  }
}

// instantiated w/ 4 inputs & 4 constraints
component main = IsBinary(4);

Nota que la declaración de la plantilla ha cambiado para incluir n en el paréntesis.

• n aquí se conoce como un parámetro de plantilla
• n se usa dentro del circuito para especificar el tamaño del array in
• al instanciar la plantilla, debemos especificar el valor de n

Los circuitos y las restricciones en Circom deben tener una estructura fija y conocida

Aunque las restricciones pueden generarse programáticamente, la existencia y configuración de las restricciones no pueden depender condicionalmente de las señales.

Aunque las plantillas pueden usar parámetros, el circuito debe ser estático y estar claramente definido. No hay soporte para circuitos o restricciones de “longitud dinámica” — todo debe ser fijo y estar bien definido desde el principio.

Imagina tener un sistema de restricciones R1CS cuya estructura fuera mutable basada en los valores de las señales de entrada. Ni el probador (prover) ni el verificador (verifier) podrían operar, ya que el número de restricciones no está escrito en piedra.

El valor de n debe establecerse en tiempo de compilación.

Bucle for y Variables: for, var

Ahora explicaremos el bucle for introducido anteriormente.

Copy
template IsBinary(n) {

  // array of n inputs
  signal input in[n];
    
  // n loops: n constraints
  for (var i = 0; i < n; i++) {
    in[i] * (in[i] - 1) === 0;
  }
}

// instantiated with 4 inputs & 4 constraints
component main = IsBinary(4);

• tanto las entradas como las iteraciones del bucle están definidas por n
• para cada entrada, se define una restricción con el propósito de verificar que la entrada es 0 o 1

Hemos introducido dos nuevas palabras clave en el circuito: for y var

• for funciona como estás acostumbrado.
• La palabra clave var declara una variable; en este caso, i, como se ve en la definición del bucle.
• El símbolo de igual = asigna el valor de la derecha a la variable de la izquierda.

Aquí, la variable i se usa para referirse programáticamente a diferentes señales en el array de entrada mientras se crean restricciones para ellas. Poder generar restricciones programáticamente es extremadamente útil, ya que hacer esto a mano cuando hay cientos o miles de restricciones involucradas sería muy propenso a errores.

Variables

Las variables contienen datos que no son señales y son mutables. Aquí hay un ejemplo de una declaración de variable fuera de un bucle:

Copy
template VariableExample(n) {
  var acc = 2;
  signal s;
}

• Por defecto, las variables no forman parte del sistema de restricciones R1CS.
  • En breve veremos que las variables se pueden usar como constantes aditivas o multiplicativas dentro del R1CS.
• Las variables se utilizan para calcular valores fuera del R1CS para ayudar a definir el R1CS.
• Al trabajar con variables, Circom se comporta como un lenguaje de programación normal.
• Las operaciones matemáticas se realizan módulo p. La lista completa de operadores se proporciona en la documentación de Circom aquí. Estos te resultarán familiares si vienes de un lenguaje tipo C (por ejemplo, ++, **, <=, etc.). Sin embargo, ten en cuenta que / significa multiplicación por el inverso multiplicativo, y \ significa división entera.
• Sin embargo, los únicos operadores válidos para las señales son +, *, ===, <-- y <==. Discutiremos <-- y <== en un artículo posterior.

Sentencias if

Circom nos permite crear restricciones condicionalmente usando sentencias if, pero estas condiciones deben ser deterministas y conocidas en tiempo de compilación. A continuación se muestra un ejemplo:

Ejemplo: Imponer igualdad en los índices pares

Supongamos que tenemos dos arrays. Podríamos usar la siguiente plantilla para generar restricciones que exijan que los elementos en los índices pares sean iguales (sin comprobar los impares)

Copy
template EqualOnEven(n) {
  signal input in1[n];
  signal input in2[n];
  
  for (var i = 0; i < n; i++) {
    if (i % 2 == 0) {
      in1[i] === in2[i];
    }
    // otherwise no constraint is generated
  }
}

Nota que la variable i dicta qué restricciones se generan.

Las señales no se pueden usar para condiciones de bifurcación en sentencias if o bucles for

El siguiente código no está permitido porque la señal a se usa como condicional para la sentencia if:

Copy
template IfStatementViolation() {
  signal input a;
  signal input b;
  
  if (a == 2) {
    b === 3;
  }
  else {
    b === 4;
  }
}

En un Rank 1 Constraint System, solo puede haber sumas y multiplicaciones entre señales. Circom es solo una capa fina (wrapper) sobre un Rank 1 Constraint System. Por lo tanto, no puede “traducir” una sentencia if a sumas y multiplicaciones.

Todavía es posible hacer una operación condicional (sentencia if) basada en señales en Circom — este es el tema de un capítulo posterior. Pero por ahora, considera que no hay una traducción “directa” de una sentencia if a una sola multiplicación.

Uso de variables como parte de las restricciones

Las variables pueden usarse como parte de las restricciones. En el ejemplo a continuación, imponemos que el array de entrada in[n] sea una secuencia de Fibonacci. Nota que la sintaxis para un array de variables es var varName[size]:

Copy
template IsFib(n) {
  assert(n > 1);
  
  signal input in[n];
  
  // generate the Fibonacci sequence
  var correctFibo[n];
  correctFibo[0] = 0;
  correctFibo[1] = 1;

  for (var i = 2; i < n; i++) {
    correctFibo[i] = correctFibo[i - 1] + correctFibo[i - 2];
  }
  

  // assert that the input is a Fibonacci sequence
  for (var i = 0; i < n; i++) {
    in[i] === correctFibo[i];
  }
}

A tener en cuenta:

• El assert(n > 1) no genera ninguna restricción. Evita que la plantilla sea instanciada si no se cumple la condición para el parámetro de la plantilla.
• Podemos imponer que una señal tenga un valor determinado haciendo signal === var. Esto es lo mismo que hacer signal === 5 o alguna otra constante.

Circom no tiene una palabra clave Constant

En su lugar, podemos usar variables para asignar un nombre a un número mágico con el fin de mejorar la legibilidad. Por ejemplo:

Copy
template Equality() {
  signal input in[2];
  
  var left = 0;
  var right = 1;
  
  // require the inputs
  // to be equal
  in[left] === in[right];
}

Las variables pueden sumarse y multiplicarse por otras señales

En Circom, las variables pueden sumarse o multiplicarse por señales, al igual que las constantes. En el ejemplo a continuación, requerimos que in2[] sea in1[] multiplicado por su índice.

Por ejemplo, si in1[] = [3,5,6] entonces debe darse el caso de que in2[] = [0,5,12] porque [3,5,6] se multiplica elemento por elemento por [0,1,2].

Copy
template IsIndexMultiplied(n) {
  signal input in1[n];
  signal input in2[n];
  
  for (var i = 0; i < n; i++) {
    in1[i] * i === in2[i];
  }
}

component main = IsIndexMultiplied(3);

/* INPUT = {"in1": [0,1,2], "in2": [0,1,4]} */

// accept
// in1[] = [0,1,2]
// in2[] = [0,1,4]

// reject
// in1[] = [0,1,2]
// in2[] = [0,0,2]

Puedes probar el código aquí.

Puntos clave

• Internamente, si las variables se suman o multiplican con una señal, la variable se compila como una constante en el R1CS.
• Para las señales, no está permitido hacer otras operaciones más que suma, resta o multiplicación porque un R1CS solo puede tener suma o multiplicación con una constante. La resta, internamente, es simplemente una suma con el inverso aditivo.
• Si una señal se divide por una constante (o una variable que contiene una constante), multiplicará esa señal por el inverso multiplicativo de la constante a menos que la constante sea 0, en cuyo caso el código no compilará.

Problemas de práctica

Prueba los siguientes problemas de ZK Puzzles. Ejecuta las pruebas para comprobar tu respuesta.

• https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/AllBinary/AllBinary.circom
• https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/MultiANDNoOut/MultiANDNoOut.circom
• https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/IncreasingDistance/IncreasingDistance.circom