#3.1 Symbolic Variables

When variables was introduced in chapter 2, we stated they ought to be treated normally like in any other programming language. In this article we going to illustrate the exception to this statement.

Consider the following circuit:

templage Mul3() {

		signal input a;
		signal input b;
		signal input c;
		signal input res;

		// not allowed
		res === a * b * c;
} 

// this circuit will not compile 
component main = Mul3();

From the earlier chapter outlining quadratic constraints, the reader ought to know that this circuit will not compile, as there are two multiplicative operators involving signals in the same constraint definition.

It might occur to the reader that we could instead use variables to circumvent this requirement, like so:

template Mul3() {

		signal input a;
		signal input b;
		signal input c;
		signal input res;

		var prod;
		
		// seemingly quadratic expressions
		prod = a * b;
		prod = prod * c;
		
		res === prod;
}

// this circuit will not compile 
component main = Mul3();

• Declare a variable prod and use it to calculate a * b * c.

• Constraint res against the the value of prod.

However, this circuit will yet again, fail to compile.

• It may seem like prod stores the final result; instead prod holds the full expression a * b * c.

• This results in the non-quadratic constraint: res === a * b * c, which is not allowed.

Usage of variables as in the manner above to flatten non-quadratic expressions will not work. The reader might be confused, given the prior explanation of variables in article 2. Let us clarify.

Cannot use variables to flatten non-quadratic signal expressions

When variables are used in signal operations, like the one above, they do not "flatten" the signal operations. Instead, they will hold the entire expression.

• variables which involve signal operations, will hold the entire expression.

• variables which do not involve signal operations can be treated normally.

The reader would be left with 2 questions:

1. How do we reduce non-quadratic constraints into quadratic ones?

By using intermediate signals which will be explained in the next chapter.

1. How is this mechanics with variables prove to be useful?

We examine this in the next section.

Symbolic variables store symbolic expressions

 template SumSeries(n) {

	 // inputs
	 signal input total;
	 signal input in[n];

	 ****var sum = 0;
			 
	 for(var i=0; i<n; i++) {
		 sum = sum + in[i];
	 }
	 
	 sum === total;
 
 }
 
 
 component main = SumSeries(4);

• circuit verifies that the sum of a series was known and computed correctly

• inputs: series as an array, and computed sum

Circuit has two variables: i and sum

• i is a regular variable used in the for loop

• sum is a symbolic variable that is used to create a constraint in which we add up the values of the n input signals.

At the end of the loop, sum is used to generate the constraint:

sum === total 

in[0] + in[1] + ... + in[n-1] === total