Detect stub_verified/Arbitrary recursion at compile time

[feliperodri]

Problem

When a type's kani::Arbitrary implementation reaches a function targeted by #[kani::stub_verified], verification never terminates — CBMC unwinds until it exhausts memory, after several minutes, with an out-of-memory message that never names the cause.

The cause is the contract replacement's own return-value havoc. initial_replace_stmts emits kani::any_modifies::<Ret>(), which AnyModifiesPass rewrites to kani::any::<Ret>(). So if Ret's Arbitrary impl reaches the stubbed function, the replacement re-enters itself:

Wrapper::normalize → kani_register_contract → normalize::{closure#1}   (REPLACE)
  → kani::any::<Wrapper> → <Wrapper as Arbitrary>::any → Wrapper::new
  → Wrapper::normalize                                                  ← closes

The cycle is self-contained inside the replacement. It reproduces even when the harness passes a concrete value and never calls kani::any() itself — so a caller-side guard cannot break it. This recursion has no fixpoint, so no unwind bound makes it converge.

Solution

Detect the cycle at compile time rather than letting verification hang. For each ContractMode::Replace target, FunctionWithContractPass resolves kani::any::<Ret> and walks the monomorphized call graph for a path back to the target. If one exists, it emits an error naming the path:

error: `Wrapper::normalize` is used as a verified stub, but generating an arbitrary
       value of its return type `Wrapper` calls `Wrapper::normalize` again
  = note: the contract replacement havocs its return value with `kani::any::<Wrapper>()`,
          so this forms an unbounded recursion:
              -> <Wrapper as kani::Arbitrary>::any
              -> Wrapper::new
              -> Wrapper::normalize
  = help: derive `Arbitrary` for `Wrapper` instead of implementing it manually, or
          avoid calling `Wrapper::normalize` from the `Arbitrary` implementation

This follows the existing check_mutual_recursion precedent for the analogous unsupported-recursion case.

Instance-precise, not DefId-based

Both the per-target dedup and the call-graph comparison are keyed on the monomorphized Instance, not the DefId. A generic stub_verified target can be instantiated at several return types, each with its own potential cycle, and a return type's Arbitrary impl may call a different monomorphization of the same generic function without re-entering the instance under check. Comparing by DefId alone would both:

• skip a later cyclic instantiation when an earlier acyclic one was checked first (missed detection → the hang returns), and
• flag a call to a sibling instantiation whose chain terminates (false positive → a working proof is rejected).

Why not the runtime guard

An earlier revision of this PR tracked kani::any() nesting depth (ARBITRARY_NESTING_DEPTH) and ran the original body when depth > 0. That approach is not viable and has been removed:

• It guards the wrong thing. The replace closure itself calls kani::any(), so the guard fires inside the stub. stub_verified would silently drop its abstraction for calls having nothing to do with Arbitrary.
• The soundness argument was inverted. It keys on dynamic nesting depth, not "is this an Arbitrary impl." Any contract-replaced call under a kani::any() frame loses its stub; whether that's sound depends on the caller, so it is not the blanket win the earlier description claimed.
• It conflicts with CBMC's DFCC assigns checking. Writes to global mutable state inside a contract-checked scope need to be in every modifies clause. REENTRY survives only because --nondet-static-exclude suppresses havocking (not assigns-tracking) and it is written outside the --enforce-contract frame; a counter inside kani::any() is inside that frame.

Limitation

Detection follows only statically resolvable calls, so a cycle routed through a function pointer or trait object is not reported. This is deliberate: a missed detection reproduces prior behavior, whereas a false positive would reject a working proof. Documented in the code and RFC.

This PR makes the failure diagnosable; it does not make the pattern verify. Doing that would require the return havoc to stop routing through user Arbitrary, which changes the soundness model of every stub_verified return value and warrants separate design discussion.

Testing

• tests/expected/function-contract/stub_verified_arbitrary_cycle.{rs,expected} — regression test for the new diagnostic.
• tests/expected/function-contract/stub_verified_arbitrary_cycle_generic.{rs,expected} — a generic target where only the second instantiation is cyclic; guards against DefId-keyed dedup skipping it.
• tests/kani/FunctionContracts/stub_verified_arbitrary_other_instantiation.rs — a call to a sibling instantiation whose chain terminates; guards against a DefId-based false positive. Must verify.
• tests/kani/FunctionContracts/stub_verified_safe_arbitrary.rs — derived Arbitrary (no cycle) still verifies with stub_verified.

Full runs: 592/592 kani, expected and ui suites green (the only failure, expected/shadow/unsupported_num_objects, is pre-existing and unrelated — it fails identically on a clean tree). Both CI clippy invocations and kani-fmt --check are clean.

---

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.

[Copilot]

Pull request overview

Copilot reviewed 8 out of 8 changed files in this pull request and generated no new comments.

Suppressed comments (1)

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

• find_call_path treats any call to the same FnDef as reaching the stubbed target (callee_def.def_id() == target.def_id()). For generic stub_verified targets, this can produce false positives: the return type’s Arbitrary impl might call a different monomorphization of the same generic function (same def_id, different callee_args), which does not necessarily re-enter the specific replacement instance being checked. Since this pass already deduplicates checks per monomorphized Instance, the target comparison should also be instance-precise (def_id + args).

            continue;
        };

        if callee_def.def_id() == target.def_id() {
            return Some(vec![from.name()]);

[Copilot]

Pull request overview

Copilot reviewed 9 out of 9 changed files in this pull request and generated no new comments.