The `internal_add`

function tries to efficiently insert a new range of integers into an existing list of sorted and disjoint integer ranges. For example, if we started with `[101..=102, 400..=402, 404..=405]`

and added `402..=404`

, we expect a result of `[101..=102, 400..=405]`

.

Ideally, I’d formally verify this algorithm with Rust-specific tools [1,2]. Those tools, however, seem hard to use. Instead, I chose Dafny. Dafny is a language and verification system. It is taught to undergraduates at universities around the world. It is used in industry. I find it to be addictively interactive and programmer friendly.

Aside: Dafny creator, Dr. Rustan Leino has a connection to Rust beyond the coincidence of his first name. He helped create Spec#, the first language to use a type system to avoid null pointers. Rust, of course, adopted this idea to great success.

This article covers rules 1 to 6. Part 2 will cover rules 7 to 9.

Before trying to prove the mathematical correctness of your algorithm, decide if the effort is worth the benefit.

Dafny is not Rust. Using Dafny requires porting algorithms of interest from Rust to Dafny. This port can miss details and introduce errors. Given this risk, should *you *use Dafny to verify Rust algorithms? I boldly claim that “it depends”.

- How important is your algorithm’s correctness? If you are printing a report and it looks right, it probably is right. The
`internal_add`

algorithm relates to a data structure that I’d like others to use with confidence, giving me extra motivation to verify it. - Maybe all formal verification, with current tools, is too hard. I believe, however, that Dafny makes formal verification as easy as currently possible. You will find formally verifying code easier if you are already familiar with types (for example, from Rust) and recursion/induction (used infrequently in Rust). You can read this article and decide for yourself if/when formal verification is easy enough to be valuable to you.
- Maybe fuzzing (such as
`cargo-fuzz`

) and property-based testing (such as`QuickCheck`

) are good enough. Although these methods do not provide mathematical certainty, they are clever, useful, and easy to use. (The`range-set-blaze`

crate already uses`QuickCheck. See`

Rule 9.5 in a previous article for details). - Maybe formal verification is and will always be doomed because writing a specification is as hard as writing code. I disagree. Think about refactoring. I often start coding by writing something simple. I then refactor this simple code for efficiency. For
`internal_add`

, I found the specification to be simpler than any code. (You can judge this for yourself in Rule 4.)

Aside: Verification then becomes a computer-checked refactoring from a simple specification to a final, efficient algorithm.

- Maybe formal verification is and will always be doomed because the halting problem tells us formally that formality isn’t generally possible. The halting problem does not doom us. While we can’t always understand
*arbitrary*code, we don’t need to. We only need to understand our own code, which we (hopefully) wrote to be understandable. Starting in Rule 2, we’ll see how Dafny easily verifies that*specific*loops and recursions halt. - Maybe porting to Dafny is too hard. This has not been my experience. Like Rust, Dafny mixes and matches imperative and functional programming. I found porting my algorithm to be straightforward.

Assuming you still want to verify your algorithm with Dafny, your next step is to learn Dafny.

Dafny is both a programming language and an interactive verification system. I recommend you install it as a VS Code extension.

To learn it, start at https://dafny.org/. Of special interest is the Online Tutorial and the Reference Manual. I also found the Verification Corner videos on YouTube helpful. (Of possible interest is the college textbook, *Program Proofs, *$49 for the Kindle Edition). I found the programming language part of Dafny easier to learn than Rust, perhaps similar in difficulty to C#.

Dafny, like Rust, is fully typed. Dafny, like Python, is garbage collected. Here is a “Hello World”:

`// hello.dfy`

method Main()

{

var s := "Hello World";

print s, "\n";

}

Dafny, also like Python, offers integers of arbitrary size. Here is a program that *provably *adds two natural numbers by repeatedly incrementing.

Some points of interest:

- Dafny coding guidelines follow C#, not Rust. So, we name the function
`SlowAdd`

not`slow_add`

(although either will run). - Dafny supports subtypes. For example, any
`int`

that can be shown to be non-negative is also a`nat`

. - Assignment is
`:=`

and equality is`==`

. (There is no`=`

.) - Function parameters, for example,
`x`

and`y`

above, are immutable. - Dafny uses
`ensures`

and`invariant`

