[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: a combinator-fold .sum() with no attach site (kani#4893, open), and a while … && let let-chain that #[kani::loop_invariant] could not compile (kani#4943) — now fixed in Kani (kani#4948), but after the Kani commit this repo pins, so it still blocks here. 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.

[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.