New challenge: Safety and correctness of integer logarithms

.github/workflows/book.yml

@@ -13,7 +13,7 @@ on:
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout
         uses: actions/checkout@v4
@@ -40,7 +40,7 @@ jobs:
 
   deploy:
     needs: build
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
 
     # Grant GITHUB_TOKEN the permissions required to make a Pages deployment

.github/workflows/flux.yml

@@ -13,7 +13,7 @@ env:
 
 jobs:
   check-flux-on-core:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@v4
         with:

.github/workflows/goto-transcoder.yml

@@ -20,7 +20,7 @@ defaults:
 jobs:
   verify-rust-std:
     name: Verify contracts with goto-transcoder
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       # Step 1: Check out the repository
       - name: Checkout Repository

.github/workflows/kani-metrics.yml

@@ -15,7 +15,7 @@ jobs:
       contents: write
       pull-requests: write
     if: github.repository == 'model-checking/verify-rust-std'
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
 
     steps:
     - name: Remove unnecessary software to free up disk space

.github/workflows/kani.yml

@@ -27,7 +27,7 @@ jobs:
     name: Verify std library (partition ${{ matrix.partition }})
     # When called for autoharness only, the partitions already ran for this commit.
     if: ${{ !inputs.autoharness }}
-    runs-on: ${{ matrix.os }}
+    runs-on: ${{ matrix.os == 'ubuntu-latest' && 'ubuntu-24.04' || matrix.os }}
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]
@@ -83,7 +83,7 @@ jobs:
     # This job is a required check under its matrix name, and a job skipped by a job-level
     # `if:` reports without the "(os)" suffix, which would leave PRs pending. So the gate is
     # on each step instead: on a PR the job starts, skips every step and passes in seconds.
-    runs-on: ${{ matrix.os }}
+    runs-on: ${{ matrix.os == 'ubuntu-latest' && 'ubuntu-24.04' || matrix.os }}
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]
@@ -249,7 +249,7 @@ jobs:
   run_kani_metrics:
     name: Kani Metrics
     if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness
-    runs-on: ${{ matrix.os }}
+    runs-on: ${{ matrix.os == 'ubuntu-latest' && 'ubuntu-24.04' || matrix.os }}
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]
@@ -321,7 +321,7 @@ jobs:
     name: Build JSON from logs
     if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness
     needs: [run_kani_metrics, kani_autoharness]
-    runs-on: ${{ matrix.os }}
+    runs-on: ${{ matrix.os == 'ubuntu-latest' && 'ubuntu-24.04' || matrix.os }}
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]
@@ -373,7 +373,7 @@ jobs:
   run-kani-list:
     name: Kani List
     if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Remove unnecessary software to free up disk space
         run: |
@@ -419,7 +419,7 @@ jobs:
   run-autoharness-analyzer:
     name: Kani Autoharness Analyzer
     if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || inputs.autoharness
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       # Step 1: Check out the repository
       - name: Checkout Repository

.github/workflows/kmir.yml

@@ -17,7 +17,7 @@ env:
 jobs:
   run-kmir-proofs:
     name: Run KMIR proofs
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     env:
       container_name: "kmir-${{ github.run_id }}"
 
@@ -37,7 +37,7 @@ jobs:
 
   run-kmir-proofs-negative:
     name: Run KMIR negative proofs
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     env:
       container_name: "kmir-neg-${{ github.run_id }}"
 

.github/workflows/pr_approval.yml

@@ -15,7 +15,7 @@ on:
 
 jobs:
   check-approvals:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@v2

.github/workflows/rapx.yml

@@ -14,7 +14,7 @@ env:
 jobs:
   verify-slice:
     name: Verify core::slice with RAPx
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@v4
         with:

.github/workflows/rustc.yml

@@ -20,7 +20,7 @@ defaults:
 
 jobs:
   upstream_test:
-    runs-on: ${{ matrix.os }}
+    runs-on: ${{ matrix.os == 'ubuntu-latest' && 'ubuntu-24.04' || matrix.os }}
     strategy:
       matrix:
         # Note windows-latest is currently failing.

.github/workflows/testable-simd-models.yml

@@ -19,7 +19,7 @@ defaults:
 jobs:
   testable-simd-models:
     name: Test testable simd models
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
 
     steps:
       - name: Checkout Repository

.github/workflows/verifast-negative.yml

@@ -21,7 +21,7 @@ defaults:
 jobs:
   check-verifast-on-std:
     name: Verify std library
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
 
     steps:
       - name: Checkout Repository

.github/workflows/verifast.yml

@@ -18,7 +18,7 @@ defaults:
 jobs:
   check-verifast-on-std:
     name: Verify std library
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
 
     steps:
       - name: Checkout Repository
@@ -29,7 +29,7 @@ jobs:
 
   notify-btj:
     name: Notify @btj
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04
     needs: check-verifast-on-std
     if: failure()
     permissions:

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)

doc/src/challenges/0030-integer-logarithms.md

@@ -0,0 +1,68 @@
+# Challenge 30: Safety and Correctness of Integer Logarithms
+
+- **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)
+- **Start date:** *2026/11/02*
+- **Reward:** *TBD*
+
+-------------------
+
+## Goal
+
+Verify the safety and correctness of `ilog10`, `ilog2`, and their checked variants in `core::num`,
+including `NonZero<T>::ilog2` and `NonZero<T>::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; 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
+
+| 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`, `NonZero<T>::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) |
+
+- **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.
+- 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, 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.
+
+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.
+- 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.