介绍clean：一个用于Lean4中ZK电路的形式验证DSL - ZKSECURITY

我们很高兴分享我们在 Lean4 中构建用于 ZK 电路的 clean(一个嵌入式 DSL 和形式化验证框架) 的初步步骤。 正如我们最近分享的那样，零知识电路充满了错误，但幸运的是，诸如形式化验证之类的技术可以极大地提高对 ZK 电路正确性的信心。 Clean 使我们能够在 Lean4 中定义电路，指定其所需的属性，并且——最重要的是——正式证明它们！

这项工作是zkEVM 形式化验证项目的一部分，该项目旨在提供基础设施和工具，以支持 zkEVM 的形式化验证。 请阅读下面关于 clean 的内容，或在 zkEVM 项目更新电话会议中观看我们关于它的演示文稿。

iframe

目标

我们的目标是构建一个嵌入式 DSL，用于在 Lean4 中编写 ZK 电路，这使我们能够以正式的方式推理它们。 我们相信，将电路定义与其所需的规范和正确性证明并置将使我们能够创建一个强大的可重用、经过形式化验证的电路 小工具(gadget) 库。

我们目前以 AIR 算术化为目标，并且我们假设底层证明系统提供了一个表查找 原语(primitive)。 但是，我们的长期目标是将 clean 转变为一个通用的 ZK 框架，该框架也适用于所有其他算术化。

如何形式化验证 ZK 电路

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

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

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

• 变量的集合，以及
• 对这些变量的约束和查找关系。 零知识证明系统的目标正是说服验证者，证明者 知道 一个见证(即，变量的赋值)，该见证 满足(satisfies) 给定电路的约束和查找。

在基本层面上，对于给定的电路，我们感兴趣的是约束的满足和见证之间的关系。 换句话说：如果一个见证满足约束，我们可以从中推断出什么属性？

让我们举一个具体的例子。 考虑一个仅由一个约束组成并且在一个变量 x 上定义的电路：

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

这是一个非常常见的 小工具(gadget)，可确保 x 是一个布尔值，即，它是 0 或 1。 该电路的规范可以表示为：

x = 0 ∨ x = 1

尽管这是一个非常简单的示例，但它显示了基本思想：我们有兴趣正式证明，如果对变量的赋值满足约束，则规范也成立。 我们还对另一个方向感兴趣：如果一个诚实的证明者持有一个满足规范的见证，则存在一个变量赋值满足约束。 采用以下布尔检查的替代实现：

C2 : x === 0

这个新约束是 可靠的(sound)，因为唯一满足它的有效赋值是 x = 0，这是一个布尔值。 但是，它不是 完备的(complete)，因为持有有效布尔值 x = 1 的诚实证明者无法提供满足约束的见证。

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

• 可靠性(Soundness)：如果证明者可以展示任何满足电路定义的约束和查找关系的见证，则某些规范属性适用于该见证。证明此属性可确保电路不会 约束不足(underconstrained)。
• 完备性(Completeness)：对于每个可能的输入，诚实的证明者始终可以展示一个满足电路定义的约束和查找关系的见证。证明此属性可确保电路不会 约束过度(overconstrained)。

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

实际上，我们可以：

• Witness：在电路中引入 m 个新变量，并将它们添加到见证中。 此操作还接受一个 compute 函数，该函数表示诚实证明者情况下的 见证生成(witness generation) 函数。
• Assert：向电路添加新约束。
• Lookup：向电路添加新的查找关系。查找定义了正在查找哪些变量以及在哪个其他表中查找。
• Subcircuit：向电路添加一个新的子电路。 子电路在当前环境中实例化，子电路的内部变量被添加到见证中。 这是获得 小工具(gadget) 可组合性(composability) 的主要方式。

为了增强可用性，我们提供了一种使用 monadic 接口定义电路的方法，该接口具有许多便利功能。 该接口使我们能够使用非常自然的语法结构来定义电路。

可组合验证框架的设计

我们框架的主要构建块是 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)

此结构以依赖类型的方式紧密地打包以下对象：

• β 和 α 分别是输入和输出“形状”。从本质上讲，它们定义了元素的结构化集合。
• main：电路定义本身。
• assumptions：电路对输入所做的假设。所有属性的证明都假定输入变量满足这些假设。
• spec：电路的规范属性。
• soundness：电路可靠性的证明。
• completeness：电路完备性的证明。

