Challenge 18: Verify the safety of slice iter functions

• Status: Open
• Tracking Issue: #282
• Start date: 2025-03-07
• End date: 2025-10-17
• Reward: 10000 USD

Goal

Part 1: Verify the safety of Iterator functions of std::slice generated by iterator! and forward_iterator! macros that are defined in (library/core/src/slice/iter/macros.rs): to generate impl for Iter, IterMut, SplitN, SplitNMut, RSplitN, RSplitNMut in (library/core/src/slice/iter.rs):

iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, as_ref, {
    fn is_sorted_by<F>(self, mut compare: F) -> bool
    where
        Self: Sized,
        F: FnMut(&Self::Item, &Self::Item) -> bool,
    {
        self.as_slice().is_sorted_by(|a, b| compare(&a, &b))
    }
}}

iterator! {struct IterMut -> *mut T, &'a mut T, mut, {mut}, as_mut, {}}

forward_iterator! { SplitN: T, &'a [T] }
forward_iterator! { RSplitN: T, &'a [T] }
forward_iterator! { SplitNMut: T, &'a mut [T] }
forward_iterator! { RSplitNMut: T, &'a mut [T] }

Part 2: Verify the safety of Iterator functions of std::slice that are defined in (library/core/src/slice/iter.rs).

Success Criteria

Part 1: In (library/core/src/slice/iter/macros.rs)

Prove absence of undefined behaviors of following safe functions that contain unsafe code:

Part 2: In (library/core/src/slice/iter.rs)

Write and prove the contract for the safety of the following unsafe functions:

Prove absence of undefined behaviors of following safe functions that contain unsafe code:

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.