From 71e54d04931c563a15793aaa7d5ce5ec06c7e816 Mon Sep 17 00:00:00 2001 From: Samuelsills Date: Tue, 24 Mar 2026 18:01:26 +0100 Subject: [PATCH] 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));