算术化：将计算问题转换为有限域 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 即为承诺。

步骤如下

• 调用 coset_lde_batch() 计算 LDE：

  let mut poly = domain.ifft(trace);
  let extended_domain = domain.get_coset(shift).extend(blowup);
  let extended_trace = extended_domain.fft(&poly);

  zkvm-brainfuck 中采用的爆炸因子是 1，即 log_blowup=1，所以新 trace 表的高度是原始的 2 倍（1 << log_blowup）。

• 调用 MerkleTreeMmcs::commit() 采用 MMCS (Mixed Matrix Commitment Scheme) 批量承诺多个 LDE：将新 trace 表作为叶子节点构建 Merkle 树，root 即为承诺。

过程详见：Stark101-part1

2.2 Open

代码

步骤如下：

• 生成 lookup trace

  根据 main trace 的承诺计算 lookup 挑战值，用到 LogUp 和 Multiset Hashing

• 生成 lookup trace 的 Merkle 承诺

  用与上一章承诺 main trace 同样的方式承诺 lookup trace。这种两阶段承诺方式符合随机化 AIR 预处理 (Randomized AIR with Preprocessing, RAP)

• 生成 quotient trace

  • 计算商多项式的 domain

  • 获取该 domain 上的 trace 点

  • 根据 trace 点和约束算出状态转换多项式（evaluations 形式）

  • 状态转换多项式除以相应的消失多项式 $Z_{H_i}(X) = x^n - 1$，得到商多项式 $p_i(x) = constraintsi(x) / Z{H_i}(x)$ （evaluations 形式），即为 quotient trace

• 生成 quotient trace 的 Merkle 承诺

• 根据 quotient trace 的承诺计算挑战值 $\zeta$，得到如下 Merkle 树的打开点 $z$：preprocess，main，lookup 和 quotient

• 调用 plonky3 的 open() 批量打开多个商多项式并生成打开证明： $$ \sum_i​α^i⋅\frac{p_i​(X)−y_i}{X−z} $$

  • $p_i(X)$ 是 evalutions 形式的商多项式
  • $y_i=p_i(z)$ 是 Barycentric interpolation 结果，$z$ 是打开点

  运行 FRI 协议

  • commit phase: 每轮都将多项式的次数折半，并且生成该多项式的 Merkle 承诺。如果 $log(d)$ 轮后终得到一个常数多项式，则可以说明多项式的阶接近于 $d$
  • query phase: 提供一组验证者随机选择点的评估，并生成其 Merkle proof，以便让验证者确认每一轮承诺的多项式彼此间是一致的

  从而证明多个点的打开值的一致性以及相应多项式的低度性质，确保提交的多项式满足预期约束

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

BrainSTARK, Part I: STARK Engine

stark101

zkStark

Anatomy of a STARK, Part 4: The STARK IOP