Verify safety of str iter functions (Challenge 22)

[jrey8343]

Summary

Adds 17 Kani verification harnesses proving the safety of all unsafe operations in library/core/src/str/iter.rs, covering all 16 functions listed in Challenge 22 plus the __iterator_get_unchecked safety contract proof.

Functions verified

Function	Harness	Unsafe operation
Chars::next	check_chars_next	next_code_point + char::from_u32_unchecked
Chars::next_back	check_chars_next_back	next_code_point_reverse + char::from_u32_unchecked
Chars::advance_by	check_chars_advance_by	iter.advance_by(slurp).unwrap_unchecked()
Chars::advance_by (CHUNK_SIZE)	check_chars_advance_by_large	iter.advance_by(bytes_skipped).unwrap_unchecked()
Chars::as_str	check_chars_as_str	from_utf8_unchecked(self.iter.as_slice())
SplitInternal::get_end	check_split_internal_get_end	get_unchecked(self.start..self.end)
SplitInternal::next	check_split_internal_next	get_unchecked(self.start..a)
SplitInternal::next_inclusive	check_split_internal_next_inclusive	get_unchecked(self.start..b)
SplitInternal::next_back	check_split_internal_next_back	get_unchecked(b..self.end), get_unchecked(self.start..self.end)
SplitInternal::next_back (terminator)	check_split_internal_next_back_terminator	Recursive path with allow_trailing_empty=false
SplitInternal::next_back_inclusive	check_split_internal_next_back_inclusive	get_unchecked(b..self.end), get_unchecked(self.start..self.end)
SplitInternal::remainder	check_split_internal_remainder	get_unchecked(self.start..self.end)
MatchIndicesInternal::next	check_match_indices_internal_next	get_unchecked(start..end)
MatchIndicesInternal::next_back	check_match_indices_internal_next_back	get_unchecked(start..end)
MatchesInternal::next	check_matches_internal_next	get_unchecked(a..b)
MatchesInternal::next_back	check_matches_internal_next_back	get_unchecked(a..b)
SplitAsciiWhitespace::remainder	check_split_ascii_whitespace_remainder	from_utf8_unchecked
Bytes::__iterator_get_unchecked	check_bytes_iterator_get_unchecked	Safety contract #[requires(idx < self.0.len())]

Verification approach

• Chars harnesses: Symbolic char via kani::any::<char>() encoded to UTF-8 via encode_utf8, covering all Unicode scalar values. Verifies no UB in next_code_point/from_u32_unchecked/from_utf8_unchecked.
• SplitInternal/MatchIndices/Matches harnesses: Symbolic ASCII char pattern (kani::any() + assume(c.is_ascii())) with 2-byte haystack "ab", exercising both match and no-match code paths through the Searcher.
• advance_by large: Concrete 33-byte ASCII string exercises the CHUNK_SIZE=32 branch with its chunk processing, trailing continuation byte skipping, and final character-width-based advancement.
• Bytes: Proves the existing #[requires(idx < self.0.len())] contract is sufficient for safety.

All 17 harnesses verified locally (18 total including pre-existing check_small_slice_eq).

Test plan

• All 17 new harnesses pass with kani verify-std using -Z loop-contracts --cbmc-args --object-bits 12
• Pre-existing harnesses remain passing
• Code formatted with rustfmt

[jrey8343]

CI is passing — ready for review.