Plonky3/Valida 十月回顾

2024年9月4日

目标

本文档的根本目标是向我们的开发者社区提供关于 Plonky3 和 Valida 进展的透明更新。我们理解并感谢许多人对这些库的发布及其在项目中的应用的期待和热情。在开发过程中，你的理解和耐心对我们至关重要。除了本审查标准中涵盖的具体内容外，我们还将单独发布关于 LLVM Valida 编译器的详细说明。这个单独的发布将确保对特定方面的集中和全面讨论。我们仍然坚定地致力于交付一个强大的 MVP，以满足我们社区的标准和期望。

当前，根据我们的开发轨迹，我们预计完成 MVP 总共需要两到四个人月。

早期访问计划

随着我们不断改进和扩展 Valida 及其编译器基础设施的功能，我们很高兴能探索启动早期访问计划的可能性。在我们更广泛的开源版本发布（包括 Valida 编译器、工具链和相关实用程序）之前，我们正考虑向一部分受信任的合作伙伴授予免费的早期访问权限。此举旨在促进更紧密的合作，使我们能够直接从最活跃的用户那里获得宝贵的反馈。这种合作关系将有助于改进我们的系统，确保我们在进行更广泛的发布时，能够提供一个强大、可靠且满足我们社区多样化需求的产品。如果早期参与和合作的前景引起你的共鸣，我们很高兴能与你讨论邀请你成为我们早期访问合作伙伴的机会。

请联系 [v@delendum.xyz](mailto: v@delendum.xyz) 以参加早期访问计划。

• 审查标准
  • 功能完整性与happy path正确性
  • Partiality
  • 异常处理
  • 验证器中的浮点数
  • 渐近复杂度
  • 系统支持
• Plonky3 审查
  • 功能完整性与happy path正确性
  • Partiality
  • 异常处理
  • 验证器中的浮点数
  • 渐近复杂度
• Valida 审查
  • 功能完整性与happy path正确性
  • Partiality
  • 异常处理
  • 验证器中的浮点数
  • 渐近复杂度

审查标准

本节概述了审查 Plonky3 和 Valida 的标准，以便确定 MVP 的剩余工作范围。

功能完整性与 happy path 正确性

本次审查将尝试验证 Plonky3 和 Valida 在 MVP 的目的上是否功能完整，并且“happy path”（非异常）执行模式是否正确。

Partiality

Partiality 指的是当一个 partial computable function 不是 total computable 时：即，当函数可能无法为某些输入以其指定的输出类型的结果终止时。 partial computable function 有两种方式可以在某些输入上表现出 partiality：要么它无法在这些输入上终止，要么它在这些输入上表现出异常终止条件（例如 C++ 中的段错误或 Rust 中的 panic）。

就我们的目的而言，Plonky3 和 Valida 应该由 total function 组成。对于 MVP 而言，Plonky3 和 Valida 中不应存在已知的 partiality。其 API 公开的所有函数都应在所有输入上表现出正常的终止条件。这对于确保基于这些 API 构建的服务的稳健性非常重要。

本次审查将尝试标记 Valida 和 Plonky3 中所有潜在的 partiality 原因。

异常处理

本次审查将尝试评估在预期的 Plonky3/Valida 执行路径中可能发生的边缘情况和异常条件。本次审查将尝试标记任何可能产生不良结果的边缘情况或异常条件，例如：

1. 无意或不适当地抑制错误条件，
2. 在优雅失败更可取时抛出异常，
3. 在没有充分记录错误条件的情况下优雅失败，
4. 不提供信息的错误消息，或
5. 异常终止。

验证器中的浮点数

Plonky3 和 Valida 验证器算法不得使用浮点原语，因为在 Valida STARK 内部的验证上下文中（如在递归证明中），这些原语不会被假定存在。本次审查将尝试验证浮点原语是否未在 Plonky3 和 Valida 验证器中使用，或标记其任何用法。

渐近复杂度

本次审查将尝试识别 Plonky3 和 Valida 中任何算法，这些算法的渐近复杂度类对于该问题的解决方案而言是非最优的（即，渐近慢的解决方案）。Plonky3 和 Valida 中任何渐近慢的解决方案都可能给可扩展性带来问题。

系统支持

Valida 和 Plonky3 必须能够在以下系统上构建：

• x86_64-linux

Valida 和 Plonky3 必须能够针对以下系统构建：

• x86_64-linux
• ARM64-android

Valida 和 Plonky3 验证器必须能够针对以下系统构建：

• x86_64-linux
• ARM64-android
• Valida

x86_64-linux 和 ARM-64-android 目标由 rustc（基于 LLVM）支持，因此构建 Valida 以在这些目标上运行应该不是大问题。要构建验证器以在 Valida 上运行，我们需要将 Valida LLVM 后端完成到足够的水平。

Plonky3 审查

本次审查适用于 Plonky3 的 commit 000681e190eb0f7fc8523f47b8bd06de075460d8。

Plonky3 由以下功能组件组成，以其依赖关系顺序的线性化方式列出：

