The precise keywords here are obviously not final until the Language Work Group weighs in.
A lot of alternatives have been discussed as part of the thread on the borrow and inout local declarations: Pitch: `borrow` and `inout` declaration keywords (My personal favorite is some variation of "mutate" or "mutating", but I trust the LWG to make a good decision and to make sure that aligns across all the related language features.)
The "as if rule" allows the optimizer to make any such changes that provide the same visible behavior. Over time, I'm certain the optimizer folks will be looking at how to take advantage of borrowing whenever it makes things faster without breaking the behavior. This is one reason I'm happy to wait on possibly changing the behavior of plain for..in until we get a little more experience with the backing machinery.
The other thread mentioned above is proposing a way to do exactly this (just replace "alias" with "inout" in your example to match that other pitch). The various rules about it being a "borrowing reference" are really nothing more than a particular set of compiler checks and constraints which ensure that such "aliases" are actually safe. In fact, an early draft of that proposal used the word "alias" here instead of "inout", and it's still one of the possible spellings being considered.