From c02c90af961cef20ad0f5852c5632520bcdd27f1 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Fri, 27 Mar 2026 20:30:34 -0400
Subject: [PATCH 1/3] Resolve generic trait method implementations for stubs
 (#1997)

Trait method stubbing with fully-qualified syntax like
`#[kani::stub(<X as A>::foo, stub_fn)]` already worked for non-generic
traits. This change extends support to generic traits like
`#[kani::stub(<MyType as Convert<u32>>::convert, stub_fn)]`.

The fix extracts generic type arguments from the trait path segment
(e.g., `<u32>` from `Convert<u32>`) and includes them alongside the
Self type when resolving the trait implementation via Instance::resolve.
Previously, only the Self type was passed, causing resolution to fail
for any trait with generic parameters.

Changes:
- resolve.rs: Extract trait generic args from the second-to-last path
  segment and pass them to resolve_in_trait_impl.
- resolve_in_trait_impl: Accept optional trait generic args, resolve
  them as types, and include in the GenericArgs for Instance::resolve.

Tests:
- stub_trait_method.rs: Three harnesses testing <X as A>::foo,
  <X as A>::bar, and <X as B>::bar with disambiguating syntax.
- stub_generic_trait_method.rs: Stubbing <MyType as Convert<u32>>::convert
  while leaving Convert<bool> unaffected.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 kani-compiler/src/kani_middle/resolve.rs      | 50 ++++++++++++++---
 .../Stubbing/stub_generic_trait_method.rs     | 32 +++++++++++
 tests/kani/Stubbing/stub_trait_method.rs      | 56 +++++++++++++++++++
 3 files changed, 130 insertions(+), 8 deletions(-)
 create mode 100644 tests/kani/Stubbing/stub_generic_trait_method.rs
 create mode 100644 tests/kani/Stubbing/stub_trait_method.rs

diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index 193771a9b81..382243cffbc 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -73,7 +73,21 @@ pub fn resolve_fn_path<'tcx>(
             let ty = type_resolution::resolve_ty(tcx, current_module, syn_ty)?;
             let trait_fn_id = resolve_path(tcx, current_module, &path.path)?;
             validate_kind!(tcx, trait_fn_id, "function / method", DefKind::Fn | DefKind::AssocFn)?;
-            resolve_in_trait_impl(tcx, ty, trait_fn_id)
+            // Extract generic args from the trait segment (e.g., <u32> from Convert<u32>).
+            let trait_generic_args = path
+                .path
+                .segments
+                .iter()
+                .rev()
+                .nth(1) // The trait segment is second-to-last (last is the method name)
+                .and_then(|seg| {
+                    if let syn::PathArguments::AngleBracketed(args) = &seg.arguments {
+                        Some(args)
+                    } else {
+                        None
+                    }
+                });
+            resolve_in_trait_impl(tcx, Some(current_module), ty, trait_fn_id, trait_generic_args)
         }
         // Qualified path for a primitive type, such as `<[u8]::sort>`.
         Some(QSelf { ty: syn_ty, .. }) if type_resolution::is_type_primitive(syn_ty) => {
@@ -399,8 +413,14 @@ fn resolve_in_any_trait<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty, name: &str) -> Option<F
         .into_iter()
         .filter_map(|trait_def| {
             resolve_in_trait_def_stable(tcx, trait_def, name).ok().and_then(|item| {
-                resolve_in_trait_impl(tcx, ty, rustc_internal::internal(tcx, item.def_id.def_id()))
-                    .ok()
+                resolve_in_trait_impl(
+                    tcx,
+                    None,
+                    ty,
+                    rustc_internal::internal(tcx, item.def_id.def_id()),
+                    None,
+                )
+                .ok()
             })
         })
         .collect();
@@ -411,16 +431,30 @@ fn resolve_in_any_trait<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty, name: &str) -> Option<F
 /// Resolves a trait method implementation by checking if there exists an Instance of the trait method for `ty`.
 /// This is distinct from `resolve_in_trait_def`: that function checks if the associated function is defined for the trait,
 /// while this function checks if it's implemented for `ty`.
