Skip to content

Commit 0825fd1

Browse files
feliperodrifeliperodri
authored
Merge branch 'main' into sync-2025-11-25
2 parents ac081f8 + c69b9b9 commit 0825fd1

File tree

6 files changed

+336
-0
lines changed

6 files changed

+336
-0
lines changed

‎.github/workflows/kani-metrics.yml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ defaults:
1111

1212
jobs:
1313
update-kani-metrics:
14+
permissions:
15+
contents: write
16+
pull-requests: write
1417
if: github.repository == 'model-checking/verify-rust-std'
1518
runs-on: ubuntu-latest
1619

‎.github/workflows/update-subtree.yml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,9 @@ defaults:
1111

1212
jobs:
1313
update-subtree-library:
14+
permissions:
15+
contents: write
16+
pull-requests: write
1417
if: github.repository == 'model-checking/verify-rust-std'
1518
# Changing the host platform may alter the libgit2 version as used by
1619
# splitsh-lite, which will require changing the version of git2go.

‎doc/src/challenges/0028-flt2dec.md‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# Challenge 28: Verify float to decimal conversion module
2+
3+
- **Status:** *Open*
4+
- **Solution:** *Option field to point to the PR that solved this challenge.*
5+
- **Tracking Issue:** [#524](https://github.com/model-checking/verify-rust-std/issues/524)
6+
- **Start date:** *2026/01/01*
7+
- **End date:** *2026/08/31*
8+
- **Reward:** *5,000 USD*
9+
10+
-------------------
11+
12+
13+
## Goal
14+
15+
The goal of this challenge is to verify the [flt2dec](https://doc.rust-lang.org/src/core/num/flt2dec/mod.rs.html) module, which provides functions for converting floating point numbers to decimals. To do this, it implements both the Dragon and Grisu families of algorithms.
16+
17+
## Motivation
18+
19+
Given that converting floats to decimals correctly is a relatively costly operation, the standard library’s flt2dec module employs unsafe code to enable performance-enhancing operations that are otherwise not allowed in safe Rust (e.g., lifetime laundering to get around borrow-checker restrictions). Functions from this module are primarily invoked whenever attempting to represent floats in a human-readable format, making this a potentially highly-used module.
20+
21+
## Description
22+
23+
All of the functions targeted in this challenge are safe functions whose bodies contain unsafe code. This challenge is thus centered around proving well-encapsulation, which here mainly means showing that calls to variants of assume_init() are only performed on fully-initialized structures, and that the lifetime laundering does not cause undefined behaviour.
24+
25+
### Success Criteria
26+
27+
The following functions contain unsafe code in their bodies but are not themselves marked unsafe. All of these should be proven unconditionally safe, or safety contracts should be added:
28+
29+
| Function | Location |
30+
|---------|---------|
31+
| `digits_to_dec_str` | `flt2dec` |
32+
| `digits_to_exp_str` | `flt2dec` |
33+
| `to_shortest_str` | `flt2dec` |
34+
| `to_shortest_exp_str` | `flt2dec` |
35+
| `to_exact_exp_str` | `flt2dec` |
36+
| `to_exact_fixed_str` | `flt2dec` |
37+
| `format_shortest_opt` | `flt2dec::strategy::grisu` |
38+
| `format_shortest` | `flt2dec::strategy::grisu` |
39+
| `format_exact_opt` | `flt2dec::strategy::grisu` |
40+
| `format_exact` | `flt2dec::strategy::grisu` |
41+
| `format_shortest` | `flt2dec::strategy::dragon` |
42+
| `format_exact` | `flt2dec::strategy::dragon` |
43+
44+
For functions taking inputs of generic type 'T', the proofs can be limited to primitive types only.
45+
46+
*List of UBs*
47+
48+
In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
49+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
50+
* Invoking undefined behavior via compiler intrinsics.
51+
* Mutating immutable bytes.
52+
* Producing an invalid value.
53+
54+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
55+
in addition to the ones listed above.

‎doc/src/challenges/0029-boxed.md‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
# Challenge 29: Safety of boxed
2+
3+
- **Status:** *Open*
4+
- **Solution:** *Option field to point to the PR that solved this challenge.*
5+
- **Tracking Issue:** [#526](https://github.com/model-checking/verify-rust-std/issues/526)
6+
- **Start date:** *2026/01/01*
7+
- **End date:** *2026/12/31*
8+
- **Reward:** *15,000 USD*
9+
10+
-------------------
11+
12+
13+
## Goal
14+
15+
The goal of this challenge is to verify the [boxed](https://doc.rust-lang.org/std/boxed/index.html) module, which implements the Box family of types (which includes Box and other related types such as ThinBox). A Box is a type of smart pointer that points to a uniquely-owned heap allocation for arbitrary types.
16+
17+
## Motivation
18+
19+
A Box allows the storage of data on the heap rather than the stack. This has several applications, a common [example](https://doc.rust-lang.org/book/ch15-01-box.html#enabling-recursive-types-with-boxes) being for using dynamically-sized types in contexts requiring an exact size (e.g., recursive types). While this type is useful and diverse in its applications, it also extensively uses unsafe code, meaning it is important to verify that this module is free of undefined behaviour.
20+
21+
### Success Criteria
22+
23+
All the following unsafe functions must be annotated with safety contracts and the contracts have been verified:
24+
25+
| Function | Location |
26+
|---------|---------|
27+
| `Box<mem::MaybeUninit<T>, A>::assume_init` | `alloc::boxed` |
28+
| `Box<[mem::MaybeUninit<T>], A>::assume_init` | `alloc::boxed` |
29+
| `Box<T>::from_raw` | `alloc::boxed` |
30+
| `Box<T>::from_non_null` | `alloc::boxed` |
31+
| `Box<T, A>::from_raw_in` | `alloc::boxed` |
32+
| `Box<T, A>::from_non_null_in` | `alloc::boxed` |
33+
| `<dyn Error>::downcast_unchecked` | `alloc::boxed::convert` |
34+
| `<dyn Error + Send>::downcast_unchecked` | `alloc::boxed::convert` |
35+
| `<dyn Error + Send + Sync>::downcast_unchecked` | `alloc::boxed::convert` |
36+
37+
The following functions contain unsafe code in their bodies but are not themselves marked unsafe. At least 75% of these should be proven unconditionally safe, or safety contracts should be added:
38+
39+
| Function | Location |
40+
|---------|---------|
41+
| `Box<T, A>::new_in` | `alloc::boxed` |
42+
| `Box<T, A>::try_new_in` | `alloc::boxed` |
43+
| `Box<T, A>::try_new_uninit_in` | `alloc::boxed` |
44+
| `Box<T, A>::try_new_zeroed_in` | `alloc::boxed` |
45+
| `Box<T, A>::into_boxed_slice` | `alloc::boxed` |
46+
| `Box<[T]>::new_uninit_slice` | `alloc::boxed` |
47+
| `Box<[T]>::new_zeroed_slice` | `alloc::boxed` |
48+
| `Box<[T]>::try_new_uninit_slice` | `alloc::boxed` |
49+
| `Box<[T]>::try_new_zeroed_slice` | `alloc::boxed` |
50+
| `Box<[T]>::into_array` | `alloc::boxed` |
51+
| `Box<T, A>::new_uninit_slice_in` | `alloc::boxed` |
52+
| `Box<T, A>::new_zeroed_slice_in` | `alloc::boxed` |
53+
| `Box<T, A>::try_new_uninit_slice_in` | `alloc::boxed` |
54+
| `Box<T, A>::try_new_zeroed_slice_in` | `alloc::boxed` |
55+
| `Box<mem::MaybeUninit<T>, A>::write` | `alloc::boxed` |
56+
| `Box<T>::into_non_null` | `alloc::boxed` |
57+
| `Box<T, A>::into_raw_with_allocator` | `alloc::boxed` |
58+
| `Box<T, A>::into_non_null_with_allocator` | `alloc::boxed` |
59+
| `Box<T, A>::into_unique` | `alloc::boxed` |
60+
| `Box<T, A>::leak` | `alloc::boxed` |
61+
| `Box<T, A>::into_pin` | `alloc::boxed` |
62+
| `<Box<T, A> as Drop>::drop` | `alloc::boxed` |
63+
| `<Box<T> as Default>::default` | `alloc::boxed` |
64+
| `<Box<str> as Default>::default` | `alloc::boxed` |
65+
| `<Box<T, A> as Clone>::clone` | `alloc::boxed` |
66+
| `<Box<str> as Clone>::clone` | `alloc::boxed` |
67+
| `<Box<[T]> as BoxFromSlice<T>>::from_slice` | `alloc::boxed::convert` |
68+
| `<Box<str> as From<&str>>::from` | `alloc::boxed::convert` |
69+
| `<Box<[u8], A> as From<Box<str, A>>>::from` | `alloc::boxed::convert` |
70+
| `<Box<[T; N]> as TryFrom<Box<[T]>>>::try_from` | `alloc::boxed::convert` |
71+
| `<Box<[T; N]> as TryFrom<Box<T>>>::try_from` | `alloc::boxed::convert` |
72+
| `Box<dyn Any, A>::downcast` | `alloc::boxed::convert` |
73+
| `Box<dyn Any + Send, A>::downcast` | `alloc::boxed::convert` |
74+
| `Box<dyn Any + Send + Sync, A>::downcast` | `alloc::boxed::convert` |
75+
| `<dyn Error>::downcast` | `alloc::boxed::convert` |
76+
| `<dyn Error + Send>::downcast` | `alloc::boxed::convert` |
77+
| `<dyn Error + Send + Sync>::downcast` | `alloc::boxed::convert` |
78+
| `<ThinBox<T> as Deref>::deref` | `alloc::boxed::thin` |
79+
| `<ThinBox<T> as DerefMut>::deref_mut` | `alloc::boxed::thin` |
80+
| `<ThinBox<T> as Drop>::drop` | `alloc::boxed::thin` |
81+
| `ThinBox<T>::meta` | `alloc::boxed::thin` |
82+
| `ThinBox<T>::with_header` | `alloc::boxed::thin` |
83+
| `WithHeader<H>::new` | `alloc::boxed::thin` |
84+
| `WithHeader<H>::try_new` | `alloc::boxed::thin` |
85+
| `WithHeader<H>::new_unsize_zst` | `alloc::boxed::thin` |
86+
| `WithHeader<H>::header` | `alloc::boxed::thin` |
87+
88+
For functions taking inputs of generic type 'T', the proofs can be limited to primitive types only.
89+
90+
*List of UBs*
91+
92+
In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
93+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
94+
* Invoking undefined behavior via compiler intrinsics.
95+
* Mutating immutable bytes.
96+
* Producing an invalid value.
97+
98+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
99+
in addition to the ones listed above.

‎scripts/kani-std-analysis/metrics-data-core.json‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -930,6 +930,94 @@
930930
"verified_safe_fns_under_contract": 112,
931931
"verified_safe_fns_with_loop_under_contract": 1,
932932
"total_functions_under_contract_all_crates": 424
933+
},
934+
{
935+
"date": "2026-02-08",
936+
"total_unsafe_fns": 7166,
937+
"total_unsafe_fns_with_loop": 22,
938+
"total_safe_abstractions": 1899,
939+
"total_safe_abstractions_with_loop": 90,
940+
"total_safe_fns": 16120,
941+
"total_safe_fns_with_loop": 783,
942+
"unsafe_fns_under_contract": 290,
943+
"unsafe_fns_with_loop_under_contract": 3,
944+
"verified_unsafe_fns_under_contract": 254,
945+
"verified_unsafe_fns_with_loop_under_contract": 1,
946+
"safe_abstractions_under_contract": 77,
947+
"safe_abstractions_with_loop_under_contract": 0,
948+
"verified_safe_abstractions_under_contract": 77,
949+
"verified_safe_abstractions_with_loop_under_contract": 0,
950+
"safe_fns_under_contract": 115,
951+
"safe_fns_with_loop_under_contract": 1,
952+
"verified_safe_fns_under_contract": 112,
953+
"verified_safe_fns_with_loop_under_contract": 1,
954+
"total_functions_under_contract_all_crates": 424
955+
},
956+
{
957+
"date": "2026-02-15",
958+
"total_unsafe_fns": 7166,
959+
"total_unsafe_fns_with_loop": 22,
960+
"total_safe_abstractions": 1899,
961+
"total_safe_abstractions_with_loop": 90,
962+
"total_safe_fns": 16120,
963+
"total_safe_fns_with_loop": 783,
964+
"unsafe_fns_under_contract": 290,
965+
"unsafe_fns_with_loop_under_contract": 3,
966+
"verified_unsafe_fns_under_contract": 254,
967+
"verified_unsafe_fns_with_loop_under_contract": 1,
968+
"safe_abstractions_under_contract": 77,
969+
"safe_abstractions_with_loop_under_contract": 0,
970+
"verified_safe_abstractions_under_contract": 77,
971+
"verified_safe_abstractions_with_loop_under_contract": 0,
972+
"safe_fns_under_contract": 115,
973+
"safe_fns_with_loop_under_contract": 1,
974+
"verified_safe_fns_under_contract": 112,
975+
"verified_safe_fns_with_loop_under_contract": 1,
976+
"total_functions_under_contract_all_crates": 424
977+
},
978+
{
979+
"date": "2026-02-22",
980+
"total_unsafe_fns": 7166,
981+
"total_unsafe_fns_with_loop": 22,
982+
"total_safe_abstractions": 1899,
983+
"total_safe_abstractions_with_loop": 90,
984+
"total_safe_fns": 16120,
985+
"total_safe_fns_with_loop": 783,
986+
"unsafe_fns_under_contract": 290,
987+
"unsafe_fns_with_loop_under_contract": 3,
988+
"verified_unsafe_fns_under_contract": 254,
989+
"verified_unsafe_fns_with_loop_under_contract": 1,
990+
"safe_abstractions_under_contract": 77,
991+
"safe_abstractions_with_loop_under_contract": 0,
992+
"verified_safe_abstractions_under_contract": 77,
993+
"verified_safe_abstractions_with_loop_under_contract": 0,
994+
"safe_fns_under_contract": 115,
995+
"safe_fns_with_loop_under_contract": 1,
996+
"verified_safe_fns_under_contract": 112,
997+
"verified_safe_fns_with_loop_under_contract": 1,
998+
"total_functions_under_contract_all_crates": 424
999+
},
1000+
{
1001+
"date": "2026-03-01",
1002+
"total_unsafe_fns": 7166,
1003+
"total_unsafe_fns_with_loop": 22,
1004+
"total_safe_abstractions": 1899,
1005+
"total_safe_abstractions_with_loop": 90,
1006+
"total_safe_fns": 16120,
1007+
"total_safe_fns_with_loop": 783,
1008+
"unsafe_fns_under_contract": 290,
1009+
"unsafe_fns_with_loop_under_contract": 3,
1010+
"verified_unsafe_fns_under_contract": 254,
1011+
"verified_unsafe_fns_with_loop_under_contract": 1,
1012+
"safe_abstractions_under_contract": 77,
1013+
"safe_abstractions_with_loop_under_contract": 0,
1014+
"verified_safe_abstractions_under_contract": 77,
1015+
"verified_safe_abstractions_with_loop_under_contract": 0,
1016+
"safe_fns_under_contract": 115,
1017+
"safe_fns_with_loop_under_contract": 1,
1018+
"verified_safe_fns_under_contract": 112,
1019+
"verified_safe_fns_with_loop_under_contract": 1,
1020+
"total_functions_under_contract_all_crates": 424
9331021
}
9341022
]
9351023
}

‎scripts/kani-std-analysis/metrics-data-std.json‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -813,6 +813,94 @@
813813
"verified_safe_fns_under_contract": 0,
814814
"verified_safe_fns_with_loop_under_contract": 0,
815815
"total_functions_under_contract_all_crates": 424
816+
},
817+
{
818+
"date": "2026-02-08",
819+
"total_unsafe_fns": 183,
820+
"total_unsafe_fns_with_loop": 12,
821+
"total_safe_abstractions": 517,
822+
"total_safe_abstractions_with_loop": 44,
823+
"total_safe_fns": 4133,
824+
"total_safe_fns_with_loop": 186,
825+
"unsafe_fns_under_contract": 10,
826+
"unsafe_fns_with_loop_under_contract": 1,
827+
"verified_unsafe_fns_under_contract": 7,
828+
"verified_unsafe_fns_with_loop_under_contract": 0,
829+
"safe_abstractions_under_contract": 0,
830+
"safe_abstractions_with_loop_under_contract": 0,
831+
"verified_safe_abstractions_under_contract": 0,
832+
"verified_safe_abstractions_with_loop_under_contract": 0,
833+
"safe_fns_under_contract": 0,
834+
"safe_fns_with_loop_under_contract": 0,
835+
"verified_safe_fns_under_contract": 0,
836+
"verified_safe_fns_with_loop_under_contract": 0,
837+
"total_functions_under_contract_all_crates": 424
838+
},
839+
{
840+
"date": "2026-02-15",
841+
"total_unsafe_fns": 183,
842+
"total_unsafe_fns_with_loop": 12,
843+
"total_safe_abstractions": 517,
844+
"total_safe_abstractions_with_loop": 44,
845+
"total_safe_fns": 4133,
846+
"total_safe_fns_with_loop": 186,
847+
"unsafe_fns_under_contract": 10,
848+
"unsafe_fns_with_loop_under_contract": 1,
849+
"verified_unsafe_fns_under_contract": 7,
850+
"verified_unsafe_fns_with_loop_under_contract": 0,
851+
"safe_abstractions_under_contract": 0,
852+
"safe_abstractions_with_loop_under_contract": 0,
853+
"verified_safe_abstractions_under_contract": 0,
854+
"verified_safe_abstractions_with_loop_under_contract": 0,
855+
"safe_fns_under_contract": 0,
856+
"safe_fns_with_loop_under_contract": 0,
857+
"verified_safe_fns_under_contract": 0,
858+
"verified_safe_fns_with_loop_under_contract": 0,
859+
"total_functions_under_contract_all_crates": 424
860+
},
861+
{
862+
"date": "2026-02-22",
863+
"total_unsafe_fns": 183,
864+
"total_unsafe_fns_with_loop": 12,
865+
"total_safe_abstractions": 517,
866+
"total_safe_abstractions_with_loop": 44,
867+
"total_safe_fns": 4133,
868+
"total_safe_fns_with_loop": 186,
869+
"unsafe_fns_under_contract": 10,
870+
"unsafe_fns_with_loop_under_contract": 1,
871+
"verified_unsafe_fns_under_contract": 7,
872+
"verified_unsafe_fns_with_loop_under_contract": 0,
873+
"safe_abstractions_under_contract": 0,
874+
"safe_abstractions_with_loop_under_contract": 0,
875+
"verified_safe_abstractions_under_contract": 0,
876+
"verified_safe_abstractions_with_loop_under_contract": 0,
877+
"safe_fns_under_contract": 0,
878+
"safe_fns_with_loop_under_contract": 0,
879+
"verified_safe_fns_under_contract": 0,
880+
"verified_safe_fns_with_loop_under_contract": 0,
881+
"total_functions_under_contract_all_crates": 424
882+
},
883+
{
884+
"date": "2026-03-01",
885+
"total_unsafe_fns": 183,
886+
"total_unsafe_fns_with_loop": 12,
887+
"total_safe_abstractions": 517,
888+
"total_safe_abstractions_with_loop": 44,
889+
"total_safe_fns": 4133,
890+
"total_safe_fns_with_loop": 186,
891+
"unsafe_fns_under_contract": 10,
892+
"unsafe_fns_with_loop_under_contract": 1,
893+
"verified_unsafe_fns_under_contract": 7,
894+
"verified_unsafe_fns_with_loop_under_contract": 0,
895+
"safe_abstractions_under_contract": 0,
896+
"safe_abstractions_with_loop_under_contract": 0,
897+
"verified_safe_abstractions_under_contract": 0,
898+
"verified_safe_abstractions_with_loop_under_contract": 0,
899+
"safe_fns_under_contract": 0,
900+
"safe_fns_with_loop_under_contract": 0,
901+
"verified_safe_fns_under_contract": 0,
902+
"verified_safe_fns_with_loop_under_contract": 0,
903+
"total_functions_under_contract_all_crates": 424
816904
}
817905
]
818906
}

0 commit comments

Comments
 (0)