1. 简单实用功能集合。位于 util 子目录下。
2. 围绕 rayon 的 feature-gated 包装器。位于 maybe-rayon 子目录下。
3. 具有各种实现和相关算法的字段抽象。位于 field 子目录下。
4. 用于测试字段实现的实用程序集合。位于 field-testing 子目录下。
5. 具有各种实现和相关算法的矩阵抽象。位于 matrix 子目录下。
6. AIR 相关的 trait 和实现集合，包括双行矩阵视图和列中的仿射函数对（“虚拟列”）。位于 air 子目录下。
7. 对称加密原语的框架，包括压缩函数相关的 trait 和实现、无填充覆盖模式的海绵函数、哈希 trait、序列化哈希和密码置换相关的 trait。位于 symmetric 子目录下。
8. Baby bear 字段及其四次和五次扩展字段的实现。位于 baby-bear 子目录下。
9. Goldilocks 字段及其二次扩展字段的实现。位于 goldilocks 子目录下。
10. Mersenne-31 字段及其一些字段扩展的实现，以及 Mersenne-31 的 DFT 和 radix 2 DIT 实现。位于 mersenne-31 子目录下。
11. Keccak 置换和哈希函数实现。位于 keccak 子目录下。
12. Blake3 哈希函数实现。位于 blake3 子目录下。
13. DFT 相关 trait 和实现库。位于 dft 子目录下。
14. 编码理论 trait 集合。位于 code 子目录下。
15. 用于测试的 LDE 相关 trait 和实现集合。位于 lde 子目录下。
16. Reed-Solomon 码的实现。位于 reed-solomon 子目录下。
17. 用于基于 IOP 的 transcript 生成 Fiat-Shamir 挑战的 trait 和实现集合。位于 challenger 子目录下。
18. 承诺方案 trait 集合。位于 commit 子目录下。
19. MDS 置换相关 trait 和实现集合。位于 mds 子目录下。
20. Poseidon 置换实现。位于 poseidon 子目录下。
21. Poseidon2 置换实现和相关 trait 和实现。位于 poseidon2 子目录下。
22. Rescue-XLIX 置换实现。位于 rescue 子目录下。
23. 二叉 Merkle 树实现和由二叉 Merkle 树支持的向量承诺方案。位于 merkle-tree 子目录下。
24. 基于 Spielman 的 Brakedown 论文中描述的代码的实现。位于 brakedown 子目录下。
25. 几个有助于 Lagrange 插值的函数。位于 interpolation 子目录下。
26. 与低度测试相关的 trait 和实现集合，包括基于低度测试 PCS。位于 ldt 子目录下。
27. 使用基于 BCG20 的 2 次张量码的 PCS。位于 tensor-pcs 子目录下。
28. Monolith-31 置换的实现。位于 monolith 子目录下。
29. FRI 的实现。位于 fri 子目录下。
30. 最小的 univariate STARK 框架。位于 uni-stark 子目录下。
31. 最小的 multivariate STARK 框架。位于 multi-stark 子目录下。
32. Keccak-f 置换的 AIR。位于 keccak-air 子目录下。我认为这仅用于说明目的。

功能完整性与 happy path 正确性

FRI 验证器尚未实现；请参阅 fri/src/verifier.rs。univariate STARK 验证器的一个检查被注释掉了，注释说 TODO：在通过时重新启用；请参阅 uni-stark/src/verifier.rs。multivariate STARK 框架中没有验证器模块。验证器功能不足表明证明中可能存在未被发现的错误，这些错误会在针对验证器进行测试时被清除。

我们希望 Plonky3 能够实现的主要正确性属性是可靠性和完整性。如果且仅当验证器不接受任何虚假声明作为证明时，证明协议才是可靠的。如果且仅当证明者在给定真实输入时始终成功输出证明，并且验证器接受证明者成功输出的所有证明时，证明协议才是完整的。

Plonky3 由证明协议和支持库的集合组成。Plonky3 中专门包括的证明协议是 FRI 和 Keccak AIR。Keccak AIR 似乎是一个示例，演示了如何使用 Plonky3 中的库来创建使用 FRI 多项式承诺方案 (PCS) 验证的基于 AIR 的新证明协议。我们希望 Plonky3 能够实现的主要正确性属性是 FRI 的可靠性和完整性，以及我们使用 Plonky3 构建的证明协议在正确构建时是可靠和完整的。如上所述，这些正确性属性相当模糊和不明确；特别是，它们没有定义使用 Plonky3 正确构建协议的含义。验证 Plonky3 的过程应包括尽可能正式地定义一些使用 Plonky3 构建的协议可靠性的充分条件。

可靠性无法非常有效地进行测试。可靠性测试可能包括提供随机陈述和随机证明并测试验证器是否拒绝它们（它应该以极大的概率拒绝它们）。可靠性测试还可能包括模糊测试，即采用一个真实的陈述及其有效证明，并对该陈述或证明进行随机更改，检查验证器是否拒绝结果（它应该以压倒性的概率拒绝结果）。但是，这些测试实际上不足以验证可靠性，任何测试都无法验证可靠性。可靠性必须得到证明。