-fn resolve_in_trait_impl(
-    tcx: TyCtxt<'_>,
+fn resolve_in_trait_impl<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    current_module: Option<LocalDefId>,
     ty: Ty,
     trait_fn_id: DefId,
-) -> Result<FnResolution, ResolveError<'_>> {
-    debug!(?ty, "resolve_in_trait_impl");
+    trait_args: Option<&syn::AngleBracketedGenericArguments>,
+) -> Result<FnResolution, ResolveError<'tcx>> {
+    debug!(?ty, ?trait_args, "resolve_in_trait_impl");
     // Given the `FnDef` of the *definition* of the trait method, see if there exists an Instance
     // that implements that method for `ty`.
     let trait_fn_fn_def = stable_fn_def(tcx, trait_fn_id).unwrap();
-    let desired_generic_args = GenericArgs(vec![GenericArgKind::Type(ty)]);
+
+    // Build generic args: Self type + any trait generic parameters (e.g., T in Convert<T>).
+    let mut args = vec![GenericArgKind::Type(ty)];
+    if let Some(syn_args) = trait_args {
+        let module = current_module.expect("current_module required for generic trait args");
+        for arg in &syn_args.args {
+            if let syn::GenericArgument::Type(syn_ty) = arg {
+                let resolved_ty = type_resolution::resolve_ty(tcx, module, syn_ty)?;
+                args.push(GenericArgKind::Type(resolved_ty));
+            }
+        }
+    }
+    let desired_generic_args = GenericArgs(args);
     let exists = Instance::resolve(trait_fn_fn_def, &desired_generic_args);
 
     // If such an Instance exists, return *its* FnDef (i.e., the FnDef inside the impl block for this `ty`)
diff --git a/tests/kani/Stubbing/stub_generic_trait_method.rs b/tests/kani/Stubbing/stub_generic_trait_method.rs
new file mode 100644
index 00000000000..85b89cfa0f3
--- /dev/null
+++ b/tests/kani/Stubbing/stub_generic_trait_method.rs
@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test stubbing generic trait method implementations.
+//! Regression test for https://github.com/model-checking/kani/issues/1997
+
+trait Convert<T> {
+    fn convert(&self) -> T;
+}
+
+struct MyType;
+
+impl Convert<u32> for MyType {
+    fn convert(&self) -> u32 { 100 }
+}
+
+impl Convert<bool> for MyType {
+    fn convert(&self) -> bool { false }
+}
+
+fn stub_convert_u32(_x: &MyType) -> u32 { 42 }
+
+#[kani::proof]
+#[kani::stub(<MyType as Convert<u32>>::convert, stub_convert_u32)]
+fn check_generic_trait_stub() {
+    let m = MyType;
+    assert_eq!(<MyType as Convert<u32>>::convert(&m), 42);
+    // The bool impl should NOT be affected
+    assert_eq!(<MyType as Convert<bool>>::convert(&m), false);
+}
diff --git a/tests/kani/Stubbing/stub_trait_method.rs b/tests/kani/Stubbing/stub_trait_method.rs
new file mode 100644
index 00000000000..988cd820477
--- /dev/null
+++ b/tests/kani/Stubbing/stub_trait_method.rs
@@ -0,0 +1,56 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test stubbing trait method implementations using fully-qualified syntax.
+//! Regression test for https://github.com/model-checking/kani/issues/1997
+
+trait A {
+    fn foo(&self) -> u32;
+    fn bar(&self) -> u32;
+}
+
+trait B {
+    fn bar(&self) -> u32;
+}
+
+struct X {}
+
+impl X {
+    fn new() -> Self { Self {} }
+}
+
+impl A for X {
+    fn foo(&self) -> u32 { 100 }
+    fn bar(&self) -> u32 { 200 }
+}
+
+impl B for X {
+    fn bar(&self) -> u32 { 300 }
+}
+
+fn stub_1(_x: &X) -> u32 { 1 }
+fn stub_2(_x: &X) -> u32 { 2 }
+fn stub_3(_x: &X) -> u32 { 3 }
+
+#[kani::proof]
+#[kani::stub(<X as A>::foo, stub_1)]
+fn check_stub_trait_a_foo() {
+    let x = X::new();
+    assert_eq!(x.foo(), 1);
+}
+
+#[kani::proof]
+#[kani::stub(<X as A>::bar, stub_2)]
+fn check_stub_trait_a_bar() {
+    let x = X::new();
+    assert_eq!(A::bar(&x), 2);
+}
+
+#[kani::proof]
+#[kani::stub(<X as B>::bar, stub_3)]
+fn check_stub_trait_b_bar() {
+    let x = X::new();
+    assert_eq!(<X as B>::bar(&x), 3);
+}

