indexingverificationdafnyformal-verification

Issues with converting 2D matrix indices to 1D array index


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.


Solution

  • 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;
      }
    }