Dafny assertion limitation increase?

Question

predicate Contains(haystack: string, needle: string)
    ensures Contains(haystack, needle) <==> exists k :: 0 <= k <= |haystack| && needle <= haystack[k..] 
    ensures Contains(haystack, needle) <==> exists i :: 0 <= i <= |haystack| && (needle <= haystack[i..])
    ensures !Contains(haystack, needle) <==> forall i :: 0 <= i <= |haystack| ==> !(needle <= haystack[i..])
{
    if needle <= haystack then 
        assert haystack[0..] == haystack;
        true 
    else if |haystack| > 0 then 
        assert forall i :: 1 <= i <= |haystack| ==> haystack[i..] == haystack[1..][(i-1)..];
        Contains(haystack[1..], needle)
    else 
        false
}

Testing this predicate shows some interesting but frustrating behavior.

method TestContains() {
    assert Contains("aba||xx||c", "|") == true; //verifies
    assert Contains("aba||xx||c", "||") == true; //verifies
    assert Contains("aba||xx||c", "||xx||") == true; //verifies
    assert Contains("aba||xx||c", "|||") == false; //does not verify
}

In particular Dafny cannot evaluate whether Contains("aba||xx||c", "|||") is true or false. Neither assertion will verify. All obvious true examples for Contains verify quickly but any false statement with a separator of 1 letter like Contains("aa", "b") will verify, but with 2 letters or more it will no longer verify, like Contains("axa", "ba").

Is there a way to increase the limit or otherwise convince Dafny to verify them? I tried to use {:fuel X} but it did not seem to help.

Answer 1

Here's one way to convince Dafny:

method TestContains() {
    assert !Contains("axa", "ba") by {
      assert "ba"[0] != "xa"[0];
    }
}

Here's how I actually discovered this trick. I worked backwards from the failing assertion. I decided to use a calc to manually step through the execution of Contains until Dafny got stuck:

calc {
  Contains("axa", "ba");
  Contains("xa", "ba");        
  Contains("a", "ba");  // error: previous line might not be equal to this line
}

So then I started trying to prove that Contains("xa", "ba") == Contains("a", "ba"). Reading the code of Contains, we need to know that !("ba" <= "xa"), but Dafny can't see that either.

assert !("ba" <= "xa");  // error: assertion might not hold

So then I started trying to prove that. Since <= is built-in, we can't look at its definition easily (or can we? see below). But I guessed that roughly speaking it was defined as "all the characters are the same up until the end of the shorter string". So I figured, if I can show that some character is not the same, maybe Dafny will see it.

assert "ba"[0] != "xa"[0];

That assertion passes, and what's more, it unlocks all the other failing asserts and the whole thing verifies. Here's the state of the program as of when I first got it to verify.

method TestContains() {
    assert !Contains("axa", "ba") by {
      calc {
        Contains("axa", "ba");
        Contains("xa", "ba");        
        {
          assert "ba"[0] != "xa"[0];
          assert !("ba" <= "xa");
          assert "xa"[1..] == "a";
        }
        Contains("a", "ba");
      }
    }
}

Then I did some typical cleanup-after-debugging and got to the program at the top of this answer.

---

If you are curious, it actually is pretty easy to find the definition of <=. Use this command:

dafny /print:foo.bpl foo.dfy

This will generate the underlying Boogie code. (Replace foo.dfy with the name of your file and foo.bpl with your desired output file name.)

Then open foo.bpl in your text editor and search for the line

// definition axiom for _module.__default.Contains (revealed)

You will see an axiom on the next line that, among other things, calls Seq#SameUntil. So we've learned that that's the Boogie-level name for what Dafny calls string-<=.

Now search for

function Seq#SameUntil 

and you will find its defining axiom:

axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: 
  { Seq#SameUntil(s0, s1, n) } 
  Seq#SameUntil(s0, s1, n)
     <==> (forall j: int :: 
      { Seq#Index(s0, j) } { Seq#Index(s1, j) } 
      0 <= j && j < n ==> Seq#Index(s0, j) == Seq#Index(s1, j)));

Turns out, it's exactly what I guessed.