💻 computer science

Formal Verification of Imperative First-Class Functions in Move

Ce papier présente une extension du Move Prover qui permet la vérification formelle des fonctions impératives de première classe dans le langage Move en introduisant des prédicats comportementaux, des étiquettes d'état et une stratégie de codage SMT exploitant la séparation statique de la mémoire de Move pour une vérification efficace et une inférence automatisée des spécifications.

Auteurs originaux : Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman

Publié 2026-05-14

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman

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 : L'Usine de « Contrats Intelligents »

Imaginez qu'Aptos soit une usine à haute sécurité qui fabrique des actifs numériques (comme de l'argent ou des billets) en utilisant un langage spécial appelé Move. Pour s'assurer que ces actifs ne soient ni volés ni endommagés, l'usine utilise un inspecteur robot appelé le Move Prover (MVP). Ce robot lit les plans (le code) et prouve mathématiquement que tout fonctionnera correctement avant même que l'usine ne démarre.

Pendant longtemps, ce robot était excellent pour vérifier des instructions simples. Mais récemment, l'usine a ajouté une nouvelle fonctionnalité, complexe : les Fonctions de Premier Niveau (First-Class Functions).

Pensez à ces nouvelles fonctions comme à des baguettes magiques.

L'ancienne méthode : Vous deviez tenir la baguette vous-même pour lancer un sort. Le robot savait exactement quel sort vous lanciez.
La nouvelle méthode : Vous pouvez mettre la baguette dans une boîte, donner la boîte à un ami, ranger la boîte dans un coffre-fort, ou la passer à une machine qui ne sait pas ce qu'elle contient. La machine sait seulement : « Je dois agiter une baguette », mais elle ne sait pas laquelle jusqu'à la dernière seconde.

Ceci s'appelle le Dispatch Dynamique (Dynamic Dispatch). C'est puissant, mais cela fait planter l'inspecteur robot car il ne peut pas voir l'avenir pour savoir quel sort précis est lancé.

Le Problème : Le Dilemme de la « Boîte Noire »

Le document explique comment les auteurs ont amélioré l'inspecteur robot (MVP) pour gérer ces baguettes magiques sans paniquer.

Auparavant, si une fonction était une « boîte noire » (une variable contenant une fonction), le robot devait deviner ou vérifier chaque possibilité à la fois, ce qui faisait exploser les mathématiques et ralentissait le robot.

Les auteurs ont introduit deux nouveaux outils pour résoudre ce problème :

1. Les Prédicats Comportementaux : La « Carte de Garantie »

Au lieu de regarder à l'intérieur de la baguette magique pour voir comment elle fonctionne, le robot examine maintenant la Carte de Garantie attachée à la baguette.

L'ancienne méthode : « Je dois savoir exactement comment fonctionne cette baguette calculate_price, jusqu'à chaque ligne de code, avant de vous permettre de l'utiliser. »
La nouvelle méthode : « Je ne me soucie pas de la façon dont la baguette fonctionne à l'intérieur. Je dois simplement lire sa Carte de Garantie. La carte dit : 'Si vous me donnez 5 pièces, je vous rendrai 3 pièces, et je ne casserai jamais.' »

Le document appelle cela des Prédicats Comportementaux. Ils agissent comme un contrat qui décrit :

Les préconditions : Ce qui doit être vrai avant d'agiter la baguette.
Les postconditions : Ce qui sera vrai après l'avoir agitée.
Les conditions d'arrêt : Quand la baguette pourrait exploser (échouer).

Cela permet au robot de vérifier la promesse de la baguette sans avoir besoin de connaître la recette secrète à l'intérieur.

2. Les Étiquettes d'État : La « Caméra à Horodatage »

Parfois, une séquence d'événements se produit. Imaginez une chaîne de montage où un robot peint une voiture, puis un autre robot pose les roues.

Si vous voulez prouver que la voiture est sûre, vous devez connaître l'état de la voiture après la peinture mais avant la pose des roues.

Les auteurs ont introduit des Étiquettes d'État. Pensez-y comme à des Caméras à Horodatage placées à des points spécifiques du processus.

Caméra A (Début) : La voiture est en métal nu.
Caméra B (Milieu) : La voiture est peinte.
Caméra C (Fin) : Les roues sont posées.

Le robot peut maintenant dire : « Je sais que la peinture a eu lieu entre la Caméra A et la Caméra B, et que les roues ont été ajoutées entre la Caméra B et la Caméra C. » Cela aide le robot à raisonner sur des séquences complexes d'événements sans se perdre sur l'apparence du monde à un moment donné.

Comment le Robot Fonctionne Réellement (Le « Standard Téléphonique »)

Le document décrit comment le robot traduit ces idées en mathématiques (logique SMT) qu'un ordinateur peut résoudre.

Imaginez que le robot possède un Standard Téléphonique.

