Do not dereference in slice_from_raw_parts postcondition

[tautschnig]

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 (#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 #622, #623, #624, #625, #626).

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 the verification postcondition for NonNull::slice_from_raw_parts to avoid dereferencing potentially dangling/misaligned pointers during contract evaluation, aligning the contract with the function’s documented safety behavior.

Changes:

• Replace the postcondition’s unsafe { result.as_ref() }.len() with result.len() to read slice length from wide-pointer metadata without creating a reference.
• Add an explanatory comment documenting why dereferencing in the postcondition is UB for valid (but non-dereferenceable) inputs to this safe constructor.