在Clean中验证Poseidon：为何最后的'sorry'是关于素性证明

zksecurity 发布于 2026-05-05 阅读 184

本文介绍了使用Lean形式化验证工具对Circomlib中优化的Poseidon哈希函数（arity 1）进行正确性证明的过程。

poseidon-clean

Poseidon 是零知识生态中最流行的哈希函数之一。它被设计为一种适用于 SNARK、STARK 及相关证明系统的算术化友好哈希函数（论文链接），并出现在广泛使用的库中，例如 circomlib 的 Poseidon 电路。它被用于 Merkle 树、承诺、无效器（nullifier）以及许多其他需要哈希函数且该哈希能廉价地表示为算术约束的场景。

在本文中，我们逐步讲解一个 Lean 4 的正确性证明，该证明针对 Clean 模型下的 circomlib 优化版 Poseidon 电路（arity 1）。该定理表明，建模的约束相对于 circomlib 所使用的优化版 Poseidon 规范是可靠且完备的：

def circuit : FormalCircuit (F BN254_PRIME) field field where
  Assumptions _ := True
  Spec input output := output = poseidon1Opt input
  soundness := ...
  completeness := ...

换句话说，如果约束被满足，则输出就是指定的 Poseidon 哈希值。并且对于每个输入，都存在预期的见证（witness）。

信息

该证明和规范位于 Clean 仓库：

如果你熟悉 Lean，你会知道大型证明通常是自顶向下构建的。你首先陈述辅助引理，用它们来塑造主定理，之后再填充这些引理的证明。Lean 使用关键字 sorry 标记这些未完成的证明义务。在 Poseidon 证明上工作数周后，还剩下一个 sorry：

instance : Fact (Nat.Prime BN254_PRIME) := by sorry

有趣的是，这并不仅仅是一个缺失的密码学论证。它是 BN254 标量域模数的素性证明。这个数是 BN254 曲线（也称为 alt_bn128）的标准参数，用于 以太坊配对预编译 和许多 zkSNARK 库。但 Lean 并不接受“标准参数”作为证明。为了完成定理，我们仍需证明这个 254 位整数是素数。

你可能听说过概率性素性测试，比如 Miller-Rabin。这些是实用的工程工具：运行足够轮次后，错误概率会变得极低。但高置信度并不能构成 Lean 证明。这里我们需要一个内核能够检查的证明对象。

因此，要关闭这个 sorry，需要一个 素性证书：一个有限的见证，它将“BN254_PRIME 是素数”这一主张归约为计算和更小的素性主张。令人惊讶的是，我们即将看到，所需的证书基于一个 1876 年的定理。

为什么 Poseidon 值得验证

大多数常见的哈希函数，如 SHA-256，都是面向比特位的。它们使用旋转、异或、按位布尔运算和模 2 的幂的加法。这些操作在 CPU 上很自然，但在算术电路中代价高昂。

Poseidon 是为相反场景设计的。其核心操作是域加法、域乘法、形如 $x \mapsto x^5$ 的 S 盒以及小型矩阵乘法。这些是 R1CS、PLONKish 算术化以及许多 SNARK 电路能够高效处理的操作类型。

效率是 Poseidon 在 circom 电路中如此常见的主要原因。但这也意味着电路中的 bug 是严重的。如果电路接受了一个输出并非预期哈希的见证，那么每个依赖该哈希的协议都可能继承这个 bug。这正是形式化验证旨在排除的错误类型。与其测试大量输入并希望连线正确，我们不如用数学方式陈述电路应该计算什么，并证明每个满足条件的赋值确实计算了它。

标准 Poseidon 与优化版 Poseidon

Poseidon 通常被描述为使用 MDS 矩阵的一系列全轮和部分轮。这是一个清晰的数学描述：应用 S 盒、加轮常量、混合状态、重复。然而，circomlib 电路并未以最直接的方式实现这个描述。它实现了一种优化调度，该调度在代数上旨在产生相同的置换，但约束更少。该优化在部分轮之前使用一个预稀疏矩阵，并在部分轮阶段使用稀疏矩阵。

