From 0ccf81e6cc54a310c696c546aef4cc9e4c68a590 Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Thu, 14 Nov 2024 14:53:04 -0800
Subject: [PATCH 01/21] Adds contracts for byte_add, byte_sub and byte_offset

- Also adds proofs verifying unit, int and composite types.
---
 library/core/src/ptr/mut_ptr.rs | 244 +++++++++++++++++++++++++++++++-
 1 file changed, 237 insertions(+), 7 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 7aa6a309a06b5..7be6f303f2754 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -3,6 +3,11 @@ use crate::cmp::Ordering::{Equal, Greater, Less};
 use crate::intrinsics::const_eval_select;
 use crate::mem::SizedTypeProperties;
 use crate::slice::{self, SliceIndex};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
+use core::mem;
 
 impl<T: ?Sized> *mut T {
     /// Returns `true` if the pointer is null.
@@ -94,7 +99,10 @@ impl<T: ?Sized> *mut T {
     /// // This dereference is UB. The pointer only has provenance for `x` but points to `y`.
     /// println!("{:?}", unsafe { &*bad });
     #[unstable(feature = "set_ptr_value", issue = "75091")]
-    #[cfg_attr(bootstrap, rustc_const_stable(feature = "ptr_metadata_const", since = "1.83.0"))]
+    #[cfg_attr(
+        bootstrap,
+        rustc_const_stable(feature = "ptr_metadata_const", since = "1.83.0")
+    )]
     #[must_use = "returns a new pointer rather than modifying its argument"]
     #[inline]
     pub const fn with_metadata_of<U>(self, meta: *const U) -> *mut U
@@ -277,7 +285,11 @@ impl<T: ?Sized> *mut T {
     pub const unsafe fn as_ref<'a>(self) -> Option<&'a T> {
         // SAFETY: the caller must guarantee that `self` is valid for a
         // reference if it isn't null.
-        if self.is_null() { None } else { unsafe { Some(&*self) } }
+        if self.is_null() {
+            None
+        } else {
+            unsafe { Some(&*self) }
+        }
     }
 
     /// Returns a shared reference to the value behind the pointer.
@@ -352,7 +364,11 @@ impl<T: ?Sized> *mut T {
     {
         // SAFETY: the caller must guarantee that `self` meets all the
         // requirements for a reference.
-        if self.is_null() { None } else { Some(unsafe { &*(self as *const MaybeUninit<T>) }) }
+        if self.is_null() {
+            None
+        } else {
+            Some(unsafe { &*(self as *const MaybeUninit<T>) })
+        }
     }
 
     /// Adds a signed offset to a pointer.
@@ -457,6 +473,22 @@ impl<T: ?Sized> *mut T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero, then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // are pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *mut u8 as isize).checked_add(count).is_some() &&
+            ((self as *mut u8 as usize) == (self.wrapping_byte_offset(count) as *mut u8 as usize) ||
+                kani::mem::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T)))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *mut u8 as usize) == (*result as *mut u8 as usize)) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
         unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
@@ -537,7 +569,9 @@ impl<T: ?Sized> *mut T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     pub const fn wrapping_byte_offset(self, count: isize) -> Self {
-        self.cast::<u8>().wrapping_offset(count).with_metadata_of(self)
+        self.cast::<u8>()
+            .wrapping_offset(count)
+            .with_metadata_of(self)
     }
 
     /// Masks out bits of the pointer according to a mask.
@@ -578,7 +612,9 @@ impl<T: ?Sized> *mut T {
     #[must_use = "returns a new pointer rather than modifying its argument"]
     #[inline(always)]
     pub fn mask(self, mask: usize) -> *mut T {
-        intrinsics::ptr_mask(self.cast::<()>(), mask).cast_mut().with_metadata_of(self)
+        intrinsics::ptr_mask(self.cast::<()>(), mask)
+            .cast_mut()
+            .with_metadata_of(self)
     }
 
     /// Returns `None` if the pointer is null, or else returns a unique reference to
@@ -628,7 +664,11 @@ impl<T: ?Sized> *mut T {
     pub const unsafe fn as_mut<'a>(self) -> Option<&'a mut T> {
         // SAFETY: the caller must guarantee that `self` is be valid for
         // a mutable reference if it isn't null.
-        if self.is_null() { None } else { unsafe { Some(&mut *self) } }
+        if self.is_null() {
+            None
+        } else {
+            unsafe { Some(&mut *self) }
+        }
     }
 
     /// Returns a unique reference to the value behind the pointer.
@@ -689,7 +729,11 @@ impl<T: ?Sized> *mut T {
     {
         // SAFETY: the caller must guarantee that `self` meets all the
         // requirements for a reference.
-        if self.is_null() { None } else { Some(unsafe { &mut *(self as *mut MaybeUninit<T>) }) }
+        if self.is_null() {
+            None
+        } else {
+            Some(unsafe { &mut *(self as *mut MaybeUninit<T>) })
+        }
     }
 
     /// Returns whether two pointers are guaranteed to be equal.
@@ -1052,6 +1096,22 @@ impl<T: ?Sized> *mut T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero, then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // are pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *mut u8 as isize).checked_add(count as isize).is_some() &&
+            ((self as *mut u8 as usize) == (self.wrapping_byte_add(count) as *mut u8 as usize) ||
+                kani::mem::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T)))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *mut u8 as usize) == (*result as *mut u8 as usize)) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
         unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
@@ -1167,6 +1227,22 @@ impl<T: ?Sized> *mut T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // would be pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *mut u8 as isize).checked_sub(count as isize).is_some() &&
+            ((self as *mut u8 as usize) == (self.wrapping_byte_sub(count) as *mut u8 as usize) ||
+                kani::mem::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T)))
+    )]
+    #[ensures(|result|
+         // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *mut u8 as isize) == (*result as *mut u8 as isize)) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.
         unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
@@ -2302,3 +2378,157 @@ impl<T: ?Sized> PartialOrd for *mut T {
         *self >= *other
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use crate::kani;
+    use core::mem;
+    use kani::PointerGenerator;
+
+    // generate proof for contracts for byte_add, byte_sub and byte_offset for unint types
+    macro_rules! gen_mut_byte_arith_unit_harness {
+        (byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*mut ()>::byte_offset)]
+            pub fn $proof_name() {
+                let mut val = ();
+                let ptr: *mut () = &mut val as *mut ();
+                let count: isize = kani::any();
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($fn_name:ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*mut ()>::$fn_name)]
+            pub fn $proof_name() {
+                let mut val = ();
+                let ptr: *mut () = &mut val as *mut ();
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_mut_byte_arith_unit_harness!(byte_add, check_mut_byte_add_unit);
+    gen_mut_byte_arith_unit_harness!(byte_sub, check_mut_byte_sub_unit);
+    gen_mut_byte_arith_unit_harness!(byte_offset, check_mut_byte_offset_unit);
+
+    const ARRAY_LEN: usize = 40;
+
+    // generate proof for contracts for byte_add, byte_sub and byte_offset
+    macro_rules! gen_mut_byte_arith_harness {
+        ($type:ty, byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*mut $type>::byte_offset)]
+            pub fn $proof_name() {
+                // generator with space for single element
+                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
+                // generator with space for multiple elements
+                let mut generator2 =
+                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
+
+                let ptr: *mut $type = if kani::any() {
+                    generator1.any_in_bounds().ptr as *mut $type
+                } else {
+                    generator2.any_in_bounds().ptr as *mut $type
+                };
+                let count: isize = kani::any();
+
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($type:ty, $fn_name:ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*mut $type>::$fn_name)]
+            pub fn $proof_name() {
+                // generator with space for single element
+                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
+                // generator with space for multiple elements
+                let mut generator2 =
+                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
+
+                let ptr: *mut $type = if kani::any() {
+                    generator1.any_in_bounds().ptr as *mut $type
+                } else {
+                    generator2.any_in_bounds().ptr as *mut $type
+                };
+
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_mut_byte_arith_harness!(i8, byte_add, check_mut_byte_add_i8);
+    gen_mut_byte_arith_harness!(i16, byte_add, check_mut_byte_add_i16);
+    gen_mut_byte_arith_harness!(i32, byte_add, check_mut_byte_add_i32);
+    gen_mut_byte_arith_harness!(i64, byte_add, check_mut_byte_add_i64);
+    gen_mut_byte_arith_harness!(i128, byte_add, check_mut_byte_add_i128);
+    gen_mut_byte_arith_harness!(isize, byte_add, check_mut_byte_add_isize);
+    gen_mut_byte_arith_harness!(u8, byte_add, check_mut_byte_add_u8);
+    gen_mut_byte_arith_harness!(u16, byte_add, check_mut_byte_add_u16);
+    gen_mut_byte_arith_harness!(u32, byte_add, check_mut_byte_add_u32);
+    gen_mut_byte_arith_harness!(u64, byte_add, check_mut_byte_add_u64);
+    gen_mut_byte_arith_harness!(u128, byte_add, check_mut_byte_add_u128);
+    gen_mut_byte_arith_harness!(usize, byte_add, check_mut_byte_add_usize);
+    gen_mut_byte_arith_harness!((i8, i8), byte_add, check_mut_byte_add_tuple_1);
+    gen_mut_byte_arith_harness!((f64, bool), byte_add, check_mut_byte_add_tuple_2);
+    gen_mut_byte_arith_harness!((i32, f64, bool), byte_add, check_mut_byte_add_tuple_3);
+    gen_mut_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_add,
+        check_mut_byte_add_tuple_4
+    );
+
+    gen_mut_byte_arith_harness!(i8, byte_sub, check_mut_byte_sub_i8);
+    gen_mut_byte_arith_harness!(i16, byte_sub, check_mut_byte_sub_i16);
+    gen_mut_byte_arith_harness!(i32, byte_sub, check_mut_byte_sub_i32);
+    gen_mut_byte_arith_harness!(i64, byte_sub, check_mut_byte_sub_i64);
+    gen_mut_byte_arith_harness!(i128, byte_sub, check_mut_byte_sub_i128);
+    gen_mut_byte_arith_harness!(isize, byte_sub, check_mut_byte_sub_isize);
+    gen_mut_byte_arith_harness!(u8, byte_sub, check_mut_byte_sub_u8);
+    gen_mut_byte_arith_harness!(u16, byte_sub, check_mut_byte_sub_u16);
+    gen_mut_byte_arith_harness!(u32, byte_sub, check_mut_byte_sub_u32);
+    gen_mut_byte_arith_harness!(u64, byte_sub, check_mut_byte_sub_u64);
+    gen_mut_byte_arith_harness!(u128, byte_sub, check_mut_byte_sub_u128);
+    gen_mut_byte_arith_harness!(usize, byte_sub, check_mut_byte_sub_usize);
+    gen_mut_byte_arith_harness!((i8, i8), byte_sub, check_mut_byte_sub_tuple_1);
+    gen_mut_byte_arith_harness!((f64, bool), byte_sub, check_mut_byte_sub_tuple_2);
+    gen_mut_byte_arith_harness!((i32, f64, bool), byte_sub, check_mut_byte_sub_tuple_3);
+    gen_mut_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_sub,
+        check_mut_byte_sub_tuple_4
+    );
+
+    gen_mut_byte_arith_harness!(i8, byte_offset, check_mut_byte_offset_i8);
+    gen_mut_byte_arith_harness!(i16, byte_offset, check_mut_byte_offset_i16);
+    gen_mut_byte_arith_harness!(i32, byte_offset, check_mut_byte_offset_i32);
+    gen_mut_byte_arith_harness!(i64, byte_offset, check_mut_byte_offset_i64);
+    gen_mut_byte_arith_harness!(i128, byte_offset, check_mut_byte_offset_i128);
+    gen_mut_byte_arith_harness!(isize, byte_offset, check_mut_byte_offset_isize);
+    gen_mut_byte_arith_harness!(u8, byte_offset, check_mut_byte_offset_u8);
+    gen_mut_byte_arith_harness!(u16, byte_offset, check_mut_byte_offset_u16);
+    gen_mut_byte_arith_harness!(u32, byte_offset, check_mut_byte_offset_u32);
+    gen_mut_byte_arith_harness!(u64, byte_offset, check_mut_byte_offset_u64);
+    gen_mut_byte_arith_harness!(u128, byte_offset, check_mut_byte_offset_u128);
+    gen_mut_byte_arith_harness!(usize, byte_offset, check_mut_byte_offset_usize);
+    gen_mut_byte_arith_harness!((i8, i8), byte_offset, check_mut_byte_offset_tuple_1);
+    gen_mut_byte_arith_harness!((f64, bool), byte_offset, check_mut_byte_offset_tuple_2);
+    gen_mut_byte_arith_harness!((i32, f64, bool), byte_offset, check_mut_byte_offset_tuple_3);
+    gen_mut_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_offset,
+        check_mut_byte_offset_tuple_4
+    );
+}

From aec0394315e140eb95ce5bedd85f5b570af1492f Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Thu, 14 Nov 2024 19:59:09 -0800
Subject: [PATCH 02/21] Removes unnecessary rustfmt formnatting

---
 library/core/src/ptr/mut_ptr.rs | 37 +++++++--------------------------
 1 file changed, 7 insertions(+), 30 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 7be6f303f2754..9474b680f7985 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -99,10 +99,7 @@ impl<T: ?Sized> *mut T {
     /// // This dereference is UB. The pointer only has provenance for `x` but points to `y`.
     /// println!("{:?}", unsafe { &*bad });
     #[unstable(feature = "set_ptr_value", issue = "75091")]
-    #[cfg_attr(
-        bootstrap,
-        rustc_const_stable(feature = "ptr_metadata_const", since = "1.83.0")
-    )]
+    #[cfg_attr(bootstrap, rustc_const_stable(feature = "ptr_metadata_const", since = "1.83.0"))]
     #[must_use = "returns a new pointer rather than modifying its argument"]
     #[inline]
     pub const fn with_metadata_of<U>(self, meta: *const U) -> *mut U
