From db71987dd43e7826e7cdad856ac84a26e47afbc2 Mon Sep 17 00:00:00 2001
From: JY <53210261+Jimmycreative@users.noreply.github.com>
Date: Mon, 2 Dec 2024 17:07:27 -0800
Subject: [PATCH 1/4] Contracts & Harnesses for write_volatile (#167)

Contracts & Harnesses for `core::ptr::NonNull::write_volatile`.
---
 library/core/src/ptr/non_null.rs | 47 +++++++++++++++++++++++++++++++-
 1 file changed, 46 insertions(+), 1 deletion(-)

diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index 41e667752e305..715e70b98ea1d 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -1132,6 +1132,8 @@ impl<T: ?Sized> NonNull<T> {
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[cfg_attr(kani, kani::modifies(self.as_ptr()))]
+    #[requires(ub_checks::can_write(self.as_ptr()))]
     pub unsafe fn write_volatile(self, val: T)
     where
         T: Sized,
@@ -1775,7 +1777,7 @@ mod verify {
         let maybe_null_ptr =  if kani::any() { xptr as *mut i32 } else { null_mut() };
         let _ = NonNull::new(maybe_null_ptr);
     }
-    
+
     // pub const unsafe fn read(self) -> T where T: Sized
     #[kani::proof_for_contract(NonNull::read)]
     pub fn non_null_check_read() {
@@ -2300,4 +2302,47 @@ mod verify {
             let distance = ptr_nonnull.offset_from(origin_nonnull);
         }
     }
+
+    macro_rules! generate_write_volatile_harness {
+        ($type:ty, $byte_size:expr, $harness_name:ident) => {
+            #[kani::proof_for_contract(NonNull::write_volatile)]
+            pub fn $harness_name() {
+                // Create a pointer generator for the given type with appropriate byte size
+                let mut generator = kani::PointerGenerator::<$byte_size>::new();
+
+                // Get a raw pointer from the generator
+                let raw_ptr: *mut $type = generator.any_in_bounds().ptr;
+
+                // Create a non-null pointer from the raw pointer
+                let ptr = NonNull::new(raw_ptr).unwrap();
+
+                // Create a non-deterministic value to write
+                let new_value: $type = kani::any();
+
+                unsafe {
+                    // Perform the volatile write operation
+                    ptr.write_volatile(new_value);
+
+                    // Read back the value and assert it's correct
+                    assert_eq!(ptr.as_ptr().read_volatile(), new_value);
+                }
+            }
+        };
+    }
+
+    // Generate proof harnesses for multiple types with appropriate byte sizes
+    generate_write_volatile_harness!(i8, 1, non_null_check_write_volatile_i8);
+    generate_write_volatile_harness!(i16, 2, non_null_check_write_volatile_i16);
+    generate_write_volatile_harness!(i32, 4, non_null_check_write_volatile_i32);
+    generate_write_volatile_harness!(i64, 8, non_null_check_write_volatile_i64);
+    generate_write_volatile_harness!(i128, 16, non_null_check_write_volatile_i128);
+    generate_write_volatile_harness!(isize, {core::mem::size_of::<isize>()}, non_null_check_write_volatile_isize);
+    generate_write_volatile_harness!(u8, 1, non_null_check_write_volatile_u8);
+    generate_write_volatile_harness!(u16, 2, non_null_check_write_volatile_u16);
+    generate_write_volatile_harness!(u32, 4, non_null_check_write_volatile_u32);
+    generate_write_volatile_harness!(u64, 8, non_null_check_write_volatile_u64);
+    generate_write_volatile_harness!(u128, 16, non_null_check_write_volatile_u128);
+    generate_write_volatile_harness!(usize, {core::mem::size_of::<usize>()}, non_null_check_write_volatile_usize);
+    generate_write_volatile_harness!((), 1, non_null_check_write_volatile_unit);
+
 }

From ca85f7fcaa97901ba93138bf0abbc7b42130239d Mon Sep 17 00:00:00 2001
From: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com>
Date: Tue, 3 Dec 2024 00:54:05 -0800
Subject: [PATCH 2/4] Cstr - add proof from_bytes_with_null (#198)

Towards #150

Verifies that the CStr safety invariant holds after calling :

from_bytes_with_nul --> core::ffi::c_str module
---
 library/core/src/ffi/c_str.rs | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs
index fe97ed3e5f2fb..22dcbdd834746 100644
--- a/library/core/src/ffi/c_str.rs
+++ b/library/core/src/ffi/c_str.rs
@@ -885,7 +885,20 @@ mod verify {
             assert!(c_str.is_safe());
         }
     }
-  
+
+    #[kani::proof]
+    #[kani::unwind(17)] 
+    fn check_from_bytes_with_nul() {
+        const MAX_SIZE: usize = 16;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        let result = CStr::from_bytes_with_nul(slice);
+        if let Ok(c_str) = result {
+            assert!(c_str.is_safe());
+        }
+    }
+
     // pub const fn count_bytes(&self) -> usize
     #[kani::proof]
     #[kani::unwind(32)]
@@ -956,4 +969,4 @@ mod verify {
         assert_eq!(expected_is_empty, c_str.is_empty());
         assert!(c_str.is_safe());
   }
-}
\ No newline at end of file
+}

