Verify safety of StrSearcher substring search methods (Challenge 21)

Add 14 Kani proof harnesses verifying that the 6 Searcher/ReverseSearcher
trait methods on StrSearcher produce indices on valid UTF-8 char boundaries
and cause no undefined behavior, for both EmptyNeedle and TwoWay variants.

Abstractions added under #[cfg(kani)] for CBMC-intractable internals:
- TwoWaySearcher::new(), next(), next_back() — nondeterministic results
  satisfying bounds contracts
- EmptyNeedle chars() iteration — avoids Chars iterator raw pointer blowup
- UTF-8 boundary correction loops — nondeterministic 0-3 byte skip
- next_match/next_match_back EmptyNeedle loop arms
- next_reject/next_reject_back straight-line overrides

All verification is unbounded (no fixed unwind bounds). The entire
StrSearcher implementation contains zero unsafe blocks, so UB-freedom
is structurally guaranteed by Rust's type system.

Author: jrey8343