Remove wrappers and contracts per PR comments (#2)

Author: celinval

library/core/src/unicode/mod.rs

@@ -35,51 +35,17 @@ pub const UNICODE_VERSION: (u8, u8, u8) = unicode_data::UNICODE_VERSION;
 #[cfg(kani)]
 mod verify {
     use super::conversions::{to_upper, to_lower};
-    use wrappers::*;
     use crate::kani;
-    use safety::*;
 
-    /// Wrapper functions used to verify auto-generated functions from this module.
-    ///
-    /// The files in this module are auto-generated by a script, so they are harder to annotate.
-    /// Instead, for each function that we want to verify, we create a wrapper function with
-    /// contracts.
-    mod wrappers {
-        use super::*;
-        use crate::ub_checks;
-
-        /// Wraps `conversions::to_upper` function.
-        ///
-        /// ```no_run
-        /// pub fn to_upper(c: char) -> [char; 3] {
-        /// # todo!()
-        /// }
-        /// ```
-        #[ensures(|res| ub_checks::can_dereference(res))]
-        pub fn to_upper_wrapper(c: char) -> [char; 3] {
-            to_upper(c)
-        }
-
-        /// Wraps `conversions::to_lower` function.
-        ///
-        /// ```no_run
-        /// pub fn to_lower(c: char) -> [char; 3] {
-        /// # todo!()
-        /// }
-        /// ```
-        #[ensures(|res| ub_checks::can_dereference(res))]
-        pub fn to_lower_wrapper(c: char) -> [char; 3] {
-            to_lower(c)
-        }
-    }
-
-    #[kani::proof_for_contract(to_upper_wrapper)]
+    /// Checks that `to_upper` does not trigger UB or panics for all valid characters.
+    #[kani::proof]
     fn check_to_upper_safety() {
-        let _ = to_upper_wrapper(kani::any());
+        let _ = to_upper(kani::any());
     }
 
-    #[kani::proof_for_contract(to_lower_wrapper)]
+    /// Checks that `to_lower` does not trigger UB or panics for all valid characters.
+    #[kani::proof]
     fn check_to_lower_safety() {
-        let _ = to_lower_wrapper(kani::any());
+        let _ = to_lower(kani::any());
     }
 }