From f89fb8a6364416bfd9135afc15e7e8b1f3e74acd Mon Sep 17 00:00:00 2001 From: v3risec Date: Tue, 27 Oct 2026 17:01:06 +0800 Subject: [PATCH] challenge 22 proof --- library/core/src/str/iter.rs | 1914 +++++++++++++++++++++++++++++++ library/core/src/str/pattern.rs | 335 +++++- 2 files changed, 2245 insertions(+), 4 deletions(-) diff --git a/library/core/src/str/iter.rs b/library/core/src/str/iter.rs index 472ce896a059f..79abd0d6ba92a 100644 --- a/library/core/src/str/iter.rs +++ b/library/core/src/str/iter.rs @@ -1641,3 +1641,1917 @@ macro_rules! escape_types_impls { } escape_types_impls!(EscapeDebug, EscapeDefault, EscapeUnicode); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::super::pattern::verify::{ + verifier_assert_real_char_searcher, verifier_char_searcher_invariant, + verifier_stub_char_next_match, verifier_stub_char_next_match_back, + verifier_stub_char_slice_next_match, verifier_stub_char_slice_next_match_back, + verifier_stub_str_nonempty_next_match, verifier_stub_str_nonempty_next_match_back, + }; + use super::super::pattern::{CharSearcher, CharSliceSearcher, StrSearcher}; + use super::super::validations::{utf8_char_width, utf8_is_cont_byte}; + use super::*; + + // The backing array bounds CBMC's object model, not the number of + // iteration steps. Claims of arbitrary mathematical length require an + // additional argument beyond this finite allocation model. + const MAX_BYTES: usize = 256; + const UTF8_PAD: usize = 4; + const BUFFER_BYTES: usize = MAX_BYTES + UTF8_PAD; + + // The local UTF-8 predicate and original bounded advance checks follow + // the input-model approach in PR #557; the interval protocol below + // replaces its char-specific iterator proof architecture. + // A loop-free UTF-8 validity model. For every leading byte, validate + // the sequence width, continuation bytes, and exceptional second-byte + // rules (E0/ED/F0/F4). Every continuation byte must be within three + // positions after a leading byte. Combined, these are equivalent to + // validity of buf[..len], provided len <= N - UTF8_PAD. + // Do not use from_utf8 as a symbolic-input filter under loop-contract + // instrumentation: it can abstract away the validation algorithm. + fn verifier_utf8_valid(buf: &[u8; N], len: usize) -> bool { + let p = buf.as_ptr(); + let sequences = crate::forall!(|i in (0, N - UTF8_PAD)| unsafe { + let i: usize = i; + let x0 = *p.wrapping_add(i); + let x1 = *p.wrapping_add(i.wrapping_add(1)); + let x2 = *p.wrapping_add(i.wrapping_add(2)); + let x3 = *p.wrapping_add(i.wrapping_add(3)); + let continuation0 = (x0 as i8) < -64; + let continuation1 = (x1 as i8) < -64; + let continuation2 = (x2 as i8) < -64; + let continuation3 = (x3 as i8) < -64; + let width = (x0 < 0x80) as usize + + (((x0 >= 0xC2) & (x0 < 0xE0)) as usize) * 2 + + (((x0 >= 0xE0) & (x0 < 0xF0)) as usize) * 3 + + (((x0 >= 0xF0) & (x0 < 0xF5)) as usize) * 4; + let next_is_continuation = + (*p.wrapping_add(i.wrapping_add(width)) as i8) < -64; + let second_byte_ok = ((x0 != 0xE0) | (x1 >= 0xA0)) + & ((x0 != 0xED) | (x1 < 0xA0)) + & ((x0 != 0xF0) | (x1 >= 0x90)) + & ((x0 != 0xF4) | (x1 < 0x90)); + (i >= len) + | continuation0 + | ((width > 0) + & (i.wrapping_add(width) <= len) + & ((width < 2) | (continuation1 & second_byte_ok)) + & ((width < 3) | continuation2) + & ((width < 4) | continuation3) + & ((i.wrapping_add(width) == len) | !next_is_continuation)) + }); + let covered = crate::forall!(|i in (0, N - UTF8_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)) + }); + sequences && covered + } + + fn verifier_nondet_utf8(buf: &[u8; N]) -> &str { + let len: usize = kani::any(); + // INPUT DOMAIN: allocated prefix or index extent. + kani::assume(len <= N - UTF8_PAD); + kani::cover(true, "C22-A01: verifier_nondet_utf8 assumption admitted"); + // CHALLENGE 22 assumption 4: valid UTF-8 input. + kani::assume(verifier_utf8_valid(buf, len)); + kani::cover(true, "C22-A02: verifier_nondet_utf8 assumption admitted"); + // SAFETY: verifier_utf8_valid characterizes valid UTF-8 exactly. + unsafe { from_utf8_unchecked(&buf[..len]) } + } + + fn verifier_nondet_window(s: &str) -> (usize, usize) { + let start: usize = kani::any(); + let end: usize = kani::any(); + // INPUT STATE: an ordered UTF-8 boundary window. + kani::assume(start <= end && end <= s.len()); + kani::cover(true, "C22-A03: verifier_nondet_window assumption admitted"); + // INPUT STATE: an ordered UTF-8 boundary window. + kani::assume(s.is_char_boundary(start) && s.is_char_boundary(end)); + kani::cover(true, "C22-A04: verifier_nondet_window assumption admitted"); + (start, end) + } + + fn verifier_same_slice(left: &str, right: &str) -> bool { + left.as_ptr() == right.as_ptr() && left.len() == right.len() + } + + fn verifier_slice_offset(s: &str, subslice: &str) -> usize { + let base = s.as_ptr().addr(); + let current = subslice.as_ptr().addr(); + assert!(base <= current); + current - base + } + + // Assert *both* physical range and UTF-8 boundaries. Kani's checking + // of str::get_unchecked alone is not a substitute for the latter. + fn verifier_assert_str_range(s: &str, result: &str, start: usize, end: usize) { + assert!( + start <= end && end <= s.len(), + "slice is within the haystack" + ); + assert!( + s.is_char_boundary(start) && s.is_char_boundary(end), + "slice endpoints are UTF-8 character boundaries" + ); + assert!( + result.as_ptr() == s.as_ptr().wrapping_add(start), + "slice base pointer" + ); + assert!(result.len() == end - start, "slice byte length"); + } + + // An arbitrary [start, end) window is exactly the type invariant of + // Chars: arbitrary interleavings of next/next_back preserve this set. + #[kani::proof] + pub fn harness_chars_next() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let (start, end) = verifier_nondet_window(s); + let mut iter = s[start..end].chars(); + match iter.next() { + Some(ch) => { + let next_start = start + ch.len_utf8(); + verifier_assert_str_range(s, iter.as_str(), next_start, end); + kani::cover(ch.len_utf8() == 1, "chars::next: ASCII"); + kani::cover(ch.len_utf8() == 2, "chars::next: two-byte scalar"); + kani::cover(ch.len_utf8() == 3, "chars::next: three-byte scalar"); + kani::cover(ch.len_utf8() == 4, "chars::next: four-byte scalar"); + } + None => { + assert!(start == end); + kani::cover(true, "chars::next: exhausted"); + } + } + kani::cover(true, "C22-END: harness_chars_next completed"); + } + + #[kani::proof] + pub fn harness_chars_next_back() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let (start, end) = verifier_nondet_window(s); + let mut iter = s[start..end].chars(); + match iter.next_back() { + Some(ch) => { + assert!(ch.len_utf8() <= end - start); + verifier_assert_str_range(s, iter.as_str(), start, end - ch.len_utf8()); + kani::cover(ch.len_utf8() == 1, "chars::next_back: ASCII"); + kani::cover(ch.len_utf8() == 4, "chars::next_back: four-byte scalar"); + } + None => { + assert!(start == end); + kani::cover(true, "chars::next_back: exhausted"); + } + } + kani::cover(true, "C22-END: harness_chars_next_back completed"); + } + + #[kani::proof] + pub fn harness_chars_as_str() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let (start, end) = verifier_nondet_window(s); + let window = &s[start..end]; + let mut iter = window.chars(); + assert!(verifier_same_slice(iter.as_str(), window)); + let front = iter.next().map_or(0, char::len_utf8); + let back = iter.next_back().map_or(0, char::len_utf8); + verifier_assert_str_range(s, iter.as_str(), start + front, end - back); + kani::cover(front > 0 && back > 0, "chars::as_str: both ends consumed"); + kani::cover(true, "C22-END: harness_chars_as_str completed"); + } + + const ADVANCE_MAX: usize = 8; + const ADVANCE_BYTES: usize = 128; + const CHUNK_MIN: usize = 33; + const CHUNK_MAX: usize = 40; + const CHUNK_BYTES: usize = 48; + + // Independent scalar-by-scalar reference for the bounded regression + // checks. It uses the public decoder, not advance_by's chunk counting. + fn verifier_reference_advance(s: &str, start: usize, end: usize, n: usize) -> (usize, usize) { + let mut chars = s[start..end].chars(); + let mut consumed = 0; + let mut pos = start; + while consumed < n { + match chars.next() { + Some(ch) => { + pos += ch.len_utf8(); + consumed += 1; + } + None => break, + } + } + (pos, consumed) + } + + fn verifier_check_chars_advance(s: &str, start: usize, end: usize, n: usize) { + let (expected_end, consumed) = verifier_reference_advance(s, start, end, n); + let mut iter = s[start..end].chars(); + let result = iter.advance_by(n); // real production body + verifier_assert_str_range(s, iter.as_str(), expected_end, end); + match result { + Ok(()) => assert!(consumed == n), + Err(remaining) => { + assert!(consumed < n); + assert!(expected_end == end); + assert!(remaining.get() == n - consumed); + } + } + kani::cover( + result.is_ok() && n > 0, + "chars::advance_by: successful skip", + ); + kani::cover(result.is_err(), "chars::advance_by: not enough characters"); + } + + // Both the backing allocation and advance count are bounded. The + // unwind derives from n, not string length; this is a regression proof. + #[kani::proof] + #[kani::unwind(9)] + pub fn harness_chars_advance_by_small() { + let buf: [u8; ADVANCE_BYTES + UTF8_PAD] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let (start, end) = verifier_nondet_window(s); + let n: usize = kani::any(); + // INPUT DOMAIN: this bounded request partition only. + kani::assume(n <= ADVANCE_MAX); + kani::cover(true, "C22-A05: harness_chars_advance_by_small assumption admitted"); + verifier_check_chars_advance(s, start, end, n); + kani::cover( + n == ADVANCE_MAX && start < end, + "advance_by: maximum small count", + ); + kani::cover(true, "C22-END: harness_chars_advance_by_small completed"); + } + + // Exercise the real chunk-skip loop (as well as its trailing-byte and + // character loops) on a symbolic 48-byte UTF-8 string. The 48-byte + // fixed length is a solver-budget limitation, not unbounded proof. + #[kani::proof] + // The scalar reference can take 40 steps; the chunk body has 32. + #[kani::unwind(42)] + pub fn harness_chars_advance_by_chunked() { + let buf: [u8; CHUNK_BYTES + UTF8_PAD] = kani::any(); + // CHALLENGE 22 assumption 4: valid UTF-8 input. + kani::assume(verifier_utf8_valid(&buf, CHUNK_BYTES)); + kani::cover(true, "C22-A06: harness_chars_advance_by_chunked assumption admitted"); + // SAFETY: the encoded prefix satisfies the exact UTF-8 predicate. + let s = unsafe { from_utf8_unchecked(&buf[..CHUNK_BYTES]) }; + let n: usize = kani::any(); + // INPUT DOMAIN: this bounded request partition only. + kani::assume(CHUNK_MIN <= n && n <= CHUNK_MAX); + kani::cover(true, "C22-A07: harness_chars_advance_by_chunked assumption admitted"); + verifier_check_chars_advance(s, 0, CHUNK_BYTES, n); + kani::cover( + utf8_is_cont_byte(buf[32]), + "advance_by: crosses UTF-8 chunk boundary", + ); + kani::cover(buf[0] < 0x80 && buf[31] < 0x80, "advance_by: ASCII chunk"); + kani::cover( + buf[0] >= 0xF0 + && buf[4] >= 0xF0 + && buf[8] >= 0xF0 + && buf[12] >= 0xF0 + && buf[16] >= 0xF0 + && buf[20] >= 0xF0 + && buf[24] >= 0xF0 + && buf[28] >= 0xF0, + "advance_by: chunk with eight four-byte scalars", + ); + kani::cover(true, "C22-END: harness_chars_advance_by_chunked completed"); + } + + // Challenge 22 permits assuming pattern.rs (assumption 2). This is an + // interval-protocol abstraction, not a proof of any matching algorithm. + // Each call may skip Reject steps and return any boundary-valid Match, + // including a zero-width Match. Thus widths may vary between calls. + // The common residual interval suffices for directional safety; this + // model deliberately does NOT implement DoubleEndedSearcher. Concrete + // double-ended instances are checked separately below. + // Projection argument: for a forward-only concrete searcher, front/back + // describe the unreported suffix; every real next_match return is admitted + // here. The reverse-only argument uses the unreported prefix. Consumers + // observe only haystack() and returned indices. This simulation argument + // imports assumption 2; Kani does not quantify over all Rust Pattern types. + struct ModelPattern; + + struct ModelSearcher<'a> { + haystack: &'a str, + front: usize, + back: usize, + // Fresh per-operation observers; production iterators cannot inspect + // these fields. any_split resets them when projecting a logical state. + last_match: Option<(usize, usize)>, + previous_match: Option<(usize, usize)>, + calls: usize, + } + + impl Pattern for ModelPattern { + type Searcher<'a> = ModelSearcher<'a>; + + fn into_searcher(self, haystack: &str) -> ModelSearcher<'_> { + ModelSearcher { + haystack, + front: 0, + back: haystack.len(), + last_match: None, + previous_match: None, + calls: 0, + } + } + } + + fn type_invariant_searcher(s: &ModelSearcher<'_>) -> bool { + s.front <= s.back + && s.back <= s.haystack.len() + && s.haystack.is_char_boundary(s.front) + && s.haystack.is_char_boundary(s.back) + } + + fn any_match_range(s: &str, front: usize, back: usize) -> (usize, usize) { + let a: usize = kani::any(); + let b: usize = kani::any(); + // These are Searcher guarantees imported under assumption 2, not + // properties of SplitInternal assumed after its execution. + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(front <= a && a <= b && b <= back); + kani::cover(true, "C22-A08: any_match_range assumption admitted"); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(s.is_char_boundary(a) && s.is_char_boundary(b)); + kani::cover(true, "C22-A09: any_match_range assumption admitted"); + (a, b) + } + + // SAFETY: next emits adjacent, in-bounds UTF-8 ranges. The next_match + // override summarizes zero or more skipped Rejects and one Match (or + // exhaustion). Matching contents are intentionally over-approximated. + unsafe impl<'a> Searcher<'a> for ModelSearcher<'a> { + fn haystack(&self) -> &'a str { + self.haystack + } + + fn next(&mut self) -> super::super::pattern::SearchStep { + use super::super::pattern::SearchStep; + assert!(type_invariant_searcher(self)); + if kani::any() { + let old = self.front; + self.front = self.back; + if old == self.back { + SearchStep::Done + } else { + SearchStep::Reject(old, self.back) + } + } else { + let (_, b) = any_match_range(self.haystack, self.front, self.back); + let a = self.front; + self.front = b; + if kani::any() { + SearchStep::Match(a, b) + } else { + SearchStep::Reject(a, b) + } + } + } + + fn next_match(&mut self) -> Option<(usize, usize)> { + assert!(type_invariant_searcher(self)); + self.previous_match = self.last_match; + // Instrumentation must not introduce overflow on long histories. + self.calls = self.calls.saturating_add(1); + self.last_match = if kani::any() { + let range = any_match_range(self.haystack, self.front, self.back); + self.front = range.1; + Some(range) + } else { + self.front = self.back; + None + }; + self.last_match + } + } + + // SAFETY: same range protocol, consumed from the opposite end. No claim + // is made that independent nondeterministic choices define identical + // forward/reverse streams, hence there is no DoubleEndedSearcher impl. + unsafe impl<'a> ReverseSearcher<'a> for ModelSearcher<'a> { + fn next_back(&mut self) -> super::super::pattern::SearchStep { + use super::super::pattern::SearchStep; + assert!(type_invariant_searcher(self)); + if kani::any() { + let old = self.back; + self.back = self.front; + if old == self.front { + SearchStep::Done + } else { + SearchStep::Reject(self.front, old) + } + } else { + let (a, _) = any_match_range(self.haystack, self.front, self.back); + let b = self.back; + self.back = a; + if kani::any() { + SearchStep::Match(a, b) + } else { + SearchStep::Reject(a, b) + } + } + } + + fn next_match_back(&mut self) -> Option<(usize, usize)> { + assert!(type_invariant_searcher(self)); + self.previous_match = self.last_match; + // Instrumentation must not introduce overflow on long histories. + self.calls = self.calls.saturating_add(1); + self.last_match = if kani::any() { + let range = any_match_range(self.haystack, self.front, self.back); + self.back = range.0; + Some(range) + } else { + self.back = self.front; + None + }; + self.last_match + } + } + + #[derive(Clone, Copy)] + struct SplitState { + start: usize, + end: usize, + front: usize, + back: usize, + trailing: bool, + finished: bool, + } + + fn split_state(iter: &SplitInternal<'_, ModelPattern>) -> SplitState { + SplitState { + start: iter.start, + end: iter.end, + front: iter.matcher.front, + back: iter.matcher.back, + trailing: iter.allow_trailing_empty, + finished: iter.finished, + } + } + + fn type_invariant_split(iter: &SplitInternal<'_, ModelPattern>) -> bool { + type_invariant_searcher(&iter.matcher) + && iter.start <= iter.matcher.front + && iter.matcher.back <= iter.end + && iter.end <= iter.matcher.haystack.len() + && iter.matcher.haystack.is_char_boundary(iter.start) + && iter.matcher.haystack.is_char_boundary(iter.end) + } + + fn any_split(s: &str) -> SplitInternal<'_, ModelPattern> { + let (start, end) = verifier_nondet_window(s); + let (front, back) = any_match_range(s, start, end); + SplitInternal { + start, + end, + matcher: ModelSearcher { + haystack: s, + front, + back, + last_match: None, + previous_match: None, + calls: 0, + }, + allow_trailing_empty: kani::any(), + finished: kani::any(), + } + } + + fn assert_split_frame(s: &str, iter: &SplitInternal<'_, ModelPattern>) { + assert!(type_invariant_split(iter)); + assert!(verifier_same_slice(iter.matcher.haystack(), s)); + } + + fn assert_valid_split_forward_transition( + s: &str, + old: SplitState, + iter: &SplitInternal<'_, ModelPattern>, + result: Option<&str>, + inclusive: bool, + ) { + assert_split_frame(s, iter); + assert_eq!(iter.end, old.end); + assert_eq!(iter.matcher.back, old.back); + assert_eq!(iter.allow_trailing_empty, old.trailing); + if old.finished { + assert!(result.is_none()); + assert_eq!(iter.start, old.start); + assert_eq!(iter.matcher.calls, 0); + assert_eq!(iter.matcher.front, old.front); + assert!(iter.finished); + return; + } + assert_eq!(iter.matcher.calls, 1); + match iter.matcher.last_match { + Some((a, b)) => { + let part = result.unwrap(); + verifier_assert_str_range(s, part, old.start, if inclusive { b } else { a }); + assert_eq!(iter.start, b); + assert!(!iter.finished); + kani::cover(a == b, "split: zero-width match"); + kani::cover(b - a > 4, "split: multi-character match"); + } + None => { + assert!(iter.finished); + assert_eq!(iter.start, old.start); + if old.trailing || old.start < old.end { + verifier_assert_str_range(s, result.unwrap(), old.start, old.end); + } else { + assert!(result.is_none()); + } + kani::cover(true, "split: exhausted search"); + } + } + } + + fn assert_valid_split_reverse_transition( + s: &str, + old: SplitState, + iter: &SplitInternal<'_, ModelPattern>, + result: Option<&str>, + inclusive: bool, + ) { + assert_split_frame(s, iter); + assert_eq!(iter.start, old.start); + assert_eq!(iter.matcher.front, old.front); + if old.finished { + assert!(result.is_none()); + assert_eq!(iter.end, old.end); + assert_eq!(iter.matcher.back, old.back); + assert_eq!(iter.matcher.calls, 0); + assert_eq!(iter.allow_trailing_empty, old.trailing); + assert!(iter.finished); + return; + } + assert!(iter.allow_trailing_empty); + assert!(iter.matcher.calls >= 1 && iter.matcher.calls <= 2); + if iter.finished { + match result { + Some(part) => { + // A first empty tail may have been suppressed before + // returning the remaining prefix in the second search. + verifier_assert_str_range(s, part, old.start, iter.end); + assert!(iter.end <= old.end); + } + None => assert!(!old.trailing && iter.end == old.start), + } + } else { + let (a, b) = iter.matcher.last_match.unwrap(); + let part = result.unwrap(); + let output_end = if iter.matcher.calls == 2 { + assert!(!old.trailing); + let (first_a, first_b) = iter.matcher.previous_match.unwrap(); + assert_eq!(first_b, old.end); + if inclusive { first_b } else { first_a } + } else { + old.end + }; + verifier_assert_str_range(s, part, b, output_end); + assert_eq!(iter.end, if inclusive { b } else { a }); + kani::cover(a == b, "reverse split: zero-width match"); + kani::cover(b - a > 4, "reverse split: multi-character match"); + } + kani::cover( + iter.matcher.calls == 2, + "reverse split: suppress empty tail then search again", + ); + kani::cover(result.is_none(), "reverse split: no remaining part"); + } + + #[kani::proof] + fn harness_searcher_protocol() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut iter = any_split(s); + let old = split_state(&iter); + let reverse: bool = kani::any(); + let result = if reverse { + iter.matcher.next_match_back() + } else { + iter.matcher.next_match() + }; + assert!(type_invariant_searcher(&iter.matcher)); + assert!(verifier_same_slice(iter.matcher.haystack(), s)); + match result { + Some((a, b)) => { + assert!(old.front <= a && a <= b && b <= old.back); + assert!(s.is_char_boundary(a) && s.is_char_boundary(b)); + if reverse { + assert_eq!(iter.matcher.back, a); + } else { + assert_eq!(iter.matcher.front, b); + } + kani::cover(a == b, "protocol: zero-width match"); + kani::cover(b - a > 4, "protocol: width larger than one scalar"); + } + None => assert_eq!(iter.matcher.front, iter.matcher.back), + } + if reverse { + assert_eq!(iter.matcher.front, old.front); + } else { + assert_eq!(iter.matcher.back, old.back); + } + kani::cover(true, "C22-END: harness_searcher_protocol completed"); + } + + fn assert_initial_split(s: &str, iter: &SplitInternal<'_, P>, trailing: bool) { + assert_eq!(iter.start, 0); + assert_eq!(iter.end, s.len()); + assert_eq!(iter.allow_trailing_empty, trailing); + assert!(!iter.finished); + assert!(verifier_same_slice(iter.matcher.haystack(), s)); + } + + #[kani::proof] + fn harness_split_constructors() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let needle: char = kani::any(); + assert_initial_split(s, &s.split(needle).0, true); + assert_initial_split(s, &s.split_terminator(needle).0, false); + assert_initial_split(s, &s.split_inclusive(needle).0, false); + assert!(verifier_char_searcher_invariant(&s.split(needle).0.matcher)); + assert_initial_split(s, &s.split("").0, true); + assert_initial_split(s, &s.split_terminator("").0, false); + assert_initial_split(s, &s.split_inclusive("").0, false); + let chars: [char; 2] = kani::any(); + assert_initial_split(s, &s.split(&chars[..]).0, true); + assert_initial_split(s, &s.split_terminator(chars).0, false); + assert_initial_split(s, &s.split_inclusive(&chars).0, false); + let model = s.split(ModelPattern).0; + assert_initial_split(s, &model, true); + assert!(type_invariant_split(&model)); + let terminator = s.split_terminator(ModelPattern).0; + let inclusive = s.split_inclusive(ModelPattern).0; + assert_initial_split(s, &terminator, false); + assert_initial_split(s, &inclusive, false); + assert!(type_invariant_split(&terminator)); + assert!(type_invariant_split(&inclusive)); + kani::cover(s.is_empty(), "constructors: empty haystack"); + kani::cover(!s.is_empty(), "constructors: nonempty haystack"); + kani::cover(true, "C22-END: harness_split_constructors completed"); + } + + #[kani::proof] + fn harness_split_get_end() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut iter = any_split(s); + let old = split_state(&iter); + let result = iter.get_end(); + if !old.finished && (old.trailing || old.start < old.end) { + verifier_assert_str_range(s, result.unwrap(), old.start, old.end); + kani::cover(old.start == old.end, "get_end: allowed empty tail"); + kani::cover(old.start < old.end, "get_end: nonempty tail"); + } else { + assert!(result.is_none()); + kani::cover(old.finished, "get_end: already finished"); + kani::cover(!old.finished, "get_end: suppressed empty tail"); + } + assert!(iter.finished); + assert_eq!(iter.start, old.start); + assert_eq!(iter.end, old.end); + assert_eq!(iter.matcher.front, old.front); + assert_eq!(iter.matcher.back, old.back); + assert_eq!(iter.matcher.calls, 0); + assert_split_frame(s, &iter); + kani::cover(true, "C22-END: harness_split_get_end completed"); + } + + #[kani::proof] + fn harness_split_next() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut iter = any_split(s); + let old = split_state(&iter); + let result = iter.next(); + assert_valid_split_forward_transition(s, old, &iter, result, false); + kani::cover(true, "C22-END: harness_split_next completed"); + } + + #[kani::proof] + fn harness_split_next_inclusive() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut iter = any_split(s); + let old = split_state(&iter); + let result = iter.next_inclusive(); + assert_valid_split_forward_transition(s, old, &iter, result, true); + kani::cover(true, "C22-END: harness_split_next_inclusive completed"); + } + + #[kani::proof] + fn harness_split_next_back() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut iter = any_split(s); + let old = split_state(&iter); + let result = iter.next_back(); + assert_valid_split_reverse_transition(s, old, &iter, result, false); + kani::cover(true, "C22-END: harness_split_next_back completed"); + } + + #[kani::proof] + fn harness_split_next_back_inclusive() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut iter = any_split(s); + let old = split_state(&iter); + let result = iter.next_back_inclusive(); + assert_valid_split_reverse_transition(s, old, &iter, result, true); + kani::cover(true, "C22-END: harness_split_next_back_inclusive completed"); + } + + #[kani::proof] + fn harness_split_remainder() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let iter = any_split(s); + let old = split_state(&iter); + match iter.remainder() { + Some(part) => { + assert!(!old.finished); + verifier_assert_str_range(s, part, old.start, old.end); + } + None => assert!(old.finished), + } + assert_split_frame(s, &iter); + assert_eq!(iter.matcher.calls, 0); + kani::cover(old.finished, "remainder: finished"); + kani::cover( + !old.finished && old.start == old.end, + "remainder: empty active interval", + ); + kani::cover(true, "C22-END: harness_split_remainder completed"); + } + + fn assert_valid_match_transition( + s: &str, + old_front: usize, + old_back: usize, + searcher: &ModelSearcher<'_>, + result: Option<(usize, &str)>, + reverse: bool, + ) { + assert!(type_invariant_searcher(searcher)); + assert!(verifier_same_slice(searcher.haystack(), s)); + assert_eq!(searcher.calls, 1); + match searcher.last_match { + Some((a, b)) => { + let (index, part) = result.unwrap(); + assert_eq!(index, a); + verifier_assert_str_range(s, part, a, b); + assert!(old_front <= a && b <= old_back); + if reverse { + assert_eq!(searcher.back, a); + } else { + assert_eq!(searcher.front, b); + } + kani::cover(a == b, "matches: empty match"); + kani::cover(b - a > 4, "matches: multiple-character match"); + } + None => { + assert!(result.is_none()); + assert_eq!(searcher.front, searcher.back); + } + } + if reverse { + assert_eq!(searcher.front, old_front); + } else { + assert_eq!(searcher.back, old_back); + } + kani::cover(result.is_none(), "matches: exhausted"); + } + + #[kani::proof] + fn harness_match_indices_next() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let searcher = any_split(s).matcher; + let (front, back) = (searcher.front, searcher.back); + let mut iter = MatchIndicesInternal::(searcher); + let result = iter.next(); + assert_valid_match_transition(s, front, back, &iter.0, result, false); + kani::cover(true, "C22-END: harness_match_indices_next completed"); + } + + #[kani::proof] + fn harness_match_indices_next_back() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let searcher = any_split(s).matcher; + let (front, back) = (searcher.front, searcher.back); + let mut iter = MatchIndicesInternal::(searcher); + let result = iter.next_back(); + assert_valid_match_transition(s, front, back, &iter.0, result, true); + kani::cover(true, "C22-END: harness_match_indices_next_back completed"); + } + + #[kani::proof] + fn harness_matches_next() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let searcher = any_split(s).matcher; + let (front, back) = (searcher.front, searcher.back); + let mut iter = MatchesInternal::(searcher); + let result = iter + .next() + .map(|part| (verifier_slice_offset(s, part), part)); + assert_valid_match_transition(s, front, back, &iter.0, result, false); + kani::cover(true, "C22-END: harness_matches_next completed"); + } + + #[kani::proof] + fn harness_matches_next_back() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let searcher = any_split(s).matcher; + let (front, back) = (searcher.front, searcher.back); + let mut iter = MatchesInternal::(searcher); + let result = iter + .next_back() + .map(|part| (verifier_slice_offset(s, part), part)); + assert_valid_match_transition(s, front, back, &iter.0, result, true); + kani::cover(true, "C22-END: harness_matches_next_back completed"); + } + + // Prove the stronger relation to the exact pre-call remaining interval. + // For any past prefix_end <= old.start and suffix_start >= old.end, + // these assertions imply the old ownership relation by transitivity. + // No extra assumption on ghost history bounds is needed here. + #[kani::proof] + fn harness_split_history_step() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut iter = any_split(s); + let reverse: bool = kani::any(); + let old = split_state(&iter); + let result = if reverse { + iter.next_back() + } else { + iter.next() + }; + if let Some(part) = result { + let a = verifier_slice_offset(s, part); + let b = a + part.len(); + verifier_assert_str_range(s, part, a, b); + assert!(old.start <= a && b <= old.end); + if !iter.finished { + if reverse { + assert!(iter.end <= a); + } else { + assert!(b <= iter.start); + } + } + } + if !iter.finished { + assert!(old.start <= iter.start && iter.end <= old.end); + } else { + assert!(iter.next().is_none()); + assert!(iter.next_back().is_none()); + } + assert_split_frame(s, &iter); + kani::cover( + reverse && !old.finished && result.is_some(), + "history: reverse step", + ); + kani::cover( + !reverse && !old.finished && result.is_some(), + "history: forward step", + ); + kani::cover(true, "C22-END: harness_split_history_step completed"); + } + + #[kani::proof] + pub fn harness_split_ascii_whitespace_remainder() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut iter = s.split_ascii_whitespace(); + assert!( + iter.remainder() + .is_some_and(|part| verifier_same_slice(part, s)) + ); + + // Every reachable inner slice is a UTF-8-boundary window. Cutting + // at ASCII whitespace cannot cut through a multibyte scalar. + let (start, end) = verifier_nondet_window(s); + iter.inner.iter.iter.v = s[start..end].as_bytes(); + iter.inner.iter.iter.finished = kani::any(); + let finished = iter.inner.iter.iter.finished; + match iter.remainder() { + Some(part) => { + assert!(!finished); + verifier_assert_str_range(s, part, start, end); + kani::cover(part.is_empty(), "ASCII whitespace remainder: empty window"); + kani::cover( + !part.is_empty(), + "ASCII whitespace remainder: nonempty window", + ); + } + None => { + assert!(finished); + kani::cover(true, "ASCII whitespace remainder: finished"); + } + } + kani::cover(true, "C22-END: harness_split_ascii_whitespace_remainder completed"); + } + + // Main already contains #[requires(idx < self.0.len())]. The contract + // is discharged against the original body, with Kani generating the + // precondition rather than the harness assuming the target's safety. + #[kani::proof_for_contract(Bytes::__iterator_get_unchecked)] + pub fn harness_bytes_iterator_get_unchecked() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let (start, end) = verifier_nondet_window(s); + let window = &s[start..end]; + let mut iter = window.bytes(); + let index: usize = kani::any(); + let item = unsafe { iter.__iterator_get_unchecked(index) }; + assert!(item == window.as_bytes()[index]); + kani::cover(index > 0, "bytes::get_unchecked: index past first byte"); + kani::cover(true, "C22-END: harness_bytes_iterator_get_unchecked completed"); + } + fn assert_ordered_parts(s: &str, front: Option<&str>, back: Option<&str>) { + if let Some(front) = front { + let a = verifier_slice_offset(s, front); + verifier_assert_str_range(s, front, a, a + front.len()); + } + if let Some(back) = back { + let a = verifier_slice_offset(s, back); + verifier_assert_str_range(s, back, a, a + back.len()); + } + if let (Some(front), Some(back)) = (front, back) { + let a = verifier_slice_offset(s, front); + let b = verifier_slice_offset(s, back); + assert!(a + front.len() <= b, "opposite-end outputs do not overlap"); + } + } + + fn assert_public_split_pair<'a, P>(s: &'a str, pattern: P) + where + P: Pattern: DoubleEndedSearcher<'a>>, + { + let inclusive: bool = kani::any(); + let trailing: bool = kani::any(); + let mut iter = if inclusive { + s.split_inclusive(pattern).0 + } else if trailing { + s.split(pattern).0 + } else { + s.split_terminator(pattern).0 + }; + let front_first: bool = kani::any(); + let (front, back) = if front_first { + let front = if inclusive { + iter.next_inclusive() + } else { + iter.next() + }; + let back = if inclusive { + iter.next_back_inclusive() + } else { + iter.next_back() + }; + (front, back) + } else { + let back = if inclusive { + iter.next_back_inclusive() + } else { + iter.next_back() + }; + let front = if inclusive { + iter.next_inclusive() + } else { + iter.next() + }; + (front, back) + }; + assert_ordered_parts(s, front, back); + if let Some(rest) = iter.remainder() { + let a = verifier_slice_offset(s, rest); + verifier_assert_str_range(s, rest, a, iter.end); + if let Some(front) = front { + assert!(verifier_slice_offset(s, front) + front.len() <= a); + } + if let Some(back) = back { + assert!(iter.end <= verifier_slice_offset(s, back)); + } + } else { + assert!(iter.finished); + assert!(iter.next().is_none()); + assert!(iter.next_back().is_none()); + } + kani::cover( + front_first && front.is_some() && back.is_some(), + "mixed: front then back", + ); + kani::cover( + !front_first && front.is_some() && back.is_some(), + "mixed: back then front", + ); + kani::cover( + inclusive && front.is_some() && back.is_some(), + "mixed: inclusive parts", + ); + kani::cover( + !inclusive && !trailing && front.is_some(), + "mixed: terminator parts", + ); + } + + #[kani::proof] + #[kani::stub( as Searcher<'_>>::next_match, verifier_stub_char_next_match)] + #[kani::stub( as ReverseSearcher<'_>>::next_match_back, verifier_stub_char_next_match_back)] + fn harness_split_mixed_directions() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + assert_public_split_pair(s, kani::any::()); + kani::cover(true, "C22-END: harness_split_mixed_directions completed"); + } + + #[kani::proof] + #[kani::stub( as Searcher<'_>>::next_match, verifier_stub_char_slice_next_match)] + #[kani::stub( as ReverseSearcher<'_>>::next_match_back, verifier_stub_char_slice_next_match_back)] + fn harness_split_char_slice_mixed() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let chars: [char; 2] = kani::any(); + let len: usize = kani::any(); + // INPUT DOMAIN: allocated prefix or index extent. + kani::assume(len <= chars.len()); + kani::cover(true, "C22-A10: harness_split_char_slice_mixed assumption admitted"); + assert_public_split_pair(s, &chars[..len]); + kani::cover(len == 0, "character set: empty"); + kani::cover( + len == 2 && chars[0].len_utf8() != chars[1].len_utf8(), + "character set: different widths", + ); + kani::cover(true, "C22-END: harness_split_char_slice_mixed completed"); + } + + // Concrete &str instances deliberately keep the two directions separate. + // They are integration checks under assumption 2, not a proof that all + // Pattern implementations refine the abstract protocol above. + fn assert_str_pattern_direction(s: &str, needle: &str, reverse: bool) { + let inclusive: bool = kani::any(); + let mut iter = if inclusive { + s.split_inclusive(needle).0 + } else { + s.split_terminator(needle).0 + }; + let first = if reverse { + if inclusive { + iter.next_back_inclusive() + } else { + iter.next_back() + } + } else if inclusive { + iter.next_inclusive() + } else { + iter.next() + }; + let second = if reverse { + if inclusive { + iter.next_back_inclusive() + } else { + iter.next_back() + } + } else if inclusive { + iter.next_inclusive() + } else { + iter.next() + }; + if reverse { + assert_ordered_parts(s, second, first); + } else { + assert_ordered_parts(s, first, second); + } + if let Some(rest) = iter.remainder() { + verifier_assert_str_range(s, rest, iter.start, iter.end); + } else { + assert!(iter.finished); + let terminal = if reverse { + if inclusive { + iter.next_back_inclusive() + } else { + iter.next_back() + } + } else if inclusive { + iter.next_inclusive() + } else { + iter.next() + }; + assert!(terminal.is_none()); + } + let mut indices = if reverse { + s.rmatch_indices(needle).0 + } else { + s.match_indices(needle).0 + }; + let matched = if reverse { + indices.next_back() + } else { + indices.next() + }; + if let Some((a, part)) = matched { + verifier_assert_str_range(s, part, a, a + needle.len()); + } + // A fresh instance also exercises the MatchesInternal wrapper. + let mut matches = MatchesInternal::<&str>(needle.into_searcher(s)); + if let Some(part) = if reverse { + matches.next_back() + } else { + matches.next() + } { + let a = verifier_slice_offset(s, part); + verifier_assert_str_range(s, part, a, a + needle.len()); + } + kani::cover( + first.is_some() && second.is_some(), + "str pattern: two split parts", + ); + } + + #[kani::proof] + #[kani::unwind(5)] + fn harness_str_empty_forward() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + assert_str_pattern_direction(s, "", false); + kani::cover(s.is_empty(), "empty needle: empty haystack"); + kani::cover(true, "C22-END: harness_str_empty_forward completed"); + } + + #[kani::proof] + #[kani::unwind(5)] + fn harness_str_empty_reverse() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + assert_str_pattern_direction(s, "", true); + kani::cover(s.is_empty(), "empty needle reverse: empty haystack"); + kani::cover(true, "C22-END: harness_str_empty_reverse completed"); + } + + fn any_short_needle(buf: &mut [u8; 8]) -> &str { + let first: char = kani::any(); + let mut len = first.encode_utf8(buf).len(); + if kani::any() { + let second: char = kani::any(); + len += second.encode_utf8(&mut buf[len..]).len(); + } + // SAFETY: concatenation of one or two scalar UTF-8 encodings. + unsafe { from_utf8_unchecked(&buf[..len]) } + } + + #[kani::proof] + #[kani::unwind(20)] + #[kani::stub( as Searcher<'_>>::next_match, verifier_stub_str_nonempty_next_match)] + fn harness_str_nonempty_forward() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut needle_buf = [0u8; 8]; + let needle = any_short_needle(&mut needle_buf); + assert_str_pattern_direction(s, needle, false); + kani::cover(needle.len() == 1, "str pattern: byte searcher"); + kani::cover(needle.len() > 4, "str pattern: two multibyte scalars"); + kani::cover(true, "C22-END: harness_str_nonempty_forward completed"); + } + + #[kani::proof] + #[kani::unwind(20)] + #[kani::stub( as ReverseSearcher<'_>>::next_match_back, verifier_stub_str_nonempty_next_match_back)] + fn harness_str_nonempty_reverse() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let mut needle_buf = [0u8; 8]; + let needle = any_short_needle(&mut needle_buf); + assert_str_pattern_direction(s, needle, true); + kani::cover(needle.len() == 1, "str pattern reverse: byte searcher"); + kani::cover( + needle.len() > 4, + "str pattern reverse: two multibyte scalars", + ); + kani::cover(true, "C22-END: harness_str_nonempty_reverse completed"); + } + + // Independent streaming decoder for checking the local input predicate. + // Its state is the expected continuation count and permitted next byte; + // unlike the local predicate it does not inspect overlapping windows. + fn reference_utf8_valid(bytes: &[u8]) -> bool { + let mut pending = 0usize; + let mut low = 0x80; + let mut high = 0xBF; + // Index traversal keeps this reference independent of slice iterator + // pointer models. No encoding constraint is assumed in this loop. + let mut index = 0usize; + while index < bytes.len() { + let byte = bytes[index]; + index += 1; + if pending > 0 { + if byte < low || byte > high { + return false; + } + pending -= 1; + low = 0x80; + high = 0xBF; + } else { + match byte { + 0..=0x7F => {} + 0xC2..=0xDF => pending = 1, + 0xE0 => { + pending = 2; + low = 0xA0; + } + 0xE1..=0xEC | 0xEE..=0xEF => pending = 2, + 0xED => { + pending = 2; + high = 0x9F; + } + 0xF0 => { + pending = 3; + low = 0x90; + } + 0xF1..=0xF3 => pending = 3, + 0xF4 => { + pending = 3; + high = 0x8F; + } + _ => return false, + } + } + } + pending == 0 + } + + // No UTF-8 validity filter: raw bytes include all invalid encodings. + // This checks both soundness and completeness of the local predicate + // against an independent streaming decoder throughout the largest + // allocation used by these proofs. It is not an arbitrary-N theorem. + #[kani::proof] + #[kani::unwind(257)] + fn harness_utf8_input_model() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let len: usize = kani::any(); + // INPUT-LENGTH: selecting a prefix within this allocation, not + // assuming any encoding property or expected comparison result. + // INPUT DOMAIN: allocated prefix or index extent. + kani::assume(len <= MAX_BYTES); + kani::cover(true, "C22-A11: harness_utf8_input_model assumption admitted"); + let local = verifier_utf8_valid(&buf, len); + let reference = reference_utf8_valid(&buf[..len]); + assert_eq!(local, reference); + kani::cover(local && len == MAX_BYTES, "UTF-8 model: full valid input"); + kani::cover( + !local && len == MAX_BYTES, + "UTF-8 model: rejects invalid input", + ); + kani::cover(local && len == 0, "UTF-8 model: empty input"); + kani::cover( + !local && len == 1 && buf[0] == 0xF0, + "UTF-8 model: truncated scalar", + ); + kani::cover( + local && len == 4 && buf[0] == 0xF4, + "UTF-8 model: largest scalar block", + ); + kani::cover(true, "C22-END: harness_utf8_input_model completed"); + } + + // Local safety lemmas for advance_by. These establish the obligations + // of one loop step only; the production loops are not contracted or + // replaced, so these are NOT an unbounded proof of advance_by. + #[kani::proof] + #[kani::unwind(33)] + fn harness_advance_chunk_step() { + let chunk: [u8; 32] = kani::any(); + let total_len: usize = kani::any(); + let skipped: usize = kani::any(); + let remainder: usize = kani::any(); + // LOCAL LEMMA: input precondition, not a proved production invariant. + kani::assume(skipped <= total_len && 32 <= total_len - skipped); + kani::cover(true, "C22-A12: harness_advance_chunk_step assumption admitted"); + // LOCAL LEMMA: input precondition, not a proved production invariant. + kani::assume(remainder > 32); + kani::cover(true, "C22-A13: harness_advance_chunk_step assumption admitted"); + let mut starts = [false; 32]; + for i in 0..32 { + starts[i] = !utf8_is_cont_byte(chunk[i]); + } + let count = starts.into_iter().map(|x| x as u8).sum::() as usize; + assert!(count <= 32); + assert!(count < remainder); + assert!(skipped + 32 <= total_len); + assert!(remainder - count > 0); + kani::cover(count == 32, "chunk step: all start bytes"); + kani::cover( + count == 0, + "chunk step: conservative invalid-byte over-approximation", + ); + kani::cover(true, "C22-END: harness_advance_chunk_step completed"); + } + + #[kani::proof] + fn harness_advance_character_step() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let (start, end) = verifier_nondet_window(s); + // LOCAL LEMMA: input precondition, not a proved production invariant. + kani::assume(start < end); + kani::cover(true, "C22-A14: harness_advance_character_step assumption admitted"); + let width = utf8_char_width(s.as_bytes()[start]); + assert!(1 <= width && width <= 4); + assert!(width <= end - start); + assert!(s.is_char_boundary(start + width)); + let mut bytes = s.as_bytes()[start..end].iter(); + assert!(bytes.advance_by(width).is_ok()); + assert_eq!(bytes.len(), end - start - width); + kani::cover(width == 4, "character step: four-byte scalar"); + kani::cover(true, "C22-END: harness_advance_character_step completed"); + } + + #[kani::proof] + #[kani::unwind(4)] + fn harness_advance_boundary_restore() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let pos: usize = kani::any(); + // INPUT DOMAIN: allocated prefix or index extent. + kani::assume(pos <= s.len()); + kani::cover(true, "C22-A15: harness_advance_boundary_restore assumption admitted"); + let mut iter = s.as_bytes()[pos..].iter(); + let mut skipped = 0usize; + while let Some(&byte) = iter.as_slice().first() { + if !utf8_is_cont_byte(byte) { + break; + } + assert!(iter.advance_by(1).is_ok()); + skipped += 1; + } + assert!(skipped <= 3); + assert!(s.is_char_boundary(pos + skipped)); + kani::cover(skipped == 3, "boundary restore: three continuation bytes"); + kani::cover(skipped == 0, "boundary restore: already aligned"); + kani::cover(true, "C22-END: harness_advance_boundary_restore completed"); + } + // Count-gap regression on a fixed chunk or an empty string. A symbolic + // window made CBMC duplicate the unreachable chunk loop and exceeded the + // 480-second budget. This does not cover every length/window for n=9..32. + #[kani::proof] + #[kani::unwind(34)] + fn harness_chars_advance_by_medium() { + const BYTES: usize = 32; + let buf: [u8; BYTES + UTF8_PAD] = kani::any(); + // CHALLENGE 22 assumption 4: valid UTF-8 input. + kani::assume(verifier_utf8_valid(&buf, BYTES)); + kani::cover(true, "C22-A16: harness_chars_advance_by_medium assumption admitted"); + // SAFETY: the local predicate establishes this fixed prefix's UTF-8. + let s = unsafe { from_utf8_unchecked(&buf[..BYTES]) }; + let n: usize = kani::any(); + // INPUT DOMAIN: this bounded request partition only. + kani::assume(9 <= n && n <= 32); + kani::cover(true, "C22-A17: harness_chars_advance_by_medium assumption admitted"); + let empty: bool = kani::any(); + if empty { + verifier_check_chars_advance("", 0, 0, n); + } else { + verifier_check_chars_advance(s, 0, BYTES, n); + } + kani::cover(n == 32 && !empty, "advance_by: threshold count"); + kani::cover(empty, "advance_by: large count on empty input"); + kani::cover(true, "C22-END: harness_chars_advance_by_medium completed"); + } + + // Exhaust two full chunks for any request larger than their byte count, + // including usize::MAX. Only the allocation length is fixed here. The + // reference counts UTF-8 leading bytes, independently of chunk grouping; + // there is no character-decoding reference loop proportional to n. + // Requests 41..=64 have a separate fixed-size rank-reference proof below. + // Arbitrary allocation lengths are not covered here. + #[kani::proof] + #[kani::unwind(66)] + fn harness_chars_advance_by_multichunk() { + const BYTES: usize = 64; + let buf: [u8; BYTES + UTF8_PAD] = kani::any(); + // CHALLENGE 22 assumption 4: valid UTF-8 input. + kani::assume(verifier_utf8_valid(&buf, BYTES)); + kani::cover(true, "C22-A18: harness_chars_advance_by_multichunk assumption admitted"); + // SAFETY: the local predicate establishes this fixed prefix's UTF-8. + let s = unsafe { from_utf8_unchecked(&buf[..BYTES]) }; + let n: usize = kani::any(); + // INPUT DOMAIN: this bounded request partition only. + kani::assume(n > BYTES); + kani::cover(true, "C22-A19: harness_chars_advance_by_multichunk assumption admitted"); + let mut iter = s.chars(); + let result = iter.advance_by(n); + verifier_assert_str_range(s, iter.as_str(), BYTES, BYTES); + let mut chars = 0usize; + for i in 0..BYTES { + chars += (!utf8_is_cont_byte(buf[i])) as usize; + } + assert!(16 <= chars && chars <= BYTES); + let remaining = result.unwrap_err().get(); + assert_eq!(remaining, n - chars); + kani::cover(n == usize::MAX, "advance_by: maximum request"); + kani::cover(chars == 64, "advance_by: two ASCII chunks"); + kani::cover(chars == 16, "advance_by: two chunks of four-byte scalars"); + kani::cover( + utf8_is_cont_byte(buf[32]), + "advance_by: second chunk starts inside a scalar", + ); + kani::cover(true, "C22-END: harness_chars_advance_by_multichunk completed"); + } + + // A byte-rank oracle, independent of advance_by's chunk grouping and + // continuation-restoration loop. On valid UTF-8, leading-byte rank is + // scalar rank. Locate the first boundary whose rank equals the request; + // if there is none, the expected residual string is empty. This oracle + // has a fixed allocation bound, even when n ranges over all usize values. + fn assert_advance_by_rank(buf: &[u8; N], n: usize) -> (usize, usize, usize) { + let len = N - UTF8_PAD; + // CHALLENGE 22 assumption 4: valid UTF-8 input. + kani::assume(verifier_utf8_valid(buf, len)); + kani::cover(true, "C22-A20: assert_advance_by_rank assumption admitted"); + // SAFETY: the exact local predicate constrains the whole prefix. + let s = unsafe { from_utf8_unchecked(&buf[..len]) }; + let mut rank = 0usize; + let mut expected = len; + let mut first_chunk = 0usize; + let mut first_two_chunks = 0usize; + // Six verification blocks of 16 suffice for the largest input. + // This visits every byte once; it does not summarize counts per + // production chunk. A short inner loop allows a common unwind of + // 34, instead of expanding the target's scalar tail 98 times. + for block in 0..len.div_ceil(16) { + for offset in 0..16 { + let i = block * 16 + offset; + if i >= len { + break; + } + if i == 32 { + first_chunk = rank; + } + if i == 64 { + first_two_chunks = rank; + } + if !utf8_is_cont_byte(buf[i]) { + if rank == n { + expected = i; + } + rank += 1; + } + } + } + let mut iter = s.chars(); + let result = iter.advance_by(n); // real production body, no stubs + verifier_assert_str_range(s, iter.as_str(), expected, len); + if n <= rank { + assert!(result.is_ok()); + } else { + assert_eq!(result.unwrap_err().get(), n - rank); + } + kani::cover(result.is_ok(), "rank oracle: successful skip"); + kani::cover(result.is_err(), "rank oracle: exact missing scalar count"); + (expected, first_chunk, first_two_chunks) + } + + // Fill the request-count gap with an arbitrary valid 64-byte prefix. + // Both success and shortage are checked, rather than constraining the + // needle/request by an assumed postcondition on the production iterator. + #[kani::proof] + #[kani::unwind(34)] + fn harness_chars_advance_by_count_gap() { + let buf: [u8; 64 + UTF8_PAD] = kani::any(); + let n: usize = kani::any(); + // INPUT DOMAIN: this bounded request partition only. + kani::assume(41 <= n && n <= 64); + kani::cover(true, "C22-A21: harness_chars_advance_by_count_gap assumption admitted"); + let (end, _, _) = assert_advance_by_rank(&buf, n); + kani::cover(n == 41 && end < 64, "count gap: lower request retains tail"); + kani::cover(n == 64, "count gap: upper request"); + kani::cover( + utf8_is_cont_byte(buf[32]), + "count gap: restore chunk boundary", + ); + kani::cover(true, "C22-END: harness_chars_advance_by_count_gap completed"); + } + + // n > 64 forces at least two 32-byte scans: a chunk contains at most + // 32 leading bytes. Unlike the exhaustion regression, this input also + // permits a successful skip with a nonempty residual string. The rank + // covers establish that the chunk loop exits after exactly two scans, + // then restores a boundary and consumes a positive scalar remainder. + #[kani::proof] + // The real tail has at most 32 bytes after two scans. Keep unwinding + // assertions enabled to check this bound as well as the reference loops. + #[kani::unwind(34)] + fn harness_chars_advance_by_multichunk_tail() { + let buf: [u8; 96 + UTF8_PAD] = kani::any(); + let n: usize = kani::any(); + // INPUT DOMAIN: this bounded request partition only. + kani::assume(65 <= n && n <= 96); + kani::cover(true, "C22-A22: harness_chars_advance_by_multichunk_tail assumption admitted"); + let (end, first, first_two) = assert_advance_by_rank(&buf, n); + let two_scans = n - first > 32 && n - first_two <= 32; + kani::cover(two_scans && end < 96, "multi chunk: two scans retain tail"); + kani::cover( + two_scans && end < 96 && utf8_is_cont_byte(buf[64]), + "multi chunk: restore boundary then retain tail", + ); + kani::cover( + n - first_two > 32 && end == 96, + "multi chunk: third scan exhausts input", + ); + kani::cover(n == 96, "multi chunk: upper request"); + kani::cover(true, "C22-END: harness_chars_advance_by_multichunk_tail completed"); + } + + // Check the state generator separately. This asserts consequences of + // its input bounds; no invariant or post-target property is assumed. + #[kani::proof] + fn harness_split_state_generator() { + let buf: [u8; BUFFER_BYTES] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let iter = any_split(s); + assert!(type_invariant_split(&iter)); + assert!(verifier_same_slice(s, iter.matcher.haystack())); + assert_eq!(iter.matcher.calls, 0); + assert!(iter.matcher.last_match.is_none()); + assert!(iter.matcher.previous_match.is_none()); + kani::cover( + iter.finished && iter.start < iter.end, + "state generator: finished nonempty interval", + ); + kani::cover( + !iter.finished && iter.start == iter.end, + "state generator: active empty interval", + ); + kani::cover(true, "C22-END: harness_split_state_generator completed"); + } + + // Challenge assumption 1 supplies the functional correctness of slice + // byte search. This deterministic model implements its exact last-match + // definition, not a nondeterministic return-range assumption. In particular + // None is returned only after every byte has been checked. + fn verifier_last_byte(needle: u8, bytes: &[u8]) -> Option { + let mut index = bytes.len(); + while index > 0 { + index -= 1; + if bytes[index] == needle { + return Some(index); + } + } + None + } + + // Check the leaf model against the complete last-index specification on + // arbitrary raw prefixes, including non-UTF-8 data and the empty slice. + #[kani::proof] + #[kani::unwind(20)] + fn harness_reverse_byte_model() { + let bytes: [u8; 16] = kani::any(); + let len: usize = kani::any(); + // INPUT-LENGTH: only prefixes of this initialized array are inputs. + // INPUT DOMAIN: allocated prefix or index extent. + kani::assume(len <= bytes.len()); + kani::cover(true, "C22-A23: harness_reverse_byte_model assumption admitted"); + let needle: u8 = kani::any(); + let result = verifier_last_byte(needle, &bytes[..len]); + if let Some(index) = result { + assert!(index < len); + assert_eq!(bytes[index], needle); + } + for index in 0..len { + if result.is_none_or(|last| last < index) { + assert_ne!(bytes[index], needle); + } + } + kani::cover(result.is_some(), "byte model: matching byte"); + kani::cover(result.is_none(), "byte model: no match"); + kani::cover( + len > 0 && result == Some(len - 1), + "byte model: final byte matches", + ); + kani::cover(len == 0 && result.is_none(), "byte model: empty prefix"); + kani::cover(true, "C22-END: harness_reverse_byte_model completed"); + } + + // Bounded inclusion evidence for the hand-written char adapters. Keep + // the directions separate to avoid combining both search circuits; their + // union covers the original arbitrary-direction input domain. + fn assert_char_searcher_direction(reverse: bool) { + let buf: [u8; 16 + UTF8_PAD] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let (front, back) = verifier_nondet_window(s); + let needle: char = kani::any(); + let result = verifier_assert_real_char_searcher(s, needle, front, back, reverse); + kani::cover(result.is_some(), "real char search: matching scalar"); + kani::cover(result.is_none(), "real char search: exhausted window"); + kani::cover( + result.is_some() && needle.len_utf8() == 4, + "real char search: four-byte match", + ); + kani::cover( + front == back && result.is_none(), + "real char search: empty window", + ); + } + + // The byte window has at most 16 bytes. Every failed candidate consumes + // a byte, so 18 includes the final exhaustion call and loop-exit check. + #[kani::proof] + #[kani::unwind(18)] + fn harness_char_searcher_forward_refinement() { + assert_char_searcher_direction(false); + kani::cover(true, "C22-END: harness_char_searcher_forward_refinement completed"); + } + + // Neither CharSearcher method is stubbed. Only the reverse slice byte + // leaf uses the exact deterministic model under challenge assumption 1. + #[kani::proof] + #[kani::unwind(18)] + #[kani::stub(crate::slice::memchr::memrchr, verifier_last_byte)] + fn harness_char_searcher_reverse_refinement() { + assert_char_searcher_direction(true); + kani::cover(true, "C22-END: harness_char_searcher_reverse_refinement completed"); + } + + // Independent rank check for any caller-supplied UTF-8 window. The + // caller's allocation bound is asserted, not silently assumed here. + // A u16 counter covers all 256 bytes without truncating character counts. + // No search, advance, or result property is assumed in this reference. + fn assert_advance_by_window_rank( + s: &str, + start: usize, + end: usize, + n: usize, + ) -> (usize, usize) { + assert!(s.len() <= MAX_BYTES); + assert!(start <= end && end <= s.len()); + assert!(s.is_char_boundary(start) && s.is_char_boundary(end)); + let mut iter = s[start..end].chars(); + let result = iter.advance_by(n); // real target, no stubs + let remaining = iter.as_str(); + let position = verifier_slice_offset(s, remaining); + assert!(start <= position && position <= end); + verifier_assert_str_range(s, remaining, position, end); + + // Independently rank the returned boundary. Every UTF-8 boundary + // has a unique scalar rank, so this characterizes the exact suffix + // without selecting an expected pointer once for every input byte. + let mut total = 0u16; + let mut consumed = 0u16; + let len = end - start; + for block in 0..len.div_ceil(16) { + for offset in 0..16 { + let local = block * 16 + offset; + if local >= len { + break; + } + let index = start + local; + if !utf8_is_cont_byte(s.as_bytes()[index]) { + total += 1; + if index < position { + consumed += 1; + } + } + } + } + let count = usize::from(total); + assert!(count <= len); + assert_eq!(usize::from(consumed), n.min(count)); + if n <= count { + assert!(result.is_ok()); + } else { + assert_eq!(result.unwrap_err().get(), n - count); + } + (position, count) + } + + // Full usize request domain, including zero and usize::MAX. Only the + // initialized backing object and valid UTF-8 origin bound the input. + // After chunk scanning the real scalar tail needs at most 32 iterations; + // the reference's 16-byte blocks do not force a byte-length global bound. + #[kani::proof] + #[kani::unwind(34)] + fn harness_chars_advance_by_all_counts() { + const BYTES: usize = 40; + let buf: [u8; BYTES + UTF8_PAD] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let n: usize = kani::any(); + let (position, _) = assert_advance_by_window_rank(s, 0, s.len(), n); + kani::cover(n == 0 && !s.is_empty(), "all counts: zero request"); + kani::cover( + n == 32 && position < s.len(), + "all counts: threshold retains tail", + ); + kani::cover( + n == 33 && s.len() >= 36 + && !s.is_char_boundary(32) + && !s.is_char_boundary(33) + && !s.is_char_boundary(34) + && position < s.len(), + "all counts: three continuation bytes then scalar tail", + ); + kani::cover( + n == usize::MAX && s.len() == BYTES, + "all counts: maximum usize nonempty input", + ); + kani::cover( + s.len() == BYTES && n == BYTES + 1 && position == s.len(), + "all counts: byte capacity plus one shortage", + ); + kani::cover(true, "C22-END: harness_chars_advance_by_all_counts completed"); + } + + // A distinct large-allocation domain: every 256-byte UTF-8 string and + // every request above 256. This explicit request range is not a + // postcondition assumption or a claim about requests 0..=256. + #[kani::proof] + #[kani::unwind(34)] + fn harness_chars_advance_by_eight_chunks() { + const BYTES: usize = 256; + let buf: [u8; BYTES + UTF8_PAD] = kani::any(); + // CHALLENGE 22 assumption 4: valid UTF-8 input. + kani::assume(verifier_utf8_valid(&buf, BYTES)); + kani::cover(true, "C22-A24: harness_chars_advance_by_eight_chunks assumption admitted"); + // SAFETY: the input predicate specifies a valid UTF-8 origin. + let s = unsafe { from_utf8_unchecked(&buf[..BYTES]) }; + let n: usize = kani::any(); + // INPUT DOMAIN: this bounded request partition only. + kani::assume(n > BYTES); + kani::cover(true, "C22-A25: harness_chars_advance_by_eight_chunks assumption admitted"); + // Independent 16-byte counting blocks keep the reference's adder + // chains smaller than a 256-step sum. The real target scans 32-byte + // chunks. Every local upper bound below is checked, never assumed. + let mut rank = 0u16; + for block in 0..BYTES / 16 { + let mut in_block = 0u8; + for offset in 0..16 { + let index = block * 16 + offset; + in_block += u8::from(!utf8_is_cont_byte(s.as_bytes()[index])); + assert!(usize::from(in_block) <= offset + 1); + } + rank += u16::from(in_block); + assert!(usize::from(rank) <= (block + 1) * 16); + } + let count = usize::from(rank); + let mut iter = s.chars(); + let result = iter.advance_by(n); // real target, no stubs + verifier_assert_str_range(s, iter.as_str(), BYTES, BYTES); + assert!(result.is_err()); + assert_eq!(result.unwrap_err().get(), n - count); + kani::cover(n == BYTES + 1, "eight chunks: minimum request"); + kani::cover(n == usize::MAX, "eight chunks: maximum usize request"); + kani::cover(count == BYTES, "eight chunks: 256 ASCII scalars"); + kani::cover(count == BYTES / 4, "eight chunks: all four-byte scalars"); + kani::cover(true, "C22-END: harness_chars_advance_by_eight_chunks completed"); + } + + // An independently computed byte-prefix rank table. Checked local + // UTF-8 step facts expose the relation between a boundary and its next + // scalar before the real target runs; they are not assumptions or stubs. + fn assert_advance_by_block_rank(s: &str, n: usize) -> (usize, usize) { + assert!(CAP <= MAX_BYTES && s.len() <= CAP); + let mut ranks = [0u16; MAX_BYTES + 1]; + for block in 0..CAP.div_ceil(16) { + for offset in 0..16 { + let index = block * 16 + offset; + if index >= s.len() { + break; + } + ranks[index + 1] = ranks[index] + + u16::from(!utf8_is_cont_byte(s.as_bytes()[index])); + assert!(usize::from(ranks[index + 1]) <= index + 1); + } + } + for block in 0..CAP.div_ceil(16) { + for offset in 0..16 { + let index = block * 16 + offset; + if index >= s.len() { + break; + } + if s.is_char_boundary(index) { + let width = utf8_char_width(s.as_bytes()[index]) as usize; + assert!(width > 0 && width <= 4 && width <= s.len() - index); + assert!(s.is_char_boundary(index + width)); + assert_eq!(ranks[index + width], ranks[index] + 1); + } + } + } + + let count = usize::from(ranks[s.len()]); + let mut iter = s.chars(); + let result = iter.advance_by(n); // real target, no stubs + let remaining = iter.as_str(); + let position = verifier_slice_offset(s, remaining); + assert!(position <= s.len()); + verifier_assert_str_range(s, remaining, position, s.len()); + assert_eq!(usize::from(ranks[position]), n.min(count)); + if n <= count { + assert!(result.is_ok()); + } else { + assert_eq!(result.unwrap_err().get(), n - count); + } + (position, count) + } + + // Complement the retained 0..=40-byte complete-request proof with + // explicitly new extents. The guard selects an input length domain; + // no request or target-output condition is used as a filter. + #[kani::proof] + #[kani::unwind(34)] + fn harness_chars_advance_by_extended_counts() { + const BYTES: usize = 48; + let buf: [u8; BYTES + UTF8_PAD] = kani::any(); + let s = verifier_nondet_utf8(&buf); + if s.len() <= 40 { + return; + } + let n: usize = kani::any(); + let (position, _) = assert_advance_by_window_rank(s, 0, s.len(), n); + kani::cover( + n == 41 && s.len() == BYTES - 1 && position < s.len(), + "extended counts: new length and request retain tail", + ); + kani::cover( + n == 33 && s.len() == BYTES + && !s.is_char_boundary(32) + && !s.is_char_boundary(33) + && !s.is_char_boundary(34) + && position < s.len(), + "extended counts: three continuation bytes then scalar tail", + ); + kani::cover( + n == BYTES + 1 && s.len() == BYTES && position == s.len(), + "extended counts: exact shortage beyond byte capacity", + ); + kani::cover(true, "C22-END: harness_chars_advance_by_extended_counts completed"); + } + + // A bounded view constructor, not a filter on iterator outputs. Any + // desired boundary window of at most LIMIT bytes is represented by + // choosing that same window before this constructor (it is unchanged). + fn verifier_utf8_prefix(s: &str) -> &str { + let mut end = s.len().min(LIMIT); + for _ in 0..3 { + if s.is_char_boundary(end) { + break; + } + assert!(end > 0); + end -= 1; + } + assert!(end <= LIMIT && end <= s.len()); + assert!(s.is_char_boundary(end)); + &s[..end] + } + + #[kani::proof] + #[kani::unwind(34)] + fn harness_chars_advance_by_window_rank() { + const BYTES: usize = 256; + const WINDOW_BYTES: usize = 8; + let buf: [u8; BYTES + UTF8_PAD] = kani::any(); + let s = verifier_nondet_utf8(&buf); + let (front, back) = verifier_nondet_window(s); + let selected = &s[front..back]; + let view = verifier_utf8_prefix::(selected); + verifier_assert_str_range(s, view, front, front + view.len()); + let n: usize = kani::any(); + let (position, _) = assert_advance_by_block_rank::(view, n); + assert!(front + position <= back); + kani::cover( + s.len() == BYTES && front > 0 && back < s.len() + && n == 7 && position < view.len(), + "window rank: interior large-allocation success", + ); + kani::cover( + s.len() == BYTES && front > 0 && front + view.len() < s.len() + && !view.is_empty() && n == usize::MAX, + "window rank: maximum request ends inside parent allocation", + ); + kani::cover( + view.is_empty() && front > 0 && front < s.len() && n > 0, + "window rank: empty interior shortage", + ); + kani::cover( + selected.len() > WINDOW_BYTES && view.len() + 3 == WINDOW_BYTES, + "window rank: view limit crosses three continuation bytes", + ); + kani::cover(true, "C22-END: harness_chars_advance_by_window_rank completed"); + } +} diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index ee6fd26ca0bfe..505bc32dbac3c 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -2116,20 +2116,34 @@ pub mod verify { let y: [u8; ARR_SIZE] = kani::any(); let xs = kani::slice::any_slice_of_array(&x); let ys = kani::slice::any_slice_of_array(&y); + // UNSAFE PRECONDITION: required by the operation under test. kani::assume(xs.len() == ys.len()); + kani::cover(true, "C22-A26: check_small_slice_eq assumption admitted"); unsafe { small_slice_eq(xs, ys); } + kani::cover(true, "C22-END: check_small_slice_eq completed"); } #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86 #[kani::proof] #[kani::unwind(4)] pub fn check_small_slice_eq_empty() { - let ptr_x = kani::any_where::(|val| *val != 0) as *const u8; - let ptr_y = kani::any_where::(|val| *val != 0) as *const u8; - kani::assume(ptr_x.is_aligned()); - kani::assume(ptr_y.is_aligned()); + // Zero-length raw slices still require non-null pointers. Make the + // former any_where filters explicit so each has a coverage witness. + let address_x: usize = kani::any(); + // UNSAFE PRECONDITION: required by the operation under test. + kani::assume(address_x != 0); + kani::cover(true, "C22-A27: check_small_slice_eq_empty assumption admitted"); + let address_y: usize = kani::any(); + // UNSAFE PRECONDITION: required by the operation under test. + kani::assume(address_y != 0); + kani::cover(true, "C22-A28: check_small_slice_eq_empty assumption admitted"); + let ptr_x = address_x as *const u8; + let ptr_y = address_y as *const u8; + // u8 has alignment one; prove this instead of filtering inputs. + assert!(ptr_x.is_aligned()); + assert!(ptr_y.is_aligned()); assert_eq!( unsafe { small_slice_eq( @@ -2139,5 +2153,318 @@ pub mod verify { }, true ); + kani::cover(true, "C22-END: check_small_slice_eq_empty completed"); + } + + // Challenge 22: specifications for the permitted `str::pattern` assumption. + // These helpers are inside `str::pattern::verify`, not production code. + // Iterator harnesses stub only the explicitly annotated directional search + // operations; all real production bodies remain unchanged. These are + // manual safety abstractions under assumption 2, not stub_verified proofs. + // The simulation relation is observational: iter.rs reads haystack and + // match intervals, not search-algorithm preprocessing or equality state. + // See doc/src/verification/challenge-22-coverage.md for each adapter's + // admitted returns, frame conditions, progress, and proof obligations. + + pub fn verifier_char_searcher_invariant(searcher: &CharSearcher<'_>) -> bool { + let haystack = searcher.haystack; + let mut encoded = [0u8; 4]; + let width = searcher.needle.encode_utf8(&mut encoded).len(); + searcher.finger <= searcher.finger_back + && searcher.finger_back <= haystack.len() + && haystack.is_char_boundary(searcher.finger) + && haystack.is_char_boundary(searcher.finger_back) + && searcher.utf8_size() == width + && searcher.utf8_encoded[0] == encoded[0] + && (width < 2 || searcher.utf8_encoded[1] == encoded[1]) + && (width < 3 || searcher.utf8_encoded[2] == encoded[2]) + && (width < 4 || searcher.utf8_encoded[3] == encoded[3]) + } + + // A real call is checked against the return/frame relation imported by + // the char stubs below. The caller selects a valid input window; assert + // that precondition instead of silently filtering it with kani::assume. + // The dedicated harness preserves both real CharSearcher methods; its + // reverse slice byte-search leaf uses an exact model under assumption 1. + pub fn verifier_assert_real_char_searcher( + haystack: &str, + needle: char, + front: usize, + back: usize, + reverse: bool, + ) -> Option<(usize, usize)> { + assert!(front <= back && back <= haystack.len()); + assert!(haystack.is_char_boundary(front) && haystack.is_char_boundary(back)); + let mut searcher = needle.into_searcher(haystack); + searcher.finger = front; + searcher.finger_back = back; + assert!(verifier_char_searcher_invariant(&searcher)); + let encoding = searcher.utf8_encoded; + let width = searcher.utf8_size; + let result = if reverse { + searcher.next_match_back() + } else { + searcher.next_match() + }; + assert!(verifier_char_searcher_invariant(&searcher)); + assert_eq!(searcher.haystack.as_ptr(), haystack.as_ptr()); + assert_eq!(searcher.haystack.len(), haystack.len()); + assert_eq!(searcher.needle, needle); + assert_eq!(searcher.utf8_size, width); + for i in 0..4 { + assert_eq!(searcher.utf8_encoded[i], encoding[i]); + } + if reverse { + assert_eq!(searcher.finger, front); + } else { + assert_eq!(searcher.finger_back, back); + } + match result { + Some((a, b)) => { + assert!(front <= a && a < b && b <= back); + assert_eq!(b - a, needle.len_utf8()); + assert!(haystack.is_char_boundary(a) && haystack.is_char_boundary(b)); + let mut matched = haystack[a..b].chars(); + assert_eq!(matched.next(), Some(needle)); + assert!(matched.next().is_none()); + if reverse { + assert_eq!(searcher.finger_back, a); + } else { + assert_eq!(searcher.finger, b); + } + } + None => assert_eq!(searcher.finger, searcher.finger_back), + } + result + } + + // This over-approximates Searcher::next_match under Challenge 22 + // assumption 2: either no match remains, or a needle-width boundary + // range lies between the current search frontiers. This may admit a + // sequence of shorter scalars, an intentional safety over-approximation. + // We do not assume the match actually equals the needle, so the model + // admits at least the real searcher's possible returns. + pub fn verifier_stub_char_next_match<'a: 'a>( + searcher: &mut CharSearcher<'a>, + ) -> Option<(usize, usize)> { + assert!(verifier_char_searcher_invariant(searcher)); + let found: bool = kani::any(); + if !found { + searcher.finger = searcher.finger_back; + return None; + } + let start: usize = kani::any(); + let width = searcher.needle.len_utf8(); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(searcher.finger <= start && start <= searcher.finger_back); + kani::cover(true, "C22-A29: verifier_stub_char_next_match assumption admitted"); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(width <= searcher.finger_back - start); + kani::cover(true, "C22-A30: verifier_stub_char_next_match assumption admitted"); + let end = start + width; + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume( + searcher.haystack.is_char_boundary(start) && searcher.haystack.is_char_boundary(end), + ); + kani::cover(true, "C22-A31: verifier_stub_char_next_match assumption admitted"); + searcher.finger = end; + assert!(verifier_char_searcher_invariant(searcher)); + Some((start, end)) + } + + // ReverseSearcher::next_match_back: same permitted abstraction, with + // the opposite search frontier moved to the beginning of the match. + pub fn verifier_stub_char_next_match_back<'a: 'a>( + searcher: &mut CharSearcher<'a>, + ) -> Option<(usize, usize)> { + assert!(verifier_char_searcher_invariant(searcher)); + let found: bool = kani::any(); + if !found { + searcher.finger_back = searcher.finger; + return None; + } + let start: usize = kani::any(); + let width = searcher.needle.len_utf8(); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(searcher.finger <= start && start <= searcher.finger_back); + kani::cover(true, "C22-A32: verifier_stub_char_next_match_back assumption admitted"); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(width <= searcher.finger_back - start); + kani::cover(true, "C22-A33: verifier_stub_char_next_match_back assumption admitted"); + let end = start + width; + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume( + searcher.haystack.is_char_boundary(start) && searcher.haystack.is_char_boundary(end), + ); + kani::cover(true, "C22-A34: verifier_stub_char_next_match_back assumption admitted"); + searcher.finger_back = start; + assert!(verifier_char_searcher_invariant(searcher)); + Some((start, end)) + } + // Directional adapters for Challenge 22 assumption 2. They constrain + // returned ranges and the state consumed by iter.rs, not match contents. + // In particular StrSearcher has independent forward/reverse cursors: + // it must not inherit CharSearcher's shared-finger ordering invariant. + // None normalizes a cursor to an exhausted representative. Algorithm + // metadata is unobserved by iter.rs; these are not verified contracts for + // the real search bodies. Explicit self-bounded lifetimes match the + // early-bound generic parameters required by Kani's stub checker. + pub fn verifier_stub_str_next_match<'a: 'a, 'b: 'b>( + s: &mut StrSearcher<'a, 'b>, + ) -> Option<(usize, usize)> { + if s.needle.is_empty() { + // Empty-needle Match/Reject alternation needs at most two real + // steps. Retain its actual phase, UTF-8 decoding and exhaustion. + return match s.next() { + SearchStep::Match(a, b) => Some((a, b)), + SearchStep::Done => None, + SearchStep::Reject(..) => match s.next() { + SearchStep::Match(a, b) => Some((a, b)), + SearchStep::Done => None, + SearchStep::Reject(..) => unreachable!("empty needle alternates"), + }, + }; + } + verifier_stub_str_nonempty_next_match(s) + } + + pub fn verifier_stub_str_next_match_back<'a: 'a, 'b: 'b>( + s: &mut StrSearcher<'a, 'b>, + ) -> Option<(usize, usize)> { + if s.needle.is_empty() { + return match s.next_back() { + SearchStep::Match(a, b) => Some((a, b)), + SearchStep::Done => None, + SearchStep::Reject(..) => match s.next_back() { + SearchStep::Match(a, b) => Some((a, b)), + SearchStep::Done => None, + SearchStep::Reject(..) => unreachable!("empty needle alternates"), + }, + }; + } + verifier_stub_str_nonempty_next_match_back(s) + } + + // Nonempty-only entry keeps the Empty branch's real next() out of + // this harness call graph; pattern algorithms remain assumed correct. + pub fn verifier_stub_str_nonempty_next_match<'a: 'a, 'b: 'b>( + s: &mut StrSearcher<'a, 'b>, + ) -> Option<(usize, usize)> { + assert!(!s.needle.is_empty()); + let front = match &s.searcher { + StrSearcherImpl::Byte(x) => x.position, + StrSearcherImpl::TwoWay(x) => x.position, + StrSearcherImpl::Empty(_) => unreachable!(), + }; + assert!(front <= s.haystack.len() && s.haystack.is_char_boundary(front)); + let result = + verifier_directional_match(s.haystack, front, s.haystack.len(), s.needle.len()); + let next = result.map_or(s.haystack.len(), |(_, b)| b); + match &mut s.searcher { + StrSearcherImpl::Byte(x) => x.position = next, + StrSearcherImpl::TwoWay(x) => x.position = next, + StrSearcherImpl::Empty(_) => unreachable!(), + } + result + } + + // Nonempty-only entry keeps the Empty branch's real next() out of + // this harness call graph; pattern algorithms remain assumed correct. + pub fn verifier_stub_str_nonempty_next_match_back<'a: 'a, 'b: 'b>( + s: &mut StrSearcher<'a, 'b>, + ) -> Option<(usize, usize)> { + assert!(!s.needle.is_empty()); + let back = match &s.searcher { + StrSearcherImpl::Byte(x) => x.end, + StrSearcherImpl::TwoWay(x) => x.end, + StrSearcherImpl::Empty(_) => unreachable!(), + }; + assert!(back <= s.haystack.len() && s.haystack.is_char_boundary(back)); + let result = verifier_directional_match(s.haystack, 0, back, s.needle.len()); + let next = result.map_or(0, |(a, _)| a); + match &mut s.searcher { + StrSearcherImpl::Byte(x) => x.end = next, + StrSearcherImpl::TwoWay(x) => x.end = next, + StrSearcherImpl::Empty(_) => unreachable!(), + } + result + } + + fn verifier_directional_match( + s: &str, + front: usize, + back: usize, + width: usize, + ) -> Option<(usize, usize)> { + if !kani::any::() { + return None; + } + let a: usize = kani::any(); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(front <= a && a <= back); + kani::cover(true, "C22-A35: verifier_directional_match assumption admitted"); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(width <= back - a); + kani::cover(true, "C22-A36: verifier_directional_match assumption admitted"); + let b = a + width; + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(s.is_char_boundary(a) && s.is_char_boundary(b)); + kani::cover(true, "C22-A37: verifier_directional_match assumption admitted"); + Some((a, b)) + } + + pub fn verifier_char_slice_position(s: &CharSliceSearcher<'_, '_>) -> (usize, usize) { + let front = s.0.char_indices.front_offset; + (front, front + s.0.char_indices.iter.iter.len()) + } + + fn verifier_stub_char_slice_match( + s: &mut CharSliceSearcher<'_, '_>, + reverse: bool, + ) -> Option<(usize, usize)> { + let (front, back) = verifier_char_slice_position(s); + let haystack = s.0.haystack; + assert!(front <= back && back <= haystack.len()); + assert!(haystack.is_char_boundary(front) && haystack.is_char_boundary(back)); + let result = if s.0.char_eq.is_empty() || !kani::any::() { + None + } else { + let a: usize = kani::any(); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(front <= a && a < back); + kani::cover(true, "C22-A38: verifier_stub_char_slice_match assumption admitted"); + // CHALLENGE 22 assumption 2: dependency Searcher range guarantee. + kani::assume(haystack.is_char_boundary(a)); + kani::cover(true, "C22-A39: verifier_stub_char_slice_match assumption admitted"); + // The real character width makes each result exactly one scalar, + // while the selected set element and equality are abstracted. + let width = super::super::validations::utf8_char_width(haystack.as_bytes()[a]); + assert!(width > 0 && width <= back - a); + let b = a + width; + assert!(haystack.is_char_boundary(b)); + Some((a, b)) + }; + let (new_front, new_back) = if reverse { + (front, result.map_or(front, |(a, _)| a)) + } else { + (result.map_or(back, |(_, b)| b), back) + }; + s.0.char_indices = super::super::CharIndices { + front_offset: new_front, + iter: haystack[new_front..new_back].chars(), + }; + result + } + + pub fn verifier_stub_char_slice_next_match<'a: 'a, 'b: 'b>( + s: &mut CharSliceSearcher<'a, 'b>, + ) -> Option<(usize, usize)> { + verifier_stub_char_slice_match(s, false) + } + + pub fn verifier_stub_char_slice_next_match_back<'a: 'a, 'b: 'b>( + s: &mut CharSliceSearcher<'a, 'b>, + ) -> Option<(usize, usize)> { + verifier_stub_char_slice_match(s, true) } }