MBT: keep the latest N heights per client in TLA+ model

[vitorenesduarte]

Crate

modules

Problem Definition

The TLA+ model in #601 only keeps a single height per client. The Rust implementation of the mock chain keeps, per client, a ClientState and several ConsensusStates such that the height in the ClientState is the max of the heights in the all the ConsensusStates. Keeping several ConsensusStates allows verifying messages containing proofs with heights lower than the latest height (the one in the ClientState).

Proposal

The TLA+ model should be extended to instead keep the latest N heights per client. (In the current model, N = 1.)

---

For Admin Use

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

[ancazamfir]

This is a good start. In addition we should model the ClientState, Header and ConsensusState in the TLA for ICS02. Currently all these are equated to a height. I also believe we should have a TLA spec for ICS07 at some point and have MBT tests for ICS02+ICS07 that use Tendermint specific headers and states. We can open other issues for this but want to make sure we do this at some point.

[ancazamfir]

The implementation keeps, per client, a ClientState and several ConsensusStates such that the height in the ClientState is the max of the heights in the all the ConsensusStates.

Which implementation?

[vitorenesduarte]

The implementation keeps, per client, a ClientState and several ConsensusStates such that the height in the ClientState is the max of the heights in the all the ConsensusStates.

Which implementation?

The Rust implementation. I updated the top-level comment clarifying that.

[ancazamfir]

The implementation keeps, per client, a ClientState and several ConsensusStates such that the height in the ClientState is the max of the heights in the all the ConsensusStates.

Which implementation?

The Rust implementation. I updated the top-level comment clarifying that.

Maybe we should say the Rust implementation of the mock chain?
And then should we say:
The TLA+ model should be extended to instead keep the latest N consensus states per client. (In the current model, N = 1 and the consensus state is a height.)

I also think the TLA+ model should specify that the create_client includes a client state and a consensus state while the update_client includes a header. There is no distinction among these in the mock chain implementation but this will very likely change. Then the MBT code should take this into account.

[ancazamfir]

Also, iirc the TLA+ spec keeps multiple heights per client and I thought you confirmed when we talked last time.

[vitorenesduarte]

Maybe we should say the Rust implementation of the mock chain?

Done.

And then should we say:
The TLA+ model should be extended to instead keep the latest N consensus states per client. (In the current model, N = 1 and the consensus state is a height.)
Also, iirc the TLA+ spec keeps multiple heights per client and I thought you confirmed when we talked last time.

Yes, that's why I wrote The TLA+ model should be extended to instead keep the latest N heights per client but maybe I misunderstood what's the intention here. Why should it say latest N consensus states per client instead of latest N heights per client? What else should be consensus state be in the TLA+ model?

I also think the TLA+ model should specify that the create_client includes a client state and a consensus state while the update_client includes a header. There is no distinction among these in the mock chain implementation but this will very likely change. Then the MBT code should take this into account.

The TLA+ spec (not the one for MBT) also contains a single height in the create client datagram:
https://github.com/informalsystems/ibc-rs/blob/b654af39c0c658d831cff42ccb11ac5562a43793/docs/spec/tla/ibc-core/ICS02ClientHandlers.tla#L17-L21

[ancazamfir]

Yes, in create we just add one. But update should add to the client consensus state set. I believe around here: https://github.com/informalsystems/ibc-rs/blob/b654af39c0c658d831cff42ccb11ac5562a43793/docs/spec/tla/ibc-core/ICS02ClientHandlers.tla#L62-L69