💻 computer science

Automating Bitvector and Finite Field Equivalence Proofs in Lean

本文介绍了 BitModEq，这是一种新颖的 Lean 策略，它利用范围引理和案例分析自动化位向量与有限域之间的等价性证明，在验证零知识证明电路编码方面优于最先进的 SMT 求解器。

原作者： Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker

发布于 2026-05-15

📖 1 分钟阅读☕ 轻松阅读

原作者： Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

以下是论文《在 Lean 中自动化位向量与有限域等价性证明》的通俗解释，辅以日常类比。

宏观图景：两种不同的数学语言

想象一下，你正在验证一个秘密配方（零知识证明）是否正确。问题在于，这个配方是用两种混合性极差的“语言”写成的：

有限域：将其想象为“时钟数学”世界。如果你有一个 17 小时的时钟，10 加 10 不会得到 20，而是得到 3（因为会回绕）。许多现代密码系统（如加密货币中使用的系统）正是这样进行数学运算的。
位向量：将其想象为“计算机数学”。计算机不会像时钟那样回绕；它们只有一组固定数量的开关（位），要么开，要么关。如果你进行加法运算且开关用尽，多余的位只会被直接截断。

问题所在：
当开发者构建这些密码系统时，他们必须将“时钟数学”翻译成“计算机数学”，以便在真实硬件上运行。这种翻译过程称为算术化。

如果翻译错误，整个安全系统就会崩溃。
检查翻译是否正确极其困难。
人工检查就像拿着放大镜逐字校对小说：虽然准确，但耗时极长，且容易出错。
自动检查（使用标准计算机求解器）就像使用拼写检查器：速度很快，但它常常被奇怪的“时钟数学”规则搞糊涂，面对复杂句子时往往束手无策。

解决方案："BitModEq"翻译器

作者在一个名为 Lean 的系统中构建了一个新工具，称为 BitModEq（Lean 就像一个超级严格的数学导师，会检查证明的每一步）。

将 BitModEq 想象为一个专门的翻译器，它不仅仅交换词语，还能理解词语背后的逻辑。它通过三个步骤来证明“时钟数学”配方与“计算机数学”配方完全一致：

步骤 1：“展开”（翻译）

该工具将“时钟数学”（有限域）尝试“展开”为普通数字（自然数）。

挑战：在时钟数学中，$5 - 10$ 可能是一个正数，因为发生了回绕。而在普通数学中，它是负数。
技巧：该工具观察数字并询问：“这个数字有可能发生回绕吗？”如果数字足够小（就像计算机中的位），它就知道回绕不会发生。它会安全地移除“时钟”规则，将其视为普通数学。如果不确定，它会保留“时钟”规则，但添加一个安全检查。

步骤 2：“安全网”（范围分析）

这是本文的秘诀。在工具尝试将数学转换为计算机位之前，它会执行范围分析。

类比：想象你在打包行李箱。你不会只是把衣服扔进去；你会检查行李箱的大小和衣服的大小。
工作原理：该工具查看变量并询问：“这个数字最大可能是多少？”
- 如果它知道一个数字在 0 到 1 之间（就像单个电灯开关），它可以完全忽略复杂的“时钟”规则。
- 这一步至关重要，因为它极大地简化了问题，使计算机能够轻松解决。如果没有这个“安全网”检查，计算机就会被复杂性压垮。

步骤 3：“位爆破”（最终证明）

一旦工具将问题简化为纯粹的“计算机数学”（位），它就会使用一种称为位爆破的技术。

类比：这就像拿着一把复杂的锁，尝试每一种钥匙组合，直到找到能打开它的那一把。
由于该工具在步骤 2 中简化了问题，现在的“锁”已经小到计算机可以瞬间尝试所有组合，从而证明数学是正确的。

为何重要（结果）

作者在实际密码系统（特别是 Jolt 和 CirC）上测试了他们的工具。

