Add Kani contracts and harnesses for NonZero (Challenge 12)

[kasimte]

Resolves #71

This is my solution to Challenge 12: verifying the safety of the NonZero functions the challenge
lists, and (for new/new_unchecked) the functional correctness Part 1 asks for, across all twelve
integer types (i8-i128, isize, u8-u128, usize). The contracts and proof harnesses are in
library/core/src/num/nonzero.rs, under mod num::nonzero::verify.

All of the Part 1 and Part 2 functions are covered, and every harness also rules out the undefined
behaviors the challenge calls out (invoking UB via intrinsics, reading uninitialized memory, and
producing an invalid value), which Kani checks by default. For Part 1 the harnesses prove the full
property: a NonZero is created if and only if the input is non-zero, and the stored value matches
the input.

Wherever it's feasible I verify the actual semantics rather than just the absence of UB. Most of the
inherent methods carry #[safety::ensures] contracts (plus #[safety::requires] on the unsafe
ones), checked with #[kani::proof_for_contract], with postconditions tied to the matching primitive
operation, for example result.get() == old(self).get().swap_bytes(). A handful of cases needed more
thought, and those are the ones worth calling out:

• new carries a function-level #[ensures] contract with three clauses: the same-size
  obligation the challenge's Assumptions reduce the transmute to
  (size_of::<T>() == size_of::<Option<NonZero<T>>>()), created-iff-nonzero, and value
  preservation. Each clause is a single verifier operation (raw_eq, a niche-style zero test)
  rather than a byte-slice loop, since under -Z function-contracts the contract is
  instrumented at every call site and max/min/clamp/bitor all reach new — the 128-bit
  harnesses on those paths all pass. The per-type harnesses are
  #[kani::proof_for_contract(NonZero::<T>::new)], checking the contract over the full input
  range, and additionally assert the full Part-1 property directly. from_mut is verified
  by per-type proof harnesses asserting the same property over a mutable reference.
  new_unchecked returns a plain NonZero<T> and carries the analogous byte-equality #[ensures].
• abs is safe but panics on overflow at MIN. Following the convention that safe functions carry
  no real precondition, it keeps only an #[ensures] (no #[requires]): the non-MIN value is checked
  by proof_for_contract, and the MIN-input panic by a paired #[kani::should_panic] harness.
• BitOr (the three impls) and Neg are trait impls, which the #[safety] proc-macro can't
  annotate, so they use #[kani::proof] with a functional assertion. Neg's MIN input is covered
  by paired per-type #[kani::should_panic] harnesses (the same pattern as abs), so both the
  excluded-value correctness and the overflow panic are verified.
• rotate_left / rotate_right already carried value contracts on main, written as a round-trip
  (result.rotate_right(n).get() == self). I restated them in the equivalent direct form
  (result.get() == self.rotate_left(n)): it anchors to the primitive (matching the other bitwise
  methods above) and avoids the round-trip form's call to the contracted inverse, which is more
  expensive for CBMC.
• checked_mul, saturating_mul, and isqrt are intractable for CBMC at full 64/128-bit width.
  I verify the small types full-range and the larger ones over bounded windows. The multiply windows
  sit near MIN/MAX so they still exercise overflow (mirroring the existing unchecked_mul intervals),
  and isqrt bounds its input. The challenge sets no unbounded requirement, so this stays in scope.
• checked_pow and saturating_pow I scoped to the safety property Part 2 asks for: that the
  unsafe { new_unchecked(...) } is sound (the result is non-zero), over the full range of base and
  u32 exponent. I left out a value-level check (result == base.pow(exp)). As I understand it, the
  -Z loop-contracts abstraction that keeps the full-range exponent tractable (the strengthened pow
  loop invariant in int_macros/uint_macros) preserves non-zero-ness but not the loop's exact value,
  so a value postcondition won't verify alongside it, even with a bounded exponent. Happy to revisit if
  you'd prefer value coverage here.

There's also one change outside nonzero.rs: the primitive checked_pow loop invariant in
int_macros.rs and uint_macros.rs is strengthened from true to self == 0 || (acc != 0 && base != 0)
(signed) and self == 0 || (acc > 0 && base > 0) (unsigned). It's verification-only: under
-Z loop-contracts it lets the loop abstraction preserve the nonzero property the NonZero wrappers
depend on, and it doesn't change runtime behavior, since the #[safety::loop_invariant] annotation is
inert outside Kani, exactly like the true placeholder already on main.

