From 44521dc8e9126bd6b9f5fcd876168778fa72b693 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sat, 17 Aug 2024 23:21:54 -0500 Subject: [PATCH 1/2] Add challenge for smallsort --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0008-smallsort | 54 +++++++++++++++++++++++++++++++ 2 files changed, 55 insertions(+) create mode 100644 doc/src/challenges/0008-smallsort diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 9a8023d63908a..bb064448efe87 100644 --- a/doc/src/SUMMARY.md +++ b/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) \ No newline at end of file diff --git a/doc/src/challenges/0008-smallsort b/doc/src/challenges/0008-smallsort new file mode 100644 index 0000000000000..691152e99b859 --- /dev/null +++ b/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. `::small_sort` +2. `::small_sort` +3. `::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. `::small_sort` +2. `::small_sort` +3. `::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 function listed above calls 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. From cc8096a958423b806b0e9ac28d26d4c15304bc85 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 15:13:22 +0200 Subject: [PATCH 2/2] Update doc/src/challenges/0008-smallsort --- doc/src/challenges/0008-smallsort | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0008-smallsort b/doc/src/challenges/0008-smallsort index 691152e99b859..b0a4a8f743275 100644 --- a/doc/src/challenges/0008-smallsort +++ b/doc/src/challenges/0008-smallsort @@ -36,7 +36,7 @@ Write contracts for the following public functions that show that they actually 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 function listed above calls functions that contain loops. +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