Titre original transmis 'Vitalik explique Binius en détail : un système de preuve efficace basé sur des champs binaires'

Ce post est principalement destiné aux lecteurs approximativement familiers avec la cryptographie de l'ère 2019, en particulier les SNARKs et les STARKs. Si ce n'est pas votre cas, je vous recommande de lire ces articles en premier. Un grand merci à Justin Drake, Jim Posen, Benjamin Diamond et Radi Cojbasic pour leurs retours et leurs révisions.

Au cours des deux dernières années, les STARKs sont devenues une technologie cruciale et irremplaçable pour la réalisation efficace de preuves cryptographiques faciles à vérifier de déclarations très complexes (par exemple, prouver qu'un bloc Ethereum est valide). Une raison clé en est la petite taille des champs : tandis que les SNARKs basés sur les courbes elliptiques nécessitent que vous travailliez sur des entiers de 256 bits pour être suffisamment sécurisés, les STARKs vous permettent d'utiliser des tailles de champ beaucoup plus petites, qui sont plus efficaces : d'abord le champ Goldilocks (entiers de 64 bits), puis Mersenne31 et BabyBear (tous deux de 31 bits). Grâce à ces gains d'efficacité, Plonky2, qui utilise Goldilocks, est des centaines de fois plus rapide pour prouver de nombreux types de calculs que ses prédécesseurs.

Une question naturelle à poser est : pouvons-nous pousser cette tendance à sa conclusion logique, en construisant des systèmes de preuve qui fonctionnent encore plus rapidement en opérant directement sur des zéros et des uns ? C'est exactement ce que Binius essaie de faire, en utilisant un certain nombre de tours mathématiques qui le rendent très différent des SNARKs et des STARKs d'il y a trois ans. Cette publication explique pourquoi les petits champs rendent la génération de preuves plus efficace, pourquoi les champs binaires sont exceptionnellement puissants, et les astuces que Binius utilise pour faire fonctionner les preuves sur les champs binaires de manière si efficace.

Binius. À la fin de ce post, vous devriez être capable de comprendre chaque partie de ce diagramme.

Récapitulatif : champs finis

Une des tâches clés d'un système de preuve cryptographique est de fonctionner sur de grandes quantités de données, tout en maintenant les chiffres petits. Si vous pouvez compresser une déclaration sur un grand programme en une équation mathématique impliquant quelques chiffres, mais que ces chiffres sont aussi grands que le programme original, vous n'avez rien gagné.

Pour effectuer des opérations arithmétiques complexes tout en gardant les nombres petits, les cryptographes utilisent généralement l'arithmétique modulaire. Nous choisissons un certain nombre premier “modulus” p. L'opérateur % signifie “prendre le reste de”: 15 % 7=1, 53 % 10=3, etc (notez que la réponse est toujours non négative, donc par exemple −1 % 10=9).

Vous avez probablement déjà vu l'arithmétique modulaire, dans le contexte de l'addition et de la soustraction du temps (par exemple, quelle heure est-il quatre heures après 9h00 ?). Mais ici, nous n'ajoutons pas et ne soustrayons pas simplement modulo un nombre, nous multiplions également, divisons et prenons des exposants.

Nous redéfinissons:

Les règles ci-dessus sont toutes cohérentes. Par exemple, si p=7, alors:

5+3=1 (because 8%7=1)

1-3=5 (parce que -2%7=5)

2*5=3

3/5=2

Un terme plus général pour ce type de structure est un champ fini. Un champ fini est une structure mathématique qui obéit aux lois habituelles de l'arithmétique, mais où il y a un nombre limité de valeurs possibles, de sorte que chaque valeur peut être représentée dans une taille fixe.

L'arithmétique modulaire (ou les corps premiers) est le type le plus courant de champ fini, mais il existe également un autre type : les champs d'extension. Vous avez probablement déjà vu un champ d'extension : les nombres complexes. Nous "imaginons" un nouvel élément, que nous étiquetons ι, et déclarons qu'il satisfait ι2=−1. Vous pouvez alors prendre n'importe quelle combinaison de nombres réguliers et de ι, et faire des mathématiques avec : (3ι+2)*(2ι+4)= 6ι2+12ι+4ι+8=16ι+2. Nous pouvons de manière similaire prendre des extensions de corps premiers. À mesure que nous commençons à travailler sur des champs qui sont plus petits, les extensions des corps premiers deviennent de plus en plus importantes pour préserver la sécurité, et les champs binaires (que Binius utilise) dépendent entièrement des extensions pour avoir une utilité pratique.

Récapitulatif: arithmétisation

La façon dont les SNARKs et les STARKs prouvent des choses sur les programmes informatiques passe par l'arithmétisation : vous convertissez une déclaration sur un programme que vous souhaitez prouver en une équation mathématique impliquant des polynômes. Une solution valide à l'équation correspond à une exécution valide du programme.

Pour donner un exemple simple, supposons que j'ai calculé le 100ème nombre de Fibonacci, et que je veux vous prouver ce qu'il est. Je crée un polynôme 𝐹 qui code les nombres de Fibonacci : donc 𝐹(0)=𝐹(1)=1, 𝐹(2)=2, 𝐹(3)=3, 𝐹(4)=5, et ainsi de suite pour 100 étapes. La condition que je dois prouver est que 𝐹(𝑥+2)=𝐹(𝑥)+𝐹(𝑥+1) sur la plage 𝑥={0,1…98}. Je peux vous convaincre de cela en vous donnant le quotient :

où Z(x) = (x-0) (x-1) …(x-98). . Si je peux prouver qu'il existe F et H qui satisfont cette équation, alors F doit satisfaire F(x+2)-F(x+1)-F(x) dans la plage. Si je vérifie en plus que F est satisfait, F(0)=F(1)=1, alors F(100) doit en fait être le 100e nombre de Fibonacci.

Si vous voulez prouver quelque chose de plus compliqué, alors remplacez la relation “simple” 𝐹(𝑥+2)=𝐹(𝑥)+𝐹(𝑥+1) par une équation plus compliquée, qui dit essentiellement que “𝐹(𝑥+1) est la sortie de l'initialisation d'une machine virtuelle avec l'état 𝐹(𝑥), et l'exécution d'une étape de calcul”. Vous pouvez également remplacer le nombre 100 par un nombre plus grand, par exemple 100000000, pour accommoder plus d'étapes.

Tous les SNARKs et STARKs sont basés sur cette idée d'utiliser une équation simple sur des polynômes (ou parfois des vecteurs et des matrices) pour représenter un grand nombre de relations entre des valeurs individuelles. Tous n'impliquent pas de vérifier l'équivalence entre des étapes computationnelles adjacentes de la même manière que ci-dessus : PLONK ne le fait pas, par exemple, et R1CS non plus. Mais beaucoup des plus efficaces le font, car imposer la même vérification (ou les mêmes quelques vérifications) de nombreuses fois rend plus facile la minimisation des frais généraux.

Plonky2: de SNARKs et STARKs 256 bits à 64 bits… uniquement des STARKs

Il y a cinq ans, un résumé raisonnable des différents types de preuves de connaissance nulle était le suivant. Il existe deux types de preuves : les SNARKs (basées sur les courbes elliptiques) et les STARKs (basées sur les hachages). Techniquement, les STARKs sont un type de SNARK, mais dans la pratique, il est courant d'utiliser le terme "SNARK" pour se référer uniquement à la variété basée sur les courbes elliptiques, et "STARK" pour se référer aux constructions basées sur les hachages. Les SNARKs sont petits, donc vous pouvez les vérifier très rapidement et les ajuster facilement sur la chaîne. Les STARKs sont grands, mais ils ne nécessitent pas de configurations de confiance, et ils sont résistants aux attaques quantiques.

Les STARKs fonctionnent en traitant les données comme un polynôme, en calculant les évaluations de ce polynôme sur un grand nombre de points, et en utilisant la racine de Merkle de ces données étendues comme le "engagement polynomial"

Un élément clé de l’histoire ici est que les SNARK basés sur des courbes elliptiques ont été les premiers à être largement utilisés : il a fallu attendre environ 2018 pour que les STARK deviennent suffisamment efficaces pour être utilisés, grâce à FRI, et à ce moment-là, Zcash fonctionnait déjà depuis plus d’un an. Les SNARK basés sur des courbes elliptiques ont une limitation clé : si vous voulez utiliser des SNARK basés sur des courbes elliptiques, alors l’arithmétique dans ces équations doit être faite avec des entiers modulo le nombre de points sur la courbe elliptique. Il s’agit d’un grand nombre, généralement proche de 2256 : par exemple, pour la courbe bn128, c’est 21888242871839275222246405745257275088548364400416034343698204186575808495617. Mais le calcul réel utilise de petits nombres : si vous pensez à un « vrai » programme dans votre langage préféré, la plupart des choses avec lesquelles il fonctionne sont des compteurs, des index dans des boucles for, des positions dans le programme, des bits individuels représentant Vrai ou Faux, et d’autres choses qui ne feront presque toujours que quelques chiffres.

Même si vos données « originales » sont constituées de « petits » nombres, le processus de preuve nécessite le calcul de quotients, d’extensions, de combinaisons linéaires aléatoires et d’autres transformations des données, qui conduisent à un nombre égal ou supérieur d’objets qui sont, en moyenne, aussi grands que la taille totale de votre champ. Cela crée une inefficacité clé : pour prouver un calcul sur n petites valeurs, vous devez faire encore plus de calcul sur n valeurs beaucoup plus grandes. Au début, les STARK ont hérité de l’habitude d’utiliser des champs de 256 bits des SNARK, et ont donc souffert de la même inefficacité.

Une extension Reed-Solomon de certaines évaluations polynomiales. Bien que les valeurs originales soient petites, les valeurs supplémentaires explosent toutes à la taille totale du champ (dans ce cas 2 à la puissance 31 -1)

En 2022, Plonky2 a été publié. L'innovation principale de Plonky2 était de faire de l'arithmétique modulo un plus petit nombre premier: 2⁶⁴−2³²+1=18446744069414584321. Maintenant, chaque addition ou multiplication peut toujours être effectuée en quelques instructions sur un CPU, et le hachage de toutes les données ensemble est 4 fois plus rapide qu'auparavant. Mais cela a un inconvénient : cette approche est uniquement pour STARK. Si vous essayez d'utiliser un SNARK, avec une courbe elliptique d'une taille si petite, la courbe elliptique devient non sécurisée.

Pour continuer à être en sécurité, Plonky2 devait également introduire des champs d'extension. Une technique clé dans la vérification des équations arithmétiques est l'"échantillonnage à un point aléatoire": si vous voulez vérifier si 𝐻(𝑥)∗𝑍(𝑥) équivaut effectivement à 𝐹(𝑥+2)−𝐹(𝑥+1)−𝐹(𝑥), vous pouvez choisir une coordonnée aléatoire 𝑟, fournir des preuves d'ouverture d'engagement polynomiales prouvant 𝐻(𝑟), 𝑍(𝑟), 𝐹(𝑟), 𝐹(𝑟+1) et 𝐹(𝑟+2), et ensuite vérifier effectivement si 𝐻(𝑟)∗𝑍(𝑟) équivaut à 𝐹(𝑟+2)−𝐹(𝑟+1)−𝐹(𝑟). Si l'attaquant peut deviner la coordonnée à l'avance, l'attaquant peut tromper le système de preuve - c'est pourquoi elle doit être aléatoire. Mais cela signifie aussi que la coordonnée doit être échantillonnée dans un ensemble suffisamment grand pour que l'attaquant ne puisse pas la deviner par hasard. Si le module est proche de 2²⁵⁶, c'est clairement le cas. Mais avec un module de 2⁶⁴−2³²+1, we’re not quite there, and if we drop to 2³¹−1, ce n'est certainement pas le cas. Essayer de falsifier une preuve deux milliards de fois jusqu'à ce que l'on ait de la chance est absolument dans la gamme des capacités d'un attaquant.

Pour arrêter cela, nous échantillonnons 𝑟 à partir d'un champ d'extension. Par exemple, vous pouvez définir 𝑦 où 𝑦³=5, et prendre des combinaisons de 1, 𝑦 et 𝑦². Cela augmente le nombre total de coordonnées à environ 2⁹³La majeure partie des polynômes calculés par le prouveur ne vont pas dans ce champ d'extension ; ils utilisent simplement des entiers modulo 2³¹−1, et vous obtenez toujours toutes les efficacités d'utilisation du petit champ. Mais la vérification du point aléatoire et le calcul de FRI plongent dans ce champ plus grand, afin d'obtenir la sécurité nécessaire.

De petits nombres premiers à binaire

Les ordinateurs effectuent des opérations arithmétiques en représentant de plus grands nombres sous forme de séquences de zéros et de uns, et en construisant des "circuits" sur la base de ces bits pour calculer des opérations telles que l'addition et la multiplication. Les ordinateurs sont particulièrement optimisés pour effectuer des calculs avec des entiers de 16 bits, 32 bits et 64 bits. Des modules comme 2⁶⁴−2³²+1 et 2³¹−1 sont choisis non seulement parce qu'ils rentrent dans ces limites, mais aussi parce qu'ils s'alignent bien avec ces limites : vous pouvez faire une multiplication modulo 2⁶⁴−2³²+1 en effectuant une multiplication régulière de 32 bits, et décalant et copiant les sorties bit à bit à quelques endroits; cet article explique bien certaines des astuces.

Ce qui serait encore mieux, cependant, c'est de faire des calculs en binaire directement. Et si l'addition pouvait être simplement XOR, sans avoir à se soucier du 'report' du dépassement en ajoutant 1 + 1 dans une position de bit à la position de bit suivante? Et si la multiplication pouvait être plus parallélisable de la même manière? Et tous ces avantages viendraient en plus de pouvoir représenter les valeurs Vrai/Faux avec juste un bit.

Capturer directement ces avantages de la computation binaire est exactement ce que Binius essaie de faire. Un tableau de la présentation zkSummit de l'équipe Binius montre les gains d'efficacité :

Malgré une "taille" à peu près identique, une opération de champ binaire sur 32 bits nécessite 5 fois moins de ressources computationnelles qu'une opération sur le champ de Mersenne 31 bits.

Des polynômes univariés aux hypercubes

Supposons que nous soyons convaincus par ce raisonnement et voulions tout faire avec des bits (zéros et uns). Comment nous engageons-nous réellement à un polynôme représentant un milliard de bits ?

Ici, nous rencontrons deux problèmes pratiques:

1. Pour qu'un polynôme représente beaucoup de valeurs, ces valeurs doivent être accessibles lors des évaluations du polynôme : dans notre exemple de Fibonacci ci-dessus, 𝐹(0), 𝐹(1) … 𝐹(100), et dans un calcul plus important, les indices iraient jusqu'aux millions. Et le champ que nous utilisons doit contenir des nombres allant jusqu'à cette taille.

2. Prouver quoi que ce soit sur une valeur à laquelle nous nous engageons dans un arbre de Merkle (comme le font tous les STARKs) nécessite de l'encoder en Reed-Solomon : étendre 𝑛 valeurs en par exemple 8𝑛 valeurs, en utilisant la redondance pour empêcher un prouveur malveillant de tricher en falsifiant une valeur au milieu du calcul. Cela nécessite également d'avoir un champ suffisamment grand : pour étendre un million de valeurs à 8 millions, vous avez besoin de 8 millions de points différents auxquels évaluer le polynôme.

L’idée clé de Binius est de résoudre ces deux problèmes séparément, et de le faire en représentant les mêmes données de deux manières différentes. Tout d’abord, le polynôme lui-même. Les SNARK basés sur des courbes elliptiques, les STARK de l’ère 2019, Plonky2 et d’autres systèmes traitent généralement des polynômes sur une variable : F(x). Binius, quant à lui, s’inspire du protocole spartiate, et travaille avec des polynômes multivariés : F(x1,x2... xk). En fait, nous représentons l’ensemble de la trace computationnelle sur l'« hypercube » des évaluations où chaque xi est soit 0, soit 1. Par exemple, si nous voulions représenter une suite de nombres de Fibonacci, et que nous utilisions toujours un champ suffisamment grand pour les représenter, nous pourrions visualiser les seize premiers d’entre eux comme étant quelque chose comme ceci :

C'est-à-dire que 𝐹(0,0,0,0) serait 1, 𝐹(1,0,0,0) serait également 1, 𝐹(0,1,0,0) serait 2, et ainsi de suite, jusqu'à ce que nous arrivions à 𝐹(1,1,1,1)=987. Étant donné un hypercube d'évaluations, il existe exactement un polynôme multilinéaire (degré 1 dans chaque variable) qui produit ces évaluations. Ainsi, nous pouvons considérer cet ensemble d'évaluations comme représentant le polynôme ; nous n'avons jamais réellement besoin de nous embêter à calculer les coefficients.

Cet exemple est bien sûr uniquement à des fins d'illustration : en pratique, le but de se rendre dans un hypercube est de nous permettre de travailler avec des bits individuels. La méthode « Binius-native » pour compter les nombres de Fibonacci serait d'utiliser un cube de plus haute dimension, en utilisant chaque ensemble de par exemple 16 bits pour stocker un nombre. Cela nécessite de la finesse pour implémenter l'addition d'entiers par-dessus les bits, mais avec Binius, ce n'est pas trop difficile.

Maintenant, nous arrivons au codage d’effacement. La façon dont les STARK fonctionnent est la suivante : vous prenez n valeurs, Reed-Solomon les étend à un plus grand nombre de valeurs (souvent 8n, généralement entre 2n et 32n), puis sélectionnez au hasard des branches de Merkle dans l’extension et effectuez une sorte de vérification sur elles. Un hypercube a une longueur de 2 dans chaque dimension. Par conséquent, il n’est pas pratique de l’étendre directement : il n’y a pas assez d’espace pour échantillonner les branches de Merkle à partir de 16 valeurs. Alors, qu’est-ce qu’on fait à la place ? On fait comme si l’hypercube était un carré !

Simple Binius - un exemple

Voir icipour une implémentation en python de ce protocole.

Passons par un exemple, en utilisant des entiers réguliers comme notre champ pour des raisons de commodité (dans une implémentation réelle, il s'agira d'éléments de champ binaire). Tout d'abord, nous prenons l'hypercube auquel nous voulons nous engager, et l'encodons comme un carré :

Maintenant, nous étendons Reed-Solomon le carré. C'est-à-dire, nous traitons chaque ligne comme étant un polynôme de degré 3 évalué à x = {0, 1, 2, 3}, et évaluons le même polynôme à x = {4, 5, 6, 7} :

Remarquez que les nombres explosent rapidement ! C'est pourquoi dans une implémentation réelle, nous utilisons toujours un champ fini pour cela, au lieu d'entiers réguliers : si nous utilisions des entiers modulo 11, par exemple, l'extension de la première ligne serait simplement [3, 10, 0, 6].

Si vous voulez jouer avec l'extension et vérifier les chiffres ici vous-même, vous pouvez utiliser mon code d'extension Reed-Solomon simple ici.

Ensuite, nous traitons cette extension comme des colonnes et créons un arbre de Merkle des colonnes. La racine de l'arbre de Merkle est notre engagement.

Supposons maintenant que le prouveur veuille prouver une évaluation de ce polynôme à un moment donné r={r0,r1,r2,r3}. Il y a une nuance dans Binius qui le rend un peu plus faible que les autres schémas d’engagement polynomial : le prouveur ne doit pas connaître, ou être capable de deviner, s, jusqu’à ce qu’il se soit engagé dans la racine de Merkle (en d’autres termes, r devrait être une valeur pseudo-aléatoire qui dépend de la racine de Merkle). Cela rend le schéma inutile pour la « recherche dans la base de données » (par exemple. « ok tu m’as donné la racine de Merkle, maintenant prouve-moi P(0,0,1,0) ! »). Mais les protocoles de preuve à divulgation nulle de connaissance que nous utilisons n’ont généralement pas besoin d’une « recherche dans la base de données » ; Ils ont simplement besoin de vérifier le polynôme à un point d’évaluation aléatoire. Par conséquent, cette restriction est acceptable pour nos besoins.

Supposons que nous choisissons 𝑟={1,2,3,4} (le polynôme, à ce stade, évalue à -137; vous pouvez le confirmeravec ce code. Maintenant, nous entrons dans le processus de fabrication de la preuve. Nous divisons 𝑟 en deux parties : la première partie {1,2} représentant une combinaison linéaire des colonnes dans une ligne, et la deuxième partie {3,4} représentant une combinaison linéaire des lignes. Nous calculons un "produit tensoriel", à la fois pour la partie colonne :

Et pour la partie rangée:

Ce que cela signifie, c'est : une liste de tous les produits possibles d'une valeur de chaque ensemble. Dans le cas de la ligne, nous obtenons :

[(1-r2)(1-r3), (1-r3), (1-r2)r3, r2*r3]

Utilisez r={1,2,3,4} (donc r2=3 et r3=4):

[(1-3)(1-4), 3(1-4),(1-3)4,34] = [6, -9 -8 -12]

Maintenant, nous calculons une nouvelle “rangée” 𝑡′, en prenant cette combinaison linéaire des rangées existantes. Autrement dit, nous prenons :

Vous pouvez voir ce qui se passe ici comme une évaluation partielle. Si nous devions multiplier le produit tensoriel complet ⨂𝑖=03(1−𝑟𝑖,𝑟𝑖) par le vecteur complet de toutes les valeurs, vous obtiendriez l'évaluation 𝑃(1,2,3,4)=−137. Ici, nous multiplions un produit tensoriel partiel qui n'utilise que la moitié des coordonnées d'évaluation, et nous réduisons une grille de 𝑁 valeurs à une ligne de 𝑁 valeurs. Si vous donnez cette ligne à quelqu'un d'autre, il peut utiliser le produit tensoriel de l'autre moitié des coordonnées d'évaluation pour compléter le reste du calcul.

Le prouveur fournit au vérificateur cette nouvelle ligne, 𝑡′, ainsi que les preuves de Merkle de certaines colonnes échantillonnées aléatoirement. Il s'agit de données 𝑂(𝑁). Dans notre exemple illustratif, le prouveur fournira simplement la dernière colonne; dans la vraie vie, le prouveur devrait fournir quelques dizaines de colonnes pour garantir une sécurité adéquate.

Maintenant, nous tirons parti de la linéarité des codes de Reed-Solomon. La propriété clé que nous utilisons est la suivante : prendre une combinaison linéaire d'une extension de Reed-Solomon donne le même résultat qu'une extension de Reed-Solomon d'une combinaison linéaire. Ce genre de « indépendance de l'ordre » se produit souvent lorsque vous avez deux opérations qui sont toutes deux linéaires.

Le vérificateur fait exactement cela. Ils calculent l'extension de 𝑡′, et ils calculent la même combinaison linéaire de colonnes que le prouveur avait calculée auparavant (mais seulement sur les colonnes fournies par le prouveur), et vérifient que ces deux procédures donnent la même réponse.

Dans ce cas, en étendant 𝑡′, et en calculant la même combinaison linéaire ([6,−9,−8,12]) de la colonne, donnent toutes les deux la même réponse: −10746. Cela prouve que la racine de Merkle a été construite "de bonne foi" (ou du moins "assez proche"), et elle correspond à 𝑡′: au moins la grande majorité des colonnes sont compatibles les unes avec les autres et avec 𝑡′.

Mais le vérificateur doit encore vérifier une chose de plus : en fait, vérifiez l'évaluation du polynôme à {𝑟0..𝑟3}. Jusqu'à présent, aucune des étapes du vérificateur ne dépendait réellement de la valeur que le prouveur a prétendue. Voici comment nous procédons à cette vérification. Nous prenons le produit tensoriel de ce que nous avons étiqueté comme la partie "colonne" du point d'évaluation :

Dans notre exemple, où r={1,2,3,4} donc la moitié de la colonne sélectionnée est {1,2}), cela équivaut :

Donc maintenant nous prenons cette combinaison linéaire de 𝑡′:

Ce qui équivaut exactement à la réponse que vous obtenez si vous évaluez le polynôme directement.

Ce qui précède est assez proche d'une description complète du protocole "simple" Binius. Cela présente déjà certains avantages intéressants : par exemple, parce que les données sont divisées en lignes et colonnes, vous n'avez besoin que d'un champ de moitié la taille. Mais cela ne se rapproche pas de la réalisation des avantages complets de la réalisation de calculs en binaire. Pour cela, nous aurons besoin du protocole Binius complet. Mais d'abord, approfondissons notre compréhension des champs binaires.

Champ binaire

Le plus petit champ possible est l'arithmétique modulo 2, si petit que nous pouvons écrire ses tables d'addition et de multiplication :

Nous pouvons créer des champs binaires plus grands en prenant des extensions : si nous commençons avec 𝐹2 (entiers modulo 2) et définissons ensuite 𝑥 où 𝑥2=𝑥+1, nous obtenons le tableau d'addition et de multiplication suivant :

Il s'avère que nous pouvons étendre le champ binaire à des tailles arbitrairement grandes en répétant cette construction. Contrairement aux nombres complexes sur les réels, où vous pouvez ajouter un nouvel élément 𝑖, mais vous ne pouvez pas en ajouter davantage (les quaternions existent, mais ils sont mathématiquement étranges, par exemple 𝑎𝑏≠𝑏𝑎), avec des champs finis, vous pouvez continuer à ajouter de nouvelles extensions à l'infini. Plus précisément, nous définissons les éléments comme suit :

Et ainsi de suite. Cela est souvent appelé la construction en tour, en raison de la façon dont chaque extension successive peut être considérée comme ajoutant une nouvelle couche à une tour. Ce n'est pas la seule façon de construire des champs binaires de taille arbitraire, mais elle présente certains avantages uniques dont Binius profite.

Nous pouvons représenter ces nombres sous forme de liste de bits, par exemple 1100101010001111. Le premier bit représente les multiples de 1, le deuxième bit représente les multiples de 𝑥0, puis les bits suivants représentent les multiples de : 𝑥1, 𝑥1∗𝑥0, 𝑥2, 𝑥2∗𝑥0, et ainsi de suite. Ce codage est pratique car vous pouvez le décomposer :

Il s'agit d'une notation relativement rare, mais j'aime représenter les éléments de champ binaire sous forme d'entiers, en prenant la représentation en bits où les bits plus significatifs sont à droite. Autrement dit, 1=1, 𝑥₀=01=2, 1+𝑥₀=11=3, 1+𝑥₀+𝑥₂=11001000=19, et ainsi de suite. 1100101010001111 est, dans cette représentation, 61779.

L'addition dans un champ binaire est simplement XOR (comme le fait la soustraction, d'ailleurs); notez que cela signifie que x+x=0 pour n'importe quel x. Pour multiplier deux éléments x*y, il existe un algorithme récursif très simple : divisez chaque nombre en deux moitiés :

