Remove RustItem::AllocGlobal

source/rust_verify/src/rust_to_vir.rs

@@ -229,7 +229,6 @@ fn check_item<'tcx>(
                 variant_data,
                 generics,
                 adt_def,
-                external_info,
             )?;
         }
         ItemKind::Enum(_ident, generics, enum_def) => {

source/rust_verify/src/rust_to_vir_adts.rs

@@ -3,7 +3,6 @@ use crate::context::Context;
 use crate::rust_to_vir_base::{
     check_generics_bounds_with_polarity, mk_visibility, mk_visibility_from_vis,
 };
-use crate::rust_to_vir_impl::ExternalInfo;
 use crate::unsupported_err_unless;
 use crate::util::err_span;
 use air::ast_util::str_ident;
@@ -127,7 +126,6 @@ pub(crate) fn check_item_struct<'tcx>(
     variant_data: &'tcx VariantData<'tcx>,
     generics: &'tcx Generics<'tcx>,
     adt_def: rustc_middle::ty::AdtDef<'tcx>,
-    external_info: &mut ExternalInfo,
 ) -> Result<(), VirErr> {
     assert!(adt_def.is_struct());
     let vattrs = ctxt.get_verifier_attrs(attrs)?;
@@ -144,7 +142,6 @@ pub(crate) fn check_item_struct<'tcx>(
             &vattrs,
             generics,
             adt_def,
-            external_info,
         );
     }
 
@@ -522,7 +519,6 @@ pub(crate) fn check_item_external<'tcx>(
     vattrs: &VerifierAttrs,
     generics: &'tcx Generics<'tcx>,
     proxy_adt_def: rustc_middle::ty::AdtDef<'tcx>,
-    external_info: &mut ExternalInfo,
 ) -> Result<(), VirErr> {
     // Like with functions, we disallow external_type_specification and external together
     // (This check is done in rust_to_vir)
@@ -573,17 +569,6 @@ pub(crate) fn check_item_external<'tcx>(
         );
     }
 
