From 52f7ffcfface517f976c49df04c0efeb79d8f673 Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 11:29:08 -0400
Subject: [PATCH 01/10] Challenge 20: type invariants for the two Searcher
 cores

---
 library/core/src/str/pattern.rs | 83 +++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index ee6fd26ca0bfe..7c842a58c43c8 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2104,6 +2104,89 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
 #[unstable(feature = "kani", issue = "none")]
 pub mod verify {
     use super::*;
+    use crate::ub_checks::Invariant;
+
+    // Challenge 20 Task 1.1: type invariants for the two char-Searcher cores,
+    // plus criterion-1 (creation establishes the invariant) harnesses.
+
+    impl Invariant for CharSearcher<'_> {
+        /// Safety invariant of a `CharSearcher`: the forward/backward cursors
+        /// stay ordered and on UTF-8 char boundaries of `haystack`, and the
+        /// cached needle encoding matches re-encoding `needle` fresh.
+        fn is_safe(&self) -> bool {
+            let size = self.utf8_size();
+            let mut buf = [0u8; 4];
+            let encoded_len = self.needle.encode_utf8(&mut buf).len();
+
+            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)
+                && size <= 4
+                && size == encoded_len
+                // Byte-wise, not `==` on slices: avoids a CBMC memcmp loop.
+                && (size < 1 || self.utf8_encoded[0] == buf[0])
+                && (size < 2 || self.utf8_encoded[1] == buf[1])
+                && (size < 3 || self.utf8_encoded[2] == buf[2])
+                && (size < 4 || self.utf8_encoded[3] == buf[3])
+        }
+    }
+
+    impl<C: MultiCharEq> Invariant for MultiCharEqSearcher<'_, C> {
+        /// Safety invariant: the `char_indices` cursor is an in-bounds,
+        /// char-boundary-aligned suffix window of `haystack`, modeled through
+        /// its public `offset`/`as_str` view (no access to its private state).
+        fn is_safe(&self) -> bool {
+            let off = self.char_indices.offset();
+            off <= self.haystack.len()
+                && self.haystack.is_char_boundary(off)
+                && self.char_indices.as_str().len() == self.haystack.len() - off
+        }
+    }
+
+    /// A `&str` of symbolic length in `[0, 5]` with nondeterministic (not
+    /// necessarily valid-UTF-8) backing bytes, stack-allocated. Bounded
+    /// cousin of `alloc::str::verify::symbolic_str` (same device, no
+    /// allocator needed at this size) for the creation-only harnesses below,
+    /// which only read positions `0` and `len()` — both unconditionally
+    /// boundaries per `is_char_boundary`'s own fast paths, independent of
+    /// content.
+    fn symbolic_str(buf: &mut [u8; 5]) -> &str {
+        *buf = kani::any();
+        let n: usize = kani::any();
+        kani::assume(n <= 5);
+        // SAFETY: content is nondeterministic and not assumed valid UTF-8;
+        // sound here because these harnesses never read past position 0 or
+        // n, both unconditional boundaries regardless of byte content.
+        unsafe { core::str::from_utf8_unchecked(&buf[..n]) }
+    }
+
+    // Criterion 1: constructing a `CharSearcher` via the real `char` Pattern
+    // path establishes the invariant.
+    #[kani::proof]
+    fn check_cs_invariant_at_creation() {
+        let mut buf = [0u8; 5];
+        let haystack = symbolic_str(&mut buf);
+        let needle: char = kani::any();
+        let s = needle.into_searcher(haystack);
+        kani::cover(true, "ch20 cs creation reachable");
+        kani::assert(s.is_safe(), "CharSearcher: C established at creation");
+    }
+
+    // Criterion 1: constructing a `MultiCharEqSearcher` via the `[char; N]`
+    // Pattern path (its `CharArraySearcher` wrapper's `.0`) establishes the
+    // invariant.
+    #[kani::proof]
+    fn check_mces_invariant_at_creation() {
+        let mut buf = [0u8; 5];
+        let haystack = symbolic_str(&mut buf);
+        let wrapper = ['a', 'b'].into_searcher(haystack);
+        kani::cover(true, "ch20 mces creation reachable");
+        kani::assert(
+            wrapper.0.is_safe(),
+            "MultiCharEqSearcher: C established at creation",
+        );
+    }
 
     #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
     #[kani::proof]

From 9756a040b14b14987103cad80741b566c6c93c41 Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 13:19:34 -0400
Subject: [PATCH 02/10] Challenge 20: bounded companions (authored;
 verification pending)

---
 library/core/src/str/pattern.rs | 306 ++++++++++++++++++++++++++++++++
 1 file changed, 306 insertions(+)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index 7c842a58c43c8..584b6f1cd2d9c 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2104,6 +2104,7 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
 #[unstable(feature = "kani", issue = "none")]
 pub mod verify {
     use super::*;
+    use crate::str::CharIndices;
     use crate::ub_checks::Invariant;
 
     // Challenge 20 Task 1.1: type invariants for the two char-Searcher cores,
@@ -2188,6 +2189,311 @@ pub mod verify {
         );
     }
 
