Binius STARKsの原理とその最適化思考の解析

1 はじめに

楕円曲線に基づくSNARKsとは異なり、STARKsはハッシュに基づくSNARKsと見なすことができます。現在、STARKsの効率が低い主な理由の一つは、実際のプログラムでほとんどの数値が小さいことです。たとえば、ループインデックス、ブール値、カウンターなどです。しかし、Merkleツリーに基づく証明の安全性を確保するために、Reed-Solomon符号を使用してデータを拡張する際には、多くの冗長値が全体の領域を占めることになります。元の値が非常に小さい場合でもです。この問題を解決するために、領域のサイズを縮小することが重要な戦略となります。

第1世代のSTARKsのエンコーディングビット幅は252ビット、第二世代は64ビット、第三世代は32ビットですが、32ビットのエンコーディングにはまだ大量の無駄なスペースがあります。それに対して、バイナリフィールドはビットに直接操作を行うことを許可し、エンコーディングはコンパクトで効率的で無駄がないため、第四世代のSTARKsと見なすことができます。

近年発見されたGoldilocks、BabyBear、Mersenne31などの有限体と比較して、二進体の研究は1980年代に遡ります。現在、二進体はAES(F28体)、GMAC(F2128体)、QRコード(F28のReed-Solomon符号)など、暗号学に広く応用されています。原始FRIおよびzk-STARKプロトコル、さらにSHA-3ファイナリストのGrøstlハッシュ関数もF28体に基づいています。

小さな体を使用する場合、拡張体の操作は安全性を確保するためにますます重要になります。Biniusが使用する二進法体は、完全に拡張体に依存して安全性と可用性を保証します。ほとんどのProver計算に関与する多項式は、基本体で操作するだけで済むため、小さな体内で高効率を実現します。しかし、ランダムポイントチェックやFRI計算は、必要な安全性を確保するために、より大きな拡張体で行う必要があります。

バイナリドメインに基づいて証明システムを構築する際に存在する2つの実際的な問題:

1. STARKsの計算トレース表示において、使用する域のサイズは多項式の階よりも大きい必要があります。
2. STARKsにおけるMerkleツリーのコミットメントではReed-Solomonコーディングを行う必要があり、使用するフィールドのサイズはコーディングの拡張後のサイズよりも大きくする必要があります。

Biniusはこれら2つの問題をそれぞれ処理する革新的なソリューションを提案しました。

1. 単一変数多項式の代わりに多変数(多線形)多項式を使用し、その値を「超立方体」上で表現することによって、全体の計算軌跡を示します。
2. 超立方体の各次元の長さが2であるため、STARKsのように標準的なReed-Solomon拡張を行うことはできませんが、超立方体を正方形とみなし、その正方形に基づいてReed-Solomon拡張を行うことができます。

この方法は安全性を確保しながら、コーディング効率と計算性能を大幅に向上させました。

! Bitlayer研究:Binius STARKsの原理分析と最適化思考

2 原理分析

現在ほとんどのSNARKsシステムは通常二つの部分から構成されています:

1. 情報理論多項式インタラクティブオラクル証明(PIOP): 証明システムの核心として、入力された計算関係を検証可能な多項式等式に変換します。検証者との対話を通じて、証明者は徐々に多項式を送信し、検証者は少量の多項式の評価結果を問い合わせることで計算の正確性を検証します。既存のPIOPプロトコルには、PLONK PIOP、Spartan PIOP、HyperPlonk PIOPなどがあります。

2. 多項式コミットメントスキーム(PCS): PIOPによって生成された多項式等式が成立するかどうかを証明するために使用されます。PCSは暗号学的ツールであり、証明者はある多項式に対してコミットし、その後評価結果を検証することができ、同時に多項式の他の情報を隠すことができます。一般的なPCSにはKZG、Bulletproofs、FRI、Brakedownなどがあります。

要求に応じて異なるPIOPとPCSを選択し、適切な有限体または楕円曲線と組み合わせることで、異なる属性を持つ証明システムを構築できます。例えば:

