Deprecate deref_spec

Author: rikosellic

vstd_extra/src/external/deref.rs

@@ -8,6 +8,7 @@ use vstd::prelude::*;
 verus! {
 
 /// This is a workaround to add an uninterpreted specification of Deref trait, as Deref is included in Verus but does not have spec functions.
+/// It is currently not used, and we do not recommend using it, as it adds assumptions about the core of Rust's deref semantics, which may cause soundness issues if not used carefully.
 /// It may change if Verus adds native support for spec functions in the Deref trait.
 pub trait DerefSpec: Deref {
     spec fn deref_spec(&self) -> &<Self as Deref>::Target;

vstd_extra/src/external/mod.rs

@@ -7,6 +7,7 @@ pub mod ilog2;
 pub mod nonnull;
 pub mod smart_ptr;
 
+#[deprecated(note = "If you can, do not use this module as it adds assumptions about the core of Rust's deref semantics.")]
 pub use deref::*;
 pub use ilog2::*;
 pub use nonnull::*;