Fix stub_verified infinite recursion when Arbitrary calls the stubbed function

docs/src/reference/experimental/contracts.md

@@ -62,5 +62,15 @@ fn check_foo() {
 ```
 By leveraging the stubbing feature, we can replace the (expensive) `gcd` call with a *verified abstraction* of its behavior, greatly reducing verification time for `foo`.
 
+> **Note:** `stub_verified` replaces calls globally, including inside
+> `kani::Arbitrary` implementations. Kani automatically detects when a call
+> originates from `kani::any()` (input generation) and uses the original
+> function body instead of the contract replacement. This means
+> `stub_verified` works correctly even when the type's `Arbitrary` impl calls
+> the stubbed function. If you encounter issues, you can work around them by
+> deriving `Arbitrary` (which generates field-by-field values without calling
+> user functions) or by using standalone proof harnesses instead of
+> `stub_verified`.
+
 There is far more to learn about contracts.
 We highly recommend reading our [blog post about contracts](https://model-checking.github.io/kani-verifier-blog/2024/01/29/function-contracts.html) (from which this `gcd` example is taken). We also recommend looking at the `contracts` module in our [documentation](../../crates/index.md).

library/kani_core/src/lib.rs

@@ -275,6 +275,7 @@ macro_rules! kani_intrinsics {
         #[kanitool::fn_marker = "AnyModel"]
         #[inline(always)]
         pub fn any<T: Arbitrary>() -> T {
+            let _guard = internal::ArbitraryContextGuard::enter();
             T::any()
         }
 
@@ -284,6 +285,7 @@ macro_rules! kani_intrinsics {
         /// *Note*: Any proof using a bounded symbolic value is only valid up to that bound.
         #[inline(always)]
         pub fn bounded_any<T: BoundedArbitrary, const N: usize>() -> T {
+            let _guard = internal::ArbitraryContextGuard::enter();
             T::bounded_any::<N>()
         }
 
@@ -325,7 +327,7 @@ macro_rules! kani_intrinsics {
         /// valid values for type `T`.
         #[inline(always)]
         pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
-            let result = T::any();
+            let result = any();
             assume(f(&result));
             result
         }
@@ -535,15 +537,15 @@ macro_rules! kani_intrinsics {
             #[kanitool::fn_marker = "WriteAnySliceModel"]
             #[inline(always)]
             pub unsafe fn write_any_slice<T: Arbitrary>(slice: *mut [T]) {
-                (*slice).fill_with(T::any)
+                (*slice).fill_with(|| super::any::<T>())
             }
 
             /// Fill in a pointer with kani::any.
             /// Intended as a post compilation replacement for write_any
             #[kanitool::fn_marker = "WriteAnySlimModel"]
             #[inline(always)]
             pub unsafe fn write_any_slim<T: Arbitrary>(pointer: *mut T) {
-                ptr::write(pointer, T::any())
+                ptr::write(pointer, super::any::<T>())
             }
 
             /// Fill in a str with kani::any.
@@ -601,6 +603,71 @@ macro_rules! kani_intrinsics {
             /// Insert the contract into the body of the function as assertion(s).
             pub const ASSERT: Mode = 4;
 
+            /// Nesting depth counter for `Arbitrary::any()` calls — see
+            /// `docs/dev/stub-verified-arbitrary.md` for design rationale.
+            /// Not public — only accessible via `in_arbitrary_context()` and
+            /// `ArbitraryContextGuard`.
+            ///
+            /// This static is guaranteed to be a single instance per compilation
+            /// unit: both `kani_lib!(kani)` and `kani_lib!(core)` expand
+            /// `kani_intrinsics!()` exactly once, producing one `kani::internal`
+            /// module with one copy of this static.
+            static mut ARBITRARY_NESTING_DEPTH: u32 = 0;
+
+            /// Increment the arbitrary nesting depth counter.
+            /// Note: `debug_assert!` guards are active in concrete playback
+            /// but compiled away during symbolic execution (release-like MIR).
+            #[inline(always)]
+            fn enter_arbitrary_context() {
+                unsafe {
+                    debug_assert!(
+                        ARBITRARY_NESTING_DEPTH < u32::MAX,
+                        "ArbitraryContextGuard: nesting depth overflow"
+                    );
+                    ARBITRARY_NESTING_DEPTH = ARBITRARY_NESTING_DEPTH.wrapping_add(1);
+                }
+            }
+
+            /// Decrement the arbitrary nesting depth counter.
+            #[inline(always)]
+            fn exit_arbitrary_context() {
+                unsafe {
+                    debug_assert!(
+                        ARBITRARY_NESTING_DEPTH > 0,
+                        "ArbitraryContextGuard: mismatched exit (underflow)"
+                    );
+                    ARBITRARY_NESTING_DEPTH = ARBITRARY_NESTING_DEPTH.wrapping_sub(1);
+                }
+            }
+
+            /// Returns true if we are inside a `kani::any()` call (i.e., during
+            /// `Arbitrary` input generation). Used by the contract `REPLACE` arm
+            /// to fall back to the original function body.
+            #[inline(always)]
+            pub fn in_arbitrary_context() -> bool {
+                unsafe { ARBITRARY_NESTING_DEPTH > 0 }
+            }
+
+            /// RAII guard that increments the arbitrary nesting depth on creation
+            /// and decrements it on drop. Ensures the counter is correctly
+            /// maintained even if `T::any()` panics (concrete playback mode).
+            pub struct ArbitraryContextGuard;
+
+            impl ArbitraryContextGuard {
+                #[inline(always)]
+                pub fn enter() -> Self {
+                    enter_arbitrary_context();
+                    ArbitraryContextGuard
+                }
+            }
+
+            impl Drop for ArbitraryContextGuard {
+                #[inline(always)]
+                fn drop(&mut self) {
+                    exit_arbitrary_context();
+                }
+            }
+
             /// Creates a non-fatal property with the specified condition and message.
             ///
             /// This check will not impact the program control flow even when it fails.

library/kani_macros/src/sysroot/contracts/bootstrap.rs

@@ -83,6 +83,17 @@ impl<'a> ContractConditionsHandler<'a> {
                         kani_register_contract(#recursion_ident)
                     }
                     kani::internal::REPLACE => {
+                        // When called from within kani::any() (Arbitrary input
+                        // generation), use the original body to avoid infinite
+                        // recursion from stub_verified replacing calls inside
+                        // Arbitrary impls. This early return avoids the replace
+                        // closure capturing function parameters by move.
+                        if kani::internal::in_arbitrary_context() {
+                            return #block
+                        }
+                        // The replace closure must remain at the top level of this
+                        // arm so that subsequent contract attributes can find it via
+                        // expect_closure_in_match.
                         #replace_closure;
                         kani_register_contract(#replace_ident)
                     }

rfc/src/rfcs/0002-function-stubbing.md

@@ -367,6 +367,28 @@ One possibility would be writing proofs about stubs (possibly relating their beh
 - Our proposed approach will not work with `--concrete-playback` (for now).
 - We are only able to apply abstractions to some dependencies if the user enables the MIR linker.
 
+### `stub_verified` and `Arbitrary` interaction
+
+When a type's `kani::Arbitrary` implementation calls a function targeted by
+`#[kani::stub_verified]`, the global contract replacement would normally apply
+inside `Arbitrary::any()` too, causing infinite recursion during test input
+generation.
+
+To prevent this, `kani::any()` tracks nesting depth via an internal counter
+(`ARBITRARY_NESTING_DEPTH`) managed by an RAII guard. The contract `REPLACE`
+match arm checks this counter — when inside an Arbitrary context (depth > 0),
+it executes the original function body instead of the contract replacement.
+
+This is sound because the real function produces a subset of valid outputs
+compared to the contract abstraction (which havocs all outputs). Using the real
+function during Arbitrary input generation gives tighter (more precise) inputs,
+not less sound verification.
+
+The counter (not a boolean) correctly handles nested `kani::any()` calls, e.g.,
+when `Arbitrary` for a struct calls `kani::any()` for each field. All entry
+points (`any()`, `bounded_any()`, `any_where()`, `write_any_slim()`,
+`write_any_slice()`) route through the guard.
+
 ## Future possibilities
 
 - It would increase the utility of stubbing if we supported stubs for types.

tests/kani/FunctionContracts/stub_verified_arbitrary_fix.rs

@@ -0,0 +1,49 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z function-contracts -Z stubbing
+//
+//! Regression test: stub_verified no longer causes infinite recursion when
+//! the type's Arbitrary implementation calls the stubbed function.
+//! See: docs/dev/stub-verified-arbitrary.md
+
+const LIMIT: u64 = 1000;
+
+#[derive(Clone, Copy)]
+struct Wrapper {
+    value: u64,
+}
+
+impl Wrapper {
+    #[kani::ensures(|result: &Self| result.value <= LIMIT)]
+    fn normalize(self) -> Self {
+        if self.value > LIMIT { Wrapper { value: LIMIT } } else { self }
+    }
+
+    fn new(v: u64) -> Self {
+        Wrapper { value: v }.normalize()
+    }
+}
+
+// Arbitrary calls new() which calls normalize() — the stubbed function
+impl kani::Arbitrary for Wrapper {
+    fn any() -> Self {
+        Wrapper::new(kani::any())
+    }
+}
+
+#[kani::proof_for_contract(Wrapper::normalize)]
+fn check_contract() {
+    Wrapper { value: kani::any() }.normalize();
+}
+
+// This previously caused infinite recursion because stub_verified replaced
+// normalize globally, including inside Arbitrary::any().
+// The fix: kani::any() sets ARBITRARY_NESTING_DEPTH, and the contract
+// REPLACE arm falls back to the original body when the depth is > 0.
+#[kani::proof]
+#[kani::stub_verified(Wrapper::normalize)]
+fn check_caller_with_stub() {
+    let w: Wrapper = kani::any();
+    assert!(w.normalize().value <= LIMIT);
+}

tests/kani/FunctionContracts/stub_verified_arbitrary_workaround.rs

@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z function-contracts -Z stubbing
+//
+//! Demonstrates that stub_verified works correctly even when the Arbitrary
+//! implementation calls the stubbed function, using the standalone proof
+//! pattern as an alternative approach.
+
+const LIMIT: u64 = 1000;
+
+#[derive(Clone, Copy)]
+struct Wrapper {
+    value: u64,
+}
+
+impl Wrapper {
+    #[kani::ensures(|result: &Self| result.value <= LIMIT)]
+    fn normalize(self) -> Self {
+        if self.value > LIMIT { Wrapper { value: LIMIT } } else { self }
+    }
+
+    fn new(v: u64) -> Self {
+        Wrapper { value: v }.normalize()
+    }
+
+    fn process(self) -> u64 {
+        self.normalize().value * 2
+    }
+}
+
+// Arbitrary calls new() which calls normalize()
+impl kani::Arbitrary for Wrapper {
+    fn any() -> Self {
+        Wrapper::new(kani::any())
+    }
+}
+
+// Step 1: Verify the contract
+#[kani::proof_for_contract(Wrapper::normalize)]
+fn check_normalize_contract() {
+    Wrapper { value: kani::any() }.normalize();
+}
+
+// Step 2: Use stub_verified — works even though Arbitrary calls normalize,
+// thanks to the ARBITRARY_NESTING_DEPTH mechanism.
+#[kani::proof]
+#[kani::stub_verified(Wrapper::normalize)]
+fn check_process_with_stub() {
+    let w: Wrapper = kani::any();
+    let result = w.process();
+    assert!(result <= LIMIT * 2);
+}
+
+// Alternative: standalone proof without stub_verified
+#[kani::proof]
+fn check_process_standalone() {
+    let w: Wrapper = kani::any();
+    let result = w.process();
+    assert!(result <= LIMIT * 2);
+}

tests/kani/FunctionContracts/stub_verified_safe_arbitrary.rs

@@ -0,0 +1,41 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z function-contracts -Z stubbing
+//
+//! Demonstrates that stub_verified works correctly when the Arbitrary
+//! implementation does NOT call the stubbed function.
+
+const LIMIT: u64 = 1000;
+
+#[derive(Clone, Copy, kani::Arbitrary)]
+struct MyType {
+    value: u64,
+}
+
+impl MyType {
+    #[kani::ensures(|result: &Self| result.value <= LIMIT)]
+    fn normalize(self) -> Self {
+        if self.value > LIMIT { MyType { value: LIMIT } } else { self }
+    }
+
+    fn process(self) -> u64 {
+        self.normalize().value * 2
+    }
+}
+
+// Step 1: Verify the contract
+#[kani::proof_for_contract(MyType::normalize)]
+fn check_normalize_contract() {
+    MyType { value: kani::any() }.normalize();
+}
+
+// Step 2: Use stub_verified in a caller — works because
+// kani::Arbitrary for MyType (derived) does NOT call normalize
+#[kani::proof]
+#[kani::stub_verified(MyType::normalize)]
+fn check_process_with_stub() {
+    let t: MyType = kani::any();
+    let result = t.process();
+    assert!(result <= LIMIT * 2);
+}