[Challenge 6 Safety of NonNull] Verify contracts and proofs within the library source file

[QinyuanWu]

We are AWS team 4 from CMU(@QinyuanWu @danielhumanmod @Jimmycreative @Dhvani-Kapadia) working on Challenge 6: Safety of Nonnull. We have written the contract and proof for the new_unchecked function in library/core/src/ptr/non_null.rs. We followed a similar structure as contracts and proofs in library/core/src/ptr/unique.rs.

Target function with contract:

impl<T: Sized> NonNull<T> {
    #[requires(!ptr.is_null())]
    #[ensures(|result| result.as_ptr() == ptr)]
    pub const unsafe fn new_unchecked(ptr: *mut T) -> Self {
        // SAFETY: the caller must guarantee that `ptr` is non-null.
        unsafe {
            assert_unsafe_precondition!(
                check_language_ub,
                "NonNull::new_unchecked requires that the pointer is non-null",
                (ptr: *mut () = ptr as *mut ()) => !ptr.is_null()
            );
            NonNull { pointer: ptr as _ }
        }
    }

Kani proof for new_unchecked:

#[cfg(kani)]
use crate::kani;
mod verify {
    use super::*;

    // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
    #[kani::proof_for_contract(NonNull::new_unchecked)]
    pub fn check_new_unchecked() {
        let mut x : i32 = kani::any();
        let xptr = &mut x;
        unsafe {
            let _ = NonNull::new_unchecked(xptr as *mut i32);
        }
    }
}

We followed the instructions on this page with the command kani verify-std -Z unstable-options "path/to/library/" -Z function-contracts -Z mem-predicates, and we have two issues:

1. According to the verification result, we couldn't find any relevant check that was run for the check_new_unchecked proof in non_null.rs. Are we writing proofs in the correct location?
2. It seems like when we run the command above many functions are being verified at the same time. Is there a way to only verify a single contract/harness when using verify-std -Z unstable-options?

Thank you and we appreciate your guidance^_^ @feliperodri @rahulku

[zhassan-aws]

Hi @QinyuanWu. Thanks for opening this issue. The contract for new_unchecked looks good.

From looking at the log, it seems that the harness you wrote was not run. You can specify the --harness option to run a specific one, e.g.

kani verify-std -Z unstable-options "path/to/library/" -Z function-contracts -Z mem-predicates --harness check_new_unchecked

You might also want to use the fully-qualified name for the harness to avoid running other harnesses with the same name, e.g. --harness core::ptr::non_null::verify::check_new_unchecked.

[QinyuanWu]

Thank you for the response @zhassan-aws. I found that without supplying the --harness option, both proofs in unique.rs and non_null.rs are not run. Why is this? If we want to batch run proofs in non_null.rs in the future what command should we use? --harness core::ptr::non_null::verify::check_new_unchecked did not work(error: no harnesses matched the harness filter) and so does --harness core::ptr::non_null::NonNull::check_new_unchecked. I ended up changing the harness function name to a unique one(--harness non_null_check_new_unchecked) and that was successful(the fully-qualified name still has an error).

A second question is if the contract has specified a pre-condition(e.g. !ptr.is_null()), does that mean in the harness we don't need to make the assumption that xptr is not null? In other words, the ensures clause acts like an assume statement?

[feliperodri]

Hi, @QinyuanWu! We should keep all communication about this challenge in the specific GitHub issue referenced in the book. #53 is the corresponding issue for challenge 6. I'll close this one and we can continue the discussion there.