statements to verify the code at compile-type. It then removes these statements to finish compiling. - The green check mark shows that this code verifies. Dafny’s VS Code extension will, by default, continuously try to validate each method. This adds an almost gambling-like excitement to working with Dafny. In the example above, if I make
`y`

an`int`

rather than a`nat`

, then validation should and will fail. (Can you figure out why?) Dafny will mark my function with a red X and tell me “`This postcondition might not hold: r == x + y`

”. - Dafny knows some of the mathematics of integers, arrays, sets, maps, sequences, etc. This often allows it to finish the last details of validation by itself.

Now that you know about Dafny, you should let it know about your algorithm.

The `range-set-blaze`

crate represents sets of integers as sorted, disjoint ranges. For example, this list of three ranges:

`100..=2_393,`

20_303..=30_239_000,

501_000_013..=501_000_016

represents a set of 30,220,996 integers.

In Rust, the `RangeSetBlaze`

struct represents this data structure internally with a standard `BTreeMap.`

Recall that a `BTreeMap`

represents a list of key/value pairs, sorted by key. Here, our keys are the ranges’ starts (for example, `100`

, `20_303`

, `501_000_013`

) and the values are the ranges’ inclusive ends (for example, `2_393`

, `30_239_000, 501_000_016`

. `RangeSetBlaze`

stores the list with a `BTreeMap`

rather than a `vec`

to make key look up more cache friendly.

`RangeSetBlaze`

depends on `BTreeMap`

, so must we implement `BTreeMap`

in Dafny? Happily, no. We can, instead, use Dafny’s `vec`

-like `seq`

data type. This substitution works because `BTreeMap`

, `vec`

, and `seq`

can all represent sorted lists — just with different efficiencies. For the purpose of formal verification, we only care about correctness and can ignore efficiency.

`RangeSetBlaze`

requires the list of ranges be sorted and disjoint. How do we say “sorted and disjoint” in Dafny? We can say it via this *ghost predicate* (and related code):

`ghost predicate ValidSeq(sequence: seq<NeIntRange>) {`

(forall i:nat, j:nat | i < j < |sequence| :: sequence[i].0 < sequence[j].0)

&& (forall i:nat, j:nat | i < j < |sequence| :: !Touch(sequence[i], sequence[j]))

}type IntRange = (int, int)

type NeIntRange = x: IntRange | !IsEmpty(x) witness (0,0)

function IsEmpty(r: IntRange): bool

{

r.0 > r.1

}

A *predicate* is another name for a method that returns `bool`

. A *ghost* method (or predicate) is one that can only be used for validation, not for running the final code.

At a high level, the `ValidSeq`

predicate takes as input a sequence of non-empty integer ranges. It then tests that the start values are sorted and that the ranges don’t touch. Specifically,

- An
`IntRange`

is a tuple of two`int`

values. - An
`IntRange`

`IsEmpty`

exactly when its start is greater than its end. (This follows Rust’s convention.) - A
`NeIntRange`

(non-empty integer range) is an`IntRange`

that is not empty, for example,`(0,0)`

. [All our ranges are end inclusive.] - This expression tests that the start values are sorted:

`forall i:nat, j:nat | i < j < |sequence| :: sequence[i].0 < sequence[j].0`

It can be read as “for all natural numbers *i* and *j* — such that *i* is less than *j *and *j* is less than the length of the sequence — test that the start value at index *i* is less than the start value as index *j*”.

Aside: Note that a Rust

`BTreeMap`

doesn’t support (random-access) indexing but here we are using such indexing. This is OK because`is a ghost predicate and so will only be used for validation.`

ValidSeq

- This expression tests that the ranges are disjoint:

`forall i:nat, j:nat | i < j < |sequence| :: !Touch(sequence[i], sequence[j])`

It can be read as “for all natural numbers *i* and *j* — such that *i* is less than *j *and *j* is less than the length of the sequence — test that the range at index *i* does not touch the range at index *j*. But what is `Touch`

?

We’ll define `Touch`

on two-levels. On a mathematical level, a range *i* is said to touch a range *j* if there exists an integer *i0* in range *i* and an integer *j0* in range *j* such that *i0* and *j0* are within a distance of one of each other. On an efficient programming level, we want to avoid definitions depending on “there exists”. Here is a Dafny predicate that is both mathematical and efficient:

`predicate Touch(i: NeIntRange, j: NeIntRange)`

ensures Touch(i, j) == exists i0, j0 ::

