File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 44- ** Tracking Issue:** [ #286 ] ( https://github.com/model-checking/verify-rust-std/issues/286 )
55- ** Start date:** * 2025-03-07*
66- ** End date:** * 2025-10-17*
7- - ** Reward:** * 5000 USD*
7+ - ** Reward:** * 10000 USD*
88
99-------------------
1010
@@ -16,7 +16,9 @@ Verify the safety of `VecDeque` functions in (library/alloc/src/collections/vec_
1616
1717### Success Criteria
1818
19- Verify the safety of the following functions in (library/alloc/src/collections/vec_deque/mod.rs).
19+ Verify the safety of the following functions in (library/alloc/src/collections/vec_deque/mod.rs):
20+
21+ Write and prove the contract for the safety of the following unsafe functions:
2022
2123| Function |
2224| ---------|
@@ -28,22 +30,28 @@ Verify the safety of the following functions in (library/alloc/src/collections/v
2830| copy_nonoverlapping|
2931| wrap_copy|
3032| copy_slice|
33+ | write_iter|
34+ | write_iter_wrapping|
3135| handle_capacity_increase|
3236| from_contiguous_raw_parts_in|
37+ | abort_shrink|
38+
39+ Prove the absence of undefined behavior for following safe abstractions:
40+
3341| get|
3442| get_mut|
3543| swap|
36- | capacity|
3744| reserve_exact|
3845| reserve|
3946| try_reserve_exact|
4047| try_reserve|
4148| shrink_to|
42- | abort_shrink |
49+ | truncate |
4350| as_slices|
4451| as_mut_slices|
4552| range|
4653| range_mut|
54+ | drain|
4755| pop_front|
4856| pop_back|
4957| push_front|
@@ -52,7 +60,9 @@ Verify the safety of the following functions in (library/alloc/src/collections/v
5260| remove|
5361| split_off|
5462| append|
63+ | retain_mut|
5564| grow|
65+ | resize_with|
5666| make_contiguous|
5767| rotate_left|
5868| rotate_right|
You can’t perform that action at this time.
0 commit comments