MBT low-friction maintenance

[adizere]

Crate

primarily ibc

Problem Summary

We wish to avoid reaching a situation where we have to disable MBT tests because "no one understands what's happening there," and minimize the risk of these tests becoming easily outdated.

We can close this issue if we manage to answer this question: how can an ibc-rs developer do changes to the codebase without facing significant challenges with respect to MBT?

Context

MBT is progressing very nicely for modules (#701, informalsystems/hermes#601).

Before adding additional code and features to this testing method, it would be helpful to understand how we plan to keep MBT aligned with the codebase. This is a concern because there are several major changes slated for the next few months (hopefully). Here are some:

• add proof verification (which may need an actual IAVL/kv store)
• introduce capabilities & permissions (Fix issue with the error variant of new_check_header_and_update method #406)
• refactor error-handling (see the concrete example below)
• add more clients (e.g., for solo machine Solo machine client support informalsystems/hermes#705)
• the "modifying handshake" Hermes user story (no issue yet for this)

Concrete example

To frame the discussion in a concrete example, we can look at error handling and how the codebase will (probably) evolve in that respect. Not sure if this is the best example, but its one of the simplest..

For refactoring error-handing in the modules, the discussion in informalsystems/hermes#68 provides a good idea of what we'd like to do (see in particular this comment) and almost did (#493 but it was too much work, and not a priority at that point).

A typical modification here involves changing error types. An error is currently an anomaly::Error<Kind>, so we'd like to throw away the anomaly part and retain just the enum Kind, which we can rename into enum Error. Consequently we would change the return types pretty much everywhere, for instance:

@@ -496,13 +496,13 @@ impl ClientDef for AnyClient {
         client_id: &ClientId,
         proof: &CommitmentProofBytes,
         client_state_on_counterparty: &AnyClientState,
-     ) -> Result<(), Box<dyn std::error::Error>> {
+     ) -> Result<(), Error> {
         match self {
             Self::Tendermint(client) => {
                 let client_state = downcast!(
                     client_state => AnyClientState::Tendermint
                 )
-                 .ok_or_else(|| Kind::ClientArgsTypeMismatch(ClientType::Tendermint))?;
+                 .ok_or_else(|| Error::ClientArgsTypeMismatch(ClientType::Tendermint))?;

Question: would a modification as above break MBT, because the tests assume specific error types, names? If yes, we should try to make it so that it's relatively simple to get the tests to run again.

---

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate milestone (priority) applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned

[andrey-kuprianov]

That is a great question to ask, Adi (@adizere)! I completely share your concerns. Here is my current view:

No code works without tests. Unit tests are a must, and It seems to be a consensus within Tendermint-rs & IBC-rs devs that property-based tests are also needed (see TM-rs#792, TM-rs#709, or TM-rs#815). Let's work from this assumption.

To properly write both unit tests and PB-tests, the key, imho, is abstraction -- the ability to generate your concrete datastructures from abstract inputs, with the possibility to omit a lot of details, and bring them back only when needed. Testgen is a good example of such abstraction for TM-rs types. It probably should live closer to the datastructures but that's a different story. Another example of abstraction you may find in Vitor's PR informalsystems/hermes#701, see executor/mod.rs. Interestingly, PB-tests also require this to write good strategies, so let's agree that abstraction is needed.

Thus, we have these two components:

• your code provides good abstractions;
• your code has some manually written unit- and property-based tests, that cover the basic functionality.

Those two are very important to have in any project -- they will warn you in case if what you write fundamentally breaks something. In particular, these tests will tell you "sorry, you error type has changed, I will not compile".

But as you can see from PR informalsystems/hermes#701, it is exactly this abstraction that we need also for MBT! And it is the key component to enable it. Everything else can be automated away, and we are working towards such automation. The first version will be available by the end of Q1, and by the end of Q2 we will have a more or less complete one for Rust.

Here is a preview of what we'll have. MBT will consist of

• MBT-core, that encapsulates as much as possible of the target-language independent functionality, e.g. manipulating the models, or generating, storing, and navigating the tests.
• Plugins for target languages; the first one is going to be MBT-Rust. Those will be quite thin layers that interact with MBT-core, and only execute the provided tests in the target language.

Both MBT-core and MBT-Rust will be crates and executables external to IBC-rs, so no code to maintain here. What will be in IBC-rs:

• abstractions: those are also needed for unit- and PB-tests; MBT will simply reuse them. We will help to formulate the interfaces such that the reuse will happen with least friction.
• TLA+ model & TLA+ tests: those need to be manually written, but we are going to have some degree of automation here. In particular a lot of boilerplate TLA+ will be taken away from you.
• MBT config: a pretty minimal configuration, which will tell MBT what abstractions, models and tests to use, and what to test based on them.

So, you see, the maintenance should be low. As long as your unit- and PB-tests work, MBT will also work. As for the current PR informalsystems/hermes#701, it is still within the old approach when all code lives in the repo, but this will change after Q1, when we release the first version of MBT-core + MBT-Rust. I would just go ahead and merge it, with the understanding that we will refactor it in around a month from now.

[andrey-kuprianov]

Here are a couple of diagrams.

Old-style MBT

New MBT

[plafer]

Closing this as stale; we should reformulate these issues when we address #148.