From 1f9ac980e62363e1a10dfee919bf5c2f8697c57e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 7 Mar 2025 08:41:18 -0800 Subject: [PATCH 1/6] add files --- doc/src/challenges/0023-vec-pt1.md | 81 ++++++++++++++++++++++++++++++ doc/src/challenges/0024-vec-pt2.md | 67 ++++++++++++++++++++++++ 2 files changed, 148 insertions(+) create mode 100644 doc/src/challenges/0023-vec-pt1.md create mode 100644 doc/src/challenges/0024-vec-pt2.md diff --git a/doc/src/challenges/0023-vec-pt1.md b/doc/src/challenges/0023-vec-pt1.md new file mode 100644 index 0000000000000..9494f1903c9c9 --- /dev/null +++ b/doc/src/challenges/0023-vec-pt1.md @@ -0,0 +1,81 @@ +# Challenge 17: Verify the safety of `Vec` functions part 1 + +- **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 memory safety of [`std::Vec`] functions (library/alloc/src/vec/mod.rs). + + +### Success Criteria + +Verify the memory safety of the following public functions in (library/alloc/src/vec/mod.rs): + +| Function | +|---------| +|from_raw_parts| +|from_nonnull| +|from_nonnull_in| +|into_raw_parts_with_alloc| +|into_boxed_slice| +|truncate| +|set_len| +|swap_remove| +|insert| +|remove| +|retain_mut| +|dedup_by| +|push| +|push_within_capacity| +|pop| +|append| +|append_elements| +|drain| +|clear| +|split_off| +|leak| +|spare_capacity_mut| +|split_at_spare_mut| +|split_at_spare_mut_with_len| +|extend_from_within| +|into_flattened| +|extend_with| +|spec_extend_from_within| +|deref| +|deref_mut| +|into_iter| +|extend_desugared| +|extend_trusted| +|extract_if| +|drop| +|try_from| + + + + + + + +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. diff --git a/doc/src/challenges/0024-vec-pt2.md b/doc/src/challenges/0024-vec-pt2.md new file mode 100644 index 0000000000000..ab2abe0954e11 --- /dev/null +++ b/doc/src/challenges/0024-vec-pt2.md @@ -0,0 +1,67 @@ +# Challenge 17: Verify the safety of `Vec` functions part 2 + +- **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 + +Continue from part 1 (Challenge 23), for this challenge, you need to verify the safety of [`std::Vec`] iterator functions in other files in (library/alloc/src/vec/). + + +### Success Criteria + +Verify the safety of the following functions that in implemnted for `IntoIter` in (library/alloc/src/vec/into_iter.rs): + +| Function | +|---------| +|as_slice| +|as_mut_slice| +|forget_allocation_drop_remaining| +|into_vecdeque| +|next| +|size_hint| +|advance_by| +|next_chunk| +|fold| +|try_fold| +|__iterator_get_unchecked| +|next_back| +|advance_back_by| +|drop| + +and the following functions from other files: + +| Function | in File| +|---------|---------| +|next| extract_if.rs| +|spec_extend (for IntoIter) | spec_extend.rs | +|spec_extend (for slice::Iter) | spec_extend.rs | +|from_elem (for i8)| spec_from_elem.rs | +|from_elem (for u8)| spec_from_elem.rs | +|from_elem (for ())| spec_from_elem.rs | +|from_iter| spec_from_iter.rs| +|from_iter (default)| spec_from_iter_nested.rs| + + +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 e9d20ef088219df4e5740ae4aa1fa1c11159aec8 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 14 Mar 2025 08:29:41 -0700 Subject: [PATCH 2/6] fix date format --- doc/src/challenges/0023-vec-pt1.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0023-vec-pt1.md b/doc/src/challenges/0023-vec-pt1.md index 9494f1903c9c9..7c94a4481cdc6 100644 --- a/doc/src/challenges/0023-vec-pt1.md +++ b/doc/src/challenges/0023-vec-pt1.md @@ -2,8 +2,8 @@ - **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:** *?* ------------------- From b2e240b14b0f68299cc651d28439dac721ee20a0 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 14 Mar 2025 08:31:13 -0700 Subject: [PATCH 3/6] fix typos --- doc/src/challenges/0023-vec-pt1.md | 2 +- doc/src/challenges/0024-vec-pt2.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0023-vec-pt1.md b/doc/src/challenges/0023-vec-pt1.md index 7c94a4481cdc6..ebf1d446a0c39 100644 --- a/doc/src/challenges/0023-vec-pt1.md +++ b/doc/src/challenges/0023-vec-pt1.md @@ -65,7 +65,7 @@ Verify the memory safety of the following public functions in (library/alloc/src 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 diff --git a/doc/src/challenges/0024-vec-pt2.md b/doc/src/challenges/0024-vec-pt2.md index ab2abe0954e11..60ed39db93608 100644 --- a/doc/src/challenges/0024-vec-pt2.md +++ b/doc/src/challenges/0024-vec-pt2.md @@ -51,7 +51,7 @@ and the following functions from other files: 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 45777b03ee7700bb2e14e03a867120b17d5e3f26 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 09:29:22 -0700 Subject: [PATCH 4/6] fix issue link, reward --- doc/src/challenges/0023-vec-pt1.md | 13 +++++-------- doc/src/challenges/0024-vec-pt2.md | 10 +++++----- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/doc/src/challenges/0023-vec-pt1.md b/doc/src/challenges/0023-vec-pt1.md index ebf1d446a0c39..4fbee60b37874 100644 --- a/doc/src/challenges/0023-vec-pt1.md +++ b/doc/src/challenges/0023-vec-pt1.md @@ -1,22 +1,22 @@ -# Challenge 17: Verify the safety of `Vec` functions part 1 +# Challenge 23: Verify the safety of `Vec` functions part 1 - **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Tracking Issue:** [#284](https://github.com/model-checking/verify-rust-std/issues/284) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *?* +- **Reward:** *5000 USD* ------------------- ## Goal -Verify the memory safety of [`std::Vec`] functions (library/alloc/src/vec/mod.rs). +Verify the safety of `std::Vec` functions (library/alloc/src/vec/mod.rs). ### Success Criteria -Verify the memory safety of the following public functions in (library/alloc/src/vec/mod.rs): +Verify the safety of the following public functions in (library/alloc/src/vec/mod.rs): | Function | |---------| @@ -60,9 +60,6 @@ Verify the memory safety of the following public functions in (library/alloc/src - - - The verification must be unbounded---it must hold for slices of arbitrary length. The verification must hold for generic type `T` (no monomorphization). diff --git a/doc/src/challenges/0024-vec-pt2.md b/doc/src/challenges/0024-vec-pt2.md index 60ed39db93608..02daaf96e1366 100644 --- a/doc/src/challenges/0024-vec-pt2.md +++ b/doc/src/challenges/0024-vec-pt2.md @@ -1,22 +1,22 @@ -# Challenge 17: Verify the safety of `Vec` functions part 2 +# Challenge 24: Verify the safety of `Vec` functions part 2 - **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Tracking Issue:** [#285](https://github.com/model-checking/verify-rust-std/issues/285) - **Start date:** *2025/03/07* - **End date:** *2025/10/17* -- **Reward:** *?* +- **Reward:** *5000 USD* ------------------- ## Goal -Continue from part 1 (Challenge 23), for this challenge, you need to verify the safety of [`std::Vec`] iterator functions in other files in (library/alloc/src/vec/). +Continue from part 1 (Challenge 23), for this challenge, you need to verify the safety of `std::Vec` iterator functions in other files in (library/alloc/src/vec/). ### Success Criteria -Verify the safety of the following functions that in implemnted for `IntoIter` in (library/alloc/src/vec/into_iter.rs): +Verify the safety of the following functions that in implemented for `IntoIter` in (library/alloc/src/vec/into_iter.rs): | Function | |---------| From bf153ff6449fe169993e3da5261f8fe4c61fbecd Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Mar 2025 09:41:40 -0700 Subject: [PATCH 5/6] update summary.md --- doc/src/SUMMARY.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index f1de498184d14..6942261533bf1 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -29,3 +29,5 @@ - [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) + - [23: Verify the safety of Vec functions part 1](./challenges/0023-vec-pt1.md) + - [24: Verify the safety of Vec functions part 2](./challenges/0024-vec-pt2.md) From 9330f290699f69892c19db3bef578ee2e4cab02e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 08:08:23 -0700 Subject: [PATCH 6/6] update reward --- doc/src/challenges/0023-vec-pt1.md | 2 +- doc/src/challenges/0024-vec-pt2.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0023-vec-pt1.md b/doc/src/challenges/0023-vec-pt1.md index 4fbee60b37874..3abc65775455b 100644 --- a/doc/src/challenges/0023-vec-pt1.md +++ b/doc/src/challenges/0023-vec-pt1.md @@ -4,7 +4,7 @@ - **Tracking Issue:** [#284](https://github.com/model-checking/verify-rust-std/issues/284) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *5000 USD* +- **Reward:** *10000 USD* ------------------- diff --git a/doc/src/challenges/0024-vec-pt2.md b/doc/src/challenges/0024-vec-pt2.md index 02daaf96e1366..c369dea547368 100644 --- a/doc/src/challenges/0024-vec-pt2.md +++ b/doc/src/challenges/0024-vec-pt2.md @@ -4,7 +4,7 @@ - **Tracking Issue:** [#285](https://github.com/model-checking/verify-rust-std/issues/285) - **Start date:** *2025/03/07* - **End date:** *2025/10/17* -- **Reward:** *5000 USD* +- **Reward:** *10000 USD* -------------------