Chroniques de Rox* #1

Étude de cas: un formulaire verifié

Ce billet fait partie d’une série écrite dans le cadre de mon travail de doctorat, et qui vulgarise la future chaîne de compilation Rox* (Rust-Oxide-F*) dont l’objectif est d’amener à Rust de la vérification déductive. Le contexte complet de ce projet est expliqué dans l’article initial. Le code de cette étude de cas est disponible ici.

Le module TextInput de Servo

Notre premier exemple concerne la manière dont Servo gère le mouvement du curseur à l’intérieur de l’élément HTML multi-ligne <textinput>. Toute la logique de cette fonctionnalité est contenue à l’intérieur d’un seul fichier. Afin d’éviter d’avoir à gérer les structures spécifiques à Servo comme DOMString qui ne font potentiellement pas partie du sous-ensemble traduisible vers F*, j’ai écrit une nouvelle version du fichier qui contient uniquement le cœur logique de la fonctionnalité. La structure de données principale qui décrit l’état d’une sélection de texte à l’intérieur du <textinput> est la suivante :

pub struct TextInput {
    /// Current text input content, split across lines without trailing '\n'
    lines: Text,
    /// Current cursor input point
    edit_point: TextPoint,
    /// The current selection goes from the selection_origin until the edit_point. Note that the
    /// selection_origin may be after the edit_point, in the case of a backward selection.
    selection_origin: Option<TextPoint>,
    selection_direction: SelectionDirection,
}

Deux choses à noter ici : premièrement, toutes les lignes du texte n’ont pas la même longueur. Aussi, naviguer à l’intérieur du texte n’est pas aussi simple que dans un rectangle parfait. Deuxièmement, nous devons nous souvenir de l’origine et de la direction de la zone de sélection, qui peut être mise à jour lorsque le curseur bouge. Étant donnés tous ces éléments, il n’est pas trivial de recenser toutes les situations possibles lorsque l’on presse la touche directionnelle haute. C’est précisément là où la vérification peut nous aider à ne rien oublier.

Afin d’aider à déboguer le code, le développeur de Servo a écrit une fonction très intéressante :

// Check that the selection is valid.
fn assert_ok_selection(&self) {
    if let Some(begin) = self.selection_origin {
        debug_assert!(begin.line < self.lines.len());
        debug_assert!(begin.index <= self.lines[begin.line].len());
        match self.selection_direction {
            SelectionDirection::None | SelectionDirection::Forward => {
                debug_assert!(begin <= self.edit_point)
            },

            SelectionDirection::Backward => debug_assert!(self.edit_point <= begin),
        }
    }
    debug_assert!(self.edit_point.line < self.lines.len());
    debug_assert!(self.edit_point.index <= self.lines[self.edit_point.line].len());
}

Cette fonction assert_ok_selection est appelée à la fin de chaque fonction qui met à jour TextInput, mais elle ne contient que des debug_assert et est éliminée en production. Ce motif est exactement équivalent à une postcondition, et c’est ainsi que je l’ai traduite dans mon code F*.

Une fois tout traduit en F*, j’ai prouvé que chaque fonction qui mettait à jour TextInput préservait l’invariant assert_ok_selection : si c’est vrai à l’appel de la fonction (dans la précondition), alors ça devrait être vrai après la fonction (dans la postcondition). Grâce au prouveur automatique Z3, la preuve a été presque complètement automatique, et je n’ai eu à guider le prouveur qu’en ajoutant une assertion dans une fonction. Cependant, je n’ai pas pu prouver tout de suite que l’invariant tenait pour la fonction adjust_vertical; en effet, celle-ci contenait un bug! De plus, ce bug causait des problèmes visibles dans la dernière version de Servo, comme décrit dans le ticket que j’ai ouvert immédiatement.

En utilisant les messages d’erreur de F*, j’ai pu trouver une manière de corriger le code afin de prouver la postcondition de la fonction. J’ai ensuite traduit l’équivalent de ce patch dans le code Rust originel et ai ouvert une demande de fusion de branches qui incluait le patch et quelques cas de test supplémentaires qui déclenchaient le bug.

Notons que ce travail ne garantit pas que le code est complètement « correct ». En effet, j’ai juste prouvé qu’un invariant était préservé et ce quelque soit les entrées utilisateur. Grâce à cette méthode, j’ai pu trouver une situation non couverte par les cas de test existants et qui déclenchait des crashs dans la dernière version de Servo. Avec un outil de traduction automatique de Rust vers F* ainsi qu’à l’aide de la recherche de preuves automatique, je pense que la vérification est en fait plus efficace en termes de temps de développement que de devoir imaginer tous les cas de tests qui déclencheraient toutes les situations. De plus, utiliser la vérification a l’avantage de vous faire savoir quand vous avez terminé : lorsque c’est prouvé, c’est prouvé. Écrire un test de plus ne peut jamais garantir que l’on en a écrit assez.