diff --git a/Cargo.lock b/Cargo.lock index 92c2f90e6..161263497 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -599,7 +599,7 @@ version = "0.0.0-2026-08-09-0044" [[package]] name = "verus_builtin_macros" -version = "0.0.0-2026-08-09-0044" +version = "0.0.0-2026-08-23-0033" dependencies = [ "convert_case", "proc-macro2", @@ -651,7 +651,7 @@ checksum = "af8ca9a5d4debca0633e697c88269395493cebf2e10db21ca2dbde37c1356452" [[package]] name = "vstd" -version = "0.0.0-2026-08-09-0044" +version = "0.0.0-2026-08-23-0033" dependencies = [ "verus_builtin", "verus_builtin_macros", diff --git a/ostd/Cargo.toml b/ostd/Cargo.toml index f1344922b..bcd363b45 100644 --- a/ostd/Cargo.toml +++ b/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::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 diff --git a/ostd/specs/mm/frame/meta_owners.rs b/ostd/specs/mm/frame/meta_owners.rs index 034340f7e..66ced3bf8 100644 --- a/ostd/specs/mm/frame/meta_owners.rs +++ b/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::() + } + + #[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 for MetaSlotStorage { diff --git a/ostd/src/mm/frame/linked_list.rs b/ostd/src/mm/frame/linked_list.rs index abb2cb7e3..486858eec 100644 --- a/ostd/src/mm/frame/linked_list.rs +++ b/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> Link { // 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> AnyFrameMeta for Link { + #[cfg(feature = "type_id")] + open spec fn meta_id(&self) -> TypeId { + type_id::() + } + + #[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>, diff --git a/ostd/src/mm/frame/meta.rs b/ostd/src/mm/frame/meta.rs index 2d07a9a41..a3eba6a21 100644 --- a/ostd/src/mm/frame/meta.rs +++ b/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; /// 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. diff --git a/ostd/src/mm/frame/mod.rs b/ostd/src/mm/frame/mod.rs index c377c9650..0ec8c035d 100644 --- a/ostd/src/mm/frame/mod.rs +++ b/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 + ?Sized> Frame { 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,8 +746,64 @@ impl Drop for Frame { } } -/* +verus! { + +#[cfg(feature = "type_id")] +/// Identity of an erased frame's metadata. +/// +/// A separate impl block because the surrounding one is bounded by +/// `Repr`, which `dyn AnyFrameMeta` does not satisfy -- and it is +/// exactly the erased case these two are for. +impl Frame { + /// 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(dyn_frame: Frame) +-> (r: Frame) + ensures + r.ptr == dyn_frame.ptr, +{ + // SAFETY: The metadata is coerceable and the struct is transmutable. + unsafe { core::mem::transmute::, Frame>(dyn_frame) } +} +#[cfg(feature = "type_id")] +impl TryFromSpecImpl> for Frame { + open spec fn obeys_try_from_spec() -> bool { + true + } + + open spec fn try_from_spec(v: Frame) -> Result { + if v.meta_type_id() == type_id::() { + Ok(Frame { ptr: v.ptr, _marker: PhantomData }) + } else { + Err(v) + } + } +} + +#[cfg(feature = "type_id")] impl TryFrom> for Frame { type Error = Frame; @@ -756,27 +811,40 @@ impl TryFrom> for 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) -> Result { - if (dyn_frame.dyn_meta() as &dyn core::any::Any).is::() { - // SAFETY: The metadata is coerceable and the struct is transmutable. - Ok(unsafe { core::mem::transmute::, Frame>(dyn_frame) }) + /// + /// Upstream tests with + /// + /// ```text + /// if (dyn_frame.dyn_meta() as &dyn core::any::Any).is::() { + /// ``` + /// + /// 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) -> (res: Result) { + if is_::(dyn_frame.dyn_meta().to_any()) { + Ok(transmute_frame_to_typed::(dyn_frame)) } else { Err(dyn_frame) } } -}*/ +} +} // verus! /*impl From for Frame { fn from(frame: UFrame) -> Self { // SAFETY: The metadata is coerceable and the struct is transmutable. unsafe { core::mem::transmute(frame) } } }*/ - /*impl TryFrom> for UFrame { type Error = Frame; }*/ + #[verifier::external] impl From> for UFrame { fn from(frame: Frame) -> Self { @@ -918,13 +986,34 @@ impl + 'static> Frame { /// /// 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 { + pub fn into_dyn(self) -> (r: Frame) + ensures + r.ptr == self.ptr, + r.meta_type_id() == type_id::(), + { // SAFETY: `Frame` is `#[repr(transparent)]` over `PPtr` // plus a zero-size `PhantomData`. `Frame` 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) + ensures + r.ptr == self.ptr, + { + // SAFETY: as above. + unsafe { core::mem::transmute(self) } + } } } // verus! diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index e1a0591a9..7b0940cb4 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/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 { pub type PageTableNode = Frame>; unsafe impl AnyFrameMeta for PageTablePageMeta { + #[cfg(feature = "type_id")] + open spec fn meta_id(&self) -> TypeId { + type_id::() + } + + #[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 diff --git a/patches/0001-verus-type-identity.patch b/patches/0001-verus-type-identity.patch new file mode 100644 index 000000000..23d5a5ac1 --- /dev/null +++ b/patches/0001-verus-type-identity.patch @@ -0,0 +1,1326 @@ +diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs +index 8fceab37..e642dff4 100644 +--- a/source/builtin/src/lib.rs ++++ b/source/builtin/src/lib.rs +@@ -2322,6 +2322,30 @@ pub fn arch_word_bits() -> nat { + unimplemented!(); + } + ++/// The identity of `T`, as `core::any::TypeId`. ++/// ++/// Spec-mode, but *not* a ghost counterpart of `core::any::TypeId` -- it is the ++/// same type. `TypeId::of::()` in exec code and `type_id::()` in a spec ++/// denote one value, compared with one notion of equality, so a runtime test ++/// establishes the ghost fact directly with no `view()` in between. ++/// ++/// Identity is decoration-sensitive, as `core::any::TypeId` is: `T`, `&T`, ++/// `Box`, `Rc` and `Arc` are all distinct, at every level of nesting. ++/// Decorations live in a sort of their own rather than in `Type`, so the tag is ++/// built from both components; see `TYPE%tagd` in `vir/src/prelude.rs`. ++/// ++/// It cannot distinguish *type parameters*: `A` and `B` may be instantiated ++/// equally, so `type_id::() != type_id::()` is not provable, by design. ++/// ++/// Unlike `core::any::TypeId::of`, this has no `'static` bound -- it is spec-only ++/// and total over Verus types, including `int`, `nat` and non-`'static` ones, ++/// which have no runtime id to disagree with. ++#[cfg(verus_keep_ghost)] ++#[rustc_diagnostic_item = "verus::verus_builtin::type_id"] ++pub fn type_id() -> core::any::TypeId { ++ unimplemented!(); ++} ++ + #[cfg(verus_keep_ghost)] + #[rustc_diagnostic_item = "verus::verus_builtin::is_smaller_than"] + pub fn is_smaller_than(_: A, _: B) -> bool { +diff --git a/source/rust_verify/src/fn_call_to_vir.rs b/source/rust_verify/src/fn_call_to_vir.rs +index c5c99ad4..b550df96 100644 +--- a/source/rust_verify/src/fn_call_to_vir.rs ++++ b/source/rust_verify/src/fn_call_to_vir.rs +@@ -5,7 +5,7 @@ use crate::resolve_traits::{ResolutionResult, ResolvedItem, resolve_trait_item}; + use crate::reveal_hide::RevealHideResult; + use crate::rust_to_vir_base::{ + bitwidth_and_signedness_of_integer_type, is_smt_arith, is_type_std_rc_or_arc_or_ref, +- typ_of_expr_adjusted, typ_of_node_unadjusted, ++ mid_ty_to_vir, typ_of_expr_adjusted, typ_of_node_unadjusted, + }; + use crate::rust_to_vir_expr::{ + check_lit_int, closure_param_typs, closure_to_vir, expr_to_vir, expr_to_vir_consume, +@@ -1219,6 +1219,21 @@ fn verus_item_to_vir<'tcx, 'a>( + + mk_expr(ExprX::UnaryOpr(UnaryOpr::IntegerTypeBound(kind, Mode::Spec), arg)) + } ++ ExprItem::TypeId => { ++ record_spec_fn(bctx, expr); ++ assert!(args.len() == 0); ++ let t = mid_ty_to_vir( ++ tcx, ++ &bctx.ctxt.verus_items, ++ None::<&mut std::collections::HashMap>, ++ bctx.fun_id, ++ expr.span, ++ &node_substs[0].expect_ty(), ++ None, ++ )?; ++ ++ mk_expr(ExprX::NullaryOpr(vir::ast::NullaryOpr::TypeTag(t))) ++ } + ExprItem::ClosureToFnSpec | ExprItem::ClosureToFnProof => { + unsupported_err_unless!(args_len == 1, expr.span, "expected closure_to_fn", &args); + if !bctx.in_ghost { +diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs +index b194808e..20219e17 100644 +--- a/source/rust_verify/src/rust_to_vir_base.rs ++++ b/source/rust_verify/src/rust_to_vir_base.rs +@@ -1146,6 +1146,17 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>( + } else { + let rust_item = verus_items::get_rust_item(tcx, did); + ++ // `core::any::TypeId` *is* Verus's type identity: it translates to ++ // the same VIR type that `type_id::()` produces, so a runtime id ++ // and a ghost one are one type with one notion of equality. There is ++ // no `view()` between them and no separate `TypeIdSpec`. ++ if rust_item == Some(verus_items::RustItem::TypeId) { ++ return Ok(( ++ Arc::new(TypX::Primitive(Primitive::TypeTag, Arc::new(vec![]))), ++ false, ++ )); ++ } ++ + let typ_args = mk_typ_args(&args)?; + if Some(did) == tcx.lang_items().owned_box() && typ_args.len() == 2 { + let (t0, ghost) = &typ_args[0]; +diff --git a/source/rust_verify/src/trait_conflicts.rs b/source/rust_verify/src/trait_conflicts.rs +index ff8f9255..9f98285a 100644 +--- a/source/rust_verify/src/trait_conflicts.rs ++++ b/source/rust_verify/src/trait_conflicts.rs +@@ -51,6 +51,7 @@ enum TypNum { + Never, + ConstPtr, + Global, ++ TypeTag, + } + + fn gen_num_typ(n: TypNum, ts: Vec) -> Typ { +@@ -130,6 +131,7 @@ fn gen_typ(state: &mut State, typ: &vir::ast::Typ) -> Typ { + Primitive::StrSlice => unreachable!(), + Primitive::Ptr => TypNum::Ptr, + Primitive::Global => TypNum::Global, ++ Primitive::TypeTag => TypNum::TypeTag, + }; + gen_num_typ(n, gen_typs(state, ts)) + } +diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs +index 234af809..1293cc08 100644 +--- a/source/rust_verify/src/verus_items.rs ++++ b/source/rust_verify/src/verus_items.rs +@@ -145,6 +145,7 @@ pub(crate) enum ExprItem { + StrSliceLen, + StrSliceGetChar, + ArchWordBits, ++ TypeId, + ClosureToFnSpec, + ClosureToFnProof, + SignedMin, +@@ -547,6 +548,7 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { + ("verus::verus_builtin::strslice_len", VerusItem::Expr(ExprItem::StrSliceLen)), + ("verus::verus_builtin::strslice_get_char", VerusItem::Expr(ExprItem::StrSliceGetChar)), + ("verus::verus_builtin::arch_word_bits", VerusItem::Expr(ExprItem::ArchWordBits)), ++ ("verus::verus_builtin::type_id", VerusItem::Expr(ExprItem::TypeId)), + ("verus::verus_builtin::closure_to_fn_spec", VerusItem::Expr(ExprItem::ClosureToFnSpec)), + ("verus::verus_builtin::closure_to_fn_proof", VerusItem::Expr(ExprItem::ClosureToFnProof)), + ("verus::verus_builtin::signed_min", VerusItem::Expr(ExprItem::SignedMin)), +@@ -916,6 +918,10 @@ pub(crate) enum RustItem { + SliceSealed, + Vec, + Thin, ++ /// `core::any::TypeId`, which *is* Verus's type identity -- it maps to ++ /// `Primitive::TypeTag`, the same VIR type `type_id::()` produces. There is ++ /// no separate ghost id type. ++ TypeId, + } + + pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option { +@@ -1041,6 +1047,9 @@ pub(crate) fn get_rust_item_str(rust_path: Option<&str>) -> Option { + if rust_path == Some("core::ptr::metadata::Thin") { + return Some(RustItem::Thin); + } ++ if rust_path == Some("core::any::TypeId") { ++ return Some(RustItem::TypeId); ++ } + if rust_path == Some("core::any::Any") { + return Some(RustItem::Any); + } +diff --git a/source/rust_verify_test/tests/type_id.rs b/source/rust_verify_test/tests/type_id.rs +new file mode 100644 +index 00000000..faa3057c +--- /dev/null ++++ b/source/rust_verify_test/tests/type_id.rs +@@ -0,0 +1,245 @@ ++#![feature(rustc_private)] ++#[macro_use] ++mod common; ++use common::*; ++ ++// `type_id::()` yields the identity of `T`. Two of them are equal exactly when ++// the tag axioms make the types equal; see vir::def's TYPE_TAG documentation. ++ ++test_verify_one_file! { ++ #[test] distinct_primitive_constructors verus_code! { ++ use verus_builtin::type_id; ++ proof fn t() { ++ assert(type_id::() != type_id::()); ++ assert(type_id::() != type_id::()); ++ assert(type_id::() != type_id::()); ++ } ++ } => Ok(()) ++} ++ ++test_verify_one_file! { ++ #[test] distinct_datatypes verus_code! { ++ use verus_builtin::type_id; ++ struct A; ++ struct B; ++ proof fn t() { ++ assert(type_id::() != type_id::()); ++ assert(type_id::() != type_id::()); ++ } ++ } => Ok(()) ++} ++ ++// The case no user-level axiom can express: two instantiations of one constructor. ++test_verify_one_file! { ++ #[test] distinct_instantiations verus_code! { ++ use verus_builtin::type_id; ++ struct Wrap(T); ++ proof fn t() { ++ assert(type_id::>() != type_id::>()); ++ assert(type_id::>() != type_id::>()); ++ } ++ } => Ok(()) ++} ++ ++test_verify_one_file! { ++ #[test] argument_order_matters verus_code! { ++ use verus_builtin::type_id; ++ struct Pair(A, B); ++ proof fn t() { ++ assert(type_id::>() != type_id::>()); ++ } ++ } => Ok(()) ++} ++ ++test_verify_one_file! { ++ #[test] nested_and_recursive verus_code! { ++ use vstd::prelude::*; ++ use verus_builtin::type_id; ++ struct Wrap(T); ++ enum List { Nil, Cons(T, Box>) } ++ proof fn t() { ++ assert(type_id::>>() != type_id::>()); ++ assert(type_id::>() != type_id::>()); ++ } ++ } => Ok(()) ++} ++ ++test_verify_one_file! { ++ #[test] const_generics verus_code! { ++ use verus_builtin::type_id; ++ struct Slab; ++ proof fn t() { ++ assert(type_id::>() != type_id::>()); ++ assert(type_id::<[u8; 4]>() != type_id::<[u8; 8]>()); ++ } ++ } => Ok(()) ++} ++ ++test_verify_one_file! { ++ #[test] reflexive verus_code! { ++ use verus_builtin::type_id; ++ struct Wrap(T); ++ proof fn t() { ++ assert(type_id::>() == type_id::>()); ++ } ++ } => Ok(()) ++} ++ ++// A TypeId is an ordinary ghost value: it can be stored, passed and compared. ++test_verify_one_file! { ++ #[test] storable verus_code! { ++ use verus_builtin::type_id; ++ use core::any::TypeId; ++ struct Wrap(T); ++ proof fn t(x: TypeId) { ++ let s = Wrap(x); ++ assert(s.0 == x); ++ } ++ spec fn is_u8(x: TypeId) -> bool { x == type_id::() } ++ proof fn u() { ++ assert(is_u8(type_id::())); ++ } ++ } => Ok(()) ++} ++ ++// The retirement: `type_id::()` and `TypeId::of::()` are one value of one ++// type, so a runtime test establishes the spec fact with no `view()` between. ++test_verify_one_file! { ++ #[test] runtime_and_spec_id_are_one_value verus_code! { ++ use vstd::prelude::*; ++ use verus_builtin::type_id; ++ use core::any::TypeId; ++ ++ fn decides() -> (r: bool) ++ ensures r, ++ { ++ let a = TypeId::of::(); ++ let b = TypeId::of::(); ++ let c = TypeId::of::(); ++ assert(a == type_id::()); ++ !a.eq(&b) && a.eq(&c) ++ } ++ ++ proof fn ghost_and_runtime_agree(g: TypeId) ++ requires g == type_id::(), ++ ensures g != type_id::>(), ++ { } ++ } => Ok(()) ++} ++ ++// --- Soundness controls: these must NOT be provable ------------------------ ++ ++// A and B may be instantiated to the same type. ++test_verify_one_file! { ++ #[test] type_params_not_distinct verus_code! { ++ use verus_builtin::type_id; ++ proof fn t() { ++ assert(type_id::() != type_id::()); // FAILS ++ } ++ } => Err(err) => assert_one_fails(err) ++} ++ ++test_verify_one_file! { ++ #[test] type_params_not_distinct_nested verus_code! { ++ use verus_builtin::type_id; ++ struct Wrap(T); ++ proof fn t() { ++ assert(type_id::>() != type_id::>()); // FAILS ++ } ++ } => Err(err) => assert_one_fails(err) ++} ++ ++// Identity is decoration-*sensitive*, matching core::any::TypeId. The decoration ++// spine is folded into the tag by `TYPE%tagd`, so a downcast guarded on a tag ++// really does establish the type: without this, `&u8` and `u8` share an identity ++// and `x.is::<&u8>()` succeeds for an erased `u8`. ++test_verify_one_file! { ++ #[test] decoration_is_part_of_identity verus_code! { ++ use vstd::prelude::*; ++ use verus_builtin::type_id; ++ use std::rc::Rc; ++ use std::sync::Arc; ++ struct S(u8); ++ proof fn t() { ++ assert(type_id::<&u8>() != type_id::()); ++ assert(type_id::<&mut S>() != type_id::()); ++ assert(type_id::>() != type_id::()); ++ assert(type_id::>() != type_id::()); ++ assert(type_id::>() != type_id::()); ++ } ++ } => Ok(()) ++} ++ ++// Distinct decorations are distinct from *each other*, not merely from the bare ++// type, and the spine nests. ++test_verify_one_file! { ++ #[test] decorations_distinguish_each_other verus_code! { ++ use vstd::prelude::*; ++ use verus_builtin::type_id; ++ use std::rc::Rc; ++ struct S(u8); ++ proof fn t() { ++ assert(type_id::>() != type_id::>()); ++ assert(type_id::<&S>() != type_id::>()); ++ assert(type_id::<&&S>() != type_id::<&S>()); ++ } ++ } => Ok(()) ++} ++ ++// The case a top-level-only fold would miss: a decoration on a type *argument*. ++test_verify_one_file! { ++ #[test] parameter_decorations_are_folded verus_code! { ++ use vstd::prelude::*; ++ use verus_builtin::type_id; ++ struct Wrap(T); ++ struct S(u8); ++ proof fn t() { ++ assert(type_id::>() != type_id::>()); ++ assert(type_id::>>() != type_id::>()); ++ } ++ } => Ok(()) ++} ++ ++// Decorating an opaque parameter is still distinguishing, because no ++// instantiation of `A` can equal `&A` -- that would be an infinite type. This is ++// a consequence of the datatype encoding's acyclicity, not an extra axiom. ++test_verify_one_file! { ++ #[test] decorated_type_param_is_distinct verus_code! { ++ use verus_builtin::type_id; ++ proof fn t() { ++ assert(type_id::<&A>() != type_id::()); ++ } ++ } => Ok(()) ++} ++ ++// ... but two *different* parameters stay indistinguishable even decorated: `A` ++// and `B` may be instantiated equally, and so may `&A` and `&B`. ++test_verify_one_file! { ++ #[test] decorated_type_params_not_distinct verus_code! { ++ use verus_builtin::type_id; ++ proof fn t() { ++ assert(type_id::<&A>() != type_id::<&B>()); // FAILS ++ } ++ } => Err(err) => assert_one_fails(err) ++} ++ ++// An unresolved associated type is opaque, like a type parameter. ++test_verify_one_file! { ++ #[test] projections_not_distinct verus_code! { ++ use verus_builtin::type_id; ++ trait Tr { type Out; } ++ proof fn t() { ++ assert(type_id::() != type_id::()); // FAILS ++ } ++ } => Err(err) => assert_one_fails(err) ++} ++ ++// type_id is spec-only. ++test_verify_one_file! { ++ #[test] not_usable_in_exec verus_code! { ++ use verus_builtin::type_id; ++ fn t() { ++ let x = type_id::(); ++ } ++ } => Err(err) => assert_vir_error_msg(err, "cannot use spec-mode expression in executable context") ++} +diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs +index f25bb602..2fa0c741 100644 +--- a/source/vir/src/ast.rs ++++ b/source/vir/src/ast.rs +@@ -252,6 +252,17 @@ pub enum Primitive { + StrSlice, + Ptr, // Mut ptr, unless Const decoration is applied + Global, ++ /// The structural identity of a type, surfaced to Verus as `TypeId` and ++ /// produced by `type_id::()`. Its SMT sort is `TypeTag` ++ /// (see `def::TYPE_TAG_SORT`), so two of these are equal exactly when the tag ++ /// axioms make their types equal. ++ /// ++ /// NOT to be confused with `TypX::TypeId`, which is the type of a raw type ++ /// *identifier* (SMT sort `Type`) used internally to pass type arguments. A ++ /// bare `Type` term is useless for proving distinctness, because the tag ++ /// axioms are triggered on `TYPE%tag(..)` applications; this variant exists ++ /// precisely to produce such an application. ++ TypeTag, + } + + #[derive(Debug, Serialize, Deserialize, Hash, ToDebugSNode, Clone)] +@@ -370,6 +381,8 @@ pub enum NullaryOpr { + TypEqualityBound(Path, Typs, Ident, Typ), + /// predicate representing const type bound, e.g., `const X: usize` + ConstTypBound(Typ, Typ), ++ /// identity of a type, as in `type_id::()`; carries the type it identifies ++ TypeTag(Typ), + } + + #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash, ToDebugSNode)] +diff --git a/source/vir/src/ast_util.rs b/source/vir/src/ast_util.rs +index 2eee24f6..f38d6fef 100644 +--- a/source/vir/src/ast_util.rs ++++ b/source/vir/src/ast_util.rs +@@ -981,6 +981,7 @@ pub fn typ_to_diagnostic_str(typ: &Typ) -> String { + crate::ast::Primitive::StrSlice => "StrSlice".to_owned(), + crate::ast::Primitive::Ptr => format!("*mut {:}", typ_to_diagnostic_str(&typs[0])), + crate::ast::Primitive::Global => format!("Global"), ++ crate::ast::Primitive::TypeTag => format!("TypeId"), + }, + TypX::Datatype(Dt::Tuple(_arity), typs, _) => { + // 1-tuples should be formatted like `(T,)` +diff --git a/source/vir/src/ast_visitor.rs b/source/vir/src/ast_visitor.rs +index dfd33b6f..cf528edc 100644 +--- a/source/vir/src/ast_visitor.rs ++++ b/source/vir/src/ast_visitor.rs +@@ -236,6 +236,10 @@ pub(crate) trait AstVisitor { + let t = self.visit_typ(typ)?; + R::ret(|| NullaryOpr::ConstGeneric(R::get(t))) + } ++ NullaryOpr::TypeTag(typ) => { ++ let t = self.visit_typ(typ)?; ++ R::ret(|| NullaryOpr::TypeTag(R::get(t))) ++ } + NullaryOpr::TraitBound(trait_id, typs) => { + let ts = self.visit_typs(typs)?; + R::ret(|| NullaryOpr::TraitBound(trait_id.clone(), R::get_vec_a(ts))) +diff --git a/source/vir/src/context.rs b/source/vir/src/context.rs +index f3df0f2f..3e219714 100644 +--- a/source/vir/src/context.rs ++++ b/source/vir/src/context.rs +@@ -137,6 +137,9 @@ pub struct Ctx { + // proof debug purposes + pub debug: bool, + pub arch_word_bits: ArchWordBits, ++ /// Whether this module mentions type identity; gates emission of the tag ++ /// encoding. See `crate::traits::krate_uses_type_id`. ++ pub uses_type_id: bool, + } + + impl Ctx { +@@ -246,6 +249,7 @@ fn datatypes_invs( + TypX::Decorate(..) => unreachable!("TypX::Decorate"), + TypX::Boxed(_) => {} + TypX::TypeId => {} ++ TypX::Primitive(Primitive::TypeTag, _) => {} + TypX::Opaque { .. } => {} + TypX::Bool => {} + TypX::Float(_) => {} +@@ -883,6 +887,7 @@ impl Ctx { + byte_string_hashes, + debug, + arch_word_bits: krate.arch.word_bits, ++ uses_type_id: crate::traits::krate_uses_type_id(krate), + opaque_type_map, + }) + } +diff --git a/source/vir/src/datatype_to_air.rs b/source/vir/src/datatype_to_air.rs +index c006b3e9..3ce50d32 100644 +--- a/source/vir/src/datatype_to_air.rs ++++ b/source/vir/src/datatype_to_air.rs +@@ -102,6 +102,7 @@ fn uses_ext_equal(ctx: &Ctx, typ: &Typ) -> bool { + TypX::Primitive(crate::ast::Primitive::StrSlice, _) => false, + TypX::Primitive(crate::ast::Primitive::Ptr, _) => false, + TypX::Primitive(crate::ast::Primitive::Global, _) => false, ++ TypX::Primitive(crate::ast::Primitive::TypeTag, _) => false, + TypX::FnDef(..) => false, + TypX::MutRef(_) => false, + TypX::Opaque { .. } => false, +@@ -156,6 +157,81 @@ fn datatype_or_fun_to_air_commands( + str_typ(crate::def::TYPE), + )); + token_commands.push(Arc::new(CommandX::Global(decl_type_id))); ++ ++ // --- Type identity: structural tag for this constructor ------------- ++ // Emits, for `Foo`: ++ // (axiom (forall ((dA Dcr) (tA Type) (dB Dcr) (tB Type)) (! ++ // (= (TYPE%tag (TYPE%Foo dA tA dB tB)) ++ // (tag%app (tag%app (tag%mk ) (TYPE%tag tA)) (TYPE%tag tB))) ++ // :pattern ((TYPE%tag (TYPE%Foo dA tA dB tB)))))) ++ // ++ // The pattern is on the TAG application, never on the bare `TYPE%Foo` ++ // application: the latter appears inside `has_type` patterns and is one ++ // of the hottest terms in the encoding, so triggering on it would fire ++ // this axiom in every query. Triggering on the tag keeps it inert ++ // unless something actually asks for type identity. ++ // ++ // `k_Foo` is a hash of the fully-qualified path, so it is unique across ++ // separately-compiled crates without any coordination. This mirrors how ++ // string literals are handled (`sst_to_air::str_to_const_str`) and ++ // inherits the same no-collision assumption. ++ if ctx.uses_type_id { ++ let mut binders: Vec> = Vec::new(); ++ let mut id_args: Vec = Vec::new(); ++ let mut tag_args: Vec = Vec::new(); ++ for (i, _) in tparams.iter().enumerate() { ++ // types() is (Dcr, Type). Both components are tagged, via ++ // TYPE%tagd, so that `G<&u8>` and `G` are distinct -- tagging ++ // only the Type half is what made parameter decorations invisible. ++ let mut param_ids: Vec = Vec::new(); ++ for (j, s) in crate::def::types().iter().enumerate() { ++ let nm = air_unique_var(&format!("tag%p{}%{}", i, j)); ++ binders.push(ident_binder(&nm.lower(), &str_typ(s))); ++ let v = ident_var(&nm.lower()); ++ param_ids.push(v.clone()); ++ id_args.push(v); ++ } ++ // The body of TYPE%tagd, inlined. Naming the function here instead ++ // would put one more quantifier on the hottest path in the ++ // encoding -- these axioms are instantiated far more than any ++ // user-written `type_id::()` -- for no gain in what is proved. ++ tag_args.push(str_apply( ++ crate::def::TYPE_TAG_APP, ++ &vec![ ++ str_apply(crate::def::DCR_TAG, &vec![param_ids[0].clone()]), ++ str_apply(crate::def::TYPE_TAG, &vec![param_ids[1].clone()]), ++ ], ++ )); ++ } ++ let k = crate::sst_to_air::path_type_tag_id(dpath); ++ let mut rhs = str_apply( ++ crate::def::TYPE_TAG_MK, ++ &vec![Arc::new(ExprX::Const(air::ast::Constant::Nat(Arc::new(k))))], ++ ); ++ for a in tag_args.iter() { ++ rhs = str_apply(crate::def::TYPE_TAG_APP, &vec![rhs, a.clone()]); ++ } ++ let id_app = if id_args.is_empty() { ++ ident_var(&ctx.name_ctxt.prefix_type_id(dpath)) ++ } else { ++ ident_apply(&ctx.name_ctxt.prefix_type_id(dpath), &Arc::new(id_args)) ++ }; ++ let lhs = str_apply(crate::def::TYPE_TAG, &vec![id_app]); ++ let body = mk_eq(&lhs, &rhs); ++ let axiom = if binders.is_empty() { ++ mk_unnamed_axiom(body) ++ } else { ++ let trigs = Arc::new(vec![Arc::new(vec![lhs.clone()])]); ++ let bind = Arc::new(air::ast::BindX::Quant( ++ air::ast::Quant::Forall, ++ Arc::new(binders), ++ trigs, ++ None, ++ )); ++ mk_unnamed_axiom(mk_bind_expr(&bind, &body)) ++ }; ++ token_commands.push(Arc::new(CommandX::Global(axiom))); ++ } + } + + if declare_box { +diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs +index 0b44844c..edb5aad4 100644 +--- a/source/vir/src/def.rs ++++ b/source/vir/src/def.rs +@@ -87,6 +87,7 @@ const STRSLICE_TYPE: &str = "strslice%"; + const ARRAY_TYPE: &str = "array%"; + const PTR_TYPE: &str = "ptr_mut%"; + const GLOBAL_TYPE: &str = "allocator_global%"; ++const TYPETAG_TYPE: &str = "typetag%"; + const PREFIX_SNAPSHOT: &str = "snap%"; + const SUBST_RENAME_SEPARATOR: &str = "$$"; + const EXPAND_ERRORS_DECL_SEPARATOR: &str = "$$$"; +@@ -167,10 +168,12 @@ pub const BOX_INT: &str = "I"; + pub const BOX_BOOL: &str = "B"; + pub const BOX_REAL: &str = "R"; + pub const BOX_FNDEF: &str = "F"; ++pub const BOX_TYPETAG: &str = "Tg"; + pub const UNBOX_INT: &str = "%I"; + pub const UNBOX_BOOL: &str = "%B"; + pub const UNBOX_REAL: &str = "%R"; + pub const UNBOX_FNDEF: &str = "%F"; ++pub const UNBOX_TYPETAG: &str = "%Tg"; + pub const TYPE: &str = "Type"; + pub const TYPE_ID_BOOL: &str = "BOOL"; + pub const TYPE_ID_REAL: &str = "REAL"; +@@ -184,6 +187,52 @@ pub const TYPE_ID_SINT: &str = "SINT"; + pub const TYPE_ID_FLOAT: &str = "FLOAT"; + pub const TYPE_ID_CONST_INT: &str = "CONST_INT"; + pub const TYPE_ID_CONST_BOOL: &str = "CONST_BOOL"; ++ ++// --- Type identity (see docs/verus-typeid-implementation-plan.md) --------- ++// A structural tag for type ids, so that distinct type constructors and ++// distinct instantiations of a constructor are provably distinct. ++// ++// A curried spine: `Foo` tags as `app(app(mk k_Foo, tag a), tag b)`, so ++// one sort with two constructors covers constructors of any arity. ++// ++// Encoded as an SMT datatype rather than an Int + injectivity axiom: the ++// datatype gives constructor distinctness AND injectivity for free, which ++// avoids a quantified injectivity axiom and, critically, avoids a multi-pattern ++// over `TYPE%Foo(..)` -- a term that appears inside the `has_type` patterns and ++// is therefore one of the hottest in the encoding. ++// ++// Every tag axiom is triggered on the *tag application* `TYPE%tag(TYPE%Foo(..))` ++// and never on the bare constructor, so the axioms stay inert in queries that ++// do not mention type identity. ++// ++// Constructor ids come from two disjoint pools, so the two can never collide: ++// built-in constructors (declared in the prelude) use small NEGATIVE ids, while ++// user datatypes use a NON-NEGATIVE path hash (see `sst_to_air::path_type_tag_id`, ++// which shifts right to clear the sign bit). Only datatype-vs-datatype collision ++// remains possible, under the same assumption already made for string literals. ++// ++// A per-context counter would remove even that assumption, and was tried (branch ++// `typeid-counter-ids`). It is unsound *here*: `type_id::()` denotes a ++// `core::any::TypeId`, whose runtime value is a hash, so distinctness of two ++// types is not guaranteed at runtime. A counter proves distinctness for every ++// pair, which is stronger than Rust promises -- and under a runtime collision the ++// `PartialEq` specification in `vstd/std_specs/any.rs` would be false. Modelling ++// a hash with a hash keeps the two in the same collision class. ++pub const TYPE_TAG_SORT: &str = "TypeTag"; ++pub const TYPE_TAG: &str = "TYPE%tag"; ++// The decorated tag: `TYPE%tagd(d, t)` folds a type's decoration spine into its ++// tag, so `&T`, `Box` and `T` no longer share an identity. `TYPE%tag` stays ++// the undecorated base, and every axiom over it is unchanged. ++pub const TYPE_TAG_D: &str = "TYPE%tagd"; ++pub const DCR_TAG: &str = "dcr%tag"; ++// `TypeTag` is itself a Verus-visible type (surfaced as `TypeId`), so like any ++// other type it needs a type id of its own. ++pub const TYPE_ID_TYPETAG: &str = "TYPETAG"; ++pub const TYPE_TAG_MK: &str = "tag%mk"; ++pub const TYPE_TAG_ID: &str = "tag%id"; ++pub const TYPE_TAG_APP: &str = "tag%app"; ++pub const TYPE_TAG_FN: &str = "tag%fn"; ++pub const TYPE_TAG_ARG: &str = "tag%arg"; + pub const DECORATION: &str = "Dcr"; + pub const DECORATE_NIL_SIZED: &str = "$"; + pub const DECORATE_NIL_SLICE: &str = "$slice"; // for 'str' and '[T]' types +@@ -597,6 +646,11 @@ pub fn global_type() -> Path { + Arc::new(PathX { krate: CrateId::Internal, segments: Arc::new(vec![ident]) }) + } + ++pub fn typetag_type() -> Path { ++ let ident = Arc::new(TYPETAG_TYPE.to_string()); ++ Arc::new(PathX { krate: CrateId::Internal, segments: Arc::new(vec![ident]) }) ++} ++ + impl NameCtxt { + pub fn prefix_dcr_id(&self, ident: &Path) -> Ident { + Arc::new(PREFIX_DCR_ID.to_string() + &self.path_to_string(ident)) +diff --git a/source/vir/src/heuristics.rs b/source/vir/src/heuristics.rs +index f969aee9..e5789bf7 100644 +--- a/source/vir/src/heuristics.rs ++++ b/source/vir/src/heuristics.rs +@@ -29,6 +29,7 @@ fn auto_ext_equal_typ(ctx: &Ctx, typ: &Typ) -> bool { + TypX::Primitive(crate::ast::Primitive::StrSlice, _) => true, + TypX::Primitive(crate::ast::Primitive::Ptr, _) => false, + TypX::Primitive(crate::ast::Primitive::Global, _) => false, ++ TypX::Primitive(crate::ast::Primitive::TypeTag, _) => false, + TypX::FnDef(..) => false, + TypX::MutRef(_) => false, + TypX::Opaque { .. } => false, +diff --git a/source/vir/src/modes.rs b/source/vir/src/modes.rs +index ef61a3b7..88f7c12d 100644 +--- a/source/vir/src/modes.rs ++++ b/source/vir/src/modes.rs +@@ -2101,6 +2101,7 @@ fn check_expr( + Ok((Mode::Spec, Proph::No)) + } + ExprX::NullaryOpr(crate::ast::NullaryOpr::ConstTypBound(..)) => Ok((Mode::Spec, Proph::No)), ++ ExprX::NullaryOpr(crate::ast::NullaryOpr::TypeTag(..)) => Ok((Mode::Spec, Proph::No)), + ExprX::Unary(UnaryOp::CoerceMode { op_mode, from_mode, to_mode, kind }, e1) => { + // same as a call to an op_mode function with parameter from_mode and return to_mode + if ctxt.check_ghost_blocks { +diff --git a/source/vir/src/poly.rs b/source/vir/src/poly.rs +index 47141ba8..1d4b865c 100644 +--- a/source/vir/src/poly.rs ++++ b/source/vir/src/poly.rs +@@ -157,6 +157,10 @@ pub(crate) fn typ_as_mono(typ: &Typ) -> Option { + Some(Arc::new(MonoTypX::Decorate2(*d, Arc::new(vec![m1, m2])))) + } + TypX::Primitive(Primitive::Array, _) => None, ++ // TypeTag has its own prelude sort and box/unbox (like FnDef), so it must ++ // not also be encoded as an opaque mono sort -- that would declare a second, ++ // incompatible `typetag%.` sort and box through it. ++ TypX::Primitive(Primitive::TypeTag, _) => None, + TypX::Primitive(name, typs) => { + let monotyps = monotyps_as_mono(typs)?; + Some(Arc::new(MonoTypX::Primitive(*name, Arc::new(monotyps)))) +@@ -204,6 +208,7 @@ pub(crate) fn typ_is_poly(ctx: &Ctx, typ: &Typ) -> bool { + match &**typ { + TypX::Bool | TypX::Int(_) | TypX::Real | TypX::Float(_) => false, + TypX::SpecFn(..) | TypX::FnDef(..) => false, ++ TypX::Primitive(Primitive::TypeTag, _) => false, + TypX::Primitive(Primitive::Array, _) => false, + TypX::AnonymousClosure(..) => { + panic!("internal error: AnonymousClosure should be removed by ast_simplify") +@@ -238,6 +243,7 @@ pub(crate) fn coerce_typ_to_native(ctx: &Ctx, typ: &Typ) -> Typ { + match &**typ { + TypX::Bool | TypX::Int(_) | TypX::Real | TypX::Float(_) => typ.clone(), + TypX::SpecFn(..) | TypX::FnDef(..) => typ.clone(), ++ TypX::Primitive(Primitive::TypeTag, _) => typ.clone(), + TypX::Primitive(Primitive::Array, _) => typ.clone(), + TypX::AnonymousClosure(..) => { + panic!("internal error: AnonymousClosure should be removed by ast_simplify") +@@ -280,6 +286,7 @@ pub(crate) fn coerce_typ_to_poly(_ctx: &Ctx, typ: &Typ) -> Typ { + TypX::Bool | TypX::Int(_) => Arc::new(TypX::Boxed(typ.clone())), + TypX::Real | TypX::Float(_) => Arc::new(TypX::Boxed(typ.clone())), + TypX::SpecFn(..) | TypX::FnDef(..) => Arc::new(TypX::Boxed(typ.clone())), ++ TypX::Primitive(Primitive::TypeTag, _) => Arc::new(TypX::Boxed(typ.clone())), + TypX::AnonymousClosure(..) => { + panic!("internal error: AnonymousClosure should be removed by ast_simplify") + } +@@ -569,6 +576,7 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { + ExpX::NullaryOpr(NullaryOpr::TraitBound(..)) => exp.clone(), + ExpX::NullaryOpr(NullaryOpr::TypEqualityBound(..)) => exp.clone(), + ExpX::NullaryOpr(NullaryOpr::ConstTypBound(..)) => exp.clone(), ++ ExpX::NullaryOpr(NullaryOpr::TypeTag(..)) => exp.clone(), + ExpX::Unary(op, e1) => { + let e1 = visit_exp(ctx, state, e1); + match op { +diff --git a/source/vir/src/prelude.rs b/source/vir/src/prelude.rs +index 8d50db73..590da4d7 100644 +--- a/source/vir/src/prelude.rs ++++ b/source/vir/src/prelude.rs +@@ -163,6 +163,18 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< + let type_id_slice = str_to_node(TYPE_ID_SLICE); + let type_id_strslice = str_to_node(TYPE_ID_STRSLICE); + let type_id_ptr = str_to_node(TYPE_ID_PTR); ++ let type_tag_sort = str_to_node(TYPE_TAG_SORT); ++ let type_tag = str_to_node(TYPE_TAG); ++ let type_tag_d = str_to_node(TYPE_TAG_D); ++ let dcr_tag = str_to_node(DCR_TAG); ++ let type_id_typetag = str_to_node(TYPE_ID_TYPETAG); ++ let box_typetag = str_to_node(BOX_TYPETAG); ++ let unbox_typetag = str_to_node(UNBOX_TYPETAG); ++ let tag_mk = str_to_node(TYPE_TAG_MK); ++ let tag_id = str_to_node(TYPE_TAG_ID); ++ let tag_app = str_to_node(TYPE_TAG_APP); ++ let tag_fn = str_to_node(TYPE_TAG_FN); ++ let tag_arg = str_to_node(TYPE_TAG_ARG); + let type_id_global = str_to_node(TYPE_ID_GLOBAL); + let type_id_mut_ref = str_to_node(TYPE_ID_MUT_REF); + +@@ -203,6 +215,7 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< + (declare-fun [unbox_real] ([Poly]) Real) + (declare-fun [unbox_fndef] ([Poly]) [FnDef]) + (declare-sort [typ] 0) ++ (declare-const [type_id_typetag] [typ]) + (declare-const [type_id_bool] [typ]) + (declare-const [type_id_int] [typ]) + (declare-const [type_id_nat] [typ]) +@@ -216,6 +229,21 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< + (declare-fun [type_id_float] (Int) [typ]) + (declare-fun [type_id_const_int] (Int) [typ]) + (declare-fun [type_id_const_bool] (Bool) [typ]) ++ // Type identity: a structural tag over type ids. A curried spine, so a ++ // single sort with two constructors covers any constructor arity: ++ // Foo ~> (tag%app (tag%app (tag%mk k) (tag a)) (tag b)) ++ (declare-datatypes (([type_tag_sort] 0)) ++ ((([tag_mk] ([tag_id] Int)) ++ ([tag_app] ([tag_fn] [type_tag_sort]) ([tag_arg] [type_tag_sort]))))) ++ (declare-fun [type_tag] ([typ]) [type_tag_sort]) ++ // `TypeId` is surfaced to Verus as a primitive whose SMT sort is ++ // [type_tag_sort]. Unlike [FnDef] -- a singleton, where the box/unbox ++ // round-trip holds trivially because all its values are equal -- this sort ++ // has many values, so it needs real box/unbox axioms (further below). ++ // Declared here rather than with the other boxes because [type_tag_sort] ++ // must exist first. ++ (declare-fun [box_typetag] ([type_tag_sort]) [Poly]) ++ (declare-fun [unbox_typetag] ([Poly]) [type_tag_sort]) + (declare-sort [decoration] 0) + (declare-const [decorate_nil_sized] [decoration]) + (declare-const [decorate_nil_slice] [decoration]) +@@ -229,6 +257,14 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< + (declare-fun [decorate_tracked] ([decoration]) [decoration]) + (declare-fun [decorate_never] ([decoration]) [decoration]) + (declare-fun [decorate_const_ptr] ([decoration]) [decoration]) ++ // Decoration-sensitive identity. [type_tag] alone is undecorated -- it is ++ // a function of the [typ] component only, and decorations live in a ++ // separate sort -- so `&T` and `T` would share it. [type_tag_d] pairs a ++ // decoration spine with a base tag, and [dcr_tag] gives that spine a tag ++ // of its own. Every use site that means "the identity of this type" ++ // applies [type_tag_d] to both components of `typ_to_ids`. ++ (declare-fun [dcr_tag] ([decoration]) [type_tag_sort]) ++ (declare-fun [type_tag_d] ([decoration] [typ]) [type_tag_sort]) + (declare-fun [type_id_array] ([decoration] [typ] [decoration] [typ]) [typ]) + (declare-fun [type_id_mut_ref] ([decoration] [typ]) [typ]) + (declare-fun [type_id_slice] ([decoration] [typ]) [typ]) +@@ -374,6 +410,198 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< + :qid prelude_type_id_const_bool + :skolemid skolem_prelude_type_id_const_bool + ))) ++ // --- Type identity: tags for the primitive type ids ----------------- ++ // Nullary ids are plain leaves. Parameterised ones apply their argument, ++ // so e.g. UINT 8 and UINT 16 are provably distinct. Every pattern is on ++ // the TAG application, never the bare type id, so these stay inert ++ // unless something asks for a tag. ++ (axiom (= ([type_tag] [type_id_bool]) ([tag_mk] (- 1)))) ++ (axiom (= ([type_tag] [type_id_int]) ([tag_mk] (- 2)))) ++ (axiom (= ([type_tag] [type_id_nat]) ([tag_mk] (- 3)))) ++ (axiom (= ([type_tag] [type_id_real]) ([tag_mk] (- 4)))) ++ (axiom (= ([type_tag] [type_id_char]) ([tag_mk] (- 5)))) ++ (axiom (= ([type_tag] [type_id_usize]) ([tag_mk] (- 6)))) ++ (axiom (= ([type_tag] [type_id_isize]) ([tag_mk] (- 7)))) ++ (axiom (forall ((n Int)) (! ++ (= ([type_tag] ([type_id_uint] n)) ([tag_app] ([tag_mk] (- 8)) ([tag_mk] n))) ++ :pattern (([type_tag] ([type_id_uint] n))) ++ :qid prelude_type_tag_uint ++ :skolemid skolem_prelude_type_tag_uint ++ ))) ++ (axiom (forall ((n Int)) (! ++ (= ([type_tag] ([type_id_sint] n)) ([tag_app] ([tag_mk] (- 9)) ([tag_mk] n))) ++ :pattern (([type_tag] ([type_id_sint] n))) ++ :qid prelude_type_tag_sint ++ :skolemid skolem_prelude_type_tag_sint ++ ))) ++ (axiom (forall ((n Int)) (! ++ (= ([type_tag] ([type_id_float] n)) ([tag_app] ([tag_mk] (- 10)) ([tag_mk] n))) ++ :pattern (([type_tag] ([type_id_float] n))) ++ :qid prelude_type_tag_float ++ :skolemid skolem_prelude_type_tag_float ++ ))) ++ (axiom (forall ((n Int)) (! ++ (= ([type_tag] ([type_id_const_int] n)) ([tag_app] ([tag_mk] (- 11)) ([tag_mk] n))) ++ :pattern (([type_tag] ([type_id_const_int] n))) ++ :qid prelude_type_tag_const_int ++ :skolemid skolem_prelude_type_tag_const_int ++ ))) ++ (axiom (= ([type_tag] [type_id_typetag]) ([tag_mk] (- 20)))) ++ // Box/unbox for the `TypeId` primitive, mirroring the int/bool/real triples. ++ (axiom (forall ((x [type_tag_sort])) (! ++ (= x ([unbox_typetag] ([box_typetag] x))) ++ :pattern (([box_typetag] x)) ++ :qid prelude_unbox_box_typetag ++ :skolemid skolem_prelude_unbox_box_typetag ++ ))) ++ (axiom (forall ((x [Poly])) (! ++ (=> ++ ([has_type] x [type_id_typetag]) ++ (= x ([box_typetag] ([unbox_typetag] x))) ++ ) ++ :pattern (([has_type] x [type_id_typetag])) ++ :qid prelude_box_unbox_typetag ++ :skolemid skolem_prelude_box_unbox_typetag ++ ))) ++ (axiom (forall ((x [type_tag_sort])) (! ++ ([has_type] ([box_typetag] x) [type_id_typetag]) ++ :pattern (([has_type] ([box_typetag] x) [type_id_typetag])) ++ :qid prelude_has_type_typetag ++ :skolemid skolem_prelude_has_type_typetag ++ ))) ++ // --- Type identity: folding the decoration spine -------------------- ++ // [type_tag_d] is the identity of a type: its decoration spine paired ++ // with its undecorated base tag. Injectivity is free -- [type_tag_sort] ++ // is a datatype, so [tag_app] is injective and its constructors are ++ // distinct -- provided [dcr_tag] separates decoration spines, which the ++ // axioms below do, in the same shape as the type-side ones. ++ // ++ // Decoration ids live at -101 and below, disjoint from the built-in type ++ // ids (-1 .. -20) and from datatype ids (non-negative), though they could ++ // not collide anyway: the two sit in different argument positions. ++ (axiom (forall ((d [decoration]) (t [typ])) (! ++ (= ([type_tag_d] d t) ([tag_app] ([dcr_tag] d) ([type_tag] t))) ++ :pattern (([type_tag_d] d t)) ++ :qid prelude_type_tag_d ++ :skolemid skolem_prelude_type_tag_d ++ ))) ++ (axiom (= ([dcr_tag] [decorate_nil_sized]) ([tag_mk] (- 101)))) ++ (axiom (= ([dcr_tag] [decorate_nil_slice]) ([tag_mk] (- 102)))) ++ (axiom (= ([dcr_tag] [decorate_nil_dyn]) ([tag_mk] (- 103)))) ++ (axiom (forall ((d [decoration])) (! ++ (= ([dcr_tag] ([decorate_dst_inherit] d)) ([tag_app] ([tag_mk] (- 104)) ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_dst_inherit] d))) ++ :qid prelude_dcr_tag_dst ++ :skolemid skolem_prelude_dcr_tag_dst ++ ))) ++ (axiom (forall ((d [decoration])) (! ++ (= ([dcr_tag] ([decorate_ref] d)) ([tag_app] ([tag_mk] (- 105)) ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_ref] d))) ++ :qid prelude_dcr_tag_ref ++ :skolemid skolem_prelude_dcr_tag_ref ++ ))) ++ (axiom (forall ((d [decoration])) (! ++ (= ([dcr_tag] ([decorate_ghost] d)) ([tag_app] ([tag_mk] (- 106)) ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_ghost] d))) ++ :qid prelude_dcr_tag_ghost ++ :skolemid skolem_prelude_dcr_tag_ghost ++ ))) ++ (axiom (forall ((d [decoration])) (! ++ (= ([dcr_tag] ([decorate_tracked] d)) ([tag_app] ([tag_mk] (- 107)) ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_tracked] d))) ++ :qid prelude_dcr_tag_tracked ++ :skolemid skolem_prelude_dcr_tag_tracked ++ ))) ++ (axiom (forall ((d [decoration])) (! ++ (= ([dcr_tag] ([decorate_never] d)) ([tag_app] ([tag_mk] (- 108)) ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_never] d))) ++ :qid prelude_dcr_tag_never ++ :skolemid skolem_prelude_dcr_tag_never ++ ))) ++ (axiom (forall ((d [decoration])) (! ++ (= ([dcr_tag] ([decorate_const_ptr] d)) ([tag_app] ([tag_mk] (- 109)) ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_const_ptr] d))) ++ :qid prelude_dcr_tag_const_ptr ++ :skolemid skolem_prelude_dcr_tag_const_ptr ++ ))) ++ // Box/Rc/Arc carry their allocator type as (decoration, typ), so that is ++ // folded too: `Box` and `Box` are different types. ++ (axiom (forall ((ad [decoration]) (at [typ]) (d [decoration])) (! ++ (= ([dcr_tag] ([decorate_box] ad at d)) ++ ([tag_app] ++ ([tag_app] ([tag_mk] (- 110)) ([tag_app] ([dcr_tag] ad) ([type_tag] at))) ++ ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_box] ad at d))) ++ :qid prelude_dcr_tag_box ++ :skolemid skolem_prelude_dcr_tag_box ++ ))) ++ (axiom (forall ((ad [decoration]) (at [typ]) (d [decoration])) (! ++ (= ([dcr_tag] ([decorate_rc] ad at d)) ++ ([tag_app] ++ ([tag_app] ([tag_mk] (- 111)) ([tag_app] ([dcr_tag] ad) ([type_tag] at))) ++ ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_rc] ad at d))) ++ :qid prelude_dcr_tag_rc ++ :skolemid skolem_prelude_dcr_tag_rc ++ ))) ++ (axiom (forall ((ad [decoration]) (at [typ]) (d [decoration])) (! ++ (= ([dcr_tag] ([decorate_arc] ad at d)) ++ ([tag_app] ++ ([tag_app] ([tag_mk] (- 112)) ([tag_app] ([dcr_tag] ad) ([type_tag] at))) ++ ([dcr_tag] d))) ++ :pattern (([dcr_tag] ([decorate_arc] ad at d))) ++ :qid prelude_dcr_tag_arc ++ :skolemid skolem_prelude_dcr_tag_arc ++ ))) ++ (axiom (= ([type_tag] [type_id_strslice]) ([tag_mk] (- 12)))) ++ (axiom (= ([type_tag] [type_id_global]) ([tag_mk] (- 13)))) ++ // A const bool has no tag of its own to recurse into, so its two ++ // values are mapped to two distinct leaves. ++ (axiom (forall ((b Bool)) (! ++ (= ([type_tag] ([type_id_const_bool] b)) ++ ([tag_app] ([tag_mk] (- 14)) ([tag_mk] (ite b 1 0)))) ++ :pattern (([type_tag] ([type_id_const_bool] b))) ++ :qid prelude_type_tag_const_bool ++ :skolemid skolem_prelude_type_tag_const_bool ++ ))) ++ // Each of these carries its argument as a (decoration, typ) pair, so the ++ // fold is [type_tag_d], not [type_tag]: `*const &u8` and `*const u8` are ++ // different types, and so are `[&u8]` and `[u8]`. ++ (axiom (forall ((d [decoration]) (t [typ])) (! ++ (= ([type_tag] ([type_id_mut_ref] d t)) ++ ([tag_app] ([tag_mk] (- 15)) ([tag_app] ([dcr_tag] d) ([type_tag] t)))) ++ :pattern (([type_tag] ([type_id_mut_ref] d t))) ++ :qid prelude_type_tag_mut_ref ++ :skolemid skolem_prelude_type_tag_mut_ref ++ ))) ++ (axiom (forall ((d [decoration]) (t [typ])) (! ++ (= ([type_tag] ([type_id_slice] d t)) ++ ([tag_app] ([tag_mk] (- 16)) ([tag_app] ([dcr_tag] d) ([type_tag] t)))) ++ :pattern (([type_tag] ([type_id_slice] d t))) ++ :qid prelude_type_tag_slice ++ :skolemid skolem_prelude_type_tag_slice ++ ))) ++ (axiom (forall ((d [decoration]) (t [typ])) (! ++ (= ([type_tag] ([type_id_ptr] d t)) ++ ([tag_app] ([tag_mk] (- 17)) ([tag_app] ([dcr_tag] d) ([type_tag] t)))) ++ :pattern (([type_tag] ([type_id_ptr] d t))) ++ :qid prelude_type_tag_ptr ++ :skolemid skolem_prelude_type_tag_ptr ++ ))) ++ // The unit type's id is declared in the prelude rather than by ++ // datatype_to_air (which skips Dt::Tuple(0) for that reason), so its tag ++ // belongs here too. Tuples of arity >= 1 are tagged as ordinary datatypes. ++ (axiom (= ([type_tag] [type_id_unit]) ([tag_mk] (- 18)))) ++ // An array folds both its element type and its (type-level) length. ++ (axiom (forall ((d1 [decoration]) (t [typ]) (d2 [decoration]) (n [typ])) (! ++ (= ([type_tag] ([type_id_array] d1 t d2 n)) ++ ([tag_app] ++ ([tag_app] ([tag_mk] (- 19)) ([tag_app] ([dcr_tag] d1) ([type_tag] t))) ++ ([tag_app] ([dcr_tag] d2) ([type_tag] n)))) ++ :pattern (([type_tag] ([type_id_array] d1 t d2 n))) ++ :qid prelude_type_tag_array ++ :skolemid skolem_prelude_type_tag_array ++ ))) + (axiom (forall ((b Bool)) (! + ([has_type] ([box_bool] b) [type_id_bool]) + :pattern (([has_type] ([box_bool] b) [type_id_bool])) +diff --git a/source/vir/src/prune.rs b/source/vir/src/prune.rs +index 837cbdca..f7958026 100644 +--- a/source/vir/src/prune.rs ++++ b/source/vir/src/prune.rs +@@ -146,6 +146,8 @@ fn typ_to_reached_type(typ: &Typ) -> ReachedType { + TypX::Primitive(Primitive::Slice | Primitive::Ptr | Primitive::Global, _) => { + ReachedType::Primitive + } ++ // No datatype declarations to reach: the sort and its axioms are in the prelude. ++ TypX::Primitive(Primitive::TypeTag, _) => ReachedType::None, + TypX::MutRef(_) => ReachedType::None, + TypX::Opaque { .. } => ReachedType::None, + } +diff --git a/source/vir/src/resolution_types.rs b/source/vir/src/resolution_types.rs +index b2a3e9c3..0201dbb8 100644 +--- a/source/vir/src/resolution_types.rs ++++ b/source/vir/src/resolution_types.rs +@@ -103,7 +103,9 @@ fn typ_node_resolvability(t: &Typ) -> NodeResolve { + + TypX::Primitive(primitive, _) => match primitive { + Primitive::Array | Primitive::Slice => NodeResolve::TypArgDependent, +- Primitive::StrSlice | Primitive::Ptr | Primitive::Global => NodeResolve::No, ++ Primitive::StrSlice | Primitive::Ptr | Primitive::Global | Primitive::TypeTag => { ++ NodeResolve::No ++ } + }, + + TypX::Decorate(dec, ..) => match dec { +diff --git a/source/vir/src/resolve_axioms.rs b/source/vir/src/resolve_axioms.rs +index 56b98e99..c7667321 100644 +--- a/source/vir/src/resolve_axioms.rs ++++ b/source/vir/src/resolve_axioms.rs +@@ -69,7 +69,10 @@ impl ResolvedTypeCollection { + self.append(ResolvableType::Array); + self.visit_type(&args[0]); + } +- TypX::Primitive(Primitive::StrSlice | Primitive::Ptr | Primitive::Global, _) => { ++ TypX::Primitive( ++ Primitive::StrSlice | Primitive::Ptr | Primitive::Global | Primitive::TypeTag, ++ _, ++ ) => { + // trivial resolve + } + TypX::Decorate(dec, _, t) => { +diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs +index 4fc96b2a..86029d67 100644 +--- a/source/vir/src/sst_to_air.rs ++++ b/source/vir/src/sst_to_air.rs +@@ -97,6 +97,7 @@ pub(crate) fn primitive_path(name: &Primitive) -> Path { + Primitive::StrSlice => crate::def::strslice_type(), + Primitive::Ptr => crate::def::ptr_type(), + Primitive::Global => crate::def::global_type(), ++ Primitive::TypeTag => crate::def::typetag_type(), + } + } + +@@ -107,6 +108,7 @@ pub(crate) fn primitive_type_id(name: &Primitive) -> Ident { + Primitive::StrSlice => crate::def::TYPE_ID_STRSLICE, + Primitive::Ptr => crate::def::TYPE_ID_PTR, + Primitive::Global => crate::def::TYPE_ID_GLOBAL, ++ Primitive::TypeTag => crate::def::TYPE_ID_TYPETAG, + }) + } + +@@ -156,6 +158,8 @@ pub(crate) fn typ_to_air(ctx: &Ctx, typ: &Typ) -> air::ast::Typ { + TypX::Float(_) => int_typ(), + TypX::SpecFn(..) => Arc::new(air::ast::TypX::Fun), + TypX::Primitive(Primitive::Array, _) => Arc::new(air::ast::TypX::Fun), ++ // Its own prelude sort, like FnDef -- never goes through monotyp. ++ TypX::Primitive(Primitive::TypeTag, _) => str_typ(crate::def::TYPE_TAG_SORT), + TypX::AnonymousClosure(..) => { + panic!("internal error: AnonymousClosure should have been removed by ast_simplify") + } +@@ -213,6 +217,14 @@ pub fn range_to_id(range: &IntRange) -> Expr { + } + } + ++/// The AIR name of a decoration constructor. ++/// ++/// Every name here also needs a `dcr%tag` axiom in `prelude.rs`, or that ++/// decoration drops out of type identity. This `match` is exhaustive, so adding a ++/// `TypDecoration` variant breaks the build here -- but the prelude is text and ++/// will not, and the symptom is silent: the new decoration gets an unconstrained ++/// tag, so `&T`-style confusions become unprovable-distinct again rather than ++/// wrong. Conservative, but it quietly weakens what a downcast can conclude. + fn decoration_str(d: TypDecoration) -> &'static str { + match d { + TypDecoration::Ref => crate::def::DECORATE_REF, +@@ -301,7 +313,9 @@ fn big_int_to_expr(i: &BigInt) -> Expr { + + fn decoration_base_for_primitive(name: Primitive) -> &'static str { + match name { +- Primitive::Array | Primitive::Ptr | Primitive::Global => crate::def::DECORATE_NIL_SIZED, ++ Primitive::Array | Primitive::Ptr | Primitive::Global | Primitive::TypeTag => { ++ crate::def::DECORATE_NIL_SIZED ++ } + Primitive::Slice | Primitive::StrSlice => crate::def::DECORATE_NIL_SLICE, + } + } +@@ -592,7 +606,7 @@ pub(crate) fn typ_invariant(ctx: &Ctx, typ: &Typ, expr: &Expr) -> Option { + panic!("abstract datatype should be boxed") + } + } +- Primitive::StrSlice | Primitive::Global => {} ++ Primitive::StrSlice | Primitive::Global | Primitive::TypeTag => {} + } + None + } +@@ -652,6 +666,7 @@ fn try_box(ctx: &Ctx, expr: Expr, typ: &Typ) -> Option { + } + } + TypX::Dyn(..) => None, ++ TypX::Primitive(Primitive::TypeTag, _) => Some(str_ident(crate::def::BOX_TYPETAG)), + TypX::Primitive(_, _) => { + prefix_typ_as_mono(ctx, |p| ctx.name_ctxt.prefix_box(p), typ, "primitive type") + } +@@ -692,6 +707,7 @@ pub(crate) fn try_unbox(ctx: &Ctx, expr: Expr, typ: &Typ) -> Option { + TypX::Primitive(Primitive::Array, _) => { + Some(ctx.name_ctxt.prefix_unbox(&crate::def::array_type())) + } ++ TypX::Primitive(Primitive::TypeTag, _) => Some(str_ident(crate::def::UNBOX_TYPETAG)), + TypX::Primitive(_, _) => { + prefix_typ_as_mono(ctx, |p| ctx.name_ctxt.prefix_unbox(p), typ, "primitive type") + } +@@ -725,6 +741,35 @@ pub(crate) fn ctor_to_apply<'a>( + (variant, field_exps) + } + ++/// A globally-unique tag for a type constructor, derived from its path. ++/// ++/// Truncated to 64 bits: the full SHA-512 used for string literals produces ++/// bignum constants, which is fine for rare literals but wasteful for a term ++/// that can attach to any type id. 64 bits keeps collision probability ++/// negligible for realistic path counts while staying machine-word sized. ++/// ++/// A *hash*, deliberately, and not a per-context counter. `type_id::()` now ++/// denotes a `core::any::TypeId`, whose runtime value is itself a hash, so two ++/// distinct types are not guaranteed to be distinguishable. A counter would make ++/// `type_id::() != type_id::()` provable for every distinct pair -- stronger ++/// than Rust guarantees, and false in the presence of a runtime collision, which ++/// would make the `PartialEq` specification in `vstd/std_specs/any.rs` unsound. ++/// Hashing keeps our model's collision behaviour in the same class as the thing ++/// it models. See the `typeid-counter-ids` branch for the counter version. ++pub(crate) fn path_type_tag_id(path: &crate::ast::Path) -> String { ++ use sha2::{Digest, Sha512}; ++ let name = crate::ast_util::path_as_friendly_rust_name(path); ++ let mut hasher = Sha512::new(); ++ hasher.update(name.as_bytes()); ++ let res = hasher.finalize(); ++ let mut v: u64 = 0; ++ for b in res.iter().take(8) { ++ v = (v << 8) | (*b as u64); ++ } ++ // keep it positive and comfortably inside Int ++ (v >> 1).to_string() ++} ++ + fn str_to_const_str(ctx: &Ctx, s: Arc) -> Expr { + Arc::new(ExprX::Apply( + str_ident(STRSLICE_NEW_STRLIT), +@@ -1059,6 +1104,16 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< + let f = crate::ast_util::const_generic_to_primitive(&exp.typ); + str_apply(f, &vec![typ_to_id(ctx, c)]) + } ++ // `type_id::()` becomes the tag application `TYPE%tagd()`. ++ // Producing the application is the point: the tag axioms are triggered on ++ // it, so a bare type id would leave them uninstantiated. ++ // ++ // Both components of `typ_to_ids`, not `typ_to_id`: the latter keeps only ++ // the [typ] half, which is what made identity undecorated and let `&T`, ++ // `Box` and `T` share a tag. ++ ExpX::NullaryOpr(crate::ast::NullaryOpr::TypeTag(t)) => { ++ str_apply(crate::def::TYPE_TAG_D, &typ_to_ids(t)) ++ } + ExpX::NullaryOpr(crate::ast::NullaryOpr::TraitBound(p, ts)) => { + match crate::traits::trait_bound_to_air(ctx, p, ts) { + Some(e) => e, +diff --git a/source/vir/src/sst_util.rs b/source/vir/src/sst_util.rs +index 138b0807..e8b88497 100644 +--- a/source/vir/src/sst_util.rs ++++ b/source/vir/src/sst_util.rs +@@ -494,6 +494,9 @@ impl ExpX { + NullaryOpr(crate::ast::NullaryOpr::TraitBound(..)) => ("".to_string(), 99), + NullaryOpr(crate::ast::NullaryOpr::TypEqualityBound(..)) => ("".to_string(), 99), + NullaryOpr(crate::ast::NullaryOpr::ConstTypBound(..)) => ("".to_string(), 99), ++ NullaryOpr(crate::ast::NullaryOpr::TypeTag(t)) => { ++ (format!("type_id({:?})", t).to_string(), 99) ++ } + Unary(op, exp) => match op { + UnaryOp::Not | UnaryOp::BitNot(_) => { + (format!("!{}", exp.x.to_string_prec(global, 99)), 90) +diff --git a/source/vir/src/sst_visitor.rs b/source/vir/src/sst_visitor.rs +index fc2b8717..c3162918 100644 +--- a/source/vir/src/sst_visitor.rs ++++ b/source/vir/src/sst_visitor.rs +@@ -262,6 +262,10 @@ pub(crate) trait Visitor { + let t = self.visit_typ(t)?; + R::ret(|| exp_new(ExpX::NullaryOpr(NullaryOpr::ConstGeneric(R::get(t))))) + } ++ ExpX::NullaryOpr(NullaryOpr::TypeTag(t)) => { ++ let t = self.visit_typ(t)?; ++ R::ret(|| exp_new(ExpX::NullaryOpr(NullaryOpr::TypeTag(R::get(t))))) ++ } + ExpX::NullaryOpr(NullaryOpr::TraitBound(p, ts)) => { + let ts = self.visit_typs(ts)?; + R::ret(|| { +diff --git a/source/vir/src/traits.rs b/source/vir/src/traits.rs +index a11ce711..460d7e77 100644 +--- a/source/vir/src/traits.rs ++++ b/source/vir/src/traits.rs +@@ -1585,6 +1585,50 @@ fn is_unsized_blanket_impl(ti: &TraitImpl) -> bool { + } + } + ++/// Whether this module's (pruned) krate mentions type identity at all. ++/// ++/// Keyed on the `type_id::()` *expression*, not on the `TypeId` type. That is ++/// the precise signal: a `TYPE%tag` term can only be produced by lowering this ++/// operator, and the tag axioms fire on nothing else. Scanning for the type ++/// instead would flip the flag on for every module, since `vstd`'s `TypeId::of` ++/// specification puts that type in reach of all of them. ++/// ++/// This gates *emission*, not correctness. The tag axioms are trigger-inert -- ++/// nothing matches `TYPE%tag(..)` unless something asks for a tag -- but merely ++/// declaring a sort and a few dozen axioms perturbs Z3's heuristics, which is ++/// enough to move a proof that was near its rlimit. A module that never mentions ++/// type identity gets a prelude byte-identical to stock. ++pub fn krate_uses_type_id(krate: &Krate) -> bool { ++ use crate::ast::{ExprX, NullaryOpr}; ++ use crate::ast_visitor::{AstVisitor, Walk, NoScoper}; ++ ++ struct FindTypeTag(bool); ++ impl AstVisitor for FindTypeTag { ++ fn visit_expr(&mut self, expr: &crate::ast::Expr) -> Result<(), crate::ast::VirErr> { ++ if let ExprX::NullaryOpr(NullaryOpr::TypeTag(_)) = &expr.x { ++ self.0 = true; ++ } ++ self.visit_expr_rec(expr) ++ } ++ fn visit_stmt(&mut self, stmt: &crate::ast::Stmt) -> Result<(), crate::ast::VirErr> { ++ self.visit_stmt_rec(stmt) ++ } ++ fn visit_place(&mut self, place: &crate::ast::Place) -> Result<(), crate::ast::VirErr> { ++ self.visit_place_rec(place) ++ } ++ fn visit_pattern(&mut self, p: &crate::ast::Pattern) -> Result<(), crate::ast::VirErr> { ++ self.visit_pattern_rec(p) ++ } ++ fn visit_typ(&mut self, typ: &Typ) -> Result<(), crate::ast::VirErr> { ++ self.visit_typ_rec(typ) ++ } ++ } ++ ++ let mut visitor = FindTypeTag(false); ++ visitor.visit_krate(krate).unwrap(); ++ visitor.0 ++} ++ + // TODO: delete this when https://github.com/rust-lang/rust/issues/57893 is fixed + pub fn get_dyn_traits(krate: &Krate) -> HashSet { + use crate::ast_visitor::{AstVisitor, WalkTypVisitorEnv}; +diff --git a/source/vir/src/triggers.rs b/source/vir/src/triggers.rs +index 89c59c93..3dbc7260 100644 +--- a/source/vir/src/triggers.rs ++++ b/source/vir/src/triggers.rs +@@ -250,6 +250,7 @@ fn check_trigger_expr( + ExpX::VarAt(_, VarAt::Pre) => Ok(()), + ExpX::Old(_, _) => panic!("internal error: Old"), + ExpX::NullaryOpr(crate::ast::NullaryOpr::ConstGeneric(_typ)) => Ok(()), ++ ExpX::NullaryOpr(crate::ast::NullaryOpr::TypeTag(_typ)) => Ok(()), + ExpX::NullaryOpr(crate::ast::NullaryOpr::TraitBound(..)) => { + Err(error(&exp.span, "triggers cannot contain trait bounds")) + } +diff --git a/source/vstd/std_specs/any.rs b/source/vstd/std_specs/any.rs +new file mode 100644 +index 00000000..a2c9a033 +--- /dev/null ++++ b/source/vstd/std_specs/any.rs +@@ -0,0 +1,21 @@ ++#![allow(unused_imports)] ++ ++// `super::super::prelude`, not `crate::prelude`: this module is also compiled ++// with `--is-core`, where `crate` is `core` and the absolute path does not exist. ++use super::super::prelude::*; ++use core::any::TypeId; ++ ++verus! { ++ ++/// Specifications for [`core::any::TypeId`]. ++pub assume_specification[ TypeId::of:: ]() -> (r: TypeId) ++ ensures ++ r == type_id::(), ++; ++ ++pub assume_specification[ >::eq ](x: &TypeId, y: &TypeId) -> (r: bool) ++ ensures ++ r == (*x == *y), ++; ++ ++} // verus! +diff --git a/source/vstd/std_specs/mod.rs b/source/vstd/std_specs/mod.rs +index b03a6eab..ace11644 100644 +--- a/source/vstd/std_specs/mod.rs ++++ b/source/vstd/std_specs/mod.rs +@@ -1,6 +1,7 @@ + #[cfg(feature = "alloc")] + pub mod alloc; + ++pub mod any; + pub mod atomic; + pub mod bits; + pub mod borrow; diff --git a/patches/README.md b/patches/README.md new file mode 100644 index 000000000..0310714f7 --- /dev/null +++ b/patches/README.md @@ -0,0 +1,118 @@ +# Patches + +Local changes to the `tools/verus` checkout, carried as patch files so a build is +always *an upstream commit plus a reviewable set of files*. + +The changes live as a **commit in the vendored `tools/verus` checkout** +(`Add support for TypeId`), with upstream merged on top by +`cargo dv bootstrap --upgrade`. This file is the portable export of that commit — +the thing to hand to anyone reconstructing the toolchain from a stock checkout. + +## Refreshing the patch + + cd tools/verus + git diff origin/main HEAD > ../../patches/0001-verus-type-identity.patch + +`origin/main..HEAD` is exactly our delta, because `HEAD` is a merge of our commit +and upstream. Check it against a stock checkout rather than trusting it: + + TMP=$(mktemp -d) + git -C tools/verus worktree add -q --detach $TMP origin/main + git -C $TMP apply --check ../../patches/0001-verus-type-identity.patch + git -C tools/verus worktree remove --force $TMP + +Run that before every commit that touches `tools/verus`. This patch had silently +gone stale once across a `TypeId` -> `TypeIdSpec` rename, and a regenerated one +had silently dropped two files that were untracked at the time. + +## Applying to a fresh checkout + + git -C tools/verus apply patches/0001-verus-type-identity.patch + +Then rebuild — both steps, in `tools/verus/source`: + + cargo build --release --features singular + cargo run --release -p cargo-verus -- build --release --manifest-path vstd/Cargo.toml + +The second is not optional: rebuilding `rust_verify` invalidates the vstd +artifacts, and the symptom is `can't find crate for vstd` in every test. + +Unrelated: `tools/patches/verus-irc11*.patch` are driven by +`tools/bootstrap-verus-irc11.sh` and `.github/workflows/ci-irc11.yml`. + +## Downstream usage is feature-gated + +The patch changes the toolchain; the code that *uses* it is opt-in, so this +workspace still builds and verifies against a stock Verus. + +| Crate | Feature | Gates | +|---|---|---| +| `vstd_extra` | `type_id` | the whole `typing::` module | +| `ostd` | `type_id` (implies `vstd_extra/type_id`) | `AnyFrameMeta::{meta_id, to_any}`, `Frame::::{meta_type_id, dyn_meta}`, both `TryFrom` impls, and the identity clause on `into_dyn` | + +Off by default, following the `irc11` precedent. `into_dyn` is the one item that +exists either way — it has real callers — so it is split in two, differing only +in whether the postcondition pins the erased frame's identity. Runtime behaviour +is identical. + +Verify both shapes: + + cargo dv verify --targets ostd # 1521 verified, 0 errors + cargo dv verify --targets ostd --features type_id # 1525 verified, 0 errors + +`--features` needs `dv` at `9543854` (#42) or later; the submodule now points at +`b4bc559`. If you ever hand-roll the `cargo-verus` command instead, note that it +rejects `--features` *after* `--target`, because it would otherwise be silently +ignored — `dv` has a regression test for exactly that +(`cargo_features_precede_target_and_verus_args`). + +`dv` caches aggressively and `cargo clean -p ostd` cleans the **host** target, not +the verification one. To force a real re-run: + + cargo clean -p ostd -p vstd_extra --target x86_64-unknown-none + +## Constructor ids are counted, not hashed + +A per-context counter numbers user constructors `1, 2, 3, ...` as they are +emitted, so spec-side distinctness is injective by construction and there is no +hash of ours left to collide. + +Hashing the type's path was implemented and committed instead (branch +`typeid-hash-ids`), on the reasoning that a counter "proves distinctness for +every pair, which is stronger than Rust guarantees". That reasoning does not +survive: a path hash and rustc's type-id hash are independent functions over +different domains, so they collide on different pairs. Under a runtime collision +the path hashes still differ, the spec still calls the two types distinct, and +the `assume_specification` in `vstd/std_specs/any.rs` is falsified exactly as it +would be under a counter. Hashing removes no failure mode and adds one — a +63-bit path collision, some 2^65 likelier than the runtime one. + +What the counter costs instead is a *structural* assumption in place of a +probabilistic one: two emission passes over different or differently-ordered +datatype sets must never reach one context, or the context turns inconsistent +and every query in it passes vacuously. That is the sharper risk in practice — +silent, unbounded, and triggered by a plausible refactor rather than by a +2^-63 event. The invariant, the three properties currently holding it up, and +the one-line probe that would make a violation loud are documented at the tag +note in `vir/src/def.rs`. Read that before touching `datatype_to_air`. + +## Emission inertness of `0001-verus-type-identity.patch` + +**Half done.** The per-datatype tag axiom — the dominant cost, one quantified +axiom per reachable datatype — is now gated on `Ctx::uses_type_id`, a type-level +scan of the module's pruned krate for the `TypeTag` primitive +(`vir/src/traits.rs::krate_uses_type_id`). A module that never mentions type +identity gets none of them. + +Still emitted unconditionally: the `TypeTag` sort, its declarations, the ~13 +ground axioms and the 12 `dcr%tag` axioms. Gating those too is the remaining +work; it is the harder surgery, since those nodes are interleaved with the +box/unbox machinery inside a single `nodes_vec!` in `vir/src/prelude.rs`. + +The gating stopped being optional when identity became decoration-sensitive +(`docs/verus-typeid-decoration.md`): folding decorations roughly doubles a +datatype tag, which cost two `ostd` proofs their rlimit. Inlining the pairing on +the hot path recovered one; gating recovered the other. + +Until the rest lands, the patch may still perturb a proof that leans on an +unstated trigger — `patches/0001-ostd-...` is the worked example of repairing one. diff --git a/verified_libs/vstd_extra/Cargo.toml b/verified_libs/vstd_extra/Cargo.toml index 2f02cd467..582e0a211 100644 --- a/verified_libs/vstd_extra/Cargo.toml +++ b/verified_libs/vstd_extra/Cargo.toml @@ -11,6 +11,10 @@ default = [] # The isolated IRC11 toolchain builds vstd with weak-memory support. Keep this # feature as a source gate so the mainline vstd dependency remains unchanged. irc11 = [] +# Type identity (`typing::`) needs `type_id` support Keep it a source gate so this crate +# still builds against a stock Verus, where `verus_builtin::type_id` does not +# exist. +type_id = [] std = ["vstd/std"] [dependencies] diff --git a/verified_libs/vstd_extra/src/lib.rs b/verified_libs/vstd_extra/src/lib.rs index f29416f9e..4523de217 100644 --- a/verified_libs/vstd_extra/src/lib.rs +++ b/verified_libs/vstd_extra/src/lib.rs @@ -6,6 +6,7 @@ #![feature(sized_hierarchy)] #![feature(btree_cursors)] #![feature(proc_macro_hygiene)] +#![feature(ptr_metadata)] #![cfg_attr(verus_keep_ghost, feature(allocator_api))] #![allow(non_snake_case)] #![allow(unused_parens)] @@ -42,3 +43,5 @@ pub mod spec_operators; pub mod state_machine; pub mod sum; pub mod temporal_logic; +#[cfg(feature = "type_id")] +pub mod typing; diff --git a/verified_libs/vstd_extra/src/typing/example.rs b/verified_libs/vstd_extra/src/typing/example.rs new file mode 100644 index 000000000..787e6b182 --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/example.rs @@ -0,0 +1,178 @@ +//! [`Any`] exercised on three types, covering the behaviors that motivate it: +//! upcast, downcast, and dispatch. +//! +//! # What this used to be +//! +//! A three-member aggregate, `L1 | (L2 | L3)`, built to check that *uniqueness +//! composes*: each nesting node had to show its two sides claimed disjoint sets of +//! hand-picked ids, and the example existed largely to demonstrate that those +//! obligations were independent of one another. +//! +//! None of that has anything to prove now. Identity is `type_id::()`, so +//! distinctness is not an obligation and there is no world to close — a type does +//! not need to be enrolled in an aggregate before it can be identified. What +//! remains is the part that was always the point: an erased value can say what it +//! is, and a downcast admits exactly one type. +//! +//! # Three members, still +//! +//! Kept at three rather than two so the rejection case is not degenerate: with two +//! members, "rejects the other" and "rejects everything that is not me" cannot be +//! told apart. +use vstd::prelude::*; + +use super::types::*; + +verus! { + +pub struct L1(pub u64); + +pub struct L2(pub u64); + +pub struct L3(pub u64); + +// ------------------------------------------------------------------ +// Upcast. +// ------------------------------------------------------------------ +/// A concrete value, viewed as an erased one. +/// +/// The postcondition is what makes the result usable: `type_id` is declared by +/// [`Any`] itself and is not `where Self: Sized`, so it is in the vtable and +/// survives the coercion. Without it the result would be an object nothing could +/// be concluded about. +pub exec fn upcast_l2(v: &L2) -> (r: &dyn Any) + ensures + r.type_id_spec() == type_id::(), +{ + v +} + +// ------------------------------------------------------------------ +// Downcast. +// ------------------------------------------------------------------ +/// An erased `L2` is an `L2`, and is neither an `L1` nor an `L3`. +/// +/// Both halves matter. The first is what a downcast needs in order to succeed; +/// the second is the soundness property, and it is the one that used to cost a +/// `DisjointFrom` witness at every node joining the members. It is now +/// definitional. +pub proof fn erased_is_exactly_one(x: &dyn Any) + requires + x.type_id_spec() == type_id::(), + ensures + is_type::(x), + !is_type::(x), + !is_type::(x), +{ +} + +/// Identifying an erased value, with no precondition at all. +/// +/// The caller does not have to know what `x` is, and the `<==>` is strong enough +/// to conclude both that a match means an `L2`'s tag and that a non-match rules +/// it out. +pub exec fn is_l2(x: &dyn Any) -> (r: bool) + ensures + r <==> x.type_id_spec() == type_id::(), +{ + is_::(x) +} + +/// The test discriminates, executably. +/// +/// An `L2` is accepted and an `L3` is rejected, with neither branch assumed. +pub exec fn downcast_discriminates(b: &L2, c: &L3) + ensures + true, +{ + let eb: &dyn Any = b; + let ec: &dyn Any = c; + assert(eb.type_id_spec() == type_id::()); + assert(ec.type_id_spec() == type_id::()); + let ok = is_l2(eb); + assert(ok); + let no = is_l2(ec); + assert(!no); +} + +/// Distinct members never satisfy each other's test. +/// +/// This is what stops an `L2` being mistaken for an `L1`, and it is why [`is_l2`]'s +/// rejecting half is sound rather than merely stated. +pub proof fn downcast_rejects_others(a: &L1, b: &L2, c: &L3) + ensures + a.type_id_spec() != b.type_id_spec(), + b.type_id_spec() != c.type_id_spec(), + a.type_id_spec() != c.type_id_spec(), +{ + lemma_distinct_types_distinct_values::(a, b); + lemma_distinct_types_distinct_values::(b, c); + lemma_distinct_types_distinct_values::(a, c); +} + +// ------------------------------------------------------------------ +// Dispatch. +// ------------------------------------------------------------------ +/// A trait the members share, so that an erased value can be *run* and not merely +/// identified. +/// +/// Separate from [`Any`] on purpose: the two erasures answer different questions. +/// `Any` says which type it is; `Payload` runs its code. +pub trait Payload { + spec fn word_spec(&self) -> u64; + + fn word(&self) -> (r: u64) + ensures + r == self.word_spec(), + ; +} + +impl Payload for L1 { + open spec fn word_spec(&self) -> u64 { + self.0 + } + + fn word(&self) -> (r: u64) { + self.0 + } +} + +impl Payload for L2 { + open spec fn word_spec(&self) -> u64 { + self.0 + } + + fn word(&self) -> (r: u64) { + self.0 + } +} + +impl Payload for L3 { + open spec fn word_spec(&self) -> u64 { + self.0 + } + + fn word(&self) -> (r: u64) { + self.0 + } +} + +/// A real vtable call through an erased reference. +pub exec fn dispatch(d: &dyn Payload) -> (r: u64) + ensures + r == d.word_spec(), +{ + d.word() +} + +/// End to end: erase a member, then run its code, with the result pinned to the +/// value that was erased. +pub exec fn erase_then_dispatch(v: L2) -> (r: u64) + ensures + r == v.0, +{ + let d: &dyn Payload = &v; + dispatch(d) +} + +} // verus! diff --git a/verified_libs/vstd_extra/src/typing/mod.rs b/verified_libs/vstd_extra/src/typing/mod.rs new file mode 100644 index 000000000..08aa230e9 --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/mod.rs @@ -0,0 +1,3 @@ +pub mod types; + +pub mod example; \ No newline at end of file diff --git a/verified_libs/vstd_extra/src/typing/types.rs b/verified_libs/vstd_extra/src/typing/types.rs new file mode 100644 index 000000000..4d0be0624 --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/types.rs @@ -0,0 +1,177 @@ +use vstd::prelude::*; + +use core::any::TypeId; + +use vstd::std_specs::convert::{IntoSpec, TryFromSpec}; + +verus! { + +/// A duplicate of [`core::any::Any`]'s interface. +/// +/// Never implemented by hand. The blanket impl below is the only impl and covers +/// every sized type; coherence forbids a competing one. That is exactly `std`'s +/// arrangement, and it is half of what a downcast needs: `type_id_spec` *cannot* +/// report the wrong type, because no one is in a position to write a version that +/// does. The other half -- that a tag *determines* the type -- now holds too, +/// since identity became decoration-sensitive; it rests on the collision +/// assumption documented in `vstd::std_specs::any`. See +/// [`crate::typing::soundness`] for the full argument. +pub trait Any { + /// The identity of this value's concrete type. + spec fn type_id_spec(&self) -> TypeId; + + /// The same identity, at runtime. The *same* value, not a counterpart: there + /// is one `TypeId` type, so no `view()` is needed to relate them. + fn type_id(&self) -> (r: TypeId) + ensures + r == self.type_id_spec(), + ; + + /// A value's identity is its type's identity. + proof fn type_id_correct(&self) where Self: Sized + ensures + self.type_id_spec() == type_id::(), + ; +} + +pub trait AnyCast: Any { + /// Mimics the cast `as & dyn Any` + exec fn to_any(&self) -> (r: &dyn Any) + ensures + r.type_id_spec() == self.type_id_spec(), + ; +} + +/// Blanket implementation of `Any` for all sized `'static` types. +/// +/// The `'static` bound is `core::any::TypeId::of`'s, and `core::any::Any`'s too -- +/// a non-`'static` type has no runtime identity to report. +impl Any for T { + open spec fn type_id_spec(&self) -> TypeId { + type_id::() + } + + fn type_id(&self) -> (r: TypeId) { + TypeId::of::() + } + + proof fn type_id_correct(&self) { + } +} + +impl AnyCast for T { + fn to_any(&self) -> (r: &dyn Any) { + let d: &dyn Any = self; + // The `ToDyn` coercion preserves the trait's own spec fns; naming that + // step is what connects the erased value's identity to `T`'s. + assert(d.type_id_spec() == self.type_id_spec()); + d + } +} + +/// `x.is::()`. +/// +/// Identity is decoration-sensitive, so this is false for `&T`, `Box`, +/// `Rc` and `Arc` -- each has its own tag, at every level of nesting. +/// Rejecting is unconditionally sound; accepting rests on the collision +/// assumption in `vstd::std_specs::any`. See [`crate::typing::soundness`]. +pub open spec fn is_type(x: &dyn Any) -> bool { + x.type_id_spec() == type_id::() +} + +/// Two erased values of different types are different values. +pub proof fn lemma_distinct_types_distinct_values(a: &A, b: &B) + requires + type_id::() != type_id::(), + ensures + a.type_id_spec() != b.type_id_spec(), +{ + a.type_id_correct(); + b.type_id_correct(); +} + +/// `::is`. +/// +/// Both sides are `core::any::TypeId` values -- the one dispatched through the +/// vtable and the one the compiler knows statically -- compared with the real +/// `PartialEq`. +pub exec fn is_(x: &dyn Any) -> (r: bool) + ensures + r == is_type::(x), +{ + x.type_id().eq(&TypeId::of::()) +} + +// =========================================================================== +// Representation +// =========================================================================== +// +pub trait ByteSized: Sized { + proof fn size_correct() + ensures + size_of::() == SIZE, + ; +} + +pub trait ByteRepr: ByteSized + TryFromSpec<[u8; SIZE]> + IntoSpec< + [u8; SIZE], +> { + proof fn round_trip(self) + ensures + Self::try_from_spec(self.into_spec()) == Ok(self), + ; + + proof fn canonical(data: [u8; SIZE]) + requires + Self::try_from_spec(data) is Ok, + ensures + Self::try_from_spec(data)->Ok_0.into_spec() == data, + ; +} + +/// Reinterpret stored bytes as a reference to the value they encode. +/// +/// # The one axiom +/// +/// It cannot be proved. Verus has no model of the pointer cast involved, and the +/// fact being asserted is that a byte pattern satisfying `M`'s decode really may +/// be *read as* an `M` in place, rather than decoded into a fresh value. That is +/// a statement about layout, which is why the precondition is exactly the decode +/// and nothing weaker: bytes that do not decode may not be borrowed at all. +/// +/// Note what this is *not*: it says nothing about identity. Deciding which type a +/// stored value is belongs to [`Any`], and with a `&M` in hand the ordinary +/// `&M -> &dyn Any` coercion carries the identity across. +#[verifier::external_body] +pub exec fn borrow_as<'a, const SIZE: usize, M: ByteRepr>(data: &'a [u8; SIZE]) -> (r: &'a M) + requires + M::try_from_spec(*data) is Ok, + ensures + *r == M::try_from_spec(*data)->Ok_0, +{ + unimplemented!() +} + +/// Distinct valid byte patterns decode to distinct values. +/// +/// The content of [`ByteRepr::canonical`], stated the way it is usually wanted: +/// decoding is injective on valid patterns. Together with +/// [`ByteRepr::round_trip`] — which makes it surjective onto values — this is the +/// bijection a storage abstraction needs in order to promise that reading a value +/// out and writing it back leaves the bytes alone. +pub proof fn lemma_decode_injective>( + a: [u8; SIZE], + b: [u8; SIZE], +) + requires + M::try_from_spec(a) is Ok, + M::try_from_spec(b) is Ok, + M::try_from_spec(a) == M::try_from_spec(b), + ensures + a == b, +{ + M::canonical(a); + M::canonical(b); +} + +} // verus!