From 68d06eaa31f39e54ef05b0ad8cb23a0015a41f2c Mon Sep 17 00:00:00 2001 From: Alex Le Blanc Date: Thu, 8 Jan 2026 17:10:01 -0500 Subject: [PATCH 1/4] challenge 28 text --- doc/src/challenges/0028-flt2dec.md | 53 ++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 doc/src/challenges/0028-flt2dec.md diff --git a/doc/src/challenges/0028-flt2dec.md b/doc/src/challenges/0028-flt2dec.md new file mode 100644 index 0000000000000..c0e02a0041630 --- /dev/null +++ b/doc/src/challenges/0028-flt2dec.md @@ -0,0 +1,53 @@ +# Challenge 28: Verify float to decimal conversion module + +- **Status:** *Open* +- **Solution:** *Option field to point to the PR that solved this challenge.* +- **Tracking Issue:** *Link to issue* +- **Start date:** *2026/01/01* +- **End date:** *2026/08/31* +- **Reward:** *5,000 USD* + +------------------- + + +## Goal + +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. + +## Motivation + +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. + +## Description + +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. + +### Success Criteria + +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: + +| Function | Defined in | +|---------|---------| +| `digits_to_dec_str` | `mod.rs` | +| `digits_to_exp_str` | `mod.rs` | +| `to_shortest_str` | `mod.rs` | +| `to_shortest_exp_str` | `mod.rs` | +| `to_exact_exp_str` | `mod.rs` | +| `to_exact_fixed_str` | `mod.rs` | +| `format_shortest_opt` | `strategy/grisu.rs` | +| `format_shortest` | `strategy/grisu.rs` | +| `format_exact_opt` | `strategy/grisu.rs` | +| `format_exact` | `strategy/grisu.rs` | +| `format_shortest` | `strategy/dragon.rs` | +| `format_exact` | `strategy/dragon.rs` | + +For functions taking inputs of generic type 'T', the proofs can be limited to primitive types only. + +*List of UBs* + +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): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Invoking undefined behavior via compiler intrinsics. +* Mutating immutable bytes. +* Producing an invalid value. From 2640cd5fedf7b37aaac6af6a2b41adf8e7a57f69 Mon Sep 17 00:00:00 2001 From: Alex Le Blanc Date: Thu, 8 Jan 2026 17:20:43 -0500 Subject: [PATCH 2/4] small edit Added note about verification challenge criteria. --- doc/src/challenges/0028-flt2dec.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/src/challenges/0028-flt2dec.md b/doc/src/challenges/0028-flt2dec.md index c0e02a0041630..57cdd37bfa812 100644 --- a/doc/src/challenges/0028-flt2dec.md +++ b/doc/src/challenges/0028-flt2dec.md @@ -46,8 +46,10 @@ For functions taking inputs of generic type 'T', the proofs can be limited to pr *List of UBs* 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): - * Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. * Invoking undefined behavior via compiler intrinsics. * Mutating immutable bytes. * Producing an invalid value. + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. From 57dc8e76fdcc07ce9b2f9e751a12b4e791187c43 Mon Sep 17 00:00:00 2001 From: Alex Le Blanc Date: Fri, 9 Jan 2026 13:52:30 -0500 Subject: [PATCH 3/4] added module paths --- doc/src/challenges/0028-flt2dec.md | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/doc/src/challenges/0028-flt2dec.md b/doc/src/challenges/0028-flt2dec.md index 57cdd37bfa812..f8577b990068a 100644 --- a/doc/src/challenges/0028-flt2dec.md +++ b/doc/src/challenges/0028-flt2dec.md @@ -26,20 +26,20 @@ All of the functions targeted in this challenge are safe functions whose bodies 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: -| Function | Defined in | +| Function | Location | |---------|---------| -| `digits_to_dec_str` | `mod.rs` | -| `digits_to_exp_str` | `mod.rs` | -| `to_shortest_str` | `mod.rs` | -| `to_shortest_exp_str` | `mod.rs` | -| `to_exact_exp_str` | `mod.rs` | -| `to_exact_fixed_str` | `mod.rs` | -| `format_shortest_opt` | `strategy/grisu.rs` | -| `format_shortest` | `strategy/grisu.rs` | -| `format_exact_opt` | `strategy/grisu.rs` | -| `format_exact` | `strategy/grisu.rs` | -| `format_shortest` | `strategy/dragon.rs` | -| `format_exact` | `strategy/dragon.rs` | +| `digits_to_dec_str` | `flt2dec` | +| `digits_to_exp_str` | `flt2dec` | +| `to_shortest_str` | `flt2dec` | +| `to_shortest_exp_str` | `flt2dec` | +| `to_exact_exp_str` | `flt2dec` | +| `to_exact_fixed_str` | `flt2dec` | +| `format_shortest_opt` | `flt2dec::strategy::grisu` | +| `format_shortest` | `flt2dec::strategy::grisu` | +| `format_exact_opt` | `flt2dec::strategy::grisu` | +| `format_exact` | `flt2dec::strategy::grisu` | +| `format_shortest` | `flt2dec::strategy::dragon` | +| `format_exact` | `flt2dec::strategy::dragon` | For functions taking inputs of generic type 'T', the proofs can be limited to primitive types only. From dca0fe55d0a4b70481e3cb3baae282d017bbb950 Mon Sep 17 00:00:00 2001 From: Alex Le Blanc Date: Mon, 12 Jan 2026 10:59:33 -0500 Subject: [PATCH 4/4] Update tracking issue link for Challenge 28 --- doc/src/challenges/0028-flt2dec.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0028-flt2dec.md b/doc/src/challenges/0028-flt2dec.md index f8577b990068a..a5a52a25b503d 100644 --- a/doc/src/challenges/0028-flt2dec.md +++ b/doc/src/challenges/0028-flt2dec.md @@ -2,7 +2,7 @@ - **Status:** *Open* - **Solution:** *Option field to point to the PR that solved this challenge.* -- **Tracking Issue:** *Link to issue* +- **Tracking Issue:** [#524](https://github.com/model-checking/verify-rust-std/issues/524) - **Start date:** *2026/01/01* - **End date:** *2026/08/31* - **Reward:** *5,000 USD*