Autoharness: support the `MultiCharEq` searcher types in `core::str::pattern`

[CYJ904]

Requested feature

Autoharness support for the searcher structs in core::str::pattern that wrap MultiCharEqSearcher — CharArraySearcher<'a, N>, CharArrayRefSearcher<'a, 'b, N> and CharSliceSearcher<'a, 'b> — which appear in argument position as the &mut self receivers of the Searcher/ReverseSearcher methods.

Use case

On a whole-library verify-std run, 27 functions in core are skipped for a missing Arbitrary implementation on one of these three types: next, next_match, next_reject, their _back variants, haystack, and the Clone/Debug implementations (9 per type). A further 23 functions in core are skipped on the other searchers in the same file — CharPredicateSearcher (8), CharSearcher (8) and StrSearcher (7) — which are out of scope here for the reasons given at the end.

These three types are all newtype wrappers around one private struct, so a single model shape covers them:

struct MultiCharEqSearcher<'a, C: MultiCharEq> {
    char_eq: C,
    haystack: &'a str,
    char_indices: str::CharIndices<'a>,
}

Constructing a valid instance needs no unsafe: none of these structs contains a MaybeUninit or a union, and the only raw pointers are inside slice::Iter, reached safely via bytes.iter(). Calling into_searcher establishes the representation invariants by construction rather than by assumption, the same way any_c_str_ref uses from_bytes_until_nul (#4803). The invariants that would otherwise have to be assumed are that the bytes remaining in char_indices are haystack.as_bytes()[lo..hi] with front_offset == lo, and that lo and hi are UTF-8 char boundaries.

Why the existing bounded-argument route does not reach them

&CStr (#4803), &ByteStr (#4805) and &Wtf8 (#4808) are references to an unsized type, so each is handled by adding a match arm inside the bounded branch of call_kani_any_for_ty. That branch is entered only under TyKind::RigidTy(RigidTy::Ref(region, inner, inner_mut)), and both the storage borrow and model_ret_ty are built from that region and inner. A searcher is a by-value struct, so it never reaches the branch and has no region to reuse.

It therefore falls through to implements_arbitrary / can_derive_arbitrary, and can_derive_arbitrary returns false for any ADT whose generic arguments contain a lifetime, before any field is examined. Every searcher is parameterised over the haystack lifetime, so all of them are rejected there. Relaxing that check alone would not help: the fields include haystack: &'a str, which the same function rejects on the grounds that storage for the referent would dangle once the synthesized any() returns. This is the same reason any_str_ref takes caller-owned [u8; N] storage instead of being an Arbitrary impl — Arbitrary::any() -> Self has nowhere to own the haystack bytes.

Proposed shape

A model taking harness-owned storage, as the existing bounded models do:

fn any_char_array_searcher<const N: usize, const M: usize>(
    storage: &mut [u8; N],
) -> CharArraySearcher<'_, M>

The haystack comes from storage the way any_str_ref builds a &str; the [char; M] needle is kani::any(), since [T; N] and char both implement Arbitrary; into_searcher then produces the searcher. CharArrayRefSearcher and CharSliceSearcher need a second storage local for the borrowed [char].

Wiring this up follows #4804 closely: a KaniModel variant with its fn_marker, an AnyModels field and lookup, a shared type predicate in the shape of is_c_str so that eligibility and generation cannot disagree, and a script-based test alongside cargo_autoharness_c_str. Two pieces differ:

• call_kani_any_for_ty needs a by-value branch placed ahead of the implements_arbitrary check, with a synthesized ReErased region for the storage borrow (as the RawPtr branch already does) and generic args carrying a const parameter unrelated to the storage length. This branch bypasses the final else, so it does not get assume_scalar_niche, the mined-invariant assumptions or assume_safe; since into_searcher establishes the invariants by construction, none of those appear to be needed, but that is worth confirming.
• autoharness_supported_arg_ty needs the new predicate in two places: the by-value case, and an arm in the Ref branch ahead of the _ => arbitrary_or_derive(ty) fallback, so that &mut Searcher receivers are classified as Bounded rather than falling into the lifetime rejection. call_kani_any_for_ty needs no change for the &mut case — its general Ref arm already recurses into the pointee and borrows the result, passing mutability through.

One flow-specific note: core::str::pattern is #[unstable(feature = "pattern")]. In the verify-std flow the models expand inside core itself, so naming Pattern needs no gate; in the normal flow they are compiled as part of the kani crate against std, which would need #![feature(pattern)] in library/kani/src/lib.rs.

Out of scope for this issue, as follow-ups if the approach lands: CharPredicateSearcher<'a, F> needs a concrete F: FnMut(char) -> bool, which is a modelling choice rather than a generation one; StrSearcher carries a TwoWaySearcher whose crit_pos/period/byteset must be exactly what TwoWaySearcher::new computes, so it would be built through that constructor rather than field by field; CharSearcher::next_match is the shape reported in #4790, so it may be blocked on that.

I am planning to work on this and would welcome a steer on whether the by-value branch is the shape you would want, or whether a more general mechanism for ADTs borrowing from harness-owned storage is preferred.