`<[u8]>::contains` does not converge even on fully concrete data (memchr specialization); `iter().any` verifies in 0.2s

[jakrawcz]

Summary

<[u8]>::contains does not converge under Kani even on fully concrete data, while the same predicate written as an explicit scan (iter().any(..)) verifies in ~0.2 s. Core specializes u8-slice contains to a memchr-style routine (SpecSliceContains for u8), and CBMC's symbolic execution appears unable to make progress through it.

We hit this in a production verification suite: three differently-shaped harnesses of a small lookup ([u8; 20]::contains over reserve membership lists) hung for 55–80+ minutes each on CI, including one whose inputs were entirely constant. Replacing the two contains calls with iter().any(|&g| g == id) made the fully symbolic version of the same harness verify in 6.3 s.

Minimal reproduction

#[cfg(kani)]
mod verification {
    /// Does not converge (killed after minutes).
    #[kani::proof]
    fn contains_concrete() {
        let groups: [u8; 20] = [0; 20];
        assert!(!groups.contains(&7u8));
    }

    /// Same predicate, explicit scan: ~0.2 s.
    #[kani::proof]
    fn any_concrete() {
        let groups: [u8; 20] = [0; 20];
        assert!(!groups.iter().any(|&g| g == 7u8));
    }
}

cargo kani --harness any_concrete → VERIFICATION:- SUCCESSFUL, Verification Time: 0.23s.
cargo kani --harness contains_concrete → no verdict after 60 s (killed); inside our larger crate the same probe was killed at 150 s, and the real harnesses at 55–80 min.

Environment

• kani 0.67.0 (CBMC 6.8.0 as bundled), default flags (no stubs, no unwind bounds)
• macOS aarch64 (Apple Silicon) locally; reproduced on ubuntu-latest (x86_64) in CI
• edition 2021 crate with no dependencies

Expected

A contains over 20 concrete bytes should be as cheap as the explicit scan — ideally Kani (or the std-library contract shims) would model memchr specializations without symex getting stuck, or at least surface this as a known limitation.

Workaround

An explicit iter().any(..) scan (behavior-identical for prod).