Add proof for Result method check_unwrap_unchecked

[jaisnan]

Adds a simple contract that checks for memory safety in check_unwrap_unchecked.
Also useful for my secret agenda of testing the PR workflow in production.

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

[jaisnan]

As shown by the CI run here, this proof fails verification with the following property failure

Check 158: panicking::assert_failed_inner.assertion.2
	 - Status: FAILURE
	 - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime"
	 - Location: library/core/src/panicking.rs:408:17 in function panicking::assert_failed_inner

[jaisnan]

Additionally, both Result<u32, u64> and Result<(), ()> trigger the same failure.

[celinval]

Thanks @jaisnan, let's investigate why this is failing.

[carolynzech]

Since val is a nondeterministic Result, it's not necessary equal to Result::Ok(0) (it could also be Result::Err, or Result::Ok(12), etc.).
Instead, I'd write:

pub fn check_unwrap_unchecked() {
        let val: u32= kani::any();
        let ok_variant: Result<u32, u64> = Ok(val);
        let copy = unsafe { ok_variant.unwrap_unchecked() };
        assert_eq!(val, copy);
    }

which passes verification for me locally.

(I'd also add harnesses for other types besides u32 and for unwrap_err_unchecked, but I assume you were planning on that).