dyn Trait proof for contracts of byte_offset_from

library/core/src/ptr/const_ptr.rs

@@ -2709,4 +2709,39 @@ mod verify {
         byte_offset,
         check_const_byte_offset_usize_slice
     );
+
+    trait TestTrait {}
+
+    #[cfg_attr(kani, derive(kani::Arbitrary))]
+    struct TestStruct {
+        value: i64,
+    }
+
+    impl TestTrait for TestStruct {}
+
+    // Workaround: Directly verifying `<*const dyn TestTrait>::byte_offset_from`
+    // causes a compilation error: "Failed to resolve checking function <*const dyn TestTrait>::byte_offset_from
+    // 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_from)]
+    pub fn check_const_byte_offset_from_dyn() {
+        const gen_size: usize = mem::size_of::<TestStruct>();
+        // Since the pointer generator cannot directly create pointers to `dyn Trait`,
+        // we first generate a pointer to the underlying struct and then cast it to a `dyn Trait` pointer.
+        let mut generator1 = PointerGenerator::<gen_size>::new();
+        let mut generator2 = PointerGenerator::<gen_size>::new();
+        let ptr1: *const TestStruct = generator1.any_in_bounds().ptr;
+        let ptr2: *const TestStruct = if kani::any() {
+            generator1.any_alloc_status().ptr
+        } else {
+            generator2.any_alloc_status().ptr
+        };
+
+        let ptr1 = ptr1 as *const dyn TestTrait;
+        let ptr2 = ptr2 as *const dyn TestTrait;
+
+        unsafe {
+            ptr1.byte_offset_from(ptr2);
+        }
+    } 
 }

library/core/src/ptr/mut_ptr.rs

@@ -2761,4 +2761,39 @@ mod verify {
         check_mut_offset_from_tuple_4_array
     );
 
+    trait TestTrait {}
+
+    #[cfg_attr(kani, derive(kani::Arbitrary))]
+    struct TestStruct {
+        value: i64,
+    }
+
+    impl TestTrait for TestStruct {}
+
+    // Workaround: Directly verifying `<*mut dyn TestTrait>::byte_offset_from`
+    // causes a compilation error: "Failed to resolve checking function <*mut dyn TestTrait>::byte_offset_from
+    // 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_from)]
+    pub fn check_mut_byte_offset_from_dyn() {
+        const gen_size: usize = mem::size_of::<TestStruct>();
+        // Since the pointer generator cannot directly create pointers to `dyn Trait`,
+        // we first generate a pointer to the underlying struct and then cast it to a `dyn Trait` pointer.
+        let mut generator1 = PointerGenerator::<gen_size>::new();
+        let mut generator2 = PointerGenerator::<gen_size>::new();
+        let ptr1: *mut TestStruct = generator1.any_in_bounds().ptr;
+        let ptr2: *mut TestStruct = if kani::any() {
+            generator1.any_alloc_status().ptr
+        } else {
+            generator2.any_alloc_status().ptr
+        };
+
+        let ptr1 = ptr1 as *mut dyn TestTrait;
+        let ptr2 = ptr2 as *mut dyn TestTrait;
+
+        unsafe {
+            ptr1.byte_offset_from(ptr2);
+        }
+    }
+
 }