dafny - ネストされたループのインデックス範囲外エラー

Question

このコードが「範囲外のインデックス」エラーを生成する理由を誰か教えてもらえますかinput[i*cols + j]?

method foo(input: array<int>, rows:int, cols:int)
requires input != null 
requires rows > 0 && cols > 0
requires rows * cols == input.Length
{
   var i := 0;
   while i < rows
   {
     var j := 0;
     while j < cols
     {
       var s := input[i*cols + j];
       j := j + 1;
     }
     i := i + 1;
   }
}