对于验证来说，这个区别很重要。如果电路检查的是优化调度，那么定理应该针对优化调度。直接针对教科书式规范证明电路会迫使证明也吸收优化论证。

因此，该证明使用了两个 Lean 规范：

poseidon1     -- 较简单、未经优化、全 MDS 的输出规范
poseidon1Opt  -- 优化后的 circomlib 风格调度

你可以在 Specs/Poseidon.lean 和 Specs/PoseidonOptimized.lean 中找到这些定义。

最终的电路定理是针对 poseidon1Opt 表述的，因为那正是 Clean 电路模型实际遵循的结构。更简单的 poseidon1 规范仍然有用：我们将 poseidon1Opt 与它以及与 circomlibjs 向量进行测试，作为输出层面的合理性检查。

我们证明了什么

目前，该证明是关于 arity 1 的 Poseidon。用 circomlib 术语来说，这意味着一个输入元素，加上初始零元素，因此内部状态宽度为 $t=2$。形式化验证的对象是 circomlib 优化调度的 Clean 电路模型。顶层定理证明了两个性质：

可靠性。如果一个赋值满足 Clean 电路的所有约束，那么输出就是 poseidon1Opt input。

完备性。对于每个输入，诚实计算都会产生一个满足所有约束的见证。

这两者一起表明 Clean 电路精确地计算了优化后的 Poseidon 函数。没有额外的输出被接受，也没有正确的计算被拒绝。

还有两个值得明确说明的信任边界：

  • 首先，该证明并没有机械地解析 poseidon.circom。Clean 电路是同一优化 arity-1 结构的直接手动模型。对应关系是小且明确的，但它并非从 Circom 源码到 R1CS 的已验证编译器流水线。
  • 其次，优化后的 Poseidon 规范与较简单的非优化规范以及 circomlibjs 向量进行了测试，但 poseidon1Opt = poseidon1 这一等式尚未对所有域元素证明。这是一个有用的验证层，而非形式化的等价证明。

在明确说明这些边界后，我们对 circomlib Poseidon 电路的可靠性和完备性获得了很强的信心：Lean 证明为 Clean 电路模型提供了机器检查的保证，而剩余的假设是少量可检查的建模连接，而非手动检查的数百个代数约束。

电路形状

优化后的 arity-1 电路遵循以下流水线：

[0, input]
    |
ARK C[0..1]
    |
3 轮全轮
    |
带 P 的过渡轮
    |
56 轮稀疏部分轮
    |
3 轮全轮
    |
最终 SBOX + MDS
    |
state[0]

这是优化调度，因此最终定理使用的 Lean 规范是：

Specs.PoseidonOptimized.poseidon1Opt

先证明小部分

试图一次性证明整个电路会很困难：arity-1 Poseidon 已经有超过 400 个中间见证变量，而 56 轮部分轮足以让简单展开对 Lean 来说非常吃力。因此，证明采用了自然的电路分解策略。

该证明有三层 FormalCircuit：

Sigma                                       -- x ↦ x^5
FullRoundOpt_t2 / PartialRoundOptStep_t2    -- 一轮
ApplyFullRounds / ApplyPartialRoundsOpt     -- N 轮阶段

只有 Sigma 是它自己的底层电路：它为 $x^2$、$x^4$ 和 $x^5$ 引入了见证，而可靠性证明只需重写约束并用环算术闭合。ARK 和矩阵算术直接内联到轮级电路中，因为将它们分解出来对证明的帮助还不足以弥补其带来的复杂化。

然后，轮级电路围绕 Sigma 构建：

FullRoundOpt_t2:        对两个状态元素进行 Sigma，然后 ARK，再 Mix
PartialRoundOptStep_t2: 对第一个元素进行 Sigma，对第一个元素进行 ARK，再 MixS

这赋予了证明模块化的形状。如果一个组件有误，该组件的局部定理就会失败。如果组件正确，下一层就可以使用它的规范，而无需每次都重新做代数运算。

难点：组合

一旦轮级组件具备可靠性和完备性，挑战就在于如何将 56 轮部分轮（以及两个各 3 轮的全轮阶段）粘合为一个端到端的证明。朴素的方法是编写整个流水线作为一个表达式，并让 Lean 的简化器展开每个折叠。这不可扩展：产生的项巨大，展开变得缓慢且脆弱，证明脚本也变得不可读。

