Circom 中的条件语句

Circom 对 if 语句的使用非常严格。必须遵守以下规则：

• 信号不能用于改变 if 语句的行为。
• 不能在 if 语句内部给信号赋值。

下面的示例电路演示了这两种违规情况：

template Foo() {

  signal input in;
  signal input cond;

  signal output out;

  // if 语句不能依赖于
  // 编译时未知的值
  if (in == 3) {
    // 在 if 语句内部赋值
    // 其值在编译时未知
    // 是不允许的
    out <== 4;
  }
}

如果 if 语句不受任何信号的影响，也不影响任何信号，那么它们是可以接受的。

实际上，它们不是底层 Rank 1 Constraint system (R1CS) 的一部分。

例如，如果我们想计算列表中的最大值（而不生成约束），我们可以使用以下典型解决方案，Circom 可以接受，因为不涉及任何信号：

var max;
for (var i = 0; i < n; i++) {
  if (arr[i] > max) {
    max = arr[i];
  }
}

此计算不会创建任何约束，它仅仅是为了方便。

Circom 中的分支

可能看起来 Circom 无法进行条件分支，但事实并非如此。要在 Circom 中创建条件分支，必须执行语句的所有分支，将“不需要的”分支乘以零，将“正确的”分支乘以一。

带有分支的计算示例

假设我们正在对以下计算进行建模：

def foo(x):

  if x == 5:
    out = 14
  elif x == 9:
    out = 22
  elif x == 10:
    out = 23
  else
    out = 45

  return out

由于 x 和 out 之间没有明确的数学联系，因此最好尽可能直接地对该条件进行建模。以下是我们如何用数学方式描述条件语句：

out=x\_eq\_5⋅14+x\_eq\_9⋅22+x\_eq\_10⋅23+otherwise⋅45

• 如果 x 等于 5，则 x_eq_5 等于 1，否则等于零，这可以通过 IsEqual()([x, 5]) 实现
• 当 x 等于 9 时，x_eq_9 等于 1，否则等于零
• 当 x 等于 10 时，x_eq_10 等于 1，否则等于零
• 当以上所有条件（x_eq_5、x_eq_9、x_eq_10）都为 0 时， otherwise 等于 1。

我们可以使用 Circomlib 中的 IsEqual() 模板将值分配给信号 x_eq_5、x_eq_9、x_eq_10 和 otherwise —— 这也将强制它们为 0 或 1。为了确保只有一个信号为 1，其余信号为零，我们使用以下约束：

1===x\_eq\_5+x\_eq\_9+x\_eq\_10+otherwise

一般来说，我们创建“二进制开关”，当特定分支处于活动状态时，该开关为 1，否则为 0。然后，我们将所有分支的评估结果相加，每个分支都乘以其开关。

由于只有一个 out = … 分支会处于活动状态，因此其余的评估结果都乘以 0，因此无关紧要。

以下是完整的电路：

include "./node_modules/circomlib/circuits/comparators.circom";

template MultiBranchConditional() {
  signal input x;

  signal output out;

  signal x_eq_5;
  signal x_eq_9;
  signal x_eq_10;
  signal otherwise;

  x_eq_5 <== IsEqual()([x, 5]);
  x_eq_9 <== IsEqual()([x, 9]);
  x_eq_10 <== IsEqual()([x, 10]);
  otherwise <== IsZero()(x_eq_5 + x_eq_9 + x_eq_10);

  signal branches_5_9;
  signal branches_10_otherwise;

  branches_5_9 <== x_eq_5 * 14 + x_eq_9 * 22;
  branches_10_otherwise <== x_eq_10 * 23 + otherwise * 45;

  out <== branches_5_9 + branches_10_otherwise;
}

component main = MultiBranchConditional();

为了使我们的代码更简洁，最好将四向分支作为一个单独的组件——这样，我们可以重用分支模板。

include "./node_modules/circomlib/circuits/comparators.circom";

template Branch4(cond1, cond2, cond3, branch1, branch2, branch3, branch4) {
  signal input x;
  signal output out;

  signal switch1;
  signal switch2;
  signal switch3;
  signal otherwise;

  switch1 <== IsEqual()([x, cond1]);
  switch2 <== IsEqual()([x, cond2]);
  switch3 <== IsEqual()([x, cond3]);
  otherwise <== IsZero()(switch1 + switch2 + switch3);

  signal branches_1_2 <== switch1 * branch1 + switch2 * branch2;
  signal branches_3_4 <== switch3 * branch3 + otherwise * branch4;

  out <== branches_1_2 + branches_3_4;
}

