STARK Arithmetization

1. 引言

前序博客有：

• ZKP大爆炸
• STARKs and STARK VM: Proofs of Computational Integrity
• STARK入门知识
• STARK中的FRI代码解析
• Rescue-Prime hash STARK 代码解析
• Fast Reed-Solomon Interactive Oracle Proofs of Proximity学习笔记
• STARK Low Degree Testing——FRI

通过本文，将理解如何将Computational Integrity statement转换为：

• 1）execution trace；
• 2）polynomia constraints多项式约束。

2. 初识STARK

STARK协议的目标是：

• verify computations succinctly and transparently。

STARK的第一步称为Arithmetization：

• 用于将待验证的计算问题 转换为 检查特定的低度多项式问题，使得Verifier端可高效验证（即“succinctly”验证）。

算术化是有用的，因为它可以使用纠错码领域的工具，有效地进行低度测试。
但是算术化本身近似将Computational Integrity statement转换为某多项式，然后Prover需要通过STARK Low Degree Testing——FRI 交互协议来使Verifier信服该多项式确实是低度的。当且仅当原始计算是正确时（除外概率很低），Verifier才信服该多项式是低度的。STARK最后一步会将FRI交互协议转换为非交互协议，可将相应的非交互STARK提交到链上并由任何人公开验证。

Arithmetization算术化本身分为2个阶段：

• 1）生成execution trace和多项式约束；
• 2）将execution trace和多项式约束合并为一个单一的低度多项式。

Prover和Verifier交互过程中，实际是对多项式约束达成共识。然后Prover生成execution trace，并在后续的交互过程中，Prover试图说服Verifier其execution trace满足该多项式承诺，尽管execution trace对Verifier是不可见的。

2. 回顾Computational Integrity Statements

传统的Computational Integrity Statements举例为：如，给超市的付款总金额计算正确，传统的proof是如下的收据：

收据中包含每项内容及相应的价格，总金额列在最下面。

简单起见，将该statement理解为：求和计算正确。
为验证该statement是否成立，方法之一对着收据逐项求和，检查最终的值是否与收据下方的值一致。

3. Arithmetization第一阶段——代数表示

算术化的第一阶段是将某CI statement（如“区块7218290内的第15笔交易是正确的”），转换为 formal algebraic language。

主要有2个目的：

• 1）以非模糊的方式简洁地定义了该claim；
• 2）将该claim嵌入到某algebraic domain。这种嵌入需要借助算术化第二阶段，来将某CI statement reduce为 关于特定degree多项式的claim。

algebraic表示时通常有2大要素：

• 1）an execution trace：为表示每步底层计算的表，其中每行对应一步。
• 2）a set of polynomial constraints：构建了一组多项式约束，使得当且仅当该execution trace表示了有效的计算时，这些约束才满足。

execution trace可能很长，但多项式约束可比较精简。

3.1 Execution Trace

所生成的execution trace应易于精简测试，应具有如下两个特点：

• 1）每行都可仅依赖trace中的相邻行进行验证；
• 2）每组pair of rows可应用相同的验证流程。

以上两个特点将直接影响STARK proof size。
仍然以超市收据为例，来说明何为易于精简测试：

通过引入新的一列“running total”，使得可在已知previous row的情况下，独立验证每一行。

如在计算中检查这2行：

仅需检查12.96+3.45=16.41即可。注意，对于每组pair of rows，都可使用相同的约束，我们将其称为succinct constraints。

3.2 Polynomial Constraints

将添加了新列的超市收据以table表示为：

将第$i$行第$j$列的单元格值表示为$A_{i,j}$，从而可将求和正确性 改写为 一组多项式约束：

• 1）$A_0,2=0$，因初始running total值应为0；
• 2）$\forall 1\le i\le 5:A_{i,2}-A_{i-1,2}-A_{i-1,1}=0$，每一行的running total值都计算正确；【为同一约束执行多次】
• 3）$A_{5,1}-A_{5,2}=0$，最后一行的running total值即为总额。

这些即为$A_{i,j}$的线性多项式约束。若所使用的多项式为high degree，则对proof length和生成证明所需时间 都有反向作用。因此，线性约束是我们所希望的最好状态。

多项式约束的size与收据的长度无关。

从而，将验证超市收据总额的CI problem，转换为一个精简易于测试的execution trace，以及相应的一组多项式约束，使得当前仅当原始收据的总额是正确的，这组多项式约束才成立。

3.3 更复杂的举例——Collatz Conjecture

1937年，德国名为Lothar Collatz的数学家在数论领域提出了Collatz Conjecture。初看这是一个可爱的数学谜题，但实际上，它是数论领域的一个公开难题。数年来它吸引了很多数学家的注意，获得了大量同义词（如the 3n + 1 conjecture, the Ulam conjecture, Kakutani’s problem等等）。Paul Erdős曾评论称：“Mathematics may not be ready for such problems”。

