💻 computer science

Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean

Cet article présente une formalisation dans Lean, vérifiée par machine, d'une logique modale polyadique hybride générale à plusieurs sortes avec un mécanisme de tri intrinsèque et un langage dédié au domaine, fournissant un cadre robuste et polyvalent pour la spécification et la vérification de langages de programmation et de protocoles de sécurité.

Auteurs originaux : Andrei-Alexandru Oltean, Bogdan Macovei, Ioana Leuştean

Publié 2026-06-26

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Andrei-Alexandru Oltean, Bogdan Macovei, Ioana Leuştean

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 que vous soyez un architecte essayant de construire une « boîte à outils logique » universelle qui puisse être utilisée pour vérifier si des programmes informatiques fonctionnent correctement, si des messages secrets dans des protocoles de sécurité sont sûrs, ou si des arguments philosophiques tiennent la route. Le problème est que chaque tâche nécessite un ensemble d'outils légèrement différent, et qu'en général, vous devez construire une nouvelle boîte à outils à partir de zéro pour chacune d'elles.

Ce document présente une solution : une boîte à outils logique universelle, vérifiée par machine, construite à l'intérieur d'un programme appelé Lean. Les auteurs ont créé un système suffisamment flexible pour gérer des règles complexes et multicouches (à plusieurs sortes) et capable d'examiner simultanément différents « états » ou « mondes » (logique hybride).

Voici une décomposition de leur travail utilisant des analogies de la vie quotidienne :

1. L'astuce de la liste : Construire avec des briques LEGO

Le plus grand défi de ce projet était de s'assurer que les règles de la logique soient suivies automatiquement, sans nécessiter l'intervention d'un humain pour vérifier chaque étape.