我们使用的技术是将每个循环包装到自己的 FormalCircuit 中。ApplyPartialRoundsOpt 是一个 FormalCircuit，其 main 是一个对 56 个轮级电路进行的 Circuit.foldl。它的 Spec 简单地说：“输出等于 partialRoundsOpt_t2 C_t2 S_t2 56 10 0 input”。ApplyFullRounds 对 3 轮的全轮阶段做同样的事情。每个循环都成为一个自包含的组件，带有自己的可靠性证明。

这种封装的好处是循环被隐藏在其 Spec 之后。顶层 Poseidon 电路依次组合这几个组件；它从不需要看到底层的折叠，而阶段之间的组合简化为它们规范之间的相等性链接。

在 ApplyPartialRoundsOpt.soundness 内部，我们仍然需要一个归纳推理，从“每个部分轮产生规范的下一状态”到“经过 56 轮后，状态与 partialRoundsOpt_t2 匹配”。这是通过一个私有归纳引理，以及一个从见证环境中恢复每次迭代状态的 envState 辅助函数来处理的。归纳是循环电路本地的，不会在顶层重新执行。

通过这种方式封装循环，顶层的 Poseidon1 证明相对较短。在 circuit_proof_start 展开约束假设后，一个有针对性的 simp 展开每个阶段的 Spec，最后投影提取状态元素 0。子电路规范的线性组合就是证明。

最终定理的内容

最终的电路是：

def circuit : FormalCircuit (F BN254_PRIME) field field where
  main := main
  localLength _ := 402
  Assumptions _ := True
  Spec input output :=
    output = Specs.PoseidonOptimized.poseidon1Opt input
  soundness := ...
  completeness := ...

localLength 值对应每个见证变量：

初始 ARK:         2   (InitialArk)
首批全轮:        24   (3 × 8 in ApplyFullRounds)
过渡轮:           8   (带 P 的 FullRoundOpt_t2)
部分轮:          336   (56 × 6 in ApplyPartialRoundsOpt)
最后全轮:         24   (3 × 8 in ApplyFullRounds)
最终轮:           8   (FullRoundOpt_t2)
----------------------
总计:            402

可靠性定理从一个满足约束的任意环境出发，最终得到：

Expression.eval env ((main input_var).output offset)
  = Specs.PoseidonOptimized.poseidon1Opt input

完备性定理则走向另一个方向：对于任何输入，电路的诚实见证生成都满足约束。这是核心结果。优化的 arity-1 Poseidon 的 Clean 模型精确地计算了优化后的 Poseidon 规范。

房间里的 sorry

所有这一切都发生在 BN254 标量域上：

$p=21888242871839275222246405745257275088548364400416034343698204186575808495617$。

Lean 需要知道这个数是素数。如前所述，仅仅显示它是一个可能素数（例如“Miller-Rabin 在多个基下通过”）是不够的，它必须作为一个定理是素数：

Fact (Nat.Prime BN254_PRIME)

这一点很重要，因为证明使用了域推理。如果模数是合数，那么 ZMod p 就不是一个域。在域中有效的代数事实将不再可用。

因此最后一个 sorry 至关重要，但它也独立于 Poseidon。它是一个针对固定 254 位整数的数论证书。

Lucas 测试

经典的费马测试指出，如果 $p$ 是素数，那么：

$a^{p-1} \equiv 1 \pmod{p}$

对于每个不被 $p$ 整除的 $a$ 都成立。但逆命题显然不成立。事实上，整个（无穷）家族的数字，即所谓的 Carmichael 数，可以通过费马测试尽管是合数。

Lucas 测试增加了一个关键条件。如果存在某个 $a$ 满足：

  1. $a^{n-1} \equiv 1 \pmod{n}$，

  2. 对于 $n-1$ 的每个素因子 $q$，$a^{(n-1)/q} \not\equiv 1 \pmod{n}$，

那么 $n$ 是素数。

