[v3risec]

Summary

• Add Kani safety verification for Chars, SplitInternal, MatchIndicesInternal, MatchesInternal, and SplitAsciiWhitespace, and prove the existing Bytes::__iterator_get_unchecked contract with proof_for_contract.
• Check constructor states, iterator transitions, returned slice ranges, UTF-8 boundaries, and non-overlap during mixed forward/backward iteration.
• Add a shared searcher interval model and concrete integration cases for char, empty/non-empty string needles, and character slices. Empty-string cases execute the real searcher filtering methods.
• Extend Chars::advance_by verification with independent character-rank references, multiple chunk iterations, boundary restoration, and tail handling. Selected bounded prefix and window domains cover the full usize request range.
• Audit all assumptions and add reachability covers after every explicit assume, together with completion covers for every harness.
• Keep production code unchanged.

Verification

Verified locally using the repository-pinned Kani and Rust toolchain:

• 42 Challenge 22 harnesses and 2 existing pattern harnesses passed.
• All 357 coverage goals were satisfied.
• All 55 remaining unwinding checks passed.

Limitations

• String lengths, iterator windows, and concrete pattern inputs remain bounded.
• Searcher abstractions rely on Challenge 22's permitted Pattern correctness assumption; general refinement of these abstractions is not mechanically proved.
• Reachability covers establish feasible paths, not the validity of the assumptions themselves.

Resolves #279

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

[feliperodri]

@v3risec, running the str::iter::verify harnesses locally with the pinned Kani (9461e07, 6 jobs on a 16-core, 30 GB machine): 40 pass and 4 don't finish:

Harness	Result
harness_chars_advance_by_all_counts	CBMC out of memory
harness_chars_advance_by_extended_counts	CBMC out of memory
harness_chars_advance_by_window_rank	CBMC out of memory
harness_chars_advance_by_chunked	timed out after 15 minutes

CI hits the same wall: "Verify std library (partition 2)" was killed with "The runner has received a shutdown signal" while running the str::iter harnesses, which is what happens when a job exhausts the 16 GB runner. Since the proofs have to run in CI, these four need to get smaller, for example by splitting the count ranges across several harnesses or lowering the bounds they use.

[feliperodri]

This is careful work: all 15 target functions and the __iterator_get_unchecked contract have harnesses, every assumption is followed by a reachability cover, the searcher stubs are checked against the real searchers in refinement harnesses, and nothing outside the verify modules changes. The static checks we run on every challenge PR (cfg body swaps, trivial invariants, contracts without a contract harness) are clean.

It doesn't meet the challenge yet, because Challenge 22 requires that "the verification must be unbounded---it must hold for str of arbitrary length", and the description says string lengths and windows remain bounded. The harnesses use backing buffers of at most 256 bytes and no loop invariants. #557 and #706 both claim unbounded string length for most targets, so this PR is currently behind them on the criterion that decides the challenge.

What would flip it: unbounded string length for all targets, including Chars::advance_by's chunk loop (loop invariants or a symbolic-length input that no loop is unwound over), and harnesses that complete within CI's resources.

Locally with the pinned Kani (9461e07): 40 of 44 harnesses pass; the 4 heaviest advance_by harnesses run out of memory or time out, and CI's partition 2 dies the same way (details in my comment above). Mutation testing: an off-by-one in SplitInternal::get_end fails 7 harnesses, one in next fails 6, and skipping one extra byte in Chars::advance_by fails 6, so the proofs do constrain the code within their bounds.

[feliperodri]

Bug: Challenge 22 requires the verification to hold "for str of arbitrary length". With a fixed 256-byte backing buffer, every harness here covers strings up to 256 bytes only, and the comment above this line says arbitrary length "requires an additional argument beyond this finite allocation model". Could the harnesses use a symbolic-length allocation that no loop is unwound over (as #557 and #706 do), with loop invariants where a loop does depend on the length?

[feliperodri]

Question: advance_by is the hardest target to make unbounded, because of the chunk-skip loop. #706 reports that a loop invariant there hits kani#4893 and kani#4943 (the latter is fixed in kani#4948). Have you tried #[kani::loop_invariant] on that loop with the current pin (9461e07)?

[feliperodri]

Praise: checking the real CharSearcher against the stub's contract is what makes the stubbed iterator proofs trustworthy; without it, the stubs could be weaker than the real searcher and nothing would notice.

[feliperodri]

Praise: turning the old kani::assume(ptr_x.is_aligned()) into an assertion strengthens the existing harness rather than weakening it.

[feliperodri]

FYI: the __iterator_get_unchecked contract (idx < self.0.len()) is already on main; this harness is what verifies it, which is what the challenge asks for.

[feliperodri]

Challenge 22 requires: "The verification must be unbounded---it must hold for str of arbitrary length." That requirement is final. A Kani solution will only be accepted if it is unbounded in the input size for every required function. This PR still verifies at least part of the challenge with bounded harnesses (kani::unwind bounds and/or fixed-size inputs), so I'm requesting changes until every required function is verified without a bound on the input size.