[Kieran-Hulsman]

Resolves #728.

Adds contracts and Kani harnesses for Challenge 30. No function bodies are changed.

• Correctness: every function's result is checked against is_ilog, and the checked versions return None for zero and negative inputs.
• Panics: ilog2 and ilog10 are checked to panic on zero and negative inputs.
• Safety: Kani checks the unsafe calls along the way (assert_unchecked, ctlz_nonzero, new_unchecked). The helpers only assume their documented input ranges.

Call graph of the verified functions

flowchart TD
    subgraph P["int_macros.rs, uint_macros.rs<br/>72 harnesses in mod.rs"]
        A1["ilog2, ilog10"]
        A2["checked_ilog2, checked_ilog10"]
        A1 --> A2
    end
    subgraph N["nonzero.rs, 12 harnesses"]
        B2["NonZero::ilog2"]
        B10["NonZero::ilog10"]
    end
    subgraph L["imp/int_log10.rs, 17 harnesses"]
        C["Wrappers"]
        D["Helpers"]
    end
    E["ctlz_nonzero"]
    A2 -->|unsigned| N
    A2 -->|signed ilog10| C
    A2 -->|signed ilog2| E
    B10 --> C
    B2 --> E
    C --> D

Loading

Re: Assumptions. usize is only proved for 64-bit targets, since that's all CI runs. On 16- and 32-bit targets, the usize wrapper casts to u16 or u32, the same width as usize, so new_unchecked still gets a nonzero value.

All 101 harnesses pass locally with the flags in scripts/run-kani.sh. They also pass with -Z valid-value-checks, which CI doesn't enable, to cover invalid values.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

🟢 Approval recommended

No active review issues are identified for the added integer-logarithm contracts and Kani verification harnesses.

No open issues 🎉

What changed in this PR

This PR addresses Challenge 30 (#728) by adding contracts and Kani verification harnesses for integer logarithms in the Rust standard library, without changing existing function bodies.

Changes:

• Adds correctness contracts for signed, unsigned, and NonZero base-2 and base-10 logarithms.
• Adds 101 harnesses covering correctness, invalid-input behavior, and safety.
• Introduces a shared is_ilog predicate and contracts for internal base-10 helpers; usize verification is limited to 64-bit targets.

File	Description
library/​core/​src/​num/​uint_macros.rs	Adds contracts for unsigned logarithms and their checked variants.
library/​core/​src/​num/​nonzero.rs	Adds logarithm contracts and 12 harnesses for unsigned NonZero types.
library/​core/​src/​num/​mod.rs	Adds 72 harnesses for primitive logarithm correctness and panic behavior.
library/​core/​src/​num/​int_macros.rs	Adds signed logarithm contracts, including nonpositive-input handling.
library/​core/​src/​num/​imp/​int_log10.rs	Adds helper contracts, the shared correctness predicate, and 17 harnesses.

_{Review effort: Balanced}

[feliperodri]

Thanks, Kieran. This is a correct solution: all 101 harnesses pass locally with the pinned Kani (c5e65fd), and the same 6 bugs I injected into the implementation for #749 make harnesses fail here too, with the same number of failures in each case. is_ilog is a clean single reference check for both bases.

We're prioritizing #749 for Challenge 30. Solutions are reviewed first come, first served (general-rules.md), and #749 was submitted about 14 hours before this PR. Its first commit (11-07) already had the same approach, and it reached the same results. We'll keep this PR open until #749 is merged.

One difference I noticed, for future solutions: the contract proofs for the helpers and the checked methods have no kani::cover, so nothing shows their inputs are actually reached. The positive_returns_log and nonpositive_panics harnesses do have one.