- Status: Open
- Tracking Issue: #284
- Start date: 2025-03-07
- End date: 2025-10-17
- Reward: 10000 USD
Verify the safety of std::Vec functions (library/alloc/src/vec/mod.rs).
Verify the 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 hold for generic type T (no monomorphization).
All proofs must automatically ensure the absence of the following undefined behaviors ref:
- 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 in addition to the ones listed above.