zkVM DSL对比：Halo2、Zirgen 和 Plonky3

零知识证明领域的技术创新呈爆炸式增长，但在密码学的复杂性之下，存在一个根本性的挑战：开发人员如何以零知识系统可以验证的方式表达计算逻辑？答案在于约束语言——领域特定语言（DSL），它弥合了熟悉的编程概念与零知识证明的数学基础之间的差距。

这篇文章比较了三种不同的约束编写方法：DarkFi zkVM 中使用的 Halo2 的 PLONKish 电路、RISC Zero 的基于 STARK 的虚拟机编译器 Zirgen，以及 Ziren 和 SP1 中使用的 Plonky3 的直接 AIR 约束编写。每种方法都代表了一种不同的理念，即开发人员应该如何与零知识系统交互，从高级抽象到低级数学原语。

理解这些差异不仅仅具有学术意义。你选择的约束语言不仅会影响你编写证明的方式，还会影响你思考计算本身的方式。有些方法通过类型系统来优先考虑安全性，有些方法通过直接控制来优化性能，还有一些方法则侧重于算法的自然表达。通过一个通用的 Fibonacci 示例来检验它们的架构、数据模型和实际实现，我们可以理解每种方法何时发挥作用，以及开发人员必须应对的权衡。

无论你是构建保护隐私的应用程序、可验证的计算系统，还是首次探索零知识证明，此比较都将帮助你了解现状，并为你的特定需求选择合适的工具。

电路架构

Halo2

Halo2 构建于 PLONKish 算术化之上，它将计算表示为一个值矩阵，其中每个单元格包含域元素。可以把它想象成一个电子表格，其中每一行代表一个计算步骤，列则保存不同类型的数据。PLONKish 电路根据值的矩形矩阵来定义，其中约束（称为门）强制执行这些值之间的关系，而选择器可以为不同的行打开或关闭特定的约束。

Halo2 API 通过分层架构巧妙地抽象了这种底层矩阵表示。核心是芯片，它们封装了特定的计算逻辑。使用它们的 API，开发人员可以定义“知道”如何使用特定组的自定义门以进行高效计算的芯片。例如，可以有一个芯片来实现特定的密码学算法，如标量乘法或配对。

在芯片之上，开发人员通常通过gadget进行交互，它们提供了一个更稳定和方便的 API。虽然芯片实现了特定的算法，比如乘法或配对，但 gadget 是更通用的抽象——例如，Halo2 中内置的 ECC gadget 封装了所有的椭圆曲线运算，在内部组合了乘法和配对芯片。这种间接性很有用，因为出于效率和 PLONKish 电路的限制，芯片接口通常依赖于低级实现细节，而 gadget 接口提供了一个更方便和稳定的 API，隐藏了这些细节。

layouter 编排所有内容，管理不同的芯片和区域如何在电路矩阵中排列。它负责门的 spatial 组织，并确保有效地利用可用的电路面积。

Halo2 的 API 的一个关键设计原则是电路配置和 witness 分配之间的明确分离。configure 阶段定义了电路的结构——列、门和约束——而 synthesize 阶段则用实际的 witness 值填充电路。这种分离允许相同的电路定义用于不同的证明实例，只有 witness 数据在运行之间发生变化。

Zirgen

Zirgen 构建于 STARK 证明系统之上，它以与 PLONKish 电路根本不同的方式表示计算。虚拟机的算术化是指将每条指令执行的状态转换表示为一个多项式。与矩形矩阵不同，STARK 使用执行跟踪——一段时间内的机器状态序列，其中每一行代表一个计算步骤，列代表寄存器值或内存位置。

DSL 通过提供更高级别的构造来抽象手动编写 AIR 约束的复杂性，这些构造被编译成 STARK 证明器所需的多项式约束。

该架构围绕组件展开，这些组件封装了计算的逻辑单元，类似于 Halo2 中芯片的工作方式，但专为 STARK 跟踪的顺序性质而定制。每个组件定义寄存器（状态变量）和控制这些寄存器如何从一个步骤演变到下一个步骤的转换多项式。为了获得转换多项式，证明器以符号方式在跟踪多项式中评估转换约束。

与 Halo2 的 spatial layouter 系统不同，Zirgen 通过定义机器状态进度的周期来顺序地组织计算。DSL 提供了控制流构造和条件逻辑，它们被编译成适当的多项式约束，允许开发人员以更自然的命令式风格表达算法逻辑，同时保持零知识证明所需的数学严谨性。

Plonky3

约束系统建立在 STARK 的代数中间表示（AIR）之上，具有以下几个关键模式：