Ensuite, divisez la multiplication:

La dernière pièce est la seule légèrement délicate, car vous devez appliquer la règle de réduction et remplacer 𝑅𝑥∗𝑅𝑦∗𝑥𝑘2 par 𝑅𝑥∗𝑅𝑦∗(𝑥𝑘−1∗𝑥𝑘+1). Il existe des moyens plus efficaces de faire des multiplications, des analogues de l'algorithme de Karatsuba et des transformations de Fourier rapides, mais je laisserai à l'intéressé le soin de les découvrir.

La division dans les champs binaires est effectuée en combinant la multiplication et l'inversion. La manière "simple mais lente" de faire l'inversion est une application du petit théorème de Fermat généralisé. Il existe également un algorithme d'inversion plus compliqué mais plus efficace, que vous pouvez trouver ici. Vous pouvez utiliser le code icijouer avec l'addition, la multiplication et la division de champs binaires vous-même.

Left: table d'addition pour les éléments de champ binaire à quatre bits (c'est-à-dire des éléments composés uniquement de combinaisons de 1, 𝑥₀，𝑥₁et 𝑥₀𝑥₁).

Bon : table de multiplication pour les éléments du champ binaire à quatre bits.

La belle chose à propos de ce type de champ binaire est qu'il combine certaines des meilleures parties des entiers "réguliers" et de l'arithmétique modulaire. Comme les entiers réguliers, les éléments du champ binaire sont illimités : vous pouvez continuer à étendre autant que vous le souhaitez. Mais comme l'arithmétique modulaire, si vous effectuez des opérations sur des valeurs dans une certaine limite de taille, toutes vos réponses restent également dans la même limite. Par exemple, si vous prenez des puissances successives de 42, vous obtenez :

