From 7a934e8481dffeb981a3c579b34b94d1a1958a9e Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Thu, 1 Oct 2026 12:58:36 -0400 Subject: [PATCH 1/2] Challenge 22: Kani harnesses for str iter functions --- library/alloc/src/lib.rs | 1 + library/alloc/src/str.rs | 673 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 674 insertions(+) diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index a80b1ee0daa6e..f7ce47b1d2ef1 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -90,6 +90,7 @@ // Library features: // tidy-alphabetical-start #![cfg_attr(kani, feature(kani))] +#![cfg_attr(kani, feature(str_split_remainder, str_split_whitespace_remainder))] #![cfg_attr(not(no_global_oom_handling), feature(string_replace_in_place))] #![feature(allocator_ext)] #![feature(array_into_iter_constructors)] diff --git a/library/alloc/src/str.rs b/library/alloc/src/str.rs index cd1c149c3c4fc..f3285df1e22dd 100644 --- a/library/alloc/src/str.rs +++ b/library/alloc/src/str.rs @@ -1029,3 +1029,676 @@ unsafe fn replace_ascii(utf8_bytes: &[u8], from: u8, to: u8) -> String { // SAFETY: We replaced ascii with ascii on valid utf8 strings. unsafe { String::from_utf8_unchecked(result) } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use core::kani; + use core::str::pattern::{CharSearcher, Searcher}; + use core::sync::atomic::{AtomicUsize, Ordering}; + + use crate::alloc::{Layout, alloc, alloc_zeroed}; + + // Challenge 22: safety of str iterator methods, proven at SYMBOLIC str length. + // + // Placement: the harnesses live in alloc because they build arbitrary-length str + // backing through the allocator. The allocator is harness infrastructure only — the + // functions under proof are core's str iterators, and backing provenance is + // immaterial to them. + // + // Convention: every `kani::assume` carries a one-line citation of the challenge + // assumption or measured bound it encodes, and each assume-bearing harness pairs + // with `kani::cover` witnesses showing the constrained space is nonempty. + // + // Documented input-family limits (measurements, stated in the submission): + // - Count window: `check_advance_by_chars` bounds the COUNT argument (n <= K; the + // (K, wall-clock) tuning trail sits at the assume site). Str length stays symbolic. + // Local wall exceeds the 120s line at every measured K — runtime budget is + // CANARY-ARBITRATED (settled by the CI canary run, not the local measurement). + // - Content family: the decode harnesses use the all-zero valid-UTF-8 family at + // symbolic length; bounded full-content companions reach the remaining decode arms. + // - Encoding cap: symbolic lengths cap at 2^40, the pointer-encoding budget under + // `--object-bits 12`; the cap moves with that flag and is not a property bound. + // - P = char: searcher stubs instantiate the pattern at `char`; the stub envelope + // encodes only assumption 2's correctness grant, which is pattern-generic. + + /// Symbolic length in [1, 2^40], valid backing, NONDET content. Use only for + /// content-INDEPENDENT properties. The nondeterministic content over-approximates the + /// challenge's valid-UTF-8 family (assumption 4): the resulting `&str` may violate the + /// UTF-8 library invariant, but that invariant is a library, not a language, validity + /// property (unlike `char`/`bool`), so constructing it is not UB, and proving the + /// memory safety of a content-independent method over this superset is strictly + /// stronger than proving it over the valid subset. + fn symbolic_str() -> &'static str { + let n: usize = kani::any(); + // Nonempty family; 2^40 = offset-bits budget under --object-bits 12 (measured cap). + kani::assume(n > 0 && n <= 1usize << 40); + // SAFETY: align 1 nonzero power of two; n <= 2^40 < isize::MAX. + let layout = unsafe { Layout::from_size_align_unchecked(n, 1) }; + let ptr = unsafe { alloc(layout) }; + // Harness infrastructure: model a successful allocation (OOM out of scope). + kani::assume(!ptr.is_null()); + kani::cover(true, "ch22 symbolic str live"); + // SAFETY: fresh n-byte allocation. Content is nondeterministic — callers must not + // rely on UTF-8 validity of the contents. + unsafe { core::str::from_utf8_unchecked(core::slice::from_raw_parts(ptr, n)) } + } + + /// Symbolic length, VALID content: all-zero bytes are valid (ASCII) UTF-8, so this is + /// a legitimate `&str` of arbitrary length with concrete content — for exercising + /// content-DEPENDENT paths (e.g. `advance_by`'s decode loops) without harness-side UB. + fn symbolic_str_zeroed() -> &'static str { + let n: usize = kani::any(); + // Assumption 4 family (all-zero content = valid UTF-8); same measured offset-bits cap. + kani::assume(n > 0 && n <= 1usize << 40); + // SAFETY: align 1 nonzero power of two; n <= 2^40 < isize::MAX. + let layout = unsafe { Layout::from_size_align_unchecked(n, 1) }; + let ptr = unsafe { alloc_zeroed(layout) }; + // Harness infrastructure: model a successful allocation (OOM out of scope). + kani::assume(!ptr.is_null()); + kani::cover(true, "ch22 zeroed str live"); + // SAFETY: fresh zeroed n-byte allocation; all-zero bytes are valid UTF-8. + unsafe { core::str::from_utf8_unchecked(core::slice::from_raw_parts(ptr, n)) } + } + + // Ghost state encoding the Searcher contract's forward progress: successive matches + // never regress. Reset by each harness before its first searcher call. `AtomicUsize` + // rather than `static mut` because edition 2024 forbids references to mutable statics; + // `Relaxed` is exact under Kani's single-threaded model. + static FWD_LAST_END: AtomicUsize = AtomicUsize::new(0); + + fn reset_search_ghosts() { + FWD_LAST_END.store(0, Ordering::Relaxed); + BACK_LAST_START.store(usize::MAX, Ordering::Relaxed); + } + + // Assumption 2 (Ch22 spec): pattern.rs is safe AND functionally correct. Functional + // correctness of Searcher::next_match guarantees an in-bounds, char-boundary range + // that makes forward progress. This stub over-approximates the real searcher: it + // returns ANY range satisfying that grant, without modelling which pattern matched. + // Over-approximation is the sound direction for a safety proof — the caller's + // unchecked slicing must be safe for every range the searcher could return. + fn stub_char_next_match<'a>(s: &mut CharSearcher<'a>) -> Option<(usize, usize)> + where + 'a: 'a, // early-bound: stub generic-param count must match the impl method + { + let hay = s.haystack(); + if kani::any() { + None + } else { + let a: usize = kani::any(); + let b: usize = kani::any(); + kani::assume(a <= b && b <= hay.len()); // assumption 2: match range is in-bounds + // assumption 2: successive matches never regress (forward progress) + kani::assume(a >= FWD_LAST_END.load(Ordering::Relaxed)); + // assumption 2: match endpoints lie on char boundaries + kani::assume(hay.is_char_boundary(a) && hay.is_char_boundary(b)); + FWD_LAST_END.store(b, Ordering::Relaxed); + kani::cover(true, "forward stub yields a range"); + Some((a, b)) + } + } + + static BACK_LAST_START: AtomicUsize = AtomicUsize::new(usize::MAX); + + // Reverse analogue: matches move monotonically backward from the tail. + fn stub_char_next_match_back<'a>(s: &mut CharSearcher<'a>) -> Option<(usize, usize)> + where + 'a: 'a, + { + let hay = s.haystack(); + if kani::any() { + None + } else { + let a: usize = kani::any(); + let b: usize = kani::any(); + kani::assume(a <= b && b <= hay.len()); // assumption 2: match range is in-bounds + // assumption 2: successive reverse matches never advance (reverse progress) + kani::assume(b <= BACK_LAST_START.load(Ordering::Relaxed)); + // assumption 2: match endpoints lie on char boundaries + kani::assume(hay.is_char_boundary(a) && hay.is_char_boundary(b)); + BACK_LAST_START.store(a, Ordering::Relaxed); + kani::cover(true, "reverse stub yields a range"); + Some((a, b)) + } + } + + // Chars::next / next_back decode content; the zeroed family is a VALID UTF-8 input + // family of symbolic length (assumption 4 scope note in the body's content-family row). + #[kani::proof] + fn check_next_chars() { + let s = symbolic_str_zeroed(); + let mut it = s.chars(); + let c = it.next(); + kani::cover(c.is_some(), "next yields a char"); + } + + #[kani::proof] + fn check_next_back_chars() { + let s = symbolic_str_zeroed(); + let mut it = s.chars(); + let c = it.next_back(); + kani::cover(c.is_some(), "next_back yields a char"); + } + + #[kani::proof] + fn check_as_str_chars() { + let s = symbolic_str(); // content-independent: as_str is a slice re-view + let mut it = s.chars(); + let _v = it.as_str(); + kani::cover(true, "as_str returned"); + } + + // Chars::advance_by at symbolic str length with a justified COUNT window (the str + // length stays symbolic; only the count argument is bounded). + // Window arithmetic: under the zeroed family every byte is a char start, so the + // 32-byte chunk loop retires 32 chars per iteration; n <= K bounds it to at most + // K/32 iterations, inside #[kani::unwind(34)] — the unwinding assertion itself + // DISCHARGES, making the window proof complete rather than truncated. + #[kani::proof] + #[kani::unwind(34)] + fn check_advance_by_chars() { + let s = symbolic_str_zeroed(); + let mut chars = s.chars(); + let n: usize = kani::any(); + // Count window K = 256 (measured bound, not a property bound). Local wall trail + // at kani 0.67.0 / CBMC 6.8.0, arm64: partial flag set — K=1024 -> 270.7-282.0s, + // K=512 -> 450.9s, K=256 -> 238.9s; full CI flag set (incl. float-lib/c-ffi/ + // quantifiers) — K=1024 -> 374.9s, K=256 -> 237.2s. Solve time is not monotone + // in K. K=256 is chosen because CI-class runners measure ~2x local on loaded + // macOS partitions and the autoharness job enforces a 600s per-harness timeout: + // 237.2s local projects inside that envelope; 374.9s does not with margin. + kani::assume(n <= 256); + let _ = chars.advance_by(n); + kani::cover(n < 32, "slurp-only path live"); + kani::cover(n >= 32, "chunk path live"); + kani::cover(true, "ch22 pa returned"); + } + + /// Bounded companion input: FULL nondet content, valid UTF-8 by construction + /// (assumption 4), length <= 8 — exercises every decode branch the symbolic-length + /// zeroed-family harnesses cannot reach. The family is exactly the valid UTF-8 + /// strings of length 1..=8: any such string is a concatenation of at most 8 encoded + /// nondet chars. Validity comes from `encode_utf8` (straight-line code) rather than + /// `assume(from_utf8(..).is_ok())`: under -Z loop-contracts the annotated loops in + /// `run_utf8_validation` are abstracted by invariants that do not tie the Ok result + /// to byte content, so that assume underconstrains the model (measured: the + /// advance_by companion then fails advance_by's internal unwrap_unchecked). + fn any_valid_str_bounded() -> &'static str { + const MAX: usize = 8; + let layout = unsafe { Layout::from_size_align_unchecked(MAX, 1) }; + let ptr = unsafe { alloc(layout) }; + // Harness infrastructure: model a successful allocation (OOM out of scope). + kani::assume(!ptr.is_null()); + let buf = unsafe { core::slice::from_raw_parts_mut(ptr, MAX) }; + let mut n: usize = 0; + for _ in 0..MAX { + if kani::any() { + let c: char = kani::any(); + let w = c.len_utf8(); + if n + w <= MAX { + c.encode_utf8(&mut buf[n..n + w]); + n += w; + } + } + } + kani::assume(n >= 1); // input-family shape: nonempty, matching the symbolic families' n > 0 + kani::cover(true, "bounded valid str live"); + let s = unsafe { core::slice::from_raw_parts(ptr, n) }; + // SAFETY: buf[..n] is a concatenation of encode_utf8 outputs — valid UTF-8. + unsafe { core::str::from_utf8_unchecked(s) } + } + + #[kani::proof] + #[kani::unwind(10)] + fn check_next_chars_full_content() { + let s = any_valid_str_bounded(); + let mut it = s.chars(); + let c = it.next(); + // Branch-liveness covers: all four char widths reachable (the arms the zeroed + // family cannot exercise). + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 1), "1-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 2), "2-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 3), "3-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 4), "4-byte decode live"); + } + + #[kani::proof] + #[kani::unwind(10)] + fn check_next_back_chars_full_content() { + let s = any_valid_str_bounded(); + let mut it = s.chars(); + let c = it.next_back(); + kani::cover(c.is_some_and(|ch| ch.len_utf8() >= 2), "multi-byte reverse decode live"); + } + + #[kani::proof] + #[kani::unwind(12)] + fn check_advance_by_chars_full_content() { + let s = any_valid_str_bounded(); + let mut chars = s.chars(); + let n: usize = kani::any(); + kani::assume(n <= 8); // bounded companion window; the symbolic-length harness + // carries the K-window justification + let _ = chars.advance_by(n); + kani::cover(true, "bounded advance_by returned"); + } + + // Empty string (n = 0): the zero-length edge the symbolic families structurally + // exclude — their backing allocation requires n >= 1 (`alloc(0)` is not valid). The + // `""` literal reaches it directly, covering the exhausted/first-empty-field arms. + #[kani::proof] + fn check_empty_str_edges() { + let s = ""; + kani::cover(s.chars().next().is_none(), "empty chars exhausted"); + kani::cover(s.chars().next_back().is_none(), "empty chars_back exhausted"); + kani::cover(s.bytes().next().is_none(), "empty bytes exhausted"); + let mut sp = s.split('x'); + kani::cover(sp.next() == Some(""), "empty split yields one empty field"); + } + + // ---- Split family: SplitInternal driven through the public split iterators ---- + // Content-independent (the unsafe slicing depends only on index arithmetic and the + // searcher envelope), so nondet-content `symbolic_str` applies. Searcher calls are + // stubbed per assumption 2; every stubbing harness resets the ghosts first. + // `#[kani::unwind(4)]` on these harnesses bounds the driver's internal empty-match + // skip loop; a single stubbed search resolves per call, so the bound is not reached — + // verified sufficient (no unwinding-assertion failures in any harness). + + // SplitInternal::next at symbolic length: stub Some drives the match arm, stub None + // drives get_end — the first call always yields an element. + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_next_split() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.split('x'); + let a = it.next(); + kani::cover(a.is_some(), "split next yields an element"); + } + + // SplitInternal::next_inclusive via the public split_inclusive. + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_next_inclusive_split() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.split_inclusive('x'); + let a = it.next(); + kani::cover(a.is_some(), "split_inclusive next yields an element"); + } + + // SplitInternal::next_back (its searcher.next_match_back arm) via the public rsplit. + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_match_back_split() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.rsplit('x'); + let a = it.next(); + kani::cover(a.is_some(), "rsplit next yields an element"); + } + + // SplitInternal::next_back_inclusive: allow_trailing_empty=false takes the + // self-recursive first-call path, so up to two stub calls occur — the ghost + // monotonicity (second start bound by the first) keeps the slice ranges ordered. + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_back_inclusive_split() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.split_inclusive('x'); + let a = it.next_back(); + kani::cover(a.is_some(), "split_inclusive next_back yields an element"); + } + + // SplitInternal::get_end: a nondet stub None on call 1 finishes the iterator, so + // call 2 returns None — the drive-to-completion end path at symbolic length. + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_get_end_split() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.split('x'); + let _a = it.next(); + let b = it.next(); + kani::cover(b.is_none(), "end path (get_end) exercised"); + } + + // remainder accessors: the unstable methods are reached directly — alloc's lib.rs + // enables their feature gates under cfg_attr(kani, ...) only (verification-only + // crate features; the runtime build is byte-identical). + + // Split::remainder -> SplitInternal::remainder at symbolic length: a stub Some on + // call 1 leaves the iterator live (remainder present), a stub None finishes it + // via get_end (remainder consumed) — both arms covered. + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_remainder_split() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.split('x'); + let _ = it.next(); + let r = it.remainder(); + kani::cover(r.is_some(), "split remainder present"); + kani::cover(r.is_none(), "split remainder consumed"); + } + + // SplitAsciiWhitespace::remainder, fresh state at symbolic length: zero scans run — + // the accessor's own `from_utf8_unchecked` over the inner SliceSplit state is the + // exercised unsafe op (driving next() first scans linearly in the symbolic length — + // measured wall, see ch22 log — so advanced states are covered by the bounded + // companion below, full nondet content including whitespace). + #[kani::proof] + fn check_remainder_split_ascii_whitespace() { + let s = symbolic_str(); + let it = s.split_ascii_whitespace(); + let r = it.remainder(); + kani::cover(r.is_some(), "saw remainder present (fresh state)"); + } + + #[kani::proof] + #[kani::unwind(12)] + fn check_remainder_split_ascii_whitespace_advanced() { + let s = any_valid_str_bounded(); // len <= 8, content nondet incl. whitespace + let mut it = s.split_ascii_whitespace(); + let _ = it.next(); // bounded scan, fully unwound + let r = it.remainder(); + kani::cover(r.is_some(), "saw remainder present (advanced)"); + kani::cover(r.is_none(), "saw remainder consumed (advanced)"); + } + + // ---- Matches / MatchIndices: searcher-thin wrappers ---- + // The first call maps the stubbed searcher result directly, so both arms are live. + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_next_matches() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.matches('x'); + let m = it.next(); + kani::cover(m.is_some(), "matches yields a match"); + kani::cover(m.is_none(), "matches exhausted"); + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_back_matches() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.rmatches('x'); + let m = it.next(); + kani::cover(m.is_some(), "rmatches yields a match"); + kani::cover(m.is_none(), "rmatches exhausted"); + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_next_match_indices() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.match_indices('x'); + let m = it.next(); + kani::cover(m.is_some(), "match_indices yields a match"); + kani::cover(m.is_none(), "match_indices exhausted"); + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_back_match_indices() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.rmatch_indices('x'); + let m = it.next(); + kani::cover(m.is_some(), "rmatch_indices yields a match"); + kani::cover(m.is_none(), "rmatch_indices exhausted"); + } + + // Proves main's existing contract on the hidden Iterator plumbing method + // (core/src/str/iter.rs, `#[requires(idx < self.0.len())]` on + // `Bytes::__iterator_get_unchecked`) via the qualified-path proof_for_contract form. + #[kani::proof_for_contract( as core::iter::Iterator>::__iterator_get_unchecked)] + fn check_iterator_get_unchecked_contract() { + let s = symbolic_str(); + let mut b = s.bytes(); + let idx: usize = kani::any(); + let _byte = unsafe { b.__iterator_get_unchecked(idx) }; + } + + #[kani::proof_for_contract( as core::iter::Iterator>::__iterator_get_unchecked)] + fn check_iterator_get_unchecked_contract_advanced() { + let s = symbolic_str(); + let mut b = s.bytes(); + // Nondeterministically advance 0..=2 positions before the contract call — cheap + // concrete branches covering non-fresh iterator states. + if kani::any() { + let _ = b.next(); + } + if kani::any() { + let _ = b.next(); + } + let idx: usize = kani::any(); + let _byte = unsafe { b.__iterator_get_unchecked(idx) }; + } + + // ---- S1: advanced-state (non-initial) Split/Matches harnesses ---- + // The base Split/Matches harnesses call the method once from the FRESH iterator. These + // make an UNCONDITIONAL prior call (so the checked call provably never runs from the + // initial state), then an optional second, so the checked call runs from a depth-1-or-2 + // state; two covers on `first` witness that the prior call genuinely varied the state + // (consumed a field via `Some` AND finished via `None`, both reachable). This is + // representative-depth coverage (depth 1..2), not arbitrary depth: `SplitInternal`'s + // fields are private to core, so an arbitrary-state builder would need a core-side change + // that the zero-shipped-edits spine forbids; the isomorphism of the call-k obligation to + // the call-1/2 obligation is argued in the submission. The stub's ghost monotonicity + // threads through the prior calls, so the advanced states stay consistent with the + // searcher contract. One representative per family arm: `matches`/`rmatches`/ + // `match_indices` share this driver shape; `rmatch_indices` is structurally identical to + // `rmatches`. + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_next_split_advanced() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.split('x'); + let first = it.next(); // UNCONDITIONAL: the checked call below is never depth-0 + // Witness the advanced state genuinely varied (W1). Split iterators always yield >= 1 + // field, so the first `next()` never returns None here: the `first.is_none()` witness + // is provably UNSAT and is dropped (a provably-UNSAT cover fails vacuity). The + // `first.is_some()` witness proves the prior call consumed a field, so the checked + // call runs from a genuinely advanced (consumed-field) state. + kani::cover(first.is_some(), "prior call consumed a field (advanced state)"); + if kani::any() { + let _ = it.next(); // optional second → checked call runs from depth 1 or 2 + } + let a = it.next(); // checked from a provably non-initial (depth 1..2) state + kani::cover(a.is_some(), "advanced split next yields an element"); + // NOTE: no `a.is_none()` cover — after a finishing prior call it is trivially SAT and + // adds nothing; the `first` covers already witness the finished branch. + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_next_inclusive_split_advanced() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.split_inclusive('x'); + let first = it.next(); + // Split iterators always yield >= 1 field, so `first.is_none()` is provably UNSAT on + // the first call and is dropped (fails vacuity); `first.is_some()` witnesses the + // consumed-field advanced state. + kani::cover(first.is_some(), "prior call consumed a field (advanced state)"); + if kani::any() { + let _ = it.next(); + } + let a = it.next(); + kani::cover(a.is_some(), "advanced split_inclusive next yields an element"); + } + + // rsplit is a forward iterator that drives SplitInternal::next_back, so perturb and check + // with `it.next()` under the reverse stub. + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_match_back_split_advanced() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.rsplit('x'); + let first = it.next(); + // Split iterators always yield >= 1 field, so `first.is_none()` is provably UNSAT on + // the first call and is dropped (fails vacuity); `first.is_some()` witnesses the + // consumed-field advanced state. + kani::cover(first.is_some(), "prior call consumed a field (advanced state)"); + if kani::any() { + let _ = it.next(); + } + let a = it.next(); + kani::cover(a.is_some(), "advanced rsplit next yields an element"); + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_next_matches_advanced() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.matches('x'); + let first = it.next(); + kani::cover(first.is_some(), "prior call consumed a field (advanced state)"); + kani::cover(first.is_none(), "prior call finished the iterator (advanced state)"); + if kani::any() { + let _ = it.next(); + } + let a = it.next(); + kani::cover(a.is_some(), "advanced matches next yields an element"); + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_back_matches_advanced() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.rmatches('x'); + let first = it.next(); + kani::cover(first.is_some(), "prior call consumed a field (advanced state)"); + kani::cover(first.is_none(), "prior call finished the iterator (advanced state)"); + if kani::any() { + let _ = it.next(); + } + let a = it.next(); + kani::cover(a.is_some(), "advanced rmatches next yields an element"); + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + fn check_next_match_indices_advanced() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.match_indices('x'); + let first = it.next(); + kani::cover(first.is_some(), "prior call consumed a field (advanced state)"); + kani::cover(first.is_none(), "prior call finished the iterator (advanced state)"); + if kani::any() { + let _ = it.next(); + } + let a = it.next(); + kani::cover(a.is_some(), "advanced match_indices next yields an element"); + } + + // ---- S3: hybrid joint length×content decode harnesses (decode fns only) ---- + // `Chars::next` decodes the FRONT char; `next_back` the BACK. A string that is + // full-content-valid over a bounded end char and zeroed to a symbolic total length is + // valid UTF-8 (valid char ++ valid ASCII zeros, joined at a char boundary) AND arbitrary + // length AND exercises every decode width at the touched end — jointly covering S3's + // length×content product for the decode functions. + + /// Valid UTF-8 of SYMBOLIC total length whose FRONT is a full-content char (all four + /// widths reachable) and whose remainder is zeroed (valid ASCII). Front-decoding + /// methods (`Chars::next`) then see arbitrary length AND arbitrary decoded-char content + /// in one input — the joint S3 product for the decode functions. + fn hybrid_front_str() -> &'static str { + let total: usize = kani::any(); + kani::assume(total >= 1 && total <= 1usize << 40); + let layout = unsafe { Layout::from_size_align_unchecked(total, 1) }; + let ptr = unsafe { alloc_zeroed(layout) }; // tail zeroed by construction + kani::assume(!ptr.is_null()); + // Encode ONE nondet char into the front if it fits (else the all-zero string, + // still valid). The prefix ends on a char boundary; zeros are all boundaries. + let c: char = kani::any(); + let w = c.len_utf8(); + // Mild, honest coupling (W2): a width-w front char needs total >= w, so the + // w-byte-decode witness forces length >= w. The claim is "arbitrary length (>= the + // decoded width) x arbitrary valid decoded content", not fully independent axes. + if w <= total { + let front = unsafe { core::slice::from_raw_parts_mut(ptr, w) }; + c.encode_utf8(front); + } + kani::cover(true, "hybrid front str live"); + // SAFETY: front is one encoded char (valid) or zero; tail is zero (valid ASCII); + // the join is at a char boundary → valid UTF-8 of length `total`. + unsafe { core::str::from_utf8_unchecked(core::slice::from_raw_parts(ptr, total)) } + } + + #[kani::proof] + #[kani::unwind(4)] + fn check_next_chars_hybrid() { + let s = hybrid_front_str(); + let mut it = s.chars(); + let c = it.next(); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 1), "hybrid 1-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 2), "hybrid 2-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 3), "hybrid 3-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 4), "hybrid 4-byte decode live"); + } + + /// Mirror of `hybrid_front_str`: zeroed head, full-content SUFFIX char at the tail + /// (encoded into `ptr[total-w..total]` when it fits). Back-decoding methods + /// (`Chars::next_back`) then see arbitrary length AND arbitrary decoded-char content. + fn hybrid_back_str() -> &'static str { + let total: usize = kani::any(); + kani::assume(total >= 1 && total <= 1usize << 40); + let layout = unsafe { Layout::from_size_align_unchecked(total, 1) }; + let ptr = unsafe { alloc_zeroed(layout) }; // head zeroed by construction + kani::assume(!ptr.is_null()); + let c: char = kani::any(); + let w = c.len_utf8(); + // Same honest coupling (W2): a width-w tail char needs total >= w. The suffix begins + // on a char boundary (zeros are all boundaries) → valid UTF-8. + if w <= total { + let back = unsafe { core::slice::from_raw_parts_mut(ptr.add(total - w), w) }; + c.encode_utf8(back); + } + kani::cover(true, "hybrid back str live"); + // SAFETY: head is zero (valid ASCII); tail is one encoded char (valid) or zero; + // the join is at a char boundary → valid UTF-8 of length `total`. + unsafe { core::str::from_utf8_unchecked(core::slice::from_raw_parts(ptr, total)) } + } + + #[kani::proof] + #[kani::unwind(4)] + fn check_next_back_chars_hybrid() { + let s = hybrid_back_str(); + let mut it = s.chars(); + let c = it.next_back(); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 1), "hybrid back 1-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 2), "hybrid back 2-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 3), "hybrid back 3-byte decode live"); + kani::cover(c.is_some_and(|ch| ch.len_utf8() == 4), "hybrid back 4-byte decode live"); + } +} From 295ca194841320d3340b5234611c371a4f1aaae0 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Fri, 2 Oct 2026 21:05:10 -0400 Subject: [PATCH 2/2] Challenge 22: zeroed symbolic backing; mixed-direction advanced harnesses Address Copilot review on #706: - symbolic_str now uses alloc_zeroed (valid UTF-8, no read of uninitialized memory); merge the former symbolic_str_zeroed into it since the content-independent proofs stub the searcher and never depend on nondeterministic content. - Add mixed front/back advanced-state harnesses for the double-ended Split/Matches iterators, exercising the both-cursors-moved state. The searcher stubs gain a two-sided no-cross clause (DoubleEndedSearcher consistency), a no-op for the single-direction harnesses. --- library/alloc/src/str.rs | 111 ++++++++++++++++++++++++++++----------- 1 file changed, 79 insertions(+), 32 deletions(-) diff --git a/library/alloc/src/str.rs b/library/alloc/src/str.rs index f3285df1e22dd..e6af92f489511 100644 --- a/library/alloc/src/str.rs +++ b/library/alloc/src/str.rs @@ -1055,48 +1055,29 @@ mod verify { // (K, wall-clock) tuning trail sits at the assume site). Str length stays symbolic. // Local wall exceeds the 120s line at every measured K — runtime budget is // CANARY-ARBITRATED (settled by the CI canary run, not the local measurement). - // - Content family: the decode harnesses use the all-zero valid-UTF-8 family at - // symbolic length; bounded full-content companions reach the remaining decode arms. + // - Content family: every symbolic-length harness uses the all-zero valid-UTF-8 + // family (assumption 4); bounded full-content companions reach the remaining + // decode arms. // - Encoding cap: symbolic lengths cap at 2^40, the pointer-encoding budget under // `--object-bits 12`; the cap moves with that flag and is not a property bound. // - P = char: searcher stubs instantiate the pattern at `char`; the stub envelope // encodes only assumption 2's correctness grant, which is pattern-generic. - /// Symbolic length in [1, 2^40], valid backing, NONDET content. Use only for - /// content-INDEPENDENT properties. The nondeterministic content over-approximates the - /// challenge's valid-UTF-8 family (assumption 4): the resulting `&str` may violate the - /// UTF-8 library invariant, but that invariant is a library, not a language, validity - /// property (unlike `char`/`bool`), so constructing it is not UB, and proving the - /// memory safety of a content-independent method over this superset is strictly - /// stronger than proving it over the valid subset. + /// Symbolic length in [1, 2^40], zeroed valid backing: all-zero bytes are valid + /// (ASCII) UTF-8, so this is a legitimate `&str` of arbitrary length (assumption 4 + /// family). Used by both the content-independent harnesses (searcher stubbed; + /// content never read) and the content-dependent decode paths (e.g. `advance_by`'s + /// chunk loop). fn symbolic_str() -> &'static str { let n: usize = kani::any(); // Nonempty family; 2^40 = offset-bits budget under --object-bits 12 (measured cap). kani::assume(n > 0 && n <= 1usize << 40); // SAFETY: align 1 nonzero power of two; n <= 2^40 < isize::MAX. let layout = unsafe { Layout::from_size_align_unchecked(n, 1) }; - let ptr = unsafe { alloc(layout) }; - // Harness infrastructure: model a successful allocation (OOM out of scope). - kani::assume(!ptr.is_null()); - kani::cover(true, "ch22 symbolic str live"); - // SAFETY: fresh n-byte allocation. Content is nondeterministic — callers must not - // rely on UTF-8 validity of the contents. - unsafe { core::str::from_utf8_unchecked(core::slice::from_raw_parts(ptr, n)) } - } - - /// Symbolic length, VALID content: all-zero bytes are valid (ASCII) UTF-8, so this is - /// a legitimate `&str` of arbitrary length with concrete content — for exercising - /// content-DEPENDENT paths (e.g. `advance_by`'s decode loops) without harness-side UB. - fn symbolic_str_zeroed() -> &'static str { - let n: usize = kani::any(); - // Assumption 4 family (all-zero content = valid UTF-8); same measured offset-bits cap. - kani::assume(n > 0 && n <= 1usize << 40); - // SAFETY: align 1 nonzero power of two; n <= 2^40 < isize::MAX. - let layout = unsafe { Layout::from_size_align_unchecked(n, 1) }; let ptr = unsafe { alloc_zeroed(layout) }; // Harness infrastructure: model a successful allocation (OOM out of scope). kani::assume(!ptr.is_null()); - kani::cover(true, "ch22 zeroed str live"); + kani::cover(true, "ch22 symbolic str live"); // SAFETY: fresh zeroed n-byte allocation; all-zero bytes are valid UTF-8. unsafe { core::str::from_utf8_unchecked(core::slice::from_raw_parts(ptr, n)) } } @@ -1131,6 +1112,10 @@ mod verify { kani::assume(a <= b && b <= hay.len()); // assumption 2: match range is in-bounds // assumption 2: successive matches never regress (forward progress) kani::assume(a >= FWD_LAST_END.load(Ordering::Relaxed)); + // assumption 2: front/back sequences are consistent (DoubleEndedSearcher) — + // a forward match never enters the region already yielded from the back. + // No-op (MAX) unless a harness also drives next_match_back. + kani::assume(b <= BACK_LAST_START.load(Ordering::Relaxed)); // assumption 2: match endpoints lie on char boundaries kani::assume(hay.is_char_boundary(a) && hay.is_char_boundary(b)); FWD_LAST_END.store(b, Ordering::Relaxed); @@ -1155,6 +1140,10 @@ mod verify { kani::assume(a <= b && b <= hay.len()); // assumption 2: match range is in-bounds // assumption 2: successive reverse matches never advance (reverse progress) kani::assume(b <= BACK_LAST_START.load(Ordering::Relaxed)); + // assumption 2: front/back sequences are consistent (DoubleEndedSearcher) — + // a reverse match never enters the region already yielded from the front. + // No-op (0) unless a harness also drives next_match. + kani::assume(a >= FWD_LAST_END.load(Ordering::Relaxed)); // assumption 2: match endpoints lie on char boundaries kani::assume(hay.is_char_boundary(a) && hay.is_char_boundary(b)); BACK_LAST_START.store(a, Ordering::Relaxed); @@ -1167,7 +1156,7 @@ mod verify { // family of symbolic length (assumption 4 scope note in the body's content-family row). #[kani::proof] fn check_next_chars() { - let s = symbolic_str_zeroed(); + let s = symbolic_str(); let mut it = s.chars(); let c = it.next(); kani::cover(c.is_some(), "next yields a char"); @@ -1175,7 +1164,7 @@ mod verify { #[kani::proof] fn check_next_back_chars() { - let s = symbolic_str_zeroed(); + let s = symbolic_str(); let mut it = s.chars(); let c = it.next_back(); kani::cover(c.is_some(), "next_back yields a char"); @@ -1198,7 +1187,7 @@ mod verify { #[kani::proof] #[kani::unwind(34)] fn check_advance_by_chars() { - let s = symbolic_str_zeroed(); + let s = symbolic_str(); let mut chars = s.chars(); let n: usize = kani::any(); // Count window K = 256 (measured bound, not a property bound). Local wall trail @@ -1299,7 +1288,7 @@ mod verify { // ---- Split family: SplitInternal driven through the public split iterators ---- // Content-independent (the unsafe slicing depends only on index arithmetic and the - // searcher envelope), so nondet-content `symbolic_str` applies. Searcher calls are + // searcher envelope), so the zeroed `symbolic_str` family loses nothing. Searcher calls are // stubbed per assumption 2; every stubbing harness resets the ghosts first. // `#[kani::unwind(4)]` on these harnesses bounds the driver's internal empty-match // skip loop; a single stubbed search resolves per call, so the bound is not reached — @@ -1621,6 +1610,64 @@ mod verify { kani::cover(a.is_some(), "advanced match_indices next yields an element"); } + // ---- S1: mixed-direction (front/back) advanced-state harnesses ---- + // The advanced harnesses above drive one direction. These reach the MIXED state — + // both cursors moved — where `start`, `end`, and both searcher frontiers interact. + // Both stubs are active; their no-cross clauses (assumption 2's DoubleEndedSearcher + // consistency) keep the two frontiers inside the searcher contract, and are no-ops + // for the single-direction harnesses (ghosts stay at their reset values there). + // One representative per family arm, as above. + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_split_mixed() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.split('x'); + let front = it.next(); // front cursor moves (a split's first next always yields) + kani::cover(front.is_some(), "mixed split: front call consumed a field"); + let back = it.next_back(); // back cursor moves: the mixed state + kani::cover(back.is_some(), "mixed split: back call consumed a field"); + let a = it.next(); // checked call from the both-cursors-moved state + kani::cover(a.is_some(), "mixed split next yields an element"); + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_matches_mixed() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.matches('x'); + let front = it.next(); + kani::cover(front.is_some(), "mixed matches: front call consumed a match"); + kani::cover(front.is_none(), "mixed matches: front call finished the iterator"); + let back = it.next_back(); + kani::cover(back.is_some(), "mixed matches: back call consumed a match"); + let a = it.next(); + kani::cover(a.is_some(), "mixed matches next yields an element"); + } + + #[kani::proof] + #[kani::unwind(4)] + #[kani::stub( as Searcher<'_>>::next_match, stub_char_next_match)] + #[kani::stub( as core::str::pattern::ReverseSearcher<'_>>::next_match_back, stub_char_next_match_back)] + fn check_next_match_indices_mixed() { + reset_search_ghosts(); + let s = symbolic_str(); + let mut it = s.match_indices('x'); + let front = it.next(); + kani::cover(front.is_some(), "mixed match_indices: front call consumed a match"); + kani::cover(front.is_none(), "mixed match_indices: front call finished the iterator"); + let back = it.next_back(); + kani::cover(back.is_some(), "mixed match_indices: back call consumed a match"); + let a = it.next(); + kani::cover(a.is_some(), "mixed match_indices next yields an element"); + } + // ---- S3: hybrid joint length×content decode harnesses (decode fns only) ---- // `Chars::next` decodes the FRONT char; `next_back` the BACK. A string that is // full-content-valid over a bounded end char and zeroed to a symbolic total length is