Address feedback

library/core/src/ascii/ascii_char.rs

@@ -453,7 +453,7 @@ impl AsciiChar {
     /// or returns `None` if it's too large.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
-    #[ensures(|result| (b <= 127) == result.is_some())]
+    #[ensures(|result| (b <= 127) == (result.is_some() && result.unwrap() as u8 == b))]
     pub const fn from_u8(b: u8) -> Option<Self> {
         if b <= 127 {
             // SAFETY: Just checked that `b` is in-range
@@ -472,6 +472,7 @@ impl AsciiChar {
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
     #[requires(b <= 127)]
+    #[ensures(|result| *result as u8 == b)]
     pub const unsafe fn from_u8_unchecked(b: u8) -> Self {
         // SAFETY: Our safety precondition is that `b` is in-range.
         unsafe { transmute(b) }
@@ -632,7 +633,7 @@ mod verify {
     #[kani::proof_for_contract(AsciiChar::from_u8)]
     fn check_from_u8() {
         let b: u8 = kani::any();
-        unsafe { AsciiChar::from_u8(b) };
+        AsciiChar::from_u8(b);
     }
 
     #[kani::proof_for_contract(AsciiChar::from_u8_unchecked)]

library/core/src/char/convert.rs

@@ -1,6 +1,6 @@
 //! Character conversions.
 
-use safety::requires;
+use safety::{requires, ensures};
 use crate::char::TryFromCharError;
 use crate::error::Error;
 use crate::fmt;
@@ -26,6 +26,7 @@ pub(super) const fn from_u32(i: u32) -> Option<char> {
 #[inline]
 #[must_use]
 #[requires(char_try_from_u32(i).is_ok())]
+#[ensures(|result| *result as u32 == i)]
 pub(super) const unsafe fn from_u32_unchecked(i: u32) -> char {
     // SAFETY: the caller must guarantee that `i` is a valid char value.
     unsafe {

library/core/src/char/methods.rs

@@ -1846,24 +1846,20 @@ pub fn encode_utf16_raw(mut code: u32, dst: &mut [u16]) -> &mut [u16] {
 mod verify {
     use super::*;
 
-    #[ensures(|result| c.is_ascii() == result.is_some())]
+    #[ensures(|result| c.is_ascii() == (result.is_some() && (result.unwrap() as u8 as char == *c)))]
     fn as_ascii_clone(c: &char) -> Option<ascii::Char> {
         c.as_ascii()
     }
 
     #[kani::proof_for_contract(as_ascii_clone)]
     fn check_as_ascii_ascii_char() {
         let ascii: char = kani::any_where(|c : &char| c.is_ascii());
-        unsafe { 
-            as_ascii_clone(&ascii);
-        };
+        as_ascii_clone(&ascii);
     }
 
     #[kani::proof_for_contract(as_ascii_clone)]
     fn check_as_ascii_non_ascii_char() {
         let non_ascii: char = kani::any_where(|c: &char| !c.is_ascii());
-        unsafe {
-            as_ascii_clone(&non_ascii);
-        }
+        as_ascii_clone(&non_ascii);
     }
 }