fix(contracts): Prevent stub_verified infinite recursion when Arbitrary calls stubbed function

When a type's Arbitrary implementation calls a function targeted by
stub_verified, the global contract replacement caused infinite recursion
because test input generation (kani::any()) invoked the contract
abstraction instead of the real function.

Fix: kani::any() now uses an RAII guard (ArbitraryContextGuard) that
increments a global ARBITRARY_NESTING_DEPTH counter before calling
T::any() and decrements it on drop. The contract REPLACE match arm
checks in_arbitrary_context() — when true, it executes the original
function body instead of the contract replacement.

This ensures Arbitrary impls always use the real function while
verification callers use the contract abstraction. The counter (not a
boolean) handles nested kani::any() calls correctly. Wrapping arithmetic
avoids CBMC overflow checks on the counter.

Changes:
- library/kani_core/src/lib.rs: ArbitraryContextGuard RAII guard,
  enter/exit/in_arbitrary_context() accessors, guard in kani::any()
- library/kani_core/src/lib.rs: Route write_any_slim, write_any_slice,
  and any_where through kani::any() so the guard covers all paths
- library/kani_macros/src/sysroot/contracts/bootstrap.rs: REPLACE arm
  falls back to original body when in_arbitrary_context() is true
- Tests: stub_verified_arbitrary_fix.rs (regression test),
  stub_verified_safe_arbitrary.rs (derived Arbitrary works),
  stub_verified_arbitrary_workaround.rs (standalone proof pattern)
- docs/dev/stub-verified-arbitrary.md: Design rationale and soundness

Author: feliperodri

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,8 +83,22 @@ impl<'a> ContractConditionsHandler<'a> {
                         kani_register_contract(#recursion_ident)
                     }
                     kani::internal::REPLACE => {
-                        #replace_closure;
-                        kani_register_contract(#replace_ident)
+                        if kani::internal::in_arbitrary_context() {
+                            // 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.
+                            // Note: This executes the raw body without precondition
+                            // checks or postcondition assertions. This is sound because
+                            // the real function produces a subset of valid outputs
+                            // compared to the contract abstraction (which havocs all
+                            // outputs). Invalid inputs from a buggy Arbitrary impl
+                            // would be caught by the proof_for_contract harness.
+                            #block
+                        } else {
+                            #replace_closure;
+                            kani_register_contract(#replace_ident)
+                        }
                     }
                     kani::internal::SIMPLE_CHECK => {
                         #check_closure;

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);
+}