From 30532315ca9f5c833d8a226eead9bb4c6072d786 Mon Sep 17 00:00:00 2001 From: hung1962003 <106923246+hung1962003@users.noreply.github.com> Date: Tue, 27 Oct 2026 08:34:25 +0000 Subject: [PATCH 1/7] Challenge 20: unbounded proofs for the char Searchers of str::pattern Prove next, next_match, next_back, next_match_back, next_reject and next_reject_back of CharSearcher, MultiCharEqSearcher and the four wrappers (CharArraySearcher, CharArrayRefSearcher, CharSliceSearcher, CharPredicateSearcher) for haystacks of symbolic length, without changing any method body. The loops of the provided Searcher methods and of CharSearcher::next_match{,_back} get loop invariants and a precise loop_modifies through a specialization hook (SearcherLoopContract), so that only the cursor is havocked. MultiCharEqSearcher::next/next_back get contracts, proved with proof_for_contract and used with stub_verified in the loops. The slice and UTF-8 decoding functions are modeled as the challenge allows, each model checked against upstream. Requires Kani with model-checking/kani#4947 and model-checking/kani#5071. Co-Authored-By: Claude Opus 5.5 --- library/core/src/slice/iter.rs | 17 + library/core/src/str/pattern.rs | 875 ++++++++++++++++++++++++++++++++ 2 files changed, 892 insertions(+) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 9e5a8338b8afc..525d92a14aa6e 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -168,6 +168,23 @@ impl AsRef<[T]> for Iter<'_, T> { } } +#[cfg(kani)] +impl Iter<'_, T> { + /// `(ptr, end_or_len)`, read without calls, for the contracts in + /// `str::pattern`. + pub(crate) fn kani_raw_parts(&self) -> (*const T, *const T) { + // SAFETY: `NonNull` is a transparent `*const T`. + (unsafe { mem::transmute::, *const T>(self.ptr) }, self.end_or_len) + } + + /// The same, for the loop invariants in `str::pattern`: a loop invariant + /// must not call a function that other code also calls. + pub(crate) fn kani_loop_raw_parts(&self) -> (*const T, *const T) { + // SAFETY: `NonNull` is a transparent `*const T`. + (unsafe { mem::transmute::, *const T>(self.ptr) }, self.end_or_len) + } +} + #[unstable(feature = "ub_checks", issue = "none")] impl Invariant for Iter<'_, T> { /// An iterator can be safely used if its pointer can be read for its current length. diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index ee6fd26ca0bfe..f91b8aef34280 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -53,6 +53,41 @@ use crate::kani; use crate::slice::memchr; use crate::{cmp, fmt}; +/// Loop contracts of the provided `Searcher` and `ReverseSearcher` methods, +/// which loop over `next` / `next_back` of an arbitrary searcher. A searcher +/// states its type invariant and the cursor each direction moves by +/// specializing this; the default keeps the whole searcher assignable. +#[cfg(kani)] +pub(crate) trait SearcherLoopContract { + /// The type invariant. Called from loop invariants only, so it uses casts + /// and intrinsics only: Kani gives a function that is also called from + /// ordinary code no write-set argument when an invariant calls it. + fn kani_inv(&self) -> bool; + /// The bytes a forward step (`next`) writes. + fn kani_fwd_cursor(&self) -> *const [u8]; + /// The bytes a backward step (`next_back`) writes. + fn kani_back_cursor(&self) -> *const [u8]; + /// The bytes of the pattern's own state that a step may write (a stateful + /// predicate). + fn kani_pred_state(&self) -> *const [u8]; +} + +#[cfg(kani)] +impl SearcherLoopContract for T { + default fn kani_inv(&self) -> bool { + true + } + default fn kani_fwd_cursor(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(self as *const T as *const u8, size_of_val(self)) + } + default fn kani_back_cursor(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(self as *const T as *const u8, size_of_val(self)) + } + default fn kani_pred_state(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(self as *const T as *const u8, 0) + } +} + // Pattern /// A string pattern. @@ -208,6 +243,20 @@ pub enum SearchStep { Done, } +/// For the step contracts of `MultiCharEqSearcher` (a replaced call returns +/// any value that the contract allows). +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +impl kani::Arbitrary for SearchStep { + fn any() -> Self { + match kani::any::() { + 0 => SearchStep::Match(kani::any(), kani::any()), + 1 => SearchStep::Reject(kani::any(), kani::any()), + _ => SearchStep::Done, + } + } +} + /// A searcher for a string pattern. /// /// This trait provides methods for searching for non-overlapping @@ -257,6 +306,14 @@ pub unsafe trait Searcher<'a> { /// the match begins, and end_match is the index after the end of the match. #[inline] fn next_match(&mut self) -> Option<(usize, usize)> { + #[cfg_attr( + kani, + kani::loop_modifies( + SearcherLoopContract::kani_fwd_cursor(&*self), + SearcherLoopContract::kani_pred_state(&*self) + ) + )] + #[safety::loop_invariant(SearcherLoopContract::kani_inv(&*self))] loop { match self.next() { SearchStep::Match(a, b) => return Some((a, b)), @@ -273,6 +330,14 @@ pub unsafe trait Searcher<'a> { /// of this and [`next_match`][Searcher::next_match] will overlap. #[inline] fn next_reject(&mut self) -> Option<(usize, usize)> { + #[cfg_attr( + kani, + kani::loop_modifies( + SearcherLoopContract::kani_fwd_cursor(&*self), + SearcherLoopContract::kani_pred_state(&*self) + ) + )] + #[safety::loop_invariant(SearcherLoopContract::kani_inv(&*self))] loop { match self.next() { SearchStep::Reject(a, b) => return Some((a, b)), @@ -325,6 +390,14 @@ pub unsafe trait ReverseSearcher<'a>: Searcher<'a> { /// See [`next_back()`][ReverseSearcher::next_back]. #[inline] fn next_match_back(&mut self) -> Option<(usize, usize)> { + #[cfg_attr( + kani, + kani::loop_modifies( + SearcherLoopContract::kani_back_cursor(&*self), + SearcherLoopContract::kani_pred_state(&*self) + ) + )] + #[safety::loop_invariant(SearcherLoopContract::kani_inv(&*self))] loop { match self.next_back() { SearchStep::Match(a, b) => return Some((a, b)), @@ -338,6 +411,14 @@ pub unsafe trait ReverseSearcher<'a>: Searcher<'a> { /// See [`next_back()`][ReverseSearcher::next_back]. #[inline] fn next_reject_back(&mut self) -> Option<(usize, usize)> { + #[cfg_attr( + kani, + kani::loop_modifies( + SearcherLoopContract::kani_back_cursor(&*self), + SearcherLoopContract::kani_pred_state(&*self) + ) + )] + #[safety::loop_invariant(SearcherLoopContract::kani_inv(&*self))] loop { match self.next_back() { SearchStep::Reject(a, b) => return Some((a, b)), @@ -408,6 +489,36 @@ impl CharSearcher<'_> { } } +#[cfg(kani)] +impl SearcherLoopContract for CharSearcher<'_> { + /// `finger <= finger_back <= haystack.len()`, both on char boundaries + /// (`str::len` and `str::is_char_boundary` spelled out). + fn kani_inv(&self) -> bool { + let p = self.haystack as *const str as *const u8; + let len: usize = crate::intrinsics::ptr_metadata(self.haystack as *const str); + let (f, fb) = (self.finger, self.finger_back); + // SAFETY: both reads are guarded by `< len`. + let f_ok = f == 0 + || f == len + || (f < len + && unsafe { *crate::intrinsics::arith_offset(p, f as isize) } as i8 >= -0x40); + let fb_ok = fb == 0 + || fb == len + || (fb < len + && unsafe { *crate::intrinsics::arith_offset(p, fb as isize) } as i8 >= -0x40); + f <= fb && fb <= len && f_ok && fb_ok + } + fn kani_fwd_cursor(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(&raw const self.finger as *const u8, size_of::()) + } + fn kani_back_cursor(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts( + &raw const self.finger_back as *const u8, + size_of::(), + ) + } +} + unsafe impl<'a> Searcher<'a> for CharSearcher<'a> { #[inline] fn haystack(&self) -> &'a str { @@ -442,6 +553,9 @@ unsafe impl<'a> Searcher<'a> for CharSearcher<'a> { } #[inline] fn next_match(&mut self) -> Option<(usize, usize)> { + // Within the loop `finger` may sit inside a character (see below). + #[cfg_attr(kani, kani::loop_modifies(&self.finger))] + #[safety::loop_invariant(self.finger <= self.finger_back)] loop { // get the haystack after the last character found let bytes = self.haystack.as_bytes().get(self.finger..self.finger_back)?; @@ -510,6 +624,10 @@ unsafe impl<'a> ReverseSearcher<'a> for CharSearcher<'a> { #[inline] fn next_match_back(&mut self) -> Option<(usize, usize)> { let haystack = self.haystack.as_bytes(); + // Within the loop `finger_back` may sit inside a character (see below). + #[cfg_attr(kani, kani::loop_modifies(&self.finger_back))] + #[safety::loop_invariant(self.finger <= self.finger_back + && self.finger_back <= crate::intrinsics::ptr_metadata(self.haystack as *const str))] loop { // get the haystack up to but not including the last character searched let bytes = haystack.get(self.finger..self.finger_back)?; @@ -691,6 +809,109 @@ impl Pattern for MultiCharEqPattern { } } +/// The type invariant `C` of `MultiCharEqSearcher` (and so of the four +/// searchers that wrap it): `char_indices` has exactly `haystack[front..back]` +/// left, with `front <= back <= haystack.len()` both on char boundaries. Casts +/// and intrinsics only, guarded so that it can be evaluated on any state; +/// `$parts` reads the fields of the byte iterator. +#[cfg(kani)] +macro_rules! multi_char_eq_inv { + ($s:expr, $parts:ident) => {{ + let s = $s; + let p = s.haystack as *const str as *const u8; + let len: usize = crate::intrinsics::ptr_metadata(s.haystack as *const str); + let f = s.char_indices.front_offset; + let (start, end) = s.char_indices.iter.iter.$parts(); + let b = (end as usize).wrapping_sub(p as usize); + // SAFETY: both reads are guarded by `< len`. + let f_ok = f == 0 + || f == len + || (f < len + && unsafe { *crate::intrinsics::arith_offset(p, f as isize) } as i8 >= -0x40); + let b_ok = b == 0 + || b == len + || (b < len + && unsafe { *crate::intrinsics::arith_offset(p, b as isize) } as i8 >= -0x40); + // SAFETY: `arith_offset` is a wrapping offset, never UB. + f <= b + && b <= len + && start == unsafe { crate::intrinsics::arith_offset(p, f as isize) } + && end == unsafe { crate::intrinsics::arith_offset(p, b as isize) } + && f_ok + && b_ok + }}; +} + +#[cfg(kani)] +impl MultiCharEqSearcher<'_, C> { + /// `C`, for the contracts of `next` / `next_back`. + fn kani_ok(&self) -> bool { + multi_char_eq_inv!(self, kani_raw_parts) + } + + /// A step returns a range in bounds and on char boundaries. + fn kani_step_ok(&self, step: SearchStep) -> bool { + match step { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + a <= b + && b <= self.haystack.len() + && self.haystack.is_char_boundary(a) + && self.haystack.is_char_boundary(b) + } + SearchStep::Done => true, + } + } +} + +#[cfg(kani)] +impl SearcherLoopContract for MultiCharEqSearcher<'_, C> { + fn kani_inv(&self) -> bool { + multi_char_eq_inv!(self, kani_loop_raw_parts) + } + fn kani_fwd_cursor(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts( + &raw const self.char_indices as *const u8, + size_of_val(&self.char_indices), + ) + } + fn kani_back_cursor(&self) -> *const [u8] { + self.kani_fwd_cursor() + } + default fn kani_pred_state(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, size_of::()) + } +} + +// A set of characters has no state of its own: `matches` only reads it. +#[cfg(kani)] +impl SearcherLoopContract for MultiCharEqSearcher<'_, [char; N]> { + fn kani_pred_state(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, 0) + } +} + +#[cfg(kani)] +impl SearcherLoopContract for MultiCharEqSearcher<'_, &[char; N]> { + fn kani_pred_state(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, 0) + } +} + +#[cfg(kani)] +impl SearcherLoopContract for MultiCharEqSearcher<'_, &[char]> { + fn kani_pred_state(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, 0) + } +} + +// Nor does a function pointer: a call through it does not write it. +#[cfg(kani)] +impl SearcherLoopContract for MultiCharEqSearcher<'_, fn(char) -> bool> { + fn kani_pred_state(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, 0) + } +} + unsafe impl<'a, C: MultiCharEq> Searcher<'a> for MultiCharEqSearcher<'a, C> { #[inline] fn haystack(&self) -> &'a str { @@ -698,6 +919,15 @@ unsafe impl<'a, C: MultiCharEq> Searcher<'a> for MultiCharEqSearcher<'a, C> { } #[inline] + #[cfg_attr( + kani, + kani::modifies( + SearcherLoopContract::kani_fwd_cursor(self), + SearcherLoopContract::kani_pred_state(self) + ) + )] + #[safety::requires(self.kani_ok())] + #[safety::ensures(|step| self.kani_ok() && self.kani_step_ok(*step))] fn next(&mut self) -> SearchStep { let s = &mut self.char_indices; // Compare lengths of the internal byte slice iterator @@ -718,6 +948,15 @@ unsafe impl<'a, C: MultiCharEq> Searcher<'a> for MultiCharEqSearcher<'a, C> { unsafe impl<'a, C: MultiCharEq> ReverseSearcher<'a> for MultiCharEqSearcher<'a, C> { #[inline] + #[cfg_attr( + kani, + kani::modifies( + SearcherLoopContract::kani_fwd_cursor(self), + SearcherLoopContract::kani_pred_state(self) + ) + )] + #[safety::requires(self.kani_ok())] + #[safety::ensures(|step| self.kani_ok() && self.kani_step_ok(*step))] fn next_back(&mut self) -> SearchStep { let s = &mut self.char_indices; // Compare lengths of the internal byte slice iterator @@ -2141,3 +2380,639 @@ pub mod verify { ); } } + +/// Challenge 20: unbounded proofs for `CharSearcher`, and for +/// `MultiCharEqSearcher` through its four wrappers. +/// +/// # Haystack +/// +/// Every harness runs on a haystack of symbolic length (up to the CBMC object +/// model, as in the accepted VecDeque solution) and arbitrary contents, with no +/// unwind bound: the loops are discharged by their loop contracts. UTF-8 +/// validity is never stated as a quantified property. `utf8_ok_at(i)` is the +/// local rule that every valid UTF-8 string satisfies at every position `i`, +/// and the harnesses assume it only where a position is consumed: where the +/// decoder starts (the decoder models below), and at the start of a match +/// that `next_match{,_back}` returns. Each assumption holds for every valid +/// haystack (assumption 3), so no execution on a valid haystack is lost. +/// +/// # Models +/// +/// * `next_code_point{,_reverse}` (assumption 2): assume the local rule where +/// the decode starts, then the upstream body with its helpers inlined. The +/// `unwrap_unchecked`s stay checked, so a decode that does not start on a +/// char boundary is still caught. `check_*_model_matches_upstream` shows the +/// models only add assumptions. +/// * `memchr` / `memrchr` (assumption 1): return a matching index, or `None`. +/// This allows more behaviors than the real functions (`None` while a match +/// exists, a match that is not the first/last), which is sound for safety. +/// * slice equality of bytes (assumption 1): a recursive byte comparison in +/// place of `compare_bytes`. `check_slice_eq_model_matches_upstream` shows it +/// returns what upstream returns. +/// * `<[char]>::contains` (assumption 1): any result. The searchers use only +/// this result, so a character set is never read and may have any size. +/// +/// # Predicates +/// +/// A predicate returns any result on every call, with no state of its own +/// (`fn(char) -> bool`) or with state that it writes on every call (`Toggle`). +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify_char_searcher { + use super::*; + use crate::slice::Iter; + use crate::str::validations::utf8_is_cont_byte; + + /// CBMC's object model: with `--object-bits 12` an object has 52 offset + /// bits. Same bound as the accepted VecDeque solution. It only excludes + /// allocations no real machine could back either. + const MAX_ALLOCATION_BYTES: usize = 1 << 48; + + unsafe extern "C" { + /// CBMC's `malloc` model (`-Z c-ffi`): `core` has no allocator, and a + /// fixed-size array this large cannot be flattened. + fn malloc(size: usize) -> *mut u8; + } + + /// The haystack the decoder models read. Set by `any_haystack`. + static mut GHOST: (*const u8, usize) = (crate::ptr::null(), 0); + + unsafe fn byte(i: usize) -> u8 { + // SAFETY: callers keep `i < GHOST.1`. + unsafe { *GHOST.0.wrapping_add(i) } + } + + /// Width of the sequence a lead byte starts; 0 for any other byte. + fn lead_width(b: u8) -> usize { + match b { + 0x00..=0x7F => 1, + 0xC2..=0xDF => 2, + 0xE0..=0xEF => 3, + 0xF0..=0xF4 => 4, + _ => 0, + } + } + + /// The second byte of a sequence (Unicode Table 3-7). + fn second_ok(lead: u8, b: u8) -> bool { + match lead { + 0xE0 => (0xA0..=0xBF).contains(&b), + 0xED => (0x80..=0x9F).contains(&b), + 0xF0 => (0x90..=0xBF).contains(&b), + 0xF4 => (0x80..=0x8F).contains(&b), + _ => utf8_is_cont_byte(b), + } + } + + /// Local UTF-8 well-formedness at byte `i` of the ghost haystack. It holds + /// at every position of a valid UTF-8 string, and holding at every + /// position is equivalent to validity. + fn utf8_ok_at(i: usize) -> bool { + let len = unsafe { GHOST.1 }; + if i >= len { + return true; + } + // SAFETY: every read below is at an index `< len`. + unsafe { + let b = byte(i); + let w = lead_width(b); + if w >= 1 { + // a lead byte: its sequence is in bounds and well formed, and + // the next byte starts a new character + i + w <= len + && (w < 2 || second_ok(b, byte(i + 1))) + && (w < 3 || utf8_is_cont_byte(byte(i + 2))) + && (w < 4 || utf8_is_cont_byte(byte(i + 3))) + && (i + w == len || !utf8_is_cont_byte(byte(i + w))) + } else if utf8_is_cont_byte(b) { + // a continuation byte: its lead is at most 3 bytes back + (i >= 1 && lead_width(byte(i - 1)) >= 2) + || (i >= 2 && utf8_is_cont_byte(byte(i - 1)) && lead_width(byte(i - 2)) >= 3) + || (i >= 3 + && utf8_is_cont_byte(byte(i - 1)) + && utf8_is_cont_byte(byte(i - 2)) + && lead_width(byte(i - 3)) == 4) + } else { + false // C0, C1, F5..FF never occur + } + } + } + + /// The range of the ghost haystack a byte iterator still covers. + trait GhostRange { + fn ghost_range(&self) -> Option<(usize, usize)>; + } + impl GhostRange for I { + default fn ghost_range(&self) -> Option<(usize, usize)> { + None + } + } + impl GhostRange for Iter<'_, u8> { + fn ghost_range(&self) -> Option<(usize, usize)> { + let rest = self.as_slice(); + let (base, len) = unsafe { GHOST }; + let start = (rest.as_ptr() as usize).wrapping_sub(base as usize); + let end = start.wrapping_add(rest.len()); + (start <= end && end <= len).then_some((start, end)) + } + } + + const CONT_MASK: u8 = 0b0011_1111; + + /// Model of `next_code_point`: the local rule where the decode starts, + /// then the upstream body. + unsafe fn model_next_code_point<'a, I: Iterator>(bytes: &mut I) -> Option { + // `&*bytes`: `bytes.ghost_range()` would pick the blanket impl for `&mut I` + if let Some((start, _)) = GhostRange::ghost_range(&*bytes) { + kani::assume(utf8_ok_at(start)); + } + // ---- upstream body, `utf8_first_byte` / `utf8_acc_cont_byte` inlined ---- + let x = *bytes.next()?; + if x < 128 { + return Some(x as u32); + } + let init = (x & (0x7F >> 2)) as u32; + // SAFETY: as upstream. + let y = unsafe { *bytes.next().unwrap_unchecked() }; + let mut ch = (init << 6) | (y & CONT_MASK) as u32; + if x >= 0xE0 { + // SAFETY: as upstream. + let z = unsafe { *bytes.next().unwrap_unchecked() }; + let y_z = (((y & CONT_MASK) as u32) << 6) | (z & CONT_MASK) as u32; + ch = init << 12 | y_z; + if x >= 0xF0 { + // SAFETY: as upstream. + let w = unsafe { *bytes.next().unwrap_unchecked() }; + ch = (init & 7) << 18 | (y_z << 6) | (w & CONT_MASK) as u32; + } + } + Some(ch) + } + + /// Model of `next_code_point_reverse`: the local rule on the (up to four) + /// bytes the decode can read, then the upstream body. + unsafe fn model_next_code_point_reverse<'a, I>(bytes: &mut I) -> Option + where + I: DoubleEndedIterator, + { + if let Some((_, end)) = GhostRange::ghost_range(&*bytes) { + kani::assume(end < 1 || utf8_ok_at(end - 1)); + kani::assume(end < 2 || utf8_ok_at(end - 2)); + kani::assume(end < 3 || utf8_ok_at(end - 3)); + kani::assume(end < 4 || utf8_ok_at(end - 4)); + } + // ---- upstream body, `utf8_first_byte` / `utf8_acc_cont_byte` inlined ---- + let w = match *bytes.next_back()? { + next_byte if next_byte < 128 => return Some(next_byte as u32), + back_byte => back_byte, + }; + let mut ch; + // SAFETY: as upstream. + let z = unsafe { *bytes.next_back().unwrap_unchecked() }; + ch = (z & (0x7F >> 2)) as u32; + if utf8_is_cont_byte(z) { + // SAFETY: as upstream. + let y = unsafe { *bytes.next_back().unwrap_unchecked() }; + ch = (y & (0x7F >> 3)) as u32; + if utf8_is_cont_byte(y) { + // SAFETY: as upstream. + let x = unsafe { *bytes.next_back().unwrap_unchecked() }; + ch = (x & (0x7F >> 4)) as u32; + ch = (ch << 6) | (y & CONT_MASK) as u32; + } + ch = (ch << 6) | (z & CONT_MASK) as u32; + } + ch = (ch << 6) | (w & CONT_MASK) as u32; + Some(ch) + } + + /// Model of `memchr` (assumption 1): some index of `x` in `text`, or `None`. + fn model_memchr(x: u8, text: &[u8]) -> Option { + if kani::any() { + return None; + } + let i: usize = kani::any(); + kani::assume(i < text.len() && text[i] == x); + Some(i) + } + + /// Model of `memrchr` (assumption 1): some index of `x` in `text`, or `None`. + fn model_memrchr(x: u8, text: &[u8]) -> Option { + model_memchr(x, text) + } + + /// Model of the byte-wise slice equality `compare_bytes(lhs, rhs, size) == 0` + /// (assumption 1). It recurses instead of looping: CBMC 6.11 rejects writes + /// to the locals of a contract-less loop in a callee of a contracted loop + /// (kani#4790, fixed after 6.11), which also rules out the `memcmp` builtin. + unsafe fn model_equal_same_length(lhs: *const A, rhs: *const B, len: usize) -> bool { + // SAFETY: as upstream, both are readable for `len` elements. + let size = unsafe { crate::intrinsics::unchecked_mul(len, crate::mem::size_of::()) }; + // SAFETY: as above, both are readable for `size` bytes. + unsafe { bytes_equal(lhs as *const u8, rhs as *const u8, size) } + } + + /// # Safety + /// `lhs` and `rhs` are readable for `n` bytes. + unsafe fn bytes_equal(lhs: *const u8, rhs: *const u8, n: usize) -> bool { + // SAFETY: if `n > 0`, the first byte and the `n - 1` after it are readable. + n == 0 || unsafe { *lhs == *rhs && bytes_equal(lhs.add(1), rhs.add(1), n - 1) } + } + + /// Model of `<[T]>::contains` (assumption 1): any result. The searchers use + /// only this result, so the set is never read and its size is unbounded. + fn model_contains(_set: &[T], _x: &T) -> bool { + kani::any() + } + + /// A character set of symbolic length. Its contents are never read (see + /// `model_contains`). + fn any_char_slice() -> &'static [char] { + let len: usize = kani::any(); + kani::assume(len <= MAX_ALLOCATION_BYTES / 4); + let p: *const char = if len == 0 { + crate::ptr::NonNull::::dangling().as_ptr() + } else { + // SAFETY: CBMC's `malloc` model. + let p = unsafe { malloc(len * 4) } as *const char; + kani::assume(!p.is_null()); + p + }; + // SAFETY: `p` is valid for `len` chars; they are never read. + unsafe { crate::slice::from_raw_parts(p, len) } + } + + /// Symbolic length, arbitrary contents: no validity assumption at all. + fn any_haystack() -> &'static str { + let len: usize = kani::any(); + kani::assume(len <= MAX_ALLOCATION_BYTES); + let p: *const u8 = if len == 0 { + crate::ptr::NonNull::::dangling().as_ptr() + } else { + // SAFETY: CBMC's `malloc` model. + let p = unsafe { malloc(len) }; + kani::assume(!p.is_null()); + p + }; + unsafe { GHOST = (p, len) }; + // SAFETY: `p` is valid for `len` reads; UTF-8 validity is imported + // where it is relied on (see the module documentation). + unsafe { super::super::from_utf8_unchecked(crate::slice::from_raw_parts(p, len)) } + } + + /// The type invariant `C` of `CharSearcher`. The encoding is compared byte + /// by byte: a slice `==` is a `memcmp` loop of symbolic length. + fn char_searcher_inv(s: &CharSearcher<'_>) -> bool { + let mut utf8 = [0; 4]; + let n = s.needle.encode_utf8(&mut utf8).len(); + let e = &s.utf8_encoded; + 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() == n + && e[0] == utf8[0] + && (n < 2 || e[1] == utf8[1]) + && (n < 3 || e[2] == utf8[2]) + && (n < 4 || e[3] == utf8[3]) + } + + /// An arbitrary `CharSearcher` over `haystack` that satisfies `C`. + fn any_char_searcher(haystack: &'static str) -> CharSearcher<'static> { + let needle: char = kani::any(); + let mut utf8_encoded = [0; 4]; + let utf8_size = needle.encode_utf8(&mut utf8_encoded).len() as u8; + let s = CharSearcher { + haystack, + finger: kani::any(), + finger_back: kani::any(), + needle, + utf8_size, + utf8_encoded, + }; + kani::assume(char_searcher_inv(&s)); + s + } + + /// The returned range is in bounds and on char boundaries (safety + /// property 2), and `C` still holds. + fn check_result(s: &CharSearcher<'_>, range: Option<(usize, usize)>) { + if let Some((a, b)) = range { + assert!(a <= b && b <= s.haystack.len()); + assert!(s.haystack.is_char_boundary(a) && s.haystack.is_char_boundary(b)); + } + assert!(char_searcher_inv(s)); + } + + fn step_range(step: SearchStep) -> Option<(usize, usize)> { + match step { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => Some((a, b)), + SearchStep::Done => None, + } + } + + /// `C` holds for every searcher created from a haystack (criterion 1). + #[kani::proof] + fn check_char_searcher_into_searcher() { + let haystack = any_haystack(); + let needle: char = kani::any(); + let s = needle.into_searcher(haystack); + assert!(char_searcher_inv(&s)); + } + + #[kani::proof] + #[kani::stub(crate::str::validations::next_code_point, model_next_code_point)] + fn check_char_searcher_next() { + let mut s = any_char_searcher(any_haystack()); + let r = step_range(s.next()); + check_result(&s, r); + kani::cover(r.is_some_and(|(_, b)| b > 4096), "a step far into the haystack"); + } + + #[kani::proof] + #[kani::stub(crate::str::validations::next_code_point_reverse, model_next_code_point_reverse)] + fn check_char_searcher_next_back() { + let mut s = any_char_searcher(any_haystack()); + let r = step_range(s.next_back()); + check_result(&s, r); + kani::cover(r.is_some_and(|(a, _)| a > 4096), "a step far into the haystack"); + } + + #[kani::proof] + #[kani::stub(crate::str::validations::next_code_point, model_next_code_point)] + fn check_char_searcher_next_reject() { + let mut s = any_char_searcher(any_haystack()); + let r = s.next_reject(); + check_result(&s, r); + kani::cover(r.is_some_and(|(_, b)| b > 4096), "a reject far into the haystack"); + kani::cover(r.is_none(), "searched to the end"); + } + + #[kani::proof] + #[kani::stub(crate::str::validations::next_code_point_reverse, model_next_code_point_reverse)] + fn check_char_searcher_next_reject_back() { + let mut s = any_char_searcher(any_haystack()); + let r = s.next_reject_back(); + check_result(&s, r); + kani::cover(r.is_some_and(|(a, _)| a > 4096), "a reject far into the haystack"); + kani::cover(r.is_none(), "searched to the start"); + } + + // `unwind(5)`: the needle comparison compares `utf8_size <= 4` bytes; the + // search loop itself has a contract and is not unwound. + #[kani::proof] + #[kani::unwind(5)] + #[kani::stub(crate::slice::memchr::memchr, model_memchr)] + #[kani::stub( + >::equal_same_length, + model_equal_same_length + )] + fn check_char_searcher_next_match() { + let mut s = any_char_searcher(any_haystack()); + let r = s.next_match(); + if let Some((a, _)) = r { + // The match starts at a lead byte: its sequence ends on a boundary. + kani::assume(utf8_ok_at(a)); + } + check_result(&s, r); + kani::cover(r.is_some_and(|(_, b)| b > 4096), "a match far into the haystack"); + kani::cover(r.is_none(), "searched to the end"); + } + + // `unwind(5)`: as for `next_match`. + #[kani::proof] + #[kani::unwind(5)] + #[kani::stub(crate::slice::memchr::memrchr, model_memrchr)] + #[kani::stub( + >::equal_same_length, + model_equal_same_length + )] + fn check_char_searcher_next_match_back() { + let mut s = any_char_searcher(any_haystack()); + let r = s.next_match_back(); + if let Some((a, _)) = r { + // The match starts at a lead byte: its sequence ends on a boundary. + kani::assume(utf8_ok_at(a)); + } + check_result(&s, r); + kani::cover(r.is_some_and(|(a, _)| a > 4096), "a match far into the haystack"); + kani::cover(r.is_none(), "searched to the start"); + } + + /// The decoder models only add assumptions: on every valid 1..=4-byte + /// input they return what upstream returns and consume the same bytes. + #[kani::proof] + #[kani::unwind(6)] + fn check_next_code_point_model_matches_upstream() { + let bytes: [u8; 4] = kani::any(); + let n: usize = kani::any_where(|n| *n >= 1 && *n <= 4); + let s = &bytes[..n]; + kani::assume(crate::str::from_utf8(s).is_ok()); + unsafe { GHOST = (s.as_ptr(), n) }; + let (mut a, mut b) = (s.iter(), s.iter()); + let ra = unsafe { model_next_code_point(&mut a) }; + let rb = unsafe { crate::str::validations::next_code_point(&mut b) }; + assert!(ra == rb && a.as_slice().len() == b.as_slice().len()); + kani::cover(n == 4 && ra.is_some(), "a 4-byte character"); + } + + #[kani::proof] + #[kani::unwind(6)] + fn check_next_code_point_reverse_model_matches_upstream() { + let bytes: [u8; 4] = kani::any(); + let n: usize = kani::any_where(|n| *n >= 1 && *n <= 4); + let s = &bytes[..n]; + kani::assume(crate::str::from_utf8(s).is_ok()); + unsafe { GHOST = (s.as_ptr(), n) }; + let (mut a, mut b) = (s.iter(), s.iter()); + let ra = unsafe { model_next_code_point_reverse(&mut a) }; + let rb = unsafe { crate::str::validations::next_code_point_reverse(&mut b) }; + assert!(ra == rb && a.as_slice().len() == b.as_slice().len()); + kani::cover(n == 4 && ra.is_some(), "a 4-byte character"); + } + + /// The memchr models allow every result of the real functions. + #[kani::proof] + #[kani::unwind(10)] + fn check_memchr_models_cover_upstream() { + let text: [u8; 8] = kani::any(); + let text = kani::slice::any_slice_of_array(&text); + let x: u8 = kani::any(); + if let Some(i) = crate::slice::memchr::memchr(x, text) { + assert!(i < text.len() && text[i] == x); + } + if let Some(i) = crate::slice::memchr::memrchr(x, text) { + assert!(i < text.len() && text[i] == x); + } + } + + /// The slice equality model returns what upstream returns. + #[kani::proof] + #[kani::unwind(5)] + fn check_slice_eq_model_matches_upstream() { + let (a, b): ([u8; 4], [u8; 4]) = (kani::any(), kani::any()); + let n: usize = kani::any(); + kani::assume(n <= 4); + // SAFETY: both arrays are readable for `n <= 4` bytes. + let model = unsafe { model_equal_same_length(a.as_ptr(), b.as_ptr(), n) }; + assert!((a[..n] == b[..n]) == model); + } + + /// An arbitrary `MultiCharEqSearcher` over `haystack` that satisfies `C`. + fn any_multi_char_eq_searcher( + haystack: &'static str, + char_eq: C, + ) -> MultiCharEqSearcher<'static, C> { + let (f, b): (usize, usize) = (kani::any(), kani::any()); + kani::assume(f <= b && b <= haystack.len()); + kani::assume(haystack.is_char_boundary(f) && haystack.is_char_boundary(b)); + // SAFETY: `f <= b <= haystack.len()`. + let rest = unsafe { haystack.as_bytes().get_unchecked(f..b) }; + let char_indices = crate::str::CharIndices { + front_offset: f, + iter: crate::str::Chars { iter: rest.iter() }, + }; + MultiCharEqSearcher { char_eq, haystack, char_indices } + } + + /// As `check_result`, for `MultiCharEqSearcher`. + fn check_multi_char_eq_result( + s: &MultiCharEqSearcher<'_, C>, + range: Option<(usize, usize)>, + ) { + if let Some((a, b)) = range { + assert!(a <= b && b <= s.haystack.len()); + assert!(s.haystack.is_char_boundary(a) && s.haystack.is_char_boundary(b)); + } + assert!(s.kani_ok()); + } + + /// The proofs for one `MultiCharEq` instance, through the searcher that + /// wraps it: creation establishes `C` (criterion 1); `next` / `next_back` + /// meet their contracts from any state that satisfies `C` (criteria 2 and + /// 3); the four searching methods (the provided trait methods, reached + /// through the wrapper) run with those verified contracts in place of the + /// steps, so their loops never read through the cursor that the loop + /// contract havocs. The set itself is abstracted (`model_contains`), so no + /// loop is unwound anywhere. + macro_rules! multi_char_eq_proofs { + ($m:ident, $wrapper:ident, $c:ty, |$set:ident| $eq:expr) => { + mod $m { + use super::*; + + #[kani::proof] + fn check_into_searcher() { + let $set: [char; 2] = kani::any(); + let s = $eq.into_searcher(any_haystack()); + assert!(s.0.kani_ok()); + } + + #[kani::proof_for_contract( as Searcher>::next)] + #[kani::stub(crate::str::validations::next_code_point, model_next_code_point)] + #[kani::stub(<[char]>::contains, model_contains)] + fn check_next() { + let $set: [char; 2] = kani::any(); + let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); + let r = step_range(s.next()); + check_multi_char_eq_result(&s.0, r); + kani::cover(r.is_some_and(|(_, b)| b > 4096), "a step far into the haystack"); + } + + #[kani::proof_for_contract( as ReverseSearcher>::next_back)] + #[kani::stub( + crate::str::validations::next_code_point_reverse, + model_next_code_point_reverse + )] + #[kani::stub(<[char]>::contains, model_contains)] + fn check_next_back() { + let $set: [char; 2] = kani::any(); + let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); + let r = step_range(s.next_back()); + check_multi_char_eq_result(&s.0, r); + kani::cover(r.is_some_and(|(a, _)| a > 4096), "a step far into the haystack"); + } + + #[kani::proof] + #[kani::stub_verified( as Searcher>::next)] + fn check_next_match() { + let $set: [char; 2] = kani::any(); + let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); + let r = s.next_match(); + check_multi_char_eq_result(&s.0, r); + kani::cover(r.is_some_and(|(_, b)| b > 4096), "a match far into the haystack"); + kani::cover(r.is_none(), "searched to the end"); + } + + #[kani::proof] + #[kani::stub_verified( as Searcher>::next)] + fn check_next_reject() { + let $set: [char; 2] = kani::any(); + let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); + let r = s.next_reject(); + check_multi_char_eq_result(&s.0, r); + kani::cover(r.is_some_and(|(_, b)| b > 4096), "a reject far into the haystack"); + kani::cover(r.is_none(), "searched to the end"); + } + + #[kani::proof] + #[kani::stub_verified( as ReverseSearcher>::next_back)] + fn check_next_match_back() { + let $set: [char; 2] = kani::any(); + let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); + let r = s.next_match_back(); + check_multi_char_eq_result(&s.0, r); + kani::cover(r.is_some_and(|(a, _)| a > 4096), "a match far into the haystack"); + kani::cover(r.is_none(), "searched to the start"); + } + + #[kani::proof] + #[kani::stub_verified( as ReverseSearcher>::next_back)] + fn check_next_reject_back() { + let $set: [char; 2] = kani::any(); + let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); + let r = s.next_reject_back(); + check_multi_char_eq_result(&s.0, r); + kani::cover(r.is_some_and(|(a, _)| a > 4096), "a reject far into the haystack"); + kani::cover(r.is_none(), "searched to the start"); + } + } + }; + } + + // `N` only sets the size of the set value: the set is never read. + multi_char_eq_proofs!(char_array, CharArraySearcher, [char; 2], |set| set); + multi_char_eq_proofs!(char_array_ref, CharArrayRefSearcher, &[char; 2], |set| &set); + multi_char_eq_proofs!(char_slice, CharSliceSearcher, &[char], |set| { + let _ = set; + any_char_slice() + }); + // Any predicate result on every call. + multi_char_eq_proofs!(char_predicate, CharPredicateSearcher, fn(char) -> bool, |set| { + let _ = set; + (|_| kani::any()) as fn(char) -> bool + }); + // A predicate that also writes state of its own (inside `char_eq`). + multi_char_eq_proofs!(char_predicate_state, CharPredicateSearcher, Toggle, |set| { + let _ = set; + Toggle(kani::any()) + }); + + /// A predicate with state: it flips a flag on every call, like a `move` + /// closure that updates a capture, and returns any result. + struct Toggle(bool); + + impl FnOnce<(char,)> for Toggle { + type Output = bool; + + extern "rust-call" fn call_once(mut self, args: (char,)) -> bool { + self.call_mut(args) + } + } + + impl FnMut<(char,)> for Toggle { + extern "rust-call" fn call_mut(&mut self, _: (char,)) -> bool { + self.0 = !self.0; + kani::any() + } + } +} From f610507d7ec9ff870858334a30801fb311bbcb08 Mon Sep 17 00:00:00 2001 From: hung1962003 <106923246+hung1962003@users.noreply.github.com> Date: Tue, 27 Oct 2026 12:16:17 +0000 Subject: [PATCH 2/7] Challenge 20: speed up the char Searcher proofs - CharSearcher::next / next_back get step contracts, proved with proof_for_contract and used through stub_verified in the provided next_reject / next_reject_back loops, as MultiCharEqSearcher already does. check_char_searcher_next_reject_back now takes 33 s instead of 17 min, and 2 GB of memory instead of 6 GB. - The next_code_point_reverse model assumes the local UTF-8 rule only at the last byte, where the decode starts: that is all its safety needs. - The proof_for_contract harnesses no longer repeat the contract's ensures; kani_step_ok is shared by both searchers. - multi_char_eq_inv uses the wrapping_sub intrinsic (loop invariants call casts and intrinsics only). All 46 harnesses take 78 min instead of 125 min; the slowest takes 3.2 min instead of 17 min. Co-Authored-By: Claude Opus 5.5 --- library/core/src/str/pattern.rs | 75 ++++++++++++++++++--------------- 1 file changed, 42 insertions(+), 33 deletions(-) diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index f91b8aef34280..4eced457fe509 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -257,6 +257,20 @@ impl kani::Arbitrary for SearchStep { } } +/// A step returns a range in bounds of `haystack` and on char boundaries. +#[cfg(kani)] +fn kani_step_ok(haystack: &str, step: SearchStep) -> bool { + match step { + SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { + a <= b + && b <= haystack.len() + && haystack.is_char_boundary(a) + && haystack.is_char_boundary(b) + } + SearchStep::Done => true, + } +} + /// A searcher for a string pattern. /// /// This trait provides methods for searching for non-overlapping @@ -489,6 +503,18 @@ impl CharSearcher<'_> { } } +#[cfg(kani)] +impl CharSearcher<'_> { + /// The fingers part of `C`, for the contracts of `next` / `next_back`: the + /// safety of a step depends on nothing else. + fn kani_ok(&self) -> bool { + 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) + } +} + #[cfg(kani)] impl SearcherLoopContract for CharSearcher<'_> { /// `finger <= finger_back <= haystack.len()`, both on char boundaries @@ -525,6 +551,9 @@ unsafe impl<'a> Searcher<'a> for CharSearcher<'a> { self.haystack } #[inline] + #[cfg_attr(kani, kani::modifies(&self.finger))] + #[safety::requires(self.kani_ok())] + #[safety::ensures(|step| self.kani_ok() && kani_step_ok(self.haystack, *step))] fn next(&mut self) -> SearchStep { let old_finger = self.finger; // SAFETY: 1-4 guarantee safety of `get_unchecked` @@ -602,6 +631,9 @@ unsafe impl<'a> Searcher<'a> for CharSearcher<'a> { unsafe impl<'a> ReverseSearcher<'a> for CharSearcher<'a> { #[inline] + #[cfg_attr(kani, kani::modifies(&self.finger_back))] + #[safety::requires(self.kani_ok())] + #[safety::ensures(|step| self.kani_ok() && kani_step_ok(self.haystack, *step))] fn next_back(&mut self) -> SearchStep { let old_finger = self.finger_back; // SAFETY: see the comment for next() above @@ -822,7 +854,7 @@ macro_rules! multi_char_eq_inv { let len: usize = crate::intrinsics::ptr_metadata(s.haystack as *const str); let f = s.char_indices.front_offset; let (start, end) = s.char_indices.iter.iter.$parts(); - let b = (end as usize).wrapping_sub(p as usize); + let b = crate::intrinsics::wrapping_sub(end as usize, p as usize); // SAFETY: both reads are guarded by `< len`. let f_ok = f == 0 || f == len @@ -848,19 +880,6 @@ impl MultiCharEqSearcher<'_, C> { fn kani_ok(&self) -> bool { multi_char_eq_inv!(self, kani_raw_parts) } - - /// A step returns a range in bounds and on char boundaries. - fn kani_step_ok(&self, step: SearchStep) -> bool { - match step { - SearchStep::Match(a, b) | SearchStep::Reject(a, b) => { - a <= b - && b <= self.haystack.len() - && self.haystack.is_char_boundary(a) - && self.haystack.is_char_boundary(b) - } - SearchStep::Done => true, - } - } } #[cfg(kani)] @@ -927,7 +946,7 @@ unsafe impl<'a, C: MultiCharEq> Searcher<'a> for MultiCharEqSearcher<'a, C> { ) )] #[safety::requires(self.kani_ok())] - #[safety::ensures(|step| self.kani_ok() && self.kani_step_ok(*step))] + #[safety::ensures(|step| self.kani_ok() && kani_step_ok(self.haystack, *step))] fn next(&mut self) -> SearchStep { let s = &mut self.char_indices; // Compare lengths of the internal byte slice iterator @@ -956,7 +975,7 @@ unsafe impl<'a, C: MultiCharEq> ReverseSearcher<'a> for MultiCharEqSearcher<'a, ) )] #[safety::requires(self.kani_ok())] - #[safety::ensures(|step| self.kani_ok() && self.kani_step_ok(*step))] + #[safety::ensures(|step| self.kani_ok() && kani_step_ok(self.haystack, *step))] fn next_back(&mut self) -> SearchStep { let s = &mut self.char_indices; // Compare lengths of the internal byte slice iterator @@ -2549,17 +2568,14 @@ pub mod verify_char_searcher { Some(ch) } - /// Model of `next_code_point_reverse`: the local rule on the (up to four) - /// bytes the decode can read, then the upstream body. + /// Model of `next_code_point_reverse`: the local rule at the last byte, + /// where the decode starts, then the upstream body. unsafe fn model_next_code_point_reverse<'a, I>(bytes: &mut I) -> Option where I: DoubleEndedIterator, { if let Some((_, end)) = GhostRange::ghost_range(&*bytes) { kani::assume(end < 1 || utf8_ok_at(end - 1)); - kani::assume(end < 2 || utf8_ok_at(end - 2)); - kani::assume(end < 3 || utf8_ok_at(end - 3)); - kani::assume(end < 4 || utf8_ok_at(end - 4)); } // ---- upstream body, `utf8_first_byte` / `utf8_acc_cont_byte` inlined ---- let w = match *bytes.next_back()? { @@ -2666,10 +2682,7 @@ pub mod verify_char_searcher { let mut utf8 = [0; 4]; let n = s.needle.encode_utf8(&mut utf8).len(); let e = &s.utf8_encoded; - 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.kani_ok() && s.utf8_size() == n && e[0] == utf8[0] && (n < 2 || e[1] == utf8[1]) @@ -2720,26 +2733,24 @@ pub mod verify_char_searcher { assert!(char_searcher_inv(&s)); } - #[kani::proof] + #[kani::proof_for_contract(::next)] #[kani::stub(crate::str::validations::next_code_point, model_next_code_point)] fn check_char_searcher_next() { let mut s = any_char_searcher(any_haystack()); let r = step_range(s.next()); - check_result(&s, r); kani::cover(r.is_some_and(|(_, b)| b > 4096), "a step far into the haystack"); } - #[kani::proof] + #[kani::proof_for_contract(::next_back)] #[kani::stub(crate::str::validations::next_code_point_reverse, model_next_code_point_reverse)] fn check_char_searcher_next_back() { let mut s = any_char_searcher(any_haystack()); let r = step_range(s.next_back()); - check_result(&s, r); kani::cover(r.is_some_and(|(a, _)| a > 4096), "a step far into the haystack"); } #[kani::proof] - #[kani::stub(crate::str::validations::next_code_point, model_next_code_point)] + #[kani::stub_verified(::next)] fn check_char_searcher_next_reject() { let mut s = any_char_searcher(any_haystack()); let r = s.next_reject(); @@ -2749,7 +2760,7 @@ pub mod verify_char_searcher { } #[kani::proof] - #[kani::stub(crate::str::validations::next_code_point_reverse, model_next_code_point_reverse)] + #[kani::stub_verified(::next_back)] fn check_char_searcher_next_reject_back() { let mut s = any_char_searcher(any_haystack()); let r = s.next_reject_back(); @@ -2914,7 +2925,6 @@ pub mod verify_char_searcher { let $set: [char; 2] = kani::any(); let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); let r = step_range(s.next()); - check_multi_char_eq_result(&s.0, r); kani::cover(r.is_some_and(|(_, b)| b > 4096), "a step far into the haystack"); } @@ -2928,7 +2938,6 @@ pub mod verify_char_searcher { let $set: [char; 2] = kani::any(); let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); let r = step_range(s.next_back()); - check_multi_char_eq_result(&s.0, r); kani::cover(r.is_some_and(|(a, _)| a > 4096), "a step far into the haystack"); } From de6549692b8475044ef00b1cd1abb44e1fe70df9 Mon Sep 17 00:00:00 2001 From: hung1962003 <106923246+hung1962003@users.noreply.github.com> Date: Tue, 27 Oct 2026 17:36:44 +0000 Subject: [PATCH 3/7] Challenge 20: havoc the MultiCharEq cursor as words A replaced step (stub_verified) havocs a modifies target element by element, and each of those writes is checked against the write set of the enclosing loop. Naming char_indices as its 3 words instead of its 24 bytes cuts the peak memory of every MultiCharEq loop proof from about 7.3 GB to about 2 GB (and its time from about 150 s to about 40 s), so they fit the 7 GB macOS CI runner. The loop_modifies names the same bytes as before. All 46 harnesses: 47 min instead of 78 min; peak memory 4.4 GB. Co-Authored-By: Claude Opus 5.5 --- library/core/src/str/pattern.rs | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 4eced457fe509..cf0ceed5da6ed 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -880,6 +880,16 @@ impl MultiCharEqSearcher<'_, C> { fn kani_ok(&self) -> bool { multi_char_eq_inv!(self, kani_raw_parts) } + + /// `char_indices` as the words it consists of, for the step contracts. A + /// replaced step havocs its targets element by element, so this takes + /// three writes where a byte range would take one per byte. + fn kani_cursor_words(&self) -> *const [usize] { + crate::ptr::slice_from_raw_parts( + &raw const self.char_indices as *const usize, + size_of_val(&self.char_indices) / size_of::(), + ) + } } #[cfg(kani)] @@ -940,10 +950,7 @@ unsafe impl<'a, C: MultiCharEq> Searcher<'a> for MultiCharEqSearcher<'a, C> { #[inline] #[cfg_attr( kani, - kani::modifies( - SearcherLoopContract::kani_fwd_cursor(self), - SearcherLoopContract::kani_pred_state(self) - ) + kani::modifies(self.kani_cursor_words(), SearcherLoopContract::kani_pred_state(self)) )] #[safety::requires(self.kani_ok())] #[safety::ensures(|step| self.kani_ok() && kani_step_ok(self.haystack, *step))] @@ -969,10 +976,7 @@ unsafe impl<'a, C: MultiCharEq> ReverseSearcher<'a> for MultiCharEqSearcher<'a, #[inline] #[cfg_attr( kani, - kani::modifies( - SearcherLoopContract::kani_fwd_cursor(self), - SearcherLoopContract::kani_pred_state(self) - ) + kani::modifies(self.kani_cursor_words(), SearcherLoopContract::kani_pred_state(self)) )] #[safety::requires(self.kani_ok())] #[safety::ensures(|step| self.kani_ok() && kani_step_ok(self.haystack, *step))] From c6a42ee42c67759f8e129b360eaf4a513c37142e Mon Sep 17 00:00:00 2001 From: hung1962003 <106923246+hung1962003@users.noreply.github.com> Date: Wed, 28 Oct 2026 03:34:52 +0000 Subject: [PATCH 4/7] Challenge 20: simplify the slice model and the pattern state hook - The slice equality model compares the at most 4 bytes of a char's encoding without recursion, and asserts that bound, so the two CharSearcher next_match harnesses no longer need kani::unwind. - kani_pred_state is empty by default: Kani checks every write against modifies and loop_modifies, so a pattern that writes state it does not name fails its proofs. Only the stateful test predicate Toggle names its state, in place of four specializations to empty. All 46 harnesses verify (46 min, peak memory 4.2 GB). Co-Authored-By: Claude Opus 5.5 --- library/core/src/str/pattern.rs | 73 +++++++++++---------------------- 1 file changed, 25 insertions(+), 48 deletions(-) diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index cf0ceed5da6ed..6ed8622cf95a1 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -68,7 +68,8 @@ pub(crate) trait SearcherLoopContract { /// The bytes a backward step (`next_back`) writes. fn kani_back_cursor(&self) -> *const [u8]; /// The bytes of the pattern's own state that a step may write (a stateful - /// predicate). + /// predicate). None by default: Kani checks every write against `modifies` + /// and `loop_modifies`, so a pattern that writes more fails its proofs. fn kani_pred_state(&self) -> *const [u8]; } @@ -907,36 +908,6 @@ impl SearcherLoopContract for MultiCharEqSearcher<'_, C> { self.kani_fwd_cursor() } default fn kani_pred_state(&self) -> *const [u8] { - crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, size_of::()) - } -} - -// A set of characters has no state of its own: `matches` only reads it. -#[cfg(kani)] -impl SearcherLoopContract for MultiCharEqSearcher<'_, [char; N]> { - fn kani_pred_state(&self) -> *const [u8] { - crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, 0) - } -} - -#[cfg(kani)] -impl SearcherLoopContract for MultiCharEqSearcher<'_, &[char; N]> { - fn kani_pred_state(&self) -> *const [u8] { - crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, 0) - } -} - -#[cfg(kani)] -impl SearcherLoopContract for MultiCharEqSearcher<'_, &[char]> { - fn kani_pred_state(&self) -> *const [u8] { - crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, 0) - } -} - -// Nor does a function pointer: a call through it does not write it. -#[cfg(kani)] -impl SearcherLoopContract for MultiCharEqSearcher<'_, fn(char) -> bool> { - fn kani_pred_state(&self) -> *const [u8] { crate::ptr::slice_from_raw_parts(&raw const self.char_eq as *const u8, 0) } } @@ -2429,7 +2400,8 @@ pub mod verify { /// * `memchr` / `memrchr` (assumption 1): return a matching index, or `None`. /// This allows more behaviors than the real functions (`None` while a match /// exists, a match that is not the first/last), which is sound for safety. -/// * slice equality of bytes (assumption 1): a recursive byte comparison in +/// * slice equality of bytes (assumption 1): a byte by byte comparison of at +/// most 4 bytes (asserted: the searchers compare the encoding of a char) in /// place of `compare_bytes`. `check_slice_eq_model_matches_upstream` shows it /// returns what upstream returns. /// * `<[char]>::contains` (assumption 1): any result. The searchers use only @@ -2622,21 +2594,22 @@ pub mod verify_char_searcher { } /// Model of the byte-wise slice equality `compare_bytes(lhs, rhs, size) == 0` - /// (assumption 1). It recurses instead of looping: CBMC 6.11 rejects writes - /// to the locals of a contract-less loop in a callee of a contracted loop - /// (kani#4790, fixed after 6.11), which also rules out the `memcmp` builtin. + /// (assumption 1), for the at most 4 bytes of a char's encoding. It has no + /// loop: CBMC 6.11 rejects writes to the locals of a contract-less loop in a + /// callee of a contracted loop (kani#4790, fixed after 6.11), which also + /// rules out the `memcmp` builtin. unsafe fn model_equal_same_length(lhs: *const A, rhs: *const B, len: usize) -> bool { // SAFETY: as upstream, both are readable for `len` elements. let size = unsafe { crate::intrinsics::unchecked_mul(len, crate::mem::size_of::()) }; + assert!(size <= 4); + let (l, r) = (lhs as *const u8, rhs as *const u8); // SAFETY: as above, both are readable for `size` bytes. - unsafe { bytes_equal(lhs as *const u8, rhs as *const u8, size) } - } - - /// # Safety - /// `lhs` and `rhs` are readable for `n` bytes. - unsafe fn bytes_equal(lhs: *const u8, rhs: *const u8, n: usize) -> bool { - // SAFETY: if `n > 0`, the first byte and the `n - 1` after it are readable. - n == 0 || unsafe { *lhs == *rhs && bytes_equal(lhs.add(1), rhs.add(1), n - 1) } + unsafe { + (size < 1 || *l == *r) + && (size < 2 || *l.add(1) == *r.add(1)) + && (size < 3 || *l.add(2) == *r.add(2)) + && (size < 4 || *l.add(3) == *r.add(3)) + } } /// Model of `<[T]>::contains` (assumption 1): any result. The searchers use @@ -2773,10 +2746,7 @@ pub mod verify_char_searcher { kani::cover(r.is_none(), "searched to the start"); } - // `unwind(5)`: the needle comparison compares `utf8_size <= 4` bytes; the - // search loop itself has a contract and is not unwound. #[kani::proof] - #[kani::unwind(5)] #[kani::stub(crate::slice::memchr::memchr, model_memchr)] #[kani::stub( >::equal_same_length, @@ -2794,9 +2764,7 @@ pub mod verify_char_searcher { kani::cover(r.is_none(), "searched to the end"); } - // `unwind(5)`: as for `next_match`. #[kani::proof] - #[kani::unwind(5)] #[kani::stub(crate::slice::memchr::memrchr, model_memrchr)] #[kani::stub( >::equal_same_length, @@ -3028,4 +2996,13 @@ pub mod verify_char_searcher { kani::any() } } + + impl SearcherLoopContract for MultiCharEqSearcher<'_, Toggle> { + fn kani_pred_state(&self) -> *const [u8] { + crate::ptr::slice_from_raw_parts( + &raw const self.char_eq as *const u8, + size_of::(), + ) + } + } } From 080960b9f7edbb6cc50eb41b810aa6d5bc0d857f Mon Sep 17 00:00:00 2001 From: hung1962003 <106923246+hung1962003@users.noreply.github.com> Date: Wed, 28 Oct 2026 06:05:38 +0000 Subject: [PATCH 5/7] Keep check_from_ptr_contract off loop-contract mode check_from_ptr_contract reaches CharSearcher::next_match only through panic formatting, where it never runs. Its new loop contract made Kani apply loop contracts to this harness, and CBMC 6.11 then rejects the contract-less loop of its built-in strlen ("Check that len is assignable", fixed by diffblue/cbmc#9164). Stub next_match in this harness so the loop contract is not compiled into it; in the instrumented program next_match still has no body, so the harness proves the same. Co-Authored-By: Claude Opus 5.5 --- library/core/src/ffi/c_str.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index e299f44e03181..c543db95e8806 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -1149,7 +1149,12 @@ mod verify { } // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr + // The stub: this harness reaches `CharSearcher::next_match` only through + // panic formatting, where it never runs. Its loop contract would make Kani + // apply loop contracts here, and CBMC 6.11 then rejects the loop of its + // built-in `strlen` (fixed by diffblue/cbmc#9164). #[kani::proof_for_contract(CStr::from_ptr)] + #[kani::stub(::next_match, any_match)] #[kani::unwind(33)] fn check_from_ptr_contract() { const MAX_SIZE: usize = 32; @@ -1161,6 +1166,14 @@ mod verify { } } + // `'a: 'a` makes `'a` early-bound, like the lifetime of the impl. + fn any_match<'a>(_: &mut crate::str::pattern::CharSearcher<'a>) -> Option<(usize, usize)> + where + 'a: 'a, + { + kani::any() + } + // pub const fn is_empty(&self) -> bool #[kani::proof] #[kani::unwind(33)] From d686f3e47a6539ee85ab13bdf80607212d0f72d7 Mon Sep 17 00:00:00 2001 From: hung1962003 <106923246+hung1962003@users.noreply.github.com> Date: Wed, 28 Oct 2026 17:22:21 +0000 Subject: [PATCH 6/7] Challenge 20: decode with one iterator write, model Iter::len The step contracts check every write to the cursor against their write set, and each check copies the set. Upstream moves the byte iterator once per byte, and Iter::len goes through the contract of NonNull::offset_from_unsigned. The decoder models now read the bytes from the slice the iterator has left and move it once, and a stub of Iter::len calls the raw pointer offset_from_unsigned, which keeps its UB checks. This halves the memory of the step proofs. check_iter_len_model_matches_upstream checks the new stub; the existing check_next_code_point{,_reverse}_model_matches_upstream check the decoders. Co-Authored-By: Claude Opus 5.5 --- library/core/src/slice/iter.rs | 2 +- library/core/src/str/pattern.rs | 214 +++++++++++++++++++++----------- 2 files changed, 143 insertions(+), 73 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 525d92a14aa6e..9cf52e3959cf5 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -170,7 +170,7 @@ impl AsRef<[T]> for Iter<'_, T> { #[cfg(kani)] impl Iter<'_, T> { - /// `(ptr, end_or_len)`, read without calls, for the contracts in + /// `(ptr, end_or_len)`, read without calls, for the proofs in /// `str::pattern`. pub(crate) fn kani_raw_parts(&self) -> (*const T, *const T) { // SAFETY: `NonNull` is a transparent `*const T`. diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 6ed8622cf95a1..10c97862c2160 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -2393,10 +2393,15 @@ pub mod verify { /// # Models /// /// * `next_code_point{,_reverse}` (assumption 2): assume the local rule where -/// the decode starts, then the upstream body with its helpers inlined. The -/// `unwrap_unchecked`s stay checked, so a decode that does not start on a -/// char boundary is still caught. `check_*_model_matches_upstream` shows the -/// models only add assumptions. +/// the decode starts, then the upstream arithmetic on the bytes, with one +/// move of the iterator where upstream moves it per byte. Where upstream +/// reads a byte with `unwrap_unchecked`, the models assert that it is there, +/// so a decode that does not start on a char boundary is still caught. +/// `check_*_model_matches_upstream` shows the models only add assumptions. +/// * `>::len` (assumption 1): the upstream body on the raw +/// pointers, which keeps its UB checks. +/// `check_iter_len_model_matches_upstream` shows it returns what upstream +/// returns. /// * `memchr` / `memrchr` (assumption 1): return a matching index, or `None`. /// This allows more behaviors than the real functions (`None` while a match /// exists, a match that is not the first/last), which is sound for safety. @@ -2493,89 +2498,139 @@ pub mod verify_char_searcher { } } - /// The range of the ghost haystack a byte iterator still covers. - trait GhostRange { - fn ghost_range(&self) -> Option<(usize, usize)>; + /// The range of the ghost haystack that `s` covers. + fn ghost_range(s: &[u8]) -> Option<(usize, usize)> { + let (base, len) = unsafe { GHOST }; + let start = (s.as_ptr() as usize).wrapping_sub(base as usize); + let end = start.wrapping_add(s.len()); + (start <= end && end <= len).then_some((start, end)) } - impl GhostRange for I { - default fn ghost_range(&self) -> Option<(usize, usize)> { - None - } + + const CONT_MASK: u8 = 0b0011_1111; + + /// The decoder models, for the byte iterator of a `Chars`: the only one the + /// searchers decode from. + trait Decode { + fn decode(&mut self) -> Option; + fn decode_back(&mut self) -> Option; } - impl GhostRange for Iter<'_, u8> { - fn ghost_range(&self) -> Option<(usize, usize)> { - let rest = self.as_slice(); - let (base, len) = unsafe { GHOST }; - let start = (rest.as_ptr() as usize).wrapping_sub(base as usize); - let end = start.wrapping_add(rest.len()); - (start <= end && end <= len).then_some((start, end)) + impl Decode for I { + default fn decode(&mut self) -> Option { + panic!("the decoder models only decode from `slice::Iter`") + } + default fn decode_back(&mut self) -> Option { + panic!("the decoder models only decode from `slice::Iter`") } } - const CONT_MASK: u8 = 0b0011_1111; - - /// Model of `next_code_point`: the local rule where the decode starts, - /// then the upstream body. - unsafe fn model_next_code_point<'a, I: Iterator>(bytes: &mut I) -> Option { - // `&*bytes`: `bytes.ghost_range()` would pick the blanket impl for `&mut I` - if let Some((start, _)) = GhostRange::ghost_range(&*bytes) { - kani::assume(utf8_ok_at(start)); - } - // ---- upstream body, `utf8_first_byte` / `utf8_acc_cont_byte` inlined ---- - let x = *bytes.next()?; - if x < 128 { - return Some(x as u32); - } - let init = (x & (0x7F >> 2)) as u32; - // SAFETY: as upstream. - let y = unsafe { *bytes.next().unwrap_unchecked() }; - let mut ch = (init << 6) | (y & CONT_MASK) as u32; - if x >= 0xE0 { - // SAFETY: as upstream. - let z = unsafe { *bytes.next().unwrap_unchecked() }; + /// The upstream decoders, reading the bytes from the slice the iterator has + /// left and moving the iterator once. Upstream moves it once per byte, and + /// the step contracts check every move against their write set, at the + /// cost of a copy of the set. Where upstream reads a byte with + /// `unwrap_unchecked`, these assert that it is there. + impl Decode for Iter<'_, u8> { + fn decode(&mut self) -> Option { + let s = self.as_slice(); + if let Some((start, _)) = ghost_range(s) { + kani::assume(utf8_ok_at(start)); + } + let x = *s.first()?; + let n = if x < 128 { + 1 + } else if x < 0xE0 { + 2 + } else if x < 0xF0 { + 3 + } else { + 4 + }; + assert!(n <= s.len()); + let y = if n >= 2 { s[1] } else { 0 }; + let z = if n >= 3 { s[2] } else { 0 }; + let w = if n >= 4 { s[3] } else { 0 }; + *self = s[n..].iter(); + // ---- upstream arithmetic, `utf8_first_byte` / `utf8_acc_cont_byte` inlined ---- + let init = (x & (0x7F >> 2)) as u32; let y_z = (((y & CONT_MASK) as u32) << 6) | (z & CONT_MASK) as u32; - ch = init << 12 | y_z; - if x >= 0xF0 { - // SAFETY: as upstream. - let w = unsafe { *bytes.next().unwrap_unchecked() }; - ch = (init & 7) << 18 | (y_z << 6) | (w & CONT_MASK) as u32; + Some(match n { + 1 => x as u32, + 2 => (init << 6) | (y & CONT_MASK) as u32, + 3 => init << 12 | y_z, + _ => (init & 7) << 18 | (y_z << 6) | (w & CONT_MASK) as u32, + }) + } + + fn decode_back(&mut self) -> Option { + let s = self.as_slice(); + let len = s.len(); + if let Some((_, end)) = ghost_range(s) { + kani::assume(end < 1 || utf8_ok_at(end - 1)); } + let w = *s.last()?; + if w < 128 { + *self = s[..len - 1].iter(); + return Some(w as u32); + } + assert!(len >= 2); + let z = s[len - 2]; + let n = if !utf8_is_cont_byte(z) { + 2 + } else { + assert!(len >= 3); + if !utf8_is_cont_byte(s[len - 3]) { + 3 + } else { + assert!(len >= 4); + 4 + } + }; + let y = if n >= 3 { s[len - 3] } else { 0 }; + let x = if n >= 4 { s[len - 4] } else { 0 }; + *self = s[..len - n].iter(); + // ---- upstream arithmetic, `utf8_first_byte` / `utf8_acc_cont_byte` inlined ---- + let mut ch = match n { + 2 => (z & (0x7F >> 2)) as u32, + 3 => (y & (0x7F >> 3)) as u32, + _ => (((x & (0x7F >> 4)) as u32) << 6) | (y & CONT_MASK) as u32, + }; + if n >= 3 { + ch = (ch << 6) | (z & CONT_MASK) as u32; + } + Some((ch << 6) | (w & CONT_MASK) as u32) } - Some(ch) } - /// Model of `next_code_point_reverse`: the local rule at the last byte, - /// where the decode starts, then the upstream body. + /// Model of `next_code_point` (assumption 2): the local rule where the + /// decode starts, then the upstream decode. + unsafe fn model_next_code_point<'a, I: Iterator>(bytes: &mut I) -> Option { + Decode::decode(bytes) + } + + /// Model of `next_code_point_reverse` (assumption 2): the local rule at the + /// last byte, where the decode starts, then the upstream decode. unsafe fn model_next_code_point_reverse<'a, I>(bytes: &mut I) -> Option where I: DoubleEndedIterator, { - if let Some((_, end)) = GhostRange::ghost_range(&*bytes) { - kani::assume(end < 1 || utf8_ok_at(end - 1)); - } - // ---- upstream body, `utf8_first_byte` / `utf8_acc_cont_byte` inlined ---- - let w = match *bytes.next_back()? { - next_byte if next_byte < 128 => return Some(next_byte as u32), - back_byte => back_byte, - }; - let mut ch; - // SAFETY: as upstream. - let z = unsafe { *bytes.next_back().unwrap_unchecked() }; - ch = (z & (0x7F >> 2)) as u32; - if utf8_is_cont_byte(z) { - // SAFETY: as upstream. - let y = unsafe { *bytes.next_back().unwrap_unchecked() }; - ch = (y & (0x7F >> 3)) as u32; - if utf8_is_cont_byte(y) { - // SAFETY: as upstream. - let x = unsafe { *bytes.next_back().unwrap_unchecked() }; - ch = (x & (0x7F >> 4)) as u32; - ch = (ch << 6) | (y & CONT_MASK) as u32; - } - ch = (ch << 6) | (z & CONT_MASK) as u32; + Decode::decode_back(bytes) + } + + /// Model of ` as ExactSizeIterator>::len` (assumption 1): + /// the upstream body, with the raw pointer `offset_from_unsigned` that + /// `NonNull::offset_from_unsigned` wraps. That keeps its UB checks and + /// drops the contract around the wrapper, which costs a copy of the write + /// set per call in the step contracts. + fn model_iter_len<'a, T>(it: &Iter<'a, T>) -> usize + where + 'a: 'a, // early-bound, like the lifetime of the impl + { + let (ptr, end) = it.kani_raw_parts(); + if size_of::() == 0 { + end.addr() + } else { + // SAFETY: as upstream, `ptr <= end` in the same allocation. + unsafe { end.offset_from_unsigned(ptr) } } - ch = (ch << 6) | (w & CONT_MASK) as u32; - Some(ch) } /// Model of `memchr` (assumption 1): some index of `x` in `text`, or `None`. @@ -2712,6 +2767,7 @@ pub mod verify_char_searcher { #[kani::proof_for_contract(::next)] #[kani::stub(crate::str::validations::next_code_point, model_next_code_point)] + #[kani::stub( as crate::iter::ExactSizeIterator>::len, model_iter_len)] fn check_char_searcher_next() { let mut s = any_char_searcher(any_haystack()); let r = step_range(s.next()); @@ -2720,6 +2776,7 @@ pub mod verify_char_searcher { #[kani::proof_for_contract(::next_back)] #[kani::stub(crate::str::validations::next_code_point_reverse, model_next_code_point_reverse)] + #[kani::stub( as crate::iter::ExactSizeIterator>::len, model_iter_len)] fn check_char_searcher_next_back() { let mut s = any_char_searcher(any_haystack()); let r = step_range(s.next_back()); @@ -2829,6 +2886,17 @@ pub mod verify_char_searcher { } } + /// The `len` model returns what upstream returns. + #[kani::proof] + fn check_iter_len_model_matches_upstream() { + let bytes: [u8; 8] = kani::any(); + let mut it = kani::slice::any_slice_of_array(&bytes).iter(); + if kani::any() { + it.next(); + } + assert!(model_iter_len(&it) == it.len()); + } + /// The slice equality model returns what upstream returns. #[kani::proof] #[kani::unwind(5)] @@ -2892,6 +2960,7 @@ pub mod verify_char_searcher { #[kani::proof_for_contract( as Searcher>::next)] #[kani::stub(crate::str::validations::next_code_point, model_next_code_point)] + #[kani::stub( as crate::iter::ExactSizeIterator>::len, model_iter_len)] #[kani::stub(<[char]>::contains, model_contains)] fn check_next() { let $set: [char; 2] = kani::any(); @@ -2905,6 +2974,7 @@ pub mod verify_char_searcher { crate::str::validations::next_code_point_reverse, model_next_code_point_reverse )] + #[kani::stub( as crate::iter::ExactSizeIterator>::len, model_iter_len)] #[kani::stub(<[char]>::contains, model_contains)] fn check_next_back() { let $set: [char; 2] = kani::any(); From e86cb4f6a541b77a957dea46d3ae0df982d8f6b6 Mon Sep 17 00:00:00 2001 From: hung1962003 <106923246+hung1962003@users.noreply.github.com> Date: Wed, 28 Oct 2026 19:36:41 +0000 Subject: [PATCH 7/7] Challenge 20: shorten the proofs, decode without `?` Share the char-boundary check, the memchr model, the allocation helper and the result check between the two searchers, and merge the decoder harnesses into check_decoder_models_match_upstream. The reverse decoder reads its bytes first and moves the iterator once, without the `?` operator (its ControlFlow temporary is tracked by the write set). Co-Authored-By: Claude Opus 5.5 --- library/core/src/str/pattern.rs | 170 ++++++++++++++------------------ 1 file changed, 72 insertions(+), 98 deletions(-) diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 10c97862c2160..eaa45e35458f0 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -89,6 +89,19 @@ impl SearcherLoopContract for T { } } +/// `str::is_char_boundary` of `$i` for the `$len` bytes at `$p`, with casts and +/// intrinsics only, for the type invariants that loop invariants call. +#[cfg(kani)] +macro_rules! kani_boundary { + ($p:expr, $len:expr, $i:expr) => { + $i == 0 + || $i == $len + // SAFETY: the read is guarded by `< len`. + || ($i < $len + && unsafe { *crate::intrinsics::arith_offset($p, $i as isize) } as i8 >= -0x40) + }; +} + // Pattern /// A string pattern. @@ -524,16 +537,7 @@ impl SearcherLoopContract for CharSearcher<'_> { let p = self.haystack as *const str as *const u8; let len: usize = crate::intrinsics::ptr_metadata(self.haystack as *const str); let (f, fb) = (self.finger, self.finger_back); - // SAFETY: both reads are guarded by `< len`. - let f_ok = f == 0 - || f == len - || (f < len - && unsafe { *crate::intrinsics::arith_offset(p, f as isize) } as i8 >= -0x40); - let fb_ok = fb == 0 - || fb == len - || (fb < len - && unsafe { *crate::intrinsics::arith_offset(p, fb as isize) } as i8 >= -0x40); - f <= fb && fb <= len && f_ok && fb_ok + f <= fb && fb <= len && kani_boundary!(p, len, f) && kani_boundary!(p, len, fb) } fn kani_fwd_cursor(&self) -> *const [u8] { crate::ptr::slice_from_raw_parts(&raw const self.finger as *const u8, size_of::()) @@ -856,22 +860,13 @@ macro_rules! multi_char_eq_inv { let f = s.char_indices.front_offset; let (start, end) = s.char_indices.iter.iter.$parts(); let b = crate::intrinsics::wrapping_sub(end as usize, p as usize); - // SAFETY: both reads are guarded by `< len`. - let f_ok = f == 0 - || f == len - || (f < len - && unsafe { *crate::intrinsics::arith_offset(p, f as isize) } as i8 >= -0x40); - let b_ok = b == 0 - || b == len - || (b < len - && unsafe { *crate::intrinsics::arith_offset(p, b as isize) } as i8 >= -0x40); // SAFETY: `arith_offset` is a wrapping offset, never UB. f <= b && b <= len && start == unsafe { crate::intrinsics::arith_offset(p, f as isize) } && end == unsafe { crate::intrinsics::arith_offset(p, b as isize) } - && f_ok - && b_ok + && kani_boundary!(p, len, f) + && kani_boundary!(p, len, b) }}; } @@ -2397,7 +2392,8 @@ pub mod verify { /// move of the iterator where upstream moves it per byte. Where upstream /// reads a byte with `unwrap_unchecked`, the models assert that it is there, /// so a decode that does not start on a char boundary is still caught. -/// `check_*_model_matches_upstream` shows the models only add assumptions. +/// `check_decoder_models_match_upstream` shows the models only add +/// assumptions. /// * `>::len` (assumption 1): the upstream body on the raw /// pointers, which keeps its UB checks. /// `check_iter_len_model_matches_upstream` shows it returns what upstream @@ -2534,7 +2530,10 @@ pub mod verify_char_searcher { if let Some((start, _)) = ghost_range(s) { kani::assume(utf8_ok_at(start)); } - let x = *s.first()?; + if s.is_empty() { + return None; + } + let x = s[0]; let n = if x < 128 { 1 } else if x < 0xE0 { @@ -2566,28 +2565,34 @@ pub mod verify_char_searcher { if let Some((_, end)) = ghost_range(s) { kani::assume(end < 1 || utf8_ok_at(end - 1)); } - let w = *s.last()?; - if w < 128 { - *self = s[..len - 1].iter(); - return Some(w as u32); + if len == 0 { + return None; } - assert!(len >= 2); - let z = s[len - 2]; - let n = if !utf8_is_cont_byte(z) { - 2 + let w = s[len - 1]; + let n = if w < 128 { + 1 } else { - assert!(len >= 3); - if !utf8_is_cont_byte(s[len - 3]) { - 3 + assert!(len >= 2); + if !utf8_is_cont_byte(s[len - 2]) { + 2 } else { - assert!(len >= 4); - 4 + assert!(len >= 3); + if !utf8_is_cont_byte(s[len - 3]) { + 3 + } else { + assert!(len >= 4); + 4 + } } }; + let z = if n >= 2 { s[len - 2] } else { 0 }; let y = if n >= 3 { s[len - 3] } else { 0 }; let x = if n >= 4 { s[len - 4] } else { 0 }; *self = s[..len - n].iter(); // ---- upstream arithmetic, `utf8_first_byte` / `utf8_acc_cont_byte` inlined ---- + if n == 1 { + return Some(w as u32); + } let mut ch = match n { 2 => (z & (0x7F >> 2)) as u32, 3 => (y & (0x7F >> 3)) as u32, @@ -2633,7 +2638,8 @@ pub mod verify_char_searcher { } } - /// Model of `memchr` (assumption 1): some index of `x` in `text`, or `None`. + /// Model of `memchr` and `memrchr` (assumption 1): some index of `x` in + /// `text`, or `None`. fn model_memchr(x: u8, text: &[u8]) -> Option { if kani::any() { return None; @@ -2643,11 +2649,6 @@ pub mod verify_char_searcher { Some(i) } - /// Model of `memrchr` (assumption 1): some index of `x` in `text`, or `None`. - fn model_memrchr(x: u8, text: &[u8]) -> Option { - model_memchr(x, text) - } - /// Model of the byte-wise slice equality `compare_bytes(lhs, rhs, size) == 0` /// (assumption 1), for the at most 4 bytes of a char's encoding. It has no /// loop: CBMC 6.11 rejects writes to the locals of a contract-less loop in a @@ -2673,35 +2674,31 @@ pub mod verify_char_searcher { kani::any() } + /// `len` elements from CBMC's `malloc` model (dangling if `len == 0`). + fn any_alloc(len: usize) -> *const T { + if len == 0 { + return crate::ptr::NonNull::dangling().as_ptr(); + } + // SAFETY: CBMC's `malloc` model. + let p = unsafe { malloc(len * size_of::()) } as *const T; + kani::assume(!p.is_null()); + p + } + /// A character set of symbolic length. Its contents are never read (see /// `model_contains`). fn any_char_slice() -> &'static [char] { let len: usize = kani::any(); kani::assume(len <= MAX_ALLOCATION_BYTES / 4); - let p: *const char = if len == 0 { - crate::ptr::NonNull::::dangling().as_ptr() - } else { - // SAFETY: CBMC's `malloc` model. - let p = unsafe { malloc(len * 4) } as *const char; - kani::assume(!p.is_null()); - p - }; - // SAFETY: `p` is valid for `len` chars; they are never read. - unsafe { crate::slice::from_raw_parts(p, len) } + // SAFETY: valid for `len` chars; they are never read. + unsafe { crate::slice::from_raw_parts(any_alloc(len), len) } } /// Symbolic length, arbitrary contents: no validity assumption at all. fn any_haystack() -> &'static str { let len: usize = kani::any(); kani::assume(len <= MAX_ALLOCATION_BYTES); - let p: *const u8 = if len == 0 { - crate::ptr::NonNull::::dangling().as_ptr() - } else { - // SAFETY: CBMC's `malloc` model. - let p = unsafe { malloc(len) }; - kani::assume(!p.is_null()); - p - }; + let p = any_alloc(len); unsafe { GHOST = (p, len) }; // SAFETY: `p` is valid for `len` reads; UTF-8 validity is imported // where it is relied on (see the module documentation). @@ -2740,13 +2737,13 @@ pub mod verify_char_searcher { } /// The returned range is in bounds and on char boundaries (safety - /// property 2), and `C` still holds. - fn check_result(s: &CharSearcher<'_>, range: Option<(usize, usize)>) { + /// property 2), and `C` still holds (`inv`). + fn check_result(haystack: &str, range: Option<(usize, usize)>, inv: bool) { if let Some((a, b)) = range { - assert!(a <= b && b <= s.haystack.len()); - assert!(s.haystack.is_char_boundary(a) && s.haystack.is_char_boundary(b)); + assert!(a <= b && b <= haystack.len()); + assert!(haystack.is_char_boundary(a) && haystack.is_char_boundary(b)); } - assert!(char_searcher_inv(s)); + assert!(inv); } fn step_range(step: SearchStep) -> Option<(usize, usize)> { @@ -2788,7 +2785,7 @@ pub mod verify_char_searcher { fn check_char_searcher_next_reject() { let mut s = any_char_searcher(any_haystack()); let r = s.next_reject(); - check_result(&s, r); + check_result(s.haystack, r, char_searcher_inv(&s)); kani::cover(r.is_some_and(|(_, b)| b > 4096), "a reject far into the haystack"); kani::cover(r.is_none(), "searched to the end"); } @@ -2798,7 +2795,7 @@ pub mod verify_char_searcher { fn check_char_searcher_next_reject_back() { let mut s = any_char_searcher(any_haystack()); let r = s.next_reject_back(); - check_result(&s, r); + check_result(s.haystack, r, char_searcher_inv(&s)); kani::cover(r.is_some_and(|(a, _)| a > 4096), "a reject far into the haystack"); kani::cover(r.is_none(), "searched to the start"); } @@ -2816,13 +2813,13 @@ pub mod verify_char_searcher { // The match starts at a lead byte: its sequence ends on a boundary. kani::assume(utf8_ok_at(a)); } - check_result(&s, r); + check_result(s.haystack, r, char_searcher_inv(&s)); kani::cover(r.is_some_and(|(_, b)| b > 4096), "a match far into the haystack"); kani::cover(r.is_none(), "searched to the end"); } #[kani::proof] - #[kani::stub(crate::slice::memchr::memrchr, model_memrchr)] + #[kani::stub(crate::slice::memchr::memrchr, model_memchr)] #[kani::stub( >::equal_same_length, model_equal_same_length @@ -2834,7 +2831,7 @@ pub mod verify_char_searcher { // The match starts at a lead byte: its sequence ends on a boundary. kani::assume(utf8_ok_at(a)); } - check_result(&s, r); + check_result(s.haystack, r, char_searcher_inv(&s)); kani::cover(r.is_some_and(|(a, _)| a > 4096), "a match far into the haystack"); kani::cover(r.is_none(), "searched to the start"); } @@ -2843,7 +2840,7 @@ pub mod verify_char_searcher { /// input they return what upstream returns and consume the same bytes. #[kani::proof] #[kani::unwind(6)] - fn check_next_code_point_model_matches_upstream() { + fn check_decoder_models_match_upstream() { let bytes: [u8; 4] = kani::any(); let n: usize = kani::any_where(|n| *n >= 1 && *n <= 4); let s = &bytes[..n]; @@ -2853,17 +2850,6 @@ pub mod verify_char_searcher { let ra = unsafe { model_next_code_point(&mut a) }; let rb = unsafe { crate::str::validations::next_code_point(&mut b) }; assert!(ra == rb && a.as_slice().len() == b.as_slice().len()); - kani::cover(n == 4 && ra.is_some(), "a 4-byte character"); - } - - #[kani::proof] - #[kani::unwind(6)] - fn check_next_code_point_reverse_model_matches_upstream() { - let bytes: [u8; 4] = kani::any(); - let n: usize = kani::any_where(|n| *n >= 1 && *n <= 4); - let s = &bytes[..n]; - kani::assume(crate::str::from_utf8(s).is_ok()); - unsafe { GHOST = (s.as_ptr(), n) }; let (mut a, mut b) = (s.iter(), s.iter()); let ra = unsafe { model_next_code_point_reverse(&mut a) }; let rb = unsafe { crate::str::validations::next_code_point_reverse(&mut b) }; @@ -2926,18 +2912,6 @@ pub mod verify_char_searcher { MultiCharEqSearcher { char_eq, haystack, char_indices } } - /// As `check_result`, for `MultiCharEqSearcher`. - fn check_multi_char_eq_result( - s: &MultiCharEqSearcher<'_, C>, - range: Option<(usize, usize)>, - ) { - if let Some((a, b)) = range { - assert!(a <= b && b <= s.haystack.len()); - assert!(s.haystack.is_char_boundary(a) && s.haystack.is_char_boundary(b)); - } - assert!(s.kani_ok()); - } - /// The proofs for one `MultiCharEq` instance, through the searcher that /// wraps it: creation establishes `C` (criterion 1); `next` / `next_back` /// meet their contracts from any state that satisfies `C` (criteria 2 and @@ -2989,7 +2963,7 @@ pub mod verify_char_searcher { let $set: [char; 2] = kani::any(); let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); let r = s.next_match(); - check_multi_char_eq_result(&s.0, r); + check_result(s.0.haystack, r, s.0.kani_ok()); kani::cover(r.is_some_and(|(_, b)| b > 4096), "a match far into the haystack"); kani::cover(r.is_none(), "searched to the end"); } @@ -3000,7 +2974,7 @@ pub mod verify_char_searcher { let $set: [char; 2] = kani::any(); let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); let r = s.next_reject(); - check_multi_char_eq_result(&s.0, r); + check_result(s.0.haystack, r, s.0.kani_ok()); kani::cover(r.is_some_and(|(_, b)| b > 4096), "a reject far into the haystack"); kani::cover(r.is_none(), "searched to the end"); } @@ -3011,7 +2985,7 @@ pub mod verify_char_searcher { let $set: [char; 2] = kani::any(); let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); let r = s.next_match_back(); - check_multi_char_eq_result(&s.0, r); + check_result(s.0.haystack, r, s.0.kani_ok()); kani::cover(r.is_some_and(|(a, _)| a > 4096), "a match far into the haystack"); kani::cover(r.is_none(), "searched to the start"); } @@ -3022,7 +2996,7 @@ pub mod verify_char_searcher { let $set: [char; 2] = kani::any(); let mut s = $wrapper(any_multi_char_eq_searcher(any_haystack(), $eq)); let r = s.next_reject_back(); - check_multi_char_eq_result(&s.0, r); + check_result(s.0.haystack, r, s.0.kani_ok()); kani::cover(r.is_some_and(|(a, _)| a > 4096), "a reject far into the haystack"); kani::cover(r.is_none(), "searched to the start"); }