Circom循环中的组件

本文介绍了在 Circom 中如何在循环中使用组件。由于 Circom 不允许在循环中直接实例化组件,文章提供了通过预先声明组件数组并在循环内指定组件类型的方式来解决这一问题,并提供了三个实际案例:求数组最大值、检查数组是否已排序以及确保数组中所有元素都是唯一的,展示了如何在循环中有效地使用 Circom 组件,以及一些使用 circom 的小技巧。

Circom 不允许在循环中直接实例化组件。例如,编译以下代码会导致下面的错误。

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

template IsSorted(n) {
  signal input in[n];

  for (var i = 0; i < n; i++) {
    component lt = LessEqThan(252); // 这里出错
    lt.in[0] <== in[0];
    lt.in[1] <== in[1];
    lt.out === 1;
  }
}

component main = IsSorted(8);
Signal or component declaration inside While scope. Signal and component can only be defined in the initial scope or in If scopes with known condition
在 While 作用域内声明了信号或组件。信号和组件只能在初始作用域或具有已知条件的 If 作用域中定义。

解决办法是声明一个组件数组,但不指定组件类型:

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

template IsSorted(n) {

  signal input in[n];

  // 声明组件数组
  // 但不指定组件类型
  component lessThan[n];

  for (var i = 0; i < n - 1; i++) {
    lessThan[i] = LessEqThan(252); // 在循环中指定类型
    lessThan[i].in[0] <== in[i];
    lessThan[i].in[1] <== in[i+1];
    lessThan[i].out === 1;
  }
}

component main = IsSorted(8);

当以这种方式声明组件时,不可能像下面这样对信号进行“单行赋值”:

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

template IsSorted() {

  signal input in[4];
  signal leq1;  
  signal leq2;  
  signal leq3;  

  // 对信号进行单行赋值
  leq1 <== LessEqThan(252)([in[0], in[1]]);
  leq2 <== LessEqThan(252)([in[1], in[2]]);
  leq3 <== LessEqThan(252)([in[2], in[3]]);

  leq1 === 1;
  leq2 === 1;
  leq3 === 1;
}

component main = IsSorted();

在循环外,可以在单行上设置信号。然而,在循环内,我们必须用更多步骤写出赋值,就像我们在 lessThan[i] = LessEqThan(252); // 在循环中指定类型 中所做的那样。

例子 1:数组的最大值

为了说明在循环中声明组件的一个有用的例子,我们展示了如何证明 k 是一个数组的最大值。为此,我们需要约束 k 大于或等于每个其他元素,并且它等于至少一个元素。为了理解为什么等式检查是必要的,考虑一下 18 大于或等于 [7, 8, 15] 中的所有元素,但它不是该数组的最大值。

以下 Circom 代码计算数组的最大值而不生成约束。然后,它运行 nGreaterEqualThan 组件来约束提议的 max 值确实是最大值,并且还使用 IsEqual 组件的数组检查是否至少有一个元素等于 k

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

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

  // 这里没有约束,只是一个计算
  // 找到最大值

  var max = 0;
  for (var i = 0; i < n; i++) {
    max = in[i] > max ? in[i] : max;
  }

  signal maxSignal;
  maxSignal <-- max;

  // 对于数组中的每个元素,断言
  // max ≥ 该元素
  component GTE[n];
  component EQ[n];
  var acc;
  for (var i = 0; i < n; i++) {
    GTE[i] = GreaterEqThan(252);
    GTE[i].in[0] <== maxSignal;
    GTE[i].in[1] <== in[i];
    GTE[i].out === 1;

    // 这用于
    // 下面的代码块中,以确保
    // maxSignal 至少等于
    // 一个输入
    EQ[i] = IsEqual();
    EQ[i].in[0] <== maxSignal;
    EQ[i].in[1] <== in[i];

    // acc 大于零
    // (acc != 0) 如果 EQ[i].out
    // 至少等于 1 一次
    acc += EQ[i].out;
  }

  // 断言 maxSignal
  // 等于至少一个
  // 输入。如果 acc = 0,那么
  // 没有输入等于
  // maxSignal
  signal allZero;
  allZero <== IsEqual()([0, acc]);
  allZero === 0;
  out <== max;
}

component main = Max(8);

练习: 创建一个电路,其功能与上述相同,但针对 min

例子 2:数组已排序

我们可以通过检查每个元素是否小于或等于后续元素来断言数组已排序。与需要 n 个组件的先前示例不同,我们需要 n - 1 个组件,因为我们将相邻值相互比较。因为我们有 n 个元素,所以我们将进行 n - 1 次比较。

这是一个约束输入数组 in[n] 已排序的模板。请注意,如果一个数组只有一个元素,则根据定义它是排序的,并且下面的电路也与这种情况兼容:

pragma circom 2.1.6;

include "circomlib/comparators.circom";

template IsSorted(n) {
  signal input in[n];

  component lt[n - 1];

  // 循环到 n - 1,而不是 n
  for (var i = 0; i < n - 1; i++) {
    lt[i] = LessThan(252);
    lt[i].in[0] <== in[i];
    lt[i].in[1] <== in[i+1];
    lt[i].out === 1;
  }
}

component main = IsSorted(3);

例子 3:所有项都是唯一的

为了检查列表中所有项是否唯一,最直接的方法是使用哈希映射 —— 但哈希映射在算术电路中不可用。第二有效的方法是对列表进行排序,但在电路内部进行排序非常棘手,所以我们现在避免这样做。这给我们留下了将每个元素与其他每个元素进行比较的蛮力解决方案。这需要一个嵌套的 for 循环。

我们正在进行的计算可以如下图所示:

$$ \begin{array}{c|c|c|c|c|} &a_1&a_2&a_3&a_4\\ \hline a_1&&\neq&\neq&\neq\\ \hline a_2&&&\neq&\neq\\ \hline a_3&&&&\neq\\ \hline a_4\\ \hline \end{array} $$

一般来说,将会有

$$ \frac{n(n-1)}{2} $$

不等式检查,所以我们需要那么多组件。

我们展示了如何完成以下操作:

pragma circom 2.1.8;

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

template ForceNotEqual() {
  signal input in[2];

  component iseq = IsEqual();
  iseq.in[0] <== in[0];
  iseq.in[1] <== in[1];
  iseq.out === 0;
}

template AllUnique (n) {
  signal input in[n];

  // 下面的嵌套循环将运行
  // n * (n - 1) / 2 次
  component Fneq[n * (n-1)/2];

  // 从 0 循环到 n - 1
  var index = 0;
  for (var i = 0; i < n - 1; i++) {
    // 从 i + 1 循环到 n
    for (var j = i + 1; j < n; j++) {
      Fneq[index] = ForceNotEqual();
      Fneq[index].in[0] <== in[i];
      Fneq[index].in[1] <== in[j];
      index++;
    }
  }
}

component main = AllUnique(5);

总结

为了在循环中使用 Circom 组件,我们在循环外声明一个组件数组而不指定类型。

然后在循环内,我们声明组件并约束组件的输入和输出。

  • 原文链接: rareskills.io/post/circo...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
RareSkills
RareSkills
https://www.rareskills.io/