undefined | Better HN

0 pointsworldsavior11mo ago0 comments

The test is supposed to be the verification.

0 comments

Test verify that the code works on specific inputs. Formal verification checks that it works on every input.

Can't you make the tests check every input? (This is also what they're supposed to do.)

I don't know why you are trolling us. Tests aren't supposed to check every input. The entire point of classic testing is to define static execution traces by hand. That is obviously meant to only cover a finite number of execution traces. Even 100% test coverage doesn't give you proof over all possible execution traces. Tests prove that the software "works", but they do not prove the absence of bugs (which inherently requires you to specify what a "bug" is, hence the need for a specification).

Not only is static verification more powerful, there is also a massive usability difference. You define your pre and post conditions in each function (also known as specification or design contract) and the tool will automatically check that you do not violate these conditions. It solves a very different problem from classic unit or integration tests.

sangel11mo ago

Obviously not. Suppose the input to my function is a 64-bit integer. My test cannot possibly try every possible 64-bit integer. It would take years for such a test to finish.

This is why tools like formal verification and symbolic analyses can help you establish that for all possible integers X, your function does the right thing (for some definition of “right”). You get this assurance without having to actually enumerate all X.

1 more reply

nextaccountic11mo ago

But why? Tests can't catch everything. A single verified predicate is equivalent to a very large, potentially infinite number of tests.

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

    #[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

https://github.com/model-checking/verify-rust-std/blob/00169...

    #[requires(!ptr.is_null())]
    #[ensures(|result| result.as_ptr() == ptr)]

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.

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.

keybored11mo ago

Say I have as input a byte. I create a test that exercises every possible byte value.

A verification would be the equivalent of that. In practice that matters since the input space is often much larger than just one byte.

j / k navigate · click thread line to collapse

0 comments

GolDDranks11mo ago

Test verify that the code works on specific inputs. Formal verification checks that it works on every input.

worldsaviorOP11mo ago

Can't you make the tests check every input? (This is also what they're supposed to do.)

imtringued11mo ago

sangel11mo ago

Obviously not. Suppose the input to my function is a 64-bit integer. My test cannot possibly try every possible 64-bit integer. It would take years for such a test to finish.

1 more reply

nextaccountic11mo ago

But why? Tests can't catch everything. A single verified predicate is equivalent to a very large, potentially infinite number of tests.

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

    #[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);
        }
    }

https://github.com/model-checking/verify-rust-std/blob/00169...

    #[requires(!ptr.is_null())]
    #[ensures(|result| result.as_ptr() == ptr)]

Which means: if the caller guarantees that the parameter ptr is not null, then result.as_ptr() is the same as the passed ptr

You can check out other proofs here https://github.com/search?q=repo%3Amodel-checking%2Fverify-r...

keybored11mo ago

Say I have as input a byte. I create a test that exercises every possible byte value.

A verification would be the equivalent of that. In practice that matters since the input space is often much larger than just one byte.

j / k navigate · click thread line to collapse