Ghostly DSTs

[jaybosamiya]

Since Ghost<T> has no execution-time impact, it is zero-sized. It thus seems silly that we currently require T: Sized (or more specifically, we don't explicitly say T: ?Sized, which would allow for T to also be a Dynamically Sized Type (aka DST), in addition to regular sized types).

Why we care about DSTs

Sometimes, when writing traits, we might wish to do things like returning a Ghost<Self>. This is currently disallowed unless you declare the trait's supertrait to be Sized (i.e., the trait in question can only be applied to sized types). This adds a tiny syntactic burden, and also (somewhat) reduces the situations where the trait itself could be applied (although not by all that much).

For example,

  trait Foo {
    fn foo(&self) -> Ghost<Self>;
  }

does not work, requiring either:

  trait Foo : Sized {
    fn foo(&self) -> Ghost<Self>;
  }

or

  trait Foo {
    fn foo(&self) -> Ghost<Self>
      where Self: Sized; // equivalent to above in this case, but useful if you just want to
                         // restrict a single function but not all
  }

When do DSTs come into play?

From the nomicon:

There are two major DSTs exposed by the language:

• trait objects: dyn MyTrait
• slices: [T], str, and others

There can also be custom DSTs (i.e., user-defined types that are also DSTs), but

(Yes, custom DSTs are a largely half-baked feature for now.)

Notice that none of these types are types that are ever really referred to directly. They are often used via either a reference, or a Box<_> or such. Also, note that something like Vec<T> is not a DST, since the Vec<T>'s size is known at compile-time, it is only its pointee (i.e., backing store on the heap for the members of the Vec<T>) that is a DST. Thus, for the most part, people don't ever need to worry about DSTs. There is a reason DSTs are considered "Exotically Sized Types".

How should Verus handle them?

Here, we're talking only about ghostly contexts (so in particular, DSTs in exec contexts should behave as they do in Rust).

Alternative 1 (Change Nothing)

We can keep the current implementation as is. This has the advantage of requiring no changes to Verus, but requires users of Verus to be aware of this tiny edge case whenever they define a trait that might have things like Ghost<Self>. The error message provided is somewhat useful anyways, and at least points to one of the solutions:

error[E0277]: the size for values of type `Self` cannot be known at compilation time
   --> .../src/main.rs:23:22
    |
23  |     fn foo(&self) -> Ghost<Self>;
    |                      ^^^^^^^^^^^ doesn't have a size known at compile-time
    |
note: required by a bound in `builtin::Ghost`
   --> .../verus/source/builtin/src/lib.rs:238:49
    |
238 | pub struct Ghost<#[verifier(strictly_positive)] A> {
    |                                                 ^ required by this bound in `builtin::Ghost`
help: consider further restricting `Self`
    |
23  |     fn foo(&self) -> Ghost<Self> where Self: std::marker::Sized;
    |                                  ++++++++++++++++++++++++++++++

A minor alteration to this alternative would be to provide a more Verus-specific diagnostic.

Alternative 2 (Questionably Sized Ghosts)

We could introduce the : ?Sized constraint to the definition of Ghost<_>:

- pub struct Ghost<#[verifier(strictly_positive)] A> {
+ pub struct Ghost<#[verifier(strictly_positive)] A: ?Sized> {

The advantage to this is that we'd no longer have the seemingly-silly restriction on what types can be inside a Ghost<_>. It does carry a non-trivial number of downsides immediately though, largely due to how .view() behaves. In particular, the current implementation of view() for Ghost<_> looks like:

    #[spec]
    pub fn view(self) -> A {
        unimplemented!()
    }

This means that A is exposed without anything to constrain its size. It doesn't matter that this can only be invoked in spec contexts. It means that if we want A to be possibly-unsized, we either need this function to return &A (either via &'static A or introducing a new lifetime, via fn view<'a>(self) -> &'a A; I believe both would behave relatively similarly, since we can only invoke this in spec contexts), or need it to return a Box<A> or similar, so that we aren't unnecessarily having to manage lifetimes here.

