Circom es muy estricto con el uso de las sentencias if. Se deben seguir las siguientes reglas:

• Las señales no pueden usarse para alterar el comportamiento de una sentencia if.
• No se le puede asignar un valor a una señal dentro de una sentencia if.

El siguiente circuito de ejemplo demuestra ambas violaciones:

Copy
template Foo() {

  signal input in;
  signal input cond;
  
  signal output out;
  
  // if-statements cannot depend on 
  // values not known at compile time
  if (in == 3) {
    // assigning a value inside an if-statement
    // whose value is unknown at compile time
    // is not allowed
    out <== 4;
  }
}

Las sentencias if son aceptables si no se ven afectadas por ninguna señal y si no afectan a ninguna señal.

Efectivamente, no forman parte del Rank 1 Constraint system (R1CS) subyacente.

Por ejemplo, si quisiéramos calcular el valor máximo en una lista (sin generar restricciones), podemos usar la siguiente solución típica, la cual Circom acepta ya que no hay señales involucradas:

Copy
var max;
for (var i = 0; i < n; i++) {
  if (arr[i] > max) {
    max = arr[i];
  }
}

Este cálculo no crea restricciones, es simplemente por conveniencia.

Ramificación en Circom

Podría parecer que Circom es incapaz de realizar ramificaciones condicionales, pero este no es el caso. Para crear ramas condicionales en Circom, se deben ejecutar todas las ramas de una sentencia, multiplicando las ramas ‘no deseadas’ por cero y la rama ‘correcta’ por uno.

Ejemplo de un cálculo con ramas

Supongamos que estamos modelando el siguiente cálculo:

Copy
def foo(x):

  if x == 5:
    out = 14
  elif x == 9:
    out = 22
  elif x == 10:
    out = 23
  else
    out = 45
    
  return out

Al no haber un vínculo matemático claro entre x y out, lo mejor es modelar este condicional de la forma más directa posible. Así es como describimos matemáticamente la sentencia condicional:

• x_eq_5 es igual a 1 si x es igual a 5, y cero en caso contrario, lo cual se puede lograr con IsEqual()([x, 5])
• x_eq_9 es igual a 1 cuando x es igual a 9, y cero en caso contrario
• x_eq_10 es igual a 1 cuando x es igual a 10, y cero en caso contrario
• otherwise es igual a 1 cuando todos los anteriores (x_eq_5, x_eq_9, x_eq_10) son 0.

Podemos asignar los valores a las señales x_eq_5, x_eq_9, x_eq_10 y otherwise utilizando el template IsEqual() de Circomlib — esto también forzará que sean 0 o 1. Para garantizar que exactamente una señal sea 1 y el resto sean ceros, utilizamos la siguiente restricción:

En general, creamos “interruptores binarios” que valen 1 cuando una rama en particular está activa y 0 en caso contrario. Luego, sumamos la evaluación de todas las ramas, cada una multiplicada por su interruptor.

Dado que solo una rama de $\texttt{out = }...$ estará activa, el resto de las evaluaciones se multiplican por 0 y por lo tanto no importan.

Aquí está el circuito completo:

Copy
include "./node_modules/circomlib/circuits/comparators.circom";

template MultiBranchConditional() {
  signal input x;
  
  signal output out;
  
  signal x_eq_5;
  signal x_eq_9;
  signal x_eq_10;
  signal otherwise;
  
  x_eq_5 <== IsEqual()([x, 5]);
  x_eq_9 <== IsEqual()([x, 9]);
  x_eq_10 <== IsEqual()([x, 10]);
  otherwise <== IsZero()(x_eq_5 + x_eq_9 + x_eq_10);
  
  signal branches_5_9;
  signal branches_10_otherwise;
  
  branches_5_9 <== x_eq_5 * 14 + x_eq_9 * 22;
  branches_10_otherwise <== x_eq_10 * 23 + otherwise * 45;
  
  out <== branches_5_9 + branches_10_otherwise;
}

component main = MultiBranchConditional();

Para que nuestro código sea más limpio, sería mejor colocar la ramificación de cuatro vías como un componente separado — de esa manera, podemos reutilizar el template de ramificación.

Copy
include "./node_modules/circomlib/circuits/comparators.circom";

template Branch4(cond1, cond2, cond3, branch1, branch2, branch3, branch4) {
  signal input x;
  signal output out;
  
  signal switch1;
  signal switch2;
  signal switch3;
  signal otherwise;
  
  switch1 <== IsEqual()([x, cond1]);
  switch2 <== IsEqual()([x, cond2]);
  switch3 <== IsEqual()([x, cond3]);
  otherwise <== IsZero()(switch1 + switch2 + switch3);
  
  signal branches_1_2 <== switch1 * branch1 + switch2 * branch2;
  signal branches_3_4 <== switch3 * branch3 + otherwise * branch4;
  
  out <== branches_1_2 + branches_3_4;
}

