Dafny unable to reason about unmodified arrays involving existential quantifier

[anithag]

I am trying to understand why Dafny isn't able to verify the following test method that takes an input array and returns nothing. The method test uses the loop invariant that for all indices k, there exists another index l such that a[k] == a[l]. Note that l is guaranteed to exist---at the minimum, l should be k since the method does not modify the input array.

method test1(a:array<int>)
  requires a.Length > 0
{
    var i:= 0;
  
    while i < a.Length
      invariant i >=0
      invariant i <= a.Length
      invariant unchanged(a)
      invariant forall k: int::0 <= k < i ==> exists l | 0 <= l < i:: a[k] == a[l]
    {
      assert forall k: int::0 <= k < i ==>  exists l | 0 <= l < i:: a[k] == a[l];
      i := i+1;
      assert forall k: int::0 <= k <i ==> exists l | 0 <= l < i:: a[k] == a[l];
    }
}

Dafny fails to verify both the assertions as well as the last invariant. I think the existential could be the problem. The following counter example shown at line i:=i+1 does not make any sense to me either.

a:_System.array<int> = (Length :=2) i:int := 2 k:int := 0

I think the verifier is struggling to construct a value for l? Any insight helps.

[racko]

In your example code we see that Dafny can neither prove the first assertion in the loop, even though it is literally the same as the invariant, nor can it prove the invariant from the second assertion though it's the same as well.

Dafny uses "triggers" to figure out that it should use some available invariants/assertions to prove others¹.
Often Dafny works reasonably well even when it cannot infer triggers, but especially with existential quantification, you usually need a trigger.

Knowing that, you can introduce two predicates p and q:

method test1(a: array<int>)
    requires a.Length > 0
{
    var i:= 0;

    var p := (k, l) reads a requires 0 <= k < a.Length requires 0 <= l < a.Length => a[k] == a[l];
    var q := (i, k) reads a requires 0 <= i => 0 <= k < i <= a.Length ==> exists l | 0 <= l < i :: p(k, l);
  
    while i < a.Length
        invariant i >= 0
        invariant i <= a.Length
        invariant unchanged(a)
        invariant forall k: int :: q(i, k)
    {
        assert forall k: int :: q(i, k);
        i := i + 1;
        assert forall k: int :: q(i, k);
    }
}

Now Dafny is able to prove the first assertion from the invariant and the invariant from the second assertion. Only the second assertion is failing, but now you can help the verifier along as usual.

Footnotes

1. https://stackoverflow.com/a/50671326/8857097 ↩

[keyboardDrummer]

Related issue: #4920