for-range: 0 <= i cannot be proven without len(x) > 0

[ThomasMayerl]

In for-range loops, assertions concerning the current index cannot be verified if we don't assert that the length of the slice is larger than 0. For example, if we take the example from the range1 testfile:

preserves acc(x)
requires len(x) > 0
ensures forall i int :: 0 <= i && i < len(x) ==> max >= x[i]
decreases
func foo(x []uint) (max uint) {
	max = x[0]
	invariant acc(x)
	invariant 0 <= i && i <= len(x)
	invariant forall k int :: 0 <= k && k < i0 ==> max >= x[k]
	decreases len(x) - i0
	for i, j := range x with i0 {
		if j > max {
			max = j
		}
	}
}

And modify it so that we don't need an element to be present (by setting max to 0 by default) and remove the precondition that len(x) > 0, we get a verification error that the precondition might not be established: Assertion 0 <= i might not hold.

preserves acc(x)
ensures max == 0 || forall i int :: 0 <= i && i < len(x) ==> max >= x[i]
decreases
func foo2(x []uint) (max uint) {
	max = 0
	invariant acc(x)
	invariant 0 <= i && i <= len(x)
	invariant forall k int :: 0 <= k && k < i0 ==> max >= x[k]
	decreases len(x) - i0
	for i, j := range x with i0 {
		if j > max {
			max = j
		}
	}
}

Should this be the case?

[ThomasMayerl]

So what happens is that Gobra basically creates a conditional, where, if len(x) == 0, we don't create any assumptions about i, nor i0. We just assume that i == i0. Afterwards, there are asserts for each of the invariants. A fix would thus be to simply initialize i to 0, even if len(x) == 0. However, according to test regressions/features/loops/range-fail8.gobra, this should fail. I wonder what the intuition behind this is. In my opinion, the above code should also work if we don't know anything about the length of x. If the length is 0, we still have access to all of its elements, because there are none. I'd have a fix ready but I'd appreciate any insight as to whether this change would be sound, before opening a PR.