ZK Security Logo get in touch about us 介绍 clean，一个使用 Lean4 构建的用于 ZK 电路的 Formal Verification DSL

Written by Giorgio Dell'Immagine on Mar 27, 2025

我们非常高兴分享我们在构建 clean 方面迈出的初步 পদক্ষেপ，clean 是一个嵌入式 DSL 和 formal verification 框架，用于 Lean4 中的 ZK 电路。正如我们最近分享的，Zero Knowledge 电路充满 bugs，但幸运的是，像 formal verification 这样的技术可以极大地提高我们对 ZK 电路正确性的信心。Clean 使我们能够在 Lean4 中定义电路，指定其所需的属性，并且——最重要的是——正式地证明它们！这项工作是 zkEVM Formal Verification Project 的一部分，该项目旨在提供基础设施和工具，以实现对 zkEVM 的 formal verification。请阅读下面的 clean，或者在 zkEVM 项目更新电话会议上观看我们的演示。

目标

我们的目标是构建一个用于在 Lean4 中编写 zk 电路的嵌入式 DSL，该 DSL 允许我们以正式的方式对它们进行推理。我们相信，将电路定义与其所需的规范和正确性证明放在一起将使我们能够创建一个健壮的可重用的正式验证的电路小工具库。

我们目前的目标是 AIR arithmetization，并且我们假设底层证明系统提供了一个表查找原语。

如何正式验证 ZK 电路

为了正式地推理 ZK 电路，我们首先需要定义一个正式模型。这涉及以下步骤：

  1. 定义我们的电路语言支持哪些primitives，即，我们可以使用哪些操作来定义电路。
  2. 定义这些 primitives 的semantics。
  3. 定义我们感兴趣为给定电路正式证明的properties。

我们的语言允许我们指定一个 circuit，它由两个主要对象组成。

在基本层面上，对于给定的电路，我们感兴趣的是 constraints 的满足和 witness 之间如何关联。换句话说：如果一个 witness 满足 constraints，我们可以从中推断出什么 property？

让我们举一个具体的例子。考虑一个定义在一个变量 x 上的电路，它只由一个 constraint 组成：

C1 : x * (x - 1) === 0

这是一个非常常见的 gadget，它确保 x 是一个 boolean 值，即，它要么是 0，要么是 1。这个电路的规范可以表示为：

x = 0 ∨ x = 1

尽管这是一个非常简单的例子，但它展示了基本思想：我们有兴趣正式证明，如果变量的赋值满足 constraints，那么规范也成立。我们也对另一个方向感兴趣：如果一个诚实的证明者持有一个满足规范的 witness，那么存在一个满足 constraints 的变量赋值。以下是 boolean 检查的另一种实现方式

C2 : x === 0

这个新的 constraint 是 sound，因为满足它的唯一有效赋值是 x = 0，这是一个 boolean 值。然而，它不是 complete，因为一个诚实的证明者持有一个有效的 boolean x = 1 无法提供一个满足 constraint 的 witness。

更正式地说，我们想要证明的两个 properties 是：

DSL 设计

在我们的 DSL 中，我们支持四种基本操作来定义电路。

inductive Operation (F : Type) [Field F] where
 | witness : (m: ℕ) -> (compute : Environment F -> Vector F m) -> Operation F
 | assert : Expression F -> Operation F
 | lookup : Lookup F -> Operation F
 | subcircuit : {n : ℕ} -> SubCircuit F n -> Operation F

实际上，我们可以：

为了提高可用性，我们提供了一种使用 monadic interface 定义电路的方法，具有许多便利函数。此 interface 允许我们使用非常自然的语法结构定义电路。

可组合验证框架的设计

我们框架的主要构建块是 FormalCircuit 结构。

structure FormalCircuit (F: Type) (β α: TypeMap)
 [Field F] [ProvableType α] [ProvableType β]
where
 main: Var β F -> Circuit F (Var α F)
 assumptions: β F -> Prop
 spec: β F -> α F -> Prop
 soundness:
  ∀ offset : ℕ, ∀ env,
  -- for all inputs that satisfy the assumptions
  ∀ b_var : Var β F, ∀ b : β F, eval env b_var = b ->
  assumptions b ->
  -- if the constraints hold
  constraints_hold.soundness env (circuit.main b_var |>.operations offset) ->
  -- the spec holds on the input and output
  let a := eval env (circuit.output b_var offset)
  spec b a
 completeness:
  -- for all environments which _use the default witness generators for local variables_
  ∀ offset : ℕ, ∀ env, ∀ b_var : Var β F,
  env.uses_local_witnesses (circuit.main b_var |>.operations offset) ->
  -- for all inputs that satisfy the assumptions
  ∀ b : β F, eval env b_var = b ->
  assumptions b ->
  -- the constraints hold
  constraints_hold.completeness env (circuit.main b_var |>.operations offset)

此结构以 dependent-type 方式紧密地打包以下对象：

