连续只读内存约束：一个使用Lambdaworks的实现
- lambdaclass
- 发布于 2024-12-03 10:58
- 阅读 15
本文深入探讨了STARKs中约束的概念，并通过Lambdaworks库，以Cairo的非确定性连续只读内存的约束实现为例，详细解释了如何使用多项式来总结trace values之间的高度复杂关系。文章详细介绍了连续只读内存的定义，以及如何通过引入排序和辅助列，将验证内存属性简化为验证连续性约束、单值约束和排列约束。
介绍
当我们首次探索 STARKs 的世界时，我们遇到的最令人困惑的概念之一就是约束。我们一直在问自己：仅仅使用几个多项式，怎么可能概括 trace 值之间高度复杂的关系？直到我们开始实现一些示例时，我们才真正理解了该领域中采用的巧妙、几乎神奇的技术。
在这篇文章中，我们旨在分享那段旅程的一部分，以一种实践的方式解释我们获得的见解。我们坚信，学习的最佳方式是通过实践，我们将引导你完成一个具体的示例：使用 Lambdaworks 库实现 Cairo 的非确定性连续只读存储器的约束。这些约束在 Cairo 白皮书 的第 9.7 节中有详细说明。
我们不会解释协议中的基本概念，因为我们假设如果你正在阅读本文，你已经对 STARK 协议、执行 trace 的概念以及定义约束的目的有所了解。为了更深入地理解或加强某些概念，请查看深入 DEEP-FRI、从头开始实现 FRI 和 Stone prover。
什么是连续只读存储器？
那么，我们所说的“连续、非确定性、只读存储器”是什么意思？
论文中的定义如下：
9.7.1 定义
定义 4. 存储器访问是一个对 (a,v)∈F2(a,v)∈F2，其中 aa 表示地址，vv 表示该地址的存储器值。如果对于所有 i,j∈[0,n)i,j∈[0,n)，如果 ai=aj,ai=aj，则 vi=vjvi=vj，则存储器访问列表 (ai,vi)(ai,vi) 对于 i∈[0,n)i∈[0,n) (1≤n≤P1≤n≤P) 被称为只读存储器。如果集合 ai:i∈[0,n)ai:i∈[0,n) 等于 [m0,m1)[m0,m1)，对于某些满足 m1=m0+tm1=m0+t 的 m0,m1∈Fm0,m1∈F，其中 t<Pt<P 是一个自然数，则它被称为连续的。特别地，对于给定的连续只读存储器访问列表，我们可以定义一个函数 f:[m0,m1)→Ff:[m0,m1)→F，使得对于所有 i∈[0,n)i∈[0,n)，f(ai)=vif(ai)=vi。任何扩展 ff 的函数 m:F→Fm:F→F 被称为存储器访问列表的存储器函数。\
让我们简化这个冗长而复杂的定义。想象一个 trace，有两列和 nn 行。这些行表示执行的每个步骤。第一列指示在该步骤中访问的存储器地址，第二列指示从该地址检索到的值。\ \ 对于只读存储器，相同的地址必须始终具有相同的值。如果 trace 中的两行引用相同的地址，则这些行中的值必须相同。\ \ 例如，考虑以下 trace：\ \ 地址 值 \ 1 56 3 34 5 97 4 25 5 41 3 34 \ 这个 trace 是无效的，因为地址 5 有两个不同的值：第一次出现时是 97，第二次出现时是 41。只读存储器不允许这样做。\ \ 对于连续存储器，从起点（例如，地址 1）到最后一个地址的每个存储器地址必须至少出现一次。\ \ 在上面的示例中，由于没有地址 2 的条目，因此该 trace 也是无效的。\ \ 因此，要验证一个 trace，我们需要确保：\ \
- 只读属性：相同的地址始终映射到相同的值。\
连续性属性：范围内的每个存储器地址至少出现一次。\ \ 值得注意的是，地址可以以任何顺序出现多次。\ \ 困难的部分是弄清楚如何将这两个条件转换为方程，然后可以将其表示为多项式。\ \ 像任何工程问题一样，这里存在权衡：保持 trace 简单会使约束更加复杂，而使用更简单的约束可能需要向 trace 添加更多信息。\ \ 如果我们检查前面提到的条件，很明显，如果行按地址排序，则验证它们会更容易。例如，人类很难确定像 (7,5,12,4,5,11,9,10,4,4,11,7,8)(7,5,12,4,5,11,9,10,4,4,11,7,8) 这样的序列是否是连续的，但如果对其进行排序，则会变得更加简单：(4,4,5,5,7,7,8,9,10,11,11,12)(4,4,5,5,7,7,8,9,10,11,11,12)。\ \ 因此，Cairo 的 VM 在 trace 中添加了两个额外的列：地址列和值列的排序版本。\ \ 例如：\ \ address (a)(a) value (v)(v) sorted_address (a′)(a′) sorted_value (v′)(v′) 1 56 1 56 5 14 1 56 3 25 2 34 3 25 3 25 4 44 3 25 1 56 4 44 2 34 5 14 \ 虽然这会复制 trace 列，但它大大简化了验证连续性和只读属性的过程，我们将在接下来看到。\ \ 但是，添加这两列会带来一个新的挑战：我们需要一种方法来验证新列是原始列的排列。我们将通过排列约束来处理这个问题（剧透：这需要 prover 向 trace 添加另一列）。\ \ 因此，通过添加这些新列，验证内存属性归结为证明以下更简单的方法约束：\ \
- 连续性约束\
- 单值约束\
- 排列约束\ \
约束\
\
连续性约束\
\ 我们的第一个约束将确保存储器地址形成一个没有间隙的连续范围。例如，如果地址 5 出现，则地址 4 和 6 也必须出现以保持连续性。\ \ 连续存储器的有效示例：\ \ sorted_addresses (a′)(a′) sorted_values (v′)(v′) ... ... 100 42 101 17 102 35 103 22 104 88 ... ...
\ 一个无效的例子：\ \ sorted_addresses (a′)(a′) sorted_values (v′)(v′) ... ... 100 42 101 17 103 22 104 88 ... ... \ 这里，地址 102 缺失，破坏了连续性。\ \ 为了检查连续性，我们检查排序后的地址列，确保连续地址之间的差始终为 0（如果它们相同）或 1（如果它们是连续的）。以下 Cairo 约束捕获了这一点：\ \ (a′i+1−a′i)(a′i+1−a′i−1)=0 for all i∈[0,n−1](ai+1′−ai′)(ai+1′−ai′−1)=0 对于所有 i∈[0,n−1]\ \ 其中 a′iai′ 表示排序后的地址列中第 ii 行的地址，v′ivi′ 表示对应的值。\ \ 在这个等式中：\ \
- 第一个因子 (a′i+1−a′i)(ai+1′−ai′) 在地址相同时等于零。\
- 第二个因子 (a′i+1−a′i−1)(ai+1′−ai′−1) 在地址相差 1 时等于零。\ \ 由于乘积必须等于零，因此地址必须相同或相差正好 1，以确保连续性。\ \ 这是在 Rust 中的实现方式：\ \
fn evaluate( &self, frame: &Frame<F, F>, transition_evaluations: &mut [FieldElement<F>], _periodic_values: &[FieldElement<F>], _rap_challenges: &[FieldElement<F>], ) { transition_evaluations .get_mut(self.constraint_idx()) .map(|transition_eval| { let first_step = frame.get_evaluation_step(0); let second_step = frame.get_evaluation_step(1);
let a_sorted_0 = first_step.get_main_evaluation_element(0, 2);
let a_sorted_1 = second_step.get_main_evaluation_element(0, 2);
let res = (a_sorted_1 - a_sorted_0)
* (a_sorted_1 - a_sorted_0 - FieldElement::<F>::one());
*transition_eval = res;
});}
\
其中：\
\
```rust
let first_step = frame.get_evaluation_step(0);
\ 使我们能够访问 trace 的第一行，并且\ \
let a_sorted_0 = first_step.get_main_evaluation_element(0, 2); //a'_0
\ 将可以访问第二个第三列，即元素 2\ \ 然后方程看起来像\ \
let res = (a_sorted_1 - a_sorted_0)
* (a_sorted_1 - a_sorted_0 - FieldElement::<F>::one());
*transition_eval = res;
\
单值约束\
| \ 此约束确保每个存储器地址具有单个一致的值。即使多次访问同一地址，该值也必须始终保持不变。\ \ 一个有效的例子：\ \ | 地址 | 值 |
|---|---|---|
| ... | ... | |
| 101 | 17 | |
| 101 | 17 | |
| 104 | 88 | |
| ... | ... |
| \ 一个无效的例子：\ \ | 地址 | 值 |
|---|---|---|
| ... | ... | |
| 101 | 17 | |
| 101 | 42 | |
| 102 | 88 | |
| ... | ... |
\ 这里，地址 101 有两个不同的值，违反了约束。\ \ 使用与连续性约束中使用的类似逻辑，Cairo 论文将单值约束定义为：\ \ (v′i+1−v′i)(a′i+1−a′i−1)=0for all i∈[0,n−1](vi+1′−vi′)(ai+1′−ai′−1)=0对于所有 i∈[0,n−1]\ \ 在这个等式中：\ \
- 第一个因子 (v′i+1−v′i)(vi+1′−vi′) 确保相同地址的值相同。\
-
第二个因子 (a′i+1−a′i−1)(ai+1′−ai′−1) 确保此检查仅适用于相同的地址。\ \ 这是在 Rust 中的实现方式\ \
fn evaluate( &self, frame: &Frame<F, F>, transition_evaluations: &mut [FieldElement<F>], _periodic_values: &[FieldElement<F>], _rap_challenges: &[FieldElement<F>], ) { transition_evaluations .get_mut(self.constraint_idx()) .map(|transition_eval| { let first_step = frame.get_evaluation_step(0); let second_step = frame.get_evaluation_step(1); let a_sorted_0 = first_step.get_main_evaluation_element(0, 2); let a_sorted_1 = second_step.get_main_evaluation_element(0, 2); let v_sorted_0 = first_step.get_main_evaluation_element(0, 3); let v_sorted_1 = second_step.get_main_evaluation_element(0, 3); let res = (v_sorted_1 - v_sorted_0) * (a_sorted_1 - a_sorted_0 - FieldElement::<F>::one()); *transition_eval = res; }); }
\
与连续性约束一样，我们提取相关的行和元素：\
\
```rust=
let a_sorted_0 = first_step.get_main_evaluation_element(0, 2); // a'_i
let a_sorted_1 = second_step.get_main_evaluation_element(0, 2); // a'_{i+1}
let v_sorted_0 = first_step.get_main_evaluation_element(0, 3); // v'_i
let v_sorted_1 = second_step.get_main_evaluation_element(0, 3); // v'_{i+1}`
\ 评估结果确保如果两个地址相等，则它们对应的值是一致的。\ \
排列约束\
| \ 现在我们知道 a′a′ 和 v′v′ 表示连续的只读存储器，我们必须证明 a′a′ 和 v′v′ 是原始 aa 和 vv 列的排列。我们将使用交互式协议来实现这一点：\ \ 首先，verifier 将两个随机的 field element z,α∈Fz,α∈F 发送给 prover，被称为 challenges。要记住的一个细节是，如果我们使用小的 field FF，这些元素应该从一个 extension field 中采样，因此以下所有排列约束都将在 extension 上进行。\ \ 注意： 在实践中，协议不是交互式的；相反，Fiat-Shamir 启发式用于获取随机值，从而实现非交互式方法。\ \ 其次，使用这些 challenges，prover 构造一个 auxiliary column pp，它被添加到 main trace table。该列的计算方式为：\ \ p0=z−(a0+αv0)z−(a′0+αv′0),p1=z−(a0+αv0)z−(a′0+αv′0)⋅z−(a1+αv1)z−(a′1+αv′1)=p0⋅z−(a1+αv1)z−(a′1+αv′1),p2=p1⋅z−(a2+αv2)z−(a′2+αv′2).p0=z−(a0+αv0)z−(a0′+αv0′),p1=z−(a0+αv0)z−(a0′+αv0′)⋅z−(a1+αv1)z−(a1′+αv1′)=p0⋅z−(a1+αv1)z−(a1′+αv1′),p2=p1⋅z−(a2+αv2)z−(a2′+αv2′).\ \ 继续这个过程，我们得到：\ \ pi+1=pi⋅z−(ai+1+αvi+1)z−(a′i+1+αv′i+1) 对于 i∈0,…,n−2pi+1=pi⋅z−(ai+1+αvi+1)z−(ai+1′+αvi+1′) 对于 i∈0,…,n−2\ \ 例如，如果 main trace table 是：\ \ | aa | vv | a′a′ | v′v′ |
|---|---|---|---|---|
| 2 | 10 | 0 | 7 | |
| 0 | 7 | 0 | 7 | |
| 0 | 7 | 1 | 20 | |
| 1 | 20 | 2 | 10 |
| \ 那么带有 auxiliary column pp 的表将如下所示：\ \ | aa | vv | a′a′ | v′v′ | pp |
|---|---|---|---|---|---|
| 2 | 10 | 0 | 7 | z−(2+α10)z−(0+α7)z−(2+α10)z−(0+α7) | |
| 0 | 7 | 0 | 7 | z−(2+α10)z−(0+α7)⋅z−(0+α7)z−(0+α7)z−(2+α10)z−(0+α7)⋅z−(0+α7)z−(0+α7) | |
| 0 | 7 | 1 | 20 | z−(2+α10)z−(0+α7)⋅z−(0+α7)z−(0+α7)⋅z−(0+α7)z−(1+α20)z−(2+α10)z−(0+α7)⋅z−(0+α7)z−(0+α7)⋅z−(0+α7)z−(1+α20) | |
| 1 | 20 | 2 | 10 | z−(2+α10)z−(0+α7)⋅z−(0+α7)z−(0+α7)⋅z−(0+α7)z−(1+α20)⋅z−(1+α20)z−(2+α10)z−(2+α10)z−(0+α7)⋅z−(0+α7)z−(0+α7)⋅z−(0+α7)z−(1+α20)⋅z−(1+α20)z−(2+α10) |
\ 查看示例，让我们观察到列 pp 中的最后一个值给出了之前所有值的乘积。由于这些值确实来自排列，因此 numerator（源自 aa 和 vv）中的每个因子必须在 denominator（源自 a′a′ 和 v′v′）中出现一次，相互抵消，从而导致整个乘积等于 11。例如，在上表中，第一个 numerator（橙色）与最后一个 denominator（橙色）抵消：\ \ z−(2+α10)z−(0+α7)⋅z−(0+α7)z−(0+α7)⋅z−(0+α7)z−(1+α20)⋅z−(1+α20)z−(2+α10)=1z−(2+α10)z−(0+α7)⋅z−(0+α7)z−(0+α7)⋅z−(0+α7)z−(1+α20)⋅z−(1+α20)z−(2+α10)=1\ \ 将其推广到任何具有 nn 行的 trace，我们得到以下最后一个值，称为 Grand Product：\ \ pn−1=z−(a0+αv0)z−(a′0+αv′0)⋅z−(a1+αv1)z−(a′1+αv′1)…z−(an−1+αvn−1)z−(a′n−1+αv′n−1)pn−1=z−(a0+αv0)z−(a0′+αv0′)⋅z−(a1+αv1)z−(a1′+αv1′)…z−(an−1+αvn−1)z−(an−1′+αvn−1′)\ \ 然后，使用 zz 和 αα 的随机性（以及 Schwartz–Zippel Lemma），我们知道，为了证明 a′a′ 和 v′v′ 是 aa 和 vv 的排列，足以检查：\ \ pn−1=1pn−1=1\ \ 通过这种方式，保证正确排列的约束被简化为两个 boundary 约束和一个 transition 约束（你可以在 Cairo Paper 的第 9.7.2 节中找到它们）：\ \
1. 初始值 Boundary 约束：\
\ p0=z−(a0+αv0)z−(a′0+αv′0)p0=z−(a0+αv0)z−(a0′+αv0′) 我们检查辅助列中的第一个值是否正确。\ \
2. 最终值 Boundary 约束：\
\
pn−1=1pn−1=1 我们检查 Grand Product 是否等于 1。\
\
在我们的代码中，这两个 Boundary 约束位于 ReadOnlyRAP<F> 的 AIR 实现的 boundary_constraints() 函数中。你可以在注释 //Auxiliary boundary constraints 之后看到它们：\
\
fn boundary_constraints(
&self,
rap_challenges: &[FieldElement<Self::FieldExtension>],
) -> BoundaryConstraints<Self::FieldExtension> {
let a0 = &self.pub_inputs.a0;
let v0 = &self.pub_inputs.v0;
let a_sorted0 = &self.pub_inputs.a_sorted0;
let v_sorted0 = &self.pub_inputs.v_sorted0;
let z = &rap_challenges[0];
let alpha = &rap_challenges[1];
// Main boundary constraints
let c1 = BoundaryConstraint::new_main(0, 0, a0.clone());
let c2 = BoundaryConstraint::new_main(1, 0, v0.clone());
let c3 = BoundaryConstraint::new_main(2, 0, a_sorted0.clone());
let c4 = BoundaryConstraint::new_main(3, 0, v_sorted0.clone());
// Auxiliary boundary constraints
let num = z - (a0 + alpha * v0);
let den = z - (a_sorted0 + alpha * v_sorted0);
let p0_value = num / den;
let c_aux1 = BoundaryConstraint::new_aux(0, 0, p0_value);
let c_aux2 = BoundaryConstraint::new_aux(
0,
self.trace_length - 1,
FieldElement::<Self::FieldExtension>::one(),
);
BoundaryConstraints::from_constraints(vec![c1, c2, c3, c4, c_aux1, c_aux2])
}
\ 请注意，verifier 还必须知道来自 trace 第一行的 aa、a′a′、vv、v′v′ 的值，才能执行 Initial Value 约束的检查。这是我们之前没有遇到的问题（其余约束不依赖于 trace），因为 verifier 只能访问 trace 的 commitment，而不是它的元素。因此，第一行必须是 public input 的一部分。\ \
3. 排列 Transition 约束：\
\
(z−(a′i+1+αv′i+1))⋅pi+1−(z−(ai+1+αvi+1))⋅pi=0(z−(ai+1′+αvi+1′))⋅pi+1−(z−(ai+1+αvi+1))⋅pi=0 对于所有 i∈0,…,n−2i∈0,…,n−2.\
\
通过这种方式，我们检查 pp 的每个元素是否被正确构造，最后一个元素是 Grand Product。在我们的代码中，我们将此 transition 约束称为 PermutationConstraint。在实现其对应的 evaluate() 函数（link）时，可以看到此等式的使用：\
\
fn evaluate(
&self,
frame: &Frame<F, F>,
transition_evaluations: &mut [FieldElement<F>],
_periodic_values: &[FieldElement<F>],
rap_challenges: &[FieldElement<F>],
) {
let first_step = frame.get_evaluation_step(0);
let second_step = frame.get_evaluation_step(1);
let p0 = first_step.get_aux_evaluation_element(0, 0);
let p1 = second_step.get_aux_evaluation_element(0, 0);
let z = &rap_challenges[0];
let alpha = &rap_challenges[1];
let a1 = second_step.get_main_evaluation_element(0, 0);
let v1 = second_step.get_main_evaluation_element(0, 1);
let a_sorted_1 = second_step.get_main_evaluation_element(0, 2);
let v_sorted_1 = second_step.get_main_evaluation_element(0, 3);
let res = (z - (a_sorted_1 + alpha * v_sorted_1)) * p1
- (z - (a1 + alpha * v1)) * p0;
transition_evaluations[self.constraint_idx()] = res;
}
\
摘要\
\ 通过引入排序后的列和 auxiliary column，我们将验证连续只读存储器的问题简化为证明三个更简单的约束：\ \
- 连续性，确保所有存储器地址形成一个完整的范围。\
- 单值，确保每个地址始终返回相同的值。\
- 排列，确保排序后的列是原始列的排列。\
\
这些约束演示了 STARKs 在将复杂关系编码为多项式方程方面的简单性。\
\
\
\
我们采访了正在开发 Iroh 的团队，Iroh 是一个可以直接使用的 Rust peer-to-peer 库。\
\
\
\
介绍\
\
交互式证明是 prover PP 和 verifier VV 之间的协议，其中 prover 尝试说服 verifier 语句的有效性。通过利用随机性和交互性，verifier 可以比完成所有事情更有效地检查语句\
\
\
\
TL;DR: 这篇文章讨论了 Pod，一种新的共识概念，通过消除副本间通信，实现了 200 毫秒的 one round-trip 最佳延迟。我们相信本文和 pod network 的工作是开创性的，我们希望其他人也能分享我们对他们的工作的兴奋和热情，
- 原文链接： blog.lambdaclass.com/con...
- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
