Contract attributes on a specialization default fn fail to parse ("expected fn") #5116

Using #[kani::ensures] and #[kani::modifies] on a default fn (with min_specialization) fails during macro expansion with expected `fn` at the default keyword. The E0046 and E0520 errors that follow are a knock-on effect: the method disappears from the impl. The same attributes on the specializing u8 method verify successfully.

I tried this code (standalone crate, no dependencies):

#![feature(min_specialization)]
#[cfg(kani)]
mod check {
    trait SmallSort { fn small_sort(v: &mut [u8]); }
    impl<T> SmallSort for T {
        #[kani::ensures(|_| true)]
        #[kani::modifies(v)]
        default fn small_sort(v: &mut [u8]) { pair(v); }
    }
    impl SmallSort for u8 {
        fn small_sort(v: &mut [u8]) { pair(v); }
    }
    fn pair(v: &mut [u8]) {
        if v.len() == 2 && v[1] < v[0] { v.swap(0, 1); }
    }
    #[kani::proof_for_contract(<u16 as SmallSort>::small_sort)]
    #[kani::unwind(3)]
    fn check_default() {
        let mut v: [u8; 2] = kani::any();
        <u16 as SmallSort>::small_sort(&mut v);
    }
}

Command:

cargo kani -Z function-contracts

Tested with Kani built from source at 9461e07af7ec (reports 0.68.0, nightly-2026-10-12) and at main 744b3e84d6eb (nightly-2026-10-23). Same output on both. CI run.

I expected the crate to compile and the harness to check the contract of the blanket default fn (u16 selects it).

Instead, this happened:

error: expected `fn`
 --> src/lib.rs:8:9
  |
8 |         default fn small_sort(v: &mut [u8]) { pair(v); }
  |         ^^^^^^^

error[E0046]: not all trait items implemented, missing: `small_sort`
 --> src/lib.rs:5:5

error[E0520]: `small_sort` specializes an item from a parent `impl`, but that item is not marked `default`
  --> src/lib.rs:11:9

Moving the same two attributes to the non-default impl SmallSort for u8 (and targeting <u8 as SmallSort>::small_sort) gives VERIFICATION:- SUCCESSFUL.

Likely cause: contract_main parses the annotated item as syn::ItemFn (mod.rs#L689), and ItemFn doesn't accept default; only syn's impl-item parser does. I only tried ensures and modifies; requires goes through the same function, so I'd expect the same, but I haven't run it.

Context: this blocks contracts on the blanket small_sort impls in core::slice::sort::shared::smallsort (verify-rust-std Challenge 8). For now we put contracts on wrapper functions instead.

Disclosure: I used an AI assistant to help prepare this report.