From 96a8a2e79428ab08ccb06315fceae00ffaa04234 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 23 Oct 2024 12:58:18 -0700
Subject: [PATCH 1/6] refactored function contracts for add, sub and offset
 using the same_allocation api, modified their proof for harness accordingly

---
 library/core/src/ptr/mut_ptr.rs | 73 ++++++++++++++++++++++++++-------
 1 file changed, 59 insertions(+), 14 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 83d30e0c01375..0252c9656a255 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -408,9 +408,8 @@ impl<T: ?Sized> *mut T {
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(kani::mem::can_dereference(self))]
-    // TODO: Determine the valid value range for 'count' and update the precondition accordingly.
-    #[requires(count == 0)] // This precondition is currently a placeholder.
-    #[ensures(|result| kani::mem::can_dereference(result))]
+    #[requires(count.checked_mul(core::mem::size_of::<T>() as isize).is_some())]
+    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))]
     pub const unsafe fn offset(self, count: isize) -> *mut T
     where
         T: Sized,
@@ -956,9 +955,9 @@ impl<T: ?Sized> *mut T {
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(kani::mem::can_dereference(self))]
-    // TODO: Determine the valid value range for 'count' and update the precondition accordingly.
-    #[requires(count == 0)] // This precondition is currently a placeholder.
-    #[ensures(|result| kani::mem::can_dereference(result))]
+    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some()
+        && count * core::mem::size_of::<T>() <= isize::MAX as usize)]
+    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1035,9 +1034,9 @@ impl<T: ?Sized> *mut T {
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(kani::mem::can_dereference(self))]
-    // TODO: Determine the valid value range for 'count' and update the precondition accordingly.
-    #[requires(count == 0)] // This precondition is currently a placeholder.
-    #[ensures(|result| kani::mem::can_dereference(result))]
+    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some()
+        && count * core::mem::size_of::<T>() <= isize::MAX as usize)]
+    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -2220,17 +2219,52 @@ mod verify {
     use crate::kani;
 
     macro_rules! generate_mut_add_and_sub_harness {
-        ($type:ty, $proof_name:ident, $func_name:ident) => {
-            #[kani::proof_for_contract(<*mut $type>::$func_name)]
+        ($type:ty, $proof_name:ident, add) => {
+            #[kani::proof_for_contract(<*mut $type>::add)]
             pub fn $proof_name() {
                 let mut test_val: $type = kani::any::<$type>();
+                let offset: usize = kani::any();
+                let count: usize = kani::any();                
+                if(core::mem::size_of::<$type>() == 0) { // unit type
+                    kani::assume(offset == 0);
+                    kani::assume(count == 0);
+                } else {
+                    kani::assume(offset == 0 || offset == 1);
+                    kani::assume(count == 0 || count == 1);
+                    kani::assume(offset + count <= 1);
+                } 
+                
                 let test_ptr: *mut $type = &mut test_val;
-                let count: usize = kani::any();
+                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                
+                
                 unsafe {
-                    test_ptr.$func_name(count);
+                    ptr_with_offset.add(count);
                 }
             }
         };
+        ($type:ty, $proof_name:ident, sub) => {
+            #[kani::proof_for_contract(<*mut $type>::sub)]
+            pub fn $proof_name() {
+                let mut test_val: $type = kani::any::<$type>();
+                let offset: usize = kani::any();
+                let count: usize = kani::any();
+                if(core::mem::size_of::<$type>() == 0) { // unit type
+                    kani::assume(offset == 0);
+                    kani::assume(count == 0);
+                } else {
+                    kani::assume(offset == 0 || offset == 1);
+                    kani::assume(count == 0 || count == 1); 
+                    kani::assume(count <= offset);
+                }
+                
+                let test_ptr: *mut $type = &mut test_val;
+                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);
+                
+                unsafe {
+                    ptr_with_offset.sub(count);
+                }
+            }
+        }
     }
 
     // <*mut T>:: add() integer types verification
@@ -2287,9 +2321,20 @@ mod verify {
             pub fn $proof_name() {
                 let mut test_val: $type = kani::any::<$type>();
                 let test_ptr: *mut $type = &mut test_val;
+                let offset: usize = kani::any();
                 let count: isize = kani::any();
+                if(core::mem::size_of::<$type>() == 0) { // unit type
+                    kani::assume(offset == 0);
+                    kani::assume(count == 0);
+                } else {
+                    kani::assume(offset == 0 || offset == 1);
+                    kani::assume(count == 0 || count == 1);
+                    kani::assume(offset as isize + count == 0 || offset as isize + count == 1);    
+                }
+                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);
+                
                 unsafe {
-                    test_ptr.offset(count);
+                    ptr_with_offset.offset(count);
                 }
             }
         };

