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

Resolves #53

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