Challenge 24: Verify the safety of Vec functions part 2
- Status: Open
- Tracking Issue: #285
- Start date: 2025/03/07
- End date: 2025/10/17
- Reward: 15000 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/).
Success Criteria
Verify the safety of the following functions that in implemented 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 hold for generic type T (no monomorphization).
List of UBs
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.