From 852e96f4c20540bbfb9b1807f3eec8da8825594a Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 23 Oct 2024 13:11:23 -0700
Subject: [PATCH 2/6] merged macros for add, sub and offset

---
 library/core/src/ptr/mut_ptr.rs | 147 +++++++++++++++-----------------
 1 file changed, 71 insertions(+), 76 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 0252c9656a255..df97e30bcbe3e 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2218,7 +2218,7 @@ impl<T: ?Sized> PartialOrd for *mut T {
 mod verify {
     use crate::kani;
 
-    macro_rules! generate_mut_add_and_sub_harness {
+    macro_rules! generate_mut_arithmetic_harness {
         ($type:ty, $proof_name:ident, add) => {
             #[kani::proof_for_contract(<*mut $type>::add)]
             pub fn $proof_name() {
@@ -2264,59 +2264,8 @@ mod verify {
                     ptr_with_offset.sub(count);
                 }
             }
-        }
-    }
-
-    // <*mut T>:: add() integer types verification
-    generate_mut_add_and_sub_harness!(i8, check_mut_add_i8, add);
-    generate_mut_add_and_sub_harness!(i16, check_mut_add_i16, add);
-    generate_mut_add_and_sub_harness!(i32, check_mut_add_i32, add);
-    generate_mut_add_and_sub_harness!(i64, check_mut_add_i64, add);
-    generate_mut_add_and_sub_harness!(i128, check_mut_add_i128, add);
-    generate_mut_add_and_sub_harness!(isize, check_mut_add_isize, add);
-    generate_mut_add_and_sub_harness!(u8, check_mut_add_u8, add);
-    generate_mut_add_and_sub_harness!(u16, check_mut_add_u16, add);
-    generate_mut_add_and_sub_harness!(u32, check_mut_add_u32, add);
-    generate_mut_add_and_sub_harness!(u64, check_mut_add_u64, add);
-    generate_mut_add_and_sub_harness!(u128, check_mut_add_u128, add);
-    generate_mut_add_and_sub_harness!(usize, check_mut_add_usize, add);   
-
-    // <*mut T>:: add() unit type verification
-    generate_mut_add_and_sub_harness!((), check_mut_add_unit, add);
-
-    // <*mut T>:: add() composite types verification
-    generate_mut_add_and_sub_harness!((i8, i8), check_mut_add_tuple_1, add);
-    generate_mut_add_and_sub_harness!((f64, bool), check_mut_add_tuple_2, add);
-    generate_mut_add_and_sub_harness!((i32, f64, bool), check_mut_add_tuple_3, add);
-    generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add);
-
-    // <*mut T>:: sub() integer types verification
-    generate_mut_add_and_sub_harness!(i8, check_mut_sub_i8, sub);
-    generate_mut_add_and_sub_harness!(i16, check_mut_sub_i16, sub);
-    generate_mut_add_and_sub_harness!(i32, check_mut_sub_i32, sub);
-    generate_mut_add_and_sub_harness!(i64, check_mut_sub_i64, sub);
-    generate_mut_add_and_sub_harness!(i128, check_mut_sub_i128, sub);
-    generate_mut_add_and_sub_harness!(isize, check_mut_sub_isize, sub);
-    generate_mut_add_and_sub_harness!(u8, check_mut_sub_u8, sub);
-    generate_mut_add_and_sub_harness!(u16, check_mut_sub_u16, sub);
-    generate_mut_add_and_sub_harness!(u32, check_mut_sub_u32, sub);
-    generate_mut_add_and_sub_harness!(u64, check_mut_sub_u64, sub);
-    generate_mut_add_and_sub_harness!(u128, check_mut_sub_u128, sub);
-    generate_mut_add_and_sub_harness!(usize, check_mut_sub_usize, sub);
-
-    // <*mut T>:: sub() unit type verification
-    generate_mut_add_and_sub_harness!((), check_mut_sub_unit, sub);
-
-    // <*mut T>:: sub() composite types verification
-    generate_mut_add_and_sub_harness!((i8, i8), check_mut_sub_tuple_1, sub);
-    generate_mut_add_and_sub_harness!((f64, bool), check_mut_sub_tuple_2, sub);
-    generate_mut_add_and_sub_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub);
-    generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub);
-  
-  
-    // fn <*mut T>::offset verification begin
-    macro_rules! generate_mut_offset_harness {
-      ($type:ty, $proof_name:ident) => {
+        };
+        ($type:ty, $proof_name:ident, offset) => {
             #[kani::proof_for_contract(<*mut $type>::offset)]
             pub fn $proof_name() {
                 let mut test_val: $type = kani::any::<$type>();
@@ -2340,26 +2289,72 @@ mod verify {
         };
     }
 
-    // fn <*mut T>::offset integer types verification
-    generate_mut_offset_harness!(i8, check_mut_offset_i8);
-    generate_mut_offset_harness!(i16, check_mut_offset_i16);
-    generate_mut_offset_harness!(i32, check_mut_offset_i32);
-    generate_mut_offset_harness!(i64, check_mut_offset_i64);
-    generate_mut_offset_harness!(i128, check_mut_offset_i128);
-    generate_mut_offset_harness!(isize, check_mut_offset_isize);
-    generate_mut_offset_harness!(u8, check_mut_offset_u8);
-    generate_mut_offset_harness!(u16, check_mut_offset_u16);
-    generate_mut_offset_harness!(u32, check_mut_offset_u32);
-    generate_mut_offset_harness!(u64, check_mut_offset_u64);
-    generate_mut_offset_harness!(u128, check_mut_offset_u128);
-    generate_mut_offset_harness!(usize, check_mut_offset_usize);
-
-    // fn <*mut T>::offset unit type verification
-    generate_mut_offset_harness!((), check_mut_offset_unit);
-
-    // fn <*mut T>::offset composite type verification
-    generate_mut_offset_harness!((i8, i8), check_mut_offset_tuple_1);
-    generate_mut_offset_harness!((f64, bool), check_mut_offset_tuple_2);
-    generate_mut_offset_harness!((i32, f64, bool), check_mut_offset_tuple_3);
-    generate_mut_offset_harness!((i8, u16, i32, u64, isize), check_mut_offset_tuple_4);
+    // <*mut T>:: add() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_add_i8, add);
+    generate_mut_arithmetic_harness!(i16, check_mut_add_i16, add);
+    generate_mut_arithmetic_harness!(i32, check_mut_add_i32, add);
+    generate_mut_arithmetic_harness!(i64, check_mut_add_i64, add);
+    generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add);
+    generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add);
+    generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add);
+    generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add);
+    generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add);
+    generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add);
+    generate_mut_arithmetic_harness!(u128, check_mut_add_u128, add);
+    generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add);   
+
+    // <*mut T>:: add() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_add_unit, add);
+
+    // <*mut T>:: add() composite types verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add);
+    generate_mut_arithmetic_harness!((f64, bool), check_mut_add_tuple_2, add);
+    generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_add_tuple_3, add);
+    generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add);
+
+    // <*mut T>:: sub() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_sub_i8, sub);
+    generate_mut_arithmetic_harness!(i16, check_mut_sub_i16, sub);
+    generate_mut_arithmetic_harness!(i32, check_mut_sub_i32, sub);
+    generate_mut_arithmetic_harness!(i64, check_mut_sub_i64, sub);
+    generate_mut_arithmetic_harness!(i128, check_mut_sub_i128, sub);
+    generate_mut_arithmetic_harness!(isize, check_mut_sub_isize, sub);
+    generate_mut_arithmetic_harness!(u8, check_mut_sub_u8, sub);
+    generate_mut_arithmetic_harness!(u16, check_mut_sub_u16, sub);
+    generate_mut_arithmetic_harness!(u32, check_mut_sub_u32, sub);
+    generate_mut_arithmetic_harness!(u64, check_mut_sub_u64, sub);
+    generate_mut_arithmetic_harness!(u128, check_mut_sub_u128, sub);
+    generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub);
+
+    // <*mut T>:: sub() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub);
+
+    // <*mut T>:: sub() composite types verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub);
+    generate_mut_arithmetic_harness!((f64, bool), check_mut_sub_tuple_2, sub);
+    generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub);
+    generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub); 
+
+    // fn <*mut T>::offset() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_offset_i8, offset);
+    generate_mut_arithmetic_harness!(i16, check_mut_offset_i16, offset);
+    generate_mut_arithmetic_harness!(i32, check_mut_offset_i32, offset);
+    generate_mut_arithmetic_harness!(i64, check_mut_offset_i64, offset);
+    generate_mut_arithmetic_harness!(i128, check_mut_offset_i128, offset);
+    generate_mut_arithmetic_harness!(isize, check_mut_offset_isize, offset);
+    generate_mut_arithmetic_harness!(u8, check_mut_offset_u8, offset);
+    generate_mut_arithmetic_harness!(u16, check_mut_offset_u16, offset);
+    generate_mut_arithmetic_harness!(u32, check_mut_offset_u32, offset);
+    generate_mut_arithmetic_harness!(u64, check_mut_offset_u64, offset);
+    generate_mut_arithmetic_harness!(u128, check_mut_offset_u128, offset);
+    generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset);
+
+    // fn <*mut T>::offset() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset);
+
+    // fn <*mut T>::offset() composite type verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset);
+    generate_mut_arithmetic_harness!((f64, bool), check_mut_offset_tuple_2, offset);
+    generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_offset_tuple_3, offset);
+    generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_offset_tuple_4, offset);
 }

