Info on whether a type implements a trait

[carolynzech]

I'm working on a new feature for Kani where we can automatically verify certain functions for you. Currently, to use Kani you need to write a "proof harness" that invokes the function you want to verify on concrete types, e.g.:

fn foo<T: Clone + PartialEq + Eq>(x: T) -> bool {
    x == x.clone()
}

#[kani::proof]
fn harness() {
    let x: u8 = kani::any(); // Generate a nondeterministic u8
    foo(x); // Verify foo with all possible u8 values
}

We would like to make it so that the user doesn't need to write harness at all. Kani would ideally be able to look at the type signature of foo and come up with a handful of types that would satisfy its trait bounds, so that it can autogenerate harnesses for those types. (Note I say "a handful" instead of "all" -- there are obviously many types that implement Clone, PartialEq, and Eq, and it isn't necessarily good UX to generate proofs for all of them. But that's more of a Kani UX problem that we can solve later).

My (purposefully broad) question is: any thoughts about the best way to go about this using the StableMIR APIs? I want to avoid asking an XY question, so I'll outline a few solutions I've thought of, but open to other suggestions as well:

• Go from type --> trait: Have a hardcoded list of options for T in Kani (e.g., the primitive types). Use a method like type_implements_trait to filter those defaults by which satisfy T's trait bounds, then generate harnesses for those.
• Go from trait --> type: Somehow(?) provide the Rust compiler with a list of traits that I need satisfied, and ask it which types it knows of that implement those traits. I suspect this is hard/impossible because of the issues discussed here.

TIA!

[oli-obk]

• Go from trait --> type: Somehow(?) provide the Rust compiler with a list of traits that I need satisfied, and ask it which types it knows of that implement those traits. I suspect this is hard/impossible because of the issues discussed here.

What is possible is to ask for the impls of a trait (which isn't the same thing, there being generic impls and specialization and stuff): https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/query/plumbing/struct.TyCtxtAt.html#method.trait_impls_of

So you can at least find types that explicitly impl a trait

• Go from type --> trait: Have a hardcoded list of options for T in Kani (e.g., the primitive types). Use a method like type_implements_trait to filter those defaults by which satisfy T's trait bounds, then generate harnesses for those.

Not sure we already have full TraitRefs in SMIR, but we'd need those to satisfy T: PartialEq<T> (which T: PartialEq means) instead of just looking for any PartialEq impl. After that we can indeed just add type_implements_trait