Repository navigation
New challenge: Safety and correctness of integer logarithms - #729
Kieran-Hulsman wants to merge 2 commits into
Conversation
|
The macOS Kani Metrics failure matches model-checking/kani#4963, fixed by model-checking/kani#4964. The Kani pin update is included in #727. I’ll update this branch once that lands and rerun CI. |
feliperodri
added
the
Challenge Proposal
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
This is a well-scoped challenge: the target code has real unsafe obligations (assert_unchecked result bounds in int_log10, intrinsics::ctlz_nonzero in signed checked_ilog2, NonZero::new_unchecked in the usize wrapper), none of it is covered by an existing challenge or harness, and the success criteria are concrete and checkable. The exclusion of arbitrary-base ilog is argued, and the helpers' input domains are documented in the source, so "each helper's documented input domain" is well defined.
I checked feasibility before reviewing the criteria. With Kani 0.68.0, proving the full correctness criterion (b^r <= n < b^(r+1), None for non-positive inputs) over every input takes 1 s for u128/i128 checked_ilog2, 2 s for u64 checked_ilog10, and 18–19 s for u128/i128 checked_ilog10. So no bounds are needed and the CI cost is small. I ran this on the public methods with Kani's bundled std, not as contracts on the internal helpers in this repo.
Three things block approval (inline comments): NonZero::ilog10 is missing from the target list, the challenge number 30 is also used by #592, and the template's Start date field is missing. The other comments are suggestions.
What would flip this to approval:
- Add
NonZero<T>::ilog10to the target table. - Renumber if #592 merges first (file name, title and
SUMMARY.md). - Add the
Start datefield.
The usize width question and the UB-list trim are worth doing but don't block.
| @@ -0,0 +1,62 @@ | |||
| # Challenge 30: Safety and Correctness of Integer Logarithms | |||
There was a problem hiding this comment.
Bug: #592 ("Progress Public MIR") also adds doc/src/challenges/0030-progress-public-mir.md, and #595 uses 31. The template numbers challenges by publication date, so whichever merges second needs renumbering. If this one goes second, please update the file name, the title and the SUMMARY.md entry to the next free number.
| - **Status:** Open | ||
| - **Solution:** Not yet submitted. | ||
| - **Tracking Issue:** [#728](https://github.com/model-checking/verify-rust-std/issues/728) | ||
| - **Reward:** TBD |
There was a problem hiding this comment.
Bug: the template has a - **Start date:** YYYY/MM/DD field between Tracking Issue and Reward, and it's missing here.
| | 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<T>::ilog2` | All unsigned integer types | [nonzero.rs](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/nonzero.rs) | |
There was a problem hiding this comment.
Bug: NonZero<T>::ilog10 (nonzero.rs:2152) isn't listed, and it's the public entry point to the main unsafe obligation: it calls int_log10::$Int, which holds the assert_unchecked result bound, and unsigned checked_ilog10 goes through it. The internal wrappers are listed, so the code would be covered, but a solution could reasonably leave the public NonZero::ilog10 without a proof. Please add it to this row.
|
|
||
| ## Goal | ||
|
|
||
| Verify the safety and correctness of `ilog10`, `ilog2`, and their checked variants in `core::num`. |
There was a problem hiding this comment.
Nit: the goal mentions ilog10, ilog2 and their checked variants, but the table also covers NonZero methods and the internal helpers. Mentioning them here would make the scope clear from the first sentence.
| | `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<T>::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) | |
There was a problem hiding this comment.
Question: the usize wrapper picks its helper with #[cfg(target_pointer_width = "16" | "32" | "64")], and CI only runs 64-bit targets, so the 16- and 32-bit branches can't be verified there. Is it enough to verify the 64-bit configuration, or should solutions also cover the other widths (for example by verifying the u16/u32 helpers they select, and arguing the new_unchecked cast is safe for each width)? Stating this in the Assumptions avoids a dispute at review time.
| 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. |
There was a problem hiding this comment.
Praise: this is precise and directly checkable: "greatest r with b^r <= n, powers interpreted mathematically" rules out solutions that only check bounds, and it avoids the overflow trap for 10^(r+1) at the top of the range.
| - Invoking undefined behavior through compiler intrinsics. | ||
| - Reading from uninitialized memory. | ||
| - Mutating immutable bytes. | ||
| - Producing an invalid value. |
There was a problem hiding this comment.
Suggestion: this code has no pointers or memory accesses, so "reading from uninitialized memory" and "mutating immutable bytes" can't arise, and listing them invites the open question in #733 about how Kani-based solutions are judged on those items. The ones that apply are "invoking undefined behavior through compiler intrinsics" (ctlz_nonzero, assert_unchecked) and "producing an invalid value" (NonZero::new_unchecked in the usize wrapper). I'd keep only those two.
| - 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. |
There was a problem hiding this comment.
FYI: the full-input proofs above take under 20 s per harness, so this criterion is easy to meet with Kani. Solutions will likely be per-type harnesses or contracts on the helpers, both of which fit the existing CI partitions.
|
@patricklam could you take a look at this proposal as well? |
|
@feliperodri I should declare a conflict of interest on reviewing this; Kieran is working with me. |
Proposes a challenge to verify the safety and correctness of
ilog10,ilog2, their checked variants, and unsignedNonZero::ilog2, including the internal decimal-logarithm calculations and unsafe assertions.Adds the challenge document and its book entry.
Tracking issue: #728
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.