Binius STARKs原理解析及其優化思考

進階1/9/2025, 8:33:21 AM
構建基於二進制域的證明系統時面臨兩個主要挑戰:首先,STARKs中用於表示軌跡的域大小必須大於多項式的度數;其次,用於Merkle樹承諾的域大小也需大於經過Reed-Solomon編碼擴展後的大小。Binius提供了一種創新的解決方案,通過兩種不同的方式來表示相同的數據,從而解決這兩個問題。

1. 引言

與基於橢圓曲線的SNARKs不同,STARKs可以看作是基於哈希的SNARKs。目前STARKs效率低下的一個主要原因是,實際程序中的大部分值相對較小,比如for循環中的索引、布爾值和計數器。然而,為了確保Merkle樹證明的安全性,採用Reed-Solomon編碼對數據進行擴展,這導致了大量冗餘值佔用整個域,儘管原始值很小。為了解決這個效率問題,減少域的大小已成為關鍵策略。

如表1所示,第1代STARKs編碼位寬為252bit,第2代STARKs編碼位寬為64bit,第3代STARKs編碼位寬為32bit,但32bit編碼位寬仍然存在大量的浪費空間。相較而言,二進制域允許直接對位進行操作,編碼緊湊高效而無任意浪費空間,即第4代STARKs。

表 1:STARKs 推導路徑

與近期受到關注的有限域(如Goldilocks、BabyBear和Mersenne31)相比,二進制域的研究可以追溯到1980年代。如今,二進制域在密碼學中被廣泛應用,主要包括以下幾個例子:

  • 基於 𝐹28 域的高級加密標準(AES);
  • 基於 𝐹2128 域的伽羅瓦消息認證碼(GMAC);
  • 使用基於 𝐹28 域的Reed-Solomon編碼的QR碼;
  • 原始的FRI和zk-STARK協議,以及在SHA-3競賽中成為決賽選手的Grøstl哈希函數,該函數基於 𝐹28 域,適合遞歸哈希算法。

在使用較小的域時,域擴展操作對確保安全性變得尤為重要。Binius所採用的二進制域完全依賴於域擴展,以保證安全性和實用性。大多數與Prover操作相關的多項式計算無需進入擴展域,只需在基域中進行操作,從而在小域中實現高效率。然而,隨機點檢查和FRI計算仍需在更大的擴展域中進行,以確保必要的安全級別。

在基於二進制域構建證明系統時,有兩個實際挑戰:首先,STARKs中用於軌跡表示的域大小必須大於多項式的度數;其次,STARKs中用於Merkle樹承諾的域大小需大於經過Reed-Solomon編碼擴展後的大小。

Binius通過兩種不同的方式來解決這兩個問題,提供了一種創新的解決方案:首先,使用多變量(特別是多線性)多項式代替單變量多項式,通過在“超立方體”上的評估來表示整個計算軌跡;其次,由於超立方體的每個維度長度為2,無法像STARKs那樣進行標準的Reed-Solomon擴展,但可以將超立方體視為一個正方形,並基於這個正方形進行Reed-Solomon擴展。這種方法不僅確保了安全性,還大幅提升了編碼效率和計算性能。

2. Binius原理

現代大多數SNARK系統的構建通常包含兩個主要組件:

  • 信息論多項式交互式神諭證明(PIOP):作為證明系統的核心,PIOP將輸入的計算關係轉換為可驗證的多項式方程。不同的PIOP協議允許證明者通過與驗證者的交互逐步發送多項式,使驗證者能夠通過查詢少量多項式評估來確認計算的正確性。各種PIOP協議(如PLONK PIOP、Spartan PIOP和HyperPlonk PIOP)以不同的方式處理多項式表達式,從而影響SNARK系統的整體性能和效率。
  • 多項式承諾方案(PCS):PCS是一種加密工具,用於證明由PIOP生成的多項式方程是有效的。它允許證明者承諾一個多項式並驗證其評估,而不需要透露多項式的其他信息。常見的PCS方案包括KZG、Bulletproofs、FRI(快速Reed-Solomon IOPP)和Brakedown,每種方案都有其獨特的性能特點、安全保障和適用場景。

通過選擇不同的PIOP和PCS方案,並將它們與適當的有限域或橢圓曲線結合,可以構建具有不同特性的證明系統。例如:

  • Halo2:結合PLONK PIOP與Bulletproofs PCS,並在Pasta曲線上運行,旨在提高可擴展性,並消除了ZCash協議中使用的可信設置。
  • Plonky2:結合PLONK PIOP與FRI PCS,基於Goldilocks域,優化了高效遞歸。

在設計這些系統時,所選PIOP、PCS與有限域或橢圓曲線之間的兼容性對於確保系統的正確性、性能和安全性至關重要。這些組合會影響SNARK證明的大小、驗證效率,並決定系統是否能夠在沒有可信設置的情況下實現透明性,以及是否支持遞歸證明或證明聚合等高級功能。

Binius結合了HyperPlonk PIOP與Brakedown PCS,並在二進制域中運作。具體來說,Binius結合了五項關鍵技術,以實現效率和安全性:

  1. 基於二進制域塔的算術,形成Binius的計算基礎,簡化了在二進制域內的操作;
  2. HyperPlonk乘積和置換檢查,確保變量及其置換之間的安全和高效一致性;
  3. 新的多線性移位論證,提升了在小域內驗證多線性關係的效率;
  4. 改進的Lasso查找論證,引入了更靈活和安全的查找機制;
  5. 針對小域量身定製的小域多項式承諾方案(PCS),減少了與較大域相關的開銷,從而在二進制域中實現高效的證明系統。

這些創新使Binius能夠提供一個緊湊且高性能的SNARK系統,專為二進制域優化,同時保持強大的安全性和可擴展性。

2.1 有限域:基於塔式二進制域的算術

塔式二進制域是實現快速可驗證計算的關鍵,主要歸因於兩個方面:高效計算和高效算術化。二進制域本質上支持高度高效的算術操作,使其成為對性能要求敏感的密碼學應用的理想選擇。此外,二進制域結構支持簡化的算術化過程,即在二進制域上執行的運算可以以緊湊且易於驗證的代數形式表示。這些特性,加上能夠通過塔結構充分利用其層次化的特性,使得二進制域特別適合於諸如Binius這樣可擴展的證明系統。

  1. 其中“canonical”是指在二進制域中元素的唯一且直接的表示方式。
  2. 例如,在最基本的二進制域F2中,任意k位的字符串都可以直接映射到一個k位的二進制域元素。這與素數域不同,素數域無法在給定位數內提供這種規範的表示。儘管32位的素數域可以包含在32位中,但並非每個32位的字符串都能唯一地對應一個域元素,而二進制域則具備這種一對一映射的便利性。在素數域Fp中,常見的歸約方法包括Barrett歸約、Montgomery歸約,以及針對Mersenne-31或Goldilocks-64等特定有限域的特殊歸約方法。在二進制域F2k中,常用的歸約方法包括特殊歸約(如AES中使用)、Montgomery歸約(如POLYVAL中使用)和遞歸歸約(如Tower)。論文《 Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations》指出,二進制域在加法和乘法運算中均無需引入進位,且二進制域的平方運算非常高效,因為它遵循(𝑋+𝑌)2=𝑋2+𝑌2的簡化規則。

圖 1: 塔式二進制域

