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.

[Copilot]

Copilot wasn't able to review any files in this pull request.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Verification-soundness review — Challenge 20 (PR #620)

Bottom line: this PR does not repeat #537's anti-pattern. It genuinely verifies the real searcher code and its assumes are challenge-licensed rather than circular. I'm recommending COMMENT (not APPROVE) only because of a few non-blocking items a maintainer should confirm.

1. cfg-swap vacuity (the #537 check) — PASS

All five #[cfg(not(kani))] sites classified:

Site	diff line	Classification
CharSearcher::next	L124 vs L143	Real body retained under both cfgs; kani branch only appends assume_valid_utf8_forward_boundary. Not a swap.
CharSearcher::next_back	L349 vs L368	Same — identical real body, boundary assume appended.
next_match inner compare	L208	slice == utf8_encoded[..n] → utf8_encoded_matches(slice) (L28–51), a faithful width-matched byte comparison to dodge CBMC memcmp.
next_match_back inner compare	L454	Same helper.
MultiCharEq for &[char]::matches	L558	self.contains(&c) → kani::any(); sound over-approx of the match/reject bit, which cannot affect the returned range.

Crucially, unlike #537, no method body is compiled out and replaced by a nondeterministic stub that kani::assumes the char-boundary conclusion. The real unsafe { get_unchecked(..) } slicing and finger arithmetic execute and are UB-checked in every CharSearcher method.

2. Assume-the-conclusion vs licensed precondition — PASS

The boundary assumes encode the challenge's explicit permission ("assume str/validations.rs is functionally correct / haystack is valid UTF-8"), applied after proving the algebraic facts CBMC can establish:

• assume_valid_utf8_forward_boundary (L1664) / _reverse_ (L1689): assume is_char_boundary(new_finger) only after asserting ordering/in-bounds; this is the decode-lands-on-boundary theorem, licensed.
• assume_valid_utf8_next_match_boundaries (L1735): asserts b-a==utf8_size, utf8_encoded_matches(candidate), utf8_encoding_matches_needle (i.e. the returned range really holds needle's encoding) before importing boundaries. Not circular.

3. Type invariant C — meaningful

type_invariant_char_searcher (L944) requires ordered fingers, both on char boundaries, 1<=utf8_size<=4, and utf8_encoding_matches_needle() (L54, ties cached bytes to needle). type_invariant_multi_char_eq_searcher (L1044) requires iterator Invariant::is_safe, ptr::eq of the remaining slice to the haystack window, and both window ends on boundaries. Non-trivial.

4. Contract-liveness (T7) — PASS

Exactly 2 #[kani::proof_for_contract]: CharSearcher::next (L2077) and CharSearcher::next_back (L2161), each with requires/modifies/ensures. Contracts are consumed via #[kani::stub_verified(CharSearcher::next)] / (next_back) in the next_reject / next_reject_back harnesses (L2136, L2232), so they are live.

5. Over-constrained/empty-haystack vacuity — PASS

any_valid_utf8_str (L903) uses any_slice_of_array over 4 bytes → lengths 0..4, plus symbolic finger/finger_back/needle. Not empty-only.

6. Unbounded — PASS (with a caveat, see below)

No #[kani::unwind] on any searcher harness. Loops are handled by #[kani::loop_invariant] (next_reject L258, next_match_back L422, etc.) and by the verify-one-representative-iteration + over-approximate-remainder stubs (stub_char_next_match_remaining L1007, stub_multi_char_eq_* L1177+). Iteration count is genuinely unbounded.

7. Success criteria — all three met against real methods

• (1) init establishes C: harness_*_into_searcher call the real into_searcher and assert C (L2066, L2288 macro).
• (2) C ⇒ safety (indices on boundaries): returned (a,b) checked via valid_range_on_haystack (L1108) inside valid_char_next_step / valid_char_next_filtered_result.
• (3) each method preserves C: preservation asserted from an arbitrary C-state via any_char_searcher_state (L1996) / set_any_multi_char_eq_active_window (L2022), which is a sound superset of reachable states.

Coverage spans all 6 methods across CharSearcher, MultiCharEqSearcher, and the four wrappers (via the generate_multi_char_eq_harnesses! macro, L2270+).

---

Non-blocking concerns (reasons this is COMMENT, not APPROVE)

1. Haystack literally bounded to 4 bytes (MAX_UTF8_BYTES, L901; used in every harness). The argument for effective unboundedness is: max UTF-8 char = 4 bytes, so a 4-byte window exercises every single-decode case, and loop abstraction makes iteration count unbounded. This is defensible, but please confirm 4 bytes suffices to exercise next_match's window scan for every needle width — the literal input size is bounded even if the reasoning is per-char-local.

2. next_reject/next_reject_back (CharSearcher, L247/L467) and all four MultiCharEqSearcher filtered methods (L630, L690, L757, L818) are #[cfg(kani)] reimplementations of the Searcher/ReverseSearcher trait defaults, not the literal shipped default methods. They appear faithful to the defaults (loop { match self.next() { Reject/Match => return, Done => None, _ => continue } }), but the proof covers the reimplementation, not the exact upstream default body. Worth an explicit note in the PR that these mirror the defaults verbatim.

3. The manual loop-acceleration stubs (stub_char_next_match_remaining etc.) rely on: loop-head over-approx (valid_*_loop_head, deliberately dropping the finger-on-boundary fact, L959), strict progress asserts (L223–225), and a stub exit relation (valid_*_stub_result). The inductive soundness looks correct, but this is the most intricate part of the proof and deserves a careful maintainer audit that each stub exit relation truly over-approximates every concrete suffix.

None of these break soundness; the proof is non-vacuous and verifies real code, which is the critical bar #537 failed.