Verify String::remove in alloc::string

[szlee118]

Intro

This verification harness is designed to validate the behavior of the remove method on Rust's String type. The remove method removes a character at a specified index from a string and returns it. The harness leverages Kani's verification capabilities to ensure correctness under various constraints.

Key Pointer Functions Related:

• *const T::add / *mut T::add:
  • Used in self.vec.as_ptr().add(next) and self.vec.as_mut_ptr().add(idx) to compute the addresses of the source and destination pointers for the copy operation.
• *const T::sub / *mut T::sub:
  • Conceptually used for addressing adjustments (e.g., computing len - next).

Purpose

The primary goal of this harness is to verify:
The remove method correctly decreases the string length by one.
The character removed from the string is valid and remains consistent with the original input constraints.

Resolves model-checking#76

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