Can not use same_allocation in API with ?Size generic type

[danielhumanmod]

Hi team,
I am trying to use the same_allocation API to verify whether two pointers refer to the same object allocation. However, for the API under the implementation impl<T: ?Sized> NonNull<T>, it seems this API is not permitted. Below is the relevant code snippet:

// Function Contracts (under the implementation of impl<T: ?Sized> NonNull<T>) 
    #[must_use]
    #[inline(always)]
    #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
    #[rustc_allow_const_fn_unstable(set_ptr_value)]
    #[stable(feature = "non_null_convenience", since = "1.80.0")]
    #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
    #[requires(kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_offset(count)))]
    #[ensures(
        |result: &NonNull<T>|
        (result.as_ptr() as *const () as usize) == ((self.as_ptr() as *const () as usize) + count)
    )]
    pub const unsafe fn byte_add(self, count: usize) -> Self {
        // SAFETY: the caller must uphold the safety contract for `add` and `byte_add` has the same
        // safety contract.
        // Additionally safety contract of `add` guarantees that the resulting pointer is pointing
        // to an allocation, there can't be an allocation at null, thus it's safe to construct
        // `NonNull`.
        unsafe { NonNull { pointer: self.pointer.byte_add(count) } }
    }

// Proof Harness
    #[kani::proof_for_contract(NonNull::byte_add)]
    pub fn non_null_byte_add_proof() {
        const ARR_SIZE: usize = 100000;
        let arr: [i32; ARR_SIZE] = kani::any();
        let offset = kani::any_where(|x| *x <= ARR_SIZE);
        let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32;
        let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() };
        let count: usize = kani::any();

        kani::assume(count < usize::MAX);
        kani::assume(count.checked_mul(mem::size_of::<i32>()).is_some());
        kani::assume(count * mem::size_of::<i32>() <= (isize::MAX as usize));
        // kani::assume(count < ARR_SIZE - offset);

        unsafe {
            let result = ptr.byte_add(count);
        }
    }

Given the current design of the API, could we continue using our previous workaround by adding the necessary precondition directly in the proof harness? Specifically, we previously added the following assumption:
kani::assume(count < ARR_SIZE - offset)

Please let me know if this approach is acceptable or if there are other alternatives you would suggest.
cc @zhassan-aws

[celinval]

That's a good point. We should change that API to include unsized pointers. Can you please create an issue in Kani for that. Thanks

[danielhumanmod]

Thanks for your response, Celina. Sure I will create an issue on Kani

[celinval]

Btw, I made a comment in the issue you created. As a work around, you can cast the pointer to a thin pointer using ptr as *const () (or use pointer::to_raw_parts), and use that pointer instead.