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. There are no cfg(kani) body swaps, no stubs of the functions under test, no kani::assume in the module, and nothing is assumed about the results of the functions under test.

• 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 and the four from_utf16* functions. The reasons and minimal reproducers are below, with links to the upstream Kani issues.
• Non-(U) functions: pop, remove, insert, drain, into_boxed_str and leak. These are also verified for arbitrary lengths, since their harnesses are loop-free.
• Panic harnesses: ten #[kani::should_panic] harnesses, two per function, show that the documented panic conditions the other harnesses stay out of do panic: an index strictly inside a multi-byte char, and separately an index past the end (insert, insert_str, split_off, drain, replace_range).

Status per function

Function	(U) required	Status	Harness
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_inside_char, check_replace_range_panics_past_end
remove_matches	yes	receiver unbounded, <= 5 matches	check_remove_matches
retain	yes	bounded, <= 12 chars (<= 48 bytes) (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 <= 12 bytes (tool limit)	check_from_utf16be_bounded
from_utf16be_lossy	yes	bounded, input <= 12 bytes (tool limit)	check_from_utf16be_lossy_bounded
pop	no	arbitrary length	check_pop
remove	no	arbitrary length	check_remove
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_inside_char, check_drain_panics_past_end
into_boxed_str	no	arbitrary length	check_into_boxed_str
leak	no	arbitrary length	check_leak

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 documented panics (see 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 (idx <= len, and start <= end <= len for ranges, which also keeps the main harnesses out of the out-of-range panics), the bounds in the table above, and, in the panic harnesses, indices without a char boundary. The documented preconditions (indices on char boundaries) are not assumed either: they hold by construction. The harnesses that pick an index assert! that it is a char boundary before the call; remove removes at the start of the encoded char by construction, and check_pop truncates the string right after the char from with_char_at, so pop decodes exactly that char. The replacement string of replace_range is built constructively (up to 4 arbitrary chars encoded into a zeroed buffer, so every valid UTF-8 string of at most 4 bytes), not filtered through from_utf8.

Panics. Panics are not UB, so the main harnesses stay out of the documented panic conditions by construction. Ten #[kani::should_panic] harnesses, two per function, show that insert, insert_str, split_off, drain and replace_range panic for an index strictly inside a multi-byte char (*_panics_inside_char) and, separately, for an index past the end (*_panics_past_end). In the first, the string has an arbitrary char at an arbitrary position and the index is strictly inside it; for drain and replace_range, one end of the range a..b (a <= b) is inside the char and the other end is in bounds, so only a char-boundary check can panic. The two cases are separate harnesses because a should_panic harness passes as soon as some input panics: with both kinds of index in one harness, the past-the-end inputs alone would make it pass without the char-boundary checks (found in review). Reversed ranges and Bound overflow (..=usize::MAX) are not exercised. Kani accepts such a harness only if a panic-class failure is reachable and every failing check is of that class (assertions, which also include arithmetic overflow and out-of-bounds indexing), so no UB is reachable before the panic (Kani uses panic=abort). That the failing checks are exactly the documented panics (the is_char_boundary assertions, except in check_drain_panics_past_end and check_replace_range_panics_past_end, where it is the end-past-length panic of slice::range) was checked in the logs. As an extra local check (not part of this PR), a kani::cover placed after the call is UNREACHABLE in all ten harnesses, so every input in these domains panics. pop has no panic condition. remove has no panic harness: for an index inside a char, its panic path formats the error message with loops over the string (see the next paragraph).

check_remove and #[kani::unwind(2)]. self[idx..] has a panic path (str::slice_error_fail) that formats the error message with loops over the string. Under the harness that path is infeasible (idx is the start of a well-formed char), but symbolic execution would otherwise unfold it without end. The bound only cuts that path: unwinding assertions stay enabled, so a reachable loop needing more iterations would fail the proof, and no loop is reachable on the verified path.

Bounded harnesses. retain runs on every valid string of up to 12 chars (arbitrary chars encoded back to back into a zeroed buffer) with an arbitrary keep-predicate, and asserts that the new length is exactly the total UTF-8 length of the chars the predicate kept (counted inside the predicate). A cover shows a multi-byte char kept after a deletion, i.e. the unsafe re-encode path. The from_utf16* harnesses run on every sub-slice of an arbitrary byte array, so odd lengths and both odd and even start addresses (the align_to fast path and the unaligned path) are covered. They check an output-length bound and that the strict variants return Err for an input that starts with a low surrogate (which is always unpaired there); covers show a leading surrogate pair that decodes and a leading unpaired low surrogate. 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.

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; remove_matches does one copy per kept segment. 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 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; it holds for every index of the all-NUL receiver, which is therefore the haystack on which the contract allows the most match sequences (remove_matches itself only moves the bytes, it never inspects them). With up to 5 matches the Vec of matches grows past its initial capacity, and a cover shows that reallocation path is reached.

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 and remove_matches, the get_unchecked / from_raw_parts_mut accesses and the re-encode of retain, 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). Kani's -Z uninit-checks cannot be added as an extra check: at the pinned Kani it does not work for 20 of the 21 harnesses. 12 hit an internal compiler error on the function pointers in the reachable formatting code (Tracking Issue: Automatically Verify Memory Initialization kani#3300), 5 hit another internal error in its layout code (ty_layout.rs:190), and 3 did not finish compiling within 30 minutes. check_leak passes with it.
• Mutating immutable bytes. Kani has no check for this (it does not model immutability or aliasing rules such as Stacked Borrows), so this item rests on inspection only: 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 and Drain::next 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) would be reported by Kani's unreachable code checks. The CI configuration does not check the validity of other intermediate values. As an extra check outside CI, 13 of the 21 harnesses, including every harness that decodes UTF-8 from the String (check_pop, check_remove, check_drain_next, check_retain_bounded), also pass with -Z valid-value-checks added, with every cover satisfied. The other 8 each stop at one construct this checker does not support yet (copy_nonoverlapping::<u8>, or drop_in_place of some types), which Kani reports as their only failure; since that cuts the paths behind it, the extra check is incomplete for those 8. They include the four from_utf16* harnesses, whose chars come from char::from_u32_unchecked in DecodeUtf16::next.

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 (0.67.0, commit 152c6a8c, CBMC 6.10.0) none of these loops can carry one:

