TLA+ Relayer invariants/safety properties

[istoilkovska]

Summary

In the current Relayer TLA+ specification, we check invariants and liveness properties:

• the invariants ensure that the relayer creates datagrams consistently with the chain states,
• the liveness properties state that the chains eventually act upon the datagrams they receive from the relayer.

We should also specify safety properties, which ensure that a chain does not act upon a datagram that was not created (or was created by a faulty relayer).

Problem Definition

The invariants we have currently are of the following kind:

• If the relayer sends a datagram, then the chain for which the datagram is designated was in a state that triggered the creation of the datagram.
• Example: if the relayer sends a CreateClient datagram for chainA, then there is no client for chainB at chainA.

These invariants hold true only when the Relay action is atomic: that is, when we assume that the created datagrams are immediately delivered.
In a version of the TLA+ specification, where we have separate actions for creating and delivering datagrams, these invariants are violated.

Example: Suppose we are in a state where chainA has not created a client for chainB yet. The following execution violates the invariant stated above:

1. the relayer creates a CreateClient datagram for chainA
2. chainB takes a step
3. the relayer delivers the CreateClient datagram to chainA
4. chainB takes a step
5. the relayer creates a second CreateClient datagram for chainA (chainA still does not have a client for chainB)
6. chainA creates a client for chainB by processing the received CreateClient datagram, delivered in step (3)
7. the relayer delivers the second CreateClient datagram, created in step (5)
   the client for chainB on chainA is already created -> violation

This issue appears even in the setting of one correct relayer, in the case when the creation and delivery of datagrams are two separate actions. It is anticipated that it will occur in the setting with multiple relayers as well.

The current specification would discard the second datagram, as specified in HandleCreateClient in ClientHandlers.tla. Thus, the invariants are not expressing what we are interested in verifying.

Proposal

We should define the following safety properties in the TLA+ specification of the relayer:

ICS18Safety: Bad datagrams are not used to update the chain stores.

• Example: a ClientUpdate datagram with height less than the current highest counterparty client height is never added to the set of counterparty client heights.

ICS18Validity: If ChainB receives a datagram from ChainA, then the datagram was sent by ChainA

• Example: chainA does not update a client unless it receives a ClientUpdate datagram, created by a correct relayer.

In addition, we should specify safety properties for the handlers that the chains use to process the incoming datagrams. These safety properties should express that the handlers work as expected.

---

For Admin Use

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

[adizere]

Having separate actions for creating and delivering datagrams sounds like a good feature.

The invariants we have currently are of the following kind:
If the relayer sends a datagram, then the chain for which the datagram is designated was in a state that triggered the creation of the datagram.

Maybe we can refine this invariant. Below are two ways to restate it:

• If any relayer creates a datagram for a chain, then the chain for which the datagram is designated is in a state that triggered the creation of the datagram. [this probably reflects the behavior of a good relayer in practice, and should not be violated]
• If any chain processes (this is the post-delivery action) a datagram, then the chain is in the state that triggered the creation of that datagram. [this should reflect the safe behavior of a chain]

[adizere]

Also, from the work on the English spec for ICS3, we have the following safety properties:

1. [ICS3-Proto-1-ConnectionUniqueness] A module accepts (i.e., initializes on) a ConnectionEnd e at most once.

2. [ICS3-Proto-2-ConnectionIntegrity] If any two modules open a connection e, then either one module or the other or both modules accepted (i.e., initialized with) e.

3. [ICS3-Proto-3-StateConsistency] If any two modules open a connection, then the client in the first module is consistent with the state of the second module.

Do any of these properties fall into the scope of the relayer spec? If so, it would be useful to capture them.

[istoilkovska]

Addressed in #117