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.

[v3risec]

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

Yes, they can be reviewed independently. For Challenge 21, #621 and #538 are alternative implementations, not complementary ones.

[v3risec]

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

Blocking issue 2

This issue is addressed by harness_str_searcher_two_way_into_searcher. The harness executes the real production path:

Pattern::into_searcher
    -> StrSearcher::new
    -> TwoWaySearcher::new

It requires a non-empty needle, checks that the resulting implementation is StrSearcherImpl::TwoWay, and immediately asserts type_invariant_two_way_searcher after construction. It also checks the initial cursor state and covers both period branches. Therefore, within the documented bounded input domain, the production constructor is now machine-checked to establish C, and the preservation harnesses are no longer disconnected from the constructor.

Non-blocking observation 1

I manually checked the preservation obligations for the valid_two_way_*_loop_state summaries against the production branches. This review covered cursor monotonicity, short-period updates to memory and memory_back, preservation of the long-period sentinel, and the Reject/Match/Done exits in both the forward and reverse directions.

These summaries are therefore supported by a documented trusted argument, and their preservation obligations have been manually checked against the production control flow. This is an informal manual justification rather than a separate Kani harness proving inductiveness for every loop transition.

Non-blocking observation 2

I also checked the relevant kani::assume(false) sites. In next_reject and next_reject_back, they occur only after a representative iteration returns Match, indicating that the surrounding loop continues. Before pruning, the harness checks cursor progress and the corresponding loop-state relation. Concrete Reject and Done exits return directly, while paths with multiple preceding Match steps are represented by choosing the symbolic prefix at the final loop head.

The other assume(false) sites either terminate paths after a boundary assertion has already failed or filter invalid UTF-8 inputs. This is the intended symbolic-prefix loop-cut idiom.

Unbounded verification

I agree that the current verification is bounded rather than genuinely unbounded. I experimented with a symbolic Vec model to remove the fixed byte-array bound, but the verification took too long(over 500s) and was not acceptable under the current CBMC object-size and CI configuration. I therefore do not present it as an unbounded proof.

The remaining proof has an explicit bounded scope: the Two-Way constructor harness covers haystacks of up to 4 bytes and non-empty needles of up to 3 bytes. Within that domain, the constructive generator reaches every valid UTF-8 string and kani::cover covers both the short-period and long-period branches. The existing method harnesses retain their documented bounded models.

This is a justified bounded verification, but I am not claiming that it satisfies the challenge’s literal requirement for arbitrary-size inputs.

I would appreciate any further feedback on this scope or on ways to make the summaries and harnesses more precise. I would be happy to make further changes or optimizations based on your suggestions.