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)

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	Directly verifies that the public owned [char; 4] construction path establishes the wrapper invariant. Its six search methods are covered compositionally by the direct MultiCharEqSearcher<[char; 4]> harnesses: CharArraySearcher is a single-field wrapper, each method delegates directly to self.0, and its safety invariant is exactly the inner invariant. The six redundant wrapper method harnesses are disabled because repeating the same proof adds substantial solver cost and makes Kani CI runtime unstable.
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 outside the proof.

Five searcher families have one constructor harness and six method harnesses. CharArraySearcher retains its constructor harness, while its six delegating methods reuse the exact MultiCharEqSearcher<[char; 4]> safety proof. This gives a total of 36 active Challenge 20 harnesses while avoiding duplicate solver work in CI.

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.

The #[cfg(kani)] overrides for CharSearcher::next_reject, CharSearcher::next_reject_back, and the four filtered MultiCharEqSearcher methods reproduce the trait defaults' Match/Reject/Done branching. They exist only so verification can refer to concrete searcher state and attach loop contracts or conservative continuation summaries. Non-Kani builds continue to use the upstream default implementations.

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-head relations are conservative as well. In particular, valid_char_next_match_loop_head intentionally does not require the current finger to be a UTF-8 boundary, because the byte-oriented scan may stop after a matching byte inside another multi-byte character before a later iteration finds a complete needle. The MultiCharEqSearcher loop-head relations retain only the valid active window and direction-specific bounds while omitting matcher state. Thus every concrete continuation head satisfies the corresponding relation, while additional abstract heads are admitted.

Each stub exit relation was audited against its corresponding concrete loop suffix. For a forward Some result, it preserves the untouched back cursor, places the returned non-empty UTF-8 range inside the remaining search window, and rebuilds the state immediately after that range. A forward None result rebuilds the exhausted state at the back cursor. The reverse relations enforce the symmetric conditions. The CharSearcher::next_match relation additionally retains the complete cached-needle comparison required by every concrete successful exit.

The summaries deliberately omit the identities and classifications of skipped characters, matcher-internal state, and first/last-match ordering. They therefore admit additional abstract exits while retaining every concrete suffix exit. Strict progress ensures that every summarized suffix or prefix starts from a strictly smaller remaining window.

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 is a bounded input model rather than a literal proof over arbitrary haystack lengths.
• Four bytes are sufficient for the safety-local obligations of one real scan iteration: every UTF-8 scalar and every complete next_match candidate occupies at most four bytes, so all needle widths can be exercised.
• Within this bounded input model, continuations after the representative iteration are handled by inductive loop contracts or conservative suffix/prefix summaries rather than a fixed unwind count. These abstractions do not enlarge the literal haystack beyond four bytes or concretely exercise histories containing multiple maximum-width characters. Generalization to longer inputs relies on the per-iteration locality of the safety argument; the PR does not claim full functional matching semantics over arbitrary-length concrete inputs.
• 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.
• The borrowed-array, slice, and predicate wrapper harnesses exercise their public searcher types directly. The owned-array constructor is verified directly, while its six single-field delegation methods reuse the exact MultiCharEqSearcher<[char; 4]> safety proof. Their duplicate harnesses are disabled to reduce solver cost and keep Kani CI runtime stable.
• The predicate harness exercises one mutable captured-state update per real iteration, but matcher-state correctness remains outside the proof boundary.

Verification

The active Challenge 20 verification suite contains 36 harnesses. The six disabled CharArraySearcher method harnesses duplicate the exact MultiCharEqSearcher<[char; 4]> safety proof and are retained as commented code for documentation and possible future use.

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.

[v3risec]

@feliperodri Thank you for the detailed review. I checked the three non-blocking concerns as follows.

1. Four-byte haystack bound

I confirmed that four bytes are sufficient for the byte-dependent part of one representative CharSearcher::next_match iteration for every needle width.

Let w = utf8_size, where 1 <= w <= 4. After memchr selects an occurrence of the final byte of the encoded needle, the implementation examines only:

haystack[new_finger - w..new_finger]

Thus, a complete candidate window contains at most four bytes. The memchr stub may select any in-bounds matching occurrence, so the safety argument does not depend on the distance between the current cursor and that occurrence.

The four-byte model also exercises repeated continuation-byte behavior. For example, U+10000 is encoded as F0 90 80 80. A scan may first find the 80 at index 2 and continue because the cursor has not yet reached width 4. A representative loop-head state at index 3 then exercises the successful comparison of the complete four-byte candidate. A different valid four-byte character with the same final continuation byte exercises the full-width mismatch branch. Widths 1 through 4, early final-byte occurrences, successful candidates, applicable mismatch cases, and memchr returning None are therefore covered locally.

