[hung1962003]

This is a solution to Challenge 20. It proves the six searching methods (next, next_match, next_back, next_match_back, next_reject, next_reject_back) of CharSearcher, MultiCharEqSearcher, CharArraySearcher, CharArrayRefSearcher, CharSliceSearcher and CharPredicateSearcher. The proofs are unbounded: the haystack has symbolic length (up to 2^48 bytes) and arbitrary contents, character sets have symbolic size, and no loop over the haystack is unwound. No method body is changed: everything added is cfg(kani) attributes, contracts, hooks and harnesses.

Depends on model-checking/kani#4947 and model-checking/kani#5071. Kani's explicit loop_modifies cannot yet name the MIR temporaries in these loops (e.g. the destination of self.next()). CI will fail until the Kani pin includes both PRs; I will bump tool_config/kani-version.toml here once they merge. Everything else runs with the pinned CBMC 6.11.0.

One change outside str::pattern: ffi::c_str::verify::check_from_ptr_contract reaches CharSearcher::next_match only through panic formatting, where it never runs. Its new loop contract made Kani apply loop contracts to that harness, and CBMC 6.11 then rejects the contract-less loop of its built-in strlen (Check that len is assignable, fixed by diffblue/cbmc#9164). The harness now stubs next_match, so the loop contract is not compiled into it; next_match still has no body in its instrumented program, so it proves the same. The stub can go once Kani ships a CBMC with rust-lang#9164.

Approach

Type invariants C.

• CharSearcher: finger <= finger_back <= haystack.len(), both on char boundaries, and utf8_encoded[..utf8_size] is the UTF-8 encoding of needle.
• MultiCharEqSearcher<C>: the CharIndices cursor covers haystack[front_offset..back] with both ends on char boundaries (kani_ok).

Loops. The provided methods next_match, next_reject, next_match_back and next_reject_back (trait defaults), plus CharSearcher::next_match{,_back}, get #[safety::loop_invariant] and a precise #[kani::loop_modifies]. The write set names only the cursor, through a SearcherLoopContract hook trait with specialization. Havocking the whole searcher would also havoc its haystack pointer, and CBMC then loses that pointer's value set (the issue in model-checking/kani#4993).

Contracts. The steps next / next_back of CharSearcher and MultiCharEqSearcher get requires(C) / ensures(C && the step is in bounds and on char boundaries) and a modifies that names only the cursor (for CharSearcher, C here is its fingers part: the safety of a step depends on nothing else). They are proved with proof_for_contract and used through stub_verified inside the provided-method loops. So the loops never read through the havocked slice::Iter cursor (a user-side answer to model-checking/kani#4993), and a loop proof does not verify its step again. The modifies of MultiCharEqSearcher names its cursor as the three words it consists of: a replaced step havocs a target element by element, and three writes instead of 24 byte writes keep each loop proof near 2 GB of memory instead of 7 GB.

Predicates. A predicate returns any result on every call. Two predicates are covered: one with no state of its own (fn(char) -> bool) and one that writes its own state on every call (Toggle, like a move closure updating a capture). That state is in the contracts' modifies and the loops' loop_modifies.

Assumptions (as allowed by the challenge)

1. Slice module:

   • memchr / memrchr return any matching index or None.
   • Byte-slice equality compares the at most 4 bytes of a char's encoding one by one (the bound is asserted).
   • <[char]>::contains returns any result, so a character set is never read and may have any size.
   • <slice::Iter<T>>::len runs the upstream body on the raw pointer offset_from_unsigned, which keeps its UB checks. It skips the contract of the NonNull wrapper, which costs a copy of the write set per call in the step contracts.

   check_memchr_models_cover_upstream, check_slice_eq_model_matches_upstream and check_iter_len_model_matches_upstream check the models against upstream.

2. validations.rs: next_code_point{,_reverse} assume the local UTF-8 rule at the position where decoding starts, then run the upstream arithmetic on the bytes the iterator has left. They move the iterator once where upstream moves it per byte, because every move is checked against the step contract's write set. Where upstream reads a byte with unwrap_unchecked, the models assert that it is there. check_decoder_models_match_upstream shows that the models only add assumptions.

3. The haystack is valid UTF-8. UTF-8 validity is never stated as a quantified property. It is assumed locally, only where a position is consumed, and every valid haystack satisfies it.

Criteria

1. check_*_into_searcher: a searcher built by into_searcher from any haystack satisfies C.
2. and 3. Each searching method runs from any state satisfying C. The step contracts' ensures (for next / next_back) and the harnesses (for the other four methods) check that every returned index lies on a char boundary in the haystack, and that the searcher still satisfies C.

Results

46 harnesses, all VERIFICATION:- SUCCESSFUL with Kani at the pin plus the two PRs above, and the pinned CBMC 6.11.0. Each harness takes between 0.5 s and 5 min (46 min for all 46, run one after another) and at most 4.3 GB of memory (the two CharSearcher::next_match{,_back} proofs; every other one stays under 2.3 GB, the step contracts under 1.4 GB), and every kani::cover is satisfied (no vacuous proofs).

Mutation testing

Each mutant changes one line so that a method returns, or moves its cursor to, an index that is out of bounds or not on a char boundary. With all ten built together, every harness of a mutated method fails; the unmutated code verifies.

Mutant	Harnesses that fail (failed check)
CharSearcher::next: finger += 1	check_char_searcher_next (ensures)
CharSearcher::next_back: finger_back -= 1	check_char_searcher_next_back (ensures)
CharSearcher::next_match returns (found_char + 1, finger)	check_char_searcher_next_match (char boundary)
CharSearcher::next_match_back: finger_back = found_char + 1	check_char_searcher_next_match_back (bounds, char boundary)
MultiCharEqSearcher::next returns Reject(i, i + 1)	char_array::check_next, char_predicate_state::check_next (ensures)
MultiCharEqSearcher::next_back returns Reject(i, i + 1)	char_array::check_next_back (ensures)
provided next_match returns (a, b + 1)	char_array::check_next_match (bounds, char boundary)
provided next_reject returns (a, b + 1)	check_char_searcher_next_reject, char_array::check_next_reject (bounds, char boundary)
provided next_match_back returns (a, b + 1)	char_array::check_next_match_back (bounds, char boundary)
provided next_reject_back returns (a, b + 1)	check_char_searcher_next_reject_back, char_array::check_next_reject_back (bounds, char boundary)

Resolves #277

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

🤖 Generated with Claude Code

[hung1962003]

@feliperodri #740 is ready for review. It proves every method of the six char searchers for a symbolic haystack of any length up to 2^48 bytes. The shipped bodies only gain loop contract attributes; no statement changes, and all other verification code is additive. Locally all 46 harnesses verify and every cover is satisfied.

The 4 red CI jobs fail only on the expected "Check that … is assignable" in the 24 loop-contract harnesses. They pass with model-checking/kani#4947 (approved) plus the small follow-up model-checking/kani#5071. Neither has run CI yet: their workflow runs have been waiting for approval since 2026-10-24 and 2026-10-27. Once they are merged, I will bump the Kani pin in this PR.

[Copilot]

🟡 Changes recommended

The pinned Kani toolchain cannot run the affected proofs, and verification also leaves gaps for mutable predicates, array sizes, and larger slices.

4 open issues

• Pinned Kani toolchain cannot run the new loop write-set proofs · New
• Empty predicate write set misses captured and referenced mutations · New
• 2^48 byte cap excludes valid larger haystacks · New
• Array searcher proofs cover only N = 2 · New

What changed in this PR

This PR proposes a Kani solution to Challenge 20 (#277), adding symbolic-length safety proofs for character-based str::pattern searchers without changing their runtime method bodies.

Changes:

• Adds searcher invariants, step and loop contracts, and 46 verification harnesses with supporting models.
• Adds Kani-only iterator accessors for inspecting cursor state.
• Adds a targeted stub to the existing CStr::from_ptr harness to avoid a CBMC loop-contract limitation.

File	Description
library/​core/​src/​str/​pattern.rs	Adds contracts, models, and harnesses for character-searcher safety.
library/​core/​src/​slice/​iter.rs	Exposes iterator pointer fields through Kani-only helpers.
library/​core/​src/​ffi/​c_str.rs	Isolates an existing harness from the new searcher loop contracts.

_{Review effort: Balanced}

[feliperodri]

Requesting changes for one reason: this can't merge until the Kani it depends on exists. At the current pin (9461e07) CI fails 24 of 1,792 harnesses, all of them the loop-contract proofs of next_match, next_reject and their _back versions, on assigns checks such as "Check that var_12 is assignable". That matches the description: the proofs need model-checking/kani#4947 and model-checking/kani#5071, both still open. Once both merge and the pin includes them, I expect to approve.

Everything else holds up, and this is the first Challenge 20 submission that meets the unbounded requirement:

• The haystack has symbolic length up to MAX_ALLOCATION_BYTES with arbitrary contents, no searcher harness has an unwind bound, and every loop the methods run carries a loop contract. Character sets are never read, so their size is unbounded too.
• The diff is additive (+939/-0). No method body changes; the cfg(kani) items are all top-level, the cfg-swap, invariant-strength and contract-coverage checks are clean, and every contract has a contract harness.
• The models (memchr, byte equality, Iter::len, the UTF-8 decoders) trace to the challenge's assumptions 1 and 2, and three of them are checked against upstream by dedicated harnesses. utf8_ok_at is a genuine local validity rule, so the assumptions built on it hold for every valid haystack (assumption 3).
• The four wrapper searchers are exercised through their own methods, and the stateful predicate (Toggle) covers patterns that write their own state.

Compared with the other Challenge 20 PRs: #722 and #537 are sound but bounded (#537 to 5-byte haystacks), and #620 verifies cfg(kani) replacements of the trait defaults. This one is the solution to prioritize.

Locally with the pinned Kani: the same 23 harnesses pass and the same 24 fail as in CI. Mutation testing on the passing part: shifting the forward finger by one byte (self.finger += old_len - iter.iter.len() + 1) fails check_char_searcher_next, and the same change to the backward finger fails check_char_searcher_next_back.

What would flip this to approval: kani#4947 and rust-lang#5071 merged, tool_config/kani-version.toml bumped to a Kani that includes them, and CI green. I'll re-run the 24 loop-contract harnesses then.

[feliperodri]

FYI: I checked this isn't assuming the conclusion. a holds the needle's lead byte, which in valid UTF-8 only starts a character, so the boundary at a follows from the byte and the assumption only supplies the boundary at b. Holds for every valid haystack. A sentence saying that in the comment would help the next reader.

[hung1962003]

Done in 85f21af: the comment now says that a holds the needle's lead byte, a boundary by itself, so the local rule only adds the boundary at b. next_match_back points to it.

[feliperodri]

FYI: because the loop contracts sit on the trait default methods, every other searcher gets invariant true and a whole-searcher havoc. That's sound but over-approximate, so future proofs of, e.g., StrSearcher (Challenge 21) through these defaults will need their own specialization. Worth a line in the doc comment.

[hung1962003]

Done in 85f21af: the doc of SearcherLoopContract now says that a searcher without a specialization gets invariant true and a havoc of the whole searcher, and that a proof of another searcher through these methods (e.g. StrSearcher, Challenge 21) needs its own specialization.

[feliperodri]

Question: this works around CBMC 6.11 rejecting the built-in strlen loop once loop contracts are enabled (diffblue/cbmc#9164). Could you open a tracking issue so the stub, and the slice::iter raw-parts helpers, are removed once Kani ships a CBMC with that fix?

[hung1962003]

Opened #748. It tracks the strlen stub (diffblue/cbmc#9164) and also Iter::kani_loop_raw_parts, which depends on model-checking/kani#4796 rather than on the CBMC fix. kani_raw_parts stays, since the invariants need the private fields of Iter.

[feliperodri]

Nit: "as in the accepted VecDeque solution" — #681 isn't accepted (it has changes requested). Suggest "as in #681" or dropping the reference.

[hung1962003]

Fixed in 85f21af, here and in the doc of MAX_ALLOCATION_BYTES.

[feliperodri]

@hung1962003 I'll give another round of review once model-checking/kani#5071 is merged.