template MultiBranchConditional() {
  signal input x;

  signal output out;

  component branch4 = Branch4(5,9,10,14,22,23,45);

  branch4.x <== x;
  branch4.out ==> out; // same as out <== branch4.out
}

component main = MultiBranchConditional();

涉及多个分支时的代码

在上面的代码中，我们必须显式地编写 switch1、switch2、…、otherwise，如果代码有很多分支，这可能会非常繁琐。

相反，我们可以将我们的计算视为开关和分支的内积（广义点积）：

out===⟨[switch1,switch2,…,switchn],[branch1,branch2,…,branchn]⟩=switch1⋅branch1+switch2⋅branch2+⋯+switchn⋅branchn1===switch1+switch2+…+switchn0===switchi∗(switchi−1),i = 1…n

以上公式确保只有一个开关处于活动状态（等于 1），而所有其他开关都为 0，从而使相应的分支成为输出。

为了在 Circom 中高效地实现这一点，我们使用了来自 multiplexer.circom 的 EscalarProduct 模板。 此模板接受两个长度为 n 的向量，将它们按元素相乘，然后对结果求和。 在下面的代码块中，我们使用 EscalarProduct 将每个开关乘以每个分支。 请注意，最后一个开关和分支的处理方式略有不同，因为最后一个条件是一个“包罗万象”的 else 语句。

include "./node_modules/circomlib/circuits/comparators.circom";
include "./node_modules/circomlib/circuits/multiplexer.circom";

template BranchN(n) {
  assert(n > 1); // too small

  signal input x;

  // conds n - 1 is otherwise
  signal input conds[n - 1];

  // branch n - 1 is the otherwise branch
  signal input branches[n];
  signal output out;

  signal switches[n];

  component EqualityChecks[n - 1];

  // only compute IsEqual up to the second-to-last switch
  for (var i = 0; i < n - 1; i++) {
    EqualityChecks[i] = IsEqual();

    EqualityChecks[i].in[0] <== x;
    EqualityChecks[i].in[1] <== conds[i];
    switches[i] <== EqualityChecks[i].out;
  }

  // check the last condition
  var total = 0;
  for (var i = 0; i < n - 1; i++) {
    total += switches[i];
  }

  // if none of the first n - 1 switches
  // are active, then `otherwise` must be 1
  switches[n - 1] <== IsZero()(total);

  component InnerProduct = EscalarProduct(n);
  for (var i = 0; i < n; i++) {
    InnerProduct.in1[i] <== switches[i];
    InnerProduct.in2[i] <== branches[i];
  }

  out <== InnerProduct.out;
}

template MultiBranchConditional() {
    signal input x;

    signal output out;

    component branchn = BranchN(4);

  var conds[3] = [5, 9, 10];
  var branches[4] = [14, 22, 23, 45];
  for (var i = 0; i < 4; i++) {
    if (i < 3) {
        branchn.conds[i] <== conds[i];
    }

    branchn.branches[i] <== branches[i];
  }

  branchn.x <== x;
  branchn.out ==> out; // same as out <== branch4.out
}

component main = MultiBranchConditional();

什么时候可以使用 if 语句？

假设我们想要创建一个模板，该模板根据电路参数返回一个完全不同的电路。例如，如果我们正在创建一个 Max 组件，该组件接受一个数组 in[n] 并返回最大值，如果 n 等于 1，那么简单地返回索引中的第 0 个项目会更有效率。

下面，我们展示了一个有效的 if 语句用例，当与定义约束一起使用时。在这里，if 语句在编译时执行，因此模板将生成一个定义明确的电路：

include "./node_modules/circomlib/circuits/comparators.circom";

template Max(n) {
  signal input in[n];
  signal output out;

  assert(n > 0);

  if (n == 1) {
    out <== in[0];
  }

  // 可以在内部声明信号
  // if 语句，因为评估
  // if 语句在编译时已知
  else if (n == 2) {
    signal zeroGtOne;
    signal branch0;
    signal branch1;

    zeroGtOne <== GreaterThan(252)([in[0], in[1]]);
    branch0 <== zeroGtOne * in[0];
    branch1 <== (1 - zeroGtOne) * in[1];

    out <== branch0 + branch1;
  }
  else {
    // case for n > 2
  }
}

component main = Max(2);

条件语句对 ZK 不友好

一个关键的设计意义是，Circom 电路中的每个条件都会使其大小加倍，因为分支不能“短路”。与传统编程不同，所有分支都会被计算。

当使用 ZK 来证明计算时，我们希望优化以下内容

1. 尽可能少的分支，因为每个分支都会增加证明者的工作量。
2. 最小化所有分支的总计算成本，而不仅仅是基于分支概率的预期计算。
3. 尽可能避免条件语句。

• 原文链接： rareskills.io/post/circo...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～