Modelling the interaction between relayers and chains

[adizere]

Summary

At higher-levels of specification (L1, L2), in the English and TLA+ specs, it is not clear what is the most accurate and helpful approach to capture the interface between relayers and chains.

Problem Definition

We are mostly interested in the context of the connection handshake problem.
Related issues: #33 #35 #36

Proposal

The API could look as follows:

// Alice invokes this to `write` the object `connection` to her local store
localStore.set(identifier, connection)

// Relayer invokes this to `read` from Alice's local store
chains[Alice].store.getConnection(identifier) // returns `connection`

// Relayer invokes this to append a datagram to a position in Bob's local store
chains[Bob].store.push("outstandingDatagrams", ConnOpenTry{ ... })
// Bob eventually consumes elements from his local store "outstandingDatagrams"
// for each datagram, Bob invokes the corresponding handler, e.g., ConnOpenTry

// Relayer can also append a datagram to a position in Alice's local store
chains[Alice].store.push("outstandingDatagrams", ConnOpenAck{ ... })

Discussion:

@istoilkovska :

In the TLA+ specification, the relayer reads the connection ends of both Alice and Bob, and writes the new datagrams to pendingDatagrams, a variable which is shared between the chains and the relayer. It's a record that stores a set of datagrams designated for Alice and another set of datagrams designated for Bob. When Alice and Bob are ready to process the datagrams, they read from their pendingDatagrams set and update their respective local states.

As far as I understand, you propose to move each pendingDatagrams set to the corresponding chain, and allow the relayer write to this set. The TLA+ specification can easily be fixed to capture this. However, in this case, the relayer has write access to the local state of a chain, which can be potentially dangerous in my opinion.

Moreover, in ICS 018, the relayer is defined as an off-chain process that can read the local state of the chains and submit transactions (it does not have write access to the local state of each chain). So, I propose to introduce a shared memory which is outside of the state of each chain, and allow the relayer to write to it and the chains to read from it.

@adizere :

The way I understand the interaction relayer <-> chain is that relayers do have the capability to “write” to a chain. The function store.push (in the suggestion above) represents an abstract version of submitDatagram (cf. ICS 018). Both of these functions essentially write to the state of a chain — with some caveats, but mainly: they submit a transaction (or a bundle of them), which goes through the consensus module, and ends up written in the blockchain.

---

For Admin Use

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

[adizere]

Expanding @istoilkovska comment from above, with code snippets extracted from #55.

There are two sides to this interface: (i) the side of the party (or chain), and (ii) the side of the relayer.

For the party:

// Suppose the party is Alice. She has access to her private buffer of pendingDatagrams
VARIABLE pendingDatagrams

// Alice can read an arbitrary element from her buffer
LET connOpenInitDgrs == {dgr \in datagrams : 
                             /\ dgr.type = "ConnOpenInit"
                             /\ dgr.connectionID = GetConnectionID(chainID)}

// And Alice can also "flush" (i.e., empty) her private buffer
pendingDatagrams = {}

Relayer side:

VARIABLE pendingDatagrams // this is Alice's buffer

// The relayer has write access to Alice's buffer
pendingDatagrams' = 
                         [ pendingDatagrams EXCEPT 
                             ![srcChainID] = pendingDatagrams[srcChainID] \union datagramsAndRelayerUpdate.src ]

// Also, the relayer has full read-access to Alice's state, e.g.:

IF Alice.ConnectionEnd.state = "UNINIT" /\ Bob.ConnectionEnd.state = "UNINIT" THEN ... 

[ancazamfir]

I read through the comments and it is not clear to me what the problem is with using pendingDatagrams the way it is done in #55.
One note, that the datagrams don't go in the chain store (something like chain[Alice].store.push... doesn't apply). They are transactions that need to be first processed and they may or may not change the chain state.
Also a correct chain will not read from pendingDatagrams out of order. The order of transactions is important. The typical example is a clientUpdate followed by a handshake transaction.

[adizere]

I read through the comments and it is not clear to me what the problem is with using pendingDatagrams the way it is done in #55.

The goal is to agree on what is our "standard" approach of writing the relayers/chain interface.

The problem is that we're using different names in different specs, so the specs are inconsistent. There is nothing wrong with #55, but ideally the relayer/chain interface in #55 should be consistent with the interface in CH English and TLA specs (#42 and #58) and should inform (help design) the code we'll be writing later on.

[adizere]

One note, that the datagrams don't go in the chain store (something like chain[Alice].store.push... doesn't apply). They are transactions that need to be first processed and they may or may not change the chain state.
Also a correct chain will not read from pendingDatagrams out of order. The order of transactions is important. The typical example is a clientUpdate followed by a handshake transaction.

OK, so some of the constraints for the relayer/chain interface are:

• the chain.store is not the right level of abstraction for storing inbound datagrams to a chain; it should be a separate buffer, like pendingDatagrams (Relayer TLA+ specification, connection and channel handshake datagrams #55) or inMsg (Connection Handshake (ICS3) L2 TLA+ spec #58).
• FIFO: the inbound buffer of datagrams to a chain respects FIFO ordering (the chain processes datagrams in the order they were added to the buffer);

One question that I don't know how to address yet is whether the inbound buffer should be bounded in size or not.

[adizere]

After many discussions about the high-level ICS3 spec in TLA+ (see here), we decided to model the interface to each chain as consisting of two buffers:

VARIABLES inBuf, outBuf

The former holds incoming messages, and the latter outgoing messages. In TLA+, these are each a Sequence with a bounded length CONSTANT MaxBufLen. The relayer (i.e., the environment) has access to reading some parts of the state of each chain. For instance, the relayer can read the current height of chain A so that it may update the client on chain B with this information:

chmB!UpdateClient(storeChainA.latestHeight)

Furthermore, the relayer can write almost arbitrary messages into the input buffer of any chain. The only constraint is that the relayer should not fill-up the buffer, concretely: Len(bufChainA) < MaxBufLen - 1.

[adizere]

This issue is superseded by work in #84 and #89.