Description
There's another aspect of provenance that we haven't officially decided yet and that is implicitly answered by the current wording in rust-lang/reference#1664: do the individual bytes in a pointer "remember" where in the pointer they are, and have to be put back in the same order? Some formal models require this, and if we ever allow "taking apart" the bytes of a pointer in const-eval (rust-lang/const-eval#72) we'll also have to require this, but for runtime semantics we could decide either way.
The one example of code that I am aware of that breaks this requirement is XOR linked lists, which can be implemented in the semantics sketched in MiniRust right now but can't be implemented if bytes with provenance remember their position in the pointer. That's not exactly realistic code, but it is somewhat satisfying that (on architectures where pointers have at least 2 bytes), XOR linked lists can be implemented.
The main upside of requiring the same bytes in the same order is that it rules out pointer crimes like XOR linked lists so if there's some unexpected interactions there, we'd not be affected. It would also make the runtime semantics more consistent with the const-eval semantics. I am not aware of an optimization that would benefit from this UB, it's mostly a case of "ruling out some rather cursed programs to avoid locking ourselves into an unexpected corner". In some sense the model becomes a bit simpler since we can just say, pointer bytes must be put back together in the same order they started out as before they can be treated as a pointer again, but the actual op.sem would become more complicated because of the extra bookkeeping required to enforce this.