Challenge 21: Verify safety of StrSearcher with Kani

[v3risec]

Summary

This PR adds Kani verification for the substring searcher in core::str::pattern, covering the empty-needle implementation and the forward and reverse Two-Way search methods required by Challenge 21.

Verification Coverage Report (12/12 Harnesses Verified)

Searcher	Target	Coverage
Empty needle	next	Verifies forward Match/Reject alternation, completion, cursor movement by one UTF-8 character, valid returned ranges, and invariant preservation.
Empty needle	next_match	Verifies the finite Match filter, including the path that skips one Reject, without a loop contract or fixed unwind bound.
Empty needle	next_reject	Verifies the finite Reject filter, including the path that skips one Match, without a loop contract or fixed unwind bound.
Empty needle	next_back	Verifies reverse Match/Reject alternation, completion, cursor movement by one UTF-8 character, valid returned ranges, and invariant preservation.
Empty needle	next_match_back	Verifies the finite reverse Match filter, including the path that skips one Reject.
Empty needle	next_reject_back	Verifies the finite reverse Reject filter, including the path that skips one Match.
Two-Way	next	Verifies a representative real RejectAndMatch candidate, summarized forward/reverse byte scans, rejection boundary repair, forward progress, valid Match/Reject ranges, and invariant preservation.
Two-Way	next_match	Verifies MatchOnly search from an arbitrary failed-candidate prefix through one real candidate and a conservative suffix summary that covers a later Match or exhaustion.
Two-Way	next_reject	Verifies an arbitrary prefix of Match results followed by one real next step, covering every Reject or Done exit while checking progress and invariant preservation.
Two-Way	next_back	Verifies the reverse RejectAndMatch path, summarized reverse/forward byte scans, rejection boundary repair, reverse progress, valid Match/Reject ranges, and invariant preservation.
Two-Way	next_match_back	Verifies reverse MatchOnly search from an arbitrary failed-candidate prefix through one real candidate and a conservative suffix summary.
Two-Way	next_reject_back	Verifies an arbitrary prefix of reverse Match results followed by one real next_back step, covering every Reject or Done exit.

Verification Approach

The verification defines a stable-state invariant C for both StrSearcher implementations.

For EmptyNeedle, C requires the forward and reverse cursors to remain in bounds and on UTF-8 boundaries. The constructor harness establishes C, and each method harness starts from an arbitrary state satisfying C, checks the returned transition, and proves that C is preserved. The Kani-only character step nondeterministically selects a width from 1 through 4, bounds it by the remaining bytes, and imports the UTF-8 boundary fact permitted by Challenge 21. Because empty-needle results strictly alternate between Match and Reject, the four filtering methods need at most two concrete calls to next or next_back; this removes their production loops without adding a loop invariant or unwind bound.

For TwoWaySearcher, C captures the safety-relevant stable state: bounded UTF-8 cursor positions, nonzero bounded periods, bounded critical positions, consistent long-period sentinels, valid short-period memory states, and UTF-8 boundary facts for the short-period cuts. Each of the six method harnesses starts from a symbolic state satisfying this invariant and proves valid output ranges, cursor progress, preservation of preprocessing fields, valid memory-state transitions, and restoration of C before returning.

The Two-Way candidate loops use loop stubbing. A nondeterministic loop head represents any prefix of failed candidates, one representative candidate retains the real production control flow and arithmetic, and a suffix summary over-approximates any number of later failed candidates followed by either a Match, a Reject, or exhaustion. The summaries havoc only loop-carried state and constrain it with the corresponding loop-state relation.

The forward and reverse byte-scan loops are summarized by KaniTwoWayScan. A nondeterministic representative scan index checks the real indexing operations over the complete scan interval. The summary then conservatively chooses a mismatch position or a completed scan while retaining the first and last UTF-8 character bytes and the period probe needed to justify safe Match boundaries.

Two-Way Reject results may initially stop at byte positions that are not character boundaries. The Kani-only boundary-repair summaries first prove that the raw cursor is within the haystack, execute the real increment/decrement operation at a representative non-boundary loop head, and then use the Challenge 21 UTF-8 assumption that a character has at most three continuation bytes to summarize arrival at a nearby character boundary.

Verification Tradeoffs

