ZK中的32位仿真

ZK 中默认的数据类型是域元素，所有的算术运算都是在一个大素数的模下进行的。然而，大多数 “实际” 计算都是使用 32 位、64 位或 256 位的数字完成的，具体取决于虚拟机或执行环境。

为什么我们需要 32 位仿真？

许多密码学哈希函数都在 32 位字上运行，因为从历史上看，32 位是许多 CPU 的默认字长。后来增加到 64 位。EVM 使用 256 位，以便能够轻松地容纳 keccak256 哈希。

如果我们想使用 ZK 来证明传统哈希函数或某些不使用有限域的虚拟机（大多数都不使用）的正确执行，那么我们需要用一个域元素来 “建模” 传统的数据类型。因此，我们在 Circom 中使用一个域元素（信号）来保存一个不能超过 32 位数字可以保存的数字，即使该信号可以保存比 32 位大得多的值。

32 位字 vs 有限域元素

32 位字和有限域元素之间的关键区别在于它们溢出的点。在 Circom 中，或任何使用 bn128 曲线的语言中，溢出发生在 p 处，其中 p = 21888242871839275222246405745257275088548364400416034343698204186575808495617。在 32 位机器中，溢出发生在 4294967296，或者更一般地说，发生在 2n 处，其中 n 是虚拟机中的位数。

可以将 32 位虚拟机看作是以 232 为模进行所有算术运算。默认情况下，普通虚拟机在该数字处溢出。然而，当在有限域中进行模运算时，计算模 232 会增加相当多的约束（我们稍后会看到），但幸运的是，有一个有用的数学技巧可以有效地做到这一点。

以下两个函数在计算模 232 时是等效的：

contract DemoMod32 {
  function mod32(uint256 x) public pure returns (uint256) {
    return x % (2**32);
  }

  function mod32e(uint256 x) public pure returns (uint256) {
    // only keep the 32 least significant bits
    return uint256(uint32(x)); 
  }
}

我们可以通过仅保留 32 个最低有效位来计算 mod232。对此的形式化验证在附录中。在我们对包含 32 位数字的信号进行任何算术运算之前，我们首先需要完全确定该信号保存的数字实际上适合 32 位。

32 位范围检查

如果我们正在创建一个 ZK 电路，该电路使用 32 位字来模拟计算，那么我们需要确保没有信号保存大于或等于 232 的值。一个直观的做法是使用 LessThan 模板，如下所示：

signal safe;
safe <== LessThan(252)([x, 2**32]);
safe === 1;

但是，此电路创建的约束比必要的更多。

一种更有效的方法是利用二进制表示。关键思想是用 32 位编码一个数字，如果它适合 32 位，则电路正常执行。相反，如果该数字不适合 32 位，则无法满足约束。因此，下面的电路确保 in 是 232−1 或更小。

include "circomlib/comparators.circom";

// 8 bit range check
template RangeCheck() {
  signal input in;
  component n2b = Num2Bits(32);
  n2b.in <== in;
}

component main = RangeCheck();

// if in = 2**32 - 1, it will accept
// if in = 2**32 it will reject

没有必要像使用 LessThan 那样约束 Num2Bits 的输出，因为在内部，它已经将 out 约束为零或一，并且还约束二进制表示等于输入（通过 lc1 === in），这可以在下面的 Num2Bits 模板中看到：

template Num2Bits(n) {
    signal input in;
    signal output out[n];
    var lc1=0;

    var e2=1;
    for (var i = 0; i<n; i++) {
        out[i] <-- (in >> i) & 1;
        out[i] * (out[i] -1 ) === 0; // CONSTRAINT HAPPENS HERE
        lc1 += out[i] * e2;
        e2 = e2+e2;
    }

    lc1 === in;
}

32 位加法

假设我们想将两个域元素 x 和 y 相加，它们代表 32 位数字。

32 位加法的简单实现是将域元素转换为 32 位，然后构建一个 “加法电路”，该电路将每个位相加并进位溢出。但是，这样会创建比必要的更大的电路。

相反，我们可以这样做：

1. 使用上述策略范围检查 x 和 y
2. 将 x 和 y 作为域元素相加，即 z <== x + y
3. 将 z 转换为 33 位数字
4. 将 33 位数字的最低有效 32 位转换为域元素。

这可以可视化如下：

x + y 最多可以溢出到 33 位数字。考虑 x 和 y 可以保持的最大值是 232−1。如果我们将该值添加到自身，我们得到

(232−1)+(232−1)=2⋅(232−1)=233−2

最终数字需要 33 位才能保持。（回想一下，33 位可以保持的最大数字是 233–1。因此，上面的数字是 33 位可以保持的第二大数字。）因此，我们只需要 33 位来保持总和，然后我们删除第 33 位。

下面是使用 Circom 模拟和验证 32 位加法的代码：

include "circomlib/comparators.circom";
include "circomlib/bitify.circom";

template Add32(n) {
  signal input x;
  signal input y;
  signal output out;

  // range check x and y
  component rCheckX = Num2Bits(32);
  component rCheckY = Num2Bits(32);
  rCheckX.in <== x;
  rCheckY.in <== y;

  // convert the sum to 33 bits
  component n2b33 = Num2Bi...