STARK：AIR、低度测试与透明性

2025-12-07 约 2974 字预计阅读 6 分钟

Scope. 本文沿用上一篇算术化文章中的四行 Fibonacci trace，追踪它从 AIR 约束进入 composition oracle，再落到第一轮 FRI 查询。

STARK 的证明对象是一张 execution trace。AIR 把 trace 的合法性写成多项式约束，composition polynomial 将多条约束合成一个受度数界约束的对象，FRI 再检查 prover 承诺的评值 oracle 是否接近相应的低度多项式。三部分通过承诺和 transcript 顺序连接：

\[ \text{trace} \longrightarrow \text{AIR constraints} \longrightarrow \text{composition polynomial} \longrightarrow \text{FRI low-degree test}. \]

STARK 证明的对象是什么

STARK 的 witness 通常写成某个 computation 的 execution trace。

设一个计算被展开成 \(N\) 个时间步，且每步有 \(k\) 个寄存器列。则 trace table 可写成

\[ T \in \mathbb{F}^{N \times k}. \]

第 \(i\) 行是第 \(i\) 步状态，第 \(j\) 列是一条寄存器轨迹。这里 prover 声称：

这整张 trace 是某个合法计算的执行结果。

AIR Constraint System

AIR, Algebraic Intermediate Representation，把这句“trace 合法”拆成两类约束。

第一类是 boundary constraints。它们固定某些特定位置的值，例如初始状态、公开输入、终止输出：

\[ T_{0,1} = x,\qquad T_{N-1,2} = y. \]

第二类是 transition constraints。它们描述相邻若干行之间必须满足的递推关系。例如某个单寄存器递推可以写成

\[ T_{i+1,1} - T_{i,1}^2 - c = 0. \]

更一般地，若一组列在窗口大小 \(\ell\) 上满足某个多变量多项式关系，则写成

\[ \Phi\big(T(i), T(i+1), \dots, T(i+\ell)\big)=0 \]

对所有有效步成立。

AIR 的最小接口由 trace domain、boundary constraints 和 transition constraints 组成。源码或 VM 语义必须先被编译到这组接口，才能进入后续证明。

从 AIR 到 Composition Polynomial

仅仅列出很多条 AIR constraints 还不够。和 QAP 一样，证明系统更喜欢一个被合成后的单一对象。

Trace Columns As Polynomials

首先把每一列 trace 在某个评估域 \(D\) 上插值成列多项式：

\[ t_j(X),\qquad j=1,\dots,k. \]

这样，原来“第 \(i\) 步第 \(j\) 列的值”就被编码成“在域点 \(\omega_i\) 上的多项式取值”。

于是 boundary constraints 可以改写成某些固定点评值条件，transition constraints 可以改写成这些列多项式在相邻点上的多变量关系。

Constraint Combination

STARK 不会把每一条约束都单独证明。常见做法是用随机系数把多条约束组合成一个 composition polynomial。形式上，可以把若干归一化后的约束项写成

\[ C_1(X), C_2(X), \dots, C_m(X), \]

然后取随机挑战系数 \(\alpha_1,\dots,\alpha_m\)，构造

\[ \mathrm{Comp}(X) = \sum_{j=1}^m \alpha_j C_j(X). \]

这里每个 \(C_j(X)\) 往往已经除掉了相应的 vanishing factors，使其在合法 trace 上应当保持低度。

composition polynomial 承担三项工作：

把很多局部约束压成一个统一对象
让 prover 无法分别对不同约束作弊
让 verifier 只需对一个组合对象做低度性和一致性检查

Key Observation. STARK 里的 composition polynomial，扮演的是和 QAP 中 quotient/divisibility claim 类似的接口角色：把很多局部约束压成 verifier 真正要消费的单一代数对象。

沿用四行 Trace 算出 Composition

上一篇在 \(\mathbb F_{17}\) 中取 \(\omega=4\) 与

\[ H=\{1,4,16,13\}, \]

并把 trace \((1,1,2,3)\) 插值为

\[ t(X)=6+6X+4X^2+2X^3. \]

对应的两个 boundary quotients 和 transition quotient 为

\[ Q_0(X)=2X^2+6X+12, \]\[ Q_1(X)=2X^2+12X+3, \]\[ Q_{\mathrm{tr}}(X)=4X+7. \]

为便于手算，本节固定 \((\alpha_0,\alpha_1,\alpha_2)=(1,2,3)\)。于是

\[ \begin{aligned} C(X) &=Q_0(X)+2Q_1(X)+3Q_{\mathrm{tr}}(X)\\ &=6X^2+8X+5 \pmod {17}. \end{aligned} \]

实际协议不能预先固定这些系数。prover 先承诺 trace LDE，verifier 再从 transcript 导出 \(\alpha_i\)；否则 prover 可以针对已知线性组合安排约束误差相消。这里的固定值只用于把同一条 trace 继续带入 FRI。

低度为什么是 soundness certificate

低度界把局部 AIR 约束变成可随机抽查的全局结构，是 soundness 分析的一部分。

Low-Degree Extension

trace 和 composition object 通常会扩展到更大的评估域，也就是 low-degree extension, LDE。verifier 随后在这个较大域上抽查对象行为。

满足 AIR 的 trace 会产生具有已知度数上界的列多项式和 composition polynomial。

What A Cheating Trace Breaks

若 prover 伪造了一张不合法的 trace，会发生什么？

边界条件或转移条件一旦被破坏，组合约束对象就不再与某个低度多项式一致。也就是说，作弊者也许能在少量点上伪装局部值，但它很难让整张 oracle table 在全域上继续看起来像一个满足度数界的对象。

