From 4ab985b1d09a27ec7441746786240c2002586d50 Mon Sep 17 00:00:00 2001 From: Kieran Hulsman Date: Thu, 15 Oct 2026 12:14:06 -0400 Subject: [PATCH 1/3] 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/3] 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 From fc937870387cbf2845dff98c8226064ab432a273 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sat, 7 Nov 2026 20:25:07 +0000 Subject: [PATCH 3/3] unblocking merge with workflow fix ubuntu-latest is moving to Ubuntu 26.04, where Kani's install_cbmc.sh downloads a 404 page (there is no CBMC package for 26.04) and every Kani job fails. Pin the Linux runners to ubuntu-24.04. The matrix jobs keep `os: ubuntu-latest` and only map it to ubuntu-24.04 in runs-on. Their check names, which branch protection requires (e.g. "upstream_test (ubuntu-latest)"), and their artifact names stay the same. --- .github/workflows/book.yml | 4 ++-- .github/workflows/flux.yml | 2 +- .github/workflows/goto-transcoder.yml | 2 +- .github/workflows/kani-metrics.yml | 2 +- .github/workflows/kani.yml | 12 ++++++------ .github/workflows/kmir.yml | 4 ++-- .github/workflows/pr_approval.yml | 2 +- .github/workflows/rapx.yml | 2 +- .github/workflows/rustc.yml | 2 +- .github/workflows/testable-simd-models.yml | 2 +- .github/workflows/verifast-negative.yml | 2 +- .github/workflows/verifast.yml | 4 ++-- 12 files changed, 20 insertions(+), 20 deletions(-) diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml index 0d016bddb1cb1..fe3d14393fe1b 100644 --- a/.github/workflows/book.yml +++ b/.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 diff --git a/.github/workflows/flux.yml b/.github/workflows/flux.yml index da012b1afdb6d..8ff3e67617a06 100644 --- a/.github/workflows/flux.yml +++ b/.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: diff --git a/.github/workflows/goto-transcoder.yml b/.github/workflows/goto-transcoder.yml index 7272f2d657a0f..f1fc477403e59 100644 --- a/.github/workflows/goto-transcoder.yml +++ b/.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 diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml index 443ac9d18f546..d42668b637aea 100644 --- a/.github/workflows/kani-metrics.yml +++ b/.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 diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 21eb1e2a2d490..d93b0ecc26b16 100644 --- a/.github/workflows/kani.yml +++ b/.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 diff --git a/.github/workflows/kmir.yml b/.github/workflows/kmir.yml index bcd905c781dbf..a7e66edaf6dc0 100644 --- a/.github/workflows/kmir.yml +++ b/.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 }}" diff --git a/.github/workflows/pr_approval.yml b/.github/workflows/pr_approval.yml index a244de66c6097..addfa005a036c 100644 --- a/.github/workflows/pr_approval.yml +++ b/.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 diff --git a/.github/workflows/rapx.yml b/.github/workflows/rapx.yml index c8a5053c14832..a73dedfdf9d80 100644 --- a/.github/workflows/rapx.yml +++ b/.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: diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml index abc2a1a31552b..35dfc027e5e35 100644 --- a/.github/workflows/rustc.yml +++ b/.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. diff --git a/.github/workflows/testable-simd-models.yml b/.github/workflows/testable-simd-models.yml index 7bd27d768fd12..606d92650eb6e 100644 --- a/.github/workflows/testable-simd-models.yml +++ b/.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 diff --git a/.github/workflows/verifast-negative.yml b/.github/workflows/verifast-negative.yml index cc1793f560c28..01cd9e55d7527 100644 --- a/.github/workflows/verifast-negative.yml +++ b/.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 diff --git a/.github/workflows/verifast.yml b/.github/workflows/verifast.yml index ec97d018dc01b..5f835ccb17eaf 100644 --- a/.github/workflows/verifast.yml +++ b/.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: