// 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);
        }
    }