From a8327e7668c9375f4555a7670247c1b352507272 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 10 Mar 2025 13:16:25 -0700 Subject: [PATCH 1/5] add vecdeque challenge --- doc/src/challenges/0025-vecdeque.md | 77 +++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 doc/src/challenges/0025-vecdeque.md diff --git a/doc/src/challenges/0025-vecdeque.md b/doc/src/challenges/0025-vecdeque.md new file mode 100644 index 0000000000000..2b0d90afa0ca7 --- /dev/null +++ b/doc/src/challenges/0025-vecdeque.md @@ -0,0 +1,77 @@ +# Challenge 17: Verify the safety of `VecDeque` functions + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *?* + +------------------- + + +## Goal + +Verify the safety of [`VecDeque`] functions in (library/alloc/src/collections/vec_deque/mod.rs). + + +### Success Criteria + +Verify the safety of the following functions in (library/alloc/src/collections/vec_deque/mod.rs). + +| Function | +|---------| +|push_unchecked| +|buffer_read| +|buffer_write| +|buffer_range| +|copy| +|copy_nonoverlapping| +|wrap_copy| +|copy_slice| +|handle_capacity_increase| +|from_contiguous_raw_parts_in| +|get| +|get_mut| +|swap| +|capacity| +|reserve_exact| +|reserve| +|try_reserve_exact| +|try_reserve| +|shrink_to| +|abort_shrink| +|as_slices| +|as_mut_slices| +|range| +|range_mut| +|pop_front| +|pop_back| +|push_front| +|push_back| +|insert| +|remove| +|split_off| +|append| +|grow| +|make_contiguous| +|rotate_left| +|rotate_right| +|rotate_left_inner| +|rotate_right_inner| + +The verification must be unbounded---it must hold for slices of arbitrary length. + +The verification must be hold for generic type `T` (no monomorphization). + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](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 except for padding or unions. +* 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 d12cb6225ba1d4026b34fb3e59ecaca77ccc8723 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 14 Mar 2025 08:21:59 -0700 Subject: [PATCH 2/5] fix date format --- doc/src/challenges/0025-vecdeque.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/src/challenges/0025-vecdeque.md b/doc/src/challenges/0025-vecdeque.md index 2b0d90afa0ca7..a304ee99d1576 100644 --- a/doc/src/challenges/0025-vecdeque.md +++ b/doc/src/challenges/0025-vecdeque.md @@ -1,9 +1,9 @@ -# Challenge 17: Verify the safety of `VecDeque` functions +# Challenge 25: Verify the safety of `VecDeque` functions - **Status:** Open - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* +- **Start date:** *2025-03-07* +- **End date:** *2025-10-17* - **Reward:** *?* ------------------- @@ -61,7 +61,7 @@ Verify the safety of the following functions in (library/alloc/src/collections/v The verification must be unbounded---it must hold for slices of arbitrary length. -The verification must be hold for generic type `T` (no monomorphization). +The verification must hold for generic type `T` (no monomorphization). ### List of UBs From 5aae69d64f924156fc9d905545b9c0d5cf264af5 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 09:33:27 -0700 Subject: [PATCH 3/5] fix issue link, reward --- doc/src/challenges/0025-vecdeque.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/src/challenges/0025-vecdeque.md b/doc/src/challenges/0025-vecdeque.md index a304ee99d1576..1fc3a6948d3c4 100644 --- a/doc/src/challenges/0025-vecdeque.md +++ b/doc/src/challenges/0025-vecdeque.md @@ -1,17 +1,17 @@ # Challenge 25: Verify the safety of `VecDeque` functions - **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Tracking Issue:** [#286](https://github.com/model-checking/verify-rust-std/issues/286) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *?* +- **Reward:** *5000 USD* ------------------- ## Goal -Verify the safety of [`VecDeque`] functions in (library/alloc/src/collections/vec_deque/mod.rs). +Verify the safety of `VecDeque` functions in (library/alloc/src/collections/vec_deque/mod.rs). ### Success Criteria From 872cb9bddf4b52d9688b57239afcf73d7793c447 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Mar 2025 09:44:56 -0700 Subject: [PATCH 4/5] update summary.md --- doc/src/SUMMARY.md | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index f1de498184d14..98bc7d30c6cd1 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -29,3 +29,4 @@ - [13: Safety of `CStr`](./challenges/0013-cstr.md) - [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md) - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md) + - [25: Verify the safety of `VecDeque` functions](./challenges/0025-vecdeque.md) From af01d6e5207df6dbebbabe1653a749301c198664 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 08:36:21 -0700 Subject: [PATCH 5/5] update reward --- doc/src/challenges/0025-vecdeque.md | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/doc/src/challenges/0025-vecdeque.md b/doc/src/challenges/0025-vecdeque.md index 1fc3a6948d3c4..97ce51a91eb61 100644 --- a/doc/src/challenges/0025-vecdeque.md +++ b/doc/src/challenges/0025-vecdeque.md @@ -4,7 +4,7 @@ - **Tracking Issue:** [#286](https://github.com/model-checking/verify-rust-std/issues/286) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *5000 USD* +- **Reward:** *10000 USD* ------------------- @@ -16,7 +16,9 @@ Verify the safety of `VecDeque` functions in (library/alloc/src/collections/vec_ ### Success Criteria -Verify the safety of the following functions in (library/alloc/src/collections/vec_deque/mod.rs). +Verify the safety of the following functions in (library/alloc/src/collections/vec_deque/mod.rs): + +Write and prove the contract for the safety of the following unsafe functions: | Function | |---------| @@ -28,22 +30,28 @@ Verify the safety of the following functions in (library/alloc/src/collections/v |copy_nonoverlapping| |wrap_copy| |copy_slice| +|write_iter| +|write_iter_wrapping| |handle_capacity_increase| |from_contiguous_raw_parts_in| +|abort_shrink| + +Prove the absence of undefined behavior for following safe abstractions: + |get| |get_mut| |swap| -|capacity| |reserve_exact| |reserve| |try_reserve_exact| |try_reserve| |shrink_to| -|abort_shrink| +|truncate| |as_slices| |as_mut_slices| |range| |range_mut| +|drain| |pop_front| |pop_back| |push_front| @@ -52,7 +60,9 @@ Verify the safety of the following functions in (library/alloc/src/collections/v |remove| |split_off| |append| +|retain_mut| |grow| +|resize_with| |make_contiguous| |rotate_left| |rotate_right|