This does not mean that one concrete four-byte input reproduces every complete execution over an arbitrarily long haystack. The claim is narrower: four bytes cover the largest byte window inspected by one transition. Within the bounded input model, arbitrary loop-head selection, strict progress, and conservative remainder summaries make the safety proof independent of a fixed unwind count.

2. Kani-specific implementations of trait defaults

In non-Kani builds, CharSearcher::next_reject and next_reject_back use the Searcher and ReverseSearcher defaults. The four filtered MultiCharEqSearcher methods also use their trait defaults.

Under #[cfg(kani)], these six methods have concrete overrides so loop contracts and summaries can refer to concrete searcher state. The overrides preserve the defaults' filtering structure: repeatedly call next or next_back, return the target classification unchanged, return None on Done, and continue on the opposite classification. Where a loop stub is used, omitted iterations are conservatively summarized by a safety-relevant exit relation.

The Kani proof therefore executes the verification-specific overrides, not the literal upstream default bodies. The shipped defaults are safe compositionally: they do not synthesize new ranges or perform indexing themselves; they only filter and forward ranges produced by the verified next or next_back operation. Non-Kani behavior is unchanged.

3. Audit of the manual remainder stubs

I compared all five remainder stubs with their corresponding concrete continuation behavior.

The loop-head relations are conservative. In particular, valid_char_next_match_loop_head intentionally does not require the current finger to be a UTF-8 boundary, because the byte scan may stop after a matching continuation byte. The MultiCharEqSearcher loop heads retain the valid active window and fixed directional endpoint while omitting matcher state. Every concrete continuation head satisfies these relations, while additional abstract heads are admitted.

For stub_char_next_match_remaining, every concrete Some((a, b)) exit satisfies b == self.finger, b <= search_end, b - a == utf8_size, and equality between haystack[a..b] and the cached needle encoding. It also satisfies a >= search_start. Every concrete None exit sets self.finger == self.finger_back == search_end.

The relation intentionally does not require a to be at or after the finger at stub entry. Repeated final bytes can cause a later successful candidate to begin before the current byte-scan cursor. Omitting that constraint may admit additional non-monotonic abstract exits, but it does not exclude a concrete exit.

For the two forward MultiCharEqSearcher stubs, a concrete Some((a, b)) satisfies suffix_start <= a < b <= search_end, has width at most char::MAX_LEN_UTF8, has UTF-8 boundaries at both ends, and leaves the concrete CharIndices window at b..search_end. None exhausts the window. The two reverse relations are symmetric, leaving search_start..a for Some and an empty window for None.

Strict forward progress increases finger or front while preserving the back endpoint; strict reverse progress decreases back while preserving the front endpoint. Since the cursor remains within the finite active window, every normally returning concrete continuation reaches a Some or None exit included by the corresponding relation.

For MultiCharEqSearcher, the over-approximation is over the safety-relevant projection, not the complete matcher state. Omitted FnMut calls may mutate captured state, but matcher state is deliberately absent from invariant C and the exit relations because it only chooses Match versus Reject; it cannot change the range already consumed by CharIndices. Predicate call counts, side effects, captured-state semantics, and exact matching behavior remain outside the proof scope.

Based on this audit, every concrete continuation's safety-relevant exit is included by its stub relation. Additional functionally unreachable exits are the conservative over-approximation required by this safety proof.

4. CharArraySearcher CI-cost deduplication

I also disabled the six direct CharArraySearcher method harnesses after they caused substantial duplicate solver cost and unstable Kani CI runtime.

CharArraySearcher<'a, 4> is a single-field wrapper around the exact MultiCharEqSearcher<'a, [char; 4]> instantiated by the direct harnesses. Its six methods only delegate to self.0, and type_invariant_char_array is exactly the invariant of the inner searcher. Running both harness sets therefore repeated the same underlying safety proof; in the failed CI run, the six wrapper method harnesses accounted for roughly 548 seconds of aggregate verification time.

The public [char; 4]::into_searcher constructor harness remains active to verify that construction establishes the wrapper invariant. The six method harnesses are retained as commented code. Their safety coverage is now compositional through the directly verified inner searcher and the wrapper's one-line delegation, rather than through six duplicate solver runs. This change addresses CI cost and does not reflect a soundness failure in those harnesses.

Please let me know if there are any other changes you would like me to make.