Basic support for dyn

[Chris-Hawblitzel]

This implements the type dyn T for trait T, following the design from #1047 (made much easier thanks to #1529 ). In particular, it extends the existing Rust "dyn compatibility" with rules for proof functions and spec functions, as described in #1047:

• proof functions must either be explicitly non-dispatchable or have a tracked self
• spec functions must either be explicitly non-dispatchable or have no ensures clauses

This pull request doesn't support additional auto traits like dyn T + Send + Sync; I want to leave this for later in order to look into our handling of Send, Sync, etc. first. (It's important for trait dispatch that dyn T + Send + Sync have a different type id from dyn T, for example.)

dyn T is implemented at the AIR level as Poly, with a new unsized decoration $dyn, a type id DYN%T, and coercion to_dyn%T from values to dyn T values. For example, for:

trait T {
    spec fn f(&self, i: int) -> int;
}
impl T for u8 {
    spec fn f(&self, i: int) -> int { 3 }
}

this AIR is generated if dyn T is reachable after pruning:

(declare-const DYN%scratch!T. Type)
(declare-fun to_dyn%scratch!T. (Dcr Type Poly) Poly)

(axiom (forall ((self! Poly) (i! Poly)) (!
   (=
    (T.f.? $dyn DYN%T. (to_dyn%T. $ (UINT 8) self!) i!)
    (T.f.? $ (UINT 8) self! i!)
   )
   :pattern ((T.f.? $dyn DYN%T. (to_dyn%T. $ (UINT 8) self!) i!))
)))

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[tjhance]

What's your plan for dealing with the coherence issue with blanket impls? (rust issue 57893)? Will the trait-conflict-checker catch any issues?

[Chris-Hawblitzel]

What's your plan for dealing with the coherence issue with blanket impls? (rust issue 57893)? Will the trait-conflict-checker catch any issues?

Right now, the pull request prohibits this up front. Any trait T with a blanket impl for an unsized type parameter gets marked DynCompatible::RejectUnsizedBlanketImpl and is rejected if the user tries to use dyn T, with the message "Verus disallows dyn for trait T because it has an unsized blanket impl (see rust-lang/rust#57893 )".

[tjhance]

I think those aren't the only problematic cases, e.g., we have this example from this comment:

trait TraitA { type Item: ?Sized; }

trait TraitB<T> { }

impl<X: TraitA> TraitB<X> for X::Item { }

impl TraitA for () {
    type Item = dyn TraitB<()>;
}

[Chris-Hawblitzel]

trait TraitA { type Item: ?Sized; }

trait TraitB<T> { }

impl<X: TraitA> TraitB<X> for X::Item { }

impl TraitA for () {
    type Item = dyn TraitB<()>;
}

Ok, I updated trait_conflicts.rs to check for rust-lang/rust#57893 in general. The obvious blanket impl still gets checked by well_formed.rs up front, but more obscure cases get caught in trait_conflicts.rs. This also includes some improvements to make trait_conflicts.rs more precise about sized structs.