为何Circom中加法未生成约束，乘法却生成非线性约束？

我编写了一个输出两输入之和的简单Circom电路：

pragma circom 2.1.4;

template Add() {
   signal input a, b;
   signal output c;

   c <== a + b;
}

component main  = Add();

使用以下命令编译该电路：

circom Add.circom --r1cs --sym --wasm

得到的编译结果如下：

template instances: 1
non-linear constraints: 0
linear constraints: 0
public inputs: 0
private inputs: 2 (none belong to witness)
public outputs: 1
wires: 2
labels: 4
Written successfully: ./Add.r1cs
Written successfully: ./Add.sym
Written successfully: ./Add_js/Add.wasm
Everything went okay

但奇怪的是，这个加法表达式没有生成任何线性或非线性约束。当我把加法改为乘法（即c <== a*b）时，Circom的编译输出里却包含了1个非线性约束：

template instances: 1
non-linear constraints: 1
linear constraints: 0
public inputs: 0
private inputs: 2
public outputs: 1
wires: 4
labels: 4
Written successfully: ./Add.r1cs
Written successfully: ./Add.sym
Written successfully: ./Add_js/Add.wasm
Everything went okay

这是为什么？

原因解析 #

Circom的约束生成逻辑和信号赋值方式直接相关：

• 加法场景：c <== a + b属于直接赋值，Circom会在生成witness时直接计算c的取值为a + b，这个关系是确定的，不需要额外生成约束来验证——c只是a和b的组合结果，没有引入需要零知识证明的新关系，所以不会统计线性约束。
• 乘法场景：c <== a*b是需要约束验证的非线性关系，乘法无法通过直接赋值让witness生成器自行推导，必须生成一个非线性约束c - a*b = 0来强制验证c确实等于a与b的乘积，因此编译时会统计出1个非线性约束。

额外说明：如果想让加法生成线性约束，可以改用约束赋值语法 c === a + b，此时Circom会生成对应的线性约束c - a - b = 0，编译结果里的线性约束数量会变为1。

内容的提问来源于stack exchange，提问作者wannik