竞争：他们将工具与现有的最佳自动求解器（如 cvc5）进行了比较。
结果：当问题变大（例如 32 位数字）时，现有求解器经常卡住或超时。它们就像试图阅读字典的拼写检查器。
BitModEq 的胜利：新工具比现有最佳工具多解决了 19% 的问题。它能够处理其他工具失败的大得多的数字（高达 32 位）。
额外优势：因为它在 Lean 内部运行，所以证明经过了内核检查。这意味着计算机不仅仅是猜测；它遵循了一套严格且保证正确的逻辑规则，从而降低了隐藏错误的风险。

现实世界的发现

在测试过程中，该工具实际上在 CirC 编译器中发现了一个 bug。该编译器在处理大数字（具体是 32 位右移）时存在错误。这个 bug 只有在处理大数字时才会显现，这就是为什么之前的小规模测试错过了它的原因。作者在报告后，开发人员修复了这个 bug。

总结

这篇论文提出了一种自动验证密码数学是否正确的新方法。与其挣扎于手动或使用笨拙的工具在“时钟数学”和“计算机数学”之间进行翻译，他们构建了一个智能翻译器，该翻译器：

首先检查数字的大小（范围分析）。
通过移除不必要的“时钟”规则来简化数学。
使用暴力逻辑证明最终结果是正确的。

这使得验证复杂安全系统的速度更快、更可靠，并且能够捕捉到其他工具遗漏的错误。

技术摘要：在 Lean 中自动化位向量与有限域等价性证明

问题陈述

零知识证明（ZKP）电路编码的验证面临一个关键挑战：证明同时利用位向量运算（模 $2^N$ 的标准机器算术）和有限域运算（模大素数 $P$ 的算术）的无量化陈述的正确性。ZKP 系统通常需要“算术化”，即将位向量逻辑编码为有限域多项式。确保这些编码的正确性对于 ZKP 系统的可靠性至关重要，然而构建这些编码极易出错。

现有的验证工作流程存在两个主要局限性：

手动验证：将完整的 ZKP 系统嵌入交互式定理证明器（ITP，如 Lean）可提供强有力的保证，但需要大量人力。随着 ZKP 优化技术的快速演进，这些手动证明经常需要大量的重构工作。
自动 SMT 验证：将验证简化为可满足性模理论（SMT）查询可提供更高的自动化程度，但在两个基本问题上存在困难：
- 理论转换：SMT 求解器缺乏在有限域与位向量之间进行转换的原生支持。像位拆分（bit-splitting）这样的变通方法会引入过多的变量，而范围检查则需要复杂的多项式，从而降低求解器的性能。
- 可信代码库（TCB）：SMT 求解器的可信代码库远大于 ITP，增加了遗漏漏洞的风险。

方法论

作者提出了 BitModEq，这是一种新颖的 Lean 策略（tactic），旨在自动证明有限域编码与其对应的位向量语义之间的等价性。该方法利用 ITP 丰富的语义执行直接的类型转换，同时通过专门的工作流程保留 SMT 求解的自动化能力。

核心工作流程

BitModEq 在四个不同的阶段运行（如论文图 1 所示）：

有限域到自然数转换：将所有有限域（$FP $）类型的项转换为自然数（$ N$）。这涉及将转换操作符（如 toNat）向内推入算术表达式中。
范围分析：使用专用的范围分析算法消除转换过程中生成的自然数不等式。
自然数到位向量转换：将剩余的自然数项转换为位向量（ $BV_N$ ）。
位爆破（Bit-Blasting）：使用在 Lean 中实现的位爆破决策过程 bv_decide 来消除最终的位向量等式目标。

关键技术组件

1. 翻译演算（第 4.2 节）
该策略采用一组翻译规则在不同域之间移动：

$FP \to N$ ：诸如 distNat 的规则将 toNat 分配到加法和乘法上。关键在于，该策略区分了可以排除模数回绕的情况（允许简单的减法）和无法排除的情况（需要加上模数 $P$ 后执行模运算）。诸如 sqrBds 的规则检测位编码（其中 $x^2 = x$ ）并将其转换为边界（ $x \le 1$ ）。
$N \to BV$ ：诸如 distBV 的规则将 toBV 分配到操作上。与 $FP \to N$ 步骤不同，这些规则不需要添加模运算符，因为目标空间天然就是模 $2^N$ 的。

