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
        }
    }
}

Challenge 12: Safety of NonZero #71

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Challenge 12: Safety of `NonZero` #71