Include racy reads in Rust memory model with `MaybeInvalid<T>`

Adding any new primitive operation to a memory model requires re-doing all proofs about the model. Memory models aren't "additive"; their correctness relies as much on the exact details of the existing operations as it does on the absence of other operations.

IIUC, the goal of this thread is to enable SeqLocks in well-defined Rust. The by far most promising avenue to achieve that is atomic bytewise memcpy. The alternatives you are proposing are a lot more complicated in terms of what would have to be done to ensure they are well-defined and sound.