Valida三月审查记录

2024年9月4日

0. 本次审核的范围

本次审核旨在确定 Valida 中必须解决的 MVP 问题。本次审核是对2023年10月 Plonky3 / Valida 审核的补充，但并非冗余。该审核针对的是早期版本的代码，其中存在一些当前版本中不存在的问题。此外，本次审核尝试更深入地研究2023年10月审核中未完全解决的某些问题，同时也不会像2023年10月审核那样深入研究某些已解决的问题。

本次审核不应被视为对 Valida 的全面内部审计。其目标不是确保 Valida 的正确性；这将需要比此处进行的更深层次的审核。相反，目标是找出 MVP 所需的关键问题，这些问题可以通过代码审查轻松地在此处发现。本次审核的主要重点是检查 STARK 实现的可靠性和完整性。证明 STARK 实现的可靠性和完整性不是目标，本次审核也没有实现这一目标。本次审核确实指出了当前 STARK 实现的一些问题。

可靠性和完整性是所有证明系统必须满足的两个基本正确性属性。可靠性基本上意味着无法创建虚假陈述的证明（或者这样做的可能性可以忽略不计）。完整性基本上意味着证明者可以为任何陈述创建一个证明，只要该陈述有一个真值见证（或者证明者无法做到这一点的概率可以忽略不计）。严格来说，可靠性是验证者的属性（它不会接受虚假陈述的证明），而完整性是证明者/验证者对的属性（对于所涵盖的每一种真实陈述，证明者都可以在给定见证的情况下证明它，并且验证者接受该证明）。

Valida 证明者/验证者对的可靠性和完整性证明将以 FRI 多项式承诺方案 (PCS) 的可靠性和完整性为前提，Valida 证明者/验证者对建立在该方案之上。FRI PCS 的可靠性和完整性证明反过来将以 FRI 低度测试 (LDT) 的可靠性和完整性为前提，FRI PCS 建立在该测试之上。本次审核不涵盖 FRI PCS 或 FRI LDT。这并不是因为它们不值得进一步审查，而是因为它们不在本次审核的范围内，本次审核仅关注 Valida 代码，而不关注 Plonky3 代码。

除了可靠性和完整性之外，我们关心的另外两个正确性属性是简洁性和零知识。简洁性基本上意味着证明足够小且易于验证。零知识基本上意味着拥有证明并不能帮助找到用于生成证明的输入，就像了解它们证明的事实更有助于找到这些输入一样。

目前，Valida 证明不是零知识的。为了使它们具有零知识，我们必须在适当的点引入盲化因子。

我们关心的另一个正确性属性是功能完整性，这意味着 VM 必须能够运行编译器后端输出的程序。

本次审核并不试图对 Valida 的正确性属性一锤定音。据我所知，Valida 的可靠性和完整性从未得到证明。我不声称修复本次审核中概述的未决问题会导致 Valida 的证明者/验证者对是可靠和完整的，或者会导致 Valida 在功能上是完整的。本次审核中没有引用或包含任何证明。关于 Valida 还有很多验证工作要做。本次审核只是朝着验证 Valida 和确定使 Valida 达到规范的剩余工作的部分贡献。

1. Valida 简洁参数概述

Valida 中使用的 STARK 参数遵循零知识证明中使用的常见论证风格。它承诺将跟踪表示为多项式。它承诺对所有约束多项式的线性组合与用于从跟踪生成多项式的评估域的零化多项式的商进行承诺。存在该商的陈述以高概率暗示所有约束多项式在所有行处均为零，即在所有约束多项式沿其多项式图存在的评估域中的所有点处均为零。

验证者通过处理证明者发送的多项式承诺，以及使用 Fiat-Shamir 启发法选择的伪随机点上的这些多项式的开放，简洁地验证商的存在。这些承诺和开放允许验证者简洁地验证在伪随机选择的点上，方程 P(x) = Q(x) * Z(x) 成立，对于某些 Q(x)，其中 P(x) 是约束多项式在证明中承诺的跟踪多项式上的一些随机线性组合。

Valida 使用 STARK 参数的集合来证明单个程序执行。每个 STARK 参数都是如上所述的形式，简洁地证明/验证 P(x) = Q(x) * Z(x) 形式的方程，对于 P(x) 是约束多项式的随机线性组合。每个芯片都应该有自己的 STARK 参数（至少一个，但可能超过一个）。

一些芯片需要相互交互。每个芯片都有自己的跟踪，有时这些跟踪需要以某种方式相互关联，才能实现一致性。例如，内存芯片跟踪需要与自身保持一致（每次读取都会产生上次写入同一地址的值），但内存芯片跟踪也需要与 CPU 芯片跟踪保持一致（因此每个LOAD32 和 STORE32 指令跟踪都与内存跟踪一致）。前者（内存一致性）是对单个芯片跟踪（内存跟踪）的约束，而后者（与 CPU 芯片跟踪的内存一致性）是关联两个芯片跟踪（内存跟踪和 CPU 芯片跟踪）的约束。

跨芯片交互是使用 Valida 代码的 machine crate 中定义的 Interaction 抽象来定义的。交互有四种类型：本地发送、本地接收、全局发送和全局接收。每个交互都定义了它覆盖的列、用于跟踪交互的计数列以及用于证明交互的总线参数的索引。

每个总线参数要么是本地总线参数，要么是全局总线参数。它们之间的区别在于，本地总线参数是单个芯片本地的，而全局总线参数是非本地的，跨多个芯片。我不清楚这在实践中有何不同，因为它们在证明者/验证者对中以类似的方式处理。本地总线参数可用作查找参数的一种形式。本地总线参数仅出现在内存芯片中。

机器上所有芯片之间的所有交互都在单个置换参数中一起证明。此置换参数声明项的累积和等于零。置换参数跟踪的每个交互都会对累积和贡献该交互的字段元素的随机线性组合的值的乘法逆。这些随机线性组合意味着使得相应发送和接收的累积和中的项相互抵消。假设上，除非发送和接收实际上是一对一对应的并且彼此一致，否则这种情况不太可能发生。该假设将是置换参数可靠性证明中的关键引理。

2. 代码审核笔记

随附的电子表格总结了基本机器中芯片的约束以及它们之间的交互。

本次审核中引用了以下版本的 Valida 和 Plonky3：

• Valida：d5ece10968f4ca0c66cb77c4777fd711d322cbfd @ origin (git@github.com:valida-xyz/valida.git)
• Plonky3：16b590da6d9b235efa67e69e7b67d6ed3b270589 @ origin (git@github.com:Plonky3/Plonky3.git)

3. 可靠性和完整性

为了解决 Valida 证明者/验证者对是否可靠和完整的问题，需要考虑以下问题：

1. 使用的 STARK 参数是否确保（以足够高的概率）输入到其中的多项式约束为真？
2. 使用的置换参数是否确保参数指定的芯片交互的要求为真？
3. 除了置换参数之外的多项式约束，以及芯片交互的要求，是否足以确保应该证明的陈述为真？
4. 对于输入到证明者的任何有效跟踪输入，约束是否总是可以满足，并且可以生成可验证的证明？

本次审核考虑了这些问题。STARK 参数本身或置换参数未发现任何问题；同时，未排除这些部分存在错误的可能性。

没有已知的情况是有效的轨迹无法证明有效。应执行更广泛的测试，以帮助发现任何无法证明有效轨迹的情况。

多项式约束和交互存在一些已知问题和可能的问题，这意味着芯片的多项式约束和交互的要求并非在每种情况下都足以确保轨迹有效。这些问题如下：

1. 在 CPU 芯片的相等性测试中，其中一个约束声明 not_equal = diff * diff_inv。由于 not_equal 为 0 或 1，因此仅当 diff_inv 是 diff 的乘法逆元时，或者当 diff 为零时，或者当 diff_inv 为零时，才满足此条件。如果 not_equal 为 1，则 diff_inv 是 diff 的乘法逆元，这意味着 diff 不为零，这意味着输入值不相等。不清楚的是，如果 not_equal 为 0，则 diff 为 0。看起来 diff 可能不为零，diff_inv 为 0，not_equal 为 0。因此，该论证是不可靠的。我们可以通过添加另一个约束来解决此问题：(1 - not_equal) * diff = 0。这应该完成对 diff 的零测试的约束。此问题可能会在其他出现零测试的地方重现。

2. 内存一致性参数似乎有问题。该参数应该检查每次读取是否产生上次写入同一地址的值。据我所知，该参数背后的推理过程大致如下。

内存跟踪的每一行都有一个时钟值，指示它对应于主跟踪的哪一行。但是，这些行应该首先按内存地址排序，然后按时钟值排序，而不是按时钟值的升序放置在跟踪中。

不清楚内存地址组是否必须相对于彼此按特定顺序排列。甚至不清楚对应于特定内存地址的所有跟踪行是否必须排序到单个组中。但是，每次读取都需要在对应的写入之前进行，这意味着单个内存地址的每组跟踪行都需要以写入开头。

内存参数声明每个内存芯片跟踪行都包含一个计数器值，并且这些计数器值按顺序递增到跟踪的最后一行。它还声明每个内存芯片跟踪行都包含一个 diff 值，对于分组的最后一行之外的任何行，该值等于 (next.clk - local.clk)。内存芯片具有与自身交互，将 diff 发送到计数器。这向我表明，每个 diff 都需要是计数器在某个时刻取的值。这似乎确保内存跟踪至少与内存跟踪的两个相邻行之间的时钟值中的最大差值一样长。例如，如果内存跟踪至少与主 CPU 跟踪一样长，则可以确保这一点。为了平衡这一点，对于每个计数器值，counter_mult 必须设置为等于它的 diff 值的数量的计数。但是，我不确定内存芯片与自身交互背后的确切意图是什么。

