深入探讨 Cairo 的 AIR 以及我们在 Lambdaworks 中为兼容 Starknet Stone Prover 所做的更改

介绍

在最近的几个月里，我们一直在努力将 Lambdaworks STARK Platinum prover 与 Starknet 的 Stone prover 结合起来。我们还希望 STARK Platinum 足够灵活，可以用作其他 STARK prover 的直接替代品，例如 Winterfell（在 Miden 中用作默认 prover）。其中一个主要的困难在于如何以一种简单且可表达的方式提供 algebraic intermediate representation (AIR) 和约束，并能够尝试和测试几种 trace configuration layouts。在之前的文章中，我们讨论了 STARK prover 的不同设计选择，例如使用虚拟列、内置组件和芯片以及它们的权衡。我们希望 prover 尽可能模块化，以便我们可以尝试不同的设计选项，整合新的工具或字段，并评估性能。之前的方法的一个不便之处是，AIR 的更改或选择新的布局需要大量的重写。此外，当使用虚拟列时，prover 必须为每个约束提供 zerofiers，这取决于列的交错方式，使得它既困难又容易出错。

在这篇文章中，我们将介绍在 STARK Platinum 中实现 transition constraints 和 AIR 的新方法，这应该会让我们在测试和移动事物方面有更多的自由，从而更直接地添加新的布局。我们还提供工具来评估 zerofiers，而无需用户给出确切的表达式。如果你不熟悉某些概念，你可以看看我们关于 STARKs 的文章 1 和 2。

Transition constraints

我们定义了 public trait pub trait TransitionConstraint<F, E>: Send + Sync where F: IsSubFieldOf<E> + IsFFTField + Send + Sync, E: IsField + Send + Sync,，它包含处理 transition constraints 所需的所有方法。它对两个字段是泛型的，F 是基本字段，E 可能是 F 的字段扩展。如果我们不需要扩展字段，我们将简单地使 E 等于 F。基本字段也应该是 FFT 友好的字段，也就是说，它应该包含大小为 $2^m$ 的乘法子群（例如，$p=2^{64}−2^{32}+1$ 具有大小为 $2^{64}−2^{32}$ 的乘法群，它可以被 $2^{32}$ 整除）。下面，我们列出主要方法：

• fn degree 给出 transition constraint 的度数。Cairo vm 的所有约束的度数最多为 3。约束的度数越高，计算 transition constraints 所需的评估域就越大。
• fn constraint_idx 给出约束标识符，这是一个介于 0 和 transition constraints 总数之间的唯一整数。
• fn evaluate 提供了如何在 trace 的低度扩展 (LDE) 上评估约束的方法。根据约束，可能需要 periodic_values 或 rap_challenges。这些值存储在 transition_evaluations 向量中，位置与 constraint_idx 相对应。
• fn period 指示约束应用的频率。如果约束在每个步骤都应用，则设置为 1。某些约束可能每隔几个步骤应用一次（例如，16 或 256），这对于正确评估 zerofier 是必要的。
• fn offset 指示我们从第一个步骤开始应用约束的位置。如果约束从第一个步骤开始应用，则设置为 0。如果约束从 1 开始，周期为 16，这意味着该约束对步骤 1、17、33、49 等有效。我们需要这个来正确评估 zerofier。
• fn end_exemptions 指示约束是否应用于 trace 的最后 $n$ 步。如果它应用于每个步骤，则设置为 0。如果最后两个步骤不强制执行约束，则设置为 2。
• fn exemptions_period 和 fn periodic_exemptions_offset 是从约束中删除几个中间步骤所必需的。所有 exemptions 都是正确评估 zerofier 所必需的。
• 几个用于评估约束的 zerofier 的方法 fn end_exemptions_poly、fn zerofier_evaluations_on_extended_domain 和 fn evaluate_zerofier。第二个函数需要评估组合多项式，而第三个函数需要在域外点 $z$ 处进行评估。

理解 exemptions 和 zerofiers

斐波那契数列

为了确定 exemptions 的工作方式，让我们看一些例子。最容易理解的是 end_exemptions。例如，在计算斐波那契数列时会出现这些情况：

$a_0 = a_1 = 1$

$a{n+2} = a{n+1} + a_n$

单个 trace 列可以表示这一点，并且可以用以下多项式关系表示：

$t(g^2x) - t(gx) - t(x) = 0$

除了最后两个计算步骤外，此约束对所有计算步骤都有效。请记住，我们用 $g$ 的幂表示每个步骤，$g$ 是第 $n$ 个单位本原根（$n$ 等于 trace 长度）。因此，zerofier 看起来像

$ZC(x) = \prod{i=0}^{n-3} (x - g^i) = \frac{\prod_{i=0}^{n-1} (x - g^i)}{(x - g^{n-2})(x - g^{n-1})}$

zerofier 是

$Z(x) = \prod_{i=0}^{n-1} (x - g^i) = x^n - 1$

而 exemptions 只是

