From fee9360da78e952c1aeff95f395ecac5fe43469e Mon Sep 17 00:00:00 2001 From: v3risec Date: Sat, 7 Nov 2026 23:49:13 +0800 Subject: [PATCH 1/3] Verify integer logarithms with Kani --- library/core/src/num/imp/int_log10.rs | 152 ++++++++++++++++++++++++++ library/core/src/num/int_macros.rs | 63 +++++++++++ library/core/src/num/nonzero.rs | 30 +++++ library/core/src/num/uint_macros.rs | 63 +++++++++++ 4 files changed, 308 insertions(+) diff --git a/library/core/src/num/imp/int_log10.rs b/library/core/src/num/imp/int_log10.rs index 1da029c6a21c4..64ae76198d94f 100644 --- a/library/core/src/num/imp/int_log10.rs +++ b/library/core/src/num/imp/int_log10.rs @@ -1,10 +1,16 @@ //! These functions compute the integer logarithm of their type, assuming //! that someone has already checked that the value is strictly positive. +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; use crate::num::NonZero; // 0 < val <= u8::MAX #[inline] +#[requires(val > 0)] +#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] const fn u8_impl(val: u8) -> u32 { let val = val as u32; @@ -26,6 +32,8 @@ const fn u8_impl(val: u8) -> u32 { // 0 < val < 100_000 #[inline] +#[requires(val > 0 && val < 100_000)] +#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] const fn less_than_5(val: u32) -> u32 { // Similar to u8, when adding one of these constants to val, // we get two possible bit patterns above the low 17 bits, @@ -47,12 +55,16 @@ const fn less_than_5(val: u32) -> u32 { // 0 < val <= u16::MAX #[inline] +#[requires(val > 0)] +#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] const fn u16_impl(val: u16) -> u32 { less_than_5(val as u32) } // 0 < val <= u32::MAX #[inline] +#[requires(val > 0)] +#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] const fn u32_impl(mut val: u32) -> u32 { let mut log = 0; if val >= 100_000 { @@ -64,6 +76,8 @@ const fn u32_impl(mut val: u32) -> u32 { // 0 < val <= u64::MAX #[inline] +#[requires(val > 0)] +#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] const fn u64_impl(mut val: u64) -> u32 { let mut log = 0; if val >= 10_000_000_000 { @@ -79,6 +93,8 @@ const fn u64_impl(mut val: u64) -> u32 { // 0 < val <= u128::MAX #[inline] +#[requires(val > 0)] +#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] const fn u128_impl(mut val: u128) -> u32 { let mut log = 0; if val >= 100_000_000_000_000_000_000_000_000_000_000 { @@ -96,6 +112,7 @@ const fn u128_impl(mut val: u128) -> u32 { macro_rules! define_unsigned_ilog10 { ($($ty:ident => $impl_fn:ident,)*) => {$( #[inline] + #[ensures(|result: &u32| verify::log10_correct(val.get() as u128, *result))] pub(in crate::num) const fn $ty(val: NonZero<$ty>) -> u32 { let result = $impl_fn(val.get()); @@ -117,6 +134,7 @@ define_unsigned_ilog10! { } #[inline] +#[ensures(|result: &u32| verify::log10_correct(val.get() as u128, *result))] pub(in crate::num) const fn usize(val: NonZero) -> u32 { #[cfg(target_pointer_width = "16")] let impl_fn = u16; @@ -136,6 +154,10 @@ macro_rules! define_signed_ilog10 { ($($ty:ident => $impl_fn:ident,)*) => {$( // 0 < val <= $ty::MAX #[inline] + #[ensures(|result: &Option| match result { + Some(log) => val > 0 && verify::log10_correct(val as u128, *log), + None => val <= 0, + })] pub(in crate::num) const fn $ty(val: $ty) -> Option { if val > 0 { let result = $impl_fn(val.cast_unsigned()); @@ -169,3 +191,133 @@ define_signed_ilog10! { pub(in crate::num) const fn panic_for_nonpositive_argument() -> ! { panic!("argument of integer logarithm must be positive") } + +#[unstable(feature = "kani", issue = "none")] +#[cfg(kani)] +mod verify { + use crate::kani; + use crate::num::NonZero; + + // For r < 128, this is exactly 2^r <= n < 2^(r+1), including r = 127. + pub(crate) const fn log2_correct(n: u128, r: u32) -> bool { + r < 128 && n >> r == 1 + } + + // All representable powers of ten. 10^39 exceeds u128::MAX, so the last + // interval has no representable upper bound. The oracle does not call ilog. + const POWERS_OF_TEN: [u128; 39] = [ + 1, + 10, + 100, + 1_000, + 10_000, + 100_000, + 1_000_000, + 10_000_000, + 100_000_000, + 1_000_000_000, + 10_000_000_000, + 100_000_000_000, + 1_000_000_000_000, + 10_000_000_000_000, + 100_000_000_000_000, + 1_000_000_000_000_000, + 10_000_000_000_000_000, + 100_000_000_000_000_000, + 1_000_000_000_000_000_000, + 10_000_000_000_000_000_000, + 100_000_000_000_000_000_000, + 1_000_000_000_000_000_000_000, + 10_000_000_000_000_000_000_000, + 100_000_000_000_000_000_000_000, + 1_000_000_000_000_000_000_000_000, + 10_000_000_000_000_000_000_000_000, + 100_000_000_000_000_000_000_000_000, + 1_000_000_000_000_000_000_000_000_000, + 10_000_000_000_000_000_000_000_000_000, + 100_000_000_000_000_000_000_000_000_000, + 1_000_000_000_000_000_000_000_000_000_000, + 10_000_000_000_000_000_000_000_000_000_000, + 100_000_000_000_000_000_000_000_000_000_000, + 1_000_000_000_000_000_000_000_000_000_000_000, + 10_000_000_000_000_000_000_000_000_000_000_000, + 100_000_000_000_000_000_000_000_000_000_000_000, + 1_000_000_000_000_000_000_000_000_000_000_000_000, + 10_000_000_000_000_000_000_000_000_000_000_000_000, + 100_000_000_000_000_000_000_000_000_000_000_000_000, + ]; + + pub(crate) const fn log10_correct(n: u128, r: u32) -> bool { + r < 39 && POWERS_OF_TEN[r as usize] <= n && (r == 38 || n < POWERS_OF_TEN[(r + 1) as usize]) + } + + // should_panic alone only witnesses a panic for some input. A safety-check + // failure is not accepted as an expected panic, so any normal return fails + // the harness. This checks every nonpositive input without stubbing code. + pub(crate) fn reject_normal_return() { + kani::safety_check(false, "a nonpositive logarithm must not return"); + } + + macro_rules! check_integer_logarithm { + ($int:ty, $method:ident, $harness:ident) => { + #[kani::proof_for_contract($int::$method)] + fn $harness() { + let n: $int = kani::any(); + let _ = n.$method(); + kani::cover(true, "checked logarithm returns"); + } + }; + ($int:ty, $method:ident, $harness:ident, positive) => { + #[kani::proof_for_contract($int::$method)] + fn $harness() { + let n: $int = kani::any(); + if n > 0 { + let _ = n.$method(); + kani::cover(true, "positive logarithm returns"); + } + } + }; + ($int:ty, $method:ident, $harness:ident, panic) => { + #[kani::proof] + #[kani::should_panic] + fn $harness() { + let n: $int = kani::any(); + kani::assume(n <= 0); + kani::cover(true, "nonpositive input is reachable"); + let _ = n.$method(); + crate::num::imp::int_log10::verify::reject_normal_return(); + } + }; + } + pub(crate) use check_integer_logarithm; + + macro_rules! check_internal_contracts { + ($($target:ident: $arg:ty),+ $(,)?) => {$( + #[kani::proof_for_contract(crate::num::imp::int_log10::$target)] + fn $target() { + let n: $arg = kani::any(); + let _ = crate::num::imp::int_log10::$target(n); + kani::cover(true, "internal logarithm contract returns"); + } + )+}; + } + check_internal_contracts! { + u8_impl: u8, + u16_impl: u16, + u32_impl: u32, + u64_impl: u64, + u128_impl: u128, + less_than_5: u32, + u8: NonZero, + u16: NonZero, + u32: NonZero, + u64: NonZero, + u128: NonZero, + usize: NonZero, + i8: i8, + i16: i16, + i32: i32, + i64: i64, + i128: i128, + } +} diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 5ded53fbce0fd..2406ee3eeccc4 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -3514,6 +3514,9 @@ macro_rules! int_impl { without modifying the original"] #[inline] #[track_caller] + #[ensures(|result: &u32| { + self > 0 && imp::int_log10::verify::log2_correct(self as u128, *result) + })] pub const fn ilog2(self) -> u32 { if let Some(log) = self.checked_ilog2() { log @@ -3539,6 +3542,9 @@ macro_rules! int_impl { without modifying the original"] #[inline] #[track_caller] + #[ensures(|result: &u32| { + self > 0 && imp::int_log10::verify::log10_correct(self as u128, *result) + })] pub const fn ilog10(self) -> u32 { if let Some(log) = self.checked_ilog10() { log @@ -3593,6 +3599,10 @@ macro_rules! int_impl { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|result: &Option| match result { + Some(log) => self > 0 && imp::int_log10::verify::log2_correct(self as u128, *log), + None => self <= 0, + })] pub const fn checked_ilog2(self) -> Option { if self <= 0 { None @@ -3617,6 +3627,10 @@ macro_rules! int_impl { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|result: &Option| match result { + Some(log) => self > 0 && imp::int_log10::verify::log10_correct(self as u128, *log), + None => self <= 0, + })] pub const fn checked_ilog10(self) -> Option { imp::int_log10::$ActualT(self as $ActualT) } @@ -4196,3 +4210,52 @@ macro_rules! int_impl { } } } + +#[unstable(feature = "kani", issue = "none")] +#[cfg(kani)] +mod verify { + use crate::kani; + use crate::num::imp::int_log10::verify::check_integer_logarithm; + + check_integer_logarithm!(i8, checked_ilog2, checked_ilog2_i8); + check_integer_logarithm!(i8, checked_ilog10, checked_ilog10_i8); + check_integer_logarithm!(i8, ilog2, ilog2_i8, positive); + check_integer_logarithm!(i8, ilog10, ilog10_i8, positive); + check_integer_logarithm!(i8, ilog2, ilog2_i8_nonpositive, panic); + check_integer_logarithm!(i8, ilog10, ilog10_i8_nonpositive, panic); + + check_integer_logarithm!(i16, checked_ilog2, checked_ilog2_i16); + check_integer_logarithm!(i16, checked_ilog10, checked_ilog10_i16); + check_integer_logarithm!(i16, ilog2, ilog2_i16, positive); + check_integer_logarithm!(i16, ilog10, ilog10_i16, positive); + check_integer_logarithm!(i16, ilog2, ilog2_i16_nonpositive, panic); + check_integer_logarithm!(i16, ilog10, ilog10_i16_nonpositive, panic); + + check_integer_logarithm!(i32, checked_ilog2, checked_ilog2_i32); + check_integer_logarithm!(i32, checked_ilog10, checked_ilog10_i32); + check_integer_logarithm!(i32, ilog2, ilog2_i32, positive); + check_integer_logarithm!(i32, ilog10, ilog10_i32, positive); + check_integer_logarithm!(i32, ilog2, ilog2_i32_nonpositive, panic); + check_integer_logarithm!(i32, ilog10, ilog10_i32_nonpositive, panic); + + check_integer_logarithm!(i64, checked_ilog2, checked_ilog2_i64); + check_integer_logarithm!(i64, checked_ilog10, checked_ilog10_i64); + check_integer_logarithm!(i64, ilog2, ilog2_i64, positive); + check_integer_logarithm!(i64, ilog10, ilog10_i64, positive); + check_integer_logarithm!(i64, ilog2, ilog2_i64_nonpositive, panic); + check_integer_logarithm!(i64, ilog10, ilog10_i64_nonpositive, panic); + + check_integer_logarithm!(i128, checked_ilog2, checked_ilog2_i128); + check_integer_logarithm!(i128, checked_ilog10, checked_ilog10_i128); + check_integer_logarithm!(i128, ilog2, ilog2_i128, positive); + check_integer_logarithm!(i128, ilog10, ilog10_i128, positive); + check_integer_logarithm!(i128, ilog2, ilog2_i128_nonpositive, panic); + check_integer_logarithm!(i128, ilog10, ilog10_i128_nonpositive, panic); + + check_integer_logarithm!(isize, checked_ilog2, checked_ilog2_isize); + check_integer_logarithm!(isize, checked_ilog10, checked_ilog10_isize); + check_integer_logarithm!(isize, ilog2, ilog2_isize, positive); + check_integer_logarithm!(isize, ilog10, ilog10_isize, positive); + check_integer_logarithm!(isize, ilog2, ilog2_isize_nonpositive, panic); + check_integer_logarithm!(isize, ilog10, ilog10_isize_nonpositive, panic); +} diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index d63805e401973..1b61bbb4d4f0c 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2120,6 +2120,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|result: &u32| imp::int_log10::verify::log2_correct(self.get() as u128, *result))] pub const fn ilog2(self) -> u32 { Self::BITS - 1 - self.leading_zeros() } @@ -2149,6 +2150,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|result: &u32| imp::int_log10::verify::log10_correct(self.get() as u128, *result))] pub const fn ilog10(self) -> u32 { imp::int_log10::$Int(self) } @@ -5231,4 +5233,32 @@ mod verify { u128::MAX - 0xFFFFu128, u128::MAX ); + + mod logarithms { + use crate::kani; + use crate::num::NonZero; + + macro_rules! check_logarithms { + ($($int:ident),+ $(,)?) => {$( + mod $int { + use super::*; + + #[kani::proof_for_contract(NonZero::::ilog2)] + fn ilog2() { + let n: NonZero = kani::any(); + let _ = n.ilog2(); + kani::cover(true, "nonzero logarithm returns"); + } + + #[kani::proof_for_contract(NonZero::::ilog10)] + fn ilog10() { + let n: NonZero = kani::any(); + let _ = n.ilog10(); + kani::cover(true, "nonzero logarithm returns"); + } + } + )+}; + } + check_logarithms!(u8, u16, u32, u64, u128, usize); + } } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index ac72f1142c3d5..adb85e430f41b 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -1834,6 +1834,9 @@ macro_rules! uint_impl { without modifying the original"] #[inline] #[track_caller] + #[ensures(|result: &u32| { + self > 0 && imp::int_log10::verify::log2_correct(self as u128, *result) + })] pub const fn ilog2(self) -> u32 { if let Some(log) = self.checked_ilog2() { log @@ -1859,6 +1862,9 @@ macro_rules! uint_impl { without modifying the original"] #[inline] #[track_caller] + #[ensures(|result: &u32| { + self > 0 && imp::int_log10::verify::log10_correct(self as u128, *result) + })] pub const fn ilog10(self) -> u32 { if let Some(log) = self.checked_ilog10() { log @@ -1957,6 +1963,10 @@ macro_rules! uint_impl { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|result: &Option| match result { + Some(log) => self > 0 && imp::int_log10::verify::log2_correct(self as u128, *log), + None => self == 0, + })] pub const fn checked_ilog2(self) -> Option { match NonZero::new(self) { Some(x) => Some(x.ilog2()), @@ -1978,6 +1988,10 @@ macro_rules! uint_impl { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|result: &Option| match result { + Some(log) => self > 0 && imp::int_log10::verify::log10_correct(self as u128, *log), + None => self == 0, + })] pub const fn checked_ilog10(self) -> Option { match NonZero::new(self) { Some(x) => Some(x.ilog10()), @@ -4412,3 +4426,52 @@ macro_rules! uint_impl { } } } + +#[unstable(feature = "kani", issue = "none")] +#[cfg(kani)] +mod verify { + use crate::kani; + use crate::num::imp::int_log10::verify::check_integer_logarithm; + + check_integer_logarithm!(u8, checked_ilog2, checked_ilog2_u8); + check_integer_logarithm!(u8, checked_ilog10, checked_ilog10_u8); + check_integer_logarithm!(u8, ilog2, ilog2_u8, positive); + check_integer_logarithm!(u8, ilog10, ilog10_u8, positive); + check_integer_logarithm!(u8, ilog2, ilog2_u8_nonpositive, panic); + check_integer_logarithm!(u8, ilog10, ilog10_u8_nonpositive, panic); + + check_integer_logarithm!(u16, checked_ilog2, checked_ilog2_u16); + check_integer_logarithm!(u16, checked_ilog10, checked_ilog10_u16); + check_integer_logarithm!(u16, ilog2, ilog2_u16, positive); + check_integer_logarithm!(u16, ilog10, ilog10_u16, positive); + check_integer_logarithm!(u16, ilog2, ilog2_u16_nonpositive, panic); + check_integer_logarithm!(u16, ilog10, ilog10_u16_nonpositive, panic); + + check_integer_logarithm!(u32, checked_ilog2, checked_ilog2_u32); + check_integer_logarithm!(u32, checked_ilog10, checked_ilog10_u32); + check_integer_logarithm!(u32, ilog2, ilog2_u32, positive); + check_integer_logarithm!(u32, ilog10, ilog10_u32, positive); + check_integer_logarithm!(u32, ilog2, ilog2_u32_nonpositive, panic); + check_integer_logarithm!(u32, ilog10, ilog10_u32_nonpositive, panic); + + check_integer_logarithm!(u64, checked_ilog2, checked_ilog2_u64); + check_integer_logarithm!(u64, checked_ilog10, checked_ilog10_u64); + check_integer_logarithm!(u64, ilog2, ilog2_u64, positive); + check_integer_logarithm!(u64, ilog10, ilog10_u64, positive); + check_integer_logarithm!(u64, ilog2, ilog2_u64_nonpositive, panic); + check_integer_logarithm!(u64, ilog10, ilog10_u64_nonpositive, panic); + + check_integer_logarithm!(u128, checked_ilog2, checked_ilog2_u128); + check_integer_logarithm!(u128, checked_ilog10, checked_ilog10_u128); + check_integer_logarithm!(u128, ilog2, ilog2_u128, positive); + check_integer_logarithm!(u128, ilog10, ilog10_u128, positive); + check_integer_logarithm!(u128, ilog2, ilog2_u128_nonpositive, panic); + check_integer_logarithm!(u128, ilog10, ilog10_u128_nonpositive, panic); + + check_integer_logarithm!(usize, checked_ilog2, checked_ilog2_usize); + check_integer_logarithm!(usize, checked_ilog10, checked_ilog10_usize); + check_integer_logarithm!(usize, ilog2, ilog2_usize, positive); + check_integer_logarithm!(usize, ilog10, ilog10_usize, positive); + check_integer_logarithm!(usize, ilog2, ilog2_usize_nonpositive, panic); + check_integer_logarithm!(usize, ilog10, ilog10_usize_nonpositive, panic); +} From ab5a67195e3dccccc0d7d900745a0a13afa2fa4c Mon Sep 17 00:00:00 2001 From: v3risec Date: Sun, 8 Nov 2026 17:06:14 +0800 Subject: [PATCH 2/3] Fix Challenge 30 harness visibility and organization --- library/core/src/num/imp/int_log10.rs | 4 +-- library/core/src/num/int_macros.rs | 4 +-- library/core/src/num/nonzero.rs | 51 ++++++++++++--------------- library/core/src/num/uint_macros.rs | 4 +-- 4 files changed, 29 insertions(+), 34 deletions(-) diff --git a/library/core/src/num/imp/int_log10.rs b/library/core/src/num/imp/int_log10.rs index 64ae76198d94f..82dc6f9a9fdfe 100644 --- a/library/core/src/num/imp/int_log10.rs +++ b/library/core/src/num/imp/int_log10.rs @@ -192,9 +192,9 @@ pub(in crate::num) const fn panic_for_nonpositive_argument() -> ! { panic!("argument of integer logarithm must be positive") } -#[unstable(feature = "kani", issue = "none")] #[cfg(kani)] -mod verify { +#[unstable(feature = "kani", issue = "none")] +pub mod verify { use crate::kani; use crate::num::NonZero; diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 2406ee3eeccc4..2e0c2dc156de2 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -4211,9 +4211,9 @@ macro_rules! int_impl { } } -#[unstable(feature = "kani", issue = "none")] #[cfg(kani)] -mod verify { +#[unstable(feature = "kani", issue = "none")] +pub mod verify { use crate::kani; use crate::num::imp::int_log10::verify::check_integer_logarithm; diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 1b61bbb4d4f0c..f6311331e6978 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -3047,9 +3047,9 @@ nonzero_integer! { reversed = "0x6a2c48091e6a2c48", } -#[unstable(feature = "kani", issue = "none")] #[cfg(kani)] -mod verify { +#[unstable(feature = "kani", issue = "none")] +pub mod verify { use super::*; macro_rules! nonzero_check { @@ -5234,31 +5234,26 @@ mod verify { u128::MAX ); - mod logarithms { - use crate::kani; - use crate::num::NonZero; - - macro_rules! check_logarithms { - ($($int:ident),+ $(,)?) => {$( - mod $int { - use super::*; - - #[kani::proof_for_contract(NonZero::::ilog2)] - fn ilog2() { - let n: NonZero = kani::any(); - let _ = n.ilog2(); - kani::cover(true, "nonzero logarithm returns"); - } - - #[kani::proof_for_contract(NonZero::::ilog10)] - fn ilog10() { - let n: NonZero = kani::any(); - let _ = n.ilog10(); - kani::cover(true, "nonzero logarithm returns"); - } - } - )+}; - } - check_logarithms!(u8, u16, u32, u64, u128, usize); + macro_rules! nonzero_check_logarithm { + ($int:ty, $method:ident, $harness:ident) => { + #[kani::proof_for_contract(NonZero::<$int>::$method)] + fn $harness() { + let n: NonZero<$int> = kani::any(); + let _ = n.$method(); + kani::cover(true, "nonzero logarithm returns"); + } + }; } + nonzero_check_logarithm!(u8, ilog2, nonzero_check_ilog2_u8); + nonzero_check_logarithm!(u8, ilog10, nonzero_check_ilog10_u8); + nonzero_check_logarithm!(u16, ilog2, nonzero_check_ilog2_u16); + nonzero_check_logarithm!(u16, ilog10, nonzero_check_ilog10_u16); + nonzero_check_logarithm!(u32, ilog2, nonzero_check_ilog2_u32); + nonzero_check_logarithm!(u32, ilog10, nonzero_check_ilog10_u32); + nonzero_check_logarithm!(u64, ilog2, nonzero_check_ilog2_u64); + nonzero_check_logarithm!(u64, ilog10, nonzero_check_ilog10_u64); + nonzero_check_logarithm!(u128, ilog2, nonzero_check_ilog2_u128); + nonzero_check_logarithm!(u128, ilog10, nonzero_check_ilog10_u128); + nonzero_check_logarithm!(usize, ilog2, nonzero_check_ilog2_usize); + nonzero_check_logarithm!(usize, ilog10, nonzero_check_ilog10_usize); } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index adb85e430f41b..6b9b0de697c51 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -4427,9 +4427,9 @@ macro_rules! uint_impl { } } -#[unstable(feature = "kani", issue = "none")] #[cfg(kani)] -mod verify { +#[unstable(feature = "kani", issue = "none")] +pub mod verify { use crate::kani; use crate::num::imp::int_log10::verify::check_integer_logarithm; From 794b3d02ccb6182b4d03f3c73da2ae76cfbd4404 Mon Sep 17 00:00:00 2001 From: v3risec Date: Mon, 9 Nov 2026 11:43:33 +0800 Subject: [PATCH 3/3] Refine Challenge 30 specifications and proof harnesses --- library/core/src/num/imp/int_log10.rs | 219 +++++++++++--------------- library/core/src/num/int_macros.rs | 56 +------ library/core/src/num/nonzero.rs | 36 ++--- library/core/src/num/uint_macros.rs | 56 +------ 4 files changed, 116 insertions(+), 251 deletions(-) diff --git a/library/core/src/num/imp/int_log10.rs b/library/core/src/num/imp/int_log10.rs index 82dc6f9a9fdfe..3df1d89ccdf85 100644 --- a/library/core/src/num/imp/int_log10.rs +++ b/library/core/src/num/imp/int_log10.rs @@ -10,7 +10,7 @@ use crate::num::NonZero; // 0 < val <= u8::MAX #[inline] #[requires(val > 0)] -#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] +#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))] const fn u8_impl(val: u8) -> u32 { let val = val as u32; @@ -33,7 +33,7 @@ const fn u8_impl(val: u8) -> u32 { // 0 < val < 100_000 #[inline] #[requires(val > 0 && val < 100_000)] -#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] +#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))] const fn less_than_5(val: u32) -> u32 { // Similar to u8, when adding one of these constants to val, // we get two possible bit patterns above the low 17 bits, @@ -56,7 +56,7 @@ const fn less_than_5(val: u32) -> u32 { // 0 < val <= u16::MAX #[inline] #[requires(val > 0)] -#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] +#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))] const fn u16_impl(val: u16) -> u32 { less_than_5(val as u32) } @@ -64,7 +64,7 @@ const fn u16_impl(val: u16) -> u32 { // 0 < val <= u32::MAX #[inline] #[requires(val > 0)] -#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] +#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))] const fn u32_impl(mut val: u32) -> u32 { let mut log = 0; if val >= 100_000 { @@ -77,7 +77,7 @@ const fn u32_impl(mut val: u32) -> u32 { // 0 < val <= u64::MAX #[inline] #[requires(val > 0)] -#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] +#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))] const fn u64_impl(mut val: u64) -> u32 { let mut log = 0; if val >= 10_000_000_000 { @@ -94,7 +94,7 @@ const fn u64_impl(mut val: u64) -> u32 { // 0 < val <= u128::MAX #[inline] #[requires(val > 0)] -#[ensures(|result: &u32| verify::log10_correct(old(val) as u128, *result))] +#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))] const fn u128_impl(mut val: u128) -> u32 { let mut log = 0; if val >= 100_000_000_000_000_000_000_000_000_000_000 { @@ -112,7 +112,7 @@ const fn u128_impl(mut val: u128) -> u32 { macro_rules! define_unsigned_ilog10 { ($($ty:ident => $impl_fn:ident,)*) => {$( #[inline] - #[ensures(|result: &u32| verify::log10_correct(val.get() as u128, *result))] + #[ensures(|result: &u32| log10_correct(val.get() as u128, *result))] pub(in crate::num) const fn $ty(val: NonZero<$ty>) -> u32 { let result = $impl_fn(val.get()); @@ -134,7 +134,7 @@ define_unsigned_ilog10! { } #[inline] -#[ensures(|result: &u32| verify::log10_correct(val.get() as u128, *result))] +#[ensures(|result: &u32| log10_correct(val.get() as u128, *result))] pub(in crate::num) const fn usize(val: NonZero) -> u32 { #[cfg(target_pointer_width = "16")] let impl_fn = u16; @@ -155,7 +155,7 @@ macro_rules! define_signed_ilog10 { // 0 < val <= $ty::MAX #[inline] #[ensures(|result: &Option| match result { - Some(log) => val > 0 && verify::log10_correct(val as u128, *log), + Some(log) => val > 0 && log10_correct(val as u128, *log), None => val <= 0, })] pub(in crate::num) const fn $ty(val: $ty) -> Option { @@ -192,132 +192,89 @@ pub(in crate::num) const fn panic_for_nonpositive_argument() -> ! { panic!("argument of integer logarithm must be positive") } +// For r < 128, this is exactly 2^r <= n < 2^(r+1), including r = 127. #[cfg(kani)] -#[unstable(feature = "kani", issue = "none")] -pub mod verify { - use crate::kani; - use crate::num::NonZero; - - // For r < 128, this is exactly 2^r <= n < 2^(r+1), including r = 127. - pub(crate) const fn log2_correct(n: u128, r: u32) -> bool { - r < 128 && n >> r == 1 - } - - // All representable powers of ten. 10^39 exceeds u128::MAX, so the last - // interval has no representable upper bound. The oracle does not call ilog. - const POWERS_OF_TEN: [u128; 39] = [ - 1, - 10, - 100, - 1_000, - 10_000, - 100_000, - 1_000_000, - 10_000_000, - 100_000_000, - 1_000_000_000, - 10_000_000_000, - 100_000_000_000, - 1_000_000_000_000, - 10_000_000_000_000, - 100_000_000_000_000, - 1_000_000_000_000_000, - 10_000_000_000_000_000, - 100_000_000_000_000_000, - 1_000_000_000_000_000_000, - 10_000_000_000_000_000_000, - 100_000_000_000_000_000_000, - 1_000_000_000_000_000_000_000, - 10_000_000_000_000_000_000_000, - 100_000_000_000_000_000_000_000, - 1_000_000_000_000_000_000_000_000, - 10_000_000_000_000_000_000_000_000, - 100_000_000_000_000_000_000_000_000, - 1_000_000_000_000_000_000_000_000_000, - 10_000_000_000_000_000_000_000_000_000, - 100_000_000_000_000_000_000_000_000_000, - 1_000_000_000_000_000_000_000_000_000_000, - 10_000_000_000_000_000_000_000_000_000_000, - 100_000_000_000_000_000_000_000_000_000_000, - 1_000_000_000_000_000_000_000_000_000_000_000, - 10_000_000_000_000_000_000_000_000_000_000_000, - 100_000_000_000_000_000_000_000_000_000_000_000, - 1_000_000_000_000_000_000_000_000_000_000_000_000, - 10_000_000_000_000_000_000_000_000_000_000_000_000, - 100_000_000_000_000_000_000_000_000_000_000_000_000, - ]; +pub(in crate::num) const fn log2_correct(n: u128, r: u32) -> bool { + r < 128 && n >> r == 1 +} - pub(crate) const fn log10_correct(n: u128, r: u32) -> bool { - r < 39 && POWERS_OF_TEN[r as usize] <= n && (r == 38 || n < POWERS_OF_TEN[(r + 1) as usize]) - } +// Generate the powers at compile time. 10^39 exceeds every representable input. +#[cfg(kani)] +pub(in crate::num) const fn log10_correct(n: u128, r: u32) -> bool { + const POWERS: [u128; 39] = { + let mut powers = [1; 39]; + let mut i = 1; + while i < 39 { + powers[i] = powers[i - 1] * 10; + i += 1; + } + powers + }; + r < 39 && POWERS[r as usize] <= n && (r == 38 || n < POWERS[(r + 1) as usize]) +} - // should_panic alone only witnesses a panic for some input. A safety-check - // failure is not accepted as an expected panic, so any normal return fails - // the harness. This checks every nonpositive input without stubbing code. - pub(crate) fn reject_normal_return() { - kani::safety_check(false, "a nonpositive logarithm must not return"); - } +#[cfg(kani)] +macro_rules! check_logarithms { + ($($name:ident: $target:path => $arg:ty $(, $domain:expr)?;)+) => {$( + #[kani::proof_for_contract($target)] + fn $name() { + let n: $arg = kani::any(); + $(kani::assume(($domain)(n)); + kani::cover(true, "logarithm input is reachable");)? + let _ = $target(n); + kani::cover(true, "logarithm contract returns"); + } + )+}; +} - macro_rules! check_integer_logarithm { - ($int:ty, $method:ident, $harness:ident) => { - #[kani::proof_for_contract($int::$method)] - fn $harness() { - let n: $int = kani::any(); - let _ = n.$method(); - kani::cover(true, "checked logarithm returns"); - } - }; - ($int:ty, $method:ident, $harness:ident, positive) => { - #[kani::proof_for_contract($int::$method)] - fn $harness() { - let n: $int = kani::any(); - if n > 0 { - let _ = n.$method(); - kani::cover(true, "positive logarithm returns"); - } - } - }; - ($int:ty, $method:ident, $harness:ident, panic) => { - #[kani::proof] - #[kani::should_panic] - fn $harness() { - let n: $int = kani::any(); - kani::assume(n <= 0); - kani::cover(true, "nonpositive input is reachable"); - let _ = n.$method(); - crate::num::imp::int_log10::verify::reject_normal_return(); - } - }; - } - pub(crate) use check_integer_logarithm; +#[cfg(kani)] +macro_rules! check_integer_logarithms { + ($($int:ident),+) => {$( + check_integer_logarithms!(@checked $int, checked_ilog2, checked_ilog10); + check_integer_logarithms!(@positive $int, ilog2, ilog10); + )+}; + (@checked $int:ident, $($method:ident),+) => { + check_logarithms! { $(${concat($method, _, $int)}: $int::$method => $int;)+ } + }; + (@positive $int:ident, $($method:ident),+) => {$( + check_logarithms! { ${concat($method, _, $int)}: $int::$method => $int, |n| n > 0; } + #[kani::proof] + #[kani::should_panic] + fn ${concat($method, _, $int, _nonpositive)}() { + let n: $int = kani::any(); + kani::assume(n <= 0); + kani::cover(true, "nonpositive input is reachable"); + let _ = n.$method(); + // A safety-check failure cannot satisfy should_panic: every input must panic. + kani::safety_check(false, "a nonpositive logarithm must not return"); + } + )+}; +} +#[cfg(kani)] +pub(in crate::num) use {check_integer_logarithms, check_logarithms}; - macro_rules! check_internal_contracts { - ($($target:ident: $arg:ty),+ $(,)?) => {$( - #[kani::proof_for_contract(crate::num::imp::int_log10::$target)] - fn $target() { - let n: $arg = kani::any(); - let _ = crate::num::imp::int_log10::$target(n); - kani::cover(true, "internal logarithm contract returns"); - } - )+}; - } - check_internal_contracts! { - u8_impl: u8, - u16_impl: u16, - u32_impl: u32, - u64_impl: u64, - u128_impl: u128, - less_than_5: u32, - u8: NonZero, - u16: NonZero, - u32: NonZero, - u64: NonZero, - u128: NonZero, - usize: NonZero, - i8: i8, - i16: i16, - i32: i32, - i64: i64, - i128: i128, +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + check_logarithms! { + u8_impl: super::u8_impl => u8; + u16_impl: super::u16_impl => u16; + u32_impl: super::u32_impl => u32; + u64_impl: super::u64_impl => u64; + u128_impl: super::u128_impl => u128; + less_than_5: super::less_than_5 => u32; + u8: super::u8 => NonZero; + u16: super::u16 => NonZero; + u32: super::u32 => NonZero; + u64: super::u64 => NonZero; + u128: super::u128 => NonZero; + usize: super::usize => NonZero; + i8: super::i8 => i8; + i16: super::i16 => i16; + i32: super::i32 => i32; + i64: super::i64 => i64; + i128: super::i128 => i128; } } diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 2e0c2dc156de2..82ddcec8ce4f8 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -3515,7 +3515,7 @@ macro_rules! int_impl { #[inline] #[track_caller] #[ensures(|result: &u32| { - self > 0 && imp::int_log10::verify::log2_correct(self as u128, *result) + self > 0 && imp::int_log10::log2_correct(self as u128, *result) })] pub const fn ilog2(self) -> u32 { if let Some(log) = self.checked_ilog2() { @@ -3543,7 +3543,7 @@ macro_rules! int_impl { #[inline] #[track_caller] #[ensures(|result: &u32| { - self > 0 && imp::int_log10::verify::log10_correct(self as u128, *result) + self > 0 && imp::int_log10::log10_correct(self as u128, *result) })] pub const fn ilog10(self) -> u32 { if let Some(log) = self.checked_ilog10() { @@ -3600,7 +3600,7 @@ macro_rules! int_impl { without modifying the original"] #[inline] #[ensures(|result: &Option| match result { - Some(log) => self > 0 && imp::int_log10::verify::log2_correct(self as u128, *log), + Some(log) => self > 0 && imp::int_log10::log2_correct(self as u128, *log), None => self <= 0, })] pub const fn checked_ilog2(self) -> Option { @@ -3628,7 +3628,7 @@ macro_rules! int_impl { without modifying the original"] #[inline] #[ensures(|result: &Option| match result { - Some(log) => self > 0 && imp::int_log10::verify::log10_correct(self as u128, *log), + Some(log) => self > 0 && imp::int_log10::log10_correct(self as u128, *log), None => self <= 0, })] pub const fn checked_ilog10(self) -> Option { @@ -4213,49 +4213,9 @@ macro_rules! int_impl { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] -pub mod verify { +mod verify { use crate::kani; - use crate::num::imp::int_log10::verify::check_integer_logarithm; - - check_integer_logarithm!(i8, checked_ilog2, checked_ilog2_i8); - check_integer_logarithm!(i8, checked_ilog10, checked_ilog10_i8); - check_integer_logarithm!(i8, ilog2, ilog2_i8, positive); - check_integer_logarithm!(i8, ilog10, ilog10_i8, positive); - check_integer_logarithm!(i8, ilog2, ilog2_i8_nonpositive, panic); - check_integer_logarithm!(i8, ilog10, ilog10_i8_nonpositive, panic); - - check_integer_logarithm!(i16, checked_ilog2, checked_ilog2_i16); - check_integer_logarithm!(i16, checked_ilog10, checked_ilog10_i16); - check_integer_logarithm!(i16, ilog2, ilog2_i16, positive); - check_integer_logarithm!(i16, ilog10, ilog10_i16, positive); - check_integer_logarithm!(i16, ilog2, ilog2_i16_nonpositive, panic); - check_integer_logarithm!(i16, ilog10, ilog10_i16_nonpositive, panic); - - check_integer_logarithm!(i32, checked_ilog2, checked_ilog2_i32); - check_integer_logarithm!(i32, checked_ilog10, checked_ilog10_i32); - check_integer_logarithm!(i32, ilog2, ilog2_i32, positive); - check_integer_logarithm!(i32, ilog10, ilog10_i32, positive); - check_integer_logarithm!(i32, ilog2, ilog2_i32_nonpositive, panic); - check_integer_logarithm!(i32, ilog10, ilog10_i32_nonpositive, panic); - - check_integer_logarithm!(i64, checked_ilog2, checked_ilog2_i64); - check_integer_logarithm!(i64, checked_ilog10, checked_ilog10_i64); - check_integer_logarithm!(i64, ilog2, ilog2_i64, positive); - check_integer_logarithm!(i64, ilog10, ilog10_i64, positive); - check_integer_logarithm!(i64, ilog2, ilog2_i64_nonpositive, panic); - check_integer_logarithm!(i64, ilog10, ilog10_i64_nonpositive, panic); - - check_integer_logarithm!(i128, checked_ilog2, checked_ilog2_i128); - check_integer_logarithm!(i128, checked_ilog10, checked_ilog10_i128); - check_integer_logarithm!(i128, ilog2, ilog2_i128, positive); - check_integer_logarithm!(i128, ilog10, ilog10_i128, positive); - check_integer_logarithm!(i128, ilog2, ilog2_i128_nonpositive, panic); - check_integer_logarithm!(i128, ilog10, ilog10_i128_nonpositive, panic); - - check_integer_logarithm!(isize, checked_ilog2, checked_ilog2_isize); - check_integer_logarithm!(isize, checked_ilog10, checked_ilog10_isize); - check_integer_logarithm!(isize, ilog2, ilog2_isize, positive); - check_integer_logarithm!(isize, ilog10, ilog10_isize, positive); - check_integer_logarithm!(isize, ilog2, ilog2_isize_nonpositive, panic); - check_integer_logarithm!(isize, ilog10, ilog10_isize_nonpositive, panic); + use crate::num::imp::int_log10::{check_integer_logarithms, check_logarithms}; + + check_integer_logarithms!(i8, i16, i32, i64, i128, isize); } diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index f6311331e6978..7f499a0f800ad 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2120,7 +2120,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] - #[ensures(|result: &u32| imp::int_log10::verify::log2_correct(self.get() as u128, *result))] + #[ensures(|result: &u32| imp::int_log10::log2_correct(self.get() as u128, *result))] pub const fn ilog2(self) -> u32 { Self::BITS - 1 - self.leading_zeros() } @@ -2150,7 +2150,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] - #[ensures(|result: &u32| imp::int_log10::verify::log10_correct(self.get() as u128, *result))] + #[ensures(|result: &u32| imp::int_log10::log10_correct(self.get() as u128, *result))] pub const fn ilog10(self) -> u32 { imp::int_log10::$Int(self) } @@ -3047,10 +3047,11 @@ nonzero_integer! { reversed = "0x6a2c48091e6a2c48", } -#[cfg(kani)] #[unstable(feature = "kani", issue = "none")] -pub mod verify { +#[cfg(kani)] +mod verify { use super::*; + use crate::num::imp::int_log10::check_logarithms; macro_rules! nonzero_check { ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => { @@ -5234,26 +5235,13 @@ pub mod verify { u128::MAX ); - macro_rules! nonzero_check_logarithm { - ($int:ty, $method:ident, $harness:ident) => { - #[kani::proof_for_contract(NonZero::<$int>::$method)] - fn $harness() { - let n: NonZero<$int> = kani::any(); - let _ = n.$method(); - kani::cover(true, "nonzero logarithm returns"); - } + macro_rules! nonzero_check_logarithms { + ($($int:ident),+) => { + check_logarithms! { $( + ${concat(nonzero_check_ilog2_, $int)}: NonZero::<$int>::ilog2 => NonZero<$int>; + ${concat(nonzero_check_ilog10_, $int)}: NonZero::<$int>::ilog10 => NonZero<$int>; + )+ } }; } - nonzero_check_logarithm!(u8, ilog2, nonzero_check_ilog2_u8); - nonzero_check_logarithm!(u8, ilog10, nonzero_check_ilog10_u8); - nonzero_check_logarithm!(u16, ilog2, nonzero_check_ilog2_u16); - nonzero_check_logarithm!(u16, ilog10, nonzero_check_ilog10_u16); - nonzero_check_logarithm!(u32, ilog2, nonzero_check_ilog2_u32); - nonzero_check_logarithm!(u32, ilog10, nonzero_check_ilog10_u32); - nonzero_check_logarithm!(u64, ilog2, nonzero_check_ilog2_u64); - nonzero_check_logarithm!(u64, ilog10, nonzero_check_ilog10_u64); - nonzero_check_logarithm!(u128, ilog2, nonzero_check_ilog2_u128); - nonzero_check_logarithm!(u128, ilog10, nonzero_check_ilog10_u128); - nonzero_check_logarithm!(usize, ilog2, nonzero_check_ilog2_usize); - nonzero_check_logarithm!(usize, ilog10, nonzero_check_ilog10_usize); + nonzero_check_logarithms!(u8, u16, u32, u64, u128, usize); } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 6b9b0de697c51..52319921bc5db 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -1835,7 +1835,7 @@ macro_rules! uint_impl { #[inline] #[track_caller] #[ensures(|result: &u32| { - self > 0 && imp::int_log10::verify::log2_correct(self as u128, *result) + self > 0 && imp::int_log10::log2_correct(self as u128, *result) })] pub const fn ilog2(self) -> u32 { if let Some(log) = self.checked_ilog2() { @@ -1863,7 +1863,7 @@ macro_rules! uint_impl { #[inline] #[track_caller] #[ensures(|result: &u32| { - self > 0 && imp::int_log10::verify::log10_correct(self as u128, *result) + self > 0 && imp::int_log10::log10_correct(self as u128, *result) })] pub const fn ilog10(self) -> u32 { if let Some(log) = self.checked_ilog10() { @@ -1964,7 +1964,7 @@ macro_rules! uint_impl { without modifying the original"] #[inline] #[ensures(|result: &Option| match result { - Some(log) => self > 0 && imp::int_log10::verify::log2_correct(self as u128, *log), + Some(log) => self > 0 && imp::int_log10::log2_correct(self as u128, *log), None => self == 0, })] pub const fn checked_ilog2(self) -> Option { @@ -1989,7 +1989,7 @@ macro_rules! uint_impl { without modifying the original"] #[inline] #[ensures(|result: &Option| match result { - Some(log) => self > 0 && imp::int_log10::verify::log10_correct(self as u128, *log), + Some(log) => self > 0 && imp::int_log10::log10_correct(self as u128, *log), None => self == 0, })] pub const fn checked_ilog10(self) -> Option { @@ -4429,49 +4429,9 @@ macro_rules! uint_impl { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] -pub mod verify { +mod verify { use crate::kani; - use crate::num::imp::int_log10::verify::check_integer_logarithm; - - check_integer_logarithm!(u8, checked_ilog2, checked_ilog2_u8); - check_integer_logarithm!(u8, checked_ilog10, checked_ilog10_u8); - check_integer_logarithm!(u8, ilog2, ilog2_u8, positive); - check_integer_logarithm!(u8, ilog10, ilog10_u8, positive); - check_integer_logarithm!(u8, ilog2, ilog2_u8_nonpositive, panic); - check_integer_logarithm!(u8, ilog10, ilog10_u8_nonpositive, panic); - - check_integer_logarithm!(u16, checked_ilog2, checked_ilog2_u16); - check_integer_logarithm!(u16, checked_ilog10, checked_ilog10_u16); - check_integer_logarithm!(u16, ilog2, ilog2_u16, positive); - check_integer_logarithm!(u16, ilog10, ilog10_u16, positive); - check_integer_logarithm!(u16, ilog2, ilog2_u16_nonpositive, panic); - check_integer_logarithm!(u16, ilog10, ilog10_u16_nonpositive, panic); - - check_integer_logarithm!(u32, checked_ilog2, checked_ilog2_u32); - check_integer_logarithm!(u32, checked_ilog10, checked_ilog10_u32); - check_integer_logarithm!(u32, ilog2, ilog2_u32, positive); - check_integer_logarithm!(u32, ilog10, ilog10_u32, positive); - check_integer_logarithm!(u32, ilog2, ilog2_u32_nonpositive, panic); - check_integer_logarithm!(u32, ilog10, ilog10_u32_nonpositive, panic); - - check_integer_logarithm!(u64, checked_ilog2, checked_ilog2_u64); - check_integer_logarithm!(u64, checked_ilog10, checked_ilog10_u64); - check_integer_logarithm!(u64, ilog2, ilog2_u64, positive); - check_integer_logarithm!(u64, ilog10, ilog10_u64, positive); - check_integer_logarithm!(u64, ilog2, ilog2_u64_nonpositive, panic); - check_integer_logarithm!(u64, ilog10, ilog10_u64_nonpositive, panic); - - check_integer_logarithm!(u128, checked_ilog2, checked_ilog2_u128); - check_integer_logarithm!(u128, checked_ilog10, checked_ilog10_u128); - check_integer_logarithm!(u128, ilog2, ilog2_u128, positive); - check_integer_logarithm!(u128, ilog10, ilog10_u128, positive); - check_integer_logarithm!(u128, ilog2, ilog2_u128_nonpositive, panic); - check_integer_logarithm!(u128, ilog10, ilog10_u128_nonpositive, panic); - - check_integer_logarithm!(usize, checked_ilog2, checked_ilog2_usize); - check_integer_logarithm!(usize, checked_ilog10, checked_ilog10_usize); - check_integer_logarithm!(usize, ilog2, ilog2_usize, positive); - check_integer_logarithm!(usize, ilog10, ilog10_usize, positive); - check_integer_logarithm!(usize, ilog2, ilog2_usize_nonpositive, panic); - check_integer_logarithm!(usize, ilog10, ilog10_usize_nonpositive, panic); + use crate::num::imp::int_log10::{check_integer_logarithms, check_logarithms}; + + check_integer_logarithms!(u8, u16, u32, u64, u128, usize); }