notes about variance

[tjhance]

I started looking into the subject of variance. In Rust, Rc<T> is covariant in T. (That means if T is a subtype of U then Rc<T> is a subtype of Rc<U>. This is mostly relevant for lifetimes.)

However, in Verus, Rc is implemented as follows:

tracked struct GhostStuff<S> {
    pub tracked rc_perm: cell::PointsTo<u64>,
    pub tracked rc_token: RefCounter::counter<MemPerms<S>>,
}

struct_with_invariants!{
    struct MyRc<S> {
        pub inst: Tracked< RefCounter::Instance<MemPerms<S>> >,
        pub inv: Tracked< Duplicable<LocalInvariant<_, GhostStuff<S>, _>> >,
        pub reader: Tracked< RefCounter::reader<MemPerms<S>> >,

        pub ptr: PPtr<InnerRc<S>>,

        pub rc_cell: Ghost< PCell<u64> >,
    }

When all's said and done, this implementation results in MyRc<S> being nonvariant in S.

How can we fix this? Well, let's enumerate the issues:

• GhostStuff<S> needs to take the S parameter to pass it to RefCounter::counter, but RefCounter::counter really only stores an integer value. If our tokenized_state_machine was more precise, we could remove this type parameter.
• RefCounter::reader<MemPerms<S>> is a similar problem, but in this case, we can't remove the type parameter. However, I think in principle, I think the tokenizer could make RefCounter::reader covariant.
• Funnily enough, the biggest issue is RefCounter::Instance<MemPerms<S>>. The Instance things usually aren't a problem, but in this case, it's important that the Instance is nonvariant in its type parameter.

However, I think we might be able to fix the last problem with proof_fn ... Rather than holding onto an 'instance', we could hold onto proof functions that do all the things we would have used the instance to do. However... for what I have in mind to work, these proof fns would need to have type signatures like for<T> (&RefCounter::reader<T>) -> RefCounter::reader<T>. Now, Rust doesn't have for <T>, but I think you could do some junk with trait generics and dyn?

For this to work, we also need to generalize the tokenization operations. For example, right now the tokenizer generates do_clone like this:

do_clone(&RefCounter::Instance<T>, &RefCounter::reader<T>) -> &RefCounter::reader<T>
and we actually need:
do_clone(&RefCounter::Instance<T>, &RefCounter::reader<U>) -> &RefCounter::reader<U>

which definitely seems weird, but would in principle be totally sound. I'm pretty sure. It woudl take some care to figure out how to generate stuff that looks like this, but I think if we free our minds and think dependent-typed-ly and treat type arguments like any other argument in the tokenization process, then the right rules will basically fall out. It just might be hard to figure out the right way to express things in Rust's type system.