Room 206 (2nd floor, badged access)
29 November 2018 - 14h00
Importation d'oracles ML impératifs dans du code Coq vérifié
by Sylvain Boulmé from Verimag
Résumé : L'utilisation d'oracles dans du code Coq est une des clés du succès de CompCert (le premier compilateur C formellement vérifié). Un tel oracle correspond à du code non vérifié développé en OCaml, et qui produit des résultats qui sont vérifiés par du code prouvé en Coq. Cependant, dans CompCert, les oracles sont actuellement déclarés à travers une FFI (Foreign Function Interface) potentiellement incorrecte.
L'exposé présentera quelques écueils de cette FFI. Il présentera une FFI alternative, dont la correction est encore une conjecture. Cette FFI permet d'importer n'importe quelle fonction ML impérative en Coq, ce qui permet de facto d'avoir en Coq un langage impératif d'ordre supérieur complet (mais exécutable uniquement après extraction): références avec aliasing, égalité de pointeurs, récursion arbitraire, exceptions, entrées/sorties, etc.
Au niveau Coq, les raisonnements formels sur ces traits impératifs sont limités: on ne peut prouver que des invariants qu'on peut déduire du type polymorphe des oracles (theorems for free à la Wadler). Cette limitation des raisonnements formels donne en contrepartie une grande liberté pour implémenter les oracles en OCaml: ils doivent juste avoir un type ML compatible avec celui déclaré en Coq. Avec quelques exemples emblématiques (comme SatAnsCert, un vérificateur prouvé en Coq de SAT-solveurs booléens), l'exposé illustrera que le rapport expressivité/bureaucratie est très intéressant pour vérifier formellement des propriétés fonctionnelles en correction partielle.
Slides of the Presentation.
