ZK 中的 32 位模拟

Last updated on Aug 20, 2025

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

为什么我们需要 32 位模拟？

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

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

32 位字与有限域元素

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

人们可以将 32 位虚拟机视为在模 $2^{32}$ 下进行所有算术运算。普通虚拟机会默认在该数字处溢出。然而，在有限域中进行模运算时，计算模 $2^{32}$ 会增加相当多的约束（我们稍后将看到），但幸运的是，有一个实用的数学技巧可以高效地完成它。

以下两个函数在计算模 $2^{32}$ 时是等效的：

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 位来计算 $\mod 2^{32}$ 。附录中对此进行了形式化验证。在对包含 32 位数字的信号进行任何算术运算之前，我们首先需要完全确定该信号所持有的数字实际上确实适合 32 位。

32 位范围检查

如果我们正在创建一个模拟使用 32 位字计算的 ZK 电路，那么我们需要确保没有任何信号包含大于或等于 $2^{32}$ 的值。一种直观的做法是使用 LessThan 模板，如下所示：

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

然而，这个电路产生了超出必要的约束。

更高效的方法是利用二进制表示。核心思想是用 32 位对数字进行编码，如果它能够放进 32 位，电路就会正常执行。相反，如果该数字放不进 32 位，则无法满足约束条件。因此，下面的电路确保了 in 小于或等于 $2^{32}-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 约束为 0 或 1，并且还约束了二进制表示等于输入（通过 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 位加法

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

32 位加法的朴素实现方式是将域元素转换为 32 位，然后构建一个“加法电路”，将每一位相加并处理进位溢出。然而，这会产生一个比必要规模更大的电路。

相反，我们可以执行以下操作：

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

这可以通过以下方式可视化：

x + y 最多只会溢出为一个 33 位数字。考虑到 x 和 y 能容纳的最大值是 $2^{32}-1$ 。如果我们将该值与其自身相加，我们会得到：

\begin{align*} &(2^{32}-1)+(2^{32}-1)\\ &=2\cdot(2^{32}-1)\\ &=2^{33}-2 \end{align*}

最终的数字需要 33 位来保存。（回想一下，33 位能保存的最大数字是 $2^{33} - 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 = Num2Bits(33);
  n2b33.in <== x + y;

  // convert the least significant 32 bits
  // to the final result
  component b2n = Bits2Num(32);
  for (var i = 0; i < 32; i++) {
    b2n.in[i] <== n2b33.out[i];
  }

  b2n.out ==> out;
}

32 位乘法

32 位乘法的逻辑与 32 位加法极其相似，不同之处在于，我们需要允许 32 位乘法在仅保存最终 32 位之前，临时需要最多 64 位：

\begin{align*} &=(2^{32}-1)(2^{32}-1)\\ &=2^{64}-2^{32}-2^{32}+2\\ &=2^{64}-2^{33}+2 \end{align*}

最终的数字需要 64 位来保存。

该电路的实现留给读者作为练习。

32 位除法和取模

整数除法是 ZK 中最容易引发 Bug 的问题之一，因为对它进行适当的约束要比加法和乘法的例子困难得多。以下是一些实际中因约束不足导致的除法问题示例：

在整数除法中，分子（numerator）、分母（denominator）、商（quotient）和余数（remainder）之间的关系是：

\text{numerator}=\text{denominator}\times\text{quotient}+\text{remainder}

然而，仅仅有这个约束不足以确保除法被正确执行。

例如，假设我们试图证明我们计算了 12 / 7 = 1。我们的电路将具有以下值：

12 = 7 \times 1 +5

然而，以下见证（witness）同样满足该约束：

12 = 7 \times 0 + 12

我们可以通过添加一个“余数严格小于分母”的约束来防止这种情况。

此外，我们应该注意以下潜在的 Bug：

对于 254 位域（这是 Circom 使用的默认域）中的 32 位来说这不是问题，但我们要确保 $\text{denominator}\times\text{quotient}$ 的计算不会溢出底层的有限域。
更普遍地说，我们不希望 $\text{denominator}\times\text{quotient}+\text{remainder}$ 的计算发生溢出。如果 denominator 和 quotient 都被进行了 32 位范围检查，那么乘积 $\text{denominator}\times\text{quotient}$ 最多占用 64 位，如果 remainder 也进行了 32 位范围检查，那么 $\text{denominator}\times\text{quotient}+\text{remainder}$ 最多需要 65 位。因此，使用 32 位 VM 位大小对于 Circom 的默认域来说不是问题，但对于其他 VM 位大小（例如 128 位），则有可能发生溢出。
除以零可能会产生意外的行为，具体取决于你所考虑的 ZKVM。例如，当发生除以零时，EVM 不会 panic，而是返回 0。在 RISC-V 架构中，除以零会返回一个所有位都设置为 1 的字。

