Skip to content

Commit d2b6a64

Browse files
thanhnguyen-awscarolynzechtautschnig
authored
Add Challenges 17 18 for slices (#265)
This PR adds: 1. Challenge 17 : for slice functions 2. Chalenge 18: for slice-iter's functions generated by macros By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech <[email protected]> Co-authored-by: Michael Tautschnig <[email protected]>
1 parent b152f68 commit d2b6a64

File tree

3 files changed

+223
-0
lines changed

3 files changed

+223
-0
lines changed

‎doc/src/SUMMARY.md

+2
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,5 @@
2929
- [13: Safety of `CStr`](./challenges/0013-cstr.md)
3030
- [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md)
3131
- [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md)
32+
- [17: Verify the safety of slice functions](./challenges/0017-slice.md)
33+
- [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter-pt1.md)

‎doc/src/challenges/0017-slice.md

+83
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
# Challenge 17: Verify the safety of `slice` functions
2+
3+
- **Status:** Open
4+
- **Tracking Issue:** [#281](https://github.com/model-checking/verify-rust-std/issues/281)
5+
- **Start date:** *2025-03-07*
6+
- **End date:** *2025-10-17*
7+
- **Reward:** *10000 USD*
8+
9+
-------------------
10+
11+
12+
## Goal
13+
14+
Verify the safety of `std::slice` functions in (library/core/src/slice/mod.rs).
15+
16+
17+
### Success Criteria
18+
19+
For the following unsafe functions (in library/core/src/slice/mod.rs):
20+
- Write contracts specifying the safety precondition(s) that the caller must uphold, then
21+
- Verify that if the caller respects those preconditions, the function does not cause undefined behavior.
22+
23+
| Function |
24+
|---------|
25+
|get_unchecked|
26+
|get_unchecked_mut|
27+
|swap_unchecked|
28+
|as_chunks_unchecked|
29+
|as_chunks_unchecked_mut|
30+
|split_at_unchecked|
31+
|split_at_mut_unchecked|
32+
|align_to|
33+
|align_to_mut|
34+
|get_disjoint_unchecked_mut|
35+
36+
Prove that the following safe abstractions (in library/core/src/slice/mod.rs) do not cause undefined behavior:
37+
38+
| Function |
39+
|---------|
40+
|first_chunk|
41+
|first_chunk_mut|
42+
|split_first_chunk|
43+
|split_first_chunk_mut|
44+
|split_last_chunk|
45+
|split_last_chunk_mut|
46+
|last_chunk|
47+
|last_chunk_mut|
48+
|reverse|
49+
|as_chunks|
50+
|as_chunks_mut|
51+
|as_rchunks|
52+
|split_at_checked|
53+
|split_at_mut_checked|
54+
|binary_search_by|
55+
|partition_dedup_by|
56+
|rotate_left|
57+
|rotate_right|
58+
|copy_from_slice|
59+
|copy_within|
60+
|swap_with_slice|
61+
|as_simd|
62+
|as_simd_mut|
63+
|get_disjoint_mut|
64+
|get_disjoint_check_valid|
65+
|as_flattened|
66+
|as_flattened_mut|
67+
68+
The verification must be unbounded---it must hold for slices of arbitrary length.
69+
70+
The verification must hold for generic type `T` (no monomorphization).
71+
72+
### List of UBs
73+
74+
All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
75+
76+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
77+
* Reading from uninitialized memory except for padding or unions.
78+
* Mutating immutable bytes.
79+
* Producing an invalid value
80+
81+
82+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
83+
in addition to the ones listed above.

‎doc/src/challenges/0018-slice-iter.md

+138
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
# Challenge 18: Verify the safety of `slice` iter functions
2+
3+
- **Status:** Open
4+
- **Tracking Issue:** [#282](https://github.com/model-checking/verify-rust-std/issues/282)
5+
- **Start date:** *2025-03-07*
6+
- **End date:** *2025-10-17*
7+
- **Reward:** *10000 USD*
8+
9+
-------------------
10+
11+
12+
## Goal
13+
**Part 1:**
14+
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):
15+
to generate impl for Iter, IterMut, SplitN, SplitNMut, RSplitN, RSplitNMut in (library/core/src/slice/iter.rs):
16+
17+
```
18+
iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, as_ref, {
19+
fn is_sorted_by<F>(self, mut compare: F) -> bool
20+
where
21+
Self: Sized,
22+
F: FnMut(&Self::Item, &Self::Item) -> bool,
23+
{
24+
self.as_slice().is_sorted_by(|a, b| compare(&a, &b))
25+
}
26+
}}
27+
28+
iterator! {struct IterMut -> *mut T, &'a mut T, mut, {mut}, as_mut, {}}
29+
30+
forward_iterator! { SplitN: T, &'a [T] }
31+
forward_iterator! { RSplitN: T, &'a [T] }
32+
forward_iterator! { SplitNMut: T, &'a mut [T] }
33+
forward_iterator! { RSplitNMut: T, &'a mut [T] }
34+
```
35+
36+
**Part 2:**
37+
Verify the safety of Iterator functions of `std::slice` that are defined in (library/core/src/slice/iter.rs).
38+
39+
### Success Criteria
40+
41+
**Part 1:** In (library/core/src/slice/iter/macros.rs)
42+
43+
Prove absence of undefined behaviors of following safe functions that contain unsafe code:
44+
45+
| Function |
46+
|---------|
47+
|make_slice|
48+
|len|
49+
|is_empty|
50+
|next|
51+
|size_hint|
52+
|count|
53+
|nth|
54+
|advance_by|
55+
|last|
56+
|fold|
57+
|for_each|
58+
|position|
59+
|rposition|
60+
|next_back|
61+
|nth_back|
62+
|advance_back_by|
63+
64+
65+
**Part 2:** In (library/core/src/slice/iter.rs)
66+
67+
Write and prove the contract for the safety of the following unsafe functions:
68+
69+
| Function | Impl for |
70+
|---------| ---------|
71+
|__iterator_get_unchecked| Windows|
72+
|__iterator_get_unchecked| Chunks|
73+
|__iterator_get_unchecked| ChunksMut|
74+
|__iterator_get_unchecked| ChunksExact|
75+
|__iterator_get_unchecked| ChunksExact|
76+
|__iterator_get_unchecked| ArrayChunks|
77+
|__iterator_get_unchecked| ArrayChunksMut|
78+
|__iterator_get_unchecked| RChunks|
79+
|__iterator_get_unchecked| RChunksMut|
80+
|__iterator_get_unchecked| RChunksExact|
81+
|__iterator_get_unchecked| RChunksExactMut|
82+
83+
Prove absence of undefined behaviors of following safe functions that contain unsafe code:
84+
85+
| Function | Impl for |
86+
|---------| ---------|
87+
|new| Iter|
88+
|new| IterMut|
89+
|into_slice| IterMut|
90+
|as_mut_slice| IterMut|
91+
|next| Split|
92+
|next_back| Split|
93+
|next_back| Chunks|
94+
|next| ChunksMut|
95+
|nth| ChunksMut|
96+
|next_back| ChunksMut|
97+
|nth_back| ChunksMut|
98+
|new| ChunksExact|
99+
|new| ChunksExactMut|
100+
|next| ChunksExactMut|
101+
|nth| ChunksExactMut|
102+
|next_back| ChunksExactMut|
103+
|nth_back| ChunksExactMut|
104+
|next| ArrayWindows|
105+
|nth| ArrayWindows|
106+
|next_back| ArrayWindows|
107+
|nth_back| ArrayWindows|
108+
|next| RChunks|
109+
|next_back| RChunks|
110+
|next| RChunksMut|
111+
|nth| RChunksMut|
112+
|last| RChunksMut|
113+
|next_back| RChunksMut|
114+
|nth_back| RChunksMut|
115+
|new| RChunksExact|
116+
|new| RChunksExactMut|
117+
|next| RChunksExactMut|
118+
|nth| RChunksExactMut|
119+
|next_back| RChunksExactMut|
120+
|nth_back| RChunksExactMut|
121+
122+
123+
The verification must be unbounded---it must hold for slices of arbitrary length.
124+
125+
The verification must hold for generic type `T` (no monomorphization).
126+
127+
### List of UBs
128+
129+
All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
130+
131+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
132+
* Reading from uninitialized memory except for padding or unions.
133+
* Mutating immutable bytes.
134+
* Producing an invalid value
135+
136+
137+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
138+
in addition to the ones listed above.

0 commit comments

Comments
 (0)