I am trying to write a Dafny function that converts 2D matrix indices to a 1D array index. Below contains my current code.
The issue I face is that Dafny's verification times out after 20 seconds. Is there something particularly complex about what I am trying to verify?
Here is my code:
method calc_index(i: int, j: int, rows: int, cols: int) returns (index: int)
requires 0 <= i < rows && 0 <= j < cols
requires rows > 0 && cols > 0
ensures 0 <= index < rows*cols
{
assert 0 <= i < rows && 0 <= j < cols;
index := (i * cols) + j;
}
Working it out by hand, I am convinced that this conversion is done correctly and I wasn't expecting to face any major issues.
Z3 which is underlying solver for Dafny has hard time proving this non linear inequality (In general it is undecidable). You can guide it though using calculation style proof.
method calc_index(i: int, j: int, rows: int, cols: int) returns (index: int)
requires 0 <= i < rows && 0 <= j < cols
requires rows > 0 && cols > 0
ensures 0 <= index < rows*cols
{
index := (i * cols) + j;
calc >= {
rows * cols - 1;
(rows - 1) * cols + cols - 1;
i * cols + cols - 1;
i * cols + j;
}
}