Toward Certification for Free! ; Toward Certification for Free!: Correct-By-Construction ML Oracles with Polymorphic LCF Style

This preprint has been largely rewritten and integrated into Sylvain Boulmé's Habilitation in 2021, See http://www-verimag.imag.fr/~boulme/hdr.html. ; How can we reduce the required effort to develop certified programs in proof assistants such as Coq? A major trend is to introduce untrusted oracles able to justify their answers by producing a certificate, i.e. a witness of their computations. A trustworthy result is then built from this certificate by a certified checker. This alleviates the burden of proof, but producing certificates is a requirement which increases complexity of oracle development. We propose a design pattern, called Polymorphic LCF Style, that removes the need for certificates: ML oracles directly compute the certified result by invoking trusted operators and datastructures extracted from Coq. But, oracles only handle these datastructures as polymorphic values, which forbids oracles to forge incorrect results. This design thus delegates a part of the certification to the ML typechecker. Correctness comes from a weak parametricity property of imperative ML polymorphic types that we call parametric invariance. We demonstrate the relevance of Polymorphic LCF Style for the certification of a realistic library: an abstract domain of convex polyhedra.