本次审查未包括为确定 Plonky3 的实现在其 happy path 中是正确的而进行的协同努力。由于验证器实现的不完整，证明者实现可能在某些方面存在错误，因为在没有完整的验证器实现的情况下，无法测试证明者实现的完整性或可靠性。

Partiality

在非测试代码中有一个 todo!() 实例。它在 matrix/src/lib.rs 中 MatrixRows<T> 的 trait 定义中 stubbing out 了 to_row_major_matrix 的实现。

在非测试代码中有 10 个 panic!() 实例：

1. 在 air/src/two_matrix.rs 中，针对 TwoRowMatrixView<'_, T> 的 MatrixRows<T>::row 实现。
2. 在 air/src/two_matrix.rs 中，针对 TwoRowMatrixView<'_, T> 的 MatrixRowSlices<T>::row_slice 实现。
3. 在 baby-bear/src/aarch64_neon.rs 中，针对 PackedBabyBearNeon 的 PackedField::interleave 的不安全实现。
4. 在 mersenne-31/src/aarch64_neon.rs 中，针对 PackedMersenne31Neon 的 PackedField::interleave 的实现。
5. 在 commit/src/mmcs.rs 中，针对 Mmcs<T> 的 trait 定义中 get_max_height 的实现。
6. 在 field/src/packed.rs 中，针对 F: Field 的 PackedField::interleave 的实现。
7. 在 fri/src/prover.rs 中，针对 prove 的实现。
8. 在 multi-stark/src/folder.rs 中，针对 ConstraintFolder<'a, F, Challenge, PackedChallenge> 的 AirBuilder::is_transition_window 的实现。
9. 在 uni-stark/src/folder.rs 中，针对 ProverConstraintFolder<'a, SC> 的 AirBuilder::is_transition_window 的实现。
10. 在 uni-stark/src/folder.rs 中，针对 VerifierConstraintFolder<'a, Challenge> 的 AirBuilder::is_transition_window 的实现。

在非测试代码中有 9 个 .expect() 实例：

1. 在 challenger/src/duplex_challenger.rs 中，针对 DuplexChallenger<F, P, WIDTH> 的 CanSample<F>::sample 实现。
2. 在 challenger/src/hash_challenger.rs 中，针对 HashChallenger<F, H, OUT_LEN> 的 CanSample<F>::sample 实现。
3. 在 fields/src/extension/binomial_extension.rs 中，针对 BinomialExtensionField<F, D> 的 AbstractExtensionField<F>::from_base_slice 实现。
4. 在 field/src/field.rs 中，Field::inverse 的默认实现。
5. 在 field/src/helpers.rs 中，sum_vecs 的实现。
6. 在 ldt/src/quotient.rs 中， get_repeated 的实现。
7. 在 mersenne-31/src/lib.rs 中，针对 Mersenne31 的 AbstractField::from_canonical_u64 实现。
8. 在 mersenne-31/src/lib.rs 中，针对 Mersenne31 的 AbstractField::from_canonical_usize 实现。
9. 在 rescue/src/util.rs 中，get_inverse 的实现。

在非测试代码中有 20 个 .unwrap() 实例：

1. 在 field/src/batch_inverse.rs 中， batch_multiplicative_inverse 的实现。
2. 在 keccak/src/lib.rs 中，针对 KeccakF 的 Permutation::permute 实现。
3. 在 ldt/src/quotient.rs 中，针对 QuotientMmcs<F, EF, Inner> 的 Mccs<EF>::open_batch 实现。
4. 在 ldt/src/quotient.rs 中，针对 QuotientMmcs<F, EF, Inner> 的 Mccs<EF>::verify_batch 实现。
5. 在 mds/src/coset_mds.rs 中，针对 CosetMds<F, N> 的 Default::default 实现。
6. 在 mds/src/util.rs 中，apply_circulant_fft 的实现。
7. 在 merkle-tree/src/merkle-tree.rs 中，FieldMerkleTree<F, DIGEST_ELEMS>::new 的实现。
8. 在 merkle-tree/src/merkle-tree.rs 中，FieldMerkleTree<F, DIGEST_ELEMS>::root 的实现。
9. 在 merkle-tree/src/mmcs.rs 中，针对 FieldMerkleTreeMmcs<P, H, C, DIGEST_ELEMS> 的 Mmcs<P::Scalar>::verify_batch 实现。
10. 在 monolith/src/monolith.rs 中，针对 MonolithMdsMatrixMersenne31<NUM_ROUNDS> 的 Permutation::permute 实现。
11. 在 rescue/src/rescue.rs 中，针对 Rescue<F, Mds, Sbox, WIDTH>::num_rounds 实现。
12. 在 rescue/src/util.rs 中，get_alpha 的实现。
13. 在 rescue/src/util.rs 中，get_inverse 的实现。
14. 在 symmetric/src/compression.rs 中，TruncatedPermutation<InnerP, N, CHUNK, WIDTH> 的 PseudoCompressionFunction<[T; CHUNK], N>::compress 实现。
15. 在 symmetric/serializing_hasher.rs 中，针对 SerializingHasher<F, Inner> 的 CryptographicHasher<F, [F; 4]>::hash_iter 实现。
16. 在 symmetric/serializing_hasher.rs 中，针对 SerializingHasher<F, Inner> 的 CryptographicHasher<F, [F; 8]>::hash_iter 实现。
17. 在 symmetric/src/sponge.rs 中，针对 PaddingFreeSponge<P, WIDTH, RATE, OUT> 的 CryptographicHasher<T, [T; OUT]>::hash_iter 实现。
18. 在 tensor_pcs/src/reshape.rs 中，optimal_wraps 的实现。
19. 在 tensor-pcs/src/wrapped_matrix.rs 中，针对 WrappedMatrixRow<'a, T, M> 的 Iterator::next 实现。
20. 在 uni-stark/src/prover.rs 中，针对 prove 的实现。

