Contract targets with fn-pointer type arguments fail to resolve (Map/Filter-style adapters) #4909

Requested feature

Support fn-pointer type arguments in proof_for_contract target paths. resolve_ty rejects Type::BareFn, so a path whose type arguments include a fn(...) -> ... type cannot have its arguments resolved, keeps the definition's uninstantiated identity type, and the target fails to resolve. A Type::BareFn arm in resolve_ty that builds the corresponding fn-pointer type would resolve these.

This is a prerequisite already named in #4830, which lists BareFn and TraitObject as the argument kinds resolve_ty must support for the semantic-resolution rewrite. This issue tracks the user-facing target support specifically: the BareFn arm delivers it on its own, and can land ahead of the larger #4830 refactor.

One boundary: closure arguments stay out of reach for any resolver change, because a closure's type cannot be written in path syntax. A closure-instantiated Map or Filter cannot be named as a contract target; only its fn-pointer instantiations can.

Use case

Writing proof_for_contract harnesses for the standard library's iterator adapters, e.g. <std::iter::Map<std::slice::Iter<u8>, fn(&u8) -> u8> as Iterator>::__iterator_get_unchecked. The Challenge 16 submission (model-checking/verify-rust-std#549) falls back to kani::assume mirror harnesses for these adapters' __iterator_get_unchecked because the targets cannot be named. The #4865 review measured the boundary: with that change the closure-free adapters (Cloned, Zip) resolve — their mirrors can become real proof_for_contract — but Map does not, because its mapping-function type argument still cannot be resolved. (Filter hits the same wall through its predicate parameter.)

Test case

Naming a fn-pointer-instantiated target in proof_for_contract fails to resolve. To reproduce (self-contained, no standard library), save as min_fnptr.rs:

struct Wrap<T>(T);
trait Probe {
    fn probe(&self) -> u32;
}

impl Probe for Wrap<fn(u8) -> u8> {
    #[kani::ensures(|r| *r == 0)]
    fn probe(&self) -> u32 {
        0
    }
}

#[kani::proof_for_contract(<Wrap<fn(u8) -> u8> as Probe>::probe)]
fn check() {
    fn id(x: u8) -> u8 {
        x
    }
    let w = Wrap(id as fn(u8) -> u8);
    let _ = w.probe();
}

using the following command line invocation:

kani min_fnptr.rs -Z function-contracts

with Kani version: 0.68.0 (CBMC 6.11.0). Resolution fails (location lines elided):

error: failed to resolve `<Wrap < fn (u8) -> u8 > as Probe>::probe`: unable to find implementation of associated function `Probe::probe` for Wrap<T>
   = note: Kani does not currently support stubs or function contracts on generic functions in traits.
            See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.

for Wrap<T> is the uninstantiated identity type: the fn(u8) -> u8 argument was dropped, so the concrete impl cannot match, and the note places this in the #1997 class. On the #4865 branch (head 25090dd), which instantiates concrete arguments, the same target with Wrap<u8> in place of the fn pointer resolves and verifies while this one still fails — isolating the residual to the rejected fn-pointer argument. The std Map target fails the same way there, ending for std::iter::Map<I, F>.

With the requested BareFn arm, this test case should resolve and verify as written — the impl carries a contract — giving the change a self-contained acceptance test.