Le Problème : Dans la logique traditionnelle, vous pourriez écrire une formule puis devoir exécuter un « correcteur orthographique » séparé pour voir si elle a du sens (ex : « Avez-vous essayé d'ajouter un nombre à une phrase ? »).
La Solution (L'astuce de la liste) : Les auteurs ont traité les formules logiques comme des listes de briques LEGO. Ils ont conçu le système de sorte que vous ne puissiez physiquement pas emboîter deux briques incompatibles. Si vous essayez de connecter une brique « rouge » (un type de règle spécifique) à une brique « bleue » (un type différent), le système refusera simplement de les assembler.
Pourquoi c'est important : Cela signifie que si une formule existe dans leur système, elle est garantie correcte par définition. Ils n'ont pas besoin de vérifier les erreurs plus tard car la structure elle-même empêche les erreurs de se produire dès le départ.

2. Le pointeur de « Contexte » : Trouver une aiguille dans une botte de foin

La logique qu'ils ont construite permet des opérations complexes où vous pourriez avoir besoin de modifier une partie spécifique d'une phrase longue et compliquée.

L'Analogie : Imaginez que vous avez un long paragraphe de texte et que vous voulez remplacer le mot « chat » par « chien ». Dans un document normal, vous pourriez simplement faire un « rechercher et remplacer ». Mais dans leur système, il pourrait y avoir plusieurs « chats », et vous devez changer uniquement celui de la deuxième phrase, pas celui de la cinquième.
La Solution : Ils ont créé un « pointeur » numérique (appelé Contexte). Ce pointeur est comme une coordonnée GPS qui dit : « Je pointe spécifiquement vers le "chat" de la deuxième phrase. » Lorsqu'ils appliquent une règle, ils utilisent ce pointeur pour remplacer exactement ce mot spécifique, laissant tout le reste intact. Cela leur permet de gérer des règles complexes à plusieurs parties sans s'embrouiller.

3. Le DSL : Un « Traducteur de Langage »

Pour rendre ce système puissant utilisable par des personnes ordinaires (comme des programmeurs ou des experts en sécurité), les auteurs ont construit un Langage Spécifique au Domaine (DSL).

L'Analogie : Considérez la logique centrale comme un langage de programmation de haut niveau (comme le C++ ou l'Assembly) qui est très puissant mais difficile à lire. Le DSL est comme un traducteur qui permet aux utilisateurs d'écrire dans un style convivial et familier (comme une recette ou un organigramme).
Comment ça marche : Un utilisateur peut écrire une règle qui ressemble à un programme informatique standard (ex : « Si X, alors fais Y »). Le système traduit automatiquement cela en briques logiques sous-jacentes complexes. Cela signifie que les utilisateurs n'ont pas besoin d'être des logiciens pour utiliser le système ; ils ont seulement besoin de connaître leur domaine spécifique (comme le codage ou la sécurité).

4. Trois tests en conditions réelles

Pour prouver que leur boîte à outils fonctionne, ils l'ont utilisée pour résoudre trois problèmes très différents :

Le Vérificateur de Programme (Machine SMC) : Ils ont utilisé le système pour vérifier un programme informatique simple. Ils ont traduit les étapes du programme en leur logique et ont prouvé que si l'on part de nombres spécifiques, le programme aboutira définitivement au résultat correct. C'est comme prouver qu'une équation mathématique est vraie avant même de lancer la calculatrice.
Le Détective de Protocole de Sécurité (Logique BAN) : Ils ont modélisé la façon dont deux personnes échangent des clés secrètes via un réseau. Ils ont utilisé la logique pour prouver que si un message est chiffré avec une clé spécifique, le destinataire peut être sûr à 100 % de l'identité de l'expéditeur. Ils ont vérifié avec succès un protocole de sécurité célèbre (Needham-Schroeder) pour montrer que le système peut détecter les failles de sécurité potentielles.
Le Simplificateur Philosophique (Logique S5) : Ils ont montré que leur système complexe peut également gérer la logique simple et standard (S5). Cela prouve que leur système est assez polyvalent pour être un « couteau suisse » : il peut gérer les scénarios les plus complexes à plusieurs mondes, mais il peut aussi se réduire pour gérer la logique simple et quotidienne si nécessaire.

5. La garantie de « Correction » (Soundness)

L'affirmation la plus importante du document est la Correction (Soundness).

L'Analogie : Imaginez un juge dans un tribunal. Le juge doit être certain que s'il déclare quelqu'un « coupable », la personne a réellement commis le crime selon la loi.
Le Résultat : Les auteurs ont utilisé le logiciel Lean pour prouver mathématiquement que leur système est correct (sound). Cela signifie que : Si le système déclare qu'une affirmation est vraie, il est mathématiquement impossible qu'elle soit fausse. Ils n'ont pas seulement deviné ; ils ont construit une preuve vérifiée par machine que leurs règles ne mènent jamais au mensonge.

Résumé

En bref, les auteurs ont construit un moteur logique ultra-flexible et infaillible à l'intérieur d'un programme informatique. Ils ont créé une manière pour les utilisateurs de définir leurs propres règles facilement, ont traduit ces règles dans un format que l'ordinateur peut vérifier avec une certitude de 100 %, et ont prouvé que le moteur fonctionne correctement pour tout, de la vérification de code à la sécurisation de messages numériques. C'est un traducteur universel qui transforme les idées humaines en vérités mathématiquement garanties.

Résumé technique : Formalisation d'une logique modale hybride polyadique à plusieurs tris dans Lean

Énoncé du problème

Le document traite du défi consistant à fournir un fondement axiomatique uniforme et mathématiquement rigoureux pour spécifier et vérifier des systèmes divers, tels que les langages de programmation et les protocoles de sécurité. Les formalisations existantes manquent souvent de la flexibilité nécessaire pour gérer des signatures à plusieurs tris (où différents types d'entités existent) et des opérateurs modaux polyadiques (opérateurs ayant des arités arbitraires) au sein d'un cadre unique. De plus, bien que les logiques hybrides (qui incluent des nominaux et des variables d'état) soient puissantes pour référencer des états spécifiques, leur formalisation dans les assistants de preuve a traditionnellement été limitée aux contextes mono-trés ou monadiques. Les auteurs visent à combler cette lacune en créant un cadre général dans l'assistant de preuve Lean qui supporte des signatures arbitraires, des opérateurs polyadiques et des fonctionnalités hybrides, tout en garantissant que la syntaxe est intrinsèquement bien triée pour éviter les erreurs de type lors de la vérification.

Méthodologie

Les auteurs implémentent une formalisation de la logique modale hybride générale $H_\Sigma(@, \forall)$ dans la théorie des types dépendants de Lean. Leur méthodologie repose sur trois innovations techniques fondamentales :

1. Tri intrinsèque via le « List Trick » (l'astuce de la liste)

Pour éviter le besoin de fonctions séparées de « vérification de tri », les auteurs utilisent les types dépendants de Lean pour imposer les contraintes de tri au niveau du type.

Types inductifs : Les formules sont représentées par un type inductif FormL indexé par une List de tris (sorts).
Le List Trick : Alors que les formules standards correspondent à des listes de tris à élément unique, les auteurs introduisent un constructeur artificiel cons qui permet de construire des listes de formules indexées par des listes de tris non singulières.
Mécanisme : Les opérateurs modaux sont définis pour prendre une liste d'arguments (les domaines des tris) et retourner une formule d'un tri de portée spécifique. Le vérificateur de type vérifie que la liste des tris d'arguments correspond exactement à la signature du domaine de l'opérateur. Cela garantit que tout terme construit est une formule bien triée par définition.
Contextes : Pour gérer les opérateurs polyadiques et les axiomes impliquant des arguments génériques (par exemple, la substitution au sein d'un emplacement d'argument arbitraire d'un opérateur), les auteurs définissent un type inductif Context. Un Context agit comme un pointeur vers une occurrence spécifique d'une sous-formule au sein d'une liste de formules, permettant une substitution rigoureuse sans dépendre d'une notation informelle « ... ».

2. Formalisation sémantique

La sémantique est définie à l'aide de cadres de Kripke et de modèles qui sont également à plusieurs tris.

Mondes : Un cadre (frame) associe à chaque tri un type dans un univers.
Relations d'accessibilité : Les relations sont définies comme des ensembles de WProd (un type produit construit à partir de la liste des tris), représentant des tuples de mondes qui satisfont la relation.
Satisfaction : La relation de satisfaction est définie de manière récursive. Le « list trick » simplifie la gestion des opérateurs polyadiques : la satisfaction d'une liste d'arguments est définie comme la satisfaction simultanée de la liste à un produit de mondes.

3. Extensions axiomatiques et système de preuve

Le système de preuve est paramétrique par rapport à une extension axiomatique $\Lambda$ .

Ensembles d'axiomes : Les axiomes sont définis comme des ensembles de formules S-triés.
Preuves inductives : Le type Proof est une famille inductive. Crucialement, les auteurs utilisent des types inductifs pour définir des schémas d'axiomes. Au lieu de lister manuellement des instances infinies, ils définissent une famille inductive d'axiomes (par exemple, pour la machine SMC ou la logique BAN) où les constructeurs représentent des motifs de schémas. L'ensemble des théorèmes est alors la clôture de ces schémas sous les règles de déduction.
Correction (Soundness) : Les auteurs prouvent le Théorème de correction du cadre (Frame-Soundness Theorem) : si une formule est prouvable à partir d'un ensemble d'axiomes $\Lambda$ , elle est valide dans tous les cadres où $\Lambda$ est valide.

Contributions clés et résultats

Formalisation générale : Le papier présente la première formalisation vérifiée par machine d'une logique modale hybride polyadique à plusieurs tris générale dans Lean. Ce système supporte des signatures arbitraires, des opérateurs polyadiques et des fonctionnalités hybrides (nominaux, opérateurs de satisfaction $@$ et lieurs $\forall$ ).
Correction mécanisée : Une preuve complète et « sans sorry » (sans recours à l'omission de preuve) du théorème de correction est fournie. Au cours de ce processus, les auteurs ont identifié et corrigé des erreurs dans la présentation originale du système de preuve trouvée dans la littérature antérieure (spécifiquement concernant l'axiome de Barcan et les règles Name@ et Paste), fournissant une version corrigée avec les conditions latérales syntaxiques nécessaires.
DSL pour la définition de signatures : Les auteurs ont développé un langage de domaine spécifique (DSL) utilisant le mot-clé hybrid_def. Cela permet aux utilisateurs de définir des signatures à plusieurs tris en utilisant une notation familière de type BNF (Backus-Naur Form), qui est automatiquement élaborée dans les structures de données sous-jacentes de Lean (Symbols, Signature, etc.).
Trois applications vérifiées : La polyvalence du cadre est démontrée par trois applications distinctes :
- Machine SMC (Analyse de programme) : Les auteurs ont formalisé la sémantique opérationnelle de la machine SMC (un langage impératif) en tant que signature de logique hybride. Ils ont dérivé des règles d'inférence de type Hoare et ont vérifié la correction d'un programme impliquant l'échange de variables et l'exécution conditionnelle avec effets de bord.
- Protocoles de sécurité : Le cadre a été utilisé pour intégrer la logique BAN et une logique hybride pour les protocoles de sécurité. Ils ont vérifié les propriétés d'authentification dans le protocole Needham-Schroeder Public Key (NSPK) et ont analysé le protocole One-Sided Secrecy (OSS), prouvant l'authentification mutuelle et les propriétés de connaissance.
- Logique modale S5 : Les auteurs ont démontré que le système peut se restreindre à un fragment purement modal (en supprimant les fonctionnalités hybrides) pour définir et prouver des théorèmes dans le système S5, montrant la capacité du cadre à gérer des fragments moins expressifs de la logique de base.

Signification et revendications

Le papier affirme que le système proposé sert de cadre de vérification général capable d'unifier la spécification des langages de programmation, leurs sémantiques opérationnelles et les propriétés de correction au sein d'un fondement logique unique.

Modularité et extensibilité : Les auteurs soulignent que l'architecture est modulaire. Les utilisateurs peuvent définir des langages ou des protocoles personnalisés comme des signatures à plusieurs tris et spécifier des axiomes propres au domaine sans modifier la logique centrale.
Sécurité intrinsèque : En utilisant le tri intrinsèque, le cadre garantit que toute formule construite est un parse valide de la grammaire définie, éliminant une classe d'erreurs communes dans d'autres formalisations.
Outil de recherche : La représentation des variables comme des noms concrets (plutôt que des indices de de Bruijn) est un choix délibéré pour faciliter la migration de la recherche en logique « papier-crayon » vers le cadre formel, minimisant la surcharge de représentation.

Ce travail se positionne comme une fondation rigoureuse pour de futures extensions, notant spécifiquement que le Théorème de Complétude reste une cible pour de futures mécanisations, et que le développement de tactiques conviviales est une priorité pour rendre le système accessible aux non-experts dans les détails de l'implémentation. Le code est disponible en libre accès, soutenant la reproductibilité et le développement ultérieur dans le domaine des méthodes formelles.