From 8386444eee381adf1cb774895e8f43ec0a1273d2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 29 Jul 2026 08:41:29 +0000
Subject: [PATCH 1/3] Autoharness: support BoundedArbitrary argument types

Functions taking owned container arguments like Vec<T> or String were
skipped with 'Missing Arbitrary implementation', even though Kani already
ships BoundedArbitrary implementations for exactly these types (and a
derive macro for user types).

Reuse that machinery directly: when an argument type does not implement
(and cannot derive) Arbitrary, but does implement BoundedArbitrary --
detected by the same Instance-resolution approach as implements_arbitrary,
via a new fn_marker on kani::bounded_any -- the generated harness calls
kani::bounded_any::<T, 4>() instead of kani::any(). This covers Vec<T>,
String, Box<[T]>, and user types deriving BoundedArbitrary.

The bound of 4 reflects measured verification cost: BoundedArbitrary values
are heap allocated, and String's implementation reasons about UTF-8
validity; a bound of 8 already makes simple String harnesses exceed Kani's
default 60s harness timeout. As with slices and strings, the
only-valid-up-to-the-bound caveat is documented in the autoharness
reference.

The eligibility loop no longer inserts top-level argument verdicts into the
shared Arbitrary cache at all: argument-position support (slice references,
BoundedArbitrary containers) differs from field-position support, and
implements_arbitrary already memoizes its own recursion, so the top-level
memoization was both redundant and a poisoning hazard.

Towards #3832

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .../src/reference/experimental/autoharness.md |  8 +++
 .../src/kani_middle/codegen_units.rs          | 22 ++++---
 .../src/kani_middle/kani_functions.rs         |  2 +
 kani-compiler/src/kani_middle/mod.rs          | 58 +++++++++++++++++--
 .../src/kani_middle/transform/automatic.rs    | 51 +++++++++++++---
 library/kani_core/src/lib.rs                  |  1 +
 .../cargo_autoharness_bounded/Cargo.toml      | 10 ++++
 .../bounded.expected                          | 13 +++++
 .../cargo_autoharness_bounded/bounded.sh      |  8 +++
 .../cargo_autoharness_bounded/config.yml      |  5 ++
 .../cargo_autoharness_bounded/src/lib.rs      | 53 +++++++++++++++++
 11 files changed, 211 insertions(+), 20 deletions(-)
 create mode 100644 tests/script-based-pre/cargo_autoharness_bounded/Cargo.toml
 create mode 100644 tests/script-based-pre/cargo_autoharness_bounded/bounded.expected
 create mode 100755 tests/script-based-pre/cargo_autoharness_bounded/bounded.sh
 create mode 100644 tests/script-based-pre/cargo_autoharness_bounded/config.yml
 create mode 100644 tests/script-based-pre/cargo_autoharness_bounded/src/lib.rs

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index a1376d8fdd2..5b1e77c223a 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -165,6 +165,14 @@ smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution.
 chosen to stay below the default loop-unwinding bound of 20, so that loops over the slice can
 be fully unwound by default.
 
