[Kieran-Hulsman]

Proposes a challenge to verify the safety and correctness of ilog10, ilog2, their checked variants, and unsigned NonZero::ilog2, including the internal decimal-logarithm calculations and unsafe assertions.

Adds the challenge document and its book entry.

Tracking issue: #728

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

[Kieran-Hulsman]

The macOS Kani Metrics failure matches model-checking/kani#4963, fixed by model-checking/kani#4964. The Kani pin update is included in #727. I’ll update this branch once that lands and rerun CI.

[feliperodri]

This is a well-scoped challenge: the target code has real unsafe obligations (assert_unchecked result bounds in int_log10, intrinsics::ctlz_nonzero in signed checked_ilog2, NonZero::new_unchecked in the usize wrapper), none of it is covered by an existing challenge or harness, and the success criteria are concrete and checkable. The exclusion of arbitrary-base ilog is argued, and the helpers' input domains are documented in the source, so "each helper's documented input domain" is well defined.

I checked feasibility before reviewing the criteria. With Kani 0.68.0, proving the full correctness criterion (b^r <= n < b^(r+1), None for non-positive inputs) over every input takes 1 s for u128/i128 checked_ilog2, 2 s for u64 checked_ilog10, and 18–19 s for u128/i128 checked_ilog10. So no bounds are needed and the CI cost is small. I ran this on the public methods with Kani's bundled std, not as contracts on the internal helpers in this repo.

Three things block approval (inline comments): NonZero::ilog10 is missing from the target list, the challenge number 30 is also used by #592, and the template's Start date field is missing. The other comments are suggestions.

What would flip this to approval:

1. Add NonZero<T>::ilog10 to the target table.
2. Renumber if #592 merges first (file name, title and SUMMARY.md).
3. Add the Start date field.

The usize width question and the UB-list trim are worth doing but don't block.

[feliperodri]

@patricklam could you take a look at this proposal as well?

[patricklam]

@feliperodri I should declare a conflict of interest on reviewing this; Kieran is working with me.

[feliperodri]

Does one of you have some bandwidth to review this proposed challenge? @rafaelsamenezes, @lucasccordeiro, @DiuDiu777

[DiuDiu777]

I've gone through the proposal, and the scope and acceptance criteria look clear. The boundary with the existing challenges also makes sense.

I don't have any further comments.