`#[kani::stub]` on contracted functions

[feliperodri]

Using #[kani::stub(target, replacement)] where target has a #[kani::ensures] contract produces a compilation error: Failed to find contract closure __kani_recursion_check_<fn_name>.

Minimal reproducer

#[kani::ensures(|result: &i32| *result >= 0)]
fn abs_val(x: i32) -> i32 {
    if x < 0 { -x } else { x }
}

fn stub_abs_val(_x: i32) -> i32 {
    let r: i32 = kani::any();
    kani::assume(r >= 0);
    r
}

fn caller(x: i32) -> i32 {
    abs_val(x) + 1
}

#[kani::proof]
#[kani::stub(abs_val, stub_abs_val)]
fn check_caller() {
    let x: i32 = kani::any();
    let result = caller(x);
    assert!(result >= 1);
}

$ cargo kani -Z function-contracts -Z stubbing
error: Failed to find contract closure `__kani_recursion_check_abs_val` in function `abs_val`

Expected behavior

#[kani::stub] should work on functions that have contracts. The stub replaces the function body entirely, so the contract instrumentation should be irrelevant.

Impact

This prevents compositional verification where a function has been proved correct via proof_for_contract and callers want to use a standard stub (not stub_verified) to abstract it away. The workaround is to remove the ensures contract from the target function, but this breaks the proof_for_contract harness.