Collatz数列以任意正整数开始，其中后续元素的计算规则为：

• 1）若前一元素为偶数，将其除2；
• 2）若前一元素为奇数且大于1，则将其乘以3再加1；
• 3）若前一元素为1，则停止。

以初始值为52为例，有：
52 -> 26 -> 13 -> 40 -> 20 -> 10 -> 5 -> 16 -> 8 -> 4 -> 2 -> 1.

Collatz Conjecture是指：以任意正整数开始，最终Collatz数列都将达到1值。

不过，Collatz Conjecture本身并不在本文考虑范畴，本文重点关注：如何验证以某特定整数开始的Collatz数列计算正确。

3.3.1 Collatz数列 Execution Trace

Collatz数列的CI statement为：
“A Collatz sequence that starts with 52, ends with 1 after 11 iterations”。

令$A$为该数列计算的execution trace，第$i$行表示为$A_i$，对应为该数列中的第$i$个元素。所有元素都以二进制表示，使得其易于在多项式中表示其奇偶性。以$A_{i,j}$表示数列中第$i$个元素的第$j$个最低有效位。如$A_0=001011$表示初始值52（注意52的二进制表示为1101001，在此处以逆序表示，以简化后续多项式约束中的索引）。

对应的execution trace为：

注意，该trace中仅有6列，是因为6个bit就足以表达该数列中的最大值了。若初始值为51，则最大值为154，相应的trace表示需引入8列。

3.3.2 Collatz数列多项式约束

当且仅当trace A中描述了指定的Collatz数列（以52开始，以1结束，相邻2行的transition计算正确），相应的多项式约束才成立。
本例中，trace A的size为6x12，即表示Collatz数列中有12个6-bit数字，相应的多项式约束为：【$n=12,m=6$】

前三个约束很直观：

• 1）第一个约束第一行初始值的二进制表示为52；
• 2）第二个约束最后一行的二进制表示为1；
• 3）第三个约束trace中所有值均为bits，仅可取0或1值；
• 4）第4个约束是表示该序列succinct computation的核心，即表示了every相邻行之间的关联。将计算约束表示为局部约束的循环模式（即简洁性）的能力是Verifier比计算的简单重放快指数的基础。【The ability to express computational constraints as a recurring pattern of local constraints (i.e. succinctness), is fundamental to the verifier being exponentially faster than a naive replay of the computation.】

接下来仔细检查这些约束，对于任意的$i<n-1$，有：

对于每一个$i<n-1$，有约束：

$A_{i,0}$为第$i$个元素的最低有效位，可确定该整数的极性，因此，该约束可用于描述Collatz sequence的规则。

总之，当前仅当execution trace代表了某Collatz sequence的有效计算时，以上所有约束才能满足。

注意，任意长度为$n$的Collatz数列，可以$n\ast m$大小的trace来表示，其中$m$为该数列中最大值所需要的bit数，相应的多项式约束也需要调整。但是，注意，多项式约束并不会随着$n和m$增加，仍保持简单和简洁性。

已知Collatz数列的某特定初始值，一个简单的计算机程序就可输出相应的execution trace和多项式约束。

3.4 算术化第一阶段小结

以Collatz数列为例，展示了如何将CI statement转换为execution trace和多项式约束。类似的方法也可用于转换任何计算，通常，任意CI statement都可转换为该形式。具体的细节可能千差万别。
同时，对于同一计算，可能有多种execution trace和多项式约束表示方法，但是，只有一小部分方法会产生一个小的、可以有效构造的STARK证明。Starkware团队推荐使用AIR（Algebraic Intermediate Representation）来生成好的多项式约束。

4. 算术化第二阶段

算术化第二阶段，用于将算术化第一阶段中生成的execution trace和一系列多项式约束 转换为a single polynomial，使得当且仅当该多项式是低度的，原始计算才是正确的。这样转换之后，可实现succinct verification，使得Verifier该计算所需的资源 为指数级少于 自己直接重放整个计算。

4.1 Queries and Error Correction Codes

回顾下，基本目的是，支持Verifier向Prover询问非常少量的问题，然后以很高的准确性来判断是接受还是拒绝该proof。
理论上，Verifier可让Prover提供execution trace中的少量随机位置的值，然后检查多项式约束在这些位置是否成立。正确的execution trace自然可测试通过，但是，构建一个并不完全错误的execution trace并不困难，使得仅在某个单点位置违背了相应的约束，将导致一个完全不同的输出。为识别类似这种错误，仅通过少量随机queries是极不可能的。

针对该问题的通用技术为Error Correction Codes，纠错码。

