Verified Code Generation from Isabelle/HOL
In this thesis, I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees.
This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation.
The work consists of three major contributions.
First, I have implemented a certifying routine to eliminate type classes and instances in Isabelle specifications. Based on defining equations of constants, it derives new definitions that do not use type classes. This can be used to bypass an unverified step in the current code generator.
Second, I formalized an algebra for higher-order λ-terms that generalizes the notions of free variables, matching, and substitution. Terms can be thought of as consisting of a generic (free variables, constants, application) and a specific part (abstraction, bound variables). With this algebra, it becomes possible to reason abstractly over a variety of different types.
These two parts are independent from each other and can also be used for other purposes. For example, I have successfully instantiated the term algebra for other term types in the Isabelle universe.
Third, a compiler that works similarly to the existing code generator, but produces a CakeML abstract syntax tree together with a correctness theorem. More precisely, I have combined a simple proof producing translation of recursion equations in Isabelle into a deeply embedded term language with a fully verified compilation chain to the target language CakeML.
An Algebra for Higher-Order Terms
In this formalization, I introduce a higher-order term algebra, generalizing the notions of free variables, matching, and substitution. The need arose from the work on a verified compiler from Isabelle to CakeML. Terms can be thought of as consisting of a generic (free variables, constants, application) and a specific part. As example applications, this entry provides instantiations for de-Bruijn terms, terms with named variables, and Blanchette’s λ-free higher-order terms. Furthermore, I implement translation functions between de-Bruijn terms and named terms and prove their correctness.
Certifying Dictionary Construction in Isabelle/HOL
Type classes are a well-known extensions to various type systems. Classes usually participate in type inference; that is, the type checker will automatically deduce class constraints and select appropriate instances. Compilers for such languages face the challenge that concrete instances are generally not directly mentioned in the source text. In the runtime, type class operations need to be packaged into dictionaries that are passed around as pointers. This article presents the most common approach for compilation of type classes – the dictionary construction – carried out in a trustworthy fashion in Isabelle/HOL, a proof assistant.
CakeML is a functional programming language with a proven-correct compiler and runtime system. This entry contains an unofficial version of the CakeML semantics that has been exported from the Lem specifications to Isabelle. Additionally, there are some hand-written theory files that adapt the exported code to Isabelle and port proofs from the HOL4 formalization, e.g. termination and equivalence proofs.
A Verified Compiler from Isabelle/HOL to CakeML
European Symposium on Programming (ESOP, Open Access), 2018
The final publication is available at Springer Link.
Many theorem provers can generate functional programs from definitions or proofs. However, this code generation needs to be trusted. Except for the HOL4 system, which has a proof producing code generator for a subset of ML. We go one step further and provide a verified compiler from Isabelle/HOL to CakeML. More precisely we combine a simple proof producing translation of recursion equations in Isabelle/HOL into a deeply embedded term language with a fully verified compilation chain to the target language CakeML.
Archive of Formal Proofs, 2017
Isabelle's code generator natively supports type classes. For targets that do not have language support for classes and instances, it performs the well-known dictionary translation, as described by Haftmann and Nipkow. This translation happens outside the logic, i.e., there is no guarantee that it is correct, besides the pen-and-paper proof. This work implements a certified dictionary translation that produces new class-free constants and derives equality theorems.
Archive of Formal Proofs, 2017
Isabelle's code generator performs various adaptations for target languages. Among others, constructor applications have to be fully saturated. That means that for constructor calls occuring as arguments to higher-order functions, synthetic lambdas have to be inserted. This entry provides tooling to avoid this construction altogether by introducing constructor functions.
Lazifying case constants
Archive of Formal Proofs, 2017
Isabelle's code generator performs various adaptations for target languages. Among others, case statements are printed as match expressions. Internally, this is a sophisticated procedure, because in HOL, case statements are represented as nested calls to the case combinators as generated by the datatype package. Furthermore, the procedure relies on laziness of match expressions in the target language, i.e., that branches guarded by patterns that fail to match are not evaluated. Similarly, if-then-else is printed to the corresponding construct in the target language. This entry provides tooling to replace these special cases in the code generator by ignoring these target language features, instead printing case expressions and if-then-else as functions.
Development of a verified code generator from Isabelle/HOL to CakeML, a verified subset of Standard ML. The vision of this project is to provide an alternative (or extension) to the current code generation facility that reduces the trusted code base.
- What is the trusted code base of the pipeline?
- We rely on faithful export from Lem to Isabelle, an unverified printer of CakeML AST to CakeML source text, and the kernel of Isabelle. There is ongoing work to use OpenTheory to get a more faithful representation of the CakeML formalization in Isabelle.
- Does the pipeline target existing CakeML library constructs, like the built-in lists?
- No, it does not, and it is not intended at the moment.
- Does the pipeline target existing CakeML native constructs, like machine integers?
- No, it does not, but it is intended for the future, and actively being worked on.
- Does that mean that arithmetic on natural numbers in Isabelle is mapped to unary in CakeML?
- That is accurate:
nats are treated as a proper datatype with
- How are (8-bit) characters treated?
- The most naive possible translation, 256-way enumerations, would lead to very large code sizes. Instead, we translate characters to bytes, i.e. 8-tuples of
bools. As of Isabelle2018, this will become the default of code generation in Isabelle, including other (unverified) targets.
- Is the generated code guaranteed to terminate?
- The current Isabelle code generator only guarantees partial correctness (which has been proved on paper).
While our work is designed for total correctness (all functions that are exported are internally proved to be terminating), we have only proved partial correctness so far.
The CakeML compiler team has proved total correctness.
Update, August 2018: Some (not all) compiler phases have been proved to be totally correct.
- Why isn’t there a full compilation pipeline in the AFP?
- We’re working on it. Some parts of it are already available as stand-alone entries, and we want to make sure it’s published in modular parts. In the meantime, use the packaged version that accompanies the main paper (see below).
- Formalization for “A Verified Compiler from Isabelle/HOL to CakeML”
Archived as: DOI 10.5281/zenodo.1167616
The ESOP’18 paper has an error in Definition 7 (page 20), third rule (
Vrecabs), second line.
After the bounded quantifiers (before the ≈ operator), instead of σ₁, it should read rs.
This is an error in the transcription from the formalization (supplementary material) to the paper.
The error is not present in the supplementary material.
The second precondition of the
Vrecabs case should compare the constants with the rule set rs.
σ₁ is the variable environment from the previous semantics and does not carry constant definitions.