Skip to content

Challenge 30: Verify integer logarithm safety and correctness #749

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
v3risec wants to merge 7 commits into
base: main
Choose a base branch
from
+168 −0
Open

Challenge 30: Verify integer logarithm safety and correctness #749

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
fee9360
Verify integer logarithms with Kani
v3risec Nov 7, 2026
681c55d
Merge remote-tracking branch 'upstream/main' into challenge-30-integer
v3risec Nov 8, 2026
ab5a671
Fix Challenge 30 harness visibility and organization
v3risec Nov 8, 2026
794b3d0
Refine Challenge 30 specifications and proof harnesses
v3risec Nov 9, 2026
4331af4
Merge branch 'main' into challenge-30-integer
v3risec Nov 9, 2026
620bc91
Merge branch 'main' into challenge-30-integer
v3risec Nov 9, 2026
cfb89b1
Merge branch 'main' into challenge-30-integer
v3risec Nov 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
109 changes: 109 additions & 0 deletions library/core/src/num/imp/int_log10.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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| log10_correct(old(val) as u128, *result))]
const fn u8_impl(val: u8) -> u32 {
let val = val as u32;

Expand All @@ -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| 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,
Expand All @@ -47,12 +55,16 @@ const fn less_than_5(val: u32) -> u32 {

// 0 < val <= u16::MAX
#[inline]
#[requires(val > 0)]
#[ensures(|result: &u32| 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| log10_correct(old(val) as u128, *result))]
const fn u32_impl(mut val: u32) -> u32 {
let mut log = 0;
if val >= 100_000 {
Expand All @@ -64,6 +76,8 @@ const fn u32_impl(mut val: u32) -> u32 {

// 0 < val <= u64::MAX
#[inline]
#[requires(val > 0)]
#[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 {
Expand All @@ -79,6 +93,8 @@ const fn u64_impl(mut val: u64) -> u32 {

// 0 < val <= u128::MAX
#[inline]
#[requires(val > 0)]
#[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 {
Expand All @@ -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| log10_correct(val.get() as u128, *result))]
pub(in crate::num) const fn $ty(val: NonZero<$ty>) -> u32 {
let result = $impl_fn(val.get());

Expand All @@ -117,6 +134,7 @@ define_unsigned_ilog10! {
}

#[inline]
#[ensures(|result: &u32| log10_correct(val.get() as u128, *result))]
pub(in crate::num) const fn usize(val: NonZero<usize>) -> u32 {
#[cfg(target_pointer_width = "16")]
let impl_fn = u16;
Expand All @@ -136,6 +154,10 @@ macro_rules! define_signed_ilog10 {
($($ty:ident => $impl_fn:ident,)*) => {$(
// 0 < val <= $ty::MAX
#[inline]
#[ensures(|result: &Option<u32>| match result {
Some(log) => val > 0 && log10_correct(val as u128, *log),
None => val <= 0,
})]
pub(in crate::num) const fn $ty(val: $ty) -> Option<u32> {
if val > 0 {
let result = $impl_fn(val.cast_unsigned());
Expand Down Expand Up @@ -169,3 +191,90 @@ define_signed_ilog10! {
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)]
pub(in crate::num) const fn log2_correct(n: u128, r: u32) -> bool {
r < 128 && n >> r == 1
}

// 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])
}

#[cfg(kani)]
macro_rules! check_logarithms {
($($name:ident: $target:path => $arg:ty $(, $domain:expr)?;)+) => {$(
#[kani::proof_for_contract($target)]

@v3risec v3risec Nov 10, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the review. As documented in the PR summary, I have already run the complete set of 101 harnesses locally with the repository-pinned Kani and -Z valid-value-checks. All 101 proofs and 125 cover properties passed, including the additional invalid-value checks.

The repository's existing CI configuration does not enable this flag, and this PR does not modify the CI infrastructure. Therefore, this is a limitation of the current shared CI configuration rather than a missing verification step in the contributed harnesses.

I'm happy to provide the exact local verification command or logs if helpful. If the maintainers would like -Z valid-value-checks to be enforced in CI for Challenge 30, I'm happy to discuss the appropriate approach.

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");
}
)+};
}

#[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};

#[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<u8>;
u16: super::u16 => NonZero<u16>;
u32: super::u32 => NonZero<u32>;
u64: super::u64 => NonZero<u64>;
u128: super::u128 => NonZero<u128>;
usize: super::usize => NonZero<usize>;
i8: super::i8 => i8;
i16: super::i16 => i16;
i32: super::i32 => i32;
i64: super::i64 => i64;
i128: super::i128 => i128;
}
}
23 changes: 23 additions & 0 deletions library/core/src/num/int_macros.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3514,6 +3514,9 @@ macro_rules! int_impl {
without modifying the original"]
#[inline]
#[track_caller]
#[ensures(|result: &u32| {
self > 0 && imp::int_log10::log2_correct(self as u128, *result)
})]
pub const fn ilog2(self) -> u32 {
if let Some(log) = self.checked_ilog2() {
log
Expand All @@ -3539,6 +3542,9 @@ macro_rules! int_impl {
without modifying the original"]
#[inline]
#[track_caller]
#[ensures(|result: &u32| {
self > 0 && imp::int_log10::log10_correct(self as u128, *result)
})]
pub const fn ilog10(self) -> u32 {
if let Some(log) = self.checked_ilog10() {
log
Expand Down Expand Up @@ -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<u32>| match result {
Some(log) => self > 0 && imp::int_log10::log2_correct(self as u128, *log),
None => self <= 0,
})]
pub const fn checked_ilog2(self) -> Option<u32> {
if self <= 0 {
None
Expand All @@ -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<u32>| match result {
Some(log) => self > 0 && imp::int_log10::log10_correct(self as u128, *log),
None => self <= 0,
})]
pub const fn checked_ilog10(self) -> Option<u32> {
imp::int_log10::$ActualT(self as $ActualT)
}
Expand Down Expand Up @@ -4196,3 +4210,12 @@ macro_rules! int_impl {
}
}
}

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use crate::kani;
use crate::num::imp::int_log10::{check_integer_logarithms, check_logarithms};

