Verify safety of str iter functions (Challenge 22)

[jrey8343]

Verify safety of str iter functions (Challenge 22)

Towards #279 (Challenge 22).

Stacked on #537 only: the branch is #537's head plus one commit appending the verification module to str/iter.rs. The UTF-8 input model (PAD/utf8_local/any_utf8) is a self-contained copy inside that module, so this PR does not depend on #538. iter.rs's production code is byte-identical to main (the diff is one appended verify module); in pattern.rs the only production changes are #537's runtime-no-op contract attributes on CharSearcher::next_match/next_match_back and the safety::{ensures, requires} import — no body changes.

Summary

Rework per the 2026-09-12 review. The proofs are unbounded in string length (no loop is unwound to the haystack size) for 17 of the 18 harnesses, and unbounded in iterator state throughout; Chars::advance_by's chunk-skip loop body is exercised and checked against a reference; get_end has a direct harness. All 15 target functions and the __iterator_get_unchecked contract are covered; every harness runs the real, unmodified iterator code.

Input model: strings of arbitrary length

Every harness except the chunk-skip one takes a symbolic-length slice of a kani::any() byte array constrained to valid UTF-8 by a loop-free byte-table predicate (utf8_local/any_utf8, two constant-bound kani::forall! facts local to a 4-byte window, defined in the module; the same input model #538 uses). Contents, length and every character width are symbolic; the only size parameter is the backing allocation — a CBMC memory-model parameter, like ARR_SIZE in check_run_utf8_validation and HAY_MAX in #538: HAY_MAX = 256 (two harnesses were also run at 1000: 113 s each, ~11× the 256-byte solve time), 128 for check_chars_advance_by (its per-character loop is unwound, so memory grows with the array), and a fixed 48-byte string for the chunk-skip harness (see below). Fourteen of the fifteen target functions reach no loop other than the two inside CharSearcher::next_match/next_match_back; once those are replaced by their separately proved contracts, the remaining call graphs are loop-free and their 16 harnesses carry no #[kani::unwind] at all. The two advance_by harnesses are the only ones in str::iter::verify with an unwind bound (the two searcher contract proofs in pattern.rs keep #537's unwind(7) over a 5-byte haystack).

Why the backing array rather than an object-model-sized allocation (the "symbolic capacity bounded only by CBMC's object model" shape accepted on #681): the content predicate is a quantified byte-table fact whose range must be a constant that CBMC expands into one conjunct per index (and the pinned Kani now fails verification outright when the backend drops a quantifier, kani#4719), so a symbolic length is meaningful only up to the constant array size; core has no allocator; and the harnesses must live in core::str::iter::verify to reach the private SplitInternal/MatchIndicesInternal fields. An alloc-side symbolic-length tail would give length without content (every byte past the window would be a fixed value), which is the trade-off this PR does not make.

Iterator state: Challenge 20 methodology

Each iterator type has a type invariant C; a base case shows the constructors establish it — a dedicated harness for SplitInternal (split/split_terminator/split_inclusive), pattern::verify::verify_cs_into_searcher (#537) for the searcher invariant of MatchesInternal/MatchIndicesInternal, the k = 0, m = len instance of the arbitrary window for Chars, and an inline check of the fresh iterator for SplitAsciiWhitespace. Every method harness starts from an arbitrary C-satisfying state (a superset of the states any call sequence reaches), runs the method, asserts the facts the unsafe blocks rely on — str::get_unchecked only checks bounds, so char-boundary-ness of every produced index/slice is asserted explicitly — and re-asserts C.

• Chars: C = "the iterator's bytes are a char-boundary window of the string"; harnesses start from s[k..m].chars() for symbolic boundaries k <= m.
• SplitInternal<char>: C = searcher invariant ∧ start..end is a char-boundary range ∧ start <= finger ∧ finger_back <= end (allow_trailing_empty/finished symbolic).
• MatchIndicesInternal/MatchesInternal: C = the searcher invariant.
• SplitAsciiWhitespace: C = "the inner slice::Split's v is a char-boundary window" (every reachable v is cut at ASCII whitespace, i.e. at one-byte characters).

The searchers: a proven contract, not an assumption

The SplitInternal/Matches* bodies contain no loops; every loop they can reach is inside CharSearcher::next_match/next_match_back (pattern.rs). Challenge 22 assumption 2 allows assuming all of pattern.rs; these harnesses assume strictly less. The two methods now carry their Searcher contract as #[requires]/#[ensures]/kani::modifies attributes (runtime no-ops; this is #537's delta):

• requires: the finger/boundary clauses of the invariant documented on the struct (finger <= finger_back <= len, both char boundaries);
• ensures: a returned range is a needle-width range on char boundaries, at or after the finger on entry (next_match) / at or before the finger_back on entry (next_match_back), with that finger left at its end/start; None leaves the two fingers equal;
• modifies(&self.finger) / modifies(&self.finger_back).

pattern::verify::verify_cs_next_match/verify_cs_next_match_back are the #[kani::proof_for_contract] harnesses checking that contract against the real bodies: next_match runs core's real cfg(kani) memchr (the byte-by-byte memchr_naive since #628) and next_match_back the semantically identical linear-scan stub of memrchr as in #537 (Challenge 20 assumption 1; the harness's unwind bound fully unwinds the scan); the report shows the postcondition, self->finger is assignable write-set and single-call checks. The iterator harnesses use #[kani::stub_verified], which asserts the precondition at every call site (C ⟹ the searcher's precondition; visible in the report as the check "self.finger <= self.finger_back && ...") and assumes only the postcondition, which is discharged against the real bodies by those contract proofs. The boundary facts the iterator harnesses themselves assume are exactly the type invariant C of the arbitrary starting state; every index and slice a method produces is asserted, never assumed. No #[cfg(kani)] body swaps.

Why not loop contracts on the searcher loops: the slice comparison slice == &self.utf8_encoded[0..self.utf8_size()] lowers to CBMC's builtin memcmp, whose locals fail the loop-contract assigns check (kani#4790; every boundary assertion, the invariant and C verify, only those four checks fail). The root cause is fixed in CBMC by diffblue/cbmc#9164 (merged 2026-09-16), which is in no CBMC release yet; the pinned Kani uses CBMC 6.11.0. The contract proofs therefore keep Challenge 20's bounded haystack; that bound lives inside Challenge 20's scope (#537).

Chars::advance_by

The only target with loops (chunk-skip, trailing-continuation, per-character). Two harnesses run the real body; in each the only bound on the count is what sizes the unwinding, and no unwind bound is derived from a string length:

• check_chars_advance_by — the per-character path: an arbitrary window of a string of arbitrary length (128-byte backing array; measured peak RSS 4.8 GB at 256 bytes, 1.8 GB at 128), n <= 8, unwind(9).
• check_chars_advance_by_chunked — the chunk-skip path: 33 <= n <= 40, which makes the chunk-skip loop body run exactly once (it runs while more than 32 characters remain and a 32-byte chunk is available; a chunk of valid UTF-8 holds at least 8 characters, so afterwards at most 32 remain), then the trailing-continuation loop (≤ 3) and the per-character loop (≤ 16); unwind(34). This harness fixes the string length (48 bytes: one full chunk plus a 16-byte tail; contents fully symbolic), because CBMC drops the unrolled copies of the chunk-skip body only when the chunk iterator's end is known at unwinding time — with a symbolic length, or even a symbolic start of a fixed-length window, the 33 copies the bound implies each read a whole chunk at a symbolic offset and run two 32-iteration loops, and the harness exceeded 11 GB RSS in our runs (the CI macOS runners have 7 GB). CBMC's unwinding assertions check the iteration counts above rather than assume them.

Both check the result against a loop-free reference (up to 40 unrolled utf8_char_width steps): the remainder starts exactly where the reference ends (hence on a char boundary), Ok iff n characters were available, Err(rem) with rem == n − chars otherwise. Covers witness the chunk of eight 4-byte characters (the fewest a chunk can hold), a chunk starting and ending in ASCII, the trailing-continuation loop skipping a byte, and the Ok/Err arms.

Loop contracts are not applied to these loops because the invariant of a loop that advances a slice::Iter through a method call cannot be stated at the pinned Kani: loop-modifies inference misses fields written by callees (Kani reference › loop contracts › limitations), and after the iterator is havocked its len()/as_slice() trip the same-allocation check in Kani's ptr_offset_from model before any invariant could re-pin it.

Coverage vs the challenge function list

Challenge function	Harness	Bound
Chars::next / next_back / as_str	check_chars_next / check_chars_next_back / check_chars_as_str	none
Chars::advance_by	check_chars_advance_by (per-character path) / check_chars_advance_by_chunked (chunk-skip path)	n <= 8, string unbounded / 33 <= n <= 40, 48-byte string
SplitInternal::get_end	check_split_get_end (direct; four covers: the two Some outcomes and the two None outcomes)	none
SplitInternal::next / next_inclusive	check_split_next / check_split_next_inclusive	none
SplitInternal::next_match_back (no such method; the next_match_back call its next_back makes)	pattern::verify::verify_cs_next_match_back (contract proof, real body) + check_split_next_back (its call site, incl. the allow_trailing_empty == false recursive path)	contract proof: Challenge 20's haystack bound
SplitInternal::next_back_inclusive	check_split_next_back_inclusive	none
SplitInternal::remainder	check_split_remainder (direct)	none
MatchIndicesInternal::next / next_back	check_match_indices_next / _next_back	none
MatchesInternal::next / next_back	check_matches_next / _next_back	none
SplitAsciiWhitespace::remainder	check_split_ascii_whitespace_remainder (fresh + arbitrary state)	none
Bytes::__iterator_get_unchecked (safety contract)	check_bytes_iterator_get_unchecked (proof_for_contract, arbitrary window)	none
base case	check_split_constructors_establish_invariant	none

Verification results

Local, pinned Kani 1640445 (0.68.0 + 72 commits), CBMC 6.11.0, toolchain nightly-2026-09-25, CI's exact flags (-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts --cbmc-args --object-bits 12):

• core::str::iter::verify: 18 of 18 harnesses verified, 0 failures, every cover property satisfied. In a 4-way parallel run (409 s of CBMC time in total): the 16 loop-free harnesses 1–24 s each, check_chars_advance_by_chunked 87 s, check_chars_advance_by 74 s. The same set passes in autoharness mode (--jobs=3 --harness-timeout 10m --default-unwind 1000), the configuration of the required autoharness CI job; in that mode check_chars_advance_by_chunked takes 94 s and check_chars_advance_by 75 s, everything else at most 30 s.
• core::str::pattern::verify at this head (the Challenge 20 harnesses, including the two contract proofs): 17 of 17 verified.

Also in this PR

• pattern.rs (via Verify safety of char-related Searcher methods (Challenge 20) #537): the contracts above; type_invariant_cs/any_char_searcher/assert_valid_range made pub with cs_finger/cs_finger_back/cs_needle accessors; the needle clause of C stated byte-wise (loop-free) so harnesses that state C need no unwind bound; safety::{ensures, requires} imported unconditionally (they were x86_64-only); the memchr stub dropped in favour of core's real cfg(kani) path.

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

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

[feliperodri]

Thanks @jrey8343. Reviewed against Challenge 22 with our vacuity tooling + local Kani (0.67.0 / CBMC 6.8.0). Between the two open Challenge 22 solutions we're prioritizing this one. It's sound and a real improvement over the earlier approach: T1 clean (production iter.rs is byte-identical to upstream — the historical cfg(kani) body-swap concern is absent), fully symbolic UTF-8 inputs and symbolic patterns, and the __iterator_get_unchecked contract is now genuinely enforced via #[kani::proof_for_contract] (no longer decorative). All 15 target fns + the contract have harnesses.

Requesting changes because it doesn't meet the success criteria yet:

1. Fails the unbounded requirement. Every harness caps at ≤5-byte strings (HAYSTACK_BYTES=5, #[kani::unwind(8)]), which the PR openly concedes. Challenge 22 mandates arbitrary length — this needs loop contracts, not unwind caps.
2. Chars::advance_by is only partially exercised — its 32-byte chunk-skip loop body is never entered at ≤5 bytes, so its main path is unverified.
3. get_end is reached only indirectly (not asserted).

Sound and the most complete of the two; the blocker is unboundedness. Nice work getting the contract genuinely proved.

[jrey8343]

Thanks for the review. All three points are addressed in the rework; the PR description is rewritten to match the diff.

1. Unbounded. Every harness except the chunk‑skip one takes a symbolic‑length string over a kani::any() backing array constrained to valid UTF‑8 by the loop‑free byte‑table predicate Verify safety of StrSearcher (Challenge 21) #538 introduced (pattern::verify::any_utf8): contents, length and character widths are all symbolic, and the only size parameter is the backing allocation (HAY_MAX = 256, a CBMC memory‑model parameter like ARR_SIZE in check_run_utf8_validation; 128 for check_chars_advance_by, whose per‑character loop makes memory grow with the array; a fixed 48‑byte string for the chunk‑skip harness — see point 2; two harnesses were also run at 1000, at ~11× the solve time). Fourteen of the fifteen target functions reach no loop other than the two inside CharSearcher::next_match/next_match_back; once those are replaced by their separately proved contracts, the remaining call graphs are loop‑free and their 16 harnesses carry no unwind bound at all. They are also unbounded in iterator state: each harness starts from an arbitrary state satisfying the type's invariant C (Challenge 20 methodology), with base cases for the constructors.

   The searcher loops: rather than loop contracts (which the pinned Kani cannot apply there — the slice comparison lowers to CBMC's memcmp model whose locals fail the assigns check, and both stub routes around it are rejected by the compiler; exact errors in the PR description and the module comment), the two methods now carry their Searcher contract as #[requires]/#[ensures]/modifies on the real, byte‑identical bodies, checked by #[kani::proof_for_contract] harnesses in pattern::verify (Verify safety of char-related Searcher methods (Challenge 20) #537; memchr/memrchr stubbed by linear scans as before), and the iterator harnesses compose with them through #[kani::stub_verified]. Each call site asserts the contract's precondition (C ⟹ the searcher's finger invariant — visible in the report as the check "self.finger <= self.finger_back && …") and assumes only its postcondition, which is discharged against the real bodies by those contract proofs (over Challenge 20's 5‑byte haystack). The boundary facts the iterator harnesses themselves assume are the type invariant C of the arbitrary starting state; every index and slice a method produces is asserted, never assumed. That is strictly less than Challenge 22's assumption 2 (all of pattern.rs may be assumed), and the contract proofs' haystack bound is Challenge 20's, not this PR's.

2. Chars::advance_by. Two harnesses run the real body: the per‑character path on an arbitrary window of a string of arbitrary length (n <= 8), and the chunk‑skip path (33 <= n <= 40, so the chunk‑skip body runs exactly once, then the trailing‑continuation and per‑character loops) on a 48‑byte string of fully symbolic contents. The chunk harness fixes the length because CBMC drops the unrolled copies of the chunk‑skip body only when the chunk iterator's end is known at unwinding time — with a symbolic length (or even a symbolic start of a fixed‑length window) the 33 copies each read a whole chunk at a symbolic offset and run two 32‑iteration loops, and the harness exceeded 11 GB RSS in our runs. In both, the unwind bound is derived from the count and the constant chunk size, never from a string length, and CBMC's unwinding assertions check the iteration counts. The result is checked against a loop‑free reference (Ok iff n characters were available, Err(rem) with rem == n − chars, remainder exactly where the reference ends, on a boundary); covers witness the chunk of eight 4‑byte characters, an ASCII chunk, the trailing‑continuation loop skipping a byte, and both result arms. Loop contracts on these loops are blocked by the pinned Kani (loop‑modifies inference misses slice::Iter fields written by callees, and a havocked iterator's len() trips the same‑allocation check in the ptr_offset_from model before an invariant could re‑pin it); the harness comment cites both.

3. get_end. check_split_get_end calls it directly on an arbitrary C‑state and asserts the outcomes (finished on entry ⇒ None and no state change; otherwise finished flips and the result is start..end iff allow_trailing_empty || end > start), with covers on both Some and both None outcomes. remainder has a direct harness too, and the next_match_back | SplitInternal row is mapped to the contract proof plus its call site in check_split_next_back, which also covers the allow_trailing_empty == false recursive path.

Results (pinned Kani d4df833, CBMC 6.8.0, CI flags): 18/18 str::iter::verify harnesses verified, every cover satisfied (4‑way parallel run: loop‑free harnesses 5–22 s each, check_chars_advance_by_chunked 92 s, check_chars_advance_by 195 s — 81 s / 86 s alone); 36/36 str::pattern::verify harnesses verified at this head.

[jrey8343]

For the record on the remaining bounded corner: the two searcher contract proofs (CharSearcher::next_match/next_match_back) inherit the 5-byte haystack from #537, where the only obstacle to loop contracts on the two memchr loops is now filed upstream with a minimized reproducer: model-checking/kani#4790 (reproduces on 0.67.0 and on Kani main; details in the linked comment on #537). Challenge 22's assumption 2 permits assuming all of pattern.rs; these harnesses assume strictly less than that, since the searcher contracts are proved (bounded) rather than assumed.

[jrey8343]

@feliperodri — this PR is re-cut on top of current main (toolchain nightly-2026-09-25, Kani pin 1640445 = 0.68.0 + 72 commits, CBMC 6.11.0), and it no longer stacks on #538: it is #537's head plus one commit appending the verify module to str/iter.rs, with its own copy of the UTF-8 input model (PAD/utf8_local/any_utf8). Reasons: main's sync added a single-byte StrSearcher variant that #538 has to cover first, and nothing here ever depended on it — Challenge 22 assumption 2 lets pattern.rs be assumed safe and correct, and these harnesses still assume strictly less than that, through stub_verified of the two CharSearcher contracts proved in #537. The force-push rewrites the branch history accordingly (the repo squash-merges).

At the new pin: 18 of 18 harnesses verify, 0 failures, every cover satisfied under CI's exact flags (4-way parallel run, 409 s of CBMC time in total; the 16 loop-free harnesses 1–24 s each, check_chars_advance_by_chunked 87 s, check_chars_advance_by 74 s), and the same set passes in autoharness mode (--jobs=3 --harness-timeout 10m --default-unwind 1000). check_bytes_iterator_get_unchecked passes goto-instrument at CBMC 6.11.

Two notes on scope, also in the description: the symbolic-length model stays at a 256-byte backing array rather than an object-model-sized allocation, because the UTF-8 content predicate needs constant quantifier bounds (CBMC expands them per index, and the pinned Kani now fails hard on a dropped quantifier) and the harnesses must stay in core::str::iter::verify to reach the private SplitInternal/MatchIndicesInternal fields; and the two searcher contract proofs keep Challenge 20's bounded haystack (kani#4790; its root-cause fix cbmc#9164 is merged but unreleased — see #537).

Could you re-review when you get a chance? The 2026-09-12 items (unbounded length, the chunk-skip path of advance_by, a direct get_end harness) were addressed on 09-13 and are unchanged here.