Proving correctness of Matrix Addition

I want to prove the correctness of 2D matrix addition in Dafny (using the VSCode extension) with the aim of identifying SMT-proveable loop invariants. I believe this should be fairly straight forward as the computations only involve addition.

My implementation involves 2 loops. An outer loop iterating over the rows. And an inner loop iterating over the columns. Dafny is throwing errors regarding my outer loop invariant.

I believe I have not 'helped' Dafny enough with reasoning about the invariant. However I am unsure with how to proceed.

Below is my implementation. Without the assertion at the end of the outer loop, Dafny reports this invariant could not be proved to be maintained by the loop. When I include the assertion of the invariant at the end of the outer loop body, Dafny reports assertion might not hold.

method Order2Addition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
    requires m1 != m3 && m2 != m3
    requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
    ensures CorrectMatrixAddition(m1, m2, m3)
    modifies m3
    {
        var rows: int := m1.Length0;
        assert(rows == m2.Length0 && rows == m3.Length0);
        var cols: int := m1.Length1;
        assert(cols == m2.Length1 && cols == m3.Length1);
        var i: int := 0;
        while (i < rows)
            invariant 0 <= i <= rows
            // All rows up to row i-1 are correct
            invariant forall i':int, j':int :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']
            decreases rows - i
            modifies m3
        {
            var j: int := 0;
            while (j < cols)
                invariant 0 <= j <= cols
                // All column values on row i, up to column j-1 are correct
                invariant forall j': int :: 0 <= j' < j ==> m3[i, j'] == m1[i, j'] + m2[i, j'] 
                decreases cols - j
                modifies m3
            {
                m3[i, j] := m1[i, j] + m2[i, j];
                j := j + 1;
            }
            i := i + 1;
            assert(forall i':int, j':int :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']);
        }
    }

predicate CorrectMatrixAddition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
    requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
    requires m1 != m3 && m2 != m3
    reads m1, m2, m3
{
    forall i: int, j: int {:trigger m3[i,j]} ::  0 <= i < m1.Length0 && 0 <= j < m1.Length1 ==> m3[i, j] == m1[i, j] + m2[i, j]
}

The reason your program does not verify is that the inner loop also needs the invariant that "All rows up to row i-1 are correct". (My book "Program Proofs" discusses this point in section 14.1.1.)

You can also shorten many things. The following is a version that verifies:

method Order2Addition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
  requires m1 != m3 && m2 != m3
  requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
  ensures CorrectMatrixAddition(m1, m2, m3)
  modifies m3
{
  var rows, cols := m1.Length0, m1.Length1;
  var i := 0;
  while i < rows
    invariant 0 <= i <= rows
    // All rows up to row i-1 are correct
    invariant forall i', j' :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']
  {
    var j := 0;
    while j < cols
      invariant 0 <= j <= cols
      // All column values on row i, up to column j-1 are correct
      invariant forall i', j' :: 0 <= i' < i && 0 <= j' < cols ==> m3[i', j'] == m1[i', j'] + m2[i', j']
      invariant forall j' :: 0 <= j' < j ==> m3[i, j'] == m1[i, j'] + m2[i, j'] 
    {
      m3[i, j] := m1[i, j] + m2[i, j];
      j := j + 1;
    }
    i := i + 1;
  }
}

predicate CorrectMatrixAddition(m1: array2<int>, m2: array2<int>, m3: array2<int>)
  requires m1.Length0 == m2.Length0 == m3.Length0 && m1.Length1 == m2.Length1 == m3.Length1
  reads m1, m2, m3
{
  forall i, j :: 0 <= i < m1.Length0 && 0 <= j < m1.Length1 ==> m3[i, j] == m1[i, j] + m2[i, j]
}

You can also use for loops instead of the while loops, if you prefer.

In fact, you can also do this example in Dafny without any loops at all, which saves you having to write any loop invariants (but I suppose that won't help your goal of trying to identify SMT-solvable loop invariants). You can replace the body of the method with this aggregate statement:

  forall i, j | 0 <= i < m1.Length0 && 0 <= j < m1.Length1 {
    m3[i, j] := m1[i, j] + m2[i, j];
  }