@@ -285,11 +282,7 @@ impl<T: ?Sized> *mut T {
     pub const unsafe fn as_ref<'a>(self) -> Option<&'a T> {
         // SAFETY: the caller must guarantee that `self` is valid for a
         // reference if it isn't null.
-        if self.is_null() {
-            None
-        } else {
-            unsafe { Some(&*self) }
-        }
+        if self.is_null() { None } else { unsafe { Some(&*self) } }
     }
 
     /// Returns a shared reference to the value behind the pointer.
@@ -364,11 +357,7 @@ impl<T: ?Sized> *mut T {
     {
         // SAFETY: the caller must guarantee that `self` meets all the
         // requirements for a reference.
-        if self.is_null() {
-            None
-        } else {
-            Some(unsafe { &*(self as *const MaybeUninit<T>) })
-        }
+        if self.is_null() { None } else { Some(unsafe { &*(self as *const MaybeUninit<T>) }) }
     }
 
     /// Adds a signed offset to a pointer.
@@ -569,9 +558,7 @@ impl<T: ?Sized> *mut T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     pub const fn wrapping_byte_offset(self, count: isize) -> Self {
-        self.cast::<u8>()
-            .wrapping_offset(count)
-            .with_metadata_of(self)
+        self.cast::<u8>().wrapping_offset(count).with_metadata_of(self)
     }
 
     /// Masks out bits of the pointer according to a mask.
@@ -612,9 +599,7 @@ impl<T: ?Sized> *mut T {
     #[must_use = "returns a new pointer rather than modifying its argument"]
     #[inline(always)]
     pub fn mask(self, mask: usize) -> *mut T {
-        intrinsics::ptr_mask(self.cast::<()>(), mask)
-            .cast_mut()
-            .with_metadata_of(self)
+        intrinsics::ptr_mask(self.cast::<()>(), mask).cast_mut().with_metadata_of(self)
     }
 
     /// Returns `None` if the pointer is null, or else returns a unique reference to
@@ -664,11 +649,7 @@ impl<T: ?Sized> *mut T {
     pub const unsafe fn as_mut<'a>(self) -> Option<&'a mut T> {
         // SAFETY: the caller must guarantee that `self` is be valid for
         // a mutable reference if it isn't null.
-        if self.is_null() {
-            None
-        } else {
-            unsafe { Some(&mut *self) }
-        }
+        if self.is_null() { None } else { unsafe { Some(&mut *self) } }
     }
 
     /// Returns a unique reference to the value behind the pointer.
@@ -729,11 +710,7 @@ impl<T: ?Sized> *mut T {
     {
         // SAFETY: the caller must guarantee that `self` meets all the
         // requirements for a reference.
-        if self.is_null() {
-            None
-        } else {
-            Some(unsafe { &mut *(self as *mut MaybeUninit<T>) })
-        }
+        if self.is_null() { None } else { Some(unsafe { &mut *(self as *mut MaybeUninit<T>) }) }
     }
 
     /// Returns whether two pointers are guaranteed to be equal.

From 60ba93ec81f626b673b303b5dedaec42e4f5b47d Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Thu, 14 Nov 2024 20:01:09 -0800
Subject: [PATCH 03/21] Adds comment for amgic numbers

---
 library/core/src/ptr/mut_ptr.rs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 9474b680f7985..55bb607cba97e 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2395,6 +2395,7 @@ pub mod verify {
     gen_mut_byte_arith_unit_harness!(byte_sub, check_mut_byte_sub_unit);
     gen_mut_byte_arith_unit_harness!(byte_offset, check_mut_byte_offset_unit);
 
+    // bounding space for PointerGenerator to accommodate 40 elements.
     const ARRAY_LEN: usize = 40;
 
     // generate proof for contracts for byte_add, byte_sub and byte_offset

From 57c591f51d2dcb3d5c94d641c901c24c32c23463 Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Thu, 14 Nov 2024 20:20:10 -0800
Subject: [PATCH 04/21] Adds some comments

---
 library/core/src/ptr/mut_ptr.rs | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 55bb607cba97e..1649570b512fb 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2363,7 +2363,10 @@ pub mod verify {
     use core::mem;
     use kani::PointerGenerator;
 
-    // generate proof for contracts for byte_add, byte_sub and byte_offset for unint types
+    // generate proof for contracts of byte_add, byte_sub and byte_offset to verify
+    // unit pointee type
+    // - `$fn_name`: function for which the contract must be verified
+    // - `$proof_name`: name of the harness generated
     macro_rules! gen_mut_byte_arith_unit_harness {
         (byte_offset, $proof_name:ident) => {
             #[kani::proof_for_contract(<*mut ()>::byte_offset)]
@@ -2399,6 +2402,9 @@ pub mod verify {
     const ARRAY_LEN: usize = 40;
 
     // generate proof for contracts for byte_add, byte_sub and byte_offset
+    // - `$type`: pointee type
+    // - `$fn_name`: function for which the contract must be verified
+    // - `$proof_name`: name of the harness generated
     macro_rules! gen_mut_byte_arith_harness {
         ($type:ty, byte_offset, $proof_name:ident) => {
             #[kani::proof_for_contract(<*mut $type>::byte_offset)]

From a02ed87ccabe595dfcbc9de4d291d63b74af7d59 Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Fri, 15 Nov 2024 15:02:33 -0800
Subject: [PATCH 05/21] Adds slice harnesses

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

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 1649570b512fb..c1bbfbdffa363 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2367,7 +2367,7 @@ pub mod verify {
     // unit pointee type
     // - `$fn_name`: function for which the contract must be verified
     // - `$proof_name`: name of the harness generated
-    macro_rules! gen_mut_byte_arith_unit_harness {
+    macro_rules! gen_mut_byte_arith_harness_for_unit {
         (byte_offset, $proof_name:ident) => {
             #[kani::proof_for_contract(<*mut ()>::byte_offset)]
             pub fn $proof_name() {
@@ -2394,9 +2394,9 @@ pub mod verify {
         };
     }
 
-    gen_mut_byte_arith_unit_harness!(byte_add, check_mut_byte_add_unit);
-    gen_mut_byte_arith_unit_harness!(byte_sub, check_mut_byte_sub_unit);
-    gen_mut_byte_arith_unit_harness!(byte_offset, check_mut_byte_offset_unit);
+    gen_mut_byte_arith_harness_for_unit!(byte_add, check_mut_byte_add_unit);
+    gen_mut_byte_arith_harness_for_unit!(byte_sub, check_mut_byte_sub_unit);
+    gen_mut_byte_arith_harness_for_unit!(byte_offset, check_mut_byte_offset_unit);
 
     // bounding space for PointerGenerator to accommodate 40 elements.
     const ARRAY_LEN: usize = 40;
@@ -2515,4 +2515,76 @@ pub mod verify {
         byte_offset,
         check_mut_byte_offset_tuple_4
     );
+
+    macro_rules! gen_mut_byte_arith_harness_for_slice {
+        ($type:ty, byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*mut [$type]>::byte_offset)]
+            pub fn $proof_name() {
+                let mut arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
+                let slice: &mut [$type] = kani::slice::any_slice_of_array_mut(&mut arr);
+                let ptr: *mut [$type] = slice as *mut [$type];
+
+                let count: isize = kani::any();
+
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($type:ty, $fn_name: ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*mut [$type]>::$fn_name)]
+            pub fn $proof_name() {
+                let mut arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
+                let slice: &mut [$type] = kani::slice::any_slice_of_array_mut(&mut arr);
+                let ptr: *mut [$type] = slice as *mut [$type];
+
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_mut_byte_arith_harness_for_slice!(i8, byte_add, check_mut_byte_add_i8_slice);
+    gen_mut_byte_arith_harness_for_slice!(i16, byte_add, check_mut_byte_add_i16_slice);
+    gen_mut_byte_arith_harness_for_slice!(i32, byte_add, check_mut_byte_add_i32_slice);
+    gen_mut_byte_arith_harness_for_slice!(i64, byte_add, check_mut_byte_add_i64_slice);
+    gen_mut_byte_arith_harness_for_slice!(i128, byte_add, check_mut_byte_add_i128_slice);
+    gen_mut_byte_arith_harness_for_slice!(isize, byte_add, check_mut_byte_add_isize_slice);
+    gen_mut_byte_arith_harness_for_slice!(u8, byte_add, check_mut_byte_add_u8_slice);
+    gen_mut_byte_arith_harness_for_slice!(u16, byte_add, check_mut_byte_add_u16_slice);
+    gen_mut_byte_arith_harness_for_slice!(u32, byte_add, check_mut_byte_add_u32_slice);
+    gen_mut_byte_arith_harness_for_slice!(u64, byte_add, check_mut_byte_add_u64_slice);
+    gen_mut_byte_arith_harness_for_slice!(u128, byte_add, check_mut_byte_add_u128_slice);
+    gen_mut_byte_arith_harness_for_slice!(usize, byte_add, check_mut_byte_add_usize_slice);
+
+    gen_mut_byte_arith_harness_for_slice!(i8, byte_sub, check_mut_byte_sub_i8_slice);
+    gen_mut_byte_arith_harness_for_slice!(i16, byte_sub, check_mut_byte_sub_i16_slice);
+    gen_mut_byte_arith_harness_for_slice!(i32, byte_sub, check_mut_byte_sub_i32_slice);
+    gen_mut_byte_arith_harness_for_slice!(i64, byte_sub, check_mut_byte_sub_i64_slice);
+    gen_mut_byte_arith_harness_for_slice!(i128, byte_sub, check_mut_byte_sub_i128_slice);
+    gen_mut_byte_arith_harness_for_slice!(isize, byte_sub, check_mut_byte_sub_isize_slice);
+    gen_mut_byte_arith_harness_for_slice!(u8, byte_sub, check_mut_byte_sub_u8_slice);
+    gen_mut_byte_arith_harness_for_slice!(u16, byte_sub, check_mut_byte_sub_u16_slice);
+    gen_mut_byte_arith_harness_for_slice!(u32, byte_sub, check_mut_byte_sub_u32_slice);
+    gen_mut_byte_arith_harness_for_slice!(u64, byte_sub, check_mut_byte_sub_u64_slice);
+    gen_mut_byte_arith_harness_for_slice!(u128, byte_sub, check_mut_byte_sub_u128_slice);
+    gen_mut_byte_arith_harness_for_slice!(usize, byte_sub, check_mut_byte_sub_usize_slice);
+
+    gen_mut_byte_arith_harness_for_slice!(i8, byte_offset, check_mut_byte_offset_i8_slice);
+    gen_mut_byte_arith_harness_for_slice!(i16, byte_offset, check_mut_byte_offset_i16_slice);
+    gen_mut_byte_arith_harness_for_slice!(i32, byte_offset, check_mut_byte_offset_i32_slice);
+    gen_mut_byte_arith_harness_for_slice!(i64, byte_offset, check_mut_byte_offset_i64_slice);
+    gen_mut_byte_arith_harness_for_slice!(i128, byte_offset, check_mut_byte_offset_i128_slice);
+    gen_mut_byte_arith_harness_for_slice!(isize, byte_offset, check_mut_byte_offset_isize_slice);
+    gen_mut_byte_arith_harness_for_slice!(u8, byte_offset, check_mut_byte_offset_u8_slice);
+    gen_mut_byte_arith_harness_for_slice!(u16, byte_offset, check_mut_byte_offset_u16_slice);
+    gen_mut_byte_arith_harness_for_slice!(u32, byte_offset, check_mut_byte_offset_u32_slice);
+    gen_mut_byte_arith_harness_for_slice!(u64, byte_offset, check_mut_byte_offset_u64_slice);
+    gen_mut_byte_arith_harness_for_slice!(u128, byte_offset, check_mut_byte_offset_u128_slice);
+    gen_mut_byte_arith_harness_for_slice!(usize, byte_offset, check_mut_byte_offset_usize_slice);
 }

From 2fdebd6dcfdf1513ba9c54b132bb860817786207 Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Sat, 16 Nov 2024 01:35:11 -0800
Subject: [PATCH 06/21] Adds contracts for byte_offset, byte_add and byte_sub

- Adds harnesses for int, unit, composite and slice types
---
 library/core/src/ptr/const_ptr.rs | 288 ++++++++++++++++++++++++++++++
 1 file changed, 288 insertions(+)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 57a7c0fc0925c..a501e6113683d 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -3,6 +3,11 @@ use crate::cmp::Ordering::{Equal, Greater, Less};
 use crate::intrinsics::const_eval_select;
 use crate::mem::SizedTypeProperties;
 use crate::slice::{self, SliceIndex};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
+use core::mem;
 
 impl<T: ?Sized> *const T {
     /// Returns `true` if the pointer is null.
@@ -459,6 +464,22 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero, then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // are pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *mut u8 as isize).checked_add(count).is_some() &&
+            ((self as *mut u8 as usize) == (self.wrapping_byte_offset(count) as *mut u8 as usize) ||
+                kani::mem::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T)))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *mut u8 as usize) == (*result as *mut u8 as usize)) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
         unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
@@ -972,6 +993,22 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero, then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // are pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *mut u8 as isize).checked_add(count as isize).is_some() &&
+            ((self as *mut u8 as usize) == (self.wrapping_byte_add(count) as *mut u8 as usize) ||
+                kani::mem::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T)))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *mut u8 as usize) == (*result as *mut u8 as usize)) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
         unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
@@ -1087,6 +1124,22 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // would be pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *mut u8 as isize).checked_sub(count as isize).is_some() &&
+            ((self as *mut u8 as usize) == (self.wrapping_byte_sub(count) as *mut u8 as usize) ||
+                kani::mem::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T)))
+    )]
+    #[ensures(|result|
+         // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *mut u8 as isize) == (*result as *mut u8 as isize)) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.
         unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
@@ -1899,3 +1952,238 @@ impl<T: ?Sized> PartialOrd for *const T {
         *self >= *other
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use crate::kani;
+    use core::mem;
+    use kani::PointerGenerator;
+
+    // generate proof for contracts of byte_add, byte_sub and byte_offset to verify
+    // unit pointee type
+    // - `$fn_name`: function for which the contract must be verified
+    // - `$proof_name`: name of the harness generated
+    macro_rules! gen_const_byte_arith_harness_for_unit {
+        (byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const ()>::byte_offset)]
+            pub fn $proof_name() {
+                let val = ();
+                let ptr: *const () = &val;
+                let count: isize = kani::any();
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($fn_name:ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const ()>::$fn_name)]
+            pub fn $proof_name() {
+                let val = ();
+                let ptr: *const () = &val;
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_const_byte_arith_harness_for_unit!(byte_add, check_const_byte_add_unit);
+    gen_const_byte_arith_harness_for_unit!(byte_sub, check_const_byte_sub_unit);
+    gen_const_byte_arith_harness_for_unit!(byte_offset, check_const_byte_offset_unit);
+
+    // bounding space for PointerGenerator to accommodate 40 elements.
+    const ARRAY_LEN: usize = 40;
+
+
+    // generate proof for contracts for byte_add, byte_sub and byte_offset
+    // - `$type`: pointee type
+    // - `$fn_name`: function for which the contract must be verified
+    // - `$proof_name`: name of the harness generated
+    macro_rules! gen_const_byte_arith_harness {
+        ($type:ty, byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const $type>::byte_offset)]
+            pub fn $proof_name() {
+                // generator with space for single element
+                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
+                // generator with space for multiple elements
+                let mut generator2 =
+                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
+
+                let ptr: *const $type = if kani::any() {
+                    generator1.any_in_bounds().ptr
+                } else {
+                    generator2.any_in_bounds().ptr
+                };
+
+                let count: isize = kani::any();
+
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($type:ty, $fn_name:ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const $type>::$fn_name)]
+            pub fn $proof_name() {
+                // generator with space for single element
+                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
+                // generator with space for multiple elements
+                let mut generator2 =
+                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
+
+                let ptr: *const $type = if kani::any() {
+                    generator1.any_in_bounds().ptr
+                } else {
+                    generator2.any_in_bounds().ptr
+                };
+
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_const_byte_arith_harness!(i8, byte_add, check_const_byte_add_i8);
+    gen_const_byte_arith_harness!(i16, byte_add, check_const_byte_add_i16);
+    gen_const_byte_arith_harness!(i32, byte_add, check_const_byte_add_i32);
+    gen_const_byte_arith_harness!(i64, byte_add, check_const_byte_add_i64);
+    gen_const_byte_arith_harness!(i128, byte_add, check_const_byte_add_i128);
+    gen_const_byte_arith_harness!(isize, byte_add, check_const_byte_add_isize);
+    gen_const_byte_arith_harness!(u8, byte_add, check_const_byte_add_u8);
+    gen_const_byte_arith_harness!(u16, byte_add, check_const_byte_add_u16);
+    gen_const_byte_arith_harness!(u32, byte_add, check_const_byte_add_u32);
+    gen_const_byte_arith_harness!(u64, byte_add, check_const_byte_add_u64);
+    gen_const_byte_arith_harness!(u128, byte_add, check_const_byte_add_u128);
+    gen_const_byte_arith_harness!(usize, byte_add, check_const_byte_add_usize);
+    gen_const_byte_arith_harness!((i8, i8), byte_add, check_const_byte_add_tuple_1);
+    gen_const_byte_arith_harness!((f64, bool), byte_add, check_const_byte_add_tuple_2);
+    gen_const_byte_arith_harness!((i32, f64, bool), byte_add, check_const_byte_add_tuple_3);
+    gen_const_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_add,
+        check_const_byte_add_tuple_4
+    );
+
+    gen_const_byte_arith_harness!(i8, byte_sub, check_const_byte_sub_i8);
+    gen_const_byte_arith_harness!(i16, byte_sub, check_const_byte_sub_i16);
+    gen_const_byte_arith_harness!(i32, byte_sub, check_const_byte_sub_i32);
+    gen_const_byte_arith_harness!(i64, byte_sub, check_const_byte_sub_i64);
+    gen_const_byte_arith_harness!(i128, byte_sub, check_const_byte_sub_i128);
+    gen_const_byte_arith_harness!(isize, byte_sub, check_const_byte_sub_isize);
+    gen_const_byte_arith_harness!(u8, byte_sub, check_const_byte_sub_u8);
+    gen_const_byte_arith_harness!(u16, byte_sub, check_const_byte_sub_u16);
+    gen_const_byte_arith_harness!(u32, byte_sub, check_const_byte_sub_u32);
+    gen_const_byte_arith_harness!(u64, byte_sub, check_const_byte_sub_u64);
+    gen_const_byte_arith_harness!(u128, byte_sub, check_const_byte_sub_u128);
+    gen_const_byte_arith_harness!(usize, byte_sub, check_const_byte_sub_usize);
+    gen_const_byte_arith_harness!((i8, i8), byte_sub, check_const_byte_sub_tuple_1);
+    gen_const_byte_arith_harness!((f64, bool), byte_sub, check_const_byte_sub_tuple_2);
+    gen_const_byte_arith_harness!((i32, f64, bool), byte_sub, check_const_byte_sub_tuple_3);
+    gen_const_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_sub,
+        check_const_byte_sub_tuple_4
+    );
+
+    gen_const_byte_arith_harness!(i8, byte_offset, check_const_byte_offset_i8);
+    gen_const_byte_arith_harness!(i16, byte_offset, check_const_byte_offset_i16);
+    gen_const_byte_arith_harness!(i32, byte_offset, check_const_byte_offset_i32);
+    gen_const_byte_arith_harness!(i64, byte_offset, check_const_byte_offset_i64);
+    gen_const_byte_arith_harness!(i128, byte_offset, check_const_byte_offset_i128);
+    gen_const_byte_arith_harness!(isize, byte_offset, check_const_byte_offset_isize);
+    gen_const_byte_arith_harness!(u8, byte_offset, check_const_byte_offset_u8);
+    gen_const_byte_arith_harness!(u16, byte_offset, check_const_byte_offset_u16);
+    gen_const_byte_arith_harness!(u32, byte_offset, check_const_byte_offset_u32);
+    gen_const_byte_arith_harness!(u64, byte_offset, check_const_byte_offset_u64);
+    gen_const_byte_arith_harness!(u128, byte_offset, check_const_byte_offset_u128);
+    gen_const_byte_arith_harness!(usize, byte_offset, check_const_byte_offset_usize);
+    gen_const_byte_arith_harness!((i8, i8), byte_offset, check_const_byte_offset_tuple_1);
+    gen_const_byte_arith_harness!((f64, bool), byte_offset, check_const_byte_offset_tuple_2);
+    gen_const_byte_arith_harness!((i32, f64, bool), byte_offset, check_const_byte_offset_tuple_3);
+    gen_const_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_offset,
+        check_const_byte_offset_tuple_4
+    );
+
+    macro_rules! gen_const_byte_arith_harness_for_slice {
+        ($type:ty, byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const [$type]>::byte_offset)]
+            pub fn $proof_name() {
+                let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
+                let slice: &[$type] = kani::slice::any_slice_of_array(&arr);
+                let ptr: *const [$type] = slice;
+
+                let count: isize = kani::any();
+
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($type:ty, $fn_name: ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const [$type]>::$fn_name)]
+            pub fn $proof_name() {
+                let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
+                let slice: &[$type] = kani::slice::any_slice_of_array(&arr);
+                let ptr: *const [$type] = slice;
+
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_const_byte_arith_harness_for_slice!(i8, byte_add, check_const_byte_add_i8_slice);
+    gen_const_byte_arith_harness_for_slice!(i16, byte_add, check_const_byte_add_i16_slice);
+    gen_const_byte_arith_harness_for_slice!(i32, byte_add, check_const_byte_add_i32_slice);
+    gen_const_byte_arith_harness_for_slice!(i64, byte_add, check_const_byte_add_i64_slice);
+    gen_const_byte_arith_harness_for_slice!(i128, byte_add, check_const_byte_add_i128_slice);
+    gen_const_byte_arith_harness_for_slice!(isize, byte_add, check_const_byte_add_isize_slice);
+    gen_const_byte_arith_harness_for_slice!(u8, byte_add, check_const_byte_add_u8_slice);
+    gen_const_byte_arith_harness_for_slice!(u16, byte_add, check_const_byte_add_u16_slice);
+    gen_const_byte_arith_harness_for_slice!(u32, byte_add, check_const_byte_add_u32_slice);
+    gen_const_byte_arith_harness_for_slice!(u64, byte_add, check_const_byte_add_u64_slice);
+    gen_const_byte_arith_harness_for_slice!(u128, byte_add, check_const_byte_add_u128_slice);
+    gen_const_byte_arith_harness_for_slice!(usize, byte_add, check_const_byte_add_usize_slice);
+
+    gen_const_byte_arith_harness_for_slice!(i8, byte_sub, check_const_byte_sub_i8_slice);
+    gen_const_byte_arith_harness_for_slice!(i16, byte_sub, check_const_byte_sub_i16_slice);
+    gen_const_byte_arith_harness_for_slice!(i32, byte_sub, check_const_byte_sub_i32_slice);
+    gen_const_byte_arith_harness_for_slice!(i64, byte_sub, check_const_byte_sub_i64_slice);
+    gen_const_byte_arith_harness_for_slice!(i128, byte_sub, check_const_byte_sub_i128_slice);
+    gen_const_byte_arith_harness_for_slice!(isize, byte_sub, check_const_byte_sub_isize_slice);
+    gen_const_byte_arith_harness_for_slice!(u8, byte_sub, check_const_byte_sub_u8_slice);
+    gen_const_byte_arith_harness_for_slice!(u16, byte_sub, check_const_byte_sub_u16_slice);
+    gen_const_byte_arith_harness_for_slice!(u32, byte_sub, check_const_byte_sub_u32_slice);
+    gen_const_byte_arith_harness_for_slice!(u64, byte_sub, check_const_byte_sub_u64_slice);
+    gen_const_byte_arith_harness_for_slice!(u128, byte_sub, check_const_byte_sub_u128_slice);
+    gen_const_byte_arith_harness_for_slice!(usize, byte_sub, check_const_byte_sub_usize_slice);
+
+    gen_const_byte_arith_harness_for_slice!(i8, byte_offset, check_const_byte_offset_i8_slice);
+    gen_const_byte_arith_harness_for_slice!(i16, byte_offset, check_const_byte_offset_i16_slice);
+    gen_const_byte_arith_harness_for_slice!(i32, byte_offset, check_const_byte_offset_i32_slice);
+    gen_const_byte_arith_harness_for_slice!(i64, byte_offset, check_const_byte_offset_i64_slice);
+    gen_const_byte_arith_harness_for_slice!(i128, byte_offset, check_const_byte_offset_i128_slice);
+    gen_const_byte_arith_harness_for_slice!(isize, byte_offset, check_const_byte_offset_isize_slice);
+    gen_const_byte_arith_harness_for_slice!(u8, byte_offset, check_const_byte_offset_u8_slice);
+    gen_const_byte_arith_harness_for_slice!(u16, byte_offset, check_const_byte_offset_u16_slice);
+    gen_const_byte_arith_harness_for_slice!(u32, byte_offset, check_const_byte_offset_u32_slice);
+    gen_const_byte_arith_harness_for_slice!(u64, byte_offset, check_const_byte_offset_u64_slice);
+    gen_const_byte_arith_harness_for_slice!(u128, byte_offset, check_const_byte_offset_u128_slice);
+    gen_const_byte_arith_harness_for_slice!(usize, byte_offset, check_const_byte_offset_usize_slice);
+}

From cd0a13429c46e1037a913295bd7f4bd3215f24dc Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Sat, 16 Nov 2024 14:27:34 -0800
Subject: [PATCH 07/21] Runs rustfmt

---
 library/core/src/ptr/const_ptr.rs | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index a501e6113683d..08ff2f331b5cf 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -1998,7 +1998,6 @@ pub mod verify {
     // bounding space for PointerGenerator to accommodate 40 elements.
     const ARRAY_LEN: usize = 40;
 
-
     // generate proof for contracts for byte_add, byte_sub and byte_offset
     // - `$type`: pointee type
     // - `$fn_name`: function for which the contract must be verified
@@ -2108,7 +2107,11 @@ pub mod verify {
     gen_const_byte_arith_harness!(usize, byte_offset, check_const_byte_offset_usize);
     gen_const_byte_arith_harness!((i8, i8), byte_offset, check_const_byte_offset_tuple_1);
     gen_const_byte_arith_harness!((f64, bool), byte_offset, check_const_byte_offset_tuple_2);
-    gen_const_byte_arith_harness!((i32, f64, bool), byte_offset, check_const_byte_offset_tuple_3);
+    gen_const_byte_arith_harness!(
+        (i32, f64, bool),
+        byte_offset,
+        check_const_byte_offset_tuple_3
+    );
     gen_const_byte_arith_harness!(
         (i8, u16, i32, u64, isize),
         byte_offset,
@@ -2179,11 +2182,19 @@ pub mod verify {
     gen_const_byte_arith_harness_for_slice!(i32, byte_offset, check_const_byte_offset_i32_slice);
     gen_const_byte_arith_harness_for_slice!(i64, byte_offset, check_const_byte_offset_i64_slice);
     gen_const_byte_arith_harness_for_slice!(i128, byte_offset, check_const_byte_offset_i128_slice);
-    gen_const_byte_arith_harness_for_slice!(isize, byte_offset, check_const_byte_offset_isize_slice);
+    gen_const_byte_arith_harness_for_slice!(
+        isize,
+        byte_offset,
+        check_const_byte_offset_isize_slice
+    );
     gen_const_byte_arith_harness_for_slice!(u8, byte_offset, check_const_byte_offset_u8_slice);
     gen_const_byte_arith_harness_for_slice!(u16, byte_offset, check_const_byte_offset_u16_slice);
     gen_const_byte_arith_harness_for_slice!(u32, byte_offset, check_const_byte_offset_u32_slice);
     gen_const_byte_arith_harness_for_slice!(u64, byte_offset, check_const_byte_offset_u64_slice);
     gen_const_byte_arith_harness_for_slice!(u128, byte_offset, check_const_byte_offset_u128_slice);
-    gen_const_byte_arith_harness_for_slice!(usize, byte_offset, check_const_byte_offset_usize_slice);
+    gen_const_byte_arith_harness_for_slice!(
+        usize,
+        byte_offset,
+        check_const_byte_offset_usize_slice
+    );
 }

From 40eb29d1061fdc801b4e1b7ca974162a66f73cab Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Wed, 20 Nov 2024 23:55:15 -0800
Subject: [PATCH 08/21] Some refactoring

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

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index c1bbfbdffa363..6f610cb03ab14 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2372,7 +2372,7 @@ pub mod verify {
             #[kani::proof_for_contract(<*mut ()>::byte_offset)]
             pub fn $proof_name() {
                 let mut val = ();
-                let ptr: *mut () = &mut val as *mut ();
+                let ptr: *mut () = &mut val;
                 let count: isize = kani::any();
                 unsafe {
                     ptr.byte_offset(count);
@@ -2384,7 +2384,7 @@ pub mod verify {
             #[kani::proof_for_contract(<*mut ()>::$fn_name)]
             pub fn $proof_name() {
                 let mut val = ();
-                let ptr: *mut () = &mut val as *mut ();
+                let ptr: *mut () = &mut val;
                 //byte_add and byte_sub need count to be usize unlike byte_offset
                 let count: usize = kani::any();
                 unsafe {
@@ -2416,9 +2416,9 @@ pub mod verify {
                     PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
 
                 let ptr: *mut $type = if kani::any() {
-                    generator1.any_in_bounds().ptr as *mut $type
+                    generator1.any_in_bounds().ptr
                 } else {
-                    generator2.any_in_bounds().ptr as *mut $type
+                    generator2.any_in_bounds().ptr
                 };
                 let count: isize = kani::any();
 
@@ -2438,9 +2438,9 @@ pub mod verify {
                     PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
 
                 let ptr: *mut $type = if kani::any() {
-                    generator1.any_in_bounds().ptr as *mut $type
+                    generator1.any_in_bounds().ptr
                 } else {
-                    generator2.any_in_bounds().ptr as *mut $type
+                    generator2.any_in_bounds().ptr
                 };
 
                 //byte_add and byte_sub need count to be usize unlike byte_offset
@@ -2522,7 +2522,7 @@ pub mod verify {
             pub fn $proof_name() {
                 let mut arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
                 let slice: &mut [$type] = kani::slice::any_slice_of_array_mut(&mut arr);
-                let ptr: *mut [$type] = slice as *mut [$type];
+                let ptr: *mut [$type] = slice;
 
                 let count: isize = kani::any();
 
@@ -2537,7 +2537,7 @@ pub mod verify {
             pub fn $proof_name() {
                 let mut arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
                 let slice: &mut [$type] = kani::slice::any_slice_of_array_mut(&mut arr);
-                let ptr: *mut [$type] = slice as *mut [$type];
+                let ptr: *mut [$type] = slice;
 
                 //byte_add and byte_sub need count to be usize unlike byte_offset
                 let count: usize = kani::any();

From 81fe7c9ae7396f775490f37359e39357f4bdb33a Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Thu, 21 Nov 2024 00:38:38 -0800
Subject: [PATCH 09/21] Refactors the function contracts

---
 library/core/src/ptr/const_ptr.rs | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 08ff2f331b5cf..db5b08e59be90 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -471,14 +471,14 @@ impl<T: ?Sized> *const T {
         // bytes doesn't cause overflow and that both pointers `self` and the result
         // are pointing to the same address or in the same allocation
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *mut u8 as isize).checked_add(count).is_some() &&
-            ((self as *mut u8 as usize) == (self.wrapping_byte_offset(count) as *mut u8 as usize) ||
-                kani::mem::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T)))
+            (self as *const u8 as isize).checked_add(count).is_some() &&
+            ((self as *const u8 as usize) == (self.wrapping_byte_offset(count) as *const u8 as usize) ||
+                kani::mem::same_allocation(self, self.wrapping_byte_offset(count))))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *mut u8 as usize) == (*result as *mut u8 as usize)) ||
-        (kani::mem::same_allocation(self as *const T, *result as *const T))
+        ((self as *const u8 as usize) == (*result as *const u8 as usize)) ||
+        (kani::mem::same_allocation(self, *result))
     )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
@@ -1000,14 +1000,14 @@ impl<T: ?Sized> *const T {
         // bytes doesn't cause overflow and that both pointers `self` and the result
         // are pointing to the same address or in the same allocation
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *mut u8 as isize).checked_add(count as isize).is_some() &&
-            ((self as *mut u8 as usize) == (self.wrapping_byte_add(count) as *mut u8 as usize) ||
-                kani::mem::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T)))
+            (self as *const u8 as isize).checked_add(count as isize).is_some() &&
+            ((self as *const u8 as usize) == (self.wrapping_byte_add(count) as *const u8 as usize) ||
+                kani::mem::same_allocation(self, self.wrapping_byte_add(count))))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *mut u8 as usize) == (*result as *mut u8 as usize)) ||
-        (kani::mem::same_allocation(self as *const T, *result as *const T))
+        ((self as *const u8 as usize) == (*result as *const u8 as usize)) ||
+        (kani::mem::same_allocation(self, *result))
     )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
@@ -1131,14 +1131,14 @@ impl<T: ?Sized> *const T {
         // bytes doesn't cause overflow and that both pointers `self` and the result
         // would be pointing to the same address or in the same allocation
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *mut u8 as isize).checked_sub(count as isize).is_some() &&
-            ((self as *mut u8 as usize) == (self.wrapping_byte_sub(count) as *mut u8 as usize) ||
-                kani::mem::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T)))
+            (self as *const u8 as isize).checked_sub(count as isize).is_some() &&
+            ((self as *const u8 as usize) == (self.wrapping_byte_sub(count) as *const u8 as usize) ||
+                kani::mem::same_allocation(self, self.wrapping_byte_sub(count))))
     )]
     #[ensures(|result|
          // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *mut u8 as isize) == (*result as *mut u8 as isize)) ||
-        (kani::mem::same_allocation(self as *const T, *result as *const T))
+        ((self as *const u8 as isize) == (*result as *const u8 as isize)) ||
+        (kani::mem::same_allocation(self, *result))
     )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.

From 5e4f6162bc1ea7a4ea6be4b042b5eaf1e051155d Mon Sep 17 00:00:00 2001
From: Surya Togaru <stogaru@andrew.cmu.edu>
Date: Mon, 25 Nov 2024 23:00:39 -0800
Subject: [PATCH 10/21] Addresses commennts on PR

---
 library/core/src/ptr/const_ptr.rs | 58 ++++++++++++++-----------------
 library/core/src/ptr/mut_ptr.rs   | 53 +++++++++++++---------------
 2 files changed, 51 insertions(+), 60 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index bbd6ee6d52fc5..85a3f81ba50d8 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -465,19 +465,18 @@ impl<T: ?Sized> *const T {
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
-        // If the size of the pointee is zero, then `count` must also be zero
-        (mem::size_of_val_raw(self) == 0 && count == 0) ||
-        // If the size of the pointee is not zero, then ensure that adding `count`
-        // bytes doesn't cause overflow and that both pointers `self` and the result
-        // are pointing to the same address or in the same allocation
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) ||
+        // Else if count is not zero, then ensure that adding `count` doesn't cause 
+        // overflow and that both pointers `self` and the result are in the same 
+        // allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *const u8 as isize).checked_add(count).is_some() &&
-            ((self as *const u8 as usize) == (self.wrapping_byte_offset(count) as *const u8 as usize) ||
-                kani::mem::same_allocation(self, self.wrapping_byte_offset(count))))
+            (self.addr() as isize).checked_add(count).is_some() &&
+            kani::mem::same_allocation(self, self.wrapping_byte_offset(count)))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *const u8 as usize) == (*result as *const u8 as usize)) ||
+        (self.addr() == (*result).addr()) ||
         (kani::mem::same_allocation(self, *result))
     )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
