proof_for_contract cannot resolve methods on impls defined outside the type's own module when multiple same-named candidates exist

[kasimte]

A method whose impl block lives outside the type's own module cannot be targeted by #[kani::proof_for_contract(...)] under any path spelling when it also has multiple same-named sibling impls — its def_path_str rendering (path::to::module::<impl path::to::Type<Args>>::method) is a form no user-spellable path can match.

This is the remaining half of the multi-impl resolution work from #3773: that fix (and its regression test, tests/kani/FunctionContracts/multiple_inherent_impls.rs) covers same-named impls in the type's own module, where def_path_str renders Type::<Args>::method; the out-of-module rendering was left unmatchable. A companion PR accompanies this issue with a fix and a self-contained regression test (cross_module_multiple_impls.rs) that reproduces the failure outside the standard library.

Reproduction

I tried this code — verify-rust-std at kani d4df833. alloc::boxed::convert defines three same-named methods on sibling impls, in a different module (boxed/convert.rs) than Box itself (boxed.rs); I added a safety contract to each and targeted the first with a #[kani::proof_for_contract(...)] harness:

impl<A: Allocator> Box<dyn Any, A>                 { pub unsafe fn downcast_unchecked<T: Any>(..) }
impl<A: Allocator> Box<dyn Any + Send, A>          { pub unsafe fn downcast_unchecked<T: Any>(..) }
impl<A: Allocator> Box<dyn Any + Send + Sync, A>   { pub unsafe fn downcast_unchecked<T: Any>(..) }

using the following command line invocation:

kani verify-std -Z unstable-options ./library -Z function-contracts -Z mem-predicates -Z loop-contracts --harness boxed::convert::verify::check_downcast_unchecked_any_u32 --exact --cbmc-args --object-bits 12

with Kani version: d4df833 (0.67.0 era), CBMC 6.8.0.

I expected to see this happen: the target resolves against one of the three listed impls and its contract is verified.

Instead, this happened: resolution fails for every path spelling tried — five for the first impl:

1. Box::<dyn Any, Global>::downcast_unchecked::<u32>
2. Box::<dyn Any + 'static, Global>::downcast_unchecked::<u32>
3. Box::<dyn Any, A>::downcast_unchecked::<u32>
4. Box::<dyn Any + 'static, A>::downcast_unchecked::<u32>
5. Box::<dyn core::any::Any + 'static, A>::downcast_unchecked::<u32>

Representative error (spelling 4):

error: failed to resolve `Box :: < dyn Any + 'static , A >::downcast_unchecked :: < u32 >`: the generic arguments ::<dynAny+'static,A> are invalid. The available implementations are: 
       boxed::convert::<impl boxed::Box<(dyn core::any::Any + 'static), A>>::downcast_unchecked
       boxed::convert::<impl boxed::Box<(dyn core::any::Any + core::marker::Send + 'static), A>>::downcast_unchecked
       boxed::convert::<impl boxed::Box<(dyn core::any::Any + core::marker::Send + core::marker::Sync + 'static), A>>::downcast_unchecked

The resolver prints the candidate impls it knows, yet accepts no spelling of them — including spelling 5, which mirrors the printed trait path.

Root cause

resolve_in_type_def (kani-compiler/src/kani_middle/resolve.rs) disambiguates multiple candidates via last_two_items_of_path_match, a whitespace-stripped string comparison between the user's turbofish and the last two ::-separated segments of def_path_str(candidate). An impl in the type's own module renders as Type::<Args>::method, which can match; an impl in another module renders as <impl Type<Args>>, whose <impl prefix no turbofish can produce — and the trait-object bound is additionally wrapped in parens in that rendering.

Controls consistent with this:

• Single-candidate methods skip disambiguation entirely and resolve regardless of module (e.g. Rc::<dyn Any, Global>::downcast_unchecked::<T>, one impl — see verify-rust-std PR RMC should use fully qualified name for harness selection and it should not rely on no_mangle attribute #661).
• Multi-candidate methods whose impls are in the type's own module resolve when spelled with the impl's own generic tokens (e.g. Box::<core::mem::MaybeUninit<T>, A>::assume_init works; the concrete Box::<core::mem::MaybeUninit<u32>>::assume_init does not — a second, milder symptom of the string-matching approach).
• A standalone two-parameter type (each method name on a single impl) resolves under concrete spellings — the single-candidate path again, independent of the joint T/A generics.

Impact

Contract-bearing methods in this position (the three Box<dyn Any…>::downcast_uncheckeds arise in verify-rust-std's Challenge 29 work, model-checking/verify-rust-std#669) cannot be machine-linked to their contracts; verification falls back to plain harnesses asserting the postconditions manually.

With the companion fix

All three methods resolve (spelled Box::<dyn core::any::Any + 'static, A>::…, with auto-traits fully qualified for the + Send/+ Send + Sync variants) and their contracts verify.