Scénario A (Baguette Connue) : Si le robot voit une baguette spécifique et connue (par exemple, la fonction product), il bascule l'interrupteur en « Mode Direct ». Il ignore la carte de garantie et vérifie simplement le code réel de cette baguette spécifique.
Scénario B (Baguette Inconnue) : Si le robot voit une boîte générique (une variable), il bascule l'interrupteur en « Mode Abstrait ». Il ignore totalement le code et s'appuie uniquement sur la Carte de Garantie (les prédicats comportementaux) pour prouver que le système est sûr.

C'est efficace car le robot n'a pas à essayer d'ouvrir chaque boîte possible. Il n'ouvre que celles qu'il connaît, et pour le reste, il fait confiance au contrat.

L'« Auto-Inspecteur » (Inférence de Spécification)

L'un des aspects les plus cool du document est que le robot peut maintenant écrire ses propres Cartes de Garantie.

Habituellement, les humains doivent écrire ces cartes manuellement, ce qui est fastidieux. Les auteurs ont amélioré le robot pour qu'il puisse examiner le code, déterminer ce que la Carte de Garantie devrait dire, et l'écrire pour vous.

Entrée : Un morceau de code désordonné avec une baguette magique.
Action du Robot : « Je vois que ce code vérifie si des frais existent. Je vais écrire une Carte de Garantie qui dit : 'Cette baguette explosera si les frais sont manquants.' »
Résultat : Le robot vérifie son propre travail. Si le code correspond à la carte, il valide.

Ceci est démontré dans le document avec un exemple de Market Maker Automatisé (AMM). Il s'agit d'un système qui échange des actifs. Le robot a prouvé que même si la règle de tarification (la baguette magique) pouvait être modifiée par l'utilisateur, le système ne planterait jamais ni ne perdrait d'argent, à condition que la nouvelle baguette suive les règles écrites sur sa Carte de Garantie.

Résumé de la Réalisation

Le document affirme avoir résolu un gros problème dans la vérification des contrats intelligents :