“低度 acts as a soundness certificate”可以拆成三项可检查的陈述：

合法计算诱导低度结构
非法计算往往只能伪造局部一致性
verifier 通过随机查询低度结构，捕捉这种全局不一致

Groth16 最终检查 pairing 空间里的代数等式；这里 verifier 检查承诺后的 oracle 是否同时满足低度性和 AIR 查询一致性。两者消费的算术化接口不同。

FRI 在 STARK 里扮演什么角色

现在把 FRI 放回主流水线。

STARK prover 会把 trace / composition objects 的评值表承诺成 oracle，通常再用 Merkle tree 固定。verifier 拿到的是：

一个承诺好的 evaluation oracle
若干随机挑战
若干查询路径与一致性证明

FRI 的任务就是回答：

这个 oracle 是否确实接近某个低度多项式？

一轮 FRI 的承诺与查询

FRI 的核心仍然是 folding。对一个多项式

\[ f(X)=f_0(X^2)+Xf_1(X^2), \]

取随机挑战 \(\beta\)，构造

\[ g(X)=f_0(X)+\beta f_1(X). \]

这会把原来的低度测试问题压缩到更小域、更低度的新对象上。反复多轮后，verifier 检查：

每轮 folding 前后的局部值是否一致
最终压缩到很小的对象是否满足显式低度界

把上面的 \(C(X)=6X^2+8X+5\) 放到八点域 \(D=\langle 2\rangle\subset\mathbb F_{17}^{*}\) 上。prover 先发送其评值表的 Merkle root \(R_0\)，transcript 吸收 \(R_0\) 后给出 folding challenge。手算继续取 \(\beta=7\)。将

\[ C(X)=C_0(X^2)+XC_1(X^2) \]

拆为

\[ C_0(Y)=6Y+5,\qquad C_1(Y)=8, \]

得到下一层多项式

\[ G(Y)=C_0(Y)+\beta C_1(Y)=6Y+10. \]

prover 对 \(G\) 在平方后的四点域上求值并发送新 root \(R_1\)。查询索引必须在 \(R_0,R_1\) 均固定后产生。若 transcript 选到 \(x=2\)，prover 打开

\[ C(2)=11,\qquad C(-2)=C(15)=13, \]

以及 \(G(2^2)=G(4)=0\)，并为三个叶子提供 Merkle authentication paths。verifier 从第一层的两个值重建

\[ C_0(4)=\frac{C(2)+C(-2)}{2}=12, \]\[ C_1(4)=\frac{C(2)-C(-2)}{2\cdot2}=8, \]

再检查

\[ G(4)=C_0(4)+7C_1(4)=0\pmod {17}. \]

Merkle binding 固定每层 oracle，\(\beta\) 防止 prover 预先选择有利的偶/奇分解，末尾才产生的 query index 则阻止 prover 只修补将被抽查的位置。实际 soundness 还依赖 Reed–Solomon distance、每轮度数下降、足够的查询次数和 grinding 参数；这一轮等式本身不提供完整误差界。

From FRI Back To AIR

FRI 接收前面 composition pipeline 产出的 oracle。AIR 查询还要把 composition 开值与 trace 开值、相邻行开值对齐，防止 prover 分别承诺两个互不一致的低度对象。

因此 STARK 的 soundness 叙事是两段连在一起的：

AIR 把 trace 合法性压成 composition polynomial 应满足的结构
FRI 证明 prover 承诺的那个组合对象确实具有相应的低度与一致性

如果 AIR 查询没有绑定到 FRI oracle，低度测试只说明某个多项式低度；如果没有低度测试，少量 AIR 查询无法约束整张远距离 oracle。完整论证需要两部分共享承诺与查询点。

透明性与 post-quantum 定位

STARK 最常被拿来宣传的两个词是 transparent 和 post-quantum。这两个词都该拆开讲。

Transparent Setup

transparent 在这里表示：

不需要像 Groth16/KZG 那样的 toxic waste ceremony
verifier 和 prover 只依赖公开域、公开哈希、公开随机挑战流程

也就是说，系统不依赖某个秘密结构参数没有泄露。这和前面的 pairings + structured CRS 路线形成明确对照。

Why People Call It Post-Quantum

STARK 常被称为 post-quantum，主要因为其核心安全叙事更接近：

哈希函数安全性
信息论式或组合式 low-degree testing soundness
不依赖 pairing 或传统离散对数那类结构化代数假设

这个定位仍需声明量子随机预言机模型、哈希输出长度和具体参数；“STARK”这一名称本身不构成量子安全证明。其主要安全基础通常比 pairing-based SNARK 更适合 post-quantum setting。

所以这里也要避免口号化。transparent 说的是 ceremony boundary；post-quantum 说的是主要依赖的 hardness surface。

Summary

STARK 可以按一条连续流水线复核：

witness 被展开成 execution trace
AIR 把合法执行写成 boundary constraints 和 transition constraints
这些约束被组合成 composition polynomial
prover 对相应 oracle objects 做承诺
FRI 证明这些对象确实保持预期低度与 folding 一致性

verifier 的结论来自两组绑定检查：

这张 trace 的约束组合对象看起来像合法低度多项式
少量随机查询足以高概率发现伪造 trace 的全局不一致

如果把 Groth16 看成 QAP + structured CRS + pairing equation，那么 STARK 可以看成

\[ \text{AIR} + \text{oracle commitment} + \text{FRI low-degree test}. \]

这条路线换来了 transparent setup、更大的 proof、以及更 query-based 的 verifier 工作方式。下一层进入更现代系统时，PLONKish、递归和工程约束讨论的，其实都是在这些不同 algebraic surfaces 和 proof pipelines 上继续做设计。

目录