Resolve fn-pointer type arguments in contract target paths

[kasimte]

A contract target whose type arguments include a fn-pointer type (<Wrap<fn(u8) -> u8> as Probe>::probe, or the standard adapters' <std::iter::Map<std::slice::Iter<u8>, fn(&u8) -> u8> as Iterator>::__iterator_get_unchecked) failed to resolve: resolve_ty's Type::BareFn arm returned unsupported, so the fn-pointer argument was dropped and the concrete impl could not match. This PR builds the fn-pointer type in that arm (Rust ABI, non-variadic; inputs and output resolved recursively; lifetimes erased like every other path argument; safety carried through), so these targets resolve.

Verification

test (-Zfunction-contracts)	expect
tests/kani/FunctionContracts/generic_fn_pointer_argument.rs	3 targets verify. A plain fn-pointer argument (fn(u8) -> u8); a reference-carrying fn pointer (fn(&u8) -> u8) whose impl type is late-bound (for<'a> fn(&'a u8) -> u8), where the erased argument still matches; and an unsafe fn pointer (safety carried through the built signature). The three impls have distinct postconditions, so each harness verifies only if resolution picks its own fn-pointer instantiation.
tests/expected/function-contract/generic_fn_pointer_cabi.rs	still fails to resolve (expected-output test; the diagnostic is the pass). A non-Rust-ABI fn pointer (extern "C" fn(u8) -> u8) is not built by the arm and keeps the uninstantiated type.

Confirmed locally: generic_fn_pointer_argument verifies 3/3; generic_fn_pointer_cabi fails to resolve (the expected diagnostic); the resolver suites are unchanged (generic_argument_instantiation 6, cross_module_multiple_impls 7, multiple_inherent_impls 3). The std target <std::iter::Map<std::slice::Iter<u8>, fn(&u8) -> u8> as std::iter::Iterator>::__iterator_get_unchecked resolves, failing only on the absent contract (__iterator_get_unchecked has no contract). CI runs the full suite on the pinned toolchain.

Mechanism: fn-pointer types were the last commonly-written argument shape resolve_ty rejected outright. Building the signature (Rust ABI only, non-variadic, arguments resolved through the same resolve_ty recursion, lifetimes erased, unsafe safety carried) makes the argument concrete, and the existing full resolution then matches the impl. Anything the arm does not build (a non-Rust ABI, or a variadic fn pointer) keeps the old uninstantiated type, so nothing that resolved before changes.

Resolves #4909. That issue reports this wall for the standard iterator adapters: Map and Filter carry a mapping or predicate function argument whose fn-pointer instantiation could not be named. The Challenge 16 submission (model-checking/verify-rust-std#549) falls back to a kani::assume mirror harness for Map's __iterator_get_unchecked for this reason; with the arm, Map<Iter<u8>, fn(&u8) -> u8> resolves as a proof_for_contract target. As #4909 notes, closure instantiations stay out of reach for any resolver change (a closure's type cannot be written in path syntax), so only the fn-pointer instantiations are addressed here. BareFn is also one of the two argument kinds #4830 names as prerequisites for the semantic-resolution rewrite; it lands here on its own, ahead of that refactor.

Scope: lifetimes are erased, so a higher-ranked fn pointer resolves against an erased signature; if a fn(&'static u8) -> u8 sibling impl also exists, the higher-ranked target resolves to it instead. The generic_fn_pointer_higher_ranked.rs fixme test documents this, and binding the late-bound regions is tracked as a follow-up (#4933).

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

[Copilot]

Copilot review overview

🟢 Approval recommended

The implementation is focused, consistent with existing lifetime handling, and covers supported and unsupported cases.

Review effort: Balanced
Findings: None

What changed in this PR

Adds contract-target resolution for Rust ABI function-pointer type arguments.

Changes:

• Constructs safe/unsafe, non-variadic Rust fn-pointer types recursively.
• Adds positive resolution tests and preserves unsupported C ABI behavior.

File	Description
kani-compiler/​src/​kani_middle/​resolve/​type_resolution.rs	Resolves supported bare function types.
tests/​kani/​FunctionContracts/​generic_fn_pointer_argument.rs	Tests plain, reference, and unsafe pointers.
tests/​expected/​function-contract/​generic_fn_pointer_cabi.rs	Tests unsupported C ABI resolution.
tests/​expected/​function-contract/​generic_fn_pointer_cabi.expected	Records the expected diagnostic.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.