Merge remote-tracking branch 'origin/main' into layout-harnesses

Author: tautschnig

doc/src/SUMMARY.md

@@ -18,3 +18,5 @@
   - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
   - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
   - [Inductive data type](./challenges/0005-linked-list.md)
+  - [Contracts for SmallSort](./challenges/0008-smallsort.md)
+  - [Memory safety of String](./challenges/0010-string.md)

doc/src/challenges/0008-smallsort.md

@@ -0,0 +1,54 @@
+# Challenge 8: Contracts for SmallSort
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/56)
+- **Start date:** *2024-08-17*
+- **End date:** *2024-12-10*
+
+-------------------
+
+
+## Goal
+
+The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting
+algorithms optimized for slices with small lengths.
+In this challenge, the goal is to, first prove the memory safety of the public functions in the `smallsort` module, and, second, write contracts for them to
+show that the sorting algorithms actually sort the slices.
+
+### Success Criteria
+
+Prove absence of undefined behavior of the following public functions.
+
+1. `<T as slice::sort::shared::smallsort::StableSmallSortTypeImpl>::small_sort`
+2. `<T as slice::sort::shared::smallsort::UnstableSmallSortTypeImpl>::small_sort`
+3. `<T as slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl>::small_sort`
+4. `slice::sort::shared::smallsort::swap_if_less`
+5. `slice::sort::shared::smallsort::insertion_sort_shift_left`
+6. `slice::sort::shared::smallsort::sort4_stable`
+7. `slice::sort::shared::smallsort::has_efficient_in_place_swap`
+
+Write contracts for the following public functions that show that they actually sort the slices.
+
+1. `<T as slice::sort::shared::smallsort::StableSmallSortTypeImpl>::small_sort`
+2. `<T as slice::sort::shared::smallsort::UnstableSmallSortTypeImpl>::small_sort`
+3. `<T as slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl>::small_sort`
+
+The memory safety and the contracts of the above listed functions must be verified
+for all possible slices with arbitrary valid length.
+
+Note that most of the functions listed above call functions that contain loops.
+Function contracts and loop contracts of those callee functions may be required.
+
+### List of UBs
+
+In addition to any properties called out as `SAFETY` comments in the source
+code,
+all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.

doc/src/challenges/0010-string.md

@@ -0,0 +1,75 @@
+# Challenge X: Memory safety of String
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/61)
+- **Start date:** *2024-08-19*
+- **End date:** *2024-12-10*
+
+-------------------
+
+## Goal
+
+In this challenge, the goal is to verify the memory safety of `std::string::String`.
+Even though the majority of `String` methods are safe, many of them are safe abstractions over unsafe code.
+
+For instance, the `insert` method is implemented as follows in v1.80.1:
+```rust
+pub fn insert(&mut self, idx: usize, ch: char) {
+    assert!(self.is_char_boundary(idx));
+    let mut bits = [0; 4];
+    let bits = ch.encode_utf8(&mut bits).as_bytes();
+
+    unsafe {
+        self.insert_bytes(idx, bits);
+    }
+}
+```
+where `insert_bytes` has the following implementation:
+```rust
+unsafe fn insert_bytes(&mut self, idx: usize, bytes: &[u8]) {
+    let len = self.len();
+    let amt = bytes.len();
+    self.vec.reserve(amt);
+
+    unsafe {
+        ptr::copy(self.vec.as_ptr().add(idx), self.vec.as_mut_ptr().add(idx + amt), len - idx);
+        ptr::copy_nonoverlapping(bytes.as_ptr(), self.vec.as_mut_ptr().add(idx), amt);
+        self.vec.set_len(len + amt);
+    }
+}
+```
+The call to the unsafe `insert_bytes` method (which itself contains unsafe code) makes `insert` susceptible to undefined behavior.
+
+### Success Criteria
+
+Verify the memory safety of all public functions that are safe abstractions over unsafe code:
+
+1. `from_utf16le` (unbounded)
+1. `from_utf16le_lossy`(unbounded)
+1. `from_utf16be` (unbounded)
+1. `from_utf16be_lossy` (unbounded)
+1. `pop`
+1. `remove`
+1. `remove_matches` (unbounded)
+1. `retain` (unbounded)
+1. `insert`
+1. `insert_str` (unbounded)
+1. `split_off` (unbounded)
+1. `drain`
+1. `replace_range` (unbounded)
+1. `into_boxed_str`
+1. `leak`
+
+Ones marked as unbounded must be verified for any string/slice length.
+
+### List of UBs
+
+All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.