Contains(i, i0) && Contains(j, j0) && -1 <= i0 - j0 <= 1

{

assert Contains(i, i.0) && Contains(i, i.1) && Contains(j, j.0) && Contains(j, j.1);

if i.1 < j.0 then

assert (-1 <= i.1 - j.0 <= 1) == (i.1+1 == j.0);

i.1+1 == j.0

else if j.1 < i.0 then

assert (-1 <= j.1 - i.0 <= 1) == (j.1+1 == i.0);

j.1+1 == i.0

else

var k0 := Max(i.0, j.0);

assert Contains(i, k0) && Contains(j, k0);

true

}function Contains(r: IntRange, i: int): bool

{

r.0 <= i && i <= r.1

}

function Max(a: int, b: int): int

{

if a < b then b else a

}

Some points of interest:

`Touch`

is not a ghost. In other words, we can use it in both regular code and validation code.- The
`assert`

statements help Dafny prove that the regular code meets the mathematical`ensures`

statement. - For efficiency, the Dafny prover validates the inside of a
`method`

separately from its outside. Only the`ensures`

(and the yet-to-be-seen,`requires`

) statements cross this border. In contrast to a`method`

, a Dafny`function`

is transparent to the validator. (I think of it as inlining code with respect to validation.)

With concepts such as `ValidSeq`

and `Touch`

defined, we next move onto specifying what our algorithm is supposed to do.

Ultimately, I want to prove that my specific Rust algorithm for inserting a new range into a `RangeSetBlaze`

is correct. Before we do that, however, let’s define what “correct” range insertion is.

`method InternalAdd(xs: seq<NeIntRange>, a: IntRange) returns (rs: seq<NeIntRange>)`

requires ValidSeq(xs)

ensures ValidSeq(rs)

ensures SeqToSet(rs) == SeqToSet(xs) + RangeToSet(a)

{

if IsEmpty(a)

{

rs := xs;

}

else

{

assume false; // cheat for now

}

}

This says that `InternalAdd`

is a method that takes `xs`

, a sequence of non-empty integer ranges, and `a`

, an integer range (that could be empty). The method outputs `rs`

, a new sequence of non-empty integer ranges.

We need to say that `xs`

and `rs`

must be sorted and disjoint. That is easily done with the `ValidSeq`

’s in the `requires`

and first `ensures`

.

We also need to say that `rs`

contains the right stuff. Is this hard? It is not. We just say that the set of integers in `rs`

must equal the set of integers in `xs`

unioned with the integers in `a`

.

Aside: In Dafny, “+” when applied to sets is “union”.

The set of integers in a range is:

`ghost function RangeToSet(pair: IntRange): set<int>`

{

set i {:autotriggers false} | pair.0 <= i <= pair.1 :: i

}

And the set of integers in a sequence of non-empty ranges can be define inductively (that is, recursively):

`ghost function SeqToSet(sequence: seq<NeIntRange>): set<int>`

decreases |sequence|

requires ValidSeq(sequence)

{

if |sequence| == 0 then {}

else if |sequence| == 1 then RangeToSet(sequence[0])

else RangeToSet(sequence[0]) + SeqToSet(sequence[1..])

}

Some points of interest:

- The line:
`assume false; // cheat for now`

makes validation work even if it really shouldn’t. We use it as a temporary placeholder. - We make
`RangeToSet`

and`SeqToSet`

*ghosts*to stop us from using them in regular code. We make them*functions*(instead of*methods*) - Because Dafny knows a lot about creating and manipulating sets and sequences, we often profit by using sets and sequences in our specification.
- Even if our regular code uses loops instead of recursion, our validation code will often use recursive-like induction.
- The
`{:autotriggers false}`

relates to avoiding a warning message. For more information see this Stack Overflow answer by Prof. James Wilcox.

We now have a formal specification of `InternalAdd`

. I find this specification short and intuitive. But what if you need help figuring out a specification or other Dafny code?

The main forum for Dafny questions is Stack Overflow. To my surprise, I actually received much useful help there.

I recommend starting your question’s title with “Dafny:”. Also, be sure to tag your question with `dafny`

and, perhaps, `formal-verification`

.

Aside: On the site, you can see my 11 questions and Divyanshu Ranjan’s 48 Dafny-related answers.

