[Feature Request] Ability to stub out function on primitive types (such as `[T]`)

[roypat]

Requested feature: I recently ran across a situation where I wanted to stub the binary_search_by_key function on slices because I knew my slice would always have length 1, which would allow me to save on some unrolls. I ran into some problems expressing this stub however, since [T]::binary_search_by_key is not a valid path (even the impl [T] in the standard library seems to be special-cased into the compiler).

Test case:

I'm really not sure how to express this, since [T] cannot really be part of paths, but I guess I'd like

// kani_example.rs
fn stub_len<T>(this: &[T]) -> usize {
    0
}

#[kani::proof]
#[kani::stub(std::slice::[T]::len, stub_len)]
fn verify_len() {
    assert_eq!(vec![1].as_slice().len(), 0);
}

to work. Currently, the output I get from running kani kani_example.rs is

$ kani kani_example.rs 
Kani Rust Verifier 0.33.0 (standalone)
warning: unused variable: `this`
 --> kani_example.rs:1:16
  |
1 | fn stub_len<T>(this: &[T]) -> usize {
  |                ^^^^ help: if this is intentional, prefix it with an underscore: `_this`
  |
  = note: `#[warn(unused_variables)]` on by default

warning: function `stub_len` is never used
 --> kani_example.rs:1:4
  |
1 | fn stub_len<T>(this: &[T]) -> usize {
  |    ^^^^^^^^
  |
  = note: `#[warn(dead_code)]` on by default

error: attribute `kani::stub` takes two path arguments; found 0
 --> kani_example.rs:6:1
  |
6 | #[kani::stub(std::slice::[T]::len, stub_len)]
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = note: this error originates in the attribute macro `kani::stub` (in Nightly builds, run with -Z macro-backtrace for more info)

[celinval]

Just to clarify, the problem is that slice methods are represented using qualified paths, and today we only support simple paths.

For example, here is a dummy test that calls len() via a function pointer:

#[test]
fn test_len() {
    assert_eq!(len_ptr(&[1u8]), 1);
}

fn len_ptr<T>(slice: &[T]) -> usize {
    let ptr = <[T]>::len;
    ptr(slice)
}

@feliperodri one workaround that might be easier to implement is to allow users to stub using type alias. @roypat, would something like this work for you:

type Slice<T> = [T];

#[kani::proof]
#[kani::stub(Slice::len, stub_len)]
fn verify_len() {
    assert_eq!(vec![1u8].as_slice().len(), 1);
    assert_eq!(vec![1u8].as_slice().len(), 0);
}