Skip to content

Latest commit

 

History

History
67 lines (48 loc) · 1.98 KB

0024-vec-pt2.md

File metadata and controls

67 lines (48 loc) · 1.98 KB

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: 10000 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.