Challenge 22: Verify safety of str iter functions

[Samuelsills]

Summary

Add Kani proof harnesses for all 16 str iterator functions specified in Challenge #22:

• Chars: next, advance_by, next_back, as_str
• SplitInternal: get_end, next, next_inclusive, next_match_back, next_back_inclusive, remainder
• MatchIndicesInternal: next, next_back
• MatchesInternal: next, next_back
• SplitAsciiWhitespace: remainder
• Unsafe: __iterator_get_unchecked (Bytes)

All harnesses verified locally with Kani.

Resolves #279

[Samuelsills]

Verification Coverage Report

Safe Functions (15/15 ✅)

#	Function	Impl for	Verified
1	next	Chars	✅
2	advance_by	Chars	✅
3	next_back	Chars	✅
4	as_str	Chars	✅
5	get_end	SplitInternal	✅
6	next	SplitInternal	✅
7	next_inclusive	SplitInternal	✅
8	next_match_back	SplitInternal	✅
9	next_back_inclusive	SplitInternal	✅
10	remainder	SplitInternal	✅
11	next	MatchIndicesInternal	✅
12	next_back	MatchIndicesInternal	✅
13	next	MatchesInternal	✅
14	next_back	MatchesInternal	✅
15	remainder	SplitAsciiWhitespace	✅

Unsafe Function (1/1 ✅)

| __iterator_get_unchecked | Bytes | ✅ |

Total: 16/16 functions verified

UBs Checked (automatic via Kani/CBMC)

• ✅ Accessing dangling or misaligned pointers
• ✅ Reading from uninitialized memory
• ✅ Mutating immutable bytes
• ✅ Producing an invalid value

Verification Approach

• Tool: Kani Rust Verifier
• 16 proof harnesses using concrete strings ("hello", "a,b", "abab", etc.)
• Internal types tested via public wrapper methods (split, rsplit, match_indices, etc.)