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, plus the Bytes::__iterator_get_unchecked safety contract. 33 harnesses in a new #[cfg(kani)] mod verify, all gated so non-Kani builds are unchanged.

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

Success criteria

Criterion	Status
15 functions, safety (no UB)	Done. 33 harnesses over real bodies, including advanced-state (depth 1–2, single and mixed direction) 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 PR proves it.
Listed UBs absent	Done. Kani checks them on every harness.
Unbounded (arbitrary length)	Symbolic kani::any() length, capped only by CBMC's --object-bits 12 pointer-offset budget, not a fixed array. advance_by additionally caps its skip count (see Limitations).

What the harnesses check

• Real bodies. The shipped methods run unchanged, with no #[cfg(kani)] rewrites. 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, so the module lives in alloc::str.
• Assumption-cited stubs. 19 harnesses (10 SplitInternal, 9 Matches/MatchIndices) 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. No-UB under the stub therefore gives no-UB for the real searcher.
• Advanced state. Split/Matches methods are proven from depth-1 and depth-2 states, not just fresh, including mixed front/back consumption, each with a witness cover.
• Content. Chars::next and next_back are proven jointly over arbitrary length and arbitrary valid-UTF-8 content, both ends.
• Non-vacuity. Every assume-bearing harness carries a satisfied cover (74 total).

Limitations

• advance_by skip count is unwind-bounded while the str length stays symbolic. A loop invariant on the chunk-skip loop hits two Kani walls we filed (kani#4893, kani#4943): a combinator-fold .sum() with no attach site, and a while … && let let-chain that #[kani::loop_invariant] cannot compile. Same open committee question as the other unbounded-verification challenges.
• advance_by on macOS CI. check_advance_by_chars verifies on the Linux runner (all safety checks pass) but exceeds Kani's per-harness CBMC time budget on the slower macOS runner, where the autoharness job reports a timeout. The limit is runner wall-clock, not coverage or a missing property.
• 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.

[Copilot]

Copilot review overview

🟡 Changes recommended

Some harnesses invoke undefined behavior, and bounded inputs leave required unbounded and reachable-state cases unproven.

Review effort: Balanced
Findings: 1 · 3

Open (4)

• Constructs invalid UTF-8 from uninitialized memory · New
• Length bound excludes valid arbitrarily long strings · New
• Finite advance_by bound does not prove unbounded safety · New
• Shallow directional samples do not prove iterator state safety · New

What changed in this PR

Adds Kani verification for Challenge 22’s str iterator safety obligations.

Changes:

• Adds 30 iterator and contract harnesses.
• Models searcher behavior and symbolic strings.
• Enables required unstable APIs under Kani.

File	Description
library/​alloc/​src/​str.rs	Adds Challenge 22 verification harnesses and helpers.
library/​alloc/​src/​lib.rs	Enables remainder API features for Kani builds.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.