Can Dafny verify summing elements from the right?

Question

Hi I gather that when performing induction Dafny unfold the specification of a function. Thus when writing a method that implements the function it is best to traverse an array in the similar direction. This understanding corresponds the behaviour of sumLeftChange (given below) But I can not verify sumRightChange at all. Can anyone explain what I am missing?

function method sumSpec(input:seq<nat>) : nat
decreases input 
{  if |input| == 0 then 0 else input[0]+ sumSpec(input[1..]) }
function method sumSpecR(input:seq<nat>) : nat
decreases input 
{ if |input| == 0 then 0 else input[|input|-1]+ sumSpecR(input[..|input|-1]) }
method sumLeftChange(input:seq<nat>) returns (r:nat)
  ensures r == sumSpec(input)
//  ensures r == sumSpecR(input)
{   r :=0; var i:nat := 0;
    while (i<|input|)
     decreases |input| - i
     invariant i<= |input|
     invariant  r == sumSpec(input[|input| - i..])
   //  invariant  r == sumSpecR(input[|input| - i..]) //fails and should fail
    {   r:= r+input[|input| - i-1]; // first element is from right |input|-1
        i := i+1;
        print "sumLeftChange  ", i," r  ", r,"  ", sumSpec(input[|input| - i..]) ,"\n";
    } 
}
method sumRightChange(input:seq<nat>) returns (r:nat)
{  r :=0; var i:nat := 0;
    while (i<|input|)
     decreases |input| - i
     invariant i <= |input|    
    // invariant  r == sumSpecR(input[..i]) //I can get nothing to work
    {  
        r:= r+input[i];  // first element is from left  0     
        i := i+1; 
    print "sumRightChange   ", i," r= ", r,"  sumSpecR(input[..i])= ", sumSpecR(input[..i]) ,"\n";
    }
}
method Main() {
    var sl:nat := sumSpec([1,2,3,4]);
    print "\n";
    var sr:nat := sumSpecR([1,2,3,4]);
    print "\n";
    var sLc:nat := sumLeftChange([1,2,3,4]);
    print "\n";
    var sRc:nat := sumRightChange([1,2,3,4]);
    print "sl ", sl,"  sL= ",sLc, "\n";
    print "sr ", sr,"  sR= ",sRc, "\n";
}

Answer 1

Adding assert input[..i+1][..i] == input[..i]; to the beginning of the loop body will cause sumRightChange to verify.

This is an instance where we have a true fact that Dafny will not think to "try" on its own until you ask it, but once you ask it "hey, is input[..i+1][..i] == input[..i]?" then is says "oh, yeah, obviously." And then it has that fact lying around to help the proof later. (This kind of "you have to ask for it" behavior is very common when working with equations between collections such as sets, lists, or maps in Dafny. For more information, see this answer.)

---

Probably the more important question is, how did I determine that this is the right fact to "point out" to Dafny?

Here's how. (I apologize for how long this got, but I wanted to show you my full process and explain what I was doing at each step. I won't be offended if you don't read it all.)

I started with the following loop inside sumRightChange, uncommenting the failing invariant. (I deleted the print statement for brevity.)

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    r := r + input[i]; 
    i := i + 1;
  }

Dafny reports "invariant might not be maintained". I know that this means that Dafny tried to assert the invariant at the bottom of the loop, and it failed. Just to double check myself, I copy paste the invariant and convert it into an assert at the bottom of the loop.

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    r := r + input[i]; 
    i := i + 1;
    assert r == sumSpecR(input[..i]);  // added this line
  }

As expected, Dafny reports an assertion violation. But, the error on the invariant goes away, which gives me confidence that if I can prove this assertion, I'm done.

I also know that I get to assume the invariant at the top of the loop. I'd like to "move" these two facts (the assumed invariant at the top and the asserted invariant at the bottom) towards each other. It turns out to be easier to move things backwards than forwards, so I will proceed to try to move the assertion at the bottom of the loop up bit by bit.

The trick for moving an assertion backwards across an assignment is to manually "undo" the assignment inside the assertion. So, to move the assertions r == sumSpecR(input[..i]) backwards across the assignment i := i + 1, I will replace all the occurences of i with i + 1. This is the "same fact", just asserted at a different time. Since the value of i is different at that different time, the assertion has to be syntactically modified in order to be the "same fact". Hopefully that makes some sense... Anyway, performing that transformation yields this loop:

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    r := r + input[i];
    assert r == sumSpecR(input[..i+1]);  // moved this assertion up one line
    i := i + 1;
  }

Dafny still reports an assertion violation. And critically it still does not report an invariant violation. So we still know that if we can prove the assertion, we have verified the whole loop.

(Notice what would happen if we made a mistake while moving the assertion. For example, if we had not manually replaced i with i+1 and instead just blindly moved the assertion up one line. Then Dafny reports an assertion violation and an invariant violation, so we know we screwed up!)

Now let's move the assertion up one more line, backwards across the assignment r := r + input[i];. Again, the trick is to manually undo this assignment by replacing r with r + input[i] in the assertion, like this:

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    assert r + input[i] == sumSpecR(input[..i+1]);  // moved this assertion up one line
    r := r + input[i];
    i := i + 1;
  }