Après 255 étapes, vous êtes de retour à 42²⁵⁵= 1. Tout comme les entiers positifs et l'arithmétique modulaire, ils suivent les lois mathématiques habituelles : ab=ba, a(b+c)=a b+a*c, il y a même de nouvelles lois étranges.

Enfin, les champs binaires facilitent la manipulation des bits : si vous effectuez des opérations mathématiques avec des nombres qui correspondent à 2^kbits, alors toute votre sortie s'adaptera également à 2 k bits. Cela évite l'embarras. Dans l'EIP-4844 d'Ethereum, chaque “bloc” d'un blob doit être un module numérique 52435875175126190479447740508185965837690552500527637822603658699938581184513, donc encoder les données binaires nécessite de jeter un certain espace et de faire un contrôle supplémentaire pour s'assurer que chaque élément stocke une valeur inférieure à 2²⁴⁸. Cela signifie également que les opérations de champ binaire sont très rapides sur les ordinateurs - à la fois les CPU et les conceptions FPGA et ASIC théoriquement optimales.

Ce que tout cela signifie, c'est que nous pouvons faire quelque chose comme le codage de Reed-Solomon que nous avons fait ci-dessus, d'une manière qui évite complètement l'“explosion” des entiers, comme nous l'avons vu dans notre exemple, et de manière très “explosive”. Manière “native”, le genre de calcul que les ordinateurs excellent. L'attribut “split” des champs binaires - comment nous le faisons 1100101010001111=11001010+10001111*x₃et puis le diviser selon nos besoins est également crucial pour obtenir beaucoup de flexibilité.

