Skip to content

New challenge: Safety and correctness of integer logarithms - #729

Open
Kieran-Hulsman wants to merge 1 commit into
model-checking:mainfrom
Kieran-Hulsman:kieran/ilog-challenge-proposal
Open

Kieran-Hulsman wants to merge 1 commit into
model-checking:mainfrom
Kieran-Hulsman:kieran/ilog-challenge-proposal

Conversation

@Kieran-Hulsman

Copy link
Copy Markdown

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

Copy link
Copy Markdown
Author

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 feliperodri self-assigned this Oct 20, 2026
@feliperodri feliperodri added the Challenge Proposal Used to tag a challenge proposal PR / Issue label Oct 20, 2026

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Challenge Proposal Used to tag a challenge proposal PR / Issue

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants