NonZero (new_unchecked) Proof for Contract (Init)

library/core/src/num/nonzero.rs

@@ -8,7 +8,9 @@ use crate::ops::{BitOr, BitOrAssign, Div, DivAssign, Neg, Rem, RemAssign};
 use crate::panic::{RefUnwindSafe, UnwindSafe};
 use crate::str::FromStr;
 use crate::{fmt, intrinsics, ptr, ub_checks};
-
+use safety::{ensures, requires};
+#[cfg(kani)]
+use crate::kani;
 /// A marker trait for primitive types which can be zero.
 ///
 /// This is an implementation detail for <code>[NonZero]\<T></code> which may disappear or be replaced at any time.
@@ -348,6 +350,7 @@ where
     #[rustc_const_stable(feature = "const_nonzero_int_methods", since = "1.47.0")]
     #[must_use]
     #[inline]
+
     pub const fn new(n: T) -> Option<Self> {
         // SAFETY: Memory layout optimization guarantees that `Option<NonZero<T>>` has
         //         the same layout and size as `T`, with `0` representing `None`.
@@ -364,6 +367,23 @@ where
     #[rustc_const_stable(feature = "nonzero", since = "1.28.0")]
     #[must_use]
     #[inline]
+    #[rustc_allow_const_fn_unstable(const_refs_to_cell)]
+    #[requires({
+        let size = core::mem::size_of::<T>();
+        let ptr = &n as *const T as *const u8;
+        let slice = unsafe { core::slice::from_raw_parts(ptr, size) };
+        !slice.iter().all(|&byte| byte == 0)
+    })]
+    #[ensures(|result: &Self|{
+        let size = core::mem::size_of::<T>();
+        let n_ptr: *const T = &n;
+        let result_inner: T = result.get();
+        let result_ptr: *const T = &result_inner;
+        let n_slice = unsafe { core::slice::from_raw_parts(n_ptr as *const u8, size) };
+        let result_slice = unsafe { core::slice::from_raw_parts(result_ptr as *const u8, size) };
+
+        n_slice == result_slice
+    })]
     pub const unsafe fn new_unchecked(n: T) -> Self {
         match Self::new(n) {
             Some(n) => n,
@@ -442,6 +462,9 @@ where
     }
 }
 
+
+
+
 macro_rules! nonzero_integer {
     (
         #[$stability:meta]
@@ -2171,3 +2194,38 @@ nonzero_integer! {
     swapped = "0x5634129078563412",
     reversed = "0x6a2c48091e6a2c48",
 }
+
+#[unstable(feature="kani", issue="none")]
+#[cfg(kani)]
+    mod verify {
+    use core::num::NonZeroI32; // Use core::num instead of std::num
+    use super::*;
+    use NonZero;
+
+    macro_rules! nonzero_check {
+        ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => {
+            #[kani::proof_for_contract(NonZero::new_unchecked)]
+            pub fn $nonzero_check_new_unchecked_for() {
+                let x: $t = kani::any();  // Generates a symbolic value of the provided type
+
+                unsafe {
+                    <$nonzero_type>::new_unchecked(x);  // Calls NonZero::new_unchecked for the specified NonZero type
+                }
+            }
+        };
+    }
+
+    // Use the macro to generate different versions of the function for multiple types
+    nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8);
+    nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16);
+    nonzero_check!(i32, core::num::NonZeroI32, nonzero_check_new_unchecked_for_32);
+    nonzero_check!(i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64);
+    nonzero_check!(i128, core::num::NonZeroI128, nonzero_check_new_unchecked_for_128);
+    nonzero_check!(isize, core::num::NonZeroIsize, nonzero_check_new_unchecked_for_isize);
+    nonzero_check!(u8, core::num::NonZeroU8, nonzero_check_new_unchecked_for_u8);
+    nonzero_check!(u16, core::num::NonZeroU16, nonzero_check_new_unchecked_for_u16);
+    nonzero_check!(u32, core::num::NonZeroU32, nonzero_check_new_unchecked_for_u32);
+    nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64);
+    nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128);
+    nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize);
+}