纠错码可将一组非常相似的字符串，转换为，相互非常不同的字符串，相比于原始字符串，纠错码编码之后的字符串长度更长。

有趣的是，多项式可用于构建很好的纠错码，因为对于2个不同的degree为$d$的多项式，基于比$d$更大的domain进行evaluate时，其几乎在所有位置都是不同的，这样的码也称为Reed-Solomon码。
即相应的多项式fact为：

经观察可发现，可将execution trace看成是某多项式基于某domain的evaluation值，并扩展为在更大的domain对同一多项式evaluate。以类似的方式扩展不正确的execution trace会导致非常不同的字符串，这反过来使得Verifier可以使用少量查询来区分这些情况。

所以，接下来的计划是：

• 1）将execution trace重组为某多项式
• 2）将该多项式扩展至更大的域【在将约束合并前，已将execution trace扩展至更大的域了】
• 3）与多项式约束一起，转换为另一多项式，使得该多项式是低度的，当且仅当该execution trace是正确的。

4.2 玩具举例——Boolean Execution Trace

如，CI statement为：
“The prover has a sequence of 512 numbers, all of which are either 0 or 1”。

希望通过读取远远少于512个数字来验证这一点。

接下来看相应的execution trace和多项式约束为：

• 1）execution trace具有512行，每行具有一个cell，要么为0或1；
• 2）多项式约束为：$A_i\ast A_i-A_i=0$，约束每个cell值要么为0或1。

未来将execution trace重组为多项式：

• 1）取域为$Z_{96769}$——由整数$0,1,\cdots ,96768$组成，具有基于96769的模乘和模加运算。$96769-1=2^9\ast 3^3\ast 7$
• 2）基于$Z_{96769}^{\ast }$选择subgroup $G$，使得$|G|=2^9=512$，且$G$的generator为$g$。（以$F^{\ast }$来表示$F$的乘法群，乘法群元素为域中的零值除外）
• 3）可将execution trace中的元素看成是某degree小于512的多项式$f(x)$的evaluation值：第$i$个cell为evaluate $f$ at $g^i$的值：
  
• 4）可通过插值来获得degree最多为512的多项式，然后基于更大的domain对其进行evaluate，形成一种Reed-Solomon编码特例。【更大的domain意味着更小的soundness error。】
• 5）最后，使用该多项式来创建另一个低度多项式，该低度多项式取决于execution trace所需满足的约束。为此，需引入tangent和roots of polynomials。

4.2.1 Roots of Polynomials 以及 合并为一个低度多项式

多项式及其roots的一个基本fact为：
若$p(x)$为某多项式，且对于某$a$有$p(a)=0$，则当且仅当存在某多项式$q(x)$，使得$(x-a)q(x)=p(x)$，且$\mathrm{deg}(p)=\mathrm{deg}(q)+1$。

对于所有的$x\ne a$，可evaluate $q(x)$为：
$$q(x)=\frac{p(x)}{(x-a)}$$

依次类推，对于$k$个roots { a 0 , a 1 , ⋯   , a k − 1 } \{a_0,a_1,\cdots,a_{k-1}\} {a0​,a1​,⋯,ak−1​}，存在degree为$\mathrm{deg}(p)-k$的多项式$q(x)$：
$$q(x)=\frac{p(x)}{{\prod }_{i=0}^{k-1}(x-a_i)}$$

将约束$A_i\ast A_i-A_i=0$以$f$多项式表示为：
$$f(x{)}^2-f(x)=0$$
定义其roots为$1,g,g^2,\cdots ,g^{511}$，当且仅当execution trace中的cell为0或1。从而可定义：
$$p(x)=\frac{f(x{)}^2-f(x)}{{\prod }_{i=0}^{511}(x-g^i)}$$
即存在degree最多为$2\cdot \mathrm{deg}(f)-512$ 的某多项式agrees with $p$ on all x ∉ { 1 , g , g 2 , ⋯   , g 511 } x\notin\{1,g,g^2,\cdots,g^{511}\} x∈/{1,g,g2,⋯,g511} 当且仅当 该execution trace确实为a list of 512 bits（即0或1）。

注意，此前，Prover已将该execution trace扩展至更大的domain了，因此querying for the polynomial values in that domain is well defined。

若存在某协议（见STARK Low Degree Testing——FRI）使得Prover可使Verifier信服该多项式确实是低度的，使得Verifier仅需请求该execution trace之外的值，从而仅当该CI statement确实为true时，Verifier才会被说服。

4.3 举例——Fibonacci数列

如需证明基于$Z_{96769}$域的Fibonacci数列计算正确：
$a_0=1$
$a_1=1$
$a_{n+2}=(a_{n+1}+a_n)\mathrm{mod}96769$

claim为$a_{511}=62215$。

相应的execution trace为：

