Replace byte-inspection NonZero contracts with niche test and raw_eq - #624
Merged
feliperodri merged 1 commit intoAug 28, 2026
Merged
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.
This was referenced Aug 3, 2026
feliperodri
approved these changes
Aug 27, 2026
feliperodri
left a comment
feliperodri
left a comment
Member
There was a problem hiding this comment.
Static review (no local Kani run this time). The new #[requires(NonZero::new(n).is_some())] / #[ensures(raw_eq(&result.get(), &n))] are semantically equivalent to the previous byte-slice inspections but avoid symbolic pointer indirection and iterator reasoning: NonZero::new is intrinsics::transmute_unchecked (so no recursion with new_unchecked), new(n).is_some() is exactly the condition under which the body's match Self::new(n) takes Some, and raw_eq is bit-equivalent for these padding-free integer types. Both new_unchecked and from_mut_unchecked are covered by proof_for_contract. No concerns.
rajath-mk
approved these changes
Aug 28, 2026
feliperodri
enabled auto-merge
August 28, 2026 20:51
feliperodri
disabled auto-merge
August 28, 2026 20:52
Merged
via the queue into
model-checking:main
with commit Aug 28, 2026
215990e
28 of 29 checks passed
DiuDiu777
pushed a commit
to safer-rust/rapx-verify-rust-std
that referenced
this pull request
Aug 29, 2026
…ing#627) `NonNull::slice_from_raw_parts` is a safe function with no validity requirements on `data`: per its documentation, it is safe to construct the pointer, and only its *use* is subject to safety conditions. Its postcondition however evaluated `unsafe { result.as_ref() }.len()`, creating a reference to the pointed-to memory just to read the slice length — undefined behavior when `data` is dangling or misaligned, and a failing check when the contract is evaluated in such a context. This surfaces with dependency contracts asserted (the Kani default since model-checking/kani#3802): `ptr::non_null::verify::non_null_check_as_uninit_slice_mut` constructs, legitimately, a `NonNull` slice pointer whose span may exceed the backing allocation; evaluating `slice_from_raw_parts`' postcondition then fails with "misaligned pointer to reference cast" / "dereference failure: pointer invalid" inside `NonNull::as_ref`. CI currently masks this with `--no-assert-contracts`. This PR reads the length from the wide-pointer metadata via `NonNull::len` instead, which involves no dereference (and no unsafe code) and is the property the clause is about in the first place. Blame: the dereferencing clause dates to the original contracts in 07318df (model-checking#127). Verified with Kani 152c6a8c + CBMC 6.10.0: `non_null_check_as_uninit_slice_mut`, `non_null_check_slice_from_raw_parts`, `non_null_check_as_uninit_slice` and `non_null_check_len` pass both with and without `--no-assert-contracts` (the first previously failed with contracts asserted — the last remaining failure of that kind known on the 125-harness sample after model-checking#622, model-checking#623, model-checking#624, model-checking#625, model-checking#626). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
DiuDiu777
pushed a commit
to safer-rust/rapx-verify-rust-std
that referenced
this pull request
Aug 29, 2026
…-checking#625) The requires/ensures clauses of the pointer arithmetic operations (`<*mut T>::{offset,add,sub}`, `<*const T>::{offset,add,sub}`, `NonNull::{add,sub}`, `NonNull::offset_from_unsigned`) demand `same_allocation` unconditionally (modulo a ZST escape), although the documented semantics explicitly permit zero-sized offsets on any pointer, including dangling ones: only "if the computed offset is non-zero, then self must be derived from a pointer to some allocated object". The stricter-than-documented clauses are violated by legitimate std code: empty slices may be backed by dangling pointers (`slice::from_raw_parts(ptr, 0)` for arbitrary aligned non-null `ptr` — exactly what `slice::iter`'s own `any_slice` helper generates), whereupon `Iter::new` computes `ptr.add(0)` and `len()` computes `end.offset_from_unsigned(begin)` on two equal dangling pointers. With dependency contracts asserted (the Kani default since model-checking/kani#3802), the `slice::iter::verify::verify_tup` harnesses fail on these clauses — and evaluating `same_allocation` on an allocation-less pointer is additionally a Kani unsupported construct ("Kani does not support reasoning about pointer to unallocated memory"). CI currently masks this via `--no-assert-contracts`. This PR adds the documented escape hatches: `count == 0 ||` ahead of the same-allocation disjunct in offset/add/sub requires and ensures — matching the precedent already present in `NonNull::offset` — and an equal-address escape in `NonNull::offset_from_unsigned`, matching the precedent in `<*const T>::offset_from`. Blame: the unconditional clauses date back to the original contract PRs model-checking#113 (014965a) and model-checking#93 (688b15b) and siblings. Verified with Kani 152c6a8c + CBMC 6.10.0: * `slice::iter::verify::verify_tup::{check_next_back_unchecked,check_advance_back_by}` now pass with contracts asserted; * all 265 proof harnesses matching `non_null_check_{add,sub,offset_from_unsigned}` and `ptr::verify::check_{mut,const}_{add,sub,offset}` pass both with and without `--no-assert-contracts`. Together with model-checking#622, model-checking#623, model-checking#624 and model-checking/kani#4709/rust-lang#4710, this resolves all verdict differences found on a 125-harness sample when running without `--no-assert-contracts`, except `non_null_check_from_raw_part_trait` (Kani's "unstable vtable comparison 'Eq'" limitation, reached by `as_ptr`'s postcondition on a `dyn Trait` pointee — tracked separately). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.