Reject mutual recursion with #[kani::recursion]

[feliperodri]

Emit a compilation error when a function with #[kani::recursion] is involved in mutual recursion. The per-function REENTRY mechanism only handles direct recursion soundly since mutual recursion silently produces unsound verification results.

Contributes to #3316, #3273.

Problem

The #[kani::recursion] attribute uses a per-function REENTRY flag to detect when a function calls itself, replacing the recursive call with the function's contract. For mutual recursion (f calls g, g calls f), the REENTRY flag for g is never set when verifying f's contract, so g's body executes fully instead of being replaced by its contract. Verification succeeds but the result is meaningless — a silent soundness gap.

Solution

check_mutual_recursion() in the contract transform pass scans the MIR body of functions in RecursiveCheck mode for calls to other functions that also have #[kani::recursion] and a contract. For each such callee, it checks if the callee's body calls back to the original function. If so, it emits a span_err (not a warning) because the result would be unsound.

This is an error rather than a warning because soundness violations should not be silently ignorable.

Limitations

• Only detects one level of indirection (f→g→f), not deeper chains (f→g→h→f).
• Reports only the first mutual-recursive callee per function.

Example error

error: `#[kani::recursion]` is used on `mutual_a`, which calls `mutual_b`
       that calls back to `mutual_a`. Mutual recursion is not supported by
       contract verification and may produce unsound results. Only direct
       recursion (a function calling itself) is handled correctly.
  --> tests/expected/function-contract/mutual_recursion_unsound.rs:12:30

Testing

• mutual_recursion_unsound.rs — two mutually recursive functions (mutual_a ↔ mutual_b) with contracts and #[kani::recursion], verifying the error is emitted.

---

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

[rajathmCMU]

Should this be a warn or an error?