Fix stub_verified infinite recursion when Arbitrary calls the stubbed function

[feliperodri]

Problem

When a type's kani::Arbitrary implementation calls a function that is the target of #[kani::stub_verified], verification hits infinite recursion. The contract replacement (ContractMode::Replace) applies globally, including inside Arbitrary::any(), so test input generation itself invokes the contract abstraction instead of the real function.

impl kani::Arbitrary for Wrapper {
    fn any() -> Self {
        Wrapper::new(kani::any())  // new() calls normalize()
    }
}

#[kani::proof]
#[kani::stub_verified(Wrapper::normalize)]  // replaces ALL calls to normalize
fn check() {
    let w: Wrapper = kani::any();  // Arbitrary → new() → normalize() → STUBBED → recursion
}

Solution

kani::any() now tracks nesting depth via a global counter (ARBITRARY_NESTING_DEPTH). 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.

Implementation details

• RAII guard (ArbitraryContextGuard): Increments the counter on creation, decrements on drop. Ensures correctness even if T::any() panics during concrete playback.
• All paths covered: kani::any(), any_where(), write_any_slim(), and write_any_slice() all go through the guard.
• Wrapping arithmetic: Avoids CBMC overflow checks on the counter.
• Contract bootstrap change: The REPLACE arm in bootstrap.rs checks in_arbitrary_context() and falls back to #block (the original function body) when true.

Soundness

Excluding Arbitrary from stub replacement is sound: the real function produces a subset of valid values; the stub produces a superset. Using the real function gives tighter (more precise) input generation, not less sound verification.

Testing

• stub_verified_arbitrary_fix.rs — Regression test: Wrapper::Arbitrary calls normalize() (the stubbed function). Previously caused infinite recursion, now works.
• stub_verified_safe_arbitrary.rs — Derived Arbitrary (doesn't call stubbed function) works with stub_verified.
• stub_verified_arbitrary_workaround.rs — Documents the standalone proof pattern as an alternative.

---

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[feliperodri]

I attempted to implement a runtime fix (nesting depth counter) but it conflicts with CBMC's DFCC assigns checking: writes to global mutable state inside contract-checked scopes trigger assigns violations. CBMC provides no mechanism to exempt infrastructure writes from DFCC tracking. So back to the drawing board...

[Copilot]

Pull request overview

This PR addresses an infinite-recursion/hang scenario caused by #[kani::stub_verified] contract replacements re-entering themselves through kani::any::<Ret>() when Ret’s kani::Arbitrary implementation calls the stubbed function. The implementation in this diff prevents the hang by detecting the cycle during compilation and emitting a targeted error with a call-path trace, and it documents the limitation/workarounds.

Changes:

• Add a stub_verified/Arbitrary cycle check in FunctionWithContractPass (compiler MIR transform) and emit a compile-time diagnostic with a call trace.
• Add tests covering (a) a safe derived-Arbitrary case that should verify, and (b) a cycle case that should error with an expected message.
• Document the limitation and workarounds in both the RFC and the user reference docs.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tests/kani/FunctionContracts/stub_verified_safe_arbitrary.rs	New positive test ensuring stub_verified works when derived Arbitrary does not call the stubbed function.
tests/expected/function-contract/stub_verified_arbitrary_cycle.rs	New negative test setting up the stub_verified/Arbitrary recursion cycle.
tests/expected/function-contract/stub_verified_arbitrary_cycle.expected	Expected diagnostic output for the new cycle detection error.
rfc/src/rfcs/0002-function-stubbing.md	RFC documentation of the stub_verified/Arbitrary interaction and workarounds.
kani-compiler/src/kani_middle/transform/contracts.rs	Compiler-side cycle detection logic and diagnostic emission for verified stubs.
docs/src/reference/experimental/contracts.md	User docs note about the stub_verified/Arbitrary recursion limitation and mitigation.

Suppressed comments (2)

kani-compiler/src/kani_middle/transform/contracts.rs:533

• The trace formatting in this diagnostic does not match the expected output in tests/expected/function-contract/stub_verified_arbitrary_cycle.expected: it currently (1) includes the kani::any::<Ret> frame, (2) does not prefix the first line with -> , and (3) adds extra indentation before the trace. This will make the UI test brittle / fail.

Consider building the trace as one -> ... entry per line and dropping the initial kani::any::<Ret> frame so the first line is the Arbitrary::any call (which is where the recursion actually starts).

        // Use the resolved instance name for the trace tail so it matches the
        // crate-qualified names that `Instance::name` produces for the path.
        let trace = path.join("\n    -> ") + "\n    -> " + &instance.name();
        tcx.dcx()
            .struct_span_err(

kani-compiler/src/kani_middle/transform/contracts.rs:316

• After switching arbitrary_cycle_checked to be keyed by monomorphized Instance, this insert should use the instance parameter rather than *def; otherwise different instantiations of the same generic function still get deduped and may skip the cycle check.

                    if mode == ContractMode::Replace && self.arbitrary_cycle_checked.insert(*def) {
                        self.check_arbitrary_cycle(tcx, *def, args);
                    }

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.