Initialement publié en anglais par StarkWare le 20 février, 2019.

Voici la deuxième partie de notre série sur les mathématiques des STARKs (première partie ici), et le premier des deux posts sur l'arithmétique.

À la fin de cet article, vous devriez avoir une bonne idée de ce que sont la trace d'exécution et les contraintes polynomiales, et de la façon dont une déclaration d'intégrité informatique est transformée en ces dernières. Nous commencerons par un exemple simple, celui d'un ticket de caisse de supermarché, puis nous passerons à un exemple légèrement plus complexe, celui des séquences de Collatz, qui se rapporte à un problème ouvert bien connu en théorie des nombres. Nous supposerons une familiarité de base avec des polynômes finis et les représentations binaires des entiers.

.

L'objectif du protocole STARK est de vérifier les calculs de manière succincte et transparente. La première étape STARK est appelée arithmétisation et consiste à traduire (souvent appelée "réduction") le problème de la vérification d'un calcul en un problème consistant à vérifier qu'un certain polynôme, qui peut être évalué efficacement du côté du vérifieur (c'est la partie "succincte"), est de faible degré. L'arithmétisation est utile car elle permet l'utilisation d'outils issus du domaine des codes de correction d'erreurs qui testent efficacement le faible degré. Cependant, l'arithmétisation elle-même ne fait que traduire une déclaration d'intégrité informatique en un polynôme, ce qui prépare le terrain pour la phase suivante de STARK, qui est un autre protocole interactif dans lequel un prouveur tente de convaincre un vérificateur que le polynôme est effectivement de faible degré. Le vérificateur est convaincu que le polynôme est de faible degré si et seulement si le calcul original est correct (sauf pour une probabilité infinitésimale). Dans la dernière étape STARK, le protocole interactif est transformé en une preuve unique non interactive, qui peut être publiée sur une blockchain et vérifiée publiquement par n'importe qui.

L'arithmétisation elle-même est composée de deux étapes : la première consiste à générer une trace d'exécution et des contraintes polynomiales, la seconde à transformer ces deux objets en un seul polynôme de faible degré. En termes d'interaction entre le prouveur et le verificateur, se mettent d'accord à l'avance sur les contraintes polynomiales. Le prouveur génère alors une trace d'exécution, et dans l'interaction suivante, le prouveur tente de convaincre le vérificateur que les contraintes polynomiales sont satisfaites sur cette trace d'exécution, sans que le vérificateur ne le voit.

Dans le post précédent, nous avons discuté de la notion d'une déclaration d'intégrité informatique (CI = Computational Integrity), l'affirmation que la sortie d'un certain calcul est correcte, d'un point de vue abstrait. Voyons un exemple concret d'une déclaration d'intégrité informatique : la somme totale que nous devons payer au supermarché a été calculée correctement. La preuve conventionnelle de cette affirmation particulière est le ticket de caisse. En général, les articles figurant sur le ticket de caisse sont énumérés avec leur prix, et la somme totale est indiquée en bas, comme suit :

Pour simplifier, nous considérons qu'il s'agit uniquement d'une affirmation selon laquelle la somme est correcte. Pour voir si cette affirmation du CI est valable, on peut parcourir la liste - sans sauter aucun article - pour calculer la somme totale et la comparer au chiffre figurant au bas du reçu. Il s'agit d'un exemple très naïf, mais nous l'utiliserons plus loin dans cet article pour démontrer l'idée de testabilité succincte.

La première étape de l'arithmétisation consiste à prendre un certain énoncé du CI (tel que "la cinquième transaction du bloc 7218290 est correcte") et à le traduire en langage algébrique formel. Cela sert deux objectifs :

1. définir l'affirmation de manière succincte et non ambiguë,

2. intégrer l'affirmation dans un domaine algébrique.

Cette intégration est ce qui permet la deuxième étape de l'arithmétisation, qui réduit l'énoncé de l'CI à une affirmation sur le degré d'un polynôme spécifique.

La représentation algébrique que nous utilisons à deux composantes principales :

1. une trace d'exécution

2. un ensemble de contraintes polynomiales.

La trace d'exécution est un tableau qui représente les étapes du calcul sous-jacent, où chaque ligne représente une seule étape. L'ensemble de contraintes polynomiales est construit de telle sorte que toutes les contraintes sont satisfaites si et seulement si la trace représente un calcul valide. Bien que la trace d'exécution puisse être très longue, nous travaillerons avec un ensemble succinct de contraintes polynomiales.

