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...