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.

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

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

Strengthened loop invariant on checked_pow in uint_macros.rs and
int_macros.rs from `true` to `self == 0 || (acc > 0 && base > 0)`.
This is a verification-only annotation (no-op at runtime) that
preserves the nonzero property through exponentiation loop iterations.

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

Resolves #71

Author: Samuelsills

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.

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));