Challenge 12: Safety of `NonZero`

[carolynzech]

Challenge link: https://model-checking.github.io/verify-rust-std/challenges/0012-nonzero.html

[aa-luna]

We are Team 1 and currently working on this challenge.

PM: Shivani
TL: @aa-luna
Devs: @SahithiMV ; @lang280

[aa-luna]

Team,

We are currently trying to test an initial harness but are having some issues. We confirmed it has a unique name and qualified name, it is under mod verify, and follows the similar syntax of AsciiChar. Appreciate any feedback.

Commands:

verify-rust-std/library$ kani verify-std -Z unstable-options "." -Z function-contracts -Z mem-predicates --harness nonzero_check_new_unchecked

and received:

error: no harnesses matched the harness filter: `nonzero_check_new_unchecked`

We also tested:

kani verify-std -Z unstable-options "." -Z function-contracts -Z mem-predicates --harness core::num::nonzero::nonzero_check_new_unchecked

and received:

error: no harnesses matched the harness filter: `core::num::nonzero::nonzero_check_new_unchecked`

Our current contract function:

#[requires(n != T::zero())]
#[ensures(|result: Self| result.get() == n)]
pub const unsafe fn new_unchecked(n: T) -> Self {
	match Self::new(n) {
		Some(n) => n,
		None => {
			// SAFETY: The caller guarantees that `n` is non-zero, so this is unreachable.
			unsafe {
				ub_checks::assert_unsafe_precondition!(
					check_language_ub,
					"NonZero::new_unchecked requires the argument to be non-zero",
					() => false,
				);
				intrinsics::unreachable()
			}
		}
	}
}

Proof for contract:

#[unstable(feature="kani", issue="none")]
#[cfg(kani)]
mod verify {
use core::num::NonZeroI32; // Use core::num instead of std::num

// pub const unsafe fn newunchecked(n: T) -> Self
#[kani::proof_for_contract(NonZero::new_unchecked)]
pub fn nonzero_check_new_unchecked() {
    let x: i32 = kani::any();  // Generates a symbolic value of type i32

    // Only proceed if x is not zero, because passing zero would violate the precondition
    kani::assume(x != 0);

    unsafe {
        let _ = NonZeroI32::new_unchecked(x);  // Calls NonZero::new_unchecked
        }
    }
}

[QinyuanWu]

@aa-luna try --harness num::nonzero::verify::nonzero_check_new_unchecked Also could you point me to the location of your harness?

[aa-luna]

Thanks, @QinyuanWu, but still did not find. I'm guessing it's a placement issue. We will keep looking around to resolve this.
https://github.com/RustyRelic/verify-rust-std/blob/main/library/core/src/num/nonzero.rs

[carolynzech]

@aa-luna I cloned your repository, and when I do the following:

1. Build Kani from the features/verify-rust-std branch (see here)
2. Run export PATH=../kani/scripts:$PATH in a terminal window for the verify-rust-std repo (substitute the path to Kani appropriately depending on where yours lives)
3. Run kani verify-std -Z unstable-options ./library --target-dir /tmp/verify-rust-std -Z function-contracts -Z mem-predicates --harness nonzero_check_new_unchecked 2>&1

I get some compilation errors about your contracts:

error[E0599]: no function or associated item named `zero` found for type parameter `T` in the current scope
   --> /Users/cmzech/student/library/core/src/num/nonzero.rs:371:24
    |
345 | impl<T> NonZero<T>
    |      - function or associated item `zero` not found for this type parameter
...
371 |     #[requires(n != T::zero())]
    |                        ^^^^ function or associated item not found in `T`
    |
    = help: items from traits can only be used if the type parameter is bounded by the trait
help: the following trait defines an item `zero`, perhaps you need to restrict type parameter `T` with it:
    |
347 |     T: ZeroablePrimitive + fmt::num::DisplayInt,
    |                          ++++++++++++++++++++++

error[E0369]: binary operation `==` cannot be applied to type `T`
   --> /Users/cmzech/student/library/core/src/num/nonzero.rs:372:43
    |
372 |     #[ensures(|result: Self| result.get() == n)]
    |                              ------------ ^^ - T
    |                              |
    |                              T
    |
help: consider further restricting this bound
    |
347 |     T: ZeroablePrimitive + cmp::PartialEq,
    |                          ++++++++++++++++

error: aborting due to 2 previous errors

These compilation errors would happen earlier in the pipeline than a harness location issue. I would make sure that you're following the steps above so that rustc is compiling the version of your code with contracts attached. Once you fix these compilation errors, you should be able to run the command in step 3 to run your harness.

[aa-luna]

Issue resolved. Thank you.