Trace d'exécution

Le type de trace d'exécution que nous cherchons à générer doit avoir la particularité d'être succinctement testable - chaque ligne peut être vérifiée en se basant uniquement sur les lignes qui lui sont proches dans la trace, et la même procédure de vérification est appliquée à chaque paire de lignes. Ce trait affecte directement la taille de la preuve. Pour illustrer ce que nous entendons par "testable succinctement", revenons au ticket de caisse du supermarché et ajoutons une colonne supplémentaire pour le total courant :

Cette simple addition nous permet de vérifier chaque ligne individuellement, étant donné sa ligne précédente.

Nous pouvons, par exemple, examiner ces deux lignes :

Et être convaincu que cette étape particulière du calcul (c'est-à-dire le nombre 16,41) est correcte puisque 12,96+3,45=16,41. Remarquez que la même contrainte est appliquée à chaque paire de lignes. C'est ce que nous entendons par contraintes succinctes.

Contraintes polynomiales

Réécrivons le ticket de caisse du supermarché (avec le total courant) sous la forme d'un tableau :

Désignons la valeur de la cellule de la i-ème ligne et de la j-ème colonne par Ai,j (nous désignerons les indices de cette façon car Medium ne supporte pas LaTeX). Nous pouvons maintenant reformuler les conditions de correction comme cet ensemble de contraintes polynomiales :

Ce sont des contraintes polynomiales linéaires dans Ai,j. Si l'ensemble de contraintes polynomiales que nous utilisons est d'un degré élevé, cela a un effet négatif sur la longueur de la preuve et le temps qu'il faut pour la générer. Par conséquent, les contraintes linéaires sont ce que nous pouvons espérer de mieux. Remarquez que (2) est en réalité une seule contrainte appliquée plusieurs fois, et la taille totale de l'ensemble est indépendante de la longueur de la preuve.

En résumé, nous avons pris un problème de vérification d'un ticket de caisse de supermarché, et l'avons transformé en une trace d'exécution succinctement testable, et un ensemble correspondant de contraintes polynomiales qui tiennent si et seulement si la somme totale dans le ticket de caisse original est correcte.

Voyons un exemple plus complexe.

La conjecture de Collatz

En 1937, un mathématicien allemand nommé Lothar Collatz a présenté une conjecture dans le domaine de la théorie des nombres. À première vue, cette conjecture pourrait sembler n'être qu'une jolie énigme mathématique, mais il s'agit en fait d'un problème ouvert difficile en théorie des nombres. Elle a attiré l'attention de nombreux mathématiciens au fil des ans et a acquis de nombreux synonymes (par exemple, la conjecture 3n + 1, la conjecture d'Ulam, le problème de Kakutani et bien d'autres). Paul Erdős a dit un jour à propos de cette conjecture : "Les mathématiques ne sont peut-être pas prêtes pour de tels problèmes".

Une séquence de Collatz commence par un entier positif quelconque, où chaque élément suivant de la séquence est obtenu à partir du précédent de la manière suivante :

• Si l'élément précédent est pair : divisez-le par 2.

• Si l'élément précédent est impair et supérieur à 1 : le multiplier par 3 et ajouter 1.

• Si l'élément précédent est 1, arrêtez-vous.

Prenons un exemple simple où le terme initial est 52 :

52 -> 26 -> 13 -> 40 -> 20 -> 10 -> 5 -> 16 -> 8 -> 4 -> 2 -> 1.

Conjecture de Collatz : pour tout entier positif par lequel on commence, la suite atteint toujours 1.

Malheureusement, la résolution de la conjecture de Collatz dépasse le cadre de cet article. Nous allons plutôt nous pencher sur le problème de la vérification d'un calcul qui vérifie la conjecture pour un entier de départ particulier.

La trace d'exécution de la séquence de Collatz

L'énoncé de l'CI est : "Une séquence de Collatz qui commence par 52, se termine par 1 après 11 itérations".

Soit A la trace d'exécution du calcul de la séquence. La i-ème ligne, désignée par Ai, représente le i-ème nombre de la séquence. Tous les nombres sont représentés sous forme de chaînes binaires, afin de faciliter l'expression de la condition paire/impaire avec des polynômes. Ai,j est égal au ji-ème bit le moins significatif du i-ème nombre de la séquence. Par exemple, A0=001011 : le premier terme est 52, sa représentation binaire est 110100 et ensuite on inverse l'ordre des bits (l'ordre d'inversion des bits simplifie l'indexation dans la notation des contraintes polynomiales).

