Skip to content

Latest commit

 

History

History
67 lines (47 loc) · 1.88 KB

0019-rawvec.md

File metadata and controls

67 lines (47 loc) · 1.88 KB

Challenge 25: Verify the safety of RawVec functions

  • Status: Open
  • Tracking Issue: #283
  • 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 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

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:

  • 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.