Relayer TLA+ spec enhancements/features originating from PR reviews

[istoilkovska]

Summary

This issue summarizes questions raised and suggestions proposed during pull request reviews of the Relayer TLA+ specification, which may need further discussion/clarification.

Problem Definition

1. Relayer client heights. Currently, each relayer process stores the latest height of each chain locally.
   Questions:

   • Should the relayer store client heights?
   • Should it have action that updates the heights of its clients?

2. Datagram transmission. Currently, the datagrams the relayers create are stored in a set, thus losing the order in which they were created.
   Questions:

   • Should the outgoing datagrams from the relayer and the incoming datagrams to the chains be stored in a set or sequence?

3. Creation of client datagrams. It would be nice to paramterize the operators for creating client datagrams by height. If the datagrams are created for height h, then the light client updates are created for height h+1, as the root hash for datagrams created at height h is stored in the block h+1.

4. openInit datagrams. Currently, the relayer creates ConnOpenInit and ChanOpenInit datagrams. In ICS003 and ICS004, it is noted that the chains are initiators of these datagrams
   Questions:

   • Should the relayer trigger the creation of ConnOpenInit and ChanOpenInit datagrams, or should it be done by the environment using non-deterministically assigned Boolean flags?

5. Packet datagrams creation. The TLA+ specification at the moment follows ICS018, where the relayer does not do any checks locally on the validity of the data it uses to create PacketRecv and PacketAck datagrams. It is assumed that the handlers on the chain side do these checks and discard the irrelevant datagrams. It would be good to add these checks in order to model the cases when it is desirable to not even send invalid datagrams to the chains (e.g., in the case when a fee has to be paid). Necessary checks:
   a. check that the counterparty has not yet received the packet when creating PacketRecv datagrams
   b. check that the packet commitment has been deleted when creating PacketAck datagrams

---

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned

[ebuchman]

@milosevic @istoilkovska based on #224 (comment) I'm going to bump this to v0.0.5 so we can focus on #124 first (though it's possible point 2 about datagram ordering will be relevant for that).