I'd welcome the committee's feedback and am glad to iterate on any of this, whether that means
strengthening a contract, widening coverage, or reworking one of the approaches above.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

Adds Kani verification for Challenge 12’s NonZero safety and correctness requirements.

Changes:

• Adds contracts and proof harnesses across integer types.
• Adds bounded arithmetic and square-root proofs.
• Strengthens primitive checked_pow loop invariants.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 5 comments.

File	Description
library/core/src/num/nonzero.rs	Adds NonZero contracts and Kani harnesses.
library/core/src/num/int_macros.rs	Strengthens signed checked_pow invariant.
library/core/src/num/uint_macros.rs	Strengthens unsigned checked_pow invariant.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Overall

This is careful, largely sound verification work. I ran the full soundness checklist and found no FATAL vacuity: there are no #[cfg(not(kani))] body swaps (grep -c over the diff = 0), no loop_invariant(true) / type_invariant..{true} left behind, and no assume-the-conclusion patterns. Every contract added or modified has a matching #[kani::proof_for_contract] harness, and the contracts I checked are faithful. The gaps below are coverage/criteria-completeness issues, not vacuous passes, so this is a mild REQUEST_CHANGES rather than a rejection.

Strengths (credit)

• Loop-invariant strengthening is genuine, not decorative. int_macros.rs and uint_macros.rs replace #[safety::loop_invariant(true)] on checked_pow with self == 0 || (acc != 0 && base != 0) (signed) / self == 0 || (acc > 0 && base > 0) (unsigned). This is inductive (acc starts at 1, base=self; try_opt!(checked_mul) bails on overflow so nonzero×nonzero stays nonzero) and it is exactly what lets NonZero::checked_pow/saturating_pow discharge new_unchecked's "result != 0" precondition after the loop is abstracted under -Z loop-contracts. The self == 0 disjunct correctly keeps the primitive's own 0.checked_pow(n) harness passing. This is a verification-only annotation (inert in the runtime.rs safety backend), so it does not touch std runtime logic.
• Contract-liveness is clean. All 25 contracted functions modified in nonzero.rs (count_ones, rotate_left/right, swap_bytes, reverse_bits, from_be/le, to_be/le, checked_mul, saturating_mul, checked_add, saturating_add, checked_next_power_of_two, midpoint, isqrt, abs, checked_abs, overflowing_abs, saturating_abs, wrapping_abs, unsigned_abs, checked_neg, overflowing_neg, wrapping_neg) have a proof_for_contract harness. The abs/neg/overflowing contracts are faithful (e.g. overflowing_abs: result.1 == (old == MIN) and result.0 == wrapping_abs; checked_abs: Some ⇔ != MIN).
• Part 2 function-table coverage is complete when combined with the sound pre-existing harnesses in this file (max/min/clamp+clamp_panic, unchecked_mul, unchecked_add, from_mut_unchecked, new_unchecked all pre-date this PR at base). This PR adds the remaining bitor×3 / neg (trait impls, correctly done via #[kani::proof]+functional assert since #[safety] can't annotate ImplItemFn), pow-family (safety), from_mut, and the abs/neg/byte/arith contracts.
• abs at MIN is handled correctly with the established clamp/clamp_panic pattern: a value harness scoped by kani::assume(x != MIN) plus a paired #[kani::should_panic] harness (diff lines ~826-843).

Concerns (blocking)

1. Part 1 new is verified by an ordinary proof, not a contract (nonzero_check_new macro, diff ~2023-2051; file ~4852). Challenge 0012 Part 1 literally says "write and verify contracts specifying" (a) created iff nonzero and (b) value == n, plus the same-size transmute obligation. The proof soundly asserts r.is_some() == (x != 0) and v.get() == x, so the behavior is verified — but the required compositional #[requires]/#[ensures] contract on new (and the size obligation) is absent. The author's stated reason (contracting a hot fn instruments all call sites and regresses 128-bit harnesses) is real, but the criterion is explicit. Either add the contract or get an explicit waiver from the challenge owners; don't silently substitute a proof. (Matches Copilot comment #1.)

2. Neg MIN path is entirely unverified (nonzero_check_neg macro, diff 1807-1817; file ~4638). The harness does kani::assume(x.get() != MIN) but, unlike abs, provides no paired should_panic harness. neg is a Part-2-listed function; at MIN the primitive negation overflows (Kani would flag it), so the MIN input is neither proven UB-free nor proven to panic — the domain is simply dropped. Add a per-type #[kani::should_panic] neg-at-MIN harness mirroring nonzero_check_abs. (Copilot comment #4.)

Concerns (should-improve, non-blocking)

3. Big-width checked_mul/saturating_mul contracts are proven only over narrow windows (nonzero_check_binary_bounded, diff 1252-1264; file ~4084). For u32/u64/u128/usize and signed i32+, operands are confined to [1,20]/[MAX-20,MAX] (and [MIN,MIN+20]), plus M1 windows near sqrt(MAX). Because both operands share one interval per harness, mixed-sign large-operand overflow (one operand near MIN, the other near MAX) is never exercised for signed types, and the functional equality #[ensures] is not established over the full domain. This is honest bounded verification (documented) and the safety property is value-uniform (the wrapper is if let Some = primitive { new_unchecked }, and nonzero×nonzero can't produce Some(0)), so no UB escapes — but the stated contract is broader than what's verified. Note these contracts are not currently used as abstractions elsewhere, so there's no downstream unsoundness today. Consider a full-domain partition or documenting the safety-uniformity argument in-code. (Copilot comment #2.)

4. isqrt on u32+ is bounded to <= 65535 (nonzero_check_unary_bounded, diff 1741-1751; file ~4572). isqrt is total with no precondition, so this truncates verification of the equality contract for the vast majority of inputs. Safety again holds uniformly (result >= 1 for nonzero input), but the contract is only partially established. (Copilot comment #3.)

5. Pre-existing unchecked_mul interval harnesses (Copilot comment #5, file lines ~2767-3025) are not touched by this PR and are out of scope for judging #600, but they carry the same window-truncation limitation and are worth revisiting when tightening Part 2.

Direction

Minimum to unblock: (2) add per-type should_panic harnesses for Neg at MIN, and (1) either add the new contract or record an explicit owner-approved waiver for using a proof. Recommended follow-ups: (3)/(4) either widen to full-domain / domain-partition proofs for the big-width mul and isqrt contracts, or add an in-code note that the safety obligation is value-uniform and the equality contract is intentionally bounded per Challenge 12's bounded allowance.

[kasimte]

Thanks for the review, @feliperodri. Both blocking items are addressed in the pushed commits.

1. Contract on new

new now carries a #[ensures] contract with three clauses: the same-size transmute obligation (size_of::<T>() == size_of::<Option<NonZero<T>>>(), per the challenge's Assumptions), created-iff-nonzero, and value preservation. The clauses use raw_eq and a niche-style zero test — the same single-operation forms #624 uses — instead of the byte-slice inspection that originally kept new uncontracted.

The 12 nonzero_check_new_* harnesses are now #[kani::proof_for_contract(NonZero::<T>::new)], checking the contract over the full input range for every type. The 2a/2b assertions remain in the harnesses.

The pre-existing 128-bit harnesses whose call graphs reach new (clamp/max/min/unchecked_add, and the new_unchecked contract proofs) pass with unchanged solve times (e.g. nonzero_check_clamp_for_u128: 0.315s after, 0.314s before).

2. Neg at MIN

Added #[kani::should_panic] neg-at-MIN harnesses for all six signed types, mirroring nonzero_check_abs: nonzero_check_neg_min_panics_{i8,i16,i32,i64,i128,isize}. All six verify — the overflow panic fires — so MIN is covered on both paths.

3–5. Bounded windows

Added in-code notes at the checked_mul/saturating_mul and isqrt window macros: the windows bound only the functional-equality check, and the safety obligation holds for all inputs (if let Some(v) = primitive_checked_op { new_unchecked(v) } cannot produce Some(0) from nonzero operands; isqrt >= 1 for nonzero input). The pre-existing unchecked_mul interval harnesses reference the same note.

Also in this push

• Merged current main (nightly-2025-11-25 subtree, Kani d4df833c pin); no runtime-logic changes to the target functions.
• Full num::nonzero::verify suite under the CI flag set: 476 harnesses, 0 failures.
• CI on the updated branch is green: all Verify std partitions, both autoharness jobs, and upstream_test pass.