💻 computer science

Satisfiability Modulo Extensional Constant Arrays (Extended Version)

Cet article présente une nouvelle procédure de décision correcte pour la théorie SMT des tableaux extensionnels avec tableaux constants, qui prend en charge des domaines d'index arbitraires, surmontant les limitations précédentes aux cas finis ou infinis, et démontre son efficacité grâce à son implémentation dans le solveur Bitwuzla.

Auteurs originaux : Mathias Preiner, Aina Niemetz, Clark Barrett

Publié 2026-05-20

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Mathias Preiner, Aina Niemetz, Clark Barrett

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 êtes un détective tentant de résoudre une énigme impliquant une bibliothèque massive et infinie de livres (un tableau). Chaque livre possède un numéro de case spécifique (un indice) et contient une histoire (un élément).

Dans le monde de la vérification informatique, nous devons souvent poser des questions telles que : « Si je modifie l'histoire de la case 5, l'histoire de la case 10 change-t-elle ? » ou « Ces deux bibliothèques sont-elles exactement identiques ? »

Pendant longtemps, les outils utilisés pour répondre à ces questions (appelés solveurs SMT) présentaient un angle mort majeur. Ils excellaient à gérer des bibliothèques où l'on pouvait modifier des livres individuels, mais ils peinaient lorsque la bibliothèque commençait avec une « histoire par défaut » écrite sur chaque page unique avant même que vous ne commenciez.

Le Problème : Le Dilemme de la « Page Blanche »

Imaginez une bibliothèque où chaque livre commence par la même histoire par défaut : « La Fin ».

L'Ancienne Méthode : Si vous vouliez dire à l'ordinateur : « D'accord, conservez « La Fin » partout, mais modifiez la case 5 en « Chapitre 1 » », l'ordinateur devait écrire une liste massive et imbriquée : « Modifiez la case 5, puis modifiez la case 6, puis modifiez la case 7... » jusqu'à l'infini.
Le Résultat : Cela rendait l'ordinateur lent, confus et sujet aux erreurs. C'était comme essayer de décrire un mur blanc en listant chaque pixel blanc individuellement.

De plus, les outils précédents ne pouvaient gérer ce concept d'« histoire par défaut » que si la bibliothèque était infinie. Si la bibliothèque était finie (comme une petite étagère avec seulement 4 cases), les anciens outils donnaient souvent la mauvaise réponse. Ils ne parvenaient pas à comprendre que si vous écrasez chaque case unique sur une petite étagère, l'« histoire par défaut » n'a plus d'importance.

La Solution : Le « Tampon Magique »

Les auteurs de cet article, Mathias Preiner, Aina Niemetz et Clark Barrett, ont construit une nouvelle procédure de décision (un nouvel ensemble de règles pour le détective) appelée CAEXT.

Imaginez leur solution comme un Tampon Magique.
Au lieu de lister chaque livre individuellement, vous pouvez maintenant dire : « Toute cette étagère est estampillée avec l'histoire « La Fin ». »

L'Innovation : Leur nouveau système peut gérer ce « Tampon Magique » que l'étagère soit infinie ou simplement une toute petite étagère finie.
L'Astuce : Ils ont réalisé que pour une étagère finie, vous n'avez besoin de vérifier que si vous avez estampillé chaque case. Si c'est le cas, l'étagère n'est plus que la nouvelle histoire. Si ce n'est pas le cas, l'« histoire par défaut » s'applique toujours aux cases vides.

Comment Cela Fonctionne (Le Jeu de la « Relais »)

L'article décrit leur méthode comme un jeu de Passage du Témoignage.

Le Déroulement : Vous avez une étagère avec un « Tampon Magique » (un tableau constant) et certaines modifications spécifiques (des mises à jour).
La Poursuite : Le système tente de retracer le chemin de l'information. Si vous modifiez la case 1, cette modification affecte-t-elle la case 2 ?
Le Conflit : Parfois, le système trouve une contradiction. Par exemple, il pourrait constater que « La case 1 est « La Fin » » mais aussi que « La case 1 est « Chapitre 1 » ».
La Résolution : Les nouvelles règles permettent au système de dire : « Attendez, si l'étagère ne contient que 4 cases, et que j'ai modifié 4 cases différentes, alors le « Tampon Magique » a complètement disparu. L'étagère n'est maintenant que les nouvelles histoires. »

L'article prouve mathématiquement que ce nouvel ensemble de règles est sain. Cela signifie :

Fidélité Réfutationnelle : Si le système dit « C'est impossible », c'est 100 % correct. Il ne ment jamais sur une contradiction.
Fidélité de Satisfaisabilité : Si le système dit « C'est possible », c'est 100 % correct. Il ne ment jamais sur l'existence d'une solution.

Le Test du Monde Réel

Les auteurs n'ont pas seulement écrit de la théorie ; ils ont construit un outil appelé Bitwuzla et l'ont testé contre d'autres outils de premier plan (comme Z3, cvc5 et MathSAT5).

