Loop contracts: locals of the builtin `memcmp` model fail the assigns check when the loop body compares slices with `==`

[jrey8343]

I tried this code (a scan loop with a loop contract whose body compares a window of the haystack against a short needle with ==, the shape of CharSearcher::next_match in core::str::pattern):

#![feature(stmt_expr_attributes, proc_macro_hygiene)]

pub fn find(haystack: &[u8], needle: &[u8]) -> Option<usize> {
    let mut finger = 0;
    #[kani::loop_invariant(finger <= haystack.len())]
    while finger < haystack.len() {
        finger += 1;
        if finger >= needle.len() {
            if let Some(window) = haystack.get(finger - needle.len()..finger) {
                if window == needle {
                    return Some(finger - needle.len());
                }
            }
        }
    }
    None
}

#[cfg(kani)]
mod verify {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)] // for the <= 4-byte needle comparison only
    fn check_find() {
        const N: usize = 16;
        let hay: [u8; N] = kani::any();
        let len: usize = kani::any();
        kani::assume(len <= N);
        let needle: [u8; 4] = kani::any();
        let nlen: usize = kani::any();
        kani::assume(1 <= nlen && nlen <= 4);
        if let Some(i) = find(&hay[..len], &needle[..nlen]) {
            assert!(i + nlen <= len);
            assert!(&hay[i..i + nlen] == &needle[..nlen]);
        }
    }
}

using the following command line invocation:

cargo kani -Z loop-contracts -Z function-contracts --harness check_find

with Kani version: 0.67.0 (release; CBMC 6.8.0; nightly-2025-11-21, aarch64-apple-darwin)

I expected to see this happen: verification success. The loop invariant holds (base and step checks pass), and finger is the only variable the loop writes.

Instead, this happened:

SUMMARY:
 ** 4 of 131 failed
Failed Checks: Check that sc1 is assignable
 File: "<builtin-library-memcmp>", line 27, in memcmp
Failed Checks: Check that sc2 is assignable
 File: "<builtin-library-memcmp>", line 27, in memcmp
Failed Checks: Check that res is assignable
 File: "<builtin-library-memcmp>", line 27, in memcmp
Failed Checks: Check that n is assignable
 File: "<builtin-library-memcmp>", line 25, in memcmp

VERIFICATION:- FAILED
Verification Time: 9.687538s

Every other check passes, including Check invariant before entry for loop find.0, Check invariant after step for loop find.0, and the assignable checks for the loop's own locals (finger, window, the hoisted temporaries). The four failures are the locals of CBMC's builtin memcmp model. window == needle lowers to <[u8] as PartialEq<[u8]>>::eq → SlicePartialEq::equal → core::intrinsics::compare_bytes, which Kani maps to memcmp; the model is linked in after the loop's assigns clause has been inferred, so its locals are not covered.

Things I tried that do not work around it:

• Explicit #[kani::loop_modifies(&finger)] on the loop: the same four memcmp failures, plus the loop-body locals that Kani hoists (window, var_16) now fail too, since they cannot be named in the clause.
• Stubbing the comparison: #[kani::stub(<[u8] as core::cmp::PartialEq<[u8]>>::eq, model)] is rejected with "unable to find implementation of associated function std::cmp::PartialEq::eq for [u8] … Kani does not currently support stubs or function contracts on generic functions in traits" (the impl is the blanket impl<A, B> PartialEq<[B]> for [A]). compare_bytes is a bodyless intrinsic and cannot be stubbed either; SlicePartialEq is private to core.
• Control: replacing window == needle with element-wise comparisons (window[0] == needle[0] && window[last] == needle[last]) verifies in 2.4 s with the same invariant, so the loop contract itself is fine; the slice comparison is the only trigger.

Also reproduced on main at b07abe8 (built with cargo build-dev, run with CBMC 6.10.0 on PATH rather than the pinned 6.11.0): the same four memcmp checks fail, 4 of 130 failed, everything else passes.

Context: this is the one thing standing between bounded and unbounded proofs of CharSearcher::next_match/next_match_back in model-checking/verify-rust-std (Challenge 20, PR model-checking/verify-rust-std#537); with a loop invariant on the two real memchr loops everything verifies except these four checks. A fix in either direction would do: have the assigns inference cover the builtin models' locals, or let a Rust-level model replace the slice comparison (a stub target for compare_bytes, or stub support for the blanket slice PartialEq impl).