Challenge 12: safety and correctness of NonZero

[stefanzetzsche]

Towards #71. Solves Challenge 12: Safety of NonZero: contracts and Kani harnesses for NonZero<T>, covering Part 1 (new/new_unchecked) and all 36 Part 2 functions. Since Kani checks each concrete type separately, every function gets one harness per NonZero type it's defined on (NonZeroI8 through NonZeroUsize). All 498 harnesses in num::nonzero::verify pass via scripts/run-kani.sh.

Changes

File	Change
nonzero.rs	Contracts on new and the Part 2 methods; harnesses in mod verify; fix for pre-existing unchecked_mul harnesses that were passing without checking anything (see below)
int_macros.rs, uint_macros.rs	checked_pow's placeholder loop_invariant(true) strengthened to `self == 0

Part 1

The contract on new states the size equality the challenge accepts in place of full transmute verification (size_of::<T>() == size_of::<Option<NonZero<T>>>()), plus the two required correctness properties: a NonZero is created if and only if the input is nonzero (2a), and the inner value equals the input (2b). Verified with #[kani::proof_for_contract] for all 12 types; new_unchecked keeps its existing verified contract.

Part 2

Each function gets a safety::{requires,ensures} contract and per-type harnesses. The common safety property: the value passed to the internal new_unchecked is never zero (ruling out the "producing an invalid value" UB). Most contracts also state the exact result value.

Functions	Approach
count_ones, bit ops (swap_bytes, reverse_bits, rotate_*, from_be/le, to_be/le), checked/saturating_add, checked_next_power_of_two, midpoint, checked/overflowing/saturating/wrapping_abs, unsigned_abs, checked/overflowing/wrapping_neg	proof_for_contract over all possible inputs
checked_pow, saturating_pow	proof_for_contract over all possible inputs, with no exponent bound — the strengthened loop invariant makes this possible. In return, the contracts state only that the result is nonzero, not its exact value (after loop abstraction, the exact value is not provable)
checked/saturating/unchecked_mul, isqrt	All inputs up to 32 bits; value ranges at 64/128 bits, because CBMC cannot handle full-width multiplication. For isqrt, the unverified middle range is called out in-code as a known gap
max, min, clamp, bitor (3 impls)	Plain harnesses with assertions — Kani cannot attach contracts to these generic trait methods (cf. #202)
abs, neg	Two harnesses each: one proves the contract for every input except MIN, one proves that MIN panics (#[kani::should_panic])
from_mut, from_mut_unchecked	Plain harnesses with assertions — a contract would read through the mutably aliased return value

Wherever a harness restricts its inputs with kani::assume, a kani::cover check confirms that some input actually satisfies the restriction. Without that check, an impossible restriction makes the proof pass while checking nothing — which is exactly what was wrong with the pre-existing unchecked_mul harnesses: both operands came from the same near-extreme range, every product overflowed, so no input satisfied the function's precondition and the proofs were passing empty. Fixed by pairing each extreme range with a small range for the other operand, and adding a cover for the precondition itself.

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

[feliperodri]

Approve — strongest of the Challenge 12 solutions, no known correctness gap

Reviewed against the challenge criteria (issue #71) and compared with the other open Challenge-12 PRs (#565, #600, #544; plus the complementary perf refactor #624). This is the solution I'd upstream.

Verified against the diff

• No vacuity. 0 cfg(kani)/cfg(not(kani)) body-swaps in the added lines — the harnesses exercise the real std bodies, not a hand-written abstraction.
• Part 1 done as mandated. Real #[kani::proof_for_contract(NonZero::new)] with the sanctioned transmute size-equality stand-in plus the 2a (created-iff-nonzero) and 2b (value-preservation) properties. new_unchecked keeps its verified contract. This is the only open solution that discharges Part 1 with verified contracts rather than plain proofs.
• Broad verified coverage. 32 #[kani::proof_for_contract] with functional #[ensures] per integer width (e.g. result.get() == old(self).get().swap_bytes(), from_be/to_le), beyond the safety-only minimum.
• checked_pow handled correctly. The placeholder loop_invariant(true) is strengthened to self == 0 || (acc != 0 && base != 0) (> 0 unsigned), not reverted — keeping pow unbounded (no exponent cap) and preserving the #327 annotation.
• abs/neg at MIN fully verified. Each carries a normal harness (assume != MIN) plus a #[kani::should_panic] MIN harness proving the overflow panic — no over-restrictive #[requires(!=MIN)] mis-statement.
• Non-vacuity discipline. 11 kani::cover witnesses confirm the restricted paths are reachable, and the fix to the pre-existing unchecked_mul harnesses (pairing each extreme interval with a small one) removes 16 previously-vacuous proofs — exactly the kind of empty-proof this review campaign has been screening for.
• Trait-generic items Kani can't contract (max/min/clamp, the three BitOr impls, from_mut) are covered with direct safety-crate harnesses.

Note on evidence

This approval is based on static + diff verification and the prior local-Kani run data from the review campaign; I did not re-run the full harness suite locally for this pass. CI (kani.yml) gates the 498 harnesses, and the author reports all pass via scripts/run-kani.sh.

Nice work — this is the first Challenge-12 submission with no known correctness gap.

[feliperodri]

Hi, committee members (@celinval @rahulku @pnkfelix @zhassan-aws @remi-delmas-3000 @qinheping @tautschnig @patricklam @ranjitjhala @carolynzech @robdockins @HuStmpHrrr @Eh2406 @jswrenn @havelund @jorajeev @rajath-mk @thanhnguyen-aws). This PR is ready for a second look. I've reviewed and approved it: it's the strongest of the open Challenge-12 submissions, meets Part 1's verified-contract requirement, covers all 36 Part 2 functions, and has no known correctness gap AFAIK. Since it needs a committee review to merge, does anyone have the bandwidth to take a pass?