Verified VCG and Verified Compiler for Dafny

TL;DR

This paper develops a formally verified compiler and verification condition generator for a subset of Dafny, ensuring foundational correctness guarantees and enabling reliable compilation from Dafny to executable machine code.

Contribution

It introduces a verified semantics, VCG, and compiler for a significant subset of Dafny, mechanized in HOL4, with correctness guarantees for the entire compilation process.

Findings

Verified VCG enables correctness proofs for Dafny programs.

Verified compiler preserves correctness from Dafny to CakeML.

Mechanized proofs in HOL4 ensure foundational soundness.

Abstract

Dafny is a verification-aware programming language that comes with a compiler and static program verifier. However, neither the compiler nor the verifier is proved correct; in fact, soundness bugs have been found in both tools. This paper shows that the aforementioned Dafny tools can be developed with foundational correctness guarantees. We present a functional big-step semantics for an imperative subset of Dafny and, based on this semantics, a verified verification condition generator (VCG) and a verified compiler for Dafny. The subset of Dafny we have formalized includes mutually recursive method calls, while loops, and arrays -- these language features are significant enough to cover challenging examples such as McCarthy's 91 function and array-based programs that are used when teaching Dafny. The verified VCG allows one to prove functional correctness of annotated Dafny programs, while the verified compiler can be used to compile verified Dafny programs to CakeML programs. From there, one can obtain executable machine code via the (already verified) CakeML compiler, all while provably maintaining the functional correctness guarantees that were proved for the source-level Dafny programs. Our work has been mechanized in the HOL4 theorem prover.