Directly unwinding the nested Two-Way candidate and byte-scan loops does not finish within a practical verification budget and would make the proof depend on a fixed search length. The loop summaries avoid fixed unwind bounds for those loops and over-approximate their safety-relevant behavior.

The scan and candidate summaries are proof cuts for memory safety and valid UTF-8 result boundaries. They do not prove that every reported Match is the first or semantically correct substring match, nor do they prove the full functional correctness of the Two-Way algorithm.

The concrete harness inputs are symbolic valid UTF-8 subslices of 16-byte storage arrays. The loop summaries cover arbitrary loop prefixes and suffixes without fixed unwinding, but the current harness models do not constitute an arbitrary-length input proof.

Scope Assumptions

• This PR verifies safety properties: absence of the challenge-listed undefined behavior, valid UTF-8 output boundaries, ordered in-bounds ranges, and preservation of the stated stable-state invariant.
• UTF-8 decoding and boundary facts are imported only where permitted by the Challenge 21 assumptions.
• The six Two-Way method proofs are conditional on type_invariant_two_way_searcher.
• All Kani-specific implementations and proof summaries are isolated with #[cfg(kani)] and do not affect non-Kani builds.

Verification

All added Challenge 21 harnesses pass locally with Kani.

Resolves #278

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

[feliperodri]

@v3risec is this a complement for #538?

[v3risec]

@feliperodri Not exactly. The main differences are:

• Invariant: Verify safety of StrSearcher (Challenge 21) #538 mainly constrains the Two-Way cursors to be in bounds and on UTF-8 boundaries. This PR additionally constrains the period, critical positions, long/short-period states, and valid memory/memory_back states.
• Two-Way verification: Verify safety of StrSearcher (Challenge 21) #538 replaces TwoWaySearcher::new, next, and next_back with nondeterministic abstractions satisfying output constraints. This PR preserves a representative iteration of the real control flow, indexing, arithmetic, and state updates, while summarizing the scans and remaining loop iterations.
• Properties checked: In addition to valid UTF-8 result ranges and invariant preservation, this PR checks cursor progress, preprocessing-field preservation, memory transitions, and the relationship between returned ranges and the resulting state.
• EmptyNeedle: The coverage mostly overlaps, although this PR keeps the finite filtering behavior more concrete instead of replacing it with a general nondeterministic result.

So I would describe this PR as an alternative and strengthening of the Challenge 21 portion of #538, rather than a direct complement.

[feliperodri]

@v3risec can I review both PRs independently? If this one got approve, should I ignore #538?

[feliperodri]

Review: PR #621 — Challenge 21 (StrSearcher safety)

Verdict rationale

This PR is substantially and qualitatively different from the rejected #538. It does not repeat #538's fatal pattern, and it does real, careful verification work. However, it fails two required criteria that the author openly acknowledges in-code, so it cannot be approved as-is.

It is NOT the #538 body-swap / assume-the-conclusion failure (credit where due)

I classified all 12 #[cfg(not(kani))] blocks. None compile out TwoWaySearcher::new/next/next_back and replace them with pure nondeterministic stubs. Instead:

• Boundary-repair loop swaps — forward Searcher::next (pattern.rs diff L96/L177 → kani at L115-145) and reverse next_back (L334/L362/L443): the real searcher.next::<RejectAndMatch>(...)/next_back::<...> call is preserved; only the while !is_char_boundary(b) { b += 1 } repair loop is summarized.
• Candidate-loop swaps — continue 'search (L807, L1093) replaced by suffix summaries (kani_stub_after_failed_forward_candidate / ...reverse...).
• Inner byte-scan for-loop swaps — (L820, L859, L1101, L1152) replaced by kani_scan_forward/kani_scan_reverse, which still index needle[index]/haystack[position+index] at a nondeterministic representative index over the complete scan interval (diff L590-598), so memory-safety of the real indexing is genuinely checked.
• Empty-needle char decode (L68) — real .chars().next() retained in non-kani; kani models it as a nondet width 1..=4 bounded by remaining bytes plus a UTF-8 boundary assumption.

The real control flow, arithmetic (self.position += i - self.crit_pos + 1, self.position += self.period, etc.), and state transitions of the Two-Way algorithm are executed for one representative candidate. This is legitimate loop summarization, not a function-body swap.