-    if crate::verus_items::get_rust_item(ctxt.tcx, external_adt_def.did())
-        == Some(crate::verus_items::RustItem::AllocGlobal)
-    {
-        // Don't need to add this to the krate, since we handle this as as a VIR Primitive.
-        // We only get this far so we can add ourselves to the type_ids list.
-        // note: seems that Global is added to lang_items in future version of Rust,
-        // which makes it easier to get the ID so we can simplify this.
-        external_info.add_type_id(external_adt_def.did());
-        return Ok(());
-    }
-
     // Check that the type args match.
 
     crate::rust_to_vir_base::check_item_external_generics(

source/rust_verify/src/rust_to_vir_base.rs

@@ -996,13 +996,6 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>(
             } else {
                 let rust_item = verus_items::get_rust_item(tcx, did);
 
-                if let Some(RustItem::AllocGlobal) = rust_item {
-                    return Ok((
-                        Arc::new(TypX::Primitive(Primitive::Global, 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];

source/rust_verify/src/rust_to_vir_impl.rs

@@ -53,10 +53,6 @@ impl ExternalInfo {
         }
     }
 
-    pub(crate) fn add_type_id(&mut self, def_id: DefId) {
-        self.type_id_map.insert(def_id, true);
-    }
-
     pub(crate) fn has_type_id<'tcx>(&mut self, ctxt: &Context<'tcx>, def_id: DefId) -> bool {
         match self.type_id_map.get(&def_id).copied() {
             None => {

source/rust_verify/src/verus_items.rs

@@ -711,8 +711,6 @@ pub(crate) enum RustItem {
     CloneClone,
     CloneFrom,
     IntIntrinsic(RustIntIntrinsicItem),
-    AllocGlobal,
-    Allocator,
     TryTraitBranch,
     ResidualTraitFromResidual,
     IntoIterFn,
@@ -825,12 +823,6 @@ pub(crate) fn get_rust_item_str(rust_path: Option<&str>) -> Option<RustItem> {
         return Some(RustItem::CloneFrom);
     }
 
-    if rust_path == Some("alloc::alloc::Global") {
-        return Some(RustItem::AllocGlobal);
-    }
-    if rust_path == Some("core::alloc::Allocator") {
-        return Some(RustItem::Allocator);
-    }
     if rust_path == Some("core::slice::index::private_slice_index::Sealed") {
         return Some(RustItem::SliceSealed);
     }

source/rust_verify_test/tests/adts.rs

@@ -236,6 +236,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test_well_founded1 verus_code! {
+        use vstd::std_specs::alloc::*;
         enum List {
             Cons(int, Box<List>)
         }
@@ -244,6 +245,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test_well_founded2 verus_code! {
+        use vstd::std_specs::alloc::*;
         enum List {
             Cons1(int, Box<List>),
             Cons2(int, Box<List>),
@@ -253,6 +255,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test_well_founded3 verus_code! {
+        use vstd::std_specs::alloc::*;
         enum List1 {
             Cons(int, Box<List2>)
         }
@@ -264,6 +267,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test_well_founded4 verus_code! {
+        use vstd::std_specs::alloc::*;
         enum List {
             Cons(int, (Box<List>, bool))
         }
@@ -272,6 +276,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test_well_field_unbox verus_code! {
+        use vstd::std_specs::alloc::*;
         struct B { b: bool }
         fn foo(s1: Box<B>, s2: &Box<B>, s3: Box<&B>, s4: Box<(bool, bool)>) {
             let z1 = s1.b;

source/rust_verify_test/tests/external_type_specification.rs

@@ -436,14 +436,21 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] type_recursion_is_handled verus_code! {
+        use vstd::std_specs::alloc::*;
+        #[verifier(external)]
+        pub enum SomeStruct<T> {
+            No,
+            Yes(T),
+        }
+
         #[verifier(external_type_specification)]
-        #[verifier::reject_recursive_types(U)]
-        pub struct ExOption<U>(core::option::Option<U>);
+        #[verifier(reject_recursive_types(U))]
+        pub struct ExSomeStruct<U>(SomeStruct<U>);
 
         struct Test {
-            t: Box<core::option::Option<Test>>,
+            t: Box<SomeStruct<Test>>,
         }
-    } => Err(err) => assert_vir_error_msg(err, "crate::Test recursively uses type crate::Test in a non-positive position")
+    } => Err(err) => assert_vir_error_msg(err, "Type test_crate::Test recursively uses type test_crate::Test in a non-positive position")
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/match.rs

@@ -71,6 +71,7 @@ test_verify_one_file! {
 
 test_verify_one_file_with_options! {
     #[test] test2 ["exec_allows_no_decreases_clause"] => verus_code! {
+        use vstd::std_specs::alloc::*;
         enum List<A> {
             Nil,
             Cons(A, Box<List<A>>),
@@ -120,6 +121,7 @@ test_verify_one_file_with_options! {
 
 test_verify_one_file_with_options! {
     #[test] test2_struct ["exec_allows_no_decreases_clause"] => verus_code! {
+        use vstd::std_specs::alloc::*;
         enum List<A> {
             Nil,
             Cons { hd: A, tl: Box<List<A>> },
@@ -169,6 +171,7 @@ test_verify_one_file_with_options! {
 
 test_verify_one_file_with_options! {
     #[test] test2_fails ["exec_allows_no_decreases_clause"] => verus_code! {
+        use vstd::std_specs::alloc::*;
         enum List<A> {
             Nil,
             Cons(A, Box<List<A>>),
@@ -575,6 +578,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test_or_patterns verus_code! {
+        use vstd::std_specs::alloc::*;
         #[is_variant]
         enum Foo {
             Bar(u64),

source/rust_verify_test/tests/recursion.rs

@@ -1637,6 +1637,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] decrease_through_abstract_type verus_code! {
+        use vstd::std_specs::alloc::*;
         mod m1 {
             use verus_builtin::*;
             pub struct S<A, B>(A, B);
@@ -1708,6 +1709,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] height_intrinsic verus_code! {
+        use vstd::std_specs::alloc::*;
         #[is_variant]
         enum Tree {
             Node(Box<Tree>, Box<Tree>),
@@ -1745,6 +1747,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] height_intrinsic_mode verus_code! {
+        use vstd::std_specs::alloc::*;
         #[is_variant]
         enum Tree {
             Node(Box<Tree>, Box<Tree>),
@@ -1759,6 +1762,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] datatype_height_axiom_checks_the_variant verus_code! {
+        use vstd::std_specs::alloc::*;
         #[is_variant]
         enum List {
             Cons(Box<List>),

source/rust_verify_test/tests/recursive_types.rs

@@ -5,6 +5,7 @@ use common::*;
 
 test_verify_one_file! {
     #[test] test1 verus_code! {
+        use vstd::std_specs::alloc::*;
         enum E1 {
             N(),
             E(Box<E1>),
@@ -14,6 +15,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test2 verus_code! {
+        use vstd::std_specs::alloc::*;
         enum E1 {
             N(),
             E(Box<E2>),
@@ -28,6 +30,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test3 verus_code! {
+        use vstd::std_specs::alloc::*;
         struct List<A> {
             a: A,
         }
@@ -46,6 +49,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test4 verus_code! {
+        use vstd::std_specs::alloc::*;
         struct List<A> {
             a: A,
         }
@@ -64,6 +68,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test1_ok verus_code! {
+        use vstd::std_specs::alloc::*;
         struct List<A> {
             a: A,
         }
@@ -78,6 +83,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test1_fails verus_code! {
+        use vstd::std_specs::alloc::*;
         #[verifier::reject_recursive_types(A)]
         struct List<A> {
             a: A,
@@ -93,6 +99,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test2_ok verus_code! {
+        use vstd::std_specs::alloc::*;
         struct List<A> {
             a: A,
         }
@@ -112,6 +119,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test2_fails verus_code! {
+        use vstd::std_specs::alloc::*;
         #[verifier::reject_recursive_types(A)]
         struct List<A> {
             a: A,
@@ -132,6 +140,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test3_ok verus_code! {
+        use vstd::std_specs::alloc::*;
         struct List<A> {
             a: A,
         }
@@ -151,6 +160,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test3_fails verus_code! {
+        use vstd::std_specs::alloc::*;
         #[verifier::reject_recursive_types(A)]
         struct List<A> {
             a: A,
@@ -271,6 +281,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] no_ground_variant2 verus_code! {
+        use vstd::std_specs::alloc::*;
         enum UngroundedList<A> {
             // error: no ground variant; the only variant is Cons, which recursively uses UngroundedList
             Cons(A, Box<UngroundedList<A>>),
@@ -280,6 +291,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] no_ground_variant_via_generics1 verus_code! {
+        use vstd::std_specs::alloc::*;
         // from https://github.com/verus-lang/verus/issues/538
         struct I<A>(A);
         struct R(Box<I<R>>);
@@ -303,6 +315,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] no_ground_variant_via_generics2 verus_code! {
+        use vstd::std_specs::alloc::*;
         // from https://github.com/verus-lang/verus/issues/538
         #[verifier::accept_recursive_types(A)]
         struct I<A>(A);

source/rust_verify_test/tests/regression.rs

@@ -340,6 +340,7 @@ test_verify_one_file_with_options! {
 
 test_verify_one_file! {
     #[test] air_function_names_issue_376 verus_code! {
+        use vstd::std_specs::alloc::*;
         enum Nat {
             Zero,
             Succ(Box<Nat>),

source/rust_verify_test/tests/traits.rs

@@ -4144,6 +4144,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test_recursion_through_sync_impl_is_checked verus_code! {
+        use vstd::std_specs::alloc::*;
         trait Tr {
             proof fn tr_g() {
             }
@@ -4192,6 +4193,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] test_recursion_through_send_impl_is_checked verus_code! {
+        use vstd::std_specs::alloc::*;
         trait Tr {
             proof fn tr_g() {
             }

source/rust_verify_test/tests/traits_dyn.rs

@@ -337,6 +337,7 @@ test_verify_one_file! {
 
 test_verify_one_file! {
     #[test] dyn_cycle3 verus_code! {
+        use vstd::std_specs::alloc::*;
         trait T {
             spec fn f(&self, d: &S) -> int;
         }