Symbolic Variables in Circom

A symbolic variable in Circom is a variable that has been assigned values from a signal.

When a signal is assigned to a variable (thereby turning it into a symbolic variable), the variable becomes a container for that signal and for any arithmetic operations applied to it. A symbolic variable is declared using the var keyword, just like other variables.

For example, the following two circuits are equivalent, i.e. they produce the same underlying R1CS:

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;
}

In ExampleB, the symbolic variable v is simply a placeholder for the expression a * b. Both ExampleA and ExampleB are compiled using the exact same R1CS, and there is zero functional difference between them.

Use cases of symbolic variables

Checking That $\sum\texttt{in}[i]=\texttt{sum}$

Symbolic variables are extremely handy if we want to sum up an array of signals in a loop. In fact, summing signals in a loop is their most common use case:

// 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;
}

Checking That in Is a Valid Binary Representation of k

A more interesting example is proving that in[n] is the binary representation of k for a templated value of n. In the circuit below, we check that:

If all the signals in in are constrained to be $\set{0,1}$, then that implies in[] is the binary representation of k:

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;
}

Why symbolic variables are helpful

Consider the earlier example of proving that $\sum\texttt{in}[i]=\texttt{sum}$. Without symbolic variables, it’s very clumsy to express

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

if we don’t know what n is in advance. Even if n was fixed, say at 32, actually typing out 32 variables by hand would be annoying. Thus, symbolic variables enable us to incrementally construct in[0] + in[1] + in[2] + ... without explicitly writing out the signals.

Non quadratic Constraints With Symbolic Variables

Because symbolic variables can “contain” a multiplication between two signals, they can lead to embedding two multiplications into one constraint if we aren’t careful. Consider the following example, that will not compile:

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;
}

In the code above, the symbolic variable v has one multiplication in it and we declared v == a*b. So the constraint v === c * d; is equivalent to a * b = c * d;. Hence, the above code will not compile.

Arbitrary operators are allowed with non-symbolic variables

Doing operations like computing the modulo or bitshifting are allowed with (non-symbolic) variables. However, this means that the variable can no longer be used as part of a constraint:

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

The above example will compile because v is not used in a constraint. However, if we use v in a constraint, the code will not compile. An example of this is shown below:

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

Symbolic variables cannot be used to determine the boundary of a loop or the condition

Similarly, only regular variables can be used to determine the boundary of a loop or the condition of an if statement. If a symbolic variable is used, then the code will not compile:

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;
	}
}

Summary

Symbolic variables are variables that were assigned a value from a signal. They are most frequently used for adding a parameterizable number of signals together, as the sum can be accumulated in a for loop. They are effectively a “container” or “bucket” that holds either a single signal or a collection of signals that are added or multiplied together. If a variable is never assigned a value from a signal, then it is not a symbolic variable.

Since symbolic variables contain signals, care must be taken to avoid quadratic constraint violations when using them.