From 04bd61e55faa37f4256b7ced3b4bc1fc1c529f7f Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 23 Oct 2024 19:32:34 -0700
Subject: [PATCH 3/6] updated function contracts and proof for contracts for
 add(), sub() and offset()

---
 library/core/src/ptr/mut_ptr.rs | 77 ++++++++++++++-------------------
 1 file changed, 33 insertions(+), 44 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index df97e30bcbe3e..4dce768cef784 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -407,9 +407,11 @@ impl<T: ?Sized> *mut 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(kani::mem::can_dereference(self))]
-    #[requires(count.checked_mul(core::mem::size_of::<T>() as isize).is_some())]
-    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))]
+    #[requires(
+        count.checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
+        kani::mem::same_allocation(self, self.wrapping_offset(count))
+    )]
+    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *mut T
     where
         T: Sized,
@@ -954,10 +956,12 @@ impl<T: ?Sized> *mut 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(kani::mem::can_dereference(self))]
-    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some()
-        && count * core::mem::size_of::<T>() <= isize::MAX as usize)]
-    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))]
+    #[requires(
+            count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+            count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+            kani::mem::same_allocation(self, self.wrapping_add(count))
+    )]
+    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1033,10 +1037,12 @@ impl<T: ?Sized> *mut T {
     #[rustc_allow_const_fn_unstable(unchecked_neg)]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
-    #[requires(kani::mem::can_dereference(self))]
-    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some()
-        && count * core::mem::size_of::<T>() <= isize::MAX as usize)]
-    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))]
+    #[requires(
+        count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+        count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+        kani::mem::same_allocation(self, self.wrapping_sub(count))
+    )]
+    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -2225,18 +2231,12 @@ mod verify {
                 let mut test_val: $type = kani::any::<$type>();
                 let offset: usize = kani::any();
                 let count: usize = kani::any();                
-                if(core::mem::size_of::<$type>() == 0) { // unit type
-                    kani::assume(offset == 0);
-                    kani::assume(count == 0);
-                } else {
-                    kani::assume(offset == 0 || offset == 1);
-                    kani::assume(count == 0 || count == 1);
-                    kani::assume(offset + count <= 1);
-                } 
+                kani::assume(offset <= 1);
+                kani::assume(count <= 1);
+                kani::assume(offset + count <= 1);
                 
                 let test_ptr: *mut $type = &mut test_val;
-                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                
-                
+                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                   
                 unsafe {
                     ptr_with_offset.add(count);
                 }
@@ -2248,18 +2248,12 @@ mod verify {
                 let mut test_val: $type = kani::any::<$type>();
                 let offset: usize = kani::any();
                 let count: usize = kani::any();
-                if(core::mem::size_of::<$type>() == 0) { // unit type
-                    kani::assume(offset == 0);
-                    kani::assume(count == 0);
-                } else {
-                    kani::assume(offset == 0 || offset == 1);
-                    kani::assume(count == 0 || count == 1); 
-                    kani::assume(count <= offset);
-                }
+                kani::assume(offset <= 1);
+                kani::assume(count <= 1); 
+                kani::assume(count <= offset);
                 
                 let test_ptr: *mut $type = &mut test_val;
                 let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);
-                
                 unsafe {
                     ptr_with_offset.sub(count);
                 }
@@ -2269,19 +2263,14 @@ mod verify {
             #[kani::proof_for_contract(<*mut $type>::offset)]
             pub fn $proof_name() {
                 let mut test_val: $type = kani::any::<$type>();
-                let test_ptr: *mut $type = &mut test_val;
                 let offset: usize = kani::any();
                 let count: isize = kani::any();
-                if(core::mem::size_of::<$type>() == 0) { // unit type
-                    kani::assume(offset == 0);
-                    kani::assume(count == 0);
-                } else {
-                    kani::assume(offset == 0 || offset == 1);
-                    kani::assume(count == 0 || count == 1);
-                    kani::assume(offset as isize + count == 0 || offset as isize + count == 1);    
-                }
-                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);
-                
+                kani::assume(offset <= 1);
+                kani::assume(count >= -1 && count <= 1);
+                kani::assume(offset as isize + count >= 0 && offset as isize + count <= 1);    
+
+                let test_ptr: *mut $type = &mut test_val;
+                let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                
                 unsafe {
                     ptr_with_offset.offset(count);
                 }
@@ -2304,7 +2293,7 @@ mod verify {
     generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add);   
 
     // <*mut T>:: add() unit type verification
-    generate_mut_arithmetic_harness!((), check_mut_add_unit, add);
+    // generate_mut_arithmetic_harness!((), check_mut_add_unit, add);
 
     // <*mut T>:: add() composite types verification
     generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add);
@@ -2327,7 +2316,7 @@ mod verify {
     generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub);
 
     // <*mut T>:: sub() unit type verification
-    generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub);
+    // generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub);
 
     // <*mut T>:: sub() composite types verification
     generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub);
