Specs for raw pointers & ghost ownership for pointers

[Armael]

I'm extracting extern specs for basic raw pointer operations (mainly getting their address and comparing with null) from ghost_ptr.rs because I need them in another context. (cc @dewert99)

In the process I went and skimmed the docs (https://doc.rust-lang.org/std/ptr/index.html and https://doc.rust-lang.org/std/primitive.pointer.html) and I ended up with a more conservative model of raw pointers than ghost_ptr.rs, where pointers always have some hidden "metadata" associated, and one basically can never logically deduce equality of pointers except by calling ==.

I have two questions:

• does this seem too conservative (ie not expressive enough)? Glancing at the docs I could tell if there could be a more precise yet reasonable model.
• the specs currently do not say anything about == (there is no DeepModel instance in particular). I would like to say that the DeepModel of a *mut T is "itself" (and we know nothing more), and that if p == q returns true then we know that p = q in the logic and also p.addr_logic() = q.addr_logic(). What do I need to write to express that in Creusot?

If the current approach seems OK then I'll have a go at updating ghost_ptr.rs to use the new model.

[xldenis]

. I would like to say that the DeepModel of a *mut T is "itself" (and we know nothing more), and that if p == q returns true then we know that p = q in the logic and also p.addr_logic() = q.addr_logic(). What do I need to write to express that in Creusot?

This sounds like a spec on == no? As it is, the specification of == says that result ==> p.deep_model() == q.deep_model(), you can then also add that the addresses must be the same.

Is it true that p.addr_logic() == q.addr_logic() ==> p = q?

[Armael]

Is it true that p.addr_logic() == q.addr_logic() ==> p = q?

no! that's precisely what we want to avoid

[xldenis]

no! that's precisely what we want to avoid

Ah right, addr_logic doesn't include provenance.

[jhjourdan]

I would like to say that the DeepModel of a *mut T is "itself"

But then that would mean that program equality implies equality of provenance, which is wrong?

[Armael]

Indeed... I'll push an updated version later.

[jhjourdan]

As for the DeepModel impl for pointers, I don't know what to say: metadata should be taken into account, but we cannot say that the pointer is only the address and the metadata, because of provenance.

We could have an instance for Sized types only?

@xldenis : is it possible to have two pointer of equal address and underlying types, but without the same metadata.

[jhjourdan]

Suggested change

	#[ensures(result.addr_logic() == 0)]
	#[ensures(result == Self::null_logic())]

Otherwise, null_logic should be removed.

[Armael]

this is not sound wrt the existence of multiple nulls. We could remove Self::null_logic() if it's too tempting to incorrectly use it to test nullity (instead of .is_null_logic()). In principle, null_logic() gives you the ability to talk about "a null pointer" in the logic, but I don't know how useful that is...

[jhjourdan]

What is not sound is to assume that all the null types are equal. This is not what I am proposing here.

What I am proposing is essentially to assume that the null function is deterministic (it always returns the same value). I am not completely sure, but this seems very reasonable.

Now, you may argue that this is useless, which I may agree on. But if we do not add this post-condition, then we should remove null_logic, because I think this is useless too.

[Armael]

Indeed, I agree. To sum things up, there are two choices:

• keep Self::null_logic() and specify that it is equal to the result of the null() program function (thus specifying that null() is deterministic;
• remove Self::null_logic and only use is_null() / compare addr_logic() to 0.

I'm leaning towards option 2, because having a logical NULL is not so useful and gives the wrong idea (that there is only one NULL pointer). Using is_null instead of comparing to NULL is the better option.

[jhjourdan]

Makes sense, and this does not prevent us from adding this in the future.

[Armael]

I pushed changes implementing Option 2, with an additional helper function is_null_logic() which simply unfolds to .addr_logic() == 0. (I found this convenient in practice because it mirrors is_null() in program code.)

[arnaudgolfouse]

@xldenis : is it possible to have two pointer of equal address and underlying types, but without the same metadata.

I think so:

let s1: &[i32] = &[1];
let s2: &[i32] = &s1[..0];
let p1: *const [i32] = s1;
let p2: *const [i32] = s2;

p1 and p2 are the same pointer, and have the same type, but their metadata is different (1 vs 0).

[jhjourdan]

Well, obviously...

[Armael]

Soundly updating the specifications in ghost_ptr.rs without reintroducing addr = addr ==> ptr = ptr doesn't seem so obvious...
One way would be to first introduce a new module for a single pointer with ghost ownership, and use it to implement ghost_ptr.rs (which defines a map -- or region -- of pointers).

[Armael]

Ah, and note (in the current version of the PR) how I've tried to handle DeepModel: by choosing a DeepModelTy composed of the address and a private "runtime metadata" about which we know nothing. (Conceptually, a pointer would then be composed of three things: its address, runtime metadata, and other metadata not tested by the equality (e.g. provenance))

[jhjourdan]

You changes look good!

[Armael]

I've now added a ptr_own library that provides "ghost ownership tokens" for raw pointers, and a linked-list example that illustrate their use.
The previous ghost_ptr module has been removed. It predated ghost code and provided a notion of ghost ownership for a region of memory; this should be doable now by simply storing PtrOwn tokens in a ghost FMap.

[Armael]

@dewert99 as a heads up, this PR (which evolved to include a new module for "ghost ownership tokens" for pointers) removes your ghost_ptr module. The idea is that the functionality provided by ghost_ptr should still be possible by combining simpler building blocks: the ptr_own module from this PR (which provides ghost tokens for the ownership of a single pointer), the ghost mechanism recently added to creusot (with GhostBox<T> and ghost!{} blocks), and FMap (which can now be used in ghost code and be used to store ghost tokens to represent ownership over a memory region).

I don't know if you were still using ghost_ptr, but if so I'm happy to help if it turns out it's not easy to port the code to the new primitives introduced here.

[arnaudgolfouse]

Why are ZST unsupported? Is this because the address of two ZST objects are always the same or something like that?

[Armael]

That's a good question, I don't know; I took the assert from ghost_ptr (cc @dewert99 ?).
Could there be issues with using Box::{into,from}_raw on ZSTs maybe?

[jhjourdan]

The problem is that if you call Box::new on a ZST several times, you get the same pointer in the end. So the tokens are not unique.

struct ZST {}

fn p_of_mut<T>(p: &mut T) -> *mut T {
    p
}

fn main() {
    
    let mut b1 = Box::new(ZST{});
    let mut b2 = Box::new(ZST{});
    
    let b1p : *mut ZST = p_of_mut(&mut *b1);
    let b2p : *mut ZST = p_of_mut(&mut *b2);
    
    eprintln!("{b1p:?} {b2p:?}")
}

The example above prints "0x1 0x1".

We should add as a pre-condition the fact that the underlying value is not a ZST, but there is noway to do that currently in Creusot (I think).

[Armael]

could it be achieved using a const failure (instead of a dynamic one)?

[jhjourdan]

If T is not Sized, then this is dynamic information only.

[Armael]

Thanks for the review!
I've addressed the easy changes, and I've moved the functions in ptr_own to be associated functions of PtrOwn as discussed with @arnaudgolfouse .

I'm not sure what to do regarding the ZST-related assert, but I'd rather merge this now and remove the assert later if it is needed and sound.

[jhjourdan]

I'm not sure what to do regarding the ZST-related assert, but I'd rather merge this now and remove the assert later if it is needed and sound.

It is indeed needed (see above), and the current situation is "unsound" (Creusot is supposed to prevent panics). Butfixing this would require reasonning about the size of a value pointed to by a Box, which we don't do currently. (That's probably not very difficult to add, but this requires some design decisions, etc...).