FormalCircuit 封装了一个正式证明的、可重用的 gadget：当实例化一个 FormalCircuit 作为 subcircuit 时，我们能够重用 subcircuit 的 soundness 和 completeness 证明来证明整个电路的 soundness 和 completeness properties。这是通过 自动将 subcircuit 的 constraints 替换为其 (经过正式验证的) spec 来完成的。通过这种方式，我们可以通过应用 divide-et-impera 方法来正式验证甚至大型电路：我们首先定义和证明低级可重用 gadget 的正确性，然后将它们组合起来构建越来越复杂的电路。

一个具体的例子：8 位加法

让我们来看看我们已经实现和验证的一个简单的 gadget：8 位数字的加法。这是一个 gadget，它将两个字节和一个输入 carry 作为输入，并返回两个字节的和模 256，以及输出 carry。首先，我们需要定义输入和输出形状。

structure Inputs (F : Type) where
 x: F
 y: F
 carry_in: F
structure Outputs (F : Type) where
 z: F
 carry_out: F

现在，我们定义电路对输入值的 assumptions，以及电路应该满足的规范。

def assumptions (input : Inputs (F p)) :=
 let { x, y, carry_in } := input
 x.val < 256 ∧ y.val < 256 ∧ (carry_in = 0 ∨ carry_in = 1)
def spec (input : Inputs (F p)) (out : Outputs (F p)) :=
 let { x, y, carry_in } := input
 out.z.val = (x.val + y.val + carry_in.val) % 256 ∧
 out.carry_out.val = (x.val + y.val + carry_in.val) / 256

主电路定义如下。

def add8_full_carry (input : Var Inputs (F p)) :
  Circuit (F p) (Var Outputs (F p)) := do
 let { x, y, carry_in } := input
 -- witness the result
 let z <- witness (fun eval => mod_256 (eval (x + y + carry_in)))
 -- do a lookup over the byte table for z
 lookup (ByteLookup z)
 -- witness the output carry
 let carry_out <- witness (fun eval => floordiv (eval (x + y + carry_in)) 256)
 -- ensures that the output carry is boolean
 -- by instantiating the Boolean.circuit as a subcircuit
 assertion Boolean.circuit carry_out
 -- main 8-bit addition constraint
 assert_zero (x + y + carry_in - z - carry_out * (const 256))
 return { z, carry_out }

最后，我们定义 FormalCircuit 结构，它将所有这些定义与 soundness 和 completeness 证明一起打包。

def circuit : FormalCircuit (F p) Inputs Outputs where
 main := add8_full_carry
 assumptions := assumptions
 spec := spec
 soundness := by
  ...
 completeness := by
  ...

请注意，此定义是 generic over the field prime p，但是我们需要对素数进行额外的假设，即 $p > 512$，否则电路不 sound!

variable {p : ℕ} [Fact p.Prime]
variable [p_large_enough: Fact (p > 512)]

验证具体的 AIR 表

FormalCircuit 抽象提供了经过验证的电路的模块化定义，并且它在很大程度上与 arithmetization 无关。但是，我们希望以 AIR 作为具体的 arithmetization 为目标，因为它是 zkVM 设计领域中非常流行的选择。AIR 电路是在 traces 上定义的：constraints 与 application domain 一起指定，这表示它们应该应用于哪些行。原则上，可以选择任意 domain，但是，在实践中，我们选择在 vanishing polynomial 方面具有简洁表示的 domains。

以下是一些具有简洁表示并在实践中使用的 domain 的示例。

作为一个具体的例子，假设我们想要给出一个 trace 的 constraint，用于正确地计算 Fibonacci sequence，其定义如下。 $$ \begin{cases} F_0 = 0 \\ F_1 = 1 \\ F_n = F_{n-2} + F_{n-1} \end{cases} $$ 我们可以使用由两列组成的 trace 来实现它：$x$ 和 $y$。我们想要证明的 invariant 是：在第 $i$ 行，$x_i$ 应该包含 $F_i$，而 $y_i$ 应该包含 $F_{i+1}$。我们可以通过施加以下 constraints 来实现此行为。

Fibonacci trace 很容易看出，如果一个 trace 满足这些 constraints，那么在第 $i$ 行，我们将在第一列中找到第 $i$ 个 Fibonacci 数。

请注意，这组 constraints 也可以被认为是定义了一个正确的 states 序列，每个状态对应一行：

在我们的框架中，我们通过以下方式支持 AIR constraints：

您可以在此处查看使用 8 位加法的 Fibonacci 表的 soundness 证明，该证明满足以下稍微复杂的规范： $$ \text{For every row } i, \quad x_i = (F_i \mod 256) $$

即将进行的工作

该框架仍处于开发的早期阶段，但已经显示出令人鼓舞的结果。一些计划的后续步骤是：

整个项目是开源的，可在 GitHub 上获得，请务必查看！