相应的多项式约束为：

4.3.1 将多项式约束转换为多项式

定义degree最多为512的多项式$f(x)$，使得：

将多项式约束以$f$表示为：

由于多项式的组合仍然为一个多项式——将约束中的$A_i$替换为$f(g^i)$仍然是多项式约束。
注意，其中的1、2、4约束仅引用$f$的某单个值，我们将这种约束称为boundary constraints。

Fibonacci的递归关系，体现在了基于整个execution trace的一组约束，可重组表示为：

使用generator $g$来作为execution trace行的索引，有助于以简单的代数关系来表示“下一行”。若$x$为execution trace中的某行，则$gx$表示其下一行，$g^{2}x$表示下两行，$g^{-1}x$表示前一行。

最后两行除外，对于execution trace中的每一行的index$x$值，递归关系多项式$f(g^{2}x)-f(gx)-f(x)=0$。即意味着$1,g,g^2,\cdots ,g^{509}$为该递归关系多项式的all roots（且该递归关系多项式的degree最多为510），从而可构建如下$q(x)$：

在STARK中，通常将$q(x)$称为组合多项式（composition polynomial）。当原始的execution trace遵循该Fibonacci递归关系时，仅当on all but these 510 values：$1,g,g^2,\cdots ,g^{509}$时，$q(x)$这种表示对应某degree最多为2的多项式（注意$f$的degree最多为512）。不过composition polynomial这个属于有些不准确——当execution trace不满足相应的多项式约束时，$q(x)$的evaluation值 differ from any low degree polynomial in many places。换句话说，当且仅当原始CI是正确的时，$q(x)$ close to 某低度多项式，这正是我们的目的。

通过以上步骤，可将 “检查某些特定多项式是否成立的问题” 转换为 “检查某多项式（对Prover已知）是否具有low degree”。

4.3.2 Succinctness

对于STARK来说，具有高效的verification技术至关重要。
STARK验证过程由2部分组成：

• 1）使用少量的query：可通过纠错码实现，使得仅需query很少的位置。
• 2）每次query，Verifier仅需做少量计算

Verifier的工作主要有：

• 1）query composition polynomial的随机点；【原因在于Prover可能作弊，当Verifier请求composition polynomial位置$x$的evaluation时，Prover可能返回某个确实是低度的多项式在$x$处的evaluation值，但是该值并不是相应的composition polynomial，从而使得low-degree testing无法通过。】
• 2）基于这些query，做low-degreeness检查。【详细见STARK Low Degree Testing——FRI】

为避免1）中的情况，Verifier在query Fibonacci execution trace at 某行$w$时，实际是请求$f$在3个位置的值：$f(w),f(gw),f(g^{2}w)$。

Verifier可自行计算composition polynomial在$w$处的值：

其中：

• 分子可根据Prover给的值计算，这有一些rub，后续将处理掉。
• 分母为与execution trace完全独立的部分，Verifier可在与Prover通信之前计算出来。

不过，trace中可能包含数十万行，计算分母将消耗Verifier大量时间。

以下计算对于succinctness来说至关重要——因，对the powers of $g$形成的subgroup，有：

该等式成立，因等式两端均为degree为$|G|$的多项式，其root正好都是$G$中的元素。

若计算等式右侧看起来需要的计算量与$|G|$呈线性关系，但是，若借助exponentiation by squaring技术，等式左侧的计算running time为logarithmic in $|G|$。

实际，可将Fibonacci composition polynomial的分母重写为：

这样，看起来将占用Verifier大量计算的分母，其实际仅需polylogarithmic time，这仅对“将execution trace看成是某多项式对某域的subgroup进行的evaluation”的情况下才成立，且多项式约束基于该subgroup成立。

类似的小技巧可用于更成熟的execution trace，但是，最重要的是，约束中的重复模型应对于域的某subgroup。

5. More Constraints, More Columns

以上例子都很简单，以说明算术化的关键部分。
一个问题自然出现：
当有多列和多个约束时，该如何处理呢？

答案为：

• 多列：意味着需处理多个多项式
• 多个约束：可派生出多个composition polynomial，然后通过随机线性组合，合并为单个多项式。以用于STARK的最后阶段——低度测试。当且仅当所有元素都成立时，则该线性组合大概率是低度的。

6. 小结

We have shown how, given an execution trace and constraint polynomials, the prover can construct a polynomial which is of low degree if and only if the original CI statement holds. Furthermore, we have shown how the verifier can query the values of this polynomial efficiently, making sure that the prover did not replace the true polynomial with some false low-degree one.

参考资料

[1] Starkware 2019年博客 Arithmetization I
[2] Starkware 2019年博客 Arithmetization II
[3] Starkware Eli Be-Sasson 2019年讲义 STARK Arithmetization