Full Binius

Voir icipour une implémentation python de ce protocole.

Maintenant, nous pouvons passer au "Binius complet", qui ajuste le "Binius simple" pour (i) fonctionner sur des champs binaires, et (ii) nous permettre de nous engager sur des bits individuels. Ce protocole est difficile à comprendre, car il passe continuellement d'un point de vue à un autre sur une matrice de bits; il m'a certainement fallu plus de temps pour le comprendre que pour comprendre habituellement un protocole cryptographique. Mais une fois que vous comprenez les champs binaires, la bonne nouvelle est qu'il n'y a pas de "mathématiques plus difficiles" sur lesquelles Binius dépend. Ce n'est pas des appariements de courbes elliptiques, où il y a des dédales de géométrie algébrique de plus en plus profonds à explorer; ici, les champs binaires sont tout ce dont vous avez besoin.

Revenons à nouveau sur le diagramme complet :

À ce stade, vous devriez être familier avec la plupart des composants. L'idée de "aplatir" un hypercube dans une grille, l'idée de calculer une combinaison de lignes et une combinaison de colonnes en tant que produits tensoriels du point d'évaluation, et l'idée de vérifier l'équivalence entre "étendre Reed-Solomon puis calculer la combinaison de lignes" et "calculer la combinaison de lignes puis étendre Reed-Solomon", étaient tous dans le simple Binius.

