From 9854f9300313426e9198e53dd1367673c2e09e3f Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 09:29:24 -0700 Subject: [PATCH 1/3] add rawvec challenge --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0019-rawvec.md | 67 +++++++++++++++++++++++++++++++ 2 files changed, 68 insertions(+) create mode 100644 doc/src/challenges/0019-rawvec.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index f1de498184d14..ad0a163720548 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) + - [13: Safety of `RawVec`](./challenges/0019-rawvec.md) diff --git a/doc/src/challenges/0019-rawvec.md b/doc/src/challenges/0019-rawvec.md new file mode 100644 index 0000000000000..2e1dbc90e1264 --- /dev/null +++ b/doc/src/challenges/0019-rawvec.md @@ -0,0 +1,67 @@ +# Challenge 25: Verify the safety of `RawVec` functions + +- **Status:** Open +- **Tracking Issue:** [#286](https://github.com/model-checking/verify-rust-std/issues/286) +- **Start date:** *2025-03-07* +- **End date:** *2025-10-17* +- **Reward:** *10000 USD* + +------------------- + + +## Goal + +Verify the safety of `RawVec` functions in (library/alloc/src/raw_vec/mod.rs). + +## Motivation + +`RawVec` is the type of `Vec` and `VecDeque` main component: the buffer. Therefore, the safety of the functions of `Vec` and `VecDeque` depend on these of ``RawVec`. + +### Success Criteria + +Verify the safety of the following functions in (library/alloc/src/raw_vec/mod.rs): + +Write and prove the contract for the safety of the following unsafe functions: + +| Function | +|---------| +|new_cap| +|into_box| +|from_raw_parts_in| +|from_nonnull_in| +|set_ptr_and_cap| +|shrink_unchecked| +|deallocate| + +Prove the absence of undefined behavior for following safe abstractions: + +| Function | +|---------| +|drop| +|new_in| +|with_capacity_in| +|try_allocate_in| +|current_memory| +|try_reserve| +|try_reserve_exact| +|grow_amortized| +|grow_exact| +|shrink| +|finish_grow| + +The verification must be unbounded---it must hold for slices of arbitrary length. + +The verification must 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 613291d0d90863d027882e9124717a2f1dcb0609 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 09:31:07 -0700 Subject: [PATCH 2/3] add rawvec challenge --- doc/src/challenges/0019-rawvec.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0019-rawvec.md b/doc/src/challenges/0019-rawvec.md index 2e1dbc90e1264..796d393a18a3a 100644 --- a/doc/src/challenges/0019-rawvec.md +++ b/doc/src/challenges/0019-rawvec.md @@ -1,7 +1,7 @@ # Challenge 25: Verify the safety of `RawVec` functions - **Status:** Open -- **Tracking Issue:** [#286](https://github.com/model-checking/verify-rust-std/issues/286) +- **Tracking Issue:** [#283](https://github.com/model-checking/verify-rust-std/issues/283) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* - **Reward:** *10000 USD* From c3ed50af7b4401d74d00b87c405b6da51a8bba95 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Apr 2025 12:40:22 +0200 Subject: [PATCH 3/3] Update doc/src/challenges/0019-rawvec.md --- doc/src/challenges/0019-rawvec.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0019-rawvec.md b/doc/src/challenges/0019-rawvec.md index 796d393a18a3a..7d25a0bc9f8a3 100644 --- a/doc/src/challenges/0019-rawvec.md +++ b/doc/src/challenges/0019-rawvec.md @@ -15,7 +15,7 @@ Verify the safety of `RawVec` functions in (library/alloc/src/raw_vec/mod.rs). ## Motivation -`RawVec` is the type of `Vec` and `VecDeque` main component: the buffer. Therefore, the safety of the functions of `Vec` and `VecDeque` depend on these of ``RawVec`. +`RawVec` is the type of the main component of both `Vec` and `VecDeque`: the buffer. Therefore, the safety of the functions of `Vec` and `VecDeque` depend on the safety of `RawVec`. ### Success Criteria