Dafny Standard Libraries

I am an engineer and I love Dafny.

Why? Because Dafny is a programming language designed from the ground up to support expressing the behavior of code directly in the code itself. Dafny lets you precisely specify what it means to sort a sequence of values, not just as a giant comment on your sorting function you hope no-one misinterprets, but as a machine-readable expression in the same language. Even better, the Dafny tool can statically tell you whether your implementation is correct or not, without ever running a single test.

When I first learned about Dafny, this was mind-blowing. Having worked as an engineer for decades, I've seen my share of subtle and catastrophic bugs in production, and often thought it should be possible to catch more of them before they happen. I've always been passionate about inventing and building tools to help more engineers do their job better, and now, getting to help maintain and contribute to Dafny every day has been the definition of a dream job.

At the same time, it's getting to the end of 2023 and I'm really looking forward to a break this year. Having bought my son a Lego advent calendar and my wife a crossword advent calendar (always on the lookout for alternatives to candy), I thought I would try my hand at Advent of Code, a popular code puzzle advent calendar that's been around since 2015. But to make it extra fun, I thought I'd write my solutions in Dafny.

I was pleased to hear several colleagues had the same idea in years past, but also heard a common refrain that it seemed harder than it should be. To be fair, Dafny is never going to be the best choice if you're trying to solve the puzzles as fast as possible and climb the leaderboard: Dafny is built for carefully writing a verifiably-correct solution, not a probably-correct solution as fast as possible. But even though the Dafny language itself is easily expressive and full-featured enough, it didn't give you much help with basic tasks like parsing a number from its string representation.

We've been collecting lots of valuable reusable Dafny code in a separate dafny-lang/libraries repository for several years now. I frequently pointed folks to this repository whenever I saw questions like “how do I map a function over a sequence in Dafny?”, knowing that there was already a Seq.Map function just waiting there to be used. But it was obvious users didn't naturally discover this code, and not all projects could easily add it as a submodule in order to access it.

This is why I'm so excited about the recent release of Dafny 4.4: we spent months refactoring all these libraries and importing them into the Dafny distribution itself, so that they are now available to any and all Dafny users out of the box.

To show off what a difference this makes, let's look at what it's like to solve the very first Advent of Code puzzle.

Getting started

The requirements for the first puzzle boil down to:

The newly-improved calibration document consists of lines of text; each line originally contained a specific calibration value that the Elves now need to recover. On each line, the calibration value can be found by combining the first digit and the last digit (in that order) to form a single two-digit number.

…

Consider your entire calibration document. What is the sum of all of the calibration values?

No problem, we can handle this!

To ensure full backwards compatibility for existing Dafny projects, Dafny 4.4 doesn't make the standard libraries available by default: they are enabled by a --standard-libraries option to the dafny CLI. But we can do better than that: we can use a Dafny project file to indicate we want to use the standard libraries, which will let the Dafny IDE understand that dependency.

Start by installing Dafny 4.4, ideally opting to use the VS Code extension which will download its own copy automatically. Create a new directory with an empty solution.dfy file and a dfyconfig.toml file with these contents:

[options]
standard-libraries = true

Now for the actual code. Let's start from the bottom-up: we're clearly going to need a function to extract the calibration value as a number from a single line of text.

  function CalibrationValue(line: string): nat {
    // ...
  }

How do we find the first and last digits?

Sequences and Wrappers

Having a look at the top-level index of Dafny standard libraries, we notice there's a Std.Collections library with a submodule for Seq, and sure enough, there are functions like IndexOf and LastIndexOf. Perfect!

Or perhaps you were distracted by the Std.Strings module, where you might expect these utilities to live. But in Dafny, strings are really nothing more than sequences of characters: the type string is just an alias for seq<char>. This means many typical string operations are provided as general sequence operations instead. Don't worry, we'll get to that library in a moment.

Let's consider for a moment how you might want to use a function like IndexOf in general. Finding the index of an element in a sequence will certainly not always succeed, since the sequence might not contain the element. In most standard libraries, a function like IndexOf may return an invalid sentinel index value, like the length of the sequence or -1. But often you actually know the element is in the sequence because of the way the rest of the program is structured. Perhaps you just added the element to a list and then sorted it. Because of the invariants of sorting, you know the element is still in there. The great thing about Dafny is that it can actually understand this kind of reasoning, and know when it is safe to assume an operation will succeed.