Quoi de neuf dans « Gate complet »? Fondamentalement trois choses :

• Les valeurs individuelles dans l'hypercube et dans le carré doivent être des bits (0 ou 1)
• Le processus d'extension étend les bits en plus de bits, en regroupant les bits en colonnes et en prétendant temporairement qu'ils sont de plus grands éléments de champ
• Après l'étape de combinaison de lignes, il y a une étape de « décomposition en bits » élément par élément, qui convertit l'extension en bits

Nous passerons en revue les deux tour à tour. Tout d'abord, la nouvelle procédure d'extension. Un code de Reed-Solomon a la limitation fondamentale que si vous étendez 𝑛 valeurs à 𝑘∗𝑛 valeurs, vous devez travailler dans un champ qui a 𝑘∗𝑛 différentes valeurs que vous pouvez utiliser comme coordonnées. Avec 𝐹₂(alias, bits), vous ne pouvez pas faire cela. Et donc ce que nous faisons, c'est que nous “emballons” les voisins 𝐹₂rassembler les éléments en des valeurs plus grandes. Dans l'exemple ici, nous regroupons deux bits à la fois dans des éléments de {0,1,2,3}, car notre extension ne comporte que quatre points d'évaluation et c'est donc suffisant pour nous. Dans une preuve "réelle", nous regrouperions probablement 16 bits à la fois. Ensuite, nous appliquons le code de Reed-Solomon à ces valeurs regroupées, et les décompressons à nouveau en bits.

