Remove spurious comments about the need for quantifiers - #457
Merged
Conversation
None of the (three) cases where we previously claimed a need for quantifiers actually require them.
feliperodri
approved these changes
Aug 12, 2025
carolynzech
reviewed
Aug 13, 2025
feliperodri
enabled auto-merge
October 8, 2025 15:48
thanhnguyen-aws
approved these changes
Oct 8, 2025
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>
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
5 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.
None of the (three) cases where we previously claimed a need for quantifiers actually require them.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.