Verify safety of char-related Searcher methods (Challenge 20)

Add unbounded verification of 6 methods (next, next_match, next_back,
next_match_back, next_reject, next_reject_back) across all 6 char-related
searcher types in str::pattern using Kani with loop contracts.

Key techniques:
- Loop invariants on all internal loops for unbounded verification
- memchr/memrchr abstract stubs per challenge assumptions
- #[cfg(kani)] abstraction for loop bodies calling self.next()/next_back()
- Unrolled byte comparison to avoid memcmp assigns check failures

22 proof harnesses covering all 36 method-searcher combinations.
All pass with `--cbmc-args --object-bits 12` and no --unwind.

Resolves #277

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: jrey8343