Adopt Property Based Testing

[ebuchman]

We want to produce an example of using property based testing in our code.

This issue will be complete when a single example is completed. This can be as simple as a spike.

Tony mentioned proptest in - #261 (comment) and #248 (comment)

[tony-iqlusion]

Some alternatives to consider:

• quickcheck - original Rust port of QuickCheck
• crux-mir - symbolic execution of Rust MIR code inside the yices SMT solver, with the ability to write tests in Rust. Requires an awful lot of RAM for anything remotely complicated.

All that said, I use proptest.

[ebuchman]

@thanethomson want to look into this at some point? We've had a lot of serialization issues like #451 from insufficient testing ...

I'm going to add this to next milestone which already has a lot of other testing stuff for the light client but we should keep in mind the need to improve testing the serialization boundary as well even if it needs to happen iteratively through follow up issues

[thanethomson]

@ebuchman sure thing! Added it to the backlog 👍

[ebuchman]

Interesting emerging relevant work from Google: https://alastairreid.github.io/why-not-both/

[konnov]

Nice that Google joins the race. Microsoft Research has been generating unit tests with model checking for ages: https://www.microsoft.com/en-us/research/publication/pex-white-box-test-generation-for-net/

[tarcieri]

The Project Oak approach is quite a bit different from "generating unit tests with model checking".

It provides a common API for property-based testing and symbolic execution systems, which is nice because those systems have a common developer-facing API (test oracle versus assertions) but different tradeoffs (exhaustiveness vs system resource requirements).

[shonfeder]

I talked with @thanethomson and @ebuchman about picking up this issue. Thane and I are going to sync next week, and I've reached out to Romain to get some pointers from him as well.

[thanethomson]

I'd say that we now have a few examples of PBT in the codebase and it certainly adds some additional assurances to the correctness of the code it's testing, so subsequent issues regarding PBT can focus on more specific areas to be tested and this one can be closed.