以下文件在非测试代码中包含 assert!() 和/或 assert_eq!() 实例：

01. baby-bear/src/aarch64\_neon.rs
    1. 在 PackedField::from\_slice for PackedBabyBearNeon，第 572 行
    2. 在 PackedField::from\_slice\_mut for PackedBabyBearNeon，第 582 行
02. field/src/field.rs
    1. 在 AbstractExtensionField<AF>::from\_base\_slice for AF :
        AbstractField，第 309 行
03. field/src/helpers.rs
    1. 在 add\_vecs，第 36 行
04. keccak-air/src/columns.rs
    1. 在 Borrow<KeccakCols<T>> for \[T\]，第 126 行
    2. 在 Borrow<KeccakCols<T>> for \[T\]，第 127 行
    3. 在 Borrow<KeccakCols<T>> for \[T\]，第 128 行
    4. 在 BorrowMut<KeccakCols<T>> for \[T\]，第 137 行
    5. 在 BorrowMut<KeccakCols<T>> for \[T\]，第 138 行
    6. 在 BorrowMut<KeccakCols<T>> for \[T\]，第 139 行
05. matrix/src/mul.rs
    1. 在 mul\_csr\_dense，第 19 行
06. matrix/src/stack.rs
    1. 在 VerticalPair<T, First, Second>::new，第 14 行
07. mersenne-31/src/aarch64\_neon.rs
    1. 在 PackedField::from\_slice for PackedMersenne31Neon，第 522 行
    2. 在 PackedField::from\_slice\_mut for PackedMersenne31Neon，第 533 行
08. mersenne-31/src/complex.rs
    1. 在 TwoAdicField::two\_adic\_generator for
        Mersenne31Complex<Mersenne31>，第 275 行

    2. 在 AbstractExtensionField<AF>::from\_base\_slice for
        Mersenne31Complex<AF> where AF: AbstractField<F = Mersenne31>
09. monolith/src/monolith.rs
    1. 在 MonolithMersenne31<Mds, WIDTH, NUM\_FULL\_ROUNDS>::new where
        Mds: MdsPermutation<Mersenne31, WIDTH>，第 38 行

    2. 在 MonolithMersenne31<Mds, WIDTH, NUM\_FULL\_ROUNDS>::new where
        Mds: MdsPermutation<Mersenne31, WIDTH>，第 39 行

    3. 在 MonolithMersenne31<Mds, WIDTH, NUM\_FULL\_ROUNDS>::new where
        Mds: MdsPermutation<Mersenne31, WIDTH>，第 40 行
10. poseidon/src/lib.rs
    1. 在 Poseidon<F, Mds, WIDTH, ALPHA>::new，第 40 行
11. tensor-pcs/src/wrapped\_matrix.rs
    1. 在 WrappedMatrix::new，第 16 行
12. uni-stark/src/prover.rs
    1. 在 prove，第 45 行
13. util/src/lib.rs
    1. 在 log2\_strict\_usize，第 32 行

以下文件包含 unsafe 代码块，在进一步审查之前，应假定可能导致 partiality：

01. baby-bear/src/aarch64\_neon.rs
02. dft/src/butterflies.rs
03. dft/src/util.rs
04. field/src/packed.rs
05. goldilocks/src/lib.rs
06. keccak-air/src/columns.rs
07. matrix/src/dense.rs
08. mersenne-31/src/aarch64\_neon.rs
09. monolith/src/monolith.rs
10. util/src/lib.rs

以下算术运算可能导致除以零，这将导致 panic：

1. 在 matrix/src/dense.rs 中，针对 RowMajorMatrix<T> 的 Matrix<T>::height 的实现，第 179 行。
2. 在 matrix/src/dense.rs 中，针对 RowMajorMatrixViewM<;'_, T> 的 Matrix<T>::height 的实现，第 256 行。
3. 在 matrix/src/dense.rs 中，针对 VerticallyStridedMatrixView<Inner> 的 Matrix<T>::height 的实现，第 16 行。
4. 在 ldt/src/quotient.rs 中，针对 QuotientMmcs<F, EF, Inner> 的 Mmcs<EF>::open_batch 的实现，在第 71 行。
5. 在 tensor-pcs/src/wrapped_matrix.rs 中，针对 WrappedMatrix<T, M> 的 Matrix<T>::height 的实现，第 34 行。