Therefore a common pattern in the Dafny standard libraries is to have two different versions of a function or method: a partial version with preconditions, and a complete version that may not succeed. The Std.Wrappers library provides a few extremely common datatypes for this: Option<T>, for a value that may not exist, and Result<T, E>, for the result of an operation that may fail with an error value instead. The Seq library and most of the other libraries use these datatypes all over the place in order to define partial operations.

In our specific case, there is both an IndexOf function, which requires the element is present in the sequence and returns a nat that is always a valid index in the sequence, and IndexOfOption, which produces an Option<nat> instead of a nat. The latter is the better match for our situation, since we're eventually going to read our puzzle input from a file on disk, and we don't actually know that every line contains at least one digit.

Note that in general we could get by with only the partial version of all these operations, since we could always just explicitly check the precondition first before invoking the operation. The downside of that approach, though, is that there's a performance cost: you end up iterating through the sequence twice, once to check if the element is there and then again to actually fetch the element.

Finally, in our case we're not looking for a specific concrete element, we're looking for any digit. In other words, we want to find the first and last index of elements that satisfy a particular predicate. Fortunately Seq has us covered here too, and the two functions we actually want to use are IndexByOption and LastIndexByOption.

Strings and Numbers

Let's see how much of our CalibrationValue function we can write now. We can import the Std.Collections.Seq module into the default top-level module with an import statement. In most Dafny codebases you'll see import opened statements, especially for very common modules like Std.Wrappers: these statements make the contents of the imported module directly available in the importing module. That lets you say things like Some(42) and None rather than Wrappers.Some(42) and Wrappers.None. For this exercise I'm just using import statements so it's more obvious when we're using things from the standard libraries.

  import Std.Collections.Seq

  function CalibrationValue(line: string): nat {
    var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
    var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);

    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];

    // Still need to parse the result as a number...
  }

Progress! We'll figure out what to pass for the second arguments on the first two lines in a moment. First, how do we convert our resultAsString to a number, more specifically a nat? This is more specifically an operation on strings rather than generic sequences. That means now we can open our Std.Strings present, and see that it contains a shiny new ToNat function!

  import Std.Collections.Seq
  import Std.Strings

  function CalibrationValue(line: string): nat {
    var firstDigitIndex := Seq.IndexByOption(line, /* hmm... */);
    var lastDigitIndex := Seq.LastIndexByOption(line, /* hmm... */);

    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];

    Strings.ToNat(resultAsString)
  }

Even better, digging into the implementation of ToNat leads us to what we need to plug the holes we skipped over: the Strings.DecimalConversion.IsDigitChar predicate tells us if a character is a digit.

  import Std.Collections.Seq
  import Std.Strings
  import Std.Strings.DecimalConversion

  function CalibrationValue(line: string): nat {
    var firstDigitIndex := Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
    var lastDigitIndex := Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);

    // Error: incorrect type for selection into string (got Option<nat>)
    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];

    Strings.ToNat(resultAsString)
  }

Before we pat ourselves on the back too hard, though, we notice this program doesn't typecheck yet: firstDigitIndex and lastDigitIndex are not plain nat values but Option<nat> values. And if we think about that a bit more, it means our CalibrationValue function also needs to produce an Option<nat> instead of a nat, because if line doesn't contain any digits we can't succeed in producing a calibration value either.

Thankfully another nice thing about Std.Wrappers is that the types in that module are failure-compatible types. That means they can be used with the :- “elephant operator”, which is a convenient way to propogate failure. Let's change our return type, change the two regular := assignment operators to elephants instead, and wrap up our result as an Option<nat> so it matches our new return type:

  import Std.Collections.Seq
  import Std.Strings
  import Std.Strings.DecimalConversion
  import Std.Wrappers

  function CalibrationValue(line: string): Wrappers.Option<nat> {
    var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar);
    var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar);

    var resultAsString := [line[firstDigitIndex], line[lastDigitIndex]];

    Wrappers.Some(Strings.ToNat(resultAsString))
  }

