Spike: Model-based testing of Hydra protocol using quickcheck-dynamic

[abailly-iohk]

Context

• Step 1 of certification for DApps involve implementing model-based testing along the lines of https://plutus-apps.readthedocs.io/en/latest/plutus/tutorials/contract-models.html#becoming-level-1-certification-ready
• On top of on-chain contracts, Hydra Head Protocol add off-chain interactions and protocol between the Hydra nodes
• Following the discussion in https://github.com/input-output-hk/hydra-poc/wiki/Formalising-Hydra we need our model to take into account both on-chain and off-chain parts in order to be able to test/prove the expected security properties (eg. Consistency, Completeness ...)

Details

In order to check one important property of the Head Protocol, namely Completeness: Whenever a tx is confirmed on L2, it's eventually fanned-out on L1.

We want to model the system at UI layer and replacing or supplementing the existing BehaviorSpec with MBT using:

• QD for modelling and driving the state
• the same kind of idealised chain and network we use in BehaviorSpec

Ideally, later on we will integrate this with on-chain code through emulation of chain.

[ch1bo]

Closed by #391, we have identified some follow ups in sub-tasks to #194