仅使用加法和乘法直接计算整数除法是不切实际的（像用于乘法的 Karatsuba’s method 或用于 efficient integer division 的高效算法使用了 for 循环或递归，这并不能很好地映射到加法和乘法），因此最好在约束之外计算整数除法的结果。

在 Circom 中，/ 运算符是指模除（乘以乘法逆元），而 \ 运算符是指整数除法。以下代码展示了如何证明我们正确计算了商和余数。我们加入了余数的计算，因为当证明正确计算了整数除法时，这顺便就得到了。

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

template DivMod(wordSize) {
  // a wordSize over this could overflow 252
  assert(wordSize < 125);

  signal input numerator;
  signal input denominator;

  signal output quotient;
  signal output remainder;

  quotient <-- numerator \ denominator;
  remainder <-- numerator % denominator;
  
  // quotient and remainder still need
  // to be range checked because the
  // prover can supply any value
  
  // range check all the signals
  component n2bN = Num2Bits(wordSize);
  component n2bD = Num2Bits(wordSize);
  component n2bQ = Num2Bits(wordSize);
  component n2bR = Num2Bits(wordSize);
  n2bN.in <== numerator;
  n2bD.in <== denominator;
  n2bQ.in <== quotient;
  n2bR.in <== remainder;

  // core constraint
  numerator === quotient * denominator  + remainder;

  // remainder must be less than the denominator
  signal remLtDen;
  
  // depending on the application, we might be able
  // to use fewer than 252 bits
  remLtDen <== LessThan(wordSize)([remainder, denominator]);
  remLtDen === 1;

  // denominator is not zero
  signal isZero;
  isZero <== IsZero()(denominator);
  isZero === 0;
}

component main = DivMod(32);

32 位位移

假设我们希望模拟以下代码：

uint32 x;
uint32 s;
x << s;

向左移位 s 等同于乘以 $2^s$ ，其中 $s$ 是移位大小，而向右移位 s 等同于除以 $2^s$ 。正如在上一章中所见，计算幂会产生相当庞大的约束集。因此，预先计算直到字长减 1 的每一个 2 的幂通常更为高效。所以，对于 32 位数字的左移，我们预先计算一直到 31（字长 (32) - 1）的所有 2 的幂：1, 2, 4, 8, …, $2^{31}$ ，并使用前面讨论的条件选择技术将 x 乘以适当的选择项。如果移位量为 32 或更大，我们乘以零。

该实现留给读者作为练习。

32 位 AND、NOT、OR、XOR 和 NOT

Circomlib gates library 对这些电路都有相应的实现，并且它们不言自明，因此我们鼓励读者直接阅读那里的代码。我们在下面展示了如何模拟以下操作的模板：

按位 AND

uint32 a;
uint32 b;
a & b;

按位 NOT

uint32 x;
~x; // flip all the bits

下面是用于计算和约束 a 和 b 的按位 AND 的代码。

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

template BitwiseAnd32() {
  signal input a;
  signal input b;
  signal output out;

  // range check
  component n2ba = Num2Bits(32);
  component n2bb = Num2Bits(32);
  n2ba.in <== a;
  n2bb.in <== b;

  component b2n = Bits2Num(32);
  component Ands[32];
  for (var i = 0; i < 32; i++) {
    Ands[i] = AND();
    Ands[i].a <== n2ba.out[i];
    Ands[i].b <== n2bb.out[i];
    Ands[i].out ==> b2n.in[i];
  }

  b2n.out ==> out;
}

component main = BitwiseAnd32();

剩余的 NOT、OR 和 XOR 操作留给读者作为练习。

ZK EVM 如何处理 256 位数字

默认的 Circom 域不能保存 256 位数字。相反，EVM 中的每个字都必须用一组较小的字长来建模，这类似于 64 位计算机模拟 EVM 的方式。

例如，一个 256 位数字可以用四个 64 位字进行建模。相加时，我们将溢出从低有效位字进位到高有效位字。如果最高有效位字溢出，我们只需丢弃该溢出即可。

附录 A：等效性证明

我们使用 Certora 证明器来论证以下函数的等效性：

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)); 
    }
}

这是 Certora 验证语言规则：

methods {
  function mod32(uint256) external returns (uint256) envfree;
  function mod32e(uint256) external returns (uint256) envfree;
}

rule test_Mod32AndMod32E_Equivalence() {
  uint256 x;
  assert mod32(x) == mod32e(x);
}

这是 Certora 报告：

https://prover.certora.com/output/541734/6cd3303cb5f5441e8773adb5c79787d7?anonymousKey=0b945ee1440cd67efed3efba3162b0f924e8cf8f