I am new to Dafny, and here is my Dafny code that finds the index of an input array such that the value in the array at that index is the maximal. However, Dafny indicates that there is an index out of range problem on line 8 (var max: int := a[0];). This is highly confusing as it seems trivially correct. Can anyone offer insights to this problem? Thank you!

method FindMax(a: array<int>) returns (index: int)
    ensures 0 <= index && index < a.Length
    ensures forall i:: 0 <= i && i < a.Length && i != index ==> a[i] <= a[index]
{
    // Can you write code that satisfies the postcondition?
    // Hint: you can do it with one statement.
    var i: nat := 0;
    var max: int := a[0]; // index out of range ???
    var max_idx: int := i;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant 0 <= max_idx <= a.Length
    {
        if a[i] > max 
        {
            max_idx := i;
            max := a[i];
        }
        i := i + 1;
    }
    return max_idx;
}

I ran this code in VS Code with Dafny extension installed.