From 892ee59fa710697c5740cb239b5db15d16369ed0 Mon Sep 17 00:00:00 2001
From: Daniel Tu <135958699+danielhumanmod@users.noreply.github.com>
Date: Tue, 3 Dec 2024 06:07:28 -0800
Subject: [PATCH 3/4] Contracts & Harnesses for `byte_add`, `byte_offset`, and
 `byte_offset_from` (#103)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

# Description:

This PR introduces function contracts and proof harness for the NonNull
pointer in the Rust core library. Specifically, it verifies three new
APIs—`byte_offset`, `byte_add`, and `byte_offset_from` with Kani. These
changes enhance the functionality of pointer arithmetic and verification
for NonNull pointers.

# Changes Overview:

**Covered APIs:**
1. `NonNull::byte_add`: Adds a specified byte offset to a pointer.
2. `NonNull::byte_offset`: Allows calculating an offset from a pointer
in bytes.
4. `NonNull::byte_offset_from`: Calculates the distance between two
pointers in bytes.

**Proof harness:**
1. `non_null_byte_add_proof`
2. `non_null_byte_offset_proof`
3. `non_null_byte_offset_from_proof`

Towards #53
---
 library/core/src/ptr/non_null.rs | 86 ++++++++++++++++++++++++++++++++
 1 file changed, 86 insertions(+)

diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index 715e70b98ea1d..c347d8b82c4ac 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -526,6 +526,11 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[requires(
+        (self.as_ptr().addr() as isize).checked_add(count).is_some() &&
+        kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_byte_offset(count))
+    )]
+    #[ensures(|result: &Self| result.as_ptr() == self.as_ptr().wrapping_byte_offset(count))]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset` and `byte_offset` has
         // the same safety contract.
@@ -607,6 +612,10 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[requires(
+        count <= (isize::MAX as usize) - self.as_ptr().addr() &&  // Ensure the offset doesn't overflow
+        (count == 0 || kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_byte_add(count))) // Ensure the offset is within the same allocation
+    )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same
         // safety contract.