As an open-source project on GitHub, Dafny also hosts GitHub Discussions and Issues.

The Dafny community is small but seems enthusiastic about helping users and improving the project.

With help at hand, we must next find an algorithm that meets the specification.

As a novice to formal verification, I decided to postpone work on the real `internal_add`

used in my Rust code. Instead, I started work on an `InternalAdd`

algorithm that I hoped would be easier to validate. I ended up with this:

`method InternalAdd(xs: seq<NeIntRange>, a: IntRange) returns (rs: seq<NeIntRange>)`

requires ValidSeq(xs)

ensures ValidSeq(rs)

ensures SeqToSet(rs) == SeqToSet(xs) + RangeToSet(a)

{

if IsEmpty(a)

{

rs := xs;

}

else

{

var notTouching, merged := PartitionAndMerge(xs, a);

var indexAfter := NoTouchIndexAfter(notTouching, merged);

rs := InsertAt(notTouching, [merged], indexAfter);

}

}

The idea is that if range `a`

is empty, we return the input sequence unchanged. Otherwise, we divide the work into three steps, which we can validate independently. The first step, `PartitionAndMerge,`

returns:

`notTouching`

, a sequence of ranges that don’t touch range`a`

, and`merged`

, a single range created from`a`

and everything it touches.

Here is an example input and output:

`InternalAdd`

next finds where to insert `merged`

and, finally, inserts it.

Here is the code for `PartitionAndMerge:`

`method PartitionAndMerge(xs: seq<NeIntRange>, a: NeIntRange) returns (notTouching: seq<NeIntRange>, merged: NeIntRange)`

requires ValidSeq(xs)ensures ValidSeq(notTouching)

ensures RangeToSet(merged) >= RangeToSet(a)

ensures forall range | range in notTouching :: !Touch(range, merged)

ensures SeqToSet(xs) + RangeToSet(a) == SeqToSet(notTouching) + RangeToSet(merged)

{

// Split into touching and not touching seqs

var touching: seq<NeIntRange>;

touching, notTouching := Partition(a, xs);

// Merge the touching seq into one range with our original range

merged := UnionSeq(a, touching);

}

This says that `PartitionAndMerge`

`requires`

that `xs`

be a valid sequence of non-empty integer ranges and that `a`

be a non-empty integer range. It ensures that `nonTouching`

is another valid sequence of non-empty integer ranges. It ensures that the integers in range `merged`

are a superset of those in range `a`

. It ensures that no range in `notTouching`

touches range `merged`

. And finally, it ensures that the integers in `xs`

and `a`

are exactly the same as the integers in `notTouching`

and `merged`

.

`PartitionAndMerge`

also divides the work, this time into two steps (`Partition `

and `UnionSeq`

) that can be validated independently. Those steps continue to subdivide their work. Where does it end? Let’s look at one example.

The method `UnionSeq`

calls `UnionRange`

which merges two ranges:

`function UnionRange(x: IntRange, y: IntRange): IntRange`

requires IsEmpty(x) || IsEmpty(y) || Touch(x, y)

ensures RangeToSet(x) + RangeToSet(y) == RangeToSet(UnionRange(x,y))

{

if IsEmpty(x) then y

else if IsEmpty(y) then x

else (Min(x.0, y.0), Max(x.1, y.1))

}

The `UnionRange`

code handles the empty cases and then returns the minimum bounding range. (The minimum bounding range is the range from the smaller of the two starts to the larger of the two ends.) But how can this be correct? In general, a minimum bounding range of two ranges might include extra integers. We might get something bigger than the union of the inputs, like so:

The code is correct because it `requires`

that the two input ranges touch or are empty. This `ensures`

that the union of the integers in range `x`

with the integers in range `y`

are exactly the integers in the output range.

At compile time, Dafny proves this function correct. Beyond that, it proves that everything that calls this function provides inputs that are empty or touching.

I think of this as a generalization of Rust’s borrow checker. At compile-time Rust checks that we are safe from many memory errors. At compile time, verification systems, such as Dafny, can prove almost arbitrary properties. Of course, as we are seeing, this ability comes at the cost of complexity.

The full code for this verified algorithm is about 200 lines, organized into about a dozen methods and functions.

This rule shows that we can verify *an* algorithm for `InternalAdd`

, but it is not the algorithm I used in Rust. We will turn to that next.

## Be the first to comment