Challenge proposal: SmallSort (model-checking#57)

Author: qinheping

doc/src/SUMMARY.md

@@ -18,3 +18,4 @@
   - [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)

doc/src/challenges/0008-smallsort

@@ -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.