关于circom生成约束的一个疑问

[timimm]

Background

最近在使用 circom 编写电路时观察 circom 编译器输出的约束数目时产生了一些疑惑

Question

1. For循环

在之前的学习中，了解到 for 循环在 circom 语言中作为语法糖可以让 var 压缩多个 signal 的运算，最后生成约束时会展开成 signal 的形式，比如：

template Example () {
    signal input a[5];
    signal input b;
    
    var sum;
    for (var i = 0; i < 5; i++) {
        sum += a[i];
    }
    b === sum;
}

component main = Example();

/* INPUT = {
    "a": ["1", "2", "3", "4", "5"],
    "b": "15"
} */

但是观察circom编译器的输出，为：

template instances: 1
non-linear constraints: 0
linear constraints: 0
public inputs: 0
public outputs: 0
private inputs: 6
private outputs: 0
wires: 1
labels: 7

发现这里没有生成任何约束，但是如果我把 b 改成其他任意值，会触发断言错误。
请教大佬们，为啥这里输出的约束数量为0？【预期是线性约束为1】

我的思考

参考文章
根据上面的参考文章，circom编译器在处理非二次操作时，不生成任何约束。取而代之的是，对非二次操作的 <== 和 === 会在生成witness步骤中进行断言，这是一种不涉及约束系统的另类“约束”。这样的方式的目的：减少约束数目。

2. 未使用signal的处理

在circom开发中，对于未使用到的signal往往也要做约束处理，参考0xPARC的漏洞归类。

这里我做了一个小实验，我把未使用的signal的约束从二次约束（即平方）修改为线性约束。这样的话circom编译器就不会对其进行生成约束。正如0xparc文章所述，我可以由此生成任意的证明。

那么我对此的问题是：为什么这里不会跟问题1一样由于断言而无法生成证明呢？