La machinerie de la preuve

Types, invariants, solveurs : par quels moyens concrets une machine démontre quelque chose sur un programme

L'article précédent a posé le principe : le raisonnement suit la forme du programme. Reste à voir qui raisonne, et comment. Il existe cinq familles d'outils. Elles ne font pas la même chose, elles ne coûtent pas la même chose, et on les emploie rarement seules.

I. Les types : la preuve que tout le monde utilise déjà

Commençons par le cas où la preuve est si banale qu'on ne la voit plus.

fonction longueur(texte : Texte) : Entier

Cette ligne énonce une propriété : pour toute exécution, si l'argument est un texte, le résultat est un entier. Le compilateur la vérifie avant toute exécution. S'il accepte le programme, il est démontré qu'aucune exécution ne renverra un texte ni ne recevra une date.

C'est une preuve. Elle porte sur une infinité de cas, elle est automatique, elle est instantanée. Chaque compilation d'un programme typé est un petit théorème vérifié par une machine.

La propriété démontrée est faible : « c'est un entier », pas « c'est le bon entier ». Mais la classe de fautes ainsi éliminée est, en pratique, considérable — et le coût est nul.

L'intérêt est qu'on peut monter. Rien n'oblige un type à se limiter à « entier ». Certains langages permettent d'écrire l'équivalent de :

fonction tete(liste : Liste non vide) : Element

Appeler tete sur une liste vide ne devient pas une erreur à l'exécution : cela devient un programme qui ne compile pas. La faute a changé de nature. Elle n'est plus un événement possible, elle est une phrase impossible à écrire.

Poussé à bout, ce mécanisme permet d'exprimer dans un type des énoncés arbitrairement précis — « cette fonction renvoie une liste triée, permutation de son entrée ». Le compilateur devient alors un vérificateur de démonstration à part entière. C'est le contenu de la correspondance de Curry-Howard : un type est un énoncé, un programme de ce type en est une démonstration. Ce n'est pas une métaphore mais une correspondance formelle, terme à terme, et c'est le fondement des assistants de preuve dont il sera question plus bas.

Le prix à payer est que le programmeur doit alors convaincre le compilateur, ce qui est parfois plus long qu'écrire le programme.

II. Les contrats : dire ce qu'on attend et ce qu'on promet

L'étage suivant consiste à annoter les fonctions avec deux énoncés logiques.

// exige :   diviseur != 0
// garantit : resultat * diviseur <= dividende
fonction division(dividende, diviseur) { ... }

La précondition (exige) est ce que l'appelant doit assurer. La postcondition (garantit) est ce que la fonction promet en retour. C'est un contrat au sens juridique, avec la même logique de responsabilité : si l'appelant viole la précondition, la fonction ne doit plus rien.

Cette répartition est ce qui rend la vérification modulaire, et la modularité est ce qui la rend faisable. Pour démontrer qu'une fonction est correcte, l'outil n'a pas besoin de lire le code des fonctions qu'elle appelle : leurs contrats lui suffisent. Un programme d'un million de lignes se vérifie fonction par fonction. Sans cela, il faudrait raisonner sur le programme entier d'un seul tenant, et rien de sérieux ne passerait à l'échelle.

Le raisonnement lui-même a été formalisé par Tony Hoare en 1969, sous la forme de triplets notés

{P} C {Q}

qui se lisent simplement : si P est vrai avant d'exécuter C, alors Q est vrai après. La logique de Hoare fournit une règle par construction du langage — une pour l'affectation, une pour la séquence, une pour le si, une pour la boucle — et ces règles s'enchaînent mécaniquement le long du texte du programme. C'est la mise en forme rigoureuse du principe « le raisonnement suit la forme du programme ».

III. Les invariants de boucle : le seul endroit qui résiste

Tout ce qui précède se traite mécaniquement. Les boucles, non. C'est le point dur de toute la discipline, et il vaut la peine de s'y arrêter.

Une boucle peut tourner zéro, trois, ou un million de fois. Son effet n'est pas déterminé par sa seule forme. Il faut trouver un énoncé qui reste vrai à chaque tour, quel que soit leur nombre : un invariant.

Somme des éléments d'un tableau :

s = 0
i = 0
tant que i < n :
    s = s + t[i]
    i = i + 1

Invariant : s est la somme des i premiers éléments de t.

Vérifions-le en trois temps — ce sont exactement les trois obligations que l'outil produira.

À l'entrée. i = 0, s = 0. La somme de zéro élément vaut zéro. Vrai.
Conservation. Supposons l'invariant vrai en début de tour : s est la somme des i premiers. Le corps ajoute t[i], donc s devient la somme des i+1 premiers ; puis i devient i+1. L'invariant est de nouveau vrai. Vrai.
À la sortie. La boucle s'arrête quand i = n. L'invariant donne : s est la somme des n premiers éléments — c'est-à-dire de tout le tableau. C'est la postcondition voulue.

Trois vérifications, aucune exécution, et la conclusion vaut pour tout n. Le lecteur aura reconnu une récurrence : initialisation, hérédité, conclusion. C'est le seul argument mathématique réellement nécessaire à toute cette histoire, et il est enseigné au lycée.

