Lambdaworks 作为 Winterfell 的直接替代品来证明 Miden-VM

介绍

Lambdaworks 是我们用于有限域、椭圆曲线和证明系统的库。其中，我们有 STARK、Plonk、Groth 16 证明器，并且我们正在努力实现一个完全兼容的 使用 STARK 的 Cairo 证明器。我们希望继续添加新的证明系统和多项式承诺方案，以便用户拥有一个适合他们特定需求的库，并且易于进行实验。

在过去的几个月里，我们一直在努力与 Winterfell 兼容，这是一个流行的通用 STARK 证明器。Polygon 使用 Winterfell 来证明 Miden-VM 的执行，这是一个 ZK 友好的 VM，可以实现基于 EVM 的 L1 和 L2 目前无法提供的特性和优势。

即使主要组件相同，例如执行轨迹、辅助轨迹、使用 Merkle 树进行承诺和 FRI 协议，但在某些部分，将 Lambdaworks 用作 Winterfell 的直接替代品并不容易。一个障碍与域后端有关。Miden 被设计为在素数 $2^{64} - 2^{32} + 1$（有些人称之为 Mini-Goldilocks）上工作，并且必须处理扩展域以实现密码学安全性，而我们的 STARK 证明器使用 252 位域。在第一部分中，我们纯粹专注于兼容性，而忽略了我们可以添加以提高性能的优化。

在这篇文章中，我们将介绍我们为与 Winterfell 兼容所做的主要工作，以便你可以在需要时在你的项目中替换它。这增加了冗余和健壮性，因为我们有不同的、具有不同设计选择的证明器，并且可以帮助检测错误。

域和轨迹

为了与 Winterfell 配合使用，我们将 Lambdaworks 的域 trait 实现为 Winterfell 的原生域。换句话说，我们正在使用 Winterfell 域运行我们的 STARK 证明器。

由于 Miden 使用 mini-Goldilocks，因此从验证者那里提取的辅助轨迹和随机挑战属于域扩展。处理这个问题的一种简单方法是让所有元素都属于扩展域，这将增加主轨迹元素的开销（因为它们存在于较小的基域中）。

为了解决这个问题，我们将轨迹分为两部分，一部分属于主轨迹并使用小域，扩展部分属于较大的域。

此外，我们还添加了一些有用的泛化。由于很多时候，扩展域中的元素乘以属于基域的元素，因此可以改进该操作。这类似于我们在复数中做的那样，例如，当我们将其乘以实数时。如果我们想要计算 $2 \times (1 + i)$，我们进行分配并进行两次乘法，而不是使用公式 $(2 + 0i) \times (1 + i)$ 进行朴素的乘法。

为了处理这种情况，我们实现了 子域逻辑。这允许我们定义域元素之间的运算以及当子域元素与其父域元素运算时的特殊情况。并且由于这只是在编译时选择正确运算的问题，因此没有开销。所有这些额外的逻辑都不会给域增加开销，正如可以在我们的基准测试中测量的那样。

随着域的更改，我们还对 FFT 进行了更改，以便它可以在扩展域上工作。现在，辅助轨迹的插值和组合多项式的计算必须在更大的域上进行。

Winterfell 适配器

Winterfell 适配器将 Winterfell AIR（代数中间表示）转换为 Lambdaworks AIR。

在内部，它使用 Winterfell 中的所有配置创建一个 Air trait 的新实现。一个细节是，约束的评估在这里委托给 Winterfell 中的实现，以避免重新定义，这对于已经在 Winterfell 中定义了 Air 的人来说会花费更长的时间。

要查看它的工作原理，我们可以查看以下链接，其中包含一个如何为 Fibonacci AIR 生成证明的示例。让我们检查一下。

代码和示例

让我们看看 Winterfell 适配器是如何与一个简单的 Air 一起使用的。

Fibonacci Air

假设你想使用 WinterfellFibonacciAIR 运行 Lambdaworks 证明器。

use winterfell::Air;

struct WinterfellFibonacciAIR {
    /// ...
}

impl Air for WinterfellFibonacciAIR {
    /// ...
}

步骤 1：转换你的 Winterfell 轨迹表

使用 Lambdaworks AirAdapter 转换你的 Winterfell 轨迹：

let trace = &AirAdapter::convert_winterfell_trace_table(winterfell_trace)

步骤 2：转换你的公共输入

