💻 computer science

Automating Bitvector and Finite Field Equivalence Proofs in Lean

Ce papier présente BitModEq, une nouvelle tactique Lean qui automatise les preuves d'équivalence entre les vecteurs de bits et les corps finis en utilisant des lemmes de plage et une analyse de cas, surpassant les solveurs SMT les plus avancés dans la vérification des encodages de circuits de preuves à divulgation nulle de connaissance.

Auteurs originaux : Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker

Publié 2026-05-15

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

La Vue d'Ensemble : Deux Langues Différentes pour les Mathématiques

Imaginez que vous essayez de vérifier qu'une recette secrète (une Preuve à Divulgation Nulle de Connaissance) fonctionne correctement. Le problème est que la recette est écrite dans deux langues différentes qui ne se mélangent pas bien :

Les Corps Finis : Imaginez cela comme un monde de « Mathématiques d'Horloge ». Si vous avez une horloge avec 17 heures, ajouter 10 et 10 ne vous donne pas 20 ; cela vous donne 3 (car vous faites le tour). C'est ainsi que de nombreux systèmes cryptographiques modernes (comme ceux utilisés dans les cryptomonnaies) effectuent leurs calculs.
Les Vecteurs de Bits : Imaginez cela comme les « Mathématiques Informatiques ». Les ordinateurs ne font pas le tour comme des horloges ; ils ont simplement un nombre fixe d'interrupteurs (bits) qui sont soit allumés, soit éteints. Si vous additionnez des nombres et que vous manquez d'interrupteurs, les bits excédentaires sont tout simplement coupés.

Le Problème :
Lorsque les développeurs construisent ces systèmes cryptographiques, ils doivent traduire les « Mathématiques d'Horloge » en « Mathématiques Informatiques » pour les faire fonctionner sur du matériel réel. Cette traduction s'appelle l'arithmétrisation.

Si la traduction est incorrecte, tout le système de sécurité est compromis.
Vérifier si la traduction est correcte est incroyablement difficile.
La vérification manuelle est comme relire un roman en lisant chaque mot avec une loupe : c'est précis mais cela prend une éternité et est sujet aux erreurs humaines.
La vérification automatique (utilisant des solveurs informatiques standards) est comme utiliser un correcteur orthographique : c'est rapide, mais il est souvent confus par les règles étranges de la « Mathématique d'Horloge » et abandonne face aux phrases complexes.

La Solution : Le Traducteur « BitModEq »

