Una variable simbólica en Circom es una variable a la que se le han asignado valores provenientes de una señal.

Cuando se asigna una señal a una variable (convirtiéndola así en una variable simbólica), la variable se convierte en un contenedor para esa señal y para cualquier operación aritmética que se le aplique. Una variable simbólica se declara utilizando la palabra clave var, al igual que otras variables.

Por ejemplo, los siguientes dos circuitos son equivalentes, es decir, producen el mismo R1CS subyacente:

Copy
template ExampleA() {
	signal input a;
	signal input b;
	signal input c;
	
	a * b === c;
}

template ExampleB() {
	signal input a;
	signal input b;
	signal input c;
	
	// symbolic variable v "contains" a * b
	var v = a * b;
	
	// a * b === c under the hood
	v === c;
}

En ExampleB, la variable simbólica v es simplemente un marcador de posición para la expresión a * b. Tanto ExampleA como ExampleB se compilan utilizando exactamente el mismo R1CS, y no hay ninguna diferencia funcional entre ellos.

Casos de uso de las variables simbólicas

Comprobar que $\sum\texttt{in}[i]=\texttt{sum}$

Las variables simbólicas son extremadamente útiles si queremos sumar un array de señales en un bucle. De hecho, sumar señales en un bucle es su caso de uso más común:

Copy
// assert sum of in === sum
template Sum(n) {
	signal input in[n];
	signal input sum;
	
	var accumulator;
	for (var i = 0; i < n; i++) {
		accumulator += in[i];
	}
	
	// in[0] + in[1] + in[2] + ... + in[n - 1] === sum
	accumulator === sum;
}

Comprobar que in es una representación binaria válida de k

Un ejemplo más interesante es demostrar que in[n] es la representación binaria de k para un valor parametrizado de n. En el siguiente circuito, comprobamos que:

Si todas las señales en in están restringidas a ser $\set{0,1}$, entonces eso implica que in[] es la representación binaria de k:

Copy
template IsBinaryRepresentation(n) {

	signal input in[n];
	signal input k;
	
	// in is binary only
	for (var i = 0; i < n; i++) {
		in[i] * (in[i] - 1) === 0;
	}
	
	// in is the binary representation of k
	var acc; // symbolic variable
	var powersOf2 = 1; // regular variable
	for (var i = 0; i < n; i++) {
		acc += powersOf2 * in[i];
		powersOf2 *= 2;
	}
	
	acc === k;
}

Por qué son útiles las variables simbólicas

Consideremos el ejemplo anterior de demostrar que $\sum\texttt{in}[i]=\texttt{sum}$. Sin variables simbólicas, resulta muy engorroso expresar

Copy
sum === in[0] + in[1] + in[2] + ... + in[n-1];

si no sabemos de antemano cuál es el valor de n. Incluso si n fuera fijo, digamos en 32, escribir a mano las 32 variables resultaría molesto. Por lo tanto, las variables simbólicas nos permiten construir incrementalmente in[0] + in[1] + in[2] + ... sin escribir explícitamente las señales.

Restricciones no cuadráticas con variables simbólicas

Debido a que las variables simbólicas pueden “contener” una multiplicación entre dos señales, si no tenemos cuidado, pueden llevar a incorporar dos multiplicaciones en una sola restricción. Consideremos el siguiente ejemplo, que no compilará:

Copy
template QViolation() {
	signal input a;
	signal input b;
	signal input c;
	signal input d;
	
	// v "contains" a * b
	var v = a * b;
	
	// error: there are two
	// multiplications
	// in this constraint
	v === c * d;
}

En el código anterior, la variable simbólica v tiene una multiplicación en su interior y declaramos v == a*b. Por lo que la restricción v === c * d; es equivalente a a * b = c * d;. Por ende, el código anterior no compilará.

Se permiten operadores arbitrarios con variables no simbólicas

Realizar operaciones como calcular el módulo o desplazamientos de bits (bitshifting) está permitido con variables (no simbólicas). Sin embargo, esto significa que la variable ya no se puede usar como parte de una restricción:

Copy
// this has no constraints
// but it will compile
template Ok() {
	signal input a;
	signal input b;
	
	var v = a % b;
}

El ejemplo anterior compilará porque v no se utiliza en una restricción. Sin embargo, si usamos v en una restricción, el código no compilará. A continuación se muestra un ejemplo de esto:

Copy
template NotOk() {
	signal input a;
	signal input b;
	signal input c;
	
	var v = a % b;
	
	// non-quadratic constraint
	c === v;
}

Las variables simbólicas no se pueden utilizar para determinar el límite de un bucle o una condición

De forma similar, solo se pueden utilizar variables regulares para determinar el límite de un bucle o la condición de una sentencia if. Si se utiliza una variable simbólica, el código no compilará:

Copy
template NotOk() {
	signal input a;
	signal input b;
	signal input c;
	
	var v = a * b;
	
	// v is a symbolic variable
	// used in an if statement
	if (v == 0) {
		c === 0;
	} else {
		c === 1;
	}
}

Resumen

Las variables simbólicas son variables a las que se les ha asignado un valor proveniente de una señal. Se usan con mayor frecuencia para sumar un número parametrizable de señales, ya que la suma se puede acumular en un bucle for. Efectivamente, son un “contenedor” o “cubo” que contiene una sola señal o una colección de señales que se suman o multiplican entre sí. Si a una variable nunca se le asigna un valor proveniente de una señal, entonces no es una variable simbólica.

Dado que las variables simbólicas contienen señales, se debe tener cuidado para evitar violaciones de restricciones cuadráticas al utilizarlas.