@@ -2350,7 +2339,7 @@ mod verify {
     generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset);
 
     // fn <*mut T>::offset() unit type verification
-    generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset);
+    // generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset);
 
     // fn <*mut T>::offset() composite type verification
     generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset);

From 7557fc557da59fee7c2e8397466e0bdec84bb600 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 30 Oct 2024 18:02:43 -0700
Subject: [PATCH 4/6] added support for unit type pointers

---
 library/core/src/ptr/mut_ptr.rs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 4dce768cef784..c35458c8f91f3 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -409,9 +409,9 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         count.checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
-        kani::mem::same_allocation(self, self.wrapping_offset(count))
+        ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count))))
     )]
-    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))]
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *mut T
     where
         T: Sized,
@@ -959,9 +959,9 @@ impl<T: ?Sized> *mut T {
     #[requires(
             count.checked_mul(core::mem::size_of::<T>()).is_some() &&
             count * core::mem::size_of::<T>() <= isize::MAX as usize &&
-            kani::mem::same_allocation(self, self.wrapping_add(count))
+            ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count))))
     )]
-    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))]
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1040,9 +1040,9 @@ impl<T: ?Sized> *mut T {
     #[requires(
         count.checked_mul(core::mem::size_of::<T>()).is_some() &&
         count * core::mem::size_of::<T>() <= isize::MAX as usize &&
-        kani::mem::same_allocation(self, self.wrapping_sub(count))
+        ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count))))
     )]
