{
"$type": "site.standard.document",
"bskyPostRef": {
"cid": "bafyreif2f73l4hkqylhwdjthxh54wwyftqyanj3g6q2avecdmfrgxi5f5q",
"uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mmmcuql4jo42"
},
"path": "/t/include-racy-reads-in-rust-memory-model-with-maybeinvalid-t/24289?page=2#post_21",
"publishedAt": "2026-05-24T14:52:26.000Z",
"site": "https://internals.rust-lang.org",
"textContent": "Are the proofs in question publicly available? It would be interesting to look at them to see whether the new operation would invalidate any of the existing steps in the proof. (I had intended to prove it to be a sound extension to the memory model by quantifying over all possible implementations and showing that none could be affected, but it would probably be easier to check the existing proofs to make sure that they still work.)",
"title": "Include racy reads in Rust memory model with `MaybeInvalid<T>`"
}