Analyse des principes et réflexion sur l'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 Reed-Solomon pour étendre les données entraîne de nombreuses valeurs redondantes supplémentaires qui occupent l'ensemble du domaine. Pour résoudre ce problème, la réduction de la taille du domaine est devenue une stratégie clé.

La largeur de codage des STARKs de première génération est de 252 bits, celle de la deuxième génération est de 64 bits, et celle de la troisième génération est de 32 bits, mais la largeur de codage de 32 bits présente encore une grande quantité d'espace gaspillé. En comparaison, le domaine binaire permet d'opérer directement sur les bits, le codage est compact et efficace sans aucun espace gaspillé, soit les STARKs de quatrième génération.

Le domaine binaire utilisé par Binius doit entièrement dépendre de l'extension de domaine pour garantir sa sécurité et sa praticabilité. La plupart des polynômes impliqués dans les calculs Prover n'ont pas besoin d'entrer dans l'extension de domaine, mais doivent simplement opérer sous le domaine de base, permettant ainsi d'atteindre une haute efficacité dans un petit domaine. Cependant, les vérifications de points aléatoires et les calculs FRI doivent encore s'approfondir dans une extension de domaine plus grande pour assurer la sécurité requise.

Binius a proposé une solution innovante : tout d'abord, en utilisant des polynômes multivariés (en particulier des polynômes multilinéaires) à la place de polynômes à une seule variable, pour représenter l'ensemble de la trajectoire de calcul par leurs valeurs sur des "hyper-cubes" ; ensuite, étant donné que la longueur de chaque dimension de l'hyper-cube est de 2, il n'est pas possible de procéder à une extension standard de Reed-Solomon comme avec les STARKs, mais on peut considérer l'hyper-cube comme un carré, basé sur lequel on peut effectuer une extension de Reed-Solomon.

2. Analyse des principes

Binius comprend cinq technologies clés :

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

2.1 Domain fini : arithmétisation basée sur les tours de champs binaires

Les avantages du domaine binaire en forme de tour:

• Calcul efficace : le domaine binaire supporte essentiellement des opérations arithmétiques très efficaces.
• Arithmetic efficace : la structure de champ binaire supporte un processus arithmétique simplifié.
• Représentation standardisée : les éléments dans le domaine binaire ont une représentation unique et directe.

Avantages du domaine binaire :

• Les opérations d'addition et de multiplication ne nécessitent pas de report.
• L'opération de carré est très efficace, suivant la règle de simplification (X + Y)^2 = X^2 + Y^2
• Indiquer la flexibilité : une chaîne de 128 bits peut être considérée comme un élément unique dans un domaine binaire de 128 bits, ou être interprétée comme une combinaison de plusieurs éléments de domaine de tour.

2.2 PIOP: version adaptée de HyperPlonk Product et PermutationCheck

Mécanisme de vérification du noyau PIOP de Binius:

• GateCheck
• PermutationCheck
• LookupCheck
• MultisetCheck
• ProductCheck
• ZeroCheck
• SumCheck
• BatchCheck

Améliorations de Binius sur HyperPlonk :

• Optimisation de ProductCheck
• Gestion du problème de la division par zéro
• Support de vérification de permutation en croix

2.3 PIOP: nouvel argument de décalage multilinéraire

Méthode clé:

• Emballage : optimisation des opérations en regroupant les éléments adjacents
• Opérateurs de décalage : réorganiser les éléments à l'intérieur des blocs

2.4 PIOP: version modifiée de l'argument de recherche Lasso

Composition du protocole Lasso:

• Abstraction des polynômes virtuels de grande table
• Recherche de petite table
• Vérification multiple des ensembles

L'adaptation de Binius pour Lasso:

• Introduction de la version multiplicative du protocole Lasso
• Exiger que la partie prouvante s'engage à un vecteur de compte de lecture non nul partout.

2.5 PCS: version adaptée Brakedown PCS

Idée principale : packing

Deux schémas d'engagement polynomiaux Brakedown basés sur des domaines binaires :

1. Instanciation du code concaténé
2. Utiliser la technologie de codage au niveau des blocs, prenant en charge l'utilisation séparée des codes de Reed-Solomon.

Principales technologies:

• Engagement de polynômes de petite portée et évaluation dans un domaine étendu
• Petite zone de construction universelle
• Codage par blocs et code de Reed-Solomon

3. Optimisation de la pensée

Quatre points d'optimisation clés :

3.1 PIOP basé sur GKR : multiplication de domaine binaire basée sur GKR

Avantages par rapport à la solution de recherche Binius :

• Il suffit d'un engagement auxiliaire
• Réduire les coûts de Sumchecks

3.2 ZeroCheck PIOP optimisation : équilibre des coûts de calcul entre Prover et Verifier

Méthodes d'optimisation:

• Réduire le transfert de données des parties prouvantes
• Réduire le nombre de points d'évaluation des parties prouvantes
• Optimisation par interpolation algébrique

3.3 Optimisation PIOP de Sumcheck : protocole de Sumcheck basé sur un petit domaine

Point clé :

• Impact et facteur d'amélioration du changement de tour
• L'impact de la taille de la base sur les performances
• Rendement d'optimisation de l'algorithme de Karatsuba
• Amélioration de l'efficacité de la mémoire

3.4 PCS optimisation : FRI-Binius réduction de la taille de preuve de Binius

Quatre innovations de FRI-Binius:

• Polynomiale aplatie
• Polynomiales de disparition de sous-espaces
• Emballage de base algébrique
• Échange de somme de l'anneau

FRI-Binius PCS processus:

• Phase d'engagement
• Phase d'évaluation

4. Conclusion

La proposition de valeur de Binius:

• Peut utiliser le domaine power-of-two minimum pour les témoins
• Solution de conception collaborative, faible utilisation de la mémoire, preuve rapide.
• Élimination fondamentale du goulot d'étranglement des engagements de commit de Prover
• Le nouveau goulot d'étranglement réside dans le protocole Sumcheck, qui peut être efficacement résolu à l'aide de matériel spécialisé.

FRI-Binius方案:

• Éliminer les frais d'intégration du niveau de preuve de domaine
• Ne provoquera pas une augmentation des coûts de la couche de preuve d'agrégation.

Progrès actuel :

• L'équipe Irreducible développe une couche récursive, en collaboration avec Polygon pour construire un zkVM basé sur Binius.
• JoltzkVM passe de Lasso à Binius
• L'équipe Ingonyama a réalisé la version FPGA de Binius