Again, Dafny reports an assertion violation but not an invariant violation. (And, again, if we had messed up, it would have reported an invariant violation.)

Now we have the assertion at the top of the loop, where we know the invariant holds. It's time to do a proof.

We are trying to prove an equation. I like to use Dafny's calc statement to debug proofs about equations. If you're not familiar with the calc statement, the basic form is

calc {
  A;
  B;
  C;
  D;
}

which proves A == D by proving A == B, B == C, and C == D. This makes for a convenient way to add intermediate steps to the equational proof, and to narrow down exactly where Dafny is confused.

To convert an assertion of an equation into a calc statement, we can just put the left-hand side of the equation on the first line, and the right-hand side on the second line. So far, this changes nothing, but let's just make sure:

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    // replaced old assertion with the following calc statement
    calc {
      r + input[i];
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Dafny reports an error in the calc statement, but still not on the invariant, so we still know we're proving the right fact to finish verifying the loop.

The error is on the second line of the body of the calc statement, and the message says "the calculation step between the previous line and this line might not hold". Basically, Dafny could not prove the two lines equal. Not surprising, since we produced this calc statement from a failing assertion.

Now we're in a position to start adding intermediate steps. Sometimes, it makes sense to work forwards from the top line, while other times it makes sense to work from the last line upwards. I think the second strategy makes more sense here.

Let's manually unfold the definition of sumSpecR and see where we get stuck. Looking at the definition of sumSpecR, it first checks whether |input| == 0. Be careful, because input here refers to the argument to sumSpecR, not the argument to sumRightChange! In the context of the last line of our calc statement, we're passing input[..i+1] into sumSpecR, so the definition is asking whether this list has length zero. But we know it does not, since i >= 0 and we add 1 to it. So we will be in the else branch of the definition.

The else branch takes apart the list from the right. Let's try to be systematic and just copy-paste the else branch of the definition, substituting the actual argument input[..i+1] for the parameter name input. (I like to use my text editor to search and replace for this step.)

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      // added the following line by copy-pasting the else branch of the 
      // definition of sumSpecR and then replacing its parameter
      // input with the actual argument input[..i+1]
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Now pay close attention to what happens to the error message. It moves up a line! This means we're making progress, because Dafny agrees with us that our new middle line of the body of the calc statement is equal to the last line.

There are lots of simplifications we can do now. Let's start by simplifying |input[..i+1]| to i+1. You could do that by modifying the line we just added, but I like to do it by adding yet another line above it, so that I can record my progress, and make sure Dafny agrees that I'm moving in the right direction.

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      // added the following line simplifying |input[..i+1]| into i+1
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Again, the error message moves up a line. Yay!

Now we can simplify i+1-1 into i and also input[..i+1][i] into input[i]. Again, I prefer to do this on a new line.

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      input[i] + sumSpecR(input[..i+1][..i]);  // added this line
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

The error message continues to march upward.

The next simplification I'd like to do is to convert input[..i+1][..i] into input[..i]. Again, I use a new line.

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {  
    calc {
      r + input[i];
      input[i] + sumSpecR(input[..i]);  // added this line
      input[i] + sumSpecR(input[..i+1][..i]);
      input[..i+1][i+1-1] + sumSpecR(input[..i+1][..i+1-1]);
      input[..i+1][|input[..i+1]|-1] + sumSpecR(input[..i+1][..|input[..i+1]|-1]);
      sumSpecR(input[..i+1]);
    }
    r := r + input[i];
    i := i + 1;
  }

Pay close attention to what happens to the error message. It does not move! That tells us two things. First, Dafny does not agree with our most recent simplification. Second, Dafny says that our newly added line is equal to the first line of the calc statement! (Here Dafny is making use of the assumption of the loop invariant telling us r == sumSpecR(input[..i]).) So even though we were working from the last line upward, we now actually have reached the top, with a gap remaining in between lines 2 and 3.

So, Dafny fails to see that

input[i] + sumSpecR(input[..i]) == input[i] + sumSpecR(input[..i+1][..i])

What gives? The expression input[i] appears on both sides, so what remains to show is

sumSpecR(input[..i]) == sumSpecR(input[..i+1][..i])

Here we have a function sumSpecR applied to two syntactically different arguments that we believe are the same. It doesn't matter what the definition of sumSpecR is at this point, all that matters is that it is a function being applied to equal arguments. So we can try to check that the arguments really are equal.

assert input[..i] == input[..i+1][..i];

And that's the assertion we needed to get the whole proof to go through.

---

At the end of a debugging process like this, I usually like to clean things up and keep only the facts that Dafny actually needed to do the proof. So I just try deleting stuff and seeing whether the proof still works. In this case, only the very last assertion we discovered is required; everything else can be deleted.

Here is my final loop:

  while (i < |input|)
    decreases |input| - i
    invariant i <= |input|    
    invariant r == sumSpecR(input[..i])
  {
    assert input[..i] == input[..i+1][..i];  // load-bearing assertion due to sequence extensionality
    r := r + input[i];
    i := i + 1;
  }

I like to leave myself a little note reminding me that I think the proof will not work without this assertion, along with my best guess as to why the assertion is needed.