template MultiBranchConditional() {
  signal input x;
  
  signal output out;
  
  component branch4 = Branch4(5,9,10,14,22,23,45);
  
  branch4.x <== x;
  branch4.out ==> out; // same as out <== branch4.out
}

component main = MultiBranchConditional();

Código cuando hay muchas ramas involucradas

En el código anterior, tuvimos que escribir explícitamente switch1, switch2,…, otherwise, lo cual podría ser muy tedioso si el código tiene muchas ramas.

En su lugar, podríamos pensar en nuestro cálculo como el producto interno (producto escalar generalizado) de los interruptores y las ramas:

Esta formulación anterior asegura que exactamente un interruptor esté activo (igual a 1), mientras que todos los demás son 0, haciendo que la rama correspondiente sea la salida.

Para implementar esto de manera eficiente en Circom, utilizamos el template EscalarProduct de multiplexer.circom . Este template toma dos vectores de longitud n, los multiplica elemento por elemento y suma el resultado. En el siguiente bloque de código, usamos EscalarProduct para multiplicar cada interruptor por cada rama. Tenga en cuenta que el interruptor y la rama final se manejan de manera ligeramente diferente porque la condición final es una sentencia else general (“catch-all”).

Copy
include "./node_modules/circomlib/circuits/comparators.circom";
include "./node_modules/circomlib/circuits/multiplexer.circom";

template BranchN(n) {
  assert(n > 1); // too small

  signal input x;

  // conds n - 1 is otherwise
  signal input conds[n - 1];
  
  // branch n - 1 is the otherwise branch
  signal input branches[n];
  signal output out;
  
  signal switches[n];
  
  component EqualityChecks[n - 1];
  
  // only compute IsEqual up to the second-to-last switch
  for (var i = 0; i < n - 1; i++) {
    EqualityChecks[i] = IsEqual();
    
    EqualityChecks[i].in[0] <== x;
    EqualityChecks[i].in[1] <== conds[i];
    switches[i] <== EqualityChecks[i].out;
  }
  
  // check the last condition
  var total = 0;
  for (var i = 0; i < n - 1; i++) {
    total += switches[i];
  }
  
  // if none of the first n - 1 switches
  // are active, then `otherwise` must be 1
  switches[n - 1] <== IsZero()(total);
  
  component InnerProduct = EscalarProduct(n);
  for (var i = 0; i < n; i++) {
    InnerProduct.in1[i] <== switches[i];
    InnerProduct.in2[i] <== branches[i];
  }
  
  out <== InnerProduct.out;
}

template MultiBranchConditional() {
	signal input x;
	
	signal output out;
	
	component branchn = BranchN(4);

  var conds[3] = [5, 9, 10];
  var branches[4] = [14, 22, 23, 45];
  for (var i = 0; i < 4; i++) {
    if (i < 3) {
        branchn.conds[i] <== conds[i];
    }
    
    branchn.branches[i] <== branches[i];
  }

  branchn.x <== x;
  branchn.out ==> out; // same as out <== branch4.out
}

component main = MultiBranchConditional();

¿Cuándo está bien usar sentencias if?

Supongamos que quisiéramos crear un template que devuelva un circuito completamente diferente dependiendo del parámetro del circuito. Por ejemplo, si estamos creando un componente Max que toma un arreglo in[n] y devuelve el máximo, sería más eficiente simplemente devolver el elemento 0 del índice si n es igual a 1.

A continuación, mostramos un ejemplo de un uso válido de la sentencia if cuando se usa con la definición de restricciones. Aquí, la sentencia if se ejecuta en tiempo de compilación, por lo que el template producirá un circuito bien definido:

Copy
include "./node_modules/circomlib/circuits/comparators.circom";

template Max(n) {
  signal input in[n];
  signal output out;
  
  assert(n > 0);

  if (n == 1) {
    out <== in[0];
  }
  
  // it is okay to declare signals inside
  // the if-statement because the evaluation
  // of the if-statement is known at compile time
  else if (n == 2) {
    signal zeroGtOne;
    signal branch0;
    signal branch1;

    zeroGtOne <== GreaterThan(252)([in[0], in[1]]);
    branch0 <== zeroGtOne * in[0];
    branch1 <== (1 - zeroGtOne) * in[1];
    
    out <== branch0 + branch1;
  }
  else {
    // case for n > 2
  }
}

component main = Max(2);

Las sentencias condicionales no son amigables con ZK

Una implicación clave de diseño es que cada condición en un circuito de Circom duplica su tamaño ya que las ramas no pueden ser “cortocircuitadas”. A diferencia de la programación tradicional, se calculan todas las ramas.

Al usar ZK para probar un cálculo, queremos optimizar para:

1. Tener la menor cantidad de ramas posible, ya que cada rama aumenta el trabajo del probador (prover).
2. Minimizar el costo computacional total en todas las ramas, no solo el cálculo esperado basado en la probabilidad de una rama.
3. Evitar las sentencias condicionales siempre que sea posible.