$E(x) = (x - g^{n-2})(x - g^{n-1})$

两者的组合给出了约束的 zerofier。为了表示这些约束，我们将使 fn end_exemptions 返回 2，fn period 返回 1，fn offset 产生 0。

Cairo Flags 示例

此示例遵循 Cairo vm 中包含所有标志的虚拟列中的约束。AIR 在这里提供。该列由 15 个二进制值的重复组成，后跟一个零值。有两个 transition constraints：

$t(1-t) = 0$

$t = 0$

第一个约束对除每第 16 个值之外的所有值都成立。另一方面，第二个约束仅对每 16 行成立，从第 15 行开始。让我们首先计算第二个约束的 zerofier：

$Z_C(x) = (x - g^{15})(x - g^{31})(x - g^{47})...$

项数为 $n/16$。我们可以将 $g^{15}$ 作为公因子，并调用 $y = x/g^{15}$。因此，

$ZC(x) = g^{15 \cdot n/16} \prod{j=0}^{n/16 - 1} (y - g^{16j})$

请记住，如果 $g$ 是第 $n$ 个单位根，$g^{16}$ 是第 $n/16$ 个单位根。由于我们将所有 $n/16$ 个单位根相乘，我们得到

$Z_C(y) = g^{15 \cdot n/16} (y^{n/16} - 1)$

分配并记住 $x$ 和 $y$ 之间的关系

$Z_C(x) = x^{n/16} - g^{15 \cdot n/16}$

此 zerofier 与等于 15 的 fn offset 和等于 16 的 fn period 兼容，没有 exemptions。

可以通过了解整个 trace 的 zerofiers 和零标志约束的 zerofier 来计算第一个约束的 zerofier。这是，

$ZF(x) = \frac{x^n - 1}{x^{n/16} - g^{15 \cdot n/16}}$

第一个约束的 fn periodic_exemptions_offset 等于 15，fn exemptions_period 等于 16，本质上计算与零标志相同的 zerofier 并从完整 trace zerofier 中获取它。

Algebraic Intermediate Representation

我们建立了一个 AIR trait，其中包含表示 trace、约束及其评估所需的所有方法。

方法 fn trace_layout(&self) -> (usize, usize) 提供了主 trace 和辅助 trace 的列数（如果存在）。主 trace 包含基本字段中的元素（例如，Stark252 或 Mini-Goldilocks）。相比之下，如果需要，辅助 trace 可能具有扩展字段中的元素，以实现密码安全性。

为了评估 transition constraints，我们有方法 fn compute_transition_prover、fn compute_transition_verifier、fn transition_constraints 和 fn transition_zerofier_evaluations。

fn transition_zerofier_evaluations 具有默认实现。鉴于某些约束可能共享相同的 zerofier（因为它们在执行 trace 的相同步骤中应用），我们通过使用 zerofier_group_key 进行检查来避免重新计算 zerofiers。

 fn transition_zerofier_evaluations(
        &self,
        domain: &Domain<Self::Field>,
    ) -> Vec<Vec<FieldElement<Self::Field>>> {
        let mut evals = vec![Vec::new(); self.num_transition_constraints()];

        let mut zerofier_groups: HashMap<ZerofierGroupKey, Vec<FieldElement<Self::Field>>> =
            HashMap::new();

        self.transition_constraints().iter().for_each(|c| {
            let period = c.period();
            let offset = c.offset();
            let exemptions_period = c.exemptions_period();
            let periodic_exemptions_offset = c.periodic_exemptions_offset();
            let end_exemptions = c.end_exemptions();

            // This hashmap is used to avoid recomputing with an fft the same zerofier evaluation
            // If there are multiple domains and subdomains they can be further optimized
            // as to share computation between them

            let zerofier_group_key = (
                period,
                offset,
                exemptions_period,
                periodic_exemptions_offset,
                end_exemptions,
            );
            zerofier_groups
                .entry(zerofier_group_key)
                .or_insert_with(|| c.zerofier_evaluations_on_extended_domain(domain));

            let zerofier_evaluations = zerofier_groups.get(&zerofier_group_key).unwrap();
            evals[c.constraint_idx()] = zerofier_evaluations.clone();
        });

        evals
    }

实现 CairoAIR

CairoAIR 的实现从这里开始。我们首先定义 fn new，它包含 64 个约束、transition exemptions 和 AIRContext。由于 Stone Prover 使用虚拟列，因此约束的最终数量（计算 transition 和 boundary constraints）将为 46。主 trace 有六列，辅助 trace 有 2 列。一个步骤的普通布局可以在我们 prover 的文档中找到。

每个约束的 TransitionConstraint trait 的实现在这里完成。这是使用普通布局的 CairoAIR 的 transition constraints 列表：