-    #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))]
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -2293,7 +2293,7 @@ mod verify {
     generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add);   
 
     // <*mut T>:: add() unit type verification
-    // generate_mut_arithmetic_harness!((), check_mut_add_unit, add);
+    generate_mut_arithmetic_harness!((), check_mut_add_unit, add);
 
     // <*mut T>:: add() composite types verification
     generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add);
@@ -2316,7 +2316,7 @@ mod verify {
     generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub);
 
     // <*mut T>:: sub() unit type verification
-    // generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub);
+    generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub);
 
     // <*mut T>:: sub() composite types verification
     generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub);
@@ -2339,7 +2339,7 @@ mod verify {
     generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset);
 
     // fn <*mut T>::offset() unit type verification
-    // generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset);
+    generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset);
 
     // fn <*mut T>::offset() composite type verification
     generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset);

From 76b231170608507847b56f21c954e424b01c76b6 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 6 Nov 2024 09:45:25 -0800
Subject: [PATCH 5/6] updated function contracts, removed unnecessary
 kani::assmue

---
 library/core/src/ptr/mut_ptr.rs | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index c35458c8f91f3..efc9e9095eb84 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -409,6 +409,7 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         count.checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
+        (self as isize).checked_add((count * core::mem::size_of::<T>() as isize)).is_some() &&
         ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count))))
     )]
     #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
@@ -959,6 +960,7 @@ impl<T: ?Sized> *mut T {
     #[requires(
             count.checked_mul(core::mem::size_of::<T>()).is_some() &&
             count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+            (self as isize).checked_add((count * core::mem::size_of::<T>()) as isize).is_some() &&
             ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count))))
     )]
     #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
