NonZero (new_unchecked) Proof for Contract (Init)

library/core/Cargo.toml

@@ -26,6 +26,7 @@ test = true
 
 [dependencies]
 safety = {path = "../contracts/safety" }
+paste = "1.0"
 
 [dev-dependencies]
 rand = { version = "0.8.5", default-features = false }

library/core/src/num/nonzero.rs

@@ -8,6 +8,10 @@ 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;
+use paste::paste;
 
 /// A marker trait for primitive types which can be zero.
 ///
@@ -348,6 +352,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 +369,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,
@@ -381,6 +403,10 @@ where
         }
     }
 
+
+
+
+
     /// Converts a reference to a non-zero mutable reference
     /// if the referenced value is not zero.
     #[unstable(feature = "nonzero_from_mut", issue = "106290")]
@@ -442,6 +468,9 @@ where
     }
 }
 
+
+
+
 macro_rules! nonzero_integer {
     (
         #[$stability:meta]
@@ -2171,3 +2200,43 @@ 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) => {
+            paste! {
+                #[kani::proof_for_contract(NonZero::new_unchecked)]
+                pub fn [<nonzero_check_new_unchecked_for_ $t>]() {
+                    let x: $t = kani::any();  // Generates a symbolic value of the provided type
+
+                    // Only proceed if x is not zero, because passing zero would violate the precondition
+                    kani::assume(x != 0);
+
+                    unsafe {
+                        let _ = <$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!(i16, core::num::NonZeroI16);
+    nonzero_check!(i32, core::num::NonZeroI32);
+    nonzero_check!(i64, core::num::NonZeroI64);
+    nonzero_check!(i128, core::num::NonZeroI128);
+    nonzero_check!(u8, core::num::NonZeroU8);
+    nonzero_check!(u16, core::num::NonZeroU16);
+    nonzero_check!(u32, core::num::NonZeroU32);
+    nonzero_check!(u64, core::num::NonZeroU64);
+    nonzero_check!(u128, core::num::NonZeroU128);
+    nonzero_check!(usize, core::num::NonZeroUsize);
+    nonzero_check!(isize, core::num::NonZeroIsize);
+}