在 Air::eval(...) 方法内部，开发人员使用 AirBuilder 编写 trace上的多项式恒等式。构建器提供对当前行（本地）和下一行（单步旋转）的访问以表达状态转换，镜像程序执行的顺序性质。

指示器和选择器列编码指令分派，其功能类似于 Halo2 中的选择器，但具有 VM 特定的语义。该系统强制每个执行周期只激活一种指令类型，并且每条指令的语义约束都受 when_...() 函数保护。

边界约束通过第一行和最后一行保护建立虚拟机的初始和最终状态。

模块化架构允许将虚拟机的不同方面实现为单独的 AIR 模块——CPU 逻辑、ALU 操作、内存管理和 I/O 处理都可以有自己的约束实现。一个更高级别的聚合器管理跨表约束，创建清晰的关注点分离。

结果是一个系统，它允许开发人员以熟悉的命令式、循序渐进的方式思考，同时直接使用 STARK 系统所需的多项式约束原语。与更高级别的抽象不同，这种方法提供了对约束生成的细粒度控制，同时保持了在虚拟机上证明程序执行的概念清晰度。

列类型：数据容器

Halo2

Halo2 电路使用三种基本列类型，每种都有不同的用途：

Advice 列保存私有 witness 数据——只有证明者知道的秘密输入和中间计算结果。这些值随每次证明生成而变化，并包含正在计算的实际数据。

Instance 列存储证明者和验证者都知道的公共输入和输出。这些是电路公开提交的值，例如哈希函数的输入或计算的最终结果。

Fixed 列包含电路常量和配置数据，这些数据在所有证明实例中都保持不变。矩阵中的列数，以及每个列作为固定列、advice 列或 instance 列的规范，定义了电路结构。

选择器是特殊的 fixed 列，用于启用或禁用特定行上的特定约束。它们就像开关，允许同一个门仅在需要时才激活，从而使电路更加灵活和高效。

struct FibonacciConfig {
    advice: Column<Advice>,
    selector: Selector,
    instance: Column<Instance>,
}

上面的代码将我们的电路将使用的特定列分组到一个配置结构中。

Zirgen

Zirgen 电路围绕两个基本的寄存器组件构建，这些组件处理执行跟踪中状态管理的不同方面：

基础是 NondetReg 组件，它在跟踪中创建一个单独的列，并允许证明者写入任何值而无需施加约束。“Nondeterministic”一词表示这些寄存器本质上是自由变量，证明者可以任意设置，使它们成为将 witness 数据引入电路的主要机制。

在此基础之上，Reg 组件提供受约束的寄存器行为。它也内置于语言中，并被定义为包装了带有附加等式约束的 NondetReg 的组合：

component Reg(v: Val) {
   reg := NondetReg(v);
   v = reg;
   reg
}

这个实现展示了 Zirgen 的组合方法——Reg 接受一个 NondetReg 并添加一个约束，确保寄存器的值等于输入参数。这会将不受约束的 witness 分配转换为确定性分配，其中寄存器的值完全由电路逻辑指定。

这种双层设计展示了 Zirgen 的架构原则，即从基本的、可组合的组件构建复杂的约束系统。原始 witness 分配和受约束分配之间的分离为开发人员提供了引入任意 witness 数据的灵活性，以及强制执行确定性计算关系的工具。

Plonky3

与 Halo2 的类型化列系统（Advice/Instance/Fixed）或 Zirgen 的声明式寄存器关键字（Reg/NondetReg）不同，Plonky3 的方法将所有跟踪元素视为通用的列，没有固有的类型区分。语义角色——数据是公共的还是私有的，受约束的还是不受约束的——完全来自你如何连接约束和边界条件，而不是来自编译时类型注释。

这种设计理念反映了 Plonky3 的较低级别的约束编写方法。Plonky3 不是提供编码常见模式的高级抽象，而是让开发人员直接访问底层数学原语，从而需要为其他系统自动提供的行为构造显式约束。

受约束与不受约束的列完全由约束的存在决定。只有在 Air::eval(...) 中断言方程时，列才会受到约束。如果没有约束将列与其他值相关联——没有等式、范围检查或转换关系触及它——则该列充当证明者可以任意设置的自由 witness 数据。没有特殊的 NondetReg 类型；不受约束的行为源于约束的不存在。

公共数据与私有数据代表协议边界，而不是列分类。公共值通过证明的 public_values 向量流动，证明者和验证者都知道该向量。你的 AIR 必须通过边界约束（例如“第一行等于公共输入”或“最后一行等于公共输出”）将特定的 trace 单元显式绑定到这些公共插槽。所有未显式绑定到公共插槽的内容都保留为私有 witness 数据。

