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.

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.

• matrix-multiplication
• verification
• dafny

2 Answers 2

Dafny has support for multidimensional arrays. You can use the type array2, or array3, etc.. all the way up to 20 I think.

Do you need the array to be mutable or just need to do the matrix methods correctly? If the former you can stick with array2, but otherwise it is better to use an immutable datatype and pure functions on that type. Verifying methods about mutable datatypes is consistently much harder in Dafny than verifying functions on immutable data.

Secondly, you can write lemmas about functions but not about methods in Dafny. To verifying further calculations you may want to compose several operations and make statements about that combination, but you cannot do to that easily with methods.

I have some matrix operations defined here for example.

The issue comes from reads a[..]. 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.