NonZero (rotate_left, rotate_right, max, min, clamp, count_ones, cmp) Proofs - #202
Merged
tautschnig merged 12 commits intoDec 11, 2024
Merged
Conversation
tautschnig
reviewed
Dec 2, 2024
tautschnig
reviewed
Dec 3, 2024
tautschnig
approved these changes
Dec 4, 2024
tautschnig
left a comment
Member
There was a problem hiding this comment.
Thank you for all the updates!
carolynzech
reviewed
Dec 5, 2024
carolynzech
left a comment
There was a problem hiding this comment.
Instead of having a module for each function, can you move all of these harnesses inside of mod verify?
tautschnig
approved these changes
Dec 6, 2024
Author
Done! All in mod verify now |
This was referenced Dec 10, 2024
Closed
carolynzech
approved these changes
Dec 10, 2024
carolynzech
enabled auto-merge (squash)
December 10, 2024 19:12
tautschnig
disabled auto-merge
December 10, 2024 20:53
stefanzetzsche
added a commit
to stefanzetzsche/verify-rust-std
that referenced
this pull request
Aug 19, 2026
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.
kasimte
pushed a commit
to kasimte/verify-rust-std
that referenced
this pull request
Aug 26, 2026
Towards model-checking#71. Solves [Challenge 12: Safety of NonZero](https://model-checking.github.io/verify-rust-std/challenges/0012-nonzero.html): 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 || (acc != 0 && base != 0)` (unsigned: `> 0`). With the placeholder, `-Z loop-contracts` treats the loop result as an arbitrary value, so `NonZero::checked_pow` could not be verified at all | ## 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. model-checking#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.
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
3 participants
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.
Working on #71 (Safety of NonZero)
We are looking for feedback on our proof for rotate_left & rotate_right.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.