Loop contracts: for loops over iterators without a KaniIntoIter impl (e.g. char::DecodeUtf16) cannot carry a contract #4907

Requested feature: allow #[kani::loop_invariant] on a for loop over any Iterator, not only over the types that implement kani::KaniIntoIter (at this commit: arrays, &[T], &mut [T] and slice::Iter<T> with T: Copy, Range, StepBy, Chain, Zip, Map, Enumerate, Take, Rev). For example, there could be a fallback that lowers for x in it to let mut it = it.into_iter(); while let Some(x) = it.next(), keeping the invariant on the loop head.

Use case: verifying std code for unbounded input length. The only loop of alloc::string::String::from_utf16 is

for c in char::decode_utf16(v.iter().cloned()) { ... }

This loop is written directly in the function under verification, so it can be annotated. But DecodeUtf16<Cloned<slice::Iter<'_, u16>>> has no KaniIntoIter impl, so the contract is rejected at compile time. Rewriting the production loop only for verification is not acceptable in model-checking/verify-rust-std.

Link to relevant documentation: https://model-checking.github.io/kani/reference/experimental/loop-contracts.html (Limitations, item 1).

Test case (Kani 0.67.0 built from source at 152c6a8, CBMC 6.10.0, Arch Linux x86_64):

#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]

pub fn from_utf16_copy(v: &[u16]) -> Option<String> {
    let mut ret = String::with_capacity(v.len());
    #[kani::loop_invariant(kani::index <= v.len())]
    for c in char::decode_utf16(v.iter().cloned()) {
        let Ok(c) = c else { return None; };
        ret.push(c);
    }
    Some(ret)
}

#[kani::proof]
fn check_from_utf16() {
    let a: [u16; 4] = kani::any();
    let n: usize = kani::any_where(|n: &usize| *n <= 4);
    let _ = from_utf16_copy(&a[..n]);
}

kani for_decode_utf16.rs -Z loop-contracts

error[E0277]: the trait bound `std::char::DecodeUtf16<std::iter::Cloned<std::slice::Iter<'_, u16>>>: kani::KaniIntoIter` is not satisfied
 --> for_decode_utf16.rs:8:14
  = help: the following other types implement trait `kani::KaniIntoIter`:

Note: kani::index is a natural thing to use here, but a length-based fallback would not be available for iterators like DecodeUtf16 whose item count is not known in advance. A while let-style lowering, where the invariant refers to the iterator state, would still be useful.

Doc note: at this commit the loop-contracts page lists while let loops as unsupported. The loop_invariant macro in library/kani_macros/src/sysroot/loop_contracts/mod.rs, however, rewrites while let into loop + match. If that is intended to be supported, the Limitations list could be updated.