选择器列和指示器列通过你手动约束为布尔值的普通列来处理指令分派和控制流。该系统不提供特殊的选择器类型——你必须显式断言每个布尔标志为 s(1-s) = 0，并确保互斥的操作码满足 ∑ᵢ sᵢ = 1。然后，你使用这些指示器门控特定于操作码的恒等式，从而创建指令集语义所需的条件逻辑。

这种方法创造了力量和责任。缺乏内置类型安全性意味着你很容易意外创建不受约束的列——忘记覆盖一种指令情况或省略边界约束会在 witness 中留下自由度。但是，这种灵活性允许精确控制约束生成，并且在谨慎使用时可以带来更高效的电路。

公共接口

Halo2

公共输入流和输出通过实例列，从而在私有电路计算和公共接口之间创建桥梁。最常见的模式是使用 assign_advice_from_instance() 将公共值从实例列复制到 advice 列，advice 列中可以使用它们进行私有计算。

例如，在 Fibonacci 电路中，前两个 Fibonacci 数和最终输出是公共的——它们被加载到实例列中，然后复制到 advice 列中，advice 列中会发生实际的计算。函数 constrain_instance 用于约束 cell 中实例列的行值和绝对位置。

expose_public() 模式同样重要，它允许通过将私有计算结果约束到特定的实例列位置来使其公开。这在私有计算逻辑和公共接口之间创建了清晰的分离，同时保持了密码学保证。

let mut a_cell = region.assign_advice_from_instance(
    || "1",
    self.config.instance,
    0,
    self.config.advice,
    0,
)?;

pub fn expose_public(
    &self,
    mut layouter: impl Layouter<F>,
    cell: AssignedCell<F, F>,
    row: usize,
) -> Result<(), Error> {
    layouter.constrain_instance(cell.cell(), self.config.instance, row)
}

Zirgen

Zirgen 通过 public 关键字管理私有计算和公共验证之间的边界，该关键字将特定寄存器标记为外部可见。公共寄存器充当电路内部状态和外部验证器之间的接口，类似于 Halo2 的实例列如何桥接私有和公共数据。

当寄存器被标记为公共时，其在执行跟踪中特定点的值将成为公共输入/输出接口的一部分。这允许电路提交到某些计算结果或接受外部输入，同时保持中间计算步骤的私密性。证明者必须证明公共值与电路的执行一致，而无需公开私有 witness 数据。

component CycleCounter() {
  cycle := NondetReg(GetCycle());
  public is_first_cycle := IsZero(cycle);

  ...
}

Plonky3

Plonky3 的公共数据处理方法与 Halo2 的实例列和 Zirgen 的 public 关键字都有根本的不同。在 Plonky3 框架中，证明携带一个 域元素的 public_values 向量，证明者和验证者都知道该向量。至关重要的是，没有列本质上是按类型“公共的”——你必须在 Air::eval() 中使用边界约束或受保护的约束来绑定这个向量中的特定跟踪单元和指定的槽。

公共接口协定需要约束作者和证明使用者之间的仔细协调。public_values 中元素的顺序必须与你编写的约束绑定完全匹配，从而创建一个精确但可能很脆弱的接口规范。

let pis = builder.public_values();

let a = pis[0];
let b = pis[1];
let x = pis[2];

...

when_first_row.assert_eq(local.left.clone(), a);
when_first_row.assert_eq(local.right.clone(), b);
builder.when_last_row().assert_eq(local.right.clone(), x);

第一行和最后一行绑定表示输入/输出处理的最常见模式。这种方法在初始执行步骤中注入输入，并在最后一步公开输出，模仿传统的程序接口：

当计算具有清晰的初始化和完成阶段时，此模式效果很好，但要求所有公共输入在程序启动时可用，并且所有输出在程序完成时准备就绪。

Witnesses、约束和门：计算核心

Halo2

advice 列中的 witness 数据驱动实际计算，但约束确保正确性。Halo2 提供了几种强大的约束模式，这些模式超越了简单的同行关系。

同行约束是最直接的，它关系到单行内的值。在 Fibonacci 示例中，create_gate 函数定义了一个门，其约束为 s * (a + b - c)，这确保了当选择器 s 处于活动状态时，值 a + b 必须等于同一行中的 c。

旋转约束允许门跨越多行，从而在同一列中不同行的值之间创建关系。Fibonacci 门中的 Rotation::next() 和 Rotation(2) 展示了这一点——我们约束当前值加上下一个值等于两行下的值。这对于需要访问先前计算状态的算法特别强大。

