Poseidon1 证明详解

===== 开始 MARKDOWN_CONTENT ===== 本文档详细介绍了针对 BN254 的 Poseidon 元数-1（$t=2$）可靠性（soundness）与完备性（completeness）证明的结构，该证明在 Poseidon.lean 中实现，并与 Clean/Specs/Poseidon.lean 和 Clean/Specs/PoseidonOptimized.lean 中的规范进行对照。

1. 从非优化的输出规范开始

Clean/Specs/Poseidon.lean 定义了一个简单、非优化的 Poseidon 置换，参数化为 $t$，用作输出层的参考规范：

• S 盒 $\sigma(x) = x^5$ (BN254)
• ark：添加轮常量切片 C[offset..offset+t]
• mix：乘以完整的 MDS 矩阵 $M$ ($t \times t$)
• fullRoundCircom：sbox_full → ark → mix
• partialRoundCircom：仅对元素 0 执行 sbox，仅对元素 0 执行 ark，执行 mix（完整 M 矩阵）
• poseidon1..poseidon4：元数 $t=2..5$ 的完整哈希，轮调度为 ARK_initial → 4 个全轮 → nP 个部分轮 → 3 个全轮 → (SBOX → MIX)

该文件并非优化后的 circom 电路或当前 circomlibjs 参考实现的逐行模型。特别是，poseidon_reference.js 在其循环内部使用了传统的在 S 盒之前添加轮常数的轮顺序。Clean/Specs/Poseidon.lean 的作用是提供一个紧凑的、完整 MDS 的、输出兼容的参考规范，并对照 circomlibjs 向量进行验证。

参考资料：

• Grassi, Khovratovich, Rechberger, Roy, Schofnegger.
  Poseidon: A New Hash Function for Zero-Knowledge Proof Systems.
  USENIX Security '21. <https://eprint.iacr.org/2019/458>
• iden3 circomlibjs, src/poseidon_reference.js（用作测试向量交叉检查的输出预言机的参考 JS 实现）。
  <https://github.com/iden3/circomlibjs/blob/main/src/poseidon_reference.js>

常量 C_t*、M_t* 直接复制自 circomlib 的 poseidon_constants.circom。

2. 与 circomlibjs 进行交叉检查

为防止常量和轮调度中的转录错误，规范文件包含了来自 circomlibjs 的测试向量：

每个测试都是一个 example : poseidon_k inputs = known_hash := by native_decide（参见 Clean/Specs/Poseidon.lean 底部）。共 7 个向量。

3. 专门针对 circomlib 优化变体

Clean/Specs/PoseidonOptimized.lean 定义了与 circomlib 的优化版 circuits/poseidon.circom 调度相对应的变体（即 poseidon.circom 使用优化形式 —— Clean/Specs/Poseidon.lean 不是 poseidon.circom 的结构模型，仅是预期输出的模型）：

• 在从第一个全轮过渡到部分轮时，使用一个预稀疏矩阵 $P$。
• 部分轮使用稀疏混合矩阵（mixS），每轮仅需 3 个非平凡常量，而非 $t^2$ 个。
• poseidon1Opt、poseidon2Opt、poseidon3Opt 实现了此调度。

数学上，这应当与标准变体等价（这是 circomlib/snarkjs 使用的标准“Poseidon 优化技巧”）。Lean 定义是对优化的元数-1 电路结构的直接手工建模，Clean 逐约束地证明了该电路。

参考：

• iden3 circomlib, circuits/poseidon.circom（该文件手工建模了其元数-1 结构的优化 circom 电路）。
  <https://github.com/iden3/circomlib/blob/master/circuits/poseidon.circom>

等价性通过同一文件中的 native_decide 测试向量经验性地建立：

• poseidon1Opt = poseidon1 在输入 1、0、123、BN254_PRIME - 1 上成立
• poseidon2Opt = poseidon2 在 [1,2]、[0,0]、[1,0]、[0,1]、[3,4]、[12345, 67890]、[BN254_PRIME-1, 1] 上成立——加上一个与已知 circomlibjs 哈希的匹配。
• poseidon3Opt = poseidon3 在 [1,0,0]、[0,0,0]、[1,2,3] 上成立——加上两个与已知 circomlibjs 哈希的匹配。

（没有 poseidon1Opt = poseidon1 的正式证明；仅通过该测试集进行验证。）

4. 每个组件电路的可靠性与完备性

Clean/Circomlib/Poseidon.lean 为每个 Poseidon 构建块引入了一个 FormalCircuit，并分别解决其 soundness + completeness 义务。每个组件都足够小，可以用 circuit_proof_start + 几行策略脚本证明：

5. 将组件组合成 Poseidon1

顶层 Poseidon1.main 电路由 6 个阶段组成：

let state ← InitialArk.circuit input
let state ← ApplyFullRounds.circuit 2 (by omega) state
let state ← FullRound_t2.circuit C_t2 P_t2 ⟨8, by omega⟩ state
let state ← ApplyPartialRoundsOpt.circuit state
let state ← ApplyFullRounds.circuit 66 (by omega) state
let state ← FullRound_t2.circuit (.replicate 72 0) M_t2 ⟨0, by omega⟩ state
return state[0]

最终定理的内容

def circuit : FormalCircuit F field field where
  ...
  Spec (input : F) (output : F) :=
    output = Specs.PoseidonOptimized.poseidon1Opt input
  soundness := ...
  completeness := ...

因此，Clean 电路模型精确实现了 poseidon1Opt。该优化后的规范与 poseidon1 以及 circomlibjs 在所有测试输入上一致。将这些串联起来，可以高度（尽管并非完全形式化）确信元数-1 的 circomlib Poseidon 电路计算了指定的哈希。

正式证明了什么？

正式证明：

• Clean 模型 Poseidon1.circuit 相对于 Specs.PoseidonOptimized.poseidon1Opt 是可靠的：任何满足的赋值都会产生指定的输出。
• Clean 模型 Poseidon1.circuit 是完备的：对于每个输入，诚实证明者的见证都满足约束。
• 组件证明涵盖了 S 盒、初始 ARK、全轮、折叠全轮、优化部分轮、折叠部分轮以及完整的元数-1 组合。

尚未正式证明：

• 从原始 poseidon.circom 源码到此 Clean 模型的转换未经过机械检查；它是对相同优化结构的直接手工建模。
• poseidon1Opt = poseidon1 仅在代表性输入上进行了测试，但未对所有域元素进行证明。
• BN254 素数实例仍用 sorry 声明；可以单独用 Pratt/Lucas 证书关闭。

开放项

• instance : Fact (Nat.Prime BN254_PRIME) 使用 by sorry 声明（位于 Clean/Circomlib/Poseidon.lean 顶部附近）。关闭它需要一个 Pratt/Lucas 证书；Mathlib 的 lucas_primality 是合适的工具。
• poseidon1Opt = poseidon1 仅通过 native_decide 对少量输入进行了检查，未得到证明。
• 元数 2、3、4 具有规范和测试向量，但没有电路或形式化证明。 ===== 结束 MARKDOWN_CONTENT =====

• 原文链接： github.com/Verified-zkEV...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～