Any-style dynamic downcasts

[SNoAnd]

This PR introduces two related structures: a trait mechanism representing a collection of distinct types, distinguished by an abstract type_id; and an implementation as a fixed-size array of bytes with the type_id tracked as a ghost variable (GhostTaggedArray).

This allows us to:

• represent the byte array in MetaSlot with an object that is binary-equivalent, as opposed to MetaSlotStorage, which carries an extra tag to distinguish its contents
• up- and down-cast to and from dyn AnyFrameMeta soundly
• prove that write_meta preserves the proper relationship between the metadata type as seen by the compiler, the type's bit-pattern, and vtable_ptr

An alternative approach would be to modify Verus to expose its internal typeIds to the verification. Then we could do away with the complex trait system, but keep the underling ghost-tagged-array representation.