复制约束强制不同位置的单元格包含相同的值，这通过 Halo2 的排列参数实现。这些约束是使用 AssignedCell::copy_advice 调用建立的，但需要通过 ConstraintSystem::enable_equality 为相关列启用排列检查。它们对于连接电路的不同部分并确保跨区域的数据一致性至关重要。

查找参数完全提供了一种不同的约束机制，允许电路证明 witness 值存在于预定义的查找表中，而无需公开访问了哪些特定条目。这对于范围检查或通过表格查找实现复杂函数等操作特别有用。

赋值过程通过 layouter 填充这些 witness 值，通常在将相关约束分组在一起的 assign_region() 调用中。每个区域代表一个具有自己局部坐标系的计算逻辑单元，从而使电路开发更模块化和可管理。

meta.create_gate("add", |meta| {
    let s = meta.query_selector(selector);
    let a = meta.query_advice(advice, Rotation::cur());
    let b = meta.query_advice(advice, Rotation::next());
    let c = meta.query_advice(advice, Rotation(2));
    vec![s * (a + b - c)]
});

Zirgen

在 Zirgen 基于 STARK 的模型中，计算核心围绕状态转换和控制寄存器如何在执行跟踪中演变的约束展开。witness 数据由完整的执行跟踪组成——演示有效计算的寄存器状态序列。

同一步骤约束在单个执行步骤中运行，关系到必须在同一时间点满足某些关系的寄存器值。这些约束类似于 Halo2 的同行约束。例如，约束可能确保两个寄存器始终在同一计算步骤中加起来成为第三个寄存器。

偏移约束使用 @ 语法在执行跟踪中不同点的寄存器值之间创建关系。@ 运算符允许引用先前或未来步骤中的寄存器值。例如，reg@1 引用前一个执行步骤中寄存器的值。这种顺序引用对于表达跨越多个计算周期的状态机转换和算法依赖关系至关重要。

通过 mux（多路复用器）类型的条件逻辑在电路中提供分支功能。mux 允许电路根据寄存器值在不同的计算路径之间进行选择，从而在保持 STARK 系统所需的多项式约束的同时实现复杂的控制流。这个分支机制被编译成多项式约束，确保在任何给定时间只有一个分支处于活动状态。

component CycleCounter() {
  global total_cycles := NondetReg(6);

  cycle := NondetReg(GetCycle());
  public is_first_cycle := IsZero(cycle);

  [is_first_cycle, 1-is_first_cycle] -> ({
    // First cycle; previous cycle should be the last cycle.
    cycle@1 = total_cycles - 1;
  }, {
    // Not first cycle; cycle number should advance by one for every row.
    cycle = cycle@1 + 1;
  });
  cycle
}

  // Copy previous two terms forward
  d2 : Reg;
  d3 : Reg;
  d1 := Reg([first, 1-first] -> (f0, d2@1));
  d2 := Reg([first, 1-first] -> (f1, d3@1));

  // Compute the next Fibonacci term
  d3 := Reg(d1 + d2);

Plonky3

约束是你在 Air::eval(...) 中编写的多项式恒等式，当替换为实际 witness 值时，这些恒等式必须评估为零。 约束编写通过构建器 API 的行访问和断言方法完成。你使用主跟踪的当前行和下一行（概念上为“本地”和“下一个”旋转），使用构建器方法（如 assert_eq 和 assert_zero）来发出多项式等式。这种直接访问消除了约束意图和底层数学实施之间的抽象层。

保护机制通过行选择器提供条件约束应用程序。每个保护包装断言，以确保它们仅应用于预期的行：

• 边界保护处理初始和最终状态的“第一行”和“最后一行”条件
• 转换保护覆盖逐步关系的所有内部行

每个保护将你的恒等式乘以一个选择器多项式，该选择器多项式在预期的行上等于 1，在其他地方等于 0，从而创建对约束应用位置的精确数学控制。 边界约束**通过固定第一行或最后一行的特定单元格并将指定的单元格绑定到公共向量条目来处理输入/输出和初始化，就像我们在上一节中看到的那样。

转换约束使用本地/下一个访问来关系到连续的执行步骤，以强制执行状态演变。一般形式 s_trans · F(local, next) = 0 捕获了机器状态必须如何从一个周期前进到下一个周期。

行本地门控语义在操作码或分支指示符下实现特定于操作的逻辑。当选择器 s_k 处于活动状态时，约束 s_k · G_k(local) = 0 强制执行适当的计算语义。

范围和字节约束使用查找参数来证明全局表中的成员资格，而不是临时不等式，从而为结构化值提供有效的范围检查。