Maintenant, la combinaison de lignes. Pour rendre les vérifications "évaluer à un point aléatoire" cryptographiquement sécurisées, nous avons besoin que ce point soit échantillonné à partir d'un espace assez grand, beaucoup plus grand que l'hypercube lui-même. Ainsi, alors que les points à l'intérieur de l'hypercube sont des bits, les évaluations à l'extérieur de l'hypercube seront beaucoup plus grandes. Dans notre exemple ci-dessus, la "combinaison de lignes" se révèle être [11,4,6,1].

Cela pose un problème : nous savons comment combiner des paires de bits pour former une valeur plus grande, puis effectuer une extension de Reed-Solomon, mais comment faites-vous la même chose avec des paires de valeurs beaucoup plus grandes ?

Le truc dans Binius consiste à le faire bit à bit : nous regardons les bits individuels de chaque valeur (par exemple, pour ce que nous avons étiqueté comme "11", c'est [1,1,0,1]), puis nous étendons ligne par ligne. C'est-à-dire que nous effectuons la procédure d'extension sur la ligne 1 de chaque élément, puis sur la ligne 𝑥0, puis sur le "𝑥"₁“ rangée, puis sur le 𝑥₀∗𝑥₁ligne, et ainsi de suite (eh bien, dans notre exemple simplifié, nous nous arrêtons là, mais dans une implémentation réelle, nous irions jusqu'à 128 lignes (la dernière étant 𝑥₆∗ …∗ 𝑥₀)).