@@ -820,6 +829,14 @@ impl<T: ?Sized> NonNull<T> {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[requires(
+        self.as_ptr().addr() == origin.as_ptr().addr() ||
+        kani::mem::same_allocation(self.as_ptr() as *const(), origin.as_ptr() as *const())
+    )]
+    #[ensures(
+        |result: &isize|
+        *result == (self.as_ptr() as *const u8).offset_from(origin.as_ptr() as *const u8)
+    )]
     pub const unsafe fn byte_offset_from<U: ?Sized>(self, origin: NonNull<U>) -> isize {
         // SAFETY: the caller must uphold the safety contract for `byte_offset_from`.
         unsafe { self.pointer.byte_offset_from(origin.pointer) }
@@ -1736,6 +1753,7 @@ impl<T: ?Sized> From<&T> for NonNull<T> {
 mod verify {
     use super::*;
     use crate::ptr::null_mut;
+    use crate::mem;
     use kani::PointerGenerator;
 
     trait SampleTrait {
@@ -2345,4 +2363,72 @@ mod verify {
     generate_write_volatile_harness!(usize, {core::mem::size_of::<usize>()}, non_null_check_write_volatile_usize);
     generate_write_volatile_harness!((), 1, non_null_check_write_volatile_unit);
 
+    #[kani::proof_for_contract(NonNull::byte_add)]
+    pub fn non_null_byte_add_proof() {
+        // Make size as 1000 to ensure the array is large enough to cover various senarios
+        // while maintaining a reasonable proof runtime
+        const ARR_SIZE: usize = mem::size_of::<i32>() * 1000;
+        let mut generator = PointerGenerator::<ARR_SIZE>::new();
+
+        let count: usize = kani::any();
+        let raw_ptr: *mut i32 = generator.any_in_bounds().ptr as *mut i32;
+
+        unsafe {
+            let ptr = NonNull::new(raw_ptr).unwrap();
+            let result = ptr.byte_add(count);
+        }
+    }
+
+    #[kani::proof_for_contract(NonNull::byte_add)]
+    pub fn non_null_byte_add_dangling_proof() {
+        let ptr = NonNull::<i32>::dangling();
+        unsafe {
+            let _ = ptr.byte_add(0);
+        }
+    }
+
+    #[kani::proof_for_contract(NonNull::byte_offset)]
+    pub fn non_null_byte_offset_proof() {
+        const ARR_SIZE: usize = mem::size_of::<i32>() * 1000;
+        let mut generator = PointerGenerator::<ARR_SIZE>::new();
+
+        let count: isize = kani::any();
+        let raw_ptr: *mut i32 = generator.any_in_bounds().ptr as *mut i32;
+
+        unsafe {
+            let ptr = NonNull::new(raw_ptr).unwrap();
+            let result = ptr.byte_offset(count);
+        }
+    }
+
+    #[kani::proof_for_contract(NonNull::byte_offset_from)]
+    pub fn non_null_byte_offset_from_proof() {
+        const SIZE: usize = mem::size_of::<i32>() * 1000;
+        let mut generator1 = PointerGenerator::<SIZE>::new();
+        let mut generator2 = PointerGenerator::<SIZE>::new();
+
+        let ptr: *mut i32 = generator1.any_in_bounds().ptr as *mut i32;
+
+        let origin: *mut i32 = if kani::any() {
+            generator1.any_in_bounds().ptr as *mut i32
+        } else {
+            generator2.any_in_bounds().ptr as *mut i32
+        };
+
+        let ptr_nonnull = unsafe { NonNull::new(ptr).unwrap() };
+        let origin_nonnull = unsafe { NonNull::new(origin).unwrap() };
+
+        unsafe {
+            let result = ptr_nonnull.byte_offset_from(origin_nonnull);
+        }
+    }
+
+    #[kani::proof_for_contract(NonNull::byte_offset_from)]
+    pub fn non_null_byte_offset_from_dangling_proof() {
+        let origin = NonNull::<i32>::dangling();
+        let ptr = origin;
+        unsafe {
+            let _ = ptr.byte_offset_from(origin);
+        }
+    }
 }

From d0d9de25c44d829f52c837636284cbfa776f544e Mon Sep 17 00:00:00 2001
From: Yifei Wang <40480373+xsxszab@users.noreply.github.com>
Date: Tue, 3 Dec 2024 07:36:24 -0800
Subject: [PATCH 4/4] Contracts and Harnesses for `<*const T>::add`, `sub` and
 `offset` (#166)

Towards #76

**Summary**
* Adds contracts for <*const T>::add, sub and offset.
* Adds proof for contracts for above methods, verifying following
pointee types:
    * All integer types
    * Tuples (representing composite types)
    * Slices
    * Unit type
---
 library/core/src/ptr/const_ptr.rs | 369 ++++++++++++++++++++++++++++--
 1 file changed, 356 insertions(+), 13 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index b2cecbf053c81..ec67d891686fd 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -406,6 +406,21 @@ impl<T: ?Sized> *const T {
     #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`.
+        // Precondition 2: adding the computed offset to `self` does not cause overflow.
+        // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
+        count.checked_mul(core::mem::size_of::<T>() as isize)
+        .map_or(false, |computed_offset| (self as isize).checked_add(computed_offset).is_some()) &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_offset(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *const T
     where
         T: Sized,
@@ -673,7 +688,7 @@ impl<T: ?Sized> *const T {
         // Ensure the distance between `self` and `origin` is aligned to `T`
         (self as isize - origin as isize) % (mem::size_of::<T>() as isize) == 0 &&
         // Ensure both pointers are in the same allocation or are pointing to the same address
-        (self as isize == origin as isize || kani::mem::same_allocation(self, origin))
+        (self as isize == origin as isize || core::ub_checks::same_allocation(self, origin))
     )]
     // The result should equal the distance in terms of elements of type `T` as per the documentation above
     #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::<T>() as isize))]
@@ -928,6 +943,23 @@ impl<T: ?Sized> *const T {
     #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`.
+        // Precondition 2: adding the computed offset to `self` does not cause overflow.
+        // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani. 
+        count.checked_mul(core::mem::size_of::<T>())
+        .map_or(false, |computed_offset| {
+            computed_offset <= isize::MAX as usize && (self as isize).checked_add(computed_offset as isize).is_some()
+        }) &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_add(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1035,6 +1067,23 @@ impl<T: ?Sized> *const T {
     #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`.
+        // Precondition 2: substracting the computed offset from `self` does not cause overflow.
+        // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
+        count.checked_mul(core::mem::size_of::<T>())
+        .map_or(false, |computed_offset| {
+            computed_offset <= isize::MAX as usize && (self as isize).checked_sub(computed_offset as isize).is_some()
+        }) &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_sub(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -1726,19 +1775,300 @@ mod verify {
     use core::mem;
     use kani::PointerGenerator;
 
-    // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0
-    #[kani::proof_for_contract(<*const ()>::offset_from)]
-    #[kani::should_panic]
-    pub fn check_const_offset_from_unit() {
-        let val: () = ();
-        let src_ptr: *const () = &val;
-        let dest_ptr: *const () = &val;
-        unsafe {
-            dest_ptr.offset_from(src_ptr);
-        }
+    /// This macro generates a single verification harness for the `offset`, `add`, or `sub`
+    /// pointer operations, supporting integer, composite, or unit types.
+    /// - `$ty`: The type of the slice's elements (e.g., `i32`, `u32`, tuples).
+    /// - `$fn_name`: The name of the function being checked (`add`, `sub`, or `offset`).
+    /// - `$proof_name`: The name assigned to the generated proof for the contract.
+    /// - `$count_ty:ty`: The type of the input variable passed to the method being invoked.
+    ///
+    /// Note: This macro is intended for internal use only and should be invoked exclusively
+    /// by the `generate_arithmetic_harnesses` macro. Its purpose is to reduce code duplication,
+    /// and it is not meant to be used directly elsewhere in the codebase.
+    macro_rules! generate_single_arithmetic_harness {
+        ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => {
+            #[kani::proof_for_contract(<*const $ty>::$fn_name)]
+            pub fn $proof_name() {
+                // 200 bytes are large enough to cover all pointee types used for testing
+                const BUF_SIZE: usize = 200;
+                let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+                let test_ptr: *const $ty = generator.any_in_bounds().ptr;
+                let count: $count_ty = kani::any();
+                unsafe {
+                    test_ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    /// This macro generates verification harnesses for the `offset`, `add`, and `sub`
+    /// pointer operations, supporting integer, composite, or unit types.
+    /// - `$ty`: The pointee type (e.g., i32, u32, tuples).
+    /// - `$offset_fn_name`: The name for the `offset` proof for contract.
+    /// - `$add_fn_name`: The name for the `add` proof for contract.
+    /// - `$sub_fn_name`: The name for the `sub` proof for contract.
+    macro_rules! generate_arithmetic_harnesses {
+        ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => {
+            generate_single_arithmetic_harness!($ty, $add_fn_name, add, usize);
+            generate_single_arithmetic_harness!($ty, $sub_fn_name, sub, usize);
+            generate_single_arithmetic_harness!($ty, $offset_fn_name, offset, isize);
+        };
     }
 
-    // Array size bound for kani::any_array
+    // Generate harnesses for unit type (add, sub, offset)
+    generate_arithmetic_harnesses!(
+        (),
+        check_const_add_unit,
+        check_const_sub_unit,
+        check_const_offset_unit
+    );
+
+    // Generate harnesses for integer types (add, sub, offset)
+    generate_arithmetic_harnesses!(
+        i8,
+        check_const_add_i8,
+        check_const_sub_i8,
+        check_const_offset_i8
+    );
+    generate_arithmetic_harnesses!(
+        i16,
+        check_const_add_i16,
+        check_const_sub_i16,
+        check_const_offset_i16
+    );
+    generate_arithmetic_harnesses!(
+        i32,
+        check_const_add_i32,
+        check_const_sub_i32,
+        check_const_offset_i32
+    );
+    generate_arithmetic_harnesses!(
+        i64,
+        check_const_add_i64,
+        check_const_sub_i64,
+        check_const_offset_i64
+    );
+    generate_arithmetic_harnesses!(
+        i128,
+        check_const_add_i128,
+        check_const_sub_i128,
+        check_const_offset_i128
+    );
+    generate_arithmetic_harnesses!(
+        isize,
+        check_const_add_isize,
+        check_const_sub_isize,
+        check_const_offset_isize
+    );
+    generate_arithmetic_harnesses!(
+        u8,
+        check_const_add_u8,
+        check_const_sub_u8,
+        check_const_offset_u8
+    );
+    generate_arithmetic_harnesses!(
+        u16,
+        check_const_add_u16,
+        check_const_sub_u16,
+        check_const_offset_u16
+    );
+    generate_arithmetic_harnesses!(
+        u32,
+        check_const_add_u32,
+        check_const_sub_u32,
+        check_const_offset_u32
+    );
+    generate_arithmetic_harnesses!(
+        u64,
+        check_const_add_u64,
+        check_const_sub_u64,
+        check_const_offset_u64
+    );
+    generate_arithmetic_harnesses!(
+        u128,
+        check_const_add_u128,
+        check_const_sub_u128,
+        check_const_offset_u128
+    );
+    generate_arithmetic_harnesses!(
+        usize,
+        check_const_add_usize,
+        check_const_sub_usize,
+        check_const_offset_usize
+    );
+
+    // Generte harnesses for composite types (add, sub, offset)
+    generate_arithmetic_harnesses!(
+        (i8, i8),
+        check_const_add_tuple_1,
+        check_const_sub_tuple_1,
+        check_const_offset_tuple_1
+    );
+    generate_arithmetic_harnesses!(
+        (f64, bool),
+        check_const_add_tuple_2,
+        check_const_sub_tuple_2,
+        check_const_offset_tuple_2
+    );
+    generate_arithmetic_harnesses!(
+        (i32, f64, bool),
+        check_const_add_tuple_3,
+        check_const_sub_tuple_3,
+        check_const_offset_tuple_3
+    );
+    generate_arithmetic_harnesses!(
+        (i8, u16, i32, u64, isize),
+        check_const_add_tuple_4,
+        check_const_sub_tuple_4,
+        check_const_offset_tuple_4
+    );
+
+    // Constant for array size used in all tests
+    const ARRAY_SIZE: usize = 5;
+
+    /// This macro generates a single verification harness for the `offset`, `add`, or `sub`
+    /// pointer operations for a slice type.
+    /// - `$ty`: The type of the array's elements (e.g., `i32`, `u32`, tuples).
+    /// - `$fn_name`: The name of the function being checked (`add`, `sub`, or `offset`).
+    /// - `$proof_name`: The name assigned to the generated proof for the contract.
+    /// - `$count_ty:ty`: The type of the input variable passed to the method being invoked.
+    ///
+    /// Note: This macro is intended for internal use only and should be invoked exclusively
+    /// by the `generate_slice_harnesses` macro. Its purpose is to reduce code duplication,
+    /// and it is not meant to be used directly elsewhere in the codebase.
+    macro_rules! generate_single_slice_harness {
+        ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => {
+            #[kani::proof_for_contract(<*const $ty>::$fn_name)]
+            fn $proof_name() {
+                let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array();
+                let test_ptr: *const $ty = arr.as_ptr();
+                let offset: usize = kani::any();
+                kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>());
+                let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset);
+
+                let count: $count_ty = kani::any();
+                unsafe {
+                    ptr_with_offset.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    /// This macro generates verification harnesses for the `offset`, `add`, and `sub`
+    /// pointer operations for a slice type.
+    /// - `$ty`: The type of the array (e.g., i32, u32, tuples).
+    /// - `$offset_fn_name`: The name for the `offset` proof for contract.
+    /// - `$add_fn_name`: The name for the `add` proof for contract.
+    /// - `$sub_fn_name`: The name for the `sub` proof for contract.
+    macro_rules! generate_slice_harnesses {
+        ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => {
+            generate_single_slice_harness!($ty, $add_fn_name, add, usize);
+            generate_single_slice_harness!($ty, $sub_fn_name, sub, usize);
+            generate_single_slice_harness!($ty, $offset_fn_name, offset, isize);
+        };
+    }
+
+    // Generate slice harnesses for various types (add, sub, offset)
+    generate_slice_harnesses!(
+        i8,
+        check_const_add_slice_i8,
+        check_const_sub_slice_i8,
+        check_const_offset_slice_i8
+    );
+    generate_slice_harnesses!(
+        i16,
+        check_const_add_slice_i16,
+        check_const_sub_slice_i16,
+        check_const_offset_slice_i16
+    );
+    generate_slice_harnesses!(
+        i32,
+        check_const_add_slice_i32,
+        check_const_sub_slice_i32,
+        check_const_offset_slice_i32
+    );
+    generate_slice_harnesses!(
+        i64,
+        check_const_add_slice_i64,
+        check_const_sub_slice_i64,
+        check_const_offset_slice_i64
+    );
+    generate_slice_harnesses!(
+        i128,
+        check_const_add_slice_i128,
+        check_const_sub_slice_i128,
+        check_const_offset_slice_i128
+    );
+    generate_slice_harnesses!(
+        isize,
+        check_const_add_slice_isize,
+        check_const_sub_slice_isize,
+        check_const_offset_slice_isize
+    );
+    generate_slice_harnesses!(
+        u8,
+        check_const_add_slice_u8,
+        check_const_sub_slice_u8,
+        check_const_offset_slice_u8
+    );
+    generate_slice_harnesses!(
+        u16,
+        check_const_add_slice_u16,
+        check_const_sub_slice_u16,
+        check_const_offset_slice_u16
+    );
+    generate_slice_harnesses!(
+        u32,
+        check_const_add_slice_u32,
+        check_const_sub_slice_u32,
+        check_const_offset_slice_u32
+    );
+    generate_slice_harnesses!(
+        u64,
+        check_const_add_slice_u64,
+        check_const_sub_slice_u64,
+        check_const_offset_slice_u64
+    );
+    generate_slice_harnesses!(
+        u128,
+        check_const_add_slice_u128,
+        check_const_sub_slice_u128,
+        check_const_offset_slice_u128
+    );
+    generate_slice_harnesses!(
+        usize,
+        check_const_add_slice_usize,
+        check_const_sub_slice_usize,
+        check_const_offset_slice_usize
+    );
+
+    // Generate slice harnesses for tuples (add, sub, offset)
+    generate_slice_harnesses!(
+        (i8, i8),
+        check_const_add_slice_tuple_1,
+        check_const_sub_slice_tuple_1,
+        check_const_offset_slice_tuple_1
+    );
+    generate_slice_harnesses!(
+        (f64, bool),
+        check_const_add_slice_tuple_2,
+        check_const_sub_slice_tuple_2,
+        check_const_offset_slice_tuple_2
+    );
+    generate_slice_harnesses!(
+        (i32, f64, bool),
+        check_const_add_slice_tuple_3,
+        check_const_sub_slice_tuple_3,
+        check_const_offset_slice_tuple_3
+    );
+    generate_slice_harnesses!(
+        (i8, u16, i32, u64, isize),
+        check_const_add_slice_tuple_4,
+        check_const_sub_slice_tuple_4,
+        check_const_offset_slice_tuple_4
+    );
+
+    // Array size bound for kani::any_array for `offset_from` verification
     const ARRAY_LEN: usize = 40;
 
     macro_rules! generate_offset_from_harness {
@@ -1781,6 +2111,19 @@ mod verify {
         };
     }
 
+    // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0
+    #[kani::proof_for_contract(<*const ()>::offset_from)]
+    #[kani::should_panic]
+    pub fn check_const_offset_from_unit() {
+        let val: () = ();
+        let src_ptr: *const () = &val;
+        let dest_ptr: *const () = &val;
+        unsafe {
+            dest_ptr.offset_from(src_ptr);
+        }
+    }
+
+    // fn <*const T>::offset_from() integer and integer slice types verification
     generate_offset_from_harness!(
         u8,
         check_const_offset_from_u8,
@@ -1811,7 +2154,6 @@ mod verify {
         check_const_offset_from_usize,
         check_const_offset_from_usize_arr
     );
-
     generate_offset_from_harness!(
         i8,
         check_const_offset_from_i8,
@@ -1843,6 +2185,7 @@ mod verify {
         check_const_offset_from_isize_arr
     );
 
+    // fn <*const T>::offset_from() tuple and tuple slice types verification
     generate_offset_from_harness!(
         (i8, i8),
         check_const_offset_from_tuple_1,