We are developing a verified compiler. The frontend abstracts over the low-level values and operations (e.g., unary and binary operations). The backend instantiates these from CompCert’s Clight language.
In the frontend, we would like to guarantee that the concrete definitions cannot be exploited. In the backend, however, we need to reason about them.
So far we considered three different solutions.
-
Using a signature to abstract over the low-level values. The frontend is implemented as a functor parameterized by this signature. We instantiate the functor before reasoning about the backend. In theory, this solution is perfect. In practice, we have tens of files each of which must be a functor with a list of arguments that grows and grows as later functors import earlier ones. Also, tools for analyzing dependencies and generating documentation work less well on these files.
-
Using type classes. The frontend uses the class abstractly and the backend uses an instance. This solution requires adding a section with context to each file. The extracted definitions require additional arguments and use
Obj.magic. -
Just using the concrete module but with opaque definitions. This seems to be a pragmatic compromise, but only a certain discipline ensures that the initial stages do not rely on the concrete definitions.
Has anyone else had a similar problem? Are there any other Coq features we could consider? (Multi-file functors?)