TypeId in Verus to support Any

[SNoAnd]

This PR won't run on stock Verus. In order to run it, first apply patches/0001-verus-type-identity.patch to the Verus tree. That patch adds a TypeIdSpec type to Verus, such that each registered type in the program receives a unique ID. We then consume that ID in the Any trait, which exposes it as an exec object. The payoff can be seen in Frame<dyn AnyFrameMeta>::try_from, which casts the meta up to an Any and then checks its type ID and casts it down to the target type if correct.

One remaining gap in this setup is the up-cast. In Rust it is allowed as a normal cast, because AnyFrameMeta: Any. Verus forbids using user-defined traits as supertraits of traits that will have dyn usage. The current approach is to put the equivalent method in AnyFrameMeta.

[rikosellic]

There seems to be a dependency issue.

[SNoAnd]

Yes, the patch was outdated. I've updated it.

[rikosellic]

@SNoAnd Maybe you can create a new branch in asterinas/verus? Then it will be easier to maintain, and it is natural to contribute to verus/verus. It is easy to switch between branches through cargo dv bootstrap --upgrade --branch <branch_name>

[rikosellic]

BTW, can we try to create a PR to get feedback from the Verus team? This is a big change and I'm not very confident.