Challenge 12: safety and correctness of NonZero - #637
Open
stefanzetzsche wants to merge 1 commit into
Open
Conversation
Part 1 (new / new_unchecked): an #[ensures] contract on NonZero::new
verifying the layout precondition backing its transmute_unchecked
(size_of::<T>() == size_of::<Option<NonZero<T>>>()), that a NonZero is
produced iff the input is nonzero (2a), and that the inner value equals
the input (2b) — with proof_for_contract harnesses across all 12
integer widths. from_mut is verified by plain harnesses with in-body
assertions (its returned Option<&mut Self> mutably aliases the input,
so an #[ensures] reading both would introduce an aliasing hazard).
Part 2 (36 functions): tool-agnostic safety::{requires,ensures}
contracts plus per-width Kani harnesses in nonzero.rs mod verify —
checked/saturating mul, pow and add, the neg and abs families,
count_ones, bit operations (swap_bytes, reverse_bits, rotations,
endian conversions), midpoint, isqrt, and checked_next_power_of_two.
Trait-generic items Kani cannot attach contracts to (max/min/clamp via
Ord — cf. model-checking#202 — and the three const BitOr impls) are covered by
direct harnesses with assertions instead. Partial methods (abs, neg)
use paired value/should_panic harnesses so both the defined and the
panicking (MIN) domains are covered.
The placeholder #[safety::loop_invariant(true)] on checked_pow's loop
(int_macros.rs / uint_macros.rs, added in model-checking#327) is strengthened to
`self == 0 || (acc > 0 && base > 0)` (unsigned) and
`self == 0 || (acc != 0 && base != 0)` (signed). Under
-Z loop-contracts a `true` invariant havocs the accumulator and makes
every nonzero-dependent caller unverifiable; the strengthened
invariant is inductive and discharges NonZero::checked_pow's
new_unchecked obligation with unbounded, full-domain harnesses on
every width. Trade-off, documented in-code: only invariant-derived
facts (nonzero-ness) are provable about the loop's result, so the two
pow contracts state the safety property rather than exact-value
equality (a functional invariant would need ghost state for the
original exponent).
Every assume-bearing harness macro carries a non-vacuity witness;
unchecked_mul's interval harnesses cover the contract precondition
itself (cover(x.checked_mul(y).is_some())) so an interval pairing
that cannot satisfy the assumed #[requires] fails loudly instead of
verifying vacuously. The isqrt wide-width interval strategy is
documented as an explicit known verification gap, with mid-band
harnesses at the root's half-width transition narrowing it.
All 498 harnesses in num::nonzero::verify verified
(VERIFICATION: SUCCESSFUL) via scripts/run-kani.sh.
Towards model-checking#71.
By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 and MIT licenses.
stefanzetzsche
force-pushed
the
nonzero-challenge-12
branch
from
August 19, 2026 12:43
f3a666a to
e28529c
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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 perNonZerotype it's defined on (NonZeroI8throughNonZeroUsize). All 498 harnesses innum::nonzero::verifypass viascripts/run-kani.sh.Changes
nonzero.rsnewand the Part 2 methods; harnesses inmod verify; fix for pre-existingunchecked_mulharnesses that were passing without checking anything (see below)int_macros.rs,uint_macros.rschecked_pow's placeholderloop_invariant(true)strengthened to `self == 0Part 1
The contract on
newstates 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: aNonZerois 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_uncheckedkeeps 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 internalnew_uncheckedis never zero (ruling out the "producing an invalid value" UB). Most contracts also state the exact result value.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_negproof_for_contractover all possible inputschecked_pow,saturating_powproof_for_contractover 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,isqrtisqrt, the unverified middle range is called out in-code as a known gapmax,min,clamp,bitor(3 impls)abs,negMIN, one proves thatMINpanics (#[kani::should_panic])from_mut,from_mut_uncheckedWherever a harness restricts its inputs with
kani::assume, akani::covercheck 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-existingunchecked_mulharnesses: 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.