Contracts & Harnesses for Reference Conversion APIs at std::NonNull

[danielhumanmod]

Description:
This PR introduces function contracts and proof harness for the NonNull pointer in the Rust core library. Specifically, it verifies reference conversion APIs, covering:

• NonNull::as_mut<'a>
• NonNull::as_ref<'a>
• NonNull::as_uninit_mut<'a>
• NonNull::as_uninit_ref<'a>
• NonNull::as_uninit_slice<'a>
• NonNull::as_uninit_slice_mut<'a>
• NonNull::get_unchecked_mut

Proof harness:

• non_null_check_as_mut
• non_null_check_as_ref
• non_null_check_as_uninit_mut
• non_null_check_as_as_uninit_ref
• non_null_check_as_as_uninit_slice
• non_null_check_as_uninit_slice_mut
• non_null_check_as_get_unchecked_mut

Towards #53

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[danielhumanmod]

Hi @carolynzech , thanks for your review and suggestions! I have updated the code based on your comments, and solved most of them.

But one thing I can not directly do is add a in-bound check in function contracts for get_unchecked_mut.

The reason is the input index cannot be reused after being consumed in the precondition due to the shift of ownership. And SliceIndex trait does not guarantee that index implements Clone or Copy, it cannot be reused after being consumed in the precondition. To comply with Rust's ownership rules and ensure index is only used once, the in-bounds check is moved to the proof harness as a workaround.

[qinheping]

LGTM, thank you!

[danielhumanmod]

Hi @carolynzech @qinheping , do you mind triggering the merge flow for this PR again, I just solved some conflicts, thanks!

[carolynzech]

trigger approval workflow