Implement MBT for ICS04 Channel handlers

[andrey-kuprianov]

We need to initiate model-based testing for IBC-rs; while initially IBC client handlers (ICS02) have been chosen for that, we have decided to do it for ICS04 Channel handlers instead; see the explanation below.

The goal is to complement the current manual tests for channel handlers with MBT-based ones, such that model-based tests will be able to explore unexpected corner cases.

We can split the work here in multiple parts, as follows:

• ICS02: Model-based tests for ICS02 informalsystems/hermes#601
• ICS03: MBT for ICS03 informalsystems/hermes#701
• ICS04

Bugs found with MBT:

• modules: Fix panic in conn open try when no connection id is provided informalsystems/hermes#626
• Overflow if ctx.host_current_height().revision_height < ctx.host_chain_history_size() informalsystems/hermes#685
• conn open ack does not succeed in the happy case informalsystems/hermes#699

[andrey-kuprianov]

We have figured out that client handlers are too primitive to throw the heavy MBT machinery at them; e.g. the CreateClient handler is only incrementing one counter, so no real logic to test.

Considering that now the Channel handlers are coming to completeness, we are shifting focus to them. They have quite non-trivial implementation, that deserves thorough testing; see e.g. the ChanOpenTry handler.

The corresponding TLA+ model is also non-trivial, so this seems to be a good match for MBT.

[plafer]

Closing this as stale; we should reformulate these issues when we address #148 (and our correctness strategy in general).