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

ais523:

Or in other words, I don't see the angelic choices as being made immediately. Rather, I think that sort of choice works like variables in Prolog:

You are describing something more akin to symbolic execution than angelic choice. Symbolic execution is indeed a way to approximate or even implement angelic choice. But having that in an actual program run (rather than in a program analyzer) requires explicitly adding symbolic state to the program state, which in turn affects everything else that reasons about the program state.

For ptr2int casts specifically, the PNVI-ae-udi model in C does pretty much that: the "udi" mechanism introduces a symbolic form of provenance that approximates the angelic semantics. Sadly it does not easily work with more complicated models such as Stacked/Tree Borrows, or even with restrict in C.