[v3risec]

Summary

This PR adds Kani proof harnesses for the 15 String functions targeted by Challenge 10 in library/alloc/src/string.rs.

It introduces 34 verification harnesses: 15 for normal execution and 19 for documented panic conditions. All harnesses exercise the real implementations. No production function bodies are changed or replaced with Kani-specific abstractions, and no kani::assume is used to assume the safety of the operations under test.

Verification approach

• Construct initialized, valid UTF-8 strings using zero-initialized buffers and complete encodings of symbolic Unicode characters.

• Use symbolic string lengths, capacities, and indices to exercise pointer arithmetic, copying, reallocation, and boundary conditions.

• Exercise real ptr::copy, ptr::copy_nonoverlapping, Vec::splice, and iterator-based implementations.

• Use kani::cover to demonstrate reachability of important paths, including reallocation, middle insertion/removal, multibyte character movement, and UTF-16 decoding cases.

• Keep the normal-path proofs separate from the panic proofs so that invalid inputs do not obscure memory-safety failures.

Coverage of the 9 unbounded-required functions

Function	Verification scope
insert_str	Symbolic receiver length, capacity, insertion position, and inserted string length
split_off	Symbolic receiver length, capacity, and split position
replace_range	Symbolic receiver length and range position; removed and inserted spans bounded to 4 bytes
remove_matches	Symbolic receiver length with a contract-respecting symbolic Searcher; up to 5 matches
retain	Bounded to 4 arbitrary Unicode characters with a symbolic keep predicate
from_utf16le	Bounded to 12 input bytes
from_utf16le_lossy	Bounded to 12 input bytes
from_utf16be	Bounded to 16 input bytes
from_utf16be_lossy	Bounded to 16 input bytes

The insert_str and split_off proofs have no fixed small input-length bound, apart from CBMC's object model. The symbolic allocation limit is 2^51 - 1 under the configured --object-bits 12 model.

For replace_range and remove_matches, the receiver length is symbolic, but the number of edited bytes or matches remains bounded. These are partial unbounded proofs, not full proofs over arbitrary edit or match counts.

The remaining 5 functions are explicitly bounded because their real implementations contain input-dependent loops that cannot currently be verified without additional proof techniques.

Panic verification

The 19 #[kani::should_panic] harnesses cover:

• Indices strictly inside multibyte UTF-8 characters.

• Indices beyond the end of a string.

• remove at the end of the string.

• Invalid range endpoints and reversed ranges in drain and replace_range.

The different panic causes are tested separately to avoid the vacuity problem where one reachable panic can mask another untested panic condition.

The five replace_range panic harnesses are individual functions with #[kani::unwind(2)], avoiding unnecessary expansion of internal Vec::Splice loops on paths that should panic before the splice operation.

UTF-8 and UTF-16 validity

All generated String inputs are valid UTF-8 by construction.

The retain harness exercises its real implementation, including character iteration and byte movement. A Kani-only stub replaces core::str::from_utf8 in the debug validation path, using an explicit UTF-8 byte validator for the bounded input. It does not replace String::retain or its memory operations.

The UTF-16 harnesses use an independent specification to check strict decoding success and the expected output length for lossy decoding. They cover aligned and unaligned inputs, odd lengths, surrogate pairs, and invalid surrogate sequences within the documented bounds.

Limitations

This PR does not claim to have completed all 9 strict unbounded requirements.

In particular:

• replace_range and remove_matches still have bounded loop-dependent operations.

• retain and all 4 UTF-16 functions remain bounded.

• Kani's default memory-safety checks do not provide complete coverage of every Rust undefined-behavior category, including uninitialized reads and aliasing/immutability violations.

These restrictions are documented rather than hidden behind assumptions, disabled unwinding checks, or changes to the implementations under test.

Resolves #61

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

[feliperodri]

Challenge 10 requires: "Ones marked as unbounded must be verified for any string/slice length." That requirement is final. A Kani solution will only be accepted if the functions marked "(unbounded)" (from_utf16le, from_utf16le_lossy, from_utf16be, from_utf16be_lossy, remove_matches, retain, insert_str, split_off, replace_range) are verified without a bound on the string or slice length. This PR still verifies at least some of them with bounded inputs, so I'm requesting changes until all of them are unbounded.