diff --git a/library/core/src/str/iter.rs b/library/core/src/str/iter.rs index 34e2ab79b9d34..130304ebcd9d2 100644 --- a/library/core/src/str/iter.rs +++ b/library/core/src/str/iter.rs @@ -1613,3 +1613,900 @@ macro_rules! escape_types_impls { } escape_types_impls!(EscapeDebug, EscapeDefault, EscapeUnicode); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use super::super::pattern::verify::{ + PAD, any_char_searcher, any_utf8, cs_finger, cs_finger_back, cs_needle, type_invariant_cs, + utf8_local, + }; + use super::super::validations::{utf8_char_width, utf8_is_cont_byte}; + use super::*; + + // ================================================================= + // Challenge 22: verify safety of str iter functions. + // + // Every harness runs the real, unmodified iterator code; no product + // code path is compiled out under Kani. The proofs are unbounded in + // the two dimensions the challenge cares about: + // + // - String length. The haystack is a symbolic-length slice of an + // arbitrary byte array constrained to valid UTF-8 by a loop-free + // byte-table predicate (`pattern::verify::any_utf8`); every valid + // UTF-8 string of at most HAY_MAX bytes — contents, length and + // character widths all symbolic — is one input. HAY_MAX is the + // size of the symbolic backing allocation, a CBMC memory-model + // parameter (as `ARR_SIZE` in + // `str::validations::verify::check_run_utf8_validation` and + // `HAY_MAX` in `str::pattern::verify`); no loop is unwound to it. + // - Iterator state. Following the Challenge 20 methodology, each + // iterator type has a type invariant `C`; a base-case harness + // shows the constructors establish `C`, and every method harness + // starts from an *arbitrary* `C`-satisfying state (a superset of + // the states any call sequence reaches), runs the method, asserts + // the safety facts the unsafe blocks rely on (`str::get_unchecked` + // only checks bounds, so char-boundary-ness of every produced + // index and slice is asserted explicitly) and re-asserts `C`. + // + // The pattern searchers. The `SplitInternal`/`MatchesInternal`/ + // `MatchIndicesInternal` bodies contain no loops; every loop they can + // reach is inside `CharSearcher::next_match`/`next_match_back` + // (`str::pattern`). Challenge 22 assumption 2 allows assuming the + // safety and functional correctness of everything in `pattern.rs`; + // these harnesses assume strictly less than that: the two methods are + // replaced (`#[kani::stub_verified]`) by their *function contract*, + // which is the `Searcher` trait's documented guarantee (indices on + // char boundaries) plus the struct's documented finger invariant, is + // attached to the real, byte-identical method bodies, and is checked + // against those bodies by `pattern::verify::verify_cs_next_match`/ + // `verify_cs_next_match_back` (`#[kani::proof_for_contract]`). Under + // `stub_verified` each call site asserts the contract's precondition + // (`C` for the searcher) and assumes its postcondition; nothing about + // boundaries is `kani::assume`d by these harnesses. Lifting the + // searcher loops themselves with loop contracts is not possible with + // the pinned Kani: the slice comparison inside them lowers to CBMC's + // builtin `memcmp`, whose locals fail the loop-contract assigns check, + // and neither the `compare_bytes` intrinsic ("invalid stub: function + // does not have a body") nor `<[u8] as PartialEq>::eq` ("unable to + // find implementation ... for [u8]") can be stubbed around it. The + // contract proofs in `pattern::verify` therefore keep Challenge 20's + // bounded haystack; that bound is the one accepted limitation of + // this suite and it lives entirely inside Challenge 20's scope. + // + // `Chars::advance_by` is the only target function with loops. Its + // harness is unbounded in string length and bounded only in the + // advance count `n` (`ADVANCE_MAX`); every unwind bound derives from + // `ADVANCE_MAX` and the constant chunk size, never from the string + // length. See `check_chars_advance_by` for why loop contracts cannot + // be applied to those loops with the pinned Kani. + // + // Harness-writing rules (both consequences of CI's `-Z loop-contracts`): + // never filter inputs through `from_utf8` (its loop invariants make + // the result unreliable), and never reach a `#[safety::loop_invariant]` + // (`from_utf8`, `is_ascii`, `chars().count()`, ...) from a harness, + // which silently switches it into loop-contract mode. Equality of + // string slices is checked by pointer and length (`same_str`) rather + // than `==`, which lowers to `memcmp` over the whole slice. + // ================================================================= + + /// Maximum haystack length in bytes: the size of the symbolic backing + /// allocation, not a loop bound (see the module comment). Haystack + /// lengths range over `0..=HAY_MAX`; 256 keeps every harness within + /// a few minutes under CI's flags (at 1000 the loop-free harnesses + /// take about 2 minutes each run alone, ~11x the time at 256, and + /// `check_chars_advance_by` did not finish within an hour). + // TODO: HAY_MAX can be much larger with cbmc argument `--arrays-uf-always` + const HAY_MAX: usize = 256; + /// Size of the backing array behind a `HAY_MAX`-byte haystack. + const HAY_ARR: usize = HAY_MAX + PAD; + + /// An arbitrary haystack: a valid UTF-8 string of symbolic length + /// `0..=N - PAD` (contents, length and character widths symbolic), + /// via the byte-table input model shared with `str::pattern::verify` + /// (`utf8_local`/`any_utf8`; see there for why `from_utf8` cannot be + /// the filter). + fn any_haystack(arr: &[u8; N]) -> &str { + let s = any_utf8(arr); + kani::cover(s.len() == N - PAD, "a haystack of the maximum length"); + s + } + + /// Identity of two string slices (same address and length). Used + /// instead of `==`, which lowers to `memcmp` over the whole slice. + fn same_str(a: &str, b: &str) -> bool { + a.as_ptr() == b.as_ptr() && a.len() == b.len() + } + + /// Byte offset of `sub` inside `s`; `sub` must be a subslice of `s`. + fn offset_in(s: &str, sub: &str) -> usize { + sub.as_ptr().addr() - s.as_ptr().addr() + } + + /// An arbitrary in-bounds char-boundary window `k..m` of `s`. + fn any_window(s: &str) -> (usize, usize) { + let k: usize = kani::any(); + let m: usize = kani::any(); + kani::assume(k <= m && m <= s.len()); + kani::assume(s.is_char_boundary(k) && s.is_char_boundary(m)); + (k, m) + } + + /// The window `k..m` of `s` as returned by `any_window`. + fn window(s: &str, k: usize, m: usize) -> &str { + // SAFETY: `any_window` assumed `k <= m <= s.len()` and that both + // are char boundaries. + unsafe { s.get_unchecked(k..m) } + } + + // ------------------------------------------------------------------ + // Chars + // + // Type invariant: the iterator's bytes are a char-boundary window of + // a valid UTF-8 string (the `str` invariant `Chars` documents). Every + // state reachable by `next`/`next_back`/`advance_by` from `s.chars()` + // is such a window, and every window is reachable as + // `s[k..m].chars()`, so the harnesses start from an arbitrary window. + // ------------------------------------------------------------------ + + /// `Chars::next`: the real `next_code_point` (whose + /// `char::from_u32_unchecked` result Kani checks for validity) on an + /// arbitrary window; the consumed prefix is one whole character. + #[kani::proof] + pub fn check_chars_next() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let w = window(s, k, m); + let mut it = w.chars(); + match it.next() { + Some(c) => { + let rest = it.as_str(); + assert!(rest.len() + c.len_utf8() == w.len()); + assert!(offset_in(s, rest) == k + c.len_utf8()); + assert!(s.is_char_boundary(k + c.len_utf8())); + kani::cover(c.len_utf8() == 1, "1-byte char consumed"); + kani::cover(c.len_utf8() == 2, "2-byte char consumed"); + kani::cover(c.len_utf8() == 3, "3-byte char consumed"); + kani::cover(c.len_utf8() == 4, "4-byte char consumed"); + } + None => { + assert!(w.is_empty()); + kani::cover(true, "empty window"); + } + } + } + + /// `Chars::next_back`: the real `next_code_point_reverse` on an + /// arbitrary window; the consumed suffix is one whole character. + #[kani::proof] + pub fn check_chars_next_back() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let w = window(s, k, m); + let mut it = w.chars(); + match it.next_back() { + Some(c) => { + let rest = it.as_str(); + assert!(rest.len() + c.len_utf8() == w.len()); + assert!(offset_in(s, rest) == k); + assert!(s.is_char_boundary(m - c.len_utf8())); + kani::cover(c.len_utf8() == 1, "1-byte char consumed"); + kani::cover(c.len_utf8() == 2, "2-byte char consumed"); + kani::cover(c.len_utf8() == 3, "3-byte char consumed"); + kani::cover(c.len_utf8() == 4, "4-byte char consumed"); + } + None => { + assert!(w.is_empty()); + kani::cover(true, "empty window"); + } + } + } + + /// `Chars::as_str` (`from_utf8_unchecked` over the iterator's bytes) + /// on an arbitrary window, and again after consuming from both ends. + #[kani::proof] + pub fn check_chars_as_str() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let w = window(s, k, m); + let mut it = w.chars(); + assert!(same_str(it.as_str(), w)); + let front = it.next().map_or(0, char::len_utf8); + let back = it.next_back().map_or(0, char::len_utf8); + let rest = it.as_str(); + assert!(offset_in(s, rest) == k + front); + assert!(rest.len() + front + back == w.len()); + assert!(s.is_char_boundary(k + front) && s.is_char_boundary(m - back)); + kani::cover(front > 0 && back > 0, "consumed from both ends"); + } + + /// Advance-count bound of `check_chars_advance_by`, the per-character + /// path of `Chars::advance_by` (counts below `CHUNK_SIZE` never enter + /// the chunk-skip phase). + const ADVANCE_MAX: usize = 8; + /// Backing-array size of `check_chars_advance_by`. Its per-character + /// loop is unwound, so unlike the loop-free harnesses its memory use + /// grows with the array (measured peak RSS: 4.8 GB at HAY_MAX, 1.8 GB + /// at 128); 128 keeps it inside the budget of CI's macOS runners. + /// Like HAY_MAX it is the size of the symbolic backing allocation, + /// not a loop bound. + const ADVANCE_HAY_MAX: usize = 128; + const ADVANCE_ARR: usize = ADVANCE_HAY_MAX + PAD; + /// Advance-count range of `check_chars_advance_by_chunked`, the + /// chunk-skip path: at least 33 so the chunk-skip loop body runs (it + /// runs while more than 32 characters remain to be skipped and a full + /// 32-byte chunk is available), at most 40 so it runs exactly once (a + /// 32-byte chunk of valid UTF-8 holds at least 8 characters, so + /// afterwards at most 32 remain and the guard fails). + const CHUNKED_MIN: usize = 33; + const CHUNKED_MAX: usize = 40; + /// String length of `check_chars_advance_by_chunked`: one full 32-byte + /// chunk plus a 16-byte tail. The length is a compile-time constant + /// (the contents are fully symbolic) because CBMC only drops the + /// unrolled copies of the chunk-skip loop when the chunk iterator's + /// end is known at unwinding time: each copy of that loop body reads + /// a whole chunk at a symbolic offset and runs two 32-iteration + /// loops, and with a symbolic string length -- or a symbolic start of + /// a fixed-length window -- the 33 copies the unwind bound implies + /// exceed 11 GB of RSS (measured). So the chunk-skip path is verified for every + /// 48-byte string; the per-character path (`check_chars_advance_by`) + /// for arbitrary windows of strings of arbitrary length. + const CHUNKED_WINDOW: usize = 48; + const _: () = assert!(ADVANCE_MAX <= WALK_MAX && CHUNKED_MAX <= WALK_MAX); + /// Number of unrolled steps in `walk`. + const WALK_MAX: usize = 40; + + /// Reference for `advance_by`: the position reached by skipping up to + /// `n <= WALK_MAX` characters from `off` (never past `m`) and the + /// number of characters skipped. Loop-free: `WALK_MAX` unrolled + /// conditional `utf8_char_width` steps, so it adds nothing to the + /// harness's unwind bound. + fn walk(bytes: &[u8], off: usize, m: usize, n: usize) -> (usize, usize) { + let mut off = off; + let mut steps = 0; + macro_rules! step { + () => { + if steps < n && off < m { + off += utf8_char_width(bytes[off]); + steps += 1; + } + }; + } + macro_rules! steps8 { + () => { + step!(); + step!(); + step!(); + step!(); + step!(); + step!(); + step!(); + step!(); + }; + } + // WALK_MAX = 5 * 8 steps + steps8!(); + steps8!(); + steps8!(); + steps8!(); + steps8!(); + (off, steps) + } + + /// Shared body of the two `advance_by` harnesses: the real + /// `Chars::advance_by` on the window `k..m` of `s` for the advance + /// count `n`, checked against `walk`. The remainder must start exactly + /// where the walk ends (and so on a char boundary); `Ok` iff `n` + /// characters were available, otherwise `Err(n - characters)`. + fn check_advance_by(s: &str, k: usize, m: usize, n: usize) -> (usize, usize) { + let bytes = s.as_bytes(); + let (off, steps) = walk(bytes, k, m, n); + + let mut it = window(s, k, m).chars(); + let res = it.advance_by(n); + let rest = it.as_str(); + assert!(offset_in(s, rest) == off); + assert!(rest.len() == m - off); + assert!(s.is_char_boundary(off)); + match res { + Ok(()) => { + assert!(steps == n); + kani::cover(n > 0, "advanced by a nonzero count"); + } + Err(rem) => { + assert!(off == m); + assert!(rem.get() == n - steps); + kani::cover(true, "ran out of characters"); + } + } + (off, steps) + } + + /// `Chars::advance_by`, per-character path: the real per-character + /// loop on an arbitrary window of a string of arbitrary length, for + /// counts up to `ADVANCE_MAX`. The unwind bound follows from + /// `ADVANCE_MAX` alone (the loop decrements `remainder` each + /// iteration); the string length plays no part in it. + /// + /// Loop contracts are not used on `advance_by`'s loops because, with + /// the pinned Kani, the invariant of a loop that advances a + /// `slice::Iter` through a method call cannot be stated: loop-modifies + /// inference misses fields written by callees (Kani reference, loop + /// contracts, limitations), and after the iterator is havocked its + /// `len()`/`as_slice()` trip the same-allocation check in Kani's + /// `ptr_offset_from` model before an invariant could re-pin it. + #[kani::proof] + #[kani::unwind(9)] + pub fn check_chars_advance_by() { + let arr: [u8; ADVANCE_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let n: usize = kani::any(); + kani::assume(n <= ADVANCE_MAX); + let (off, _) = check_advance_by(s, k, m, n); + kani::cover(n > 0 && off - k == 4 * n, "skipped only 4-byte characters"); + } + + /// `Chars::advance_by`, chunk-skip path: the real chunk-skip loop (its + /// body runs exactly once for these counts, see `CHUNKED_MAX`), the + /// trailing-continuation loop and the per-character loop, on a + /// `CHUNKED_WINDOW`-byte string of arbitrary contents. The unwind + /// bound is 34: the two loops over a chunk run 32 times, the + /// per-character loop at most 16 times (the bytes left after the + /// chunk), the trailing-continuation loop at most 3 (a character has + /// at most 3 continuation bytes); CBMC's unwinding assertions check + /// these counts rather than assume them. + #[kani::proof] + #[kani::unwind(34)] + pub fn check_chars_advance_by_chunked() { + let arr: [u8; CHUNKED_WINDOW + PAD] = kani::any(); + kani::assume(utf8_local(&arr, CHUNKED_WINDOW)); + // SAFETY: `utf8_local` is the byte-table definition of UTF-8 + // validity of `arr[..CHUNKED_WINDOW]` (see `pattern::verify`). + let s = unsafe { from_utf8_unchecked(&arr[..CHUNKED_WINDOW]) }; + let bytes = s.as_bytes(); + let n: usize = kani::any(); + kani::assume(CHUNKED_MIN <= n && n <= CHUNKED_MAX); + check_advance_by(s, 0, CHUNKED_WINDOW, n); + kani::cover( + utf8_is_cont_byte(bytes[32]), + "trailing-continuation loop skipped a byte after the chunk", + ); + kani::cover( + bytes[0] >= 0xF0 + && bytes[4] >= 0xF0 + && bytes[8] >= 0xF0 + && bytes[12] >= 0xF0 + && bytes[16] >= 0xF0 + && bytes[20] >= 0xF0 + && bytes[24] >= 0xF0 + && bytes[28] >= 0xF0, + "chunk of eight 4-byte characters (the fewest a chunk can hold)", + ); + kani::cover(bytes[0] < 0x80 && bytes[31] < 0x80, "chunk starting and ending in ASCII"); + } + + // ------------------------------------------------------------------ + // SplitInternal<'_, char> + // + // Type invariant `C`: the searcher satisfies its own invariant, the + // unconsumed range `start..end` is a char-boundary range of the + // haystack, and the searcher's fingers lie within it + // (`start <= finger` and `finger_back <= end`). The constructors + // establish it (`check_split_constructors_establish_invariant`); every + // reachable state in fact has `start == finger`, and `finger_back == + // end` except after `next_back_inclusive` (which leaves `end` at the + // match end while `finger_back` is at its start), so the arbitrary + // `C`-states below are a superset of the reachable ones. + // ------------------------------------------------------------------ + + /// Type invariant `C` of `SplitInternal<'_, char>`. + fn split_invariant(it: &SplitInternal<'_, char>) -> bool { + let h = it.matcher.haystack(); + type_invariant_cs(&it.matcher) + && it.start <= cs_finger(&it.matcher) + && cs_finger_back(&it.matcher) <= it.end + && it.end <= h.len() + && h.is_char_boundary(it.start) + && h.is_char_boundary(it.end) + } + + /// An arbitrary `C`-satisfying `SplitInternal` over `s` with a + /// symbolic `char` pattern and symbolic flags. + fn any_split(s: &str) -> SplitInternal<'_, char> { + let it = SplitInternal { + start: kani::any(), + end: kani::any(), + matcher: any_char_searcher(s), + allow_trailing_empty: kani::any(), + finished: kani::any(), + }; + kani::assume(split_invariant(&it)); + it + } + + /// Snapshot of the parts of a `SplitInternal` state that a method must + /// leave alone, checked after the call. + struct SplitFrame { + start: usize, + end: usize, + finger: usize, + finger_back: usize, + needle: char, + } + + fn split_frame(it: &SplitInternal<'_, char>) -> SplitFrame { + SplitFrame { + start: it.start, + end: it.end, + finger: cs_finger(&it.matcher), + finger_back: cs_finger_back(&it.matcher), + needle: cs_needle(&it.matcher), + } + } + + /// `part` is the char-boundary range `lo..hi` of `s` (by address). + fn assert_is_range(s: &str, part: &str, lo: usize, hi: usize) { + assert!(offset_in(s, part) == lo); + assert!(lo + part.len() == hi); + assert!(hi <= s.len()); + assert!(s.is_char_boundary(lo) && s.is_char_boundary(hi)); + } + + /// Criterion 1: `split`, `split_terminator` and `split_inclusive` + /// establish `C`. + #[kani::proof] + pub fn check_split_constructors_establish_invariant() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let p: char = kani::any(); + let a = s.split(p).0; + assert!(split_invariant(&a) && a.start == 0 && a.end == s.len() && !a.finished); + let b = s.split_terminator(p).0; + assert!(split_invariant(&b) && b.start == 0 && b.end == s.len() && !b.finished); + let c = s.split_inclusive(p).0; + assert!(split_invariant(&c) && c.start == 0 && c.end == s.len() && !c.finished); + } + + /// `SplitInternal::next` from an arbitrary `C`-state: the fragment is + /// `start..a` for the match `a..b` the searcher contract returns, the + /// new `start` is `b`, and on exhaustion `get_end` yields + /// `start..end` at most once. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match)] + pub fn check_split_next() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + match it.next() { + Some(part) => { + assert!(!finished); + if it.finished { + assert_is_range(s, part, f.start, f.end); + assert!(it.start == f.start); + kani::cover(true, "next: trailing fragment from get_end"); + } else { + let a = f.start + part.len(); + assert_is_range(s, part, f.start, a); + assert!(a >= f.finger); + assert!(it.start == a + f.needle.len_utf8()); + assert!(it.start == cs_finger(&it.matcher)); + kani::cover(part.is_empty(), "next: empty fragment between adjacent matches"); + kani::cover(!part.is_empty(), "next: nonempty fragment"); + } + } + None => { + assert!(it.finished); + kani::cover(finished, "next: already finished"); + kani::cover(!finished, "next: exhausted without a trailing fragment"); + } + } + assert!(split_invariant(&it)); + assert!(it.end == f.end); + assert!(cs_finger_back(&it.matcher) == f.finger_back); + assert!(cs_needle(&it.matcher) == f.needle); + assert!(same_str(it.matcher.haystack(), s)); + } + + /// `SplitInternal::next_inclusive` from an arbitrary `C`-state: the + /// fragment is `start..b` and the new `start` is `b`. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match)] + pub fn check_split_next_inclusive() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + match it.next_inclusive() { + Some(part) => { + assert!(!finished); + if it.finished { + assert_is_range(s, part, f.start, f.end); + assert!(it.start == f.start); + kani::cover(true, "next_inclusive: trailing fragment from get_end"); + } else { + let b = f.start + part.len(); + assert_is_range(s, part, f.start, b); + assert!(part.len() >= f.needle.len_utf8()); + assert!(it.start == b); + assert!(it.start == cs_finger(&it.matcher)); + kani::cover( + part.len() == f.needle.len_utf8(), + "next_inclusive: fragment is just the separator", + ); + kani::cover( + part.len() > f.needle.len_utf8(), + "next_inclusive: fragment with content before the separator", + ); + } + } + None => { + assert!(it.finished); + kani::cover(finished, "next_inclusive: already finished"); + kani::cover(!finished, "next_inclusive: exhausted without a trailing fragment"); + } + } + assert!(split_invariant(&it)); + assert!(it.end == f.end); + assert!(cs_finger_back(&it.matcher) == f.finger_back); + assert!(cs_needle(&it.matcher) == f.needle); + assert!(same_str(it.matcher.haystack(), s)); + } + + /// `SplitInternal::next_back` from an arbitrary `C`-state, including + /// the `allow_trailing_empty == false` path that first calls itself + /// to drop an empty trailing fragment: every fragment is a + /// char-boundary sub-range of the unconsumed range, `end` only + /// decreases, and `start` is untouched. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match_back)] + pub fn check_split_next_back() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + let trailing = it.allow_trailing_empty; + match it.next_back() { + Some(part) => { + assert!(!finished); + let lo = offset_in(s, part); + let hi = lo + part.len(); + assert!(f.start <= lo && hi <= f.end); + assert!(s.is_char_boundary(lo) && s.is_char_boundary(hi)); + if it.finished { + // the final fragment `start..end` (of the range as it + // was when the searcher ran out of matches) + assert!(lo == f.start); + kani::cover(true, "next_back: final fragment"); + } else { + // `b..end` for a match `a..b` at or after `finger`; + // `end` becomes `a` + assert!(lo > f.finger); + assert!(it.end == cs_finger_back(&it.matcher)); + assert!(it.end + f.needle.len_utf8() == lo); + kani::cover(part.is_empty(), "next_back: empty fragment"); + kani::cover(!part.is_empty(), "next_back: nonempty fragment"); + } + kani::cover( + !trailing && !part.is_empty(), + "next_back: fragment returned with allow_trailing_empty == false", + ); + } + None => { + assert!(it.finished); + kani::cover(finished, "next_back: already finished"); + kani::cover( + !finished && !trailing, + "next_back: only an empty trailing fragment remained", + ); + } + } + assert!(split_invariant(&it)); + assert!(it.start == f.start); + assert!(it.end <= f.end); + assert!(cs_finger(&it.matcher) == f.finger); + assert!(cs_needle(&it.matcher) == f.needle); + assert!(same_str(it.matcher.haystack(), s)); + } + + /// `SplitInternal::next_back_inclusive` from an arbitrary `C`-state: + /// as `next_back`, but `end` becomes the match end `b` (so + /// `finger_back < end` afterwards, which `C` allows). + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match_back)] + pub fn check_split_next_back_inclusive() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + let trailing = it.allow_trailing_empty; + match it.next_back_inclusive() { + Some(part) => { + assert!(!finished); + let lo = offset_in(s, part); + let hi = lo + part.len(); + assert!(f.start <= lo && hi <= f.end); + assert!(s.is_char_boundary(lo) && s.is_char_boundary(hi)); + if it.finished { + assert!(lo == f.start); + kani::cover(true, "next_back_inclusive: final fragment"); + } else { + assert!(it.end == lo); + assert!(cs_finger_back(&it.matcher) + f.needle.len_utf8() == lo); + kani::cover(part.is_empty(), "next_back_inclusive: empty fragment"); + kani::cover(!part.is_empty(), "next_back_inclusive: nonempty fragment"); + } + kani::cover( + !trailing && !part.is_empty(), + "next_back_inclusive: fragment returned with allow_trailing_empty == false", + ); + } + None => { + assert!(it.finished); + kani::cover(finished, "next_back_inclusive: already finished"); + kani::cover( + !finished && !trailing, + "next_back_inclusive: only an empty trailing fragment remained", + ); + } + } + assert!(split_invariant(&it)); + assert!(it.start == f.start); + assert!(it.end <= f.end); + assert!(cs_finger(&it.matcher) == f.finger); + assert!(cs_needle(&it.matcher) == f.needle); + assert!(same_str(it.matcher.haystack(), s)); + } + + /// `SplitInternal::get_end` from an arbitrary `C`-state, called + /// directly: on an unfinished iterator it finishes it and returns + /// `start..end` iff a trailing empty fragment is allowed or the range + /// is nonempty; on a finished one it is a no-op returning `None`. + #[kani::proof] + pub fn check_split_get_end() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = any_split(s); + let f = split_frame(&it); + let finished = it.finished; + let trailing = it.allow_trailing_empty; + let res = it.get_end(); + assert!(it.finished); + match res { + Some(part) => { + assert!(!finished); + assert!(trailing || f.end > f.start); + assert_is_range(s, part, f.start, f.end); + kani::cover( + trailing && part.is_empty(), + "get_end: empty trailing fragment allowed", + ); + kani::cover( + !trailing && !part.is_empty(), + "get_end: nonempty fragment, trailing empty disallowed", + ); + } + None => { + assert!(finished || (!trailing && f.end == f.start)); + kani::cover(finished, "get_end: already finished"); + kani::cover(!finished, "get_end: empty trailing fragment suppressed"); + } + } + assert!(split_invariant(&it)); + assert!(it.start == f.start && it.end == f.end); + assert!(cs_finger(&it.matcher) == f.finger && cs_finger_back(&it.matcher) == f.finger_back); + } + + /// `SplitInternal::remainder` from an arbitrary `C`-state: `None` iff + /// finished, else `start..end`; the state is untouched. + #[kani::proof] + pub fn check_split_remainder() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let it = any_split(s); + let f = split_frame(&it); + match it.remainder() { + Some(rem) => { + assert!(!it.finished); + assert_is_range(s, rem, f.start, f.end); + kani::cover(rem.is_empty(), "remainder: empty"); + kani::cover(!rem.is_empty(), "remainder: nonempty"); + } + None => { + assert!(it.finished); + kani::cover(true, "remainder: finished"); + } + } + assert!(split_invariant(&it)); + assert!(it.start == f.start && it.end == f.end); + } + + // ------------------------------------------------------------------ + // MatchIndicesInternal / MatchesInternal + // + // Type invariant: the wrapped searcher satisfies its own invariant + // (nothing else is stored). Arbitrary `C`-states are produced by + // `any_char_searcher`. + // ------------------------------------------------------------------ + + /// `MatchIndicesInternal::next`: the returned index is the match + /// start, a char boundary, and the slice is the match. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match)] + pub fn check_match_indices_next() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it: MatchIndicesInternal<'_, char> = MatchIndicesInternal(any_char_searcher(s)); + let (finger, finger_back, needle) = + (cs_finger(&it.0), cs_finger_back(&it.0), cs_needle(&it.0)); + match it.next() { + Some((i, m)) => { + assert!(finger <= i); + assert_is_range(s, m, i, i + needle.len_utf8()); + assert!(i + m.len() <= finger_back); + assert!(cs_finger(&it.0) == i + m.len()); + kani::cover(m.len() > 1, "match_indices next: multibyte match"); + kani::cover(i > 0, "match_indices next: match after the start"); + } + None => { + assert!(cs_finger(&it.0) == finger_back); + kani::cover(true, "match_indices next: no match"); + } + } + assert!(type_invariant_cs(&it.0)); + assert!(cs_finger_back(&it.0) == finger_back && cs_needle(&it.0) == needle); + assert!(same_str(it.0.haystack(), s)); + } + + /// `MatchIndicesInternal::next_back`: as `next`, searching backwards. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match_back)] + pub fn check_match_indices_next_back() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it: MatchIndicesInternal<'_, char> = MatchIndicesInternal(any_char_searcher(s)); + let (finger, finger_back, needle) = + (cs_finger(&it.0), cs_finger_back(&it.0), cs_needle(&it.0)); + match it.next_back() { + Some((i, m)) => { + assert!(finger <= i); + assert_is_range(s, m, i, i + needle.len_utf8()); + assert!(i + m.len() <= finger_back); + assert!(cs_finger_back(&it.0) == i); + kani::cover(m.len() > 1, "match_indices next_back: multibyte match"); + kani::cover( + i + m.len() < finger_back, + "match_indices next_back: match before the end", + ); + } + None => { + assert!(cs_finger_back(&it.0) == finger); + kani::cover(true, "match_indices next_back: no match"); + } + } + assert!(type_invariant_cs(&it.0)); + assert!(cs_finger(&it.0) == finger && cs_needle(&it.0) == needle); + assert!(same_str(it.0.haystack(), s)); + } + + /// `MatchesInternal::next`: the returned slice is the match. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match)] + pub fn check_matches_next() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it: MatchesInternal<'_, char> = MatchesInternal(any_char_searcher(s)); + let (finger, finger_back, needle) = + (cs_finger(&it.0), cs_finger_back(&it.0), cs_needle(&it.0)); + match it.next() { + Some(m) => { + let i = offset_in(s, m); + assert!(finger <= i); + assert_is_range(s, m, i, i + needle.len_utf8()); + assert!(i + m.len() <= finger_back); + assert!(cs_finger(&it.0) == i + m.len()); + kani::cover(m.len() > 1, "matches next: multibyte match"); + } + None => { + assert!(cs_finger(&it.0) == finger_back); + kani::cover(true, "matches next: no match"); + } + } + assert!(type_invariant_cs(&it.0)); + assert!(cs_finger_back(&it.0) == finger_back && cs_needle(&it.0) == needle); + assert!(same_str(it.0.haystack(), s)); + } + + /// `MatchesInternal::next_back`: as `next`, searching backwards. + #[kani::proof] + #[kani::stub_verified(crate::str::pattern::CharSearcher::next_match_back)] + pub fn check_matches_next_back() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it: MatchesInternal<'_, char> = MatchesInternal(any_char_searcher(s)); + let (finger, finger_back, needle) = + (cs_finger(&it.0), cs_finger_back(&it.0), cs_needle(&it.0)); + match it.next_back() { + Some(m) => { + let i = offset_in(s, m); + assert!(finger <= i); + assert_is_range(s, m, i, i + needle.len_utf8()); + assert!(i + m.len() <= finger_back); + assert!(cs_finger_back(&it.0) == i); + kani::cover(m.len() > 1, "matches next_back: multibyte match"); + } + None => { + assert!(cs_finger_back(&it.0) == finger); + kani::cover(true, "matches next_back: no match"); + } + } + assert!(type_invariant_cs(&it.0)); + assert!(cs_finger(&it.0) == finger && cs_needle(&it.0) == needle); + assert!(same_str(it.0.haystack(), s)); + } + + // ------------------------------------------------------------------ + // SplitAsciiWhitespace + // + // Type invariant: the inner `slice::Split`'s unconsumed slice `v` is a + // char-boundary window of the string. `split_ascii_whitespace` + // starts with the whole string; each `next` (`next_back`) cuts `v` + // after (before) an ASCII-whitespace byte, which is a one-byte + // character, so every reachable `v` is such a window, and every + // window is one `C`-state. + // ------------------------------------------------------------------ + + /// `SplitAsciiWhitespace::remainder` (`from_utf8_unchecked` over `v`) + /// on the fresh iterator and on an arbitrary `C`-state. + #[kani::proof] + pub fn check_split_ascii_whitespace_remainder() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let mut it = s.split_ascii_whitespace(); + assert!(it.remainder().is_some_and(|rem| same_str(rem, s))); + let (k, m) = any_window(s); + it.inner.iter.iter.v = window(s, k, m).as_bytes(); + it.inner.iter.iter.finished = kani::any(); + match it.remainder() { + Some(rem) => { + assert!(!it.inner.iter.iter.finished); + assert_is_range(s, rem, k, m); + kani::cover(!rem.is_empty(), "split_ascii_whitespace remainder: nonempty"); + } + None => { + assert!(it.inner.iter.iter.finished); + kani::cover(true, "split_ascii_whitespace remainder: finished"); + } + } + } + + // ------------------------------------------------------------------ + // Bytes + // ------------------------------------------------------------------ + + /// Contract harness for `Bytes::__iterator_get_unchecked`: its + /// `#[requires(idx < self.0.len())]` rules out UB in the body, for a + /// `Bytes` over any window of a string of arbitrary length. Under + /// CI's `--no-assert-contracts` a contract is only checked by a + /// `proof_for_contract` harness. + #[kani::proof_for_contract(Bytes::__iterator_get_unchecked)] + pub fn check_bytes_iterator_get_unchecked() { + let arr: [u8; HAY_ARR] = kani::any(); + let s = any_haystack(&arr); + let (k, m) = any_window(s); + let w = window(s, k, m); + let mut bytes = w.bytes(); + let idx: usize = kani::any(); + let b = unsafe { bytes.__iterator_get_unchecked(idx) }; + assert!(b == w.as_bytes()[idx]); + kani::cover(idx > 0, "bytes get_unchecked: index past the start"); + } +} diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index ae234e95a491b..515cb00628960 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -39,7 +39,8 @@ )] #[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] -use safety::{loop_invariant, requires}; +use safety::loop_invariant; +use safety::{ensures, requires}; use crate::cmp::Ordering; use crate::convert::TryInto as _; @@ -434,6 +435,30 @@ unsafe impl<'a> Searcher<'a> for CharSearcher<'a> { } } #[inline] + // Kani contract (a runtime no-op). `requires` restates the safety + // invariant documented on `CharSearcher`: both fingers are in-bounds + // char boundaries of the haystack (`into_searcher` establishes it and + // every method preserves it; see `verify`). `ensures` restates the + // `Searcher` guarantee this method gives its callers: a returned + // range is a needle-width range on char boundaries, at or after the + // finger on entry and within `finger_back`, and `finger` is left at + // its end; `None` leaves `finger` at `finger_back`. Only `finger` is + // written. Checked against this body by `verify::verify_cs_next_match`. + #[requires(self.finger <= self.finger_back + && self.finger_back <= self.haystack.len() + && self.haystack.is_char_boundary(self.finger) + && self.haystack.is_char_boundary(self.finger_back))] + #[ensures(|result| match *result { + Some((a, b)) => old(self.finger) <= a + && a < b + && b == self.finger + && b <= self.finger_back + && b - a == self.utf8_size() + && self.haystack.is_char_boundary(a) + && self.haystack.is_char_boundary(b), + None => self.finger == self.finger_back, + })] + #[cfg_attr(kani, kani::modifies(&self.finger))] fn next_match(&mut self) -> Option<(usize, usize)> { loop { // get the haystack after the last character found @@ -501,6 +526,26 @@ unsafe impl<'a> ReverseSearcher<'a> for CharSearcher<'a> { } } #[inline] + // Kani contract (a runtime no-op); see `next_match`. A returned range + // is a needle-width range on char boundaries, at or before the + // `finger_back` on entry and at or after `finger`, and `finger_back` + // is left at its start; `None` leaves `finger_back` at `finger`. Only + // `finger_back` is written. Checked by `verify::verify_cs_next_match_back`. + #[requires(self.finger <= self.finger_back + && self.finger_back <= self.haystack.len() + && self.haystack.is_char_boundary(self.finger) + && self.haystack.is_char_boundary(self.finger_back))] + #[ensures(|result| match *result { + Some((a, b)) => a == self.finger_back + && a < b + && b - a == self.utf8_size() + && b <= old(self.finger_back) + && self.finger <= a + && self.haystack.is_char_boundary(a) + && self.haystack.is_char_boundary(b), + None => self.finger_back == self.finger, + })] + #[cfg_attr(kani, kani::modifies(&self.finger_back))] fn next_match_back(&mut self) -> Option<(usize, usize)> { let haystack = self.haystack.as_bytes(); loop { @@ -2030,4 +2075,1302 @@ 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`). + // + // Accepted limitation: bounded haystack length. + // + // The challenge asks for proofs over haystacks of arbitrary size. + // These proofs are bounded in exactly one dimension: the haystack is + // at most `HAYSTACK_BYTES` bytes long, and every harness that runs a + // search loop carries the matching `#[kani::unwind]` bound. Within + // that bound the proofs are exhaustive: + // - every haystack: contents and length are symbolic, so every + // valid UTF-8 string of at most HAYSTACK_BYTES bytes, with every + // combination of the four UTF-8 width classes that fits, is one + // symbolic input; + // - every needle: an arbitrary `char` (`CharSearcher`) or + // `[char; 2]` (`MultiCharEqSearcher` and the wrappers); + // - every searcher state: the inductive-step harnesses start from + // an arbitrary `C`-satisfying state, a superset of the states any + // call sequence reaches, so they are unbounded in the number of + // calls made before the one under verification. + // + // Why HAYSTACK_BYTES = 5. A 4-byte (maximum-width) character plus one + // neighbour is the smallest haystack in which every case the search + // loops distinguish is reachable: every needle width; a memchr hit on + // a continuation byte that is *not* the end of the needle, which + // leaves `finger` mid-character for the next iteration (the + // `EA 81 81` case discussed in `CharSearcher::next_match`); a match + // preceded by such a false hit (a multi-iteration loop); the needle + // partially overlapping the end of the search window; and "found + // nothing". The `kani::cover`s in the harnesses witness that these + // arms execute. + // + // Why the unwind bounds are sound. Every iteration of every loop + // under verification moves a cursor by at least one byte + // (`finger += index + 1` / `finger_back = index` in the memchr loops; + // `next`/`next_back` consume one whole character in the trait + // defaults), so over a haystack of at most HAYSTACK_BYTES bytes a + // loop runs at most HAYSTACK_BYTES + 1 iterations and the bound + // HAYSTACK_BYTES + 2 unwinds it completely. Kani checks this: a bound + // that is too small fails the unwinding assertion rather than + // silently truncating the proof. + // + // Why the bound is not lifted with loop contracts. Four of the loops + // under verification are the generic `Searcher`/`ReverseSearcher` + // trait defaults (`next_match`, `next_reject`, `next_match_back`, + // `next_reject_back`), which loop over `self.next()`/`next_back()`. + // A loop invariant strong enough to re-enter `self.next()` safely + // must state the concrete searcher's `C`, which a generic trait body + // cannot name without changing shipped trait code. The unbounded + // argument for those loops is the inductive-step harnesses on + // `next`/`next_back` (the per-iteration lemma the loops need: one + // step from any `C`-state returns a boundary-valid range and + // re-establishes `C`) together with the bounded end-to-end harnesses + // that run the real default bodies. The two remaining loops, + // `CharSearcher::next_match`/`next_match_back`, are unwound within + // the same bound. Lifting it with a `#[safety::loop_invariant]` on + // those two loops was tried with the pinned Kani (branch + // `c20-loop-contracts-experiment` on the author's fork): with the + // invariant `finger <= finger_back && finger_back <= haystack.len()`, + // a symbolic-length haystack over a 16-byte backing array, and + // loop-free first/last-occurrence specifications of memchr/memrchr, + // every boundary assertion, the loop invariant and `C` verify in + // about 10 s per direction -- but the proofs cannot be merged: the + // slice comparison `slice == &self.utf8_encoded[..]` lowers to + // CBMC's builtin `memcmp`, whose internal locals are linked in after + // Kani's loop-modifies inference and so fail the loop-contract + // assigns check (four spurious "is assignable" failures per harness, + // nothing else). The comparison cannot be stubbed around it: the + // pinned Kani rejects a stub of the `compare_bytes` intrinsic + // ("invalid stub: function does not have a body, but is not an + // extern function") and cannot name the blanket `PartialEq` impl for + // `[u8]` (`<[u8] as crate::cmp::PartialEq<[u8]>>::eq`: "unable to + // find implementation of associated function `cmp::PartialEq::eq` + // for [u8]"), and an explicit `kani::loop_modifies` clause fails on + // the loop-body locals Kani hoists. That is a tool limitation to + // report upstream; the bounded proofs here are the shipped evidence. + // + // Contracts. `CharSearcher::next_match` and `next_match_back` carry + // their `Searcher` contract as `#[requires]`/`#[ensures]` attributes + // (runtime no-ops): the precondition is `C`, and the postcondition + // is the guarantee callers rely on -- a returned range is a + // needle-width range on char boundaries, at or after the finger on + // entry (at or before the `finger_back` on entry), and that finger + // is left at the range's end (start); `None` leaves the two fingers + // equal; nothing but that finger is written. `verify_cs_next_match` + // and `verify_cs_next_match_back` are the `#[kani::proof_for_contract]` + // harnesses that check the contract against the real bodies (within + // the bound above). This is what lets the `str` iterators (Challenge + // 22, `str::iter::verify`) compose with the searchers through + // `#[kani::stub_verified]` rather than assume anything about them. + // ================================================================== + + /// Maximum haystack length in bytes — the one accepted bound of these + /// proofs (see the section comment). 5 fits a 4-byte (maximum-width) + /// character plus a neighbour, so every UTF-8 width class and every + /// arm of the search loops is reachable. Every loop under + /// verification advances a cursor by at least one byte per iteration, + /// so an unwind bound of `HAYSTACK_BYTES + 2` (the `#[kani::unwind]` + /// literals below are at least that) unwinds it completely: at most + /// HAYSTACK_BYTES + 1 iterations, plus one for the unwinding + /// assertion. + const HAYSTACK_BYTES: usize = 5; + + /// 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.) + pub 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 + // byte-wise rather than `==` on the slices, which lowers to + // CBMC's `memcmp` loop and would force an unwind bound on + // every harness that states `C` (`enc_len >= 1` always) + && s.utf8_encoded[0] == enc[0] + && (enc_len < 2 || s.utf8_encoded[1] == enc[1]) + && (enc_len < 3 || s.utf8_encoded[2] == enc[2]) + && (enc_len < 4 || s.utf8_encoded[3] == enc[3]) + } + + /// 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`). + pub 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. + pub 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)); + } + + /// `CharSearcher::finger`, for invariants stated outside this module + /// (the fields are private to `str::pattern`). + pub fn cs_finger(s: &CharSearcher<'_>) -> usize { + s.finger + } + + /// `CharSearcher::finger_back`, for invariants stated outside this module. + pub fn cs_finger_back(s: &CharSearcher<'_>) -> usize { + s.finger_back + } + + /// `CharSearcher::needle`, for invariants stated outside this module. + pub fn cs_needle(s: &CharSearcher<'_>) -> char { + s.needle + } + + /// 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)); + } + + /// Contract proof for the real `CharSearcher::next_match` (the memchr + /// loop, with memchr replaced by the semantically identical + /// `stub_memchr`, see above) and criteria 2+3 for it: Kani assumes + /// the `#[requires]` (which `any_char_searcher` establishes anyway), + /// checks the `#[ensures]` and the write set on return, and the body + /// re-asserts the boundary property and `C`. Every loop iteration + /// advances `finger` by at least one byte, so the unwind bound fully + /// unwinds the search. + #[kani::proof_for_contract(CharSearcher::next_match)] + #[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)); + } + + /// Contract proof for the real `CharSearcher::next_match_back` (the + /// memrchr loop, with memrchr replaced by the semantically identical + /// `stub_memrchr`) and criteria 2+3 for it, as `verify_cs_next_match`. + /// Every iteration decreases `finger_back` by at least one byte. + #[kani::proof_for_contract(CharSearcher::next_match_back)] + #[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 the unwind bound 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. Shared with `str::iter::verify` (Challenge 22). + pub 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`. + pub 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. Shared with + /// `str::iter::verify` (Challenge 22). + pub 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); }