以下未经检查的数组索引实例可能导致索引超出范围的错误和 panic：

1. 在 merkle_tree/src/merkle_tree.rs 中，FieldMerkleTree<F, DIGEST_ELEMS>::root，第 53 行。
2. 在 merkle_tree/src/merkle_tree.rs 中，first_digest_layer，第 107 行。
3. 在 merkle_tree/src/merkle_tree.rs 中，compress_and_inject，第 160, 171, 172, 188, 189, 198 和 199 行。
4. 在 merkle_tree/src/merkle_tree.rs 中，compress，第 230, 231, 241, 242 行。
5. 在 uni-stark/src/prover.rs 中，prove，第 75, 76 和 77 行。

异常处理

Goldilocks 字段实现允许非规范形式，这意味着字段元素可以用大于最大字段元素的 64 位整数表示，具有环绕语义。这可能导致意外行为；例如，同一字段元素的两个实例可能具有不同的哈希值，因为一个实例是规范形式，另一个实例是非规范形式。

以下算术运算可能导致未经检查的算术溢出或下溢：

1. 在 mersenne-31/src/lib.rs 的第 257 行，针对 Mersenne31 的 PrimeField64::linear_combination_u64 中的乘法。
2. 在 mersenne-31/src/lib.rs 的第 259 行，针对 Mersenne31 的 PrimeField64::linear_combination_u64 中的乘法。
3. 在 mersenne/src/radix_2_dit.rs 中 dit_butterfly_inner 的实现，第 133-148 行。
4. 在 dft/src/traits.rs 的第 93 行，TwoAdicSubgroupDft::coset_lde_batch 的默认实现。
5. 在 code/src/systematic.rs 的第 15 行，SystematicCode::parity_len 的默认实现。
6. 在 interpolation/src/lib.rs 中 interpolate_coset 的实现，第 55 行。

验证器中的浮点数

Plonky3 使用浮点数来计算 rescue/src/rescue.rs 中第 40 行的 Rescue<F, Mds, Sbox, WIDTH>::num_rounds。这个函数很可能参与到使用 Rescue-XLIX 作为其哈希函数的 Plonky3 验证器算法中。

渐近复杂度

本次审查未发现渐近慢的算法。

Valida 审查

本次审查适用于 Valida（可在 lita-xyz 分支中找到）的 commit eddd2b031a13278bc4855dea802fbc045f1378d8。本次审查不包括 assembler 子目录中的汇编器。以下 Valida 功能组件在范围内（以其依赖关系顺序的线性化方式列出）：

1. 一些用于派生 Machine、Borrow 和 BorrowMut 的 trait 实现的宏。位于 derive 子目录下。
2. 一些实用功能，位于 util 子目录下。
3. 一个操作码字典，位于 opcodes 子目录下。
4. 用于构建 Valida 芯片 AIR、Valida VM 和 Valida zk-VM STARK 的 trait、类型和实现集合。位于 machine 子目录下。
5. 总线相关的 trait 集合。位于 bus 子目录下。
6. 具有关联 AIR 实现的 RAM 芯片实现。位于 memory 子目录下。
7. 具有关联 AIR 实现的程序 ROM 芯片实现。位于 program 子目录下。
8. 具有关联 AIR 实现的范围检查器芯片实现。位于 range 子目录下。
9. 具有关联 AIR 实现的 CPU 芯片实现。位于 cpu 子目录下。
10. 具有关联 AIR 实现的 32 位 ALU 芯片实现。位于 alu_u32 子目录下。
11. 具有关联 AIR 实现的 native field 芯片实现。位于 native_field 子目录下。
12. 具有关联 AIR 实现的输出芯片实现。位于 output 子目录下。
13. 基本 Valida zk-VM 实现和一个运行其证明器的包装器。位于 basic 子目录下。
14. 验证器存根。位于 verifier 子目录下。

功能完整性与 happy path 正确性

验证器未实现；请参阅 verifier/src/lib.rs。

ALU_U32 AIR 的 DIV32 AIR 未实现；请参阅 alu_u32/src/div/stark.rs。

alu_u32/src/mul/mod.rs 的第 84 行，Mul32Chip 的 Chip<M>::localSends 的实现被 stubbed out 。

cpu/src/stark.rs 的 Air<AB>::eval 的实现中，立即值的约束缺少对 read_value_2 的范围检查；请参阅第 41 行。

并非 transcript 的所有部分都被 challenger 观察到。这可能导致可靠性错误。请参阅 derive/src/lib.rs 的第 253 行和第 277 行。

machine/src/__internal/folding_builder.rs 的第 32 行，PermutationAirBuilder::permutation_randomness for ConstraintFolder<a, F, EF, M> 的实现被 stubbed out。

machine/src/__internal/folding_builder.rs 的第 88 行，AirBuilder::assert_zero for ConstraintFolder<'a, F, EF, M> 的实现被 stubbed out。

machine/src/__internal/prove.rs 中 prove 的实现被 stubbed out。

范围检查器芯片 STARK 未实现；请参阅 range/src/stark.rs。