@@ -1004,19 +1003,18 @@ impl<T: ?Sized> *const T {
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
-        // If the size of the pointee is zero, then `count` must also be zero
-        (mem::size_of_val_raw(self) == 0 && count == 0) ||
-        // If the size of the pointee is not zero, then ensure that adding `count`
-        // bytes doesn't cause overflow and that both pointers `self` and the result
-        // are pointing to the same address or in the same allocation
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that adding `count` doesn't cause 
+        // overflow and that both pointers `self` and the result are in the same 
+        // allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *const u8 as isize).checked_add(count as isize).is_some() &&
-            ((self as *const u8 as usize) == (self.wrapping_byte_add(count) as *const u8 as usize) ||
-                kani::mem::same_allocation(self, self.wrapping_byte_add(count))))
+            (self.addr() as isize).checked_add(count as isize).is_some() && 
+            kani::mem::same_allocation(self, self.wrapping_byte_add(count)))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *const u8 as usize) == (*result as *const u8 as usize)) ||
+        (self.addr() == (*result).addr()) ||
         (kani::mem::same_allocation(self, *result))
     )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
@@ -1135,19 +1133,18 @@ impl<T: ?Sized> *const T {
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
-        // If the size of the pointee is zero, then `count` must also be zero
-        (mem::size_of_val_raw(self) == 0 && count == 0) ||
-        // If the size of the pointee is not zero then ensure that adding `count`
-        // bytes doesn't cause overflow and that both pointers `self` and the result
-        // would be pointing to the same address or in the same allocation
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that subtracting `count` doesn't 
+        // cause overflow and that both pointers `self` and the result are in the 
+        // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *const u8 as isize).checked_sub(count as isize).is_some() &&
-            ((self as *const u8 as usize) == (self.wrapping_byte_sub(count) as *const u8 as usize) ||
-                kani::mem::same_allocation(self, self.wrapping_byte_sub(count))))
+            (self.addr() as isize).checked_sub(count as isize).is_some() && 
+            kani::mem::same_allocation(self, self.wrapping_byte_sub(count)))
     )]
     #[ensures(|result|
-         // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *const u8 as isize) == (*result as *const u8 as isize)) ||
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        (self.addr() == (*result).addr()) ||
         (kani::mem::same_allocation(self, *result))
     )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
