Explore interaction of model-based and property-based testing

[andrey-kuprianov]

Following the efforts to apply PBT in #709 (see backward.rs), #792, #815, as well as discussion within the MBT team, we need to understand how to properly integrate MBT and PBT.

The high-level idea is not to reinvent the wheel by writing our own fuzzers, and instead to leverage the PBT infrastructure as done by proptest. In that, the test cases that span over several computation steps will be generated by MBT, and then mutated by PB strategies tendermint-rs datastructures. The main complication here is how to correctly express what changes should happen to the expected test outcome when the intermediate computation steps are mutated.

As the first step for the exploration we have decided to replace one of the manual fuzzing steps as done in model_based.rs with the proptest-based one, in particular to replace fuzzing of Time.

For successful completion of this issue:

• write a PB-test that accepts the MB-test case, and fuzzes time fields in various test case blocks
• fuzzing should be done using combinators over the proptest strategies developed in Property based tests of Time #815
• the PB-test should explore different options wrt. how the fuzzed time relates to other times in the test case:
  • to the trusting period
  • to the time of neighbouring blocks
    Depending on that the expected verdict should be modified accordingly.
• (optional) explore possible new macros to concisely express such MBT-specific PB-tests/strategies.