This particular example is especially amusing; in the current provenance proposal for C, casting a_plus_1 back up to a pointer produces a value that has provenance of either a or b; the choice is up to the programmer, so long as they are consistent. In dereferencing it, the programmer has asserted it isn't a one-past-the-end pointer, and thus its provenance is fixed to b forevermore.
(Your example is useful, but this is nonetheless an important corner case within the corner case.)
I don't believe there is a "current" definition, beyond whatever the latest proposal @RalfJung has written down is. Rust just does the unsound "haha this kind of exists" all the other compilers do (mostly due to inheriting it from LLVM). I don't think there is a status quo to measure against.