Deux avertissements.

L'invariant n'est pas déductible du code. C'est l'idée qui explique pourquoi la boucle est écrite ainsi ; le code n'en est que la trace. Trouver l'invariant, c'est comprendre l'algorithme, et cela reste largement un travail humain. Les outils savent en deviner de simples ; pour un algorithme non trivial, c'est le programmeur qui l'écrit. C'est là que passe l'essentiel du coût de la vérification.

L'invariant ne dit rien de la terminaison. L'invariant garantit que si la boucle s'arrête, le résultat est bon. Une boucle qui tourne indéfiniment le respecte parfaitement. Pour la terminaison il faut un second argument, un variant : une quantité entière positive qui décroît strictement à chaque tour. Ici n - i convient : elle diminue de un par tour et ne peut pas descendre sous zéro, donc le nombre de tours est fini. On distingue pour cette raison la correction partielle (le résultat est bon si on l'obtient) de la correction totale (on l'obtient, et il est bon).

IV. Les solveurs : la force de frappe

Une fois les contrats et les invariants posés, un outil parcourt le programme et applique les règles de Hoare. Il en sort ce qu'on appelle des obligations de preuve : des formules logiques pures, où il ne reste plus une seule instruction.

Pour la boucle précédente, la deuxième obligation ressemble à :

Pour tous entiers i, n, s : si 0 ≤ i < n et s = somme(t, 0, i), alors s + t[i] = somme(t, 0, i+1).

Le programme a disparu. Il ne reste que des mathématiques. C'est la transformation centrale de tout l'édifice : la vérification de programme a été ramenée à de la démonstration de formules, et on peut désormais employer une machine spécialisée dans les formules.

Cette machine s'appelle un solveur SMT — Z3, cvc5, Alt-Ergo. Le nom compte peu ; ce qu'il fait compte beaucoup. Un solveur SMT décide si une formule est valide dans des théories utiles au programmeur : arithmétique entière, arithmétique 32 et 64 bits avec débordement, tableaux, listes, structures, flottants.

Sa méthode est un retournement instructif : il ne cherche pas à démontrer la formule, il cherche un contre-exemple. Il nie l'énoncé et tente de construire des valeurs qui le rendent faux.

S'il en trouve un, il le rend. Ce n'est pas un message d'erreur : c'est un jeu de valeurs concret qui casse le programme. Pour la dichotomie de l'article précédent, il aurait répondu bas = 1 073 741 825, haut = 2 147 483 647 — les deux nombres qu'aucun test n'avait essayés en vingt ans.
S'il démontre qu'aucun contre-exemple n'existe, la formule est valide. La propriété est établie.
S'il ne conclut pas dans le temps imparti, il le dit. Ce troisième cas est fréquent et constitue la principale friction du métier : l'outil ne répond ni oui ni non, et il faut l'aider en découpant la propriété, en ajoutant des étapes intermédiaires, en simplifiant le code.

Le solveur est le moteur commun de presque tous les vérificateurs modernes. Ses progrès depuis les années 2000 expliquent pour l'essentiel que la vérification soit passée du laboratoire à l'industrie.

V. Le model checking : explorer tous les états

Les outils précédents raisonnent sur un programme séquentiel. Il existe une classe de problèmes où ils sont mal armés : les systèmes concurrents — plusieurs processus, plusieurs machines, des messages qui se croisent, se perdent, arrivent dans le désordre.

Ces systèmes n'échouent presque jamais à cause d'une ligne fausse. Ils échouent à cause d'un entrelacement : un enchaînement d'événements que personne n'avait envisagé parce qu'il exige que trois choses improbables se produisent dans un ordre précis. Un tel scénario ne se teste pas — il se reproduit une fois sur dix millions, en production, sous charge.

Le model checking attaque autrement : on ne vérifie pas le code, on écrit un modèle du système — ses états, ses transitions — et l'outil énumère tous les états atteignables. Tous, exhaustivement. Puis il vérifie sur chacun les propriétés voulues : « deux processus ne sont jamais ensemble dans la section critique », « toute requête reçoit finalement une réponse ».

Quand une propriété est violée, l'outil ne dit pas seulement « faux ». Il rend la trace : la suite exacte d'événements qui mène à la faute. Un scénario de bug, lisible, reproductible.

L'obstacle porte un nom : l'explosion combinatoire. Dix processus à dix états chacun font dix milliards de combinaisons. Trois familles de parades l'ont rendu praticable : la représentation symbolique, qui manipule des ensembles d'états plutôt que des états un par un ; la réduction d'ordre partiel, qui ignore les entrelacements équivalents ; et le model checking borné, qui n'explore que les exécutions de longueur limitée — incomplet, mais redoutable pour trouver des fautes.

TLA+, conçu par Leslie Lamport, est le représentant le plus connu. Amazon Web Services l'emploie depuis le début des années 2010 sur ses systèmes distribués — S3, DynamoDB — et le compte rendu publié en 2015 est franc : la méthode a mis au jour des défauts « subtils », dans des protocoles relus par des ingénieurs chevronnés, qu'aucune autre technique n'aurait trouvés.

À noter, car c'est une différence de nature : on vérifie le modèle, pas le code. Que le programme implémente fidèlement le modèle reste à établir par d'autres moyens. On n'a pas démontré que le système est correct ; on a démontré que sa conception l'est — ce qui est déjà l'endroit où logent les fautes les plus coûteuses.

VI. L'interprétation abstraite : approximer sans jamais se tromper de côté

Une cinquième approche, différente des quatre autres, mérite d'être connue parce qu'elle passe à l'échelle industrielle sans annotation humaine.

L'idée : au lieu de suivre les valeurs exactes, on suit une approximation délibérément grossière.

Plutôt que « x vaut 7 », on retient « x est dans l'intervalle [0, 10] ». Plutôt que d'explorer les deux branches d'un si séparément, on fusionne les intervalles. Le domaine abstrait est petit, le calcul converge vite, et un programme d'un million de lignes s'analyse en quelques heures sans que personne ait rien annoté.

La contrepartie est une asymétrie qu'il faut avoir en tête pour interpréter les résultats. L'approximation est choisie pour être toujours plus large que la réalité : l'ensemble calculé contient à coup sûr toutes les valeurs réellement possibles. Par conséquent :

Aucune alarme ⇒ aucune erreur. Si l'analyse ne signale rien sur une division, c'est que le diviseur n'est nul dans aucune exécution. Cette garantie est solide.
Une alarme ⇒ peut-être rien. L'erreur signalée peut n'exister que dans l'approximation, pas dans le programme. C'est une fausse alarme, et le travail de l'ingénieur consiste largement à les trier.

Tout l'art consiste à choisir des domaines abstraits assez fins pour que les fausses alarmes restent rares. L'analyseur Astrée, développé en France, a été affiné jusqu'à atteindre zéro fausse alarme sur les logiciels de commande de vol des Airbus A340 et A380 : il y démontre l'absence d'erreurs à l'exécution — débordement, division par zéro, accès hors bornes — sur des centaines de milliers de lignes, sans aucune annotation.

VII. Les assistants de preuve : quand la machine ne suffit plus

Pour les propriétés qu'aucun outil automatique n'atteint, il reste la méthode la plus lourde et la plus puissante : l'humain écrit la démonstration, la machine la vérifie.

Rocq (longtemps nommé Coq), Isabelle et Lean sont les principaux. On y écrit le programme, l'énoncé, puis la preuve — étape par étape, avec de l'automatisation locale, mais sous conduite humaine. L'outil ne laisse passer aucun trou : pas de « on montre de même », pas de « le cas suivant est analogue ».

La confiance repose sur un point d'architecture décisif : le noyau. Toute la preuve, aussi longue soit-elle, est finalement relue par un vérificateur minuscule — quelques milliers de lignes — qui applique les règles logiques de base. Le reste de l'outil peut être aussi compliqué qu'on voudra : une preuve fausse ne franchit pas le noyau. On concentre ainsi toute la confiance sur un morceau assez petit pour être audité à la main.

Deux réalisations donnent la mesure de ce qu'on obtient, et de ce qu'on paie.

CompCert est un compilateur C dont la traduction est démontrée en Rocq : le code machine produit a exactement le comportement du code source. Cela résout un problème gênant — à quoi bon prouver un programme si le compilateur le traduit mal ? Une étude publiée en 2011, qui a soumis les principaux compilateurs C à des millions de programmes engendrés au hasard, a trouvé des fautes de génération de code dans tous, sauf dans la partie vérifiée de CompCert. Les auteurs notent qu'il s'agit du seul compilateur de leur panel où leur outil n'a trouvé aucune erreur de ce type.

seL4 est un micro-noyau de système d'exploitation dont la conformité à sa spécification a été démontrée en Isabelle, vers 2009. L'ordre de grandeur est éloquent : environ dix mille lignes de C, et de l'ordre de deux cent mille lignes de preuve — soit une vingtaine de lignes de démonstration par ligne de code, et des années-hommes d'effort.

Ce rapport est le vrai sujet de l'article suivant.

Récapitulation

Méthode	Ce qu'elle démontre	Coût	Limite principale
Types	Cohérence des valeurs manipulées	Nul	Propriétés faibles
Contrats + solveur	Conformité d'une fonction à sa spécification	Moyen	Les invariants restent à écrire
Model checking	Correction d'un protocole concurrent	Moyen	Vérifie le modèle, pas le code
Interprétation abstraite	Absence d'erreurs à l'exécution	Faible	Fausses alarmes
Assistant de preuve	Tout ce qui est énonçable	Très élevé	La preuve est écrite à la main

Aucune de ces méthodes ne remplace les autres. Un projet sérieux les empile : des types partout, des contrats aux frontières, un analyseur statique en intégration continue, du model checking sur les protocoles, un assistant de preuve sur le noyau critique — et des tests, toujours, parce qu'ils attrapent ce qu'on avait mal spécifié.