Skip to content

Commit 1a4548f

Browse files
thanhnguyen-awsthanhnguyen-aws
authored
Merge branch 'main' into addvariant
2 parents 99597c1 + 3f4234a commit 1a4548f

File tree

207 files changed

+5147
-3447
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

207 files changed

+5147
-3447
lines changed

‎.github/workflows/verifast-negative.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -42,4 +42,4 @@ jobs:
4242
run: |
4343
export PATH=~/verifast-25.02/bin:$PATH
4444
cd verifast-proofs
45-
mysh check-verifast-proofs-negative.mysh
45+
bash check-verifast-proofs-negative.sh

‎.github/workflows/verifast.yml

+26-1
Original file line numberDiff line numberDiff line change
@@ -39,4 +39,29 @@ jobs:
3939
run: |
4040
export PATH=~/verifast-25.02/bin:$PATH
4141
cd verifast-proofs
42-
mysh check-verifast-proofs.mysh
42+
bash check-verifast-proofs.sh
43+
44+
notify-btj:
45+
name: Notify @btj
46+
runs-on: ubuntu-latest
47+
needs: check-verifast-on-std
48+
if: failure()
49+
permissions:
50+
id-token: write
51+
52+
steps:
53+
- name: Get GitHub OIDC token
54+
id: get_token
55+
uses: actions/github-script@v7
56+
with:
57+
script: |
58+
const audience = 'notify-bart-jacobs';
59+
return await core.getIDToken(audience);
60+
result-encoding: string
61+
62+
- name: Call notification endpoint
63+
run: |
64+
curl -X POST "https://verify-rust-std-verifast-monitor.bart-jacobs.workers.dev/" \
65+
-H "Authorization: Bearer ${{ steps.get_token.outputs.result }}" \
66+
-H "Content-Type: application/json" \
67+
-d '{}'

‎doc/src/SUMMARY.md

+3
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,6 @@
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+
- [16: Verify the safety of Iterator functions](./challenges/0016-iter.md)
33+
- [17: Verify the safety of slice functions](./challenges/0017-slice.md)
34+
- [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter-pt1.md)

‎doc/src/challenges/0016-iter.md

+74
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
# Challenge 16: Verify the safety of Iterator functions
2+
3+
- **Status:** Open
4+
- **Tracking Issue:** [#280](https://github.com/model-checking/verify-rust-std/issues/280)
5+
- **Start date:** *2025-03-07*
6+
- **End date:** *2025-10-17*
7+
- **Reward:** *10,000 USD*
8+
9+
-------------------
10+
11+
12+
## Goal
13+
14+
Verify the safety of iter functions that are defined in (library/core/src/iter/adapters):
15+
16+
17+
18+
### Success Criteria
19+
20+
Write and prove the contract for the safety of the following unsafe functions:
21+
22+
| Function | Defined in |
23+
|---------| ---------|
24+
|__iterator_get_unchecked| clone.rs|
25+
|next_unchecked| clone.rs|
26+
|__iterator_get_unchecked| copied.rs|
27+
|__iterator_get_unchecked| enumerate.rs|
28+
|__iterator_get_unchecked | fuse.rs|
29+
|__iterator_get_unchecked | map.rs|
30+
|next_unchecked | map.rs|
31+
|__iterator_get_unchecked | skip.rs|
32+
|__iterator_get_unchecked | zip.rs|
33+
|get_unchecked| zip.rs|
34+
35+
Prove the absence of undefined behavior for following safe abstractions:
36+
37+
| Function | Defined in |
38+
|---------| ---------|
39+
|next_back_remainder| array_chunks.rs|
40+
|fold| array_chunks.rs|
41+
|spec_next_chunk| copied.rs|
42+
|next_chunk_dropless| filter.rs|
43+
|next_chunk| filter_map.rs|
44+
|as_array_ref | map_windows.rs|
45+
|as_uninit_array_mut | map_windows.rs|
46+
|push | map_windows.rs|
47+
|drop | map_windows.rs|
48+
|original_step | step_by.rs|
49+
|spec_fold| take.rs|
50+
|spec_for_each| take.rs|
51+
|fold| zip.rs|
52+
|next| zip.rs|
53+
|nth| zip.rs|
54+
|next_back| zip.rs|
55+
|spec_fold| zip.rs|
56+
57+
58+
59+
The verification must be unbounded---it must hold for slices of arbitrary length.
60+
61+
The verification must hold for generic type `T` (no monomorphization).
62+
63+
### List of UBs
64+
65+
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):
66+
67+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
68+
* Reading from uninitialized memory except for padding or unions.
69+
* Mutating immutable bytes.
70+
* Producing an invalid value
71+
72+
73+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
74+
in addition to the ones listed above.

‎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)