Compiling Dependent Type Preconditions to Runtime Checks With Agda2Hs

Abstract

Formally verified programs can be embedded in larger non-verified code bases by means of syntactically faithful source-to-source translation: systems like Agda2Hs make it possible to translate verified code written in a dependently typed programming language to a general-purpose functional programming language, Agda and Haskell in this case. Such systems can enable verification for critical functionality while keeping wider ecosystem access and easier to write code for peripheral functionality. However, this interfacing leaves a gap in the formal guarantees of the verified code: preconditions that were only expressible as a dependent type and have thus got erased upon translation might not be met. We present runtime checking these preconditions as a way to close this gap and ensure that computation does not continue on ill-formed input. As an extension to Agda2Hs, we have implemented a solution to automatically insert runtime checks for the preconditions and only make those definitions accessible in the output that are also checkable. The runtime check insertions do not only cover functions, but also data types and non-class records in the form of smart constructors; higher-order erased arguments are supported as well. We make a formal completeness analysis of a simplified version of the checks we generate for well- and ill-typed programs.
In our solution, class instances are not supported for runtime checking due to their different nature, and capabilities for recovering from a failed runtime check are still rudimentary. Despite these limitations, we conclude that a closure of the input precondition verification gap is possible, and that the development time trade-off in comparison to handwriting checks can be worthwhile.