|
| 1 | +# Challenge 29: Safety of boxed |
| 2 | + |
| 3 | +- **Status:** *Open* |
| 4 | +- **Solution:** *Option field to point to the PR that solved this challenge.* |
| 5 | +- **Tracking Issue:** [#526](https://github.com/model-checking/verify-rust-std/issues/526) |
| 6 | +- **Start date:** *2026/01/01* |
| 7 | +- **End date:** *2026/12/31* |
| 8 | +- **Reward:** *15,000 USD* |
| 9 | + |
| 10 | +------------------- |
| 11 | + |
| 12 | + |
| 13 | +## Goal |
| 14 | + |
| 15 | +The goal of this challenge is to verify the [boxed](https://doc.rust-lang.org/std/boxed/index.html) module, which implements the Box family of types (which includes Box and other related types such as ThinBox). A Box is a type of smart pointer that points to a uniquely-owned heap allocation for arbitrary types. |
| 16 | + |
| 17 | +## Motivation |
| 18 | + |
| 19 | +A Box allows the storage of data on the heap rather than the stack. This has several applications, a common [example](https://doc.rust-lang.org/book/ch15-01-box.html#enabling-recursive-types-with-boxes) being for using dynamically-sized types in contexts requiring an exact size (e.g., recursive types). While this type is useful and diverse in its applications, it also extensively uses unsafe code, meaning it is important to verify that this module is free of undefined behaviour. |
| 20 | + |
| 21 | +### Success Criteria |
| 22 | + |
| 23 | +All the following unsafe functions must be annotated with safety contracts and the contracts have been verified: |
| 24 | + |
| 25 | +| Function | Location | |
| 26 | +|---------|---------| |
| 27 | +| `Box<mem::MaybeUninit<T>, A>::assume_init` | `alloc::boxed` | |
| 28 | +| `Box<[mem::MaybeUninit<T>], A>::assume_init` | `alloc::boxed` | |
| 29 | +| `Box<T>::from_raw` | `alloc::boxed` | |
| 30 | +| `Box<T>::from_non_null` | `alloc::boxed` | |
| 31 | +| `Box<T, A>::from_raw_in` | `alloc::boxed` | |
| 32 | +| `Box<T, A>::from_non_null_in` | `alloc::boxed` | |
| 33 | +| `<dyn Error>::downcast_unchecked` | `alloc::boxed::convert` | |
| 34 | +| `<dyn Error + Send>::downcast_unchecked` | `alloc::boxed::convert` | |
| 35 | +| `<dyn Error + Send + Sync>::downcast_unchecked` | `alloc::boxed::convert` | |
| 36 | + |
| 37 | +The following functions contain unsafe code in their bodies but are not themselves marked unsafe. At least 75% of these should be proven unconditionally safe, or safety contracts should be added: |
| 38 | + |
| 39 | +| Function | Location | |
| 40 | +|---------|---------| |
| 41 | +| `Box<T, A>::new_in` | `alloc::boxed` | |
| 42 | +| `Box<T, A>::try_new_in` | `alloc::boxed` | |
| 43 | +| `Box<T, A>::try_new_uninit_in` | `alloc::boxed` | |
| 44 | +| `Box<T, A>::try_new_zeroed_in` | `alloc::boxed` | |
| 45 | +| `Box<T, A>::into_boxed_slice` | `alloc::boxed` | |
| 46 | +| `Box<[T]>::new_uninit_slice` | `alloc::boxed` | |
| 47 | +| `Box<[T]>::new_zeroed_slice` | `alloc::boxed` | |
| 48 | +| `Box<[T]>::try_new_uninit_slice` | `alloc::boxed` | |
| 49 | +| `Box<[T]>::try_new_zeroed_slice` | `alloc::boxed` | |
| 50 | +| `Box<[T]>::into_array` | `alloc::boxed` | |
| 51 | +| `Box<T, A>::new_uninit_slice_in` | `alloc::boxed` | |
| 52 | +| `Box<T, A>::new_zeroed_slice_in` | `alloc::boxed` | |
| 53 | +| `Box<T, A>::try_new_uninit_slice_in` | `alloc::boxed` | |
| 54 | +| `Box<T, A>::try_new_zeroed_slice_in` | `alloc::boxed` | |
| 55 | +| `Box<mem::MaybeUninit<T>, A>::write` | `alloc::boxed` | |
| 56 | +| `Box<T>::into_non_null` | `alloc::boxed` | |
| 57 | +| `Box<T, A>::into_raw_with_allocator` | `alloc::boxed` | |
| 58 | +| `Box<T, A>::into_non_null_with_allocator` | `alloc::boxed` | |
| 59 | +| `Box<T, A>::into_unique` | `alloc::boxed` | |
| 60 | +| `Box<T, A>::leak` | `alloc::boxed` | |
| 61 | +| `Box<T, A>::into_pin` | `alloc::boxed` | |
| 62 | +| `<Box<T, A> as Drop>::drop` | `alloc::boxed` | |
| 63 | +| `<Box<T> as Default>::default` | `alloc::boxed` | |
| 64 | +| `<Box<str> as Default>::default` | `alloc::boxed` | |
| 65 | +| `<Box<T, A> as Clone>::clone` | `alloc::boxed` | |
| 66 | +| `<Box<str> as Clone>::clone` | `alloc::boxed` | |
| 67 | +| `<Box<[T]> as BoxFromSlice<T>>::from_slice` | `alloc::boxed::convert` | |
| 68 | +| `<Box<str> as From<&str>>::from` | `alloc::boxed::convert` | |
| 69 | +| `<Box<[u8], A> as From<Box<str, A>>>::from` | `alloc::boxed::convert` | |
| 70 | +| `<Box<[T; N]> as TryFrom<Box<[T]>>>::try_from` | `alloc::boxed::convert` | |
| 71 | +| `<Box<[T; N]> as TryFrom<Box<T>>>::try_from` | `alloc::boxed::convert` | |
| 72 | +| `Box<dyn Any, A>::downcast` | `alloc::boxed::convert` | |
| 73 | +| `Box<dyn Any + Send, A>::downcast` | `alloc::boxed::convert` | |
| 74 | +| `Box<dyn Any + Send + Sync, A>::downcast` | `alloc::boxed::convert` | |
| 75 | +| `<dyn Error>::downcast` | `alloc::boxed::convert` | |
| 76 | +| `<dyn Error + Send>::downcast` | `alloc::boxed::convert` | |
| 77 | +| `<dyn Error + Send + Sync>::downcast` | `alloc::boxed::convert` | |
| 78 | +| `<ThinBox<T> as Deref>::deref` | `alloc::boxed::thin` | |
| 79 | +| `<ThinBox<T> as DerefMut>::deref_mut` | `alloc::boxed::thin` | |
| 80 | +| `<ThinBox<T> as Drop>::drop` | `alloc::boxed::thin` | |
| 81 | +| `ThinBox<T>::meta` | `alloc::boxed::thin` | |
| 82 | +| `ThinBox<T>::with_header` | `alloc::boxed::thin` | |
| 83 | +| `WithHeader<H>::new` | `alloc::boxed::thin` | |
| 84 | +| `WithHeader<H>::try_new` | `alloc::boxed::thin` | |
| 85 | +| `WithHeader<H>::new_unsize_zst` | `alloc::boxed::thin` | |
| 86 | +| `WithHeader<H>::header` | `alloc::boxed::thin` | |
| 87 | + |
| 88 | +For functions taking inputs of generic type 'T', the proofs can be limited to primitive types only. |
| 89 | + |
| 90 | +*List of UBs* |
| 91 | + |
| 92 | +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): |
| 93 | +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. |
| 94 | +* Invoking undefined behavior via compiler intrinsics. |
| 95 | +* Mutating immutable bytes. |
| 96 | +* Producing an invalid value. |
| 97 | + |
| 98 | +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) |
| 99 | +in addition to the ones listed above. |
0 commit comments