From 71e54d04931c563a15793aaa7d5ce5ec06c7e816 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Tue, 24 Mar 2026 18:01:26 +0100 Subject: [PATCH 1/4] Challenge 12: Verify safety of NonZero Verify all 38 NonZero functions listed in the challenge specification. 432 Kani proof harnesses across all 12 integer types, 0 failures. 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. --- doc/src/challenges/0012-nonzero.md | 70 +++ library/core/src/num/int_macros.rs | 2 +- library/core/src/num/nonzero.rs | 843 ++++++++++++++++++++++++++++ library/core/src/num/uint_macros.rs | 2 +- 4 files changed, 915 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index 2c48386dfdb3c..10e6d8edecd8a 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -85,3 +85,73 @@ code, all proofs must automatically ensure the absence of the following undefine Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) in addition to the ones listed above. + +------------------- + +## Verification Summary + +All 38 functions verified using Kani proof harnesses. 432 total harnesses pass across all 12 integer types. + +### Part 1: Core Creation + +| Function | Harness | Types | Approach | +|----------|---------|-------|----------| +| `new` | `nonzero_check_new` | all 12 | `#[kani::proof]` — proves iff: `result.is_some() == (n != 0)` and `nz.get() == n` | +| `new_unchecked` | `nonzero_check` (pre-existing) | all 12 | `#[kani::proof_for_contract]` — verifies `#[requires]` + `#[ensures]` | +| `from_mut` | `nonzero_check_from_mut` | all 12 | `#[kani::proof]` — proves iff + dereferences returned reference | +| `from_mut_unchecked` | `nonzero_check_from_mut_unchecked` (pre-existing) | all 12 | `#[kani::proof_for_contract]` — verifies `#[requires]` | + +### Part 2: Bitwise & Conversion + +| Function | Harness | Types | +|----------|---------|-------| +| `bitor` (NZ\|NZ) | `nonzero_check_bitor_nznz` | all 12 | +| `bitor` (NZ\|T) | `nonzero_check_bitor_nzt` | all 12 | +| `bitor` (T\|NZ) | `nonzero_check_bitor_tnz` | all 12 | +| `count_ones` | `nonzero_check_count_ones` | all 12 | +| `rotate_left` | `nonzero_check_rotate_left` | all 12 | +| `rotate_right` | `nonzero_check_rotate_right` | all 12 | +| `swap_bytes` | `nonzero_check_swap_bytes` | all 12 | +| `reverse_bits` | `nonzero_check_reverse_bits` | all 12 | +| `from_be` | `nonzero_check_from_be` | all 12 | +| `from_le` | `nonzero_check_from_le` | all 12 | +| `to_be` | `nonzero_check_to_be` | all 12 | +| `to_le` | `nonzero_check_to_le` | all 12 | + +### Part 2: Arithmetic + +| Function | Harness | Types | Notes | +|----------|---------|-------|-------| +| `checked_mul` | `nonzero_check_checked_mul` | all 12 | | +| `saturating_mul` | `nonzero_check_saturating_mul` | all 12 | | +| `unchecked_mul` | `check_mul_unchecked_*` (pre-existing) | all 12 | `proof_for_contract` with interval testing | +| `checked_pow` | `nonzero_check_checked_pow` | all 12 | Required strengthened loop invariant | +| `saturating_pow` | `nonzero_check_saturating_pow` | all 12 | Required strengthened loop invariant | +| `checked_add` | `nonzero_check_checked_add` | 6 unsigned | | +| `saturating_add` | `nonzero_check_saturating_add` | 6 unsigned | | +| `unchecked_add` | `nonzero_check_add` (pre-existing) | 6 unsigned | `proof_for_contract` | +| `checked_next_power_of_two` | `nonzero_check_checked_next_power_of_two` | 6 unsigned | | +| `midpoint` | `nonzero_check_midpoint` | 6 unsigned | | +| `isqrt` | `nonzero_check_isqrt` | 6 unsigned | `#[kani::unwind(65)]` | + +### Part 2: Absolute Value & Negation (signed only) + +| Function | Harness | Types | Notes | +|----------|---------|-------|-------| +| `abs` | `nonzero_check_abs` | 6 signed | Excludes MIN (documented overflow) | +| `checked_abs` | `nonzero_check_checked_abs` | 6 signed | | +| `overflowing_abs` | `nonzero_check_overflowing_abs` | 6 signed | | +| `saturating_abs` | `nonzero_check_saturating_abs` | 6 signed | | +| `wrapping_abs` | `nonzero_check_wrapping_abs` | 6 signed | Covers MIN | +| `unsigned_abs` | `nonzero_check_unsigned_abs` | 6 signed | | +| `neg` | `nonzero_check_neg` | 6 signed | Excludes MIN (documented overflow) | +| `checked_neg` | `nonzero_check_checked_neg` | 6 signed | | +| `overflowing_neg` | `nonzero_check_overflowing_neg` | 6 signed | Covers MIN | +| `wrapping_neg` | `nonzero_check_wrapping_neg` | 6 signed | Covers MIN | +| `max` | `nonzero_check_max` (pre-existing) | all 12 | | +| `min` | `nonzero_check_min` (pre-existing) | all 12 | | +| `clamp` | `nonzero_check_clamp` (pre-existing) | all 12 | | + +### Additional Changes + +Strengthened `#[safety::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 annotation fix, not a runtime logic change. diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 4468c1489bfb5..680311ae5678a 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -1736,7 +1736,7 @@ macro_rules! int_impl { let mut base = self; let mut acc: Self = 1; - #[safety::loop_invariant(true)] + #[safety::loop_invariant(self == 0 || (acc != 0 && base != 0))] loop { if (exp & 1) == 1 { acc = try_opt!(acc.checked_mul(base)); diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 9c9d3a136a1e0..5b425c37b41d8 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -3025,4 +3025,847 @@ mod verify { nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64); nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128); nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize); + + // ===================================================================== + // Bitwise & Conversion Operations + // ===================================================================== + + // --- bitor (NonZero | NonZero) --- + macro_rules! nonzero_check_bitor_nznz { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x | y; + let _ = result.get(); + } + }; + } + + nonzero_check_bitor_nznz!(core::num::NonZeroI8, nonzero_check_bitor_nznz_for_i8); + nonzero_check_bitor_nznz!(core::num::NonZeroI16, nonzero_check_bitor_nznz_for_i16); + nonzero_check_bitor_nznz!(core::num::NonZeroI32, nonzero_check_bitor_nznz_for_i32); + nonzero_check_bitor_nznz!(core::num::NonZeroI64, nonzero_check_bitor_nznz_for_i64); + nonzero_check_bitor_nznz!(core::num::NonZeroI128, nonzero_check_bitor_nznz_for_i128); + nonzero_check_bitor_nznz!(core::num::NonZeroIsize, nonzero_check_bitor_nznz_for_isize); + nonzero_check_bitor_nznz!(core::num::NonZeroU8, nonzero_check_bitor_nznz_for_u8); + nonzero_check_bitor_nznz!(core::num::NonZeroU16, nonzero_check_bitor_nznz_for_u16); + nonzero_check_bitor_nznz!(core::num::NonZeroU32, nonzero_check_bitor_nznz_for_u32); + nonzero_check_bitor_nznz!(core::num::NonZeroU64, nonzero_check_bitor_nznz_for_u64); + nonzero_check_bitor_nznz!(core::num::NonZeroU128, nonzero_check_bitor_nznz_for_u128); + nonzero_check_bitor_nznz!(core::num::NonZeroUsize, nonzero_check_bitor_nznz_for_usize); + + // --- bitor (NonZero | T) --- + macro_rules! nonzero_check_bitor_nzt { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let y: $t = kani::any(); + let result = x | y; + let _ = result.get(); + } + }; + } + + nonzero_check_bitor_nzt!(i8, core::num::NonZeroI8, nonzero_check_bitor_nzt_for_i8); + nonzero_check_bitor_nzt!(i16, core::num::NonZeroI16, nonzero_check_bitor_nzt_for_i16); + nonzero_check_bitor_nzt!(i32, core::num::NonZeroI32, nonzero_check_bitor_nzt_for_i32); + nonzero_check_bitor_nzt!(i64, core::num::NonZeroI64, nonzero_check_bitor_nzt_for_i64); + nonzero_check_bitor_nzt!(i128, core::num::NonZeroI128, nonzero_check_bitor_nzt_for_i128); + nonzero_check_bitor_nzt!(isize, core::num::NonZeroIsize, nonzero_check_bitor_nzt_for_isize); + nonzero_check_bitor_nzt!(u8, core::num::NonZeroU8, nonzero_check_bitor_nzt_for_u8); + nonzero_check_bitor_nzt!(u16, core::num::NonZeroU16, nonzero_check_bitor_nzt_for_u16); + nonzero_check_bitor_nzt!(u32, core::num::NonZeroU32, nonzero_check_bitor_nzt_for_u32); + nonzero_check_bitor_nzt!(u64, core::num::NonZeroU64, nonzero_check_bitor_nzt_for_u64); + nonzero_check_bitor_nzt!(u128, core::num::NonZeroU128, nonzero_check_bitor_nzt_for_u128); + nonzero_check_bitor_nzt!(usize, core::num::NonZeroUsize, nonzero_check_bitor_nzt_for_usize); + + // --- bitor (T | NonZero) --- + macro_rules! nonzero_check_bitor_tnz { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $t = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x | y; + let _ = result.get(); + } + }; + } + + nonzero_check_bitor_tnz!(i8, core::num::NonZeroI8, nonzero_check_bitor_tnz_for_i8); + nonzero_check_bitor_tnz!(i16, core::num::NonZeroI16, nonzero_check_bitor_tnz_for_i16); + nonzero_check_bitor_tnz!(i32, core::num::NonZeroI32, nonzero_check_bitor_tnz_for_i32); + nonzero_check_bitor_tnz!(i64, core::num::NonZeroI64, nonzero_check_bitor_tnz_for_i64); + nonzero_check_bitor_tnz!(i128, core::num::NonZeroI128, nonzero_check_bitor_tnz_for_i128); + nonzero_check_bitor_tnz!(isize, core::num::NonZeroIsize, nonzero_check_bitor_tnz_for_isize); + nonzero_check_bitor_tnz!(u8, core::num::NonZeroU8, nonzero_check_bitor_tnz_for_u8); + nonzero_check_bitor_tnz!(u16, core::num::NonZeroU16, nonzero_check_bitor_tnz_for_u16); + nonzero_check_bitor_tnz!(u32, core::num::NonZeroU32, nonzero_check_bitor_tnz_for_u32); + nonzero_check_bitor_tnz!(u64, core::num::NonZeroU64, nonzero_check_bitor_tnz_for_u64); + nonzero_check_bitor_tnz!(u128, core::num::NonZeroU128, nonzero_check_bitor_tnz_for_u128); + nonzero_check_bitor_tnz!(usize, core::num::NonZeroUsize, nonzero_check_bitor_tnz_for_usize); + + // --- count_ones --- + macro_rules! nonzero_check_count_ones { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.count_ones(); + assert!(result.get() > 0); + } + }; + } + + nonzero_check_count_ones!(core::num::NonZeroI8, nonzero_check_count_ones_for_i8); + nonzero_check_count_ones!(core::num::NonZeroI16, nonzero_check_count_ones_for_i16); + nonzero_check_count_ones!(core::num::NonZeroI32, nonzero_check_count_ones_for_i32); + nonzero_check_count_ones!(core::num::NonZeroI64, nonzero_check_count_ones_for_i64); + nonzero_check_count_ones!(core::num::NonZeroI128, nonzero_check_count_ones_for_i128); + nonzero_check_count_ones!(core::num::NonZeroIsize, nonzero_check_count_ones_for_isize); + nonzero_check_count_ones!(core::num::NonZeroU8, nonzero_check_count_ones_for_u8); + nonzero_check_count_ones!(core::num::NonZeroU16, nonzero_check_count_ones_for_u16); + nonzero_check_count_ones!(core::num::NonZeroU32, nonzero_check_count_ones_for_u32); + nonzero_check_count_ones!(core::num::NonZeroU64, nonzero_check_count_ones_for_u64); + nonzero_check_count_ones!(core::num::NonZeroU128, nonzero_check_count_ones_for_u128); + nonzero_check_count_ones!(core::num::NonZeroUsize, nonzero_check_count_ones_for_usize); + + // --- rotate_left --- + macro_rules! nonzero_check_rotate_left { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let n: u32 = kani::any(); + let result = x.rotate_left(n); + assert!(result.rotate_right(n) == x); + } + }; + } + + nonzero_check_rotate_left!(core::num::NonZeroI8, nonzero_check_rotate_left_for_i8); + nonzero_check_rotate_left!(core::num::NonZeroI16, nonzero_check_rotate_left_for_i16); + nonzero_check_rotate_left!(core::num::NonZeroI32, nonzero_check_rotate_left_for_i32); + nonzero_check_rotate_left!(core::num::NonZeroI64, nonzero_check_rotate_left_for_i64); + nonzero_check_rotate_left!(core::num::NonZeroI128, nonzero_check_rotate_left_for_i128); + nonzero_check_rotate_left!(core::num::NonZeroIsize, nonzero_check_rotate_left_for_isize); + nonzero_check_rotate_left!(core::num::NonZeroU8, nonzero_check_rotate_left_for_u8); + nonzero_check_rotate_left!(core::num::NonZeroU16, nonzero_check_rotate_left_for_u16); + nonzero_check_rotate_left!(core::num::NonZeroU32, nonzero_check_rotate_left_for_u32); + nonzero_check_rotate_left!(core::num::NonZeroU64, nonzero_check_rotate_left_for_u64); + nonzero_check_rotate_left!(core::num::NonZeroU128, nonzero_check_rotate_left_for_u128); + nonzero_check_rotate_left!(core::num::NonZeroUsize, nonzero_check_rotate_left_for_usize); + + // --- rotate_right --- + macro_rules! nonzero_check_rotate_right { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let n: u32 = kani::any(); + let result = x.rotate_right(n); + assert!(result.rotate_left(n) == x); + } + }; + } + + nonzero_check_rotate_right!(core::num::NonZeroI8, nonzero_check_rotate_right_for_i8); + nonzero_check_rotate_right!(core::num::NonZeroI16, nonzero_check_rotate_right_for_i16); + nonzero_check_rotate_right!(core::num::NonZeroI32, nonzero_check_rotate_right_for_i32); + nonzero_check_rotate_right!(core::num::NonZeroI64, nonzero_check_rotate_right_for_i64); + nonzero_check_rotate_right!(core::num::NonZeroI128, nonzero_check_rotate_right_for_i128); + nonzero_check_rotate_right!(core::num::NonZeroIsize, nonzero_check_rotate_right_for_isize); + nonzero_check_rotate_right!(core::num::NonZeroU8, nonzero_check_rotate_right_for_u8); + nonzero_check_rotate_right!(core::num::NonZeroU16, nonzero_check_rotate_right_for_u16); + nonzero_check_rotate_right!(core::num::NonZeroU32, nonzero_check_rotate_right_for_u32); + nonzero_check_rotate_right!(core::num::NonZeroU64, nonzero_check_rotate_right_for_u64); + nonzero_check_rotate_right!(core::num::NonZeroU128, nonzero_check_rotate_right_for_u128); + nonzero_check_rotate_right!(core::num::NonZeroUsize, nonzero_check_rotate_right_for_usize); + + // --- swap_bytes --- + macro_rules! nonzero_check_swap_bytes { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.swap_bytes(); + let _ = result.get(); + } + }; + } + + nonzero_check_swap_bytes!(core::num::NonZeroI8, nonzero_check_swap_bytes_for_i8); + nonzero_check_swap_bytes!(core::num::NonZeroI16, nonzero_check_swap_bytes_for_i16); + nonzero_check_swap_bytes!(core::num::NonZeroI32, nonzero_check_swap_bytes_for_i32); + nonzero_check_swap_bytes!(core::num::NonZeroI64, nonzero_check_swap_bytes_for_i64); + nonzero_check_swap_bytes!(core::num::NonZeroI128, nonzero_check_swap_bytes_for_i128); + nonzero_check_swap_bytes!(core::num::NonZeroIsize, nonzero_check_swap_bytes_for_isize); + nonzero_check_swap_bytes!(core::num::NonZeroU8, nonzero_check_swap_bytes_for_u8); + nonzero_check_swap_bytes!(core::num::NonZeroU16, nonzero_check_swap_bytes_for_u16); + nonzero_check_swap_bytes!(core::num::NonZeroU32, nonzero_check_swap_bytes_for_u32); + nonzero_check_swap_bytes!(core::num::NonZeroU64, nonzero_check_swap_bytes_for_u64); + nonzero_check_swap_bytes!(core::num::NonZeroU128, nonzero_check_swap_bytes_for_u128); + nonzero_check_swap_bytes!(core::num::NonZeroUsize, nonzero_check_swap_bytes_for_usize); + + // --- reverse_bits --- + macro_rules! nonzero_check_reverse_bits { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.reverse_bits(); + let _ = result.get(); + } + }; + } + + nonzero_check_reverse_bits!(core::num::NonZeroI8, nonzero_check_reverse_bits_for_i8); + nonzero_check_reverse_bits!(core::num::NonZeroI16, nonzero_check_reverse_bits_for_i16); + nonzero_check_reverse_bits!(core::num::NonZeroI32, nonzero_check_reverse_bits_for_i32); + nonzero_check_reverse_bits!(core::num::NonZeroI64, nonzero_check_reverse_bits_for_i64); + nonzero_check_reverse_bits!(core::num::NonZeroI128, nonzero_check_reverse_bits_for_i128); + nonzero_check_reverse_bits!(core::num::NonZeroIsize, nonzero_check_reverse_bits_for_isize); + nonzero_check_reverse_bits!(core::num::NonZeroU8, nonzero_check_reverse_bits_for_u8); + nonzero_check_reverse_bits!(core::num::NonZeroU16, nonzero_check_reverse_bits_for_u16); + nonzero_check_reverse_bits!(core::num::NonZeroU32, nonzero_check_reverse_bits_for_u32); + nonzero_check_reverse_bits!(core::num::NonZeroU64, nonzero_check_reverse_bits_for_u64); + nonzero_check_reverse_bits!(core::num::NonZeroU128, nonzero_check_reverse_bits_for_u128); + nonzero_check_reverse_bits!(core::num::NonZeroUsize, nonzero_check_reverse_bits_for_usize); + + // --- from_be --- + macro_rules! nonzero_check_from_be { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = <$nonzero_type>::from_be(x); + let _ = result.get(); + } + }; + } + + nonzero_check_from_be!(core::num::NonZeroI8, nonzero_check_from_be_for_i8); + nonzero_check_from_be!(core::num::NonZeroI16, nonzero_check_from_be_for_i16); + nonzero_check_from_be!(core::num::NonZeroI32, nonzero_check_from_be_for_i32); + nonzero_check_from_be!(core::num::NonZeroI64, nonzero_check_from_be_for_i64); + nonzero_check_from_be!(core::num::NonZeroI128, nonzero_check_from_be_for_i128); + nonzero_check_from_be!(core::num::NonZeroIsize, nonzero_check_from_be_for_isize); + nonzero_check_from_be!(core::num::NonZeroU8, nonzero_check_from_be_for_u8); + nonzero_check_from_be!(core::num::NonZeroU16, nonzero_check_from_be_for_u16); + nonzero_check_from_be!(core::num::NonZeroU32, nonzero_check_from_be_for_u32); + nonzero_check_from_be!(core::num::NonZeroU64, nonzero_check_from_be_for_u64); + nonzero_check_from_be!(core::num::NonZeroU128, nonzero_check_from_be_for_u128); + nonzero_check_from_be!(core::num::NonZeroUsize, nonzero_check_from_be_for_usize); + + // --- from_le --- + macro_rules! nonzero_check_from_le { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = <$nonzero_type>::from_le(x); + let _ = result.get(); + } + }; + } + + nonzero_check_from_le!(core::num::NonZeroI8, nonzero_check_from_le_for_i8); + nonzero_check_from_le!(core::num::NonZeroI16, nonzero_check_from_le_for_i16); + nonzero_check_from_le!(core::num::NonZeroI32, nonzero_check_from_le_for_i32); + nonzero_check_from_le!(core::num::NonZeroI64, nonzero_check_from_le_for_i64); + nonzero_check_from_le!(core::num::NonZeroI128, nonzero_check_from_le_for_i128); + nonzero_check_from_le!(core::num::NonZeroIsize, nonzero_check_from_le_for_isize); + nonzero_check_from_le!(core::num::NonZeroU8, nonzero_check_from_le_for_u8); + nonzero_check_from_le!(core::num::NonZeroU16, nonzero_check_from_le_for_u16); + nonzero_check_from_le!(core::num::NonZeroU32, nonzero_check_from_le_for_u32); + nonzero_check_from_le!(core::num::NonZeroU64, nonzero_check_from_le_for_u64); + nonzero_check_from_le!(core::num::NonZeroU128, nonzero_check_from_le_for_u128); + nonzero_check_from_le!(core::num::NonZeroUsize, nonzero_check_from_le_for_usize); + + // --- to_be --- + macro_rules! nonzero_check_to_be { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.to_be(); + let _ = result.get(); + } + }; + } + + nonzero_check_to_be!(core::num::NonZeroI8, nonzero_check_to_be_for_i8); + nonzero_check_to_be!(core::num::NonZeroI16, nonzero_check_to_be_for_i16); + nonzero_check_to_be!(core::num::NonZeroI32, nonzero_check_to_be_for_i32); + nonzero_check_to_be!(core::num::NonZeroI64, nonzero_check_to_be_for_i64); + nonzero_check_to_be!(core::num::NonZeroI128, nonzero_check_to_be_for_i128); + nonzero_check_to_be!(core::num::NonZeroIsize, nonzero_check_to_be_for_isize); + nonzero_check_to_be!(core::num::NonZeroU8, nonzero_check_to_be_for_u8); + nonzero_check_to_be!(core::num::NonZeroU16, nonzero_check_to_be_for_u16); + nonzero_check_to_be!(core::num::NonZeroU32, nonzero_check_to_be_for_u32); + nonzero_check_to_be!(core::num::NonZeroU64, nonzero_check_to_be_for_u64); + nonzero_check_to_be!(core::num::NonZeroU128, nonzero_check_to_be_for_u128); + nonzero_check_to_be!(core::num::NonZeroUsize, nonzero_check_to_be_for_usize); + + // --- to_le --- + macro_rules! nonzero_check_to_le { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.to_le(); + let _ = result.get(); + } + }; + } + + nonzero_check_to_le!(core::num::NonZeroI8, nonzero_check_to_le_for_i8); + nonzero_check_to_le!(core::num::NonZeroI16, nonzero_check_to_le_for_i16); + nonzero_check_to_le!(core::num::NonZeroI32, nonzero_check_to_le_for_i32); + nonzero_check_to_le!(core::num::NonZeroI64, nonzero_check_to_le_for_i64); + nonzero_check_to_le!(core::num::NonZeroI128, nonzero_check_to_le_for_i128); + nonzero_check_to_le!(core::num::NonZeroIsize, nonzero_check_to_le_for_isize); + nonzero_check_to_le!(core::num::NonZeroU8, nonzero_check_to_le_for_u8); + nonzero_check_to_le!(core::num::NonZeroU16, nonzero_check_to_le_for_u16); + nonzero_check_to_le!(core::num::NonZeroU32, nonzero_check_to_le_for_u32); + nonzero_check_to_le!(core::num::NonZeroU64, nonzero_check_to_le_for_u64); + nonzero_check_to_le!(core::num::NonZeroU128, nonzero_check_to_le_for_u128); + nonzero_check_to_le!(core::num::NonZeroUsize, nonzero_check_to_le_for_usize); + + // ===================================================================== + // Arithmetic Operations + Creation Wrappers + // ===================================================================== + + // --- checked_mul --- + macro_rules! nonzero_check_checked_mul { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.checked_mul(y); + if let Some(nz) = result { + let _ = nz.get(); + } + } + }; + } + + nonzero_check_checked_mul!(core::num::NonZeroI8, nonzero_check_checked_mul_for_i8); + nonzero_check_checked_mul!(core::num::NonZeroI16, nonzero_check_checked_mul_for_i16); + nonzero_check_checked_mul!(core::num::NonZeroI32, nonzero_check_checked_mul_for_i32); + nonzero_check_checked_mul!(core::num::NonZeroI64, nonzero_check_checked_mul_for_i64); + nonzero_check_checked_mul!(core::num::NonZeroI128, nonzero_check_checked_mul_for_i128); + nonzero_check_checked_mul!(core::num::NonZeroIsize, nonzero_check_checked_mul_for_isize); + nonzero_check_checked_mul!(core::num::NonZeroU8, nonzero_check_checked_mul_for_u8); + nonzero_check_checked_mul!(core::num::NonZeroU16, nonzero_check_checked_mul_for_u16); + nonzero_check_checked_mul!(core::num::NonZeroU32, nonzero_check_checked_mul_for_u32); + nonzero_check_checked_mul!(core::num::NonZeroU64, nonzero_check_checked_mul_for_u64); + nonzero_check_checked_mul!(core::num::NonZeroU128, nonzero_check_checked_mul_for_u128); + nonzero_check_checked_mul!(core::num::NonZeroUsize, nonzero_check_checked_mul_for_usize); + + // --- saturating_mul --- + macro_rules! nonzero_check_saturating_mul { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.saturating_mul(y); + let _ = result.get(); + } + }; + } + + nonzero_check_saturating_mul!(core::num::NonZeroI8, nonzero_check_saturating_mul_for_i8); + nonzero_check_saturating_mul!(core::num::NonZeroI16, nonzero_check_saturating_mul_for_i16); + nonzero_check_saturating_mul!(core::num::NonZeroI32, nonzero_check_saturating_mul_for_i32); + nonzero_check_saturating_mul!(core::num::NonZeroI64, nonzero_check_saturating_mul_for_i64); + nonzero_check_saturating_mul!(core::num::NonZeroI128, nonzero_check_saturating_mul_for_i128); + nonzero_check_saturating_mul!(core::num::NonZeroIsize, nonzero_check_saturating_mul_for_isize); + nonzero_check_saturating_mul!(core::num::NonZeroU8, nonzero_check_saturating_mul_for_u8); + nonzero_check_saturating_mul!(core::num::NonZeroU16, nonzero_check_saturating_mul_for_u16); + nonzero_check_saturating_mul!(core::num::NonZeroU32, nonzero_check_saturating_mul_for_u32); + nonzero_check_saturating_mul!(core::num::NonZeroU64, nonzero_check_saturating_mul_for_u64); + nonzero_check_saturating_mul!(core::num::NonZeroU128, nonzero_check_saturating_mul_for_u128); + nonzero_check_saturating_mul!(core::num::NonZeroUsize, nonzero_check_saturating_mul_for_usize); + + // --- checked_pow --- + macro_rules! nonzero_check_checked_pow { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let exp: u32 = kani::any(); + let result = x.checked_pow(exp); + if let Some(nz) = result { + let _ = nz.get(); + } + } + }; + } + + nonzero_check_checked_pow!(core::num::NonZeroI8, nonzero_check_checked_pow_for_i8); + nonzero_check_checked_pow!(core::num::NonZeroI16, nonzero_check_checked_pow_for_i16); + nonzero_check_checked_pow!(core::num::NonZeroI32, nonzero_check_checked_pow_for_i32); + nonzero_check_checked_pow!(core::num::NonZeroI64, nonzero_check_checked_pow_for_i64); + nonzero_check_checked_pow!(core::num::NonZeroI128, nonzero_check_checked_pow_for_i128); + nonzero_check_checked_pow!(core::num::NonZeroIsize, nonzero_check_checked_pow_for_isize); + nonzero_check_checked_pow!(core::num::NonZeroU8, nonzero_check_checked_pow_for_u8); + nonzero_check_checked_pow!(core::num::NonZeroU16, nonzero_check_checked_pow_for_u16); + nonzero_check_checked_pow!(core::num::NonZeroU32, nonzero_check_checked_pow_for_u32); + nonzero_check_checked_pow!(core::num::NonZeroU64, nonzero_check_checked_pow_for_u64); + nonzero_check_checked_pow!(core::num::NonZeroU128, nonzero_check_checked_pow_for_u128); + nonzero_check_checked_pow!(core::num::NonZeroUsize, nonzero_check_checked_pow_for_usize); + + // --- saturating_pow --- + macro_rules! nonzero_check_saturating_pow { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let exp: u32 = kani::any(); + let result = x.saturating_pow(exp); + let _ = result.get(); + } + }; + } + + nonzero_check_saturating_pow!(core::num::NonZeroI8, nonzero_check_saturating_pow_for_i8); + nonzero_check_saturating_pow!(core::num::NonZeroI16, nonzero_check_saturating_pow_for_i16); + nonzero_check_saturating_pow!(core::num::NonZeroI32, nonzero_check_saturating_pow_for_i32); + nonzero_check_saturating_pow!(core::num::NonZeroI64, nonzero_check_saturating_pow_for_i64); + nonzero_check_saturating_pow!(core::num::NonZeroI128, nonzero_check_saturating_pow_for_i128); + nonzero_check_saturating_pow!(core::num::NonZeroIsize, nonzero_check_saturating_pow_for_isize); + nonzero_check_saturating_pow!(core::num::NonZeroU8, nonzero_check_saturating_pow_for_u8); + nonzero_check_saturating_pow!(core::num::NonZeroU16, nonzero_check_saturating_pow_for_u16); + nonzero_check_saturating_pow!(core::num::NonZeroU32, nonzero_check_saturating_pow_for_u32); + nonzero_check_saturating_pow!(core::num::NonZeroU64, nonzero_check_saturating_pow_for_u64); + nonzero_check_saturating_pow!(core::num::NonZeroU128, nonzero_check_saturating_pow_for_u128); + nonzero_check_saturating_pow!(core::num::NonZeroUsize, nonzero_check_saturating_pow_for_usize); + + // --- checked_add (unsigned only) --- + macro_rules! nonzero_check_checked_add { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let y: $t = kani::any(); + let result = x.checked_add(y); + if let Some(nz) = result { + let _ = nz.get(); + } + } + }; + } + + nonzero_check_checked_add!(u8, core::num::NonZeroU8, nonzero_check_checked_add_for_u8); + nonzero_check_checked_add!(u16, core::num::NonZeroU16, nonzero_check_checked_add_for_u16); + nonzero_check_checked_add!(u32, core::num::NonZeroU32, nonzero_check_checked_add_for_u32); + nonzero_check_checked_add!(u64, core::num::NonZeroU64, nonzero_check_checked_add_for_u64); + nonzero_check_checked_add!(u128, core::num::NonZeroU128, nonzero_check_checked_add_for_u128); + nonzero_check_checked_add!(usize, core::num::NonZeroUsize, nonzero_check_checked_add_for_usize); + + // --- saturating_add (unsigned only) --- + macro_rules! nonzero_check_saturating_add { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let y: $t = kani::any(); + let result = x.saturating_add(y); + let _ = result.get(); + } + }; + } + + nonzero_check_saturating_add!(u8, core::num::NonZeroU8, nonzero_check_saturating_add_for_u8); + nonzero_check_saturating_add!(u16, core::num::NonZeroU16, nonzero_check_saturating_add_for_u16); + nonzero_check_saturating_add!(u32, core::num::NonZeroU32, nonzero_check_saturating_add_for_u32); + nonzero_check_saturating_add!(u64, core::num::NonZeroU64, nonzero_check_saturating_add_for_u64); + nonzero_check_saturating_add!( + u128, + core::num::NonZeroU128, + nonzero_check_saturating_add_for_u128 + ); + nonzero_check_saturating_add!( + usize, + core::num::NonZeroUsize, + nonzero_check_saturating_add_for_usize + ); + + // --- checked_next_power_of_two (unsigned only) --- + macro_rules! nonzero_check_checked_next_power_of_two { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.checked_next_power_of_two(); + if let Some(nz) = result { + let _ = nz.get(); + } + } + }; + } + + nonzero_check_checked_next_power_of_two!( + core::num::NonZeroU8, + nonzero_check_checked_next_power_of_two_for_u8 + ); + nonzero_check_checked_next_power_of_two!( + core::num::NonZeroU16, + nonzero_check_checked_next_power_of_two_for_u16 + ); + nonzero_check_checked_next_power_of_two!( + core::num::NonZeroU32, + nonzero_check_checked_next_power_of_two_for_u32 + ); + nonzero_check_checked_next_power_of_two!( + core::num::NonZeroU64, + nonzero_check_checked_next_power_of_two_for_u64 + ); + nonzero_check_checked_next_power_of_two!( + core::num::NonZeroU128, + nonzero_check_checked_next_power_of_two_for_u128 + ); + nonzero_check_checked_next_power_of_two!( + core::num::NonZeroUsize, + nonzero_check_checked_next_power_of_two_for_usize + ); + + // --- midpoint (unsigned only) --- + macro_rules! nonzero_check_midpoint { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.midpoint(y); + let _ = result.get(); + } + }; + } + + nonzero_check_midpoint!(core::num::NonZeroU8, nonzero_check_midpoint_for_u8); + nonzero_check_midpoint!(core::num::NonZeroU16, nonzero_check_midpoint_for_u16); + nonzero_check_midpoint!(core::num::NonZeroU32, nonzero_check_midpoint_for_u32); + nonzero_check_midpoint!(core::num::NonZeroU64, nonzero_check_midpoint_for_u64); + nonzero_check_midpoint!(core::num::NonZeroU128, nonzero_check_midpoint_for_u128); + nonzero_check_midpoint!(core::num::NonZeroUsize, nonzero_check_midpoint_for_usize); + + // --- isqrt (unsigned only) --- + macro_rules! nonzero_check_isqrt { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + #[kani::unwind(65)] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.isqrt(); + let _ = result.get(); + } + }; + } + + nonzero_check_isqrt!(core::num::NonZeroU8, nonzero_check_isqrt_for_u8); + nonzero_check_isqrt!(core::num::NonZeroU16, nonzero_check_isqrt_for_u16); + nonzero_check_isqrt!(core::num::NonZeroU32, nonzero_check_isqrt_for_u32); + nonzero_check_isqrt!(core::num::NonZeroU64, nonzero_check_isqrt_for_u64); + nonzero_check_isqrt!(core::num::NonZeroU128, nonzero_check_isqrt_for_u128); + nonzero_check_isqrt!(core::num::NonZeroUsize, nonzero_check_isqrt_for_usize); + + // --- new (Part 1: iff assertion) --- + macro_rules! nonzero_check_new { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let n: $t = kani::any(); + let result = <$nonzero_type>::new(n); + assert!(result.is_some() == (n != 0)); + if let Some(nz) = result { + assert!(nz.get() == n); + } + } + }; + } + + nonzero_check_new!(i8, core::num::NonZeroI8, nonzero_check_new_for_i8); + nonzero_check_new!(i16, core::num::NonZeroI16, nonzero_check_new_for_i16); + nonzero_check_new!(i32, core::num::NonZeroI32, nonzero_check_new_for_i32); + nonzero_check_new!(i64, core::num::NonZeroI64, nonzero_check_new_for_i64); + nonzero_check_new!(i128, core::num::NonZeroI128, nonzero_check_new_for_i128); + nonzero_check_new!(isize, core::num::NonZeroIsize, nonzero_check_new_for_isize); + nonzero_check_new!(u8, core::num::NonZeroU8, nonzero_check_new_for_u8); + nonzero_check_new!(u16, core::num::NonZeroU16, nonzero_check_new_for_u16); + nonzero_check_new!(u32, core::num::NonZeroU32, nonzero_check_new_for_u32); + nonzero_check_new!(u64, core::num::NonZeroU64, nonzero_check_new_for_u64); + nonzero_check_new!(u128, core::num::NonZeroU128, nonzero_check_new_for_u128); + nonzero_check_new!(usize, core::num::NonZeroUsize, nonzero_check_new_for_usize); + + // --- from_mut (Part 1: iff assertion + dereference) --- + macro_rules! nonzero_check_from_mut { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let mut n: $t = kani::any(); + let original = n; + let result = <$nonzero_type>::from_mut(&mut n); + assert!(result.is_some() == (original != 0)); + if let Some(nz_ref) = result { + assert!(nz_ref.get() == original); + } + } + }; + } + + nonzero_check_from_mut!(i8, core::num::NonZeroI8, nonzero_check_from_mut_for_i8); + nonzero_check_from_mut!(i16, core::num::NonZeroI16, nonzero_check_from_mut_for_i16); + nonzero_check_from_mut!(i32, core::num::NonZeroI32, nonzero_check_from_mut_for_i32); + nonzero_check_from_mut!(i64, core::num::NonZeroI64, nonzero_check_from_mut_for_i64); + nonzero_check_from_mut!(i128, core::num::NonZeroI128, nonzero_check_from_mut_for_i128); + nonzero_check_from_mut!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_for_isize); + nonzero_check_from_mut!(u8, core::num::NonZeroU8, nonzero_check_from_mut_for_u8); + nonzero_check_from_mut!(u16, core::num::NonZeroU16, nonzero_check_from_mut_for_u16); + nonzero_check_from_mut!(u32, core::num::NonZeroU32, nonzero_check_from_mut_for_u32); + nonzero_check_from_mut!(u64, core::num::NonZeroU64, nonzero_check_from_mut_for_u64); + nonzero_check_from_mut!(u128, core::num::NonZeroU128, nonzero_check_from_mut_for_u128); + nonzero_check_from_mut!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_for_usize); + + // ===================================================================== + // Signed Operations (abs, neg variants — signed types only) + // ===================================================================== + + // --- abs --- + // abs() uses #[rustc_inherit_overflow_checks] which panics on MIN in debug. + // The MIN case is verified separately by overflowing_abs/wrapping_abs harnesses. + macro_rules! nonzero_check_abs { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + kani::assume(x.get() != <$t>::MIN); + let result = x.abs(); + let _ = result.get(); + } + }; + } + + nonzero_check_abs!(i8, core::num::NonZeroI8, nonzero_check_abs_for_i8); + nonzero_check_abs!(i16, core::num::NonZeroI16, nonzero_check_abs_for_i16); + nonzero_check_abs!(i32, core::num::NonZeroI32, nonzero_check_abs_for_i32); + nonzero_check_abs!(i64, core::num::NonZeroI64, nonzero_check_abs_for_i64); + nonzero_check_abs!(i128, core::num::NonZeroI128, nonzero_check_abs_for_i128); + nonzero_check_abs!(isize, core::num::NonZeroIsize, nonzero_check_abs_for_isize); + + // --- checked_abs --- + macro_rules! nonzero_check_checked_abs { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.checked_abs(); + if let Some(nz) = result { + let _ = nz.get(); + } + } + }; + } + + nonzero_check_checked_abs!(core::num::NonZeroI8, nonzero_check_checked_abs_for_i8); + nonzero_check_checked_abs!(core::num::NonZeroI16, nonzero_check_checked_abs_for_i16); + nonzero_check_checked_abs!(core::num::NonZeroI32, nonzero_check_checked_abs_for_i32); + nonzero_check_checked_abs!(core::num::NonZeroI64, nonzero_check_checked_abs_for_i64); + nonzero_check_checked_abs!(core::num::NonZeroI128, nonzero_check_checked_abs_for_i128); + nonzero_check_checked_abs!(core::num::NonZeroIsize, nonzero_check_checked_abs_for_isize); + + // --- overflowing_abs --- + macro_rules! nonzero_check_overflowing_abs { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let (result, overflowed) = x.overflowing_abs(); + let _ = result.get(); + let _ = overflowed; + } + }; + } + + nonzero_check_overflowing_abs!(core::num::NonZeroI8, nonzero_check_overflowing_abs_for_i8); + nonzero_check_overflowing_abs!(core::num::NonZeroI16, nonzero_check_overflowing_abs_for_i16); + nonzero_check_overflowing_abs!(core::num::NonZeroI32, nonzero_check_overflowing_abs_for_i32); + nonzero_check_overflowing_abs!(core::num::NonZeroI64, nonzero_check_overflowing_abs_for_i64); + nonzero_check_overflowing_abs!(core::num::NonZeroI128, nonzero_check_overflowing_abs_for_i128); + nonzero_check_overflowing_abs!( + core::num::NonZeroIsize, + nonzero_check_overflowing_abs_for_isize + ); + + // --- saturating_abs --- + macro_rules! nonzero_check_saturating_abs { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.saturating_abs(); + let _ = result.get(); + } + }; + } + + nonzero_check_saturating_abs!(core::num::NonZeroI8, nonzero_check_saturating_abs_for_i8); + nonzero_check_saturating_abs!(core::num::NonZeroI16, nonzero_check_saturating_abs_for_i16); + nonzero_check_saturating_abs!(core::num::NonZeroI32, nonzero_check_saturating_abs_for_i32); + nonzero_check_saturating_abs!(core::num::NonZeroI64, nonzero_check_saturating_abs_for_i64); + nonzero_check_saturating_abs!(core::num::NonZeroI128, nonzero_check_saturating_abs_for_i128); + nonzero_check_saturating_abs!(core::num::NonZeroIsize, nonzero_check_saturating_abs_for_isize); + + // --- wrapping_abs --- + macro_rules! nonzero_check_wrapping_abs { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.wrapping_abs(); + let _ = result.get(); + } + }; + } + + nonzero_check_wrapping_abs!(core::num::NonZeroI8, nonzero_check_wrapping_abs_for_i8); + nonzero_check_wrapping_abs!(core::num::NonZeroI16, nonzero_check_wrapping_abs_for_i16); + nonzero_check_wrapping_abs!(core::num::NonZeroI32, nonzero_check_wrapping_abs_for_i32); + nonzero_check_wrapping_abs!(core::num::NonZeroI64, nonzero_check_wrapping_abs_for_i64); + nonzero_check_wrapping_abs!(core::num::NonZeroI128, nonzero_check_wrapping_abs_for_i128); + nonzero_check_wrapping_abs!(core::num::NonZeroIsize, nonzero_check_wrapping_abs_for_isize); + + // --- unsigned_abs --- + macro_rules! nonzero_check_unsigned_abs { + ($nonzero_type:ty, $unsigned_nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result: $unsigned_nonzero_type = x.unsigned_abs(); + let _ = result.get(); + } + }; + } + + nonzero_check_unsigned_abs!( + core::num::NonZeroI8, + core::num::NonZeroU8, + nonzero_check_unsigned_abs_for_i8 + ); + nonzero_check_unsigned_abs!( + core::num::NonZeroI16, + core::num::NonZeroU16, + nonzero_check_unsigned_abs_for_i16 + ); + nonzero_check_unsigned_abs!( + core::num::NonZeroI32, + core::num::NonZeroU32, + nonzero_check_unsigned_abs_for_i32 + ); + nonzero_check_unsigned_abs!( + core::num::NonZeroI64, + core::num::NonZeroU64, + nonzero_check_unsigned_abs_for_i64 + ); + nonzero_check_unsigned_abs!( + core::num::NonZeroI128, + core::num::NonZeroU128, + nonzero_check_unsigned_abs_for_i128 + ); + nonzero_check_unsigned_abs!( + core::num::NonZeroIsize, + core::num::NonZeroUsize, + nonzero_check_unsigned_abs_for_isize + ); + + // --- neg (Neg trait) --- + // neg() overflows on MIN (e.g. -(-128i8) = 128 > i8::MAX). + // The MIN case is verified by overflowing_neg/wrapping_neg harnesses. + macro_rules! nonzero_check_neg { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + kani::assume(x.get() != <$t>::MIN); + let result = -x; + let _ = result.get(); + } + }; + } + + nonzero_check_neg!(i8, core::num::NonZeroI8, nonzero_check_neg_for_i8); + nonzero_check_neg!(i16, core::num::NonZeroI16, nonzero_check_neg_for_i16); + nonzero_check_neg!(i32, core::num::NonZeroI32, nonzero_check_neg_for_i32); + nonzero_check_neg!(i64, core::num::NonZeroI64, nonzero_check_neg_for_i64); + nonzero_check_neg!(i128, core::num::NonZeroI128, nonzero_check_neg_for_i128); + nonzero_check_neg!(isize, core::num::NonZeroIsize, nonzero_check_neg_for_isize); + + // --- checked_neg --- + macro_rules! nonzero_check_checked_neg { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.checked_neg(); + if let Some(nz) = result { + let _ = nz.get(); + } + } + }; + } + + nonzero_check_checked_neg!(core::num::NonZeroI8, nonzero_check_checked_neg_for_i8); + nonzero_check_checked_neg!(core::num::NonZeroI16, nonzero_check_checked_neg_for_i16); + nonzero_check_checked_neg!(core::num::NonZeroI32, nonzero_check_checked_neg_for_i32); + nonzero_check_checked_neg!(core::num::NonZeroI64, nonzero_check_checked_neg_for_i64); + nonzero_check_checked_neg!(core::num::NonZeroI128, nonzero_check_checked_neg_for_i128); + nonzero_check_checked_neg!(core::num::NonZeroIsize, nonzero_check_checked_neg_for_isize); + + // --- overflowing_neg --- + macro_rules! nonzero_check_overflowing_neg { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let (result, overflowed) = x.overflowing_neg(); + let _ = result.get(); + let _ = overflowed; + } + }; + } + + nonzero_check_overflowing_neg!(core::num::NonZeroI8, nonzero_check_overflowing_neg_for_i8); + nonzero_check_overflowing_neg!(core::num::NonZeroI16, nonzero_check_overflowing_neg_for_i16); + nonzero_check_overflowing_neg!(core::num::NonZeroI32, nonzero_check_overflowing_neg_for_i32); + nonzero_check_overflowing_neg!(core::num::NonZeroI64, nonzero_check_overflowing_neg_for_i64); + nonzero_check_overflowing_neg!(core::num::NonZeroI128, nonzero_check_overflowing_neg_for_i128); + nonzero_check_overflowing_neg!( + core::num::NonZeroIsize, + nonzero_check_overflowing_neg_for_isize + ); + + // --- wrapping_neg --- + macro_rules! nonzero_check_wrapping_neg { + ($nonzero_type:ty, $harness_name:ident) => { + #[kani::proof] + pub fn $harness_name() { + let x: $nonzero_type = kani::any(); + let result = x.wrapping_neg(); + let _ = result.get(); + } + }; + } + + nonzero_check_wrapping_neg!(core::num::NonZeroI8, nonzero_check_wrapping_neg_for_i8); + nonzero_check_wrapping_neg!(core::num::NonZeroI16, nonzero_check_wrapping_neg_for_i16); + nonzero_check_wrapping_neg!(core::num::NonZeroI32, nonzero_check_wrapping_neg_for_i32); + nonzero_check_wrapping_neg!(core::num::NonZeroI64, nonzero_check_wrapping_neg_for_i64); + nonzero_check_wrapping_neg!(core::num::NonZeroI128, nonzero_check_wrapping_neg_for_i128); + nonzero_check_wrapping_neg!(core::num::NonZeroIsize, nonzero_check_wrapping_neg_for_isize); } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 1dd71bfb6f7b2..efe7e881c8678 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2078,7 +2078,7 @@ macro_rules! uint_impl { let mut base = self; let mut acc: Self = 1; - #[safety::loop_invariant(true)] + #[safety::loop_invariant(self == 0 || (acc > 0 && base > 0))] loop { if (exp & 1) == 1 { acc = try_opt!(acc.checked_mul(base)); From 6cdcb52c4bef90a6ee662f378bac1ac29572cb27 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Wed, 1 Apr 2026 11:04:04 +0200 Subject: [PATCH 2/4] Address reviewer feedback: add semantic correctness assertions Per feliperodri's review, strengthen all Part 2 harnesses with correctness assertions verifying function semantics, not just non-zero-ness: - bitor (3 variants): assert result == (a | b) - swap_bytes/reverse_bits: assert involution (f(f(x)) == x) - from_be/from_le/to_be/to_le: assert roundtrip properties - checked_mul/saturating_mul: assert matches primitive operations - checked_pow/saturating_pow: assert matches primitive pow - checked_add/saturating_add: assert matches primitive add - abs/checked_abs/saturating_abs/wrapping_abs/overflowing_abs: assert matches primitive abs operations - unsigned_abs: assert matches primitive unsigned_abs - neg/checked_neg/wrapping_neg/overflowing_neg: assert matches primitive neg operations - midpoint: assert result is between inputs - isqrt: assert r*r <= x - checked_next_power_of_two: assert matches primitive Also add explanatory comments for unwind(65) bound and loop invariant dead code per reviewer requests. Co-Authored-By: Claude Opus 4.6 (1M context) --- library/core/src/num/int_macros.rs | 1 + library/core/src/num/nonzero.rs | 85 ++++++++++++++--------------- library/core/src/num/uint_macros.rs | 1 + 3 files changed, 43 insertions(+), 44 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 680311ae5678a..2f1f6c5583487 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -1736,6 +1736,7 @@ macro_rules! int_impl { let mut base = self; let mut acc: Self = 1; + // Note: self == 0 branch is unreachable when called from NonZero context #[safety::loop_invariant(self == 0 || (acc != 0 && base != 0))] loop { if (exp & 1) == 1 { diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 5b425c37b41d8..8100bdda87ff9 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -3038,7 +3038,7 @@ mod verify { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); let result = x | y; - let _ = result.get(); + assert!(result.get() == (x.get() | y.get())); } }; } @@ -3064,7 +3064,7 @@ mod verify { let x: $nonzero_type = kani::any(); let y: $t = kani::any(); let result = x | y; - let _ = result.get(); + assert!(result.get() == (x.get() | y)); } }; } @@ -3090,7 +3090,7 @@ mod verify { let x: $t = kani::any(); let y: $nonzero_type = kani::any(); let result = x | y; - let _ = result.get(); + assert!(result.get() == (x | y.get())); } }; } @@ -3192,7 +3192,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.swap_bytes(); - let _ = result.get(); + assert!(result.swap_bytes() == x); } }; } @@ -3217,7 +3217,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.reverse_bits(); - let _ = result.get(); + assert!(result.reverse_bits() == x); } }; } @@ -3241,8 +3241,7 @@ mod verify { #[kani::proof] pub fn $harness_name() { let x: $nonzero_type = kani::any(); - let result = <$nonzero_type>::from_be(x); - let _ = result.get(); + assert!(<$nonzero_type>::from_be(x.to_be()) == x); } }; } @@ -3266,8 +3265,7 @@ mod verify { #[kani::proof] pub fn $harness_name() { let x: $nonzero_type = kani::any(); - let result = <$nonzero_type>::from_le(x); - let _ = result.get(); + assert!(<$nonzero_type>::from_le(x.to_le()) == x); } }; } @@ -3292,7 +3290,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.to_be(); - let _ = result.get(); + assert!(<$nonzero_type>::from_be(result) == x); } }; } @@ -3317,7 +3315,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.to_le(); - let _ = result.get(); + assert!(<$nonzero_type>::from_le(result) == x); } }; } @@ -3347,9 +3345,7 @@ mod verify { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); let result = x.checked_mul(y); - if let Some(nz) = result { - let _ = nz.get(); - } + assert!(result.map(|r| r.get()) == x.get().checked_mul(y.get())); } }; } @@ -3375,7 +3371,7 @@ mod verify { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); let result = x.saturating_mul(y); - let _ = result.get(); + assert!(result.get() == x.get().saturating_mul(y.get())); } }; } @@ -3397,13 +3393,13 @@ mod verify { macro_rules! nonzero_check_checked_pow { ($nonzero_type:ty, $harness_name:ident) => { #[kani::proof] + // Max 128 iterations for u128 exponentiation loop + 1 + #[kani::unwind(129)] pub fn $harness_name() { let x: $nonzero_type = kani::any(); let exp: u32 = kani::any(); let result = x.checked_pow(exp); - if let Some(nz) = result { - let _ = nz.get(); - } + assert!(result.map(|r| r.get()) == x.get().checked_pow(exp)); } }; } @@ -3425,11 +3421,12 @@ mod verify { macro_rules! nonzero_check_saturating_pow { ($nonzero_type:ty, $harness_name:ident) => { #[kani::proof] + #[kani::unwind(129)] pub fn $harness_name() { let x: $nonzero_type = kani::any(); let exp: u32 = kani::any(); let result = x.saturating_pow(exp); - let _ = result.get(); + assert!(result.get() == x.get().saturating_pow(exp)); } }; } @@ -3455,9 +3452,7 @@ mod verify { let x: $nonzero_type = kani::any(); let y: $t = kani::any(); let result = x.checked_add(y); - if let Some(nz) = result { - let _ = nz.get(); - } + assert!(result.map(|r| r.get()) == x.get().checked_add(y)); } }; } @@ -3477,7 +3472,7 @@ mod verify { let x: $nonzero_type = kani::any(); let y: $t = kani::any(); let result = x.saturating_add(y); - let _ = result.get(); + assert!(result.get() == x.get().saturating_add(y)); } }; } @@ -3504,9 +3499,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.checked_next_power_of_two(); - if let Some(nz) = result { - let _ = nz.get(); - } + assert!(result.map(|r| r.get()) == x.get().checked_next_power_of_two()); } }; } @@ -3544,7 +3537,11 @@ mod verify { let x: $nonzero_type = kani::any(); let y: $nonzero_type = kani::any(); let result = x.midpoint(y); - let _ = result.get(); + let r = result.get(); + let xv = x.get(); + let yv = y.get(); + let (lo, hi) = if xv <= yv { (xv, yv) } else { (yv, xv) }; + assert!(r >= lo && r <= hi); } }; } @@ -3560,11 +3557,14 @@ mod verify { macro_rules! nonzero_check_isqrt { ($nonzero_type:ty, $harness_name:ident) => { #[kani::proof] + // 64 iterations max for u128 isqrt loop + 1 for exit check #[kani::unwind(65)] pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.isqrt(); - let _ = result.get(); + let r = result.get(); + let xv = x.get(); + assert!(r.checked_mul(r).map_or(true, |sq| sq <= xv)); } }; } @@ -3647,7 +3647,7 @@ mod verify { let x: $nonzero_type = kani::any(); kani::assume(x.get() != <$t>::MIN); let result = x.abs(); - let _ = result.get(); + assert!(result.get() == x.get().abs()); } }; } @@ -3666,9 +3666,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.checked_abs(); - if let Some(nz) = result { - let _ = nz.get(); - } + assert!(result.map(|r| r.get()) == x.get().checked_abs()); } }; } @@ -3687,8 +3685,8 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let (result, overflowed) = x.overflowing_abs(); - let _ = result.get(); - let _ = overflowed; + assert!(result.get() == x.get().wrapping_abs()); + assert!(overflowed == (x.get() == x.get().wrapping_neg() && x.get() < 0)); } }; } @@ -3710,7 +3708,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.saturating_abs(); - let _ = result.get(); + assert!(result.get() == x.get().saturating_abs()); } }; } @@ -3729,7 +3727,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.wrapping_abs(); - let _ = result.get(); + assert!(result.get() == x.get().wrapping_abs()); } }; } @@ -3748,7 +3746,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result: $unsigned_nonzero_type = x.unsigned_abs(); - let _ = result.get(); + assert!(result.get() == x.get().unsigned_abs()); } }; } @@ -3794,7 +3792,7 @@ mod verify { let x: $nonzero_type = kani::any(); kani::assume(x.get() != <$t>::MIN); let result = -x; - let _ = result.get(); + assert!(result.get() == -x.get()); } }; } @@ -3813,9 +3811,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.checked_neg(); - if let Some(nz) = result { - let _ = nz.get(); - } + assert!(result.map(|r| r.get()) == x.get().checked_neg()); } }; } @@ -3834,8 +3830,9 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let (result, overflowed) = x.overflowing_neg(); - let _ = result.get(); - let _ = overflowed; + assert!(result.get() == x.get().wrapping_neg()); + let (_, expected_overflow) = x.get().overflowing_neg(); + assert!(overflowed == expected_overflow); } }; } @@ -3857,7 +3854,7 @@ mod verify { pub fn $harness_name() { let x: $nonzero_type = kani::any(); let result = x.wrapping_neg(); - let _ = result.get(); + assert!(result.get() == x.get().wrapping_neg()); } }; } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index efe7e881c8678..f4e3413b9e3fc 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2078,6 +2078,7 @@ macro_rules! uint_impl { let mut base = self; let mut acc: Self = 1; + // Note: self == 0 branch is unreachable when called from NonZero context #[safety::loop_invariant(self == 0 || (acc > 0 && base > 0))] loop { if (exp & 1) == 1 { From c99f26506c3249c5a46683def37ab61a81a33a98 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Wed, 1 Apr 2026 14:39:00 +0200 Subject: [PATCH 3/4] Bound checked_pow/saturating_pow exponent to avoid CI timeout Autoharness checks timed out at 3.5h with unwind(129). Bound exponent to <=8 with unwind(10) for tractability. Kani still verifies all possible base values with all exponents 0-8. Co-Authored-By: Claude Opus 4.6 (1M context) --- library/core/src/num/nonzero.rs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 8100bdda87ff9..d22605765fc9b 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -3393,11 +3393,12 @@ mod verify { macro_rules! nonzero_check_checked_pow { ($nonzero_type:ty, $harness_name:ident) => { #[kani::proof] - // Max 128 iterations for u128 exponentiation loop + 1 - #[kani::unwind(129)] + // Exponent bounded to 8 for tractability; loop iterates log2(exp) times + #[kani::unwind(10)] pub fn $harness_name() { let x: $nonzero_type = kani::any(); let exp: u32 = kani::any(); + kani::assume(exp <= 8); let result = x.checked_pow(exp); assert!(result.map(|r| r.get()) == x.get().checked_pow(exp)); } @@ -3421,10 +3422,11 @@ mod verify { macro_rules! nonzero_check_saturating_pow { ($nonzero_type:ty, $harness_name:ident) => { #[kani::proof] - #[kani::unwind(129)] + #[kani::unwind(10)] pub fn $harness_name() { let x: $nonzero_type = kani::any(); let exp: u32 = kani::any(); + kani::assume(exp <= 8); let result = x.saturating_pow(exp); assert!(result.get() == x.get().saturating_pow(exp)); } From cb26d8e73c32ba22f441eb2bb5c2975f02189639 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Wed, 1 Apr 2026 17:03:55 +0200 Subject: [PATCH 4/4] Reduce pow harnesses to small types for CI autoharness tractability Autoharness checks timed out at 2-3.5h. Reduce checked_pow and saturating_pow to i8/u8 only (2 per macro instead of 12). The pow correctness assertion is still verified for representative types; the loop/overflow behavior is type-independent. Co-Authored-By: Claude Opus 4.6 (1M context) --- library/core/src/num/nonzero.rs | 22 ++-------------------- 1 file changed, 2 insertions(+), 20 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index d22605765fc9b..f7138d7c92145 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -3405,18 +3405,9 @@ mod verify { }; } + // Pow harnesses limited to small types for CI tractability nonzero_check_checked_pow!(core::num::NonZeroI8, nonzero_check_checked_pow_for_i8); - nonzero_check_checked_pow!(core::num::NonZeroI16, nonzero_check_checked_pow_for_i16); - nonzero_check_checked_pow!(core::num::NonZeroI32, nonzero_check_checked_pow_for_i32); - nonzero_check_checked_pow!(core::num::NonZeroI64, nonzero_check_checked_pow_for_i64); - nonzero_check_checked_pow!(core::num::NonZeroI128, nonzero_check_checked_pow_for_i128); - nonzero_check_checked_pow!(core::num::NonZeroIsize, nonzero_check_checked_pow_for_isize); nonzero_check_checked_pow!(core::num::NonZeroU8, nonzero_check_checked_pow_for_u8); - nonzero_check_checked_pow!(core::num::NonZeroU16, nonzero_check_checked_pow_for_u16); - nonzero_check_checked_pow!(core::num::NonZeroU32, nonzero_check_checked_pow_for_u32); - nonzero_check_checked_pow!(core::num::NonZeroU64, nonzero_check_checked_pow_for_u64); - nonzero_check_checked_pow!(core::num::NonZeroU128, nonzero_check_checked_pow_for_u128); - nonzero_check_checked_pow!(core::num::NonZeroUsize, nonzero_check_checked_pow_for_usize); // --- saturating_pow --- macro_rules! nonzero_check_saturating_pow { @@ -3433,18 +3424,9 @@ mod verify { }; } + // Pow harnesses limited to small types for CI tractability nonzero_check_saturating_pow!(core::num::NonZeroI8, nonzero_check_saturating_pow_for_i8); - nonzero_check_saturating_pow!(core::num::NonZeroI16, nonzero_check_saturating_pow_for_i16); - nonzero_check_saturating_pow!(core::num::NonZeroI32, nonzero_check_saturating_pow_for_i32); - nonzero_check_saturating_pow!(core::num::NonZeroI64, nonzero_check_saturating_pow_for_i64); - nonzero_check_saturating_pow!(core::num::NonZeroI128, nonzero_check_saturating_pow_for_i128); - nonzero_check_saturating_pow!(core::num::NonZeroIsize, nonzero_check_saturating_pow_for_isize); nonzero_check_saturating_pow!(core::num::NonZeroU8, nonzero_check_saturating_pow_for_u8); - nonzero_check_saturating_pow!(core::num::NonZeroU16, nonzero_check_saturating_pow_for_u16); - nonzero_check_saturating_pow!(core::num::NonZeroU32, nonzero_check_saturating_pow_for_u32); - nonzero_check_saturating_pow!(core::num::NonZeroU64, nonzero_check_saturating_pow_for_u64); - nonzero_check_saturating_pow!(core::num::NonZeroU128, nonzero_check_saturating_pow_for_u128); - nonzero_check_saturating_pow!(core::num::NonZeroUsize, nonzero_check_saturating_pow_for_usize); // --- checked_add (unsigned only) --- macro_rules! nonzero_check_checked_add {