Respect new_unchecked precondition in IndexRange proof harnesses - #623
Merged
feliperodri merged 1 commit intoAug 28, 2026
Merged
Conversation
The proof_for_contract harnesses for IndexRange::next_unchecked and IndexRange::next_back_unchecked, introduced in commit a0fca1c ("A bunch of LLM-generated contracts (model-checking#451)"), construct their IndexRange via `IndexRange::new_unchecked(start, end)` with entirely unconstrained `start` and `end`. That violates new_unchecked's documented safety precondition (and #[requires] contract) `start <= end`: the assumption provided by the contract under verification only takes effect at the call to next_unchecked / next_back_unchecked, after the UB of the unchecked constructor call has already happened. The violation is currently invisible in CI because run-kani.sh passes --no-assert-contracts; with dependency contracts asserted (the Kani default since model-checking/kani#3802), proof_for_index_range_next_back_unchecked fails on the asserted `start <= end` clause. Constrain both harnesses with `kani::assume(start <= end)`. The stronger `start < end` required by the functions under verification continues to be assumed from their own contracts, preserving the intent of the harnesses. Verified (Kani 152c6a8c + CBMC 6.10.0) that all three ops::index_range::verify harnesses pass both with and without --no-assert-contracts. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
This PR fixes Kani contract-proof harnesses for IndexRange::next_unchecked and IndexRange::next_back_unchecked so they do not invoke IndexRange::new_unchecked with inputs that violate its documented safety precondition (start <= end). This prevents a latent UB/contract violation from being masked when dependency contracts are asserted (the Kani default).
Changes:
- Add
kani::assume(start <= end)in theproof_for_contractharness forIndexRange::next_unchecked. - Add
kani::assume(start <= end)in theproof_for_contractharness forIndexRange::next_back_unchecked. - Document why this assumption is needed (constructor precondition) and why the stricter
start < endcondition is still covered by the verified functions’ own contracts.
feliperodri
reviewed
Aug 3, 2026
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.
Confirmed the fix: the harnesses now respect new_unchecked's existing requires(start <= end) precondition, so the latent contract violation surfaced by asserting dependency contracts is resolved. Verified locally that all three ops::index_range::verify harnesses pass with and without --no-assert-contracts. LGTM.
rajath-mk
approved these changes
Aug 28, 2026
Merged
via the queue into
model-checking:main
with commit Aug 28, 2026
c461b6a
27 of 30 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
…g#622) The `x % 2 != 0` precondition on `ptr::mod_inv`, added in 6be9ca4 (model-checking#457), is violated by `mod_inv`'s only caller: `align_offset::<T>(p, 1)` with `size_of::<T>() > 1` takes the GENERAL_CASE path (since `1 % stride != 0`) and computes `s2 = (stride & 0) >> 0 = 0`, calling `mod_inv(0, 1)`. This is reachable e.g. via `<[u16]>::align_to::<u8>()`. The violation is currently invisible in CI because `run-kani.sh` passes `--no-assert-contracts`; with dependency contracts asserted (the Kani default since model-checking/kani#3802), the harnesses `slice::verify::align_to_from_u16::align_to_u8`, `slice::verify::align_to_mut_from_char::align_to_mut_u8`, `slice::verify::align_to_mut_from_u32::align_to_mut_u8`, and `ptr::verify::check_align_offset_u16` all fail on the asserted `x % 2 != 0` clause. The call is mathematically sound — modulo `m == 1` every value is trivially an inverse (the unique residue is 0), and `align_offset` masks the returned value with `a2 - 1 == 0` — so it is the precondition that is too strict, not the caller that is wrong: an inverse of `x` modulo a power of two `m` exists iff `gcd(x, m) == 1`, which for `m > 1` means odd `x` but for `m == 1` holds for all `x`. This PR weakens the precondition to `m == 1 || x % 2 != 0` and fixes the (kani-disabled) postcondition for the same degenerate case (`% m == 1 % m` instead of `% m == 1`, since modulo 1 the result is 0). Verified with Kani 152c6a8c + CBMC 6.10.0: the four harnesses above now pass with contracts asserted, and the eight `ptr::verify::check_align_offset*` proof harnesses pass both with and without `--no-assert-contracts`. Found while investigating what still blocks removing `--no-assert-contracts` from `run-kani.sh`: this is one of two genuine latent contract violations that asserting dependency contracts surfaces (the other: model-checking#623). 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>
DiuDiu777
pushed a commit
to safer-rust/rapx-verify-rust-std
that referenced
this pull request
Aug 29, 2026
…odel-checking#624) 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 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`. 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), and `intrinsics::raw_eq` compares object representations without constructing slices. Neither requires additional trait bounds on `T`. Measured with Kani 152c6a8c + CBMC 6.10.0: * `check_mul_u32_small` with contracts asserted: 59.6s → 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`. Part of the effort to make dropping `--no-assert-contracts` from `run-kani.sh` feasible (see also model-checking#622, model-checking#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. 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
proof_for_contractharnesses forIndexRange::next_uncheckedandIndexRange::next_back_unchecked, introduced in a0fca1c (#451), construct theirIndexRangeviaIndexRange::new_unchecked(start, end)with entirely unconstrainedstartandend. That violatesnew_unchecked's documented safety precondition (and#[requires]contract)start <= end: the assumption provided by the contract under verification only takes effect at the call tonext_unchecked/next_back_unchecked, after the UB of the unchecked constructor call has already happened.The violation is currently invisible in CI because
run-kani.shpasses--no-assert-contracts; with dependency contracts asserted (the Kani default since model-checking/kani#3802),proof_for_index_range_next_back_uncheckedfails on the assertedstart <= endclause.This PR constrains both harnesses with
kani::assume(start <= end). The strongerstart < endrequired by the functions under verification continues to be assumed from their own contracts, preserving the intent of the harnesses.Verified with Kani 152c6a8c + CBMC 6.10.0: all three
ops::index_range::verifyharnesses pass both with and without--no-assert-contracts.Found while investigating what still blocks removing
--no-assert-contractsfromrun-kani.sh: this is one of two genuine latent contract violations that asserting dependency contracts surfaces (the other: #622).By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.