From 4ab985b1d09a27ec7441746786240c2002586d50 Mon Sep 17 00:00:00 2001 From: Kieran Hulsman Date: Thu, 15 Oct 2026 12:14:06 -0400 Subject: [PATCH 1/2] Propose safety and correctness verification of integer logarithms --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0030-integer-logarithms.md | 62 +++++++++++++++++++ 2 files changed, 63 insertions(+) create mode 100644 doc/src/challenges/0030-integer-logarithms.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index f33ce888233e5..672dacdf348ea 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -46,3 +46,4 @@ - [27: Verify atomically reference-counted Cell implementation](./challenges/0027-arc.md) - [28: Verify float to decimal conversion module](./challenges/0028-flt2dec.md) - [29: Safety of `boxed`](./challenges/0029-boxed.md) + - [30: Safety and Correctness of Integer Logarithms](./challenges/0030-integer-logarithms.md) diff --git a/doc/src/challenges/0030-integer-logarithms.md b/doc/src/challenges/0030-integer-logarithms.md new file mode 100644 index 0000000000000..efd47b15398fc --- /dev/null +++ b/doc/src/challenges/0030-integer-logarithms.md @@ -0,0 +1,62 @@ +# Challenge 30: Safety and Correctness of Integer Logarithms + +- **Status:** Open +- **Solution:** Not yet submitted. +- **Tracking Issue:** [#728](https://github.com/model-checking/verify-rust-std/issues/728) +- **Reward:** TBD + +------------------- + +## Goal + +Verify the safety and correctness of `ilog10`, `ilog2`, and their checked variants in `core::num`. + +## Motivation + +Decimal logarithms make unsafe promises about arithmetic result bounds; binary logarithms +call intrinsics that require nonzero inputs. Violating either requirement is undefined +behavior, even though the public APIs are safe. + +## Description + +| Function | Integer Types | Location | +|---------|---------------|----------| +| `ilog10`, `checked_ilog10`, `ilog2`, `checked_ilog2` | All signed and unsigned integer types | [int_macros.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/int_macros.rs), [uint_macros.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/uint_macros.rs) | +| `NonZero::ilog2` | All unsigned integer types | [nonzero.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/nonzero.rs) | +| `u8_impl`, `u16_impl`, `u32_impl`, `u64_impl`, `u128_impl`, `less_than_5` | Each helper's documented input domain | [int_log10.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/imp/int_log10.rs) | +| Internal wrappers `u8`, `u16`, `u32`, `u64`, `u128`, `usize`, `i8`, `i16`, `i32`, `i64`, `i128` | Corresponding integer types | [int_log10.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/imp/int_log10.rs) | + +- **Signed:** `i8`, `i16`, `i32`, `i64`, `i128`, `isize`. +- **Unsigned:** `u8`, `u16`, `u32`, `u64`, `u128`, `usize`. + +Arbitrary-base `ilog` is excluded: its general calculation contains no direct unsafe +operations, and its unsafe dependencies overlap with the implementations above. + +This extends [Challenge 11](0011-floats-ints.md) to logarithm methods, which are not +in that challenge's target list. NonZero constructor verification belongs to +[Challenge 12](0012-nonzero.md) and is not repeated here. + +### Assumptions + +- Existing verified NonZero contracts and documented layout guarantees may be reused. + +### Success Criteria + +Cover every input to the public methods and each internal helper's documented input domain: + +- Verify the safety conditions of all unsafe operations, including result-bound assertions and nonzero-input requirements. +- For positive input `n`, prove the result is the greatest nonnegative integer `r` with `b^r <= n`, where `b` is 2 or 10 and powers are interpreted mathematically. +- Prove checked methods return `None` for zero or negative inputs, and `ilog2` and `ilog10` panic on those inputs. +- Prove the calculations do not overflow or underflow. +- The proofs must run automatically in the repository's CI without breaking existing verification workflows. + +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): + +- Invoking undefined behavior through compiler intrinsics. +- Reading from uninitialized memory. +- 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 7b08cc25da75b34bd7dfe70b771e242e7f48b758 Mon Sep 17 00:00:00 2001 From: Kieran Hulsman Date: Mon, 2 Nov 2026 21:46:54 -0500 Subject: [PATCH 2/2] Address review feedback on integer logarithm challenge --- doc/src/challenges/0030-integer-logarithms.md | 26 ++++++++++++------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/doc/src/challenges/0030-integer-logarithms.md b/doc/src/challenges/0030-integer-logarithms.md index efd47b15398fc..2671a69855a22 100644 --- a/doc/src/challenges/0030-integer-logarithms.md +++ b/doc/src/challenges/0030-integer-logarithms.md @@ -1,20 +1,24 @@ # Challenge 30: Safety and Correctness of Integer Logarithms -- **Status:** Open -- **Solution:** Not yet submitted. +- **Status:** *Open* +- **Solution:** *Option field to point to the PR that solved this challenge.* - **Tracking Issue:** [#728](https://github.com/model-checking/verify-rust-std/issues/728) -- **Reward:** TBD +- **Start date:** *2026/11/02* +- **Reward:** *TBD* ------------------- ## Goal -Verify the safety and correctness of `ilog10`, `ilog2`, and their checked variants in `core::num`. +Verify the safety and correctness of `ilog10`, `ilog2`, and their checked variants in `core::num`, +including `NonZero::ilog2` and `NonZero::ilog10` for unsigned types and the internal +`int_log10` helpers they rely on. ## Motivation Decimal logarithms make unsafe promises about arithmetic result bounds; binary logarithms -call intrinsics that require nonzero inputs. Violating either requirement is undefined +call intrinsics that require nonzero inputs; the `usize` decimal-logarithm wrapper creates a +`NonZero` value without checking it. Violating any of these requirements is undefined behavior, even though the public APIs are safe. ## Description @@ -22,7 +26,7 @@ behavior, even though the public APIs are safe. | Function | Integer Types | Location | |---------|---------------|----------| | `ilog10`, `checked_ilog10`, `ilog2`, `checked_ilog2` | All signed and unsigned integer types | [int_macros.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/int_macros.rs), [uint_macros.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/uint_macros.rs) | -| `NonZero::ilog2` | All unsigned integer types | [nonzero.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/nonzero.rs) | +| `NonZero::ilog2`, `NonZero::ilog10` | All unsigned integer types | [nonzero.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/nonzero.rs) | | `u8_impl`, `u16_impl`, `u32_impl`, `u64_impl`, `u128_impl`, `less_than_5` | Each helper's documented input domain | [int_log10.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/imp/int_log10.rs) | | Internal wrappers `u8`, `u16`, `u32`, `u64`, `u128`, `usize`, `i8`, `i16`, `i32`, `i64`, `i128` | Corresponding integer types | [int_log10.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/imp/int_log10.rs) | @@ -39,23 +43,25 @@ in that challenge's target list. NonZero constructor verification belongs to ### Assumptions - Existing verified NonZero contracts and documented layout guarantees may be reused. +- The repository's CI runs only 64-bit targets, so proofs need only run on the 64-bit + configuration of pointer-width-dependent code: the `usize` wrapper and the `isize` methods. + For the 16- and 32-bit configurations, it suffices to verify the `u16`/`u32` wrappers that + `usize` selects and the `i16`/`i32` wrappers that `isize` uses, and to argue that the + `NonZero::new_unchecked` conversion in the `usize` wrapper is safe for each pointer width. ### Success Criteria Cover every input to the public methods and each internal helper's documented input domain: -- Verify the safety conditions of all unsafe operations, including result-bound assertions and nonzero-input requirements. +- Verify the safety conditions of all unsafe operations, including result-bound assertions, nonzero-input requirements, and the `NonZero::new_unchecked` conversion in the `usize` wrapper. - For positive input `n`, prove the result is the greatest nonnegative integer `r` with `b^r <= n`, where `b` is 2 or 10 and powers are interpreted mathematically. - Prove checked methods return `None` for zero or negative inputs, and `ilog2` and `ilog10` panic on those inputs. - Prove the calculations do not overflow or underflow. -- The proofs must run automatically in the repository's CI without breaking existing verification workflows. 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): - Invoking undefined behavior through compiler intrinsics. -- Reading from uninitialized memory. -- Mutating immutable bytes. - Producing an invalid value. Note: All solutions to verification challenges need to satisfy the criteria established in the