Les Résultats : Leur nouvel outil a résolu significativement plus d'énigmes que les autres.
Le « Piège » : Ils ont découvert que les autres outils, confrontés à ces énigmes d'« étagère finie », donnaient souvent de mauvaises réponses. Ils déclaraient une énigme soluble alors qu'elle ne l'était pas, ou l'inverse. Bitwuzla, en utilisant leur nouvelle logique de « Tampon Magique », a eu raison à chaque fois.
Où cela a été utilisé : Ils l'ont testé sur des problèmes réels comme la vérification de conceptions matérielles et la validation de contrats intelligents (accords numériques) sur la blockchain Ethereum.

Résumé

En termes simples, cet article introduit une manière plus intelligente pour les ordinateurs de raisonner sur des structures de données qui commencent avec une valeur par défaut.

Avant : Les ordinateurs étaient lents et confus lorsqu'ils traitaient des « valeurs par défaut » sur de petits ensembles de données finis.
Maintenant : La nouvelle méthode traite ces défauts comme un « Tampon Magique » qui peut être facilement suivi et écrasé, fonctionnant parfaitement pour les scénarios infinis et finis.
Impact : Cela rend les outils informatiques utilisés pour vérifier des logiciels critiques pour la sécurité (comme les voitures autonomes ou les contrats blockchain) plus rapides, plus précis et capables de résoudre des problèmes qui étaient auparavant impossibles.

Résumé technique : Satisfiabilité modulo tableaux constants extensionnels

Énoncé du problème

Le raisonnement sur les structures de données tableaux, en particulier en combinaison avec des entiers machine, constitue une exigence fondamentale pour la vérification matérielle et logicielle. La théorie standard des tableaux extensionnels (Satisfiability Modulo Theories, SMT), telle que définie dans SMT-LIB et axiomatisée par McCarthy, fournit les opérateurs select (lecture) et store (écriture) ainsi qu'un axiome d'extensionnalité. Bien que suffisante pour de nombreuses tâches de vérification, cette théorie manque de concision lors de la modélisation de tableaux initialisés avec une valeur par défaut (par exemple, une mémoire initialisée à zéro).

Dans la théorie standard, une telle initialisation doit être exprimée via des expressions store profondément imbriquées écrivant la valeur par défaut à chaque index pertinent. Cela entraîne des imprécisions de modélisation (les index ne peuvent être écrasés explicitement) et des inefficacités sévères dans les procédures de résolution en raison de la profondeur des chaînes de store.

L'extension de la théorie avec des tableaux constants — des tableaux stockant un seul élément à chaque index — offre une solution concise. Cependant, les procédures de décision existantes pour les tableaux constants extensionnels sont restreintes aux domaines d'index infinis. Pour les domaines d'index finis, les solveurs SMT existants ne prennent en charge que des fragments non extensionnels ou, dans le cas de certains solveurs, produisent des réponses incorrectes lors du raisonnement sur l'extensionnalité de tableaux constants avec des index finis. Le défi central réside dans la détermination de savoir si deux séquences d'opérations store sur différents tableaux constants à domaines finis peuvent être rendues égales en mettant à jour suffisamment les index, un problème qui ne se pose pas dans le cas infini.

Méthodologie

Les auteurs présentent une nouvelle procédure de décision pour la théorie des tableaux constants extensionnels ( $T_{\langle A \rangle}$ ) prenant en charge des domaines d'index arbitraires, y compris les domaines finis. La procédure est formalisée comme un calcul abstrait, CAEXT, qui généralise et étend la procédure Lemmas on Demand (LOD) pour les tableaux extensionnels (DPA) présentée dans des travaux antérieurs.

Le calcul CAEXT

Le calcul opère sur des configurations $\langle A, I, \pi \rangle$ , où $A$ est un ensemble de littéraux plats, $I$ est une interprétation dans la théorie vide ( $T_E$ ), et $\pi$ est une carte d'étapes de propagation. La procédure évite l'introduction de lectures virtuelles pour tous les index (ce qui est irréalisable pour les domaines infinis et coûteux en calcul pour les grands domaines finis) en propageant les valeurs par défaut et en suivant les index mis à jour.

Les composants clés du calcul incluent :

Calcul de base (AEXT) : Il généralise la procédure LOD aux sorts d'index et d'éléments arbitraires, la découplant des combinaisons de théories spécifiques. Il propage les informations de lecture basées sur les axiomes de lecture-sur-écriture de McCarthy (row-eq, row-ne) et l'axiome d'extensionnalité (ext).
Extension aux tableaux constants :
- Propagation des valeurs par défaut : Au lieu de générer des lectures pour chaque index, le calcul propage la valeur par défaut $v$ d'un tableau constant $\langle v \rangle$ vers d'autres tableaux. Il maintient un ensemble d'index mis à jour $I(a, \langle v \rangle)$ , représentant les index où le tableau $a$ diffère de la valeur par défaut $\langle v \rangle$ le long du chemin de propagation.
- Détection de conflits (CongC) : Lorsque deux valeurs par défaut différentes $v$ et $w$ sont propagées vers le même tableau $a$ , le calcul vérifie si l'ensemble des index mis à jour $I(a, \langle v \rangle) \cup I(a, \langle w \rangle)$ couvre l'ensemble du domaine d'index. Si le domaine est fini et que les index mis à jour ne couvrent pas tous les index possibles, un conflit survient sauf si $v \approx w$ .
- Encodage DistinctN : Pour traiter efficacement la formule quantifiée $\exists i : \sigma. \bigwedge_{k \in I} i \neq k$ (vérifiant l'existence d'un index non mis à jour), l'implémentation encode cela comme une contrainte spécialisée distinctN. Cela vérifie si l'ensemble des index mis à jour contient au moins $n$ valeurs distinctes, où $n$ est la taille du domaine d'index.

