Ça fait un petit bout de temps que les questions de preuve de programme m’intéressent. Ça viens en partie d’une certaine frustration que certaines propriétés ne se prêtent vraiment pas aux tests, comme vérifier qu’un parser ne crash pas, mais aussi du fait que je me retrouve en permanence à écrire du code pour vérifier que les arguments de ma fonction sont valide (par exemple que les pointeurs ne sont pas nuls). Même si je peux aller vérifier que maintenant ces vérifications ne sont pas nécessaires et que je peux mettre un commentaire pour dire que les arguments doivent être valide, forcément, il arrivera un jour où une petite modification de rien va casser les préconditions, ce qui ne sera pas forcément détecté par les tests.
Voici une liste non exhaustive de propriétés que l’on pourrais vouloir prouver:
- on ne déréférence pas de pointeurs nuls.
- le programme (ou certaines fonctions en particuliers) se finissent toujours.
- on n’accède pas à un élément hors des limites d’un tableau.
- on ne divise jamais un nombre par 0.
- une fonction de recherche dichotomique n’est appelé qu’avec un conteneur dont le contenu est ordonné.
- la fonction de comparaison donné à une fonction de tri possède certaines propriétés, comme la transitivité.
- deux implémentations différente d’une fonction donnent le même même résultat pour toutes les entrées possibles.
Sur la papier, c’est génial parce que ça permet de garantir que certains bugs ou catégories de bugs ne sont pas présent dans un programme1. En contre partie, il va falloir prouver que toutes ces propriétés sont vrai. D’où la question: à quel point c’est galère de prouver des trucs non-triviaux? Question à laquelle je vais tenter de réponde (très subjectivement) dans cette série d’articles, en plus de présenter mes découvertes.
J’ai choisi de me focaliser sur le langage F* pour plusieurs raisons:
- il est associé à un SMT solver (Z3), qui est sensé s’occuper des parties "triviales" des preuves. C’est absolument nécessaire pour moi: j’ai essayé d’utiliser Lean (qui n’a pas de SMT solver) avant et après avoir passé plusieurs heures à essayer de prouver que
1 > 0, sans réussir, j’ai jeté l’éponge. - c’est avant tout un langage de programmation, avant d’être un outil de preuve de programme. Donc je m’attends à pouvoir écrire un programme utile à peu près aussi facilement que dans n’importe quel autre langage de programmation.
- il m’a donné l’impression d’être l’un des projets les plus mature dans le domaine satisfaisant les deux contraintes précédentes.
Je suis encore un gros débutant avec F* et dans la preuve de programmes de manière générale. Il est parfaitement possible que je raconte des grosses bêtises à un moment dans ce billet, si ce n’est pas déjà fait. Prenez ce que je dis avec des pincettes.
Le logo de l’article est celui de F*, distribué sous licence Apache 2.0.
- À supposer que l’outil de preuve utilisé n’a pas lui-même des bugs et que les propriétés que l’on veut garantir sont correctement décrites.
↩
Une introduction rapide
De prime abord, F* est un langage fonctionnel et ressemble beaucoup à OCaml, dont il s’est inspiré. Ça fait un bout de temps que je n’ai pas touché à OCaml, mais j’ai pu noter deux différences assez importantes.
Premièrement, F* n’a ni variables mutables, ni boucles. Ça n’est pas exactement dérangeant étant donné que ce sont des fonctionnalités qui peuvent facilement rendre les choses plus difficiles à prouver et que l’on peut facilement s’en passer à coup de récursion. Il est cependant possible d’imiter ces fonctionnalités (et plus) en utilisant des monades, ce qui ressemble plus à du Haskell qu’à du OCaml.
Deuxièmement, F* à un système de type qui laisse beaucoup plus de libertés qu’en OCaml:
- On peut appliquer des restrictions arbitraires aux types. Par exemple, les entiers strictement positifs s’écrivent
i:int{i > 0}, à lire "leside typeintqui satisfonti > 0". Ça peut être utilisé pour des trucs nettement plus fantaisistes, comme pour définir un type qui contient les nombres premiers avec quelque chose du genrep:int{isPrime p}. - Le type d’un argument ou de la valeur de retour d’une fonction peut dépendre des arguments précédents. Donc
a:int -> b:int{b > a} -> c:int, c’est simplement une fonction dont le premier argument est un entier, le deuxième argument est un entier strictement supérieur au premier argument et dont la valeur de retour est un entier1. - On peut avoir un type en tant qu’argument ou valeur de retour d’une fonction. Donc écrire une fonction qui prend en argument un entier
net qui retourne le type correspondant aux vecteurs de booléens de taillen, c’est pas un soucis.
C’est en utilisant cette liberté dans la définition des types que l’on va pouvoir introduire toutes les propriétés que l’on veut prouver. Par exemple, le type de la fonction valeur absolue peut s’écrire: a:int -> b:int{b >= 0 && (b = a || b = -a)}. C’est à dire que l’on prend en entrée un entier a et qu’en sortie on a un entier positif b qui est égal à l’entrée ou à l’opposé de l’entrée. Dans cet exemple, le type de sortie contraint entièrement la fonction et pour chaque entrée, une seule valeur de sortie est possible. Dans des cas un peu plus complexes, ça peu devenir trop long ou compliqué de contraindre autant le type de sortie, donc on se contentera du stricte minimum pour pouvoir prouver les propriétés qui nous intéressent vraiment.
- c’est pas exactement vrai parce que les fonctions sont curryfiées. Mais bon, ça n’a pas une grande importance ici.↩
Un objectif non-trivial pour tester F*
Afin de me donner une bonne impression sur les capacités de F* et de ses limitations, je me suis donné pour objectif d’écrire deux implémentations différentes d’une fonction qui résout un problème simple (mais pas trop) et d’ensuite prouver que ces deux fonctions sont équivalentes.
Le problème
Il est très fortement inspiré du problème numéro 1 du projet Euler: étant donné 3 entiers positifs , et , calculez la somme des entiers positifs multiple de ou strictement inférieurs à .
Solution 1
L’idée de la première implémentation est très simple: prendre tous les entiers positifs strictement inférieurs à , les filtrer pour ne conserver que les entiers multiples de ou et en faire leur somme.
Solution 2
Le résultat peut se calculer via une formule qui se trouve sans trop de difficultés en manipulant notre somme. Prenons , et .
Les entiers qui sont multiples de ou et strictement inférieurs à sont: , , , , , , et .
On peut réécrire la somme comme ceci:
On se retrouve avec 3 cas de "somme des entiers positifs de 1 à ", dont la formule est:
On serait donc tenté de généraliser la somme en:
Avec
Cependant, les nombres en commun dans les deux premières somme et qui doivent être retiré avec la troisième somme ne correspondent aux multiples de que si et sont premiers entre eux. S’ils ne le sont pas, les nombres en commun dans les deux premières sommes sont les multiples du plus petit commun multiple de et , qui est s’ils sont premiers entre eux. Donc la bonne formule est:
Avec
Implémentation de la solution 1
Sans plus attendre, on va se pencher sur l’implémentation de la première solution.
Afin de faire un peu plus qu’appeler 3 fonctions standard (ce qui ne serait pas très intéressant), j’ai décider de ré-implémenter un type pour la liste d’entiers, ainsi que les quelques fonctions associés qu’il faudra.
Représenter une liste d’entiers
Toujours pour pimenter un peu les choses et tester les possibilités de F*, j’ai défini un type vec qui utilise le type de ses éléments (normal), mais aussi le nombre d’éléments qu’il contient. Donc vec int 3 correspond à une liste de 3 entiers.
Comme pour toute bonne liste dans un langage fonctionnel, on a une liste vide Nil et un constructeur Cons qui prends un élément (la tête, hd) et le reste de la liste (la queue, tl):
type vec a : nat -> Type =
| Nil : vec a 0
| Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n+1)
Dans F*, : permet d’indiquer le type d’un truc. Donc Cons : blabla dit que Cons à le type blabla. C’est utilisé aussi au sein du type de Cons, dans hd:a qui dit que hd est de type a (qui est le type des éléments de la liste). Ici, les noms hd et tl pourraient être omis, mais je les ai laissé pour indiquer à quoi correspondent chaque élément.
Le type nat correspond aux entiers naturels (donc i:int{i >= 0}), ce qui nous permet de garantir qu’on n’aura pas de liste avec un nombre négatif d’éléments. On voit au passage l’avantage d’avoir un SMT solver: sans rien dire de plus, le compilateur va être capable de vérifier qu’avec n un entier naturel, n+1 est aussi un entier naturel.
L’argument #n:nat est un argument implicite (indiqué par le #), que F* devra déduire. Par exemple, dans Cons 2 Nil, Nil est de type vec int 0, donc F* déduit que le n vaut 0.
Voici quelques exemples de listes pour bien comprendre comment ça fonctionne:
// Une liste d'entiers vide.
let empty : vec int 0 = Nil
// Une liste qui contient un seul entier (42).
// J'ai réutilisé `empty` déclaré plus haut, mais j'aurais pu utiliser Nil.
let one_element : vec int 1 = Cons 42 empty
// Une liste de 3 booléens.
let many_bools : vec bool 3 = Cons true (Cons false (Cons true Nil))
Sommer des entiers
On continue sur du simple en définissant la fonction qui va nous servir à sommer une liste d’entiers:
let rec sum (#n:nat) (v:vec nat n) : nat
= match v with
| Nil -> 0
| Cons hd tl -> hd + sum tl
Encore une fois, on retrouve un argument implicite pour n. Et encore une fois, j’apprécie de ne pas avoir à écrire moi-même une preuve du fait que la fonction se termine, que 0 est un entier naturel et que le résultat de notre somme d’entiers naturels est effectivement un entier naturel.
Ça peut paraître con dit comme ça, mais je rappelle avoir été traumatisé par Lean, où je n’ai pas été capable de prouver que 1 > 0 après plusieurs heures à essayer. J’espère que ça remet en perspective à quel point, même un truc qui paraît simple, peut être difficile à prouver quand on ne sait pas comment faire.
Générer une liste d’entiers successifs
Même si on a uniquement besoin d’une liste d’entiers de 1 à N, j’ai généralisé la fonction pour qu’elle donne une liste d’entiers entre a et b (inclus) avec a <= b.
let rec generate (a:nat) (b:nat{b >= a})
: Tot (vec nat (b-a+1)) (decreases (b-a))
= if a = b then
Cons a Nil
else
Cons a (generate (a+1) b)
Ici, on a 2 cas de types dépendants: le type de b, qui dépend de a et le type de retour qui dépend de a et b pour indiquer la taille de la liste de retour.
Le type de retour n’est pas simplement vec nat (b-a+1), parce que F* n’est pas capable de prouver tout seul que la fonction se termine. En revanche, il suffit de lui donner une valeur entière positive, dépendante des arguments de la fonction et strictement décroissante lors des appels récursifs et il sera capable de faire le reste de la démonstration pour prouver que la fonction se termine1.
Tot (vec nat (b-a+1)) (decreases (b-a)) indique que la fonction est totale (c’est à dire qui n’a pas d’effets de bords et qui se termine), retourne un vec nat (b-a+1) et que b-a décroît strictement lors des appels récursifs.
Filtrer une liste
On est maintenant sur la partie de l’implémentation qui m’a posé le plus de problèmes. On veut une fonction qui prend en argument une fonction de filtre de type a->bool, une liste de type vec a n et qui retourne une liste de type vec a m. Du moins, c’est ce que j’ai initialement essayé, mais le compilateur a dit non.
Le problème devient apparent en se penchant sur l’implémentation, qui contient cette condition:
if f hd then
// Si l'élément passe le filtre, on doit l'ajouter au reste de la liste filtré
Cons hd (filter f tl)
else
// Sinon, la liste de retour est le reste de la liste filtré
filter f tl
Donc si filter f tl est de type vec a m, alors Cons hd (filter f tl) est de type vec a (m+1) et les deux branches de notre condition ont des types différents, ce que le compilateur n’apprécie pas du tout.
Catastrophe! Tonnerre de Brest! Nom d’une pipe! Sacrebleu! Mais comment résoudre ce problème? Est-ce que je me suis tiré une balle dans le pied en utilisant un type de liste dont la taille fait partie du type?
Et bien non, la taille de la liste de retour est exactement le nombre d’éléments qui sont acceptés par le filtre. Littéralement. Écrivons-donc cette fonction:
let rec num_filtered #a (#n:nat) (f:a -> bool) (v:vec a n) : (r:nat{r <= n})
= match v with
| Nil -> 0
| Cons hd tl -> (if f hd then 1 else 0) + num_filtered f tl
J’y ai ajouté une petite touche sur le type de retour pour indiquer que le nombre d’éléments qui passent le filtre est inférieur ou égal au nombre d’éléments de la liste d’entrée. C’est pas super utile, mais vu que F* est capable de nous prouver ça tout seul (enfin, avec l’aide de Z3), ça coûte pas grand chose.
Muni de cette fonction, on peut donc dire que le type de retour de notre fonction filtre est vec a (num_filtered f v), qui dépend donc des deux arguments de la fonction:
let rec filter #a (#n:nat) (f:a -> bool) (v:vec a n) : vec a (num_filtered f v)
= match v with
| Nil -> Nil
| Cons hd tl ->
if f hd then
Cons hd (filter f tl)
else
filter f tl
Le cerise sur le gâteau, c’est qu’il n’est pas nécessaire de donner plus d’info pour que F* soit capable de prouver que le type de retour est correcte et que la fonction se termine. Elle est pas belle la vie?
On met tout ensemble
Voilà, toutes les fonctions utilitaires nécessaires pour la première solution sont défini. Sans plus attendre, voici la solution:
let answer1 (a:pos) (b:pos) (c:nat) : nat
= let candidates = generate 0 c in
let ab_filter = filter (fun (x:nat) -> x%a = 0 || x%b = 0) in
sum (ab_filter candidates)
La dernière chose à noter, c’est que a et b sont défini comme pos, c’est à dire i:int{i > 0} parce que la division et le modulo entier ne sont défini que sur les entiers non-nuls.
Et voilà. Au final, il n’y a quasiment rien eu à faire pour que F* soit capable de vérifier une bonne quantité de propriétés, notamment de terminaison, mais aussi certaines propriétés arithmétiques. Jusque là, c’est très prometteur.
- C’est suffisant, mais pas nécessaire. F* accepte en fait n’importe quel mesure, qui est une valeur dépendant des arguments de la fonction, qui décroît strictement lors des appels récursifs et défini sur un ensemble qui n’admet pas de chaîne infiniment décroissante. Il n’est d’ailleurs pas nécessaire que l’ordre soit total sur l’ensemble.↩
Pour rendre le billet plus digeste et plus facile à écrire, j’ai décidé de le découper en 3 (j’espère) parties.
Je parlerais de l’implémentation de la deuxième solution dans un second billet, où je vais devoir mettre les mains dans le cambouis parce qu’on arrive très vite sur des propriétés arithmétiques non-triviales, comme prouver que l’algorithme d’Euclide pour calculer le PGCD est correcte.
La preuve final que les deux solutions donnent le même résultat fera probablement l’objet d’un troisième billet. À moins que le troisième billet explique pourquoi je n’y arrive pas. 
Petit teaser pour la suite, voici comment on peut prouver qu’avoir un élément x dans la liste generate a b est équivalent à a <= x && x <= b:
// Fonction indiquant si une valeur x est dans le vecteur v.
// eqtype contient tous les types sur lesquels l'égalité est défini,
// on peut donc appeler la fonction `=` sur les éléments de a.
let rec contains (#a:eqtype) (#n:nat) (x:a) (v:vec a n) : bool
= match v with
| Nil -> false
| Cons hd tl -> if hd = x then true else contains x tl
// La preuve est récursive.
let rec generate_contains (x:nat) (a:nat) (b:nat{b >= a})
// ensures indique la propriété que l'on veut prouver.
: Lemma (ensures contains x (generate a b) <==> a <= x && x <= b)
(decreases (b-a)) // Ça, c'est pour montrer la terminaison de la preuve
= if a = b then
() // Cas trivial, (generate a b) n'a qu'un seul élément
else if a = x then
() // Cas trivial, x est le premier élément de (generate a b)
else
// Cas récursif, x est dans (generate (a+1) b)
generate_contains x (a+1) b
Comme vous pouvez le voir, F* se débrouille très bien pour gérer les cas triviaux, mais aussi pour gérer tous les détails que je n’ai pas écris, mais qui sont nécessaire pour l’application du cas récursif.
