在 Circom 中，符号变量（symbolic variable）是指被赋予了信号（signal）值的变量。

当一个信号被赋值给一个变量时（从而将其转化为符号变量），该变量就成为了这个信号以及对其应用的任何算术运算的容器。符号变量使用 var 关键字声明，就像其他普通变量一样。

例如，以下两个电路是等效的，即它们生成相同的底层 R1CS：

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

在 ExampleB 中，符号变量 v 仅仅是表达式 a * b 的占位符。ExampleA 和 ExampleB 都被编译为完全相同的 R1CS，它们之间在功能上没有任何区别。

符号变量的用例

检查 $\sum\texttt{in}[i]=\texttt{sum}$

如果我们想在循环中对一个信号数组求和，符号变量会非常方便。事实上，在循环中对信号求和是它们最常见的用例：

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

检查 in 是否为 k 的有效二进制表示

一个更有趣的例子是，在模板化参数 n 的情况下，证明 in[n] 是 k 的二进制表示。在下面的电路中，我们检查：

如果 in 中的所有信号都被约束为 $\set{0,1}$，那么这就意味着 in[] 是 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;
}

为什么符号变量很有用

考虑前面证明 $\sum\texttt{in}[i]=\texttt{sum}$ 的例子。如果没有符号变量，要表达以下逻辑会非常笨拙：

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

特别是当我们事先不知道 n 是多少时。即使 n 是固定的（比如说 32），实际上手动输入 32 个变量也会相当麻烦。因此，符号变量使我们能够增量式地构造 in[0] + in[1] + in[2] + ...，而无需显式地将所有信号都写出来。

包含符号变量的非二次约束

因为符号变量可以“包含”两个信号之间的乘法，如果不小心，它们可能会导致在一个约束中嵌入了两个乘法运算。考虑以下无法编译的例子：

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

在上面的代码中，符号变量 v 内部包含一个乘法，并且我们声明了 v == a*b。因此，约束 v === c * d; 等效于 a * b = c * d;。所以，上述代码将无法编译。

非符号变量允许使用任意运算符

对于（非符号）变量，允许执行计算取模或位移等操作。然而，这意味着该变量不能再用作约束的一部分：

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

上面的例子可以通过编译，因为 v 没有被用在约束中。然而，如果我们把 v 用在约束中，代码将无法编译。下面展示了一个相关示例：

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

符号变量不能用于决定循环边界或条件

类似地，只有常规变量才能用来决定循环的边界或 if 语句的条件。如果使用了符号变量，则代码将无法编译：

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

总结

符号变量是被赋予了信号值的变量。它们最常用于将可参数化数量的信号加在一起，因为总和可以在 for 循环中累加。它们实际上是一个“容器”或“桶”，用于存放单个信号，或者存放相加、相乘在一起的一组信号。如果一个变量从未被赋予过信号值，那么它就不是符号变量。

由于符号变量包含信号，在使用它们时必须小心，以避免违反二次约束。