其直觉与群中元素的阶有关。第一个条件表明 $a$ 的阶整除 $n-1$。第二个条件表明它不整除任何通过移除一个素因子得到的更小的候选阶。两者共同迫使 $a$ 的阶恰好为 $n-1$，而这只有在 $n$ 是素数时才会发生。Mathlib 中包含这个定理，名为 lucas_primality。

Pratt 证书

Lucas 测试似乎需要知道 $n-1$ 的素因子分解，包括这些因子是素数的证明。Pratt 的观察是，可以使用递归策略来通过 Lucas 测试证明素性。

要证明 $n$ 是素数，需要提供：

  1. 一个 Lucas 见证 $a$，

  2. $n-1$ 的分解，

  3. 每个素因子的 Pratt 证书。

递归在数字 2 处停止，如下例所示。

Pratt 证书树，对应 2063

这就给出了一个紧凑的证明对象，证明助手可以检查。寻找分解和见证的相对昂贵的计算可以离线完成。Lean 只需验证证书。

对于 BN254，$p-1$ 的顶层分解是：

$p-1 = 2^{28} \times 3 \times 13 \times 29 \times 983 \times 11003 \times 237073 \times 405928799 \times 1670836401704629 \times 13818066809895115352007386748515426880336692474882178609894547503$。

最大的因子本身也很大，因此需要它自己的证书树。但结构在所有层次上都相同。

Verified-zkEVM 项目 维护着 CompPoly，一个用于可计算多项式的 Lean 库，其中在其 BN254 域形式化 中已经包含了对 BN254 标量域素数的机器检查的 Pratt 证书。该证书可以通过提供缺失的 Fact (Nat.Prime BN254_PRIME) 实例来关闭剩余的 sorry。

BN254 的 Pratt 证书草图

在撰写本文时，这个最后的 sorry 仍然存在于我们的 Clean 开发中。缺失的成分不是一个全新的数论论证，因为证书已经存在。剩余的工作是工程工作：将 Clean 的 Lean 工具链升级到 CompPoly 所针对的 4.29 版本，以便可以导入证书并消除 sorry。这项工作正在进行中。

这给我们带来了什么

在关闭素性证书后，Lean 证明确立了 Clean arity-1 模型对于 poseidon1Opt 是可靠且完备的。最强的剩余不确定性不再存在于 Lean 证明内部。它位于建模边界：

poseidon.circom 源码
        |
   在 Clean 中手动建模
        |
Lean 证明的可靠性和完备性
        |
优化后的 Poseidon 规范
        |
与非优化规范及 circomlibjs 的测试向量一致

这一结果之所以有用，正是因为这种转移。问题不再是“我们是否正确检查了 402 个见证变量和数十个轮常量？”（这是人类读者很难自信回答的），而是“这个 Clean 模型是否与它所声称建模的 Circom 电路匹配？”——审计者可以通过并排阅读两者来验证这一点。

下一步

当前的证明覆盖 arity 1。Circomlib Poseidon 也常用于 arity 2、3 和 4，例如在二叉树 Merkle 树和更宽的哈希输入中。

这些 arity 的规范和测试向量已经存在。下一步是扩展电路证明。同样的模式应该可以沿用：一个小型 S 盒电路、带有内联算术的轮级组件、以及阶段级的循环电路。较难的部分再次是更大状态宽度下的组合问题。

还有两种自然的方式来强化这个陈述：

  1. 证明优化版和非优化版的 Poseidon 规范对所有输入等价，

  2. 机械地将 Clean 模型与原始 Circom 源码或编译器输出连接起来。

当前的结果是一个有用的里程碑：一个机器检查的证明，表明一个现实世界的优化 ZK 哈希电路模型精确地计算了它声称要计算的函数，而最后一个缺失的假设被归约为一个经典的素性证书。

致谢 我们感谢 Gregor Mitscha-Baude、平井洋一和 David Tedgui 对 Clean 证明的帮助以及对这篇博文的有价值评论。

zkSecurity 为密码学系统提供审计、研究和开发服务，包括零知识证明、MPC、FHE 和共识协议。

了解更多 →

  • 原文链接： blog.zksecurity.xyz/post...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
微信扫码分享

相关文章

0 条评论

登录后发表评论