Relayer TLA+ specification: Multiple relayers and modular ICS protocols

[istoilkovska]

Summary

The idea is to refactor and restructure the existing modules of the Relayer TLA+ specification such that a system where multiple relayers (at least two correct and one faulty) can be specified in a straightforward way.

Problem Definition

In the existing Relayer TLA+ specification, we assume that we have a single correct relayer, that relays datagrams between two chains, that constitute its environment. The relayer logic follows the naive relayer algorithm, proposed in ICS 018.

By refactoring and restructuring the Relayer TLA+ specification, we aim at producing a more modular specification, where the modules can be composed easily, and the properties of a system containing instances of several modules can be checked efficiently. Additionally, we aim at providing the possibility to check the properties of the modules in isolation as well, and thus avoid duplicate specifications of the same protocols.

Proposal

We propose the following modular structure of the Relayer TLA+ specification:

• module Relayer.tla:
  • contains the relayer logic and encodes a process running the relayer algorithm,
  • stores heights for participating chains, and produces datagrams,
  • defines Boolean constants, which flag which kinds of datagrams are being created and which properties are being checked (e.g., one can restrict the relayer to only create connection handshake datagrams, and check properties about eventual delivery of connection handshake datagrams);
• module Chain.tla:
  • contains the chain logic,
  • stores a chain height, a set of counterparty client heights, connection and channel ends (in the current specification, this is maintained by the environment),
  • defines chain actions, such as, increasing the chain height, or processing incoming datagrams;
• modules ProtocolHandlers.tla, where Protocol is one of Client, Connection, Channel:
  • defines operators that are used by a chain to handle Protocol datagrams;
• module RelayerDefinitions.tla:
  • defines operators shared by all the modules;
• main module RelayerSystem.tla:
  • specifies a system with one or more relayers, two or more communicating chains,
  • defines system variables and creates instances of Relayer.tla and Chain.tla, by ensuring the variables are correctly shared,
  • defines the system initial state predicate and next state action by reasonably composing the initial state predicates and next state actions of the instantiated modules.

The main module RelayerSystem.tla is not unique: depending on what kinds of systems we are interested in specifying and verifying, multiple such main modules may exist. For example, if we are interested in specifying a system with two correct relayers creating only client datagrams, and two communicating chains, the main module RelayerSystem.tla:

• creates two instances, relayer1, relayer2, of Relayer.tla, where the flags for client datagrams are set to TRUE, and the remaining ones are set to FALSE
• creates two instances of Chain.tla
• defines Init and Next as :

Init ==
  /\ relayer1!Init
  /\ relayer2!Init
  /\ chainA!Init
  /\ chainB!Init

Next ==
  \/ relayer1!Next
  \/ relayer2!Next
  \/ chainA!Next
  \/ chainB!Next

---

For Admin Use

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