在 Plonky3 的方法中，控制和责任意味着你通过保护直接控制身份的应用位置，以及通过断言强制执行的内容。没有单独的“门对象”——你编写的多项式恒等式就是门。这种能力伴随着相应的责任：仅当边界约束明确地将单元格与公共向量中的位置联系起来时值才会变为公共值，而不是通过列类型声明。

常见的陷阱源于不完整的约束覆盖。通过缺少保护或边界联系来留下未约束的列或执行分支会创建可能损害证明健全性的自由度。忘记对指示符进行布尔运算或求和为一约束，或者省略对字节或标志等结构化值的范围检查，可能会允许无效的 witness 分配来满足约束系统。

let mut when_transition = builder.when_transition();

// a' <- b
when_transition.assert_eq(local.right.clone(), next.left.clone());

// b' <- a + b
when_transition.assert_eq(local.left.clone() + local.right.clone(), next.right.clone());

Fibonacci 示例：将所有内容放在一起

Halo2

让我们跟踪提供的 Fibonacci 实现，以了解这些概念在实践中的运用。该电路从初始值 1、1 开始计算第 9 个 Fibonacci 数 (55)。

use halo2_proofs::{arithmetic::FieldExt, circuit::*, plonk::*, poly::Rotation};
use std::marker::PhantomData;

#[derive(Debug, Clone)]
struct ACell<F: FieldExt>(AssignedCell<F, F>);

#[derive(Debug, Clone)]
struct FibonacciConfig {
    advice: Column<Advice>,
    selector: Selector,
    instance: Column<Instance>,
}

#[derive(Debug, Clone)]
struct FibonacciChip<F: FieldExt> {
    config: FibonacciConfig,
    _marker: PhantomData<F>,
}

impl<F: FieldExt> FibonacciChip<F> {
    pub fn construct(config: FibonacciConfig) -> Self {
        Self {
            config,
            _marker: PhantomData,
        }
    }

    pub fn configure(
        meta: &mut ConstraintSystem<F>,
        advice: Column<Advice>,
        instance: Column<Instance>,
    ) -> FibonacciConfig {
        let selector = meta.selector();

        meta.enable_equality(advice);
        meta.enable_equality(instance);

        meta.create_gate("add", |meta| {
            //
            // advice | selector
            //   a    |   s
            //   b    |
            //   c    |
            //
            let s = meta.query_selector(selector);
            let a = meta.query_advice(advice, Rotation::cur());
            let b = meta.query_advice(advice, Rotation::next());
            let c = meta.query_advice(advice, Rotation(2));
            vec![s * (a + b - c)]
        });

        FibonacciConfig {
            advice,
            selector,
            instance,
        }
    }

    pub fn assign(
        &self,
        mut layouter: impl Layouter<F>,
        nrows: usize,
    ) -> Result<AssignedCell<F, F>, Error> {
        layouter.assign_region(
            || "entire fibonacci table",
            |mut region| {
                self.config.selector.enable(&mut region, 0)?;
                self.config.selector.enable(&mut region, 1)?;

                let mut a_cell = region.assign_advice_from_instance(
                    || "1",
                    self.config.instance,
                    0,
                    self.config.advice,
                    0,
                )?;
                let mut b_cell = region.assign_advice_from_instance(
                    || "1",
                    self.config.instance,
                    1,
                    self.config.advice,
                    1,
                )?;

                for row in 2..nrows {
                    if row < nrows - 2 {
                        self.config.selector.enable(&mut region, row)?;
                    }

                    let c_cell = region.assign_advice(
                        || "advice",
                        self.config.advice,
                        row,
                        || a_cell.value().copied() + b_cell.value(),
                    )?;

                    a_cell = b_cell;
                    b_cell = c_cell;
                }

                Ok(b_cell)
            },
        )
    }

    pub fn expose_public(
        &self,
        mut layouter: impl Layouter<F>,
        cell: AssignedCell<F, F>,
        row: usize,
    ) -> Result<(), Error> {
        layouter.constrain_instance(cell.cell(), self.config.instance, row)
    }
}

#[derive(Default)]
struct MyCircuit<F>(PhantomData<F>);

impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
    type Config = FibonacciConfig;
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self {
        Self::default()
    }

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let advice = meta.advice_column();
        let instance = meta.instance_column();
        FibonacciChip::configure(meta, advice, instance)
    }

    fn synthesize(
        &self,
        config: Self::Config,
        mut layouter: impl Layouter<F>,
    ) -> Result<(), Error> {
        let chip = FibonacciChip::construct(config);

        let out_cell = chip.assign(layouter.namespace(|| "entire table"), 10)?;

        chip.expose_public(layouter.namespace(|| "out"), out_cell, 2)?;

        Ok(())
    }
}

