A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
Ce papier présente une chaîne de vérification fiable et vérifiée par le noyau qui intègre des outils d'extraction de Rust vers Lean, des bibliothèques cryptographiques formelles et des prouveurs d'IA pour générer avec succès des preuves de correction vérifiées par machine pour du code cryptographique Rust de production dans le cadre du projet zkEVM de la Fondation Ethereum.
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
Imaginez une usine à haut risque qui fabrique les clés numériques d'un coffre-fort massif et invisible (une Machine Virtuelle à Connaissance Zéro). Si même un seul petit engrenage de cette usine est légèrement tordu, la sécurité de tout le coffre-fort est compromise, et personne ne le saura avant qu'il ne soit trop tard.
Pendant des années, vérifier ces engrenages a été comparable à engager une équipe de mécaniciens experts pour inspecter chaque boulon à la main. C'est lent, coûteux, et cela repose sur le fait que les mécaniciens ne manquent rien.
Ce papier décrit une nouvelle chaîne de montage automatisée qui fait trois choses :
- Traduit les plans de l'usine (écrits dans un langage complexe appelé Rust) vers un langage mathématique universel (Lean 4) qu'un ordinateur peut comprendre parfaitement.
- Fournit une « norme d'or » parfaite et pré-écrite de la façon dont la machine devrait fonctionner (en utilisant des bibliothèques appelées ArkLib et CompPoly).
- Engage un assistant IA ultra-intelligent (appelé Aleph et Aristotle) pour comparer les plans traduits à la norme d'or et rédiger la preuve qu'ils correspondent.
Voici comment le processus fonctionne, en utilisant des analogies simples :
1. Le Traducteur (de Rust vers Lean)
Les plans de l'usine sont écrits en Rust, un langage que les ingénieurs adorent pour construire des logiciels rapides et sûrs. Cependant, les « juges mathématiques » (le système Lean 4) ne parlent pas Rust ; ils ne parlent que le pur mathématique.
Le papier utilise des outils appelés Aeneas et Hax comme traducteurs. Ils prennent le code Rust et le convertissent en mathématiques « purement fonctionnelles ».
- L'Analogie : Imaginez prendre une recette écrite dans l'argot d'un chef (Rust) et la traduire en une formule chimique stricte et étape par étape (Lean). Le traducteur ajoute également des « étiquettes de sécurité » à chaque étape. Si une étape pourrait échouer (comme diviser par zéro ou manquer d'ingrédients), la traduction le marque clairement afin que les mathématiques puissent le vérifier.
2. La Norme d'Or (Les Spécifications)
On ne peut pas prouver qu'une machine fonctionne sans avoir une définition du « fonctionnement ».
- L'Analogie : Considérez ArkLib et CompPoly comme le « Manuel Officiel » de la cryptographie. Ils contiennent les définitions parfaites et abstraites de la façon dont des choses comme « plier un papier » (repliement FRI) ou « vérifier un arbre de Merkle » devraient se comporter mathématiquement.
- L'objectif est de prouver que le code Rust traduit (la machine de l'usine) fait exactement ce que le Manuel dit qu'il devrait faire, ni plus ni moins.
3. L'IA Rédactrice de Preuves (Le « Cerveau »)
C'est la partie la plus excitante. Une fois le code traduit et le manuel prêt, il faut rédiger une preuve qu'ils correspondent. Traditionnellement, un mathématicien humain devait rédiger cette preuve, ce qui équivaut à résoudre un puzzle massif et complexe.
Le papier introduit des Preuveurs IA (Aleph et Aristotle) pour faire le gros du travail.
- L'Analogie : Imaginez l'IA comme un détective infatigable et ultra-rapide. Vous lui donnez le plan traduit et le manuel, et il dit : « Je vois le lien ! Voici la preuve. »
- Contrôle de Sécurité Crucial : L'IA ne se contente pas de dire qu'elle a raison ; elle rédige la preuve dans un langage que le Noyau Lean (le juge ultime) peut lire. Le Noyau vérifie chaque étape de la logique de l'IA. Si l'IA devine mal, le Noyau la rejette. Ainsi, l'IA peut être créative, mais elle ne peut pas tricher.
Ce qu'ils ont réellement fait
L'équipe a appliqué cette chaîne de montage à du code cryptographique réel utilisé dans les projets de la Fondation Ethereum (spécifiquement Plonky3 et RISC Zero).
- Le Succès : Ils ont prouvé avec succès que des parties spécifiques du code (comme calculer comment plier des données ou vérifier si un arbre est inclus correctement) étaient mathématiquement parfaites.
- Le Rôle de l'IA : Dans un exemple spécifique impliquant une fonction appelée
compute_log_arity_for_round, l'IA (Aleph) a automatiquement rédigé deux preuves complexes qui étaient auparavant bloquées (marquées comme « sorry », signifiant « nous savons que c'est vrai, mais nous ne l'avons pas encore prouvé »). - Le Rôle de l'Humain : L'IA était excellente pour gérer des énigmes logiques, des scénarios « si-alors » et des mathématiques de base. Cependant, elle avait toujours besoin des humains pour :
- Concevoir la stratégie globale (le « Manuel »).
- Gérer des boucles complexes (comme trouver le bon motif dans une séquence répétitive).
- Corriger les erreurs de traduction là où le code Rust était trop astucieux pour que le traducteur puisse le gérer.
Les Accrocs (Lacunes Techniques)
Le papier admet que la chaîne de montage n'est pas encore parfaite.
- Incompatibilité de Versions : Les traducteurs, les manuels et l'IA parlent tous légèrement différents « dialectes » du langage mathématique. L'équipe a dû coordonner pour mettre tout le monde sur la même version.
- Limites de Traduction : Certaines fonctionnalités complexes de Rust (comme les types génériques ou les bibliothèques externes) sont difficiles à convertir pour les traducteurs. L'équipe a dû réécrire certains codes dans un « modèle » plus simple juste pour que le traducteur puisse le comprendre.
La Conclusion
Ce papier ne prétend pas que l'IA a remplacé les ingénieurs humains. Au contraire, il montre une chaîne de montage où :
- Les humains traduisent le code et définissent les objectifs.
- L'IA agit comme un assistant puissant pour rédiger les preuves logiques fastidieuses.
- Un juge informatique strict (le Noyau) vérifie tout pour garantir la sécurité.
Le résultat est un système fonctionnel qui transforme du code cryptographique de niveau production en preuves vérifiées par machine et garanties mathématiquement, rendant le « coffre-fort invisible » considérablement plus sûr.
Noyé(e) sous les articles dans votre domaine ?
Recevez des digests quotidiens des articles les plus récents correspondant à vos mots-clés de recherche — avec des résumés techniques, dans votre langue.