Verify safety of NonZero operations (Challenge 12)

[jrey8343]

Summary

Resolves #71 (Challenge 12: Safety of NonZero)

Adds 376 new Kani verification harnesses for all remaining NonZero functions specified in the challenge, covering:

• Bit operations: count_ones, swap_bytes, reverse_bits, rotate_left, rotate_right (12 types each)
• Byte order: from_be, from_le, to_be, to_le (12 types each)
• Bitor: all 3 implementations — NonZero|NonZero, NonZero|T, T|NonZero (12 types each)
• Checked/saturating arithmetic: checked_mul, saturating_mul, checked_add, saturating_add (unsigned-only for add)
• Power operations: checked_pow, saturating_pow (12 types each)
• Unsigned-only: checked_next_power_of_two, midpoint, isqrt
• Signed-only: neg, abs, checked_abs, overflowing_abs, saturating_abs, wrapping_abs, unsigned_abs, checked_neg, overflowing_neg, wrapping_neg
• Reference: from_mut

Changes

• library/core/src/num/nonzero.rs: 376 new verification harnesses in mod verify
• library/core/src/num/uint_macros.rs: Remove trivial #[safety::loop_invariant(true)] from checked_pow that caused CBMC assigns check interference with NonZero::new_unchecked verification
• library/core/src/num/int_macros.rs: Same loop_invariant removal for signed types

Verification

All 385 harnesses pass (376 new + 9 existing):

Manual Harness Summary:
Complete - 385 successfully verified harnesses, 0 failures, 385 total.

Run with:

./scripts/run-kani.sh --kani-args --harness nonzero_check -p core --features core/kani

[jrey8343]

CI is passing — ready for review.

[Copilot]

Pull request overview

This PR expands Kani-based verification coverage for core::num::NonZero* operations (Challenge 12), and adjusts checked_pow implementations to avoid CBMC/Kani interference from a trivial loop-invariant annotation.

Changes:

• Add a large set of new Kani verification harnesses under core::num::nonzero::verify for many remaining NonZero operations (bit ops, byte-order, bitor, arithmetic, pow, signed/unsigned-only ops, and from_mut).
• Remove #[safety::loop_invariant(true)] from checked_pow loops in both unsigned and signed integer macro implementations to prevent CBMC assigns-check interference during verification.
• Add bounded-unwind / bounded-exponent variants for 128-bit pow harnesses to keep verification tractable.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
library/core/src/num/nonzero.rs	Adds many new Kani harnesses for NonZero* APIs in mod verify.
library/core/src/num/uint_macros.rs	Removes a trivial loop-invariant annotation from checked_pow’s loop.
library/core/src/num/int_macros.rs	Removes the same trivial loop-invariant annotation from signed checked_pow.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

NonZero::isqrt() is implemented for all unsigned nonzero types (u8/u16/u32/u64/u128/usize), but the verification harnesses here only cover u8/u16/u32. If the goal is to verify all remaining NonZero operations across all integer widths, add harnesses for NonZeroU64/NonZeroU128/NonZeroUsize as well (or document/encode an explicit bound or performance rationale for excluding the wider types).

Suggested change

	nonzero_check_isqrt!(core::num::NonZeroU32, nonzero_check_isqrt_u32);
	nonzero_check_isqrt!(core::num::NonZeroU32, nonzero_check_isqrt_u32);
	nonzero_check_isqrt!(core::num::NonZeroU64, nonzero_check_isqrt_u64);
	nonzero_check_isqrt!(core::num::NonZeroU128, nonzero_check_isqrt_u128);
	nonzero_check_isqrt!(core::num::NonZeroUsize, nonzero_check_isqrt_usize);