[CYJ904]

Resolves #4811. Part of #4879.

With --bounded-arguments, autoharness can now generate CharArraySearcher<'_, N>, CharArrayRefSearcher<'_, '_, N> and CharSliceSearcher<'_, '_> arguments, by value, & or &mut. These are the searchers for [char; N], &[char; N] and &[char] patterns in core::str::pattern.

Changes

1. New kani_core models build the searcher through the public Pattern::into_searcher API over a bounded nondeterministic haystack (from any_str_ref, string bound) and a nondeterministic needle ([char; N], or a &[char] of up to the slice bound for CharSliceSearcher). They then advance it a nondeterministic number of steps from each end, so that searchers in partially advanced states are also generated.
2. multi_char_eq_searcher_kind identifies the three types by definition path and is shared by the eligibility check and harness generation.
3. The searchers' Debug::fmt methods are verified as ordinary functions rather than through the formatting-trait model, since the searcher needs harness-owned storage.
4. The storage-array construction of the slice/str branches is factored into build_any_array_storage_ref.
5. The reference page and the --slice-bound/--string-bound help text document the new argument types.

Testing

1. New test cargo_autoharness_multichareq_searcher: 10 harnesses, 9 pass and 1 fails as expected, and all 90 cover properties are satisfied. It takes about 7 minutes with --string-bound 4 --slice-bound 4. I kept these bounds because smaller ones exclude 4-byte UTF-8 characters or leave some covers unreachable, but happy to lower them if CI time is a concern.
2. All 42 autoharness regression tests pass. cargo fmt --check and cargo clippy --workspace --tests -- -D warnings pass.

Results on verify-std

1. With --bounded-arguments, all 27 functions listed in Autoharness: support the MultiCharEq searcher types in core::str::pattern #4811 now get harnesses (9 per searcher type). The other 23 functions in pattern.rs (CharPredicateSearcher, CharSearcher, StrSearcher) are still skipped and are out of scope here.
2. Verifying the 27 harnesses (release build, string bound 4, slice bound 16, 10-minute timeout each): 8 fail and 19 time out.
3. The 8 failures are the preconditions of char::from_u32_unchecked and hint::unreachable_unchecked, caused by Autoharness: &str arguments can be invalid UTF-8 under verify-std, causing spurious failures #5030 (&str from any_str_ref can be invalid UTF-8 under verify-std). CBMC traces for CharArraySearcher::haystack and CharArraySearcher::next confirm this: the haystack bytes are mis-validated by from_utf8, and the failures occur while the model advances the searcher, before the function under test runs. For next, the call graph shows the unreachable_unchecked check is reachable only from UTF-8 decoding. The other 6 fail on the same two checks and very likely share the cause, but I did not trace them individually.

Notes

1. This PR and Restructure and update the autoharness reference page #4991 both edit docs/src/reference/experimental/autoharness.md. I'll resolve the conflict in whichever merges second.
2. Related: Challenge 20: Verify char-class Searcher safety in str::pattern with Kani verify-rust-std#722 adds hand-written harnesses for these searchers and builds haystacks with encode_utf8.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.