Récapitulatif:

• Nous prenons les bits dans l'hypercube et les convertissons en une grille
• Ensuite, nous traitons les groupes de bits adjacents sur chaque ligne comme des éléments de champ plus grands, et effectuons des opérations arithmétiques sur eux pour étendre les lignes de Reed-Solomon
• Ensuite, nous prenons une combinaison de rangée de chaque colonne de bits, et obtenons une colonne de bits (beaucoup plus petite pour les carrés plus grands que 4x4) pour chaque rangée en tant que sortie
• Ensuite, nous regardons la sortie comme une matrice et traitons à nouveau les bits comme des lignes

Pourquoi est-ce que cela fonctionne? En mathématiques « normales », la capacité à effectuer (souvent) des opérations linéaires dans n'importe quel ordre et obtenir le même résultat cesse de fonctionner si vous commencez à découper un nombre en chiffres. Par exemple, si je commence avec le nombre 345, et que je le multiplie par 8 puis par 3, j'obtiens 8280, et si je fais ces deux opérations dans l'ordre inverse, j'obtiens également 8280. Mais si j'insère une opération de « découpe par chiffre » entre les deux étapes, cela se décompose : si vous faites 8x puis 3x, vous obtenez :

Mais si vous faites 3x, puis 8x, vous obtenez :

Mais dans un champ binaire construit avec une structure en tour, cette approche fonctionne. La raison réside dans leur séparabilité : si vous multipliez une grande valeur par une petite valeur, ce qui se passe sur chaque segment reste sur chaque segment. Si nous multiplions 1100101010001111 par 11, c'est la même chose que la première factorisation de 1100101010001111, qui est

Et puis multiplier chaque composant par 11 séparément.

Mettre tout cela ensemble

En général, les systèmes de preuve de connaissance zéro fonctionnent en faisant des déclarations sur des polynômes qui représentent simultanément des déclarations sur les évaluations sous-jacentes : tout comme nous l'avons vu dans l'exemple de Fibonacci, 𝐹(𝑋+2)−𝐹(𝑋+1)−𝐹(𝑋)=𝑍(𝑋)∗𝐻(𝑋) vérifie simultanément toutes les étapes du calcul de Fibonacci. Nous vérifions des déclarations sur des polynômes en prouvant des évaluations à un point aléatoire. Cette vérification à un point aléatoire remplace la vérification du polynôme entier : si l'équation polynomiale ne correspond pas, la probabilité qu'elle corresponde à une coordonnée aléatoire spécifique est minime.

En pratique, une source majeure d'inefficacité provient du fait que, dans les vrais programmes, la plupart des nombres avec lesquels nous travaillons sont minuscules : indices dans les boucles for, valeurs Vrai/Faux, compteurs et choses similaires. Mais lorsque nous « étendons » les données en utilisant le codage Reed-Solomon pour leur donner la redondance nécessaire pour rendre les vérifications basées sur la preuve de Merkle sûres, la plupart des valeurs « supplémentaires » finissent par prendre la taille totale d'un champ, même si les valeurs d'origine sont petites.

