Challenge 20: Verify Char Searcher with Kani

[v3risec]

Summary

This PR solves Challenge 20 by adding Kani verification for the char-related searchers in core::str::pattern.

The verification covers CharSearcher, the generic MultiCharEqSearcher, and the public searchers for owned character arrays, borrowed character arrays, character slices, and FnMut(char) -> bool predicates.

For each searcher family, the proofs check that construction establishes a safety invariant, forward and reverse search operations preserve the safety-relevant state, and returned ranges are ordered, in bounds, and located on valid UTF-8 boundaries in the original haystack.

All verification-only implementations and abstractions are gated behind #[cfg(kani)]. Normal library behavior is unchanged.

Verification Coverage Report (36/36 Methods Verified, 42 Harnesses)

Searcher	Coverage
CharSearcher	Verifies into_searcher, next, next_match, next_reject, next_back, next_match_back, and next_reject_back. The proofs cover arbitrary invariant-admitted cursor states within the bounded symbolic haystack, cached UTF-8 encodings for all character widths, direction-specific progress, and returned-range safety.
MultiCharEqSearcher	Verifies construction and all six search methods. The invariant ties the internal CharIndices iterator to the exact active window of the original haystack and requires both ends of that window to be UTF-8 boundaries.
CharArraySearcher	Verifies the owned [char; N] wrapper, including construction, delegation to the inner searcher, invariant preservation, and forward and reverse result ranges.
CharArrayRefSearcher	Verifies the borrowed &[char; N] wrapper with the same constructor, state-preservation, and range-safety obligations.
CharSliceSearcher	Verifies borrowed &[char] patterns with symbolic slice length and all required search methods.
CharPredicateSearcher	Verifies the searcher safety properties with a concrete stateful FnMut(char) -> bool whose result is symbolic on each executed call. Predicate state semantics are intentionally outside the proof.

Each searcher has one constructor harness and six method harnesses, for a total of 42 Challenge 20 harnesses.

Verification Approach

The proofs define a safety invariant C for each searcher family.

For CharSearcher, C establishes that:

• finger..finger_back is an ordered, in-bounds range in the haystack;
• both cursors are UTF-8 character boundaries;
• utf8_size is in 1..=4;
• utf8_encoded[..utf8_size] is exactly the UTF-8 encoding of needle.

The constructor harness proves that the production char::into_searcher implementation establishes this invariant. Method harnesses start from arbitrary states satisfying C within the bounded symbolic input and prove the required state transition and invariant preservation.

For MultiCharEqSearcher, C establishes that the internal byte iterator is safe and points to exactly the remaining CharIndices window in the original haystack. The wrapper invariants for arrays, slices, and predicates reduce to this inner invariant because matcher output only selects Match versus Reject; it does not determine the already-consumed UTF-8 range.

The next and next_back harnesses execute the production implementations and prove their exact safety projection: one complete UTF-8 character is consumed, only the appropriate end of the active window moves, and the returned range matches that movement. Filtered method harnesses additionally prove that Some returns a non-empty safe range and that None exhausts the active window.

CharSearcher::next and next_back have verified Kani contracts. The Kani-only next_reject and next_reject_back overrides use those contracts while verifying their surrounding default-search loops.

Loop Verification

The search loops are handled with loop contracts or safety-only loop stubs instead of relying on a fixed unwind count.

For CharSearcher::next_match, the Kani path checks a real representative loop iteration from an arbitrary valid loop-head state, proves strict progress, and uses a conservative stub for the unexecuted suffix. next_match_back, next_reject, and next_reject_back use inductive loop contracts that preserve the cached character representation and direction-specific cursor constraints.

The four filtered MultiCharEqSearcher methods (next_match, next_reject, next_match_back, and next_reject_back) use loop stubbing:

1. Snapshot the initial concrete CharIndices window.
2. Execute one real next or next_back iteration, including the real matcher call for that iteration.
3. Prove the type invariant, the exact UTF-8 projection, and strict progress when the loop continues.
4. Over-approximate the unexecuted suffix or prefix with any Some/None exit satisfying the safety-relevant range and exhaustion conditions.
5. Rebuild a concrete valid CharIndices state for the summarized exit.

The loop summary deliberately forgets matcher-internal state and does not claim first-match, first-reject, or rightmost-result semantics. It proves only the state and range properties required for searcher safety.

Verification Abstractions and Tradeoffs

The memchr and memrchr calls used by CharSearcher are replaced with a shared conservative stub. It may return None or any in-bounds occurrence of the requested byte and does not assume first- or last-occurrence semantics. A successful character match is accepted only after checking the complete candidate against the cached UTF-8 encoding of needle.

The Kani path for symbolic-length &[char] membership returns a nondeterministic boolean. The predicate harness likewise returns a fresh nondeterministic boolean on every executed predicate call. These are safety over-approximations because classification occurs after CharIndices has already computed and consumed the UTF-8 range.

For summarized predicate iterations, the loop stub does not execute the omitted FnMut calls or model their captured-state transitions. The PR therefore does not prove predicate call counts, captured state, side effects, panic behavior, or exact matching semantics. It proves only the normally returning classification outcomes relevant to cursor and returned-range safety.

The proofs use Challenge 20's permitted assumptions about slice operations, valid UTF-8 haystacks, and the functional correctness of str::validations. UTF-8 facts are imported only after the associated ordering and state-transition facts have been asserted.

Scope Assumptions

• This PR proves the safety properties targeted by Challenge 20 for the covered searcher operations.
• It proves the memory-safety part of the unsafe Searcher and ReverseSearcher contracts: returned indices are valid UTF-8 boundaries in the original haystack and preserve a valid search state.
• It does not prove full functional matching semantics or matcher-internal behavior.
• Symbolic haystacks are arbitrary valid subslices of a 4-byte symbolic array. This covers empty inputs, multiple ASCII characters, and all UTF-8 character widths, but it is a bounded input model rather than a proof over arbitrary haystack lengths.
• Loop contracts and loop stubs make reasoning about the modeled scan independent of a fixed unwind count within that bounded input model.
• All Kani-specific behavior is isolated behind #[cfg(kani)].

Notes

• The explicit Kani-only CharSearcher::next_reject and next_reject_back overrides allow loop contracts to refer directly to concrete searcher state; non-Kani builds continue to use the trait defaults.
• The Kani-only UTF-8 comparison avoids lowering symbolic-length slice equality to CBMC's memcmp model while checking the same 1-to-4-byte cached representation.
• Wrapper harnesses exercise the public searcher types directly instead of relying only on verification of MultiCharEqSearcher.
• The predicate harness exercises one mutable captured-state update per real iteration, but matcher-state correctness remains outside the proof boundary.

Verification

All 42 added Challenge 20 harnesses pass locally with Kani. The seven CharPredicateSearcher harnesses also pass after routing the filtered methods through the safety loop stubs.

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.