Support stubbing trait method implementations

[feliperodri]

Enable stubbing of trait method implementations using fully-qualified syntax (<Type as Trait>::method), including generic traits. Previously, Kani's stub resolution only searched inherent impl blocks and trait method implementations were silently ignored.

Resolves #1997.

Problem

Users could not stub trait method implementations. Writing #[kani::stub(<MyType as MyTrait>::method, mock_method)] failed because the resolution algorithm did not search through trait implementations for the concrete type. This was a significant limitation since many Rust APIs are trait-based.

Solution

Resolution (resolve.rs)

resolve_in_trait_impl now correctly resolves trait method implementations by:

1. Extracting generic arguments from the trait segment (e.g., <u32> from Convert<u32>)
2. Building the full GenericArgs with the Self type + trait generic parameters
3. Resolving the Instance for the concrete type's implementation

This handles both simple traits (<Vec<u8> as MyTrait>::method) and generic traits (<MyType as Convert<u32>>::convert).

Documentation (stubbing.md)

Updated the user-facing docs to document trait method stubbing with examples covering:

• Basic trait method stubbing syntax
• Generic trait methods
• Supported patterns (dyn dispatch, supertraits, overridden defaults)
• Known limitation: non-overridden default methods

Testing

5 passing tests:

• stub_trait_method.rs — basic <Type as Trait>::method stubbing
• stub_generic_trait_method.rs — generic trait <Type as Trait<T>>::method
• stub_trait_dyn_dispatch.rs — dynamic dispatch through &dyn Trait and Box<dyn Trait>
• stub_trait_supertrait.rs — methods defined in supertraits
• stub_trait_default_overridden.rs — default trait methods that are overridden in the impl

1 fixme test:

• fixme_stub_trait_default_method.rs — non-overridden default methods cause a type mismatch during stub validation (the default body uses Self as a placeholder type)

---

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[adpaco-aws]

Thank you!