@@ -1982,7 +1979,7 @@ mod verify {
         }
     }
 
-    // Array size bound for kani::any_array
+    // bounding space for PointerGenerator to accommodate 40 elements.
     const ARRAY_LEN: usize = 40;
 
     macro_rules! generate_offset_from_harness {
@@ -2143,9 +2140,6 @@ mod verify {
     gen_const_byte_arith_harness_for_unit!(byte_sub, check_const_byte_sub_unit);
     gen_const_byte_arith_harness_for_unit!(byte_offset, check_const_byte_offset_unit);
 
-    // bounding space for PointerGenerator to accommodate 40 elements.
-    const ARRAY_LEN: usize = 40;
-
     // generate proof for contracts for byte_add, byte_sub and byte_offset
     // - `$type`: pointee type
     // - `$fn_name`: function for which the contract must be verified
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 6f610cb03ab14..5ae20d7d9db59 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -463,19 +463,18 @@ impl<T: ?Sized> *mut T {
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
-        // If the size of the pointee is zero, then `count` must also be zero
-        (mem::size_of_val_raw(self) == 0 && count == 0) ||
-        // If the size of the pointee is not zero, then ensure that adding `count`
-        // bytes doesn't cause overflow and that both pointers `self` and the result
-        // are pointing to the same address or in the same allocation
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that subtracting `count` doesn't 
+        // cause overflow and that both pointers `self` and the result are in the 
+        // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *mut u8 as isize).checked_add(count).is_some() &&
-            ((self as *mut u8 as usize) == (self.wrapping_byte_offset(count) as *mut u8 as usize) ||
-                kani::mem::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T)))
+            (self.addr() as isize).checked_add(count).is_some() && 
+            kani::mem::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *mut u8 as usize) == (*result as *mut u8 as usize)) ||
+        (self.addr() == (*result).addr()) ||
         (kani::mem::same_allocation(self as *const T, *result as *const T))
     )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
@@ -1074,19 +1073,18 @@ impl<T: ?Sized> *mut T {
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
-        // If the size of the pointee is zero, then `count` must also be zero
-        (mem::size_of_val_raw(self) == 0 && count == 0) ||
-        // If the size of the pointee is not zero, then ensure that adding `count`
-        // bytes doesn't cause overflow and that both pointers `self` and the result
-        // are pointing to the same address or in the same allocation
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that subtracting `count` doesn't 
+        // cause overflow and that both pointers `self` and the result are in the 
+        // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *mut u8 as isize).checked_add(count as isize).is_some() &&
-            ((self as *mut u8 as usize) == (self.wrapping_byte_add(count) as *mut u8 as usize) ||
-                kani::mem::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T)))
+            (self.addr() as isize).checked_add(count as isize).is_some() && 
+            kani::mem::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *mut u8 as usize) == (*result as *mut u8 as usize)) ||
+        (self.addr() == (*result).addr()) ||
         (kani::mem::same_allocation(self as *const T, *result as *const T))
     )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
@@ -1205,19 +1203,18 @@ impl<T: ?Sized> *mut T {
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
-        // If the size of the pointee is zero, then `count` must also be zero
-        (mem::size_of_val_raw(self) == 0 && count == 0) ||
-        // If the size of the pointee is not zero then ensure that adding `count`
-        // bytes doesn't cause overflow and that both pointers `self` and the result
-        // would be pointing to the same address or in the same allocation
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that subtracting `count` doesn't 
+        // cause overflow and that both pointers `self` and the result are in the 
+        // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self as *mut u8 as isize).checked_sub(count as isize).is_some() &&
-            ((self as *mut u8 as usize) == (self.wrapping_byte_sub(count) as *mut u8 as usize) ||
-                kani::mem::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T)))
+            (self.addr() as isize).checked_sub(count as isize).is_some() && 
+            kani::mem::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T))
     )]
     #[ensures(|result|
-         // The resulting pointer should either be unchanged or still point to the same allocation
-        ((self as *mut u8 as isize) == (*result as *mut u8 as isize)) ||
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        (self.addr() == (*result).addr()) ||
         (kani::mem::same_allocation(self as *const T, *result as *const T))
     )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {

From 7e979cb9b7c20ba55a265c01e923b2b8ce178d69 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Tue, 26 Nov 2024 23:47:06 -0800
Subject: [PATCH 11/21] Implemented proof for contracts for dyn trait for
 byte_add, byte_sub and byte_offset

---
 library/core/src/ptr/const_ptr.rs | 378 +++---------------------------
 library/core/src/ptr/mut_ptr.rs   | 228 +++---------------
 2 files changed, 57 insertions(+), 549 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 85a3f81ba50d8..dc49aa77d72bf 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -1962,381 +1962,61 @@ impl<T: ?Sized> PartialOrd for *const T {
 
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
-mod verify {
+pub mod verify {
     use crate::kani;
     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);
-        }
-    }
-
-    // bounding space for PointerGenerator to accommodate 40 elements.
-    const ARRAY_LEN: usize = 40;
-
-    macro_rules! generate_offset_from_harness {
-        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
-            // Proof for a single element
-            #[kani::proof_for_contract(<*const $type>::offset_from)]
-            pub fn $proof_name1() {
-                const gen_size: usize = mem::size_of::<$type>();
-                let mut generator1 = PointerGenerator::<gen_size>::new();
-                let mut generator2 = PointerGenerator::<gen_size>::new();
-                let ptr1: *const $type = generator1.any_in_bounds().ptr;
-                let ptr2: *const $type = if kani::any() {
-                    generator1.any_alloc_status().ptr
-                } else {
-                    generator2.any_alloc_status().ptr
-                };
-
-                unsafe {
-                    ptr1.offset_from(ptr2);
-                }
-            }
-
-            // Proof for large arrays
-            #[kani::proof_for_contract(<*const $type>::offset_from)]
-            pub fn $proof_name2() {
-                const gen_size: usize = mem::size_of::<$type>();
-                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
-                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
-                let ptr1: *const $type = generator1.any_in_bounds().ptr;
-                let ptr2: *const $type = if kani::any() {
-                    generator1.any_alloc_status().ptr
-                } else {
-                    generator2.any_alloc_status().ptr
-                };
+    trait TestTrait {}
 
-                unsafe {
-                    ptr1.offset_from(ptr2);
-                }
-            }
-        };
+    struct TestStruct {
+        value: i64,
     }
 
-    generate_offset_from_harness!(
-        u8,
-        check_const_offset_from_u8,
-        check_const_offset_from_u8_arr
-    );
-    generate_offset_from_harness!(
-        u16,
-        check_const_offset_from_u16,
-        check_const_offset_from_u16_arr
-    );
-    generate_offset_from_harness!(
-        u32,
-        check_const_offset_from_u32,
-        check_const_offset_from_u32_arr
-    );
-    generate_offset_from_harness!(
-        u64,
-        check_const_offset_from_u64,
-        check_const_offset_from_u64_arr
-    );
-    generate_offset_from_harness!(
-        u128,
-        check_const_offset_from_u128,
-        check_const_offset_from_u128_arr
-    );
-    generate_offset_from_harness!(
-        usize,
-        check_const_offset_from_usize,
-        check_const_offset_from_usize_arr
-    );
-
-    generate_offset_from_harness!(
-        i8,
-        check_const_offset_from_i8,
-        check_const_offset_from_i8_arr
-    );
-    generate_offset_from_harness!(
-        i16,
-        check_const_offset_from_i16,
-        check_const_offset_from_i16_arr
-    );
-    generate_offset_from_harness!(
-        i32,
-        check_const_offset_from_i32,
-        check_const_offset_from_i32_arr
-    );
-    generate_offset_from_harness!(
-        i64,
-        check_const_offset_from_i64,
-        check_const_offset_from_i64_arr
-    );
-    generate_offset_from_harness!(
-        i128,
-        check_const_offset_from_i128,
-        check_const_offset_from_i128_arr
-    );
-    generate_offset_from_harness!(
-        isize,
-        check_const_offset_from_isize,
-        check_const_offset_from_isize_arr
-    );
-
-    generate_offset_from_harness!(
-        (i8, i8),
-        check_const_offset_from_tuple_1,
-        check_const_offset_from_tuple_1_arr
-    );
-    generate_offset_from_harness!(
-        (f64, bool),
-        check_const_offset_from_tuple_2,
-        check_const_offset_from_tuple_2_arr
-    );
-    generate_offset_from_harness!(
-        (u32, i16, f32),
-        check_const_offset_from_tuple_3,
-        check_const_offset_from_tuple_3_arr
-    );
-    generate_offset_from_harness!(
-        ((), bool, u8, u16, i32, f64, i128, usize),
-        check_const_offset_from_tuple_4,
-        check_const_offset_from_tuple_4_arr
-    );
-
-    // generate proof for contracts of byte_add, byte_sub and byte_offset to verify
-    // unit pointee type
-    // - `$fn_name`: function for which the contract must be verified
-    // - `$proof_name`: name of the harness generated
-    macro_rules! gen_const_byte_arith_harness_for_unit {
-        (byte_offset, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*const ()>::byte_offset)]
-            pub fn $proof_name() {
-                let val = ();
-                let ptr: *const () = &val;
-                let count: isize = kani::any();
-                unsafe {
-                    ptr.byte_offset(count);
-                }
-            }
-        };
+    impl TestTrait for TestStruct {}
 
-        ($fn_name:ident, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*const ()>::$fn_name)]
-            pub fn $proof_name() {
-                let val = ();
-                let ptr: *const () = &val;
-                //byte_add and byte_sub need count to be usize unlike byte_offset
-                let count: usize = kani::any();
-                unsafe {
-                    ptr.$fn_name(count);
-                }
-            }
-        };
-    }
-
-    gen_const_byte_arith_harness_for_unit!(byte_add, check_const_byte_add_unit);
-    gen_const_byte_arith_harness_for_unit!(byte_sub, check_const_byte_sub_unit);
-    gen_const_byte_arith_harness_for_unit!(byte_offset, check_const_byte_offset_unit);
-
-    // generate proof for contracts for byte_add, byte_sub and byte_offset
-    // - `$type`: pointee type
-    // - `$fn_name`: function for which the contract must be verified
-    // - `$proof_name`: name of the harness generated
-    macro_rules! gen_const_byte_arith_harness {
-        ($type:ty, byte_offset, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*const $type>::byte_offset)]
-            pub fn $proof_name() {
-                // generator with space for single element
-                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
-                // generator with space for multiple elements
-                let mut generator2 =
-                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
-
-                let ptr: *const $type = if kani::any() {
-                    generator1.any_in_bounds().ptr
-                } else {
-                    generator2.any_in_bounds().ptr
-                };
-
-                let count: isize = kani::any();
-
-                unsafe {
-                    ptr.byte_offset(count);
-                }
-            }
-        };
-
-        ($type:ty, $fn_name:ident, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*const $type>::$fn_name)]
-            pub fn $proof_name() {
-                // generator with space for single element
-                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
-                // generator with space for multiple elements
-                let mut generator2 =
-                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
-
-                let ptr: *const $type = if kani::any() {
-                    generator1.any_in_bounds().ptr
-                } else {
-                    generator2.any_in_bounds().ptr
-                };
-
-                //byte_add and byte_sub need count to be usize unlike byte_offset
-                let count: usize = kani::any();
-
-                unsafe {
-                    ptr.$fn_name(count);
-                }
-            }
-        };
-    }
-
-    gen_const_byte_arith_harness!(i8, byte_add, check_const_byte_add_i8);
-    gen_const_byte_arith_harness!(i16, byte_add, check_const_byte_add_i16);
-    gen_const_byte_arith_harness!(i32, byte_add, check_const_byte_add_i32);
-    gen_const_byte_arith_harness!(i64, byte_add, check_const_byte_add_i64);
-    gen_const_byte_arith_harness!(i128, byte_add, check_const_byte_add_i128);
-    gen_const_byte_arith_harness!(isize, byte_add, check_const_byte_add_isize);
-    gen_const_byte_arith_harness!(u8, byte_add, check_const_byte_add_u8);
-    gen_const_byte_arith_harness!(u16, byte_add, check_const_byte_add_u16);
-    gen_const_byte_arith_harness!(u32, byte_add, check_const_byte_add_u32);
-    gen_const_byte_arith_harness!(u64, byte_add, check_const_byte_add_u64);
-    gen_const_byte_arith_harness!(u128, byte_add, check_const_byte_add_u128);
-    gen_const_byte_arith_harness!(usize, byte_add, check_const_byte_add_usize);
-    gen_const_byte_arith_harness!((i8, i8), byte_add, check_const_byte_add_tuple_1);
-    gen_const_byte_arith_harness!((f64, bool), byte_add, check_const_byte_add_tuple_2);
-    gen_const_byte_arith_harness!((i32, f64, bool), byte_add, check_const_byte_add_tuple_3);
-    gen_const_byte_arith_harness!(
-        (i8, u16, i32, u64, isize),
-        byte_add,
-        check_const_byte_add_tuple_4
-    );
-
-    gen_const_byte_arith_harness!(i8, byte_sub, check_const_byte_sub_i8);
-    gen_const_byte_arith_harness!(i16, byte_sub, check_const_byte_sub_i16);
-    gen_const_byte_arith_harness!(i32, byte_sub, check_const_byte_sub_i32);
-    gen_const_byte_arith_harness!(i64, byte_sub, check_const_byte_sub_i64);
-    gen_const_byte_arith_harness!(i128, byte_sub, check_const_byte_sub_i128);
-    gen_const_byte_arith_harness!(isize, byte_sub, check_const_byte_sub_isize);
-    gen_const_byte_arith_harness!(u8, byte_sub, check_const_byte_sub_u8);
-    gen_const_byte_arith_harness!(u16, byte_sub, check_const_byte_sub_u16);
-    gen_const_byte_arith_harness!(u32, byte_sub, check_const_byte_sub_u32);
-    gen_const_byte_arith_harness!(u64, byte_sub, check_const_byte_sub_u64);
-    gen_const_byte_arith_harness!(u128, byte_sub, check_const_byte_sub_u128);
-    gen_const_byte_arith_harness!(usize, byte_sub, check_const_byte_sub_usize);
-    gen_const_byte_arith_harness!((i8, i8), byte_sub, check_const_byte_sub_tuple_1);
-    gen_const_byte_arith_harness!((f64, bool), byte_sub, check_const_byte_sub_tuple_2);
-    gen_const_byte_arith_harness!((i32, f64, bool), byte_sub, check_const_byte_sub_tuple_3);
-    gen_const_byte_arith_harness!(
-        (i8, u16, i32, u64, isize),
-        byte_sub,
-        check_const_byte_sub_tuple_4
-    );
-
-    gen_const_byte_arith_harness!(i8, byte_offset, check_const_byte_offset_i8);
-    gen_const_byte_arith_harness!(i16, byte_offset, check_const_byte_offset_i16);
-    gen_const_byte_arith_harness!(i32, byte_offset, check_const_byte_offset_i32);
-    gen_const_byte_arith_harness!(i64, byte_offset, check_const_byte_offset_i64);
-    gen_const_byte_arith_harness!(i128, byte_offset, check_const_byte_offset_i128);
-    gen_const_byte_arith_harness!(isize, byte_offset, check_const_byte_offset_isize);
-    gen_const_byte_arith_harness!(u8, byte_offset, check_const_byte_offset_u8);
-    gen_const_byte_arith_harness!(u16, byte_offset, check_const_byte_offset_u16);
-    gen_const_byte_arith_harness!(u32, byte_offset, check_const_byte_offset_u32);
-    gen_const_byte_arith_harness!(u64, byte_offset, check_const_byte_offset_u64);
-    gen_const_byte_arith_harness!(u128, byte_offset, check_const_byte_offset_u128);
-    gen_const_byte_arith_harness!(usize, byte_offset, check_const_byte_offset_usize);
-    gen_const_byte_arith_harness!((i8, i8), byte_offset, check_const_byte_offset_tuple_1);
-    gen_const_byte_arith_harness!((f64, bool), byte_offset, check_const_byte_offset_tuple_2);
-    gen_const_byte_arith_harness!(
-        (i32, f64, bool),
-        byte_offset,
-        check_const_byte_offset_tuple_3
-    );
-    gen_const_byte_arith_harness!(
-        (i8, u16, i32, u64, isize),
-        byte_offset,
-        check_const_byte_offset_tuple_4
-    );
-
-    macro_rules! gen_const_byte_arith_harness_for_slice {
-        ($type:ty, byte_offset, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*const [$type]>::byte_offset)]
+    macro_rules! gen_const_byte_arith_harness_for_dyn {
+        (byte_offset, $proof_name:ident) => {
+            // Workaround: Directly verifying the method `<*const dyn TestTrait>::byte_offset`
+            // causes a compilation error: "Failed to resolve checking function <*const dyn TestTrait>::byte_offset
+            // because Expected a type, but found trait object paths `dyn TestTrait`".
+            // As a result, the proof is annotated for the underlying struct type instead.
+            #[kani::proof_for_contract(<*const TestStruct>::byte_offset)]
             pub fn $proof_name() {
-                let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
-                let slice: &[$type] = kani::slice::any_slice_of_array(&arr);
-                let ptr: *const [$type] = slice;
+                let test_struct = TestStruct { value: 42 };
+                let trait_object: &dyn TestTrait = &test_struct;
+                let test_ptr: *const dyn TestTrait = trait_object;
 
                 let count: isize = kani::any();
 
                 unsafe {
-                    ptr.byte_offset(count);
+                    test_ptr.byte_offset(count);
                 }
             }
         };
 
-        ($type:ty, $fn_name: ident, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*const [$type]>::$fn_name)]
+        ($fn_name: ident, $proof_name:ident) => {
+            // Workaround: Directly verifying the method `<*const dyn TestTrait>::$fn_name`
+            // causes a compilation error: "Failed to resolve checking function <*const dyn TestTrait>::byte_offset
+            // because Expected a type, but found trait object paths `dyn TestTrait`".
+            // As a result, the proof is annotated for the underlying struct type instead.
+            #[kani::proof_for_contract(<*const TestStruct>::$fn_name)]
             pub fn $proof_name() {
-                let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
-                let slice: &[$type] = kani::slice::any_slice_of_array(&arr);
-                let ptr: *const [$type] = slice;
+                let test_struct = TestStruct { value: 42 };
+                let trait_object: &dyn TestTrait = &test_struct;
+                let test_ptr: *const dyn TestTrait = trait_object;
 
                 //byte_add and byte_sub need count to be usize unlike byte_offset
                 let count: usize = kani::any();
 
                 unsafe {
-                    ptr.$fn_name(count);
+                    test_ptr.$fn_name(count);
                 }
             }
         };
     }
 