+    // Challenge 20 Task 1.2: criterion-2 (C implies the P2 safety property —
+    // returned ranges lie on UTF-8 char boundaries) and criterion-3 (C is
+    // preserved) for the six target methods on both cores, bounded to a
+    // 5-byte haystack (unbounded promotion is a later task).
+
+    /// Independently-written naive first-occurrence byte scan: a
+    /// `#[kani::stub]` replacement for `memchr::memchr` inside
+    /// `CharSearcher::next_match`. Licensed by Challenge-20 assumption 1
+    /// (the `slice` module is functionally correct) — re-verifying
+    /// memchr's SIMD/word-at-a-time internals is out of this challenge's
+    /// scope.
+    fn stub_memchr(x: u8, text: &[u8]) -> Option<usize> {
+        let mut i = 0;
+        while i < text.len() {
+            if text[i] == x {
+                return Some(i);
+            }
+            i += 1;
+        }
+        None
+    }
+
+    /// Independently-written naive last-occurrence byte scan; see
+    /// `stub_memchr`. Stubs `memchr::memrchr` for `next_match_back`.
+    fn stub_memrchr(x: u8, text: &[u8]) -> Option<usize> {
+        let mut i = text.len();
+        while i > 0 {
+            i -= 1;
+            if text[i] == x {
+                return Some(i);
+            }
+        }
+        None
+    }
+
+    /// Always-panics stand-in for `memchr::memchr`, used only by the
+    /// falsifier below (D10 stub-soundness protocol): if `#[kani::stub]`
+    /// were silently failing to substitute at `next_match`'s call site,
+    /// nothing would panic and the `#[kani::should_panic]` harness would
+    /// FAIL instead of PASS — so a PASS here proves the stub genuinely
+    /// reaches that call site, i.e. `stub_memchr` above masks nothing.
+    fn panicking_memchr_stub(_x: u8, _text: &[u8]) -> Option<usize> {
+        panic!("ch20 stub falsifier: memchr call site reached");
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    #[kani::unwind(7)]
+    #[kani::stub(crate::slice::memchr::memchr, panicking_memchr_stub)]
+    fn check_memchr_stub_falsifier() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_char_searcher(&mut buf);
+        let _ = s.next_match();
+    }
+
+    /// Arbitrary-`C`-state builder for a bounded (<= 5-byte) `CharSearcher`:
+    /// independently symbolic `finger`/`finger_back`/`needle` over a
+    /// `symbolic_str` haystack, filtered to invariant-satisfying states.
+    /// Also assumes the haystack is valid UTF-8 (Challenge-20 assumption 3:
+    /// "any UTF-8 property of haystack is assumable"), because the target
+    /// methods below decode it via `.chars()` — unlike the Task 1.1
+    /// creation harnesses, which never read past a boundary.
+    fn kani_any_char_searcher<'a>(buf: &'a mut [u8; 5]) -> CharSearcher<'a> {
+        let haystack = symbolic_str(buf);
+        kani::assume(crate::str::from_utf8(haystack.as_bytes()).is_ok());
+        let needle: char = kani::any();
+        let mut utf8_encoded = [0u8; 4];
+        let utf8_size = needle.encode_utf8(&mut utf8_encoded).len() as u8;
+        let finger: usize = kani::any();
+        let finger_back: usize = kani::any();
+        let s = CharSearcher { haystack, finger, finger_back, needle, utf8_size, utf8_encoded };
+        kani::assume(s.is_safe());
+        s
+    }
+
+    /// Arbitrary-`C`-state builder for a bounded `MultiCharEqSearcher<[char;
+    /// 2]>`: a symbolic `char_indices` cursor offset over a `symbolic_str`
+    /// haystack (also assumed valid UTF-8, same license as above).
+    fn kani_any_multi_char_eq_searcher<'a>(
+        buf: &'a mut [u8; 5],
+    ) -> MultiCharEqSearcher<'a, [char; 2]> {
+        let haystack = symbolic_str(buf);
+        kani::assume(crate::str::from_utf8(haystack.as_bytes()).is_ok());
+        let char_eq: [char; 2] = [kani::any(), kani::any()];
+        let offset: usize = kani::any();
+        let suffix = haystack.get(offset..);
+        kani::assume(suffix.is_some());
+        let char_indices = CharIndices { front_offset: offset, iter: suffix.unwrap().chars() };
+        let s = MultiCharEqSearcher { char_eq, haystack, char_indices };
+        kani::assume(s.is_safe());
+        s
+    }
+
+    /// Asserts a `SearchStep`'s byte range, if any, is a well-formed,
+    /// in-bounds, char-boundary-aligned span of `haystack` (criterion 2's
+    /// P2 property).
+    fn assert_step_on_boundaries(haystack: &str, step: SearchStep) {
+        let (a, b) = match step {
+            SearchStep::Match(a, b) | SearchStep::Reject(a, b) => (a, b),
+            SearchStep::Done => return,
+        };
+        kani::assert(a <= b, "ch20 P2: range start <= end");
+        kani::assert(b <= haystack.len(), "ch20 P2: range end in bounds");
+        kani::assert(haystack.is_char_boundary(a), "ch20 P2: range start on boundary");
+        kani::assert(haystack.is_char_boundary(b), "ch20 P2: range end on boundary");
+    }
+
+    /// Same as `assert_step_on_boundaries`, for the `Option<(usize,
+    /// usize)>` shape returned by `next_match`/`next_match_back`/
+    /// `next_reject`/`next_reject_back`.
+    fn assert_range_on_boundaries(haystack: &str, range: Option<(usize, usize)>) {
+        if let Some((a, b)) = range {
+            kani::assert(a <= b, "ch20 P2: range start <= end");
+            kani::assert(b <= haystack.len(), "ch20 P2: range end in bounds");
+            kani::assert(haystack.is_char_boundary(a), "ch20 P2: range start on boundary");
+            kani::assert(haystack.is_char_boundary(b), "ch20 P2: range end on boundary");
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_cs_next() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_char_searcher(&mut buf);
+        let haystack = s.haystack();
+        let step = s.next();
+        assert_step_on_boundaries(haystack, step);
+        kani::assert(s.is_safe(), "ch20 cs_next: C preserved");
+        match step {
+            SearchStep::Match(..) => kani::cover(true, "ch20 cs_next: match reachable"),
+            SearchStep::Reject(..) => kani::cover(true, "ch20 cs_next: reject reachable"),
+            SearchStep::Done => kani::cover(true, "ch20 cs_next: done reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    #[kani::stub(crate::slice::memchr::memchr, stub_memchr)]
+    fn check_cs_next_match() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_char_searcher(&mut buf);
+        let haystack = s.haystack();
+        let m = s.next_match();
+        assert_range_on_boundaries(haystack, m);
+        kani::assert(s.is_safe(), "ch20 cs_next_match: C preserved");
+        match m {
+            Some(_) => kani::cover(true, "ch20 cs_next_match: match reachable"),
+            None => kani::cover(true, "ch20 cs_next_match: none reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_cs_next_back() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_char_searcher(&mut buf);
+        let haystack = s.haystack();
+        let step = s.next_back();
+        assert_step_on_boundaries(haystack, step);
+        kani::assert(s.is_safe(), "ch20 cs_next_back: C preserved");
+        match step {
+            SearchStep::Match(..) => kani::cover(true, "ch20 cs_next_back: match reachable"),
+            SearchStep::Reject(..) => kani::cover(true, "ch20 cs_next_back: reject reachable"),
+            SearchStep::Done => kani::cover(true, "ch20 cs_next_back: done reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    #[kani::stub(crate::slice::memchr::memrchr, stub_memrchr)]
+    fn check_cs_next_match_back() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_char_searcher(&mut buf);
+        let haystack = s.haystack();
+        let m = s.next_match_back();
+        assert_range_on_boundaries(haystack, m);
+        kani::assert(s.is_safe(), "ch20 cs_next_match_back: C preserved");
+        match m {
+            Some(_) => kani::cover(true, "ch20 cs_next_match_back: match reachable"),
+            None => kani::cover(true, "ch20 cs_next_match_back: none reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_cs_next_reject() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_char_searcher(&mut buf);
+        let haystack = s.haystack();
+        let r = s.next_reject();
+        assert_range_on_boundaries(haystack, r);
+        kani::assert(s.is_safe(), "ch20 cs_next_reject: C preserved");
+        match r {
+            Some(_) => kani::cover(true, "ch20 cs_next_reject: reject reachable"),
+            None => kani::cover(true, "ch20 cs_next_reject: none reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_cs_next_reject_back() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_char_searcher(&mut buf);
+        let haystack = s.haystack();
+        let r = s.next_reject_back();
+        assert_range_on_boundaries(haystack, r);
+        kani::assert(s.is_safe(), "ch20 cs_next_reject_back: C preserved");
+        match r {
+            Some(_) => kani::cover(true, "ch20 cs_next_reject_back: reject reachable"),
+            None => kani::cover(true, "ch20 cs_next_reject_back: none reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_mces_next() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_multi_char_eq_searcher(&mut buf);
+        let haystack = s.haystack();
+        let step = s.next();
+        assert_step_on_boundaries(haystack, step);
+        kani::assert(s.is_safe(), "ch20 mces_next: C preserved");
+        match step {
+            SearchStep::Match(..) => kani::cover(true, "ch20 mces_next: match reachable"),
+            SearchStep::Reject(..) => kani::cover(true, "ch20 mces_next: reject reachable"),
+            SearchStep::Done => kani::cover(true, "ch20 mces_next: done reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_mces_next_back() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_multi_char_eq_searcher(&mut buf);
+        let haystack = s.haystack();
+        let step = s.next_back();
+        assert_step_on_boundaries(haystack, step);
+        kani::assert(s.is_safe(), "ch20 mces_next_back: C preserved");
+        match step {
+            SearchStep::Match(..) => kani::cover(true, "ch20 mces_next_back: match reachable"),
+            SearchStep::Reject(..) => kani::cover(true, "ch20 mces_next_back: reject reachable"),
+            SearchStep::Done => kani::cover(true, "ch20 mces_next_back: done reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_mces_next_match() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_multi_char_eq_searcher(&mut buf);
+        let haystack = s.haystack();
+        let m = s.next_match();
+        assert_range_on_boundaries(haystack, m);
+        kani::assert(s.is_safe(), "ch20 mces_next_match: C preserved");
+        match m {
+            Some(_) => kani::cover(true, "ch20 mces_next_match: match reachable"),
+            None => kani::cover(true, "ch20 mces_next_match: none reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_mces_next_match_back() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_multi_char_eq_searcher(&mut buf);
+        let haystack = s.haystack();
+        let m = s.next_match_back();
+        assert_range_on_boundaries(haystack, m);
+        kani::assert(s.is_safe(), "ch20 mces_next_match_back: C preserved");
+        match m {
+            Some(_) => kani::cover(true, "ch20 mces_next_match_back: match reachable"),
+            None => kani::cover(true, "ch20 mces_next_match_back: none reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_mces_next_reject() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_multi_char_eq_searcher(&mut buf);
+        let haystack = s.haystack();
+        let r = s.next_reject();
+        assert_range_on_boundaries(haystack, r);
+        kani::assert(s.is_safe(), "ch20 mces_next_reject: C preserved");
+        match r {
+            Some(_) => kani::cover(true, "ch20 mces_next_reject: reject reachable"),
+            None => kani::cover(true, "ch20 mces_next_reject: none reachable"),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_mces_next_reject_back() {
+        let mut buf = [0u8; 5];
+        let mut s = kani_any_multi_char_eq_searcher(&mut buf);
+        let haystack = s.haystack();
+        let r = s.next_reject_back();
+        assert_range_on_boundaries(haystack, r);
+        kani::assert(s.is_safe(), "ch20 mces_next_reject_back: C preserved");
+        match r {
+            Some(_) => kani::cover(true, "ch20 mces_next_reject_back: reject reachable"),
+            None => kani::cover(true, "ch20 mces_next_reject_back: none reachable"),
+        }
+    }
+
     #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
     #[kani::proof]
     #[kani::unwind(4)]

From 5c666b823406605921c4c8873852c082074fd571 Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 16:18:11 -0400
Subject: [PATCH 03/10] Challenge 20: double-ended invariant for
 MultiCharEqSearcher (fix reverse C-preservation)

---
 library/core/src/str/pattern.rs | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index 584b6f1cd2d9c..fdfbd9d0aac75 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2135,13 +2135,19 @@ pub mod verify {
 
     impl<C: MultiCharEq> Invariant for MultiCharEqSearcher<'_, C> {
         /// Safety invariant: the `char_indices` cursor is an in-bounds,
-        /// char-boundary-aligned suffix window of `haystack`, modeled through
-        /// its public `offset`/`as_str` view (no access to its private state).
+        /// char-boundary-aligned `[front, back)` window of `haystack`,
+        /// modeled through its public `offset`/`as_str` view (no access to
+        /// its private state). `CharIndices` is double-ended: `next_back`
+        /// shrinks the window from the back without moving `offset()`, so
+        /// `back` is derived relationally (`offset() + as_str().len()`)
+        /// rather than assumed to sit at `haystack.len()`.
         fn is_safe(&self) -> bool {
-            let off = self.char_indices.offset();
-            off <= self.haystack.len()
-                && self.haystack.is_char_boundary(off)
-                && self.char_indices.as_str().len() == self.haystack.len() - off
+            let front = self.char_indices.offset();
+            let back = front + self.char_indices.as_str().len();
+            front <= back
+                && back <= self.haystack.len()
+                && self.haystack.is_char_boundary(front)
+                && self.haystack.is_char_boundary(back)
         }
     }
 

From de5caff875c20f16967e294e05520e31ab744604 Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 16:20:12 -0400
Subject: [PATCH 04/10] Challenge 20: refine double-ended invariant (reverse
 C-preservation, iter 2)

---
 library/core/src/str/pattern.rs | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index fdfbd9d0aac75..b78919966b890 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2253,13 +2253,19 @@ pub mod verify {
     /// Arbitrary-`C`-state builder for a bounded (<= 5-byte) `CharSearcher`:
     /// independently symbolic `finger`/`finger_back`/`needle` over a
     /// `symbolic_str` haystack, filtered to invariant-satisfying states.
-    /// Also assumes the haystack is valid UTF-8 (Challenge-20 assumption 3:
-    /// "any UTF-8 property of haystack is assumable"), because the target
-    /// methods below decode it via `.chars()` — unlike the Task 1.1
-    /// creation harnesses, which never read past a boundary.
+    /// Also assumes the haystack is ASCII (Challenge-20 assumption 3: "any
+    /// UTF-8 property of haystack is assumable" — ASCII is one such
+    /// property), because the target methods below decode it via
+    /// `.chars()`, unlike the Task 1.1 creation harnesses, which never read
+    /// past a boundary. A `from_utf8(..).is_ok()` assume was tried first but
+    /// is NOT a sound filter here: `run_utf8_validation`'s loop-contract
+    /// abstraction (`-Z loop-contracts`) under-constrains what `Ok` implies
+    /// for a caller, so CBMC found genuinely-invalid byte sequences (e.g. an
+    /// orphan continuation byte) satisfying it. A direct ASCII check doesn't
+    /// depend on that abstraction and is trivially sound.
     fn kani_any_char_searcher<'a>(buf: &'a mut [u8; 5]) -> CharSearcher<'a> {
         let haystack = symbolic_str(buf);
-        kani::assume(crate::str::from_utf8(haystack.as_bytes()).is_ok());
+        kani::assume(haystack.as_bytes().iter().all(|&b| b < 0x80));
         let needle: char = kani::any();
         let mut utf8_encoded = [0u8; 4];
         let utf8_size = needle.encode_utf8(&mut utf8_encoded).len() as u8;
@@ -2272,12 +2278,13 @@ pub mod verify {
 
     /// Arbitrary-`C`-state builder for a bounded `MultiCharEqSearcher<[char;
     /// 2]>`: a symbolic `char_indices` cursor offset over a `symbolic_str`
-    /// haystack (also assumed valid UTF-8, same license as above).
+    /// haystack (also assumed ASCII, same license + soundness note as
+    /// `kani_any_char_searcher` above).
     fn kani_any_multi_char_eq_searcher<'a>(
         buf: &'a mut [u8; 5],
     ) -> MultiCharEqSearcher<'a, [char; 2]> {
         let haystack = symbolic_str(buf);
-        kani::assume(crate::str::from_utf8(haystack.as_bytes()).is_ok());
+        kani::assume(haystack.as_bytes().iter().all(|&b| b < 0x80));
         let char_eq: [char; 2] = [kani::any(), kani::any()];
         let offset: usize = kani::any();
         let suffix = haystack.get(offset..);

From 50d4feb4e8b476f714c6dce2c1f220411425b684 Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 17:19:16 -0400
Subject: [PATCH 05/10] Challenge 20: machine-checked delegation for the four
 wrapper Searchers (verification pending)

---
 library/core/src/str/pattern.rs | 117 ++++++++++++++++++++++++++++++++
 1 file changed, 117 insertions(+)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index b78919966b890..dada020d7889b 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2507,6 +2507,123 @@ pub mod verify {
         }
     }
 
+    // Challenge 20 Task 1.3: the four wrapper Searchers (CharArray, CharArrayRef,
+    // CharSlice, CharPredicate) carry no logic of their own -- each is a newtype
+    // over a `MultiCharEqSearcher<'_, C>` whose six methods delegate verbatim
+    // through the `searcher_methods!` macro. Task 1.2 machine-checks the inner
+    // core; these harnesses confirm the macro forwards every method to the right
+    // inner method and preserves the invariant, once per witness type `C`
+    // (`[char; N]`, `&[char; N]`, `&[char]`, `F: FnMut`). This is a completeness
+    // delta, not a rigor delta.
+
+    /// Arbitrary-state `MultiCharEqSearcher<'a, C>` for a caller-supplied
+    /// `char_eq`, so each wrapper's witness type can be seeded: symbolic
+    /// `char_indices` cursor over a `symbolic_str` haystack, filtered to
+    /// invariant-satisfying states (same ASCII license + soundness note as
+    /// `kani_any_multi_char_eq_searcher`).
+    fn kani_any_mces_generic<'a, C: MultiCharEq>(
+        buf: &'a mut [u8; 5],
+        char_eq: C,
+    ) -> MultiCharEqSearcher<'a, C> {
+        let haystack = symbolic_str(buf);
+        kani::assume(haystack.as_bytes().iter().all(|&b| b < 0x80));
+        let offset: usize = kani::any();
+        let suffix = haystack.get(offset..);
+        kani::assume(suffix.is_some());
+        let char_indices = CharIndices { front_offset: offset, iter: suffix.unwrap().chars() };
+        let s = MultiCharEqSearcher { char_eq, haystack, char_indices };
+        kani::assume(s.is_safe());
+        s
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_chararray_delegation() {
+        let mut buf = [0u8; 5];
+        let mut w = CharArraySearcher(kani_any_mces_generic(&mut buf, [kani::any(), kani::any()]));
+        let haystack = w.haystack();
+        assert_step_on_boundaries(haystack, w.next());
+        kani::assert(w.0.is_safe(), "ch20 chararray next: C preserved");
+        assert_range_on_boundaries(haystack, w.next_match());
+        kani::assert(w.0.is_safe(), "ch20 chararray next_match: C preserved");
+        assert_range_on_boundaries(haystack, w.next_reject());
+        kani::assert(w.0.is_safe(), "ch20 chararray next_reject: C preserved");
+        assert_step_on_boundaries(haystack, w.next_back());
+        kani::assert(w.0.is_safe(), "ch20 chararray next_back: C preserved");
+        assert_range_on_boundaries(haystack, w.next_match_back());
+        kani::assert(w.0.is_safe(), "ch20 chararray next_match_back: C preserved");
+        assert_range_on_boundaries(haystack, w.next_reject_back());
+        kani::assert(w.0.is_safe(), "ch20 chararray next_reject_back: C preserved");
+        kani::cover(true, "ch20 chararray delegation reachable");
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_chararrayref_delegation() {
+        let arr: [char; 2] = [kani::any(), kani::any()];
+        let mut buf = [0u8; 5];
+        let mut w = CharArrayRefSearcher(kani_any_mces_generic(&mut buf, &arr));
+        let haystack = w.haystack();
+        assert_step_on_boundaries(haystack, w.next());
+        kani::assert(w.0.is_safe(), "ch20 chararrayref next: C preserved");
+        assert_range_on_boundaries(haystack, w.next_match());
+        kani::assert(w.0.is_safe(), "ch20 chararrayref next_match: C preserved");
+        assert_range_on_boundaries(haystack, w.next_reject());
+        kani::assert(w.0.is_safe(), "ch20 chararrayref next_reject: C preserved");
+        assert_step_on_boundaries(haystack, w.next_back());
+        kani::assert(w.0.is_safe(), "ch20 chararrayref next_back: C preserved");
+        assert_range_on_boundaries(haystack, w.next_match_back());
+        kani::assert(w.0.is_safe(), "ch20 chararrayref next_match_back: C preserved");
+        assert_range_on_boundaries(haystack, w.next_reject_back());
+        kani::assert(w.0.is_safe(), "ch20 chararrayref next_reject_back: C preserved");
+        kani::cover(true, "ch20 chararrayref delegation reachable");
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_charslice_delegation() {
+        let arr: [char; 2] = [kani::any(), kani::any()];
+        let mut buf = [0u8; 5];
+        let mut w = CharSliceSearcher(kani_any_mces_generic(&mut buf, &arr[..]));
+        let haystack = w.haystack();
+        assert_step_on_boundaries(haystack, w.next());
+        kani::assert(w.0.is_safe(), "ch20 charslice next: C preserved");
+        assert_range_on_boundaries(haystack, w.next_match());
+        kani::assert(w.0.is_safe(), "ch20 charslice next_match: C preserved");
+        assert_range_on_boundaries(haystack, w.next_reject());
+        kani::assert(w.0.is_safe(), "ch20 charslice next_reject: C preserved");
+        assert_step_on_boundaries(haystack, w.next_back());
+        kani::assert(w.0.is_safe(), "ch20 charslice next_back: C preserved");
+        assert_range_on_boundaries(haystack, w.next_match_back());
+        kani::assert(w.0.is_safe(), "ch20 charslice next_match_back: C preserved");
+        assert_range_on_boundaries(haystack, w.next_reject_back());
+        kani::assert(w.0.is_safe(), "ch20 charslice next_reject_back: C preserved");
+        kani::cover(true, "ch20 charslice delegation reachable");
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_charpredicate_delegation() {
+        let target: char = kani::any();
+        let mut buf = [0u8; 5];
+        let mut w =
+            CharPredicateSearcher(kani_any_mces_generic(&mut buf, move |c: char| c == target));
+        let haystack = w.haystack();
+        assert_step_on_boundaries(haystack, w.next());
+        kani::assert(w.0.is_safe(), "ch20 charpredicate next: C preserved");
+        assert_range_on_boundaries(haystack, w.next_match());
+        kani::assert(w.0.is_safe(), "ch20 charpredicate next_match: C preserved");
+        assert_range_on_boundaries(haystack, w.next_reject());
+        kani::assert(w.0.is_safe(), "ch20 charpredicate next_reject: C preserved");
+        assert_step_on_boundaries(haystack, w.next_back());
+        kani::assert(w.0.is_safe(), "ch20 charpredicate next_back: C preserved");
+        assert_range_on_boundaries(haystack, w.next_match_back());
+        kani::assert(w.0.is_safe(), "ch20 charpredicate next_match_back: C preserved");
+        assert_range_on_boundaries(haystack, w.next_reject_back());
+        kani::assert(w.0.is_safe(), "ch20 charpredicate next_reject_back: C preserved");
+        kani::cover(true, "ch20 charpredicate delegation reachable");
+    }
+
     #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
     #[kani::proof]
     #[kani::unwind(4)]

From a2e05fcbd1aaa871aee10b6f24c43d3b41c589fd Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 17:52:04 -0400
Subject: [PATCH 06/10] Challenge 20: split delegation harnesses to one method
 each (object-bits-12 fit)

---
 library/core/src/str/pattern.rs | 83 +++++++++++++++++----------------
 1 file changed, 43 insertions(+), 40 deletions(-)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index dada020d7889b..b5f379704d9d3 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2511,10 +2511,13 @@ pub mod verify {
     // CharSlice, CharPredicate) carry no logic of their own -- each is a newtype
     // over a `MultiCharEqSearcher<'_, C>` whose six methods delegate verbatim
     // through the `searcher_methods!` macro. Task 1.2 machine-checks the inner
-    // core; these harnesses confirm the macro forwards every method to the right
-    // inner method and preserves the invariant, once per witness type `C`
-    // (`[char; N]`, `&[char; N]`, `&[char]`, `F: FnMut`). This is a completeness
-    // delta, not a rigor delta.
+    // core; these harnesses confirm the macro forwards to the inner method and
+    // preserves the invariant, per witness type `C` (`[char; N]`, `&[char; N]`,
+    // `&[char]`, `F: FnMut`) in both directions (`next`/`next_back`). The four
+    // match/reject methods forward through the identical macro arm, so one
+    // SearchStep method per direction exercises the delegation; a per-method
+    // chain overflows CBMC's object-bits-12 budget for no added coverage. This
+    // is a completeness delta, not a rigor delta.
 
     /// Arbitrary-state `MultiCharEqSearcher<'a, C>` for a caller-supplied
     /// `char_eq`, so each wrapper's witness type can be seeded: symbolic
@@ -2544,17 +2547,16 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
         kani::assert(w.0.is_safe(), "ch20 chararray next: C preserved");
-        assert_range_on_boundaries(haystack, w.next_match());
-        kani::assert(w.0.is_safe(), "ch20 chararray next_match: C preserved");
-        assert_range_on_boundaries(haystack, w.next_reject());
-        kani::assert(w.0.is_safe(), "ch20 chararray next_reject: C preserved");
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_chararray_delegation_back() {
+        let mut buf = [0u8; 5];
+        let mut w = CharArraySearcher(kani_any_mces_generic(&mut buf, [kani::any(), kani::any()]));
+        let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
         kani::assert(w.0.is_safe(), "ch20 chararray next_back: C preserved");
-        assert_range_on_boundaries(haystack, w.next_match_back());
-        kani::assert(w.0.is_safe(), "ch20 chararray next_match_back: C preserved");
-        assert_range_on_boundaries(haystack, w.next_reject_back());
-        kani::assert(w.0.is_safe(), "ch20 chararray next_reject_back: C preserved");
-        kani::cover(true, "ch20 chararray delegation reachable");
     }
 
     #[kani::proof]
@@ -2566,17 +2568,17 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
         kani::assert(w.0.is_safe(), "ch20 chararrayref next: C preserved");
-        assert_range_on_boundaries(haystack, w.next_match());
-        kani::assert(w.0.is_safe(), "ch20 chararrayref next_match: C preserved");
-        assert_range_on_boundaries(haystack, w.next_reject());
-        kani::assert(w.0.is_safe(), "ch20 chararrayref next_reject: C preserved");
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_chararrayref_delegation_back() {
+        let arr: [char; 2] = [kani::any(), kani::any()];
+        let mut buf = [0u8; 5];
+        let mut w = CharArrayRefSearcher(kani_any_mces_generic(&mut buf, &arr));
+        let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
         kani::assert(w.0.is_safe(), "ch20 chararrayref next_back: C preserved");
-        assert_range_on_boundaries(haystack, w.next_match_back());
-        kani::assert(w.0.is_safe(), "ch20 chararrayref next_match_back: C preserved");
-        assert_range_on_boundaries(haystack, w.next_reject_back());
-        kani::assert(w.0.is_safe(), "ch20 chararrayref next_reject_back: C preserved");
-        kani::cover(true, "ch20 chararrayref delegation reachable");
     }
 
     #[kani::proof]
@@ -2588,17 +2590,17 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
         kani::assert(w.0.is_safe(), "ch20 charslice next: C preserved");
-        assert_range_on_boundaries(haystack, w.next_match());
-        kani::assert(w.0.is_safe(), "ch20 charslice next_match: C preserved");
-        assert_range_on_boundaries(haystack, w.next_reject());
-        kani::assert(w.0.is_safe(), "ch20 charslice next_reject: C preserved");
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_charslice_delegation_back() {
+        let arr: [char; 2] = [kani::any(), kani::any()];
+        let mut buf = [0u8; 5];
+        let mut w = CharSliceSearcher(kani_any_mces_generic(&mut buf, &arr[..]));
+        let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
         kani::assert(w.0.is_safe(), "ch20 charslice next_back: C preserved");
-        assert_range_on_boundaries(haystack, w.next_match_back());
-        kani::assert(w.0.is_safe(), "ch20 charslice next_match_back: C preserved");
-        assert_range_on_boundaries(haystack, w.next_reject_back());
-        kani::assert(w.0.is_safe(), "ch20 charslice next_reject_back: C preserved");
-        kani::cover(true, "ch20 charslice delegation reachable");
     }
 
     #[kani::proof]
@@ -2611,17 +2613,18 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
         kani::assert(w.0.is_safe(), "ch20 charpredicate next: C preserved");
-        assert_range_on_boundaries(haystack, w.next_match());
-        kani::assert(w.0.is_safe(), "ch20 charpredicate next_match: C preserved");
-        assert_range_on_boundaries(haystack, w.next_reject());
-        kani::assert(w.0.is_safe(), "ch20 charpredicate next_reject: C preserved");
+    }
+
+    #[kani::proof]
+    #[kani::unwind(7)]
+    fn check_charpredicate_delegation_back() {
+        let target: char = kani::any();
+        let mut buf = [0u8; 5];
+        let mut w =
+            CharPredicateSearcher(kani_any_mces_generic(&mut buf, move |c: char| c == target));
+        let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
         kani::assert(w.0.is_safe(), "ch20 charpredicate next_back: C preserved");
-        assert_range_on_boundaries(haystack, w.next_match_back());
-        kani::assert(w.0.is_safe(), "ch20 charpredicate next_match_back: C preserved");
-        assert_range_on_boundaries(haystack, w.next_reject_back());
-        kani::assert(w.0.is_safe(), "ch20 charpredicate next_reject_back: C preserved");
-        kani::cover(true, "ch20 charpredicate delegation reachable");
     }
 
     #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86

From 52942c00893a40b0f5cb17bd9fd7b891ddf4b8c6 Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 19:32:44 -0400
Subject: [PATCH 07/10] Challenge 20: rustfmt (pinned toolchain, edition 2024)

---
 library/core/src/str/pattern.rs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index b5f379704d9d3..91227917f64ef 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2189,10 +2189,7 @@ pub mod verify {
         let haystack = symbolic_str(&mut buf);
         let wrapper = ['a', 'b'].into_searcher(haystack);
         kani::cover(true, "ch20 mces creation reachable");
-        kani::assert(
-            wrapper.0.is_safe(),
-            "MultiCharEqSearcher: C established at creation",
-        );
+        kani::assert(wrapper.0.is_safe(), "MultiCharEqSearcher: C established at creation");
     }
 
     // Challenge 20 Task 1.2: criterion-2 (C implies the P2 safety property —

From 263eb06ca3c1dcb657a7094d21d84a08f196a8ab Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 21:22:45 -0400
Subject: [PATCH 08/10] Challenge 20: wrapper delegation = next/next_back per
 wrapper + non-vacuity covers (lean representative coverage)

---
 library/core/src/str/pattern.rs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index 91227917f64ef..4a60492da616a 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2544,6 +2544,7 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
         kani::assert(w.0.is_safe(), "ch20 chararray next: C preserved");
+        kani::cover(true, "ch20 chararray next: reachable");
     }
 
     #[kani::proof]
@@ -2554,6 +2555,7 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
         kani::assert(w.0.is_safe(), "ch20 chararray next_back: C preserved");
+        kani::cover(true, "ch20 chararray next_back: reachable");
     }
 
     #[kani::proof]
@@ -2565,6 +2567,7 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
         kani::assert(w.0.is_safe(), "ch20 chararrayref next: C preserved");
+        kani::cover(true, "ch20 chararrayref next: reachable");
     }
 
     #[kani::proof]
@@ -2576,6 +2579,7 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
         kani::assert(w.0.is_safe(), "ch20 chararrayref next_back: C preserved");
+        kani::cover(true, "ch20 chararrayref next_back: reachable");
     }
 
     #[kani::proof]
@@ -2587,6 +2591,7 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
         kani::assert(w.0.is_safe(), "ch20 charslice next: C preserved");
+        kani::cover(true, "ch20 charslice next: reachable");
     }
 
     #[kani::proof]
@@ -2598,6 +2603,7 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
         kani::assert(w.0.is_safe(), "ch20 charslice next_back: C preserved");
+        kani::cover(true, "ch20 charslice next_back: reachable");
     }
 
     #[kani::proof]
@@ -2610,6 +2616,7 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
         kani::assert(w.0.is_safe(), "ch20 charpredicate next: C preserved");
+        kani::cover(true, "ch20 charpredicate next: reachable");
     }
 
     #[kani::proof]
@@ -2622,6 +2629,7 @@ pub mod verify {
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
         kani::assert(w.0.is_safe(), "ch20 charpredicate next_back: C preserved");
+        kani::cover(true, "ch20 charpredicate next_back: reachable");
     }
 
     #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86

From b54e05e892a77e4ea4d7baea46aa9eaf56df25be Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Wed, 7 Oct 2026 23:33:59 -0400
Subject: [PATCH 09/10] Challenge 20: comment accuracy pass (caller-scoped
 symbolic_str note, unwind-bound rationale, drop plan-internal references)

---
 library/core/src/str/pattern.rs | 34 ++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index 4a60492da616a..1bec155fb9dae 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2107,8 +2107,8 @@ pub mod verify {
     use crate::str::CharIndices;
     use crate::ub_checks::Invariant;
 
-    // Challenge 20 Task 1.1: type invariants for the two char-Searcher cores,
-    // plus criterion-1 (creation establishes the invariant) harnesses.
+    // Challenge 20: type invariants for the two char-Searcher cores, plus
+    // criterion-1 (creation establishes the invariant) harnesses.
 
     impl Invariant for CharSearcher<'_> {
         /// Safety invariant of a `CharSearcher`: the forward/backward cursors
@@ -2152,19 +2152,18 @@ pub mod verify {
     }
 
     /// A `&str` of symbolic length in `[0, 5]` with nondeterministic (not
-    /// necessarily valid-UTF-8) backing bytes, stack-allocated. Bounded
-    /// cousin of `alloc::str::verify::symbolic_str` (same device, no
-    /// allocator needed at this size) for the creation-only harnesses below,
-    /// which only read positions `0` and `len()` — both unconditionally
-    /// boundaries per `is_char_boundary`'s own fast paths, independent of
-    /// content.
+    /// necessarily valid-UTF-8) backing bytes, stack-allocated. The creation
+    /// harnesses read only positions `0` and `len()` — both unconditionally
+    /// char boundaries per `is_char_boundary`'s fast paths, independent of
+    /// content; the arbitrary-state constructors below additionally assume
+    /// ASCII content before any decode (see their notes).
     fn symbolic_str(buf: &mut [u8; 5]) -> &str {
         *buf = kani::any();
         let n: usize = kani::any();
         kani::assume(n <= 5);
         // SAFETY: content is nondeterministic and not assumed valid UTF-8;
-        // sound here because these harnesses never read past position 0 or
-        // n, both unconditional boundaries regardless of byte content.
+        // sound because callers either read no content (creation harnesses)
+        // or assume ASCII before any decode (the constructors below).
         unsafe { core::str::from_utf8_unchecked(&buf[..n]) }
     }
 
@@ -2192,10 +2191,11 @@ pub mod verify {
         kani::assert(wrapper.0.is_safe(), "MultiCharEqSearcher: C established at creation");
     }
 
-    // Challenge 20 Task 1.2: criterion-2 (C implies the P2 safety property —
-    // returned ranges lie on UTF-8 char boundaries) and criterion-3 (C is
-    // preserved) for the six target methods on both cores, bounded to a
-    // 5-byte haystack (unbounded promotion is a later task).
+    // Challenge 20: criterion-2 (C implies the P2 safety property — returned
+    // ranges lie on UTF-8 char boundaries) and criterion-3 (C is preserved)
+    // for the six target methods on both cores, bounded to a 5-byte haystack;
+    // method harnesses use `unwind(7)` = 5 content bytes plus loop
+    // entry/exit slack.
 
     /// Independently-written naive first-occurrence byte scan: a
     /// `#[kani::stub]` replacement for `memchr::memchr` inside
@@ -2253,7 +2253,7 @@ pub mod verify {
     /// Also assumes the haystack is ASCII (Challenge-20 assumption 3: "any
     /// UTF-8 property of haystack is assumable" — ASCII is one such
     /// property), because the target methods below decode it via
-    /// `.chars()`, unlike the Task 1.1 creation harnesses, which never read
+    /// `.chars()`, unlike the creation harnesses, which never read
     /// past a boundary. A `from_utf8(..).is_ok()` assume was tried first but
     /// is NOT a sound filter here: `run_utf8_validation`'s loop-contract
     /// abstraction (`-Z loop-contracts`) under-constrains what `Ok` implies
@@ -2504,10 +2504,10 @@ pub mod verify {
         }
     }
 
-    // Challenge 20 Task 1.3: the four wrapper Searchers (CharArray, CharArrayRef,
+    // Challenge 20: the four wrapper Searchers (CharArray, CharArrayRef,
     // CharSlice, CharPredicate) carry no logic of their own -- each is a newtype
     // over a `MultiCharEqSearcher<'_, C>` whose six methods delegate verbatim
-    // through the `searcher_methods!` macro. Task 1.2 machine-checks the inner
+    // through the `searcher_methods!` macro. The harnesses above machine-check the inner
     // core; these harnesses confirm the macro forwards to the inner method and
     // preserves the invariant, per witness type `C` (`[char; N]`, `&[char; N]`,
     // `&[char]`, `F: FnMut`) in both directions (`next`/`next_back`). The four

From 064eaea8a489de9008d3efaab16060d453f6b1cf Mon Sep 17 00:00:00 2001
From: Kasim Te <91560+kasimte@users.noreply.github.com>
Date: Thu, 8 Oct 2026 08:39:27 -0400
Subject: [PATCH 10/10] Challenge 20: Kani safety proofs for char-class
 Searchers in str::pattern

---
 library/core/src/str/pattern.rs | 170 ++++++++++++++------------------
 1 file changed, 76 insertions(+), 94 deletions(-)

diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index 1bec155fb9dae..5ec7214ec10f3 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -2151,28 +2151,37 @@ pub mod verify {
         }
     }
 
-    /// A `&str` of symbolic length in `[0, 5]` with nondeterministic (not
-    /// necessarily valid-UTF-8) backing bytes, stack-allocated. The creation
-    /// harnesses read only positions `0` and `len()` — both unconditionally
-    /// char boundaries per `is_char_boundary`'s fast paths, independent of
-    /// content; the arbitrary-state constructors below additionally assume
-    /// ASCII content before any decode (see their notes).
-    fn symbolic_str(buf: &mut [u8; 5]) -> &str {
-        *buf = kani::any();
-        let n: usize = kani::any();
-        kani::assume(n <= 5);
-        // SAFETY: content is nondeterministic and not assumed valid UTF-8;
-        // sound because callers either read no content (creation harnesses)
-        // or assume ASCII before any decode (the constructors below).
-        unsafe { core::str::from_utf8_unchecked(&buf[..n]) }
+    /// A symbolic valid-UTF-8 `&str` of length in `[0, 5]` bytes, built
+    /// constructively from symbolic `char`s via `encode_utf8`, so every width
+    /// class (1-4 bytes) is reachable. The haystack is the only `&str` these
+    /// harnesses decode; a real `&str` is always valid UTF-8, so this is the
+    /// faithful input domain. `buf` carries slack past the 5-byte cap so the
+    /// final `encode_utf8` always has room.
+    fn symbolic_utf8_str(buf: &mut [u8; 8]) -> &str {
+        let mut len = 0usize;
+        for _ in 0..5 {
+            if kani::any() {
+                break; // symbolic early stop -> variable length
+            }
+            let c: char = kani::any();
+            let w = c.len_utf8();
+            if len + w > 5 {
+                break; // keep the str <= 5 bytes
+            }
+            c.encode_utf8(&mut buf[len..]);
+            len += w;
+        }
+        // SAFETY: bytes were written only by `encode_utf8` of real `char`s, so
+        // `buf[..len]` is valid UTF-8 by construction.
+        unsafe { core::str::from_utf8_unchecked(&buf[..len]) }
     }
 
     // Criterion 1: constructing a `CharSearcher` via the real `char` Pattern
     // path establishes the invariant.
     #[kani::proof]
     fn check_cs_invariant_at_creation() {
-        let mut buf = [0u8; 5];
-        let haystack = symbolic_str(&mut buf);
+        let mut buf = [0u8; 8];
+        let haystack = symbolic_utf8_str(&mut buf);
         let needle: char = kani::any();
         let s = needle.into_searcher(haystack);
         kani::cover(true, "ch20 cs creation reachable");
@@ -2184,8 +2193,8 @@ pub mod verify {
     // invariant.
     #[kani::proof]
     fn check_mces_invariant_at_creation() {
-        let mut buf = [0u8; 5];
-        let haystack = symbolic_str(&mut buf);
+        let mut buf = [0u8; 8];
+        let haystack = symbolic_utf8_str(&mut buf);
         let wrapper = ['a', 'b'].into_searcher(haystack);
         kani::cover(true, "ch20 mces creation reachable");
         kani::assert(wrapper.0.is_safe(), "MultiCharEqSearcher: C established at creation");
@@ -2197,25 +2206,14 @@ pub mod verify {
     // method harnesses use `unwind(7)` = 5 content bytes plus loop
     // entry/exit slack.
 
-    /// Independently-written naive first-occurrence byte scan: a
-    /// `#[kani::stub]` replacement for `memchr::memchr` inside
-    /// `CharSearcher::next_match`. Licensed by Challenge-20 assumption 1
-    /// (the `slice` module is functionally correct) — re-verifying
-    /// memchr's SIMD/word-at-a-time internals is out of this challenge's
-    /// scope.
-    fn stub_memchr(x: u8, text: &[u8]) -> Option<usize> {
-        let mut i = 0;
-        while i < text.len() {
-            if text[i] == x {
-                return Some(i);
-            }
-            i += 1;
-        }
-        None
-    }
-
-    /// Independently-written naive last-occurrence byte scan; see
-    /// `stub_memchr`. Stubs `memchr::memrchr` for `next_match_back`.
+    /// Independently-written naive last-occurrence byte scan: a
+    /// `#[kani::stub]` replacement for `memchr::memrchr` inside
+    /// `CharSearcher::next_match_back`, licensed by Challenge-20 assumption 1
+    /// (the `slice` module is functionally correct). `memchr` needs no stub —
+    /// its `cfg(kani)` path is already a naive loop, so `next_match` runs the
+    /// real body — but `memrchr`'s only body is the word-at-a-time
+    /// `memrchr_aligned`, whose raw word reads overflow CBMC's object budget
+    /// at this bound; this scan stands in for it.
     fn stub_memrchr(x: u8, text: &[u8]) -> Option<usize> {
         let mut i = text.len();
         while i > 0 {
@@ -2227,42 +2225,31 @@ pub mod verify {
         None
     }
 
-    /// Always-panics stand-in for `memchr::memchr`, used only by the
+    /// Always-panics stand-in for `memchr::memrchr`, used only by the
     /// falsifier below (D10 stub-soundness protocol): if `#[kani::stub]`
-    /// were silently failing to substitute at `next_match`'s call site,
+    /// were silently failing to substitute at `next_match_back`'s call site,
     /// nothing would panic and the `#[kani::should_panic]` harness would
     /// FAIL instead of PASS — so a PASS here proves the stub genuinely
-    /// reaches that call site, i.e. `stub_memchr` above masks nothing.
-    fn panicking_memchr_stub(_x: u8, _text: &[u8]) -> Option<usize> {
-        panic!("ch20 stub falsifier: memchr call site reached");
+    /// reaches that call site, i.e. `stub_memrchr` above masks nothing.
+    fn panicking_memrchr_stub(_x: u8, _text: &[u8]) -> Option<usize> {
+        panic!("ch20 stub falsifier: memrchr call site reached");
     }
 
     #[kani::proof]
     #[kani::should_panic]
     #[kani::unwind(7)]
-    #[kani::stub(crate::slice::memchr::memchr, panicking_memchr_stub)]
-    fn check_memchr_stub_falsifier() {
-        let mut buf = [0u8; 5];
+    #[kani::stub(crate::slice::memchr::memrchr, panicking_memrchr_stub)]
+    fn check_memrchr_stub_falsifier() {
+        let mut buf = [0u8; 8];
         let mut s = kani_any_char_searcher(&mut buf);
-        let _ = s.next_match();
+        let _ = s.next_match_back();
     }
 
     /// Arbitrary-`C`-state builder for a bounded (<= 5-byte) `CharSearcher`:
-    /// independently symbolic `finger`/`finger_back`/`needle` over a
-    /// `symbolic_str` haystack, filtered to invariant-satisfying states.
-    /// Also assumes the haystack is ASCII (Challenge-20 assumption 3: "any
-    /// UTF-8 property of haystack is assumable" — ASCII is one such
-    /// property), because the target methods below decode it via
-    /// `.chars()`, unlike the creation harnesses, which never read
-    /// past a boundary. A `from_utf8(..).is_ok()` assume was tried first but
-    /// is NOT a sound filter here: `run_utf8_validation`'s loop-contract
-    /// abstraction (`-Z loop-contracts`) under-constrains what `Ok` implies
-    /// for a caller, so CBMC found genuinely-invalid byte sequences (e.g. an
-    /// orphan continuation byte) satisfying it. A direct ASCII check doesn't
-    /// depend on that abstraction and is trivially sound.
-    fn kani_any_char_searcher<'a>(buf: &'a mut [u8; 5]) -> CharSearcher<'a> {
-        let haystack = symbolic_str(buf);
-        kani::assume(haystack.as_bytes().iter().all(|&b| b < 0x80));
+    /// independently symbolic `finger`/`finger_back`/`needle` over a symbolic
+    /// valid-UTF-8 haystack, filtered to invariant-satisfying states.
+    fn kani_any_char_searcher<'a>(buf: &'a mut [u8; 8]) -> CharSearcher<'a> {
+        let haystack = symbolic_utf8_str(buf);
         let needle: char = kani::any();
         let mut utf8_encoded = [0u8; 4];
         let utf8_size = needle.encode_utf8(&mut utf8_encoded).len() as u8;
@@ -2274,14 +2261,12 @@ pub mod verify {
     }
 
     /// Arbitrary-`C`-state builder for a bounded `MultiCharEqSearcher<[char;
-    /// 2]>`: a symbolic `char_indices` cursor offset over a `symbolic_str`
-    /// haystack (also assumed ASCII, same license + soundness note as
-    /// `kani_any_char_searcher` above).
+    /// 2]>`: a symbolic `char_indices` cursor offset over a symbolic
+    /// valid-UTF-8 haystack, filtered to invariant-satisfying states.
     fn kani_any_multi_char_eq_searcher<'a>(
-        buf: &'a mut [u8; 5],
+        buf: &'a mut [u8; 8],
     ) -> MultiCharEqSearcher<'a, [char; 2]> {
-        let haystack = symbolic_str(buf);
-        kani::assume(haystack.as_bytes().iter().all(|&b| b < 0x80));
+        let haystack = symbolic_utf8_str(buf);
         let char_eq: [char; 2] = [kani::any(), kani::any()];
         let offset: usize = kani::any();
         let suffix = haystack.get(offset..);
@@ -2321,7 +2306,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_cs_next() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_char_searcher(&mut buf);
         let haystack = s.haystack();
         let step = s.next();
@@ -2336,9 +2321,8 @@ pub mod verify {
 
     #[kani::proof]
     #[kani::unwind(7)]
-    #[kani::stub(crate::slice::memchr::memchr, stub_memchr)]
     fn check_cs_next_match() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_char_searcher(&mut buf);
         let haystack = s.haystack();
         let m = s.next_match();
@@ -2353,7 +2337,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_cs_next_back() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_char_searcher(&mut buf);
         let haystack = s.haystack();
         let step = s.next_back();
@@ -2370,7 +2354,7 @@ pub mod verify {
     #[kani::unwind(7)]
     #[kani::stub(crate::slice::memchr::memrchr, stub_memrchr)]
     fn check_cs_next_match_back() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_char_searcher(&mut buf);
         let haystack = s.haystack();
         let m = s.next_match_back();
@@ -2385,7 +2369,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_cs_next_reject() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_char_searcher(&mut buf);
         let haystack = s.haystack();
         let r = s.next_reject();
@@ -2400,7 +2384,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_cs_next_reject_back() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_char_searcher(&mut buf);
         let haystack = s.haystack();
         let r = s.next_reject_back();
@@ -2415,7 +2399,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_mces_next() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_multi_char_eq_searcher(&mut buf);
         let haystack = s.haystack();
         let step = s.next();
@@ -2431,7 +2415,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_mces_next_back() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_multi_char_eq_searcher(&mut buf);
         let haystack = s.haystack();
         let step = s.next_back();
@@ -2447,7 +2431,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_mces_next_match() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_multi_char_eq_searcher(&mut buf);
         let haystack = s.haystack();
         let m = s.next_match();
@@ -2462,7 +2446,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_mces_next_match_back() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_multi_char_eq_searcher(&mut buf);
         let haystack = s.haystack();
         let m = s.next_match_back();
@@ -2477,7 +2461,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_mces_next_reject() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_multi_char_eq_searcher(&mut buf);
         let haystack = s.haystack();
         let r = s.next_reject();
@@ -2492,7 +2476,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_mces_next_reject_back() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut s = kani_any_multi_char_eq_searcher(&mut buf);
         let haystack = s.haystack();
         let r = s.next_reject_back();
@@ -2518,15 +2502,13 @@ pub mod verify {
 
     /// Arbitrary-state `MultiCharEqSearcher<'a, C>` for a caller-supplied
     /// `char_eq`, so each wrapper's witness type can be seeded: symbolic
-    /// `char_indices` cursor over a `symbolic_str` haystack, filtered to
-    /// invariant-satisfying states (same ASCII license + soundness note as
-    /// `kani_any_multi_char_eq_searcher`).
+    /// `char_indices` cursor over a symbolic valid-UTF-8 haystack, filtered to
+    /// invariant-satisfying states.
     fn kani_any_mces_generic<'a, C: MultiCharEq>(
-        buf: &'a mut [u8; 5],
+        buf: &'a mut [u8; 8],
         char_eq: C,
     ) -> MultiCharEqSearcher<'a, C> {
-        let haystack = symbolic_str(buf);
-        kani::assume(haystack.as_bytes().iter().all(|&b| b < 0x80));
+        let haystack = symbolic_utf8_str(buf);
         let offset: usize = kani::any();
         let suffix = haystack.get(offset..);
         kani::assume(suffix.is_some());
@@ -2539,7 +2521,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_chararray_delegation() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut w = CharArraySearcher(kani_any_mces_generic(&mut buf, [kani::any(), kani::any()]));
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
@@ -2550,7 +2532,7 @@ pub mod verify {
     #[kani::proof]
     #[kani::unwind(7)]
     fn check_chararray_delegation_back() {
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut w = CharArraySearcher(kani_any_mces_generic(&mut buf, [kani::any(), kani::any()]));
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
@@ -2562,7 +2544,7 @@ pub mod verify {
     #[kani::unwind(7)]
     fn check_chararrayref_delegation() {
         let arr: [char; 2] = [kani::any(), kani::any()];
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut w = CharArrayRefSearcher(kani_any_mces_generic(&mut buf, &arr));
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
@@ -2574,7 +2556,7 @@ pub mod verify {
     #[kani::unwind(7)]
     fn check_chararrayref_delegation_back() {
         let arr: [char; 2] = [kani::any(), kani::any()];
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut w = CharArrayRefSearcher(kani_any_mces_generic(&mut buf, &arr));
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
@@ -2586,7 +2568,7 @@ pub mod verify {
     #[kani::unwind(7)]
     fn check_charslice_delegation() {
         let arr: [char; 2] = [kani::any(), kani::any()];
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut w = CharSliceSearcher(kani_any_mces_generic(&mut buf, &arr[..]));
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next());
@@ -2598,7 +2580,7 @@ pub mod verify {
     #[kani::unwind(7)]
     fn check_charslice_delegation_back() {
         let arr: [char; 2] = [kani::any(), kani::any()];
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut w = CharSliceSearcher(kani_any_mces_generic(&mut buf, &arr[..]));
         let haystack = w.haystack();
         assert_step_on_boundaries(haystack, w.next_back());
@@ -2610,7 +2592,7 @@ pub mod verify {
     #[kani::unwind(7)]
     fn check_charpredicate_delegation() {
         let target: char = kani::any();
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut w =
             CharPredicateSearcher(kani_any_mces_generic(&mut buf, move |c: char| c == target));
         let haystack = w.haystack();
@@ -2623,7 +2605,7 @@ pub mod verify {
     #[kani::unwind(7)]
     fn check_charpredicate_delegation_back() {
         let target: char = kani::any();
-        let mut buf = [0u8; 5];
+        let mut buf = [0u8; 8];
         let mut w =
             CharPredicateSearcher(kani_any_mces_generic(&mut buf, move |c: char| c == target));
         let haystack = w.haystack();