diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index ae234e95a491b..a767a83a58406 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -2030,4 +2030,818 @@ 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, symbolic multibyte inputs, base-case harnesses proving the + // constructor establishes the type invariant `C`, from-creation + // harnesses running full call sequences, and inductive-step + // harnesses that admit an arbitrary `C`-satisfying state. + // + // 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. + // ================================================================== + + /// Maximum needle size in bytes: covers needle lengths 1..=3, both + /// short- and long-period factorization branches. + const NEEDLE_BYTES: usize = 3; + + 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) + } + + /// Two-Way invariant `C`. + /// - Clauses 1-4: cursors in-bounds on char boundaries (cursor + /// safety; `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 type_invariant_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 + && haystack.is_char_boundary(tw.position) // 3 + && haystack.is_char_boundary(tw.end) // 4 + && 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 + && nb[..n - tw.period] == nb[tw.period..] + // 11: memorized prefix matches at current alignment + // (only meaningful while a candidate window fits) + && (tw.position + n > h.len() + || h[tw.position..tw.position + tw.memory] == nb[..tw.memory]) + // 11b: memorized suffix matches at the back alignment + && (tw.end < n + || h[tw.end - n + tw.memory_back..tw.end] == nb[tw.memory_back..]) + }) + } + + /// Per-clause assertion version of `type_invariant_two_way`, used by + /// the inductive-step harnesses so a counterexample names the exact + /// clause it violates. + fn assert_two_way_c(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!(haystack.is_char_boundary(tw.position), "c3 position boundary"); + assert!(haystack.is_char_boundary(tw.end), "c4 end boundary"); + 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!(nb[..n - tw.period] == nb[tw.period..], "c10 exact period"); + assert!( + tw.position + n > h.len() + || h[tw.position..tw.position + tw.memory] == nb[..tw.memory], + "c11 memory matches" + ); + assert!( + tw.end < n || h[tw.end - n + tw.memory_back..tw.end] == nb[tw.memory_back..], + "c11b memory_back matches" + ); + } + } + + 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: `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). + #[kani::proof] + #[kani::unwind(10)] + pub fn verify_str_searcher_new() { + let mut hbuf = [0u8; HAYSTACK_BYTES]; + let mut nbuf = [0u8; NEEDLE_BYTES]; + let haystack = symbolic_str(&mut hbuf); + let needle = symbolic_str(&mut 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"); + } + } + } + + /// Haystack bound for the from-creation harnesses. These compose the + /// real `new()` with the real search loops, which is the hardest SAT + /// shape here (the reachable-state constraint threads through the + /// whole maximal_suffix computation); 3 bytes keeps them tractable + /// while still reaching both factorization branches and multibyte + /// haystacks. The load-bearing proofs of the challenge criteria are + /// the base-case + inductive-step harnesses (which cover every + /// C-satisfying state, a superset of the reachable states exercised + /// here); these harnesses add end-to-end coverage of reachable + /// call sequences. + // 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, which + // are safe straight-line loops over `next`/`next_back`; 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`). + fn any_twoway_searcher<'a, 'b>(haystack: &'a str, needle: &'b str) -> 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(), + }; + let s = StrSearcher { haystack, needle, searcher: StrSearcherImpl::TwoWay(tw) }; + kani::assume(type_invariant_str_searcher(&s)); + s + } + + /// Inductive step for the empty-needle variant: from any + /// `C`-satisfying state, each real method returns boundary-valid + /// ranges and preserves `C`. + macro_rules! empty_needle_step { + ($name:ident, $call:ident, step) => { + #[kani::proof] + #[kani::unwind(4)] + pub fn $name() { + let mut hbuf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut 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) + } + SearchStep::Done => {} + } + assert!(type_invariant_str_searcher(&s)); + } + }; + ($name:ident, $call:ident, opt) => { + #[kani::proof] + #[kani::unwind(4)] + pub fn $name() { + let mut hbuf = [0u8; HAYSTACK_BYTES]; + let haystack = symbolic_str(&mut hbuf); + let mut s = any_empty_searcher(haystack); + if let Some((a, b)) = s.$call() { + assert_valid_range(haystack, a, b); + } + 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); + + /// Haystack bound for the Two-Way inductive-step harnesses: these are + /// the most expensive proofs in this module (arbitrary C-state x the + /// full 'search loop); 4 bytes still covers every UTF-8 width class. + const TWOWAY_STEP_BYTES: usize = 4; + + /// Inductive step for the Two-Way variant, for the four single-call + /// methods (`next`, `next_back`, `next_match`, `next_match_back`). + /// The `next_reject`/`next_reject_back` trait defaults are plain + /// loops over `next`/`next_back`, whose single-step preservation of + /// `C` is proven here; inductive variants of the full reject loops + /// are cost-prohibitive for CBMC (>1h each), so those two methods + /// are exercised end-to-end by the from-creation harnesses above + /// instead. + macro_rules! twoway_step { + ($name:ident, $call:ident, step) => { + #[kani::proof] + #[kani::unwind(14)] + pub fn $name() { + let mut hbuf = [0u8; TWOWAY_STEP_BYTES]; + let mut nbuf = [0u8; NEEDLE_BYTES]; + let haystack = symbolic_str(&mut hbuf); + let needle = symbolic_str(&mut nbuf); + kani::assume(!needle.is_empty()); + let mut s = any_twoway_searcher(haystack, needle); + match s.$call() { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + assert_valid_range(haystack, a, b) + } + SearchStep::Done => {} + } + if let StrSearcherImpl::TwoWay(ref tw) = s.searcher { + assert_two_way_c(tw, haystack, needle); + } + assert!(type_invariant_str_searcher(&s)); + } + }; + ($name:ident, $call:ident, opt) => { + #[kani::proof] + #[kani::unwind(14)] + pub fn $name() { + let mut hbuf = [0u8; TWOWAY_STEP_BYTES]; + let mut nbuf = [0u8; NEEDLE_BYTES]; + let haystack = symbolic_str(&mut hbuf); + let needle = symbolic_str(&mut nbuf); + kani::assume(!needle.is_empty()); + let mut s = any_twoway_searcher(haystack, needle); + if let Some((a, b)) = s.$call() { + assert_valid_range(haystack, a, b); + } + if let StrSearcherImpl::TwoWay(ref tw) = s.searcher { + assert_two_way_c(tw, haystack, needle); + } + assert!(type_invariant_str_searcher(&s)); + } + }; + } + + twoway_step!(verify_twoway_step_next, next, step); + twoway_step!(verify_twoway_step_next_back, next_back, step); + twoway_step!(verify_twoway_step_next_match, next_match, opt); + twoway_step!(verify_twoway_step_next_match_back, next_match_back, opt); }