Search code examples
integer-divisionformal-verificationdafny

In Dafny, how can I fix the "value does not satisfy the subset constraints of 'nat'" error on division?

This Dafny code:

method Div(n: nat, d: nat) returns (q: nat)
  requires d > 1
{
  q := n / (d - 1);
}

produces this error:

Dafny 2.1.1.10209
stdin.dfy(4,9): Error: value does not satisfy the subset constraints of 'nat'

Dafny program verifier finished with 0 verified, 1 error

Line 4, column 9 is the / symbol, indicating division.

Asserting that d - 1 != 0 does not help.

What does this error mean? How can I convince Dafny this is OK?

Solution

  • I think the problem is that the type of (d - 1) is int.

    This fixes it:

    let d1: nat = d - 1;
q := n / d1;

    My intent with this code was that all operations should be nat arithmetic. Dafny had other ideas. Here is what I think is going on (speculation ahead):

    • Dafny has an initial type inference pass that happens before the prover runs. This algorithm has no way to make use of assertions and preconditions; it only type-checks them. It does not "know" that d - 1 is guaranteed to be positive or even that d > 1.

    • So to Dafny's type-checker, when d is a nat, d - 1 has to be an int. The result of subtracting a nat from a nat can be negative.

    • Given that, it's not obvious that this program is well-typed. But that's OK! Dafny's type inference can just defer judgment on this point. It allows n / (d - 1) to be used as a nat here, and it makes a note to have the prover check that the value of n / (d - 1) really is guaranteed to fall in the nat subset of its type int.

    • Surprisingly, the prover can't handle this. I checked by changing the return type so that type-checking passes without a hitch:

      method Div(n: nat, d: nat) returns (q: int)
  requires d > 1
  ensures q >= 0
{
  q := n / (d - 1);
}

      Sure enough, Dafny 2.1.1.10209 fails to prove the postcondition.