From c52f1cae5d9ea71105c3d50c57ce17a6d1a2c643 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Fri, 27 Mar 2026 20:34:39 -0400
Subject: [PATCH 2/3] Document trait method stubbing, add default method fixme
 test

Replace the 'Trait method stubbing not supported' limitation section
in stubbing.md with feature documentation showing the fully-qualified
syntax for both simple and generic traits.

Add fixme_stub_trait_default_method.rs documenting that default trait
methods (with body in the trait definition) fail validation because
the body uses Self instead of the concrete type.

Apply rustfmt to test files.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 docs/src/reference/experimental/stubbing.md   | 36 +++++++++++++++----
 .../fixme_stub_trait_default_method.rs        | 30 ++++++++++++++++
 .../Stubbing/stub_generic_trait_method.rs     | 12 +++++--
 tests/kani/Stubbing/stub_trait_method.rs      | 28 +++++++++++----
 4 files changed, 90 insertions(+), 16 deletions(-)
 create mode 100644 tests/kani/Stubbing/fixme_stub_trait_default_method.rs

diff --git a/docs/src/reference/experimental/stubbing.md b/docs/src/reference/experimental/stubbing.md
index 99616f47ee6..7940eb30658 100644
--- a/docs/src/reference/experimental/stubbing.md
+++ b/docs/src/reference/experimental/stubbing.md
@@ -170,13 +170,37 @@ In the following, we describe the known limitations of the stubbing feature.
 
 ### Trait method stubbing
 
-Stubbing trait method implementations (e.g., `<MyType as MyTrait>::method`) is **not supported**.
-Only free functions and inherent methods can be stubbed. Rust's attribute path syntax does not
-support the fully-qualified `<Type as Trait>::method` form, and the resolution algorithm does not
-search through trait implementations.
+Kani supports stubbing trait method implementations using fully-qualified syntax:
 
-If you need to stub a trait method, consider stubbing the calling function instead, or using
-conditional compilation (`#[cfg(kani)]`) to provide an alternative implementation.
+```rust
+trait MyTrait {
+    fn method(&self) -> u32;
+}
+
+struct MyType;
+
+impl MyTrait for MyType {
+    fn method(&self) -> u32 { 0 }
+}
+
+fn stub_method(_x: &MyType) -> u32 { 42 }
+
+#[kani::proof]
+#[kani::stub(<MyType as MyTrait>::method, stub_method)]
+fn check_trait_stub() {
+    let x = MyType;
+    assert_eq!(x.method(), 42);
+}
+```
+
+This also works with generic traits:
+
+```rust
+#[kani::stub(<MyType as Convert<u32>>::convert, stub_convert)]
+```
+
+When two traits define methods with the same name, the fully-qualified syntax
+disambiguates which implementation to stub.
 
 ### Usage restrictions
 