memory/src/stark.rs 中的一条注释说 FIXME：度数约束 4，需要移除。我不清楚为什么需要移除度数为 4 的约束。这是优化还是功能完整性和正确性的要求？

valida-derive 的默认扩展字段是 Baby bear 字段，它也是默认字段。其上的注释说 FIXME：替换。请参阅 machine/src/__internal/mod.rs 的第 4 行。如果从未使用过默认值，这可能无关紧要。

对内存参数的可靠性存在担忧；请参阅 Valida issue #40。 Valida 的主要正确性属性是它的可靠性和完备性。Valida 验证器不应接受任何对错误声明的证明。此外，对于所有形式为“Valida 程序 p 在某些输入上具有输出 x”的真陈述，这些陈述通过 SNARK 大小限制内的执行跟踪进行验证，证明者可以构建该陈述的 Valida SNARK，Valida 验证器会接受它。

与 Plonky3 一样，本次审查未有协同努力来检查 Valida 在其 happy path 执行中的正确性。测试可靠性和完备性需要一个验证器。测试可靠性实际上是无法实现的，最终可靠性需要被证明。

部分性

有三个 panic!() 的实例，不包括仅在编译时执行的宏代码，以及仅用于调试的代码：

1. 在 derive/src/lib.rs 中 run_method 宏实现中的 run 的引用代码中。
2. 在 machine/src/__internal/folding_builder.rs 中 ConstraintFolder<a, F, EF, M> 的 AirBuilder::is_transition_window 的实现中。
3. 在 memory/src/lib.rs 中 MemoryChip::read 的实现中。

在非测试代码中没有 .expect() 的实例，除了在完全在编译时运行的宏代码中的一些实例。对于完全在编译时运行的代码来说，具有部分性是可以的，只要它能终止。

在非测试代码中有 16 个 .unwrap() 的实例，不包括完全在编译时运行的宏代码：

1. 在 basic/src/bin/valida.rs 的 main 实现中，调用 load_program_rom。
2. 在 basic/src/bin/valida.rs 的 main 实现中，调用 std::io::stdin().read_to_end。
3. 在 basic/src/bin/valida.rs 的 main 实现中，调用 std::io::stdout().write_all。
4. 在 machine/src/__internal/check_constraints.rs 的 check_constraints 实现中，第 30 行。
5. 在 machine/src/__internal/check_constraints.rs 的 check_constraints 实现中，第 39 行。
6. 在 machine/src/__internal/check_constraints.rs 的 check_constraints 实现中，第 44 行。
7. 在 machine/src/__internal/check_constraints.rs 的 check_cumulative_sums 实现中，第 90 行。
8. 在 machine/src/chip.rs 的 generate_permutation_trace 实现中，第 40 行。
9. 在 machine/src/chip.rs 的 generate_permutation_trace 实现中，第 169 行。
10. 在 machine/src/chip.rs 的 generate_permutation_trace 实现中，第 189 行。
11. 在 machine/src/chip.rs 的 eval_permutation_constraints 实现中，第 268 行。
12. 在 machine/src/chip.rs 的 eval_permutation_constraints 实现中，第 270 行。
13. 在 memory/src/lib.rs 的 MemoryChip::insert_dummy_reads 实现中，第 257 行。
14. 在 memory/src/lib.rs 的 MemoryChip::insert_dummy_reads 实现中，第 258 行。
15. 在 memory/src/lib.rs 的 MemoryChip::insert_dummy_reads 实现中，第 259 行。
16. 在 output/src/lib.rs 的 WriteInstruction 的 Instruction<M>::execute 实现中，第 154 行。

在编译后运行的非测试代码中有 4 个 assert_eq!() 的实例：

1. 在 machine/src/__internal/check_constraints.rs 的 check_constraints 实现中。
2. 在 machine/src/__internal/check_constraints.rs 的 check_cumulative_sums 实现中。
3. 在 output/src/lib.rs 的 WriteInstruction 的 Instruction<M>::execute 实现中，第 162 和 163 行。

在编译后运行的非测试代码中有一个 assert!() 的实例：

1. 在 program/src/lib.rs 中 MachineWithProgramChip trait 定义中 read_word 的默认实现中。

以下文件包含 unsafe 块，在进一步审查之前，应假定这些块可能导致部分性：

01. alu_u32/src/add/columns.rs
02. alu_u32/src/add/mod.rs
03. alu_u32/src/bitwise/columns.rs
04. alu_u32/src/bitwise/mod.rs
05. alu_u32/src/div/columns.rs
06. alu_u32/src/lt/columns.rs
07. alu_u32/src/lt/mod.rs
08. alu_u32/src/mul/columns.rs
09. alu_u32/src/shift/columns.rs
10. alu_u32/src/shift/mod.rs
11. alu_u32/src/sub/columns.rs
12. alu_u32/src/sub/mod.rs
13. cpu/src/columns.rs
14. cpu/src/lib.rs
15. derive/src/lib.rs
16. memory/src/columns.rs
17. memory/src/lib.rs
18. native_field/src/columns.rs
19. native_field/src/lib.rs
20. output/src/columns.rs
21. output/src/lib.rs
22. program/src/columns.rs
23. range/src/columns.rs
24. range/src/lib.rs

