How to prove a modification of an array's item was successful?

Question

I am verifying a matrix multiplication procedure: Here is my code:

predicate abvalid(a:array<array<int>>, b:array<array<int>>)
reads a, b
{
    a.Length > 0
    && b.Length > 0 
    && (forall i, j ::(0 <= i < a.Length && 0 <= j < a.Length) ==> (a[i].Length == a[j].Length == b.Length))
    && forall i, j :: (0 <= i < b.Length && 0 <= j < b.Length) ==> (b[i].Length == b[j].Length>0)
}


function rowcolmulAux(a:array<array<int>>, b:array<array<int>>, row:int, col:int, k :int) :int 
requires abvalid(a, b)
requires 0<=row < a.Length
requires 0<=col < b[0].Length
requires 0 <= k <= a[0].Length
decreases a[0].Length - k
reads a[..]
reads b[..]
reads a, b
ensures rowcolmulAux(a, b, row, col, k) == if k == a[0].Length then 0 else a[row][k] * b[k][col] + rowcolmulAux(a, b, row, col, k+1)
ensures (k == a[0].Length ==> rowcolmulAux(a, b, row, col, k) == 0) && (k < a[0].Length ==> rowcolmulAux(a, b, row, col, k) == a[row][k] * b[k][col] + rowcolmulAux(a, b, row, col, k+1))
{
    if k == a[0].Length then 0
    else a[row][k] * b[k][col] + rowcolmulAux(a, b, row, col, k+1)
}

function rowcolmul(a:array<array<int>>, b:array<array<int>>, row:int, col:int) :int 
reads a
reads b
reads a[..]
reads b[..]
requires abvalid(a, b)
requires 0<=row < a.Length
requires 0<=col < b[0].Length
ensures rowcolmul(a, b, row, col) == rowcolmulAux(a, b, row, col, 0)
ensures rowcolmul(a, b, row, col) == rowcolmul(a, b, row, col)
{
    rowcolmulAux(a, b, row, col, 0)
}
method rowmul(a:array<array<int>>, b:array<array<int>>, c1:array<int>, index:int, indexc: int)
requires abvalid(a, b)
requires 0 <= index < a.Length
requires c1.Length == b[0].Length
requires 0 <= indexc < c1.Length
modifies c1
ensures forall i :: 0 <= i < c1.Length && i != indexc ==> c1[i] == old(c1[i])
ensures c1[indexc] == rowcolmul(a, b, index, indexc)
{
    c1[indexc] := rowcolmul(a, b, index, indexc);
}

abvalid: ensures that a and b are valid matrices. rowcolmul and rowcolmulAux: two functions to do the computation for the output matrix's one item. rowmul: a method to store the computation for the output matrix's one item.

Dafny complains that Could not prove: c1[indexc] == rowcolmul(a, b, index, indexc)

The rowmul only has one statement:

c1[indexc] := rowcolmul(a, b, index, indexc);

So I assume that c1[indexc] == rowcolmul(a, b, index, indexc) holds.

Answer 1

The issue comes from reads a[..] and reads b[..]. This indicates that any reference could be read, including c1.

Making Dafny know that c1 cannot be accessed solves this issue:

method rowmul(a:array<array<int>>, b:array<array<int>>, c1:array<int>, index:int, indexc: int)
requires abvalid(a, b)
requires 0 <= index < a.Length
requires c1.Length == b[0].Length
requires 0 <= indexc < c1.Length
modifies c1
ensures forall i :: 0 <= i < c1.Length && i != indexc ==> c1[i] == old(c1[i])
ensures c1[indexc] == rowcolmulAux(a, b, index, indexc, 0)
requires forall i :: 0 <= i < a.Length ==> c1 != a[i]
requires forall i :: 0 <= i < b.Length ==> c1 != b[i]
{
    c1[indexc] := rowcolmul(a, b, index, indexc);
}

This ensures that the write to c1[indexc] in the first line of the implementation does not change any particular a[i] and b[i].

The answer comes from Dafny's Zulip channel.