Baking for Dafny: A CakeML Backend for Dafny

TL;DR

Dafny's verification-oriented language design currently relies on a two-step compilation pipeline whose backend and target-toolchains form a large part of the trusted computing base (TCB). The paper introduces a verified CakeML backend implemented within HOL4 to reduce the TCB, by formalizing a functional big-step semantics for the Dafny IR and proving a simulation theorem that the CakeML translation preserves semantics. The implementation details describe exporting the Dafny IR as S-expressions, parsing and translating to a CakeML AST, and handling multi-paradigm translation via mutual recursion and runtime conventions. The work lays out concrete Hello World and Factorial examples to illustrate the approach and outlines future plans to extend language features, manage type data, and potentially upstream the backend into the Dafny project, with continued attention to performance and semantic correctness.

Abstract

Dafny is a verification-aware programming language that allows developers to formally specify their programs and prove them correct. Currently, a Dafny program is compiled in two steps: First, a backend translates the input program to a high-level target language like C# or Rust. Second, the translated program is compiled using the target language's toolchain. Recently, an intermediate representation (IR) has been added to Dafny that serves as input to new backends. At the time of writing, none of these steps are verified, resulting in both the backend and the target language's toolchain being part of Dafny's trusted computing base (TCB). To reduce Dafny's TCB, we started developing a new backend that translates Dafny to CakeML, a verified, bootstrapped subset of Standard ML, in the interactive theorem prover HOL4. We also started to define functional big-step semantics for the Dafny IR to prove correctness of the backend.

Figures (7)

• Figure 1: Transformation steps from a Dafny program to the CakeML AST.
• Figure 2: "Hello World" in Dafny.
• Figure 3: Compilation of "Hello World" to CakeML. We do not include the definition of the Dafny module for brevity.
• Figure 4: Loop-based factorial function in Dafny.
• Figure 5: Compilation of the loop in Figure \ref{['code:dfy:factorial']} to CakeML. We do not include the declaration and initialization of variables for brevity.