check_integer_logarithms!(i8, i16, i32, i64, i128, isize);
}
13 changes: 13 additions & 0 deletions library/core/src/num/nonzero.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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::log2_correct(self.get() as u128, *result))]
pub const fn ilog2(self) -> u32 {
Self::BITS - 1 - self.leading_zeros()
}
Expand Down Expand Up @@ -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::log10_correct(self.get() as u128, *result))]
pub const fn ilog10(self) -> u32 {
imp::int_log10::$Int(self)
}
Expand Down Expand Up @@ -3049,6 +3051,7 @@ nonzero_integer! {
#[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) => {
Expand Down Expand Up @@ -5231,4 +5234,14 @@ mod verify {
u128::MAX - 0xFFFFu128,
u128::MAX
);

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_logarithms!(u8, u16, u32, u64, u128, usize);
}
23 changes: 23 additions & 0 deletions library/core/src/num/uint_macros.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1834,6 +1834,9 @@ macro_rules! uint_impl {
without modifying the original"]
#[inline]
#[track_caller]
#[ensures(|result: &u32| {
self > 0 && imp::int_log10::log2_correct(self as u128, *result)
})]
pub const fn ilog2(self) -> u32 {
if let Some(log) = self.checked_ilog2() {
log
Expand All @@ -1859,6 +1862,9 @@ macro_rules! uint_impl {
without modifying the original"]
#[inline]
#[track_caller]
#[ensures(|result: &u32| {
self > 0 && imp::int_log10::log10_correct(self as u128, *result)
})]
pub const fn ilog10(self) -> u32 {
if let Some(log) = self.checked_ilog10() {
log
Expand Down Expand Up @@ -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<u32>| match result {
Some(log) => self > 0 && imp::int_log10::log2_correct(self as u128, *log),
None => self == 0,
})]
pub const fn checked_ilog2(self) -> Option<u32> {
match NonZero::new(self) {
Some(x) => Some(x.ilog2()),
Expand All @@ -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<u32>| match result {
Some(log) => self > 0 && imp::int_log10::log10_correct(self as u128, *log),
None => self == 0,
})]
pub const fn checked_ilog10(self) -> Option<u32> {
match NonZero::new(self) {
Some(x) => Some(x.ilog10()),
Expand Down Expand Up @@ -4412,3 +4426,12 @@ macro_rules! uint_impl {
}
}
}

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use crate::kani;
use crate::num::imp::int_log10::{check_integer_logarithms, check_logarithms};

check_integer_logarithms!(u8, u16, u32, u64, u128, usize);
}
Loading