Model-based tests for ICS02

[vitorenesduarte]

Towards: cosmos/ibc-rs#30

Description

This PR is the first step towards cosmos/ibc-rs#30. For ease of reviewing, we plan to introduce one ICS at a time, starting now with ICS02.

For some details on MBT and current limitations, please check modules/tests/README.md (which steals ideas from the light-client one).

---

For contributor use:

• Updated the Unreleased section of CHANGELOG.md with the issue.
• If applicable: Unit tests written, added test to CI.
• Linked to Github issue with discussion and accepted design OR link to spec that describes this work.
• Updated relevant documentation (docs/) and code comments.
• Re-reviewed Files changed in the Github PR explorer.

[codecov-io]

Codecov Report

Merging #601 (3a991e7) into master (b1b37f5) will increase coverage by 33.1%.
The diff coverage is n/a.

@@            Coverage Diff            @@
##           master    informalsystems/hermes#601      +/-   ##
=========================================
+ Coverage    13.6%   46.8%   +33.1%     
=========================================
  Files          69     150      +81     
  Lines        3752   10091    +6339     
  Branches     1374       0    -1374     
=========================================
+ Hits          513    4725    +4212     
- Misses       2618    5366    +2748     
+ Partials      621       0     -621     

Impacted Files	Coverage Δ
modules/src/address.rs	100.0% <ø> (ø)
...application/ics20_fungible_token_transfer/error.rs	0.0% <ø> (ø)
...pplication/ics20_fungible_token_transfer/events.rs	0.0% <ø> (ø)
...ion/ics20_fungible_token_transfer/msgs/transfer.rs	0.0% <ø> (ø)
modules/src/events.rs	0.0% <ø> (ø)
modules/src/handler.rs	100.0% <ø> (ø)
modules/src/ics02_client/client_def.rs	48.3% <ø> (ø)
modules/src/ics02_client/client_type.rs	79.1% <ø> (+31.5%)	⬆️
modules/src/ics02_client/context.rs	100.0% <ø> (ø)
modules/src/ics02_client/error.rs	100.0% <ø> (ø)
... and 258 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b654af3...3a991e7. Read the comment docs.

[adizere]

Impressive work!

My main worry is that we're introducing new TLA+ specs here, instead of leveraging (part of) what we already had. I'm curious what @ancazamfir, @andrey-kuprianov, and @istoilkovska think about this: would it be possible, at least eventually, to reuse Ilina's TLA+ specs for MBT?

[vitorenesduarte]

Thanks @adizere and @romac for the review! I just finished addressing all your comments.

[ancazamfir]

Looks good after a fist pass. Entered a few comments, will take another look.

[ancazamfir]

Let's merge this one and address any pending comments in #633.

[adizere]

Good work Vitor!