Replace byte-inspection NonZero contracts with niche test and raw_eq - #624
Open
tautschnig wants to merge 1 commit into
Open
Replace byte-inspection NonZero contracts with niche test and raw_eq#624tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
The requires/ensures clauses of NonZero::new_unchecked (and the requires of from_mut_unchecked) expressed "n is not zero" and "result equals n" by building a raw byte slice over the value with slice::from_raw_parts and iterating it. Under symbolic execution every asserted occurrence of these clauses then pays for pointer indirection, slice-iterator reasoning, and allocation tracking - and since new_unchecked sits beneath most NonZero operations, harnesses whose call graph contains NonZero constructions were dominated by this: with dependency contracts asserted (the Kani default since model-checking/kani#3802), num::nonzero::verify::check_mul_u32_small takes 59.6s of CBMC solve time, against 0.3s with --no-assert-contracts. Express the same properties through operations the verifier resolves directly: `NonZero::new(n).is_some()` performs the canonical zero test via the niche layout (a transmute plus discriminant test), and `intrinsics::raw_eq` compares object representations without constructing slices. Neither requires additional trait bounds on T. With contracts asserted, check_mul_u32_small drops from 59.6s to 0.6s solve time (103x). All 56 harnesses matching nonzero_check_new_unchecked_for / nonzero_check_from_mut_unchecked / check_mul pass both with and without --no-assert-contracts (Kani 152c6a8c + CBMC 6.10.0). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
Optimizes the Kani contract clauses for core::num::NonZero constructors to reduce symbolic-execution overhead when dependency contracts are asserted, without changing runtime semantics (the runtime contract macros are currently no-ops).
Changes:
- Replaced byte-slice “non-zero” preconditions for
NonZero::new_unchecked/from_mut_uncheckedwith a niche-layout check viaNonZero::new(..).is_some(). - Replaced byte-slice equality postcondition for
new_uncheckedwithintrinsics::raw_eqto compare object representations directly. - Added explanatory comments documenting why these contract forms are cheaper for the verifier.
| // indirection and iterator reasoning, which dominated verification time | ||
| // of harnesses whose call graph contains NonZero constructions. | ||
| #[requires(NonZero::new(n).is_some())] | ||
| #[ensures(|result: &Self| unsafe { core::intrinsics::raw_eq(&result.get(), &n) })] |
This was referenced Aug 3, 2026
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
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.
The requires/ensures clauses of
NonZero::new_unchecked(and the requires offrom_mut_unchecked) expressed "n is not zero" and "result equals n" by building a raw byte slice over the value withslice::from_raw_partsand iterating it. Under symbolic execution, every asserted occurrence of these clauses pays for pointer indirection, slice-iterator reasoning, and allocation tracking — and sincenew_uncheckedsits beneath mostNonZerooperations, harnesses whose call graph containsNonZeroconstructions were dominated by this: with dependency contracts asserted (the Kani default since model-checking/kani#3802),num::nonzero::verify::check_mul_u32_smalltakes 59.6s of CBMC solve time, against 0.3s with--no-assert-contracts.This PR expresses the same properties through operations the verifier resolves directly:
NonZero::new(n).is_some()performs the canonical zero test via the niche layout (a transmute plus discriminant test), andintrinsics::raw_eqcompares object representations without constructing slices. Neither requires additional trait bounds onT.Measured with Kani 152c6a8c + CBMC 6.10.0:
check_mul_u32_smallwith contracts asserted: 59.6s → 0.6s solve time (103x).nonzero_check_new_unchecked_for*/nonzero_check_from_mut_unchecked*/check_mul*pass both with and without--no-assert-contracts.Part of the effort to make dropping
--no-assert-contractsfromrun-kani.shfeasible (see also #622, #623): the byte-inspection clauses were the single largest per-call-site cost multiplier identified when asserting dependency contracts across a 125-harness sample.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.