• Halo2: PLONK PIOP + Bulletproofs PCS + パスタカーブ
• Plonky2: PLONK PIOP + FRI PCS + ゴルディロックスドメイン
• Binius:HyperPlonk PIOP + Brakedown PCS + バイナリドメイン

Biniusには5つの主要な技術が含まれています:

1. タワー型二進法ドメインに基づく算術化:計算の基礎を構成し、二進法ドメイン内での簡略化された演算を実現する

2. HyperPlonkの乗算と置換チェックの改編: 変数と置換間の効率的な整合性チェックを確保する

3. 新しい Multilinear Shift 引数: 小さなドメインでの多重線形関係の検証効率を最適化

4. Lassoルックアップ引数の改善:ルックアップメカニズムの柔軟性とセキュリティを提供します

5. 小域多項式コミットメントスキーム: バイナリーフィールド上で効率的な証明システムを実現し、大域に関連するコストを削減する

! Bitlayer研究:Binius STARKsの原理分析と最適化思考

2.1 有限体:二値体の塔に基づく算術

タワー型二進法体は、高速で検証可能な計算を実現するための鍵であり、主に効率的な計算と効率的な算術化に起因しています。二進法体は本質的に高度に効率的な算術演算をサポートし、性能に敏感な暗号学的アプリケーションにとって理想的な選択肢となります。二進法体の構造は、簡素化された算術化プロセスをサポートしており、二進法体上で実行される演算はコンパクトで検証可能な代数形式で表現できます。これらの特性に加えて、タワー構造を通じてその階層特性を十分に活用できるため、二進法体はBiniusのようなスケーラブルな証明システムに特に適しています。

"canonical"は、二進数体内の要素の唯一かつ直接的な表現方法を指します。例えば、基本二進数体F2では、任意のkビットの文字列はkビットの二進数体の要素に直接マッピングできます。これは素数体とは異なり、素数体は指定されたビット数内でこのような標準的な表現を提供することはできません。32ビットの素数体は32ビット内に含まれることができますが、すべての32ビットの文字列が唯一の体の要素に対応できるわけではなく、二進数体はこの一対一のマッピングの便利さを備えています。

素数領域 Fp では、一般的な縮約法には、バレット縮約法、モンゴメリー還元、およびメルセンヌ-31 や Goldilocks-64 などの特定の有限体に対する特別な簡約法が含まれます。 バイナリドメインF2kでは、一般的な削減方法には、(を使用したAESなどの特別な削減)が含まれます。 POLYVALなどのモンゴメリ縮約(は、Tower)などの(および再帰的な縮約)を使用します。

論文「Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations」では、バイナリ領域では加算演算と乗算演算の両方でキャリーを導入する必要がなく、バイナリフィールドの二乗演算は次のように行われるため、非常に効率的であることを指摘しています(X + Y)2 = X2 + Y2 です。

128ビットの文字列は、バイナリフィールドの文脈でさまざまな方法で解釈できます。それは128ビットのバイナリフィールドのユニークな要素として見なされるか、2つの64ビットタワーフィールドの要素、4つの32ビットタワーフィールドの要素、16の8ビットタワーフィールドの要素、または128のF2フィールドの要素として解析できます。このような表現の柔軟性は、計算オーバーヘッドを必要とせず、ビット文字列の型変換に過ぎず、非常に興味深く有用な特性です。同時に、小さなフィールド要素は、追加の計算オーバーヘッドなしにより大きなフィールド要素にパッケージ化できます。Biniusプロトコルは、この特性を利用して計算効率を向上させます。

この論文「On Efficient Inversion in Tower Fields of Characteristic Two」では、nビットタワー (バイナリドメインにおける乗算、二乗、および反転演算の計算の複雑さを調査し、) mビットのサブドメインに分解できます。

! Bitlayer研究:Binius STARKsの原理分析と最適化思考

2.2 PIOP: バイナリドメイン用の適応 HyperPlonk プロダクトと PermutationCheck ------

BiniusプロトコルにおけるPIOP設計はHyperPlonkを参考にしており、一連のコアチェックメカニズムを使用して多項式と多変数集合の正当性を検証します:

