Challenge 22: Verify the safety of str iter functions

[kasimte]

Towards #279.

Kani harnesses for Challenge 22: Verify the safety of str iter functions: the 15 safe functions with unsafe code in core::str::iter (Chars, SplitInternal, MatchesInternal, MatchIndicesInternal, SplitAsciiWhitespace), plus the Bytes::__iterator_get_unchecked safety contract. It adds 30 harnesses in a new #[cfg(kani)] mod verify. All additions are #[cfg(kani)]-gated, so non-Kani builds are unchanged; the harnesses run the real shipped bodies (no #[cfg(kani)] rewrites), and all pass via scripts/run-kani.sh.

The challenge lets us assume slice, str::pattern, and str::validations (assumptions 1–3), and that every iterator comes from valid UTF-8 (4). The pattern searchers are therefore modeled by spec-cited stubs at their call sites, so these proofs don't re-verify the str::pattern internals (Challenges 20/21).

Chars::advance_by runs over a symbolic str of arbitrary length but a bounded skip count (a justified unwind of its chunk loop), so the count is not literally unbounded. As with the other unbounded-verification challenges, that is left to the committee and noted under Limitations.

Success criteria

Criterion	Status
15 functions, safety (no UB)	Done. 30 harnesses over real bodies, including advanced-state (depth 1–2) and content variants.
__iterator_get_unchecked: write and prove the contract	Done, via proof_for_contract. The #[requires(idx < self.0.len())] contract already exists in main (core/src/str/iter.rs); this proves it.
Listed UBs absent	Done. Kani checks them on every harness.
Unbounded (arbitrary length)	Symbolic kani::any() length (not a fixed array), capped only at ~2^40, the --object-bits 12 offset budget. Whether a capped symbolic length counts as "arbitrary", as opposed to an uncapped loop contract, is the open committee question shared across the unbounded-verification challenges (see Limitations). advance_by also caps its skip count.

What the harnesses check

• Real bodies. The shipped methods run unchanged. The diff adds the verify module and one kani-gated feature(str_split_remainder, str_split_whitespace_remainder) line in alloc/src/lib.rs (those methods are unstable). Symbolic inputs sit on zeroed backing (alloc_zeroed), valid UTF-8 by construction, which is why the module lives in alloc::str.
• Assumption-cited stubs. 16 harnesses (9 SplitInternal, 7 Matches/MatchIndices, base and advanced-state) stub the searchers at their call sites under assumption 2. A stub returns any range that is in-bounds, on UTF-8 boundaries, and monotonic: a superset of the real searcher's outputs, so no-UB under the stub gives no-UB for the real searcher. The boundary alignment is assumption 2's grant, not something the caller derives.
• Advanced state. Split/Matches methods are proven from depth-1 and depth-2 states, not just fresh, each with a witness cover, so the proofs aren't first-call-only.
• Content. Chars::next and next_back are proven jointly over arbitrary length and arbitrary valid-UTF-8 content (hybrid prefix/suffix, both ends); the one coupling is that a width-w end char needs length ≥ w.
• Non-vacuity. Every assume-bearing harness carries a satisfied cover (65 total).

Upstream

The two loop-contract gaps behind advance_by's bounded count are ones we filed: kani#4893 (a loop inside a called combinator has no attach site) and kani#4943 (#[kani::loop_invariant] on a while let-chain fails to compile).

Limitations

• advance_by skip count is unwind-bounded; the str length stays symbolic. A loop invariant on the chunk-skip loop hits two walls today: its per-chunk .sum() is a combinator fold with no attach site (kani#4893), and #[kani::loop_invariant] on the loop's while … && let let-chain fails to compile (kani#4943), so neither fix alone would close it. Same gate as the other unbounded-verification challenges.
• Symbolic length is a free kani::any() capped only at ~2^40 (the --object-bits 12 offset budget), not a fixed array. No concrete length is assumed.
• Advanced-state depth is representative (1–2), not arbitrary. SplitInternal/MatchesInternal fields are private to core, so an arbitrary post-k-call state would need a shipped-code change this diff avoids. The safety obligation depends on current field values, not the call count, so depth 1–2 exercises the same shape as a deeper state.

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