Kani not resolving qualified paths in verify-std

[dawidl022]

I was attempting to write harnesses for trait method implementations in verify-rust-std, but I could not get Kani to resolve the qualified path of the function.

I tried this code (in library/core/src/slice/index.rs):

#[cfg(kani)]
mod verify {
    use super::*;
    use crate::kani;

    #[kani::proof_for_contract(<usize as SliceIndex<[T]>>::get_unchecked)]
    pub fn check_get_unchecked() {}
}

with this contract inside unsafe impl<T> SliceIndex<[T]> for usize:

    #[inline]
    #[safety::requires(self < slice.len())]
    unsafe fn get_unchecked(self, slice: *const [T]) -> *const T {
        // ...

using the following command line invocation:

./scripts/run-kani.sh --path . --kani-args --harness core::slice::verify::check_get_unchecked

with Kani version: 0.61.0

I expected to see this happen: function name would be resolved.

Instead, this happened:

error: Failed to resolve checking function <usize as SliceIndex<[T]>>::get_unchecked because Kani currently cannot resolve qualified paths
    --> /Users/dawidl022/Development/verify-rust-std/library/core/src/slice/index.rs:1071:5
     |
1071 |     #[kani::proof_for_contract(<usize as SliceIndex<[T]>>::get_unchecked)]
     |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     |
     = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)

error: Failed to resolve `<usize as SliceIndex<[T]>>::get_unchecked` for `proof_for_contract`: Kani currently cannot resolve qualified paths
    --> /Users/dawidl022/Development/verify-rust-std/library/core/src/slice/index.rs:1072:5
     |
1072 |     pub fn check_get_unchecked() {
     |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Failed to execute cargo (exit status: 101). Found 2 compilation errors.

Since #3457 added support for qualified paths, I'm unsure if the problem is my usage, or if this is a bug.

I thought it might be because of the generic parameter in the trait, but I couldn't get path resolution to work for a non-generic trait either:

error: Failed to resolve checking function <usize as BitOr>::bitor because Kani currently cannot resolve qualified paths
    --> /Users/dawidl022/Development/verify-rust-std/library/core/src/ops/bit.rs:1039:5
     |
1039 |     #[kani::proof_for_contract(<usize as BitOr>::bitor)]
     |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     |
     = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)

[carolynzech]

Hi @dawidl022

Apologies for the delayed response. This is a Kani limitation, you're correct. https://github.com/model-checking/kani/pull/4250 augments the error message to at least be a bit more useful (see commit) until we have full support for this pattern.

Marking this as a sub-issue of #1997