2. 范围分析（第 4.3 节）
标准的 Lean 策略（如 omega、linarith）由于系数过大和变量依赖关系复杂，往往无法处理 ZKP 算术化。BitModEq 引入了一种自定义的、基于语法的范围分析演算：

占位变量：该算法引入存在性占位变量来分解复杂的不等式。
分解与消除：规则将不等式分解（例如， $a + b \le w$ 变为 $a \le w_1, b \le w_2, w_1+w_2 \le w$ ），并通过用从假设或已知属性（例如，有限域元素受限于 $P-1$ ）推导出的边界实例化它们来消除占位变量。
依赖处理：专用规则（ineqCases、ineqXOR）对模拟位（0 或 1）的变量执行有针对性的案例分析，以解决标准算术求解器遗漏的依赖关系。

3. 实现
该策略在 Lean 4.23.0 中实现，利用 mathlib 获取引理，并利用 bv_decide 进行最终的位爆破步骤。它依赖 Lean 的内核进行证明检查，从而确保最小的可信计算基础。

主要贡献

BitModEq 策略：一种将有限域运算转换为位向量并通过位爆破求解所得目标的 Lean 策略，保留了 ITP 的正确性保证。
现实世界编码的有界验证：对两个现实世界 ZKP 系统（Jolt 和 CirC）的概念验证，实现了比先前技术更高的位宽边界。
专用范围分析：一种新的 Lean 策略，用于证明由翻译产生的目标，专门设计用于处理 ZKP 算术化中常见的变量依赖关系和不等式约束。

结果与评估

作者在从 Jolt（一个 zkVM）和 CirC（一个 zkVM 编译器）提取的基准测试上，将 BitModEq 与最先进的 SMT 求解器（特别是带有完整和拆分 Gröbner 基的 cvc5）进行了评估。

性能：BitModEq 比表现最佳的 SMT 配置多解决了 19% 的基准测试。
- 在 Jolt 基准测试（8 位和 32 位查找表）上，BitModEq 比 cvc5（弱编码）多解决了 3 个 8 位实例和 7 个 32 位实例。
- 在 CirC 基准测试上，BitModEq 在 17 个测试位宽中的 13 个上解决了更多的实例。
可扩展性：虽然 cvc5 在较小位宽上表现更好，但由于位拆分导致的变量爆炸，其性能随着位宽的增加而显著下降。BitModEq 有效地扩展到 32 位输入。
效率：消融研究表明，自定义范围分析至关重要；移除案例分析会显著减少解决的基准测试数量（例如，在 CirC 上从 737 降至 720，在 Jolt 上从 24 降至 21）。用标准 Lean 策略（ring_nf、linarith 等）替换自定义分析会导致已解决实例数量急剧下降（例如，在 CirC 上为 434 对 737）。
运行时间：范围分析约占总运行时间的 52%，其次是翻译（23%）和位爆破（21%）。
漏洞发现：在评估 CirC 期间，作者发现了一个与整数溢出相关的 32 位算术右移实现中的可靠性漏洞，该漏洞在较小位宽下未被检测到。

意义与主张

本文主张，BitModEq 通过结合 ITP 的可靠性与自动推理，解决了当前 ZKP 验证工作流程的具体局限性。通过将有限域约束转换回位向量，该方法避免了 SMT 理论转换的性能瓶颈以及 SMT 求解器庞大的可信代码库。

作者强调，他们的方法对于在有限域内模拟位级操作的 ZKP 算术化特别有效，这是现代 ZK 系统中的常见模式。虽然该方法并不完备（对于某些复杂的依赖关系或特定于域的运算如逆运算，它可能会返回“未知”），但它成功验证了以前自动工具无法处理的现实世界编码，为这些关键密码组件的正确性提供了经内核检查的证明。