#[cfg(test)]
mod tests {
    use super::MyCircuit;
    use std::marker::PhantomData;
    use halo2_proofs::{dev::MockProver, pasta::Fp};

    #[test]
    fn fibonacci_example2() {
        let k = 4;

        let a = Fp::from(1); // F[0]
        let b = Fp::from(1); // F[1]
        let out = Fp::from(55); // F[9]

        let circuit = MyCircuit(PhantomData);

        let mut public_input = vec![a, b, out];

        let prover = MockProver::run(k, &circuit, vec![public_input.clone()]).unwrap();
        prover.assert_satisfied();

        public_input[2] += Fp::one();
        let _prover = MockProver::run(k, &circuit, vec![public_input]).unwrap();
        // uncomment the following line and the assert will fail
        // _prover.assert_satisfied();
    }
}

FibonacciConfig 定义了列结构：一个用于计算序列的 advice 列，一个用于公共值的 instance 列（初始值和最终结果），以及一个用于控制何时激活加法门的选择器。

自定义门 s * (a + b - c) 强制执行 Fibonacci 递推关系。启用选择器后，它会约束当前值加上下一个值等于两行下的值。旋转系统允许在 PLONKish 约束中优雅地表达这种顺序关系。

在赋值期间，前两个 advice 单元格使用 assign_advice_from_instance() 从公共实例值初始化。然后，代码迭代其余位置，将每个新的 Fibonacci 数计算为前两个数的和，并将结果分配给 advice 列。

选择器管理至关重要——我们为前 8 行（索引 0-7）启用它，但为最后两行禁用它，以避免约束不存在的值。这证明了选择器提供的对约束激活的细粒度控制。

最后，expose_public() 约束最终计算值以匹配实例列中预期的公共输出，从而完成公共-私有接口。

该测试演示了肯定和否定两种情况：使用 F[9] = 55 进行正确的计算满足所有约束，而不正确的预期输出 (56) 将导致证明失败，从而表明密码学保证如何防止作弊。

这个例子展示了 Halo2 API 的优雅之处：多项式承诺和约束系统等复杂的密码学概念被抽象为直观的操作，例如赋值、启用选择器和定义门。结果是一个既强大又足以用于复杂的密码学应用程序，又足够易于访问以进行实际开发的系统。

Zirgen

让我们研究 Zirgen 中提供的 Fibonacci 实现，以了解这些概念在实践中的工作方式。该电路在多个执行周期中计算 Fibonacci 数，展示了 Zirgen 的迭代计算方法。

extern GetCycle() : Val;

component IsZero(val: Val) {
  // Nondeterministically 'guess' the result
  isZero := NondetReg(Isz(val));

  // Compute the inverse (for non-zero values), for zero values, Inv returns 0
  inv := NondetReg(Inv(val));

  // isZero should be either 0 or 1
  isZero * (1 - isZero) = 0;
  // If isZero is 0 (i.e. nonzero) then val must have an inverse
  val * inv = 1 - isZero;
  // If isZero is 1, then val must be zero
  isZero * val = 0;
  // If isZero is 1, then inv must be zero
  isZero * inv = 0;
  isZero
}

test IsZeroTest {
  IsZero(0) = 1;
  IsZero(1) = 0;
  IsZero(2) = 0;
}

component CycleCounter() {
  global total_cycles := NondetReg(6);

  cycle := NondetReg(GetCycle());
  public is_first_cycle := IsZero(cycle);

  [is_first_cycle, 1-is_first_cycle] -> ({
    // First cycle; previous cycle should be the last cycle.
    cycle@1 = total_cycles - 1;
  }, {
    // Not first cycle; cycle number should advance by one for every row.
    cycle = cycle@1 + 1;
  });
  cycle
}

component Top() {
  global f0: Reg;
  global f1: Reg;
  global steps: Reg;

  cycle := CycleCounter();
  first := cycle.is_first_cycle;

  // Copy previous two terms forward
  d2 : Reg;
  d3 : Reg;
  d1 := Reg([first, 1-first] -> (f0, d2@1));
  d2 := Reg([first, 1-first] -> (f1, d3@1));

  // Compute the next Fibonacci term
  d3 := Reg(d1 + d2);

  // If cycle = steps, write the next term to the output
  public terminate := IsZero(cycle - steps + 1);
  [terminate, 1 - terminate] -> ({
    global f_last := Reg(d3);
    Log("f_last = %u", f_last);
  }, {});
}

