The Dependable Distributed Systems Team at Consensys R&D is using Dafny to verify the QBFT consensus algorithm. Dafny is a verification-oriented programming language that is also used to formally specify distributed protocols, their desired safety and liveness properties, and formally verify that the specification satisfies such properties like in the IronClad project.
One of the notable features of Dafny is that its toolchain supports transpilation to various executable languages, such as C#, Java, Go, Javascript, C++ and PHP. This opens up a series of potential valuable use cases requiring a Dafny program to interact with external code.
However, as you will see below, such interaction is not as straightforward as one may think! No need to worry though. We will both explain how to get over some of these hurdles and walk you through the process that we have followed in one of our recent projects.
But, let’s not get ahead of ourselves. Instead let’s start by looking at why knowing how to get transpiled Dafny code to interact with external code is actually very useful.
Use Cases
Integrate a Dafny program into a larger application.
Given that Dafny code can be formally proven to be correct, it would be interesting to use the functionality provided by such verified code in a larger application, like having a QBFT library compiled from verified Dafny code used by an Ethereum client independently developed. One could even try to gradually expand the portion of this larger application that has undergone verification, starting with the most critical sections and progressing as resources allow.
Connect a Dafny program with the rest of the world
The Dafny language doesn’t provide any I/O functionality except for console printing. This means that any Dafny program essentially runs in silos, isolated from the rest of the world, which is rarely useful. To connect a Dafny program to the rest of the world, one has to integrate the transpiled Dafny code with some external piece of code with I/O capabilities.
Reference Test Generation
It’s useful to mention here our particular subcase: using a verified Dafny program to generate reference tests that can then be used for compliance by other implementations. The idea here is to execute the Dafny program on a set of input vectors, collect the respective outputs and generate the reference tests by writing to a file which outputs should be returned by the functionality under test for each of the provided input vectors.
How to actually get a Dafny program to interact with external code
Now that we have explained why it is useful to learn how to get a Dafny program to interact with external code, we can dive into how to do it! One of the main challenges with this is that there is, as of this writing, no clearly documented way for how to do this.
We have explored three ways to go about this when a Dafny program needs to interact with external code. Let’s now look at each of these techniques in detail.
Dafny standalone application with external functions or methods
This is the only partially documented way to extend a Dafny program with external code. The idea here is that the main application is written in Dafny code with some of its functions and/or methods being left to be implemented by external code.
Here is how to do this.
Make the Dafny code compilable to a standalone application by designating one of its methods as the application entry point. Here is a link to the Dafny reference manual explaining how to do this.
Use the attribute {:extern} to mark those functions and/or methods that will be provided with an external implementation.
Provide the files containing the external implementations to the Dafny CLI.
This is great for small functions, because Dafny’s toolchain stays in charge and keeps things easy. However, this approach only fits use cases where the bulk of the application is written in Dafny. Additionally, at the time of writing this post, there is no documentation on the specific foreign function interface exposed by each supported language, which also means no documentation on the mapping between Dafny types and target language types.
Dafny binary as a library loaded by another language
When no application entry-point is specified, a Dafny program is ready to be compiled into a dynamically loaded library. Such a library can then be loaded and used by an external application.
While this method may look like the gold standard regarding reliability of a Dafny product since we don’t do anything undocumented to it, things are actually not as straightforward as they appear. For example, let’s look at the case where we want to generate a .NET DLL. This is a very reasonable use case as this would allow us to leverage on the multitude of functionalities provided by the .NET ecosystem.
However, to actually use the Dafny generated .DLL, we would have to basically reverse engineer the binary to find out how to access it through .NET reflection methods. The “reverse-engineering” part is needed because we don’t touch the intermediate C# source; we don’t even know what classes, objects, methods, types are created at the C# level.
Source-level integration of the Dafny transpiled code
Going further into undocumented territory, one can work directly at the source code level.
Basically, rather than loading the generated dynamically linked library like in the previous approach, one obtains the transpiled code via the Dafny CLI (see the /spillTargetCode option for this) and then includes it directly into the main application code base. This allows inspecting how the transpiled code works internally, and organising the main application code — the code external to the transplied Dafny code — accordingly.
The main advantage of this approach is that one is free to use any tool provided by the target language of choice. However, this approach only works if the main application is written in one of the languages supported by the Dafny toolchain. Additionally, by dealing directly with transpiled code, as opposed to executable binaries like in the previous approach, one has to put in extra attention to ensure not to do anything that would compromise the reliability of the transpiled code.
Our use case
Let’s now look at how we have proceeded in one of our recent projects. Our specific use case was generating JSON reference tests for the QBFT consensus protocol. Here is how we have gone about it:
Written a verified implementation of the QBFT specification in Dafny. The first step in the process has been writing in Dafny a verified implementation of the formally verified QBFT specification. This verification work is still ongoing.
Decided how much of the extra functionality required for generating reference tests we wanted to code in Dafny. Even if Dafny doesn’t provide I/O, one possibility would have been to extend the functionality of the Dafny code until the point where it would parse a JSON string that would have been ferried in from storage by a couple of lines of external code, and serialize its output to another JSON string, again stored by another few lines of external code. This would have allowed us to maximize the proportion of verifiable code. The disadvantage would have been the extra effort involved in actually verifying this Dafny JSON parsing code. We decided that getting quick access to mature JSON libraries like those existing for many of the various executable languages supported by Dafny was a better use of our resources.
Decided which of the three approaches described above to use. We decided to use the “Source-level integration of the Dafny transpiled code” approach, since it allowed us the easiest starting point, greatest freedom to deal with external libraries, and highest visibility into the whole process. Also, having to manage our own toolchain allowed us to discover and report a couple of bugs in the Dafny toolchain.
Decided which language to use as an intermediate language. We decided to use C# as it was the first language targeted by the Dafny compiler, and is the language in which Dafny itself is developed, so it’s presumably the most mature option. Java would have probably been a more natural choice for us, given that we develop a number of products in that language. However, Dafny did not support transpilation to Java when we started this work so this wasn’t really an option available to us.
Wrapping Up
One of the very powerful features of Dafny is that it can be transpiled into executable code. This means that you can actually execute your formally verified Dafny program. However, the most interesting use cases where this comes useful, due to the lack of I/O functionality in the Dafny language, actually require some level of interaction between the Dafny program and external code.
However, this does not come without a challenge. In this blog post we have explored both the challenges involved with this process and the techniques that are available to actually do it, and have finally walked you through how we have proceeded in one of our recent projects.
Now it’s up to you to make the best use of it! Happy hacking!