Les auteurs ont créé un nouvel outil appelé BitModEq à l'intérieur d'un système appelé Lean (qui est comme un tuteur en mathématiques super strict qui vérifie chaque étape d'une preuve).

Imaginez BitModEq comme un traducteur spécialisé qui ne se contente pas d'échanger des mots ; il comprend la logique derrière les mots. Il utilise un processus en trois étapes pour prouver que la recette « Mathématiques d'Horloge » est exactement la même que la recette « Mathématiques Informatiques » :

Étape 1 : Le « Déballage » (Traduction)

L'outil prend les « Mathématiques d'Horloge » (Corps Finis) et tente de les « déballer » en nombres normaux (Nombres Naturels).

Le Défi : Dans les Mathématiques d'Horloge, $5 - 10$ peut être un nombre positif à cause du tour. En mathématiques normales, c'est négatif.
L'astuce : L'outil examine les nombres et se demande : « Est-il possible que ce nombre fasse le tour ? » Si les nombres sont assez petits (comme les bits dans un ordinateur), il sait que le tour ne se produira pas. Il retire en toute sécurité les règles de l'« Horloge » et les traite comme des mathématiques normales. S'il n'est pas sûr, il conserve les règles de l'« Horloge » mais ajoute une vérification de sécurité.

Étape 2 : Le « Filet de Sécurité » (Analyse des Intervalles)

C'est l'ingrédient secret du document. Avant que l'outil n'essaie de convertir les mathématiques en bits informatiques, il effectue une Analyse des Intervalles.

L'Analogie : Imaginez que vous faites vos valises. Vous ne jetez pas simplement les vêtements dedans ; vous vérifiez la taille de la valise et la taille des vêtements.
Comment cela fonctionne : L'outil examine les variables et se demande : « Quelle est la valeur maximale que ce nombre pourrait avoir ? »
- S'il sait qu'un nombre est compris entre 0 et 1 (comme un seul interrupteur lumineux), il peut ignorer complètement les règles complexes de l'« Horloge ».
- Cette étape est cruciale car elle simplifie le problème au point que l'ordinateur peut le résoudre facilement. Sans cette vérification de « filet de sécurité », l'ordinateur est submergé par la complexité.

Étape 3 : Le « Tir de Bits » (Preuve Finale)

Une fois que l'outil a simplifié le problème en « Mathématiques Informatiques » pures (bits), il utilise une technique appelée tir de bits (bit-blasting).

L'Analogie : C'est comme prendre une serrure complexe et essayer chaque combinaison de clés possible jusqu'à trouver celle qui l'ouvre.
Parce que l'outil a simplifié le problème à l'étape 2, la « serrure » est maintenant assez petite pour que l'ordinateur puisse essayer chaque combinaison instantanément et prouver que les mathématiques sont correctes.

Pourquoi Cela Compte (Les Résultats)

Les auteurs ont testé leur outil sur des systèmes cryptographiques réels (spécifiquement Jolt et CirC).

La Concurrence : Ils ont comparé leur outil aux meilleurs solveurs automatiques existants (comme cvc5).
Le Résultat : Les solveurs existants étaient souvent bloqués ou dépassés par le temps lorsque les problèmes devenaient grands (comme des nombres de 32 bits). Ils étaient comme un correcteur orthographique essayant de lire un dictionnaire.
La Victoire de BitModEq : Le nouvel outil a résolu 19 % de problèmes de plus que les meilleurs outils existants. Il pouvait gérer des nombres beaucoup plus grands (jusqu'à 32 bits) là où les autres échouaient.
Bonus : Parce qu'il s'exécute dans Lean, la preuve est vérifiée par le noyau. Cela signifie que l'ordinateur n'a pas seulement deviné ; il a suivi un ensemble strict de règles logiques garanties correctes, réduisant le risque de bugs cachés.

Une Découverte du Monde Réel

Lors de leurs tests, l'outil a en fait trouvé un bug dans le compilateur CirC. Le compilateur avait une erreur dans la façon dont il gérait les grands nombres (spécifiquement, un décalage à droite de 32 bits). Le bug ne se manifestait qu'avec de grands nombres, c'est pourquoi les tests précédents, à plus petite échelle, l'avaient manqué. Les développeurs ont corrigé le bug après que les auteurs l'eurent signalé.

Résumé

Le document présente une nouvelle façon de vérifier automatiquement que les mathématiques cryptographiques fonctionnent correctement. Au lieu de lutter pour traduire manuellement ou avec des outils maladroits entre les « Mathématiques d'Horloge » et les « Mathématiques Informatiques », ils ont construit un traducteur intelligent qui :

Vérifie d'abord la taille des nombres (Analyse des Intervalles).
Simplifie les mathématiques en supprimant les règles inutiles de l'« Horloge ».
Utilise une logique de force brute pour prouver que le résultat final est correct.

Cela rend la vérification de systèmes de sécurité complexes plus rapide, plus fiable et capable de détecter des bugs que d'autres outils manquent.

Résumé technique : Automatisation des preuves d'équivalence bitvectorielle et de corps finis dans Lean

Énoncé du problème

La vérification des encodages de circuits de Preuves à Connaissance Nulle (ZKP) fait face à un défi critique : prouver la justesse d'énoncés sans quantificateurs utilisant simultanément des opérations bitvectorielles (arithmétique machine standard modulo $2^N$ ) et des opérations de corps finis (arithmétique modulo un grand nombre premier $P$ ). Les systèmes ZKP nécessitent souvent des « arithmétisations » qui encodent la logique bitvectorielle sous forme de polynômes de corps finis. Garantir la justesse de ces encodages est vital pour la validité des systèmes ZKP, pourtant leur construction est sujette aux erreurs.

Les flux de travail de vérification existants souffrent de deux limitations principales :

Vérification manuelle : L'intégration de systèmes ZKP entiers dans des Preuveurs de Théorèmes Interactifs (ITP) comme Lean offre de solides garanties mais exige un effort humain considérable. À mesure que les optimisations ZKP évoluent rapidement, ces preuves manuelles nécessitent fréquemment d'importants travaux de réécriture.
Vérification automatique par SMT : La réduction de la vérification à des requêtes de Satisfiabilité Modulo Théories (SMT) offre une plus grande automatisation mais se heurte à deux problèmes fondamentaux :
- Conversion de théories : Les solveurs SMT ne disposent pas d'un support natif pour la conversion entre corps finis et bitvectors. Des contournements comme le découpage en bits (bit-splitting) introduisent un nombre excessif de variables, et les vérifications de plages nécessitent des polynômes complexes qui dégradent les performances du solveur.
- Base de code de confiance (TCB) : Les solveurs SMT possèdent une TCB beaucoup plus large que les ITP, augmentant le risque de bugs non détectés.

Méthodologie

Les auteurs présentent BitModEq, une tactique Lean novatrice conçue pour prouver automatiquement l'équivalence entre les encodages de corps finis et leur sémantique bitvectorielle correspondante. L'approche exploite la sémantique riche des ITP pour effectuer des conversions de types directes tout en conservant l'automatisation de la résolution SMT grâce à un flux de travail spécialisé.

Flux de travail principal

BitModEq opère en quatre phases distinctes (illustrées dans la figure 1 du papier) :

Conversion du corps fini vers le nombre naturel : Tous les termes de type Corps Fini ($FP$) sont convertis en Nombres Naturels ( $N$ ). Cela implique de pousser les opérateurs de conversion (comme toNat) vers l'intérieur des expressions arithmétiques.
Analyse de plages : Les inégalités sur les nombres naturels générées lors de la conversion sont résolues à l'aide d'un algorithme dédié d'analyse de plages.
Conversion du nombre naturel vers le bitvectoriel : Les termes restants de nombres naturels sont convertis en bitvectors ( $BV_N$ ).
Éclatement en bits (Bit-Blasting) : Les objectifs finaux d'égalité bitvectorielle sont résolus à l'aide de bv_decide, une procédure de décision par éclatement en bits implémentée dans Lean.

Composants techniques clés

1. Calcul de traduction (Sections 4.2)
La tactique utilise un ensemble de règles de traduction pour passer d'un domaine à l'autre :

$FP \to N$ : Des règles telles que distNat distribuent toNat sur l'addition et la multiplication. Crucialement, la tactique distingue les cas où le dépassement modulo peut être écarté (permettant une simple soustraction) et les cas où il ne peut pas l'être (nécessitant l'ajout du module $P$ suivi d'une opération modulo). Des règles comme sqrBds détectent les encodages binaires (où $x^2 = x$ ) et les traduisent en bornes ( $x \le 1$ ).
$N \to BV$ : Des règles comme distBV distribuent toBV sur les opérations. Contrairement à l'étape $FP \to N$ , ces règles ne nécessitent pas d'ajouter un opérateur modulo car l'espace cible est naturellement modulo $2^N$ .

2. Analyse de plages (Section 4.3)
Les tactiques Lean standard (par exemple omega, linarith) échouent souvent sur les arithmétisations ZKP en raison de coefficients élevés et de dépendances complexes entre variables. BitModEq introduit un calcul d'analyse de plages personnalisé et dirigé par la syntaxe :

Variables factices : L'algorithme introduit des variables factices existentielles pour décomposer des inégalités complexes.
Décomposition et élimination : Des règles décomposent les inégalités (par exemple, $a + b \le w$ devient $a \le w_1, b \le w_2, w_1+w_2 \le w$ ) et éliminent les variables factices en les instanciant avec des bornes dérivées d'hypothèses ou de propriétés connues (par exemple, les éléments de corps finis sont bornés par $P-1$ ).
Gestion des dépendances : Des règles spécialisées (ineqCases, ineqXOR) effectuent une analyse de cas ciblée sur des variables simulant des bits (0 ou 1) pour résoudre des dépendances que les solveurs arithmétiques standards manquent.

3. Implémentation
La tactique est implémentée dans Lean 4.23.0, utilisant mathlib pour les lemmes et bv_decide pour l'étape finale d'éclatement en bits. Elle repose sur le noyau de Lean pour la vérification des preuves, assurant une Base de Calcul de Confiance minimale.

Contributions clés

Tactique BitModEq : Une tactique Lean qui traduit les opérations de corps finis en bitvectors et résout les objectifs résultants par éclatement en bits, conservant ainsi les garanties de justesse des ITP.
Vérification bornée d'encodages réels : Une vérification preuve de concept de deux systèmes ZKP réels (Jolt et CirC) qui atteint des bornes de largeur de bits supérieures aux techniques précédentes.
Analyse de plages spécialisée : Une nouvelle tactique Lean pour prouver les objectifs résultant de la traduction, spécifiquement conçue pour gérer les dépendances de variables et les contraintes d'inégalités courantes dans les arithmétisations ZKP.

Résultats et évaluation

Les auteurs ont évalué BitModEq par rapport aux solveurs SMT de l'état de l'art (spécifiquement cvc5 avec des bases de Gröbner complètes et fractionnées) sur des benchmarks extraits de Jolt (un zkVM) et de CirC (un compilateur zkVM).

Performance : BitModEq a résolu 19 % de benchmarks en plus que les configurations SMT les plus performantes.
- Sur les benchmarks Jolt (tables de recherche de 8 bits et 32 bits), BitModEq a résolu 3 instances de 8 bits et 7 instances de 32 bits de plus que cvc5 (encodage faible).
- Sur les benchmarks CirC, BitModEq a résolu plus d'instances pour 13 largeurs de bits testées sur 17.
Évolutivité : Bien que cvc5 ait de meilleures performances sur les petites largeurs de bits, ses performances se dégradent considérablement à mesure que les largeurs de bits augmentent en raison de l'explosion du nombre de variables due au découpage en bits. BitModEq s'est évolutivement bien comporté jusqu'à des entrées de 32 bits.
Efficacité : Une étude d'ablation a montré que l'analyse de plages personnalisée est cruciale ; supprimer les divisions de cas a réduit considérablement le nombre de benchmarks résolus (par exemple, de 737 à 720 sur CirC, et de 24 à 21 sur Jolt). Le remplacement de l'analyse personnalisée par des tactiques Lean standard (ring_nf, linarith, etc.) a entraîné une chute drastique du nombre d'instances résolues (par exemple, 434 contre 737 sur CirC).
Temps d'exécution : L'analyse de plages représente environ 52 % du temps d'exécution total, suivie par la traduction (23 %) et l'éclatement en bits (21 %).
Découverte de bugs : Lors de l'évaluation de CirC, les auteurs ont identifié un bug de validité dans l'implémentation du décalage arithmétique à droite de 32 bits lié au débordement d'entier, qui n'avait pas été détecté sur des largeurs de bits plus petites.

Importance et affirmations

Le papier affirme que BitModEq répond aux limitations spécifiques des flux de travail de vérification ZKP actuels en combinant la validité des ITP avec le raisonnement automatisé. En traduisant les contraintes de corps finis vers les bitvectors, l'approche évite les goulots d'étranglement de performance de la conversion de théories SMT et la grande TCB des solveurs SMT.

Les auteurs soulignent que leur approche est particulièrement efficace pour les arithmétisations ZKP qui simulent des opérations au niveau des bits au sein d'un corps fini, un motif courant dans les systèmes ZK modernes. Bien que la méthode ne soit pas complète (elle peut retourner « inconnu » pour certaines dépendances complexes ou opérations spécifiques aux corps comme les inverses), elle vérifie avec succès des encodages réels qui étaient auparavant intraitables pour les outils automatiques, fournissant des preuves vérifiées par le noyau pour la justesse de ces composants cryptographiques critiques.