ghost!{e} requires e to be Sized

[Armael]

A limitation of the current implementation of ghost!{e} is that it requires e to be Sized.
After talking with @arnaudgolfouse this is because it desugars into || GhostBox::new(e), which entails that e must be Sized since it is passed as an argument to a function.

In principle, it would be nice to also support patterns of the form:

let x : GhostBox<[u8]> = ghost!{ [] };

which are possible with the normal Box.

[xldenis]

which are possible with the normal Box.

Box is a magic type, we may not be able to copy its api as is

[jhjourdan]

Box::new(x) with x unsized is illegal as well in Rust. Apart from subtle exceptions (usually unstable extensions), unsized types can only by manipulated through pointers.

Why would we want to manipulate unsized objects in ghost code? In the example you are mentioning, you use a slice, a Rust executable concept, while a sequence, a Creusot ghost concept could do the job. Perhaps the problem is that we don't have sequence litterals, which we should add somehow.

(As we discussed recently, the name GhostBox is somewhat misleading, because this it seems to indicate that this is a pointer, while it is not. Perhaps we should change its name.)

[arnaudgolfouse]

Box::new(x) with x unsized is illegal as well in Rust. Apart from subtle exceptions (usually unstable extensions), unsized types can only by manipulated through pointers.

This is true, but Box<T> can be cast to Box<UnsizedT> in some cases, like Box<[u8; N]> to Box<[u8]>.

(As we discussed recently, the name GhostBox is somewhat misleading, because this it seems to indicate that this is a pointer, while it is not. Perhaps we should change its name.)

true... @Armael then if you really want to manipulate unsized data, you can wrap it in a Box. I think the motivation was pointer permissions, like

#[trusted]
fn into_raw_ptr<T>(p: Box<T>) -> (*mut T, GhostBox<PtrOwn<T>>) {
    (Box::into_raw(p), ghost!(panic!()))
}

In this case, if PtrOwn<T> itself contains a Box<T> and not a T, the bound can be relaxed to T: ?Sized.

[Armael]

In this case, if PtrOwn itself contains a Box and not a T, the bound can be relaxed to T: ?Sized.

OK, that's a good trick indeed.

Why would we want to manipulate unsized objects in ghost code?

But why should we restrict Ghost code to only contain Sized objects? Ghost values don't exist at runtime anyway, so I don't see why sizedness should matter.

As @arnaudgolfouse mentions, the question came up when designing an API that provides a ghost token PtrOwn<T> representing the ownership over a value T, originally contained in a Box. To make the API as general as possible, T should be allowed to be unsized, and I couldn't see why GhostBox would be limited to contain Sized data. (Ignoring implementation constrains, I think GhostBox should be as easy to use as possible and thus as general as possible.)

For into_raw_ptr specifically, I agree that it makes sense for PtrOwn<T> to contain a Box<T> and not a T, which addresses the sizedness issue.

To be clear, I'm not against requiring GhostBox to only deal with Sized data, but then I'd like to understand whether that would be for implementation reasons (it is too difficult/cumbersome to make it work with unsized data), or for design reasons (that I don't understand yet).