通过提供你的 winterfell_public_inputs 和 Lambdaworks 证明器所需的其他参数来创建 AirAdapterPublicInputs：

let pub_inputs = AirAdapterPublicInputs {
    winterfell_public_inputs: AdapterFieldElement(trace.columns()[1][7]),
    transition_degrees: vec![1, 1],    /// 每个转换的度数
    transition_exemptions: vec![1, 1], /// 转换不适用的结束步骤。
    transition_offsets: vec![0, 1],    /// 帧的大小。对于每个 Winterfell AIR，这可能都是 [0, 1]。
    composition_poly_degree_bound: 8,  /// 用于选择 H(x) 部分数量的组合度多项式的界限。
    trace_info: TraceInfo::new(2, 8),  /// 你的 winterfell 轨迹信息。
};

请注意，你可能还必须像本例中一样将你的域元素转换为 AdapterFieldElement。

步骤 3：生成证明

let proof = Prover::prove::<AirAdapter<FibonacciAIR, TraceTable<_>>>(
    &trace,
    &pub_inputs, /// 公共输入
    &proof_options,
    StoneProverTranscript::new(&[]),
);

TraceTable 是表示你的轨迹表的 Winterfell 类型。你可以查看此 crate 中的 examples 文件夹以查看更多示例。

Miden Air

让我们看看它如何与实际的 Miden AIR 和程序一起使用。

首先，我们必须编译并运行代码以生成轨迹。这以与 Miden 相同的方式完成。

整个代码有点长，但它是这样开始的：

let fibonacci_number = 16;
        let program = format!(
            "begin
                repeat.{}
                    swap dup.1 add
                end
            end",
            fibonacci_number - 1
        );
let program = Assembler::default().compile(program).unwrap();
...
// 中间还有一些代码，直到我们生成轨迹

let winter_trace = processor::execute(
    &program,
    stack_inputs.clone(),
    DefaultHost::default(),
    *ProvingOptions::default().execution_options(),)

从 Miden 生成轨迹后，证明器的真正工作就开始了。但是代码与 Fibonacci 案例并没有太大的不同；它只是有一个更复杂的 AIR，但是用户可以从中抽象出来。

要生成证明，我们运行以下代码：

let pub_inputs = AirAdapterPublicInputs {
    winterfell_public_inputs: pub_inputs,
    transition_exemptions: vec![2; 182],
    transition_offsets: vec![0, 1],
    trace_info: winter_trace.get_info(),
    metadata: winter_trace.clone().into(),
};

let trace =
    MidenVMQuadFeltAir::convert_winterfell_trace_table(winter_trace.main_segment().clone());

let proof = Prover::<MidenVMQuadFeltAir>::prove(
    &trace,
    &pub_inputs,
    &lambda_proof_options,
    QuadFeltTranscript::new(&[]),
)
.unwrap();

最后，要验证它，只需使用证明和公共输入调用验证函数：

Verifier::<MidenVMQuadFeltAir>::verify(
            &proof,
            &pub_inputs,
            &lambda_proof_options,
            QuadFeltTranscript::new(&[]),
        )

基准

要运行 Fibonacci Miden 基准测试，请运行：

cargo bench

要并行运行它，请运行：

cargo bench --features stark-platinum-prover/parallel,winter-prover/concurrent

几个 PR 为证明器和验证器添加了对扩展域的支持（716、717 和 724）。这些使我们能够在基域中表示轨迹（这具有更快的操作和更少的内存使用量），并且可以为扩展上的辅助轨迹提供不同的帧。约束计算中进行了一些修改，例如能够使用不同的域。

还有一个 Miden 适配器，其中包含一些示例测试，例如 Fibonacci 和 readme 示例。

添加周期性列

Winterfell 还使用周期性列，因此我们必须添加它们并在 PR 中测试它们的使用。这些可用于哈希函数计算或支持我们需要的常量。

结论

Lambdaworks 在过去一年中一直在增长。我们添加了几个证明系统和承诺方案，为用户提供了一个易于使用的库来进行实验和构建应用程序。我们还在努力使证明器与我们的库兼容，为用户提供直接替代品。我们决定努力与 Winterfell/Miden VM 兼容，因为我们喜欢许多设计选择以及在 AIRscript 中为推广 AIR 所做的工作。作为我们路线图的一部分，我们将继续提高证明器的性能并支持新的证明系统。

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