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