以下算术运算可能导致除零并引发 panic：

1. 在 machine/src/core.rs 的 Word<u8> 的 Div::div 实现中，第 87 行。
2. 在 memory/src/lib.rs 的 MemoryChip::insert_dummy_reads 实现中，第 222 行。
3. 在 alu_u32/src/div/mod.rs 的 Div32Instruction 的 Instruction<M>::execute 实现中，第 89 行。

以下未经检查的数组索引可能导致越界错误并引发 panic：

1. 在 machine/src/chip.rs 的 generate_permutation_trace 实现中，第 120、166、179、182 和 189 行。
2. 在 machine/src/chip.rs 的 generate_rlc_elements 实现中，第 285 和 300 行。
3. 在 cpu/src/lib.rs 的 CpuChip::set_instruction_values 实现中，第 248 行。
4. 在 cpu/src/lib.rs 的 CpuChip::pad_to_power_of_two 实现中，第 328、329、330、346、347、348、351、352、355、356 和 357 行。

zk-VM 的 run 方法可能无法终止；参见 derive/src/lib.rs，第 158-176 行。这是预料之中的，因为 Valida 是图灵完备的。然而，或许我们应该在代码中设置一个最大步数，以避免部分性。我们甚至可以将最大步数作为方法的输入传递进去。

异常处理

以下算术运算可能导致未检查的溢出，从而导致调试与发布编译模式下行为不同。对于这些情况，期望的解决方案可能是 (a) 溢出应该环绕，并且应该明确地这样做，并在调试和发布模式下都发生，或者 (b) 溢出被认为对于所有输入都是不可能的，并且应该导致包含信息性错误消息的 panic。然而，其他解决方案也是可能的，必须根据具体情况考虑这些解决方案。

• 在 machine/src/core.rs:
  1. 在 Word<u8> 的 Add::add 的实现中，第 57 行

2. 在 Word<u8> 的 Sub::sub 的实现中，第 67 行
   • 在 alu_u32/src/add/mod.rs:
3. 在 Add32Chip::op_to_row 的实现中:
   1. 第 108 行的加法
      2. 第 109 行的第一个加法
      3. 第 109 行的第二个加法
      4. 第 113 行的第一个加法
      5. 第 113 行的第二个加法

4. 在 Add32Instruction 的 Instruction<M>::execute 的实现中:

   1. 第 141 行的加法（计算 read_addr_1）

      2. 第 142 行的加法（计算 write_addr_1）

      3. 第 149 行的加法（计算 read_addr_2）

      4. 第 153 行的加法（计算 a）

• 在 cpu/src/lib.rs:

  1. 在 ReadAdviceInstruction 的 Instruction<M>::execute 的实现中:
     1. 第 410 行的两个加法
     2. 第 410 行的乘法

  2. 在 WriteAdviceInstruction 的 Instruction<M>::execute 的实现中:

     1. 第 436 行的第一个和第二个加法（即，fp + mem_addr）

     2. 第 436 行的第三个加法（即，(fp + mem_addr) + mem_buf_len）

  3. 在 Load32Instruction 的 Instruction<M>::execute 的实现中:

     1. 第 470 行的加法（计算 read_addr_1）

     2. 第 472 行的加法（计算 write_addr）

  4. 在 Store32Instruction 的 Instruction<M>::execute 的实现中:

     1. 第 491 行的加法（计算 read_addr）

     2. 第 492 行的加法（计算 write_addr）

  5. 在 JalInstruction 的 Instruction<M>::execute 的实现中:

     1. 第 512 行的加法（计算 write_addr）

     2. 第 513 行的加法（计算 next_pc）

     3. 第 518 行的加法

  6. 在 JalvInstruction 的 Instruction<M>::execute 的实现中:

     1. 第 536 行的加法（计算 write_addr）

     2. 第 537 行的加法（计算 next_pc）

     3. 第 540 行的加法（计算 read_addr）

     4. 第 543 行的加法（计算 read_addr）

     5. 第 545 行的加法赋值

  7. 在 BeqInstruction 的 Instruction<M>::execute 的实现中:

     1. 第 562 行的加法（计算 read_addr_1）

     2. 第 570 行的加法（计算 read_addr_2）

     3. 第 576 行的加法

  8. 在 BneInstruction 的 Instruction<M>::execute 的实现中:

     1. 第 594 行的加法（计算 read_addr_1）

     2. 第 602 行的加法（计算 read_addr_2）

     3. 第 608 行的加法

  9. 在 Imm32Instruction 的 Instruction<M>::execute 的实现中:
     1. 第 624 行的加法（计算 write_addr）
  10. state.cpu_mut().pc += 1; 的每个实例
  11. 在 impl CpuChip 中:
      1. 在第 655 和 660 行， self.pc += 1;
      2. 在第 668 行， self.clock += 1;

