MBT for ICS03

[vitorenesduarte]

Towards: cosmos/ibc-rs#30
Closes: #633

Description

Following #601, this is another step towards cosmos/ibc-rs#30.

This PR also closes #633 by storing all consensus states (heights in the TLA+ model), not just the latest one as before.

The number of added lines is scary but roughly 3K of them are from the test files automatically generated 😄 (these files don't need to be reviewed)

(BTW, I've noticed that the implementation distinguishes between ConnectionNotFound and UninitializedConnection, although these errors are returned in the same situation (when the connection does not exist).)

---

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 #701 (6b66f7e) into master (b1b37f5) will increase coverage by 31.0%.
The diff coverage is n/a.

@@            Coverage Diff            @@
##           master    informalsystems/hermes#701      +/-   ##
=========================================
+ Coverage    13.6%   44.7%   +31.0%     
=========================================
  Files          69     151      +82     
  Lines        3752    9905    +6153     
  Branches     1374       0    -1374     
=========================================
+ Hits          513    4429    +3916     
- Misses       2618    5476    +2858     
+ Partials      621       0     -621     

Impacted Files	Coverage Δ
modules/src/address.rs	100.0% <ø> (ø)
...application/ics20_fungible_token_transfer/error.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% <ø> (ø)
modules/src/ics02_client/events.rs	15.7% <ø> (+15.7%)	⬆️
... and 256 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 08db234...6b66f7e. Read the comment docs.

[andrey-kuprianov]

Great work, Vitor!
I am really happy to see MBT finally coming to IBC-rs:)

What's particularly valuable here is that you've managed to integrate TLC as an MBT backend, so in the future we will be able to have two backends for MBT: Apalache and TLC.

From my side everything looks good:

• contrary to the previous PR on ICS02, this is now a complete setup, allowing to add more tests via TLA+,
• The Rust code in executor also seem to provide a good basis to simplify writing unit tests,
• The TLA+ model also looks quite concise and at the same time extensible, e.g. to support multiple chains, or other ICSs.

While this PR does pollute the sources a bit with static test files, those are going to be removed when we release the combination of MBT-core + MBT-Rust. And also this PR is a good foundation for the MBT-Rust plugin, we are going to reuse there a lot of ideas from the PR.

[adizere]

Looks good. I ignored the TLA+ and json files, and beside those there are not many modifications. I'm curious: why did TLC replace Apalache?

I will open an issue to discuss how we plan to maintain this code in the face of upcoming modifications to the modules.

[adizere]

Nit, but I'd suggest the same improvement as before 5d6bf08

[vitorenesduarte]

The change in 5d6bf08 was reverted because the model doesn't know about revisions. Also, when generating the actual ChainId on the Rust side, we would get "chain-A-0-0":
https://github.com/informalsystems/ibc-rs/blob/3e513dbfd96fca6de0b2507bab5baff936b9864d/modules/tests/executor/mod.rs#L96-L98

[vitorenesduarte]

Looks good. I ignored the TLA+ and json files, and beside those there are not many modifications. I'm curious: why did TLC replace Apalache?

Because we found a way to automate the generation of those .json files given TLC's output. This is only temporary, and in the next PR both should be supported.

[ancazamfir]

impressive work! I ran all tests with coverage and we are in general > 80% coverage for the ICS02 and ICS03 handlers :)

I was trying to figure out how to increase that. For example there is a case where an OpenAck finds a connection in TryOpen state. Not sure how I should do this, if the model supports it, etc. I would normally start to look in detail through the TLA specs, properties and invariants, see if I have to add to it, or maybe we need more counterexamples? I can spend some time digging into this but was wondering if maybe it is a good idea to have a hands on session about this and understand how to approach and solve this particular problem.
At a higher level it would also help us get an idea on the effort it will take us (developers) to maintain and extend this.

update - just saw the new issue cosmos/ibc-rs#29 that is along the exact same lines.

[vitorenesduarte]

For example there is a case where an OpenAck finds a connection in TryOpen state. Not sure how I should do this, if the model supports it, etc.

Yes, the model already considers this case. It should be enough to change IBCTests.tla, adding a new test covering this case. Currently the tests described in IBCTests.tla are super simple and just specify the last actionOutcome of the test. We could instead ask for an open ack action about a connection in the TryOpen state.