Now if either attempt to find a digit fails, the execution of the function body will immediately stop, and that failure will become the result of the whole function. At this point we have a valid Dafny program, and the IDE should reward our hard work with a festive green gutter to indicate that it verifies successfully too!

But let's pause for a second, because something very cool happened we may not have even noticed: there's a precondition on ToNat(str): forall c <- str :: DecimalConversion.IsDigitChar(c). In other words, str has to be a string with only digits. That's why the return type of ToNat is just nat and not something like a Wrappers.Option<nat> or a Wrappers.Result<nat, string>, because it always succeeds in parsing the string.

How does Dafny know that resultAsString is always parsable as a non-negative integer? Because of the post-conditions of Seq.IndexByOption and Seq.LastIndexByOption, Dafny actually knows that they return the indexes of elements that satisfy the “by” predicate, and therefore deduces that [line[firstDigitIndex], line[lastDigitIndex]] is a string that only contains digits. I don't know about you but I think that's super cool.

Bits and Bytes

So now that we've solved the most interesting bit of the puzzle, we just have to feed the actual puzzle input into our Dafny code. Let's assume we've downloaded the puzzle to input.txt in the current directory. How the heck do we read this with Dafny?

Good news! There's a standard library for that too: Std.FileIO. This one is very basic for now, explicitly meant for simple cases of reading and writing file data for these kinds of use cases, rather than modelling entire file systems. Here's our first attempt at a reusable utility for reading Advent of Code puzzle input (because after all we have another month's worth of puzzles to solve!)

  // Just the imports we need for this snippet.
  import Std.FileIO
  import Std.Wrappers

  method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
    // Error: incorrect return type for method out-parameter 'res'
    input := FileIO.ReadBytesFromFile("input.txt");
  }

Note that FileIO.ReadBytesFromFile is a method rather than a function, and so ReadPuzzleInput has to be as well. A function has to behave like a pure mathematical function in order for Dafny to reason about the behavior of programs: it has to produce the same output every time it is given the same input. This is clearly not true for an operation to read the contents of a file, so ReadBytesFromFile has to be a method, which is allowed to behave non-deterministically.

Again we have a typechecking error: we want to get the puzzle input as a string, but ReadBytesFromFile produces bytes, more specifically a seq<bv8>. bv8 is short for “bit vector of length 8”, equivalent to a byte. We need to convert the bytes to characters somehow.

Realistically, we'd assume that the puzzle input is in ASCII and just convert every byte directly to its corresponding character. But let's pretend we're writing Real Code for the moment so I can show off the Std.Unicode library; hey you never know, later puzzles might have proper UTF8 content!

  import Std.BoundedInts
  import Std.FileIO
  import Std.Unicode.UnicodeStringsWithUnicodeChar
  import Std.Wrappers

  method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
    var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
    
    var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
    input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
  }

A few notes:

• The UnicodeStringsWithUnicodeChar module is named that way to emphasize that it is only correct to use with the unicode-char = true option, which is on by default in Dafny 4.x.
• The FromUTF8Checked function takes in a seq<uint8>, where uint8 is a newtype definition from Std.BoundedInts. This library defines lots of common fixed-bit-width integer types that the Dafny compiler will map to the native integer types of the target language for improved efficiency and memory usage.
• Because bv8 is a distinct type from uint8, we have to explicitly convert between them. This is a side effect of the Dafny standard libraries having multiple independent contributions from various projects, and you can expect future versions of Dafny to provide more versions of common utilities to make combining things a bit smoother.
• FromUTF8Checked returns an Option<string>, but FileIO.File returns a Result<seq<bv8>, string>. To unify with a common result type, we use Option.ToResult to convert the former value to a Result, which is a handy and common trick. See the documentation for Std.Wrappers for more details.

Sprinting to the finish

Now let's put it all together and write our main method:

  method Main() {
    var input :- expect ReadPuzzleInput();

    var lines := Seq.Split(s, '\n');

    var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);

    var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
    print total, "\n";
  }

We've used one more trick with failure-compatible types in this method: :- expect, a variation on the elephant operator to make “assign or halt” statements. ReadPuzzleInput returns a Result, but if it fails there's nothing more we can do in the main method than printing an error and exiting. :- expect means that if the right-hand side of the statement is a failure, Dafny execution will immediately halt and, if you're using the dafny run command, print the failure value to the console. This is particularly valuable for writing tests in Dafny, but be careful about using it in production code: unlike mechanisms such as exceptions from other programming languages, halting is not recoverable!