Changing this return type itself is not too much of an issue, so @utaal and I began an experiment into this on unsized_ghost, but one soon run into issues.

Specifically, the issues arise from the fact deref coercions happen only in very specific cicumstances. For example, if you tried to do x@@ where x: Ghost<Ghost<T>>, then the first @'s returned & would be coerced away, but the second wouldn't, leading you to receive a &T. This again by itself is not an issue, but if (say) you had a comparison that looked like foobar == (y@, true), then either foobar needs to have already accounted for this & that would not be coerced away, or would require one to change things to foobar == (*(y@), true) which seems to kinda break the point of even having a convenient postfix @.

This leads to multiple decisions that could be taken along the way:

Alternative 2.1

Let users deal with having to work with the added &. This is not ideal.

Alternative 2.2

Have @ perform the dereference for us. Since we control the syntax, this is feasible to do. Indeed, this is experimented with on the same branch. Unfortunately, since this is syntactic, we don't yet know if we are applying it specifically to a Ghost or to a different type, which means that we need to update all the view() functions in the codebase to return references, instead of raw types (this too has been updated in the code).

Unfortunately, this doesn't immediately and easily fix the issue, and starts requiring a lot more fixes at a non-trivial number of locations. While this is doable, this feels like a very heavy-weight fix, and requires a lot more management of references for users.

Alternative 2.3

Instead of using &, use Box; turns out this hits the same sorts of problems as Alternatives 2.1 and 2.2.

Alternative 3 (Allow DSTs in spec contexts)

This is kinda like Alternative 2, but improved user experience.

The reason we are forced to add the & or Box in Alternative 2 is because we can't have DSTs are bare types. However, the only situations where we might want bare DSTs are only in spec contexts. Thus, we could disable the Sized checking for spec contexts. Not sure how easy/difficult this would be. I don't believe this could introduce any soundness issues, but at the same time, I am not 100% sure.

Alternative 4 (Verus Traits are Sized by default)

Since DSTs are rare, and these sorts of restrictions come up largely only in the context of traits, one fix is to have traits (ones defined inside the verus!{} macro) behave similar to how polymorphic types/functions in Rust behave, i.e., assume Sized by default, requiring ?Sized to explicitly be specified if it needs to support DSTs.

For the most part, DSTs are exotic, and are very rare, and we don't actually expect normal traits to have to support DSTs, and if we expect most users of traits in Verus to add the : Sized declaration anyways, then this approach makes it easier for users, while still allowing power users (more specifically, the even smaller subset of power users who really want to work with DSTs) to get access to DSTs for their traits.

Alternative X (something I missed)

Please suggest others if I missed something

---

Personal Thoughts on the Alternatives

Alternative 1 (Change Nothing): I think many users might be willing to live with it, but it feels unsatisfying to force most users to introduce : Sized to their traits (yes, writing new traits is not the most common operation, but this is still a footgun).

Alternative 2 (Questionably Sized Ghosts): After having spent some time trying to implement this and get it working, I think this changes things up too drastically from what we're used to. More importantly, this feels like the cure is worse than the disease: requring that folks deal with &/Box in many places just so they don't have to add a : Sized once in a while feels like a bad tradeoff.

Alternative 3 (Allow DSTs in spec contexts): This might be the best alternative for users overall, but especially with the pending move away from the Rust fork, I don't know how feasible this one might be. Also, I am somewhat worried about longer-term maintainability, but maybe this is simpler/easier than I am thinking?

Alternative 4 (Verus Traits are Sized by default): This is the option I like the most. It is only flipping the defaults for a very rare and exotic feature, and one that is arguably not even seriously being used yet (and one where most regular users are going to pick adding a :Sized as a supertrait more often than not). It does move away from Rust defaults, but only does so inside the macro, and has a fairly obvious diagnostic that would be triggered for anyone trying to use such a un-annotated trait on a DST. Thus, I think it helps maintain a good user experience, while also requiring relatively minor changes and maintenance.

[tjhance]

For record's sake, I will link this old PR here, though it's unlikely to go anywhere: #792