TypeId in Verus to support Any

ostd/Cargo.toml

@@ -82,6 +82,10 @@ allow_panic = []
 # The guest OS support for Confidential VMs (CVMs), e.g., Intel TDX
 cvm_guest = ["dep:tdx-guest", "dep:iced-x86"]
 coverage = ["minicov"]
+# The erased-metadata downcast (`Frame<dyn AnyFrameMeta>::try_from` and the
+# `AnyFrameMeta` identity methods) rests on Verus type identity; see
+# `patches/README.md`. Off by default so `ostd` still builds on a stock toolchain.
+type_id = ["vstd_extra/type_id"]
 
 [lints]
 workspace = true

ostd/specs/mm/frame/meta_owners.rs

@@ -3,6 +3,10 @@
 //! - The invariants for both MetaSlot and MetaSlotModel.
 //! - The primitives for MetaSlot.
 use vstd::prelude::*;
+#[cfg(feature = "type_id")]
+use vstd_extra::typing::types::Any;
+#[cfg(feature = "type_id")]
+use core::any::TypeId;
 
 use vstd::{atomic::*, cell::pcell_maybe_uninit, simple_pptr::*};
 use vstd_extra::{
@@ -109,6 +113,18 @@ pub enum MetaSlotStorage {
 /// it can then be used to stand in for `dyn AnyFrameMeta`.
 unsafe impl AnyFrameMeta for MetaSlotStorage {
     uninterp spec fn vtable_ptr(&self) -> usize;
+
+    #[cfg(feature = "type_id")]
+    open spec fn meta_id(&self) -> TypeId {
+        type_id::<Self>()
+    }
+
+    #[cfg(feature = "type_id")]
+    fn to_any(&self) -> (r: &dyn Any) {
+        let d: &dyn Any = self;
+        assert(d.type_id_spec() == self.type_id_spec());
+        d
+    }
 }
 
 impl Repr<MetaSlotStorage> for MetaSlotStorage {

ostd/src/mm/frame/linked_list.rs

@@ -4,6 +4,10 @@
 //! This module leverages the customizability of the metadata system (see
 //! [super::meta]) to allow any type of frame to be used in a linked list.
 use vstd::prelude::*;
+#[cfg(feature = "type_id")]
+use vstd_extra::typing::types::Any;
+#[cfg(feature = "type_id")]
+use core::any::TypeId;
 
 use vstd::seq_lib::*;
 use vstd::simple_pptr::*;
@@ -1723,6 +1727,18 @@ impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Link<M> {
 // SAFETY: If `M::on_drop` reads the page using the provided `VmReader`,
 // the safety is upheld by the one who implements `AnyFrameMeta` for `M`.
 unsafe impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> AnyFrameMeta for Link<M> {
+    #[cfg(feature = "type_id")]
+    open spec fn meta_id(&self) -> TypeId {
+        type_id::<Self>()
+    }
+
+    #[cfg(feature = "type_id")]
+    fn to_any(&self) -> (r: &dyn Any) {
+        let d: &dyn Any = self;
+        assert(d.type_id_spec() == self.type_id_spec());
+        d
+    }
+
     open spec fn on_drop_pre(
         &self,
         reader: crate::mm::VmReader<'_, crate::mm::Infallible>,

ostd/src/mm/frame/meta.rs

@@ -84,10 +84,13 @@ use vstd_extra::cast_ptr::{Repr, ReprPtr};
 use vstd_extra::ownership::*;
 use vstd_extra::panic::{may_panic, panic_diverge};
 use vstd_extra::prelude::*;
+#[cfg(feature = "type_id")]
+use vstd_extra::typing::types::Any;
+#[cfg(feature = "type_id")]
+use core::any::TypeId;
 
 use core::{
     alloc::Layout,
-    any::Any,
     cell::UnsafeCell,
     fmt::Debug,
     marker::PhantomData,
@@ -216,7 +219,7 @@ type FrameMetaVtablePtr = core::ptr::DynMetadata<dyn AnyFrameMeta>;
 /// If `on_drop` reads the page using the provided `VmReader`, the
 /// implementer must ensure that the frame is safe to read.
 pub unsafe trait AnyFrameMeta:   /*Any +*/
-Send + Sync {
+Send + Sync + 'static {
     /// Per-impl precondition for [`Self::on_drop`]. Default is `true`.
     /// Impls that need richer caller-side invariants (e.g. the PT-node's
     /// reader/region invariants) override this; the trait method's
@@ -262,6 +265,26 @@ Send + Sync {
     }
 
     spec fn vtable_ptr(&self) -> usize where Self: Sized;
+
+    /// The identity of this metadata's concrete type.
+    ///
+    /// Upstream gets this from `AnyFrameMeta: Any`. We cannot: Verus propagates an
+    /// unsized-blanket-impl rejection from supertrait to subtrait
+    /// (`vir/src/traits.rs`) -- `dyn AnyFrameMeta` would stop being a legal type.
+    #[cfg(feature = "type_id")]
+    spec fn meta_id(&self) -> TypeId;
+
+    /// Mimics the upcast `self as &dyn core::any::Any`.
+    ///
+    /// Upstream writes that upcast directly, which is legal for it because
+    /// `AnyFrameMeta: Any` makes `Any` a supertrait. We make it a method
+    /// instead: each impl performs the *sized* coercion `&Self -> &dyn Any`, which
+    /// is the same operation the vtable would have performed.
+    #[cfg(feature = "type_id")]
+    fn to_any(&self) -> (r: &dyn Any)
+        ensures
+            r.type_id_spec() == self.meta_id(),
+    ;
 }
 
 /*/// Makes a structure usable as a frame metadata.

ostd/src/mm/frame/mod.rs

@@ -31,11 +31,17 @@
 //! can create custom metadata types by implementing the [`AnyFrameMeta`] trait.
 use vstd::atomic::PermissionU64;
 use vstd::prelude::*;
+#[cfg(feature = "type_id")]
+use core::any::TypeId;
 use vstd::simple_pptr::{self, PPtr};
+#[cfg(feature = "type_id")]
+use vstd::std_specs::convert::TryFromSpecImpl;
 use vstd_extra::cast_ptr::*;
 use vstd_extra::drop_tracking::*;
 use vstd_extra::ownership::*;
 use vstd_extra::panic::may_panic;
+#[cfg(feature = "type_id")]
+use vstd_extra::typing::types::{Any, is_};
 
 pub mod allocator;
 pub mod linked_list;
@@ -380,13 +386,6 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Frame<M> {
         PAGE_SIZE
     }
 
-    /*    /// Gets the dynamically-typed metadata of this frame.
-    ///
-    /// If the type is known at compile time, use [`Frame::meta`] instead.
-    pub fn dyn_meta(&self) -> FrameMeta {
-        // SAFETY: The metadata is initialized and valid.
-        unsafe { &*self.slot().dyn_meta_ptr() }
-    }*/
     /// Gets the reference count of the frame.
     ///
     /// It returns the number of all references to the frame, including all the
@@ -747,36 +746,105 @@ impl<M: ?Sized> Drop for Frame<M> {
     }
 }
 
-/*
+verus! {
+
+#[cfg(feature = "type_id")]
+/// Identity of an erased frame's metadata.
+///
+/// A separate impl block because the surrounding one is bounded by
+/// `Repr<MetaSlotStorage>`, which `dyn AnyFrameMeta` does not satisfy -- and it is
+/// exactly the erased case these two are for.
+impl Frame<dyn AnyFrameMeta> {
+    /// The identity of the metadata this frame's slot holds.
+    ///
+    /// Uninterpreted, and a property of the *slot's contents* rather than of the
+    /// handle: the frame is a pointer, and which metadata type lives behind it is
+    /// not recoverable from the pointer alone. It is pinned at the point of
+    /// erasure, by [`Frame::into_dyn`], and read back by [`Self::dyn_meta`].
+    pub uninterp spec fn meta_type_id(&self) -> TypeId;
+
+    /// Gets the dynamically-typed metadata of this frame.
+    ///
+    /// If the type is known at compile time, use [`Frame::meta`] instead.
+    ///
+    /// `external_body` until we handle the vtable pointer again.
+    #[verifier::external_body]
+    pub fn dyn_meta(&self) -> (r: &dyn AnyFrameMeta)
+        ensures
+            r.meta_id() == self.meta_type_id(),
+    {
+        unimplemented!()
+    }
+}
+
+/// The transmute half of the downcast.
+#[verifier::external_body]
+pub fn transmute_frame_to_typed<M: AnyFrameMeta>(dyn_frame: Frame<dyn AnyFrameMeta>)
+-> (r: Frame<M>)
+    ensures
+        r.ptr == dyn_frame.ptr,
+{
+    // SAFETY: The metadata is coerceable and the struct is transmutable.
+    unsafe { core::mem::transmute::<Frame<dyn AnyFrameMeta>, Frame<M>>(dyn_frame) }
+}
 
+#[cfg(feature = "type_id")]
+impl<M: AnyFrameMeta> TryFromSpecImpl<Frame<dyn AnyFrameMeta>> for Frame<M> {
+    open spec fn obeys_try_from_spec() -> bool {
+        true
+    }
+
+    open spec fn try_from_spec(v: Frame<dyn AnyFrameMeta>) -> Result<Self, Self::Error> {
+        if v.meta_type_id() == type_id::<M>() {
+            Ok(Frame { ptr: v.ptr, _marker: PhantomData })
+        } else {
+            Err(v)
+        }
+    }
+}
+
+#[cfg(feature = "type_id")]
 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) })
+    ///
+    /// Upstream tests with
+    ///
+    /// ```text
+    /// if (dyn_frame.dyn_meta() as &dyn core::any::Any).is::<M>() {
+    /// ```
+    ///
+    /// In our code the upcast is a method, [`AnyFrameMeta::to_any`]. Each impl
+    /// performs the coercion `&Self -> &dyn Any`, which Verus does model.
+    /// `is_` is then the same `is` upstream calls.
+    ///
+    /// For now, `transmute_frame_to_typed` stands in for an axiomatized `transmute`
+    /// function. Axiomatizing `transmute` is a separate task.
+    fn try_from(dyn_frame: Frame<dyn AnyFrameMeta>) -> (res: Result<Self, Self::Error>) {
+        if is_::<M>(dyn_frame.dyn_meta().to_any()) {
+            Ok(transmute_frame_to_typed::<M>(dyn_frame))
         } else {
             Err(dyn_frame)
         }
     }
-}*/
+}
 
+}  // verus!
 /*impl<M: AnyFrameMeta> From<UFrame> for Frame<M> {
     fn from(frame: UFrame) -> Self {
         // SAFETY: The metadata is coerceable and the struct is transmutable.
         unsafe { core::mem::transmute(frame) }
     }
 }*/
-
 /*impl TryFrom<Frame<FrameMeta>> for UFrame {
     type Error = Frame<FrameMeta>;
 }*/
 
+
 #[verifier::external]
 impl<M: AnyUFrameMeta> From<Frame<M>> for UFrame {
     fn from(frame: Frame<M>) -> Self {
@@ -918,13 +986,34 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + 'static> Frame<M> {
     ///
     /// Axiomatized (`external_body`) because the body is `transmute`, which
     /// Verus has no built-in spec for.
+    ///
+    /// Two versions, differing only in strength. `type_id` adds the clause that
+    /// pins the erased frame's identity, which is what makes the downcast in
+    /// [`TryFrom`] able to conclude anything; without the feature the frame still
+    /// erases, it just carries no recoverable identity. The runtime behaviour is
+    /// identical -- one `transmute` either way.
+    #[cfg(feature = "type_id")]
     #[verifier::external_body]
-    pub fn into_dyn(self) -> Frame<dyn AnyFrameMeta> {
+    pub fn into_dyn(self) -> (r: Frame<dyn AnyFrameMeta>)
+        ensures
+            r.ptr == self.ptr,
+            r.meta_type_id() == type_id::<M>(),
+    {
         // SAFETY: `Frame<M>` is `#[repr(transparent)]` over `PPtr<MetaSlot>`
         // plus a zero-size `PhantomData<M>`. `Frame<dyn AnyFrameMeta>` has
         // the same runtime layout (thin pointer + ZST phantom).
         unsafe { core::mem::transmute(self) }
     }
+
+    #[cfg(not(feature = "type_id"))]
+    #[verifier::external_body]
+    pub fn into_dyn(self) -> (r: Frame<dyn AnyFrameMeta>)
+        ensures
+            r.ptr == self.ptr,
+    {
+        // SAFETY: as above.
+        unsafe { core::mem::transmute(self) }
+    }
 }
 
 } // verus!

ostd/src/mm/page_table/node/mod.rs

@@ -37,6 +37,10 @@ pub use entry::*;
 
 use vstd::cell::pcell_maybe_uninit;
 use vstd::prelude::*;
+#[cfg(feature = "type_id")]
+use vstd_extra::typing::types::Any;
+#[cfg(feature = "type_id")]
+use core::any::TypeId;
 
 use vstd::atomic::PAtomicU8;
 use vstd_extra::array_ptr;
@@ -116,6 +120,18 @@ pub struct PageTablePageMeta<C: PageTableConfig> {
 pub type PageTableNode<C> = Frame<PageTablePageMeta<C>>;
 
 unsafe impl<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C> {
+    #[cfg(feature = "type_id")]
+    open spec fn meta_id(&self) -> TypeId {
+        type_id::<Self>()
+    }
+
+    #[cfg(feature = "type_id")]
+    fn to_any(&self) -> (r: &dyn Any) {
+        let d: &dyn Any = self;
+        assert(d.type_id_spec() == self.type_id_spec());
+        d
+    }
+
     /// Caller invariants the PT-node `on_drop` body relies on:
     /// - Reader well-formedness + `vm_io_owner` matching + read view
     ///   initialized + at least `PAGE_SIZE` bytes remaining for the