Assume-the-conclusion check (FATAL in #538): PASS. The UTF-8 boundary facts on the Match path (assume_valid_utf8_two_way_match_boundaries, diff L1821-1855; assume_valid_utf8_two_way_reverse_match_start, L1857-1877) are gated behind assert!s that the relevant needle bytes were byte-equal to the haystack over the full final character, and the needle is valid UTF-8. Assuming the boundary then follows from "byte-equality with a valid-UTF-8 needle transfers the char boundary" — which is exactly a UTF-8 decoding fact Challenge 21 explicitly permits importing (assumptions 2 and 3). This is a defensible proof cut, not a raw assumption of the type-invariant conclusion.

Invariant is non-trivial: PASS. type_invariant_two_way_searcher (diff L2430-2482) constrains cursor bounds, char-boundaries of position/end, 1 <= period <= needle_len, crit_pos/crit_pos_back bounds, long/short-period sentinel consistency (memory/memory_back), and short-period boundary summaries. It is meaningful, not true.

Proof harnesses exist: 15 challenge #[kani::proof] harnesses (1 empty constructor + 6 empty methods + 6 Two-Way methods), plus the 2 retained small_slice_eq proofs. Absence of proof_for_contract is fine here since the challenge is invariant-based, not contract-based.

Blocking issue 1 — Verification is NOT unbounded (mandatory criterion FAILS)

The challenge states: "The verification must be unbounded—it must hold for inputs of arbitrary size." This PR hard-bounds inputs:

• pattern.rs diff L1271: const MAX_UTF8_BYTES: usize = 16;
• any_valid_utf8_str (L1273-1282) takes &[u8; MAX] and slices a 16-byte array; every harness builds haystack/needle from [u8; MAX_UTF8_BYTES] (e.g. L2752-2755).

So needle.len(), period, crit_pos, position, end are all bounded by 16. The author acknowledges this directly at diff L2748-2749 ("the concrete haystack and needle models remain bounded by MAX_UTF8_BYTES") and in the PR description ("the current harness models do not constitute an arbitrary-length input proof"). Summarizing the loops removes unwind bounds but does not make the input size unbounded. This is a clear failure of a mandatory requirement.

Blocking issue 2 — Creation does not establish C for TwoWay (success criterion 1 FAILS)

Criterion 1 requires proving that a searcher created from any valid UTF-8 haystack satisfies C. This is done for the empty needle via harness_str_searcher_empty_into_searcher (diff L2557-2565), which calls the real needle.into_searcher(haystack). But for the core Two-Way case there is no constructor harness: TwoWaySearcher::new is never invoked (grep: 0 references), and the invariant is only kani::assumed (e.g. L2772). The author explicitly disclaims this at diff L2745-2747: "Establishing it for the production preprocessing algorithm is a separate proof obligation and is not claimed by this module."

This is a real gap, not a formality: because the hand-written invariant is never cross-checked against what TwoWaySearcher::new actually produces, the preservation proofs (criterion 3) run over a hand-specified state set that is never tied to reachable states. If that set under-approximates reachable states, criterion 3 coverage is incomplete; the constructor harness is what closes this.

Non-blocking observations

• The loop-state relations (valid_two_way_*_loop_state) are used as both assume (loop head) and assert (loop exit) but are not independently shown to be inductive; soundness of the suffix summaries rests on them. Worth a reviewer note even after the blockers are fixed.
• kani::assume(false) is used to prune the continued-loop path (e.g. next_reject diff L271) after the per-iteration safety asserts fire — acceptable idiom, but each such site should be double-checked to confirm every concrete exit (Reject/Match/Done) is reachable via the symbolic prefix.

Direction to author

1. Make inputs unbounded: drive the loop summaries/type_invariant off symbolic lengths rather than a fixed 16-byte array, or otherwise remove the input-size bound, so the proof holds for arbitrary-size haystack/needle.
2. Add a Two-Way constructor harness that runs the real into_searcher/TwoWaySearcher::new on a valid UTF-8 (needle, haystack) and asserts type_invariant_two_way_searcher, closing criterion 1 for the core algorithm.

Once these two are addressed, the approach here (real algorithm + Challenge-21-permitted UTF-8 imports + non-trivial invariant) is a strong basis for approval.