使用 Picus 验证 SP1 电路的确定性：Veridise 与 Succinct 之间的合作

Veridise 最近完成了与 Succinct 的初步合作，以评估 Picus 的使用——我们的工具用于形式化验证零知识 (ZK) 电路的确定性——在 SP1 上，Succinct 的 RISC-V zkVM。目标是评估 Picus 验证 SP1 电路的能力，并为更广泛地验证所有 SP1 电路的确定性奠定基础。

在合作过程中，我们使用 Picus 成功证明了几个 SP1 电路的确定性。我们还确定了原型验证流水线中的关键改进，这些改进将使 Picus 能够扩展到更复杂的电路——我们很高兴在下一阶段的合作中一起实施这些改进。

为什么检查确定性在 ZK 电路安全中很重要

ZK 电路中大多数关键的错误都源于欠约束逻辑——缺少方程式，导致恶意证明者可以生成开发者不希望的可验证证明。这些所谓的欠约束错误破坏了可靠性，并且出了名的难以检测。

确定性提供了一个强大的保障：如果一个电路的输出由其输入唯一确定，那么就不可能出现任何非预期行为。因此，证明确定性是排除一整类错误的实用方法。

有了 Picus，我们可以正式证明确定性——从数学上保证电路的行为完全符合预期，没有歧义或对抗性操作的空间。

构建桥梁：将 Succinct SP1 电路转换为 Picus

将 Picus 应用于 SP1 的一个关键挑战是电路表示的不匹配。Picus 在用 LLZK 编写的电路上运行，LLZK 是 Veridise 的中间表示，而 SP1 电路是在 Plonky3 中定义的。为了弥合这一差距，我们开发了一个原型提取器，将 Plonky3 电路转换为 LLZK。非常感谢 Succinct 的 CTO John Guibas 在此开发过程中提供的指导。

我们的提取器有两个主要组成部分：

• air-llzk：一个访问器，遍历 Plonky3 约束 AST 并发出 LLZK。
• llzk-bridge：LLZK 的 C++ API 的 Rust 绑定，使 Rust 程序能够生成 LLZK 电路。我们希望这个绑定可以被重用，以支持未来其他基于 Rust 的 EDSL，如 Halo2。

有了这个基础设施，我们能够将 Picus 应用于越来越多的 SP1 电路，并形式化验证它们的确定性。

早期结果：成功验证了 11 个操作

一旦提取流水线到位，我们便开始将基本的 SP1 操作 转换为 LLZK。转换之后，使用 Picus 验证确定性就像按下一个按钮一样简单——我们成功提取并验证了以下操作：

Plonky3 到 LLZK 流水线中的当前限制

虽然最初的结果很有希望，但扩展 Picus 以验证更复杂的 SP1 电路揭示了当前从 Plonky3 到 LLZK 的转换流水线中的几个关键限制：

1. 缺乏模块化约束块

Plonky3 尚未支持约束的逻辑分组，这使得 Picus 难以独立地推理子组件。

2. 没有原生的输入/输出注释

我们必须手动指定输入和输出列。对于小型电路来说，这是可行的，但对于更大的模块来说，可能会变得容易出错且不可扩展。理想情况下，在电路开发过程中，开发者会指定列之间的功能关系。

3. 缺少对假设和后置条件的支持

当验证一个由许多子电路组成的大型电路时，能够将整个证明分解为每个子组件的较小证明非常重要。然而，子电路证明通常依赖于调用者做出的假设——例如，输入经过范围检查，位于字节范围内。相反，调用者可能依赖于被调用者提供的保证——例如，在 one-hot 编码中，只有一个输出设置为 1。

理想情况下，这些假设和保证可以表示为代码库中的注释，并自动提取到 LLZK 中，以便在验证期间使用。

Succinct 已经认识到这些差距的重要性，并且已经投入工程资源来扩展他们的 Plonky3 Air builder（定义约束的 Rust API）来解决这些问题。

未来展望：跨所有 Succinct SP1 电路的形式化验证

我们计划继续与 Succinct 的合作，并扩展我们的桥梁，以便 Picus 可以验证 SP1 中的所有电路。通过上面指定的改进，我们乐观地认为，正式的确定性检查将成为 SP1 电路开发的常规组成部分。

作者： Shankara Pailoor，Veridise 的 ZK 工具负责人

想要了解更多关于 Veridise 的信息吗？

Twitter | LinkedIn | Github | Request Audit

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