Shifting and bit-masking integers are operations that make sense. Storing an int in memory and loading back only one of its bytes is equivalent to loading it all, then shifting and masking. It's meaningful, thus you do need to model the bits faithfully.
In contrast, shifting and masking pointers is (with some exceptions) not meaningful. Neither is it meaningful to store one of these in memory and to load back only part of it. It makes sense to use a more abstract, symbolic model for bytes of such values.
For whatever it's worth, the author's solution for bytes is the same as CompCert's: https://github.com/AbsInt/CompCert/blob/3939a1ccfdb86795e9fd...
I guess one could make a similar argument for the bytes of a unicode string.
While writing this, it occurred to me that the difficulties with casting between pointers and integers is in going from integers to pointers, where there is no unique mapping (for pointer to integer, base + offset is meaningful, but it loses information.)
That's not incorrect. However, the reason I am doing that is because this is what C is all about (nowadays, at least): Compilers doing high-level optimizations based on alias analysis and other sources, and programmers expecting to have a low-level picture of memory.
Our choice is to either give up and declare C broken beyond repair, or try to find some way to reconcile these two worlds as best as possible.
One can, of course, map {base, offset} pointers to the natural numbers (though not necessarily Rust integer types? I don't know Rust) by considering the base to be the most significant bits of the number and the offset the least, but arithmetic on these numbers is not the same as pointer arithmetic in the address-space model.
I do not follow the part, in the "what's in a byte" section, about a byte-by-byte memcpy. Is the question "what is the first byte?" any more or less problematical for a {base, offset} pointer than it is for a multi-byte integer, where place value matters?