Voici la trace d'exécution de la séquence de Collatz ci-dessus qui commence par 52 :

Notez qu'ici la trace a 6 colonnes car 6 bits sont suffisants pour représenter même le plus grand nombre de la séquence. Si nous avions commencé la séquence avec 51, le nombre suivant aurait été 154, donc la trace d'une telle séquence aurait nécessité au moins 8 colonnes.

Les contraintes polynomiales de la séquence de Collatz

Rappelons que les contraintes polynomiales que nous recherchons sont telles qu'elles sont toutes satisfaites si et seulement si l’origine de A décrit la séquence de Collatz donnée (commençant par 52, se terminant par 1, et la transition entre deux lignes consécutives est effectuée correctement). Dans notre exemple, l’origine A est de taille 6x12, c'est-à-dire qu'elle représente une séquence de Collatz de 12 nombres de 6 bits. L'ensemble des contraintes polynomiales est le suivant (n=12, m=6) :

Passons en revue chacune de ces contraintes. Les trois premières sont simples :

(1) est valable si et seulement si la première ligne est une représentation binaire de 52.

(2) est valable si et seulement si la dernière ligne est une représentation binaire de 1.

(3) est valable si et seulement si la trace ne contient que des bits (un nombre est égal à son carré si et seulement s'il vaut 0 ou 1).

Le quatrième ensemble de contraintes définit le cœur du calcul succinct de la séquence, c'est-à-dire le lien entre deux lignes consécutives. La capacité d'exprimer les contraintes de calcul comme un modèle récurrent de contraintes locales (c'est-à-dire la succinctivité) est fondamentale pour que le vérificateur soit exponentiellement plus rapide qu'un rejeu naïf du calcul.

Examinons attentivement les contraintes elles-mêmes.

Pour tout i<n-1, dénote :

Par conséquent, pour chaque i<n-1, nous obtenons la contrainte suivante :

Ai,0 est le bit le moins significatif du i-ème nombre, qui détermine sa parité en tant qu'entier, donc cette contrainte décrit la règle de la séquence de Collatz.

En résumé, toutes les contraintes sont satisfaites si et seulement si l’origine représente un calcul valide d'une séquence de Collatz.

Notez que toute séquence de Collatz de longueur n, peut être représentée en utilisant une trace de taille n*m où m est le nombre maximum de bits dans la représentation d'un nombre de la séquence, et les contraintes polynomiales correspondantes sont modifiées en conséquence. Notez que les contraintes polynomiales ne croissent pas avec n et m, mais restent simples et concises.

Étant donné un premier terme spécifique pour une séquence de Collatz, un simple programme informatique peut produire la trace d'exécution et les contraintes polynomiales.

Conclusion

Dans ce post, nous avons couvert la première étape de l'arithmétisation des instructions CI.

Nous avons vu comment une déclaration CI sur une séquence de Collatz peut être transformée en une origine d'exécution et un ensemble de contraintes polynomiales décrites succinctement. Des méthodes similaires peuvent être utilisées pour transformer n'importe quel calcul, et en général, n'importe quelle déclaration CI peut être traduite sous cette forme. Les détails, cependant, ont une grande importance. Bien qu'il existe de nombreuses façons dont une origine d'exécution (et un ensemble de contraintes polynomiales) peut décrire un calcul spécifique, seule une poignée d'entre elles donne lieu à une petite preuve STARK qui peut être construite efficacement. Une grande partie des efforts de StarkWare est consacrée à la conception de réductions qui conduisent à de bonnes contraintes polynomiales, que nous appelons AIR (Algebraic Intermediate Representation), car une grande partie des performances de nos systèmes en dépend.

Dans le prochain article, nous aborderons la deuxième étape de l'arithmétisation - la transformation de la trace d'exécution et des contraintes polynomiales en un seul polynôme, dont le faible degré est garanti, si et seulement si le calcul original est correct.

Kineret Segal & Shir Peled

StarkWare

Initialement publié en anglais par StarkWare le 20 février, 2019.

Voici la deuxième partie de notre série sur les mathématiques des STARKs (première partie ici), et le premier des deux posts sur l'arithmétique.

À la fin de cet article, vous devriez avoir une bonne idée de ce que sont la trace d'exécution et les contraintes polynomiales, et de la façon dont une déclaration d'intégrité informatique est transformée en ces dernières. Nous commencerons par un exemple simple, celui d'un ticket de caisse de supermarché, puis nous passerons à un exemple légèrement plus complexe, celui des séquences de Collatz, qui se rapporte à un problème ouvert bien connu en théorie des nombres. Nous supposerons une familiarité de base avec des polynômes finis et les représentations binaires des entiers.

.

L'objectif du protocole STARK est de vérifier les calculs de manière succincte et transparente. La première étape STARK est appelée arithmétisation et consiste à traduire (souvent appelée "réduction") le problème de la vérification d'un calcul en un problème consistant à vérifier qu'un certain polynôme, qui peut être évalué efficacement du côté du vérifieur (c'est la partie "succincte"), est de faible degré. L'arithmétisation est utile car elle permet l'utilisation d'outils issus du domaine des codes de correction d'erreurs qui testent efficacement le faible degré. Cependant, l'arithmétisation elle-même ne fait que traduire une déclaration d'intégrité informatique en un polynôme, ce qui prépare le terrain pour la phase suivante de STARK, qui est un autre protocole interactif dans lequel un prouveur tente de convaincre un vérificateur que le polynôme est effectivement de faible degré. Le vérificateur est convaincu que le polynôme est de faible degré si et seulement si le calcul original est correct (sauf pour une probabilité infinitésimale). Dans la dernière étape STARK, le protocole interactif est transformé en une preuve unique non interactive, qui peut être publiée sur une blockchain et vérifiée publiquement par n'importe qui.

L'arithmétisation elle-même est composée de deux étapes : la première consiste à générer une trace d'exécution et des contraintes polynomiales, la seconde à transformer ces deux objets en un seul polynôme de faible degré. En termes d'interaction entre le prouveur et le verificateur, se mettent d'accord à l'avance sur les contraintes polynomiales. Le prouveur génère alors une trace d'exécution, et dans l'interaction suivante, le prouveur tente de convaincre le vérificateur que les contraintes polynomiales sont satisfaites sur cette trace d'exécution, sans que le vérificateur ne le voit.

Dans le post précédent, nous avons discuté de la notion d'une déclaration d'intégrité informatique (CI = Computational Integrity), l'affirmation que la sortie d'un certain calcul est correcte, d'un point de vue abstrait. Voyons un exemple concret d'une déclaration d'intégrité informatique : la somme totale que nous devons payer au supermarché a été calculée correctement. La preuve conventionnelle de cette affirmation particulière est le ticket de caisse. En général, les articles figurant sur le ticket de caisse sont énumérés avec leur prix, et la somme totale est indiquée en bas, comme suit :

Pour simplifier, nous considérons qu'il s'agit uniquement d'une affirmation selon laquelle la somme est correcte. Pour voir si cette affirmation du CI est valable, on peut parcourir la liste - sans sauter aucun article - pour calculer la somme totale et la comparer au chiffre figurant au bas du reçu. Il s'agit d'un exemple très naïf, mais nous l'utiliserons plus loin dans cet article pour démontrer l'idée de testabilité succincte.

La première étape de l'arithmétisation consiste à prendre un certain énoncé du CI (tel que "la cinquième transaction du bloc 7218290 est correcte") et à le traduire en langage algébrique formel. Cela sert deux objectifs :

1. définir l'affirmation de manière succincte et non ambiguë,

2. intégrer l'affirmation dans un domaine algébrique.

Cette intégration est ce qui permet la deuxième étape de l'arithmétisation, qui réduit l'énoncé de l'CI à une affirmation sur le degré d'un polynôme spécifique.

La représentation algébrique que nous utilisons à deux composantes principales :

1. une trace d'exécution

2. un ensemble de contraintes polynomiales.

La trace d'exécution est un tableau qui représente les étapes du calcul sous-jacent, où chaque ligne représente une seule étape. L'ensemble de contraintes polynomiales est construit de telle sorte que toutes les contraintes sont satisfaites si et seulement si la trace représente un calcul valide. Bien que la trace d'exécution puisse être très longue, nous travaillerons avec un ensemble succinct de contraintes polynomiales.

Trace d'exécution

Le type de trace d'exécution que nous cherchons à générer doit avoir la particularité d'être succinctement testable - chaque ligne peut être vérifiée en se basant uniquement sur les lignes qui lui sont proches dans la trace, et la même procédure de vérification est appliquée à chaque paire de lignes. Ce trait affecte directement la taille de la preuve. Pour illustrer ce que nous entendons par "testable succinctement", revenons au ticket de caisse du supermarché et ajoutons une colonne supplémentaire pour le total courant :

Cette simple addition nous permet de vérifier chaque ligne individuellement, étant donné sa ligne précédente.

Nous pouvons, par exemple, examiner ces deux lignes :

Et être convaincu que cette étape particulière du calcul (c'est-à-dire le nombre 16,41) est correcte puisque 12,96+3,45=16,41. Remarquez que la même contrainte est appliquée à chaque paire de lignes. C'est ce que nous entendons par contraintes succinctes.

Contraintes polynomiales

Réécrivons le ticket de caisse du supermarché (avec le total courant) sous la forme d'un tableau :

Désignons la valeur de la cellule de la i-ème ligne et de la j-ème colonne par Ai,j (nous désignerons les indices de cette façon car Medium ne supporte pas LaTeX). Nous pouvons maintenant reformuler les conditions de correction comme cet ensemble de contraintes polynomiales :

Ce sont des contraintes polynomiales linéaires dans Ai,j. Si l'ensemble de contraintes polynomiales que nous utilisons est d'un degré élevé, cela a un effet négatif sur la longueur de la preuve et le temps qu'il faut pour la générer. Par conséquent, les contraintes linéaires sont ce que nous pouvons espérer de mieux. Remarquez que (2) est en réalité une seule contrainte appliquée plusieurs fois, et la taille totale de l'ensemble est indépendante de la longueur de la preuve.

En résumé, nous avons pris un problème de vérification d'un ticket de caisse de supermarché, et l'avons transformé en une trace d'exécution succinctement testable, et un ensemble correspondant de contraintes polynomiales qui tiennent si et seulement si la somme totale dans le ticket de caisse original est correcte.

Voyons un exemple plus complexe.

La conjecture de Collatz

En 1937, un mathématicien allemand nommé Lothar Collatz a présenté une conjecture dans le domaine de la théorie des nombres. À première vue, cette conjecture pourrait sembler n'être qu'une jolie énigme mathématique, mais il s'agit en fait d'un problème ouvert difficile en théorie des nombres. Elle a attiré l'attention de nombreux mathématiciens au fil des ans et a acquis de nombreux synonymes (par exemple, la conjecture 3n + 1, la conjecture d'Ulam, le problème de Kakutani et bien d'autres). Paul Erdős a dit un jour à propos de cette conjecture : "Les mathématiques ne sont peut-être pas prêtes pour de tels problèmes".

Une séquence de Collatz commence par un entier positif quelconque, où chaque élément suivant de la séquence est obtenu à partir du précédent de la manière suivante :

• Si l'élément précédent est pair : divisez-le par 2.

• Si l'élément précédent est impair et supérieur à 1 : le multiplier par 3 et ajouter 1.

• Si l'élément précédent est 1, arrêtez-vous.

Prenons un exemple simple où le terme initial est 52 :

52 -> 26 -> 13 -> 40 -> 20 -> 10 -> 5 -> 16 -> 8 -> 4 -> 2 -> 1.

Conjecture de Collatz : pour tout entier positif par lequel on commence, la suite atteint toujours 1.

Malheureusement, la résolution de la conjecture de Collatz dépasse le cadre de cet article. Nous allons plutôt nous pencher sur le problème de la vérification d'un calcul qui vérifie la conjecture pour un entier de départ particulier.

La trace d'exécution de la séquence de Collatz

L'énoncé de l'CI est : "Une séquence de Collatz qui commence par 52, se termine par 1 après 11 itérations".

Soit A la trace d'exécution du calcul de la séquence. La i-ème ligne, désignée par Ai, représente le i-ème nombre de la séquence. Tous les nombres sont représentés sous forme de chaînes binaires, afin de faciliter l'expression de la condition paire/impaire avec des polynômes. Ai,j est égal au ji-ème bit le moins significatif du i-ème nombre de la séquence. Par exemple, A0=001011 : le premier terme est 52, sa représentation binaire est 110100 et ensuite on inverse l'ordre des bits (l'ordre d'inversion des bits simplifie l'indexation dans la notation des contraintes polynomiales).

Voici la trace d'exécution de la séquence de Collatz ci-dessus qui commence par 52 :

Notez qu'ici la trace a 6 colonnes car 6 bits sont suffisants pour représenter même le plus grand nombre de la séquence. Si nous avions commencé la séquence avec 51, le nombre suivant aurait été 154, donc la trace d'une telle séquence aurait nécessité au moins 8 colonnes.

Les contraintes polynomiales de la séquence de Collatz

Rappelons que les contraintes polynomiales que nous recherchons sont telles qu'elles sont toutes satisfaites si et seulement si l’origine de A décrit la séquence de Collatz donnée (commençant par 52, se terminant par 1, et la transition entre deux lignes consécutives est effectuée correctement). Dans notre exemple, l’origine A est de taille 6x12, c'est-à-dire qu'elle représente une séquence de Collatz de 12 nombres de 6 bits. L'ensemble des contraintes polynomiales est le suivant (n=12, m=6) :

Passons en revue chacune de ces contraintes. Les trois premières sont simples :

(1) est valable si et seulement si la première ligne est une représentation binaire de 52.

(2) est valable si et seulement si la dernière ligne est une représentation binaire de 1.

(3) est valable si et seulement si la trace ne contient que des bits (un nombre est égal à son carré si et seulement s'il vaut 0 ou 1).

Le quatrième ensemble de contraintes définit le cœur du calcul succinct de la séquence, c'est-à-dire le lien entre deux lignes consécutives. La capacité d'exprimer les contraintes de calcul comme un modèle récurrent de contraintes locales (c'est-à-dire la succinctivité) est fondamentale pour que le vérificateur soit exponentiellement plus rapide qu'un rejeu naïf du calcul.

Examinons attentivement les contraintes elles-mêmes.

Pour tout i<n-1, dénote :

Par conséquent, pour chaque i<n-1, nous obtenons la contrainte suivante :

Ai,0 est le bit le moins significatif du i-ème nombre, qui détermine sa parité en tant qu'entier, donc cette contrainte décrit la règle de la séquence de Collatz.

En résumé, toutes les contraintes sont satisfaites si et seulement si l’origine représente un calcul valide d'une séquence de Collatz.

Notez que toute séquence de Collatz de longueur n, peut être représentée en utilisant une trace de taille n*m où m est le nombre maximum de bits dans la représentation d'un nombre de la séquence, et les contraintes polynomiales correspondantes sont modifiées en conséquence. Notez que les contraintes polynomiales ne croissent pas avec n et m, mais restent simples et concises.

Étant donné un premier terme spécifique pour une séquence de Collatz, un simple programme informatique peut produire la trace d'exécution et les contraintes polynomiales.

Conclusion

Dans ce post, nous avons couvert la première étape de l'arithmétisation des instructions CI.

Nous avons vu comment une déclaration CI sur une séquence de Collatz peut être transformée en une origine d'exécution et un ensemble de contraintes polynomiales décrites succinctement. Des méthodes similaires peuvent être utilisées pour transformer n'importe quel calcul, et en général, n'importe quelle déclaration CI peut être traduite sous cette forme. Les détails, cependant, ont une grande importance. Bien qu'il existe de nombreuses façons dont une origine d'exécution (et un ensemble de contraintes polynomiales) peut décrire un calcul spécifique, seule une poignée d'entre elles donne lieu à une petite preuve STARK qui peut être construite efficacement. Une grande partie des efforts de StarkWare est consacrée à la conception de réductions qui conduisent à de bonnes contraintes polynomiales, que nous appelons AIR (Algebraic Intermediate Representation), car une grande partie des performances de nos systèmes en dépend.

Dans le prochain article, nous aborderons la deuxième étape de l'arithmétisation - la transformation de la trace d'exécution et des contraintes polynomiales en un seul polynôme, dont le faible degré est garanti, si et seulement si le calcul original est correct.

Kineret Segal & Shir Peled

StarkWare