The use of arrays in a recursive function in Dafny leads to verification failure

Question

The following code, assert f(arr, 2) == 0;, fails to verify.

function f(bs:array<int>, hi:nat) : nat
{
  if hi==0 then 0 else f(bs, hi-1)
}

method Main() {
  var arr := new int[3][1, 1, 1];
  assert f(arr, 2) == 0;
}

Moreover, I found that:

• When I add a new hint assert f(arr, 0) == 0;, it can pass the verification.
• Or when I use a sequence (seq), it can also pass.

I really can't understand what the reason is.

Answer 1

Ordinarily, Dafny automatically unrolls a function once. That's enough to prove each of the first two assertions in your updated example. In most cases in verification, this is enough, because if you don't know the values of the parameters, the proofs are symbolic and usually done by induction in one form or another.

In the third assertion, function f needs to be unrolled 6 times in order to determine that the result value is 0. The verifier is not doing that automatically, so you have to help it along. For example, you could write the Main method as

method Main() {
  var arr := new int[5][1, 1, 1, 1, 1];
  assert f(arr, 0) == 0;
  assert forall i:: 0< i<=arr.Length ==> f(arr, i)==f(arr, i-1);
  calc {
    f(arr, arr.Length);
  ==  // by the definition of f
    f(arr, arr.Length - 1);
  ==
    f(arr, arr.Length - 2);
  ==
    f(arr, arr.Length - 3);
  ==
    f(arr, arr.Length - 4);
  ==
    f(arr, arr.Length - 5);
  ==
    0;
  }
  assert f(arr, arr.Length) == 0;
}

In general, this is what you'd need to do.

Advanced:

However, Dafny does actually help you out a little more. In some cases, it unrolls a function call twice, and in some cases, it can even continue unrolling the function until it stops. The latter happens when the parameters passed to the function are literals, or at least when the arguments that affect termination are literals. The arr.Length argument is known to equal the literal 5, but the argument arr is not a literal. So, for starters, Dafny would need to be told that termination of f depends only on the hi argument, not on bs. By default, Dafny gives you decreases bs, hi for f, but if you write decreases hi, then Dafny will know that termination depends only on hi. This may still not work automatically with the array argument, but it does work if you use a sequence instead of an array. (Sequences may be easier, because they are value types.) For example, the following program verifies automatically:

function f(bs: seq<int>, hi: nat): nat
  requires hi <= |bs|
  decreases hi
{
  if hi == 0 then 0 else f(bs, hi - 1)
}

method Main() {
  var arr := new int[5][1, 1, 1, 1, 1];
  assert f(arr[..], 0) == 0;
  assert forall i :: 0 < i <= arr.Length ==> f(arr[..], i) == f(arr[..], i - 1);
  assert f(arr[..], arr.Length) == 0;
}

(If you're interested in the details of how this works, see https://leino.science/papers/krml237.pdf.)

So, the verifier can be more automatic in some cases, but I would still suggest keeping "the verifier unrolls each function call just once" in mind as a rule of thumb.