[v3risec]

Summary

• Add Kani safety verification for Chars, SplitInternal, MatchIndicesInternal, MatchesInternal, and SplitAsciiWhitespace, and prove the existing Bytes::__iterator_get_unchecked contract with proof_for_contract.
• Check constructor states, iterator transitions, returned slice ranges, UTF-8 boundaries, and non-overlap during mixed forward/backward iteration.
• Add a shared searcher interval model and concrete integration cases for char, empty/non-empty string needles, and character slices. Empty-string cases execute the real searcher filtering methods.
• Extend Chars::advance_by verification with independent character-rank references, multiple chunk iterations, boundary restoration, and tail handling. Selected bounded prefix and window domains cover the full usize request range.
• Audit all assumptions and add reachability covers after every explicit assume, together with completion covers for every harness.
• Keep production code unchanged.

Verification

Verified locally using the repository-pinned Kani and Rust toolchain:

• 42 Challenge 22 harnesses and 2 existing pattern harnesses passed.
• All 357 coverage goals were satisfied.
• All 55 remaining unwinding checks passed.

Limitations

• String lengths, iterator windows, and concrete pattern inputs remain bounded.
• Searcher abstractions rely on Challenge 22's permitted Pattern correctness assumption; general refinement of these abstractions is not mechanically proved.
• Reachability covers establish feasible paths, not the validity of the assumptions themselves.

Resolves #279

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