PBT: Write ADR for property-based testing

[p-offtermatt]

Problem

Our current tests on ICS are mostly manually written, which necessarily means they can only cover scenarios that a human has come up with. We want a form of randomized tests that test invariants/correctness properties.

Closing criteria

We have an ADR for the infrastructure for Property-Based Testing.

Problem details

Previous approaches for this problem include difftesting and MBT. The downside of those approaches is that they need a re-implementation of the system-under-test.

Instead, we want to do property-based testing, where only correctness properties have to be written.

[p-offtermatt]

Keeping some notes for the ADR here:

We need 4 components for PBT:

• A way to express correctness properties (potentially as Quint, Golang, or potentially plain English)
• A driver that triggers the possible actions of the system (where the existing MBT driver can probably be reused)
• A way to express preconditions that describe when certain actions should be possible (see this in the Cosmos SDK simulator https://github.com/cosmos/cosmos-sdk/blob/62212dfc04b3790f3cc052cdc2fb757b32ca97d0/x/bank/simulation/operations.go#L300)
• A way to fuzz/randomly generate actions of the system to perform

It might be possible to reuse many things from the cosmos sdk simulator and the existing MBT driver utilizing ibc-go. Potentially, the best way to frame this is to expand the Cosmos SDK simulator with capability for multi-chain interactions.