copy & recursion checking

[tjhance]

I don't think this is a real issue right now, but more like something to be wary of?

Consider a (trusted) type like the following. We introduce a IsCopyable trait where the user duplicates a ghost object and then use this trait as a trait bound in the copy impl: impl<T: IsCopyable> Copy for CopyContainer<T> { }.

This is just a hypothetical type (and actually there a couple of dubious things about it, like the fact that it uses (Self) -> (Self, Self) rather than &self -> Self but it's not really material to the discussion). Realistically, I think the place we'd be most likely to add something like this would have to do with the pcm ghost state stuff.

Anyway, the point is that you can imagine someone wanting to add a type that's more or less like this, with a nontrivial trait bound in the Copy impl.

trait IsCopyable : Sized {
    proof fn make_copy(tracked self) -> (tracked res: (Self, Self))
        ensures self == res.0 && self == res.1;
}

#[verifier::external_body]
#[verifier::reject_recursive_types_in_ground_variants(T)]
tracked struct CopyContainer<T> { t: core::marker::PhantomData<T> }

impl<T: IsCopyable> Clone for CopyContainer<T> {
    #[verifier::external_body]
    fn clone(&self) -> Self {
        CopyContainer { t: core::marker::PhantomData }
    }
}

impl<T: IsCopyable> Copy for CopyContainer<T> { }

impl<T> CopyContainer<T> {
    #[verifier::external_body]
    proof fn new(tracked t: T) -> (tracked res: CopyContainer<T>)
        ensures res.view() == t
    {
        unimplemented!();
    }

    #[verifier::external_body]
    proof fn into_inner(tracked self) -> (tracked res: T)
        ensures self.view() == res
    {
        unimplemented!();
    }

    spec fn view(&self) -> T;
}

However, there's a problematic case:

// Introduce some random ghost type that isn't allowed to be copied:

#[verifier::external_body]
tracked struct Excl { }

#[verifier::external_body]
proof fn new_excl() -> (tracked res: Excl) {
    unimplemented!();
}

#[verifier::external_body]
proof fn no_two_excl(e1: Excl, e2: Excl)
    requires e1 == e2
    ensures false
{ }

// Now we can implement Copy 

impl IsCopyable for Excl {
    proof fn make_copy(tracked self) -> (tracked res: (Self, Self))
    {
        let tracked cc = CopyContainer::new(self);

        // We perform a copy here:
        let tracked cc2 = cc;

        (cc.into_inner(), cc2.into_inner())
    }
}

proof fn contradiction() {
    let tracked excl = new_excl();
    let tracked (e1, e2) = Excl::make_copy(excl);
    no_two_excl(e1, e2);
    assert(false);
}

In this case, the copy that occurs on the line // We perform a copy here implicitly depends on the Excl: IsCopyable trait bound. Thus we have a cycle.

Right now:

• Rust->VIR ignores all copies so this implicit bound would be ignored, and this cycle wouldn't be caught.
• It also happens that our lifetime checking doesn't use for the Copy bound anyway, which might be a separate bug?

So, should we find every copy and add any implied bounds to recursion checking? Or should we say that a type like the CopyContainer is unsound and shouldn't be written? If the latter, is there a safeguard we can add to prevent users from accidentally writing trusted types like this?