Implémentation

La procédure de décision est implémentée dans le solveur SMT de pointe Bitwuzla. Elle s'intègre de manière transparente à l'architecture LOD existante de Bitwuzla, où le solveur de vecteurs de bits fournit l'interprétation $I$ . L'implémentation inclut des optimisations telles que l'expansion paresseuse des contraintes distinctN et une recherche en largeur pour les chemins de propagation afin de minimiser la surcharge mémoire.

Contributions clés

Généralisation de LOD : Les auteurs généralisent la procédure LOD pour les tableaux extensionnels avec des vecteurs de bits de taille fixe aux sorts d'index et d'éléments arbitraires.
Calcul abstrait AEXT : Ils présentent AEXT comme un calcul abstrait découplé pour la théorie extensionnelle des tableaux, indépendant du paradigme de résolution LOD.
Extension aux tableaux constants (CAEXT) : Ils étendent AEXT pour gérer les tableaux constants extensionnels, prouvant la validité réfutationnelle (si une réponse unsat est rapportée, l'entrée est insatisfaisable) et la validité de satisfiabilité (si une configuration saturée est atteinte sans unsat, l'entrée est satisfaisable).
Implémentation et évaluation : La procédure est implémentée dans Bitwuzla et évaluée sur divers benchmarks, démontrant des améliorations de performance significatives par rapport à Bitwuzla de base et à d'autres solveurs leaders (Z3, cvc5, MathSAT5).

Résultats

L'évaluation a été menée sur cinq ensembles de benchmarks : smtlib (logiques quantifiées), mbqi (sous-requêtes issues de l'instanciation de quantificateurs basée sur les modèles), k-ind (vérification de modèles matériels incrémentale), hevm (machine virtuelle Ethereum) et crafted (benchmarks synthétiques spécifiquement conçus pour tester l'extensionnalité des tableaux constants finis).

Performance : Bitwuzla avec la nouvelle procédure (Bitwuzla⟨A⟩) surpasse nettement tous les autres solveurs. Sur l'ensemble smtlib, le nombre de benchmarks résolus a augmenté d'un facteur 5 par rapport à Bitwuzla de base (3 545 contre 717). Sur l'ensemble mbqi, Bitwuzla⟨A⟩ a résolu les 4 147 requêtes, alors que la version de base n'en a résolu que 4.
Correction : Sur l'ensemble crafted⟨A⟩, qui encode des égalités sur des tableaux constants finis avec des valeurs par défaut différentes, Bitwuzla⟨A⟩ a été le seul solveur à fournir des réponses correctes pour toutes les instances. Z3 et MathSAT5 ont accepté les entrées mais ont rapporté des réponses incorrectes pour un nombre significatif de benchmarks. cvc5 et Bitwuzla de base ont rejeté les entrées en raison d'un manque de prise en charge.
Vérification de la validité : Les auteurs ont vérifié les modèles produits par les solveurs sur l'ensemble crafted⟨A⟩. Seul Bitwuzla⟨A⟩ a produit des modèles cohérents avec ses propres affirmations de satisfiabilité. Z3 et MathSAT5 ont produit des modèles qui, lorsqu'ils étaient réaffirmés sur les formules originales, conduisaient à des contradictions.

Importance

L'article affirme que la procédure de décision proposée étend considérablement les capacités de résolution de Bitwuzla, lui permettant de traiter des problèmes impliquant des tableaux constants extensionnels avec des domaines d'index finis qui étaient auparavant insolubles ou gérés incorrectement par d'autres outils.

Ce travail comble une lacune critique dans la résolution SMT : bien que les tableaux constants soient un modèle standard pour l'initialisation de la mémoire, les solveurs existants soit ne les prennent pas en charge dans les domaines finis, soit fournissent des résultats non valides. En fournissant une procédure de décision valide et complète pour la théorie complète des tableaux constants extensionnels (finis et infinis), ce travail permet une vérification plus précise et efficace dans des applications telles que la vérification de modèles matériels et la vérification de contrats intelligents (spécifiquement pour la Machine Virtuelle Ethereum). Les auteurs notent que, bien que leur évaluation se soit concentrée sur les domaines finis, la procédure est agnostique à l'architecture du solveur sous-jacent et prend en charge pleinement le cas de domaine infini.