Memory predicates won't work if function with contract is compiled as a dependency

[celinval]

Let's say you have a crate crate_a that defines a copy_val function that is annotated with contracts:

///----- Crate with contract
#[requires(kani::mem::can_dereference(ptr))]
pub unsafe fn copy_val<T: Copy>(ptr: *const T) -> T {
}

Now we have a crate crate_b that uses crate_a that we want to verify using Kani:

pub fn safe_copy<T: Copy>(x: &T) -> T {
    unsafe { copy_val(x) }
}

using the following command line invocation:

cargo kani --only-codegen

with Kani version: 0.56.0

I expected to see this happen: Compilation should succeed.

Instead, this happened: Kani will fail to compile crate_a due to missing trait bounds.

[celinval]

Actually, I can trigger the same issue with a normal harness:

extern crate kani;

#[derive(Clone, Copy, kani::Arbitrary)]
struct Wrapper<T: ?Sized> {
    _size: usize,
    _value: T,
}

mod verify {
    use super::*;
    use kani::mem::can_dereference;
    #[kani::proof]
    #[kani::should_panic]
    pub fn check_invalid_dyn_ptr() {
        let raw_ptr: *const Wrapper<dyn PartialEq<u8>> =
            unsafe { new_dead_ptr::<Wrapper<u8>>(kani::any()) };
        assert!(can_dereference(raw_ptr));
    }

    unsafe fn new_dead_ptr<T>(val: T) -> *const T {
        let local = val;
        &local as *const _
    }
}

Running Kani will fail compilation:

error[E0277]: the trait bound `std::ptr::DynMetadata<dyn std::cmp::PartialEq<u8>>: kani::mem::PtrProperties<Wrapper<dyn std::cmp::PartialEq<u8>>>` is not satisfied
  --> adt_with_metadata.rs:35:33
   |
35 |         assert!(can_dereference(raw_ptr));
   |                 --------------- ^^^^^^^ the trait `kani::mem::PtrProperties<Wrapper<dyn std::cmp::PartialEq<u8>>>` is not implemented for `std::ptr::DynMetadata<dyn std::cmp::PartialEq<u8>>`
   |                 |
   |                 required by a bound introduced by this call
   |
   = help: the trait `kani::mem::PtrProperties<dyn std::cmp::PartialEq<u8>>` is implemented for `std::ptr::DynMetadata<dyn std::cmp::PartialEq<u8>>`
   = help: for that trait implementation, expected `dyn std::cmp::PartialEq<u8>`, found `Wrapper<dyn std::cmp::PartialEq<u8>>`
note: required by a bound in `kani::mem::can_dereference`