From a48f0d873ca5ac4b6e4ff53c88105507e5673530 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 28 Jul 2026 01:06:28 +0000
Subject: [PATCH 1/4] Autoharness: support generic functions

Previously, autoharness skipped all generic functions. Now, it generates a
harness for a single monomorphic instantiation: each type parameter is
substituted with the first candidate from a fixed list of primitive types
(i32, u32, usize, bool, char) such that all of the function's trait bounds
are satisfied, checked with the trait solver
(rustc_trait_selection::ObligationCtxt). Lifetime parameters are erased.
Functions whose bounds no candidate satisfies, or with const generic
parameters, are still skipped as 'Generic Function'.

The generated harness's name reflects the chosen instantiation (e.g.
foo::<i32>), making explicit that verification covers only that
instantiation; the documentation spells out this underapproximation.
Functions with any number of type, lifetime, and (unsupported) const
parameters are handled, including methods of generic impl blocks, impl-Trait
arguments, and functions with contracts. For contract harnesses, harness
metadata now stores the definition-level name of the target function rather
than the instantiated one, since gen_contracts_metadata matches it against
definition-level ContractedFunction names.

This addresses the 'Generics' item of the automatic harness generation
tracking issue, the last unchecked entry together with the invariants and
pointers work.

Towards #3832

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Signed-off-by: Felipe Monteiro <felisous@amazon.com>
---
 .../src/reference/experimental/autoharness.md |  32 ++---
 .../src/kani_middle/codegen_units.rs          | 131 +++++++++++++++---
 kani-compiler/src/kani_middle/metadata.rs     |   6 +-
 kani-compiler/src/main.rs                     |   2 +
 .../exclude.expected                          |  34 ++---
 .../cargo_autoharness_exclude/src/lib.rs      |   2 +-
 .../cargo_autoharness_filter/filter.expected  |  13 +-
 .../cargo_autoharness_filter/src/lib.rs       |   7 +-
 .../cargo_autoharness_generics/Cargo.toml     |  10 ++
 .../cargo_autoharness_generics/config.yml     |   5 +
 .../generics.expected                         |  11 ++
 .../cargo_autoharness_generics/generics.sh    |   5 +
 .../cargo_autoharness_generics/src/lib.rs     |  81 +++++++++++
 .../include.expected                          |  34 ++---
 .../cargo_autoharness_include/src/lib.rs      |   2 +-
 15 files changed, 296 insertions(+), 79 deletions(-)
 create mode 100644 tests/script-based-pre/cargo_autoharness_generics/Cargo.toml
 create mode 100644 tests/script-based-pre/cargo_autoharness_generics/config.yml
 create mode 100644 tests/script-based-pre/cargo_autoharness_generics/generics.expected
 create mode 100755 tests/script-based-pre/cargo_autoharness_generics/generics.sh
 create mode 100644 tests/script-based-pre/cargo_autoharness_generics/src/lib.rs

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index f8a44ddcbb1f..02347db03902 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -155,7 +155,9 @@ Kani will detect if a struct or enum could implement `Arbitrary` and derive it a
 Note that this automatic derivation feature is only available for autoharness.
 
 ### Generic Functions
-The current implementation does not generate harnesses for generic functions.
+For a generic function, Kani generates a harness for a single monomorphic instantiation of the function:
+it substitutes every type parameter with the first candidate from a fixed list of primitive types
+(starting with `i32`) such that all of the function's trait bounds are satisfied, and erases lifetime parameters.
 For example, given:
 ```rust
 fn foo<T: Eq>(x: T, y: T) {
@@ -164,23 +166,19 @@ fn foo<T: Eq>(x: T, y: T) {
     }
 }
 ```
-Kani would report that no functions were eligible for automatic harness generation.
-
-If, however, some caller of `foo` is eligible for an automatic harness, then a monomorphized version of `foo` may still be reachable during verification.
-For instance, if we add `main`:
-```rust
-fn main() {
-    let x: u8 = 2;
-    let y: u8 = 2;
-    foo(x, y);
-}
+Kani generates and runs a harness that verifies `foo::<i32>`, and the summary table shows the
+instantiated name, e.g.:
 ```
