在Circom中确保正确的整数除法

thogiti
发布于 2025-01-20 16:20
阅读 46

文章探讨了在素数域 $ ext{F}_p$ 中整数除法的挑战，特别是在零知识证明（ZKP）中的应用。强调了传统除法符号可能导致多个有效解的问题，并提供了两种解决方案：比特位除法算法和约束商的其他方法，以确保唯一性和安全性。讨论了使用 Circom 实现的具体代码示例及其优缺点。

## 概述

整数除法是一个教科书级别的例子，展示了在素域 $\mathbb{F}_p$ 中的算术如何与整数算术微妙地不同。天真的方法通常看起来是正确的，但可能导致在零知识证明（ZKP）中存在多个有效解，从而破坏ZKP的健壮性属性。这可能导致ZKP实现中的多种安全漏洞。通过在电路层添加适当的约束——无论是通过实现位wise 除法算法，还是通过限制商的范围——你可以恢复唯一性，并确保你的电路确实编码了你所意图的整数除法。

在实施ZKP电路时，可能会倾向于在代码中依赖诸如 `\`（除法）和 `%`（取模）等高级操作。虽然这些运算符在许多编程语言中看起来类似，但在编译为素域 $\mathbb{F}_p$ 的算术电路时，它们的表现会有所不同。这种差异可能引入 *多个有效解*，对于商和余数，打破了整数除法应只有一个可能答案的现实假设。

在这篇文章中，我将介绍：

- 一个简单的代码片段，天真的使用了 Circom 的 `\` 和 `%` 运算符。
- 为什么这些运算符无法保证在 $\mathbb{F}_p$ 中得到唯一的整数商和余数。
- 两种常见的方法来解决这个问题，包括优缺点：
    - 位wise/位移基础的除法算法，或者
    - 对商施加额外约束以确保唯一性。

我还将覆盖一些你在诊断潜在不受限制的信号时可能看到的 [CircomSpect](https://github.com/trailofbits/circomspect) 警告。

---

## 示例：一个“天真”的整数除法模板

下面是一个在 Circom 中使用内置运算符的 `IntegerDivision` 模板的简化版本：

```circom
template IntegerDivision() {
    signal input dividend;
    signal input divisor;
    signal output quotient;
    signal output remainder;

// 确保除数非零
    assert(divisor != 0);

// 使用 Circom 2.x 运算符分配商和余数
    quotient <-- dividend \ divisor;
    remainder <-- dividend % divisor;

// 约束余数 < 除数
    signal isLessThan <== SafeLessThan(252)([remainder, divisor]);
    1 === isLessThan;

// 检查数学在域中的结果是否正确
    dividend === divisor * quotient + remainder;
}
```

看起来正确，对吧？我们：

- 防止除以零。
- 确保 `remainder < divisor`。
- 强制执行通常的整数除法公式 $\text{dividend} = \text{divisor} \times \text{quotient} + \text{remainder}$。

在典型的整数语言中，这应该就是你所需要的。但在素域 $\mathbb{F}_p$ 中，我们还有一个 *额外的维度* 需要关注。

---

## 为什么在 $\mathbb{F}_p$ 中会出现多个有效解

在大小为 $p$ 的素域中，方程

$$\text{dividend} \equiv \text{divisor} \cdot \text{quotient} \;+\; \text{remainder} \pmod{p}$$

允许多个对 $(\text{quotient}, \text{remainder})$ 满足同一方程——*即使*你检查了 $\text{remainder} < \text{divisor}$ 和 $\text{divisor} \neq 0$。

### 在 $\mathbb{F}_{13}$ 中的具体例子

假设：

- $\text{dividend} = 10$  
- $\text{divisor} = 3$

在正常的整数算术中，我们有：

$$
10 = 3 \times 3 + 1
\quad\Rightarrow\quad
\text{quotient} = 3,\; \text{remainder} = 1.
$$

但在 $\mathbb{F}_{13}$ 中，考虑第二个解：

$$10 \equiv 3 \times 7 + 2 \pmod{13}.$$

检查一下：

$$3 \times 7 + 2 = 21 + 2 = 23 \equiv 10 \pmod{13}.$$

我们还有 $2 < 3$，因此“$\text{remainder} = 2$”通过了检查 `remainder < divisor`。所以电路看到了 *两个有效解* 对于相同的 $(\text{dividend}, \text{divisor})$：

- $\text{quotient} = 3,\; \text{remainder} = 1$
- $\text{quotient} = 7,\; \text{remainder} = 2$

这两种解都会通过约束。如果我们真的试图证明 $\text{quotient}$ 是“真实的整数商”，这 *不是* 我们想要的。在典型的整数数学中，商是唯一的。但在 $\mathbb{F}_p$ 中，我们需要更多的约束来确定它。

---

## 解决该问题的方法

### 选项 A：位wise 除法（电路中的长除法）

一种标准解决方案是 *从头实现整数除法*，使用逐位（或基于位移）的算法。这种方法通常：

- 将 $\text{dividend}, \text{divisor}$ 分解为二进制位：  
   $$
   \text{dividend} < 2^n,\quad
   \text{divisor} < 2^n
   $$
- 实现长除法过程：  
   - 以部分余数 = 0 开始  
   - 从 `dividend` 的最高有效位迭代到最低有效位，移位部分余数并在可行时减去 `divisor`  
   - 每一步产生 `quotient` 的一位和更新的 `remainder`
- 确保最终的 `quotient` 和 `remainder` 在正常的整数算术中是唯一的。

此电路的一般示例可能如下所示：

```circom
template SafeIntegerDivision(nBits) {
    // 我们假设 dividend < 2^nBits 和 divisor < 2^nBits。
    signal input dividend;
    signal input divisor;
    signal output quotient;
    signal output remainder;

// 确保 divisor != 0
    assert(divisor != 0);

// 将它们分解为位
    signal [nBits] dividendBits <== Num2Bits(nBits)(dividend);
    signal [nBits] divisorBits <== Num2Bits(nBits)(divisor);

signal [nBits] quotientBits;

// 我们将在循环中将 partialRemainder 作为整数存储
    var partialRemainder = 0;

// 对于从最高有效位到最低有效位的每一位
    for (var i = nBits - 1; i >= 0; i--) {
        // 将部分余数左移 1
        partialRemainder = partialRemainder * 2 + dividendBits[i];

// 如果 partialRemainder >= divisor，则在 quotient 中设置该位
        var ge = GreaterEqThan(nBits)([partialRemainder, divisor]);
        quotientBits[i] <== ge;

// 如果 ge == 1，则减去 divisor
        partialRemainder = partialRemainder - ge * divisor;
    }

// 从位重构商
    quotient <== Bits2Num(nBits)(quotientBits);
    remainder <== partialRemainder;
}
```

因为我们逐步复制通常的整数除法算法，所以电路中有恰好一个有效结果。在 $\mathbb{F}_p$ 中，你无法“移位”商并修复余数，因为每一步都由必须匹配的位序列约束。

#### 优点：

- 完全约束了解决方案，使其具有唯一的商和余数。
- 模仿标准整数除法，没有歧义。

#### 缺点：

- 电路可能更大：它要求在每次迭代中需要迭代逻辑、位分解和约束。
- 代码略微复杂，维护和调试。

---

### 选项 B：通过附加不等式约束商

另一种方法尝试继续使用 `quotient <-- dividend \ divisor; remainder <-- dividend % divisor;`，但随后强制 $\text{quotient} \le \lfloor \frac{\text{dividend}}{\text{divisor}} \rfloor$。

在普通的编程语言中，我们可能会写：

```javascript
max_quotient = floor(dividend / divisor);
// 然后确保 quotient <= max_quotient
assert(quotient <= max_quotient);
```

但是 Circom 不提供直接可以依赖的 `floor()` 或整除操作。你将不得不自己构建“基于位的检查”——或者作为某种 *公共输入* 输入 `max_quotient` 进电路，然后通过安全比较器证明 `quotient <= max_quotient`：

```circom
signal max_quotient; // 由外部提供
signal isLessOrEq <== SafeLessEqThan(252)([quotient, max_quotient]);
1 === isLessOrEq;
```

但是谁 *计算* `max_quotient`？通常你会在链外完成这项工作，但随后电路必须验证 `max_quotient` 与 `(dividend, divisor)` 一致。这又导致了一整套复杂的约束，以验证你没有关于 `max_quotient` 撒谎。因此，实际上，你重新发明了位wise 方法或部分方法。

#### 优点：

- 如果你可以依赖外部逻辑提供正确的商上限，那么这可能更简单。
- 如果你只需要 `quotient` 的小范围，你可以做一个更小的比较器电路。

#### 缺点：

- 你仍然需要额外的约束以确保 `max_quotient` 中没有溢出或欺骗。
- 不如完整的位wise 算法直接或可靠。

---

## 理解 CircomSpect 警告

当你看到来自 [CircomSpect](https://github.com/trailofbits/circomspect) 的警告时，通常集中在两个关键点：

- `<--` 与 `<==`  
   - `<--` 意思是：“在编译代码中分配值，但不生成强制等式的约束。”因此，如果你的代码只使用 `<--`，则信号可能保持 *不受约束*，除非你稍后明确约束它。  
   - `<==` 意思是：“创建强制此等式的约束。”

- 未使用的输出  
   如果模板返回 `(quotient, remainder)` 但你在后续约束中只使用 `quotient`，你可能会看到类似“输出信号 `remainder` 未受约束”的警告。这是因为从电路的角度看，`remainder` 可以是与局部逻辑一致的任何值，而如果没有后续约束提到它，它实际上是自由的。

例如：

```circom
(quotient, _) <== IntegerDivision()(a * (10  W), b);
```

在这种情况下，`_` 没有被使用，因此 CircomSpect 警告你“`remainder` 在下一步中未受到约束”。如果你确实只需要 `quotient`，这可能没关系。但如果你不小心忘记约束余数，那么就意味着你可能让电路接受了比你意图更多的解。

---

## 两种除法方法的优缺点

使用内置的 `\`, `%`：

- 优点：  
  - 代码非常简洁。  
  - Circom 在后端处理取模操作。  
- 缺点：  
  - 在素域中，结果是 *不独特的*。  
  - 你必须添加额外的约束，以确保你的整数商与真实世界的唯一除法结果匹配。

位wise/位移除法：

- 优点：  
  - 确保整数意义上的 `(quotient, remainder)` 唯一性。  
  - 完全自包含：你无需依赖外部的“max_quotient”或其他假设。  
- 缺点：  
  - 代码更多，电路中有更多约束（这可能增加证明时间）。  
  - 对于新手而言，可能不太直观。

---

## 结论

- 如果你真正需要与标准整数除法对应的唯一 `(quotient, remainder)`，则必须做的不止是：

```circom
   quotient <-- dividend \ divisor;
   remainder <-- dividend % divisor;
   ```

- 一种稳健的解决方案：实现一个逐位或基于位移的算法，复制整数除法。这确保在 $\mathbb{F}_p$ 中，只有“自然的”商和余数能够满足所有约束。  
- 或者，如果你能够提供额外的约束或“公开已知的最大商”，你仍然可以使用 `\` 和 `%`，但随后强制  
   $$
     \text{quotient} \times \text{divisor} \;\le\; \text{dividend} \,<\; (\text{quotient}+1) \times \text{divisor},
     \quad
     0 \le \text{remainder} < \text{divisor}.
   $$  
   只需意识到，验证这些不等式通常需要 *基于位的检查*。

- CircomSpect 警告：  
   - 如果你看到关于 `<--` 与 `<==` 的警告，请确认每个信号确实在代码的其他地方受到约束。  
   - 如果你看到有关“未使用”输出的警告，请确认这是故意的还是疏忽。

在“语法糖”(`\`, `%`) 与“真实约束”之间的微小差别是掌握 Circom 的关键之一。始终检查你的信号约束，以防止在 $\mathbb{F}_p$ 中出现额外的解。

>- 原文链接： [github.com/thogiti/thogi...](https://github.com/thogiti/thogiti.github.io/blob/master/_posts/2025-01-19-Ensuring-Correct-Integer-Division-in-Circom.md)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

概述

在实施ZKP电路时，可能会倾向于在代码中依赖诸如 \（除法）和 %（取模）等高级操作。虽然这些运算符在许多编程语言中看起来类似，但在编译为素域 $\mathbb{F}_p$ 的算术电路时，它们的表现会有所不同。这种差异可能引入 多个有效解，对于商和余数，打破了整数除法应只有一个可能答案的现实假设。

在这篇文章中，我将介绍：

一个简单的代码片段，天真的使用了 Circom 的 \ 和 % 运算符。
为什么这些运算符无法保证在 $\mathbb{F}_p$ 中得到唯一的整数商和余数。
两种常见的方法来解决这个问题，包括优缺点：
- 位wise/位移基础的除法算法，或者
- 对商施加额外约束以确保唯一性。

我还将覆盖一些你在诊断潜在不受限制的信号时可能看到的 CircomSpect 警告。

示例：一个“天真”的整数除法模板

下面是一个在 Circom 中使用内置运算符的 IntegerDivision 模板的简化版本：

template IntegerDivision() {
    signal input dividend;
    signal input divisor;
    signal output quotient;
    signal output remainder;

    // 确保除数非零
    assert(divisor != 0);

    // 使用 Circom 2.x 运算符分配商和余数
    quotient <-- dividend \ divisor;
    remainder <-- dividend % divisor;

    // 约束余数 < 除数
    signal isLessThan <== SafeLessThan(252)([remainder, divisor]);
    1 === isLessThan;

    // 检查数学在域中的结果是否正确
    dividend === divisor * quotient + remainder;
}

看起来正确，对吧？我们：

防止除以零。
确保 remainder < divisor。
强制执行通常的整数除法公式 $\text{dividend} = \text{divisor} \times \text{quotient} + \text{remainder}$ 。

在典型的整数语言中，这应该就是你所需要的。但在素域 $\mathbb{F}_p$ 中，我们还有一个 额外的维度 需要关注。

为什么在 $\mathbb{F}_p$ 中会出现多个有效解

在大小为 $p$ 的素域中，方程

$\text{dividend} \equiv \text{divisor} \cdot \text{quotient} \;+\; \text{remainder} \pmod{p}$

允许多个对 $(\text{quotient}, \text{remainder})$ 满足同一方程——即使你检查了 $\text{remainder} < \text{divisor}$ 和 $\text{divisor} \neq 0$ 。

在 $\mathbb{F}_{13}$ 中的具体例子

假设：

$\text{dividend} = 10$
$\text{divisor} = 3$

在正常的整数算术中，我们有：

10 = 3 \times 3 + 1 \quad\Rightarrow\quad \text{quotient} = 3,\; \text{remainder} = 1.

但在 $\mathbb{F}_{13}$ 中，考虑第二个解：

$10 \equiv 3 \times 7 + 2 \pmod{13}.$

检查一下：

$3 \times 7 + 2 = 21 + 2 = 23 \equiv 10 \pmod{13}.$

我们还有 $2 < 3$ ，因此“ $\text{remainder} = 2$ ”通过了检查 remainder < divisor。所以电路看到了 两个有效解 对于相同的 $(\text{dividend}, \text{divisor})$ ：

$\text{quotient} = 3,\; \text{remainder} = 1$
$\text{quotient} = 7,\; \text{remainder} = 2$

这两种解都会通过约束。如果我们真的试图证明 $\text{quotient}$ 是“真实的整数商”，这不是我们想要的。在典型的整数数学中，商是唯一的。但在 $\mathbb{F}_p$ 中，我们需要更多的约束来确定它。

解决该问题的方法

选项 A：位wise 除法（电路中的长除法）

一种标准解决方案是 从头实现整数除法，使用逐位（或基于位移）的算法。这种方法通常：

将 $\text{dividend}, \text{divisor}$ 分解为二进制位： $\text{dividend} < 2^n,\quad \text{divisor} < 2^n$
实现长除法过程：
- 以部分余数 = 0 开始
- 从 dividend 的最高有效位迭代到最低有效位，移位部分余数并在可行时减去 divisor
- 每一步产生 quotient 的一位和更新的 remainder
确保最终的 quotient 和 remainder 在正常的整数算术中是唯一的。

此电路的一般示例可能如下所示：

template SafeIntegerDivision(nBits) {
    // 我们假设 dividend < 2^nBits 和 divisor < 2^nBits。
    signal input dividend;
    signal input divisor;
    signal output quotient;
    signal output remainder;

    // 确保 divisor != 0
    assert(divisor != 0);

    // 将它们分解为位
    signal [nBits] dividendBits <== Num2Bits(nBits)(dividend);
    signal [nBits] divisorBits <== Num2Bits(nBits)(divisor);

    signal [nBits] quotientBits;

    // 我们将在循环中将 partialRemainder 作为整数存储
    var partialRemainder = 0;

    // 对于从最高有效位到最低有效位的每一位
    for (var i = nBits - 1; i >= 0; i--) {
        // 将部分余数左移 1
        partialRemainder = partialRemainder * 2 + dividendBits[i];

        // 如果 partialRemainder >= divisor，则在 quotient 中设置该位
        var ge = GreaterEqThan(nBits)([partialRemainder, divisor]);
        quotientBits[i] <== ge;

        // 如果 ge == 1，则减去 divisor
        partialRemainder = partialRemainder - ge * divisor;
    }

    // 从位重构商
    quotient <== Bits2Num(nBits)(quotientBits);
    remainder <== partialRemainder;
}

优点：

完全约束了解决方案，使其具有唯一的商和余数。
模仿标准整数除法，没有歧义。

缺点：

电路可能更大：它要求在每次迭代中需要迭代逻辑、位分解和约束。
代码略微复杂，维护和调试。

选项 B：通过附加不等式约束商

另一种方法尝试继续使用 quotient <-- dividend \ divisor; remainder <-- dividend % divisor;，但随后强制 $\text{quotient} \le \lfloor \frac{\text{dividend}}{\text{divisor}} \rfloor$ 。

在普通的编程语言中，我们可能会写：

max_quotient = floor(dividend / divisor);
// 然后确保 quotient <= max_quotient
assert(quotient <= max_quotient);

但是 Circom 不提供直接可以依赖的 floor() 或整除操作。你将不得不自己构建“基于位的检查”——或者作为某种 公共输入 输入 max_quotient 进电路，然后通过安全比较器证明 quotient <= max_quotient：

signal max_quotient; // 由外部提供
signal isLessOrEq <== SafeLessEqThan(252)([quotient, max_quotient]);
1 === isLessOrEq;

但是谁计算 max_quotient？通常你会在链外完成这项工作，但随后电路必须验证 max_quotient 与 (dividend, divisor) 一致。这又导致了一整套复杂的约束，以验证你没有关于 max_quotient 撒谎。因此，实际上，你重新发明了位wise 方法或部分方法。

优点：

如果你可以依赖外部逻辑提供正确的商上限，那么这可能更简单。
如果你只需要 quotient 的小范围，你可以做一个更小的比较器电路。

缺点：

你仍然需要额外的约束以确保 max_quotient 中没有溢出或欺骗。
不如完整的位wise 算法直接或可靠。

理解 CircomSpect 警告

当你看到来自 CircomSpect 的警告时，通常集中在两个关键点：

<-- 与 <==
- <-- 意思是：“在编译代码中分配值，但不生成强制等式的约束。”因此，如果你的代码只使用 <--，则信号可能保持 不受约束，除非你稍后明确约束它。
- <== 意思是：“创建强制此等式的约束。”
未使用的输出
如果模板返回 (quotient, remainder) 但你在后续约束中只使用 quotient，你可能会看到类似“输出信号 remainder 未受约束”的警告。这是因为从电路的角度看，remainder 可以是与局部逻辑一致的任何值，而如果没有后续约束提到它，它实际上是自由的。

例如：

(quotient, _) <== IntegerDivision()(a * (10  W), b);

在这种情况下，_ 没有被使用，因此 CircomSpect 警告你“remainder 在下一步中未受到约束”。如果你确实只需要 quotient，这可能没关系。但如果你不小心忘记约束余数，那么就意味着你可能让电路接受了比你意图更多的解。

两种除法方法的优缺点

使用内置的 \, %：

优点：
- 代码非常简洁。
- Circom 在后端处理取模操作。
缺点：
- 在素域中，结果是 不独特的。
- 你必须添加额外的约束，以确保你的整数商与真实世界的唯一除法结果匹配。

位wise/位移除法：

优点：
- 确保整数意义上的 (quotient, remainder) 唯一性。
- 完全自包含：你无需依赖外部的“max_quotient”或其他假设。
缺点：
- 代码更多，电路中有更多约束（这可能增加证明时间）。
- 对于新手而言，可能不太直观。

结论

如果你真正需要与标准整数除法对应的唯一 (quotient, remainder)，则必须做的不止是：
```
quotient <-- dividend \ divisor;
remainder <-- dividend % divisor;
```
一种稳健的解决方案：实现一个逐位或基于位移的算法，复制整数除法。这确保在 $\mathbb{F}_p$ 中，只有“自然的”商和余数能够满足所有约束。
或者，如果你能够提供额外的约束或“公开已知的最大商”，你仍然可以使用 \ 和 %，但随后强制
$\text{quotient} \times \text{divisor} \;\le\; \text{dividend} \,<\; (\text{quotient}+1) \times \text{divisor}, \quad 0 \le \text{remainder} < \text{divisor}.$
只需意识到，验证这些不等式通常需要 基于位的检查。
CircomSpect 警告：
- 如果你看到关于 <-- 与 <== 的警告，请确认每个信号确实在代码的其他地方受到约束。
- 如果你看到有关“未使用”输出的警告，请确认这是故意的还是疏忽。

在“语法糖”(\, %) 与“真实约束”之间的微小差别是掌握 Circom 的关键之一。始终检查你的信号约束，以防止在 $\mathbb{F}_p$ 中出现额外的解。

原文链接： github.com/thogiti/thogi...

登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

在Circom中确保正确的整数除法

概述

示例：一个“天真”的整数除法模板

为什么在 $\mathbb{F}_p$ 中会出现多个有效解

在 $\mathbb{F}_{13}$ 中的具体例子

解决该问题的方法

选项 A：位wise 除法（电路中的长除法）

优点：

缺点：

选项 B：通过附加不等式约束商

优点：

缺点：

理解 CircomSpect 警告

两种除法方法的优缺点

结论

0 条评论

文章目录

在Circom中确保正确的整数除法

概述

示例：一个“天真”的整数除法模板

为什么在 Fp\mathbb{F}_pFp​ 中会出现多个有效解

在 F13\mathbb{F}_{13}F13​ 中的具体例子

解决该问题的方法

选项 A：位wise 除法（电路中的长除法）

优点：

缺点：

选项 B：通过附加不等式约束商

优点：

缺点：

理解 CircomSpect 警告

两种除法方法的优缺点

结论

0 条评论

文章目录

为什么在 $\mathbb{F}_p$ 中会出现多个有效解

在 $\mathbb{F}_{13}$ 中的具体例子