We are generally at a point where if it's documented, it's guaranteed. This feature is really easy to describe, and so we have a high degree of confidence that when we say "this behavior is defined", we won't run into an edge case where we'd have to break it.
So, in this case, it's a documented part of Option.
I realize this answer isn't fantastic, but it's where we're at now. It's why we're working on the reference this year!