-    gen_const_byte_arith_harness_for_slice!(i8, byte_add, check_const_byte_add_i8_slice);
-    gen_const_byte_arith_harness_for_slice!(i16, byte_add, check_const_byte_add_i16_slice);
-    gen_const_byte_arith_harness_for_slice!(i32, byte_add, check_const_byte_add_i32_slice);
-    gen_const_byte_arith_harness_for_slice!(i64, byte_add, check_const_byte_add_i64_slice);
-    gen_const_byte_arith_harness_for_slice!(i128, byte_add, check_const_byte_add_i128_slice);
-    gen_const_byte_arith_harness_for_slice!(isize, byte_add, check_const_byte_add_isize_slice);
-    gen_const_byte_arith_harness_for_slice!(u8, byte_add, check_const_byte_add_u8_slice);
-    gen_const_byte_arith_harness_for_slice!(u16, byte_add, check_const_byte_add_u16_slice);
-    gen_const_byte_arith_harness_for_slice!(u32, byte_add, check_const_byte_add_u32_slice);
-    gen_const_byte_arith_harness_for_slice!(u64, byte_add, check_const_byte_add_u64_slice);
-    gen_const_byte_arith_harness_for_slice!(u128, byte_add, check_const_byte_add_u128_slice);
-    gen_const_byte_arith_harness_for_slice!(usize, byte_add, check_const_byte_add_usize_slice);
-
-    gen_const_byte_arith_harness_for_slice!(i8, byte_sub, check_const_byte_sub_i8_slice);
-    gen_const_byte_arith_harness_for_slice!(i16, byte_sub, check_const_byte_sub_i16_slice);
-    gen_const_byte_arith_harness_for_slice!(i32, byte_sub, check_const_byte_sub_i32_slice);
-    gen_const_byte_arith_harness_for_slice!(i64, byte_sub, check_const_byte_sub_i64_slice);
-    gen_const_byte_arith_harness_for_slice!(i128, byte_sub, check_const_byte_sub_i128_slice);
-    gen_const_byte_arith_harness_for_slice!(isize, byte_sub, check_const_byte_sub_isize_slice);
-    gen_const_byte_arith_harness_for_slice!(u8, byte_sub, check_const_byte_sub_u8_slice);
-    gen_const_byte_arith_harness_for_slice!(u16, byte_sub, check_const_byte_sub_u16_slice);
-    gen_const_byte_arith_harness_for_slice!(u32, byte_sub, check_const_byte_sub_u32_slice);
-    gen_const_byte_arith_harness_for_slice!(u64, byte_sub, check_const_byte_sub_u64_slice);
-    gen_const_byte_arith_harness_for_slice!(u128, byte_sub, check_const_byte_sub_u128_slice);
-    gen_const_byte_arith_harness_for_slice!(usize, byte_sub, check_const_byte_sub_usize_slice);
-
-    gen_const_byte_arith_harness_for_slice!(i8, byte_offset, check_const_byte_offset_i8_slice);
-    gen_const_byte_arith_harness_for_slice!(i16, byte_offset, check_const_byte_offset_i16_slice);
-    gen_const_byte_arith_harness_for_slice!(i32, byte_offset, check_const_byte_offset_i32_slice);
-    gen_const_byte_arith_harness_for_slice!(i64, byte_offset, check_const_byte_offset_i64_slice);
-    gen_const_byte_arith_harness_for_slice!(i128, byte_offset, check_const_byte_offset_i128_slice);
-    gen_const_byte_arith_harness_for_slice!(
-        isize,
-        byte_offset,
-        check_const_byte_offset_isize_slice
-    );
-    gen_const_byte_arith_harness_for_slice!(u8, byte_offset, check_const_byte_offset_u8_slice);
-    gen_const_byte_arith_harness_for_slice!(u16, byte_offset, check_const_byte_offset_u16_slice);
-    gen_const_byte_arith_harness_for_slice!(u32, byte_offset, check_const_byte_offset_u32_slice);
-    gen_const_byte_arith_harness_for_slice!(u64, byte_offset, check_const_byte_offset_u64_slice);
-    gen_const_byte_arith_harness_for_slice!(u128, byte_offset, check_const_byte_offset_u128_slice);
-    gen_const_byte_arith_harness_for_slice!(
-        usize,
-        byte_offset,
-        check_const_byte_offset_usize_slice
-    );
+    gen_const_byte_arith_harness_for_dyn!(byte_add, check_const_byte_add_dyn);
+    gen_const_byte_arith_harness_for_dyn!(byte_sub, check_const_byte_sub_dyn);
+    gen_const_byte_arith_harness_for_dyn!(byte_offset, check_const_byte_offset_dyn);
 }
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 5ae20d7d9db59..df0e10eb0b0dd 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2360,228 +2360,56 @@ pub mod verify {
     use core::mem;
     use kani::PointerGenerator;
 
-    // generate proof for contracts of byte_add, byte_sub and byte_offset to verify
-    // unit pointee type
-    // - `$fn_name`: function for which the contract must be verified
-    // - `$proof_name`: name of the harness generated
-    macro_rules! gen_mut_byte_arith_harness_for_unit {
-        (byte_offset, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*mut ()>::byte_offset)]
-            pub fn $proof_name() {
-                let mut val = ();
-                let ptr: *mut () = &mut val;
-                let count: isize = kani::any();
-                unsafe {
-                    ptr.byte_offset(count);
-                }
-            }
-        };
+    trait TestTrait {}
 
-        ($fn_name:ident, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*mut ()>::$fn_name)]
-            pub fn $proof_name() {
-                let mut val = ();
-                let ptr: *mut () = &mut val;
-                //byte_add and byte_sub need count to be usize unlike byte_offset
-                let count: usize = kani::any();
-                unsafe {
-                    ptr.$fn_name(count);
-                }
-            }
-        };
+    struct TestStruct {
+        value: i64,
     }
 
-    gen_mut_byte_arith_harness_for_unit!(byte_add, check_mut_byte_add_unit);
-    gen_mut_byte_arith_harness_for_unit!(byte_sub, check_mut_byte_sub_unit);
-    gen_mut_byte_arith_harness_for_unit!(byte_offset, check_mut_byte_offset_unit);
-
-    // bounding space for PointerGenerator to accommodate 40 elements.
-    const ARRAY_LEN: usize = 40;
-
-    // generate proof for contracts for byte_add, byte_sub and byte_offset
-    // - `$type`: pointee type
-    // - `$fn_name`: function for which the contract must be verified
-    // - `$proof_name`: name of the harness generated
-    macro_rules! gen_mut_byte_arith_harness {
-        ($type:ty, byte_offset, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*mut $type>::byte_offset)]
-            pub fn $proof_name() {
-                // generator with space for single element
-                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
-                // generator with space for multiple elements
-                let mut generator2 =
-                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
-
-                let ptr: *mut $type = if kani::any() {
-                    generator1.any_in_bounds().ptr
-                } else {
-                    generator2.any_in_bounds().ptr
-                };
-                let count: isize = kani::any();
+    impl TestTrait for TestStruct {}
 
-                unsafe {
-                    ptr.byte_offset(count);
-                }
-            }
-        };
-
-        ($type:ty, $fn_name:ident, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*mut $type>::$fn_name)]
-            pub fn $proof_name() {
-                // generator with space for single element
-                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
-                // generator with space for multiple elements
-                let mut generator2 =
-                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
-
-                let ptr: *mut $type = if kani::any() {
-                    generator1.any_in_bounds().ptr
-                } else {
-                    generator2.any_in_bounds().ptr
-                };
-
-                //byte_add and byte_sub need count to be usize unlike byte_offset
-                let count: usize = kani::any();
-
-                unsafe {
-                    ptr.$fn_name(count);
-                }
-            }
-        };
-    }
-
-    gen_mut_byte_arith_harness!(i8, byte_add, check_mut_byte_add_i8);
-    gen_mut_byte_arith_harness!(i16, byte_add, check_mut_byte_add_i16);
-    gen_mut_byte_arith_harness!(i32, byte_add, check_mut_byte_add_i32);
-    gen_mut_byte_arith_harness!(i64, byte_add, check_mut_byte_add_i64);
-    gen_mut_byte_arith_harness!(i128, byte_add, check_mut_byte_add_i128);
-    gen_mut_byte_arith_harness!(isize, byte_add, check_mut_byte_add_isize);
-    gen_mut_byte_arith_harness!(u8, byte_add, check_mut_byte_add_u8);
-    gen_mut_byte_arith_harness!(u16, byte_add, check_mut_byte_add_u16);
-    gen_mut_byte_arith_harness!(u32, byte_add, check_mut_byte_add_u32);
-    gen_mut_byte_arith_harness!(u64, byte_add, check_mut_byte_add_u64);
-    gen_mut_byte_arith_harness!(u128, byte_add, check_mut_byte_add_u128);
-    gen_mut_byte_arith_harness!(usize, byte_add, check_mut_byte_add_usize);
-    gen_mut_byte_arith_harness!((i8, i8), byte_add, check_mut_byte_add_tuple_1);
-    gen_mut_byte_arith_harness!((f64, bool), byte_add, check_mut_byte_add_tuple_2);
-    gen_mut_byte_arith_harness!((i32, f64, bool), byte_add, check_mut_byte_add_tuple_3);
-    gen_mut_byte_arith_harness!(
-        (i8, u16, i32, u64, isize),
-        byte_add,
-        check_mut_byte_add_tuple_4
-    );
-
-    gen_mut_byte_arith_harness!(i8, byte_sub, check_mut_byte_sub_i8);
-    gen_mut_byte_arith_harness!(i16, byte_sub, check_mut_byte_sub_i16);
-    gen_mut_byte_arith_harness!(i32, byte_sub, check_mut_byte_sub_i32);
-    gen_mut_byte_arith_harness!(i64, byte_sub, check_mut_byte_sub_i64);
-    gen_mut_byte_arith_harness!(i128, byte_sub, check_mut_byte_sub_i128);
-    gen_mut_byte_arith_harness!(isize, byte_sub, check_mut_byte_sub_isize);
-    gen_mut_byte_arith_harness!(u8, byte_sub, check_mut_byte_sub_u8);
-    gen_mut_byte_arith_harness!(u16, byte_sub, check_mut_byte_sub_u16);
-    gen_mut_byte_arith_harness!(u32, byte_sub, check_mut_byte_sub_u32);
-    gen_mut_byte_arith_harness!(u64, byte_sub, check_mut_byte_sub_u64);
-    gen_mut_byte_arith_harness!(u128, byte_sub, check_mut_byte_sub_u128);
-    gen_mut_byte_arith_harness!(usize, byte_sub, check_mut_byte_sub_usize);
-    gen_mut_byte_arith_harness!((i8, i8), byte_sub, check_mut_byte_sub_tuple_1);
-    gen_mut_byte_arith_harness!((f64, bool), byte_sub, check_mut_byte_sub_tuple_2);
-    gen_mut_byte_arith_harness!((i32, f64, bool), byte_sub, check_mut_byte_sub_tuple_3);
-    gen_mut_byte_arith_harness!(
-        (i8, u16, i32, u64, isize),
-        byte_sub,
-        check_mut_byte_sub_tuple_4
-    );
-
-    gen_mut_byte_arith_harness!(i8, byte_offset, check_mut_byte_offset_i8);
-    gen_mut_byte_arith_harness!(i16, byte_offset, check_mut_byte_offset_i16);
-    gen_mut_byte_arith_harness!(i32, byte_offset, check_mut_byte_offset_i32);
-    gen_mut_byte_arith_harness!(i64, byte_offset, check_mut_byte_offset_i64);
-    gen_mut_byte_arith_harness!(i128, byte_offset, check_mut_byte_offset_i128);
-    gen_mut_byte_arith_harness!(isize, byte_offset, check_mut_byte_offset_isize);
-    gen_mut_byte_arith_harness!(u8, byte_offset, check_mut_byte_offset_u8);
-    gen_mut_byte_arith_harness!(u16, byte_offset, check_mut_byte_offset_u16);
-    gen_mut_byte_arith_harness!(u32, byte_offset, check_mut_byte_offset_u32);
-    gen_mut_byte_arith_harness!(u64, byte_offset, check_mut_byte_offset_u64);
-    gen_mut_byte_arith_harness!(u128, byte_offset, check_mut_byte_offset_u128);
-    gen_mut_byte_arith_harness!(usize, byte_offset, check_mut_byte_offset_usize);
-    gen_mut_byte_arith_harness!((i8, i8), byte_offset, check_mut_byte_offset_tuple_1);
-    gen_mut_byte_arith_harness!((f64, bool), byte_offset, check_mut_byte_offset_tuple_2);
-    gen_mut_byte_arith_harness!((i32, f64, bool), byte_offset, check_mut_byte_offset_tuple_3);
-    gen_mut_byte_arith_harness!(
-        (i8, u16, i32, u64, isize),
-        byte_offset,
-        check_mut_byte_offset_tuple_4
-    );
-
-    macro_rules! gen_mut_byte_arith_harness_for_slice {
-        ($type:ty, byte_offset, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*mut [$type]>::byte_offset)]
+    macro_rules! gen_mut_byte_arith_harness_for_dyn {
+        (byte_offset, $proof_name:ident) => {
+            // Workaround: Directly verifying the method `<*mut dyn TestTrait>::byte_offset`
+            // causes a compilation error: "Failed to resolve checking function <*mut dyn TestTrait>::byte_offset
+            // because Expected a type, but found trait object paths `dyn TestTrait`".
+            // As a result, the proof is annotated for the underlying struct type instead.
+            #[kani::proof_for_contract(<*mut TestStruct>::byte_offset)]
             pub fn $proof_name() {
-                let mut arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
-                let slice: &mut [$type] = kani::slice::any_slice_of_array_mut(&mut arr);
-                let ptr: *mut [$type] = slice;
+                let mut test_struct = TestStruct { value: 42 };
+                let trait_object: &mut dyn TestTrait = &mut test_struct;
+                let test_ptr: *mut dyn TestTrait = trait_object;
 
                 let count: isize = kani::any();
 
                 unsafe {
-                    ptr.byte_offset(count);
+                    test_ptr.byte_offset(count);
                 }
             }
         };
 
-        ($type:ty, $fn_name: ident, $proof_name:ident) => {
-            #[kani::proof_for_contract(<*mut [$type]>::$fn_name)]
+        ($fn_name: ident, $proof_name:ident) => {
+            // Workaround: Directly verifying the method `<*mut dyn TestTrait>::$fn_name`
+            // causes a compilation error: "Failed to resolve checking function <*mut dyn TestTrait>::byte_offset
+            // because Expected a type, but found trait object paths `dyn TestTrait`".
+            // As a result, the proof is annotated for the underlying struct type instead.
+            #[kani::proof_for_contract(<*mut TestStruct>::$fn_name)]
             pub fn $proof_name() {
-                let mut arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
-                let slice: &mut [$type] = kani::slice::any_slice_of_array_mut(&mut arr);
-                let ptr: *mut [$type] = slice;
+                let mut test_struct = TestStruct { value: 42 };
+                let trait_object: &mut dyn TestTrait = &mut test_struct;
+                let test_ptr: *mut dyn TestTrait = trait_object;
 
                 //byte_add and byte_sub need count to be usize unlike byte_offset
                 let count: usize = kani::any();
 
                 unsafe {
-                    ptr.$fn_name(count);
+                    test_ptr.$fn_name(count);
                 }
             }
         };
     }
 
-    gen_mut_byte_arith_harness_for_slice!(i8, byte_add, check_mut_byte_add_i8_slice);
-    gen_mut_byte_arith_harness_for_slice!(i16, byte_add, check_mut_byte_add_i16_slice);
-    gen_mut_byte_arith_harness_for_slice!(i32, byte_add, check_mut_byte_add_i32_slice);
-    gen_mut_byte_arith_harness_for_slice!(i64, byte_add, check_mut_byte_add_i64_slice);
-    gen_mut_byte_arith_harness_for_slice!(i128, byte_add, check_mut_byte_add_i128_slice);
-    gen_mut_byte_arith_harness_for_slice!(isize, byte_add, check_mut_byte_add_isize_slice);
-    gen_mut_byte_arith_harness_for_slice!(u8, byte_add, check_mut_byte_add_u8_slice);
-    gen_mut_byte_arith_harness_for_slice!(u16, byte_add, check_mut_byte_add_u16_slice);
-    gen_mut_byte_arith_harness_for_slice!(u32, byte_add, check_mut_byte_add_u32_slice);
-    gen_mut_byte_arith_harness_for_slice!(u64, byte_add, check_mut_byte_add_u64_slice);
-    gen_mut_byte_arith_harness_for_slice!(u128, byte_add, check_mut_byte_add_u128_slice);
-    gen_mut_byte_arith_harness_for_slice!(usize, byte_add, check_mut_byte_add_usize_slice);
-
-    gen_mut_byte_arith_harness_for_slice!(i8, byte_sub, check_mut_byte_sub_i8_slice);
-    gen_mut_byte_arith_harness_for_slice!(i16, byte_sub, check_mut_byte_sub_i16_slice);
-    gen_mut_byte_arith_harness_for_slice!(i32, byte_sub, check_mut_byte_sub_i32_slice);
-    gen_mut_byte_arith_harness_for_slice!(i64, byte_sub, check_mut_byte_sub_i64_slice);
-    gen_mut_byte_arith_harness_for_slice!(i128, byte_sub, check_mut_byte_sub_i128_slice);
-    gen_mut_byte_arith_harness_for_slice!(isize, byte_sub, check_mut_byte_sub_isize_slice);
-    gen_mut_byte_arith_harness_for_slice!(u8, byte_sub, check_mut_byte_sub_u8_slice);
-    gen_mut_byte_arith_harness_for_slice!(u16, byte_sub, check_mut_byte_sub_u16_slice);
-    gen_mut_byte_arith_harness_for_slice!(u32, byte_sub, check_mut_byte_sub_u32_slice);
-    gen_mut_byte_arith_harness_for_slice!(u64, byte_sub, check_mut_byte_sub_u64_slice);
-    gen_mut_byte_arith_harness_for_slice!(u128, byte_sub, check_mut_byte_sub_u128_slice);
-    gen_mut_byte_arith_harness_for_slice!(usize, byte_sub, check_mut_byte_sub_usize_slice);
-
-    gen_mut_byte_arith_harness_for_slice!(i8, byte_offset, check_mut_byte_offset_i8_slice);
-    gen_mut_byte_arith_harness_for_slice!(i16, byte_offset, check_mut_byte_offset_i16_slice);
-    gen_mut_byte_arith_harness_for_slice!(i32, byte_offset, check_mut_byte_offset_i32_slice);
-    gen_mut_byte_arith_harness_for_slice!(i64, byte_offset, check_mut_byte_offset_i64_slice);
-    gen_mut_byte_arith_harness_for_slice!(i128, byte_offset, check_mut_byte_offset_i128_slice);
-    gen_mut_byte_arith_harness_for_slice!(isize, byte_offset, check_mut_byte_offset_isize_slice);
-    gen_mut_byte_arith_harness_for_slice!(u8, byte_offset, check_mut_byte_offset_u8_slice);
-    gen_mut_byte_arith_harness_for_slice!(u16, byte_offset, check_mut_byte_offset_u16_slice);
-    gen_mut_byte_arith_harness_for_slice!(u32, byte_offset, check_mut_byte_offset_u32_slice);
-    gen_mut_byte_arith_harness_for_slice!(u64, byte_offset, check_mut_byte_offset_u64_slice);
-    gen_mut_byte_arith_harness_for_slice!(u128, byte_offset, check_mut_byte_offset_u128_slice);
-    gen_mut_byte_arith_harness_for_slice!(usize, byte_offset, check_mut_byte_offset_usize_slice);
+    gen_mut_byte_arith_harness_for_dyn!(byte_add, check_mut_byte_add_dyn);
+    gen_mut_byte_arith_harness_for_dyn!(byte_sub, check_mut_byte_sub_dyn);
+    gen_mut_byte_arith_harness_for_dyn!(byte_offset, check_mut_byte_offset_dyn);
 }