diff --git a/tests/kani/Stubbing/fixme_stub_trait_default_method.rs b/tests/kani/Stubbing/fixme_stub_trait_default_method.rs
new file mode 100644
index 00000000000..e7643899480
--- /dev/null
+++ b/tests/kani/Stubbing/fixme_stub_trait_default_method.rs
@@ -0,0 +1,30 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test stubbing a trait's default method implementation.
+//!
+//! FIXME: Default trait methods use `Self` in their body types, which
+//! doesn't match the concrete type in the stub. The validation compares
+//! the trait definition's body (with `&Self`) against the stub (with
+//! `&MyType`), causing a false type mismatch.
+//! Tracked in: https://github.com/model-checking/kani/issues/1997
+
+trait HasDefault {
+    fn default_method(&self) -> u32 {
+        0
+    }
+}
+
+struct MyType;
+impl HasDefault for MyType {}
+
+fn stub_default(_x: &MyType) -> u32 { 42 }
+
+#[kani::proof]
+#[kani::stub(<MyType as HasDefault>::default_method, stub_default)]
+fn check_stub_default_trait_method() {
+    let x = MyType;
+    assert_eq!(x.default_method(), 42);
+}
diff --git a/tests/kani/Stubbing/stub_generic_trait_method.rs b/tests/kani/Stubbing/stub_generic_trait_method.rs
index 85b89cfa0f3..5877bb34116 100644
--- a/tests/kani/Stubbing/stub_generic_trait_method.rs
+++ b/tests/kani/Stubbing/stub_generic_trait_method.rs
@@ -13,14 +13,20 @@ trait Convert<T> {
 struct MyType;
 
 impl Convert<u32> for MyType {
-    fn convert(&self) -> u32 { 100 }
+    fn convert(&self) -> u32 {
+        100
+    }
 }
 
 impl Convert<bool> for MyType {
-    fn convert(&self) -> bool { false }
+    fn convert(&self) -> bool {
+        false
+    }
 }
 
-fn stub_convert_u32(_x: &MyType) -> u32 { 42 }
+fn stub_convert_u32(_x: &MyType) -> u32 {
+    42
+}
 
 #[kani::proof]
 #[kani::stub(<MyType as Convert<u32>>::convert, stub_convert_u32)]
diff --git a/tests/kani/Stubbing/stub_trait_method.rs b/tests/kani/Stubbing/stub_trait_method.rs
index 988cd820477..83f4f74cbb1 100644
--- a/tests/kani/Stubbing/stub_trait_method.rs
+++ b/tests/kani/Stubbing/stub_trait_method.rs
@@ -18,21 +18,35 @@ trait B {
 struct X {}
 
 impl X {
-    fn new() -> Self { Self {} }
+    fn new() -> Self {
+        Self {}
+    }
 }
 
 impl A for X {
-    fn foo(&self) -> u32 { 100 }
-    fn bar(&self) -> u32 { 200 }
+    fn foo(&self) -> u32 {
+        100
+    }
+    fn bar(&self) -> u32 {
+        200
+    }
 }
 
 impl B for X {
-    fn bar(&self) -> u32 { 300 }
+    fn bar(&self) -> u32 {
+        300
+    }
 }
 
-fn stub_1(_x: &X) -> u32 { 1 }
-fn stub_2(_x: &X) -> u32 { 2 }
-fn stub_3(_x: &X) -> u32 { 3 }
+fn stub_1(_x: &X) -> u32 {
+    1
+}
+fn stub_2(_x: &X) -> u32 {
+    2
+}
+fn stub_3(_x: &X) -> u32 {
+    3
+}
 
 #[kani::proof]
 #[kani::stub(<X as A>::foo, stub_1)]

From 9c4219de42485648fdc9ccad31e31f3decadae9c Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Sat, 28 Mar 2026 14:26:01 -0400
Subject: [PATCH 3/3] test(stubbing): Add trait stubbing tests for dyn
 dispatch, supertraits, and overridden defaults

Verify that trait method stubbing works correctly for:
- Dynamic dispatch through &dyn Trait and Box<dyn Trait>
- Methods defined in supertraits
- Default trait methods that are overridden in the impl

Update documentation to list supported trait patterns and refine
the known limitation to only non-overridden default methods.
Remove 'Traits' from the unsupported items list.
---
 docs/src/reference/experimental/stubbing.md   | 11 +++-
 kani-compiler/src/kani_middle/resolve.rs      | 33 ++++++++++--
 .../fixme_stub_trait_default_method.rs        |  6 ++-
 .../Stubbing/stub_generic_slice_index.rs}     |  9 ++--
 .../Stubbing/stub_trait_default_overridden.rs | 32 ++++++++++++
 .../kani/Stubbing/stub_trait_dyn_dispatch.rs  | 38 ++++++++++++++
 tests/kani/Stubbing/stub_trait_supertrait.rs  | 52 +++++++++++++++++++
 .../generic_slice_index.expected              | 11 ----
 .../stub_assoc_type_constraint.expected       |  1 +
 .../stub_assoc_type_constraint.rs             | 30 +++++++++++
 .../stub_const_generic_trait.expected         |  1 +
 .../stub_const_generic_trait.rs               | 28 ++++++++++
 12 files changed, 228 insertions(+), 24 deletions(-)
 rename tests/{ui/function-contracts/generic_slice_index.rs => kani/Stubbing/stub_generic_slice_index.rs} (73%)
 create mode 100644 tests/kani/Stubbing/stub_trait_default_overridden.rs
 create mode 100644 tests/kani/Stubbing/stub_trait_dyn_dispatch.rs
 create mode 100644 tests/kani/Stubbing/stub_trait_supertrait.rs
 delete mode 100644 tests/ui/function-contracts/generic_slice_index.expected
 create mode 100644 tests/ui/stubbing/stub-assoc-type-constraint/stub_assoc_type_constraint.expected
 create mode 100644 tests/ui/stubbing/stub-assoc-type-constraint/stub_assoc_type_constraint.rs
 create mode 100644 tests/ui/stubbing/stub-const-generic-trait/stub_const_generic_trait.expected
 create mode 100644 tests/ui/stubbing/stub-const-generic-trait/stub_const_generic_trait.rs

diff --git a/docs/src/reference/experimental/stubbing.md b/docs/src/reference/experimental/stubbing.md
index 7940eb30658..53fd90179ce 100644
--- a/docs/src/reference/experimental/stubbing.md
+++ b/docs/src/reference/experimental/stubbing.md
@@ -202,6 +202,16 @@ This also works with generic traits:
 When two traits define methods with the same name, the fully-qualified syntax
 disambiguates which implementation to stub.
 
+The following trait patterns are supported:
+
+- **Supertrait methods:** Stubbing a method defined in a supertrait (e.g., `<MyType as Base>::method`) works independently of subtrait methods.
+- **Overridden default methods:** If a type overrides a trait's default method, the override can be stubbed normally.
+- **Dynamic dispatch:** Stubs apply even when the method is called through a trait object (`&dyn Trait` or `Box<dyn Trait>`).
+
+**Known limitation:** Stubbing a trait's default method that is *not* overridden by the implementing type is not currently supported ([#4588](https://github.com/model-checking/kani/issues/4588)). The default method body uses `Self` as a placeholder type, which causes a type mismatch during stub validation. This applies only to default methods that are inherited as-is (i.e., the `impl` block does not provide its own definition).
+
+**Known limitation:** Traits with const generic parameters (e.g., `<Type as Buf<16>>::write`) or associated type constraints (e.g., `<Type as Iterator<Item = u32>>::next`) are not currently supported and will produce a resolution error.
+
 ### Usage restrictions
 
 Stub annotations (`#[kani::stub]`) are specified per-harness. When a crate contains multiple
@@ -215,7 +225,6 @@ Support for stubbing is currently **limited to functions and methods**. All othe
 The following are examples of items that could be good candidates for stubbing, but aren't supported:
 - Types
 - Macros
-- Traits
 - Intrinsics
 
 We acknowledge that support for method stubbing isn't as ergonomic as it could be.
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index 382243cffbc..33e6ebd9110 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -74,6 +74,9 @@ pub fn resolve_fn_path<'tcx>(
             let trait_fn_id = resolve_path(tcx, current_module, &path.path)?;
             validate_kind!(tcx, trait_fn_id, "function / method", DefKind::Fn | DefKind::AssocFn)?;
             // Extract generic args from the trait segment (e.g., <u32> from Convert<u32>).
+            // For `<Type as crate::mod::Trait<u32>>::method`, segments after `as` are
+            // [crate, mod, Trait<u32>, method]. The trait segment with generic args is
+            // always second-to-last (last is the method name).
             let trait_generic_args = path
                 .path
                 .segments
@@ -413,6 +416,9 @@ fn resolve_in_any_trait<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty, name: &str) -> Option<F
         .into_iter()
         .filter_map(|trait_def| {
             resolve_in_trait_def_stable(tcx, trait_def, name).ok().and_then(|item| {
+                // No current_module or trait_args needed: this path resolves
+                // unqualified method names (e.g., `x.foo()`), not user-specified
+                // `<Type as Trait<T>>::method` syntax.
                 resolve_in_trait_impl(
                     tcx,
                     None,
@@ -446,11 +452,30 @@ fn resolve_in_trait_impl<'tcx>(
     // Build generic args: Self type + any trait generic parameters (e.g., T in Convert<T>).
     let mut args = vec![GenericArgKind::Type(ty)];
     if let Some(syn_args) = trait_args {
-        let module = current_module.expect("current_module required for generic trait args");
+        let Some(module) = current_module else {
+            return Err(ResolveError::UnsupportedPath {
+                kind: "stub resolution requires generic trait arguments to have a known module context",
+            });
+        };
         for arg in &syn_args.args {
-            if let syn::GenericArgument::Type(syn_ty) = arg {
-                let resolved_ty = type_resolution::resolve_ty(tcx, module, syn_ty)?;
-                args.push(GenericArgKind::Type(resolved_ty));
+            match arg {
+                syn::GenericArgument::Type(syn_ty) => {
+                    let resolved_ty = type_resolution::resolve_ty(tcx, module, syn_ty)?;
+                    args.push(GenericArgKind::Type(resolved_ty));
+                }
+                syn::GenericArgument::Const(_) => {
+                    return Err(ResolveError::UnsupportedPath {
+                        kind: "const generic arguments in trait stubs",
+                    });
+                }
+                syn::GenericArgument::Lifetime(_) => {
+                    // Lifetimes are erased — safe to skip.
+                }
+                _ => {
+                    return Err(ResolveError::UnsupportedPath {
+                        kind: "associated type/const constraints in trait stubs",
+                    });
+                }
             }
         }
     }
diff --git a/tests/kani/Stubbing/fixme_stub_trait_default_method.rs b/tests/kani/Stubbing/fixme_stub_trait_default_method.rs
index e7643899480..3f9d3bb60f7 100644
--- a/tests/kani/Stubbing/fixme_stub_trait_default_method.rs
+++ b/tests/kani/Stubbing/fixme_stub_trait_default_method.rs
@@ -9,7 +9,7 @@
 //! doesn't match the concrete type in the stub. The validation compares
 //! the trait definition's body (with `&Self`) against the stub (with
 //! `&MyType`), causing a false type mismatch.
-//! Tracked in: https://github.com/model-checking/kani/issues/1997
+//! Tracked in: https://github.com/model-checking/kani/issues/4588
 
 trait HasDefault {
     fn default_method(&self) -> u32 {
@@ -20,7 +20,9 @@ trait HasDefault {
 struct MyType;
 impl HasDefault for MyType {}
 
-fn stub_default(_x: &MyType) -> u32 { 42 }
+fn stub_default(_x: &MyType) -> u32 {
+    42
+}
 
 #[kani::proof]
 #[kani::stub(<MyType as HasDefault>::default_method, stub_default)]
diff --git a/tests/ui/function-contracts/generic_slice_index.rs b/tests/kani/Stubbing/stub_generic_slice_index.rs
similarity index 73%
rename from tests/ui/function-contracts/generic_slice_index.rs
rename to tests/kani/Stubbing/stub_generic_slice_index.rs
index 5926fcd54eb..15ce4865d6e 100644
--- a/tests/ui/function-contracts/generic_slice_index.rs
+++ b/tests/kani/Stubbing/stub_generic_slice_index.rs
@@ -1,12 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts
-//! Test function contracts on generic trait implementations based on SliceIndex,
-//! c.f. https://github.com/model-checking/kani/issues/4084
-//! This `proof_for_contract` should work,
-//! but we do not yet support stubbing/contracts on trait fns with generic arguments
-//! c.f. https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734.
-//! So for now, test that we emit a nice error message.
+//! Test function contracts on generic trait implementations based on SliceIndex.
+//! Regression test for https://github.com/model-checking/kani/issues/1997
+//! and https://github.com/model-checking/kani/issues/4084.
 
 const INVALID_INDEX: usize = 10;
 
diff --git a/tests/kani/Stubbing/stub_trait_default_overridden.rs b/tests/kani/Stubbing/stub_trait_default_overridden.rs
new file mode 100644
index 00000000000..eb8e95fd8d4
--- /dev/null
+++ b/tests/kani/Stubbing/stub_trait_default_overridden.rs
@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test stubbing a trait default method that IS overridden in the impl.
+//! The stub should replace the overridden implementation, not the default.
+
+trait HasDefault {
+    fn method(&self) -> u32 {
+        0
+    }
+}
+
+struct MyType;
+
+impl HasDefault for MyType {
+    fn method(&self) -> u32 {
+        100
+    }
+}
+
+fn stub_method(_x: &MyType) -> u32 {
+    42
+}
+
+#[kani::proof]
+#[kani::stub(<MyType as HasDefault>::method, stub_method)]
+fn check_stub_overridden_default() {
+    let x = MyType;
+    assert_eq!(x.method(), 42);
+}
diff --git a/tests/kani/Stubbing/stub_trait_dyn_dispatch.rs b/tests/kani/Stubbing/stub_trait_dyn_dispatch.rs
new file mode 100644
index 00000000000..98a2d0e3d19
--- /dev/null
+++ b/tests/kani/Stubbing/stub_trait_dyn_dispatch.rs
@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test stubbing a trait method called through dynamic dispatch (trait objects).
+
+trait Animal {
+    fn sound(&self) -> u32;
+}
+
+struct Dog;
+
+impl Animal for Dog {
+    fn sound(&self) -> u32 {
+        100
+    }
+}
+
+fn stub_sound(_x: &Dog) -> u32 {
+    42
+}
+
+fn call_via_dyn(a: &dyn Animal) -> u32 {
+    a.sound()
+}
+
+#[kani::proof]
+#[kani::stub(<Dog as Animal>::sound, stub_sound)]
+fn check_stub_dyn_dispatch() {
+    let dog = Dog;
+    // Direct call — should be stubbed
+    assert_eq!(dog.sound(), 42);
+    // Call through trait object — stub applies because Kani replaces the
+    // function body globally, which is used regardless of dispatch mechanism.
+    let result = call_via_dyn(&dog);
+    assert_eq!(result, 42);
+}
diff --git a/tests/kani/Stubbing/stub_trait_supertrait.rs b/tests/kani/Stubbing/stub_trait_supertrait.rs
new file mode 100644
index 00000000000..3793e0adc18
--- /dev/null
+++ b/tests/kani/Stubbing/stub_trait_supertrait.rs
@@ -0,0 +1,52 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test stubbing a method defined in a supertrait.
+
+trait Base {
+    fn base_method(&self) -> u32;
+}
+
+trait Derived: Base {
+    fn derived_method(&self) -> u32;
+}
+
+struct MyType;
+
+impl Base for MyType {
+    fn base_method(&self) -> u32 {
+        100
+    }
+}
+
+impl Derived for MyType {
+    fn derived_method(&self) -> u32 {
+        200
+    }
+}
+
+fn stub_base(_x: &MyType) -> u32 {
+    1
+}
+
+fn stub_derived(_x: &MyType) -> u32 {
+    2
+}
+
+#[kani::proof]
+#[kani::stub(<MyType as Base>::base_method, stub_base)]
+fn check_stub_supertrait_method() {
+    let x = MyType;
+    assert_eq!(x.base_method(), 1);
+}
+
+#[kani::proof]
+#[kani::stub(<MyType as Derived>::derived_method, stub_derived)]
+fn check_stub_subtrait_method() {
+    let x = MyType;
+    assert_eq!(x.derived_method(), 2);
+    // Supertrait method should NOT be affected
+    assert_eq!(x.base_method(), 100);
+}
diff --git a/tests/ui/function-contracts/generic_slice_index.expected b/tests/ui/function-contracts/generic_slice_index.expected
deleted file mode 100644
index 140d000b6b6..00000000000
--- a/tests/ui/function-contracts/generic_slice_index.expected
+++ /dev/null
@@ -1,11 +0,0 @@
-error: failed to resolve `<usize as SliceIndex < [i32] >>::get_unchecked`: unable to find implementation of associated function `SliceIndex::get_unchecked` for usize\
-generic_slice_index.rs\
-|\
-| #[kani::proof_for_contract(<usize as SliceIndex<[i32]>>::get_unchecked)]\
-| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
-|\
-= note: Kani does not currently support stubs or function contracts on generic functions in traits.\
-    See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.
-
-
-error: aborting due to 1 previous error
diff --git a/tests/ui/stubbing/stub-assoc-type-constraint/stub_assoc_type_constraint.expected b/tests/ui/stubbing/stub-assoc-type-constraint/stub_assoc_type_constraint.expected
new file mode 100644
index 00000000000..2e7c8a3bad3
--- /dev/null
+++ b/tests/ui/stubbing/stub-assoc-type-constraint/stub_assoc_type_constraint.expected
@@ -0,0 +1 @@
+error: failed to resolve `<Counter as MyIterator < Item = u32 >>::next`: Kani currently cannot resolve associated type/const constraints in trait stubs
diff --git a/tests/ui/stubbing/stub-assoc-type-constraint/stub_assoc_type_constraint.rs b/tests/ui/stubbing/stub-assoc-type-constraint/stub_assoc_type_constraint.rs
new file mode 100644
index 00000000000..a21ffbe45c0
--- /dev/null
+++ b/tests/ui/stubbing/stub-assoc-type-constraint/stub_assoc_type_constraint.rs
@@ -0,0 +1,30 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z stubbing
+
+//! Test that stubbing a trait with associated type constraints produces a
+//! clear error message.
+
+trait MyIterator {
+    type Item;
+    fn next(&self) -> Self::Item;
+}
+
+struct Counter;
+impl MyIterator for Counter {
+    type Item = u32;
+    fn next(&self) -> u32 {
+        1
+    }
+}
+
+fn mock_next(_: &Counter) -> u32 {
+    42
+}
+
+#[kani::proof]
+#[kani::stub(<Counter as MyIterator<Item = u32>>::next, mock_next)]
+fn check_assoc_type_stub() {
+    let c = Counter;
+    assert_eq!(c.next(), 42);
+}
diff --git a/tests/ui/stubbing/stub-const-generic-trait/stub_const_generic_trait.expected b/tests/ui/stubbing/stub-const-generic-trait/stub_const_generic_trait.expected
new file mode 100644
index 00000000000..d2e0ac53819
--- /dev/null
+++ b/tests/ui/stubbing/stub-const-generic-trait/stub_const_generic_trait.expected
@@ -0,0 +1 @@
+error: failed to resolve `<MyBuf as Buf < 16 >>::write`: Kani currently cannot resolve const generic arguments in trait stubs
diff --git a/tests/ui/stubbing/stub-const-generic-trait/stub_const_generic_trait.rs b/tests/ui/stubbing/stub-const-generic-trait/stub_const_generic_trait.rs
new file mode 100644
index 00000000000..ca7cd6f03ad
--- /dev/null
+++ b/tests/ui/stubbing/stub-const-generic-trait/stub_const_generic_trait.rs
@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z stubbing
+
+//! Test that stubbing a trait with const generic parameters produces a
+//! clear error message.
+
+trait Buf<const N: usize> {
+    fn write(&self) -> usize;
+}
+
+struct MyBuf;
+impl Buf<16> for MyBuf {
+    fn write(&self) -> usize {
+        16
+    }
+}
+
+fn mock_write(_: &MyBuf) -> usize {
+    42
+}
+
+#[kani::proof]
+#[kani::stub(<MyBuf as Buf<16>>::write, mock_write)]
+fn check_const_generic_stub() {
+    let b = MyBuf;
+    assert_eq!(b.write(), 42);
+}