Add contract to unicode to_upper and to_lower

This is currently hitting a bug in Kani. :(

library/core/src/unicode/mod.rs

@@ -31,3 +31,58 @@ mod unicode_data;
 /// [Unicode 11.0 or later, Section 3.1 Versions of the Unicode Standard](https://www.unicode.org/versions/Unicode11.0.0/ch03.pdf#page=4).
 #[stable(feature = "unicode_version", since = "1.45.0")]
 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 is 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 and add
+    /// contracts for them instead.
+    mod wrappers {
+        use super::*;
+
+        /// Wraps `conversions::to_upper` function.
+        ///
+        /// ```no_run
+        /// pub fn to_upper(c: char) -> [char; 3] {
+        /// # todo!()
+        /// }
+        /// ```
+        #[ensures(|res| c.is_ascii() == res[0].is_ascii())]
+        #[ensures(|res| if c.is_ascii() { &res[1..2] == &['\0', '\0'] } else { true })]
+        #[ensures(|res| if ('a'..'z').contains(&c) { ('A'..'Z').contains(&res[0]) } else { c == res[0] })]
+        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| c.is_ascii() == res[0].is_ascii())]
+        #[ensures(|res| if c.is_ascii() { &res[1..2] == &['\0', '\0'] } else { true })]
+        #[ensures(|res| if ('A'..'Z').contains(&c) { ('a'..'z').contains(&res[0]) } else { c == res[0] })]
+        pub fn to_lower_wrapper(c: char) -> [char; 3] {
+            to_lower(c)
+        }
+    }
+
+    #[kani::proof_for_contract(to_upper_wrapper)]
+    fn check_to_upper() {
+        let _ = to_upper_wrapper(kani::any());
+    }
+
+    #[kani::proof_for_contract(to_lower_wrapper)]
+    fn check_to_lower() {
+        let _ = to_upper_wrapper(kani::any());
+    }
+}