Analyse et optimisation des STARKs de Binius

1. Introduction

Une des principales raisons de l'inefficacité des STARKs est que la plupart des valeurs dans les programmes réels sont assez petites, mais pour garantir la sécurité des preuves basées sur les arbres de Merkle, l'utilisation du codage de Reed-Solomon pour étendre les données entraîne l'occupation de nombreux valeurs redondantes supplémentaires dans tout le domaine. Réduire la taille du domaine devient une stratégie clé.

La largeur de code des STARKs de 1ère génération est de 252 bits, celle de 2ème génération est de 64 bits, et celle de 3ème génération est de 32 bits, mais la largeur de code de 32 bits présente encore un grand espace gaspillé. Le domaine binaire permet d'opérer directement sur les bits, avec un encodage compact et efficace sans espace gaspillé, ce qui pourrait être les STARKs de 4ème génération.

Binius utilise une version améliorée de la multiplication et de la vérification de permutation HyperPlonk basée sur le domaine binaire en tour, ainsi que des engagements de polynômes sur de petits domaines, afin d'améliorer l'efficacité sous différents angles.

2. Analyse des principes

Binius est composé de cinq technologies clés :

1. Arithmétique basée sur le domaine binaire en tour
2. Vérification des produits et des permutations de la version adaptée HyperPlonk
3. Nouvelle preuve de décalage multilinéraire
4. Version améliorée de la preuve de recherche Lasso
5. Schéma d'engagement de polynômes à petite portée

2.1 Arithmétique basée sur le domaine binaire en forme de tour

Le domaine binaire en forme de tour prend en charge des opérations arithmétiques efficaces et un processus d'arithmétisation simplifié. Les éléments du domaine binaire peuvent être directement mappés sur des chaînes de k bits, offrant la commodité d'une correspondance un à un.

2.2 version adaptée de l'HyperPlonk produit et vérification de permutation

Binius s'inspire du mécanisme de vérification central de HyperPlonk, y compris GateCheck, PermutationCheck, LookupCheck, etc., et apporte des améliorations dans les domaines suivants :

• Optimisation de ProductCheck
• Gestion des problèmes de division par zéro
• Vérification de permutation entre les colonnes

2.3 Nouvelle preuve de décalage multilinéaire

Binius a introduit deux méthodes clés, Packing et l'opérateur de décalage, pour construire et traiter des polynômes virtuels.

2.4 version adaptée de la recherche de preuve Lasso

Binius a adapté Lasso pour les opérations dans le domaine binaire, introduisant une version multiplicative du protocole Lasso.

2.5 engagement polynomial de domaine

Binius propose deux schémas de promesse polynomiale Brakedown basés sur le domaine binaire, utilisant principalement des promesses polynomiales sur de petits domaines avec évaluation dans un domaine étendu, construction universelle sur un petit domaine et techniques de codage au niveau des blocs avec des codes de Reed-Solomon.

3. Optimisation de la pensée

3.1 PIOP basé sur GKR

L'algorithme de multiplication dans le domaine binaire basé sur GKR, en transformant "vérifier si deux entiers 32 bits A et B satisfont A·B =? C" en "vérifier si (gA)B =? gC est vrai", réduit considérablement le coût d'engagement grâce au protocole GKR.

3.2 ZeroCheck PIOP optimisation

En ajustant la répartition du travail entre les parties prouvantes et vérificatrices, plusieurs solutions d'optimisation ont été proposées:

• Réduire le transfert de données de la partie preuve
• Réduire le nombre de points d'évaluation des entités de preuve
• Optimisation de l'interpolation algébrique

3.3 Vérification de somme optimisation PIOP

Ingonyama a proposé une amélioration du protocole Sumcheck basé sur de petits domaines, se concentrant sur le choix du tour t.

3.4 PCS optimisation: FRI-Binius

FRI-Binius a réalisé un mécanisme de pliage FRI dans le domaine binaire, apportant 4 innovations :

• Polynomiale aplatie
• Polynomials de disparition du sous-espace
• Emballage de base algébrique
• Échange de somme de cercle

4. Conclusion

Binius est une solution de conception collaborative qui utilise le protocole Sumcheck accéléré par matériel, logiciel et FPGA, permettant de prouver rapidement avec une utilisation de mémoire très faible. Dans Binius, le goulot d'étranglement de l'engagement de Prover a été pratiquement complètement éliminé, le nouveau goulot d'étranglement réside dans le protocole Sumcheck, qui peut être efficacement résolu grâce à du matériel dédié.

Le plan FRI-Binius est une variante de FRI qui permet d'éliminer le coût d'intégration de la couche de preuve de domaine sans entraîner une augmentation des coûts de la couche de preuve agrégée. Actuellement, plusieurs équipes développent des technologies liées à Binius, y compris des couches récursives, zkVM, etc.