From c98d8391acd9b3cb4b58d9ea677530e1447b83bf Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 27 Nov 2024 00:05:38 -0800
Subject: [PATCH 12/21] Reverted unnecessary changes to minimize conflict.

---
 library/core/src/ptr/const_ptr.rs | 138 ++++++++++++++++++++++++++++++
 1 file changed, 138 insertions(+)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index dc49aa77d72bf..4baf7ae332e70 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -1967,6 +1967,144 @@ pub 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);
+        }
+    }
+
+    // Array size bound for kani::any_array
+    const ARRAY_LEN: usize = 40;
+
+    macro_rules! generate_offset_from_harness {
+        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
+            // Proof for a single element
+            #[kani::proof_for_contract(<*const $type>::offset_from)]
+            pub fn $proof_name1() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<gen_size>::new();
+                let mut generator2 = PointerGenerator::<gen_size>::new();
+                let ptr1: *const $type = generator1.any_in_bounds().ptr;
+                let ptr2: *const $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.offset_from(ptr2);
+                }
+            }
+
+            // Proof for large arrays
+            #[kani::proof_for_contract(<*const $type>::offset_from)]
+            pub fn $proof_name2() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *const $type = generator1.any_in_bounds().ptr;
+                let ptr2: *const $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    generate_offset_from_harness!(
+        u8,
+        check_const_offset_from_u8,
+        check_const_offset_from_u8_arr
+    );
+    generate_offset_from_harness!(
+        u16,
+        check_const_offset_from_u16,
+        check_const_offset_from_u16_arr
+    );
+    generate_offset_from_harness!(
+        u32,
+        check_const_offset_from_u32,
+        check_const_offset_from_u32_arr
+    );
+    generate_offset_from_harness!(
+        u64,
+        check_const_offset_from_u64,
+        check_const_offset_from_u64_arr
+    );
+    generate_offset_from_harness!(
+        u128,
+        check_const_offset_from_u128,
+        check_const_offset_from_u128_arr
+    );
+    generate_offset_from_harness!(
+        usize,
+        check_const_offset_from_usize,
+        check_const_offset_from_usize_arr
+    );
+
+    generate_offset_from_harness!(
+        i8,
+        check_const_offset_from_i8,
+        check_const_offset_from_i8_arr
+    );
+    generate_offset_from_harness!(
+        i16,
+        check_const_offset_from_i16,
+        check_const_offset_from_i16_arr
+    );
+    generate_offset_from_harness!(
+        i32,
+        check_const_offset_from_i32,
+        check_const_offset_from_i32_arr
+    );
+    generate_offset_from_harness!(
+        i64,
+        check_const_offset_from_i64,
+        check_const_offset_from_i64_arr
+    );
+    generate_offset_from_harness!(
+        i128,
+        check_const_offset_from_i128,
+        check_const_offset_from_i128_arr
+    );
+    generate_offset_from_harness!(
+        isize,
+        check_const_offset_from_isize,
+        check_const_offset_from_isize_arr
+    );
+
+    generate_offset_from_harness!(
+        (i8, i8),
+        check_const_offset_from_tuple_1,
+        check_const_offset_from_tuple_1_arr
+    );
+    generate_offset_from_harness!(
+        (f64, bool),
+        check_const_offset_from_tuple_2,
+        check_const_offset_from_tuple_2_arr
+    );
+    generate_offset_from_harness!(
+        (u32, i16, f32),
+        check_const_offset_from_tuple_3,
+        check_const_offset_from_tuple_3_arr
+    );
+    generate_offset_from_harness!(
+        ((), bool, u8, u16, i32, f64, i128, usize),
+        check_const_offset_from_tuple_4,
+        check_const_offset_from_tuple_4_arr
+    );
+
     trait TestTrait {}
 
     struct TestStruct {

From 1dab4e3a0fecce6ee2c9b567190d576eadb3f9e3 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 27 Nov 2024 16:37:46 -0800
Subject: [PATCH 13/21] Formatted code using rustfmt

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

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 29742350f4f27..3ba96d889acab 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -9,7 +9,6 @@ use safety::{ensures, requires};
 use crate::kani;
 use core::mem;
 
-
 impl<T: ?Sized> *mut T {
     /// Returns `true` if the pointer is null.
     ///
@@ -2535,7 +2534,7 @@ pub mod verify {
     }
 
     impl TestTrait for TestStruct {}
-    
+
     /// This macro generates proofs for contracts on `byte_add`, `byte_sub`, and `byte_offset`
     /// operations for pointers to dyn Trait.
     /// - `$fn_name`: Specifies the arithmetic operation to verify.
@@ -2579,9 +2578,9 @@ pub mod verify {
             }
         };
     }
-    
-    // fn <*mut T>::add(), <*mut T>::sub() and <*mut T>::offset() dyn Trait verification 
+
+    // fn <*mut T>::add(), <*mut T>::sub() and <*mut T>::offset() dyn Trait verification
     gen_mut_byte_arith_harness_for_dyn!(byte_add, check_mut_byte_add_dyn);
     gen_mut_byte_arith_harness_for_dyn!(byte_sub, check_mut_byte_sub_dyn);
     gen_mut_byte_arith_harness_for_dyn!(byte_offset, check_mut_byte_offset_dyn);
-}
\ No newline at end of file
+}

From df6d4ede9d42ef7cde66ab8d5e18e47b144651d9 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Wed, 4 Dec 2024 15:38:51 -0800
Subject: [PATCH 14/21] Manually updated changes from verify/ptr_mut_byte.

---
 library/core/src/ptr/const_ptr.rs | 35 ++++++++++++++-----------------
 library/core/src/ptr/mut_ptr.rs   |  2 +-
 2 files changed, 17 insertions(+), 20 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index f6a718ee7601f..d5ba92d7416b9 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -481,14 +481,13 @@ impl<T: ?Sized> *const T {
         // Else if count is not zero, then ensure that adding `count` doesn't cause 
         // overflow and that both pointers `self` and the result are in the same 
         // allocation 
-        (mem::size_of_val_raw(self) != 0 &&
-            (self.addr() as isize).checked_add(count).is_some() &&
+        ((self.addr() as isize).checked_add(count).is_some() &&
             kani::mem::same_allocation(self, self.wrapping_byte_offset(count)))
     )]
-    #[ensures(|result|
+    #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        (self.addr() == (*result).addr()) ||
-        (kani::mem::same_allocation(self, *result))
+        (self.addr() == result.addr()) ||
+        (kani::mem::same_allocation(self, result))
     )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
@@ -1030,18 +1029,17 @@ impl<T: ?Sized> *const T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         // If count is zero, any pointer is valid including null pointer.
-        (count == 0) || 
+        (count == 0) ||
         // Else if count is not zero, then ensure that adding `count` doesn't cause 
         // overflow and that both pointers `self` and the result are in the same 
         // allocation 
-        (mem::size_of_val_raw(self) != 0 &&
-            (self.addr() as isize).checked_add(count as isize).is_some() && 
+        ((self.addr() as isize).checked_add(count as isize).is_some() &&
             kani::mem::same_allocation(self, self.wrapping_byte_add(count)))
     )]
-    #[ensures(|result|
+    #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        (self.addr() == (*result).addr()) ||
-        (kani::mem::same_allocation(self, *result))
+        (self.addr() == result.addr()) ||
+        (kani::mem::same_allocation(self, result))
     )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
@@ -1175,18 +1173,17 @@ impl<T: ?Sized> *const T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         // If count is zero, any pointer is valid including null pointer.
-        (count == 0) || 
+        (count == 0) ||
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
-        (mem::size_of_val_raw(self) != 0 &&
-            (self.addr() as isize).checked_sub(count as isize).is_some() && 
+        ((self.addr() as isize).checked_sub(count as isize).is_some() &&
             kani::mem::same_allocation(self, self.wrapping_byte_sub(count)))
     )]
-    #[ensures(|result|
+    #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
-        (self.addr() == (*result).addr()) ||
-        (kani::mem::same_allocation(self, *result))
+        (self.addr() == result.addr()) ||
+        (kani::mem::same_allocation(self, result))
     )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.
@@ -1816,7 +1813,7 @@ impl<T: ?Sized> PartialOrd for *const T {
 
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
-pub mod verify {
+mod verify {
     use crate::kani;
     use core::mem;
     use kani::PointerGenerator;
@@ -2114,7 +2111,7 @@ pub mod verify {
         check_const_offset_slice_tuple_4
     );
 
-    // Array size bound for kani::any_array for `offset_from` verification
+    // bounding space for PointerGenerator to accommodate 40 elements.
     const ARRAY_LEN: usize = 40;
 
     macro_rules! generate_offset_from_harness {
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 33b93f0450766..75dd130a6265e 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2221,7 +2221,7 @@ impl<T: ?Sized> PartialOrd for *mut T {
 
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
-pub mod verify {
+mod verify {
     use crate::kani;
     use core::mem;
     use kani::PointerGenerator;

From 633df86fe7e6b15c7894f93f07d1a79c8c4dadbd Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Thu, 5 Dec 2024 15:38:22 -0800
Subject: [PATCH 15/21] Updated tracking issues; Updated magic number comments;
 Replaced kani::mem with core::ub_checks

---
 library/core/src/ptr/const_ptr.rs | 28 +++++++++++++-----------
 library/core/src/ptr/mut_ptr.rs   | 36 +++++++++++++++----------------
 2 files changed, 33 insertions(+), 31 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index d5ba92d7416b9..d9cb2f2766e0e 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -482,12 +482,12 @@ impl<T: ?Sized> *const T {
         // overflow and that both pointers `self` and the result are in the same 
         // allocation 
         ((self.addr() as isize).checked_add(count).is_some() &&
-            kani::mem::same_allocation(self, self.wrapping_byte_offset(count)))
+            core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
@@ -1034,12 +1034,12 @@ impl<T: ?Sized> *const T {
         // overflow and that both pointers `self` and the result are in the same 
         // allocation 
         ((self.addr() as isize).checked_add(count as isize).is_some() &&
-            kani::mem::same_allocation(self, self.wrapping_byte_add(count)))
+            core::ub_checks::same_allocation(self, self.wrapping_byte_add(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
@@ -1178,12 +1178,12 @@ impl<T: ?Sized> *const T {
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
         ((self.addr() as isize).checked_sub(count as isize).is_some() &&
-            kani::mem::same_allocation(self, self.wrapping_byte_sub(count)))
+            core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count)))
     )]
     #[ensures(|&result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == result.addr()) ||
-        (kani::mem::same_allocation(self, result))
+        (core::ub_checks::same_allocation(self, result))
     )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.
@@ -2111,7 +2111,9 @@ mod verify {
         check_const_offset_slice_tuple_4
     );
 
-    // bounding space for PointerGenerator to accommodate 40 elements.
+    // The array's length is set to an arbitrary value, which defines its size.
+    // In this case, implementing a dynamic array is not possible, because 
+    // PointerGenerator does not support dynamic sized arrays.
     const ARRAY_LEN: usize = 40;
 
     macro_rules! generate_offset_from_harness {
@@ -2260,10 +2262,10 @@ mod verify {
 
     macro_rules! gen_const_byte_arith_harness_for_dyn {
         (byte_offset, $proof_name:ident) => {
+            // tracking issue: https://github.com/model-checking/kani/issues/3763
             // Workaround: Directly verifying the method `<*const dyn TestTrait>::byte_offset`
-            // causes a compilation error: "Failed to resolve checking function <*const dyn TestTrait>::byte_offset
-            // because Expected a type, but found trait object paths `dyn TestTrait`".
-            // As a result, the proof is annotated for the underlying struct type instead.
+            // causes a compilation error. As a workaround, the proof is annotated with the
+            // underlying struct type instead.
             #[kani::proof_for_contract(<*const TestStruct>::byte_offset)]
             pub fn $proof_name() {
                 let test_struct = TestStruct { value: 42 };
@@ -2279,10 +2281,10 @@ mod verify {
         };
 
         ($fn_name: ident, $proof_name:ident) => {
+            //tracking issue: https://github.com/model-checking/kani/issues/3763
             // Workaround: Directly verifying the method `<*const dyn TestTrait>::$fn_name`
-            // causes a compilation error: "Failed to resolve checking function <*const dyn TestTrait>::byte_offset
-            // because Expected a type, but found trait object paths `dyn TestTrait`".
-            // As a result, the proof is annotated for the underlying struct type instead.
+            // causes a compilation error. As a workaround, the proof is annotated with the
+            // underlying struct type instead.
             #[kani::proof_for_contract(<*const TestStruct>::$fn_name)]
             pub fn $proof_name() {
                 let test_struct = TestStruct { value: 42 };
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 75dd130a6265e..c196674841216 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -414,12 +414,12 @@ impl<T: ?Sized> *mut T {
         // 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))))
+        ((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) || kani::mem::same_allocation(self as *const T, *result as *const T))]
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *mut T
     where
         T: Sized,
@@ -483,12 +483,12 @@ impl<T: ?Sized> *mut T {
         // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
             (self.addr() as isize).checked_add(count).is_some() && 
-            kani::mem::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T))
+            core::ub_checks::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == (*result).addr()) ||
-        (kani::mem::same_allocation(self as *const T, *result as *const T))
+        (core::ub_checks::same_allocation(self as *const T, *result as *const T))
     )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
@@ -1043,12 +1043,12 @@ impl<T: ?Sized> *mut T {
         // 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))))
+        ((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) || kani::mem::same_allocation(self as *const T, *result as *const T))]
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1109,12 +1109,12 @@ impl<T: ?Sized> *mut T {
         // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
             (self.addr() as isize).checked_add(count as isize).is_some() && 
-            kani::mem::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T))
+            core::ub_checks::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == (*result).addr()) ||
-        (kani::mem::same_allocation(self as *const T, *result as *const T))
+        (core::ub_checks::same_allocation(self as *const T, *result as *const T))
     )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
@@ -1184,12 +1184,12 @@ impl<T: ?Sized> *mut T {
         // 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))))
+        ((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) || kani::mem::same_allocation(self as *const T, *result as *const T))]
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -1256,12 +1256,12 @@ impl<T: ?Sized> *mut T {
         // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
             (self.addr() as isize).checked_sub(count as isize).is_some() && 
-            kani::mem::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T))
+            core::ub_checks::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T))
     )]
     #[ensures(|result|
         // The resulting pointer should either be unchanged or still point to the same allocation
         (self.addr() == (*result).addr()) ||
-        (kani::mem::same_allocation(self as *const T, *result as *const T))
+        (core::ub_checks::same_allocation(self as *const T, *result as *const T))
     )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.
@@ -2380,10 +2380,10 @@ mod verify {
     /// - `$proof_name`: Specifies the name of the generated proof for contract.
     macro_rules! gen_mut_byte_arith_harness_for_dyn {
         (byte_offset, $proof_name:ident) => {
+            //tracking issue: https://github.com/model-checking/kani/issues/3763
             // Workaround: Directly verifying the method `<*mut dyn TestTrait>::byte_offset`
-            // causes a compilation error: "Failed to resolve checking function <*mut dyn TestTrait>::byte_offset
-            // because Expected a type, but found trait object paths `dyn TestTrait`".
-            // As a result, the proof is annotated for the underlying struct type instead.
+            // causes a compilation error. As a workaround, the proof is annotated with the
+            // underlying struct type instead.
             #[kani::proof_for_contract(<*mut TestStruct>::byte_offset)]
             pub fn $proof_name() {
                 let mut test_struct = TestStruct { value: 42 };
@@ -2398,10 +2398,10 @@ mod verify {
             }
         };
         ($fn_name: ident, $proof_name:ident) => {
+            //tracking issue: https://github.com/model-checking/kani/issues/3763
             // Workaround: Directly verifying the method `<*mut dyn TestTrait>::$fn_name`
-            // causes a compilation error: "Failed to resolve checking function <*mut dyn TestTrait>::byte_offset
-            // because Expected a type, but found trait object paths `dyn TestTrait`".
-            // As a result, the proof is annotated for the underlying struct type instead.
+            // causes a compilation error. As a workaround, the proof is annotated with the
+            // underlying struct type instead.
             #[kani::proof_for_contract(<*mut TestStruct>::$fn_name)]
             pub fn $proof_name() {
                 let mut test_struct = TestStruct { value: 42 };

From 5069cf33d91a32830369ab35959ce6f32cac0929 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Thu, 5 Dec 2024 15:56:05 -0800
Subject: [PATCH 16/21] Formatted code using rustfmt.

---
 library/core/src/ptr/const_ptr.rs |  2 +-
 library/core/src/ptr/mut_ptr.rs   | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index d9cb2f2766e0e..8ba26780c4fa6 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -2112,7 +2112,7 @@ mod verify {
     );
 
     // The array's length is set to an arbitrary value, which defines its size.
-    // In this case, implementing a dynamic array is not possible, because 
+    // In this case, implementing a dynamic array is not possible, because
     // PointerGenerator does not support dynamic sized arrays.
     const ARRAY_LEN: usize = 40;
 
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index c196674841216..18dd10b8850bc 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -477,12 +477,12 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         // If count is zero, any pointer is valid including null pointer.
-        (count == 0) || 
+        (count == 0) ||
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self.addr() as isize).checked_add(count).is_some() && 
+            (self.addr() as isize).checked_add(count).is_some() &&
             core::ub_checks::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T))
     )]
     #[ensures(|result|
@@ -1103,12 +1103,12 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         // If count is zero, any pointer is valid including null pointer.
-        (count == 0) || 
+        (count == 0) ||
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self.addr() as isize).checked_add(count as isize).is_some() && 
+            (self.addr() as isize).checked_add(count as isize).is_some() &&
             core::ub_checks::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T))
     )]
     #[ensures(|result|
