[v3risec]

Summary

This PR adds safety::{requires, ensures} contracts and Kani harnesses for Challenge 30: Safety and Correctness of Integer Logarithms.

The verification targets include:

• ilog2, ilog10, checked_ilog2, and checked_ilog10 for all signed and unsigned integer types, including isize and usize;
• NonZero<T>::ilog2 and NonZero<T>::ilog10 for all unsigned integer types;
• all 6 internal decimal-logarithm helpers and 11 wrappers listed in the challenge.

Independent mathematical predicates specify exact results using a guarded shift for binary logarithms and intervals between compile-time-generated powers of ten for decimal logarithms. Boundary cases are handled without computing overflowing powers such as 2^128 or 10^39.

Checked methods return None exactly for invalid inputs: zero for unsigned types, and zero or negative values for signed types. Dedicated panic harnesses verify the ordinary methods on these inputs and reject any normal return.

The proofs exercise the original implementations, including result-bound assertions, nonzero intrinsic requirements, and the usize wrapper's unchecked NonZero conversion. Target function bodies are unchanged. Private verification modules and shared macros reduce duplication while preserving post-call cover checks for every contract proof.

Local validation

The updated implementation passed a complete serial run using the repository-pinned Kani with -Z valid-value-checks:

• 101/101 harnesses: 77 contract proofs and 24 panic proofs;
• 125/125 cover properties, including post-call witnesses for all 77 contract proofs;
• standard intrinsic and arithmetic checks, together with the additional invalid-value checks.

The repository's default CI configuration does not enable -Z valid-value-checks; this additional verification was performed locally. No CI configuration or Kani source changes are included.

Pointer-width-dependent proofs ran on the 64-bit configuration. For 16/32-bit configurations, the corresponding fixed-width wrappers are verified, and the selected same-width conversion preserves nonzero values, as permitted by the challenge.

Resolves #728

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

[v3risec]

All required CI checks have passed, and the PR is ready for review. Thank you!

[Copilot]

🟡 Changes recommended

CI Kani runs omit -Z valid-value-checks, leaving the logarithm harnesses short of Challenge 30’s automated invalid-value verification requirement.

1 open issue

• CI omits invalid-value checks for Challenge 30 · New

What changed in this PR

This PR adds contracts and Kani proofs for Challenge 30 (#728), extending formal verification of integer logarithms in core::num without changing the target implementations.

Changes:

• Specify exact binary and decimal logarithm results, including checked-method behavior for invalid inputs.
• Add shared contract and panic harnesses for integer types, unsigned NonZero types, and internal decimal-logarithm helpers.
• Add mathematical predicates and reachability checks to support the proofs.

File	Description
library/​core/​src/​num/​uint_macros.rs	Adds unsigned logarithm contracts and harnesses.
library/​core/​src/​num/​nonzero.rs	Adds contracts and harnesses for unsigned NonZero logarithms.
library/​core/​src/​num/​int_macros.rs	Adds signed logarithm contracts and harnesses.
library/​core/​src/​num/​imp/​int_log10.rs	Adds helper contracts, mathematical predicates, and shared proof macros.

_{Review effort: Balanced}

[v3risec]

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.

[feliperodri]

This solves Challenge 30. All four success criteria are met: contracts on every listed function with a reference check for the exact result (log2_correct uses a guarded shift, log10_correct the powers of ten, and neither calls the code under test), None for zero and negative inputs, panics for ilog2/ilog10 on those inputs, and Kani's overflow and intrinsic checks along every path. No function body changes.

What I checked locally, with the pinned Kani (c5e65fd):

• All 101 harnesses pass (77 contract proofs, 24 panic proofs), each in 7 s or less.
• Mutation testing: I injected 6 bugs into the implementation (boundary constants in u8_impl and less_than_5, the 10^10 branch in u64_impl, log += 31 in u128_impl, signed checked_ilog2 letting 0 reach ctlz_nonzero, and the signed ilog10 wrapper accepting 0). Every one makes harnesses fail, and only the ones on the affected paths (39, 22, 8, 8, 12 and 17 failures).
• The covers are satisfied, including the one after the call in each contract proof, so the proofs aren't vacuous.
• Using safety_check(false) after the call in the panic harnesses is the right choice: it stops should_panic from passing just because a different assertion fails.

One note, not blocking: "Producing an invalid value" is on the UB list, and CI doesn't enable -Z valid-value-checks. You ran it locally, which helps. How Kani-based solutions are judged on this item is being decided in #733, the same for every challenge.

Thanks for the careful work.