• BitPrefixFlag0
• BitPrefixFlag1
• BitPrefixFlag2
• BitPrefixFlag3
• BitPrefixFlag4
• BitPrefixFlag5
• BitPrefixFlag6
• BitPrefixFlag7
• BitPrefixFlag8
• BitPrefixFlag9
• BitPrefixFlag10
• BitPrefixFlag11
• BitPrefixFlag12
• BitPrefixFlag13
• BitPrefixFlag14
• ZeroFlagConstraint
• InstructionUnpacking
• CpuOperandsMemDstAddr
• CpuOperandsMem0Addr
• CpuOperandsMem1Addr
• CpuUpdateRegistersApUpdate
• CpuUpdateRegistersFpUpdate
• CpuUpdateRegistersPcCondPositive
• CpuUpdateRegistersPcCondNegative
• CpuUpdateRegistersUpdatePcTmp0
• CpuUpdateRegistersUpdatePcTmp1
• CpuOperandsOpsMul
• CpuOperandsRes
• CpuOpcodesCallPushFp
• CpuOpcodesCallPushPc
• CpuOpcodesAssertEq
• MemoryDiffIsBit0
• MemoryDiffIsBit1
• MemoryDiffIsBit2
• MemoryDiffIsBit3
• MemoryDiffIsBit4
• MemoryIsFunc0
• MemoryIsFunc1
• MemoryIsFunc2
• MemoryIsFunc3
• MemoryIsFunc4
• MemoryMultiColumnPermStep0_0
• MemoryMultiColumnPermStep0_1
• MemoryMultiColumnPermStep0_2
• MemoryMultiColumnPermStep0_3
• MemoryMultiColumnPermStep0_4
• Rc16DiffIsBit0
• Rc16DiffIsBit1
• Rc16DiffIsBit2
• Rc16DiffIsBit3
• Rc16PermStep0_0
• Rc16PermStep0_1
• Rc16PermStep0_2
• Rc16PermStep0_3
• FlagOp1BaseOp0BitConstraint
• FlagResOp1BitConstraint
• FlagPcUpdateRegularBit
• FlagFpUpdateRegularBit
• CpuOpcodesCallOff0
• CpuOpcodesCallOff1
• CpuOpcodesCallFlags
• CpuOpcodesRetOff0
• CpuOpcodesRetOff2
• CpuOpcodesRetFlags

我们将看看 BitPrefixFlag0 约束的实现，我们在下面重现它：

impl TransitionConstraint<Stark252PrimeField, Stark252PrimeField> for BitPrefixFlag0 {
    fn degree(&self) -> usize {
        2
    }

    fn constraint_idx(&self) -> usize {
        0
    }

    fn evaluate(
        &self,
        frame: &stark_platinum_prover::frame::Frame<Stark252PrimeField, Stark252PrimeField>,
        transition_evaluations: &mut [Felt252],
        _periodic_values: &[Felt252],
        _rap_challenges: &[Felt252],
    ) {
        let current_step = frame.get_evaluation_step(0);

        let constraint_idx = self.constraint_idx();

        let current_flag = current_step.get_main_evaluation_element(0, constraint_idx);
        let next_flag = current_step.get_main_evaluation_element(0, constraint_idx + 1);

        let one = Felt252::one();
        let two = Felt252::from(2);

        let bit = current_flag - two * next_flag;

        let res = bit * (bit - one);

        transition_evaluations[constraint_idx] = res;
    }

    fn end_exemptions(&self) -> usize {
        0
    }
}

此约束表明对应于 Flag0 的变量是二进制的，即 $b \in {0, 1}$。从数学上讲，此条件表示为 $b(1-b) = 0$。

首先，我们定义约束的度数。由于定义约束 $b(1-b) = 0$ 的多项式是二次的，因此度数函数将返回 2。接下来，我们定义约束索引或标识符，它必须介于 0 和 63 之间。我们为该约束选择 0（但如果我们要使约束按另一个顺序排列，我们可以更改它，如果我们必须重新排列约束以实现兼容性，这将很方便）。在这种情况下，由于变量必须在每个执行步骤中都是二进制的，因此 end_exemptions 只是 0。

我们现在可以跳转到约束的 evaluate 函数。为了评估约束，我们需要 frame（包含来自主 trace 和辅助 trace 的 LDE 的元素）和 transition_evaluations，我们将修改它以添加对应于约束的值。第 17 行获取当前步骤的评估 frame，并使用约束索引，我们搜索当前和下一个标志（这是 Stone Prover 中使用的一种优化）。我们在第 27 行获取标志的位，并在第 29 行计算约束表达式（如果我们使用有效 trace 的值评估它，这应该是零）。最后，我们将该值存储在位置 constraint_idx 的 transition_evaluations 中。

结论

在这篇文章中，我们介绍了 STARK Platinum 中引入的用于处理 transition constraints 和 AIR 定义的更改。这将帮助我们更轻松地使用不同的布局，并避免让用户通过提供显式表达式来定义 zerofiers。我们介绍了如何定义 zerofiers 以及如何进行约束评估。我们还认为这些更改将有助于测试其他功能，例如在 Starknet 中使用较小的字段（尽管这可能需要进一步的更改）。

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