#[kani::proof_for_contract(NonNull::new_unchecked)]
pub fn non_null_check_new_unchecked() {
let raw_ptr = kani::any::<usize>() as *mut i32;
unsafe {
let _ = NonNull::new_unchecked(raw_ptr);
}
}
It looks like a test, but actually it is testing that every possible usize, when converted to a pointer to i32 and built with NonNull::new_unchecked, will follow the contract of NonNull::new_unchecked, which is defined here
Which means: if the caller guarantees that the parameter ptr is not null, then result.as_ptr() is the same as the passed ptr
That's a kind of trivial contract but Kani tests for all possible pointers (rather than some cherry picked pointers like the null pointer and something else), without actually brute-forcing them but instead recognizing when many inputs test the same thing (while still catching a bug if the code changes to handle some input differently). And this approach scales for non-trivial properties too, a lot of things in the stdlib have non-trivial invariants.
It's not that different from writing a regular test, it's just more powerful. And you can even use this #[requires] and #[ensures] syntax to test properties in regular tests if you use the https://crates.io/crates/contracts crate.
Really if you have ever used the https://proptest-rs.github.io/proptest/intro.html or the https://crates.io/crates/quickcheck crate, software verification is like writing a property test, but rather than testing N examples generated at random, it tests all possible examples at once. And it works when the space of possible examples is infinite or prohibitively large, too.
Right now the Rust stdlib is being verified using Kani, a model checker, https://model-checking.github.io/verify-rust-std/
In Kani, a proof looks like this
https://github.com/model-checking/verify-rust-std/blob/00169...
It looks like a test, but actually it is testing that every possible usize, when converted to a pointer to i32 and built with NonNull::new_unchecked, will follow the contract of NonNull::new_unchecked, which is defined herehttps://github.com/model-checking/verify-rust-std/blob/00169...
Which means: if the caller guarantees that the parameter ptr is not null, then result.as_ptr() is the same as the passed ptrThat's a kind of trivial contract but Kani tests for all possible pointers (rather than some cherry picked pointers like the null pointer and something else), without actually brute-forcing them but instead recognizing when many inputs test the same thing (while still catching a bug if the code changes to handle some input differently). And this approach scales for non-trivial properties too, a lot of things in the stdlib have non-trivial invariants.
You can check out other proofs here https://github.com/search?q=repo%3Amodel-checking%2Fverify-r...
It's not that different from writing a regular test, it's just more powerful. And you can even use this #[requires] and #[ensures] syntax to test properties in regular tests if you use the https://crates.io/crates/contracts crate.
Really if you have ever used the https://proptest-rs.github.io/proptest/intro.html or the https://crates.io/crates/quickcheck crate, software verification is like writing a property test, but rather than testing N examples generated at random, it tests all possible examples at once. And it works when the space of possible examples is infinite or prohibitively large, too.