Allen

Allen

crypto seeker||starknet

stark技术原理及算数化

这几天坊间传闻 stark 要发币了!乘着行情还不错的时候发币是个非常明智的选择。
在这里,想重温下 stark 的基本技术原理,之前一直断断续续有记录,现在整理下放在这(尽管还是有点乱)

计算完整性#

计算完整性(Com­pu­ta­tional In­tegrity),简单来说就是确保某个计算的输出是正确的。

第一步: 算术化#

生成执行轨迹#

其中执行轨迹实际上是一个列表,列表的每一行都表示一个计算步骤

将执行轨迹重新表述为多项式

将多项式扩展到一个较大的域

多项式约束#

多项式约束确保当且仅当执行轨迹表示有效计算时,所有的多项式约束都会被满足

使用多项式约束将其转换为另一个多项式,使得当且仅当新的多项式的执行轨迹有效时,其为一个低度多项式

Ver­i­fier 的工作主要有两项

  1. 在一个随机的位置查询合成多项式
  2. 基于这些查询,检查多项式是否是低度的

succinctness#

还有一项工作没有完成,就是 STARK 中的 S,简洁性,简洁性由下列两部分组成

  1. 只使用少量的查询
  2. 对于每次查询仅完成很少的计算量

查询时,用于计算多项式的可通过下图方法减少计算量。利用这个群的特性,我们将执行轨迹视为域上某一子群上的多项式的求值,且求值的多项式约束是关于该子群的,从而使得 Ver­i­fier 的验证时间降低到了对数阶,利用这一特性,我们可以构建更为复杂的执行轨迹,但是约束必须与域上的某个子群一致

image

数学背景知识:#

整数模 n 乘法群#

image

乘法逆元#

群 G 中任意一个元素 a,都在 G 中有唯一的逆元 a', 具有性质 aa'=a'a=e,其中 e 为群的单位元。

例如:4 关于 1 模 7 的乘法逆元为多少?

4X≡1 mod 7

这个方程等价于求一个 X 和 K,满足

4X=7K+1

其中 X 和 K 都是整数。

若 ax≡1 mod f, 则称 a 关于 1 模 f 的乘法逆元为 x。也可表示为 ax≡1 (mod f)。

当 a 与 f 互素时,a 关于模 f 的乘法逆元有解。如果不互素,则无解。如果 f 为素数,则从 1 到 f-1 的任意数都与 f 互素,即在 1 到 f-1 之间都恰好有一个关于模 f 的乘法逆元。

模运算#

模运算,即求余运算,使得运算发生在有限空间中。通过模运算,数学家们建立起一个新的运算系统,而且这个运算系统与传统数学运算系统是自洽的。我们可以在新的运算系统讨论传统系统里的各种结构,包括称为 “常规数学” 的多项式。而密码学家尤其喜欢这个新的运算系统。

模运算系统中同样有四则运算以及指数运算,不过它的除法运算实现起来比较复杂,一般是先求除数的逆元,将除法转换为乘法进行计算。

实际中,一般以质数 p为模:

image

费马小定理#

假如 a是一个整数,p是一个质数,那么 a^p-ap的倍数。

费马小定理也可以用来求逆元,这是模运算体系下除法运算的基础。

image

ap2则是a关于1p的乘法逆元。a^{p-2} 则是a关于1模p的乘法逆元。

费马小定理还有个推论,在模运算空间中,若 p-1k的倍数,x => x^k的值空间的大小为 (p-1)/k+1

欧几里得拓展算法#

欧几里得算法又叫辗转相除法,用来求两个数的最大公约数。对欧几里得算法进行拓展也可以用来求模运算下的逆元。

蒙哥马利算法#

当在模运算中有除法时,会先通过逆元将所有的除法转化为乘法。不过求逆元的操作也很麻烦,当需要求大量逆元时,也很耗时。蒙哥马利算法通过将多个求逆元的操作转化为多个乘法以及一次求逆元的操作来简化计算:

image

快速傅里叶变换#

zk-stark的计算过程中,有很多需要根据多项式系数求点值,以及根据点值求多项式系数的。使用拉格朗日插值法也可以计算,但其时间复杂度为 O(n^2),而快速傅里叶变化为 O(n*log(n))。例如若需要对100 万个点进行插值,拉格朗日方法需要计算1 万亿次,而快速傅里叶变换只需要2 千万次。不过快速傅里叶变换对取点有要求,需要按等比递增,并且个数满足 2^k

低度测试 —FRI 算法#

多项式的度指的是最高次数。假设已知一个多项式的 n个点,如何证明其度最高为 m呢(m<n-1,根据拉格朗日插值算法,n个点可以决定一个度最高为 n-1的多项式)。一个比较简单的方法是,先使用 m+1个点求出一个 m次多项式,然后验证其它点都在此多项式上。但当 m很大时,这种方法的计算量会线型增加。FRI 算法可以以小于 m次的计算量验证上述问题。

思路如下。假设有 N(比如等于 10 亿)个点,位于一个度小于 m(等于 100 万)的多项式中。假设 f(x)=x^12012+x^11011+x^3005+x^1001+x+1,现在令 y=x^1000代入可得 g(x,y)=x^12*y^12+x^11*y^11+x^5*y^3+x*y+x+1。对于 g(x,y),固定 y不变时,对 x来说,多项式的度小于 1000;同样的,固定 x不变时,对 y来说,多项式的度也是小于 1000

image

证明流程:

  • 证明者首先需要计算 g(x,y)每行每列上所有点的值,需要计算 10^18次,并得到其 Merkle Root
  • 验证者随机选出几十行和几十列,对于每一行或列,随机选择 1010个点,证明者还需要给出相应的 Merkle 路径,验证者验证 Merkle 路径以及其度是否小于 1000

可以看到在这种情景下,证明者需要计算 10^18次,下面考虑如何减少证明者的计算。

前面提到,费马小定理有个推论,在模运算空间中,若 p-1k的倍数,x => x^k的值空间的大小为 (p-1)/k+1,且每个值对应 k个元素。所以事实上,证明者只需要计算 10^9次,对于上图中的某一行,相关的点可以在前面的计算中找到;而且某一行可以插值到指定列,这样就为列上的低度计算准备了数据。

新的证明流程:

  • 证明者计算 f(x)所有点的值,需要计算 10^9次,并得到其 Merkle Root
  • 验证者随机选择一些列,在每一列上随机选择一些点,点的值来源于对应行的插值,而对应行插值的数据源是证明者已经计算的 f(x)的值,同样证明者需要给出所有用到的点的 Merkle 路径

实际计算时,往往取 y=x^4,而 y的低度证明,再次使用 FRI方法,令 z=y^4,可以不断这样进行下去。

image

zk-stark 证明思路#

  1. 程序计算的每一步会对应一个值,所有的步骤组合起来形成一条计算轨迹,也对应一个多项式 P(n)
  2. 计算轨迹的每一步计算产生一个约束 C(p)=0
  3. 将轨迹多项式与约束多项式多项式与约束多项式结合起来得到 D(x)=C(p(x),p(x-1)....)
  4. 组合多项式 D(x)在计算轨迹的每一步处都为零,即具有根式 Z(x)=(x-x_1)(x-x_2)...(x-x_n)
  5. 使用 FRI算法对多项式 T(x)=D(x)/Z(x)进行低度检验
    ji
加载中...
此文章数据所有权由区块链加密技术和智能合约保障仅归创作者所有。