How does the Dafny Programming Language compile-time check its constraints?

[lancejpollard]

I asked this question on Reddit. Here I will refine it down after receiving some comments.

My main goal is I would like to know how you actually implement the verification aspect of Dafny. I don't understand how you can do the compile-time type checking and constraint checking (with assert/ensures/invariant/requires/etc.).

I saw these slides on "weak precondition calculus", but it seems far removed from actual algorithms and implementation details, so having read through them (granted, not fully understanding every piece yet), I am still lost when it comes to trying to imagine how verification of an imperative program, like Dafny does, can happen at compile time.

Looking through the source a bit, it seems to be related to "boogie" somehow, but the code is large to say the least, so it would take a long time to parse through that :). Wondering if you could give a primer on the algorithms and implementation techniques used to implement the verification of a program. If you have any existing papers/resources that do this to some degree, those would be great as well.

I am reasonably familiar with the need for formal verification (I studied TLA+ for a while several years back), as well as the fact that your program can only be verified against a specification, so it depends on the specification correctness. However, I don't see how to apply this stuff to a programming language implementation. I am familiar with loop invariants and Hoare logic as well.

Very excited to see a project like Dafny out there in the wild!

Other stuff i am checking out currently:

• The Boogie Verification Debugger
• Using Dafny, an Automatic Program Verifier
• The Dafny Integrated Development Environment
• Formal Verification in Dafny: Use of Boogie Intermediate Verification Language for Determining the Correctness of a Program
• A Tutorial on Using Dafny to Construct Verified Software

[MikaelMayer]

Let me get started on this one, let's forget about mutable references, let's only consider a program like this, which is an unoptimized version of "maximum"

method Maximum(a: int, b: int) returns (m: int)
  ensures m >= a && m >= b;
  ensures m == a || m == b
{
  m := a;
  while (m < a || m < b)
    invariant m <= a || m <= b
  {
    m := m + 1;
  }
}

You can actually desugar this program for verification purpose into blocks that don't have loops, and into special commands that don't have a compilation equivalent like assume (but that's fine, it's no code to execute, only for Hoare logic)

method Maximum(a: int, b: int) return (m: int)
{
// Block 1, including the invariants of the loop
  // No assumptions about variables, unless we had them in "requires clauses"
  m := a;
  assert m <= a || m <= b; // Assert 1

// Block 2: the inside of the loop
  // Here we don't know anything about variables
  assume m <= a || m <= b; // We assume the invariant
  assume m < a || m < b;      // We assume the guard
  m := m + 1;
  assert m <= a || m <= b;   // Assert 2: We assert the invariant at the end of the loop 

// Bloc 3: The outside of the loop when exiting normally. "Break" statement could transform some of these assumes by guarding them with some condition, i.e. that the loop was exited normally.
  // We forget everything about variables
  assume m <= a || m <= b; // Assume the invariant
  assume !(m < a || m < b)  // Assume the negation of the guard
  assert m >= a;  // Assert 3
  assert m >= b;  // Assert 4
  assert m == a || m == b;  // Assert 5
}

Now the goal is to derive from this an equivalent mathematical formula (usually encoded in SMT format) that, if it is satisfiable, will make one of these assert to fail (the model would serve as a counter-example). Moreover, the model would provide which assert is failing.
This is where the computation of weakest preconditions helps (wp, also documented here). For block 1:

wp(
    m := a;
    assert m <= a || m <= b; 
, true)
= wp(
    m := a;
, m <= a || m <= b)
= wp(
, a <= a || m <= b)
=
    a <= a || m <= b

We give !(a <= a || m <= b) to an SMT solver which returns unsat, meaning there is no initial assignment of a, b, m that will falsify this. Thus, the assert is always verified.
Similarly for the second bloc,

wp(
    assume m <= a || m <= b;
    assume m < a || m < b;
    m := m + 1;
    assert m <= a || m <= b";
, true)
= wp(
    assume m <= a || m <= b;
    assume m < a || m < b;
    m := m + 1;
, m <= a || m <= b)
= wp(
    assume m <= a || m <= b;
    assume m < a || m < b",
, m + 1 <= a || m + 1 <= b)
= wp(
    assume m <= a || m <= b;
, (m < a || m < b) ==> (m + 1 <= a || m + 1 <= b))
=
    (m <= a || m <= b) ==> (m < a || m < b) ==> (m + 1 <= a || m + 1 <= b))

We now give !((m <= a || m <= b) ==> (m < a || m < b) ==> (m + 1 <= a || m + 1 <= b))) which returns unsat, because there is no model that would falsify the weakest precondition, so all the asserts are valid.

For the third block, we have three asserts, so if something is failing, we ought to know which assert it comes from. We can actually further encode the assertion number into another variable so that with a single counter-example, we know exactly which assert is failing: Moreover, we can also transform a Dafny "assert X" into a mathematical "assert_ X; assume_ X;" so that it guarantees that assertions. actually produce assumptions for remaining assertions.