Note also that the Seq library continues to work hard for us, splitting the input into lines, mapping our CalibrationValue function over the sequence of lines, and summing the results into the final answer. MapWithResult is a short-circuiting variation of Map where the mapped function can fail.

Let's put the sample input from the puzzle description into input.txt so we can try it out (not the actual puzzle input - I draw the line at publishing the answer in this blog post, you're just going to have to run the solution yourself to get that!)

1abc2
pqr3stu8vwx
a1b2c3d4e5f
treb7uchet

Now we can run our project and get…

% dafny run dfyconfig.toml

Dafny program verifier finished with 3 verified, 0 errors
142

Huzzah! We have a working solution to the first puzzle in less than 40 lines of Dafny code (see below for the complete program), all thanks to the Dafny standard libraries.

  import Std.BoundedInts
  import Std.Collections.Seq
  import Std.FileIO
  import Std.Strings
  import Std.Strings.DecimalConversion
  import Std.Unicode.UnicodeStringsWithUnicodeChar
  import Std.Wrappers

  method Main() {
    var input :- expect ReadPuzzleInput();

    var lines := Seq.Split(input, '\n');

    var calibrationValues :- expect Seq.MapWithResult(CalibrationValue, lines);

    var total := Seq.FoldLeft((x, y) => x + y, 0, calibrationValues);
    print total, "\n";
  }

  method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
    var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
    var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);
    
    input := UnicodeStringsWithUnicodeChar.FromUTF8Checked(bytes).ToResult("Invalid UTF8");
  }

  function CalibrationValue(line: string): Wrappers.Result<nat, string> {
    var firstDigitIndex :- Seq.IndexByOption(line, DecimalConversion.IsDigitChar).ToResult("No digits");
    var lastDigitIndex :- Seq.LastIndexByOption(line, DecimalConversion.IsDigitChar).ToResult("No digits");

    var resultStr := [line[firstDigitIndex], line[lastDigitIndex]];

    Wrappers.Success(Strings.ToNat(resultStr))
  }

Looking back and looking ahead

The standard libraries are made possible by the recent support for Dafny build artifacts: compressed files containing the contents of an entire Dafny library along with metadata about how it was verified. These files use the extension .doo for Dafny Output Object¹. They play much the same role as .jar files do for Java packages. Internally, the standard libraries are packaged up as multiple .doo files and embedded as resources in the Dafny tool. When --standard-libraries is switched on, the appropriate set of .doo files are added as additional program source.

This means the standard library source isn't re-verified every time your verify your Dafny project, but the tool checks to make sure the options they were previously verified with are compatible with the objects in your project. In particular, this means if you try to use them with the older unicode-char = false option, you'll get an explicit error right away, rather than potentially misusing code not meant for this mode.

As excited as I am about having standard libraries in Dafny, I've also been nervous about having them for a long time: I'd be sad in the future if anyone gave Dafny a pass because its footprint had grown too bloated for their environment. Part of the reason the code is labelled as “standard libraries”, plural, is to hint at the fact that they may be split up into different packages in the future. Now that we have standard libraries in Dafny, we're also setting our sights on helping Dafny users create their own shared libraries and distributing them as pre-verified .doo files in the future, so such libraries also get this layer of protection against misuse.

Another great improvement over the old dafny-lang/libraries repository is that the Dafny standard libraries are well-tested for all of the programming languages that Dafny currently compiles to: C#, Go, Python, Java and JavaScript. That means even libraries that depend on target language details such as Std.FileIO and Std.Concurrent are safe to use in multi-target Dafny projects.

Until next year

I'll leave this post at that, as I've got some catching up to do in the Advent of Code challenge before time runs out! In the meantime, install Dafny 4.4, take the standard libraries for a test drive, and feel free to cut an issue if you run into speed bumps. Even better, if you have your own spiffy reusable Dafny code you keep in your back pocket, create a pull request and get it into the standard libraries!

---

^1.This is true, but the real reason for the name is a nod to the other Daphne from Scooby Doo. ↩