当前内存参数的一个可能缺陷是，它似乎不需要单个内存地址组中的内存芯片跟踪行按任何特定顺序排列。它需要它们按时钟值的升序排列，但我没有看到任何强制执行这种情况的措施。如果单个内存地址组中的内存芯片跟踪行相对于时钟值无序，则无法保证读取/写入的一致性。但是，据我所知，按时钟值的正确排序是可以保证的，我只是没有看到它是如何保证的。我还没有以任何方式证明读取/写入的一致性是否得到保证。

内存参数交互使用一个 is_real 列，该列似乎用于区分已使用的内存跟踪行和未使用的行。但是，is_real 列未在内存参数多项式约束中显式引用。我不确定这是否是一个问题。

有关当前内存参数可能存在的问题的进一步讨论，请参见Valida 问题 #40。问题描述指的是我对代码中未实现的地址增量的某些范围检查。添加这些范围检查后，内存参数可能会更有意义，但即使那样，似乎仍然不正确，原因是在问题描述中给出的。

我认为无需更改基本方法即可修复内存参数。基本方法似乎没问题。我想看到的是，修复导致单个内存地址分组中的所有内存芯片跟踪行都按顺序按时钟值升序排列，而不会跳过与同一地址相关的任何中间内存芯片跟踪行。

如果实际上需要修复，实现这样的修复可能会大大影响证明内存参数的性能特征。最好完全采用不同的方法。Daniel Lubarov 建议，内存参数使用长而窄的跟踪这一事实是性能问题。

已经提出了一些替代内存参数的建议，这些参数可以替代当前的参数。Succinct SP1 使用 BEGKN92 内存参数，Daniel Lubarov 建议这可能是要使用的参数。

3. SRA（算术右移）指令尚未为其输出实现 STARK 约束。

4. Mul32 芯片上的 MULHU32 和 MULHS32 指令尚未为其实现 STARK 约束。这些可能不是必备项，但如果我们不打算为其实现 STARK 约束，那么至少我们应该转移到另一个不与 UMUL32 指令共享的芯片。

5. （8 位）范围检查器芯片尚未为其实现 STARK 约束系统。这需要实现。

6. Div32 芯片尚未为其实现 STARK 约束系统。这可能不是必备项。Div32 芯片要么需要删除，要么为其实现 STARK 约束。

7. 可能希望向以下芯片的输出添加范围检查发送：Mul32、Div32、Shift32、Lt32、Com32 和 Bitwise32。

8. 目前没有任何东西检查程序 ROM 跟踪是否与 CPU 主跟踪一致。检查此情况的交互由于某种原因被注释掉了；需要重新启用并可能修复它。

9. 每个 Valida 芯片都与所谓的“预处理跟踪”相关联。在退化情况下，即通常情况下，此预处理跟踪为空。只有程序和范围芯片具有非空的预处理跟踪。预处理跟踪是在设置时（即，在证明者的输入已知之前）已知其内容的跟踪。因此，预处理跟踪的内容不取决于要证明的陈述或建议数据。

STARK 验证者需要检查对编码预处理跟踪的多项式的承诺是否是对正确多项式的承诺。这应该通过发送其在伪随机选择的点处的开放证明来完成。目前尚未完成。Plonky3 问题 #250 阻止了此操作的完成。

实施预处理跟踪可能还有其他缺失的部分。这需要进一步调查和验证。

总的来说，目前的结论是 Valida 证明者/验证者对是不可靠的，并且可能它是完整的（就其语言中的所有真实陈述都是可证明的而言），但是应该做更多的工作来验证 Valida 的证明者/验证者对是完整的（除了使其可靠之外）。

4. 功能完整性

功能完整性大致是指 VM 必须能够运行编译器后端输出的程序。这意味着功能完整性是一个移动的目标，因为编译器正在发生变化。ISA（指令集架构）在理论上是编译器和 VM 之间接口的定义。我们目前正在探索 ISA 的选项，并且它的定义尚未确定。

目前，我们认为以下指令将需要在 ISA 中支持编译器 MVP：

所有不支持的必需指令（在上表中标记为❌）都需要添加到 VM 中，并且需要为其实现 STARK 约束，以实现 MVP。

我们认为以下指令最好在 ISA 中拥有，但不是严格要求的：

5. 致谢

感谢 Daniel Lubarov 和其他队友回答了一些关于内存参数、预处理跟踪和 CPU 芯片中的相等性测试的问题。

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