Contracts & Harnesses for len, is_empty, is_aligned, and is_aligned_to (#128)

Changes
added contract and harness for len, is_empty, is_aligned, and
is_aligned_to in the non-null library.

```
Complete - 4 successfully verified harnesses, 0 failures, 4 total.
```

---------

Co-authored-by: Carolyn Zech <[email protected]>

Author: Jimmycreative

library/core/src/ptr/non_null.rs

@@ -1387,6 +1387,7 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[stable(feature = "pointer_is_aligned", since = "1.79.0")]
     #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")]
+    #[ensures(|result: &bool| *result == (self.as_ptr().addr() % core::mem::align_of::<T>() == 0))]
     pub const fn is_aligned(self) -> bool
     where
         T: Sized,
@@ -1502,6 +1503,8 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[unstable(feature = "pointer_is_aligned_to", issue = "96284")]
     #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")]
+    #[requires(align.is_power_of_two())]
+    #[ensures(|result: &bool| *result == (self.as_ptr().addr() % align == 0))] // Ensure the returned value is correct based on the given alignment
     pub const fn is_aligned_to(self, align: usize) -> bool {
         self.pointer.is_aligned_to(align)
     }
@@ -1881,6 +1884,14 @@ mod verify {
     use crate::ptr::null_mut;
     use kani::PointerGenerator;
 
+    impl<T> kani::Arbitrary for NonNull<T> {
+        fn any() -> Self {
+            let ptr: *mut T = kani::any::<usize>() as *mut T;
+            kani::assume(!ptr.is_null());
+            NonNull::new(ptr).expect("Non-null pointer expected")
+        }
+    }
+
     // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
     #[kani::proof_for_contract(NonNull::new_unchecked)]
     pub fn non_null_check_new_unchecked() {
@@ -2179,4 +2190,70 @@ mod verify {
             assert_eq!(old_b, new_a);
         }
     }
+
+    #[kani::proof]
+    pub fn non_null_check_len() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i8> = kani::any();
+        // Create a non-deterministic size using kani::any()
+        let size: usize = kani::any();
+        // Create a NonNull slice from the non-null pointer and size
+        let non_null_slice: NonNull<[i8]> = NonNull::slice_from_raw_parts(non_null_ptr, size);
+
+        // Perform the length check
+        let len = non_null_slice.len();
+        assert!(len == size);
+    }
+
+    #[kani::proof]
+    pub fn non_null_check_is_empty() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i8> = kani::any();
+        // Create a non-deterministic size using kani::any(), constrained to zero
+        let size: usize = 0;
+
+        // Create a NonNull slice from the non-null pointer and size
+        let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) };
+
+        // Perform the is_empty check
+        let is_empty = non_null_slice.is_empty();
+        assert!(is_empty);
+    }
+
+    #[kani::proof_for_contract(NonNull::is_aligned)]
+    pub fn non_null_slice_is_aligned_check() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned();
+
+    }
+
+    #[kani::proof_for_contract(NonNull::is_aligned_to)]
+    pub fn non_null_check_is_aligned_to() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Create a non-deterministic alignment using kani::any()
+        let align: usize = kani::any();
+        kani::assume(align > 0); // Ensure alignment is greater than zero
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned_to(align);
+            
+    }
+
+    #[kani::proof]
+    #[kani::should_panic] // Add this if we expect a panic when the alignment is invalid
+    pub fn non_null_check_is_aligned_to_no_power_two() {
+        // Create a non-deterministic NonNull pointer using kani::any()
+        let non_null_ptr: NonNull<i32> = kani::any();
+
+        // Create a non-deterministic alignment value using kani::any()
+        let align: usize = kani::any();
+
+        // Perform the alignment check
+        let result = non_null_ptr.is_aligned_to(align);
+    }
 }