wp(
    assume m <= a || m <= b;
    assume !(m < a || m < b);
    assert m >= a;  // Assert 3
    assert m >= b;  // Assert 4
    assert m == a || m == b;  // Assert 5
, true)
=
wp(
    assume m <= a || m <= b;
    assume !(m < a || m < b);
    assert m >= a;  // Assert 3
    assert m >= b;  // Assert 4
, assertionNumber == 5  ==> (m == a || m == b))
=
wp(
    assume m <= a || m <= b;
    assume !(m < a || m < b);
    assert m >= a;  // Assert 3
    assert_ m >= b;  // Assert 4 as a raw assert
    assume_ m >= b;  // Assert 4 transformed into assume
, m >= b  ==> assertionNumber == 5  ==> (m == a || m == b))
=
wp(
    assume m <= a || m <= b;
    assume !(m < a || m < b);
    assert_ m >= a;  // Assert 3
, (assertionNumber == 4 ==> m >= b) && (m >= b ==> assertionNumber == 5  ==> (m == a || m == b))
=
wp(
    assume m <= a || m <= b;
    assume !(m < a || m < b);
,  (assertionNumber == 3 ==>  m >= a) && (m >= a ==> ((assertionNumber == 4 ==>  m >= b) && (m >= b ==> assertionNumber == 5  ==> (m == a || m == b))))
=
    (m <= a || m <= b) ==>
    !(m < a || m < b) ==>
    (assertionNumber == 3 ==>  m >= a) && (m >= a ==> ((assertionNumber == 4 ==>  m >= b) && (m >= b ==> assertionNumber == 5  ==> (m == a || m == b))))

Now we give to an SMT solver the negation of the formula above, which is

(m <= a || m <= b) && !(m < a || m < b) && (
(assertionNumber == 3 && !(m >= a)) || (m >= a && ((assertionNumber == 4 && !(m >= b)) || (m >= b && assertionNumber == 5  && !(m == a || m == b)))`)
)

It will try to find an assignment of m, a, b, assertionNumber that makes the formula above true. If you messed up any of the assert, e.g. the last one would come from assert m == a which would result in a disjunct (m >= b && assertionNumber == 5 && m != a), it makes it easy to prove with e.g. m == 5, a == 4, b == 5 and assertionNumber == 5;
To find whether other assertions are failing, you simply add the conjunct assertionNumber != 5, which invalidates the counter-example above, and if there is another failing model, then the assertionNumber will be different

Boogie is essentially the intermediate representation language that Dafny compiles to that has all these statements for verification, as well support for many other things we don't want to reimplement from scratch.

Note that in my example above, I omit to prove one of the most important features without which verification is incomplete, and this is termination.
Proving termination in Dafny consists in providing decreases X clause and proving that X is decreasing in some set in which all decreases sequences are eventually constant. For number, it's the set of positive integers.

For example, for decreases b - m, we would add the assertion assert b - m >= 0 at the end of block 1, after assuming that the guard holds, and we would add the assertion assert b - m <= b - m, where m' is a copy of the m a the beginning of the loop.

[lancejpollard]

This looks really helpful so far, but I will have to let it sink in. Thank you!

For this first block:

wp(
"m := a;
 assert m <= a || m <= b; 
", true)
  = wp("m := a;", m <= a || m <= b)
  = wp("", a <= a || m <= b)
  = a <= a || m <= b

What is happening here exactly, at each point. I am not following what is going on. Also, is there anywhere I can find an implementation of wp?

[lancejpollard]

Also, I'd be curious to know what happens with the forall statement. It doesn't literally try every possible combination, so wondering how it works. Maybe there is some general theory I am missing as well, though I have tried to read about forall in other languages like Coq before, and was never able to grok it.

predicate sorted(a: array<int>)
   requires a != null
   reads a
{
   forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}
method BinarySearch(a: array<int>, value: int) returns (index: int)
   requires a != null && 0 <= a.Length && sorted(a)
   ensures 0 <= index ==> index < a.Length && a[index] == value
   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != value
{
   var low, high := 0, a.Length;
   while low < high
      invariant 0 <= low <= high <= a.Length
      invariant forall i ::
         0 <= i < a.Length && !(low <= i < high) ==> a[i] != value
   {
      var mid := (low + high) / 2;
      if a[mid] < value
      {
         low := mid + 1;
      }
      else if value < a[mid]
      {
         high := mid;
      }
      else
      {
         return mid;
      }
   }
   return -1;
}

[MikaelMayer]

Also, is there anywhere I can find an implementation of wp?

I added this link in my answer, but Wikipedia is good as well. You can view assume P; Q as a special case of (selection statement](https://en.wikipedia.org/wiki/Predicate_transformer_semantics#Selection) like if P => Q, !P => Skip, whereas assert P, Q as a special case of selection statement such as if P => Q, !P => Abort

Also, I'd be curious to know what happens with the forall statement.

You're probably talking about the quantifier expression. Since recently, Dafny has triggers still largely undocumented, because most of the work happens automatically. It enables to instantiate automatically the forall quantifiers on certain patterns, thus providing axioms for the rest to prove.
There are other axioms that enable to prove forall expressions, such as proving the expression for a value next to a range and having it proved it for that range, etc, or simply using forall statements