@@ -1040,6 +1042,7 @@ impl<T: ?Sized> *mut T {
     #[requires(
         count.checked_mul(core::mem::size_of::<T>()).is_some() &&
         count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+        (self as isize).checked_sub((count * core::mem::size_of::<T>()) as isize).is_some() &&
         ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count))))
     )]
     #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
@@ -2232,8 +2235,8 @@ mod verify {
                 let offset: usize = kani::any();
                 let count: usize = kani::any();                
                 kani::assume(offset <= 1);
-                kani::assume(count <= 1);
-                kani::assume(offset + count <= 1);
+                // kani::assume(count <= 1);
+                // kani::assume(offset + count <= 1);
                 
                 let test_ptr: *mut $type = &mut test_val;
                 let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                   
@@ -2249,8 +2252,8 @@ mod verify {
                 let offset: usize = kani::any();
                 let count: usize = kani::any();
                 kani::assume(offset <= 1);
-                kani::assume(count <= 1); 
-                kani::assume(count <= offset);
+                // kani::assume(count <= 1); 
+                // kani::assume(count <= offset);
                 
                 let test_ptr: *mut $type = &mut test_val;
                 let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);
@@ -2266,8 +2269,8 @@ mod verify {
                 let offset: usize = kani::any();
                 let count: isize = kani::any();
                 kani::assume(offset <= 1);
-                kani::assume(count >= -1 && count <= 1);
-                kani::assume(offset as isize + count >= 0 && offset as isize + count <= 1);    
+                // kani::assume(count >= -1 && count <= 1);
+                // kani::assume(offset as isize + count >= 0 && offset as isize + count <= 1);    
 
                 let test_ptr: *mut $type = &mut test_val;
                 let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                

From cb6a17713edc486417a8b7e7e1c2f76eb70424fa Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 6 Nov 2024 10:18:16 -0800
Subject: [PATCH 6/6] added comments to function contracts

---
 library/core/src/ptr/mut_ptr.rs | 38 ++++++++++++++++++++++++---------
 1 file changed, 28 insertions(+), 10 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index efc9e9095eb84..faef82ffb343a 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -408,10 +408,18 @@ impl<T: ?Sized> *mut T {
     #[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`
         count.checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
+        // Precondition 2: adding the computed offset to `self` does not cause overflow
         (self as isize).checked_add((count * core::mem::size_of::<T>() 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_offset(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
         ((core::mem::size_of::<T>() == 0) || (kani::mem::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) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *mut T
     where
@@ -958,11 +966,19 @@ impl<T: ?Sized> *mut T {
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
-            count.checked_mul(core::mem::size_of::<T>()).is_some() &&
-            count * core::mem::size_of::<T>() <= isize::MAX as usize &&
-            (self as isize).checked_add((count * core::mem::size_of::<T>()) as isize).is_some() &&
-            ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count))))
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
+        count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+        count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+        // Precondition 2: adding the computed offset to `self` does not cause overflow
+        (self as isize).checked_add((count * core::mem::size_of::<T>()) 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) || (kani::mem::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) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
@@ -1040,11 +1056,19 @@ impl<T: ?Sized> *mut T {
     #[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`
         count.checked_mul(core::mem::size_of::<T>()).is_some() &&
         count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+        // Precondition 2: subtracting the computed offset from `self` does not cause overflow
         (self as isize).checked_sub((count * core::mem::size_of::<T>()) 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) || (kani::mem::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) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
@@ -2235,8 +2259,6 @@ mod verify {
                 let offset: usize = kani::any();
                 let count: usize = kani::any();                
                 kani::assume(offset <= 1);
-                // kani::assume(count <= 1);
-                // kani::assume(offset + count <= 1);
                 
                 let test_ptr: *mut $type = &mut test_val;
                 let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);                   
@@ -2252,8 +2274,6 @@ mod verify {
                 let offset: usize = kani::any();
                 let count: usize = kani::any();
                 kani::assume(offset <= 1);
-                // kani::assume(count <= 1); 
-                // kani::assume(count <= offset);
                 
                 let test_ptr: *mut $type = &mut test_val;
                 let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);
@@ -2269,8 +2289,6 @@ mod verify {
                 let offset: usize = kani::any();
                 let count: isize = kani::any();
                 kani::assume(offset <= 1);
-                // kani::assume(count >= -1 && count <= 1);
-                // kani::assume(offset as isize + count >= 0 && offset as isize + count <= 1);    
 
                 let test_ptr: *mut $type = &mut test_val;
                 let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset);