Use addr_eq in NonNull contracts to support wide pointers

[tautschnig]

Several postconditions in NonNull compared raw pointers with == or core::ptr::eq: as_ptr, new, new_unchecked, the slice as_mut_ptr, and — via ptr::eq — as_ref, as_mut, as_uninit_ref and as_uninit_mut. For wide pointers (T: ?Sized with dyn metadata) such comparisons also compare vtable pointers, whose identity is unspecified in Rust; Kani rejects them with "Reached unstable vtable comparison 'Eq'". With dependency contracts asserted (the Kani default since model-checking/kani#3802), any harness whose call graph evaluates these clauses on a trait-object NonNull fails, e.g. ptr::non_null::verify::non_null_check_from_raw_part_trait (the comparison surfaces in ptr::eq::<dyn SampleTrait>, reached from as_ref's postcondition).

This PR compares with core::ptr::addr_eq instead, which is well-defined for any pointer types. All these functions produce their result directly from self, so metadata is preserved by construction, and the accompanying comments already described the intent as address preservation. The casts in the as_uninit_* clauses need explicit turbofish types now that the comparison no longer constrains their type parameter.

Verified with Kani 152c6a8c + CBMC 6.10.0: non_null_check_from_raw_part_trait now passes with contracts asserted — this was the last remaining verdict difference on a 125-harness sample between runs with and without --no-assert-contracts. The non_null_check_{as_ref,as_mut,as_uninit*,from_raw_part*,as_ptr,new} harnesses pass in both configurations, with one exception: non_null_check_as_uninit_slice_mut fails with contracts asserted both with and without this change (a pre-existing dereference/alignment issue reached via asserted contracts, tracked separately).

Part of the --no-assert-contracts removal effort (#622, #623, #624, #625, model-checking/kani#4709, model-checking/kani#4710).

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

Updates NonNull contract postconditions to avoid using raw-pointer == on wide pointers (notably dyn Trait), which can compare vtable metadata and is not well-defined (and rejected by Kani). The PR switches these postconditions to core::ptr::addr_eq, aligning the contracts with the documented intent of “address preservation”.

Changes:

• Replace == pointer comparisons with core::ptr::addr_eq in NonNull::{new, new_unchecked, as_ptr} postconditions.
• Add explanatory comments documenting why addr_eq is required for wide-pointer correctness.
• Apply the same addr_eq approach to NonNull<[T]>::as_mut_ptr’s “address preservation” contract.

[feliperodri]

Static review (no local Kani run this time). Replacing == / core::ptr::eq with core::ptr::addr_eq in the NonNull address-preservation ensures clauses is correct: for wide pointers, ==/ptr::eq also compare metadata (vtable identity is unspecified, and Kani rejects the vtable comparison), whereas these postconditions only intend address preservation and the metadata is preserved by construction. The explicit cast::<MaybeUninit<T>>() turbofish is needed once type inference no longer flows through the comparison. All modified functions (as_uninit_ref/as_uninit_mut/new_unchecked/new/as_ptr/as_ref/as_mut/as_mut_ptr) have proof_for_contract. No concerns.