An approach to translating Haskell programs to Agda and reasoning about them

We are using the Agda programming language and proof assistant to formally verify correctness of a Byzantine Fault Tolerant consensus implementation based on HotStuff / DiemBFT. The Agda implementation is a translation of our Haskell implementation, which is based on DiemBFT. This short paper focuses on one aspect of this work. We have developed a library that enables the translated Agda implementation to closely mirror the Haskell code on which it is based, making review and maintenance easier and more efficient, and reducing the risk of translation errors. We also explain how we assign semantics to the syntactic features provided by our library, thus enabling formal reasoning about programs that use them; details of how we reason about the resulting Agda implementation will be presented in a future paper. The library we present is independent of our particular verification project, and is available in open source for others to use and extend.