Verify safety of str iter functions (Challenge 22)

[jrey8343]

Verify safety of str iter functions (Challenge 22)

Stacked on #538 (which contains #537). This branch carries no pattern.rs delta of its own — the searchers the iterators drive are exactly the ones verified in #537/#538. Review the delta: the verification module in str/iter.rs.

Summary

Complete rework per review: all #[cfg(kani)] abstractions are gone. The previous branch carried a stale copy of the #537/#538 pattern.rs abstractions plus a swapped-out Chars::advance_by; all of it is removed. iter.rs's product code is byte-identical to main, and the harnesses drive the real iterator internals over the real searchers:

• Chars::advance_by runs its real body — the chunked-skip loop (enterable, empty at this input size since as_chunks::<32> of ≤5 bytes yields no chunks), the trailing-continuation-byte loop, and the per-char utf8_char_width/unwrap_unchecked loop — with a fully symbolic count, asserting the Ok/Err contract against the true char count.
• SplitInternal / MatchesInternal / MatchIndicesInternal harnesses use fully symbolic multibyte haystacks (≤5 symbolic bytes, all four UTF-8 width classes) and fully symbolic char patterns — replacing the previous single-ASCII-char inputs — so the get_unchecked slicing inside the iterators is checked against indices produced by the real CharSearcher::next_match/next_match_back (verified in Verify safety of char-related Searcher methods (Challenge 20) #537), not assumed-valid stubs.
• Bytes::__iterator_get_unchecked: the pre-existing #[requires(idx < self.0.len())] is now checked by a #[kani::proof_for_contract] harness (under CI's --no-assert-contracts a contract is only verified by such a harness — previously it was decorative).
• The only stubs are core::slice::memchr::{memchr,memrchr}, replaced per-harness at their real call sites by semantically identical naive scans (Challenge 22 assumption 1; the Verify safety of NonZero operations (Challenge 12) #544 pattern — zero kani::any, zero kani::assume, fully unwound).

Coverage vs the challenge function list

Challenge function	Harness
Chars::next / advance_by / next_back / as_str	check_chars_next / check_chars_advance_by / check_chars_next_back / check_chars_as_str
SplitInternal::get_end	exercised on exhaustion inside check_split_next / check_split_next_back
SplitInternal::next	check_split_next
SplitInternal::next_inclusive	check_split_inclusive_next
SplitInternal::next_match_back	the searcher call inside check_split_next_back / check_split_terminator_next_back (there is no method of that name on SplitInternal; this is the next_match_back call its next_back makes)
SplitInternal::next_back_inclusive	check_split_inclusive_next_back
SplitInternal::remainder	check_split_remainder
MatchIndicesInternal::next / next_back	check_match_indices_next[_back] (asserts returned index is a char boundary and the slice equals the match)
MatchesInternal::next / next_back	check_matches_next[_back]
SplitAsciiWhitespace::remainder	check_split_ascii_whitespace_remainder
Bytes::__iterator_get_unchecked (safety contract)	check_bytes_iterator_get_unchecked (proof_for_contract)

Verification is bounded — stated plainly

Haystacks ≤ 5 symbolic bytes, patterns fully symbolic chars, unwind bounds stated per harness (every iteration consumes ≥1 byte). The challenge's unbounded requirement is not met at full generality; per review guidance these are documented, justified bounds. Patterns are chars, so the iterators drive the CharSearcher path; &str-pattern (Two-Way) behavior under the iterators is covered by Challenge 22's assumption 2 (all of pattern.rs may be assumed) together with the direct StrSearcher/TwoWaySearcher verification in #538.

Verification results

Local, pinned Kani 0.67.0 (d4df833), CI's exact flags:

Full str::iter::verify suite: 16 of 16 harnesses verified, 0 failures. Times: most harnesses 1–12s; check_chars_advance_by (all three real loops with a fully symbolic count) ~15 min; the proof_for_contract harness 1.1s.

Also in this PR

• Merged with current main (current Kani pin d4df833); the stale divergent pattern.rs copy is replaced wholesale by Verify safety of StrSearcher (Challenge 21) #538's.
• The previous description's unbounded-via-abstraction claims are retracted; this description matches the diff.

[Copilot]

Pull request overview

This PR adds Kani-focused abstractions and proof harnesses to support unbounded verification (no unwind bounds) of the safety of str iterator methods that contain unsafe operations, primarily by eliminating/bypassing internal search loops under #[cfg(kani)].

Changes:

• Added #[cfg(kani)] nondeterministic abstractions in str/pattern.rs to avoid unbounded loops in Searcher implementations (including Two-Way search) during Kani runs.
• Added a #[cfg(kani)] abstraction of Chars::advance_by in str/iter.rs and introduced a #[cfg(kani)] verify module with multiple Kani proof harnesses.
• Introduced/used a Kani contract style (#[requires(...)]) and a harness to exercise the Bytes::__iterator_get_unchecked safety precondition.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 10 comments.

File	Description
library/core/src/str/pattern.rs	Adds Kani-only loop abstractions for several Searcher implementations (char search, multi-char predicates, str search, two-way search) to enable unbounded verification.
library/core/src/str/iter.rs	Adds a Kani-only abstraction for Chars::advance_by and introduces Kani proof harnesses for iterator safety contracts.

[feliperodri]

Thanks for the work here. Unfortunately this uses the same #[cfg(kani)] abstraction approach as #537/#538, so the proofs pass without verifying the real iterator/searcher code that Challenge 22 targets.

The verified code is a stub, and it assumes its own safety conclusion

Chars::advance_by (str/iter.rs): the real implementation (three while loops walking UTF-8) is under #[cfg(not(kani))]. Under Kani it's replaced by:

let bytes_consumed: usize = kani::any();
kani::assume(bytes_consumed <= bytes_len);
let rem = unsafe { from_utf8_unchecked(self.iter.as_slice()) };
kani::assume(rem.is_char_boundary(bytes_consumed));           // assumes the safety conclusion
if bytes_consumed > 0 { unsafe { self.iter.advance_by(bytes_consumed).unwrap_unchecked() }; }

The unsafe op runs only with an already-assumed-valid bytes_consumed, so it can't fail. The loop logic that actually computes the byte count and determines whether it lands on a char boundary — the only place a bug could occur — is compiled out and never verified.

SplitInternal / MatchesInternal / MatchIndicesInternal: their get_unchecked(start..end) safety depends on the indices returned by CharSearcher::next_match() / next_match_back(). Those are the #[cfg(kani)] nondeterministic stubs in pattern.rs (23 #[cfg(not(kani))] blocks) that return assumed-in-bounds (start, end) without running the real search. So the get_unchecked "safety" is discharged by assumed-valid indices, and the real search that produces them isn't verified. The automated reviewer independently flagged that these abstractions don't even constrain the indices to char boundaries, and that TwoWaySearcher::new's abstraction is an under-approximation.

Scorecard vs. Challenge 22

• Criterion 2 (C ⟹ safety / indices on boundaries): not met — assumed via kani::assume, not derived.
• Criterion 3 (C preserved after each method): not met — the method run under Kani is the stub.
• Unbounded: true of the stubs, vacuous for the real code.

Also

• Bytes::__iterator_get_unchecked's #[requires(idx < self.0.len())] has no proof_for_contract, so it's not verified as a contract (a plain proof calling it ignores the contract). If you mirror it with a kani::assume in the harness, note that in the code so they can't drift.

Direction

Verify the real code: keep advance_by's loops and the searcher bodies compiled under Kani (use loop contracts with meaningful invariants, or a justified unwind), stub memchr/memrchr at their real reachable call sites per the challenge's allowed assumptions, and derive the boundary property rather than kani::assume-ing it. This PR also depends on the searcher abstractions under review in #537/#538.

[jrey8343]

@feliperodri Thanks for the review. This is the same ground-up rework as #537/#538, applied here: all cfg(kani) abstractions are gone, and the branch now carries no pattern.rs delta of its own — it stacks on #538, so the searchers under the iterators are exactly the verified ones.

On your points:

1. Chars::advance_by — the real body (all three loops) is compiled and verified: the chunked-skip loop, the trailing-continuation-byte loop, and the per-char loop whose advance_by(slurp).unwrap_unchecked() was the concern. The count is fully symbolic, and the harness asserts the Ok/Err contract against the true char count of the input. Nothing about the consumed byte count is assumed.

2. SplitInternal/MatchesInternal/MatchIndicesInternal over stubbed searchers — the nondeterministic searcher abstractions are deleted (in #537/#538); the iterators now drive the real CharSearcher::next_match/next_match_back, so the get_unchecked slicing is discharged against indices the real search computes. The match_indices harnesses additionally assert the returned index is a char boundary and that the haystack slice at it equals the match. The only stubs anywhere are naive, semantically identical memchr/memrchr scans at their real call sites (assumption 1; the #544 pattern).

3. Inputs — the single-char/ASCII-only inputs are gone: all harnesses use arbitrary multibyte UTF-8 haystacks (≤5 symbolic bytes, contents and length symbolic) with fully symbolic char patterns, generated constructively (see the #537 thread for why from_utf8 can't be used as a filter under -Z loop-contracts).

4. Bytes::__iterator_get_unchecked decorative contract — now checked by a #[kani::proof_for_contract(Bytes::__iterator_get_unchecked)] harness, so the #[requires] is verified rather than mirrored by a hand-rolled assume.

The description carries an explicit coverage table mapping every function in the challenge list to its harness (including the note that "SplitInternal::next_match_back" is the searcher call next_back makes — there is no method of that name on the type), states the bounds plainly, and notes that &str-pattern (Two-Way) behavior under the iterators rests on assumption 2 plus the direct verification in #538. Fresh local results with the pinned Kani and CI's exact flags are in the description.