Il a rendu les « Baguettes Magiques » (fonctions) sûres à utiliser d'une manière qui permet de les stocker, de les transmettre et de les modifier dynamiquement.
Il a créé un nouveau langage (Prédicats Comportementaux + Étiquettes d'État) qui permet au robot de parler de ces baguettes sans avoir besoin de voir à l'intérieur.
Il a rendu le robot plus rapide et plus intelligent en utilisant une approche de « Standard Téléphonique » qui bascule entre l'examen du code et l'examen du contrat.
Il a automatisé la paperasse en permettant au robot de générer les contrats nécessaires pour vous.

En bref, ils ont appris à l'inspecteur robot à faire confiance à la promesse d'un étranger (le contrat) sans avoir besoin de connaître les secrets de l'étranger, rendant l'usine plus sûre et plus flexible.

Résumé technique : Vérification formelle des fonctions impératives de première classe en Move

Énoncé du problème
Le Move Prover (MVP) est un outil de vérification formelle conçu pour les contrats intelligents Move, initialement construit sur un style de spécification modulaire à dispatch statique. Une extension récente du langage Move a introduit les fonctions d'ordre supérieur, permettant aux fonctions d'être des valeurs de première classe pouvant être passées en arguments, stockées dans des structures de données et persistées dans le stockage global. Cette capacité permet le dispatch dynamique mais rompt les hypothèses d'analyse statique sur lesquelles reposait MVP. Plus précisément, lorsqu'une fonction est appelée dynamiquement, ses pré- et post-conditions ne peuvent pas être résolues au site d'appel. L'appelant doit raisonner de manière abstraite sur le comportement des arguments de type valeur-fonction, tandis que le vérificateur doit réconcilier ces spécifications abstraites avec les fonctions concrètes qui peuvent atteindre le site d'appel. Les solutions existantes dans d'autres langages (par exemple, Dafny, F*, Verus) manquent soit de support pour les fonctions impératives de première classe modifiant l'état, soit reposent sur la logique de séparation, ce qui peut conduire à des encodages SMT complexes. Le défi consiste à prendre en charge ces fonctionnalités dynamiques de manière efficace, en garantissant que la vérification reste rapide, complète pour les cas pertinents et exempte d'instabilité des déclencheurs SMT.

Méthodologie
Les auteurs étendent MVP et le langage de spécification Move pour prendre en charge les fonctions d'ordre supérieur grâce à trois mécanismes principaux :

Prédicats comportementaux : Le langage de spécification est étendu avec des prédicats caractérisant le comportement des valeurs-fonction ( $f$ ) sur des arguments spécifiques ( $\bar{x}$ ) et des résultats ( $\bar{y}$ ). Ceux-ci incluent :
- requires_of<f>(x): Pré-conditions.
- aborts_of<f>(x): Conditions d'arrêt.
- ensures_of<f>(x, y): Post-conditions.
  Ces prédicats suivent implicitement les dépendances d'état en lecture et en lecture/écriture, permettant aux spécifications de faire référence de manière abstraite aux arguments de fonction sans intégrer leurs corps.
Étiquettes d'état : Pour raisonner sur les transitions d'état séquentielles et les états intermédiaires de la mémoire, les auteurs introduisent des étiquettes d'état (par exemple, $S$ ). Ces étiquettes nomment des points spécifiques dans l'exécution. Les prédicats peuvent être mono-état ( $S \mid \sim p$ ) ou bi-état ( $S.. \mid \sim q$ ), permettant la composition de prédicats comportementaux pour décrire des séquences d'opérations (par exemple, l'état postérieur d'une fonction devenant l'état préalable d'une autre).
Encodage SMT par discrimination de variantes : Au niveau SMT, les valeurs-fonction sont encodées à l'aide de types de données algébriques représentant toutes les sources possibles d'une valeur-fonction (fermetures concrètes, paramètres de fonction ou champs de structure). Lorsqu'une valeur-fonction est invoquée :
- Si la fonction concrète est connue (par exemple, une fermeture spécifique), l'invoque est remplacée par l'effet de cette fonction concrète.
- Si la fonction est inconnue (par exemple, un paramètre ou une fermeture chargée depuis le stockage), l'invoque est modélisée à l'aide des prédicats comportementaux associés au type de cette valeur-fonction.
- L'encodage utilise les constructions « havoc » et « assume » pour modéliser les modifications de mémoire et garantit que les conditions de cadre sont respectées en distinguant les cartes mémoire d'état préalable et d'état postérieur.

Contributions clés
L'article détaille les contributions spécifiques suivantes :

Extensions du langage : L'introduction de prédicats comportementaux et d'étiquettes d'état dans le langage de spécification Move, rendant les spécifications de fonctions des citoyens de première classe capables de suivre les dépendances d'état.
Implémentation dans MVP : Un encodage basé sur Boogie qui discrimine les variantes de valeurs-fonction aux sites d'appel. Cette approche évite le besoin de logique de séparation en exploitant la séparation statique de la mémoire de Move (modèle de ressources), conduisant à des encodages SMT plus efficaces.
Inférence de spécification : Une extension de l'outil d'analyse de la plus faible précondition (WP) de MVP pour gérer le code d'ordre supérieur. Cet outil dérive semi-automatiquement des spécifications basées sur des prédicats comportementaux à partir de bytecode Move arbitraire, réduisant la charge d'annotation manuelle et fournissant un pipeline de validation pour les nouveaux constructs.
Gestion des effets de bord impératifs : Contrairement à certains outils existants (par exemple, Dafny), cette approche prend en charge les fonctions impératives de première classe modifiant l'état via des références de style Rust et des variables globales.

Résultats et validation
Les auteurs démontrent l'approche en utilisant un exemple de Market Maker Automatisé (AMM) où une courbe de prix est stockée sous forme de valeur-fonction. Le système vérifie avec succès :

Invariants : Des propriétés telles que « la fonction n'arrête jamais », « monotonie de la sortie » et « préservation du produit constant » sont vérifiées à l'aide de prédicats comportementaux et d'étiquettes d'état.
Vérification de conformité : L'outil d'inférence de spécification dérive automatiquement les conditions d'arrêt pour les fonctions de prix (par exemple, détecter qu'une fonction de prix basée sur des frais arrête si une ressource de frais est manquante), permettant des vérifications de conformité lisibles par machine sans annotations manuelles.
Suite de tests : Une suite de tests complète couvrant les appels directs, la récursion mutuelle, les paramètres d'ordre supérieur et le dispatch de fermetures stockées confirme que l'encodage est cohérent en interne et que les spécifications inférées sont suffisamment précises pour que le vérificateur les valide.

Signification
L'article affirme que ce travail permet la vérification routinière et orientée production des contrats intelligents Move présentant un dispatch dynamique et des fonctions d'ordre supérieur. En préservant le modèle de coûts de MVP — où la vérification s'achève en quelques secondes par fonction — l'extension permet aux développeurs d'utiliser des motifs complexes tels que les flux d'actifs basés sur des callbacks et les gestionnaires d'actifs extensibles avec des garanties formelles. L'approche se distingue des outils basés sur la logique de séparation en exploitant la séparation statique inhérente de la mémoire de Move pour simplifier les encodages SMT. De plus, l'intégration de l'inférence de spécification offre une voie pratique pour vérifier la conformité des valeurs-fonction, répondant à un obstacle majeur à l'adoption des fonctions d'ordre supérieur dans les contrats intelligents critiques pour la sécurité. Le travail reconnaît que, si la vérification côté application est désormais comparable à celle des fonctions d'ordre premier, la vérification côté conformité (prouver qu'une fonction passée satisfait un contrat) peut encore nécessiter des indices de preuve manuels ou des hypothèses de confiance dans des cas complexes.