這幾天坊間傳聞 stark 要發幣了!乘著行情還不錯的時候發幣是個非常明智的選擇。
在這裡,想重溫下 stark 的基本技術原理,之前一直斷斷續續有記錄,現在整理下放在這(儘管還是有點亂)
計算完整性#
計算完整性(Computational Integrity),簡單來說就是確保某個計算的輸出是正確的。
第一步: 算術化#
生成執行軌跡#
其中執行軌跡實際上是一個列表,列表的每一行都表示一個計算步驟
將執行軌跡重新表述為多項式
將多項式擴展到一個較大的域
多項式約束#
多項式約束確保當且僅當執行軌跡表示有效計算時,所有的多項式約束都會被滿足
使用多項式約束將其轉換為另一個多項式,使得當且僅當新的多項式的執行軌跡有效時,其為一個低度多項式
Verifier 的工作主要有兩項
- 在一個隨機的位置查詢合成多項式
- 基於這些查詢,檢查多項式是否是低度的
succinctness#
還有一項工作沒有完成,就是 STARK 中的 S,簡潔性,簡潔性由下列兩部分組成
- 只使用少量的查詢
- 對於每次查詢僅完成很少的計算量
查詢時,用於計算多項式的可通過下圖方法減少計算量。利用這個群的特性,我們將執行軌跡視為域上某一子群上的多項式的求值,且求值的多項式約束是關於該子群的,從而使得 Verifier 的驗證時間降低到了對數階,利用這一特性,我們可以構建更為複雜的執行軌跡,但是約束必須與域上的某個子群一致
數學背景知識:
整數模 n 乘法群#
乘法逆元#
群 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
為模:
費馬小定理#
假如 a
是一個整數,p
是一個質數,那麼 a^p-a
是 p
的倍數。
費馬小定理也可以用來求逆元,這是模運算體系下除法運算的基礎。
費馬小定理還有個推論,在模運算空間中,若 p-1
是 k
的倍數,x => x^k
的值空間的大小為 (p-1)/k+1
歐幾里得拓展算法#
歐幾里得算法又叫輾轉相除法,用來求兩個數的最大公約數。對歐幾里得算法進行拓展也可以用來求模運算下的逆元。
蒙哥馬利算法#
當在模運算中有除法時,會先通過逆元將所有的除法轉化為乘法。不過求逆元的操作也很麻煩,當需要求大量逆元時,也很耗時。蒙哥馬利算法通過將多個求逆元的操作轉化為多個乘法以及一次求逆元的操作來簡化計算:
快速傅裡葉變換#
在 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
證明流程:
- 證明者首先需要計算
g(x,y)
每行每列上所有點的值,需要計算10^18
次,並得到其 Merkle Root - 驗證者隨機選出幾十行和幾十列,對於每一行或列,隨機選擇
1010
個點,證明者還需要給出相應的 Merkle 路徑,驗證者驗證 Merkle 路徑以及其度是否小於 1000
可以看到在這種情景下,證明者需要計算 10^18
次,下面考慮如何減少證明者的計算。
前面提到,費馬小定理有個推論,在模運算空間中,若 p-1
是 k
的倍數,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
,可以不斷這樣進行下去。
zk-stark 證明思路
- 程序計算的每一步會對應一個值,所有的步驟組合起來形成一條計算軌跡,也對應一個多項式
P(n)
- 計算軌跡的每一步計算產生一個約束
C(p)=0
- 將軌跡多項式與約束多項式多項式與約束多項式結合起來得到
D(x)=C(p(x),p(x-1)....)
- 組合多項式
D(x)
在計算軌跡的每一步處都為零,即具有根式Z(x)=(x-x_1)(x-x_2)...(x-x_n)
- 使用
FRI
算法對多項式T(x)=D(x)/Z(x)
進行低度檢驗