如圖1所示,一個128位字符串:該字符串可以在二進制域的上下文中以多種方式進行解釋。它可以被視為128位二進制域中的一個獨特元素,或者被解析為兩個64位塔域元素、四個32位塔域元素、16個8位塔域元素,或128個F2域元素。

這種表示的靈活性不需要任何計算開銷,只是對位字符串的類型轉換(typecast),是一個非常有趣且有用的屬性。同時,小域元素可以被打包為更大的域元素而不需要額外的計算開銷。

Binius協議利用了這一特性,以提高計算效率。此外,論文《On Efficient Inversion in Tower Fields of Characteristic Two》探討了在n位塔式二進制域中(可分解為m位子域)進行乘法、平方和求逆運算的計算複雜度。

2.2 PIOP:改編版HyperPlonk Product PermutationCheck——適用於二進制域

Binius協議中的PIOP設計借鑑了HyperPlonk,採用了一系列核心檢查機制,用於驗證多項式和多變量集合的正確性。這些核心檢查包括:

  1. GateCheck:驗證保密見證ω和公開輸入x是否滿足電路運算關係C(x,ω)=0,以確保電路正確運行。
  2. PermutationCheck:驗證兩個多變量多項式f和g在布爾超立方體上的求值結果是否為置換關係f(x) = f(π(x)),以確保多項式變量之間的排列一致性。
  3. LookupCheck:驗證多項式的求值是否在給定的查找表中,即f(Bµ) ⊆ T(Bµ),確保某些值在指定範圍內。
  4. MultisetCheck:檢查兩個多變量集合是否相等,即{(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H,保證多個集合間的一致性。
  5. ProductCheck:檢測有理多項式在布爾超立方體上的求值是否等於某個聲明的值∏x∈Hµ f(x) = s,以確保多項式乘積的正確性。
  6. ZeroCheck:驗證一個多變量多項式在布爾超立方體上的任意點是否為零∏x∈Hµ f(x) = 0,∀x ∈ Bµ,以確保多項式的零點分佈。
  7. SumCheck:檢測多變量多項式的求和值是否為聲明的值∑x∈Hµ f(x) = s。通過將多元多項式的求值問題轉化為單變量多項式求值,降低驗證方的計算複雜度。此外,SumCheck還允許批處理,通過引入隨機數,構造線性組合實現對多個和校驗實例的批處理。
  8. BatchCheck:基於SumCheck,驗證多個多變量多項式求值的正確性,以提高協議效率。

儘管Binius與HyperPlonk在協議設計上有許多相似之處,但Binius在以下3個方面做出改進:

  1. ProductCheck優化:在HyperPlonk中,ProductCheck要求分母U在超立方體上處處非零,且乘積必須等於一個特定值;Binius通過將該值特化為1,簡化這一檢查過程,從而降低計算複雜度。
  2. 除零問題的處理:HyperPlonk未能充分處理除零情況,導致無法斷言U在超立方體上的非零問題;Binius正確地處理了這一問題,即使在分母為零的情況下,Binius的ProductCheck也能繼續處理,允許推廣到任意乘積值。
  3. 跨列PermutationCheck:HyperPlonk無此功能;Binius支持在多個列之間進行PermutationCheck,這使得Binius能夠處理更復雜的多項式排列情況。

因此,Binius通過對現有PIOPSumCheck機制的改進,提升了協議的靈活性和效率,尤其在處理更復雜的多變量多項式驗證時,提供了更強的功能支持。這些改進不僅解決了HyperPlonk中的侷限性,還為未來基於二進制域的證明系統奠定了基礎。

2.3 PIOP:新的 multilinear shift argument——適用於 boolean hypercube

在Binius協議中,虛擬多項式的構造和處理是關鍵技術之一,能夠有效地生成和操作從輸入句柄或其他虛擬多項式派生出的多項式。以下是兩個關鍵方法:

  • Packing:該方法通過將詞典序中相鄰位置的較小元素打包成更大的元素來優化操作。Pack運算符針對大小為2κ的塊操作,並將它們組合成高維域中的單個元素。通過多線性擴展(Multilinear Extension, MLE),這個虛擬多項式可以高效地評估和處理,將函數t轉換為另一個多項式,從而提高了計算性能。
  • 移位運算符:移位運算符重新排列塊內的元素,基於給定偏移量o進行循環移位。該方法適用於大小為2b的塊,每個塊根據偏移量執行移位。移位運算符通過檢測函數的支持來進行定義,確保在處理虛擬多項式時保持一致性和效率。評估該構造的複雜度隨塊大小線性增長,特別適用於處理大數據集或布爾超立方體中的高維場景。

2.4 PIOP:改編版Lasso lookup argument——適用於二進制域

Lasso協議允許證明方承諾一個向量a ∈ Fm,並證明其所有元素均存在於一個預先指定的表t ∈ Fn 中。Lasso解鎖了“查找奇點”(lookup singularities)的概念,並能適用於多線性多項式承諾方案。其效率體現在以下兩個方面:

  • 證明效率:對於大小為n的表中的m次查找,證明方只需承諾m+n個域元素。這些域元素很小,均位於集合{0,…,m}中。在基於多次冪運算的承諾方案中,證明方的計算成本為O(m + n)次群運算(如橢圓曲線點加),外加證明多線性多項式在布爾超立方體上是否為表元素的求值成本。
  • 無需承諾大表:如果表t是結構化的,則無需對其進行承諾,因此可以處理超大表(如2128或更大)。證明方的運行時間僅與訪問的表條目相關。對於任意整數參數c > 1,證明方的主要成本是證明大小,承諾的域元素為 3·c m + c·n1/c 個。這些域元素都是較小的,位於集合{0,…,max{m,n1/c,q} − 1} 中,其中q為a中的最大值。

Lasso協議由以下三個組件構成:

  1. 大表的虛擬多項式抽象:通過將虛擬多項式組合,實現在大表上的操作,確保在表內進行高效的查找和處理。
  2. 小表查找:Lasso的核心是小表查找,作為虛擬多項式協議的核心構建,使用離線內存檢測驗證一個虛擬多項式在布爾超立方體上的求值是否是另一個虛擬多項式求值的子集。這一查找過程將歸約為多集合檢測的任務。
  3. 多集合檢查:Lasso引入虛擬協議來執行多集合檢查,驗證兩個集合的元素是否相等或滿足特定條件。

Binius協議將Lasso適應於二進制域的操作,假設當前域是一個大特徵的素數域(遠大於被查找列的長度)。Binius引入了乘法版本的Lasso協議,要求證明方和驗證方聯合遞增協議的“內存計數”操作,不是通過簡單的加1遞增,而是通過二進制域中的乘法生成元來遞增。然而,這一乘法改編引入了更多的複雜性,與遞增操作不同,乘法生成元並非在所有情況下遞增,在0處存在單一軌道,這可能成為攻擊點。為防止這種潛在的攻擊,證明方必須承諾一個處處非零的讀取計數向量,以確保協議的安全性。

2.5 PCS:改編版Brakedown PCS——適用於Small-Field

構建BiniusPCS的核心思想是packing。Binius論文中提供了2種基於二進制域的Brakedown多項式承諾方案:一種是採用concatenated code來實例化;另一種採用block-level encoding技術,支持單獨使用Reed-Solomon codes。第二種Brakedown PCS方案,簡化了證明和驗證流程,但proof size要比第一種略大一點,但所帶來的簡化和實現優勢,做該取捨是值得的。

Binius多項式承諾主要使用小域多項式承諾與擴展域評估、小域通用構造和塊級編碼與Reed-Solomon碼技術。

小域多項式承諾與擴展域評估:Binius協議中的承諾是在小域K上的多項式承諾,並在更大的擴展域L/K中進行評估。這種方法確保了每個多線性多項式t(X0,…,Xℓ−1)屬於域K[X0,…,Xℓ−1],而評估點可以位於更大擴展域L中。承諾方案專門設計用於小域多項式,並能在擴展域上進行查詢,同時保證承諾的安全性和效率。

小域通用構造:小域通用構造通過定義參數ℓ、域K及其相關的線性塊碼C,確保擴展域L足夠大,以支持安全評估。為了在保持計算效率的同時提高安全性,協議通過擴展域的特性,以及採用線性塊碼對多項式進行編碼,保證了承諾的穩健性。

塊級編碼與Reed-Solomon碼:針對字段比線性塊碼字母表更小的多項式,Binius提出了塊級編碼方案。通過這一方案,即使在小域(如F2)中定義的多項式,也可以使用如F216這樣的大字母表的Reed-Solomon碼高效承諾。Reed-Solomon碼之所以被選中,是因為它具有高效性和最大距離分離特性。該方案通過將消息打包並逐行編碼,之後利用Merkle樹進行承諾,簡化了操作複雜度。塊級編碼允許小域多項式的高效承諾,而不會產生通常與大域相關的高計算開銷,從而使得在F2等小域中承諾多項式成為可能,並在生成證明與驗證中保持計算效率。

3. Binius優化

為了進一步提升Binius協議的性能,本文提出了四個關鍵優化點:

  1. GKR-based PIOP:針對二進制域乘法運算,藉助GKR協議,來替換Binius論文中的的Lasso Lookup算法,可大幅降低Binius的承諾開銷;
  2. ZeroCheck PIOP優化:在Prover與Verifier之間進行計算開銷權衡,使得ZeroCheck操作更加高效;
  3. Sumcheck PIOP優化:針對小域Sumcheck的優化,進一步減少了小域上的計算負擔;
  4. PCS 優化:通過FRI-Binius優化,降低證明大小,提高協議的整體性能。

3.1 GKR-based PIOP:基於GKR的二進制域乘法

Binius論文引入一種基於lookup的方案,旨在實現高效的二進制域乘法運算。通過Lasso lookup argument 改編的二進制域乘法算法依賴於lookups和加法操作的線性關係,這些操作與單個word中的limbs數量成比例。雖然這一算法在某種程度上優化了乘法操作,但仍需要與limbs數量線性相關的輔助承諾。

GKR(Goldwasser-Kalai-Rothblum)協議中的核心思想是,證明方(P)和驗證方(V)針對一個有限域F上的layered算術電路達成一致。該電路的每個節點有兩個輸入,用於計算所需的函數。為了減少驗證方的計算複雜度,協議使用SumCheck協議,將關於電路輸出門值的聲明逐步簡化為更低層的門值聲明,直至最終將聲明簡化到關於輸入的陳述。這樣,驗證方只需檢查電路輸入的正確性即可。

基於GKR的整數乘法運算算法,通過將“檢查2個32-bit整數A和B是否滿足 A·B =? C”,轉換為“檢查中(gA)B =? gC 是否成立”,藉助GKR協議大幅減少承諾開銷。與之前的Binius lookup方案相比,基於GKR的二進制域乘法運算只需一個輔助承諾,並且通過減少Sumchecks的開銷,使該算法更加高效,特別是在Sumchecks操作比承諾生成更便宜的場景下。隨著Binius優化的推進,基於GKR的乘法運算逐漸成為減少二進制域多項式承諾開銷的有效途徑。

3.2 ZeroCheck PIOP優化:Prover與Verifier計算開銷權衡

論文《Some Improvements for the PIOP for ZeroCheck》在證明方(P)和驗證方(V)之間調整工作量的分配,提出了多種優化方案,以權衡開銷。該工作探索了不同的k值配置,使得在證明方和驗證方之間達成了成本的權衡,特別是在減少傳輸數據和降低計算複雜性方面。

減少證明方的數據傳輸:通過將一部分工作轉移給驗證方V,從而降低證明方P發送的數據量。在第i輪中,證明方P需要向驗證方V發送vi+1(X),其中X=0,…,d + 1。驗證方V檢查以下等式以驗證數據的正確性:

vi = vi+1(0) + vi+1(1).

優化方法:證明方P可以選擇不發送vi+1(1),而是讓驗證方V自行通過以下方式計算出該值

vi+1(1) = vi − vi+1(0).

此外,在第0輪,誠實的證明方P始終發送v1(0) = v1(1) = 0,這意味著無需進行任何評估計算,從而顯著減少了計算和傳輸成本,降低至d2n−1CF + (d + 1)2n−1CG。

減少證明方評估點的數量:在協議的第i輪中,驗證者在之前的i輪中已經發送了一個值序列r =(r0,…,ri−1)。當前協議要求證明者 (P) 發送多項式

vi+1(X) = ∑ δˆn(α,(r,X,x))C(r,X,x).x∈H −−1

優化方法:證明方P發送以下多項式這兩個函數之間的關係是:

vi(X) = vi′(X)·δi+1((α0,…,αi),(r,X))

其中δˆi+1因為驗證者擁有α和r,所以是完全已知的。這個修改的好處在於vi′(X)的次數比vi(X)少1,這意味著證明者需要評估的點更少。因此,主要的協議變化發生在輪次之間的檢查環節。

此外,將原本的約束vi = vi+1(0)+vi+1(1) 優化為 (1−αi)vi′+1(0)+αivi′+1(1) = vi′(X)。則證明者需要評估和發送的數據更少,進一步減少傳輸的數據量。計算δˆn−i−1也比計算δˆn更高效。通過這兩項改進,成本降低為大約:2n−1(d− 1)CF + 2n−1dCG。在常見的d=3情況下,這些優化使成本降低了5/3倍。

代數插值優化:對於誠實的證明者,C(x0,…,xn−1)在Hn上為零,可表示為:C(x0,…,xn-1)= ∑xi(xi-1)Qi(x0,…,xn-1)。雖然Qi不是唯一的,但可以通過多項式長除法構造一個有序的分解:從Rn=C開始,逐次除以xi(xi−1)來計算Qi和Ri,其中R0是C在Hn上的多線性擴展,且假設其為零。分析Qi的次數,可以得出:對於j> i,Qj 在 xi 上的次數與 C 相同;對於 j = i,次數減少 2;對於 j i,次數至多為 1。給定向量 r = (r0,…,ri),Qj(r,X) 對於所有 j ≤ i 都是多線性的。此外1)Qj(r,X) 是與 C(r,X) 在 Hn−i 上相等的唯一多線性多項式。對於任何 X 和 x ∈ Hn−i−1,可以表示為:

C(r,X,x) − Qi(r,X,x) = X(X − 1)Qi+1(r,X,x)

因此,在協議的每一輪中,僅引入一個新的Q,其評估值可以從C和先前的Q計算得出,實現插值優化。

3.3 PIOP優化:基於小域的Sumcheck協議

Binius所實現的STARKs方案,其承諾開銷很低,使得prover瓶頸不再是PCS,而在於sum-check協議。

圖 2. 切換輪次與因子改進之間的關係

Ingonyama在2024年提出了針對基於小域的Sumcheck協議的改進方案(對應圖2中的Algo3和Algo4算法),並開源了實現代碼。算法4專注於將Karatsub算法合併到算法3中,以額外的基域乘法為代價來最小化擴域乘法次數,因此當擴域乘法比基域乘法昂貴得多時,算法4的性能會更好。

  • 切換輪次的影響與改進因子

基於小域的Sumcheck協議的改進集中於切換輪次t的選擇。切換輪次是指從優化算法切換回樸素算法的時間點,論文的實驗表明,在最佳切換點時,改進因子達到最大值,隨後呈現拋物線趨勢。如果超過這一切換點,優化算法的性能優勢減弱,效率下降。這是由於小域上的基域乘法與擴域乘法相比有更高的時間比率,因此在適當時機切換回樸素算法至關重要。

對於具體應用,如涉及Cubic Sumcheck(d = 3)的情況,基於小域的Sumcheck協議相較於樸素算法的改進達到了一個數量級。例如,在基域為GF[2]的情況下,算法4的性能比樸素算法高出近30倍。

  • 基域大小對性能的影響

論文的實驗結果表明,較小的基域(如GF[2])能夠使優化算法顯示出更顯著的優勢。這是因為擴展域與基域乘法的時間比率在較小基域上更高,從而優化算法在此條件下表現出更高的改進因子。

  • Karatsuba算法的優化收益

Karatsuba算法在提升基於小域的Sumcheck性能方面表現出顯著的效果。對於基域GF[2],算法3和算法4的峰值改進因子分別為6和30,表明算法4比算法3高效五倍。Karatsuba優化不僅提升了運行效率,也優化了算法的切換點,分別在算法3的t=5和算法4的t=8達到最佳。

  • 內存效率的提升

基於小域的Sumcheck協議除了提升運行時間,還在內存效率方面表現出顯著的優勢。算法4的內存需求為O(d·t),而算法3的內存需求為O(2d·t)。當t=8時,算法4僅需0.26MB的內存,而算法3則需67MB來存儲基域的乘積。這使得算法4在內存受限設備上表現出更強的適應性,尤其適用於資源有限的客戶端證明環境。

3.4 PCS 優化:FRI-Binius降低Binius proof size

Binius協議的一個主要缺陷在於其相對較大的證明大小,隨著見證大小的平方根按O(√N)縮放。與更高效的系統相比,這種平方根大小的證明是一種侷限性。相反,對數級(polylogarithmic)證明大小對於實現真正“簡潔”的驗證器至關重要,這在像Plonky3這樣的先進系統中得到了驗證,後者通過FRI等先進技術實現了對數級證明。

論文《Polylogarithmic Proofs for Multilinears over Binary Towers》,簡稱為FRI-Binius,實現了二進制域FRI摺疊機制,帶來4個方面的創新:

  • 扁平化多項式:初始的多線性多項式被轉換為LCH(低碼高度)新穎多項式基。
  • 子空間消失多項式:用於在係數域上執行FRI,並通過加性NTT(數論變換)實現類似FFT的分解。
  • 代數基打包:支持協議中信息的高效打包,可移除嵌入開銷。
  • 環交換SumCheck:一種新穎的SumCheck方法,利用環交換技術優化性能。

基於二進制域FRI-Binius的多線性多項式承諾方案(PCS)的核心思想為:FRI-Binius協議通過將初始的二進制域多線性多項式(定義於F2上)打包為定義在更大域K上的多線性多項式來操作。

在基於二進制域的FRI-BiniusPCS中,過程如下:

  1. 承諾階段:對一個ℓ變量的多線性多項式(定義於F2上)的承諾被轉化為對一個打包後的ℓ′變量的多線性多項式(定義於F2128上)的承諾,係數個數因此減少了128倍。
  2. 評估階段:證明方和驗證方進行ℓ′輪交叉環切換SumCheck和FRI交互證明(IOPP):
    • –FRI開放證明佔據了證明大小的大部分。
    • –證明方的SumCheck成本類似於常規大域上的SumCheck成本。
    • –證明方的FRI成本與常規大域上的FRI成本相同。
    • –驗證方接收128個來自F2128的元素,並執行128個額外的乘法運算。

藉助FRI-Binius,可將Binius證明大小減少一個數量級。這使得Binius的證明大小更加接近最先進的系統,同時保持與二進制域的兼容性。專為二進制域定製的FRI摺疊技術,加上代數打包和SumCheck的優化,使得Binius能夠在保持高效驗證的同時,生成更加簡潔的證明。


表 2:Binius 與 FRI-Binius 證明大小比較


表 3:Plonky3 FRI 與 FRI-Binius 比較

4. 結論

Binius的整個價值主張是,可為witnesses使用最小的power-of-two域,因此只需根據所需來選擇域大小。Binius是“使用硬件、軟件、與FPGA中加速的Sumcheck協議”的協同設計方案,可以以非常低的內存使用率來快速證明。Halo2和Plonky3等證明系統有4個佔用大部分計算量的關鍵步驟:生成witness數據、對witness數據進行承諾、vanishingargument、openingproof。以Plonky3中的Keccak和Binius中的Grøstl哈希函數為例,二者對應的以上4大關鍵步驟計算量佔比情況如圖3所示:

圖 3. 較小的承諾成本

由此可知,Binius中已基本完全移除了Prover的commit承諾瓶頸,新的瓶頸在於Sumcheck協議,而Sumcheck協議中大量多項式evaluations和域乘法等問題,可藉助專用硬件高效解決。FRI-Binius方案,為FRI變體,可提供一個非常有吸引力的選擇——從域證明層中消除嵌入開銷,而不會導致聚合證明層的成本激增。當前,Irreducible團隊正在開發其遞歸層,並 宣佈與Polygon團隊合作構建Binius-based zkVM; JoltzkVM正從Lasso轉向Binius,以改進其遞歸性能;以及 Ingonyama團隊正在實現FPGA版本的Binius.

參考文獻

  1. 2024.04 Binius Succinct Arguments over Towers of Binary Fields
  2. 2024.07 Fri-Binius Polylogarithmic Proofs for Multilinears over Binary Towers
  3. 2024.08 Integer Multiplication in Binius: GKR-based approach
  4. 2024.06 zkStudyClub - FRI-Binius: Polylogarithmic Proofs for Multilinears over Binary Towers
  5. 2024.04 ZK11: Binius: a Hardware-Optimized SNARK - Jim Posen
  6. 2023.12 Episode 303: A Dive into Binius with Ulvetanna
  7. 2024.09 Designing high-performance zkVMs
  8. 2024.07 Sumcheck and Open-Binius
  9. 2024.04 Binius: highly efficient proofs over binary fields
  10. 2023.12 SNARKs on binary fields: Binius - Part 1
  11. 2024.06 SNARKs on binary fields: Binius - Part 2
  12. @espressosys/hyperplonk-a-zk-proof-system-for-zkevms-d45fd077bfba”>2022.10 HyperPlonk, a zk-proof system for ZKEVMs

聲明:

  1. 本文轉載自【bitlayer】,著作權歸屬原作者【lynndell】,如對轉載有異議,請聯繫 Gate Learn 團隊,團隊會根據相關流程儘速處理。
  2. 免責聲明:本文所表達的觀點和意見僅代表作者個人觀點,不構成任何投資建議。
  3. 文章其他語言版本由 Gate Learn 團隊翻譯,除非另有說明,否則禁止複製、傳播或抄襲經翻譯文章。

Binius STARKs原理解析及其優化思考

進階1/9/2025, 8:33:21 AM
構建基於二進制域的證明系統時面臨兩個主要挑戰:首先,STARKs中用於表示軌跡的域大小必須大於多項式的度數;其次,用於Merkle樹承諾的域大小也需大於經過Reed-Solomon編碼擴展後的大小。Binius提供了一種創新的解決方案,通過兩種不同的方式來表示相同的數據,從而解決這兩個問題。

1. 引言

與基於橢圓曲線的SNARKs不同,STARKs可以看作是基於哈希的SNARKs。目前STARKs效率低下的一個主要原因是,實際程序中的大部分值相對較小,比如for循環中的索引、布爾值和計數器。然而,為了確保Merkle樹證明的安全性,採用Reed-Solomon編碼對數據進行擴展,這導致了大量冗餘值佔用整個域,儘管原始值很小。為了解決這個效率問題,減少域的大小已成為關鍵策略。

如表1所示,第1代STARKs編碼位寬為252bit,第2代STARKs編碼位寬為64bit,第3代STARKs編碼位寬為32bit,但32bit編碼位寬仍然存在大量的浪費空間。相較而言,二進制域允許直接對位進行操作,編碼緊湊高效而無任意浪費空間,即第4代STARKs。

表 1:STARKs 推導路徑

與近期受到關注的有限域(如Goldilocks、BabyBear和Mersenne31)相比,二進制域的研究可以追溯到1980年代。如今,二進制域在密碼學中被廣泛應用,主要包括以下幾個例子:

  • 基於 𝐹28 域的高級加密標準(AES);
  • 基於 𝐹2128 域的伽羅瓦消息認證碼(GMAC);
  • 使用基於 𝐹28 域的Reed-Solomon編碼的QR碼;
  • 原始的FRI和zk-STARK協議,以及在SHA-3競賽中成為決賽選手的Grøstl哈希函數,該函數基於 𝐹28 域,適合遞歸哈希算法。

在使用較小的域時,域擴展操作對確保安全性變得尤為重要。Binius所採用的二進制域完全依賴於域擴展,以保證安全性和實用性。大多數與Prover操作相關的多項式計算無需進入擴展域,只需在基域中進行操作,從而在小域中實現高效率。然而,隨機點檢查和FRI計算仍需在更大的擴展域中進行,以確保必要的安全級別。

在基於二進制域構建證明系統時,有兩個實際挑戰:首先,STARKs中用於軌跡表示的域大小必須大於多項式的度數;其次,STARKs中用於Merkle樹承諾的域大小需大於經過Reed-Solomon編碼擴展後的大小。

Binius通過兩種不同的方式來解決這兩個問題,提供了一種創新的解決方案:首先,使用多變量(特別是多線性)多項式代替單變量多項式,通過在“超立方體”上的評估來表示整個計算軌跡;其次,由於超立方體的每個維度長度為2,無法像STARKs那樣進行標準的Reed-Solomon擴展,但可以將超立方體視為一個正方形,並基於這個正方形進行Reed-Solomon擴展。這種方法不僅確保了安全性,還大幅提升了編碼效率和計算性能。

2. Binius原理

現代大多數SNARK系統的構建通常包含兩個主要組件:

  • 信息論多項式交互式神諭證明(PIOP):作為證明系統的核心,PIOP將輸入的計算關係轉換為可驗證的多項式方程。不同的PIOP協議允許證明者通過與驗證者的交互逐步發送多項式,使驗證者能夠通過查詢少量多項式評估來確認計算的正確性。各種PIOP協議(如PLONK PIOP、Spartan PIOP和HyperPlonk PIOP)以不同的方式處理多項式表達式,從而影響SNARK系統的整體性能和效率。
  • 多項式承諾方案(PCS):PCS是一種加密工具,用於證明由PIOP生成的多項式方程是有效的。它允許證明者承諾一個多項式並驗證其評估,而不需要透露多項式的其他信息。常見的PCS方案包括KZG、Bulletproofs、FRI(快速Reed-Solomon IOPP)和Brakedown,每種方案都有其獨特的性能特點、安全保障和適用場景。

通過選擇不同的PIOP和PCS方案,並將它們與適當的有限域或橢圓曲線結合,可以構建具有不同特性的證明系統。例如:

  • Halo2:結合PLONK PIOP與Bulletproofs PCS,並在Pasta曲線上運行,旨在提高可擴展性,並消除了ZCash協議中使用的可信設置。
  • Plonky2:結合PLONK PIOP與FRI PCS,基於Goldilocks域,優化了高效遞歸。

在設計這些系統時,所選PIOP、PCS與有限域或橢圓曲線之間的兼容性對於確保系統的正確性、性能和安全性至關重要。這些組合會影響SNARK證明的大小、驗證效率,並決定系統是否能夠在沒有可信設置的情況下實現透明性,以及是否支持遞歸證明或證明聚合等高級功能。

Binius結合了HyperPlonk PIOP與Brakedown PCS,並在二進制域中運作。具體來說,Binius結合了五項關鍵技術,以實現效率和安全性:

  1. 基於二進制域塔的算術,形成Binius的計算基礎,簡化了在二進制域內的操作;
  2. HyperPlonk乘積和置換檢查,確保變量及其置換之間的安全和高效一致性;
  3. 新的多線性移位論證,提升了在小域內驗證多線性關係的效率;
  4. 改進的Lasso查找論證,引入了更靈活和安全的查找機制;
  5. 針對小域量身定製的小域多項式承諾方案(PCS),減少了與較大域相關的開銷,從而在二進制域中實現高效的證明系統。

這些創新使Binius能夠提供一個緊湊且高性能的SNARK系統,專為二進制域優化,同時保持強大的安全性和可擴展性。

2.1 有限域:基於塔式二進制域的算術

塔式二進制域是實現快速可驗證計算的關鍵,主要歸因於兩個方面:高效計算和高效算術化。二進制域本質上支持高度高效的算術操作,使其成為對性能要求敏感的密碼學應用的理想選擇。此外,二進制域結構支持簡化的算術化過程,即在二進制域上執行的運算可以以緊湊且易於驗證的代數形式表示。這些特性,加上能夠通過塔結構充分利用其層次化的特性,使得二進制域特別適合於諸如Binius這樣可擴展的證明系統。

  1. 其中“canonical”是指在二進制域中元素的唯一且直接的表示方式。
  2. 例如,在最基本的二進制域F2中,任意k位的字符串都可以直接映射到一個k位的二進制域元素。這與素數域不同,素數域無法在給定位數內提供這種規範的表示。儘管32位的素數域可以包含在32位中,但並非每個32位的字符串都能唯一地對應一個域元素,而二進制域則具備這種一對一映射的便利性。在素數域Fp中,常見的歸約方法包括Barrett歸約、Montgomery歸約,以及針對Mersenne-31或Goldilocks-64等特定有限域的特殊歸約方法。在二進制域F2k中,常用的歸約方法包括特殊歸約(如AES中使用)、Montgomery歸約(如POLYVAL中使用)和遞歸歸約(如Tower)。論文《 Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations》指出,二進制域在加法和乘法運算中均無需引入進位,且二進制域的平方運算非常高效,因為它遵循(𝑋+𝑌)2=𝑋2+𝑌2的簡化規則。

圖 1: 塔式二進制域

如圖1所示,一個128位字符串:該字符串可以在二進制域的上下文中以多種方式進行解釋。它可以被視為128位二進制域中的一個獨特元素,或者被解析為兩個64位塔域元素、四個32位塔域元素、16個8位塔域元素,或128個F2域元素。

這種表示的靈活性不需要任何計算開銷,只是對位字符串的類型轉換(typecast),是一個非常有趣且有用的屬性。同時,小域元素可以被打包為更大的域元素而不需要額外的計算開銷。

Binius協議利用了這一特性,以提高計算效率。此外,論文《On Efficient Inversion in Tower Fields of Characteristic Two》探討了在n位塔式二進制域中(可分解為m位子域)進行乘法、平方和求逆運算的計算複雜度。

2.2 PIOP:改編版HyperPlonk Product PermutationCheck——適用於二進制域

Binius協議中的PIOP設計借鑑了HyperPlonk,採用了一系列核心檢查機制,用於驗證多項式和多變量集合的正確性。這些核心檢查包括:

  1. GateCheck:驗證保密見證ω和公開輸入x是否滿足電路運算關係C(x,ω)=0,以確保電路正確運行。
  2. PermutationCheck:驗證兩個多變量多項式f和g在布爾超立方體上的求值結果是否為置換關係f(x) = f(π(x)),以確保多項式變量之間的排列一致性。
  3. LookupCheck:驗證多項式的求值是否在給定的查找表中,即f(Bµ) ⊆ T(Bµ),確保某些值在指定範圍內。
  4. MultisetCheck:檢查兩個多變量集合是否相等,即{(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H,保證多個集合間的一致性。
  5. ProductCheck:檢測有理多項式在布爾超立方體上的求值是否等於某個聲明的值∏x∈Hµ f(x) = s,以確保多項式乘積的正確性。
  6. ZeroCheck:驗證一個多變量多項式在布爾超立方體上的任意點是否為零∏x∈Hµ f(x) = 0,∀x ∈ Bµ,以確保多項式的零點分佈。
  7. SumCheck:檢測多變量多項式的求和值是否為聲明的值∑x∈Hµ f(x) = s。通過將多元多項式的求值問題轉化為單變量多項式求值,降低驗證方的計算複雜度。此外,SumCheck還允許批處理,通過引入隨機數,構造線性組合實現對多個和校驗實例的批處理。
  8. BatchCheck:基於SumCheck,驗證多個多變量多項式求值的正確性,以提高協議效率。

儘管Binius與HyperPlonk在協議設計上有許多相似之處,但Binius在以下3個方面做出改進:

  1. ProductCheck優化:在HyperPlonk中,ProductCheck要求分母U在超立方體上處處非零,且乘積必須等於一個特定值;Binius通過將該值特化為1,簡化這一檢查過程,從而降低計算複雜度。
  2. 除零問題的處理:HyperPlonk未能充分處理除零情況,導致無法斷言U在超立方體上的非零問題;Binius正確地處理了這一問題,即使在分母為零的情況下,Binius的ProductCheck也能繼續處理,允許推廣到任意乘積值。
  3. 跨列PermutationCheck:HyperPlonk無此功能;Binius支持在多個列之間進行PermutationCheck,這使得Binius能夠處理更復雜的多項式排列情況。

因此,Binius通過對現有PIOPSumCheck機制的改進,提升了協議的靈活性和效率,尤其在處理更復雜的多變量多項式驗證時,提供了更強的功能支持。這些改進不僅解決了HyperPlonk中的侷限性,還為未來基於二進制域的證明系統奠定了基礎。

2.3 PIOP:新的 multilinear shift argument——適用於 boolean hypercube

在Binius協議中,虛擬多項式的構造和處理是關鍵技術之一,能夠有效地生成和操作從輸入句柄或其他虛擬多項式派生出的多項式。以下是兩個關鍵方法:

  • Packing:該方法通過將詞典序中相鄰位置的較小元素打包成更大的元素來優化操作。Pack運算符針對大小為2κ的塊操作,並將它們組合成高維域中的單個元素。通過多線性擴展(Multilinear Extension, MLE),這個虛擬多項式可以高效地評估和處理,將函數t轉換為另一個多項式,從而提高了計算性能。
  • 移位運算符:移位運算符重新排列塊內的元素,基於給定偏移量o進行循環移位。該方法適用於大小為2b的塊,每個塊根據偏移量執行移位。移位運算符通過檢測函數的支持來進行定義,確保在處理虛擬多項式時保持一致性和效率。評估該構造的複雜度隨塊大小線性增長,特別適用於處理大數據集或布爾超立方體中的高維場景。

2.4 PIOP:改編版Lasso lookup argument——適用於二進制域

Lasso協議允許證明方承諾一個向量a ∈ Fm,並證明其所有元素均存在於一個預先指定的表t ∈ Fn 中。Lasso解鎖了“查找奇點”(lookup singularities)的概念,並能適用於多線性多項式承諾方案。其效率體現在以下兩個方面:

  • 證明效率:對於大小為n的表中的m次查找,證明方只需承諾m+n個域元素。這些域元素很小,均位於集合{0,…,m}中。在基於多次冪運算的承諾方案中,證明方的計算成本為O(m + n)次群運算(如橢圓曲線點加),外加證明多線性多項式在布爾超立方體上是否為表元素的求值成本。
  • 無需承諾大表:如果表t是結構化的,則無需對其進行承諾,因此可以處理超大表(如2128或更大)。證明方的運行時間僅與訪問的表條目相關。對於任意整數參數c > 1,證明方的主要成本是證明大小,承諾的域元素為 3·c m + c·n1/c 個。這些域元素都是較小的,位於集合{0,…,max{m,n1/c,q} − 1} 中,其中q為a中的最大值。

Lasso協議由以下三個組件構成:

  1. 大表的虛擬多項式抽象:通過將虛擬多項式組合,實現在大表上的操作,確保在表內進行高效的查找和處理。
  2. 小表查找:Lasso的核心是小表查找,作為虛擬多項式協議的核心構建,使用離線內存檢測驗證一個虛擬多項式在布爾超立方體上的求值是否是另一個虛擬多項式求值的子集。這一查找過程將歸約為多集合檢測的任務。
  3. 多集合檢查:Lasso引入虛擬協議來執行多集合檢查,驗證兩個集合的元素是否相等或滿足特定條件。

Binius協議將Lasso適應於二進制域的操作,假設當前域是一個大特徵的素數域(遠大於被查找列的長度)。Binius引入了乘法版本的Lasso協議,要求證明方和驗證方聯合遞增協議的“內存計數”操作,不是通過簡單的加1遞增,而是通過二進制域中的乘法生成元來遞增。然而,這一乘法改編引入了更多的複雜性,與遞增操作不同,乘法生成元並非在所有情況下遞增,在0處存在單一軌道,這可能成為攻擊點。為防止這種潛在的攻擊,證明方必須承諾一個處處非零的讀取計數向量,以確保協議的安全性。

2.5 PCS:改編版Brakedown PCS——適用於Small-Field

構建BiniusPCS的核心思想是packing。Binius論文中提供了2種基於二進制域的Brakedown多項式承諾方案:一種是採用concatenated code來實例化;另一種採用block-level encoding技術,支持單獨使用Reed-Solomon codes。第二種Brakedown PCS方案,簡化了證明和驗證流程,但proof size要比第一種略大一點,但所帶來的簡化和實現優勢,做該取捨是值得的。

Binius多項式承諾主要使用小域多項式承諾與擴展域評估、小域通用構造和塊級編碼與Reed-Solomon碼技術。

小域多項式承諾與擴展域評估:Binius協議中的承諾是在小域K上的多項式承諾,並在更大的擴展域L/K中進行評估。這種方法確保了每個多線性多項式t(X0,…,Xℓ−1)屬於域K[X0,…,Xℓ−1],而評估點可以位於更大擴展域L中。承諾方案專門設計用於小域多項式,並能在擴展域上進行查詢,同時保證承諾的安全性和效率。

小域通用構造:小域通用構造通過定義參數ℓ、域K及其相關的線性塊碼C,確保擴展域L足夠大,以支持安全評估。為了在保持計算效率的同時提高安全性,協議通過擴展域的特性,以及採用線性塊碼對多項式進行編碼,保證了承諾的穩健性。

塊級編碼與Reed-Solomon碼:針對字段比線性塊碼字母表更小的多項式,Binius提出了塊級編碼方案。通過這一方案,即使在小域(如F2)中定義的多項式,也可以使用如F216這樣的大字母表的Reed-Solomon碼高效承諾。Reed-Solomon碼之所以被選中,是因為它具有高效性和最大距離分離特性。該方案通過將消息打包並逐行編碼,之後利用Merkle樹進行承諾,簡化了操作複雜度。塊級編碼允許小域多項式的高效承諾,而不會產生通常與大域相關的高計算開銷,從而使得在F2等小域中承諾多項式成為可能,並在生成證明與驗證中保持計算效率。

3. Binius優化

為了進一步提升Binius協議的性能,本文提出了四個關鍵優化點:

  1. GKR-based PIOP:針對二進制域乘法運算,藉助GKR協議,來替換Binius論文中的的Lasso Lookup算法,可大幅降低Binius的承諾開銷;
  2. ZeroCheck PIOP優化:在Prover與Verifier之間進行計算開銷權衡,使得ZeroCheck操作更加高效;
  3. Sumcheck PIOP優化:針對小域Sumcheck的優化,進一步減少了小域上的計算負擔;
  4. PCS 優化:通過FRI-Binius優化,降低證明大小,提高協議的整體性能。

3.1 GKR-based PIOP:基於GKR的二進制域乘法

Binius論文引入一種基於lookup的方案,旨在實現高效的二進制域乘法運算。通過Lasso lookup argument 改編的二進制域乘法算法依賴於lookups和加法操作的線性關係,這些操作與單個word中的limbs數量成比例。雖然這一算法在某種程度上優化了乘法操作,但仍需要與limbs數量線性相關的輔助承諾。

GKR(Goldwasser-Kalai-Rothblum)協議中的核心思想是,證明方(P)和驗證方(V)針對一個有限域F上的layered算術電路達成一致。該電路的每個節點有兩個輸入,用於計算所需的函數。為了減少驗證方的計算複雜度,協議使用SumCheck協議,將關於電路輸出門值的聲明逐步簡化為更低層的門值聲明,直至最終將聲明簡化到關於輸入的陳述。這樣,驗證方只需檢查電路輸入的正確性即可。

基於GKR的整數乘法運算算法,通過將“檢查2個32-bit整數A和B是否滿足 A·B =? C”,轉換為“檢查中(gA)B =? gC 是否成立”,藉助GKR協議大幅減少承諾開銷。與之前的Binius lookup方案相比,基於GKR的二進制域乘法運算只需一個輔助承諾,並且通過減少Sumchecks的開銷,使該算法更加高效,特別是在Sumchecks操作比承諾生成更便宜的場景下。隨著Binius優化的推進,基於GKR的乘法運算逐漸成為減少二進制域多項式承諾開銷的有效途徑。

3.2 ZeroCheck PIOP優化:Prover與Verifier計算開銷權衡

論文《Some Improvements for the PIOP for ZeroCheck》在證明方(P)和驗證方(V)之間調整工作量的分配,提出了多種優化方案,以權衡開銷。該工作探索了不同的k值配置,使得在證明方和驗證方之間達成了成本的權衡,特別是在減少傳輸數據和降低計算複雜性方面。

減少證明方的數據傳輸:通過將一部分工作轉移給驗證方V,從而降低證明方P發送的數據量。在第i輪中,證明方P需要向驗證方V發送vi+1(X),其中X=0,…,d + 1。驗證方V檢查以下等式以驗證數據的正確性:

vi = vi+1(0) + vi+1(1).

優化方法:證明方P可以選擇不發送vi+1(1),而是讓驗證方V自行通過以下方式計算出該值

vi+1(1) = vi − vi+1(0).

此外,在第0輪,誠實的證明方P始終發送v1(0) = v1(1) = 0,這意味著無需進行任何評估計算,從而顯著減少了計算和傳輸成本,降低至d2n−1CF + (d + 1)2n−1CG。

減少證明方評估點的數量:在協議的第i輪中,驗證者在之前的i輪中已經發送了一個值序列r =(r0,…,ri−1)。當前協議要求證明者 (P) 發送多項式

vi+1(X) = ∑ δˆn(α,(r,X,x))C(r,X,x).x∈H −−1

優化方法:證明方P發送以下多項式這兩個函數之間的關係是:

vi(X) = vi′(X)·δi+1((α0,…,αi),(r,X))

其中δˆi+1因為驗證者擁有α和r,所以是完全已知的。這個修改的好處在於vi′(X)的次數比vi(X)少1,這意味著證明者需要評估的點更少。因此,主要的協議變化發生在輪次之間的檢查環節。

此外,將原本的約束vi = vi+1(0)+vi+1(1) 優化為 (1−αi)vi′+1(0)+αivi′+1(1) = vi′(X)。則證明者需要評估和發送的數據更少,進一步減少傳輸的數據量。計算δˆn−i−1也比計算δˆn更高效。通過這兩項改進,成本降低為大約:2n−1(d− 1)CF + 2n−1dCG。在常見的d=3情況下,這些優化使成本降低了5/3倍。

代數插值優化:對於誠實的證明者,C(x0,…,xn−1)在Hn上為零,可表示為:C(x0,…,xn-1)= ∑xi(xi-1)Qi(x0,…,xn-1)。雖然Qi不是唯一的,但可以通過多項式長除法構造一個有序的分解:從Rn=C開始,逐次除以xi(xi−1)來計算Qi和Ri,其中R0是C在Hn上的多線性擴展,且假設其為零。分析Qi的次數,可以得出:對於j> i,Qj 在 xi 上的次數與 C 相同;對於 j = i,次數減少 2;對於 j i,次數至多為 1。給定向量 r = (r0,…,ri),Qj(r,X) 對於所有 j ≤ i 都是多線性的。此外1)Qj(r,X) 是與 C(r,X) 在 Hn−i 上相等的唯一多線性多項式。對於任何 X 和 x ∈ Hn−i−1,可以表示為:

C(r,X,x) − Qi(r,X,x) = X(X − 1)Qi+1(r,X,x)

因此,在協議的每一輪中,僅引入一個新的Q,其評估值可以從C和先前的Q計算得出,實現插值優化。

3.3 PIOP優化:基於小域的Sumcheck協議

Binius所實現的STARKs方案,其承諾開銷很低,使得prover瓶頸不再是PCS,而在於sum-check協議。

圖 2. 切換輪次與因子改進之間的關係

Ingonyama在2024年提出了針對基於小域的Sumcheck協議的改進方案(對應圖2中的Algo3和Algo4算法),並開源了實現代碼。算法4專注於將Karatsub算法合併到算法3中,以額外的基域乘法為代價來最小化擴域乘法次數,因此當擴域乘法比基域乘法昂貴得多時,算法4的性能會更好。

  • 切換輪次的影響與改進因子

基於小域的Sumcheck協議的改進集中於切換輪次t的選擇。切換輪次是指從優化算法切換回樸素算法的時間點,論文的實驗表明,在最佳切換點時,改進因子達到最大值,隨後呈現拋物線趨勢。如果超過這一切換點,優化算法的性能優勢減弱,效率下降。這是由於小域上的基域乘法與擴域乘法相比有更高的時間比率,因此在適當時機切換回樸素算法至關重要。

對於具體應用,如涉及Cubic Sumcheck(d = 3)的情況,基於小域的Sumcheck協議相較於樸素算法的改進達到了一個數量級。例如,在基域為GF[2]的情況下,算法4的性能比樸素算法高出近30倍。

  • 基域大小對性能的影響

論文的實驗結果表明,較小的基域(如GF[2])能夠使優化算法顯示出更顯著的優勢。這是因為擴展域與基域乘法的時間比率在較小基域上更高,從而優化算法在此條件下表現出更高的改進因子。

  • Karatsuba算法的優化收益

Karatsuba算法在提升基於小域的Sumcheck性能方面表現出顯著的效果。對於基域GF[2],算法3和算法4的峰值改進因子分別為6和30,表明算法4比算法3高效五倍。Karatsuba優化不僅提升了運行效率,也優化了算法的切換點,分別在算法3的t=5和算法4的t=8達到最佳。

  • 內存效率的提升

基於小域的Sumcheck協議除了提升運行時間,還在內存效率方面表現出顯著的優勢。算法4的內存需求為O(d·t),而算法3的內存需求為O(2d·t)。當t=8時,算法4僅需0.26MB的內存,而算法3則需67MB來存儲基域的乘積。這使得算法4在內存受限設備上表現出更強的適應性,尤其適用於資源有限的客戶端證明環境。

3.4 PCS 優化:FRI-Binius降低Binius proof size

Binius協議的一個主要缺陷在於其相對較大的證明大小,隨著見證大小的平方根按O(√N)縮放。與更高效的系統相比,這種平方根大小的證明是一種侷限性。相反,對數級(polylogarithmic)證明大小對於實現真正“簡潔”的驗證器至關重要,這在像Plonky3這樣的先進系統中得到了驗證,後者通過FRI等先進技術實現了對數級證明。

論文《Polylogarithmic Proofs for Multilinears over Binary Towers》,簡稱為FRI-Binius,實現了二進制域FRI摺疊機制,帶來4個方面的創新:

  • 扁平化多項式:初始的多線性多項式被轉換為LCH(低碼高度)新穎多項式基。
  • 子空間消失多項式:用於在係數域上執行FRI,並通過加性NTT(數論變換)實現類似FFT的分解。
  • 代數基打包:支持協議中信息的高效打包,可移除嵌入開銷。
  • 環交換SumCheck:一種新穎的SumCheck方法,利用環交換技術優化性能。

基於二進制域FRI-Binius的多線性多項式承諾方案(PCS)的核心思想為:FRI-Binius協議通過將初始的二進制域多線性多項式(定義於F2上)打包為定義在更大域K上的多線性多項式來操作。

在基於二進制域的FRI-BiniusPCS中,過程如下:

  1. 承諾階段:對一個ℓ變量的多線性多項式(定義於F2上)的承諾被轉化為對一個打包後的ℓ′變量的多線性多項式(定義於F2128上)的承諾,係數個數因此減少了128倍。
  2. 評估階段:證明方和驗證方進行ℓ′輪交叉環切換SumCheck和FRI交互證明(IOPP):
    • –FRI開放證明佔據了證明大小的大部分。
    • –證明方的SumCheck成本類似於常規大域上的SumCheck成本。
    • –證明方的FRI成本與常規大域上的FRI成本相同。
    • –驗證方接收128個來自F2128的元素,並執行128個額外的乘法運算。

藉助FRI-Binius,可將Binius證明大小減少一個數量級。這使得Binius的證明大小更加接近最先進的系統,同時保持與二進制域的兼容性。專為二進制域定製的FRI摺疊技術,加上代數打包和SumCheck的優化,使得Binius能夠在保持高效驗證的同時,生成更加簡潔的證明。


表 2:Binius 與 FRI-Binius 證明大小比較


表 3:Plonky3 FRI 與 FRI-Binius 比較

4. 結論

Binius的整個價值主張是,可為witnesses使用最小的power-of-two域,因此只需根據所需來選擇域大小。Binius是“使用硬件、軟件、與FPGA中加速的Sumcheck協議”的協同設計方案,可以以非常低的內存使用率來快速證明。Halo2和Plonky3等證明系統有4個佔用大部分計算量的關鍵步驟:生成witness數據、對witness數據進行承諾、vanishingargument、openingproof。以Plonky3中的Keccak和Binius中的Grøstl哈希函數為例,二者對應的以上4大關鍵步驟計算量佔比情況如圖3所示:

圖 3. 較小的承諾成本

由此可知,Binius中已基本完全移除了Prover的commit承諾瓶頸,新的瓶頸在於Sumcheck協議,而Sumcheck協議中大量多項式evaluations和域乘法等問題,可藉助專用硬件高效解決。FRI-Binius方案,為FRI變體,可提供一個非常有吸引力的選擇——從域證明層中消除嵌入開銷,而不會導致聚合證明層的成本激增。當前,Irreducible團隊正在開發其遞歸層,並 宣佈與Polygon團隊合作構建Binius-based zkVM; JoltzkVM正從Lasso轉向Binius,以改進其遞歸性能;以及 Ingonyama團隊正在實現FPGA版本的Binius.

參考文獻

  1. 2024.04 Binius Succinct Arguments over Towers of Binary Fields
  2. 2024.07 Fri-Binius Polylogarithmic Proofs for Multilinears over Binary Towers
  3. 2024.08 Integer Multiplication in Binius: GKR-based approach
  4. 2024.06 zkStudyClub - FRI-Binius: Polylogarithmic Proofs for Multilinears over Binary Towers
  5. 2024.04 ZK11: Binius: a Hardware-Optimized SNARK - Jim Posen
  6. 2023.12 Episode 303: A Dive into Binius with Ulvetanna
  7. 2024.09 Designing high-performance zkVMs
  8. 2024.07 Sumcheck and Open-Binius
  9. 2024.04 Binius: highly efficient proofs over binary fields
  10. 2023.12 SNARKs on binary fields: Binius - Part 1
  11. 2024.06 SNARKs on binary fields: Binius - Part 2
  12. @espressosys/hyperplonk-a-zk-proof-system-for-zkevms-d45fd077bfba”>2022.10 HyperPlonk, a zk-proof system for ZKEVMs

聲明:

  1. 本文轉載自【bitlayer】,著作權歸屬原作者【lynndell】,如對轉載有異議,請聯繫 Gate Learn 團隊,團隊會根據相關流程儘速處理。
  2. 免責聲明:本文所表達的觀點和意見僅代表作者個人觀點,不構成任何投資建議。
  3. 文章其他語言版本由 Gate Learn 團隊翻譯,除非另有說明,否則禁止複製、傳播或抄襲經翻譯文章。
เริ่มตอนนี้
สมัครและรับรางวัล
$100