I believe this is because there are no writes in f. All the loads of s get coalesced into a single load, so prove can tell that the slice you're ranging over is the same as the one you're indexing.
In g, there's a write, so the s inside the loop is reloaded every time. That s might have a different length, so a bounds check is needed.
I don't think this qualifies as a bug. Closing. Maybe there's something that could be done with g, like proving that the location written doesn't alias the s global, but we haven't gone there yet.