"accessible" terminology in with_exposed_provenance docs is misleading

[saethlin]

During stabilization, we changed the documentation of exposed provenance from saying that memory outside the AM "is always exposed" to "is always accessible". Based on a conversation I just had, I believe the new documentation to be wrong, because it suggests that this program is permitted:

use std::ptr;
fn main() {
    // Create a byte we "magically" know the address of (by capturing it)
    // Another way to stash or know a valid-to-write address would make a better demo.
    let mut byte = 0u8;
    let magic_addr = &mut byte as *mut u8 as usize;
    
    let func = |r: &mut u8| {
        *r = 123;
        unsafe {
            // The docs say:
            // memory which is outside the control of the Rust abstract machine
            // (MMIO registers, for example) is always considered to be accessible
            // with an exposed provenance
            // So this address should be accessible, according to the docs.
            // But the access here is a clear violation of the noalias attribute.
            dbg!(*ptr::with_exposed_provenance::<u8>(magic_addr))
        }
    };
    
    let ptr = ptr::with_exposed_provenance_mut::<u8>(magic_addr);
    unsafe {
        func(&mut *ptr);
    }
}

The current documentation can be traced to this part of the stabilization PR discussion: #130350 (comment)

I am writing this up as I am heading to bed, so please just correct me if I seem wrong. cc @rust-lang/opsem

[wffirilat]

The "issue" here arises not because of the unsafe block inside func, but the unsafe block in main that calls func.

Creating an &mut reference from a raw pointer means it's your responsibility to ensure the relevant aliasing guarantees on that memory apply during the time that reference will exist, which is obviously nearly impossible when that memory is globally accessible from an exposed provenance.

[RalfJung]

The full wording in the docs is "is always considered to be accessible with an exposed provenance". I can see how that can be confusing -- we don't want to repeat the full aliasing model in these docs, and yet of course the entire aliasing model is relevant to determine what can truly be done with such a pointer.

I don't think we can say "memory outside the AM is always exposed" since being "exposed" is a property of a specific provenance, not some memory. That's why I reworded the docs.

Any suggestions for how to fix the ambiguity without being sloppy about what exactly is being "exposed"?

[wffirilat]

Personally I don't have issue with the word "accessible" here. Strict Provenance is fundamentally a model that restricts previously-unrestricted integer-to-pointer casts, it doesn't give permission to do anything that you couldn't do before as far as I know, only disallows doing potentially dubious things that weren't (rightly) disallowed before.

In particular, one can't truncate "always accessible with exposed provenance" into just "always accessible" and expect the meaning to remain the same.

At most, I'd like to see a more explicit definition of what "accessible" means in the context of provenance in the top-level section on pointer provenance. "Accessible with <x> provenance" is a perfectly coherent way of expressing the concept of "the provenance rules don't prohibit this", to me.

If this explicit definition of "accessible" were added, it'd basically just be a restatement or extension of the wording about pointers talking about

The provenance it has, defining the memory it has permission to access. Provenance can be absent, in which case the pointer does not have permission to access any memory.

edit: Actually, if one really wanted to be explicit, as a local fix one could change it to "always accessible [by a pointer constructed from] exposed provenance", but that feels verbose and would also imply changing anywhere else in the docs where the pointer-ness of access is elided in a similar way

edit 2: Oh wow, trying to be formal about exposed provenance not actually being a single entity makes wording this much harder. Angelic nondeterminism as we see in the theory is really not friends with the actual reality of what implementations have to look like. Maybe talking about "pointers constructed with exposed provenance" is actually the right angle, since we already have ptr::with_exposed_provenance[_mut] that uses that terminology and has docs that loosely handle the theoretical nondeterminism? (Those docs do not inspire much confidence in the output but even so that might be the best we can do?)

[wffirilat]

I got it! I'm fairly confident that the correct wording for this particular case is actually something like "An exposed provenance is always considered to exist for any region of memory which is outside the control of the Rust Abstract Machine".

If we don't want provenances to be "for" memory it's possible to rephrase that to include something about "an exposed provenance that permits access to <the specific region of memory in question that's outside the AM>", but it would involve a lot of grammar juggling and probably yield a much less legible sentence in order to not make it sound ambiguously like it might be a single provenance that can access all such memory, which is probably not the model of access permissions that we want.

[RalfJung]

a single provenance that can access all such memory, which is probably not the model of access permissions that we want.

Indeed, a single provenance can only cover a contiguous chunk of memory so there can't be a one-size-fits-all provenance for all outside memory.