@@ -1250,12 +1250,12 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[requires(
         // If count is zero, any pointer is valid including null pointer.
-        (count == 0) || 
+        (count == 0) ||
         // Else if count is not zero, then ensure that subtracting `count` doesn't 
         // cause overflow and that both pointers `self` and the result are in the 
         // same allocation 
         (mem::size_of_val_raw(self) != 0 &&
-            (self.addr() as isize).checked_sub(count as isize).is_some() && 
+            (self.addr() as isize).checked_sub(count as isize).is_some() &&
             core::ub_checks::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T))
     )]
     #[ensures(|result|

From d5ab23f2b63dd770f8ff8804522029c5aace24d8 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Thu, 5 Dec 2024 16:49:26 -0800
Subject: [PATCH 17/21] Rearranged proof for contracts.

---
 library/core/src/ptr/const_ptr.rs |   5 +-
 library/core/src/ptr/mut_ptr.rs   | 205 ++++++++++++++++++------------
 2 files changed, 130 insertions(+), 80 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index cae99c035c949..fbec6be6abe5a 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -2508,7 +2508,7 @@ mod verify {
         byte_offset,
         check_const_byte_offset_usize_slice
     );
-    
+
     trait TestTrait {}
 
     struct TestStruct {
@@ -2516,7 +2516,7 @@ mod verify {
     }
 
     impl TestTrait for TestStruct {}
-    
+
     // generate `dyn Trait` proof for contracts for byte_add, byte_sub and byte_offset.
     // - `$fn_name`: function for which the contract must be verified
     // - `$proof_name`: name of the harness generated
@@ -2533,6 +2533,7 @@ mod verify {
                 let test_ptr: *const dyn TestTrait = trait_object;
 
                 let count: isize = kani::any();
+
                 unsafe {
                     test_ptr.byte_offset(count);
                 }
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index b383e2c8e8a97..d66a93b2d1078 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2375,10 +2375,136 @@ mod verify {
     );
 
     // The array's length is set to an arbitrary value, which defines its size.
-    // In this case, implementing a dynamic array is not possible, because 
+    // In this case, implementing a dynamic array is not possible, because
     // PointerGenerator does not support dynamic sized arrays.
     const ARRAY_LEN: usize = 40;
 
+    macro_rules! generate_offset_from_harness {
+        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
+            #[kani::proof_for_contract(<*mut $type>::offset_from)]
+            // Below function is for a single element
+            pub fn $proof_name1() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<gen_size>::new();
+                let mut generator2 = PointerGenerator::<gen_size>::new();
+                let ptr1: *mut $type = generator1.any_in_bounds().ptr;
+                let ptr2: *mut $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.offset_from(ptr2);
+                }
+            }
+
+            // Below function is for large arrays
+            pub fn $proof_name2() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *mut $type = generator1.any_in_bounds().ptr;
+                let ptr2: *mut $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    // The proof for a unit type panics as offset_from needs the pointee size > 0
+    #[kani::proof_for_contract(<*mut ()>::offset_from)]
+    #[kani::should_panic]
+    pub fn check_mut_offset_from_unit() {
+        let mut val: () = ();
+        let src_ptr: *mut () = &mut val;
+        let dest_ptr: *mut () = &mut val;
+        unsafe {
+            dest_ptr.offset_from(src_ptr);
+        }
+    }
+
+    generate_offset_from_harness!(u8, check_mut_offset_from_u8, check_mut_offset_from_u8_array);
+    generate_offset_from_harness!(
+        u16,
+        check_mut_offset_from_u16,
+        check_mut_offset_from_u16_array
+    );
+    generate_offset_from_harness!(
+        u32,
+        check_mut_offset_from_u32,
+        check_mut_offset_from_u32_array
+    );
+    generate_offset_from_harness!(
+        u64,
+        check_mut_offset_from_u64,
+        check_mut_offset_from_u64_array
+    );
+    generate_offset_from_harness!(
+        u128,
+        check_mut_offset_from_u128,
+        check_mut_offset_from_u128_array
+    );
+    generate_offset_from_harness!(
+        usize,
+        check_mut_offset_from_usize,
+        check_mut_offset_from_usize_array
+    );
+
+    generate_offset_from_harness!(i8, check_mut_offset_from_i8, check_mut_offset_from_i8_array);
+    generate_offset_from_harness!(
+        i16,
+        check_mut_offset_from_i16,
+        check_mut_offset_from_i16_array
+    );
+    generate_offset_from_harness!(
+        i32,
+        check_mut_offset_from_i32,
+        check_mut_offset_from_i32_array
+    );
+    generate_offset_from_harness!(
+        i64,
+        check_mut_offset_from_i64,
+        check_mut_offset_from_i64_array
+    );
+    generate_offset_from_harness!(
+        i128,
+        check_mut_offset_from_i128,
+        check_mut_offset_from_i128_array
+    );
+    generate_offset_from_harness!(
+        isize,
+        check_mut_offset_from_isize,
+        check_mut_offset_from_isize_array
+    );
+
+    generate_offset_from_harness!(
+        (i8, i8),
+        check_mut_offset_from_tuple_1,
+        check_mut_offset_from_tuple_1_array
+    );
+    generate_offset_from_harness!(
+        (f64, bool),
+        check_mut_offset_from_tuple_2,
+        check_mut_offset_from_tuple_2_array
+    );
+    generate_offset_from_harness!(
+        (u32, i16, f32),
+        check_mut_offset_from_tuple_3,
+        check_mut_offset_from_tuple_3_array
+    );
+    generate_offset_from_harness!(
+        ((), bool, u8, u16, i32, f64, i128, usize),
+        check_mut_offset_from_tuple_4,
+        check_mut_offset_from_tuple_4_array
+    );
+
     #[kani::proof_for_contract(<*mut ()>::byte_offset)]
     #[kani::should_panic]
     pub fn check_mut_byte_offset_unit_invalid_count() {
@@ -2665,7 +2791,6 @@ mod verify {
                 let trait_object: &mut dyn TestTrait = &mut test_struct;
                 let test_ptr: *mut dyn TestTrait = trait_object;
 
-
                 //byte_add and byte_sub need count to be usize unlike byte_offset
                 let count: usize = kani::any();
 
@@ -2680,80 +2805,4 @@ mod verify {
     gen_mut_byte_arith_harness_for_dyn!(byte_add, check_mut_byte_add_dyn);
     gen_mut_byte_arith_harness_for_dyn!(byte_sub, check_mut_byte_sub_dyn);
     gen_mut_byte_arith_harness_for_dyn!(byte_offset, check_mut_byte_offset_dyn);
-
-    // The proof for a unit type panics as offset_from needs the pointee size > 0
-    #[kani::proof_for_contract(<*mut ()>::offset_from)]
-    #[kani::should_panic]
-    pub fn check_mut_offset_from_unit() {
-        let mut val: () = ();
-        let src_ptr: *mut () = &mut val;
-        let dest_ptr: *mut () = &mut val;
-        unsafe {
-            dest_ptr.offset_from(src_ptr);
-        }
-    }
-
-    macro_rules! generate_offset_from_harness {
-        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
-            #[kani::proof_for_contract(<*mut $type>::offset_from)]
-            // Below function is for a single element
-            pub fn $proof_name1() {
-                const gen_size: usize = mem::size_of::<$type>();
-                let mut generator1 = PointerGenerator::<gen_size>::new();
-                let mut generator2 = PointerGenerator::<gen_size>::new();
-                let ptr1: *mut $type = generator1.any_in_bounds().ptr;
-                let ptr2: *mut $type = if kani::any() {
-                    generator1.any_alloc_status().ptr
-                } else {
-                    generator2.any_alloc_status().ptr
-                };
-                
-                unsafe {
-                    ptr1.offset_from(ptr2);
-                }
-            }
-
-            // Below function is for large arrays
-            pub fn $proof_name2() {
-                const gen_size: usize = mem::size_of::<$type>();
-                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
-                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
-                let ptr1: *mut $type = generator1.any_in_bounds().ptr;
-                let ptr2: *mut $type = if kani::any() {
-                    generator1.any_alloc_status().ptr
-                } else {
-                    generator2.any_alloc_status().ptr
-                };
-                
-                unsafe {
-                    ptr1.offset_from(ptr2);
-                }
-            }
-
-        };
-    }
-
-    generate_offset_from_harness!(u8, check_mut_offset_from_u8, check_mut_offset_from_u8_array);
-    generate_offset_from_harness!(u16, check_mut_offset_from_u16, check_mut_offset_from_u16_array);
-    generate_offset_from_harness!(u32, check_mut_offset_from_u32, check_mut_offset_from_u32_array);
-    generate_offset_from_harness!(u64, check_mut_offset_from_u64, check_mut_offset_from_u64_array);
-    generate_offset_from_harness!(u128, check_mut_offset_from_u128, check_mut_offset_from_u128_array);
-    generate_offset_from_harness!(usize, check_mut_offset_from_usize, check_mut_offset_from_usize_array);
-
-    generate_offset_from_harness!(i8, check_mut_offset_from_i8, check_mut_offset_from_i8_array);
-    generate_offset_from_harness!(i16, check_mut_offset_from_i16, check_mut_offset_from_i16_array);
-    generate_offset_from_harness!(i32, check_mut_offset_from_i32, check_mut_offset_from_i32_array);
-    generate_offset_from_harness!(i64, check_mut_offset_from_i64, check_mut_offset_from_i64_array);
-    generate_offset_from_harness!(i128, check_mut_offset_from_i128, check_mut_offset_from_i128_array);
-    generate_offset_from_harness!(isize, check_mut_offset_from_isize, check_mut_offset_from_isize_array);
-
-    generate_offset_from_harness!((i8, i8), check_mut_offset_from_tuple_1, check_mut_offset_from_tuple_1_array);
-    generate_offset_from_harness!((f64, bool), check_mut_offset_from_tuple_2, check_mut_offset_from_tuple_2_array);
-    generate_offset_from_harness!((u32, i16, f32), check_mut_offset_from_tuple_3, check_mut_offset_from_tuple_3_array);
-    generate_offset_from_harness!(
-        ((), bool, u8, u16, i32, f64, i128, usize),
-        check_mut_offset_from_tuple_4,
-        check_mut_offset_from_tuple_4_array
-    );
-
 }

From f81a0094d53fa1352e8198a44b57c6aae33c972f Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Thu, 5 Dec 2024 16:55:59 -0800
Subject: [PATCH 18/21] Improved comments for dyn Trait related code.

---
 library/core/src/ptr/const_ptr.rs | 2 ++
 library/core/src/ptr/mut_ptr.rs   | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index fbec6be6abe5a..30806b17cef73 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -2509,8 +2509,10 @@ mod verify {
         check_const_byte_offset_usize_slice
     );
 
+    // Trait used exclusively for implementing proofs for contracts for `dyn Trait` type.
     trait TestTrait {}
 
+    // Struct used exclusively for implementing proofs for contracts for `dyn Trait` type.
     struct TestStruct {
         value: i64,
     }
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index d66a93b2d1078..1808c09243789 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2749,8 +2749,10 @@ mod verify {
     gen_mut_byte_arith_harness_for_slice!(u128, byte_offset, check_mut_byte_offset_u128_slice);
     gen_mut_byte_arith_harness_for_slice!(usize, byte_offset, check_mut_byte_offset_usize_slice);
 
+    // Trait used exclusively for implementing proofs for contracts for `dyn Trait` type.
     trait TestTrait {}
 
+    // Struct used exclusively for implementing proofs for contracts for `dyn Trait` type.
     struct TestStruct {
         value: i64,
     }

From 7b61c2f0c53b562e5f1ac70a82bd036d39658cb0 Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Mon, 9 Dec 2024 09:45:54 -0800
Subject: [PATCH 19/21] Fixed compilation error after merge.

---
 library/core/src/ptr/mut_ptr.rs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 6a32d09d8cd87..eba48201b6f03 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2528,8 +2528,7 @@ mod verify {
 
     #[kani::proof_for_contract(<*mut ()>::byte_offset)]
     pub fn check_mut_byte_offset_cast_unit() {
-        let mut generator = PointerGenerator::<
-      >::new();
+        let mut generator = PointerGenerator::<ARRAY_LEN>::new();
         let ptr: *mut u8 = generator.any_in_bounds().ptr;
         let ptr1: *mut () = ptr as *mut ();
         let count: isize = kani::any();

From b03ba84270941f241c88698c5fe03ac53a95b59d Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Mon, 9 Dec 2024 09:50:54 -0800
Subject: [PATCH 20/21] Rearranged Proofs in const_ptr.rs; Formatted code using
 rustfmt.

---
 library/core/src/ptr/const_ptr.rs | 367 +++++++++++++++---------------
 library/core/src/ptr/mut_ptr.rs   |  12 +-
 2 files changed, 192 insertions(+), 187 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 6d49b9338864e..8d2d8f9c74b93 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -2134,7 +2134,10 @@ mod verify {
         let self_ptr: *const u32 = unsafe { origin_ptr.byte_offset(offset as isize) };
         let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) };
         assert_eq!(result, offset as isize);
-        assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize));
+        assert_eq!(
+            result,
+            (self_ptr.addr() as isize - origin_ptr.addr() as isize)
+        );
     }
 
     macro_rules! generate_offset_from_harness {
@@ -2273,186 +2276,6 @@ mod verify {
         check_const_offset_from_tuple_4_arr
     );
 
-    // Proof for contact of byte_offset_from to verify unit type
-    #[kani::proof_for_contract(<*const ()>::byte_offset_from)]
-    pub fn check_const_byte_offset_from_unit() {
-        let val: () = ();
-        let src_ptr: *const () = &val;
-        let dest_ptr: *const () = &val;
-        unsafe {
-            dest_ptr.byte_offset_from(src_ptr);
-        }
-    }
-
-    // generate proofs for contracts for byte_offset_from to verify int and composite
-    // types
-    // - `$type`: pointee type
-    // - `$proof_name1`: name of the harness for single element
-    // - `$proof_name2`: name of the harness for array of elements
-    macro_rules! generate_const_byte_offset_from_harness {
-        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
-            // Proof for a single element
-            #[kani::proof_for_contract(<*const $type>::byte_offset_from)]
-            pub fn $proof_name1() {
-                const gen_size: usize = mem::size_of::<$type>();
-                let mut generator1 = PointerGenerator::<gen_size>::new();
-                let mut generator2 = PointerGenerator::<gen_size>::new();
-                let ptr1: *const $type = generator1.any_in_bounds().ptr;
-                let ptr2: *const $type = if kani::any() {
-                    generator1.any_alloc_status().ptr
-                } else {
-                    generator2.any_alloc_status().ptr
-                };
-
-                unsafe {
-                    ptr1.byte_offset_from(ptr2);
-                }
-            }
-
-            // Proof for large arrays
-            #[kani::proof_for_contract(<*const $type>::byte_offset_from)]
-            pub fn $proof_name2() {
-                const gen_size: usize = mem::size_of::<$type>();
-                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
-                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
-                let ptr1: *const $type = generator1.any_in_bounds().ptr;
-                let ptr2: *const $type = if kani::any() {
-                    generator1.any_alloc_status().ptr
-                } else {
-                    generator2.any_alloc_status().ptr
-                };
-
-                unsafe {
-                    ptr1.byte_offset_from(ptr2);
-                }
-            }
-        };
-    }
-
-    generate_const_byte_offset_from_harness!(
-        u8,
-        check_const_byte_offset_from_u8,
-        check_const_byte_offset_from_u8_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        u16,
-        check_const_byte_offset_from_u16,
-        check_const_byte_offset_from_u16_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        u32,
-        check_const_byte_offset_from_u32,
-        check_const_byte_offset_from_u32_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        u64,
-        check_const_byte_offset_from_u64,
-        check_const_byte_offset_from_u64_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        u128,
-        check_const_byte_offset_from_u128,
-        check_const_byte_offset_from_u128_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        usize,
-        check_const_byte_offset_from_usize,
-        check_const_byte_offset_from_usize_arr
-    );
-
-    generate_const_byte_offset_from_harness!(
-        i8,
-        check_const_byte_offset_from_i8,
-        check_const_byte_offset_from_i8_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        i16,
-        check_const_byte_offset_from_i16,
-        check_const_byte_offset_from_i16_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        i32,
-        check_const_byte_offset_from_i32,
-        check_const_byte_offset_from_i32_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        i64,
-        check_const_byte_offset_from_i64,
-        check_const_byte_offset_from_i64_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        i128,
-        check_const_byte_offset_from_i128,
-        check_const_byte_offset_from_i128_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        isize,
-        check_const_byte_offset_from_isize,
-        check_const_byte_offset_from_isize_arr
-    );
-
-    generate_const_byte_offset_from_harness!(
-        (i8, i8),
-        check_const_byte_offset_from_tuple_1,
-        check_const_byte_offset_from_tuple_1_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        (f64, bool),
-        check_const_byte_offset_from_tuple_2,
-        check_const_byte_offset_from_tuple_2_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        (u32, i16, f32),
-        check_const_byte_offset_from_tuple_3,
-        check_const_byte_offset_from_tuple_3_arr
-    );
-    generate_const_byte_offset_from_harness!(
-        ((), bool, u8, u16, i32, f64, i128, usize),
-        check_const_byte_offset_from_tuple_4,
-        check_const_byte_offset_from_tuple_4_arr
-    );
-
-    // length of the slice generated from PointerGenerator
-    const SLICE_LEN: usize = 10;
-
-    // generate proofs for contracts for byte_offset_from to verify slices
-    // - `$type`: type of the underlyign element within the slice pointer
-    // - `$proof_name`: name of the harness
-    macro_rules! generate_const_byte_offset_from_slice_harness {
-        ($type: ty, $proof_name: ident) => {
-            #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)]
-            pub fn $proof_name() {
-                const gen_size: usize = mem::size_of::<$type>();
-                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
-                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
-                let ptr1: *const [$type] =
-                    generator1.any_in_bounds().ptr as *const [$type; SLICE_LEN];
-                let ptr2: *const [$type] = if kani::any() {
-                    generator1.any_alloc_status().ptr as *const [$type; SLICE_LEN]
-                } else {
-                    generator2.any_alloc_status().ptr as *const [$type; SLICE_LEN]
-                };
-
-                unsafe {
-                    ptr1.byte_offset_from(ptr2);
-                }
-            }
-        };
-    }
-
-    generate_const_byte_offset_from_slice_harness!(u8, check_const_byte_offset_from_u8_slice);
-    generate_const_byte_offset_from_slice_harness!(u16, check_const_byte_offset_from_u16_slice);
-    generate_const_byte_offset_from_slice_harness!(u32, check_const_byte_offset_from_u32_slice);
-    generate_const_byte_offset_from_slice_harness!(u64, check_const_byte_offset_from_u64_slice);
-    generate_const_byte_offset_from_slice_harness!(u128, check_const_byte_offset_from_u128_slice);
-    generate_const_byte_offset_from_slice_harness!(usize, check_const_byte_offset_from_usize_slice);
-    generate_const_byte_offset_from_slice_harness!(i8, check_const_byte_offset_from_i8_slice);
-    generate_const_byte_offset_from_slice_harness!(i16, check_const_byte_offset_from_i16_slice);
-    generate_const_byte_offset_from_slice_harness!(i32, check_const_byte_offset_from_i32_slice);
-    generate_const_byte_offset_from_slice_harness!(i64, check_const_byte_offset_from_i64_slice);
-    generate_const_byte_offset_from_slice_harness!(i128, check_const_byte_offset_from_i128_slice);
-    generate_const_byte_offset_from_slice_harness!(isize, check_const_byte_offset_from_isize_slice);
-
     #[kani::proof_for_contract(<*const ()>::byte_offset)]
     #[kani::should_panic]
     pub fn check_const_byte_offset_unit_invalid_count() {
@@ -2744,7 +2567,7 @@ mod verify {
         };
 
         ($fn_name: ident, $proof_name:ident) => {
-            //tracking issue: https://github.com/model-checking/kani/issues/3763
+            // tracking issue: https://github.com/model-checking/kani/issues/3763
             // Workaround: Directly verifying the method `<*const dyn TestTrait>::$fn_name`
             // causes a compilation error. As a workaround, the proof is annotated with the
             // underlying struct type instead.
@@ -2767,4 +2590,184 @@ mod verify {
     gen_const_byte_arith_harness_for_dyn!(byte_add, check_const_byte_add_dyn);
     gen_const_byte_arith_harness_for_dyn!(byte_sub, check_const_byte_sub_dyn);
     gen_const_byte_arith_harness_for_dyn!(byte_offset, check_const_byte_offset_dyn);
+
+    // Proof for contact of byte_offset_from to verify unit type
+    #[kani::proof_for_contract(<*const ()>::byte_offset_from)]
+    pub fn check_const_byte_offset_from_unit() {
+        let val: () = ();
+        let src_ptr: *const () = &val;
+        let dest_ptr: *const () = &val;
+        unsafe {
+            dest_ptr.byte_offset_from(src_ptr);
+        }
+    }
+
+    // generate proofs for contracts for byte_offset_from to verify int and composite
+    // types
+    // - `$type`: pointee type
+    // - `$proof_name1`: name of the harness for single element
+    // - `$proof_name2`: name of the harness for array of elements
+    macro_rules! generate_const_byte_offset_from_harness {
+        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
+            // Proof for a single element
+            #[kani::proof_for_contract(<*const $type>::byte_offset_from)]
+            pub fn $proof_name1() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<gen_size>::new();
+                let mut generator2 = PointerGenerator::<gen_size>::new();
+                let ptr1: *const $type = generator1.any_in_bounds().ptr;
+                let ptr2: *const $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+
+            // Proof for large arrays
+            #[kani::proof_for_contract(<*const $type>::byte_offset_from)]
+            pub fn $proof_name2() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *const $type = generator1.any_in_bounds().ptr;
+                let ptr2: *const $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    generate_const_byte_offset_from_harness!(
+        u8,
+        check_const_byte_offset_from_u8,
+        check_const_byte_offset_from_u8_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        u16,
+        check_const_byte_offset_from_u16,
+        check_const_byte_offset_from_u16_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        u32,
+        check_const_byte_offset_from_u32,
+        check_const_byte_offset_from_u32_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        u64,
+        check_const_byte_offset_from_u64,
+        check_const_byte_offset_from_u64_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        u128,
+        check_const_byte_offset_from_u128,
+        check_const_byte_offset_from_u128_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        usize,
+        check_const_byte_offset_from_usize,
+        check_const_byte_offset_from_usize_arr
+    );
+
+    generate_const_byte_offset_from_harness!(
+        i8,
+        check_const_byte_offset_from_i8,
+        check_const_byte_offset_from_i8_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        i16,
+        check_const_byte_offset_from_i16,
+        check_const_byte_offset_from_i16_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        i32,
+        check_const_byte_offset_from_i32,
+        check_const_byte_offset_from_i32_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        i64,
+        check_const_byte_offset_from_i64,
+        check_const_byte_offset_from_i64_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        i128,
+        check_const_byte_offset_from_i128,
+        check_const_byte_offset_from_i128_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        isize,
+        check_const_byte_offset_from_isize,
+        check_const_byte_offset_from_isize_arr
+    );
+
+    generate_const_byte_offset_from_harness!(
+        (i8, i8),
+        check_const_byte_offset_from_tuple_1,
+        check_const_byte_offset_from_tuple_1_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        (f64, bool),
+        check_const_byte_offset_from_tuple_2,
+        check_const_byte_offset_from_tuple_2_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        (u32, i16, f32),
+        check_const_byte_offset_from_tuple_3,
+        check_const_byte_offset_from_tuple_3_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        ((), bool, u8, u16, i32, f64, i128, usize),
+        check_const_byte_offset_from_tuple_4,
+        check_const_byte_offset_from_tuple_4_arr
+    );
+
+    // length of the slice generated from PointerGenerator
+    const SLICE_LEN: usize = 10;
+
+    // generate proofs for contracts for byte_offset_from to verify slices
+    // - `$type`: type of the underlyign element within the slice pointer
+    // - `$proof_name`: name of the harness
+    macro_rules! generate_const_byte_offset_from_slice_harness {
+        ($type: ty, $proof_name: ident) => {
+            #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)]
+            pub fn $proof_name() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *const [$type] =
+                    generator1.any_in_bounds().ptr as *const [$type; SLICE_LEN];
+                let ptr2: *const [$type] = if kani::any() {
+                    generator1.any_alloc_status().ptr as *const [$type; SLICE_LEN]
+                } else {
+                    generator2.any_alloc_status().ptr as *const [$type; SLICE_LEN]
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    generate_const_byte_offset_from_slice_harness!(u8, check_const_byte_offset_from_u8_slice);
+    generate_const_byte_offset_from_slice_harness!(u16, check_const_byte_offset_from_u16_slice);
+    generate_const_byte_offset_from_slice_harness!(u32, check_const_byte_offset_from_u32_slice);
+    generate_const_byte_offset_from_slice_harness!(u64, check_const_byte_offset_from_u64_slice);
+    generate_const_byte_offset_from_slice_harness!(u128, check_const_byte_offset_from_u128_slice);
+    generate_const_byte_offset_from_slice_harness!(usize, check_const_byte_offset_from_usize_slice);
+    generate_const_byte_offset_from_slice_harness!(i8, check_const_byte_offset_from_i8_slice);
+    generate_const_byte_offset_from_slice_harness!(i16, check_const_byte_offset_from_i16_slice);
+    generate_const_byte_offset_from_slice_harness!(i32, check_const_byte_offset_from_i32_slice);
+    generate_const_byte_offset_from_slice_harness!(i64, check_const_byte_offset_from_i64_slice);
+    generate_const_byte_offset_from_slice_harness!(i128, check_const_byte_offset_from_i128_slice);
+    generate_const_byte_offset_from_slice_harness!(isize, check_const_byte_offset_from_isize_slice);
 }
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index eba48201b6f03..5f606a51c9151 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2817,8 +2817,7 @@ mod verify {
     gen_mut_byte_arith_harness_for_dyn!(byte_add, check_mut_byte_add_dyn);
     gen_mut_byte_arith_harness_for_dyn!(byte_sub, check_mut_byte_sub_dyn);
     gen_mut_byte_arith_harness_for_dyn!(byte_offset, check_mut_byte_offset_dyn);
-  
-    
+
     #[kani::proof]
     pub fn check_mut_byte_offset_from_fixed_offset() {
         let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array();
@@ -2827,7 +2826,10 @@ mod verify {
         let self_ptr: *mut u32 = unsafe { origin_ptr.byte_offset(offset as isize) };
         let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) };
         assert_eq!(result, offset as isize);
-        assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize));
+        assert_eq!(
+            result,
+            (self_ptr.addr() as isize - origin_ptr.addr() as isize)
+        );
     }
 
     // Proof for unit size
@@ -2970,8 +2972,8 @@ mod verify {
     );
 
     // The length of a slice is set to an arbitrary value, which defines its size.
-    // In this case, implementing a slice with a dynamic size set using kani::any() 
-    // is not possible, because PointerGenerator does not support non-deterministic 
+    // In this case, implementing a slice with a dynamic size set using kani::any()
+    // is not possible, because PointerGenerator does not support non-deterministic
     // slice pointers.
     const SLICE_LEN: usize = 10;
 

From 72c922b87e1aa75e5b0edd606564a5fa54d21fba Mon Sep 17 00:00:00 2001
From: Yifei Wang <1277495324@qq.com>
Date: Mon, 9 Dec 2024 09:55:49 -0800
Subject: [PATCH 21/21] Improved comments.

---
 library/core/src/ptr/const_ptr.rs | 12 ++++++------
 library/core/src/ptr/mut_ptr.rs   | 10 +++++-----
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 8d2d8f9c74b93..5f818f90904bf 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -2609,7 +2609,7 @@ mod verify {
     // - `$proof_name2`: name of the harness for array of elements
     macro_rules! generate_const_byte_offset_from_harness {
         ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
-            // Proof for a single element
+            // Proof for pointers to a single element
             #[kani::proof_for_contract(<*const $type>::byte_offset_from)]
             pub fn $proof_name1() {
                 const gen_size: usize = mem::size_of::<$type>();
@@ -2627,7 +2627,7 @@ mod verify {
                 }
             }
 
-            // Proof for large arrays
+            // Proof for pointers to large arrays
             #[kani::proof_for_contract(<*const $type>::byte_offset_from)]
             pub fn $proof_name2() {
                 const gen_size: usize = mem::size_of::<$type>();
@@ -2730,12 +2730,12 @@ mod verify {
         check_const_byte_offset_from_tuple_4_arr
     );
 
-    // length of the slice generated from PointerGenerator
+    // Length of the slice generated from PointerGenerator.
     const SLICE_LEN: usize = 10;
 
-    // generate proofs for contracts for byte_offset_from to verify slices
-    // - `$type`: type of the underlyign element within the slice pointer
-    // - `$proof_name`: name of the harness
+    // Generate proofs for contracts for byte_offset_from to verify slice pointee types.
+    // - `$type`: type of the underlyign element within the slice pointer.
+    // - `$proof_name`: name of the harness.
     macro_rules! generate_const_byte_offset_from_slice_harness {
         ($type: ty, $proof_name: ident) => {
             #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)]
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 5f606a51c9151..af749191f5949 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2843,8 +2843,8 @@ mod verify {
         }
     }
 
-    // Generate proofs for contracts for byte_offset_from to verify int and composite
-    // types.
+    // Generate proofs for contracts for byte_offset_from to verify pointer to int
+    // and composite types.
     // - `$type`: pointee type.
     // - `$proof_name1`: name of the harness for single element.
     // - `$proof_name2`: name of the harness for array of elements.
@@ -2977,9 +2977,9 @@ mod verify {
     // slice pointers.
     const SLICE_LEN: usize = 10;
 
-    // generate proofs for contracts for byte_offset_from to verify slices
-    // - `$type`: type of the underlyign element within the slice pointer
-    // - `$proof_name`: name of the harness
+    // Generate proofs for contracts for byte_offset_from to verify pointers to slices
+    // - `$type`: type of the underlyign element within the slice pointer.
+    // - `$proof_name`: name of the harness.
     macro_rules! generate_mut_byte_offset_from_slice_harness {
         ($type: ty, $proof_name: ident) => {
             #[kani::proof_for_contract(<*mut [$type]>::byte_offset_from)]