dyn Trait proof for contracts of byte_offset_from

library/core/src/ptr/const_ptr.rs

@@ -2536,7 +2536,8 @@ mod verify {
     // 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 used exclusively for implementing proof for contracts for `dyn Trait` type.
+    #[cfg_attr(kani, derive(kani::Arbitrary))]
     struct TestStruct {
         value: i64,
     }
@@ -2770,4 +2771,30 @@ mod verify {
     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);
+
+    // tracking issue: https://github.com/model-checking/kani/issues/3763
+    // Workaround: Directly verifying the method `<*const dyn TestTrait>::byte_offset_from`
+    // 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_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 generator_caller = PointerGenerator::<gen_size>::new();
+        let mut generator_input = PointerGenerator::<gen_size>::new();
+        let ptr_caller: *const TestStruct = generator_caller.any_in_bounds().ptr;
+        let ptr_input: *const TestStruct = if kani::any() {
+            generator_caller.any_alloc_status().ptr
+        } else {
+            generator_input.any_alloc_status().ptr
+        };
+
+        let ptr_caller = ptr_caller as *const dyn TestTrait;
+        let ptr_input = ptr_input as *const dyn TestTrait;
+
+        unsafe {
+            ptr_caller.byte_offset_from(ptr_input);
+        }
+    }
 }

library/core/src/ptr/mut_ptr.rs

@@ -2763,6 +2763,7 @@ mod verify {
     trait TestTrait {}
 
     // Struct used exclusively for implementing proofs for contracts for `dyn Trait` type.
+    #[cfg_attr(kani, derive(kani::Arbitrary))]
     struct TestStruct {
         value: i64,
     }
@@ -2775,7 +2776,7 @@ 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
+            // tracking issue: https://github.com/model-checking/kani/issues/3763
             // Workaround: Directly verifying the method `<*mut dyn TestTrait>::byte_offset`
             // causes a compilation error. As a workaround, the proof is annotated with the
             // underlying struct type instead.
@@ -2793,7 +2794,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 `<*mut dyn TestTrait>::$fn_name`
             // causes a compilation error. As a workaround, the proof is annotated with the
             // underlying struct type instead.
@@ -3013,4 +3014,30 @@ mod verify {
     generate_mut_byte_offset_from_slice_harness!(i64, check_mut_byte_offset_from_i64_slice);
     generate_mut_byte_offset_from_slice_harness!(i128, check_mut_byte_offset_from_i128_slice);
     generate_mut_byte_offset_from_slice_harness!(isize, check_mut_byte_offset_from_isize_slice);
+
+    // tracking issue: https://github.com/model-checking/kani/issues/3763
+    // Workaround: Directly verifying the method `<*mut dyn TestTrait>::byte_offset_from`
+    // 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_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 generator_caller = PointerGenerator::<gen_size>::new();
+        let mut generator_input = PointerGenerator::<gen_size>::new();
+        let ptr_caller: *mut TestStruct = generator_caller.any_in_bounds().ptr;
+        let ptr_input: *mut TestStruct = if kani::any() {
+            generator_caller.any_alloc_status().ptr
+        } else {
+            generator_input.any_alloc_status().ptr
+        };
+
+        let ptr_caller = ptr_caller as *mut dyn TestTrait;
+        let ptr_input = ptr_input as *mut dyn TestTrait;
+
+        unsafe {
+            ptr_caller.byte_offset_from(ptr_input);
+        }
+    }
 }