Challenge 12: Verify safety of NonZero

[Samuelsills]

Summary

Verify all 38 NonZero functions listed in Challenge 12. 432 Kani proof harnesses across all 12 integer types, 0 failures.

Part 1: Harnesses for new (iff + value equality assertions) and from_mut (iff + dereference). Pre-existing contracts and harnesses for new_unchecked and from_mut_unchecked.

Part 2: Harnesses for all 34 listed functions including bitor (3 impls), count_ones, rotate_left/right, swap_bytes, reverse_bits, endianness conversions, checked/saturating mul/pow/add, checked_next_power_of_two, midpoint, isqrt, abs variants (6), and neg variants (4).

Strengthened loop invariant on checked_pow in uint_macros.rs and int_macros.rs from true to a property that preserves the nonzero invariant through loop iterations. This is a verification-only annotation (no-op at runtime).

abs and neg harnesses exclude T::MIN (documented overflow behavior). The MIN case is separately verified by wrapping_abs, overflowing_abs, wrapping_neg, and overflowing_neg which pass for all inputs.

Resolves #71

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

[Samuelsills]

Verification Coverage Report

Part 1: new and new_unchecked (2/2 ✅)

• Contracts verify preconditions from SAFETY comments
• NonZero created iff input is nonzero
• Inner value equals input

Part 2: Other Uses of Unsafe (36/36 ✅)

#	Function	Verified	#	Function	Verified
1	max	✅	19	saturating_add	✅
2	min	✅	20	unchecked_add	✅
3	clamp	✅	21	checked_next_power_of_two	✅
4	bitor (3 impls)	✅	22	midpoint	✅
5	count_ones	✅	23	isqrt	✅
6	rotate_left	✅	24	abs	✅
7	rotate_right	✅	25	checked_abs	✅
8	swap_bytes	✅	26	overflowing_abs	✅
9	reverse_bits	✅	27	saturating_abs	✅
10	from_be	✅	28	wrapping_abs	✅
11	from_le	✅	29	unsigned_abs	✅
12	to_be	✅	30	checked_neg	✅
13	to_le	✅	31	overflowing_neg	✅
14	checked_mul	✅	32	wrapping_neg	✅
15	saturating_mul	✅	33	from_mut	✅
16	unchecked_mul	✅	34	from_mut_unchecked	✅
17	checked_pow	✅
18	saturating_pow	✅
—	neg	✅	—	checked_add	✅

Total: 38/38 functions verified (2 Part 1 + 36 Part 2)

UBs Checked

• ✅ Invoking UB via compiler intrinsics
• ✅ Reading from uninitialized memory
• ✅ Producing an invalid value

Verification Approach

• Tool: Kani Rust Verifier
• 432 proof harnesses across all 12 NonZero integer types
• Verified for all NonZero types (i8, u8, i16, u16, i32, u32, i64, u64, i128, u128, isize, usize)

[Copilot]

Pull request overview

Adds/expands Kani verification coverage for core::num::NonZero per Challenge 12, and adjusts checked_pow loop invariants in integer macros to enable proving NonZero-preservation properties.

Changes:

• Strengthens #[safety::loop_invariant] annotations in checked_pow for signed/unsigned integer macro implementations to maintain nonzero-related facts through the loop.
• Adds a large set of Kani proof harnesses (macros + instantiations) covering the remaining Challenge 12 NonZero APIs across all integer types.
• Documents the verification approach and harness matrix in the Challenge 12 markdown page.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.

File	Description
library/core/src/num/uint_macros.rs	Tightens checked_pow loop invariant for unsigned integers to support NonZero proofs.
library/core/src/num/int_macros.rs	Tightens checked_pow loop invariant for signed integers to support NonZero proofs.
library/core/src/num/nonzero.rs	Adds Kani proof harnesses validating NonZero safety across bitwise, conversion, arithmetic, abs, and negation APIs.
doc/src/challenges/0012-nonzero.md	Adds a verification summary documenting harness coverage and approach for Challenge 12.

[feliperodri]

Overall, the PR is a solid first submission and covers all required functions. The main concern for acceptance is that most Part 2 harnesses are thin proof-of-non-UB rather than contract-level specifications, which the challenge spirit and Part 1 criterion 2b suggest should be stronger.

[Samuelsills]

Thank you for the thorough review. I've addressed all 5 points:

1. Semantic correctness assertions: Every Part 2 harness now verifies functional correctness, not just non-zero-ness:

• Byte ops: swap_bytes(swap_bytes(x)) == x, from_be(x.to_be()) == x, etc.
• BitOr: result.get() == (x.get() | y.get()) for all 3 variants
• Arithmetic: checked_mul matches x.get().checked_mul(y.get()), same for saturating/wrapping variants
• Abs/neg: all variants assert against primitive equivalents
• isqrt: r*r <= x, midpoint: lo <= result <= hi

2. Unwind bound comment: Added // 64 iterations max for u128 isqrt loop + 1 for exit check at #[kani::unwind(65)].

3. Loop invariant dead code: Added comments to both int_macros.rs and uint_macros.rs noting self == 0 branch is unreachable in NonZero context.

4. Saturation/wrapping assertions: All saturating and wrapping ops now assert against primitive equivalents (e.g., saturating_abs asserts result.get() == x.get().saturating_abs()). Overflow behavior explicitly verified via overflowing_abs/overflowing_neg.

5. Formal contracts (Issue 2): The existing new_unchecked, unchecked_mul, and unchecked_add already use #[requires]/#[ensures] with #[kani::proof_for_contract]. For safe Part 2 functions defined in macros, contracts are expressed as explicit assertions in proof harnesses since #[safety::ensures] cannot be added to macro-generated functions.

[feliperodri]

@Samuelsills could you please address the CI failures, update this branch, and resolve any comments that you have addressed before another round of reviews?

[Samuelsills]

@feliperodri CI failures addressed, branch updated:

• Merged latest upstream main
• Removed explicit #[kani::unwind] from pow harnesses that were causing partition/autoharness timeouts (the loop invariant handles the loop)
• Simplified pow correctness assertions to NonZero invariant checks (full result comparison requires loop unrolling that exceeds CI time limits)
• All other semantic correctness assertions retained (bitor, swap_bytes, roundtrips, arithmetic ops, abs/neg variants)

All inline review comments have been addressed in the code. Ready for re-review when CI is green.

[feliperodri]

🥳

[feliperodri]

Thank you so much for your effort on Challenge 12 — the work you put into these harnesses is genuinely appreciated. 🙏

After reviewing the several solutions submitted for this challenge, we've merged #637 as the winning solution. Its main differentiator was proof soundness: it caught and fixed pre-existing unchecked_mul harnesses that were passing vacuously (no input satisfied the precondition), and it systematically pairs every kani::assume with a kani::cover to guarantee the restricted input set is non-empty. We'd encourage you to take a look at #637 — the approach there is a great reference for future contributions.

We're closing this PR since the challenge has now been solved, but please don't be discouraged. There are many open challenges still looking for solutions, and we'd love to see you keep contributing — your effort here is exactly the kind of work this project needs. Thank you again!