算术化：将计算问题转换为有限域 F 上的多项式代数问题。
zkSTARK 算数化会构建程序的代数中间表达 (Algebraic Intermediate Representation, AIR)，用 s 个多项式描述当前执行状态与下一步状态的转换约束。
算术化中会得到两种 witness：
- 整个待证明程序的执行轨迹 execution trace，对应迹多项式。轨迹可以看着一组寄存器的状态转换过程，是基于状态转换表格中的列构造出的多项式。
- 在执行过程中需要满足的约束条件 constraint，对应商多项式。约束包括两部分，边界约束和状态转换约束。
接下来对执行迹和约束条件做多项式承诺，用 FRI 证明商多项是低阶的。迹多项式没有被证明为低阶，这不会降低安全性，因为它的低阶性是由商多项式的低阶性所隐含的。
图片来源：Anatomy of a STARK, Part 1: STARK Overview
1 Setup
得到 preprocess trace 及承诺，承诺方式见 2.1。prover 和 verifier 都需要运行。
2 Prove
2.1 Commit
生成 main trace，并对所有 main trace 承诺。main trace 中不包含 lookup 列。
得到 $T$ 行 $w$ 列的 trace 表后，为找到每列的低次多项式，需对每一列进行插值，横坐标为 $o^i$，$o$ 是阶为 $T$ 的一个子群的生成元，得到的多项式为 trace 多项式。
为了引入冗余抵抗恶意篡改，trace 会被插值到更大的域（例如，从 N 点扩展到 8N 点），但多项式的度仍保持 ≤N−1。一般需要将域扩大 $2^k$ 倍，$k$ 称为爆炸因子（blowup factor），该域称为 LDE 域。
求出 trace 多项式在 LDE 域上的值，以这些值为叶子节点，组成一棵 Merkle 树，root 即为承诺。
步骤如下
- 调用 plonky3 的
natural_domain_for_degree()得到 LDE 域，一个 2-adic 乘法陪集。 调用 plonky3 的
commit()函数：- 调用
coset_lde_batch()将 trace 表的每列进行插值，得到 trace 多项式。然后将 trace 多项式在 LDE 域上求值，因为 LDE 域更大，所以 trace 表的高度会增加，但宽度保持不变。zkvm-brainfuck 中采用的爆炸因子是 1，即 log_blowup=1，所以新 trace 表的高度是原始的 2 倍（1 << log_blowup）。 - 调用
MerkleTreeMmcs::commit()采用 MMCS (Mixed Matrix Commitment Scheme) 批量承诺多个新 trace 表。将新 trace 表作为叶子节点构建 Merkle 树，root 即为承诺。
- 调用
过程详见：Stark101-part1
2.2 Open
步骤如下：
- 根据 main trace 的承诺计算 lookup 挑战值，进而生成 lookup trace
- 用与上一章承诺 main trace 同样的方式承诺 lookup trace。这种两阶段承诺方式符合随机化 AIR 预处理 (Randomized AIR with Preprocessing, RAP)
- 计算商多项式的 LDE 域：爆炸因子 k = log2(最大 preprocess 约束的度 - 1) + log2 (main trace 高度）
在在商多项式的 LDE 域上逐点评估所有 AIR 约束，并除以相应的零化器 $Z_H(X) = x^n - 1$，生成商多项式值 $quotient(x) = constraints(x) / Z_H(x)$，即为 quotient trace
具体步骤为：
- 调用
pcs.get_evaluations_on_domain()用 preprocess trace，main trace 和 lookup trace 多项式分别在商多项式的 LDE 域上计算出新的 preprocess trace，main trace 和 lookup trace 点 - 调用
chip.eval()计算 AIR 约束，得到转换多项式和边界多项式值 - 转换多项式和边界多项式值除以相应的零化器 $Z_H(X) = x^n - 1$，生成商多项式值
- 调用
- 用与上一章承诺 main trace 同样的方式承诺 quotient trace
- 根据 quotient trace 的承诺计算挑战值 $\zeta$，得到 Merkle 树的打开点：preprocess，main，lookup 和 quotient
调用 plonky3 的
open()批量打开多个多项式并生成打开证明。它利用 FRI 协议来证明多个点的打开值的一致性以及相应多项式的低度性质，确保提交的多项式满足预期约束。open()的一个关键步骤是将多个多项式组合为一个多项式：$$ q(x) = \sum_i\alpha^i(p_i(x) - y_i) / (x - z_i) $$
- $q(x)$ 是组合多项式的商多项式
- $\alpha$ 是随机挑战值，根据 lookup trace 和每个 lookup trace 表的累加和算出
- $p(x)$ 是目标多项式
- $z_i$ 是打开点
- $y_i$ 是多项式 $p_i$ 在 $z_i$ 处的打开值，使用 barycentric 插值计算
- $x_i, p_i(x)$ 在 LDE 域，$\alpha, z_i, y_i$ 在基域，基域是一个比 LDE 域大得多的域
3 Verify
步骤如下：
- 根据 quotient trace 的承诺计算挑战值 $\zeta$，得到 Merkle 树的打开点：preprocess，main，lookup 和 quotient
调用 plonky3 的
verify()运行 FRI 验证：- 验证折叠关系：在新值的 Merkle 树同一层上抽取 N 个相关的折叠点，在下一层上抽取一个点，就能验证本层的 N 个点确实按正确的随机数折叠到下一层的同一个点。
- 验证折叠后的多项式的阶
验证多项式是否匹配，确保多项式来源于转换约束、边界约束。验证者自己计算 k 个多项式的值，与证明方计算的值看是否相等，防止证明方承诺一个伪造的低阶多项式。
具体步骤为：
- 重新计算商多项式值 $quotient(\zeta)$，验证与打开点是否想等
- 重新计算约束多项式值 $constraints(\zeta)$
- 验证 $constraints(\zeta) / Z_H(\zeta) = quotient(\zeta)$
参考
Mastering SP1 zkVM design-part 3: Core proof
没有评论