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

RalfJung:

You might be tempted to pick the story "picks an arbitrary value that satisfies the validity invariant of T" (after proving that such a value exists), but then clients using this library could not, for soundness purposes, rely on actually getting back the value they wrote.

The "story" here is that we read an arbitrary value if the check has not passed, and the value of T which we wrote for the checked sequence number otherwise (i.e. the read did not race). As I wrote in my comment, we "prove" it by using external knowledge about assembler and hardware behavior. From the language point of view it's indeed an arbitrary value which has absolutely no relation to the value written previously (which is inevitable since asm! is a black box for the compiler), but IMO it's fine.

We as programmers know that we read the expected value and handle it under this assumption (e.g. by calling assume_init). To the clients we just document "pinky promise, it's the same value which you wrote previously" and it's sufficient as any other library-level safety promise.

The "stories" which we tell each other have nothing to do with how the compiler actually functions. It's just a tool to convince ourselves that the inline assembly behaves as we expect while interacting with the rest of Rust code. I know you don't like such arguments, but I can not see how asm!-based racy read could badly interact with compiler optimizations in practice (ofc only under the "black box" assumption).