1. GateCheck: 機密証明ωと公開入力xが回路計算関係C(x,ω)=0を満たしているかを検証し、回路が正しく動作することを確認します。

2. PermutationCheck:ブールハイパーキューブ上の2つの多変量多項式fとgの評価結果が順列関係であることを確認しますf(x) = f(π(x))、多項式変数間の配置の一貫性を確保します。

3. LookupCheck:多項式の評価が指定されたルックアップテーブルに存在するかどうかを検証します。すなわち、f(Bμ) ⊆ T(Bμ)、特定の値が指定された範囲内にあることを確認します。

4. MultisetCheck: 2つの多変数集合が等しいかどうかを確認します。すなわち、{(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とプロトコル設計において多くの類似点がありますが、以下の3つの点で改善を行っています:

• ProductCheckの最適化: HyperPlonkでは、ProductCheckは分母Uが超立方体上で常に非ゼロであること、および積が特定の値と等しいことを要求します。Biniusはこの値を1に特化することで、このチェックプロセスを簡素化し、計算の複雑さを低減します。

• ゼロ除算問題の処理: HyperPlonkはゼロのケースを適切に処理できず、超立方体上のUの非ゼロ問題を主張できませんでした; Biniusはこの問題を正しく処理し、分母がゼロであってもBiniusのProductCheckは処理を続け、任意の積値に拡張を許可します。

• PermutationCheck: この機能は HyperPlonk では使用できません。 Binius は複数の列間の PermutationCheck をサポートしているため、Binius はより複雑な多項式順列を処理できます。

そのため、Biniusは既存のPIOP SumCheckメカニズムの改善を通じて、プロトコルの柔軟性と効率を向上させ、特により複雑な多変数多項式検証を処理する際に、より強力な機能サポートを提供しました。これらの改善は、HyperPlonkの限界を解決するだけでなく、将来のバイナリフィールドに基づく証明システムの基盤を築くものです。

! Bitlayer研究:Binius STARKsの原理分析と最適化思考

2.3 PIOP:新しいマルチラインシフト引数------ブールハイパーキューブに適用

Biniusプロトコルでは、仮想多項式の構築と処理が重要な技術の一つであり、入力ハンドルや他の仮想多項式から派生した多項式を効果的に生成および操作することができます。以下は2つの重要な方法です:

• Packing:この方法は、辞書式順序で隣接する位置の小さい要素をより大きな要素にパッキングすることで操作を最適化します。Pack演算子はサイズが2κのブロック操作に対して、これらを高次元の領域内の単一の要素に組み合わせます。多線形拡張(Multilinear Extension, MLE)を通じて、この仮想多項式は効率的に評価および処理され、関数tを別の多項式に変換することで計算性能が向上します。

• シフト演算子: シフト演算子は、与えられたオフセットoに基づいてブロック内の要素を再配置し、循環シフトを行います。この方法はサイズが2bのブロックに適用され、各ブロックはオフセットに従ってシフトを実行します。シフト演算子は関数のサポートを検出することによって定義され、仮想多項式を処理する際の一貫性と効率を確保します。この構造の評価の複雑さはブロックサイズに対して線形に増加し、特に大規模データセットやブール超立方体における高次元シーンの処理に適しています。

! Bitlayer Research: Binius STARKs Principle Analysis and Optimization Thinking

2.4 PIOP:バイナリドメイン用の適応されたLassoルックアップ引数------

Lassoプロトコルは、証明者がベクトルa ∈ Fmをコミットし、そのすべての要素が事前に指定されたテーブルt ∈ Fnに存在することを証明できるようにします。Lassoは「特異点を探す」(lookup singularities)の概念を解放し、多項式のコミットメントスキームに適用できるようになります。その効率は以下の2つの側面に表れます:

• 証明効率: サイズnのテーブルにおけるm回の検索に対して、証明者はm+n個のドメイン要素を約束するだけです。これらのドメイン要素は非常に小さく、集合{0,...,m}の中にあります。多重冪演算に基づくコミットメントスキームでは、証明者の計算コストはO(m + n)回の群演算(です。