Pour contourner cela, nous voulons rendre le champ aussi petit que possible. Plonky2 nous a fait passer de nombres sur 256 bits à des nombres sur 64 bits, puis Plonky3 est allé plus loin pour atteindre 31 bits. Mais même cela est suboptimal. Avec des champs binaires, nous pouvons travailler sur des bits individuels. Cela rend le codage "dense" : si vos données sous-jacentes réelles ont n bits, alors votre codage aura n bits, et l'extension aura 8 * n bits, sans surcharge supplémentaire.

Maintenant, regardons le diagramme une troisième fois :

Dans Binius, nous nous engageons à un polynôme multilinéaire : un hypercube 𝑃(x₀,x₁,…x_k) où les évaluations individuelles 𝑃(0,0…0), 𝑃(0,0…1) jusqu'à 𝑃(1,1,…1) contiennent les données qui nous intéressent. Pour prouver une évaluation à un point, nous « réinterprétons » les mêmes données sous forme de carré. Nous étendons ensuite chaque ligne, en utilisant un codage Reed-Solomon sur des groupes de bits, pour donner aux données la redondance nécessaire pour que les requêtes aléatoires de branches Merkle soient sécurisées. Nous calculons ensuite une combinaison linéaire aléatoire des lignes, avec des coefficients conçus de manière à ce que la nouvelle ligne combinée contienne effectivement l'évaluation qui nous intéresse. Cette nouvelle ligne créée (qui est réinterprétée comme 128 lignes de bits) ainsi que quelques colonnes sélectionnées aléatoirement avec des branches Merkle sont transmises au vérificateur.

Le vérificateur effectue ensuite une « combinaison de rang de l'extension » (ou plutôt, quelques colonnes de l'extension), et une « extension de la combinaison de rang », et vérifie que les deux correspondent. Ils calculent ensuite une combinaison de colonnes, et vérifient qu'elle renvoie la valeur que le prouveur revendique. Et voilà notre système de preuve (ou plutôt, le schéma d'engagement polynomial, qui est le bloc de construction clé d'un système de preuve).

Qu'avons-nous oublié de couvrir?

• Des algorithmes efficaces pour étendre les lignes, qui sont nécessaires pour réellement améliorer l'efficacité computationnelle du vérificateur. Nous utilisons des transformations de Fourier rapides sur des champs binaires, décrits ici(bien que l'implémentation exacte sera différente, car ce post utilise une construction moins efficace non basée sur une extension récursive).
• Arithmétisation. Les polynômes univariés sont pratiques car vous pouvez faire des choses comme F(X+2)-F(X+1)-F(X) = Z(X)*H(X) pour relier les étapes adjacentes dans le calcul. Dans un hypercube, “l'étape suivante” est beaucoup moins interprétable que “X+1”. Vous pourriez faire X+k, des puissances de k, mais ce comportement de saut sacrifierait bon nombre des principaux avantages de Binius. La solution est présentée dans le Papier Binius(Voir la section 4.3), mais c'est un vrai labyrinthe en soi.
• Comment effectuer en toute sécurité des vérifications de valeurs spécifiques. L'exemple de Fibonacci nécessite de vérifier les conditions limites des clés : F(0)=F(1)=1 et la valeur de F(100). Mais avec Binius "brut", il est insécuritaire de vérifier aux points d'évaluation préconnus. Il existe des moyens assez simples de convertir une vérification d'évaluation connue en une vérification d'évaluation inconnue, en utilisant ce qu'on appelle des protocoles de vérification de sommes; mais nous n'aborderons pas ce sujet ici.
• Les protocoles de recherche, une autre technologie qui a récemment gagné en utilisation comme moyen de rendre les systèmes de preuve ultra-efficaces. Binius peut être combiné avec les protocoles de recherche pour de nombreuses applications.
• Dépassant le temps de vérification de la racine carrée. La racine carrée est coûteuse : une preuve Binius de bits fait environ 11 Mo. Vous pouvez remédier à cela en utilisant un autre système de preuve pour faire une « preuve d'une preuve Binius », ce qui vous permet de bénéficier à la fois de l'efficacité de Binius dans la démonstration de l'énoncé principal et d'une taille de preuve réduite. Une autre option est le protocole FRI-Binius beaucoup plus compliqué, qui crée une preuve de taille polylogarithmique (comme FRI régulier).
• Comment Binius affecte ce qui compte comme étant "SNARK-friendly". Le résumé de base est que, si vous utilisez Binius, vous n'avez plus besoin de vous soucier autant de rendre le calcul "arithmétique convivial": les hachages "réguliers" ne sont plus plus efficaces que les hachages arithmétiques traditionnels, la multiplication modulo ou modulo n'est plus un gros casse-tête par rapport à la multiplication modulo , et ainsi de suite. Mais c'est un sujet compliqué; beaucoup de choses changent lorsque tout est fait en binaire.

Je m'attends à de nombreuses autres améliorations dans les techniques de preuve basées sur les champs binaires dans les mois à venir.

Avertissement：

1. Cet article est repris de [GatePanews] Gate. Transmettre le titre original 'Vitalik explique Binius: un système de preuve efficace basé sur des champs binaires'. Tous les droits d'auteur appartiennent à l'auteur original [GateVitalik Buterin*]. If there are objections to this reprint, please contact the Porte Apprendreéquipe, et ils s'en occuperont rapidement.
2. Clause de non-responsabilité : Les points de vue et opinions exprimés dans cet article sont uniquement ceux de l'auteur et ne constituent aucun conseil en investissement.
3. Les traductions de l'article dans d'autres langues sont effectuées par l'équipe Gate Learn. Sauf mention contraire, la copie, la distribution ou le plagiat des articles traduits sont interdits.