Native TypeId in Verus — a motivating example

This accompanies a pull request adding type_id::<T>() to Verus: a spec-level map from each type to a unique identity. This example exists to show what that map is for.

The target code

Consider a downcast on a type-erased handle for a frame. This code is from Asterinas, but don't worry about understanding Frame in detail; we will move on to a simplified version:

impl<M: AnyFrameMeta> TryFrom<Frame<dyn AnyFrameMeta>> for Frame<M> {
    type Error = Frame<dyn AnyFrameMeta>;

    /// Tries converting a [`Frame<dyn AnyFrameMeta>`] into the statically-typed [`Frame`].
    ///
    /// If the usage of the frame is not the same as the expected usage, it will
    /// return the dynamic frame itself as is.
    fn try_from(dyn_frame: Frame<dyn AnyFrameMeta>) -> Result<Self, Self::Error> {
        if (dyn_frame.dyn_meta() as &dyn core::any::Any).is::<M>() {
            // SAFETY: The metadata is coerceable and the struct is transmutable.
            Ok(unsafe { core::mem::transmute::<Frame<dyn AnyFrameMeta>, Frame<M>>(dyn_frame) })
        } else {
            Err(dyn_frame)
        }
    }
}

The transmute is a separate problem. We can justify that the downcast is sound if we can express that the guard implies that dyn_frame actually is a Frame<M>. That reduces to verifying this expression:

(foo as &dyn core::any::Any).is::<F>()

where F implements a trait AnyFoo: Any, and foo is a dyn AnyFoo. An erased value is asked which type it holds, and the answer has to be trustworthy.

Verus does not support core::any::Any. Our approach here is to write our own axiomatization and work around that limitation in our own verification as far as we can. The one thing that cannot be axiomatized from outside is the map from a type to its identity, which our PR supplies.

The Verus branch in the PR is here.

any.rs duplicates the part of the Any interface we need. erase.rs implements into(dyn AnyFoo) for our AnyFoo type. The actual example of AnyFoo and its payoff is in lib.rs.

The expression becomes is::<F>(foo.to_any()), and the payoff is that whole chain F -> dyn AnyFoo -> dyn Any provably retains F's TypeId and cannot be confused with another type:

erase_then_test::<F>	erase with .into(), then show that the type remains the same
discriminate	a FooA erased is not a FooB

discriminate is the key soundness result; it holds because we get type_id::<FooA>() != type_id::<FooB>() for free from the enhanced Verus.

Building

Requires a Verus checkout at ../verus, built with the TypeId support. Then run make.

make verify-cargo goes through the Cargo.toml here instead; make help lists the rest. Point elsewhere with make VERUS_DIR=/path/to/verus.

A residual assumption

type_id::<T>() denotes a core::any::TypeId, whose runtime value is a 128-bit hash, so two distinct types could in principle collide. The assume_specification in vstd/std_specs/any.rs would then be false.

That assumption reaches back to upstream Rust: core::any::Any::downcast is sound only under the same condition.