Allow zero-sized offsets on dangling pointers in ptr contracts

[tautschnig]

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 #113 (014965a) and #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 #622, #623, #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.

[Copilot]

Pull request overview

This PR updates the formal contracts on core pointer-arithmetic APIs to match the documented Rust semantics that zero-sized offsets are permitted even on dangling pointers, avoiding unnecessary same_allocation requirements that break valid std patterns (e.g., empty slices backed by dangling-but-aligned pointers) when dependency contracts are asserted.

Changes:

• Relax #[requires]/#[ensures] for *mut T::{offset,add,sub} and *const T::{offset,add,sub} by short-circuiting allocation checks when count == 0 (and preserving the existing ZST escape).
• Relax NonNull::{add,sub} similarly with a count == 0 || size_of::<T>() == 0 escape before same_allocation.
• Relax NonNull::offset_from_unsigned by allowing equal-address pointers to bypass same_allocation (zero-sized span), matching the precedent in raw-pointer offset_from.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
library/core/src/ptr/non_null.rs	Weakens NonNull pointer arithmetic contracts to allow zero offsets / equal-address spans without requiring same_allocation.
library/core/src/ptr/mut_ptr.rs	Weakens *mut T offset/add/sub contracts to skip allocation checks when count == 0.
library/core/src/ptr/const_ptr.rs	Weakens *const T offset/add/sub contracts to skip allocation checks when count == 0.

[feliperodri]

Static review (no local Kani run this time). Adds a count == 0 (plus the existing size_of::<T>() == 0) short-circuit to the same-allocation pre/postconditions of offset/add/sub across const_ptr, mut_ptr and NonNull, and an equal-address short-circuit to NonNull::offset_from. This is a sound precondition relaxation: zero-sized offsets and zero-length spans are always valid per the pointer-method docs, including on dangling pointers such as empty-slice pointers, so the clauses previously rejected inputs that are actually UB-free. The change is identical across the three impls; the mut_ptr and NonNull versions are directly exercised by proof_for_contract.

Minor note: const_ptr's offset/add/sub have no direct proof_for_contract (pre-existing — only offset_from/byte_offset do), so those particular clauses are exercised only transitively / once dependency contracts are asserted; the change is nonetheless sound by inspection and matches the directly-verified mut_ptr/NonNull versions. No concerns.