-and run the autoharness subcommand, we get:
+| Crate    | Selected Function | Kind of Automatic Harness | Verification Result |
+| my_crate | foo::<i32>        | #[kani::proof]            | Failure             |
 ```
-Autoharness: Checking function main against all possible inputs...
+Note that verifying a single instantiation is an underapproximation of all of the function's possible behaviors:
+a successful result for `foo::<i32>` does not imply that other instantiations of `foo` are also safe.
+Kani makes this explicit by displaying the instantiated name of the verified function.
 
-Failed Checks: x and y are equal
- File: "src/lib.rs", line 3, in foo::<u8>
+Kani skips a generic function (with skip reason "Generic Function") if:
+- no candidate type satisfies the function's trait bounds, or
+- the function has const generic parameters, which Kani does not instantiate yet.
 
-VERIFICATION:- FAILED
-```
+If some caller of a generic function is eligible for an automatic harness, then additional monomorphized
+versions of the generic function may still be reachable (and thus verified) through the caller's harness.
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index 5535550eabf2..6459d7077434 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -24,13 +24,17 @@ use kani_metadata::{
 use regex::RegexSet;
 use rustc_data_structures::fx::{FxHashMap, FxHashSet};
 use rustc_hir::def_id::DefId;
-use rustc_middle::ty::TyCtxt;
+use rustc_infer::infer::TyCtxtInferExt;
+use rustc_middle::ty::{self, TyCtxt, TypingMode};
 use rustc_public::mir::mono::Instance;
 use rustc_public::rustc_internal;
-use rustc_public::ty::{FnDef, GenericArgKind, GenericArgs, RigidTy, Ty, TyKind};
+use rustc_public::ty::{
+    FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy,
+};
 use rustc_public::{CrateDef, CrateItem};
 use rustc_public_bridge::IndexedVal;
 use rustc_session::config::OutputType;
+use rustc_trait_selection::traits::{Obligation, ObligationCause, ObligationCtxt};
 use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::fs::File;
 use std::io::BufWriter;
@@ -410,6 +414,79 @@ fn autoharness_filtered_out(
     !included || excluded
 }
 
+/// The candidate types for instantiating the type parameters of a generic function, in the order
+/// in which we try them. We start with `i32` since that is Rust's default integer type, and
+/// primitive types satisfy the most common trait bounds (`Copy`, `Clone`, `Ord`, `Hash`,
+/// `Default`, `Debug`, etc.) as well as Kani's `Arbitrary`.
+fn generic_instantiation_candidates() -> Vec<Ty> {
+    vec![
+        Ty::from_rigid_kind(RigidTy::Int(IntTy::I32)),
+        Ty::from_rigid_kind(RigidTy::Uint(UintTy::U32)),
+        Ty::from_rigid_kind(RigidTy::Uint(UintTy::Usize)),
+        Ty::from_rigid_kind(RigidTy::Bool),
+        Ty::from_rigid_kind(RigidTy::Char),
+    ]
+}
+
+/// Check whether instantiating the generic parameters of `def` with `args` satisfies all of
+/// `def`'s predicates (trait bounds and where clauses).
+/// `args` must be fully monomorphic.
+fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool {
+    let infcx = tcx.infer_ctxt().build(TypingMode::PostAnalysis);
+    let ocx = ObligationCtxt::new(&infcx);
+    let param_env = ty::ParamEnv::empty();
+    let cause = ObligationCause::dummy();
+
+    let def_id = rustc_internal::internal(tcx, def.def_id());
+    let args_internal = rustc_internal::internal(tcx, args);
+    let predicates = tcx.predicates_of(def_id).instantiate(tcx, args_internal);
+    for (predicate, _span) in predicates {
+        ocx.register_obligation(Obligation::new(tcx, cause.clone(), param_env, predicate));
+    }
+    ocx.evaluate_obligations_error_on_ambiguity().is_empty()
+}
+
+/// Try to find a monomorphic instantiation of the generic function `fn_item` for which we can
+/// generate an automatic harness. Substitute each type parameter with the first candidate from
+/// `generic_instantiation_candidates` such that all of the function's trait bounds are satisfied
+/// (using the same candidate for every type parameter), and erase lifetime parameters.
+/// Return `None` if no candidate satisfies the bounds, or if the function has const generic
+/// parameters, which we do not support instantiating yet.
+fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Option<Instance> {
+    let TyKind::RigidTy(RigidTy::FnDef(def, identity_args)) = fn_item.ty().kind() else {
+        return None;
+    };
+
+    if identity_args.0.iter().any(|arg| matches!(arg, GenericArgKind::Const(_))) {
+        return None;
+    }
+
+    for candidate in generic_instantiation_candidates() {
+        let args = GenericArgs(
+            identity_args
+                .0
+                .iter()
+                .map(|arg| match arg {
+                    GenericArgKind::Type(_) => GenericArgKind::Type(candidate),
+                    GenericArgKind::Lifetime(_) => {
+                        GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased })
+                    }
+                    GenericArgKind::Const(_) => unreachable!("const generics filtered out above"),
+                })
+                .collect(),
+        );
+        if !args_satisfy_predicates(tcx, def, &args) {
+            continue;
+        }
+        if let Ok(instance) = Instance::resolve(def, &args)
+            && instance.has_body()
+        {
+            return Some(instance);
+        }
+    }
+    None
+}
+
 /// Partition every function in the crate into (chosen, skipped), where `chosen` is a vector of the Instances for which we'll generate automatic harnesses,
 /// and `skipped` is a map of function names to the reason why we skipped them.
 fn automatic_harness_partition(
@@ -435,21 +512,10 @@ fn automatic_harness_partition(
     // Cache whether a type implements or can derive Arbitrary
     let mut ty_arbitrary_cache: FxHashMap<Ty, bool> = FxHashMap::default();
 
-    // If `func` is not eligible for an automatic harness, return the reason why; if it is eligible, return None.
+    // If `instance` is not eligible for an automatic harness, return the reason why; if it is eligible, return None.
     // Note that we only return one reason for ineligiblity, when there could be multiple;
     // we can revisit this implementation choice in the future if users request more verbose output.
-    let mut skip_reason = |fn_item: CrateItem| -> Option<AutoHarnessSkipReason> {
-        if KaniAttributes::for_def_id(tcx, fn_item.def_id()).is_kani_instrumentation() {
-            return Some(AutoHarnessSkipReason::KaniImpl);
-        }
-
-        let instance = match Instance::try_from(fn_item) {
-            Ok(inst) => inst,
-            Err(_) => {
-                return Some(AutoHarnessSkipReason::GenericFn);
-            }
-        };
-
+    let mut skip_reason = |instance: Instance| -> Option<AutoHarnessSkipReason> {
         if !instance.has_body() {
             return Some(AutoHarnessSkipReason::NoBody);
         }
@@ -477,7 +543,8 @@ fn automatic_harness_partition(
         // Each argument of `instance` must be supported by automatic harness generation, i.e.,
         // implement Arbitrary (or be capable of deriving it), or be a raw pointer,
         // c.f. `autoharness_supported_arg_ty`.
-        // Note that we've already filtered out generic functions, so we know that each of these arguments has a concrete type.
+        // Note that generic functions have been instantiated with concrete types at this point,
+        // so we know that each of these arguments has a concrete type.
         let mut problematic_args = vec![];
         for (idx, arg) in body.arg_locals().iter().enumerate() {
             // Do not cache raw pointer types: `ty_arbitrary_cache` stores whether a type
@@ -521,10 +588,36 @@ fn automatic_harness_partition(
     let mut skipped = BTreeMap::new();
 
     for func in crate_fns {
-        if let Some(reason) = skip_reason(func) {
-            skipped.insert(crate::kani_middle::strip_local_crate_prefix(func.name()), reason);
+        if KaniAttributes::for_def_id(tcx, func.def_id()).is_kani_instrumentation() {
+            skipped.insert(
+                crate::kani_middle::strip_local_crate_prefix(func.name()),
+                AutoHarnessSkipReason::KaniImpl,
+            );
+            continue;
+        }
+
+        // For generic functions, try to find a monomorphic instantiation whose bounds are
+        // satisfied; the generated harness verifies the function for that instantiation only,
+        // and its name (e.g. `foo::<i32>`) reflects that.
+        let instance = match Instance::try_from(func) {
+            Ok(instance) => instance,
+            Err(_) => {
+                if let Some(instance) = choose_generic_instantiation(tcx, func) {
+                    instance
+                } else {
+                    skipped.insert(
+                        crate::kani_middle::strip_local_crate_prefix(func.name()),
+                        AutoHarnessSkipReason::GenericFn,
+                    );
+                    continue;
+                }
+            }
+        };
+
+        if let Some(reason) = skip_reason(instance) {
+            skipped.insert(crate::kani_middle::strip_local_crate_prefix(instance.name()), reason);
         } else {
-            chosen.push(Instance::try_from(func).unwrap());
+            chosen.push(instance);
         }
     }
 
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index d2348ab7b132..5f8287bf64dc 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/kani-compiler/src/kani_middle/metadata.rs
@@ -139,7 +139,11 @@ pub fn gen_automatic_proof_metadata(
 
     let kani_attributes = KaniAttributes::for_instance(tcx, *fn_to_verify);
     let harness_kind = if kani_attributes.has_contract() {
-        HarnessKind::ProofForContract { target_fn: pretty_name.clone() }
+        // Use the definition's name rather than the instance's (`pretty_name`), since the two
+        // differ for generic functions under contract (e.g. `foo::<i32>` vs. `foo`), and
+        // `gen_contracts_metadata` matches `target_fn` against the definition-level names stored
+        // in `ContractedFunction`.
+        HarnessKind::ProofForContract { target_fn: strip_local_crate_prefix(def.name()) }
     } else {
         HarnessKind::Proof
     };
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index cf00140c348c..f3d396fb4825 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -30,6 +30,7 @@ extern crate rustc_errors;
 extern crate rustc_hir;
 extern crate rustc_hir_pretty;
 extern crate rustc_index;
+extern crate rustc_infer;
 extern crate rustc_interface;
 extern crate rustc_metadata;
 extern crate rustc_middle;
@@ -40,6 +41,7 @@ extern crate rustc_public_bridge;
 extern crate rustc_session;
 extern crate rustc_span;
 extern crate rustc_target;
+extern crate rustc_trait_selection;
 // We can't add this directly as a dependency because we need the version to match rustc
 extern crate tempfile;
 
diff --git a/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected
index 9c006d210262..5a714b76557d 100644
--- a/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected
+++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected
@@ -1,29 +1,31 @@
-Kani generated automatic harnesses for 1 function(s):
-+---------------------------+-------------------+
-| Crate                     | Selected Function |
-+===============================================+
-| cargo_autoharness_include | include::simple   |
-+---------------------------+-------------------+
+Kani generated automatic harnesses for 2 function(s):
++---------------------------+-------------------------+
+| Crate                     | Selected Function       |
++=====================================================+
+| cargo_autoharness_include | include::generic::<i32> |
+|---------------------------+-------------------------|
+| cargo_autoharness_include | include::simple         |
++---------------------------+-------------------------+
 
-Kani did not generate automatic harnesses for 2 function(s).
+Kani did not generate automatic harnesses for 1 function(s).
 If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832
 +---------------------------+------------------+--------------------------------+
 | Crate                     | Skipped Function | Reason for Skipping            |
 +===============================================================================+
 | cargo_autoharness_include | excluded::simple | Did not match provided filters |
-|---------------------------+------------------+--------------------------------|
-| cargo_autoharness_include | include::generic | Generic Function               |
 +---------------------------+------------------+--------------------------------+
+Autoharness: Checking function include::generic::<i32> against all possible inputs...
 Autoharness: Checking function include::simple against all possible inputs...
-VERIFICATION:- SUCCESSFUL
 
 Manual Harness Summary:
 No proof harnesses (functions with #[kani::proof]) were found to verify.
 
 Autoharness Summary:
-+---------------------------+-------------------+---------------------------+---------------------+
-| Crate                     | Selected Function | Kind of Automatic Harness | Verification Result |
-+=================================================================================================+
-| cargo_autoharness_include | include::simple   | #[kani::proof]            | Success             |
-+---------------------------+-------------------+---------------------------+---------------------+
-Complete - 1 successfully verified functions, 0 failures, 1 total.
++---------------------------+-------------------------+---------------------------+---------------------+
+| Crate                     | Selected Function       | Kind of Automatic Harness | Verification Result |
++=======================================================================================================+
+| cargo_autoharness_include | include::generic::<i32> | #[kani::proof]            | Success             |
+|---------------------------+-------------------------+---------------------------+---------------------|
+| cargo_autoharness_include | include::simple         | #[kani::proof]            | Success             |
++---------------------------+-------------------------+---------------------------+---------------------+
+Complete - 2 successfully verified functions, 0 failures, 2 total.
diff --git a/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs
index 39676ed697ee..059459257292 100644
--- a/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs
+++ b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs
@@ -9,7 +9,7 @@ mod include {
         x
     }
 
-    // Doesn't implement Arbitrary, so still should not be included.
+    // Generic functions get instantiated with a concrete type (e.g. `i32`).
     fn generic<T>(x: u32, _y: T) -> u32 {
         x
     }
diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected
index be07996705f1..45736ebefcf3 100644
--- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected
+++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected
@@ -1,4 +1,4 @@
-Kani generated automatic harnesses for 46 function(s):
+Kani generated automatic harnesses for 47 function(s):
 +--------------------------+----------------------------------------------+
 | Crate                    | Selected Function                            |
 +=========================================================================+
@@ -24,6 +24,8 @@ Kani generated automatic harnesses for 46 function(s):
 |--------------------------+----------------------------------------------|
 | cargo_autoharness_filter | yes_harness::f_f64                           |
 |--------------------------+----------------------------------------------|
+| cargo_autoharness_filter | yes_harness::f_generic::<i32>                |
+|--------------------------+----------------------------------------------|
 | cargo_autoharness_filter | yes_harness::f_i128                          |
 |--------------------------+----------------------------------------------|
 | cargo_autoharness_filter | yes_harness::f_i16                           |
@@ -95,15 +97,13 @@ Kani generated automatic harnesses for 46 function(s):
 | cargo_autoharness_filter | yes_harness::f_usize                         |
 +--------------------------+----------------------------------------------+
 
-Kani did not generate automatic harnesses for 5 function(s).
+Kani did not generate automatic harnesses for 4 function(s).
 If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832
 +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+
 | Crate                    | Skipped Function                       | Reason for Skipping                                                              |
 +======================================================================================================================================================+
 | cargo_autoharness_filter | no_harness::doesnt_implement_arbitrary | Missing Arbitrary implementation for argument(s) x: DoesntImplementArbitrary<'_> |
 |--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
-| cargo_autoharness_filter | no_harness::unsupported_generic        | Generic Function                                                                 |
-|--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
 | cargo_autoharness_filter | no_harness::unsupported_no_arg_name    | Missing Arbitrary implementation for argument(s) _: std::vec::Vec<u8>            |
 |--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
 | cargo_autoharness_filter | no_harness::unsupported_slice          | Missing Arbitrary implementation for argument(s) _y: &[u8]                       |
@@ -112,6 +112,7 @@ If you believe that the provided reason is incorrect and Kani should have genera
 +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+
 Autoharness: Checking function yes_harness::f_mut_pointer against all possible inputs...
 Autoharness: Checking function yes_harness::f_const_pointer against all possible inputs...
+Autoharness: Checking function yes_harness::f_generic::<i32> against all possible inputs...
 Autoharness: Checking function yes_harness::f_ref against all possible inputs...
 Autoharness: Checking function yes_harness::empty_body against all possible inputs...
 Autoharness: Checking function yes_harness::f_phantom_pinned against all possible inputs...
@@ -186,6 +187,8 @@ Autoharness Summary:
 |--------------------------+----------------------------------------------+---------------------------+---------------------|
 | cargo_autoharness_filter | yes_harness::f_f64                           | #[kani::proof]            | Success             |
 |--------------------------+----------------------------------------------+---------------------------+---------------------|
+| cargo_autoharness_filter | yes_harness::f_generic::<i32>                | #[kani::proof]            | Success             |
+|--------------------------+----------------------------------------------+---------------------------+---------------------|
 | cargo_autoharness_filter | yes_harness::f_i128                          | #[kani::proof]            | Success             |
 |--------------------------+----------------------------------------------+---------------------------+---------------------|
 | cargo_autoharness_filter | yes_harness::f_i16                           | #[kani::proof]            | Success             |
@@ -256,4 +259,4 @@ Autoharness Summary:
 |--------------------------+----------------------------------------------+---------------------------+---------------------|
 | cargo_autoharness_filter | yes_harness::f_usize                         | #[kani::proof]            | Success             |
 +--------------------------+----------------------------------------------+---------------------------+---------------------+
-Complete - 46 successfully verified functions, 0 failures, 46 total.
+Complete - 47 successfully verified functions, 0 failures, 47 total.
diff --git a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs
index ab64688c0ba9..ce466568a4ae 100644
--- a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs
+++ b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs
@@ -200,13 +200,14 @@ mod yes_harness {
     fn f_mut_pointer(x: u32, _y: *mut i32) -> u32 {
         x
     }
+
+    fn f_generic<T>(x: u32, _y: T) -> u32 {
+        x
+    }
 }
 
 mod no_harness {
     use crate::{DerivesArbitrary, DoesntImplementArbitrary};
-    fn unsupported_generic<T>(x: u32, _y: T) -> u32 {
-        x
-    }
     fn unsupported_vec(x: u32, _y: Vec<u8>) -> u32 {
         x
     }
diff --git a/tests/script-based-pre/cargo_autoharness_generics/Cargo.toml b/tests/script-based-pre/cargo_autoharness_generics/Cargo.toml
new file mode 100644
index 000000000000..832b818ce535
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_generics/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_generics"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/cargo_autoharness_generics/config.yml b/tests/script-based-pre/cargo_autoharness_generics/config.yml
new file mode 100644
index 000000000000..3517a8b7d23d
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_generics/config.yml
@@ -0,0 +1,5 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: generics.sh
+expected: generics.expected
+exit_code: 1
diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.expected b/tests/script-based-pre/cargo_autoharness_generics/generics.expected
new file mode 100644
index 000000000000..e7f3b8d1098c
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_generics/generics.expected
@@ -0,0 +1,11 @@
+| cargo_autoharness_generics | needs_exotic     | Generic Function    |
+| cargo_autoharness_generics | with_const       | Generic Function    |
+| cargo_autoharness_generics | Wrapper::<i32>::get | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | contracted::<u32>   | #[kani::proof_for_contract] | Success             |
+| cargo_autoharness_generics | first::<i32>        | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | identity::<i32>     | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | max3::<i32>         | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | pair::<i32, i32>    | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | takes_impl::<u32>   | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | buggy_add::<i32>    | #[kani::proof]              | Failure             |
+Complete - 7 successfully verified functions, 1 failures, 8 total.
diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.sh b/tests/script-based-pre/cargo_autoharness_generics/generics.sh
new file mode 100755
index 000000000000..65f949b65ad3
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_generics/generics.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z autoharness -Z function-contracts
diff --git a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs
new file mode 100644
index 000000000000..e23c4cb46ccb
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs
@@ -0,0 +1,81 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that the autoharness subcommand supports generic functions by instantiating their type
+// parameters with a concrete type: the first candidate (starting from `i32`) that satisfies all
+// of the function's trait bounds. Lifetime parameters are erased; functions with const generic
+// parameters or with bounds that no candidate satisfies are skipped.
+// The "TEST NOTE" comments below explain the expected result for each function.
+
+// TEST NOTE: verified as `identity::<i32>`.
+pub fn identity<T>(x: T) -> T {
+    x
+}
+
+// TEST NOTE: verified as `max3::<i32>`; primitives satisfy the bounds.
+pub fn max3<T: Copy + PartialOrd>(a: T, b: T, c: T) -> T {
+    let mut m = a;
+    if b > m {
+        m = b;
+    }
+    if c > m {
+        m = c;
+    }
+    m
+}
+
+// TEST NOTE: verified as `buggy_add::<i32>` and FAILS, since the addition can overflow.
+// This demonstrates that instantiating a generic function can find real bugs.
+pub fn buggy_add<T: Copy + core::ops::Add<Output = T>>(a: T, b: T) -> T {
+    a + b
+}
+
+// TEST NOTE: verified as `pair::<i32, i32>`; multiple type parameters are supported.
+pub fn pair<T: Copy, U: Default>(x: T, _y: U) -> (T, U) {
+    (x, U::default())
+}
+
+// TEST NOTE: verified as `first::<i32>`; lifetime parameters are erased.
+pub fn first<'a, T: Copy>(x: &'a T) -> T {
+    *x
+}
+
+// TEST NOTE: verified as `takes_impl::<u32>`: `i32` does not satisfy `Into<u64>`,
+// so the next candidate that does (`u32`) is chosen.
+pub fn takes_impl(x: impl Into<u64> + Copy) -> u64 {
+    x.into()
+}
+
+// TEST NOTE: skipped (Generic Function), since no candidate type implements `Exotic`.
+pub trait Exotic {
+    fn exotic(&self) -> u8;
+}
+pub fn needs_exotic<T: Exotic>(x: T) -> u8 {
+    x.exotic()
+}
+
+// TEST NOTE: skipped (Generic Function), since we do not instantiate const generic
+// parameters yet.
+pub fn with_const<const N: usize>(_x: [u8; N]) -> usize {
+    N
+}
+
+// TEST NOTE: verified as `Wrapper::<i32>::get`; generic parameters of the impl block are
+// instantiated too.
+pub struct Wrapper<T> {
+    val: T,
+}
+
+impl<T: Copy> Wrapper<T> {
+    pub fn get(&self) -> T {
+        self.val
+    }
+}
+
+// TEST NOTE: verified as `contracted::<u32>` with a contract harness; the contract is checked
+// for the chosen instantiation.
+#[kani::requires(x < 1000)]
+#[kani::ensures(|r| *r >= x)]
+pub fn contracted<T: Copy + Into<u64>>(_marker: T, x: u64) -> u64 {
+    x + 1
+}
diff --git a/tests/script-based-pre/cargo_autoharness_include/include.expected b/tests/script-based-pre/cargo_autoharness_include/include.expected
index 9c006d210262..5a714b76557d 100644
--- a/tests/script-based-pre/cargo_autoharness_include/include.expected
+++ b/tests/script-based-pre/cargo_autoharness_include/include.expected
@@ -1,29 +1,31 @@
-Kani generated automatic harnesses for 1 function(s):
-+---------------------------+-------------------+
-| Crate                     | Selected Function |
-+===============================================+
-| cargo_autoharness_include | include::simple   |
-+---------------------------+-------------------+
+Kani generated automatic harnesses for 2 function(s):
++---------------------------+-------------------------+
+| Crate                     | Selected Function       |
++=====================================================+
+| cargo_autoharness_include | include::generic::<i32> |
+|---------------------------+-------------------------|
+| cargo_autoharness_include | include::simple         |
++---------------------------+-------------------------+
 
-Kani did not generate automatic harnesses for 2 function(s).
+Kani did not generate automatic harnesses for 1 function(s).
 If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832
 +---------------------------+------------------+--------------------------------+
 | Crate                     | Skipped Function | Reason for Skipping            |
 +===============================================================================+
 | cargo_autoharness_include | excluded::simple | Did not match provided filters |
-|---------------------------+------------------+--------------------------------|
-| cargo_autoharness_include | include::generic | Generic Function               |
 +---------------------------+------------------+--------------------------------+
+Autoharness: Checking function include::generic::<i32> against all possible inputs...
 Autoharness: Checking function include::simple against all possible inputs...
-VERIFICATION:- SUCCESSFUL
 
 Manual Harness Summary:
 No proof harnesses (functions with #[kani::proof]) were found to verify.
 
 Autoharness Summary:
-+---------------------------+-------------------+---------------------------+---------------------+
-| Crate                     | Selected Function | Kind of Automatic Harness | Verification Result |
-+=================================================================================================+
-| cargo_autoharness_include | include::simple   | #[kani::proof]            | Success             |
-+---------------------------+-------------------+---------------------------+---------------------+
-Complete - 1 successfully verified functions, 0 failures, 1 total.
++---------------------------+-------------------------+---------------------------+---------------------+
+| Crate                     | Selected Function       | Kind of Automatic Harness | Verification Result |
++=======================================================================================================+
+| cargo_autoharness_include | include::generic::<i32> | #[kani::proof]            | Success             |
+|---------------------------+-------------------------+---------------------------+---------------------|
+| cargo_autoharness_include | include::simple         | #[kani::proof]            | Success             |
++---------------------------+-------------------------+---------------------------+---------------------+
+Complete - 2 successfully verified functions, 0 failures, 2 total.
diff --git a/tests/script-based-pre/cargo_autoharness_include/src/lib.rs b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs
index 135f86f76874..38f69c4390e4 100644
--- a/tests/script-based-pre/cargo_autoharness_include/src/lib.rs
+++ b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs
@@ -10,7 +10,7 @@ mod include {
         x
     }
 
-    // Doesn't implement Arbitrary, so still should not be included.
+    // Generic functions get instantiated with a concrete type (e.g. `i32`).
     fn generic<T>(x: u32, _y: T) -> u32 {
         x
     }

From 0e62ab0a80e6392cb969abc2a509dbf10bd4d8c3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 28 Jul 2026 22:06:18 +0000
Subject: [PATCH 2/4] Report why a generic function could not be instantiated

Rather than the single 'Generic Function' skip reason, attach a detail
explaining what prevented instantiation: const generic parameters, or that
no candidate type satisfies the function's trait bounds. This makes the
skipped-functions table actionable and allows corpus evaluations to
classify the generic-function gap precisely.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Signed-off-by: Felipe Monteiro <felisous@amazon.com>
---
 .../src/kani_middle/codegen_units.rs          | 33 +++++++++++--------
 kani-driver/src/autoharness/mod.rs            |  7 ++--
 kani_metadata/src/lib.rs                      |  6 ++--
 .../generics.expected                         |  4 +--
 4 files changed, 30 insertions(+), 20 deletions(-)

diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index 6459d7077434..020861fba72b 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -450,15 +450,16 @@ fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool
 /// generate an automatic harness. Substitute each type parameter with the first candidate from
 /// `generic_instantiation_candidates` such that all of the function's trait bounds are satisfied
 /// (using the same candidate for every type parameter), and erase lifetime parameters.
-/// Return `None` if no candidate satisfies the bounds, or if the function has const generic
-/// parameters, which we do not support instantiating yet.
-fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Option<Instance> {
+/// Return the reason (to be attached to [AutoHarnessSkipReason::GenericFn]) if no candidate
+/// satisfies the bounds, or if the function has const generic parameters, which we do not
+/// support instantiating yet.
+fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result<Instance, String> {
     let TyKind::RigidTy(RigidTy::FnDef(def, identity_args)) = fn_item.ty().kind() else {
-        return None;
+        return Err("not a function definition".to_string());
     };
 
     if identity_args.0.iter().any(|arg| matches!(arg, GenericArgKind::Const(_))) {
-        return None;
+        return Err("const generic parameters are not supported yet".to_string());
     }
 
     for candidate in generic_instantiation_candidates() {
@@ -481,10 +482,17 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Option<Insta
         if let Ok(instance) = Instance::resolve(def, &args)
             && instance.has_body()
         {
-            return Some(instance);
+            return Ok(instance);
         }
     }
-    None
+    Err(format!(
+        "no candidate type ({}) satisfies the function's trait bounds",
+        generic_instantiation_candidates()
+            .iter()
+            .map(|ty| ty.to_string())
+            .collect::<Vec<_>>()
+            .join(", ")
+    ))
 }
 
 /// Partition every function in the crate into (chosen, skipped), where `chosen` is a vector of the Instances for which we'll generate automatic harnesses,
@@ -601,17 +609,16 @@ fn automatic_harness_partition(
         // and its name (e.g. `foo::<i32>`) reflects that.
         let instance = match Instance::try_from(func) {
             Ok(instance) => instance,
-            Err(_) => {
-                if let Some(instance) = choose_generic_instantiation(tcx, func) {
-                    instance
-                } else {
+            Err(_) => match choose_generic_instantiation(tcx, func) {
+                Ok(instance) => instance,
+                Err(detail) => {
                     skipped.insert(
                         crate::kani_middle::strip_local_crate_prefix(func.name()),
-                        AutoHarnessSkipReason::GenericFn,
+                        AutoHarnessSkipReason::GenericFn(detail),
                     );
                     continue;
                 }
-            }
+            },
         };
 
         if let Some(reason) = skip_reason(instance) {
diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs
index 2e339a588f0a..0e94590e6441 100644
--- a/kani-driver/src/autoharness/mod.rs
+++ b/kani-driver/src/autoharness/mod.rs
@@ -106,9 +106,10 @@ fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
                             .join(", ")
                     ),
                 ]),
-                AutoHarnessSkipReason::GenericFn
-                | AutoHarnessSkipReason::NoBody
-                | AutoHarnessSkipReason::UserFilter => {
+                AutoHarnessSkipReason::GenericFn(ref detail) => {
+                    Some(vec![md.crate_name.clone(), func, format!("{reason}: {detail}")])
+                }
+                AutoHarnessSkipReason::NoBody | AutoHarnessSkipReason::UserFilter => {
                     Some(vec![md.crate_name.clone(), func, reason.to_string()])
                 }
                 // We don't report Kani implementations to the user to avoid exposing Kani functions we insert during instrumentation.
diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs
index 2117c04aac17..4e7fa0d2694b 100644
--- a/kani_metadata/src/lib.rs
+++ b/kani_metadata/src/lib.rs
@@ -55,9 +55,11 @@ pub struct AutoHarnessMetadata {
 /// Reasons that Kani does not generate an automatic harness for a function.
 #[derive(Debug, Clone, Serialize, Deserialize, Display, EnumString)]
 pub enum AutoHarnessSkipReason {
-    /// The function is generic.
+    /// The function is generic and autoharness could not find a monomorphic instantiation to
+    /// verify. The payload gives the specific reason (e.g. const generic parameters, or trait
+    /// bounds that no candidate type satisfies).
     #[strum(serialize = "Generic Function")]
-    GenericFn,
+    GenericFn(String),
     /// A Kani-internal function: already a harness, implementation of a Kani associated item or Kani contract instrumentation functions).
     #[strum(serialize = "Kani implementation")]
     KaniImpl,
diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.expected b/tests/script-based-pre/cargo_autoharness_generics/generics.expected
index e7f3b8d1098c..4263f74b0479 100644
--- a/tests/script-based-pre/cargo_autoharness_generics/generics.expected
+++ b/tests/script-based-pre/cargo_autoharness_generics/generics.expected
@@ -1,5 +1,5 @@
-| cargo_autoharness_generics | needs_exotic     | Generic Function    |
-| cargo_autoharness_generics | with_const       | Generic Function    |
+| cargo_autoharness_generics | needs_exotic     | Generic Function: no candidate type (i32, u32, usize, bool, char) satisfies the function's trait bounds |
+| cargo_autoharness_generics | with_const       | Generic Function: const generic parameters are not supported yet                                        |
 | cargo_autoharness_generics | Wrapper::<i32>::get | #[kani::proof]              | Success             |
 | cargo_autoharness_generics | contracted::<u32>   | #[kani::proof_for_contract] | Success             |
 | cargo_autoharness_generics | first::<i32>        | #[kani::proof]              | Success             |

From 0cdf3bce3afa553964eca9982db8f5c632ceef66 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 29 Jul 2026 14:06:34 +0000
Subject: [PATCH 3/4] Autoharness: instantiate usize const generic parameters

Instantiate usize const generic parameters (by far the most common case,
e.g. array lengths) with the value 2, alongside the existing type-parameter
instantiation; the summary table shows the chosen value as part of the
instantiated name (e.g. with_const::<2>). Non-usize const parameters are
still skipped, now with a precise reason; the check consults the internal
generics since the public identity arguments do not carry the parameter's
type.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Signed-off-by: Felipe Monteiro <felisous@amazon.com>
---
 .../src/reference/experimental/autoharness.md |  4 ++-
 .../src/kani_middle/codegen_units.rs          | 25 ++++++++++++++++---
 .../generics.expected                         |  5 ++--
 .../cargo_autoharness_generics/src/lib.rs     | 14 ++++++++---
 4 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index 02347db03902..90e21f54ed3e 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -176,9 +176,11 @@ Note that verifying a single instantiation is an underapproximation of all of th
 a successful result for `foo::<i32>` does not imply that other instantiations of `foo` are also safe.
 Kani makes this explicit by displaying the instantiated name of the verified function.
 
+`usize` const generic parameters (e.g. array lengths) are instantiated with the value 2.
+
 Kani skips a generic function (with skip reason "Generic Function") if:
 - no candidate type satisfies the function's trait bounds, or
-- the function has const generic parameters, which Kani does not instantiate yet.
+- the function has non-`usize` const generic parameters, which Kani does not instantiate yet.
 
 If some caller of a generic function is eligible for an automatic harness, then additional monomorphized
 versions of the generic function may still be reachable (and thus verified) through the caller's harness.
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index 020861fba72b..18fd0cda8f7a 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -29,7 +29,8 @@ use rustc_middle::ty::{self, TyCtxt, TypingMode};
 use rustc_public::mir::mono::Instance;
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
-    FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy,
+    FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyConst, TyKind,
+    UintTy,
 };
 use rustc_public::{CrateDef, CrateItem};
 use rustc_public_bridge::IndexedVal;
@@ -414,6 +415,12 @@ fn autoharness_filtered_out(
     !included || excluded
 }
 
+/// The value used to instantiate `usize` const generic parameters of generic functions
+/// (e.g. array lengths). As with the choice of type-parameter candidates, verifying a single
+/// instantiation underapproximates the function's behaviors; the summary table shows the
+/// chosen value as part of the instantiated name.
+const AUTOHARNESS_CONST_GENERIC_VALUE: u64 = 2;
+
 /// The candidate types for instantiating the type parameters of a generic function, in the order
 /// in which we try them. We start with `i32` since that is Rust's default integer type, and
 /// primitive types satisfy the most common trait bounds (`Copy`, `Clone`, `Ord`, `Hash`,
@@ -458,8 +465,16 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result<Insta
         return Err("not a function definition".to_string());
     };
 
-    if identity_args.0.iter().any(|arg| matches!(arg, GenericArgKind::Const(_))) {
-        return Err("const generic parameters are not supported yet".to_string());
+    // Const generic parameters of type usize (by far the most common case, e.g. array lengths)
+    // are instantiated with AUTOHARNESS_CONST_GENERIC_VALUE; other const parameter types are
+    // not supported yet. The check consults the internal generics (the public identity
+    // arguments do not carry the parameter's type).
+    let generics = tcx.generics_of(rustc_internal::internal(tcx, def.def_id()));
+    if generics.own_params.iter().any(|param| {
+        matches!(param.kind, rustc_middle::ty::GenericParamDefKind::Const { .. })
+            && tcx.type_of(param.def_id).skip_binder() != tcx.types.usize
+    }) {
+        return Err("non-usize const generic parameters are not supported yet".to_string());
     }
 
     for candidate in generic_instantiation_candidates() {
@@ -472,7 +487,9 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result<Insta
                     GenericArgKind::Lifetime(_) => {
                         GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased })
                     }
-                    GenericArgKind::Const(_) => unreachable!("const generics filtered out above"),
+                    GenericArgKind::Const(_) => GenericArgKind::Const(
+                        TyConst::try_from_target_usize(AUTOHARNESS_CONST_GENERIC_VALUE).unwrap(),
+                    ),
                 })
                 .collect(),
         );
diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.expected b/tests/script-based-pre/cargo_autoharness_generics/generics.expected
index 4263f74b0479..4aebef62731c 100644
--- a/tests/script-based-pre/cargo_autoharness_generics/generics.expected
+++ b/tests/script-based-pre/cargo_autoharness_generics/generics.expected
@@ -1,5 +1,5 @@
 | cargo_autoharness_generics | needs_exotic     | Generic Function: no candidate type (i32, u32, usize, bool, char) satisfies the function's trait bounds |
-| cargo_autoharness_generics | with_const       | Generic Function: const generic parameters are not supported yet                                        |
+| cargo_autoharness_generics | with_bool_const  | Generic Function: non-usize const generic parameters are not supported yet                              |
 | cargo_autoharness_generics | Wrapper::<i32>::get | #[kani::proof]              | Success             |
 | cargo_autoharness_generics | contracted::<u32>   | #[kani::proof_for_contract] | Success             |
 | cargo_autoharness_generics | first::<i32>        | #[kani::proof]              | Success             |
@@ -7,5 +7,6 @@
 | cargo_autoharness_generics | max3::<i32>         | #[kani::proof]              | Success             |
 | cargo_autoharness_generics | pair::<i32, i32>    | #[kani::proof]              | Success             |
 | cargo_autoharness_generics | takes_impl::<u32>   | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | with_const::<2>     | #[kani::proof]              | Success             |
 | cargo_autoharness_generics | buggy_add::<i32>    | #[kani::proof]              | Failure             |
-Complete - 7 successfully verified functions, 1 failures, 8 total.
+Complete - 8 successfully verified functions, 1 failures, 9 total.
diff --git a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs
index e23c4cb46ccb..b690193d2da5 100644
--- a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs
+++ b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs
@@ -54,10 +54,16 @@ pub fn needs_exotic<T: Exotic>(x: T) -> u8 {
     x.exotic()
 }
 
-// TEST NOTE: skipped (Generic Function), since we do not instantiate const generic
-// parameters yet.
-pub fn with_const<const N: usize>(_x: [u8; N]) -> usize {
-    N
+// TEST NOTE: verified as `with_const::<2>`; usize const generic parameters are instantiated
+// with the value 2.
+pub fn with_const<const N: usize>(x: [u8; N]) -> usize {
+    x.len() + N
+}
+
+// TEST NOTE: skipped (Generic Function), since non-usize const generic parameters are not
+// supported yet.
+pub fn with_bool_const<const B: bool>(x: u8) -> u8 {
+    if B { x } else { 0 }
 }
 
 // TEST NOTE: verified as `Wrapper::<i32>::get`; generic parameters of the impl block are

From 4ea9fac133b63521eda2d844c86e566bd9413942 Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Fri, 21 Aug 2026 18:49:07 +0000
Subject: [PATCH 4/4] Autoharness: report body-less generic instantiations as
 NoBody

choose_generic_instantiation previously only returned an instance when it
had a body, so a generic function without a body (e.g. a generic trait
method without a default) fell through and was reported with a generic
skip reason. Return the resolved instance regardless of has_body() and let
skip_reason report NoBody, matching the behavior for non-generic body-less
functions.

Addresses a review comment on #4679.

Signed-off-by: Felipe Monteiro <felisous@amazon.com>
---
 kani-compiler/src/kani_middle/codegen_units.rs | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index 18fd0cda8f7a..c5af5b120699 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -496,9 +496,11 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result<Insta
         if !args_satisfy_predicates(tcx, def, &args) {
             continue;
         }
-        if let Ok(instance) = Instance::resolve(def, &args)
-            && instance.has_body()
-        {
+        // Return the resolved instance regardless of whether it has a body: a body-less
+        // instance (e.g. a generic trait method without a default) is then reported accurately
+        // as `NoBody` by `skip_reason`, rather than falling through to a generic-function skip
+        // reason here.
+        if let Ok(instance) = Instance::resolve(def, &args) {
             return Ok(instance);
         }
     }