Add NonZero verification harnesses

Author: Kasim Te

doc/src/challenges/0012-nonzero.md

@@ -85,3 +85,52 @@ 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
+
+This challenge is addressed with Kani contracts and proof harnesses in
+`library/core/src/num/nonzero.rs` (module `num::nonzero::verify`). All Part 1 and Part 2
+functions are verified across all twelve `NonZero` integer types.
+
+### Approach
+
+- **Inherent methods** carry `#[safety::requires]` / `#[safety::ensures]` contracts verified
+  with `#[kani::proof_for_contract]`. Postconditions tie each result to the corresponding
+  primitive operation (e.g. `result.get() == old(self).get().swap_bytes()`), going beyond mere
+  absence of UB.
+- **`abs`** is a safe method that overflows-and-panics at `MIN`; following the rule that safe
+  functions carry no real precondition, it keeps only an `#[ensures]` (no `#[requires]`). The
+  non-`MIN` value is verified with `#[kani::proof_for_contract]`, and the `MIN`-input panic with a
+  paired `#[kani::should_panic]` harness.
+- **`new_unchecked`** (Part 1) uses a byte-slice contract (generic over `ZeroablePrimitive`)
+  asserting the stored value equals the input. **`new`** is verified by per-type proof harnesses
+  asserting the full Part-1 property -- a `NonZero` is created if and only if the input is
+  nonzero, and the value is preserved. A contract on `new` itself is deliberately avoided:
+  because `new` is widely called, contract instrumentation is applied at every call site and
+  regresses unrelated 128-bit harnesses under `-Z loop-contracts`; a per-type proof verifies the
+  same property without that side effect.
+- **Operator-trait impls** (`BitOr` x3, `Neg`) are verified with `#[kani::proof]` plus a
+  functional assertion, because the `#[safety]` contract proc-macro cannot annotate trait-impl
+  methods (it parses `ItemFn`, not `ImplItemFn`).
+
+### Bounded verification
+
+Challenge 12 permits bounded verification. A few operations are intractable for CBMC at full
+64/128-bit width and are verified over representative bounded domains:
+
+- **`checked_mul` / `saturating_mul`** -- small types full-range; larger types via narrow value
+  windows (small values, plus windows near MIN/MAX to exercise overflow), mirroring the existing
+  `unchecked_mul` interval harnesses.
+- **`isqrt`** -- small types full-range; larger types with the input bounded (the internal
+  candidate-square is the cost driver).
+- **`checked_pow` / `saturating_pow`** -- Part 2 requires *safety*; the harnesses verify that the
+  `unsafe { new_unchecked(...) }` is sound (the result is nonzero) over full-range base and
+  exponent.
+
+### One supporting change outside `nonzero.rs`
+
+The primitive `checked_pow` loop invariant in `int_macros.rs` and `uint_macros.rs` was
+strengthened from `true` to `self == 0 || (acc != 0 && base != 0)` (signed) /
+`self == 0 || (acc > 0 && base > 0)` (unsigned). This is required so that, under
+`-Z loop-contracts`, the loop abstraction preserves the nonzero property that the `NonZero`
+wrappers rely on. It does not change runtime behavior.

library/core/src/num/int_macros.rs

@@ -1736,7 +1736,10 @@ macro_rules! int_impl {
             let mut base = self;
             let mut acc: Self = 1;
 
-            #[safety::loop_invariant(true)]
+            // `self == 0` covers the primitive's own harness (e.g. `0.checked_pow(n)`, where
+            // `acc` can reach 0); in the NonZero call path `self` is never 0, so it is dead
+            // but harmless there. The right disjunct (`acc != 0 && base != 0`) is the inductive core.
+            #[safety::loop_invariant(self == 0 || (acc != 0 && base != 0))]
             loop {
                 if (exp & 1) == 1 {
                     acc = try_opt!(acc.checked_mul(base));