• 在 alu_u32/src/bitwise/mod.rs:

  1. 在 Xor32Instruction 的 Instruction<M>::execute 的实现中:

     1. 第 145 行的加法（计算 read_addr_1）

     2. 第 146 行的加法（计算 write_addr）

     3. 第 153 行的加法（计算 read_addr_2）

  2. 在 And32Instruction 的 Instruction<M>::execute 的实现中:

     1. 第 181 行的加法（计算 read_addr_1）

     2. 第 182 行的加法（计算 write_addr）

     3. 第 190 行的加法（计算 read_addr_2）

  3. 在 Or32Instruction 的 Instruction<M>::execute 的实现中:

     1. 第 217 行的加法（计算 read_addr_1）

     2. 第 218 行的加法（计算 write_addr）

     3. 第 225 行的加法（计算 read_addr_2）

• 在 alu_u32/src/div/mod.rs 中, 在 Div32Instruction 的 Instruction<M>::execute 的实现中:

  1. 第 77 行的加法（计算 read_addr_1）

2. 第 78 行的加法（计算 write_addr）

3. 第 85 行的加法（计算 read_addr_2）

• 在 alu_u32/src/lt/mod.rs 中, 在 Lt32Instruction 的 Instruction<M>::execute 的实现中:
  1. 第 128 行的加法（计算 read_addr_1）

2. 第 129 行的加法（计算 write_addr）

3. 第 136 行的加法（计算 read_addr_2）

• 在 alu_u32/src/mul/mod.rs 中, 在 Mul32Instruction 的 Instruction::execute 的实现中:
  1. 第 123 行的加法（计算 read_addr_1）

2. 第 124 行的加法（计算 write_addr）

3. 第 131 行的加法（计算 read_addr_2）

4. 第 135 行的乘法（计算 a）

• 在 alu_u32/src/shift/mod.rs:

  1. 在 Shl32Instruction 的 Instruction<M>::execute 的实现中:

     1. 第 172 行的加法（计算 read_addr_1）

     2. 第 172 行的加法（计算 write_addr）

     3. 第 180 行的加法（计算 read_addr_2）

  2. 在 Shr32Instruction 的 Instruction<M>::execute 的实现中:

     1. 第 216 行的加法（计算 read_addr_1）

     2. 第 217 行的加法（计算 write_addr）

     3. 第 224 行的加法（计算 read_addr_2）

• 在 alu_u32/src/sub/mod.rs 中, 在 Sub32Instruction 的 Instruction<M>::execute 的实现中:
  1. 第 137 行的加法（计算 read_addr_1）

2. 第 138 行的加法（计算 write_addr）

3. 第 145 行的加法（计算 read_addr_2）

4. 第 149 行的减法（计算 a）

• 在 native_field/src/lib.rs:

  1. 在 AddInstruction 的 Instruction<M>::execute 的实现中:

     1. 第 157 行的加法（计算 read_addr_1）

     2. 第 158 行的加法（计算 write_addr）

     3. 第 165 行的加法（计算 read_addr_2）

  2. 在 SubInstruction 的 Instruction<M>::execute 的实现中:

     1. 第 197 行的加法（计算 read_addr_1）

     2. 第 198 行的加法（计算 write_addr）

     3. 第 205 行的加法（计算 read_addr_2）

  3. 在 MulInstruction 的 Instruction<M>::execute 的实现中:

     1. 第 237 行的加法（计算 read_addr_1）

     2. 第 238 行的加法（计算 write_addr）

     3. 第 245 行的加法（计算 read_addr_2）

• 在 output/src/lib.rs:

  1. 在 OutputChip 的 Chip<M>::generate_trace 的实现中:
     1. 第 66 行的减法（计算 cols.diff）
  2. 在 WriteInstruction 的 Instruction<M>::execute 的实现中:
     1. 第 149 行的加法（计算 read_addr_1）

验证器中的浮点数

本次审查未发现 Valida 代码库中验证器中潜在的浮点数问题。

渐近复杂度

以下算法的渐近复杂度较慢:

1. range/src/lib.rs 中 RangeCheckerChip<MAX> 的 Chip<M>::generate_trace 的实现是 O(MAX log(|self.count|))，但可以用 O(|self.count| log(|self.count|)) 完成。在这种情况下，self.count 是一个 BTreeMap<u32, u32>，其键空间为 [0, MAX)。这意味着 |self.count|，即 self.count 的基数或键的数量，小于或等于 MAX，因此该算法的渐近复杂度较慢，正如注释中所指出的。\ \ 如果你有兴趣进一步讨论这个话题或在这个主题上合作，请通过 research@delendum.xyz 与我们联系。\ \ ‍\ \ _________________________________________ \ 免责声明：\ \ 本博客的内容，包括文字、图形和图像，受版权保护 ©2024 Lita.Foundation。保留所有权利。未经本网站作者和/或所有者的明确书面许可，严禁未经授权使用和/或复制本材料。允许使用摘录和链接，前提是对 Lita.Foundation 给予充分和明确的署名，并提供指向原始内容的适当和具体链接。\ \ 如有任何问题或权限，请联系 Lita Foundation。\ \ ‍\ \ ‍

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