From 2668fa08a48040a44df2f8632c4ea8b2d65ed6b0 Mon Sep 17 00:00:00 2001 From: Sean Anderson Date: Sun, 23 Aug 2026 00:27:31 -0700 Subject: [PATCH 1/7] Verus type id support patch --- patches/0001-verus-type-identity.patch | 948 +++++++++++++++++++++++++ 1 file changed, 948 insertions(+) create mode 100644 patches/0001-verus-type-identity.patch diff --git a/patches/0001-verus-type-identity.patch b/patches/0001-verus-type-identity.patch new file mode 100644 index 000000000..be8751944 --- /dev/null +++ b/patches/0001-verus-type-identity.patch @@ -0,0 +1,948 @@ +diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs +index 8fceab37..48434b7b 100644 +--- a/source/builtin/src/lib.rs ++++ b/source/builtin/src/lib.rs +@@ -2322,6 +2322,22 @@ pub fn arch_word_bits() -> nat { + unimplemented!(); + } + ++/// ++/// Dynamic type id, as in `std::any`. ++/// ++#[cfg(verus_keep_ghost)] ++#[rustc_diagnostic_item = "verus::verus_builtin::TypeId"] ++#[verifier::external_body] ++pub struct TypeId { ++ _private: (), ++} ++ ++#[cfg(verus_keep_ghost)] ++#[rustc_diagnostic_item = "verus::verus_builtin::type_id"] ++pub fn type_id() -> 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 542ea83d..a2ca91d6 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 6a7c43ae..2a848670 100644 +--- a/source/rust_verify/src/rust_to_vir_base.rs ++++ b/source/rust_verify/src/rust_to_vir_base.rs +@@ -1129,6 +1129,8 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>( + (Arc::new(TypX::Int(IntRange::Nat)), false) + } else if let Some(VerusItem::BuiltinType(BuiltinTypeItem::Real)) = verus_item { + (Arc::new(TypX::Real), false) ++ } else if let Some(VerusItem::BuiltinType(BuiltinTypeItem::TypeId)) = verus_item { ++ (Arc::new(TypX::Primitive(Primitive::TypeTag, Arc::new(vec![]))), false) + } else { + let rust_item = verus_items::get_rust_item(tcx, did); + +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 689a1df6..45d61997 100644 +--- a/source/rust_verify/src/verus_items.rs ++++ b/source/rust_verify/src/verus_items.rs +@@ -144,6 +144,7 @@ pub(crate) enum ExprItem { + StrSliceLen, + StrSliceGetChar, + ArchWordBits, ++ TypeId, + ClosureToFnSpec, + ClosureToFnProof, + SignedMin, +@@ -405,6 +406,7 @@ pub(crate) enum BuiltinTypeItem { + FnSpec, + Ghost, + Tracked, ++ TypeId, + } + + #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] +@@ -538,6 +540,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)), +@@ -745,6 +748,7 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { + ("verus::verus_builtin::FnSpec", VerusItem::BuiltinType(BuiltinTypeItem::FnSpec)), + ("verus::verus_builtin::Ghost", VerusItem::BuiltinType(BuiltinTypeItem::Ghost)), + ("verus::verus_builtin::Tracked", VerusItem::BuiltinType(BuiltinTypeItem::Tracked)), ++ ("verus::verus_builtin::TypeId", VerusItem::BuiltinType(BuiltinTypeItem::TypeId)), + + ("verus::verus_builtin::Integer", VerusItem::BuiltinTrait(BuiltinTraitItem::Integer)), + ("verus::verus_builtin::Chainable", VerusItem::BuiltinTrait(BuiltinTraitItem::Chainable)), +diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs +index 27e6c0a4..4fbf978c 100644 +--- a/source/vir/src/ast.rs ++++ b/source/vir/src/ast.rs +@@ -255,6 +255,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)] +@@ -372,6 +383,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 cd8d44b5..70a2c5d8 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..0fe050a6 100644 +--- a/source/vir/src/context.rs ++++ b/source/vir/src/context.rs +@@ -246,6 +246,7 @@ fn datatypes_invs( + TypX::Decorate(..) => unreachable!("TypX::Decorate"), + TypX::Boxed(_) => {} + TypX::TypeId => {} ++ TypX::Primitive(Primitive::TypeTag, _) => {} + TypX::Opaque { .. } => {} + TypX::Bool => {} + TypX::Float(_) => {} +diff --git a/source/vir/src/datatype_to_air.rs b/source/vir/src/datatype_to_air.rs +index c006b3e9..4ae70b32 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,69 @@ 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. ++ { ++ 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() { ++ 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()); ++ // types() is (Dcr, Type); only the Type component is tagged ++ if j + 1 == crate::def::types().len() { ++ tag_args.push(str_apply(crate::def::TYPE_TAG, &vec![v.clone()])); ++ } ++ id_args.push(v); ++ } ++ } ++ 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 43e511e6..b3ff3663 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 = "$$$"; +@@ -168,10 +169,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"; +@@ -185,6 +188,39 @@ 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. ++pub const TYPE_TAG_SORT: &str = "TypeTag"; ++pub const TYPE_TAG: &str = "TYPE%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 +633,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 af50af46..bbbc1435 100644 +--- a/source/vir/src/modes.rs ++++ b/source/vir/src/modes.rs +@@ -2099,6 +2099,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 88b27055..434cad50 100644 +--- a/source/vir/src/prelude.rs ++++ b/source/vir/src/prelude.rs +@@ -147,6 +147,16 @@ 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_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); + +@@ -187,6 +197,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]) +@@ -200,6 +211,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]) +@@ -358,6 +384,109 @@ 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 ++ ))) ++ (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 ++ ))) ++ // The decoration argument is deliberately NOT folded in: tags model ++ // undecorated type identity, so `&T` and `T` share a tag. See the ++ // decoration note in docs/verus-typeid-implementation-plan.md. ++ (axiom (forall ((d [decoration]) (t [typ])) (! ++ (= ([type_tag] ([type_id_mut_ref] d t)) ([tag_app] ([tag_mk] (- 15)) ([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)) ([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)) ([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)) ([type_tag] t)) ([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 7f7c319e..1ff43048 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..e8933533 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") + } +@@ -301,7 +305,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 +598,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 +658,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 +699,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 +733,26 @@ 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. ++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 +1087,12 @@ 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%tag()`. ++ // Producing the application is the point: the tag axioms are triggered on ++ // it, so a bare type id would leave them uninstantiated. ++ ExpX::NullaryOpr(crate::ast::NullaryOpr::TypeTag(t)) => { ++ str_apply(crate::def::TYPE_TAG, &vec![typ_to_id(ctx, 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/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/rust_verify_test/tests/type_id.rs b/source/rust_verify_test/tests/type_id.rs +new file mode 100644 +index 00000000..7f3f8e90 +--- /dev/null ++++ b/source/rust_verify_test/tests/type_id.rs +@@ -0,0 +1,157 @@ ++#![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, 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(()) ++} ++ ++// --- 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 *undecorated*: `&T` and `T` share a TypeId. This differs from ++// core::any::TypeId, and is forced by the encoding -- a decoration is not part ++// of the `Type` sort that tags are computed from. ++test_verify_one_file! { ++ #[test] decoration_is_not_part_of_identity verus_code! { ++ use verus_builtin::type_id; ++ proof fn t() { ++ assert(type_id::<&u8>() != type_id::()); // 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") ++} +-- +2.43.0 + From d61d549a4ce909e2ff0ec20237bbc1cf04ba165c Mon Sep 17 00:00:00 2001 From: Sean Anderson Date: Sun, 23 Aug 2026 00:28:18 -0700 Subject: [PATCH 2/7] `Any` module using new type id support --- verified_libs/vstd_extra/src/lib.rs | 2 + .../vstd_extra/src/typing/example.rs | 178 ++++++++ .../vstd_extra/src/typing/example_meta.rs | 429 ++++++++++++++++++ verified_libs/vstd_extra/src/typing/mod.rs | 5 + verified_libs/vstd_extra/src/typing/types.rs | 220 +++++++++ 5 files changed, 834 insertions(+) create mode 100644 verified_libs/vstd_extra/src/typing/example.rs create mode 100644 verified_libs/vstd_extra/src/typing/example_meta.rs create mode 100644 verified_libs/vstd_extra/src/typing/mod.rs create mode 100644 verified_libs/vstd_extra/src/typing/types.rs diff --git a/verified_libs/vstd_extra/src/lib.rs b/verified_libs/vstd_extra/src/lib.rs index f29416f9e..2cd45cabb 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,4 @@ pub mod spec_operators; pub mod state_machine; pub mod sum; pub mod temporal_logic; +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..3878b22b1 --- /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), +{ +} + +/// Recovering the concrete value, with no precondition at all. +/// +/// The caller does not have to know what `x` is: [`downcast_ref`] tests, and the +/// `<==>` in its postcondition is strong enough to conclude both that a match +/// yields an `L2` and that a non-match cannot. +pub exec fn downcast_l2<'a>(x: &'a dyn Any) -> (r: Option<&'a L2>) + ensures + (r is Some) <==> x.type_id_spec() == type_id::(), +{ + downcast_ref::(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 = downcast_l2(eb); + assert(ok is Some); + let no = downcast_l2(ec); + assert(no is None); +} + +/// Distinct members never satisfy each other's test. +/// +/// This is what stops an `L2` being read as an `L1`, and it is why +/// [`downcast_ref`]'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/example_meta.rs b/verified_libs/vstd_extra/src/typing/example_meta.rs new file mode 100644 index 000000000..06f136a1a --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/example_meta.rs @@ -0,0 +1,429 @@ +//! A syntax-faithful mimic of the frame layer's `dyn` casts. +//! +//! Every item here matches `ostd/src/mm/frame/meta.rs` and +//! `ostd/src/mm/frame/mod.rs` as closely as the types allow — same field shapes, +//! same casts, same call syntax — with the metadata impls reduced to dummies. The +//! purpose is to locate precisely where Verus stops accepting the real code. +//! +//! The four casts, in the order the frame layer performs them: +//! +//! 1. `&metadata as &dyn AnyFrameMeta` then `core::ptr::metadata(..)`, capturing a +//! vtable pointer at write time — `MetaSlot::write_meta`. +//! 2. `core::ptr::from_raw_parts_mut(storage_ptr, vtable_ptr)` to rebuild a +//! `*mut dyn AnyFrameMeta`, then dispatch `on_drop` through it and +//! `drop_in_place` it — `MetaSlot::drop_meta_in_place`. +//! 3. `transmute::, Frame>` — `Frame::into_dyn`. +//! 4. `(meta as &dyn core::any::Any).is::()` then the reverse transmute — +//! `TryFrom> for Frame`. +//! +//! # Result +//! +//! Casts 1–3 are accepted as written. The wide-pointer construction, the dispatch +//! through a rebuilt `*mut dyn`, and the transmutes all typecheck, needing +//! `external_body` only because `core::ptr::metadata`, `from_raw_parts_mut`, +//! `drop_in_place` and `transmute` have no Verus specifications. Nothing about +//! `dyn` itself obstructs them. +//! +//! Three registrations are needed first, none of them hard: +//! +//! - `UnsafeCell` has no `vstd` specification, so upstream's `MetaSlot` fields +//! cannot be written until it is registered — and the registration Verus's own +//! diagnostic suggests is incomplete, needing `external_body` as well because +//! `UnsafeCell`'s field is private. This is what our `PCell`/`PPtr` fields avoid. +//! - `DynMetadata` registers cleanly, but its parameter must be bounded by +//! `PointeeSized`, not `?Sized`: under `feature(sized_hierarchy)` a `?Sized` +//! proxy still carries a `MetaSized` predicate the external type does not have, +//! and the bounds must match exactly. +//! - `write_meta` needs an explicit `M: 'static`. Upstream gets it free from +//! `AnyFrameMeta: Any`, since `Any: 'static`; without `Any` the coercion inside +//! `core::ptr::metadata` fails with `E0310`. +//! +//! Cast 4 is **impossible in Verus today**, and not for want of a proof. It needs +//! `AnyFrameMeta: Any`, and: +//! +//! - Declaring that bound makes Verus panic rather than report an error: +//! `thread 'rustc' panicked at vir/src/traits.rs:1610: compute_dyn_compatibility: +//! missing trait Path(core, ["any" :: "Any"])`. The panic fires because +//! `compute_dyn_compatibility` looks every supertrait up in its map of +//! Verus-known traits, and `core::any::Any` is registered nowhere in `vstd`. +//! - Registering it is then blocked by two checks that contradict each other. +//! `type ExternalTraitSpecificationFor: Any;` fails with *external_trait_ +//! specification trait bound mismatch*, the diagnostic naming the missing bound +//! as `'static`. Adding it — `: Any + 'static` — fails with *unexpected bound in +//! ExternalTraitSpecificationFor*. Since `Any: 'static` is part of `Any`'s own +//! definition and the bounds must match exactly, no spelling satisfies both. +//! - Without the bound, the cast is rejected by *rustc*, before Verus sees it: +//! `E0605: non-primitive cast: &dyn AnyMeta as &(dyn core::any::Any + 'static)`. +//! +//! # `EitherType` cannot stand in for `Any` either +//! +//! The natural repair is to notice that `x as &dyn Any` is a dyn-to-dyn *upcast*, +//! and to put [`super::types::EitherType`] in that slot: make it a supertrait of +//! `AnyMeta`, upcast to `&dyn EitherType`, and read the id from there. It would +//! be a one-to-one syntactic match, and it would recover the id through the +//! upcast rather than through `AnyMeta`. +//! +//! It does not work, for a reason more basic than anything about `Any`: +//! +//! > `the trait bound Dyn<2, ()>: T196_Either is not satisfied` +//! +//! **Verus's dyn type does not implement the erased trait's Verus supertraits.** +//! Probed with a parameter-free supertrait carrying a single spec fn, which fails +//! identically (`Dyn<3, ()>: T198_Marker`), so this is not about `EitherType`'s +//! generics. Only marker and auto traits (`Send`, `Sync`) survive in supertrait +//! position. The same root cause explains two earlier observations: `dyn HasId` +//! does not typecheck because `HasId: TypeSet`, and a spec fn inherited from a +//! supertrait is not preserved across the `&T -> &dyn Trait` coercion. Verus +//! simply does not model the supertrait relation for dyn types. +//! +//! Verus does have an escape hatch — its `unsized_blanketed_traits` set makes a +//! supertrait usable if it has an unbounded `impl`. That cannot help +//! here: a blanket impl gives every type the *same* id, and an identity trait +//! whose answer does not depend on the type is no identity trait. +//! +//! So a `dyn` trait in Verus must be self-contained: everything an erased value +//! needs to report has to be declared on that one trait. [`try_from_tagged`] is +//! therefore not a workaround for a missing feature — it is the only shape +//! available, and [`AnyMeta::type_id`] must live where it does. +//! +//! So `/*Any +*/` in our `AnyFrameMeta`, and the commented-out `TryFrom`, are +//! forced rather than chosen. Verus needs either a `vstd` registration of `Any` or +//! `'static` support in `external_trait_specification` before a downcast built on +//! `Any` can be verified. +//! +//! [`try_from_tagged`] is the replacement, mirroring cast 4 with the one +//! substitution that makes it expressible: `Any::is::()` becomes a comparison of +//! a dyn-dispatched tag against a statically known one. That test is *verified*, +//! and the `Result` shape, the unchanged-on-failure `Err`, and the transmute are +//! all preserved. +//! +//! Note the field types below are upstream Asterinas's, not the ones in our +//! `MetaSlot` — ours carries `vtable_ptr: PPtr` under a comment reading +//! "VERUS LIMITATION: Currently we do not verify this because of the dependency on +//! the `dyn Trait` pattern". Casts 1–3 are evidence that field can be restored to +//! `UnsafeCell>`. +use core::cell::UnsafeCell; +use core::marker::PhantomData; +use core::mem::MaybeUninit; +use core::ptr::DynMetadata; + +use vstd::prelude::*; + +use super::types::TypeId; + +verus! { + +/// Registers `UnsafeCell` with Verus. +/// +/// Needed because upstream's `MetaSlot` fields are `UnsafeCell`, and Verus has no +/// specification for it — our tree sidesteps this with `PCell`/`PPtr`. The +/// declaration is the one Verus's own diagnostic suggests. +#[verifier::reject_recursive_types(T)] +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExUnsafeCell(UnsafeCell) where T: core::marker::MetaSized + ?Sized; + +/// Registers `DynMetadata` with Verus. +/// +/// The vtable-pointer type itself. Unlike `core::any::Any` this registers without +/// trouble — it carries no `'static` bound, which is the thing that made `Any` +/// unregisterable. +#[verifier::reject_recursive_types(T)] +#[verifier::external_type_specification] +#[verifier::external_body] +pub struct ExDynMetadata(DynMetadata); + +/// Mimics `FRAME_METADATA_MAX_SIZE`. +pub const META_MAX_SIZE: usize = 8; + +/// Mimics `MetaSlotStorage`. +/// +/// Upstream this is a raw `[u8; FRAME_METADATA_MAX_SIZE]`; ours is an exec-tagged +/// union. Kept as bytes here because the casts under test do not care which. +pub struct MetaSlotStorage { + pub bytes: [u8; META_MAX_SIZE], +} + +/// Mimics `AnyFrameMeta`. +/// +/// Same shape as the real trait: `unsafe`, `Send + Sync`, an `open spec fn` +/// per-impl precondition, and an exec `on_drop` on `&mut self` whose `requires` +/// calls that precondition. The real one also threads a `VmReader` and two +/// `Tracked` owner arguments; those are dropped as orthogonal to dispatch. +/// +/// `Any` is absent from the supertraits, exactly as in our tree. See the module +/// docs — the bound cannot be written, so [`Self::type_id`] takes its place. +pub unsafe trait AnyMeta: Send + Sync { + /// The id of *this value's* type, readable through an erased reference. + /// + /// Declared here rather than inherited from a supertrait, and not + /// `where Self: Sized`, because both are needed for it to survive the + /// `&M -> &dyn AnyMeta` coercion. This is the stand-in for `Any::type_id`. + spec fn type_id(&self) -> TypeIdSpec; + + /// The executable form, dispatched through the vtable. + fn type_id_val(&self) -> (r: TypeId) + ensures + r.view() == self.type_id(), + ; + + /// A value's identity is its type's identity. + /// + /// This is the whole of what `MetaTag` used to be. That trait gave every + /// implementor a hand-chosen `usize` and then required, by hand, that the + /// value's dispatched id agree with it -- its own doc called this "the fact + /// `Any` provides for free and the one thing that has to be supplied by hand". + /// It is now supplied for free: the body is empty because `type_id::()` + /// is exactly what `type_id` is obliged to return. + proof fn type_id_coherent(&self) where Self: core::marker::Sized + ensures + self.type_id() == type_id::(), + ; + + /// Per-impl precondition for [`Self::on_drop`]. Default is `true`. + open spec fn on_drop_pre(&self) -> bool { + true + } + + fn on_drop(&mut self) + requires + old(self).on_drop_pre(), + ; +} + +/// Mimics `FrameMetaVtablePtr`. +pub type MetaVtablePtr = DynMetadata; + +/// Mimics `MetaSlot`, with the fields upstream actually uses. +pub struct MetaSlot { + pub storage: UnsafeCell, + pub vtable_ptr: UnsafeCell>, +} + +/// A dummy metadata type, standing in for e.g. `MetaPageMeta`. +pub struct MetaA { + pub val: u64, +} + +/// A second dummy, so dispatch and downcasting have something to choose between. +/// With one impl a vtable-shaped call would verify vacuously. +pub struct MetaB { + pub val: u64, +} + +#[verifier::external] +unsafe impl Send for MetaA { + +} + +#[verifier::external] +unsafe impl Sync for MetaA { + +} + +#[verifier::external] +unsafe impl Send for MetaB { + +} + +#[verifier::external] +unsafe impl Sync for MetaB { + +} + +unsafe impl AnyMeta for MetaA { + open spec fn type_id(&self) -> TypeIdSpec { + type_id::() + } + + fn type_id_val(&self) -> (r: TypeId) { + TypeId::of::() + } + + proof fn type_id_coherent(&self) { + } + + #[verifier::external_body] + fn on_drop(&mut self) { + } +} + +unsafe impl AnyMeta for MetaB { + open spec fn type_id(&self) -> TypeIdSpec { + type_id::() + } + + fn type_id_val(&self) -> (r: TypeId) { + TypeId::of::() + } + + proof fn type_id_coherent(&self) { + } + + #[verifier::external_body] + fn on_drop(&mut self) { + } +} + +impl MetaSlot { + /// Cast 1 — upcast at write time. Mimics `MetaSlot::write_meta`. + /// + /// The body is the line that is *commented out* in our tree. It typechecks; + /// `external_body` is needed only because `core::ptr::metadata` has no spec. + /// Note the explicit `'static`. Upstream it is implied by `AnyFrameMeta: Any`, + /// since `Any: 'static`; with `Any` unavailable the bound has to be written by + /// hand, or `core::ptr::metadata` rejects the coercion with `E0310`. + #[verifier::external_body] + pub unsafe fn write_meta(&self, metadata: M) { + // SAFETY: Caller ensures that the access to the fields are exclusive. + let vtable_ptr = unsafe { &mut *self.vtable_ptr.get() }; + vtable_ptr.write(core::ptr::metadata(&metadata as &dyn AnyMeta)); + } + + /// Cast 2 — rebuild a wide pointer and dispatch through it. + /// Mimics `MetaSlot::drop_meta_in_place`. + /// + /// This is the shape our tree currently keeps alive only as a type-check. It + /// is accepted as written. + #[verifier::external_body] + pub unsafe fn drop_meta_in_place(&self) { + // SAFETY: We have exclusive access to the frame metadata. + let vtable_ptr = unsafe { &mut *self.vtable_ptr.get() }; + // SAFETY: The frame metadata is initialized and valid. + let vtable_ptr = unsafe { vtable_ptr.assume_init_read() }; + + let storage_ptr: *mut () = self.storage.get() as *mut (); + let meta_ptr: *mut dyn AnyMeta = core::ptr::from_raw_parts_mut(storage_ptr, vtable_ptr); + + // SAFETY: `ptr` points to the metadata storage which is valid to be + // mutably borrowed under `vtable_ptr` because the metadata is valid, + // the vtable is correct, and we have exclusive access. + unsafe { + // Invoke the custom `on_drop` handler. + (*meta_ptr).on_drop(); + // Drop the frame metadata. + core::ptr::drop_in_place(meta_ptr); + } + } + + /// Mimics `MetaSlot::dyn_meta_ptr`, the shared-reference form. + #[verifier::external_body] + pub unsafe fn dyn_meta_ptr(&self) -> *mut dyn AnyMeta { + // SAFETY: The page metadata is valid to be borrowed immutably, since it + // will never be borrowed mutably after initialization. + let vtable_ptr = unsafe { &*self.vtable_ptr.get() }; + + // SAFETY: The page metadata is initialized and valid. + let vtable_ptr = *unsafe { vtable_ptr.assume_init_ref() }; + + core::ptr::from_raw_parts_mut(self as *const MetaSlot as *mut MetaSlot, vtable_ptr) + } +} + +/// Mimics `Frame`. +/// +/// `#[repr(transparent)]` over a pointer plus a ZST phantom, as upstream, which is +/// what makes the transmutes in casts 3 and 4 layout-valid. +#[repr(transparent)] +pub struct Frame { + pub ptr: *const MetaSlot, + pub _marker: PhantomData, +} + +impl Frame { + /// Cast 3 — erase the static metadata type. Mimics `Frame::into_dyn`. + #[verifier::external_body] + pub fn into_dyn(self) -> Frame { + // SAFETY: `Frame` is `#[repr(transparent)]` over a thin pointer plus a + // zero-size `PhantomData`. `Frame` has the same runtime + // layout (thin pointer + ZST phantom). + unsafe { core::mem::transmute(self) } + } +} + +impl Frame { + /// The id of the metadata this frame points at. + /// + /// Uninterpreted here because the dummy slot carries no ghost state; in the + /// frame layer this is the region's view of the slot. + pub uninterp spec fn meta_id(&self) -> TypeIdSpec; + + /// Mimics `Frame::::dyn_meta`. + /// + /// The `ensures` is what makes the erased reference usable: without tying the + /// dispatched id back to the frame, a caller could compare tags and conclude + /// nothing about *this* frame. + #[verifier::external_body] + pub fn dyn_meta(&self) -> (r: &dyn AnyMeta) + ensures + r.type_id() == self.meta_id(), + { + // SAFETY: The metadata is initialized and valid. + unsafe { &*(*self.ptr).dyn_meta_ptr() } + } +} + +/// Cast 4, with the one substitution that makes it expressible. +/// +/// Mirrors `TryFrom> for Frame`, except that +/// +/// ```text +/// if (dyn_frame.dyn_meta() as &dyn core::any::Any).is::() { +/// ``` +/// +/// becomes +/// +/// ```text +/// if dyn_frame.dyn_meta().type_id_val().eq(&TypeId::of::()) { +/// ``` +/// +/// Both compare an id read through the vtable against one known statically, and +/// both ids are now the *same notion of identity* -- upstream reads it with +/// `TypeIdSpec::of`, we read it with `type_id::()`. Previously the right-hand side +/// was a hand-chosen `usize` from a `MetaTag` impl, related to the real identity +/// only by an obligation each implementor discharged by hand. +/// +/// A free function rather than a `TryFrom` impl, to keep the plumbing visible; +/// the `Result` shape and the unchanged-on-failure `Err` are preserved. +/// +/// The transmute stays `external_body`, as upstream. What is *gained* is that the +/// test guarding it is verified: the postcondition records that `Ok` happens +/// exactly when the frame's metadata has `M`'s id. +pub fn try_from_tagged(dyn_frame: Frame) -> (res: Result< + Frame, + Frame, +>) + ensures + (res is Ok) == (dyn_frame.meta_id() == type_id::()), +{ + if dyn_frame.dyn_meta().type_id_val().eq(&TypeId::of::()) { + // SAFETY: The metadata is coerceable and the struct is transmutable. + Ok(transmute_to_typed::(dyn_frame)) + } else { + Err(dyn_frame) + } +} + +/// The transmute half of cast 4, split out so the test above stays verified. +#[verifier::external_body] +pub fn transmute_to_typed(dyn_frame: Frame) -> Frame { + // SAFETY: The metadata is coerceable and the struct is transmutable. + unsafe { core::mem::transmute::, Frame>(dyn_frame) } +} + +/// The downcast admits the right type and rejects the other. +/// +/// Both directions matter and neither is vacuous: `Ok` needs the tags to agree, +/// and `Err` is what stops a `MetaB` frame from being read as a `MetaA`. +pub fn downcast_discriminates(a: Frame, b: Frame) + requires + a.meta_id() == type_id::(), + b.meta_id() == type_id::(), +{ + let ra = try_from_tagged::(a); + assert(ra is Ok); + let rb = try_from_tagged::(b); + assert(rb is Err); +} + +} // 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..7db4732ad --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/mod.rs @@ -0,0 +1,5 @@ +pub mod types; + +pub mod example; + +pub mod example_meta; 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..cdc3815dc --- /dev/null +++ b/verified_libs/vstd_extra/src/typing/types.rs @@ -0,0 +1,220 @@ +use vstd::prelude::*; + +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 what makes a downcast sound: `type_id_spec` *cannot* +/// report the wrong type, because no one is in a position to write a version that +/// does. +pub trait Any { + /// The identity of this value's concrete type. + spec fn type_id_spec(&self) -> TypeIdSpec; + + /// The same identity, as a runtime value. + fn type_id(&self) -> (r: TypeId) + ensures + r.view() == 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 types. +impl Any for T { + open spec fn type_id_spec(&self) -> TypeIdSpec { + 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::()`. +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(); +} + +/// The exec counterpart of the ghost [`TypeIdSpec`]. +#[verifier::external_body] +pub struct TypeId { + _private: (), +} + +impl TypeId { + /// The ghost identity this runtime value stands for. + pub uninterp spec fn view(&self) -> TypeIdSpec; + + /// `core::any::TypeIdSpec::of::()`. + #[verifier::external_body] + pub exec fn of() -> (r: Self) + ensures + r.view() == type_id::(), + { + unimplemented!() + } + + /// Deciding identity at runtime. + #[verifier::external_body] + pub exec fn eq(&self, other: &Self) -> (r: bool) + returns + self.view() == other.view(), + { + unimplemented!() + } +} + +/// `::is` +pub exec fn is_(x: &dyn Any) -> (r: bool) + ensures + r == is_type::(x), +{ + x.type_id().eq(&TypeId::of::()) +} + +/// Reinterpretation, once identity is settled. +/// +/// The module's remaining assumed fact about identity, and it is now only the +/// *cast*: the test that guards it is [`is_`], which is verified. What licenses +/// the cast is [`Any::type_id_correct`] -- a value's reported identity is its +/// concrete type's, so a matching identity really does mean a `T`. +#[verifier::external_body] +pub exec fn downcast_ref_unchecked<'a, T: Any + Sized>(x: &'a dyn Any) -> (r: &'a T) + requires + is_type::(x), + ensures + r.type_id_spec() == x.type_id_spec(), +{ + unimplemented!() +} + +/// `::downcast_ref`. +/// +/// The `<==>` records both halves: it succeeds for the right type *and fails for +/// every other one*. +pub exec fn downcast_ref<'a, T: Any + Sized>(x: &'a dyn Any) -> (r: Option<&'a T>) + ensures + (r is Some) <==> is_type::(x), + r matches Some(v) ==> v.type_id_spec() == x.type_id_spec(), +{ + if is_::(x) { + Some(downcast_ref_unchecked::(x)) + } else { + None + } +} + +// =========================================================================== +// 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! From 15b68361b1fbe7d77665113d64fe74e59796e1b0 Mon Sep 17 00:00:00 2001 From: Sean Anderson Date: Sun, 23 Aug 2026 00:29:01 -0700 Subject: [PATCH 3/7] Verify `Frame::try_from` using new `Any` module. --- ostd/specs/mm/frame/meta_owners.rs | 11 ++++ ostd/src/mm/frame/linked_list.rs | 11 ++++ ostd/src/mm/frame/meta.rs | 20 ++++++- ostd/src/mm/frame/mod.rs | 95 +++++++++++++++++++++++++----- ostd/src/mm/page_table/node/mod.rs | 11 ++++ 5 files changed, 132 insertions(+), 16 deletions(-) diff --git a/ostd/specs/mm/frame/meta_owners.rs b/ostd/specs/mm/frame/meta_owners.rs index 034340f7e..5b0350762 100644 --- a/ostd/specs/mm/frame/meta_owners.rs +++ b/ostd/specs/mm/frame/meta_owners.rs @@ -3,6 +3,7 @@ //! - The invariants for both MetaSlot and MetaSlotModel. //! - The primitives for MetaSlot. use vstd::prelude::*; +use vstd_extra::typing::types::Any; use vstd::{atomic::*, cell::pcell_maybe_uninit, simple_pptr::*}; use vstd_extra::{ @@ -109,6 +110,16 @@ 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; + + open spec fn meta_id(&self) -> TypeIdSpec { + 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..99c1b3a44 100644 --- a/ostd/src/mm/frame/linked_list.rs +++ b/ostd/src/mm/frame/linked_list.rs @@ -4,6 +4,7 @@ //! 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::*; +use vstd_extra::typing::types::Any; use vstd::seq_lib::*; use vstd::simple_pptr::*; @@ -1723,6 +1724,16 @@ 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 { + open spec fn meta_id(&self) -> TypeIdSpec { + 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..ba858a5d1 100644 --- a/ostd/src/mm/frame/meta.rs +++ b/ostd/src/mm/frame/meta.rs @@ -84,10 +84,10 @@ use vstd_extra::cast_ptr::{Repr, ReprPtr}; use vstd_extra::ownership::*; use vstd_extra::panic::{may_panic, panic_diverge}; use vstd_extra::prelude::*; +use vstd_extra::typing::types::Any; use core::{ alloc::Layout, - any::Any, cell::UnsafeCell, fmt::Debug, marker::PhantomData, @@ -262,6 +262,24 @@ 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. + spec fn meta_id(&self) -> TypeIdSpec; + + /// 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. + 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..5d02f4afc 100644 --- a/ostd/src/mm/frame/mod.rs +++ b/ostd/src/mm/frame/mod.rs @@ -32,10 +32,12 @@ use vstd::atomic::PermissionU64; use vstd::prelude::*; use vstd::simple_pptr::{self, PPtr}; +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; +use vstd_extra::typing::types::{Any, is_}; pub mod allocator; pub mod linked_list; @@ -380,13 +382,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,7 +742,60 @@ impl Drop for Frame { } } -/* +verus! { + +/// 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) -> TypeIdSpec; + + /// 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) } +} + +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) + } + } +} impl TryFrom> for Frame { type Error = Frame; @@ -756,27 +804,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 { @@ -919,7 +980,11 @@ impl + 'static> Frame { /// Axiomatized (`external_body`) because the body is `transmute`, which /// Verus has no built-in spec for. #[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). diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index e1a0591a9..f74bbb40b 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -37,6 +37,7 @@ pub use entry::*; use vstd::cell::pcell_maybe_uninit; use vstd::prelude::*; +use vstd_extra::typing::types::Any; use vstd::atomic::PAtomicU8; use vstd_extra::array_ptr; @@ -116,6 +117,16 @@ pub struct PageTablePageMeta { pub type PageTableNode = Frame>; unsafe impl AnyFrameMeta for PageTablePageMeta { + open spec fn meta_id(&self) -> TypeIdSpec { + 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 From a4b7b3dc71c09f03935025fc80e8b0dee23f749c Mon Sep 17 00:00:00 2001 From: Sean Anderson Date: Sun, 23 Aug 2026 00:37:19 -0700 Subject: [PATCH 4/7] Update dv --- Cargo.lock | 8 ++++---- dv | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 92c2f90e6..f1945994d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -595,11 +595,11 @@ dependencies = [ [[package]] name = "verus_builtin" -version = "0.0.0-2026-08-09-0044" +version = "0.0.0-2026-08-02-0125" [[package]] name = "verus_builtin_macros" -version = "0.0.0-2026-08-09-0044" +version = "0.0.0-2026-08-02-0125" dependencies = [ "convert_case", "proc-macro2", @@ -612,7 +612,7 @@ dependencies = [ [[package]] name = "verus_prettyplease" -version = "0.0.0-2026-08-09-0044" +version = "0.0.0-2026-08-02-0125" dependencies = [ "proc-macro2", "verus_syn", @@ -651,7 +651,7 @@ checksum = "af8ca9a5d4debca0633e697c88269395493cebf2e10db21ca2dbde37c1356452" [[package]] name = "vstd" -version = "0.0.0-2026-08-09-0044" +version = "0.0.0-2026-08-02-0125" dependencies = [ "verus_builtin", "verus_builtin_macros", diff --git a/dv b/dv index b4bc559da..e07a058da 160000 --- a/dv +++ b/dv @@ -1 +1 @@ -Subproject commit b4bc559dae28c4be9cd8c782a0ecae1806af2606 +Subproject commit e07a058da918ee8ec093bfcde141c46690f9ecac From b25e52a9d0174ae9aa2ba6f9d64e86aa77e9e2b8 Mon Sep 17 00:00:00 2001 From: Sean Anderson Date: Mon, 24 Aug 2026 16:19:16 -0700 Subject: [PATCH 5/7] Update verus patch --- patches/0001-verus-type-identity.patch | 354 +++++++++++++------------ 1 file changed, 180 insertions(+), 174 deletions(-) diff --git a/patches/0001-verus-type-identity.patch b/patches/0001-verus-type-identity.patch index be8751944..87f9f3a6f 100644 --- a/patches/0001-verus-type-identity.patch +++ b/patches/0001-verus-type-identity.patch @@ -1,24 +1,33 @@ diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs -index 8fceab37..48434b7b 100644 +index 8fceab37..ed82d23d 100644 --- a/source/builtin/src/lib.rs +++ b/source/builtin/src/lib.rs -@@ -2322,6 +2322,22 @@ pub fn arch_word_bits() -> nat { +@@ -2322,6 +2322,31 @@ pub fn arch_word_bits() -> nat { unimplemented!(); } ++/// The identity of a type, as a ghost value. +/// -+/// Dynamic type id, as in `std::any`. ++/// The spec-level counterpart of `core::any::TypeId`. The name carries the `Spec` ++/// suffix so that a *runtime* type id -- which is what `std` calls `TypeId`, and ++/// what a library layered on this will want to call it too -- keeps the unsuffixed ++/// name. +/// ++/// Identity here is *undecorated*: `T` and `&T` share a `TypeIdSpec`, unlike ++/// `core::any::TypeId`, which separates them. This is forced by the encoding ++/// rather than chosen -- a type's decoration is not part of the `Type` sort that ++/// tags are computed from. +#[cfg(verus_keep_ghost)] -+#[rustc_diagnostic_item = "verus::verus_builtin::TypeId"] ++#[rustc_diagnostic_item = "verus::verus_builtin::TypeIdSpec"] +#[verifier::external_body] -+pub struct TypeId { ++pub struct TypeIdSpec { + _private: (), +} + ++/// The [`TypeIdSpec`] of `T`. +#[cfg(verus_keep_ghost)] +#[rustc_diagnostic_item = "verus::verus_builtin::type_id"] -+pub fn type_id() -> TypeId { ++pub fn type_id() -> TypeIdSpec { + unimplemented!(); +} + @@ -94,7 +103,7 @@ index ff8f9255..9f98285a 100644 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 689a1df6..45d61997 100644 +index 689a1df6..c08a9f80 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -144,6 +144,7 @@ pub(crate) enum ExprItem { @@ -125,10 +134,173 @@ index 689a1df6..45d61997 100644 ("verus::verus_builtin::FnSpec", VerusItem::BuiltinType(BuiltinTypeItem::FnSpec)), ("verus::verus_builtin::Ghost", VerusItem::BuiltinType(BuiltinTypeItem::Ghost)), ("verus::verus_builtin::Tracked", VerusItem::BuiltinType(BuiltinTypeItem::Tracked)), -+ ("verus::verus_builtin::TypeId", VerusItem::BuiltinType(BuiltinTypeItem::TypeId)), ++ ("verus::verus_builtin::TypeIdSpec", VerusItem::BuiltinType(BuiltinTypeItem::TypeId)), ("verus::verus_builtin::Integer", VerusItem::BuiltinTrait(BuiltinTraitItem::Integer)), ("verus::verus_builtin::Chainable", VerusItem::BuiltinTrait(BuiltinTraitItem::Chainable)), +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..0e25a040 +--- /dev/null ++++ b/source/rust_verify_test/tests/type_id.rs +@@ -0,0 +1,157 @@ ++#![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 TypeIdSpec 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, TypeIdSpec}; ++ struct Wrap(T); ++ proof fn t(x: TypeIdSpec) { ++ let s = Wrap(x); ++ assert(s.0 == x); ++ } ++ spec fn is_u8(x: TypeIdSpec) -> bool { x == type_id::() } ++ proof fn u() { ++ assert(is_u8(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 *undecorated*: `&T` and `T` share a TypeIdSpec. This differs from ++// core::any::TypeId, and is forced by the encoding -- a decoration is not part ++// of the `Type` sort that tags are computed from. ++test_verify_one_file! { ++ #[test] decoration_is_not_part_of_identity verus_code! { ++ use verus_builtin::type_id; ++ proof fn t() { ++ assert(type_id::<&u8>() != type_id::()); // 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 27e6c0a4..4fbf978c 100644 --- a/source/vir/src/ast.rs @@ -780,169 +952,3 @@ index 89c59c93..3dbc7260 100644 ExpX::NullaryOpr(crate::ast::NullaryOpr::TraitBound(..)) => { Err(error(&exp.span, "triggers cannot contain trait bounds")) } -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..7f3f8e90 ---- /dev/null -+++ b/source/rust_verify_test/tests/type_id.rs -@@ -0,0 +1,157 @@ -+#![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, 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(()) -+} -+ -+// --- 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 *undecorated*: `&T` and `T` share a TypeId. This differs from -+// core::any::TypeId, and is forced by the encoding -- a decoration is not part -+// of the `Type` sort that tags are computed from. -+test_verify_one_file! { -+ #[test] decoration_is_not_part_of_identity verus_code! { -+ use verus_builtin::type_id; -+ proof fn t() { -+ assert(type_id::<&u8>() != type_id::()); // 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") -+} --- -2.43.0 - From 0ae8ad4dd9e39439c47137543a99b9f8fff66c97 Mon Sep 17 00:00:00 2001 From: Sean Anderson Date: Wed, 26 Aug 2026 15:21:55 -0700 Subject: [PATCH 6/7] dv bump --- Cargo.lock | 8 ++++---- dv | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index f1945994d..161263497 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -595,11 +595,11 @@ dependencies = [ [[package]] name = "verus_builtin" -version = "0.0.0-2026-08-02-0125" +version = "0.0.0-2026-08-09-0044" [[package]] name = "verus_builtin_macros" -version = "0.0.0-2026-08-02-0125" +version = "0.0.0-2026-08-23-0033" dependencies = [ "convert_case", "proc-macro2", @@ -612,7 +612,7 @@ dependencies = [ [[package]] name = "verus_prettyplease" -version = "0.0.0-2026-08-02-0125" +version = "0.0.0-2026-08-09-0044" dependencies = [ "proc-macro2", "verus_syn", @@ -651,7 +651,7 @@ checksum = "af8ca9a5d4debca0633e697c88269395493cebf2e10db21ca2dbde37c1356452" [[package]] name = "vstd" -version = "0.0.0-2026-08-02-0125" +version = "0.0.0-2026-08-23-0033" dependencies = [ "verus_builtin", "verus_builtin_macros", diff --git a/dv b/dv index e07a058da..b4bc559da 160000 --- a/dv +++ b/dv @@ -1 +1 @@ -Subproject commit e07a058da918ee8ec093bfcde141c46690f9ecac +Subproject commit b4bc559dae28c4be9cd8c782a0ecae1806af2606 From 631791adb999f06cd19a0ea1df15c84b6ab9b24e Mon Sep 17 00:00:00 2001 From: Sean Anderson Date: Wed, 26 Aug 2026 21:10:31 -0700 Subject: [PATCH 7/7] Use feature gating to keep `Any` separate for now --- ostd/Cargo.toml | 4 + ostd/specs/mm/frame/meta_owners.rs | 7 +- ostd/src/mm/frame/linked_list.rs | 7 +- ostd/src/mm/frame/meta.rs | 9 +- ostd/src/mm/frame/mod.rs | 26 +- ostd/src/mm/page_table/node/mod.rs | 7 +- patches/0001-verus-type-identity.patch | 568 +++++++++++++++--- patches/README.md | 118 ++++ verified_libs/vstd_extra/Cargo.toml | 4 + verified_libs/vstd_extra/src/lib.rs | 1 + .../vstd_extra/src/typing/example.rs | 26 +- .../vstd_extra/src/typing/example_meta.rs | 429 ------------- verified_libs/vstd_extra/src/typing/mod.rs | 4 +- verified_libs/vstd_extra/src/typing/types.rs | 101 +--- 14 files changed, 690 insertions(+), 621 deletions(-) create mode 100644 patches/README.md delete mode 100644 verified_libs/vstd_extra/src/typing/example_meta.rs 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 5b0350762..66ced3bf8 100644 --- a/ostd/specs/mm/frame/meta_owners.rs +++ b/ostd/specs/mm/frame/meta_owners.rs @@ -3,7 +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::{ @@ -111,10 +114,12 @@ pub enum MetaSlotStorage { unsafe impl AnyFrameMeta for MetaSlotStorage { uninterp spec fn vtable_ptr(&self) -> usize; - open spec fn meta_id(&self) -> TypeIdSpec { + #[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()); diff --git a/ostd/src/mm/frame/linked_list.rs b/ostd/src/mm/frame/linked_list.rs index 99c1b3a44..486858eec 100644 --- a/ostd/src/mm/frame/linked_list.rs +++ b/ostd/src/mm/frame/linked_list.rs @@ -4,7 +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::*; @@ -1724,10 +1727,12 @@ 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 { - open spec fn meta_id(&self) -> TypeIdSpec { + #[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()); diff --git a/ostd/src/mm/frame/meta.rs b/ostd/src/mm/frame/meta.rs index ba858a5d1..a3eba6a21 100644 --- a/ostd/src/mm/frame/meta.rs +++ b/ostd/src/mm/frame/meta.rs @@ -84,7 +84,10 @@ 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, @@ -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 @@ -268,7 +271,8 @@ Send + Sync { /// 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. - spec fn meta_id(&self) -> TypeIdSpec; + #[cfg(feature = "type_id")] + spec fn meta_id(&self) -> TypeId; /// Mimics the upcast `self as &dyn core::any::Any`. /// @@ -276,6 +280,7 @@ Send + Sync { /// `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(), diff --git a/ostd/src/mm/frame/mod.rs b/ostd/src/mm/frame/mod.rs index 5d02f4afc..0ec8c035d 100644 --- a/ostd/src/mm/frame/mod.rs +++ b/ostd/src/mm/frame/mod.rs @@ -31,12 +31,16 @@ //! 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; @@ -744,6 +748,7 @@ 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 @@ -756,7 +761,7 @@ impl Frame { /// 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) -> TypeIdSpec; + pub uninterp spec fn meta_type_id(&self) -> TypeId; /// Gets the dynamically-typed metadata of this frame. /// @@ -783,6 +788,7 @@ pub fn transmute_frame_to_typed(dyn_frame: Frame, Frame>(dyn_frame) } } +#[cfg(feature = "type_id")] impl TryFromSpecImpl> for Frame { open spec fn obeys_try_from_spec() -> bool { true @@ -797,6 +803,7 @@ impl TryFromSpecImpl> for Frame { } } +#[cfg(feature = "type_id")] impl TryFrom> for Frame { type Error = Frame; @@ -979,6 +986,13 @@ 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) -> (r: Frame) ensures @@ -990,6 +1004,16 @@ impl + 'static> Frame { // 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 f74bbb40b..7b0940cb4 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -37,7 +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; @@ -117,10 +120,12 @@ pub struct PageTablePageMeta { pub type PageTableNode = Frame>; unsafe impl AnyFrameMeta for PageTablePageMeta { - open spec fn meta_id(&self) -> TypeIdSpec { + #[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()); diff --git a/patches/0001-verus-type-identity.patch b/patches/0001-verus-type-identity.patch index 87f9f3a6f..23d5a5ac1 100644 --- a/patches/0001-verus-type-identity.patch +++ b/patches/0001-verus-type-identity.patch @@ -1,33 +1,32 @@ diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs -index 8fceab37..ed82d23d 100644 +index 8fceab37..e642dff4 100644 --- a/source/builtin/src/lib.rs +++ b/source/builtin/src/lib.rs -@@ -2322,6 +2322,31 @@ pub fn arch_word_bits() -> nat { +@@ -2322,6 +2322,30 @@ pub fn arch_word_bits() -> nat { unimplemented!(); } -+/// The identity of a type, as a ghost value. ++/// The identity of `T`, as `core::any::TypeId`. +/// -+/// The spec-level counterpart of `core::any::TypeId`. The name carries the `Spec` -+/// suffix so that a *runtime* type id -- which is what `std` calls `TypeId`, and -+/// what a library layered on this will want to call it too -- keeps the unsuffixed -+/// name. ++/// 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 here is *undecorated*: `T` and `&T` share a `TypeIdSpec`, unlike -+/// `core::any::TypeId`, which separates them. This is forced by the encoding -+/// rather than chosen -- a type's decoration is not part of the `Type` sort that -+/// tags are computed from. -+#[cfg(verus_keep_ghost)] -+#[rustc_diagnostic_item = "verus::verus_builtin::TypeIdSpec"] -+#[verifier::external_body] -+pub struct TypeIdSpec { -+ _private: (), -+} -+ -+/// The [`TypeIdSpec`] of `T`. ++/// 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() -> TypeIdSpec { ++pub fn type_id() -> core::any::TypeId { + unimplemented!(); +} + @@ -35,7 +34,7 @@ index 8fceab37..ed82d23d 100644 #[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 542ea83d..a2ca91d6 100644 +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}; @@ -70,18 +69,27 @@ index 542ea83d..a2ca91d6 100644 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 6a7c43ae..2a848670 100644 +index b194808e..20219e17 100644 --- a/source/rust_verify/src/rust_to_vir_base.rs +++ b/source/rust_verify/src/rust_to_vir_base.rs -@@ -1129,6 +1129,8 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>( - (Arc::new(TypX::Int(IntRange::Nat)), false) - } else if let Some(VerusItem::BuiltinType(BuiltinTypeItem::Real)) = verus_item { - (Arc::new(TypX::Real), false) -+ } else if let Some(VerusItem::BuiltinType(BuiltinTypeItem::TypeId)) = verus_item { -+ (Arc::new(TypX::Primitive(Primitive::TypeTag, Arc::new(vec![]))), false) +@@ -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 @@ -103,10 +111,10 @@ index ff8f9255..9f98285a 100644 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 689a1df6..c08a9f80 100644 +index 234af809..1293cc08 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs -@@ -144,6 +144,7 @@ pub(crate) enum ExprItem { +@@ -145,6 +145,7 @@ pub(crate) enum ExprItem { StrSliceLen, StrSliceGetChar, ArchWordBits, @@ -114,15 +122,7 @@ index 689a1df6..c08a9f80 100644 ClosureToFnSpec, ClosureToFnProof, SignedMin, -@@ -405,6 +406,7 @@ pub(crate) enum BuiltinTypeItem { - FnSpec, - Ghost, - Tracked, -+ TypeId, - } - - #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] -@@ -538,6 +540,7 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { +@@ -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)), @@ -130,20 +130,33 @@ index 689a1df6..c08a9f80 100644 ("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)), -@@ -745,6 +748,7 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { - ("verus::verus_builtin::FnSpec", VerusItem::BuiltinType(BuiltinTypeItem::FnSpec)), - ("verus::verus_builtin::Ghost", VerusItem::BuiltinType(BuiltinTypeItem::Ghost)), - ("verus::verus_builtin::Tracked", VerusItem::BuiltinType(BuiltinTypeItem::Tracked)), -+ ("verus::verus_builtin::TypeIdSpec", VerusItem::BuiltinType(BuiltinTypeItem::TypeId)), +@@ -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, + } - ("verus::verus_builtin::Integer", VerusItem::BuiltinTrait(BuiltinTraitItem::Integer)), - ("verus::verus_builtin::Chainable", VerusItem::BuiltinTrait(BuiltinTraitItem::Chainable)), + 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..0e25a040 +index 00000000..faa3057c --- /dev/null +++ b/source/rust_verify_test/tests/type_id.rs -@@ -0,0 +1,157 @@ +@@ -0,0 +1,245 @@ +#![feature(rustc_private)] +#[macro_use] +mod common; @@ -231,22 +244,48 @@ index 00000000..0e25a040 + } => Ok(()) +} + -+// A TypeIdSpec is an ordinary ghost value: it can be stored, passed and compared. ++// 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, TypeIdSpec}; ++ use verus_builtin::type_id; ++ use core::any::TypeId; + struct Wrap(T); -+ proof fn t(x: TypeIdSpec) { ++ proof fn t(x: TypeId) { + let s = Wrap(x); + assert(s.0 == x); + } -+ spec fn is_u8(x: TypeIdSpec) -> bool { x == type_id::() } ++ 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. @@ -269,14 +308,76 @@ index 00000000..0e25a040 + } => Err(err) => assert_one_fails(err) +} + -+// Identity is *undecorated*: `&T` and `T` share a TypeIdSpec. This differs from -+// core::any::TypeId, and is forced by the encoding -- a decoration is not part -+// of the `Type` sort that tags are computed from. ++// 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_not_part_of_identity verus_code! { ++ #[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::()); // FAILS ++ 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) +} @@ -302,10 +403,10 @@ index 00000000..0e25a040 + } => 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 27e6c0a4..4fbf978c 100644 +index f25bb602..2fa0c741 100644 --- a/source/vir/src/ast.rs +++ b/source/vir/src/ast.rs -@@ -255,6 +255,17 @@ pub enum Primitive { +@@ -252,6 +252,17 @@ pub enum Primitive { StrSlice, Ptr, // Mut ptr, unless Const decoration is applied Global, @@ -323,7 +424,7 @@ index 27e6c0a4..4fbf978c 100644 } #[derive(Debug, Serialize, Deserialize, Hash, ToDebugSNode, Clone)] -@@ -372,6 +383,8 @@ pub enum NullaryOpr { +@@ -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), @@ -345,7 +446,7 @@ index 2eee24f6..f38d6fef 100644 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 cd8d44b5..70a2c5d8 100644 +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 { @@ -360,10 +461,20 @@ index cd8d44b5..70a2c5d8 100644 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..0fe050a6 100644 +index f3df0f2f..3e219714 100644 --- a/source/vir/src/context.rs +++ b/source/vir/src/context.rs -@@ -246,6 +246,7 @@ fn datatypes_invs( +@@ -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 => {} @@ -371,8 +482,16 @@ index f3df0f2f..0fe050a6 100644 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..4ae70b32 100644 +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 { @@ -383,7 +502,7 @@ index c006b3e9..4ae70b32 100644 TypX::FnDef(..) => false, TypX::MutRef(_) => false, TypX::Opaque { .. } => false, -@@ -156,6 +157,69 @@ fn datatype_or_fun_to_air_commands( +@@ -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))); @@ -405,21 +524,33 @@ index c006b3e9..4ae70b32 100644 + // 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()); -+ // types() is (Dcr, Type); only the Type component is tagged -+ if j + 1 == crate::def::types().len() { -+ tag_args.push(str_apply(crate::def::TYPE_TAG, &vec![v.clone()])); -+ } ++ 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( @@ -454,7 +585,7 @@ index c006b3e9..4ae70b32 100644 if declare_box { diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs -index 43e511e6..b3ff3663 100644 +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%"; @@ -465,7 +596,7 @@ index 43e511e6..b3ff3663 100644 const PREFIX_SNAPSHOT: &str = "snap%"; const SUBST_RENAME_SEPARATOR: &str = "$$"; const EXPAND_ERRORS_DECL_SEPARATOR: &str = "$$$"; -@@ -168,10 +169,12 @@ pub const BOX_INT: &str = "I"; +@@ -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"; @@ -478,7 +609,7 @@ index 43e511e6..b3ff3663 100644 pub const TYPE: &str = "Type"; pub const TYPE_ID_BOOL: &str = "BOOL"; pub const TYPE_ID_REAL: &str = "REAL"; -@@ -185,6 +188,39 @@ pub const TYPE_ID_SINT: &str = "SINT"; +@@ -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"; @@ -505,8 +636,21 @@ index 43e511e6..b3ff3663 100644 +// 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"; @@ -518,7 +662,7 @@ index 43e511e6..b3ff3663 100644 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 +633,11 @@ pub fn global_type() -> Path { +@@ -597,6 +646,11 @@ pub fn global_type() -> Path { Arc::new(PathX { krate: CrateId::Internal, segments: Arc::new(vec![ident]) }) } @@ -543,10 +687,10 @@ index f969aee9..e5789bf7 100644 TypX::MutRef(_) => false, TypX::Opaque { .. } => false, diff --git a/source/vir/src/modes.rs b/source/vir/src/modes.rs -index af50af46..bbbc1435 100644 +index ef61a3b7..88f7c12d 100644 --- a/source/vir/src/modes.rs +++ b/source/vir/src/modes.rs -@@ -2099,6 +2099,7 @@ fn check_expr( +@@ -2101,6 +2101,7 @@ fn check_expr( Ok((Mode::Spec, Proph::No)) } ExprX::NullaryOpr(crate::ast::NullaryOpr::ConstTypBound(..)) => Ok((Mode::Spec, Proph::No)), @@ -602,15 +746,17 @@ index 47141ba8..1d4b865c 100644 let e1 = visit_exp(ctx, state, e1); match op { diff --git a/source/vir/src/prelude.rs b/source/vir/src/prelude.rs -index 88b27055..434cad50 100644 +index 8d50db73..590da4d7 100644 --- a/source/vir/src/prelude.rs +++ b/source/vir/src/prelude.rs -@@ -147,6 +147,16 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< +@@ -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); @@ -622,7 +768,7 @@ index 88b27055..434cad50 100644 let type_id_global = str_to_node(TYPE_ID_GLOBAL); let type_id_mut_ref = str_to_node(TYPE_ID_MUT_REF); -@@ -187,6 +197,7 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< +@@ -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) @@ -630,7 +776,7 @@ index 88b27055..434cad50 100644 (declare-const [type_id_bool] [typ]) (declare-const [type_id_int] [typ]) (declare-const [type_id_nat] [typ]) -@@ -200,6 +211,21 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< +@@ -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]) @@ -652,7 +798,22 @@ index 88b27055..434cad50 100644 (declare-sort [decoration] 0) (declare-const [decorate_nil_sized] [decoration]) (declare-const [decorate_nil_slice] [decoration]) -@@ -358,6 +384,109 @@ pub(crate) fn prelude_nodes(name_ctxt: &NameCtxt, config: PreludeConfig) -> Vec< +@@ -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 ))) @@ -715,6 +876,90 @@ index 88b27055..434cad50 100644 + :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 @@ -726,23 +971,26 @@ index 88b27055..434cad50 100644 + :qid prelude_type_tag_const_bool + :skolemid skolem_prelude_type_tag_const_bool + ))) -+ // The decoration argument is deliberately NOT folded in: tags model -+ // undecorated type identity, so `&T` and `T` share a tag. See the -+ // decoration note in docs/verus-typeid-implementation-plan.md. ++ // 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)) ([type_tag] t))) ++ (= ([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)) ([type_tag] t))) ++ (= ([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)) ([type_tag] t))) ++ (= ([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 @@ -754,7 +1002,9 @@ index 88b27055..434cad50 100644 + // 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)) ([type_tag] t)) ([type_tag] 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 @@ -791,7 +1041,7 @@ index b2a3e9c3..0201dbb8 100644 TypX::Decorate(dec, ..) => match dec { diff --git a/source/vir/src/resolve_axioms.rs b/source/vir/src/resolve_axioms.rs -index 7f7c319e..1ff43048 100644 +index 56b98e99..c7667321 100644 --- a/source/vir/src/resolve_axioms.rs +++ b/source/vir/src/resolve_axioms.rs @@ -69,7 +69,10 @@ impl ResolvedTypeCollection { @@ -807,7 +1057,7 @@ index 7f7c319e..1ff43048 100644 } TypX::Decorate(dec, _, t) => { diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs -index 4fc96b2a..e8933533 100644 +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 { @@ -835,7 +1085,22 @@ index 4fc96b2a..e8933533 100644 TypX::AnonymousClosure(..) => { panic!("internal error: AnonymousClosure should have been removed by ast_simplify") } -@@ -301,7 +305,9 @@ fn big_int_to_expr(i: &BigInt) -> Expr { +@@ -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 { @@ -846,7 +1111,7 @@ index 4fc96b2a..e8933533 100644 Primitive::Slice | Primitive::StrSlice => crate::def::DECORATE_NIL_SLICE, } } -@@ -592,7 +598,7 @@ pub(crate) fn typ_invariant(ctx: &Ctx, typ: &Typ, expr: &Expr) -> Option { +@@ -592,7 +606,7 @@ pub(crate) fn typ_invariant(ctx: &Ctx, typ: &Typ, expr: &Expr) -> Option { panic!("abstract datatype should be boxed") } } @@ -855,7 +1120,7 @@ index 4fc96b2a..e8933533 100644 } None } -@@ -652,6 +658,7 @@ fn try_box(ctx: &Ctx, expr: Expr, typ: &Typ) -> Option { +@@ -652,6 +666,7 @@ fn try_box(ctx: &Ctx, expr: Expr, typ: &Typ) -> Option { } } TypX::Dyn(..) => None, @@ -863,7 +1128,7 @@ index 4fc96b2a..e8933533 100644 TypX::Primitive(_, _) => { prefix_typ_as_mono(ctx, |p| ctx.name_ctxt.prefix_box(p), typ, "primitive type") } -@@ -692,6 +699,7 @@ pub(crate) fn try_unbox(ctx: &Ctx, expr: Expr, typ: &Typ) -> Option { +@@ -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())) } @@ -871,7 +1136,7 @@ index 4fc96b2a..e8933533 100644 TypX::Primitive(_, _) => { prefix_typ_as_mono(ctx, |p| ctx.name_ctxt.prefix_unbox(p), typ, "primitive type") } -@@ -725,6 +733,26 @@ pub(crate) fn ctor_to_apply<'a>( +@@ -725,6 +741,35 @@ pub(crate) fn ctor_to_apply<'a>( (variant, field_exps) } @@ -881,6 +1146,15 @@ index 4fc96b2a..e8933533 100644 +/// 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); @@ -898,15 +1172,19 @@ index 4fc96b2a..e8933533 100644 fn str_to_const_str(ctx: &Ctx, s: Arc) -> Expr { Arc::new(ExprX::Apply( str_ident(STRSLICE_NEW_STRLIT), -@@ -1059,6 +1087,12 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< +@@ -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%tag()`. ++ // `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, &vec![typ_to_id(ctx, 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) { @@ -940,6 +1218,61 @@ index fc2b8717..c3162918 100644 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 @@ -952,3 +1285,42 @@ index 89c59c93..3dbc7260 100644 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 2cd45cabb..4523de217 100644 --- a/verified_libs/vstd_extra/src/lib.rs +++ b/verified_libs/vstd_extra/src/lib.rs @@ -43,4 +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 index 3878b22b1..787e6b182 100644 --- a/verified_libs/vstd_extra/src/typing/example.rs +++ b/verified_libs/vstd_extra/src/typing/example.rs @@ -66,16 +66,16 @@ pub proof fn erased_is_exactly_one(x: &dyn Any) { } -/// Recovering the concrete value, with no precondition at all. +/// Identifying an erased value, with no precondition at all. /// -/// The caller does not have to know what `x` is: [`downcast_ref`] tests, and the -/// `<==>` in its postcondition is strong enough to conclude both that a match -/// yields an `L2` and that a non-match cannot. -pub exec fn downcast_l2<'a>(x: &'a dyn Any) -> (r: Option<&'a L2>) +/// 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 is Some) <==> x.type_id_spec() == type_id::(), + r <==> x.type_id_spec() == type_id::(), { - downcast_ref::(x) + is_::(x) } /// The test discriminates, executably. @@ -89,16 +89,16 @@ pub exec fn downcast_discriminates(b: &L2, c: &L3) let ec: &dyn Any = c; assert(eb.type_id_spec() == type_id::()); assert(ec.type_id_spec() == type_id::()); - let ok = downcast_l2(eb); - assert(ok is Some); - let no = downcast_l2(ec); - assert(no is None); + 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 read as an `L1`, and it is why -/// [`downcast_ref`]'s rejecting half is sound rather than merely stated. +/// 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(), diff --git a/verified_libs/vstd_extra/src/typing/example_meta.rs b/verified_libs/vstd_extra/src/typing/example_meta.rs deleted file mode 100644 index 06f136a1a..000000000 --- a/verified_libs/vstd_extra/src/typing/example_meta.rs +++ /dev/null @@ -1,429 +0,0 @@ -//! A syntax-faithful mimic of the frame layer's `dyn` casts. -//! -//! Every item here matches `ostd/src/mm/frame/meta.rs` and -//! `ostd/src/mm/frame/mod.rs` as closely as the types allow — same field shapes, -//! same casts, same call syntax — with the metadata impls reduced to dummies. The -//! purpose is to locate precisely where Verus stops accepting the real code. -//! -//! The four casts, in the order the frame layer performs them: -//! -//! 1. `&metadata as &dyn AnyFrameMeta` then `core::ptr::metadata(..)`, capturing a -//! vtable pointer at write time — `MetaSlot::write_meta`. -//! 2. `core::ptr::from_raw_parts_mut(storage_ptr, vtable_ptr)` to rebuild a -//! `*mut dyn AnyFrameMeta`, then dispatch `on_drop` through it and -//! `drop_in_place` it — `MetaSlot::drop_meta_in_place`. -//! 3. `transmute::, Frame>` — `Frame::into_dyn`. -//! 4. `(meta as &dyn core::any::Any).is::()` then the reverse transmute — -//! `TryFrom> for Frame`. -//! -//! # Result -//! -//! Casts 1–3 are accepted as written. The wide-pointer construction, the dispatch -//! through a rebuilt `*mut dyn`, and the transmutes all typecheck, needing -//! `external_body` only because `core::ptr::metadata`, `from_raw_parts_mut`, -//! `drop_in_place` and `transmute` have no Verus specifications. Nothing about -//! `dyn` itself obstructs them. -//! -//! Three registrations are needed first, none of them hard: -//! -//! - `UnsafeCell` has no `vstd` specification, so upstream's `MetaSlot` fields -//! cannot be written until it is registered — and the registration Verus's own -//! diagnostic suggests is incomplete, needing `external_body` as well because -//! `UnsafeCell`'s field is private. This is what our `PCell`/`PPtr` fields avoid. -//! - `DynMetadata` registers cleanly, but its parameter must be bounded by -//! `PointeeSized`, not `?Sized`: under `feature(sized_hierarchy)` a `?Sized` -//! proxy still carries a `MetaSized` predicate the external type does not have, -//! and the bounds must match exactly. -//! - `write_meta` needs an explicit `M: 'static`. Upstream gets it free from -//! `AnyFrameMeta: Any`, since `Any: 'static`; without `Any` the coercion inside -//! `core::ptr::metadata` fails with `E0310`. -//! -//! Cast 4 is **impossible in Verus today**, and not for want of a proof. It needs -//! `AnyFrameMeta: Any`, and: -//! -//! - Declaring that bound makes Verus panic rather than report an error: -//! `thread 'rustc' panicked at vir/src/traits.rs:1610: compute_dyn_compatibility: -//! missing trait Path(core, ["any" :: "Any"])`. The panic fires because -//! `compute_dyn_compatibility` looks every supertrait up in its map of -//! Verus-known traits, and `core::any::Any` is registered nowhere in `vstd`. -//! - Registering it is then blocked by two checks that contradict each other. -//! `type ExternalTraitSpecificationFor: Any;` fails with *external_trait_ -//! specification trait bound mismatch*, the diagnostic naming the missing bound -//! as `'static`. Adding it — `: Any + 'static` — fails with *unexpected bound in -//! ExternalTraitSpecificationFor*. Since `Any: 'static` is part of `Any`'s own -//! definition and the bounds must match exactly, no spelling satisfies both. -//! - Without the bound, the cast is rejected by *rustc*, before Verus sees it: -//! `E0605: non-primitive cast: &dyn AnyMeta as &(dyn core::any::Any + 'static)`. -//! -//! # `EitherType` cannot stand in for `Any` either -//! -//! The natural repair is to notice that `x as &dyn Any` is a dyn-to-dyn *upcast*, -//! and to put [`super::types::EitherType`] in that slot: make it a supertrait of -//! `AnyMeta`, upcast to `&dyn EitherType`, and read the id from there. It would -//! be a one-to-one syntactic match, and it would recover the id through the -//! upcast rather than through `AnyMeta`. -//! -//! It does not work, for a reason more basic than anything about `Any`: -//! -//! > `the trait bound Dyn<2, ()>: T196_Either is not satisfied` -//! -//! **Verus's dyn type does not implement the erased trait's Verus supertraits.** -//! Probed with a parameter-free supertrait carrying a single spec fn, which fails -//! identically (`Dyn<3, ()>: T198_Marker`), so this is not about `EitherType`'s -//! generics. Only marker and auto traits (`Send`, `Sync`) survive in supertrait -//! position. The same root cause explains two earlier observations: `dyn HasId` -//! does not typecheck because `HasId: TypeSet`, and a spec fn inherited from a -//! supertrait is not preserved across the `&T -> &dyn Trait` coercion. Verus -//! simply does not model the supertrait relation for dyn types. -//! -//! Verus does have an escape hatch — its `unsized_blanketed_traits` set makes a -//! supertrait usable if it has an unbounded `impl`. That cannot help -//! here: a blanket impl gives every type the *same* id, and an identity trait -//! whose answer does not depend on the type is no identity trait. -//! -//! So a `dyn` trait in Verus must be self-contained: everything an erased value -//! needs to report has to be declared on that one trait. [`try_from_tagged`] is -//! therefore not a workaround for a missing feature — it is the only shape -//! available, and [`AnyMeta::type_id`] must live where it does. -//! -//! So `/*Any +*/` in our `AnyFrameMeta`, and the commented-out `TryFrom`, are -//! forced rather than chosen. Verus needs either a `vstd` registration of `Any` or -//! `'static` support in `external_trait_specification` before a downcast built on -//! `Any` can be verified. -//! -//! [`try_from_tagged`] is the replacement, mirroring cast 4 with the one -//! substitution that makes it expressible: `Any::is::()` becomes a comparison of -//! a dyn-dispatched tag against a statically known one. That test is *verified*, -//! and the `Result` shape, the unchanged-on-failure `Err`, and the transmute are -//! all preserved. -//! -//! Note the field types below are upstream Asterinas's, not the ones in our -//! `MetaSlot` — ours carries `vtable_ptr: PPtr` under a comment reading -//! "VERUS LIMITATION: Currently we do not verify this because of the dependency on -//! the `dyn Trait` pattern". Casts 1–3 are evidence that field can be restored to -//! `UnsafeCell>`. -use core::cell::UnsafeCell; -use core::marker::PhantomData; -use core::mem::MaybeUninit; -use core::ptr::DynMetadata; - -use vstd::prelude::*; - -use super::types::TypeId; - -verus! { - -/// Registers `UnsafeCell` with Verus. -/// -/// Needed because upstream's `MetaSlot` fields are `UnsafeCell`, and Verus has no -/// specification for it — our tree sidesteps this with `PCell`/`PPtr`. The -/// declaration is the one Verus's own diagnostic suggests. -#[verifier::reject_recursive_types(T)] -#[verifier::external_type_specification] -#[verifier::external_body] -pub struct ExUnsafeCell(UnsafeCell) where T: core::marker::MetaSized + ?Sized; - -/// Registers `DynMetadata` with Verus. -/// -/// The vtable-pointer type itself. Unlike `core::any::Any` this registers without -/// trouble — it carries no `'static` bound, which is the thing that made `Any` -/// unregisterable. -#[verifier::reject_recursive_types(T)] -#[verifier::external_type_specification] -#[verifier::external_body] -pub struct ExDynMetadata(DynMetadata); - -/// Mimics `FRAME_METADATA_MAX_SIZE`. -pub const META_MAX_SIZE: usize = 8; - -/// Mimics `MetaSlotStorage`. -/// -/// Upstream this is a raw `[u8; FRAME_METADATA_MAX_SIZE]`; ours is an exec-tagged -/// union. Kept as bytes here because the casts under test do not care which. -pub struct MetaSlotStorage { - pub bytes: [u8; META_MAX_SIZE], -} - -/// Mimics `AnyFrameMeta`. -/// -/// Same shape as the real trait: `unsafe`, `Send + Sync`, an `open spec fn` -/// per-impl precondition, and an exec `on_drop` on `&mut self` whose `requires` -/// calls that precondition. The real one also threads a `VmReader` and two -/// `Tracked` owner arguments; those are dropped as orthogonal to dispatch. -/// -/// `Any` is absent from the supertraits, exactly as in our tree. See the module -/// docs — the bound cannot be written, so [`Self::type_id`] takes its place. -pub unsafe trait AnyMeta: Send + Sync { - /// The id of *this value's* type, readable through an erased reference. - /// - /// Declared here rather than inherited from a supertrait, and not - /// `where Self: Sized`, because both are needed for it to survive the - /// `&M -> &dyn AnyMeta` coercion. This is the stand-in for `Any::type_id`. - spec fn type_id(&self) -> TypeIdSpec; - - /// The executable form, dispatched through the vtable. - fn type_id_val(&self) -> (r: TypeId) - ensures - r.view() == self.type_id(), - ; - - /// A value's identity is its type's identity. - /// - /// This is the whole of what `MetaTag` used to be. That trait gave every - /// implementor a hand-chosen `usize` and then required, by hand, that the - /// value's dispatched id agree with it -- its own doc called this "the fact - /// `Any` provides for free and the one thing that has to be supplied by hand". - /// It is now supplied for free: the body is empty because `type_id::()` - /// is exactly what `type_id` is obliged to return. - proof fn type_id_coherent(&self) where Self: core::marker::Sized - ensures - self.type_id() == type_id::(), - ; - - /// Per-impl precondition for [`Self::on_drop`]. Default is `true`. - open spec fn on_drop_pre(&self) -> bool { - true - } - - fn on_drop(&mut self) - requires - old(self).on_drop_pre(), - ; -} - -/// Mimics `FrameMetaVtablePtr`. -pub type MetaVtablePtr = DynMetadata; - -/// Mimics `MetaSlot`, with the fields upstream actually uses. -pub struct MetaSlot { - pub storage: UnsafeCell, - pub vtable_ptr: UnsafeCell>, -} - -/// A dummy metadata type, standing in for e.g. `MetaPageMeta`. -pub struct MetaA { - pub val: u64, -} - -/// A second dummy, so dispatch and downcasting have something to choose between. -/// With one impl a vtable-shaped call would verify vacuously. -pub struct MetaB { - pub val: u64, -} - -#[verifier::external] -unsafe impl Send for MetaA { - -} - -#[verifier::external] -unsafe impl Sync for MetaA { - -} - -#[verifier::external] -unsafe impl Send for MetaB { - -} - -#[verifier::external] -unsafe impl Sync for MetaB { - -} - -unsafe impl AnyMeta for MetaA { - open spec fn type_id(&self) -> TypeIdSpec { - type_id::() - } - - fn type_id_val(&self) -> (r: TypeId) { - TypeId::of::() - } - - proof fn type_id_coherent(&self) { - } - - #[verifier::external_body] - fn on_drop(&mut self) { - } -} - -unsafe impl AnyMeta for MetaB { - open spec fn type_id(&self) -> TypeIdSpec { - type_id::() - } - - fn type_id_val(&self) -> (r: TypeId) { - TypeId::of::() - } - - proof fn type_id_coherent(&self) { - } - - #[verifier::external_body] - fn on_drop(&mut self) { - } -} - -impl MetaSlot { - /// Cast 1 — upcast at write time. Mimics `MetaSlot::write_meta`. - /// - /// The body is the line that is *commented out* in our tree. It typechecks; - /// `external_body` is needed only because `core::ptr::metadata` has no spec. - /// Note the explicit `'static`. Upstream it is implied by `AnyFrameMeta: Any`, - /// since `Any: 'static`; with `Any` unavailable the bound has to be written by - /// hand, or `core::ptr::metadata` rejects the coercion with `E0310`. - #[verifier::external_body] - pub unsafe fn write_meta(&self, metadata: M) { - // SAFETY: Caller ensures that the access to the fields are exclusive. - let vtable_ptr = unsafe { &mut *self.vtable_ptr.get() }; - vtable_ptr.write(core::ptr::metadata(&metadata as &dyn AnyMeta)); - } - - /// Cast 2 — rebuild a wide pointer and dispatch through it. - /// Mimics `MetaSlot::drop_meta_in_place`. - /// - /// This is the shape our tree currently keeps alive only as a type-check. It - /// is accepted as written. - #[verifier::external_body] - pub unsafe fn drop_meta_in_place(&self) { - // SAFETY: We have exclusive access to the frame metadata. - let vtable_ptr = unsafe { &mut *self.vtable_ptr.get() }; - // SAFETY: The frame metadata is initialized and valid. - let vtable_ptr = unsafe { vtable_ptr.assume_init_read() }; - - let storage_ptr: *mut () = self.storage.get() as *mut (); - let meta_ptr: *mut dyn AnyMeta = core::ptr::from_raw_parts_mut(storage_ptr, vtable_ptr); - - // SAFETY: `ptr` points to the metadata storage which is valid to be - // mutably borrowed under `vtable_ptr` because the metadata is valid, - // the vtable is correct, and we have exclusive access. - unsafe { - // Invoke the custom `on_drop` handler. - (*meta_ptr).on_drop(); - // Drop the frame metadata. - core::ptr::drop_in_place(meta_ptr); - } - } - - /// Mimics `MetaSlot::dyn_meta_ptr`, the shared-reference form. - #[verifier::external_body] - pub unsafe fn dyn_meta_ptr(&self) -> *mut dyn AnyMeta { - // SAFETY: The page metadata is valid to be borrowed immutably, since it - // will never be borrowed mutably after initialization. - let vtable_ptr = unsafe { &*self.vtable_ptr.get() }; - - // SAFETY: The page metadata is initialized and valid. - let vtable_ptr = *unsafe { vtable_ptr.assume_init_ref() }; - - core::ptr::from_raw_parts_mut(self as *const MetaSlot as *mut MetaSlot, vtable_ptr) - } -} - -/// Mimics `Frame`. -/// -/// `#[repr(transparent)]` over a pointer plus a ZST phantom, as upstream, which is -/// what makes the transmutes in casts 3 and 4 layout-valid. -#[repr(transparent)] -pub struct Frame { - pub ptr: *const MetaSlot, - pub _marker: PhantomData, -} - -impl Frame { - /// Cast 3 — erase the static metadata type. Mimics `Frame::into_dyn`. - #[verifier::external_body] - pub fn into_dyn(self) -> Frame { - // SAFETY: `Frame` is `#[repr(transparent)]` over a thin pointer plus a - // zero-size `PhantomData`. `Frame` has the same runtime - // layout (thin pointer + ZST phantom). - unsafe { core::mem::transmute(self) } - } -} - -impl Frame { - /// The id of the metadata this frame points at. - /// - /// Uninterpreted here because the dummy slot carries no ghost state; in the - /// frame layer this is the region's view of the slot. - pub uninterp spec fn meta_id(&self) -> TypeIdSpec; - - /// Mimics `Frame::::dyn_meta`. - /// - /// The `ensures` is what makes the erased reference usable: without tying the - /// dispatched id back to the frame, a caller could compare tags and conclude - /// nothing about *this* frame. - #[verifier::external_body] - pub fn dyn_meta(&self) -> (r: &dyn AnyMeta) - ensures - r.type_id() == self.meta_id(), - { - // SAFETY: The metadata is initialized and valid. - unsafe { &*(*self.ptr).dyn_meta_ptr() } - } -} - -/// Cast 4, with the one substitution that makes it expressible. -/// -/// Mirrors `TryFrom> for Frame`, except that -/// -/// ```text -/// if (dyn_frame.dyn_meta() as &dyn core::any::Any).is::() { -/// ``` -/// -/// becomes -/// -/// ```text -/// if dyn_frame.dyn_meta().type_id_val().eq(&TypeId::of::()) { -/// ``` -/// -/// Both compare an id read through the vtable against one known statically, and -/// both ids are now the *same notion of identity* -- upstream reads it with -/// `TypeIdSpec::of`, we read it with `type_id::()`. Previously the right-hand side -/// was a hand-chosen `usize` from a `MetaTag` impl, related to the real identity -/// only by an obligation each implementor discharged by hand. -/// -/// A free function rather than a `TryFrom` impl, to keep the plumbing visible; -/// the `Result` shape and the unchanged-on-failure `Err` are preserved. -/// -/// The transmute stays `external_body`, as upstream. What is *gained* is that the -/// test guarding it is verified: the postcondition records that `Ok` happens -/// exactly when the frame's metadata has `M`'s id. -pub fn try_from_tagged(dyn_frame: Frame) -> (res: Result< - Frame, - Frame, ->) - ensures - (res is Ok) == (dyn_frame.meta_id() == type_id::()), -{ - if dyn_frame.dyn_meta().type_id_val().eq(&TypeId::of::()) { - // SAFETY: The metadata is coerceable and the struct is transmutable. - Ok(transmute_to_typed::(dyn_frame)) - } else { - Err(dyn_frame) - } -} - -/// The transmute half of cast 4, split out so the test above stays verified. -#[verifier::external_body] -pub fn transmute_to_typed(dyn_frame: Frame) -> Frame { - // SAFETY: The metadata is coerceable and the struct is transmutable. - unsafe { core::mem::transmute::, Frame>(dyn_frame) } -} - -/// The downcast admits the right type and rejects the other. -/// -/// Both directions matter and neither is vacuous: `Ok` needs the tags to agree, -/// and `Err` is what stops a `MetaB` frame from being read as a `MetaA`. -pub fn downcast_discriminates(a: Frame, b: Frame) - requires - a.meta_id() == type_id::(), - b.meta_id() == type_id::(), -{ - let ra = try_from_tagged::(a); - assert(ra is Ok); - let rb = try_from_tagged::(b); - assert(rb is Err); -} - -} // verus! diff --git a/verified_libs/vstd_extra/src/typing/mod.rs b/verified_libs/vstd_extra/src/typing/mod.rs index 7db4732ad..08aa230e9 100644 --- a/verified_libs/vstd_extra/src/typing/mod.rs +++ b/verified_libs/vstd_extra/src/typing/mod.rs @@ -1,5 +1,3 @@ pub mod types; -pub mod example; - -pub mod example_meta; +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 index cdc3815dc..4d0be0624 100644 --- a/verified_libs/vstd_extra/src/typing/types.rs +++ b/verified_libs/vstd_extra/src/typing/types.rs @@ -1,5 +1,7 @@ use vstd::prelude::*; +use core::any::TypeId; + use vstd::std_specs::convert::{IntoSpec, TryFromSpec}; verus! { @@ -8,17 +10,21 @@ verus! { /// /// 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 what makes a downcast sound: `type_id_spec` *cannot* +/// 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. +/// 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) -> TypeIdSpec; + spec fn type_id_spec(&self) -> TypeId; - /// The same identity, as a runtime value. + /// 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.view() == self.type_id_spec(), + r == self.type_id_spec(), ; /// A value's identity is its type's identity. @@ -36,9 +42,12 @@ pub trait AnyCast: Any { ; } -/// Blanket implementation of `Any` for all sized types. -impl Any for T { - open spec fn type_id_spec(&self) -> TypeIdSpec { +/// 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::() } @@ -50,7 +59,7 @@ impl Any for T { } } -impl AnyCast for T { +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 @@ -61,6 +70,11 @@ impl AnyCast for T { } /// `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::() } @@ -76,75 +90,18 @@ pub proof fn lemma_distinct_types_distinct_values TypeIdSpec; - - /// `core::any::TypeIdSpec::of::()`. - #[verifier::external_body] - pub exec fn of() -> (r: Self) - ensures - r.view() == type_id::(), - { - unimplemented!() - } - - /// Deciding identity at runtime. - #[verifier::external_body] - pub exec fn eq(&self, other: &Self) -> (r: bool) - returns - self.view() == other.view(), - { - unimplemented!() - } -} - -/// `::is` -pub exec fn is_(x: &dyn Any) -> (r: bool) +/// `::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::()) } -/// Reinterpretation, once identity is settled. -/// -/// The module's remaining assumed fact about identity, and it is now only the -/// *cast*: the test that guards it is [`is_`], which is verified. What licenses -/// the cast is [`Any::type_id_correct`] -- a value's reported identity is its -/// concrete type's, so a matching identity really does mean a `T`. -#[verifier::external_body] -pub exec fn downcast_ref_unchecked<'a, T: Any + Sized>(x: &'a dyn Any) -> (r: &'a T) - requires - is_type::(x), - ensures - r.type_id_spec() == x.type_id_spec(), -{ - unimplemented!() -} - -/// `::downcast_ref`. -/// -/// The `<==>` records both halves: it succeeds for the right type *and fails for -/// every other one*. -pub exec fn downcast_ref<'a, T: Any + Sized>(x: &'a dyn Any) -> (r: Option<&'a T>) - ensures - (r is Some) <==> is_type::(x), - r matches Some(v) ==> v.type_id_spec() == x.type_id_spec(), -{ - if is_::(x) { - Some(downcast_ref_unchecked::(x)) - } else { - None - } -} - // =========================================================================== // Representation // ===========================================================================