Challenge 10: Verify memory safety of String functions with Kani

[Talha-Dmr]

Partially addresses #61 (Challenge 10): all 15 functions have harnesses over the real bodies; of the 9 "(U)" functions, 2 are verified for arbitrary lengths, 2 for arbitrary receiver length with a bounded edit/match count, and 5 are bounded because of the Kani limitations documented below.

Summary

This PR adds Kani harnesses in library/alloc/src/string.rs (#[cfg(kani)] mod verify) for all 15 functions listed in Challenge 10. Every harness runs over the real function bodies. The PR changes no production lines, has no cfg(kani) body swaps, no kani::assume, and replaces no function under test. It has one stub: in the retain harness, core::str::from_utf8 (called by retain inside a debug_assert!) is replaced by a stand-in that checks the exact expected bytes (see "Bounded harnesses").

Updated for current main (merged at 8d4cbf8: nightly-2026-09-25, Kani 1640445, CBMC 6.11.0). Since the previous version, main has the PanicGuard version of retain and the new from_utf16_units loop of from_utf16le/from_utf16be; the harnesses and the explanations below follow that code.

• Fully unbounded: insert_str and split_off. The strings have symbolic length and capacity, limited only by the largest object CBMC can represent under --object-bits 12.
• Unbounded receiver, bounded edit: replace_range and remove_matches. The receiver has arbitrary length. Only the number of edited bytes or matches is bounded, because those are the only loop trip counts.
• Bounded, with the tool limitation documented: retain (at most 5 chars, exact result checked) and the four from_utf16* functions (at most 12 input bytes for the little-endian and 16 for the big-endian variants, exact result length and Ok/Err checked).
• Non-(U) functions: pop, remove, insert, drain, into_boxed_str and leak, verified for arbitrary lengths (their harnesses are loop-free).
• Panic harnesses: 23 #[kani::should_panic] harnesses cover the inputs that the other harnesses stay out of, one failing check per harness. With the main harnesses, every index of insert, insert_str, split_off and remove, and every range a..b of drain and replace_range, is in the domain of some harness (tables below).
• Range checks: 3 ordinary harnesses check that slice::try_range rejects ..=usize::MAX, (Excluded(usize::MAX), Unbounded) and every reversed range a..b with b <= len, for every length up to MAX_ALLOC. try_range returns None exactly when slice::range, which drain and replace_range use, panics. An arithmetic overflow fails these harnesses, so they show that those panics come from the range check itself.

Status per function

Function	(U) required	Status	Harnesses
insert_str	yes	unbounded	check_insert_str, check_insert_str_panics_inside_char, check_insert_str_panics_past_end
split_off	yes	unbounded	check_split_off, check_split_off_panics_inside_char, check_split_off_panics_past_end
replace_range	yes	receiver unbounded, removed and inserted bytes <= 4 each	check_replace_range, check_replace_range_panics_start_inside_char, check_replace_range_panics_end_inside_char, check_replace_range_panics_both_inside_char, check_replace_range_panics_past_end, check_replace_range_panics_reversed, check_replace_range_panics_end_included_max, check_replace_range_panics_start_excluded_max
remove_matches	yes	receiver unbounded, <= 5 matches	check_remove_matches
retain	yes	bounded, <= 5 chars (tool limit, see below)	check_retain_bounded
from_utf16le	yes	bounded, input <= 12 bytes (tool limit)	check_from_utf16le_bounded
from_utf16le_lossy	yes	bounded, input <= 12 bytes (tool limit)	check_from_utf16le_lossy_bounded
from_utf16be	yes	bounded, input <= 16 bytes (tool limit)	check_from_utf16be_bounded
from_utf16be_lossy	yes	bounded, input <= 16 bytes (tool limit)	check_from_utf16be_lossy_bounded
pop	no	arbitrary length	check_pop
remove	no	arbitrary length	check_remove, check_remove_panics_inside_char, check_remove_panics_at_end, check_remove_panics_past_end
insert	no	arbitrary length	check_insert, check_insert_panics_inside_char, check_insert_panics_past_end
drain	no	arbitrary length (one next, and drop)	check_drain_next, check_drain_drop, check_drain_panics_start_inside_char, check_drain_panics_end_inside_char, check_drain_panics_both_inside_char, check_drain_panics_past_end, check_drain_panics_reversed, check_drain_panics_end_included_max, check_drain_panics_start_excluded_max
into_boxed_str	no	arbitrary length	check_into_boxed_str
leak	no	arbitrary length	check_leak

The three check_range_rejects_* harnesses check slice::try_range, which runs the same range check as the slice::range that drain and replace_range call (see the range table below).

Input classes of the index-taking functions

Each class is the domain of one harness, and the classes of a function together contain all of its inputs. All receivers have symbolic length (and capacity) up to MAX_ALLOC; where a class needs a multi-byte char, with_char_at() places an arbitrary char at an arbitrary offset (the only indices of that string that are not char boundaries are inside this char).

Index idx	insert	insert_str	split_off	remove
char boundary, idx < len	check_insert	check_insert_str	check_split_off	check_remove
idx == len	check_insert	check_insert_str	check_split_off	check_remove_panics_at_end
strictly inside a multi-byte char	check_insert_panics_inside_char	check_insert_str_panics_inside_char	check_split_off_panics_inside_char	check_remove_panics_inside_char
idx > len	check_insert_panics_past_end	check_insert_str_panics_past_end	check_split_off_panics_past_end	check_remove_panics_past_end

drain and replace_range check a range a..b in this order: b <= len and a <= b (in slice::range), then that a, and then b, is a char boundary.

Range	drain	replace_range	slice::try_range
a <= b <= len, both char boundaries, every RangeBounds shape	check_drain_next, check_drain_drop	check_replace_range
b > len, any a	check_drain_panics_past_end	check_replace_range_panics_past_end
b <= len, a > b	check_drain_panics_reversed	check_replace_range_panics_reversed	check_range_rejects_reversed
a inside a char, b a char boundary	check_drain_panics_start_inside_char	check_replace_range_panics_start_inside_char
a a char boundary, b inside a char	check_drain_panics_end_inside_char	check_replace_range_panics_end_inside_char
a <= b, both inside the same char	check_drain_panics_both_inside_char	check_replace_range_panics_both_inside_char
..=usize::MAX	check_drain_panics_end_included_max	check_replace_range_panics_end_included_max	check_range_rejects_end_included_max
(Excluded(usize::MAX), Unbounded)	check_drain_panics_start_excluded_max	check_replace_range_panics_start_excluded_max	check_range_rejects_start_excluded_max

The panic harnesses give the range as a..b (or the shape named in the table). The main harnesses give the valid ranges in every RangeBounds shape (any_bounds). Invalid ranges in the other shapes (for example a..=b with b >= len) have no harness of their own: slice::range checks the bounds as given and panics through the same slice_index_fail, before drain or replace_range reaches any unsafe code.

The harnesses in the last column are ordinary harnesses, not should_panic ones: slice::try_range returns None exactly when slice::range panics, and an overflow fails them. So they show that the range check itself rejects these three classes (see the mutation checks below).

Approach

Symbolic strings. any_string() builds a String with symbolic capacity cap <= MAX_ALLOC and symbolic length len <= cap from a zeroed buffer (vec![0u8; cap], then truncate(len)), so every byte is initialized and the string is valid UTF-8 (any_string_max_len(m) additionally limits the length to m). No loop runs, so there is no unwinding bound. MAX_ALLOC = 2^51 - 1 is the largest single object under --object-bits 12, the setting scripts/run-kani.sh uses. It is a limit of the memory model, not a bound chosen for tractability; #681 (Challenge 25) limits its symbolic capacity by the CBMC object model in the same way.

Contents. Memory safety of these functions depends only on the lengths, the capacity, the given indices, the char-boundary checks at those indices, and at most one decoded char (pop, remove and the Drain iterator decode exactly one). So the harnesses use NUL-filled strings, and where a char is decoded, with_char_at() places a well-formed encoding of an arbitrary char at an arbitrary offset inside the zeroed buffer. On an all-NUL string every index up to the length is a char boundary, so the harnesses reach every combination of these quantities for which the boundary checks pass; the combinations for which they fail are the panics below. All inputs are initialized, valid UTF-8 by construction.

No assumptions beyond input domains. The module has no kani::assume. Every restriction of an input is a kani::any_where domain at the point where the input is generated: sizes that fit in one CBMC object, indices inside the string (which also keeps the main harnesses out of the out-of-range panics), the bounds in the table above, and, in the panic harnesses, the input class of the harness. The documented preconditions (indices on char boundaries) are not assumed: they hold by construction, and the harnesses that pick an index assert! that it is a char boundary before the call.

Panics. Panics are not UB, so the main harnesses stay out of the documented panic conditions by construction, and the 23 #[kani::should_panic] harnesses cover those inputs, with one failing check per harness: a should_panic harness passes as soon as some input panics, so a harness whose inputs could fail two different checks could pass on one of them alone (found in review). Where a range has both ends inside the same char, both checks fail and the start check fires first; that case has its own harness. Kani accepts such a harness only if a panic-class failure is reachable and every failing check is of that class, so no UB is reachable for any input of the harness (Kani uses panic=abort). For each harness, the logs show that the failing check is exactly the documented panic: an is_char_boundary assertion, the out-of-range or reversed-range panic of slice::range (slice_index_fail), the slicing panic of str (for remove), or remove's "cannot remove a char from the end of a string". pop has no panic condition.

check_remove and #[kani::unwind(2)]. self[idx..] has a panic path (str::slice_error_fail_rt) with a loop (ceil_char_boundary). Under this harness that path is infeasible (idx is the start of a well-formed char); the bound only cuts it, and unwinding assertions stay enabled. check_remove_panics_inside_char takes that path, and its #[kani::unwind(4)] covers the at most 3 iterations of that loop (the next char boundary is at most 3 bytes away).

replace_range / remove_matches. Every loop reachable from these functions iterates once per edited byte or per match (for replace_range: the Splice drop, drain, fill and extend loops; for remove_matches: the collection of matches and the compaction loop). No loop iterates once per byte of the receiver: the receiver-sized work is done by ptr::copy / copy_nonoverlapping calls (moving the tail, and the reallocation), which are loop-free. So the receiver has arbitrary length and capacity, and only the edit size or match count is bounded, with a matching #[kani::unwind]; an insufficient bound fails the unwinding assertion.

• The range is given as an arbitrary (Bound, Bound) encoding of a valid range start..end, which covers every RangeBounds shape of it; a cover per Bound variant shows each is reached (the drain harnesses use the same generator).
• For remove_matches, the pattern is a most-general Searcher (AnyPattern): it may return any sequence of up to 5 matches allowed by the Searcher contract ("adjacent, non-overlapping, covering the whole haystack, and laying on utf8 boundaries"; ranges may have zero length). The boundary requirement is asserted inside the searcher, not assumed. With 5 matches the Vec of matches grows past its initial capacity, and a cover shows that reallocation path is reached.

Bounded harnesses.

• check_retain_bounded runs retain on every string of at most 5 arbitrary chars, with every pattern of predicate answers: the answer to the i-th call is an arbitrary bool, fixed before the call. The predicate records the char of each call. After retain returns, the harness checks that the predicate was called once per char, in the order of the chars, and that the string holds exactly the kept chars: first its length, then its bytes. Covers show five paths through retain: its first loop returns (nothing removed); its second loop starts at offset 0 (the first char removed) and after a kept multi-byte char; a kept char is moved left by less than its length (ptr::copy with overlapping ranges); every char is removed.
  • The one stub: retain's PanicGuard::drop runs debug_assert!(str::from_utf8(..).is_ok()). Under CI's -Z loop-contracts, the loops of the real validator (run_utf8_validation) are replaced by their invariants, which do not keep the loop index on a char boundary, so the abstracted validator can return Err for valid UTF-8 with a multi-byte char and the assertion fails although the bytes are valid. The harness replaces from_utf8 by from_utf8_kept, which returns Ok only if the bytes are exactly the encodings of the kept chars (computed by the harness before the call) and panics otherwise. Those bytes are valid UTF-8, so the real validator returns Ok whenever the stand-in does, and on any other input the stand-in fails the harness: it can add failures but not hide one.
• The from_utf16* harnesses run on every sub-slice of an arbitrary byte array, so odd lengths and both odd and even start addresses are covered (for the little-endian variants, the align_to fast path and the unaligned path; on the little-endian CI targets the big-endian variants have only the unaligned path). A reference model of char::decode_utf16 (utf16_expected) gives the validity of the input and the UTF-8 length of the decoded string; the strict variants must return Ok exactly for valid input, and every returned string must have that length (unpaired surrogates and a trailing odd byte count as U+FFFD in the lossy variants).
• Each bounded harness has a matching #[kani::unwind], with a comment on how it follows from the input size, and an insufficient bound fails the unwinding assertion.

How the challenge's list of UB is checked

• Accessing a place that is dangling or based on a misaligned pointer. Checked by Kani's default instrumentation on every harness: each dereference is checked for null, dangling (dead or deallocated object), out-of-bounds and invalid pointers; ptr::copy and ptr::copy_nonoverlapping are checked for aligned, in-bounds source and destination (and non-overlap for the latter); pointer-to-reference casts are checked for alignment. This covers the unsafe code of these functions: the ptr::copys of insert, insert_str, remove, retain and remove_matches, the get_unchecked accesses of retain and drain, the raw String pointer in Drain, and the Vec / RawVec reallocation and Splice code underneath.
• Reading from uninitialized memory. Not checked by the CI configuration: CBMC gives uninitialized heap bytes nondeterministic values and does not report reads of them. Every input is initialized by construction (zeroed buffers, kani::any() arrays, encoded chars).
• Mutating immutable bytes. Kani has no check for this (it does not model immutability or aliasing rules), so this item rests on inspection: in these functions every write goes through a pointer obtained from &mut self (self.vec.as_mut_ptr(), as_mut_vec()), or, in Drain::drop, from the *mut String that drain creates from &mut self; leak and into_boxed_str hand out the owned buffer without writing to it.
• Producing an invalid value. The chars that pop, remove, Drain::next and retain decode are asserted to equal the encoded char, so an invalid char would fail the assertion. Reaching unreachable_unchecked (through the unwrap_unchecked of the decoded char in retain) is reported by Kani's unreachable code check. The CI configuration does not check the validity of other intermediate values.

Why retain and from_utf16* are bounded

An unbounded proof of these functions needs a loop contract on every loop whose trip count grows with the input. At the pinned Kani none of these loops can carry one:

1. retain (two loops: a fast path over char_indices, then a slow path over the unread tail).
   • The slow path reads the tail with get_unchecked(read..len).chars().next().unwrap_unchecked(), so its invariant must say that the unread tail is still valid UTF-8 after the earlier moves: a quantifier over a symbolic range. CI's SAT backend does not support such quantifiers (Kani reports an error instead of dropping them, Fail verification when the solver backend drops quantifiers kani#4719). With the z3 backend (#[kani::solver(z3)], z3 5.1.0 locally) a small model of this loop verifies, but on the verbatim loop (even with ASCII-only input) z3 did not finish within 10 minutes, the per-harness limit of the macOS autoharness job.
   • The fast path's invariant has to describe the CharIndices iterator, whose state is reachable only through method calls, and calls inside loop invariants become nondeterministic (#[kani::loop_invariant] with a method call lowers the call with "not enough arguments", substituting a non-deterministic value kani#4796).
   • Writes to the loop-body temporaries also had to be listed in loop_modifies, which was not possible (Loop contracts: explicit loop_modifies rejects writes to temporaries declared in the loop body (Check that var_N is assignable) kani#4906, fixed by Keep loop attributes on rewritten for loops and add loop-only locals to loop_modifies kani#4947, in review).
2. from_utf16*.
   • from_utf16le and from_utf16be loop with for c in char::decode_utf16(..) in from_utf16_units; Kani's loop contracts need KaniIntoIter, which this iterator does not implement (Loop contracts: for loops over iterators without a KaniIntoIter impl (e.g. char::DecodeUtf16) cannot carry a contract kani#4907).
   • The two lossy variants loop inside the default Iterator::fold (through collect::<String>()), where a loop contract has no attach site (Loop contracts have no attach site for loops inside called iterator combinators (fold/try_for_each/collect) kani#4893).
   • Every one of these loops pushes into a String and may reallocate, but CBMC's contract instrumentation, which Kani uses for loop contracts, does not allow allocation inside a loop with a contract: a minimal loop whose body is Box::new(i) and its drop fails exactly "dynamic allocation is allowed" under a loop contract (Support malloc and free in loops with loop contracts kani#3587). So a fix for Loop contracts: for loops over iterators without a KaniIntoIter impl (e.g. char::DecodeUtf16) cannot carry a contract kani#4907 alone would not make these proofs go through.

On #537 (Challenge 20), @feliperodri asked whether the scan loops could carry loop contracts, and otherwise: "If that is not yet feasible, please document this as an explicit, accepted limitation." This PR does that for these five functions. We are happy to replace the bounded harnesses with unbounded ones once Kani supports these patterns.

Verification

CI command. scripts/run-kani.sh (kani verify-std ... --cbmc-args --object-bits 12, with the script's -Z flags). All 42 harnesses were run together in one container with 3 vCPUs (and 12 GiB of memory) and --jobs=3 --output-format=terse --harness-timeout 10m --default-unwind 1000, the settings of the macOS autoharness job, and all pass:

Harness	Time (s)	Covers	Result	Failing check (panic harnesses)
check_drain_drop	18.4	7/7	SUCCESSFUL
check_drain_next	92.3	7/7	SUCCESSFUL
check_drain_panics_both_inside_char	15.0	4/4	SUCCESSFUL (panics as expected)	string.rs:2029
check_drain_panics_end_included_max	1.5	1/1	SUCCESSFUL (panics as expected)	core/slice/index.rs:50
check_drain_panics_end_inside_char	16.3	4/4	SUCCESSFUL (panics as expected)	string.rs:2030
check_drain_panics_past_end	10.5	4/4	SUCCESSFUL (panics as expected)	core/slice/index.rs:50
check_drain_panics_reversed	5.0	2/2	SUCCESSFUL (panics as expected)	core/slice/index.rs:41, core/slice/index.rs:59
check_drain_panics_start_excluded_max	1.6	1/1	SUCCESSFUL (panics as expected)	core/slice/index.rs:41
check_drain_panics_start_inside_char	13.2	4/4	SUCCESSFUL (panics as expected)	string.rs:2029
check_from_utf16be_bounded	101.6	5/5	SUCCESSFUL
check_from_utf16be_lossy_bounded	105.7	5/5	SUCCESSFUL
check_from_utf16le_bounded	121.1	5/5	SUCCESSFUL
check_from_utf16le_lossy_bounded	196.5	5/5	SUCCESSFUL
check_insert	9.4	2/2	SUCCESSFUL
check_insert_panics_inside_char	10.1	3/3	SUCCESSFUL (panics as expected)	string.rs:1769
check_insert_panics_past_end	10.2	2/2	SUCCESSFUL (panics as expected)	string.rs:1769
check_insert_str	8.6	2/2	SUCCESSFUL
check_insert_str_panics_inside_char	11.0	3/3	SUCCESSFUL (panics as expected)	string.rs:1826
check_insert_str_panics_past_end	12.1	2/2	SUCCESSFUL (panics as expected)	string.rs:1826
check_into_boxed_str	2.4	1/1	SUCCESSFUL
check_leak	0.8	1/1	SUCCESSFUL
check_pop	16.0	1/1	SUCCESSFUL
check_range_rejects_end_included_max	0.2	1/1	SUCCESSFUL
check_range_rejects_reversed	0.2	2/2	SUCCESSFUL
check_range_rejects_start_excluded_max	0.2	1/1	SUCCESSFUL
check_remove	16.4	1/1	SUCCESSFUL
check_remove_matches	405.1	2/2	SUCCESSFUL
check_remove_panics_at_end	3.0	1/1	SUCCESSFUL (panics as expected)	string.rs:1569
check_remove_panics_inside_char	13.0	3/3	SUCCESSFUL (panics as expected)	core/str/traits.rs:530
check_remove_panics_past_end	10.3	2/2	SUCCESSFUL (panics as expected)	core/str/traits.rs:530
check_replace_range	234.6	11/11	SUCCESSFUL
check_replace_range_panics_both_inside_char	14.2	4/4	SUCCESSFUL (panics as expected)	string.rs:2125
check_replace_range_panics_end_included_max	2.2	1/1	SUCCESSFUL (panics as expected)	core/slice/index.rs:50
check_replace_range_panics_end_inside_char	14.0	4/4	SUCCESSFUL (panics as expected)	string.rs:2129
check_replace_range_panics_past_end	10.7	4/4	SUCCESSFUL (panics as expected)	core/slice/index.rs:50
check_replace_range_panics_reversed	5.5	2/2	SUCCESSFUL (panics as expected)	core/slice/index.rs:59, core/slice/index.rs:41
check_replace_range_panics_start_excluded_max	2.2	1/1	SUCCESSFUL (panics as expected)	core/slice/index.rs:41
check_replace_range_panics_start_inside_char	17.6	4/4	SUCCESSFUL (panics as expected)	string.rs:2125
check_retain_bounded	196.4	5/5	SUCCESSFUL
check_split_off	3.1	1/1	SUCCESSFUL
check_split_off_panics_inside_char	10.4	3/3	SUCCESSFUL (panics as expected)	string.rs:1955
check_split_off_panics_past_end	13.6	2/2	SUCCESSFUL (panics as expected)	string.rs:1955

Times are Kani's "Verification Time" with three harnesses in flight on 3 vCPUs (head 89ab0d4). They vary between runs: in five full runs, the slowest harness (check_remove_matches) took 191 to 458 s, under the 10-minute limit. The largest single process peaked at 4.5 to 4.6 GiB across these runs (check_from_utf16le_lossy_bounded, 4.5 GiB when run alone).

• Trusting SUCCESSFUL. A result was only accepted if every kani::cover of the harness was reported satisfied. The 23 panic harnesses report SUCCESSFUL (encountered one or more panics as expected), and in each of them the only failing check is the documented one (listed in the table); by the construction of its domain, every input of the harness fails that check. In the two reversed-range harnesses, slice::range reports a start that is also past the length with the message for a start out of range, so their logs show two lines of slice_index_fail for the one check.
• Covers. Every harness has kani::covers on its inputs (long strings, interior indices, a full buffer so that insert, insert_str and replace_range reallocate, grow and shrink cases, each Bound variant, aligned, unaligned and odd-length UTF-16 input, a surrogate pair and an unpaired surrogate, the reallocation of the match Vec in remove_matches, the five paths through retain listed above). All are satisfied, so no harness is vacuous.

Mutation checks (local only, not part of this PR). Each change below was made to the library code, and the harness was run with the CI flags:

Change to the library	Harness	Result
retain does not move kept chars after a removal	check_retain_bounded	FAILED (content check in from_utf8_kept)
retain keeps the last char without calling the predicate	check_retain_bounded	FAILED (call count assertion, and content check in from_utf8_kept)
retain sets the length one byte short	check_retain_bounded	FAILED (length assertion)
from_utf16_units accepts unpaired surrogates (U+FFFD instead of Err)	check_from_utf16le_bounded, check_from_utf16be_bounded	FAILED (Ok only for valid input)
from_utf16_units drops NUL chars	check_from_utf16le_bounded, check_from_utf16be_bounded	FAILED (length)
lossy variants drop the U+FFFD for a trailing odd byte	check_from_utf16le_lossy_bounded, check_from_utf16be_lossy_bounded	FAILED (length)
remove slices with get_unchecked (no boundary check)	check_remove_panics_inside_char, check_remove_panics_past_end	FAILED (unreachable code; invalid pointer)
drain without its start boundary check	check_drain_panics_start_inside_char	FAILED (no input panics)
	check_drain_panics_end_inside_char	passes (control: its check is the end check)
replace_range without its end boundary check	check_replace_range_panics_end_inside_char	FAILED (unwinding assertion: the Splice loops become reachable)
	check_replace_range_panics_start_inside_char	passes (control: its check is the start check)
slice::range accepts reversed ranges	check_drain_panics_reversed	FAILED (invalid pointer)
	check_replace_range_panics_reversed	passes, but the failing checks move to an overflow in Vec::drain and the start boundary check
	check_range_rejects_reversed	FAILED (try_range returns Some)
slice::range without the ..=usize::MAX / Excluded(usize::MAX) checks	the four *_max harnesses	pass, but the failing check becomes attempt to add with overflow in slice::range
	check_range_rejects_end_included_max, check_range_rejects_start_excluded_max	FAILED (attempt to add with overflow in try_into_slice_range)

The should_panic rows for the last two changes show its limit: Kani accepts any panic, including an arithmetic overflow, so these harnesses alone cannot tell the documented panic from an overflow. The three check_range_rejects_* harnesses close that gap: they are ordinary harnesses, so an overflow fails them, and each of them fails on its change. On unmodified main, the logs also show the documented check in every panic harness.

Questions for the committee

1. Bounded "(U)" functions. Are bounds that are documented as Kani limitations, with upstream reproducers, acceptable for retain and the four from_utf16* functions, or should these five stay open until Kani supports the needed loop contracts?
2. "Any string length" for replace_range and remove_matches. We read the criterion as the length of the receiver, which is arbitrary here; the replaced range and the replacement are at most 4 bytes each, and the searcher returns at most 5 matches. Is that the intended reading?

Notes for reviewers

• The PR only adds code under #[cfg(kani)] (a mod verify appended to library/alloc/src/string.rs) and changes no production lines.
• Kani and CBMC issues filed while working on this PR: Loop contracts: explicit loop_modifies rejects writes to temporaries declared in the loop body (Check that var_N is assignable) kani#4906, Loop contracts: for loops over iterators without a KaniIntoIter impl (e.g. char::DecodeUtf16) cannot carry a contract kani#4907, Support stubs and function contracts on trait functions with their own generic parameters (e.g. <String as FromIterator<char>>::from_iter) kani#4908, Quantifier predicates with &&, || or if keep only one branch, so a true forall! can fail and assume(forall!(..)) can make a harness vacuous kani#5004, stub_verified panics the compiler when a modifies target's type does not implement kani::Arbitrary kani#5005, Quantifier whose body is a statement expression: a short-circuit path that skips the final expression is dropped, so false __CPROVER_exists/__CPROVER_forall assertions verify diffblue/cbmc#9189 and --z3/--cvc5: map::at exception (exit status 6) while converting a goto program that contains Rust's core::fmt::Formatter diffblue/cbmc#9190, and analysis added to #[kani::loop_invariant] with a method call lowers the call with "not enough arguments", substituting a non-deterministic value kani#4796. Related Kani fixes: Fail verification when CBMC exits abnormally after reporting results kani#4910 and Only use CBMC results that are followed by CBMC's overall status kani#4928 (merged), Keep loop attributes on rewritten for loops and add loop-only locals to loop_modifies kani#4947 (in review).

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Talha-Dmr]

A note on the two failing Kani Metrics jobs. The ubuntu-latest job was stopped by a runner shutdown (The runner has received a shutdown signal ... Process completed with exit code 143) while scripts/run-kani.sh --run metrics --with-autoharness was compiling the library. macos-latest was then cancelled by fail-fast.

This does not look related to the change. The PR only adds a #[cfg(kani)] module to library/alloc/src/string.rs, and the partition that runs the new harnesses passed (Complete - 441 successfully verified harnesses, 0 failures, 441 total). Locally, the same autoharness --list step also reaches a 9 GiB memory cap on main (c449201) with CARGO_BUILD_JOBS=2, just like this branch. So the metrics job seems to run close to the runner's memory limit.

Could the failed jobs be re-run when convenient? Thanks!

[Copilot]

Warning

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Copilot review overview

Review effort: Lite
Findings: 3 · 1

Open (4)

• String::from_utf8_unchecked(v) is invoked on v whose bytes are never proven (or constructed) to… · New
• This constructs an &str from arbitrary bytes via from_utf8_unchecked, which is UB if the slice… · New
• AnySearcher is intended to satisfy the unsafe trait Searcher contract (non-overlapping matches… · New
• The module-level documentation claims every harness is loop-free and that no #[kani::unwind]… · New

What changed in this PR

Adds Kani verification harnesses for Challenge 10 to check memory safety of String methods (including the “(U)” set) by running harnesses over real stdlib bodies under #[cfg(kani)].

Changes:

• Appends a new #[cfg(kani)] mod verify containing proof harnesses for 15 String functions.
• Introduces symbolic input generators (any_string_bytes, with_char_at) and coverage points for non-vacuity.
• Adds specialized harnessing for replace_range/remove_matches and bounded harnesses for retain/from_utf16* with documented tool limitations.

File	Description
library/​alloc/​src/​string.rs	Adds a #[cfg(kani)] verification module with Kani harnesses, helpers, and a custom Pattern/Searcher for remove_matches.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[Talha-Dmr]

Thanks for the review. ef9133a and 277b53e address the Copilot comments and a further review pass:

• Inputs: every generated String is now initialized, valid UTF-8, in all harnesses. (A small correction to comment 1: UTF-8 validity of str is a library invariant, not a validity invariant, so an invalid String is not UB by itself. But a str must be initialized.) The old generators exposed uninitialized capacity as string bytes (through set_len, or in the retain generator through a slice over spare capacity), and that was the real issue. The unbounded generators use a zeroed buffer (vec![0u8; cap], still loop-free and of symbolic size). Where a char is decoded, they place an arbitrary char at an arbitrary position. The retain generator encodes up to 12 arbitrary chars into a zeroed buffer and truncates it. The module doc explains why this covers every valid String for UB-freedom.
• replace_range: the replacement is now a checked &str, i.e. any valid UTF-8 of at most 4 bytes.
• remove_matches: the searcher is the most-general one allowed by the Searcher contract, and its SAFETY comment says exactly what it generates. On comment 3: ef9133a first added the restriction against repeated empty matches, but the contract allows them ("adjacent, non-overlapping, covering the whole haystack", and "Both ranges may have zero length"), and remove_matches just copies 0 bytes for them, so 277b53e removes it again and documents the contract instead. It now allows up to 5 matches, so the Vec of rejections grows past its initial capacity of 4 and its reallocation is exercised too.
• Covers: remove_matches now shows a real removal that leaves a long string, and a run with all 5 matches (the reallocation). retain shows a multi-byte char kept after a deletion, i.e. the path where retain re-encodes a char through its unsafe slice.
• Docs: the module doc describes the bound of each harness accurately.

All 16 harnesses pass with Kani at 8 GiB and with plain CBMC, and every cover is satisfied. For each changed harness, flipping its assertion makes CBMC report exactly that failure.

[Talha-Dmr]

CI on 277b53e: all four Verify std library partitions pass on ubuntu (441 harnesses, 0 failures). The 16 String harnesses ran in partition 1; check_remove_matches took about 7.5 minutes.

Kani List and Kani Metrics (ubuntu-latest) were stopped by a runner shutdown (The runner has received a shutdown signal, exit code 143) during the final compile step, like the Metrics job before. The same exit 143 shows up in main's merge queue runs for #696 (Kani List) and #699 (Kani Metrics), so it looks like runner memory rather than this change. Kani List passed on the previous commit of this PR. Could someone re-run those two jobs when convenient?

[Talha-Dmr]

@rajath-mk thanks again for the review. While you are looking at this PR, could the committee help with two scope questions? The answers decide where I spend the next weeks.

1. Are the bounds for retain and the four from_utf16* functions acceptable as documented tool limitations (see "Why retain and from_utf16* are bounded" in the description), or do all nine "(U)" functions need unbounded proofs for the challenge to be accepted?

2. If they must be unbounded: at the pinned Kani these loops cannot carry contracts (allocation inside a loop with a contract, and the loops inside Iterator::fold/try_fold). With VeriFast I have a local unbounded memory-safety proof of retain (unwind paths not yet covered). It depends on VeriFast changes, some of which I have submitted ([Rust] Add specs for str::get_unchecked, str::chars, Chars::next, char::len_utf8 and char::encode_utf8 verifast/verifast#1026 to [Rust] Fix elided-lifetime detection in generated contracts verifast/verifast#1029), and on how str::from_utf8_unchecked is specified, which I asked about in [Rust] Add specs for str::get_unchecked, str::chars, Chars::next, char::len_utf8 and char::encode_utf8 verifast/verifast#1026. For from_utf16*, a VeriFast proof would also need specs for core's iterator adapters (decode_utf16, map, collect) that are trusted rather than verified. Would a solution that combines Kani and VeriFast proofs, and trusts such core specs, be acceptable?

[Talha-Dmr]

Merged main into this branch (8d4cbf8) and updated the harnesses for the PanicGuard version of retain and the new from_utf16_units loop: retain is now checked byte for byte (at most 5 chars, down from 12), the from_utf16* harnesses check Ok/Err and the exact length, and new should_panic harnesses cover remove, reversed ranges, ..=usize::MAX and (Excluded(usize::MAX), Unbounded) for drain and replace_range, with one failing check per harness. Three ordinary harnesses check with slice::try_range that the range check itself, not an overflow, rejects those three range shapes. All 42 harnesses pass on 89ab0d4 with the flags of the macOS autoharness job (3 vCPUs, --jobs=3, --harness-timeout 10m), run outside CI. The description is updated, and the PR is ready for another review.