diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index ae234e95a491b..2ed4fc9cd5fdb 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -2030,4 +2030,1195 @@ pub mod verify { true ); } + + // ================================================================== + // Challenge 20: verify safety of char-related Searcher methods + // + // For each searcher type we define a type invariant `C` and prove the + // challenge's three criteria against the real, unmodified method + // bodies: + // 1. `into_searcher` establishes `C` (base-case harnesses); + // 2. `C` implies the Searcher safety property: every returned index + // pair lies on UTF-8 char boundaries (asserted on the values the + // real methods return); + // 3. every method preserves `C` (inductive-step harnesses that admit + // an arbitrary `C`-satisfying state — not just reachable ones — + // then run the real method and re-assert `C`). + // + // Verification is bounded: haystacks are arbitrary UTF-8 of up to + // HAYSTACK_BYTES bytes (all four UTF-8 width classes are reachable), + // needles are arbitrary `char`s, and unwind bounds are justified by + // the fact that every search-loop iteration advances a cursor by at + // least one byte. The inductive-step harnesses are unbounded in the + // searcher *state* given the haystack: they cover every state + // satisfying `C`, whether or not a call sequence reaches it. + // ================================================================== + + /// Maximum haystack size in bytes. 5 bytes fits a 4-byte (maximum + /// width) character plus a neighbor, so every UTF-8 width class and + /// multi-iteration search loops are covered. + const HAYSTACK_BYTES: usize = 5; + + /// Unwind bound for loops that advance at least one byte per + /// iteration over a HAYSTACK_BYTES haystack (+1 for the final + /// iteration that observes the exhausted cursor, +1 for the + /// unwinding assertion itself). + const UNWIND: usize = HAYSTACK_BYTES + 2; + + /// An arbitrary UTF-8 string of 0..=N bytes written into a + /// caller-owned buffer, built constructively as a concatenation of + /// up to N symbolic `char`s — every valid UTF-8 string of at most N + /// bytes is reachable, multibyte characters included. Constructive + /// generation is used instead of filtering `kani::any()` bytes + /// through `from_utf8`, because under CI's `-Z loop-contracts` the + /// loop invariants inside `run_utf8_validation` abstract the + /// validator's loops, making its *functional* result unreliable as + /// a filter (and the constructive form is cheaper for the solver). + /// The char-appending steps are unrolled (loop-free) so harnesses can + /// use tight unwind bounds; those bounds then cheaply truncate the + /// (infeasible) panic-formatting paths of the code under test, + /// keeping the CBMC formula within `--object-bits 12`. + fn symbolic_str(buf: &mut [u8; N]) -> &str { + let mut len = 0usize; + { + let mut step = || { + if kani::any() { + let c: char = kani::any(); + let w = c.len_utf8(); + if len + w <= N { + c.encode_utf8(&mut buf[len..]); + len += w; + } + } + }; + // HAYSTACK_BYTES steps cover every string of <= N <= 5 bytes. + step(); + step(); + step(); + step(); + step(); + } + // SAFETY: `buf[..len]` is a concatenation of UTF-8 encodings of + // `char`s, hence valid UTF-8 by construction. + unsafe { crate::str::from_utf8_unchecked(&buf[..len]) } + } + + // ------------------------------------------------------------------ + // Stubs for memchr/memrchr. + // + // Challenge 20 allows assuming "the safety and functional correctness + // of all functions in the slice module", which covers + // `core::slice::memchr::{memchr,memrchr}`. Following the stub pattern + // accepted in PR #544, these are *semantically identical + // implementations* of the first/last-occurrence contract — no + // nondeterminism, no `kani::assume` — replacing only the optimized + // word-at-a-time scan, which CBMC unwinds poorly. Each harness's + // unwind bound fully unwinds the linear scan, so the proofs remain + // exhaustive. They are applied per-harness, only where the real call + // graph reaches memchr/memrchr (`CharSearcher::next_match` / + // `next_match_back`). + // ------------------------------------------------------------------ + + fn stub_memchr(x: u8, text: &[u8]) -> Option { + let mut i = 0; + while i < text.len() { + if text[i] == x { + return Some(i); + } + i += 1; + } + None + } + + fn stub_memrchr(x: u8, text: &[u8]) -> Option { + let mut i = text.len(); + while i > 0 { + i -= 1; + if text[i] == x { + return Some(i); + } + } + None + } + + // ------------------------------------------------------------------ + // CharSearcher + // ------------------------------------------------------------------ + + /// Type invariant `C` for `CharSearcher` (the condition of challenge + /// criterion 2): both fingers are in-bounds char boundaries of the + /// haystack in the right order, and the needle metadata is the true + /// UTF-8 encoding of the needle. (Inside `next_match`/`next_match_back` + /// the fingers may transiently leave boundaries — the documented + /// mid-loop state — but every public method must restore `C` on exit, + /// which is exactly what these harnesses check.) + fn type_invariant_cs(s: &CharSearcher<'_>) -> bool { + let mut enc = [0u8; 4]; + let enc_len = s.needle.encode_utf8(&mut enc).len(); + s.finger <= s.finger_back + && s.finger_back <= s.haystack.len() + && s.haystack.is_char_boundary(s.finger) + && s.haystack.is_char_boundary(s.finger_back) + && s.utf8_size() == enc_len + && s.utf8_encoded[..enc_len] == enc[..enc_len] + } + + /// An arbitrary `CharSearcher` state satisfying `C` — the induction + /// hypothesis for the step harnesses. This covers every + /// `C`-satisfying state, a superset of the states reachable by call + /// sequences from `into_searcher` (whose base case is + /// `verify_cs_into_searcher`). + fn any_char_searcher(haystack: &str) -> CharSearcher<'_> { + let needle: char = kani::any(); + let mut utf8_encoded = [0u8; 4]; + let utf8_size = needle.encode_utf8(&mut utf8_encoded).len() as u8; + let finger: usize = kani::any(); + let finger_back: usize = kani::any(); + kani::assume(finger <= finger_back && finger_back <= haystack.len()); + kani::assume(haystack.is_char_boundary(finger)); + kani::assume(haystack.is_char_boundary(finger_back)); + CharSearcher { haystack, finger, finger_back, needle, utf8_size, utf8_encoded } + } + + /// Criterion 2's safety property for a returned index pair. + fn assert_valid_range(haystack: &str, a: usize, b: usize) { + assert!(a <= b && b <= haystack.len()); + assert!(haystack.is_char_boundary(a)); + assert!(haystack.is_char_boundary(b)); + } + + /// Criterion 1: `char::into_searcher` establishes `C`. + #[kani::proof] + #[kani::unwind(8)] + pub fn verify_cs_into_searcher() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let needle: char = kani::any(); + let searcher = needle.into_searcher(haystack); + assert!(type_invariant_cs(&searcher)); + assert!(searcher.finger == 0); + assert!(searcher.finger_back == haystack.len()); + } + + /// Criteria 2+3 for the real `CharSearcher::next`. + #[kani::proof] + #[kani::unwind(8)] + pub fn verify_cs_next() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + match s.next() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "next returned Match or Reject"); + } + SearchStep::Done => kani::cover(true, "next returned Done"), + } + assert!(type_invariant_cs(&s)); + } + + /// Criteria 2+3 for the real `CharSearcher::next_back`. + #[kani::proof] + #[kani::unwind(8)] + pub fn verify_cs_next_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + match s.next_back() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "next_back returned Match or Reject"); + } + SearchStep::Done => kani::cover(true, "next_back returned Done"), + } + assert!(type_invariant_cs(&s)); + } + + /// Criteria 2+3 for the real `CharSearcher::next_match` — the memchr + /// loop, with memchr replaced by the semantically identical + /// `stub_memchr` (see above). Every loop iteration advances `finger` + /// by at least one byte, so UNWIND fully unwinds the search. + #[kani::proof] + #[kani::unwind(7)] + #[kani::stub(crate::slice::memchr::memchr, stub_memchr)] + pub fn verify_cs_next_match() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + match s.next_match() { + Some((a, b)) => { + assert_valid_range(haystack, a, b); + assert!(b - a == s.utf8_size()); + kani::cover(true, "next_match found the needle"); + } + None => kani::cover(true, "next_match found nothing"), + } + assert!(type_invariant_cs(&s)); + } + + /// Criteria 2+3 for the real `CharSearcher::next_match_back` — the + /// memrchr loop, with memrchr replaced by the semantically identical + /// `stub_memrchr`. Every iteration decreases `finger_back` by at + /// least one byte. + #[kani::proof] + #[kani::unwind(7)] + #[kani::stub(crate::slice::memchr::memrchr, stub_memrchr)] + pub fn verify_cs_next_match_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + match s.next_match_back() { + Some((a, b)) => { + assert_valid_range(haystack, a, b); + assert!(b - a == s.utf8_size()); + kani::cover(true, "next_match_back found the needle"); + } + None => kani::cover(true, "next_match_back found nothing"), + } + assert!(type_invariant_cs(&s)); + } + + /// Criteria 2+3 for `CharSearcher::next_reject` — the real trait + /// default, looping over the real `next()`. Each `next()` consumes at + /// least one byte, so UNWIND fully unwinds the loop. + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_cs_next_reject() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + if let Some((a, b)) = s.next_reject() { + assert_valid_range(haystack, a, b); + kani::cover(true, "next_reject returned a range"); + } + assert!(type_invariant_cs(&s)); + } + + /// Criteria 2+3 for `CharSearcher::next_reject_back` — the real trait + /// default over the real `next_back()`. + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_cs_next_reject_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_char_searcher(haystack); + if let Some((a, b)) = s.next_reject_back() { + assert_valid_range(haystack, a, b); + kani::cover(true, "next_reject_back returned a range"); + } + assert!(type_invariant_cs(&s)); + } + + /// From-creation run to `Done`: every step of the real `next()` on a + /// freshly created searcher yields boundary-valid ranges and + /// preserves `C` (criteria 1+2+3 composed). + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_cs_search_to_done() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let needle: char = kani::any(); + let mut s = needle.into_searcher(haystack); + loop { + match s.next() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b) + } + SearchStep::Done => break, + } + assert!(type_invariant_cs(&s)); + } + kani::cover(true, "searched the whole haystack"); + } + + // ------------------------------------------------------------------ + // MultiCharEqSearcher (and its four delegating wrapper searchers) + // ------------------------------------------------------------------ + + /// Type invariant `C` for `MultiCharEqSearcher`: the `CharIndices` + /// iterator views exactly the haystack subrange + /// `[front, front + rem)`, and both endpoints are char boundaries. + /// This is what makes the real `next`/`next_back` (and the trait + /// defaults built on them) return boundary-valid indices: `next()` + /// yields `front` and `next_back()` yields `front + rem` positions, + /// and `Chars`/`CharIndices` step through whole characters. + fn type_invariant_mces(s: &MultiCharEqSearcher<'_, C>) -> bool { + let front = s.char_indices.front_offset; + let rem = s.char_indices.iter.iter.len(); + front + rem <= s.haystack.len() + && s.haystack.is_char_boundary(front) + && s.haystack.is_char_boundary(front + rem) + && s.char_indices.iter.iter.as_slice().as_ptr().addr() + == s.haystack.as_ptr().addr() + front + } + + /// An arbitrary `C`-satisfying `MultiCharEqSearcher` state — the + /// induction hypothesis for the step harnesses. `char_eq.matches` is + /// a pure, safe predicate, so the safety argument is independent of + /// the concrete `MultiCharEq` instantiation; harnesses use + /// `[char; 2]`. + fn any_mces(haystack: &str) -> MultiCharEqSearcher<'_, [char; 2]> { + let k: usize = kani::any(); + let j: usize = kani::any(); + kani::assume(k <= j && j <= haystack.len()); + kani::assume(haystack.is_char_boundary(k)); + kani::assume(haystack.is_char_boundary(j)); + // SAFETY: k <= j <= len and both are char boundaries (assumed + // above); get_unchecked avoids dragging the slice-error panic + // machinery into the CBMC formula. + let sub = unsafe { haystack.get_unchecked(k..j) }; + let char_indices = crate::str::CharIndices { front_offset: k, iter: sub.chars() }; + let char_eq: [char; 2] = kani::any(); + MultiCharEqSearcher { char_eq, haystack, char_indices } + } + + /// Criterion 1: `into_searcher` establishes `C` for + /// `MultiCharEqSearcher`. + #[kani::proof] + pub fn verify_mces_into_searcher() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let chars: [char; 2] = kani::any(); + let searcher = MultiCharEqPattern(chars).into_searcher(haystack); + assert!(type_invariant_mces(&searcher)); + } + + /// Criteria 2+3 for the real `MultiCharEqSearcher::next`. + #[kani::proof] + pub fn verify_mces_next() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + match s.next() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next returned Match or Reject"); + } + SearchStep::Done => kani::cover(true, "mces next returned Done"), + } + assert!(type_invariant_mces(&s)); + } + + /// Criteria 2+3 for the real `MultiCharEqSearcher::next_back`. + #[kani::proof] + pub fn verify_mces_next_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + match s.next_back() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_back returned Match or Reject"); + } + SearchStep::Done => kani::cover(true, "mces next_back returned Done"), + } + assert!(type_invariant_mces(&s)); + } + + /// Criteria 2+3 for the four trait defaults on `MultiCharEqSearcher` + /// (`next_match`, `next_reject`, `next_match_back`, + /// `next_reject_back`) — the real default loops over the real + /// `next`/`next_back`. Each iteration consumes at least one byte. + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_mces_next_match() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + if let Some((a, b)) = s.next_match() { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_match returned a range"); + } + assert!(type_invariant_mces(&s)); + } + + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_mces_next_reject() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + if let Some((a, b)) = s.next_reject() { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_reject returned a range"); + } + assert!(type_invariant_mces(&s)); + } + + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_mces_next_match_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + if let Some((a, b)) = s.next_match_back() { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_match_back returned a range"); + } + assert!(type_invariant_mces(&s)); + } + + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_mces_next_reject_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let mut s = any_mces(haystack); + if let Some((a, b)) = s.next_reject_back() { + assert_valid_range(haystack, a, b); + kani::cover(true, "mces next_reject_back returned a range"); + } + assert!(type_invariant_mces(&s)); + } + + /// The four remaining challenge searcher types + /// (`CharArraySearcher`, `CharArrayRefSearcher`, `CharSliceSearcher`, + /// `CharPredicateSearcher`) are `pattern_methods!` newtype delegations + /// to `MultiCharEqSearcher`, so their invariant is the wrapped + /// searcher's `C` and all six methods delegate to the code verified + /// above. These harnesses check the delegation itself end-to-end for + /// the array wrapper (the other three wrappers expand from the same + /// macro with a different `MultiCharEq` instance; `matches` is a pure + /// safe predicate in all four). + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_char_array_searcher_delegation() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let chars: [char; 2] = kani::any(); + let mut s = chars.into_searcher(haystack); + assert!(type_invariant_mces(&s.0)); + match s.next() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b) + } + SearchStep::Done => {} + } + if let Some((a, b)) = s.next_match() { + assert_valid_range(haystack, a, b); + } + assert!(type_invariant_mces(&s.0)); + } + + #[kani::proof] + #[kani::unwind(7)] + pub fn verify_char_array_searcher_delegation_back() { + let mut buf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut buf); + let chars: [char; 2] = kani::any(); + let mut s = chars.into_searcher(haystack); + match s.next_back() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b) + } + SearchStep::Done => {} + } + if let Some((a, b)) = s.next_match_back() { + assert_valid_range(haystack, a, b); + } + assert!(type_invariant_mces(&s.0)); + } + // ================================================================== + // Challenge 21: verify safety of StrSearcher (empty-needle and + // Two-Way searchers). + // + // Same methodology as the Challenge 20 section above: real method + // bodies, a base-case harness proving the constructor establishes the + // type invariant `C`, and inductive-step harnesses that admit an + // arbitrary `C`-satisfying state, run one real method and re-assert + // `C` and the boundary property on whatever it returned. + // + // Inputs are *symbolic-length* byte slices (`any_utf8`), constrained + // to be valid UTF-8 by the byte-table predicate `utf8_local` instead + // of being built char by char, so no proof depends on a haystack + // length: the only size parameter is the backing-array size + // (`HAY_MAX`/`NDL_MAX`), the same CBMC memory-model limitation as + // `ARR_SIZE` in `str::validations::verify::check_run_utf8_validation`. + // + // Loop bounds. The real `'search` loops are not unwound to the + // haystack length: + // - `StrSearcher::next`/`next_back` instantiate them with + // `RejectAndMatch`, whose `use_early_reject()` makes the loop + // return as soon as the cursor has moved, and every `continue + // 'search` moves the cursor by at least one byte -- so the loop + // runs at most two iterations for any haystack. Only the inner + // byte-compare loops scale, with the needle length. + // - `next_match`/`next_match_back` instantiate them with `MatchOnly`, + // whose loop body is the *same code* minus that early exit. The + // `verify_twoway_search_step_*` harnesses run one real iteration + // (the `RejectAndMatch` instantiation) from an *arbitrary* state + // satisfying the loop's invariant `S` and prove it preserves `S` + // and that any Match it reports is byte-exact and boundary-valid; + // that is the inductive step of the unbounded `MatchOnly` loop, + // machine-checked through the real code. The direct + // `verify_twoway_step_next_match*` harnesses add end-to-end + // coverage of the real `MatchOnly` loop up to the array size. + // + // The Two-Way invariant is content-coupled: boundary validity of a + // returned Match hinges on the match being byte-exact (a byte-exact + // image of valid UTF-8 starting at a boundary ends at a boundary), + // which in short-period mode depends on the memorized prefix really + // matching the haystack and `period` being an exact period of the + // needle. Those are clauses of `C`, established by `new()` and + // preserved by the search steps -- not assumptions about the result. + // Content clauses are stated with `crate::forall!` over the backing + // array (constant bounds, guarded by the real lengths), which is the + // form CBMC's SAT backend can instantiate. + // + // Loop contracts (`-Z loop-contracts`) on the real `'search` loops + // were tried and are not usable with the pinned Kani without + // rewriting the loops themselves: CBMC requires a contract on every + // nested loop, Kani's `for`-loop contract support hoists the inner + // range construction to the outer loop head (where `start` is not + // yet computed) and computes `end - start` for legitimately empty + // reversed ranges, and Kani's compiler panics on `let start = if .. + // { .. } else { cmp::max(..) }` inside a contracted loop. Keeping the + // shipped code byte-identical was preferred. + // ================================================================== + + /// Backing-array size for haystacks: haystack lengths range over + /// `0..=HAY_MAX`. No loop is unwound to this size (see the module + /// comment), so it is a CBMC memory-model parameter, not a proof + /// bound; 16 keeps every harness well inside CI's per-harness budget. + const HAY_MAX: usize = 16; + /// Backing-array size for needles in the Two-Way inductive-step + /// harnesses: needle lengths range over `1..=NDL_MAX`. The inner + /// byte-compare loops of the search are unwound to this size. + const NDL_MAX: usize = 8; + /// Needle bound for the base case `verify_str_searcher_new`, which + /// runs the real `maximal_suffix`/`reverse_maximal_suffix` (unwound; + /// see the harness comment). + const NEW_NDL_MAX: usize = 8; + /// Constant bound of the quantifiers in the content predicates + /// (`prefix_eq`, `suffix_eq`, `has_period`); must cover every needle + /// array used with them. + const NDL_QMAX: usize = 8; + /// Backing-array sizes for the direct `next_match`/`next_match_back` + /// harnesses, which do unwind the real `MatchOnly` loop to the + /// haystack length (their unbounded inductive step is + /// `verify_twoway_search_step_*`, at the full `NDL_MAX`). + const MATCH_HAY_MAX: usize = 5; + const MATCH_NDL_MAX: usize = 6; + /// Extra bytes past the maximum length so the byte-table predicates + /// may read up to four bytes after any index `< MAX` without leaving + /// the backing array. + const PAD: usize = 4; + const _: () = + assert!(NEW_NDL_MAX <= NDL_QMAX && NDL_MAX <= NDL_QMAX && MATCH_NDL_MAX <= NDL_QMAX); + + // ------------------------------------------------------------------ + // Symbolic-length UTF-8 inputs + // ------------------------------------------------------------------ + + /// The byte-table definition of "`arr[..len]` is valid UTF-8", as two + /// facts local to a 4-byte window and quantified over every index of + /// the backing array (`i >= len` positions are vacuous): + /// + /// - U-lead: every non-continuation byte at `i` is a valid leading + /// byte (`<0x80`, `0xC2..=0xDF`, `0xE0..=0xEF`, `0xF0..=0xF4`) of + /// width `w`, its `w - 1` continuation bytes are present (with the + /// second-byte restrictions for `E0`/`ED`/`F0`/`F4`: no overlong + /// forms, no surrogates, nothing above U+10FFFF), `i + w <= len`, + /// and the byte at `i + w` is a leading byte or the end of the + /// string. + /// - U-cover: every byte lies within three bytes after a + /// non-continuation byte (at `i = 0`: the first byte leads). + /// + /// Both are properties of every valid UTF-8 string, so assuming them + /// is sound; together they are equivalent to `from_utf8(..).is_ok()` + /// (U-cover at 0 starts the parse on a leading byte, U-lead makes + /// each step a valid sequence that lands on the next leading byte or + /// exactly on `len`), which justifies `from_utf8_unchecked` in + /// `any_utf8`. `from_utf8` itself is not used as the filter because + /// under CI's `-Z loop-contracts` the invariants in + /// `run_utf8_validation` abstract its loops and its result no longer + /// constrains the bytes. + /// + /// The quantifier bodies are deliberately branch-free (bitwise `&`/`|`, + /// indicator arithmetic, no helper calls, no nested closures): CBMC + /// instantiates a quantifier body as one expression, and control flow + /// or statement expressions inside it are rejected or blow up + /// instrumentation. Every read stays inside the backing array because + /// of `PAD`. + fn utf8_local(arr: &[u8; N], len: usize) -> bool { + let p = arr.as_ptr(); + let lead = crate::forall!(|i in (0, N - PAD)| unsafe { + let i: usize = i; + let b0 = *p.wrapping_add(i); + let b1 = *p.wrapping_add(i.wrapping_add(1)); + let b2 = *p.wrapping_add(i.wrapping_add(2)); + let b3 = *p.wrapping_add(i.wrapping_add(3)); + let c0 = (b0 as i8) < -64; + let c1 = (b1 as i8) < -64; + let c2 = (b2 as i8) < -64; + let c3 = (b3 as i8) < -64; + // width of the sequence led by b0 (0: not a valid leading byte) + let w: usize = (b0 < 0x80) as usize + + (((b0 >= 0xC2) & (b0 < 0xE0)) as usize) * 2 + + (((b0 >= 0xE0) & (b0 < 0xF0)) as usize) * 3 + + (((b0 >= 0xF0) & (b0 < 0xF5)) as usize) * 4; + let cw = (*p.wrapping_add(i.wrapping_add(w)) as i8) < -64; + let sec = ((b0 != 0xE0) | (b1 >= 0xA0)) + & ((b0 != 0xED) | (b1 < 0xA0)) + & ((b0 != 0xF0) | (b1 >= 0x90)) + & ((b0 != 0xF4) | (b1 < 0x90)); + (i >= len) + | c0 + | ((w != 0) + & (i.wrapping_add(w) <= len) + & ((w < 2) | (c1 & sec)) + & ((w < 3) | c2) + & ((w < 4) | c3) + & ((i.wrapping_add(w) == len) | !cw)) + }); + let cover = crate::forall!(|i in (0, N - PAD)| unsafe { + let i: usize = i; + (i >= len) + | ((*p.wrapping_add(i) as i8) >= -64) + | ((i >= 1) & ((*p.wrapping_add(i.saturating_sub(1)) as i8) >= -64)) + | ((i >= 2) & ((*p.wrapping_add(i.saturating_sub(2)) as i8) >= -64)) + | ((i >= 3) & ((*p.wrapping_add(i.saturating_sub(3)) as i8) >= -64)) + }); + lead && cover + } + + /// An arbitrary valid UTF-8 string of symbolic length `0..=N - PAD` + /// backed by a caller-owned array of arbitrary content. + fn any_utf8(arr: &[u8; N]) -> &str { + let len: usize = kani::any(); + kani::assume(len <= N - PAD); + kani::assume(utf8_local(arr, len)); + // SAFETY: `utf8_local` is the byte-table definition of UTF-8 + // validity (see its documentation). + unsafe { crate::str::from_utf8_unchecked(&arr[..len]) } + } + + // ------------------------------------------------------------------ + // Content predicates of the Two-Way invariant (constant-bound + // quantifiers; every read is guarded by the real lengths and stays + // inside the backing arrays). + // ------------------------------------------------------------------ + + /// `h[pos + j] == nb[j]` for every `j < k`. Callers establish + /// `k <= nb.len()` and `pos + k <= h.len()`. Out-of-range `j` are + /// vacuous; their read index is clamped to 0 so every read stays in + /// bounds (the quantifier body must be branch-free, see `utf8_local`). + fn prefix_eq(h: &[u8], nb: &[u8], pos: usize, k: usize) -> bool { + let hp = h.as_ptr(); + let np = nb.as_ptr(); + crate::forall!(|j in (0, NDL_QMAX)| unsafe { + let j: usize = j; + let jj = j * ((j < k) as usize); + (j >= k) | (*hp.wrapping_add(pos.wrapping_add(jj)) == *np.wrapping_add(jj)) + }) + } + + /// `h[start + j] == nb[j]` for every `j` in `m..nb.len()`. Callers + /// establish `m <= nb.len()` and `start + nb.len() <= h.len()`. + /// Out-of-range `j` are vacuous; their read index is clamped to `m`. + fn suffix_eq(h: &[u8], nb: &[u8], start: usize, m: usize) -> bool { + let n = nb.len(); + let hp = h.as_ptr(); + let np = nb.as_ptr(); + crate::forall!(|j in (0, NDL_QMAX)| unsafe { + let j: usize = j; + let inr = (j >= m) & (j < n); + let jj = m.wrapping_add(j.wrapping_sub(m) * (inr as usize)); + !inr | (*hp.wrapping_add(start.wrapping_add(jj)) == *np.wrapping_add(jj)) + }) + } + + /// `period` is a period of `nb`: `nb[j] == nb[j + period]` whenever + /// `j + period < nb.len()`. Callers establish `period <= nb.len()`. + /// Out-of-range `j` are vacuous; their read index is clamped to 0. + fn has_period(nb: &[u8], period: usize) -> bool { + let n = nb.len(); + let np = nb.as_ptr(); + crate::forall!(|j in (0, NDL_QMAX)| unsafe { + let j: usize = j; + let inr = j.wrapping_add(period) < n; + let jj = j * (inr as usize); + !inr | (*np.wrapping_add(jj) == *np.wrapping_add(jj.wrapping_add(period))) + }) + } + + // ------------------------------------------------------------------ + // Type invariant `C` + // ------------------------------------------------------------------ + + fn type_invariant_empty_needle(en: &EmptyNeedle, haystack: &str) -> bool { + en.position <= haystack.len() + && en.end <= haystack.len() + && haystack.is_char_boundary(en.position) + && haystack.is_char_boundary(en.end) + } + + /// Search-state invariant `S` of the Two-Way searcher: everything in + /// `C` except the char-boundary clauses on the cursors. `S` is what + /// the real `'search` loops maintain at *every* iteration (the + /// cursors move by algorithmic shifts and may sit inside a character + /// between iterations); `C` adds the boundary clauses that hold + /// between public calls. + /// - Clauses 1-2: cursors in-bounds (`position <= end` is + /// deliberately NOT required -- the two cursors evolve + /// independently). + /// - Clauses 5-9: constructor-established well-formedness the search + /// loops need for panic-freedom and strict cursor progress. + /// - Clauses 10-11 (short-period mode only): `period` is an exact + /// period of the needle, and the memorized bytes really match the + /// haystack at the current alignment -- the content coupling that + /// makes a Match byte-exact and hence boundary-valid. + fn search_state_two_way(tw: &TwoWaySearcher, haystack: &str, needle: &str) -> bool { + let n = needle.len(); + let h = haystack.as_bytes(); + let nb = needle.as_bytes(); + tw.position <= haystack.len() // 1 + && tw.end <= haystack.len() // 2 + && n >= 1 // 5 + && tw.crit_pos <= n // 6 + && tw.crit_pos_back <= n // 7 + && tw.period >= 1 // 8 + // 8b: the critical factorization theorem's |u| < period(x). + // This is what justifies the period-shift memorization in the + // 'search loop: after `position += period; memory = n - period`, + // the skipped prefix lies inside the previously verified right + // part (indices >= crit_pos), so clause 11 is preserved. + && tw.crit_pos < tw.period // 8b + // 8c: the mirror fact for the reverse search (the code + // comment on next_back: "We need |u| < period(x) for the + // forward case and thus |v'| < period(x) for the reverse"), + // justifying the back-shift memorization for clause 11b. + && n - tw.crit_pos_back < tw.period // 8c + && (tw.memory == usize::MAX) == (tw.memory_back == usize::MAX) // 9 + && (if tw.memory == usize::MAX { + // long-period mode: period = max(crit_pos, n - crit_pos) + 1 + // with crit_pos in [1, n-1] (crit_pos = 0 short-circuits to + // the short branch via the vacuous prefix comparison, and + // the maximal suffix is nonempty), so period <= n. The + // bound is load-bearing: next_back's `end -= period` runs + // with end >= n and would underflow if period could be + // n + 1. No memorization in this mode. + tw.period <= n + } else { + tw.period <= n + && tw.memory <= n + && tw.memory_back <= n + // 10: period is an exact period of the needle + && has_period(nb, tw.period) + // 11: memorized prefix matches at current alignment + // (only meaningful while a candidate window fits) + && (tw.position + n > h.len() + || prefix_eq(h, nb, tw.position, tw.memory)) + // 11b: memorized suffix matches at the back alignment + && (tw.end < n || suffix_eq(h, nb, tw.end - n, tw.memory_back)) + }) + } + + /// Two-Way invariant `C` = `S` plus clauses 3-4: both cursors lie on + /// char boundaries of the haystack. + fn type_invariant_two_way(tw: &TwoWaySearcher, haystack: &str, needle: &str) -> bool { + search_state_two_way(tw, haystack, needle) + && haystack.is_char_boundary(tw.position) // 3 + && haystack.is_char_boundary(tw.end) // 4 + } + + /// Per-clause assertion version of `search_state_two_way`, used by + /// the inductive-step harnesses so a counterexample names the exact + /// clause it violates. + fn assert_two_way_s(tw: &TwoWaySearcher, haystack: &str, needle: &str) { + let n = needle.len(); + let h = haystack.as_bytes(); + let nb = needle.as_bytes(); + assert!(tw.position <= haystack.len(), "c1 position bound"); + assert!(tw.end <= haystack.len(), "c2 end bound"); + assert!(n >= 1, "c5 needle nonempty"); + assert!(tw.crit_pos <= n, "c6 crit_pos bound"); + assert!(tw.crit_pos_back <= n, "c7 crit_pos_back bound"); + assert!(tw.period >= 1, "c8 period positive"); + assert!(tw.crit_pos < tw.period, "c8b crit_pos < period"); + assert!(n - tw.crit_pos_back < tw.period, "c8c n - crit_pos_back < period"); + assert!((tw.memory == usize::MAX) == (tw.memory_back == usize::MAX), "c9 mode coherence"); + if tw.memory == usize::MAX { + assert!(tw.period <= n, "c10L long period bound"); + } else { + assert!(tw.period <= n, "c10a short period bound"); + assert!(tw.memory <= n, "c10b memory bound"); + assert!(tw.memory_back <= n, "c10c memory_back bound"); + assert!(has_period(nb, tw.period), "c10 exact period"); + assert!( + tw.position + n > h.len() || prefix_eq(h, nb, tw.position, tw.memory), + "c11 memory matches" + ); + assert!( + tw.end < n || suffix_eq(h, nb, tw.end - n, tw.memory_back), + "c11b memory_back matches" + ); + } + } + + /// Per-clause assertion version of `type_invariant_two_way`. + fn assert_two_way_c(tw: &TwoWaySearcher, haystack: &str, needle: &str) { + assert_two_way_s(tw, haystack, needle); + assert!(haystack.is_char_boundary(tw.position), "c3 position boundary"); + assert!(haystack.is_char_boundary(tw.end), "c4 end boundary"); + } + + fn type_invariant_str_searcher(s: &StrSearcher<'_, '_>) -> bool { + match &s.searcher { + StrSearcherImpl::Empty(en) => { + s.needle.is_empty() && type_invariant_empty_needle(en, s.haystack) + } + StrSearcherImpl::TwoWay(tw) => { + !s.needle.is_empty() && type_invariant_two_way(tw, s.haystack, s.needle) + } + } + } + + // ------------------------------------------------------------------ + // Criterion 1: creation establishes `C` + // ------------------------------------------------------------------ + + /// `StrSearcher::new` establishes `C` for both the empty-needle and + /// Two-Way variants (this is also the base case for the + /// inductive-step harnesses below). The haystack has symbolic length + /// (only its length reaches `new`). The needle is bounded by + /// `NEW_NDL_MAX`: `new` runs the real `maximal_suffix` / + /// `reverse_maximal_suffix`, whose `while let` loops are unwound + /// here (at most 2n+2 iterations each, hence the unwind bound), and the clauses `C` takes + /// from them (`crit_pos < period`, `period <= n`, exactness of the + /// short-mode period) are consequences of the critical factorization + /// theorem rather than of a loop-local invariant. The inductive steps + /// assume nothing but `C`, so this bound is confined to the pure + /// function of the needle. + #[kani::proof] + #[kani::unwind(20)] + pub fn verify_str_searcher_new() { + let hbuf: [u8; HAY_MAX + PAD] = kani::any(); + let nbuf: [u8; NEW_NDL_MAX + PAD] = kani::any(); + let haystack = any_utf8(&hbuf); + let needle = any_utf8(&nbuf); + let s = StrSearcher::new(haystack, needle); + assert!(type_invariant_str_searcher(&s)); + match &s.searcher { + StrSearcherImpl::Empty(_) => kani::cover(true, "empty-needle variant created"), + StrSearcherImpl::TwoWay(tw) => { + assert!(tw.position == 0 && tw.end == haystack.len()); + kani::cover(tw.memory == usize::MAX, "long-period factorization reached"); + kani::cover(tw.memory != usize::MAX, "short-period factorization reached"); + } + } + } + + // ------------------------------------------------------------------ + // Criteria 2+3: inductive steps + // ------------------------------------------------------------------ + + // No Two-Way-arm "from creation" harnesses: composing the real + // `new()` (whose reachable-state constraint threads through the whole + // maximal_suffix computation) with the real search loops overflows + // CBMC's `--object-bits 12` limit at any useful input size. They are + // also logically redundant: `verify_str_searcher_new` machine-checks + // that creation establishes `C`, and the `verify_twoway_step_*` + // harnesses machine-check that from EVERY `C`-satisfying state (a + // superset of all reachable states) the real methods return + // boundary-valid ranges and preserve `C` -- so any call sequence from + // creation is covered by induction. The same composition argument + // covers the `next_reject`/`next_reject_back` trait defaults on the + // Two-Way arm: they are `Searcher`-generic loops over `next`/ + // `next_back` that cannot carry a `StrSearcher`-specific loop + // invariant, and each iteration is one of the steps proven here. + // Their empty-needle variants are machine-checked below + // (`verify_empty_step_next_reject`/`_back`). + + /// An arbitrary `C`-satisfying empty-needle searcher (induction + /// hypothesis; base case in `verify_str_searcher_new`). + fn any_empty_searcher<'a>(haystack: &'a str) -> StrSearcher<'a, 'static> { + let position: usize = kani::any(); + let end: usize = kani::any(); + kani::assume(position <= haystack.len() && end <= haystack.len()); + kani::assume(haystack.is_char_boundary(position)); + kani::assume(haystack.is_char_boundary(end)); + StrSearcher { + haystack, + needle: "", + searcher: StrSearcherImpl::Empty(EmptyNeedle { + position, + end, + is_match_fw: kani::any(), + is_match_bw: kani::any(), + is_finished: kani::any(), + }), + } + } + + /// An arbitrary `C`-satisfying Two-Way searcher (induction + /// hypothesis; base case in `verify_str_searcher_new`). All eight + /// fields are symbolic; `byteset` is unconstrained, so the proofs + /// also show memory safety does not depend on the fingerprint. + /// `long_period` selects the factorization mode (`memory == + /// usize::MAX` or not); each harness below is instantiated once per + /// mode, which halves the formula CBMC has to solve at a time while + /// still covering every `C`-state between the two. + fn any_twoway_searcher<'a, 'b>( + haystack: &'a str, + needle: &'b str, + long_period: bool, + ) -> StrSearcher<'a, 'b> { + let tw = TwoWaySearcher { + crit_pos: kani::any(), + crit_pos_back: kani::any(), + period: kani::any(), + byteset: kani::any(), + position: kani::any(), + end: kani::any(), + memory: kani::any(), + memory_back: kani::any(), + }; + kani::assume((tw.memory == usize::MAX) == long_period); + let s = StrSearcher { haystack, needle, searcher: StrSearcherImpl::TwoWay(tw) }; + kani::assume(type_invariant_str_searcher(&s)); + s + } + + /// An arbitrary `S`-satisfying Two-Way search state -- the induction + /// hypothesis for the single-iteration lemmas below (a superset of + /// the `C`-states, since `S` drops the boundary clauses). + fn any_twoway_search_state(haystack: &str, needle: &str, long_period: bool) -> TwoWaySearcher { + let tw = TwoWaySearcher { + crit_pos: kani::any(), + crit_pos_back: kani::any(), + period: kani::any(), + byteset: kani::any(), + position: kani::any(), + end: kani::any(), + memory: kani::any(), + memory_back: kani::any(), + }; + kani::assume((tw.memory == usize::MAX) == long_period); + kani::assume(search_state_two_way(&tw, haystack, needle)); + tw + } + + /// Inductive step for the empty-needle variant: from any + /// `C`-satisfying state, each real method returns boundary-valid + /// ranges and preserves `C`. Unbounded in the haystack: the arm is + /// loop-free per call (`Chars::next`/`next_back` decode one scalar + /// straight-line) and alternates Match/Reject, so the `next_match`/ + /// `next_reject` default loops run at most two iterations. + macro_rules! empty_needle_step { + ($name:ident, $call:ident, step) => { + #[kani::proof] + #[kani::unwind(3)] + pub fn $name() { + let hbuf: [u8; HAY_MAX + PAD] = kani::any(); + let haystack = any_utf8(&hbuf); + let mut s = any_empty_searcher(haystack); + match s.$call() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "empty-needle step returned a range"); + } + SearchStep::Done => kani::cover(true, "empty-needle step returned Done"), + } + assert!(type_invariant_str_searcher(&s)); + } + }; + ($name:ident, $call:ident, opt) => { + #[kani::proof] + #[kani::unwind(3)] + pub fn $name() { + let hbuf: [u8; HAY_MAX + PAD] = kani::any(); + let haystack = any_utf8(&hbuf); + let mut s = any_empty_searcher(haystack); + match s.$call() { + Some((a, b)) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "empty-needle step returned a range"); + } + None => kani::cover(true, "empty-needle step returned None"), + } + assert!(type_invariant_str_searcher(&s)); + } + }; + } + + empty_needle_step!(verify_empty_step_next, next, step); + empty_needle_step!(verify_empty_step_next_back, next_back, step); + empty_needle_step!(verify_empty_step_next_match, next_match, opt); + empty_needle_step!(verify_empty_step_next_match_back, next_match_back, opt); + empty_needle_step!(verify_empty_step_next_reject, next_reject, opt); + empty_needle_step!(verify_empty_step_next_reject_back, next_reject_back, opt); + + /// Inductive step for the Two-Way variant through the public methods + /// (`next`, `next_back`, `next_match`, `next_match_back`): from any + /// `C`-satisfying state the real method returns boundary-valid ranges + /// and re-establishes `C`. + /// + /// Unwind bounds. For `next`/`next_back` (`NDL_MAX + 1`) the `'search` + /// loop runs at most two iterations for *any* haystack (see the + /// module comment), the inner byte-compare loops at most `NDL_MAX`, + /// and the char-boundary walks in `StrSearcher::next`/`next_back` at + /// most 3 (U-cover); the bound covers all of them, and the haystack + /// length is unconstrained up to the array size. For `next_match`/ + /// `next_match_back` (`MATCH_HAY_MAX + 2 = MATCH_NDL_MAX + 1`) the + /// `MatchOnly` loop advances the cursor by at least one byte per + /// iteration, so the bound covers every iteration up to the smaller + /// array sizes these coverage harnesses use; their unbounded + /// inductive step is `verify_twoway_search_step_*` below. + macro_rules! twoway_step { + ($name:ident, $call:ident, $long:expr, step) => { + #[kani::proof] + #[kani::unwind(9)] + pub fn $name() { + let hbuf: [u8; HAY_MAX + PAD] = kani::any(); + let nbuf: [u8; NDL_MAX + PAD] = kani::any(); + let haystack = any_utf8(&hbuf); + let needle = any_utf8(&nbuf); + kani::assume(!needle.is_empty()); + let mut s = any_twoway_searcher(haystack, needle, $long); + match s.$call() { + SearchStep::Match(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "two-way step returned Match"); + } + SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "two-way step returned Reject"); + } + SearchStep::Done => kani::cover(true, "two-way step returned Done"), + } + if let StrSearcherImpl::TwoWay(ref tw) = s.searcher { + assert_two_way_c(tw, haystack, needle); + } else { + unreachable!(); + } + } + }; + ($name:ident, $call:ident, $long:expr, opt) => { + #[kani::proof] + #[kani::unwind(7)] + pub fn $name() { + let hbuf: [u8; MATCH_HAY_MAX + PAD] = kani::any(); + let nbuf: [u8; MATCH_NDL_MAX + PAD] = kani::any(); + let haystack = any_utf8(&hbuf); + let needle = any_utf8(&nbuf); + kani::assume(!needle.is_empty()); + let mut s = any_twoway_searcher(haystack, needle, $long); + match s.$call() { + Some((a, b)) => { + assert_valid_range(haystack, a, b); + kani::cover(true, "two-way step found a match"); + } + None => kani::cover(true, "two-way step found nothing"), + } + if let StrSearcherImpl::TwoWay(ref tw) = s.searcher { + assert_two_way_c(tw, haystack, needle); + } else { + unreachable!(); + } + } + }; + } + + // `_short`: short-period mode (memorization active, content clauses + // 10/11/11b live); `_long`: long-period mode (`memory == usize::MAX`). + twoway_step!(verify_twoway_step_next_short, next, false, step); + twoway_step!(verify_twoway_step_next_long, next, true, step); + twoway_step!(verify_twoway_step_next_back_short, next_back, false, step); + twoway_step!(verify_twoway_step_next_back_long, next_back, true, step); + twoway_step!(verify_twoway_step_next_match_short, next_match, false, opt); + twoway_step!(verify_twoway_step_next_match_long, next_match, true, opt); + twoway_step!(verify_twoway_step_next_match_back_short, next_match_back, false, opt); + twoway_step!(verify_twoway_step_next_match_back_long, next_match_back, true, opt); + + /// One real iteration of the `'search` loops, from an arbitrary + /// `S`-state: `TwoWaySearcher::next::` (resp. + /// `next_back`) returns as soon as the cursor moves (or on the first + /// iteration), so it *is* the loop body shared with `MatchOnly` (whose + /// only difference is not taking that early exit). Proves: `S` is + /// preserved; a `Match(a, b)` is byte-exact (`haystack[a..b] == + /// needle`), hence `a` and `b` lie on char boundaries (U-lead on the + /// needle's last leading byte and on the haystack); a `Reject` spans + /// `old_cursor..cursor` in bounds. Together with + /// `verify_str_searcher_new` this is the induction proving + /// `next_match`/`next_match_back` safe for haystacks of any length. + /// Instantiated per direction and per factorization mode. + macro_rules! twoway_search_step { + ($name:ident, fwd, $long:expr) => { + #[kani::proof] + #[kani::unwind(9)] + pub fn $name() { + let hbuf: [u8; HAY_MAX + PAD] = kani::any(); + let nbuf: [u8; NDL_MAX + PAD] = kani::any(); + let haystack = any_utf8(&hbuf); + let needle = any_utf8(&nbuf); + kani::assume(!needle.is_empty()); + let mut tw = any_twoway_search_state(haystack, needle, $long); + let old_pos = tw.position; + match tw.next::(haystack.as_bytes(), needle.as_bytes(), $long) { + SearchStep::Match(a, b) => { + assert!( + b == a + needle.len() && b <= haystack.len(), + "match window in bounds" + ); + assert!( + haystack.as_bytes()[a..b] == *needle.as_bytes(), + "match is byte-exact" + ); + assert_valid_range(haystack, a, b); + assert!(tw.position == b, "cursor moved past the match"); + kani::cover(true, "forward search step: Match"); + } + SearchStep::Reject(a, b) => { + assert!(a == old_pos && a <= b && b <= haystack.len(), "reject window"); + assert!(tw.position == b, "cursor at reject end"); + kani::cover(true, "forward search step: Reject"); + } + SearchStep::Done => unreachable!("RejectAndMatch never yields Done"), + } + assert_two_way_s(&tw, haystack, needle); + } + }; + ($name:ident, bwd, $long:expr) => { + #[kani::proof] + #[kani::unwind(9)] + pub fn $name() { + let hbuf: [u8; HAY_MAX + PAD] = kani::any(); + let nbuf: [u8; NDL_MAX + PAD] = kani::any(); + let haystack = any_utf8(&hbuf); + let needle = any_utf8(&nbuf); + kani::assume(!needle.is_empty()); + let mut tw = any_twoway_search_state(haystack, needle, $long); + let old_end = tw.end; + match tw.next_back::(haystack.as_bytes(), needle.as_bytes(), $long) + { + SearchStep::Match(a, b) => { + assert!( + b == a + needle.len() && b <= haystack.len(), + "match window in bounds" + ); + assert!( + haystack.as_bytes()[a..b] == *needle.as_bytes(), + "match is byte-exact" + ); + assert_valid_range(haystack, a, b); + assert!(tw.end == a, "cursor moved before the match"); + kani::cover(true, "backward search step: Match"); + } + SearchStep::Reject(a, b) => { + assert!(b == old_end && a <= b, "reject window"); + assert!(tw.end == a, "cursor at reject start"); + kani::cover(true, "backward search step: Reject"); + } + SearchStep::Done => unreachable!("RejectAndMatch never yields Done"), + } + assert_two_way_s(&tw, haystack, needle); + } + }; + } + + twoway_search_step!(verify_twoway_search_step_fwd_short, fwd, false); + twoway_search_step!(verify_twoway_search_step_fwd_long, fwd, true); + twoway_search_step!(verify_twoway_search_step_bwd_short, bwd, false); + twoway_search_step!(verify_twoway_search_step_bwd_long, bwd, true); }