1. retain. An unbounded proof of the real body needs two things the pinned tools do not provide:
   • A loop contract whose write set can include the loop-body temporaries, such as the Chars built by get_unchecked(..).chars().next(). Kani declares every MIR local at function entry, so writes to them inside callees fail "Check that self->ptr is assignable" (Loop contracts: explicit loop_modifies rejects writes to temporaries declared in the loop body (Check that var_N is assignable) kani#4906). With a prototype Kani fix (not part of this PR), a verbatim copy of the body passes with a loop contract whose invariant is quantified over a constant range (0 of 755 checks failed), so this part is fixable in Kani.
   • An invariant quantified over the unprocessed suffix guard.idx..len, which is what justifies the unchecked unwrap of the char that next_code_point decodes: a forall with symbolic bounds. The SAT backend drops such quantifiers (current Kani main reports this as an error, Fail verification when the solver backend drops quantifiers kani#4719), and the SMT backends (z3, cvc5) crash while encoding a harness with this invariant. So even with macro definitions escape from local scopes rust-lang/rust#4906 fixed, an unbounded retain proof needs quantifier support in CBMC.
   • In addition, calls inside loop_invariant closures become nondeterministic (#[kani::loop_invariant] with a method call lowers the call with "not enough arguments", substituting a non-deterministic value kani#4796, with our analysis in a comment there).
2. from_utf16*. The four functions reach three different loops:
   • Only from_utf16le on the aligned path reaches the for c in char::decode_utf16(..) loop in String::from_utf16. Kani's loop-contract macro needs KaniIntoIter, which is not implemented for this iterator (Loop contracts: for loops over iterators without a KaniIntoIter impl (e.g. char::DecodeUtf16) cannot carry a contract kani#4907).
   • The unaligned path of from_utf16le and all of from_utf16be loop in the default Iterator::try_fold (while let, reached through collect::<Result<String, _>>(), String::extend, for_each and GenericShunt::try_fold), and both lossy variants loop in the default Iterator::fold (through collect::<String>(), extend and Map::fold). These generic default loops cannot carry a useful invariant, because the iterator fields and the String captured by the closure cannot be named, and an annotation in core would apply to every harness that reaches fold. Stubbing or contracting <String as FromIterator<char>>::from_iter instead is rejected, because Kani does not support stubs or contracts on generic trait functions (Support stubs and function contracts on trait functions with their own generic parameters (e.g. <String as FromIterator<char>>::from_iter) kani#4908).
   • Every one of these loops pushes into a String and may reallocate, but CBMC's contract instrumentation (DFCC), which Kani uses for loop contracts, creates loop write sets with allocation and deallocation disabled: a minimal loop whose body is Box::new(i) and its drop fails exactly "dynamic allocation is allowed" and "Check that ptr is freeable" under a loop contract, with CBMC 6.10 and 6.11. 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, with minimal reproducers in the linked issues. 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 ... --output-format=terse --cbmc-args --object-bits 12, with the script's -Z flags). Every harness was run in exactly that form, one container per harness (2 vCPU, 8 GiB). All 26 pass:

Harness	CBMC time (s)	Wall, incl. std build (s)	Covers satisfied	Result
check_drain_drop	18.4	76	7/7	SUCCESSFUL
check_drain_next	44.0	95	7/7	SUCCESSFUL
check_drain_panics_inside_char	13.8	109	5/5	SUCCESSFUL (panics as expected)
check_drain_panics_past_end	6.5	87	3/3	SUCCESSFUL (panics as expected)
check_from_utf16be_bounded	47.6	148	5/5	SUCCESSFUL
check_from_utf16be_lossy_bounded	50.7	110	5/5	SUCCESSFUL
check_from_utf16le_bounded	110.8	214	5/5	SUCCESSFUL
check_from_utf16le_lossy_bounded	251.7	370	5/5	SUCCESSFUL
check_insert	11.1	116	2/2	SUCCESSFUL
check_insert_panics_inside_char	7.9	91	3/3	SUCCESSFUL (panics as expected)
check_insert_panics_past_end	9.7	111	2/2	SUCCESSFUL (panics as expected)
check_insert_str	7.0	60	2/2	SUCCESSFUL
check_insert_str_panics_inside_char	12.4	72	3/3	SUCCESSFUL (panics as expected)
check_insert_str_panics_past_end	12.6	134	2/2	SUCCESSFUL (panics as expected)
check_into_boxed_str	3.3	96	1/1	SUCCESSFUL
check_leak	0.6	53	1/1	SUCCESSFUL
check_pop	12.6	72	1/1	SUCCESSFUL
check_remove	151.6	266	1/1	SUCCESSFUL
check_remove_matches	457.7	536	2/2	SUCCESSFUL
check_replace_range	268.6	376	11/11	SUCCESSFUL
check_replace_range_panics_inside_char	16.4	144	5/5	SUCCESSFUL (panics as expected)
check_replace_range_panics_past_end	11.9	125	3/3	SUCCESSFUL (panics as expected)
check_retain_bounded	389.7	492	1/1	SUCCESSFUL
check_split_off	4.6	106	1/1	SUCCESSFUL
check_split_off_panics_inside_char	6.2	89	3/3	SUCCESSFUL (panics as expected)
check_split_off_panics_past_end	5.8	90	2/2	SUCCESSFUL (panics as expected)

• Time and memory. The slowest CBMC time is 458 s (check_remove_matches). CBMC times vary between identical runs by up to about 1.5x (312 s and 458 s for check_remove_matches in two runs). Peak memory (largest process) is at most 4.3 GiB (check_from_utf16le_lossy_bounded); every other harness stays at or below 2.5 GiB.
• Trusting SUCCESSFUL. Because of Kani reports VERIFICATION SUCCESSFUL when CBMC runs out of memory while writing its JSON results kani#4905 (fixed on Kani main by Fail verification when CBMC exits abnormally after reporting results kani#4910, after the pinned version), a result was only accepted if every kani::cover of the harness was reported satisfied and no out-of-memory message appeared. The ten panic harnesses report SUCCESSFUL (encountered one or more panics as expected), and their failing checks are only the documented panics: the is_char_boundary assertions of the function, except in check_drain_panics_past_end and check_replace_range_panics_past_end, where it is the out-of-bounds panic of slice::range.
• 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 leading surrogate pair that decodes and a leading unpaired low surrogate, the reallocation of the match Vec in remove_matches, a multi-byte char moved by retain). All are satisfied, so no harness is vacuous.
• Mutation check (local only, not part of this PR). For every harness, flipping its key assertion (the length, decoded-char or output-bound check) makes it fail with exactly the flipped assertion reported, both in Kani's CI mode and with plain CBMC on the same goto binary. Negating the assert!s that replaced the former assumptions (in check_insert, in check_drain_next and inside the remove_matches searcher) fails as well, so they are evaluated. In check_retain_bounded, counting chars instead of bytes in the predicate makes the exact-length assertion fail. In the strict from_utf16* harnesses, asserting that a leading low surrogate never yields Err fails, so that path is reached. For the panic harnesses, replacing the char-boundary checks of insert, insert_str and split_off by idx <= len and removing those of drain and replace_range makes each of the five *_panics_inside_char harnesses fail, while the five *_panics_past_end harnesses still pass.
• Extra checks outside CI. -Z valid-value-checks and -Z uninit-checks, see the UB section above.

Questions for the committee

1. Bounded "(U)" functions. Are bounds that are documented as Kani limitations, with upstream reproducers, acceptable for retain (<= 12 chars) and the four from_utf16* functions (inputs of <= 12 bytes), 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, or should the replacement length and the number of matches be unbounded too?

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; lib.rs is untouched.
• Kani 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, and reproducers or analysis added to Kani reports VERIFICATION SUCCESSFUL when CBMC runs out of memory while writing its JSON results kani#4905, #[kani::loop_invariant] with a method call lowers the call with "not enough arguments", substituting a non-deterministic value kani#4796 and High memory consumption for interior mutability function contract test  kani#3611.
• Kani reports VERIFICATION SUCCESSFUL when CBMC runs out of memory while writing its JSON results kani#4905 (Kani can report VERIFICATION:- SUCCESSFUL when CBMC runs out of memory while writing traces) is why the harnesses keep covers on the inputs and why a result was only trusted when every cover was reported satisfied. We fixed it on Kani main in Fail verification when CBMC exits abnormally after reporting results kani#4910 (merged), with a follow-up in Only use CBMC results that are followed by CBMC's overall status kani#4928; the pinned Kani 0.67 does not have the fix.

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?