component FibTest(f0: Val, f1: Val, steps: Val, out: Val) {
  // Supply inputs
  global f0 := Reg(f0);
  global f1 := Reg(f1);
  global steps := Reg(steps);

  top := Top();

  // Check the output
  [top.terminate, 1 - top.terminate] -> ({
    global f_last : Reg;
    f_last = out;
  }, {});
}

test FirstCycle {
  FibTest(1, 2, 1, 3);
}

test SecondCycle {
  FibTest(1, 2, 2, 5);
}

test SixthCycle {
  FibTest(1, 2, 6, 34);
}

```实现从 `IsZero` 组件开始，该组件展示了复杂的约束组合。它使用了两个 `NondetReg` 组件 —— 一个用于猜测输入是否为零 (`isZero`)，另一个用于计算倒数 (`inv`)。这些约束确保了数学上的一致性：`isZero * (1 - isZero) = 0` 强制结果为二进制，而 `val * inv = 1 - isZero` 确保非零值具有适当的倒数。这个组件展示了 Zirgen 如何通过数学约束而不是显式分支来处理条件逻辑。

`CycleCounter` 组件管理跨多个步骤的执行流程。它使用外部函数 `GetCycle()` 来跟踪当前的执行步骤，并使用 `IsZero` 组件来检测第一个周期。mux 语法 `[is_first_cycle, 1-is_first_cycle] -> ({...}, {...})` 展示了条件执行 —— 不同的约束块根据是否为第一个周期来激活。偏移约束 `cycle = cycle@1 + 1` 展示了寄存器值如何在执行步骤中演变，确保每个周期都正确递增。

在 `Top` 组件中，实际的斐波那契计算通过寄存器演变展开。全局寄存器 `f0`、`f1` 和 `steps` 存储初始条件和迭代计数。核心计算使用三个寄存器 (`d1`、`d2`、`d3`)，它们表示连续的斐波那契项，值通过偏移约束向前流动，例如 `d2@1` 引用前一个周期的值。

mux 结构 `[first, 1-first] -> (f0, d2@1)` 优雅地处理了初始化与继续逻辑 —— 在第一个周期，`d1` 采用初始值 `f0`，但在随后的周期中，它采用前一个周期的 `d2` 值。这个模式对于 `d2` 重复，创建了特征斐波那契滑动窗口。

终止检测使用 `IsZero(cycle - steps + 1)` 来识别何时应该完成计算，通过另一个 mux 结构触发最终的输出赋值。`terminate` 标志控制是否将最终结果写入全局 `f_last` 寄存器。

`FibTest` 组件展示了测试框架，设置初始条件并验证输出。这些测试展示了电路计算 F₃=3、F₄=5 和 F₈=34，验证了跨不同迭代计数的正确性。

这个例子说明了几个关键的 Zirgen 原则：组件自然地组合以构建复杂的功能，基于约束的条件逻辑取代了显式的控制流，偏移语法优雅地表达了跨周期的依赖关系，并且执行跟踪捕获了完整的计算演变。与 Halo2 的空间约束满足不同，Zirgen 的方法通过状态机在执行周期中的演变自然地表达了迭代算法。

### Plonky3

让我们来追踪提供的斐波那契实现，看看 Plonky3 在实践中如何直接编写约束。这个电路使用 Plonky3 的 AIR 框架计算斐波那契数列。

```rust code-highlight
use core::borrow::Borrow;

use p3_air::{Air, AirBuilder, AirBuilderWithPublicValues, BaseAir};
use p3_baby_bear::{BabyBear, Poseidon2BabyBear};
use p3_challenger::{DuplexChallenger, HashChallenger, SerializingChallenger32};
use p3_commit::ExtensionMmcs;
use p3_dft::Radix2DitParallel;
use p3_field::extension::BinomialExtensionField;
use p3_field::{Field, PrimeCharacteristicRing, PrimeField64};
use p3_fri::{HidingFriPcs, TwoAdicFriPcs, create_test_fri_params};
use p3_keccak::{Keccak256Hash, KeccakF};
use p3_matrix::Matrix;
use p3_matrix::dense::RowMajorMatrix;
use p3_merkle_tree::{MerkleTreeHidingMmcs, MerkleTreeMmcs};
use p3_symmetric::{
    CompressionFunctionFromHasher, PaddingFreeSponge, SerializingHasher, TruncatedPermutation,
};
use p3_uni_stark::{StarkConfig, prove, verify};
use rand::SeedableRng;
use rand::rngs::SmallRng;

/// 用于测试公共值特性
pub struct FibonacciAir {}

impl<F> BaseAir<F> for FibonacciAir {
    fn width(&self) -> usize {
        NUM_FIBONACCI_COLS
    }
}