+Additionally (also requiring `--bounded-arguments`), for arguments whose type implements
+[`BoundedArbitrary`](https://model-checking.github.io/kani/reference/experimental/bounded-arbitrary.html)
+(e.g. `Vec<T>`, `String`, or user types deriving it), the harness generates a bounded
+nondeterministic value with **bound 4** (via `kani::bounded_any`). The same caveat applies:
+verification results only hold up to the bound. The smaller bound reflects that these values are
+heap allocated and, for `String`, involve UTF-8 reasoning, both of which are costly for symbolic
+execution.
+
 Nested slice references (e.g. `&&[u8]`) and slices inside user-defined types remain unsupported.
 
 ## Limitations
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index bd20dbc30a2..e5e97c01b76 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -108,6 +108,7 @@ impl CodegenUnits {
                     args,
                     &crate_info.name,
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
+                    *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(),
                 );
                 AUTOHARNESS_MD
                     .set(AutoHarnessMetadata {
@@ -524,6 +525,7 @@ fn automatic_harness_partition(
     args: &Arguments,
     crate_name: &str,
     kani_any_def: FnDef,
+    kani_bounded_any_def: FnDef,
 ) -> (Vec<(Instance, bool)>, BTreeMap<String, AutoHarnessSkipReason>) {
     let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::<FxHashSet<_>>();
     // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions
@@ -574,8 +576,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), be a raw pointer, or -- if the user
-        // opted in via --bounded-arguments -- be a supported slice/string reference,
-        // c.f. `autoharness_supported_arg_ty`.
+        // opted in via --bounded-arguments -- be a supported slice/string reference or a
+        // BoundedArbitrary container type, c.f. `autoharness_supported_arg_ty`.
         // 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![];
@@ -584,12 +586,16 @@ fn automatic_harness_partition(
             // Note: we deliberately do not insert the verdict into `ty_arbitrary_cache` here.
             // The cache stores whether a type implements (or can derive) Arbitrary, which is the
             // wrong semantics for types that are supported in argument position only (raw
-            // pointers, and slice/string references whose backing storage the harness owns):
-            // caching the argument-position verdict under the same key would poison the cache for
-            // the ADT-field checks. `implements_arbitrary` memoizes its own recursion internally,
-            // so repeated argument types stay cheap.
-            let support =
-                autoharness_supported_arg_ty(arg.ty, kani_any_def, &mut ty_arbitrary_cache);
+            // pointers, slice/string references whose backing storage the harness owns, and
+            // BoundedArbitrary container types): caching the argument-position verdict under the
+            // same key would poison the cache for the ADT-field checks. `implements_arbitrary`
+            // memoizes its own recursion internally, so repeated argument types stay cheap.
+            let support = autoharness_supported_arg_ty(
+                arg.ty,
+                kani_any_def,
+                kani_bounded_any_def,
+                &mut ty_arbitrary_cache,
+            );
 
             if support == ArgSupport::Arbitrary {
                 continue;
diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs
index b4ea258288a..6b7cc8da30d 100644
--- a/kani-compiler/src/kani_middle/kani_functions.rs
+++ b/kani-compiler/src/kani_middle/kani_functions.rs
@@ -75,6 +75,8 @@ pub enum KaniModel {
     AnyStrRef,
     #[strum(serialize = "AssumeSafeModel")]
     AssumeSafe,
+    #[strum(serialize = "BoundedAnyModel")]
+    BoundedAny,
     #[strum(serialize = "CopyInitStateModel")]
     CopyInitState,
     #[strum(serialize = "CopyInitStateSingleModel")]
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 62e301ee9b0..23fd130394b 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -13,7 +13,8 @@ use rustc_public::mir::mono::{Instance, MonoItem};
 use rustc_public::mir::{Mutability, TerminatorKind};
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
-    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyKind,
+    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyConst,
+    TyKind,
 };
 use rustc_public::visitor::{Visitable, Visitor as TyVisitor};
 use rustc_public::{CrateDef, DefId, local_crate};
@@ -348,6 +349,45 @@ fn implements_invariant(
     res
 }
 
+/// Inspect a `kani::bounded_any::<T, N>()` (c.f. `KaniModel::BoundedAny`) instantiation to
+/// determine if `T: BoundedArbitrary`. The model looks like:
+/// ```rust
+/// fn bounded_any<T: BoundedArbitrary, const N: usize>() -> T {
+///   T::bounded_any::<N>()
+/// }
+/// ```
+/// So we select the terminator that calls `T::bounded_any::<N>()`, then try to resolve it to an
+/// Instance; `T` implements `BoundedArbitrary` iff we successfully resolve the Instance
+/// (mirroring `implements_arbitrary`).
+fn implements_bounded_arbitrary(ty: Ty, kani_bounded_any_def: FnDef) -> bool {
+    if ty.kind().rigid().is_none() {
+        return false;
+    }
+
+    let args = GenericArgs(vec![
+        GenericArgKind::Type(ty),
+        GenericArgKind::Const(TyConst::try_from_target_usize(1).unwrap()),
+    ]);
+    let Ok(instance) = Instance::resolve(kani_bounded_any_def, &args) else {
+        return false;
+    };
+    let Some(body) = instance.body() else {
+        return false;
+    };
+
+    for bb in body.blocks.iter() {
+        let TerminatorKind::Call { func, .. } = &bb.terminator.kind else {
+            continue;
+        };
+        if let TyKind::RigidTy(RigidTy::FnDef(def, args)) =
+            func.ty(body.arg_locals()).unwrap().kind()
+        {
+            return Instance::resolve(def, &args).is_ok();
+        }
+    }
+    false
+}
+
 /// Is `ty` a struct or enum whose fields/variants implement Arbitrary, or a reference to such a
 /// type?
 fn can_derive_arbitrary(
@@ -422,7 +462,10 @@ pub enum ArgSupport {
 /// - slice references (`&[T]`/`&mut [T]`, provided `T` implements or can derive `Arbitrary`) and
 ///   string slices (`&str`): for those, the harness generates a slice of *bounded* nondeterministic
 ///   length backed by harness-local storage, c.f. `KaniModel::AnySliceRef` and
-///   `KaniModel::AnyStrRef`.
+///   `KaniModel::AnyStrRef` (reported as [ArgSupport::Bounded]);
+/// - types that implement `BoundedArbitrary` (e.g. `Vec<T>`, `String`, or user types deriving
+///   it): the harness generates a bounded nondeterministic value via `KaniModel::BoundedAny`
+///   (reported as [ArgSupport::Bounded]).
 ///
 /// Note that raw pointers and slice/string references are only supported as immediate harness
 /// arguments (raw pointers also through other raw pointers): such a type behind a reference or
@@ -431,6 +474,7 @@ pub enum ArgSupport {
 fn autoharness_supported_arg_ty(
     ty: Ty,
     kani_any_def: FnDef,
+    kani_bounded_any_def: FnDef,
     ty_arbitrary_cache: &mut FxHashMap<Ty, bool>,
 ) -> ArgSupport {
     let arbitrary_or_derive = |ty: Ty, cache: &mut FxHashMap<Ty, bool>| {
@@ -446,7 +490,7 @@ fn autoharness_supported_arg_ty(
     if let TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) = ty.kind() {
         // A raw pointer is supported as long as its pointee is: propagate the pointee's verdict,
         // so a pointer to a bounded pointee (e.g. `*mut &[T]`) is itself reported as bounded.
-        autoharness_supported_arg_ty(inner_ty, kani_any_def, ty_arbitrary_cache)
+        autoharness_supported_arg_ty(inner_ty, kani_any_def, kani_bounded_any_def, ty_arbitrary_cache)
     } else if let TyKind::RigidTy(RigidTy::Ref(_, inner_ty, inner_mutability)) = ty.kind() {
         match inner_ty.kind() {
             TyKind::RigidTy(RigidTy::Slice(elem_ty)) => {
@@ -468,6 +512,12 @@ fn autoharness_supported_arg_ty(
             _ => arbitrary_or_derive(ty, ty_arbitrary_cache),
         }
     } else {
-        arbitrary_or_derive(ty, ty_arbitrary_cache)
+        if arbitrary_or_derive(ty, ty_arbitrary_cache) == ArgSupport::Arbitrary {
+            ArgSupport::Arbitrary
+        } else if implements_bounded_arbitrary(ty, kani_bounded_any_def) {
+            ArgSupport::Bounded
+        } else {
+            ArgSupport::Unsupported
+        }
     }
 }
diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs
index cabf24ebe37..5b03e540cbc 100644
--- a/kani-compiler/src/kani_middle/transform/automatic.rs
+++ b/kani-compiler/src/kani_middle/transform/automatic.rs
@@ -12,7 +12,7 @@ use crate::kani_middle::codegen_units::CodegenUnit;
 use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel};
 use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
-use crate::kani_middle::{implements_arbitrary, implements_invariant};
+use crate::kani_middle::{can_derive_arbitrary, implements_arbitrary, implements_invariant};
 use crate::kani_queries::QueryDb;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::TyCtxt;
@@ -44,6 +44,8 @@ struct AnyModels {
     kani_any_str_ref: FnDef,
     /// The FnDef of KaniModel::AssumeSafe
     kani_assume_safe: FnDef,
+    /// The FnDef of KaniModel::BoundedAny
+    kani_bounded_any: FnDef,
 }
 
 impl AnyModels {
@@ -55,6 +57,7 @@ impl AnyModels {
             kani_any_slice_ref: *kani_fns.get(&KaniModel::AnySliceRef.into()).unwrap(),
             kani_any_str_ref: *kani_fns.get(&KaniModel::AnyStrRef.into()).unwrap(),
             kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(),
+            kani_bounded_any: *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(),
         }
     }
 }
@@ -172,6 +175,14 @@ const AUTOHARNESS_SLICE_BOUND: u64 = 16;
 /// not time out should raise `--harness-timeout`).
 const AUTOHARNESS_STR_BOUND: u64 = 4;
 
+/// The bound for nondeterministic values of types that implement `BoundedArbitrary` (rather
+/// than `Arbitrary`) that automatic harnesses generate, e.g. `Vec<T>` or `String`.
+/// Verification results for functions with such arguments are only valid up to this bound.
+/// This is smaller than the slice/str bounds since `BoundedArbitrary` values are heap
+/// allocated, and for `String` additionally involve UTF-8 reasoning; a bound of 8 already
+/// makes simple `String` harnesses exceed Kani's default 60s harness timeout.
+const AUTOHARNESS_BOUNDED_ANY_BOUND: u64 = 4;
+
 /// For raw pointer types, insert a call to the `KaniModel::AnyPtr` model instead, which generates
 /// a pointer in a nondeterministic allocation state (null, out of bounds, or valid);
 /// in the valid case, the pointer points to a nondeterministic value stored in a dedicated local
@@ -180,12 +191,15 @@ const AUTOHARNESS_STR_BOUND: u64 = 4;
 /// models instead, which return a slice of nondeterministic length (bounded by
 /// [AUTOHARNESS_SLICE_BOUND]) backed by a nondeterministic array stored in a dedicated local,
 /// which stays alive for the entire harness.
+/// If `ty` does not implement `Arbitrary` (and cannot derive it) but implements `BoundedArbitrary`
+/// (e.g. `Vec<T>` or `String`), insert a call to the `KaniModel::BoundedAny` model, which returns
+/// a *bounded* nondeterministic value (bounded by [AUTOHARNESS_BOUNDED_ANY_BOUND]).
 /// If `ty` is an ADT that implements `Invariant`, additionally insert a call to the
 /// `KaniModel::AssumeSafe` model (`kani_assume_safe`), which assumes that the nondeterministic
 /// value respects the type's safety invariant, c.f.
 /// <https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#validity-and-safety-invariant>.
-/// Panics if `ty` does not implement Arbitrary (and is not a reference or raw pointer to such a
-/// type, or a reference to a slice or str of such a type).
+/// Panics if `ty` does not implement Arbitrary or BoundedArbitrary (and is not a reference or raw
+/// pointer to such a type, or a reference to a slice or str of such a type).
 fn call_kani_any_for_ty(
     models: AnyModels,
     body: &mut MutableBody,
@@ -367,16 +381,37 @@ fn call_kani_any_for_ty(
             ptr_lcl
         }
     } else {
-        let kani_any_inst =
-            Instance::resolve(models.kani_any, &GenericArgs(vec![GenericArgKind::Type(ty)]))
-                .unwrap_or_else(|_| panic!("expected a ty that implements Arbitrary, got {ty}"));
+        // Prefer an unbounded nondeterministic value via (implemented or compiler-derived)
+        // Arbitrary; fall back to BoundedArbitrary for container types like Vec<T> or String.
+        // Note: use a fresh cache for the Arbitrary check -- `invariant_cache` memoizes a
+        // different predicate (Invariant), so the two must not share a map.
+        let mut arbitrary_cache = FxHashMap::default();
+        let use_arbitrary = implements_arbitrary(ty, models.kani_any, &mut arbitrary_cache)
+            || can_derive_arbitrary(ty, models.kani_any, &mut arbitrary_cache);
+        let (model, generic_args) = if use_arbitrary {
+            (models.kani_any, GenericArgs(vec![GenericArgKind::Type(ty)]))
+        } else {
+            (
+                models.kani_bounded_any,
+                GenericArgs(vec![
+                    GenericArgKind::Type(ty),
+                    GenericArgKind::Const(
+                        TyConst::try_from_target_usize(AUTOHARNESS_BOUNDED_ANY_BOUND).unwrap(),
+                    ),
+                ]),
+            )
+        };
+        let any_inst = Instance::resolve(model, &generic_args).unwrap_or_else(|_| {
+            panic!("expected a ty that implements Arbitrary or BoundedArbitrary, got {ty}")
+        });
         let lcl = body.new_local(ty, source.span(body.blocks()), mutability);
-        body.insert_call(&kani_any_inst, source, InsertPosition::Before, vec![], Place::from(lcl));
+        body.insert_call(&any_inst, source, InsertPosition::Before, vec![], Place::from(lcl));
 
         // If the type has a safety invariant, assume that it holds for the nondeterministic value.
         // We only check ADTs since those are the only types for which users can implement
         // `Invariant` in a way that constrains the values (the library's implementations for
-        // primitive types are trivially `true`).
+        // primitive types are trivially `true`). This applies regardless of whether the value was
+        // generated via Arbitrary or BoundedArbitrary.
         if matches!(ty.kind(), TyKind::RigidTy(RigidTy::Adt(..)))
             && implements_invariant(ty, models.kani_assume_safe, invariant_cache)
         {
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 181eb9008eb..5dbfda083ae 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -302,6 +302,7 @@ macro_rules! kani_intrinsics {
         /// implementing BoundedArbitrary decides exactly what size means for them.
         ///
         /// *Note*: Any proof using a bounded symbolic value is only valid up to that bound.
+        #[kanitool::fn_marker = "BoundedAnyModel"]
         #[inline(always)]
         pub fn bounded_any<T: BoundedArbitrary, const N: usize>() -> T {
             T::bounded_any::<N>()
diff --git a/tests/script-based-pre/cargo_autoharness_bounded/Cargo.toml b/tests/script-based-pre/cargo_autoharness_bounded/Cargo.toml
new file mode 100644
index 00000000000..ca66247aca8
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_bounded/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_bounded"
+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_bounded/bounded.expected b/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected
new file mode 100644
index 00000000000..fec1bdbd8c1
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected
@@ -0,0 +1,13 @@
+[without --bounded-arguments]
+| cargo_autoharness_bounded | packet_check                                    | Requires --bounded-arguments for argument(s) p: Packet                                |
+[with --bounded-arguments]
+| cargo_autoharness_bounded | nested_vec                                      | Missing Arbitrary implementation for argument(s) xs: std::vec::Vec<std::vec::Vec<u8>> |
+- Status: SATISFIED
+| cargo_autoharness_bounded | packet_check      | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_bounded | string_head       | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_bounded | vec_cover         | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_bounded | vec_sum           | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_bounded | string_first_byte | #[kani::proof] (bounded)  | Failure             |
+| cargo_autoharness_bounded | vec_first         | #[kani::proof] (bounded)  | Failure             |
+Note: harnesses marked "(bounded)" use bounded nondeterministic values for some arguments (--bounded-arguments);
+Complete - 4 successfully verified functions, 2 failures, 6 total.
diff --git a/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh b/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh
new file mode 100755
index 00000000000..6f6b0c659ed
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+echo "[without --bounded-arguments]"
+cargo kani autoharness -Z autoharness --list 2>&1 | grep -m1 'Requires --bounded-arguments'
+echo "[with --bounded-arguments]"
+cargo kani autoharness -Z autoharness --bounded-arguments
diff --git a/tests/script-based-pre/cargo_autoharness_bounded/config.yml b/tests/script-based-pre/cargo_autoharness_bounded/config.yml
new file mode 100644
index 00000000000..830a5e4ae57
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_bounded/config.yml
@@ -0,0 +1,5 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: bounded.sh
+expected: bounded.expected
+exit_code: 1
diff --git a/tests/script-based-pre/cargo_autoharness_bounded/src/lib.rs b/tests/script-based-pre/cargo_autoharness_bounded/src/lib.rs
new file mode 100644
index 00000000000..8db3f493e0a
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_bounded/src/lib.rs
@@ -0,0 +1,53 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that the autoharness subcommand supports arguments whose types implement
+// `BoundedArbitrary` (rather than `Arbitrary`), e.g. `Vec<T>`, `String`, or user types
+// deriving it. The generated harness produces a bounded nondeterministic value via
+// `kani::bounded_any` with bound AUTOHARNESS_BOUNDED_ANY_BOUND (4); verification results
+// only hold up to that bound. The "TEST NOTE" comments explain the expected result per
+// function.
+
+// TEST NOTE: should PASS: summing at most 4 u8s cannot overflow u64.
+pub fn vec_sum(xs: Vec<u8>) -> u64 {
+    xs.iter().map(|&x| x as u64).sum()
+}
+
+// TEST NOTE: should FAIL: the vector may be empty, so the index may be out of bounds.
+pub fn vec_first(xs: Vec<u8>) -> u8 {
+    xs[0]
+}
+
+// TEST NOTE: should PASS: strings generated via String's BoundedArbitrary implementation.
+pub fn string_head(s: String) -> Option<char> {
+    s.chars().next()
+}
+
+// TEST NOTE: should FAIL: the string may be empty, so the index may be out of bounds.
+pub fn string_first_byte(s: String) -> u8 {
+    s.as_bytes()[0]
+}
+
+// TEST NOTE: should PASS: user-defined types deriving BoundedArbitrary are supported too.
+#[derive(kani::BoundedArbitrary)]
+pub struct Packet {
+    #[bounded]
+    payload: Vec<u8>,
+    flag: bool,
+}
+
+pub fn packet_check(p: Packet) -> usize {
+    if p.flag { p.payload.len() } else { 0 }
+}
+
+// TEST NOTE: should PASS, and the cover check must be SATISFIED: maximum-length vectors
+// with specific nondeterministic contents are generated.
+pub fn vec_cover(xs: Vec<u8>) {
+    kani::cover!(xs.len() == 4 && xs[0] == 42, "max-length vec with specific contents");
+}
+
+// TEST NOTE: skipped: Vec<Vec<u8>> is unsupported, since Vec's BoundedArbitrary
+// implementation requires the element type to implement Arbitrary.
+pub fn nested_vec(xs: Vec<Vec<u8>>) -> usize {
+    xs.len()
+}

From b6a36cfa61ca7e52b83ba2ebc0b1d20ba39f1149 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 30 Jul 2026 03:51:15 +0000
Subject: [PATCH 2/3] Guard BoundedArbitrary probing against unsized types;
 assert before emitting bounded_any

Probing implements_bounded_arbitrary with an unsized type instantiates the
generic model with that type, which can crash constant evaluation during
body retrieval (found by re-running the top-100 crates.io evaluation, e.g.
on bytes). Reject unsized types up front.

Also assert that the type implements BoundedArbitrary before emitting a
bounded_any call in harness generation: Instance::resolve does not check
trait bounds, so an eligibility/transform mismatch would otherwise only
surface as an ICE during reachability.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .../src/kani_middle/codegen_units.rs          |  1 +
 kani-compiler/src/kani_middle/mod.rs          | 23 ++++++--
 .../src/kani_middle/transform/automatic.rs    | 53 +++++++++++++++----
 3 files changed, 64 insertions(+), 13 deletions(-)

diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index e5e97c01b76..6d7703ab288 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -591,6 +591,7 @@ fn automatic_harness_partition(
             // same key would poison the cache for the ADT-field checks. `implements_arbitrary`
             // memoizes its own recursion internally, so repeated argument types stay cheap.
             let support = autoharness_supported_arg_ty(
+                tcx,
                 arg.ty,
                 kani_any_def,
                 kani_bounded_any_def,
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 23fd130394b..407b89ea803 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -349,6 +349,14 @@ fn implements_invariant(
     res
 }
 
+/// Whether `ty` is statically sized. Nondeterministic-value generation (and the resolution
+/// checks probing for it) must not instantiate generic models with unsized types: apart from
+/// being ungeneratable, this can crash constant evaluation during body retrieval.
+fn ty_is_sized(tcx: TyCtxt, ty: Ty) -> bool {
+    rustc_internal::internal(tcx, ty)
+        .is_sized(*tcx.at(rustc_span::DUMMY_SP), rustc_middle::ty::TypingEnv::fully_monomorphized())
+}
+
 /// Inspect a `kani::bounded_any::<T, N>()` (c.f. `KaniModel::BoundedAny`) instantiation to
 /// determine if `T: BoundedArbitrary`. The model looks like:
 /// ```rust
@@ -359,8 +367,8 @@ fn implements_invariant(
 /// So we select the terminator that calls `T::bounded_any::<N>()`, then try to resolve it to an
 /// Instance; `T` implements `BoundedArbitrary` iff we successfully resolve the Instance
 /// (mirroring `implements_arbitrary`).
-fn implements_bounded_arbitrary(ty: Ty, kani_bounded_any_def: FnDef) -> bool {
-    if ty.kind().rigid().is_none() {
+fn implements_bounded_arbitrary(tcx: TyCtxt, ty: Ty, kani_bounded_any_def: FnDef) -> bool {
+    if ty.kind().rigid().is_none() || !ty_is_sized(tcx, ty) {
         return false;
     }
 
@@ -472,6 +480,7 @@ pub enum ArgSupport {
 /// inside an ADT remains unsupported, since the pointee/backing storage that the generated harness
 /// allocates would not outlive the generated value.
 fn autoharness_supported_arg_ty(
+    tcx: TyCtxt,
     ty: Ty,
     kani_any_def: FnDef,
     kani_bounded_any_def: FnDef,
@@ -490,7 +499,13 @@ fn autoharness_supported_arg_ty(
     if let TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) = ty.kind() {
         // A raw pointer is supported as long as its pointee is: propagate the pointee's verdict,
         // so a pointer to a bounded pointee (e.g. `*mut &[T]`) is itself reported as bounded.
-        autoharness_supported_arg_ty(inner_ty, kani_any_def, kani_bounded_any_def, ty_arbitrary_cache)
+        autoharness_supported_arg_ty(
+            tcx,
+            inner_ty,
+            kani_any_def,
+            kani_bounded_any_def,
+            ty_arbitrary_cache,
+        )
     } else if let TyKind::RigidTy(RigidTy::Ref(_, inner_ty, inner_mutability)) = ty.kind() {
         match inner_ty.kind() {
             TyKind::RigidTy(RigidTy::Slice(elem_ty)) => {
@@ -514,7 +529,7 @@ fn autoharness_supported_arg_ty(
     } else {
         if arbitrary_or_derive(ty, ty_arbitrary_cache) == ArgSupport::Arbitrary {
             ArgSupport::Arbitrary
-        } else if implements_bounded_arbitrary(ty, kani_bounded_any_def) {
+        } else if implements_bounded_arbitrary(tcx, ty, kani_bounded_any_def) {
             ArgSupport::Bounded
         } else {
             ArgSupport::Unsupported
diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs
index 5b03e540cbc..6417b485326 100644
--- a/kani-compiler/src/kani_middle/transform/automatic.rs
+++ b/kani-compiler/src/kani_middle/transform/automatic.rs
@@ -125,7 +125,7 @@ impl TransformPass for AutomaticArbitraryPass {
     /// ```
     /// We match the implementations that kani_macros::derive creates for structs and enums,
     /// so see that module for full documentation of what the generated bodies look like.
-    fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+    fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
         debug!(function=?instance.name(), "AutomaticArbitraryPass::transform");
 
         let unexpected_ty = |ty: &Ty| {
@@ -148,8 +148,8 @@ impl TransformPass for AutomaticArbitraryPass {
 
         if let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() {
             match def.kind() {
-                AdtKind::Enum => (true, self.generate_enum_body(def, args, body)),
-                AdtKind::Struct => (true, self.generate_struct_body(def, args, body)),
+                AdtKind::Enum => (true, self.generate_enum_body(tcx, def, args, body)),
+                AdtKind::Struct => (true, self.generate_struct_body(tcx, def, args, body)),
                 AdtKind::Union => unexpected_ty(ty),
             }
         } else {
@@ -201,6 +201,7 @@ const AUTOHARNESS_BOUNDED_ANY_BOUND: u64 = 4;
 /// Panics if `ty` does not implement Arbitrary or BoundedArbitrary (and is not a reference or raw
 /// pointer to such a type, or a reference to a slice or str of such a type).
 fn call_kani_any_for_ty(
+    tcx: TyCtxt,
     models: AnyModels,
     body: &mut MutableBody,
     ty: Ty,
@@ -248,6 +249,7 @@ fn call_kani_any_for_ty(
         let elem_lcls = (0..bound)
             .map(|_| {
                 call_kani_any_for_ty(
+                    tcx,
                     models,
                     body,
                     elem_ty,
@@ -315,8 +317,15 @@ fn call_kani_any_for_ty(
             slice_lcl
         }
     } else if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() {
-        let inner_lcl =
-            call_kani_any_for_ty(models, body, inner_ty, inner_mutability, source, invariant_cache);
+        let inner_lcl = call_kani_any_for_ty(
+            tcx,
+            models,
+            body,
+            inner_ty,
+            inner_mutability,
+            source,
+            invariant_cache,
+        );
         let ref_lcl = body.new_local(ty, source.span(body.blocks()), mutability);
         let borrow_kind = if inner_mutability == Mutability::Not {
             BorrowKind::Shared
@@ -334,8 +343,15 @@ fn call_kani_any_for_ty(
         // Generate the storage for the valid-pointer case: a local with a nondeterministic value
         // of the pointee type. Since it is a local of the body being transformed, it stays alive
         // for as long as that body executes.
-        let storage_lcl =
-            call_kani_any_for_ty(models, body, inner_ty, Mutability::Mut, source, invariant_cache);
+        let storage_lcl = call_kani_any_for_ty(
+            tcx,
+            models,
+            body,
+            inner_ty,
+            Mutability::Mut,
+            source,
+            invariant_cache,
+        );
 
         // Pass a mutable reference to the storage to the AnyPtr model, which returns a `*mut T`
         // that is either null, out of bounds (one past the end), or pointing to the storage.
@@ -391,6 +407,13 @@ fn call_kani_any_for_ty(
         let (model, generic_args) = if use_arbitrary {
             (models.kani_any, GenericArgs(vec![GenericArgKind::Type(ty)]))
         } else {
+            // `Instance::resolve` does not check trait bounds, so ensure the type actually
+            // implements BoundedArbitrary before emitting the call: an unresolvable
+            // `T::bounded_any` would otherwise only surface as an ICE during reachability.
+            assert!(
+                crate::kani_middle::implements_bounded_arbitrary(tcx, ty, models.kani_bounded_any),
+                "expected a ty that implements Arbitrary or BoundedArbitrary, got {ty}"
+            );
             (
                 models.kani_bounded_any,
                 GenericArgs(vec![
@@ -448,6 +471,7 @@ impl AutomaticArbitraryPass {
     #[allow(clippy::too_many_arguments)]
     fn call_kani_any_for_variant(
         &self,
+        tcx: TyCtxt,
         adt_def: AdtDef,
         adt_args: &GenericArgs,
         body: &mut MutableBody,
@@ -462,6 +486,7 @@ impl AutomaticArbitraryPass {
         // Construct nondeterministic values for each of the variant's fields
         for ty in fields.iter().map(|field| field.ty_with_args(adt_args)) {
             let lcl = call_kani_any_for_ty(
+                tcx,
                 self.models,
                 body,
                 ty,
@@ -500,7 +525,7 @@ impl AutomaticArbitraryPass {
     ///   _ => Enum::LastVariant
     /// }
     /// ```
-    fn generate_enum_body(&self, def: AdtDef, args: GenericArgs, body: Body) -> Body {
+    fn generate_enum_body(&self, tcx: TyCtxt, def: AdtDef, args: GenericArgs, body: Body) -> Body {
         // Autoharness only deems a function with an enum eligible if it has at least one variant, c.f. `can_derive_arbitrary`
         assert!(def.num_variants() > 0);
 
@@ -511,6 +536,7 @@ impl AutomaticArbitraryPass {
 
         // Generate a nondet u128 to switch on
         let discr_lcl = call_kani_any_for_ty(
+            tcx,
             self.models,
             &mut new_body,
             Ty::from_rigid_kind(RigidTy::Uint(UintTy::U128)),
@@ -535,6 +561,7 @@ impl AutomaticArbitraryPass {
         for (idx, variant) in def.variants_iter().enumerate() {
             let variant_idx = VariantIdx::to_val(idx);
             let target_bb = self.call_kani_any_for_variant(
+                tcx,
                 def,
                 &args,
                 &mut new_body,
@@ -568,7 +595,13 @@ impl AutomaticArbitraryPass {
     ///   ...
     /// }
     /// ```
-    fn generate_struct_body(&self, def: AdtDef, args: GenericArgs, body: Body) -> Body {
+    fn generate_struct_body(
+        &self,
+        tcx: TyCtxt,
+        def: AdtDef,
+        args: GenericArgs,
+        body: Body,
+    ) -> Body {
         assert_eq!(def.num_variants(), 1);
 
         let mut new_body = MutableBody::from(body);
@@ -579,6 +612,7 @@ impl AutomaticArbitraryPass {
         let variant = def.variants()[0];
         // A struct has a single variant at index 0.
         self.call_kani_any_for_variant(
+            tcx,
             def,
             &args,
             &mut new_body,
@@ -706,6 +740,7 @@ impl TransformPass for AutomaticHarnessPass {
             .iter()
             .map(|local_decl| {
                 call_kani_any_for_ty(
+                    tcx,
                     self.models,
                     &mut harness_body,
                     local_decl.ty,

From 7392fd0a1f5cc42d5ae1ddff76cf0e7c40f367ed Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Sun, 23 Aug 2026 02:02:11 +0000
Subject: [PATCH 3/3] Autoharness: address review/CI feedback on
 bounded-container support

- Skip derived `kani::BoundedArbitrary` impls (their generated `bounded_any`
  method) from automatic harness selection, consistent with how `kani::Arbitrary`
  and `kani::Invariant` impls are already skipped. Without this, autoharness
  picked up e.g. `<Packet as kani::BoundedArbitrary>::bounded_any::<2>` as an
  extra harness, which is Kani-internal machinery rather than user code.
- Update cargo_autoharness_filter expected output: Vec<u8> arguments now
  implement BoundedArbitrary, so they are skipped with 'Requires
  --bounded-arguments' rather than 'Missing Arbitrary implementation'
  (the run does not pass --bounded-arguments).
- Harden the cargo_autoharness_bounded test: validate the 'cargo kani --list'
  status instead of masking it behind grep, assert the cover description with
  its SATISFIED status, and raise --harness-timeout so the UTF-8 String
  harnesses do not spuriously time out on slow CI runners. Match the skip
  reasons by their (unique) reason substring rather than the full rendered
  table row, so the assertions do not depend on column widths that shift with
  the set of selected functions.
- Docs: fix the BoundedArbitrary link (was a 404 to a nonexistent
  experimental/ page) and reconcile the 'Arguments Implementing Arbitrary'
  limitations section with the BoundedArbitrary/slice/string bounded support.
---
 docs/src/reference/experimental/autoharness.md     | 11 ++++++-----
 kani-compiler/src/kani_middle/codegen_units.rs     |  1 +
 .../cargo_autoharness_bounded/bounded.expected     |  7 ++++---
 .../cargo_autoharness_bounded/bounded.sh           | 14 ++++++++++++--
 .../cargo_autoharness_filter/filter.expected       |  4 ++--
 5 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index 5b1e77c223a..0bfbcc1ad43 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -166,7 +166,7 @@ chosen to stay below the default loop-unwinding bound of 20, so that loops over
 be fully unwound by default.
 
 Additionally (also requiring `--bounded-arguments`), for arguments whose type implements
-[`BoundedArbitrary`](https://model-checking.github.io/kani/reference/experimental/bounded-arbitrary.html)
+[`BoundedArbitrary`](../bounded_arbitrary.md)
 (e.g. `Vec<T>`, `String`, or user types deriving it), the harness generates a bounded
 nondeterministic value with **bound 4** (via `kani::bounded_any`). The same caveat applies:
 verification results only hold up to the bound. The smaller bound reflects that these values are
@@ -178,12 +178,13 @@ Nested slice references (e.g. `&&[u8]`) and slices inside user-defined types rem
 ## Limitations
 ### Arguments Implementing Arbitrary
 Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically.
-By default, it must be able to do so *without bounds*; the `--bounded-arguments` option (see above) relaxes this to
-additionally allow argument types that can only be represented up to a bound, such as slice (`&[T]`/`&mut [T]`) and
-string (`&str`) references.
-In technical terms, each of the arguments needs to implement the `Arbitrary`
+By default, it must be able to do so *without bounds*: each argument needs to implement the `Arbitrary`
 trait or be capable of deriving it, or be a reference (mutable or immutable)
 where any of the prior requirements is fulfilled by the referenced type.
+The `--bounded-arguments` option (see above) relaxes this to
+additionally allow argument types that can only be represented up to a bound: slice (`&[T]`/`&mut [T]`) and
+string (`&str`) references, and types implementing [`BoundedArbitrary`](../bounded_arbitrary.md)
+(e.g. `Vec<T>`, `String`, or user types deriving it).
 Kani will detect if a struct or enum could implement `Arbitrary` and derive it automatically.
 Note that this automatic derivation feature is only available for autoharness.
 
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index 6d7703ab288..39ac29f260f 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -565,6 +565,7 @@ fn automatic_harness_partition(
 
         if is_proof_harness(tcx, instance)
             || name.contains("kani::Arbitrary")
+            || name.contains("kani::BoundedArbitrary")
             || name.contains("kani::Invariant")
         {
             return Err(AutoHarnessSkipReason::KaniImpl);
diff --git a/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected b/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected
index fec1bdbd8c1..6f6a94b3311 100644
--- a/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected
+++ b/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected
@@ -1,8 +1,9 @@
 [without --bounded-arguments]
-| cargo_autoharness_bounded | packet_check                                    | Requires --bounded-arguments for argument(s) p: Packet                                |
+Requires --bounded-arguments for argument(s) p: Packet
 [with --bounded-arguments]
-| cargo_autoharness_bounded | nested_vec                                      | Missing Arbitrary implementation for argument(s) xs: std::vec::Vec<std::vec::Vec<u8>> |
-- Status: SATISFIED
+Missing Arbitrary implementation for argument(s) xs: std::vec::Vec<std::vec::Vec<u8>>
+Status: SATISFIED\
+Description: "max-length vec with specific contents"
 | cargo_autoharness_bounded | packet_check      | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_bounded | string_head       | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_bounded | vec_cover         | #[kani::proof] (bounded)  | Success             |
diff --git a/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh b/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh
index 6f6b0c659ed..581b26d5f7d 100755
--- a/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh
+++ b/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh
@@ -2,7 +2,17 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+set -eu
+
 echo "[without --bounded-arguments]"
-cargo kani autoharness -Z autoharness --list 2>&1 | grep -m1 'Requires --bounded-arguments'
+# Capture the command status explicitly: piping straight into `grep` would mask a
+# failure of `cargo kani ... --list` (the pipeline would report grep's status).
+list_output=$(cargo kani autoharness -Z autoharness --list 2>&1)
+echo "$list_output" | grep -m1 'Requires --bounded-arguments'
+
 echo "[with --bounded-arguments]"
-cargo kani autoharness -Z autoharness --bounded-arguments
+# `string_head`/`string_first_byte` reason about UTF-8 over a bounded nondeterministic
+# `String`, which is expensive; on slower CI runners it can exceed the autoharness default
+# 60s harness timeout, so raise it here to keep these harnesses from spuriously timing out.
+# This run reports failures (`vec_first`/`string_first_byte`), so it exits non-zero (see config.yml).
+cargo kani autoharness -Z autoharness -Z unstable-options --bounded-arguments --harness-timeout 5m
diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected
index 2e619294cc1..b7cbf3029a9 100644
--- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected
+++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected
@@ -104,11 +104,11 @@ If you believe that the provided reason is incorrect and Kani should have genera
 +======================================================================================================================================================+
 | cargo_autoharness_filter | no_harness::doesnt_implement_arbitrary | Missing Arbitrary implementation for argument(s) x: DoesntImplementArbitrary<'_> |
 |--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
-| 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_no_arg_name    | Requires --bounded-arguments for argument(s) _: std::vec::Vec<u8>                |
 |--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
 | cargo_autoharness_filter | no_harness::unsupported_slice          | Requires --bounded-arguments for argument(s) _y: &[u8]                           |
 |--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
-| cargo_autoharness_filter | no_harness::unsupported_vec            | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec<u8>           |
+| cargo_autoharness_filter | no_harness::unsupported_vec            | Requires --bounded-arguments for argument(s) _y: std::vec::Vec<u8>               |
 +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+
 Autoharness: Checking function yes_harness::f_mut_pointer against all possible inputs...
 Autoharness: Checking function yes_harness::f_const_pointer against all possible inputs...