FormalCircuit 封装了一个经过形式证明，可重用的 小工具(gadget)：在将 FormalCircuit 实例化为子电路时，我们能够重用子电路的可靠性和完备性证明，以证明整个电路的可靠性和完备性属性。 这是通过自动将子电路的约束替换为其(经过形式验证的)规范来完成的。 通过这种方式，我们可以通过应用 分而治之 的方法来形式化验证甚至大型电路：我们首先定义和证明低级可重用 小工具(gadget) 的正确性，然后将它们组合起来以构建越来越复杂的电路。

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

让我们来看一下我们已经实现和验证的简单 小工具(gadget) 之一：8 位数字的加法。 这是一个 小工具(gadget)，它将两个字节和一个输入进位作为输入，并返回两个字节对 256 取模的和以及输出进位。

首先，我们需要定义输入和输出形状。

structure Inputs (F : Type) where
  x: F
  y: F
  carry_in: F

structure Outputs (F : Type) where
  z: F
  carry_out: F

现在，我们定义电路对输入值所做的假设，以及电路应满足的规范。

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
  -- 对 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
  -- ensures that the output carry is boolean
  -- 通过实例化 Boolean.circuit 作为子电路来确保输出进位是布尔值
  assertion Boolean.circuit carry_out

  -- main 8-bit addition constraint
  -- 主要的 8 位加法约束
  assert_zero (x + y + carry_in - z - carry_out * (const 256))

  return { z, carry_out }

最后，我们定义 FormalCircuit 结构，该结构将所有这些定义与可靠性和完备性证明一起打包

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

请注意，此定义是通用的，适用于 域素数(field prime) p。但是，我们需要对 素数(prime) 进行额外的假设，即 p > 512，否则电路将不可靠！

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

验证具体的 AIR 表

FormalCircuit 抽象提供了已验证电路的模块化定义，并且在很大程度上与算术化无关。 但是，我们希望以 AIR 作为具体的算术化为目标，因为它是 zkVM 设计领域中非常受欢迎的选择。 AIR 电路是在 轨迹(traces) 上定义的: 约束与 应用域(application domain) 一起指定，该 应用域(application domain) 表示应该将约束应用于哪些行。 原则上，可以选择任意 域(domain)。但是，在实践中，我们选择在消失多项式方面具有简洁表示的 域(domain)。

以下是一些 域(domain) 的示例，这些 域(domain) 具有简洁的表示形式并在实践中使用：

• 该约束应用于 轨迹(trace) 的一个特定行。这通常被称为 边界约束(boundary constraint)。
• 该约束应用于 轨迹(trace) 的所有行。这通常被称为 循环约束(recurring constraint)。一个功能是应用于每一行的约束都可以访问相邻的行：例如，它们可以访问下一行或上一行。
• 该约束应用于所有行，除了选定的小行集。例如，它可以应用于除最后一行或除第一行之外的每一行。
• 该约束应用于 轨迹(trace) 的每 n 行。

作为一个具体的例子，假设我们要对 轨迹(trace) 施加一个约束，以正确计算 斐波那契数列(Fibonacci sequence)，其定义如下： {F0=0F1=1Fn=Fn−2+Fn−1

我们可以使用由两列组成的 轨迹(trace) 来实现它：x 和 y。 我们要证明的不变量是：在第 i 行中，xi 应该包含 Fi，而 yi 应该包含 Fi+1。 我们可以通过施加以下约束来实现此行为：

• 我们对第一行施加一个 边界(boundary) 约束：x0=0 且 y0=1。
• 此外，我们施加两个 循环(recurring) 约束，以实现递归关系：对于每个 i – 除最后一个外 –, yi+1=xi+yi，且 xi+1=yi。

这组约束在下图中描述。

很容易看出，如果 轨迹(trace) 满足这些约束，那么在第 i 行中，我们将在第一列中找到第 i 个斐波那契数。

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

• 边界(boundary) 约束确保 初始状态是有效的(initial state is valid)，而
• 循环(recurring) 约束确保 状态转换函数(state transition function) 执行正确(executed correctly)。

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

• 定义一个归纳 轨迹(trace) 数据结构，我们将其建模为行序列。
• 建模使用特定 域(domain) 将约束应用于 轨迹(trace) 的含义：实际上，这是通过提供从抽象变量到具体 轨迹(trace) 单元格的赋值，然后应用原始约束语义来完成的。

你可以在此处查看使用 8 位加法的斐波那契表的可靠性证明，该证明满足以下稍微复杂的规范： 对于每一行 i,xi=(Fimod256)

即将开展的工作

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

• 继续添加低级 小工具(gadget)，以便我们拥有丰富的基本可重用电路库。
• 定义常见的哈希函数电路并证明其正确性。
• 为 RISC-V 的子集构建一个经过形式验证的最小 VM。

整个项目是开源的，可以在GitHub上找到，请务必查看！

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