impl<AB: AirBuilderWithPublicValues> Air<AB> for FibonacciAir {
    fn eval(&self, builder: &mut AB) {
        let main = builder.main();

        let pis = builder.public_values();

        let a = pis[0];
        let b = pis[1];
        let x = pis[2];

        let (local, next) = (
            main.row_slice(0).expect("Matrix is empty?"), //矩阵为空？
            main.row_slice(1).expect("Matrix only has 1 row?"), // 矩阵只有一行?
        );
        let local: &FibonacciRow<AB::Var> = (*local).borrow();
        let next: &FibonacciRow<AB::Var> = (*next).borrow();

        let mut when_first_row = builder.when_first_row();

        when_first_row.assert_eq(local.left.clone(), a);
        when_first_row.assert_eq(local.right.clone(), b);

        let mut when_transition = builder.when_transition();

        // a' <- b
        when_transition.assert_eq(local.right.clone(), next.left.clone());

        // b' <- a + b
        when_transition.assert_eq(local.left.clone() + local.right.clone(), next.right.clone());

        builder.when_last_row().assert_eq(local.right.clone(), x);
    }
}

pub fn generate_trace_rows<F: PrimeField64>(a: u64, b: u64, n: usize) -> RowMajorMatrix<F> {
    assert!(n.is_power_of_two());

    let mut trace = RowMajorMatrix::new(F::zero_vec(n * NUM_FIBONACCI_COLS), NUM_FIBONACCI_COLS);

    let (prefix, rows, suffix) = unsafe { trace.values.align_to_mut::<FibonacciRow<F>>() };
    assert!(prefix.is_empty(), "Alignment should match"); // 对齐应该匹配
    assert!(suffix.is_empty(), "Alignment should match"); // 对齐应该匹配
    assert_eq!(rows.len(), n);

    rows[0] = FibonacciRow::new(F::from_u64(a), F::from_u64(b));

    for i in 1..n {
        rows[i].left = rows[i - 1].right;
        rows[i].right = rows[i - 1].left + rows[i - 1].right;
    }

    trace
}

const NUM_FIBONACCI_COLS: usize = 2;

pub struct FibonacciRow<F> {
    pub left: F,
    pub right: F,
}

impl<F> FibonacciRow<F> {
    const fn new(left: F, right: F) -> Self {
        Self { left, right }
    }
}

impl<F> Borrow<FibonacciRow<F>> for [F] {
    fn borrow(&self) -> &FibonacciRow<F> {
        debug_assert_eq!(self.len(), NUM_FIBONACCI_COLS);
        let (prefix, shorts, suffix) = unsafe { self.align_to::<FibonacciRow<F>>() };
        debug_assert!(prefix.is_empty(), "Alignment should match"); // 对齐应该匹配
        debug_assert!(suffix.is_empty(), "Alignment should match"); // 对齐应该匹配
        debug_assert_eq!(shorts.len(), 1);
        &shorts[0]
    }
}

实现从通过 FibonacciRow<F> 的trace结构定义开始，它封装了斐波那契计算所需的两个值：left 和 right。这个简单的结构直接映射到 trace 列，其中 NUM_FIBONACCI_COLS = 2 定义了 trace 宽度。Borrow 实现提供了原始字段元素切片和结构化行表示之间的安全类型转换。

FibonacciAir 结构实现了定义约束结构和评估的核心 AIR 特征。BaseAir 实现只是声明了 trace 宽度，而 Air<AB> 实现包含了约束逻辑。

约束评估展示了 Plonky3 直接编写多项式恒等式的方法。通过显式切片和类型转换访问 trace 行，使你可以直接控制如何解释 witness 数据。

初始化边界约束将第一行绑定到公共输入。when_first_row() 保护确保这些约束仅在执行开始时应用。 用于递归的转换约束在所有内部行中实现斐波那契关系。when_transition() 保护将这些约束应用于除第一个和最后一个步骤之外的每个步骤。 输出边界约束将最终结果绑定到预期的公共值。

Witness 生成通过 generate_trace_rows() 单独发生，它模拟斐波那契计算以产生具体的字段元素赋值。这个 trace 生成创建了将在证明中提交的 witness 数据，每一行都包含该执行步骤的斐波那契对。

这个例子展示了 Plonky3 的哲学方法：约束正是你编写的多项式恒等式，没有隐藏的门抽象。三个约束族（初始化边界、转换、输出边界）直接实现了证明斐波那契计算正确性所需的数学关系。Witness 生成和约束规范之间的明确分离允许相同的 AIR 定义与不同的计算参数一起使用，同时保持密码学的健全性。

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