Channel closing handshake

[istoilkovska]

Closes: #126

Description

A small PR that deals with creation and handling of channel closing datagrams in the relayer TLA+ specification.

Also, relayer-old is deleted.

Key points

1. the environment non-deterministically sets two Boolean flags, closeChannelA and closeChannelB.
2. a relayer reads the value of these flags, and sends ChanCloseInit to the appropirate chain once the flag is true.
3. a relayer reads that a chain set its channel end state to CLOSED and that its counterparty channel end is not closed yet, and sends ChanCloseConfirm to the its counterparty chain
4. a chain handles ChanCloseInit and ChanCloseConfirm by setting its channel end state to CLOSED

Properties

• ChannelCloseSafety ensures that once a channel is closed, it is never open again.
• ChanCloseInitDelivery ensures that once ChanCloseInit is sent, eventually both channel ends are closed.

---

For contributor use:

• Unit tests written
• Added test to CI if applicable
• Updated CHANGELOG_PENDING.md
• Linked to Github issue with discussion and accepted design OR link to spec that describes this work.
• Updated relevant documentation (docs/) and code comments
• Re-reviewed Files changed in the Github PR explorer

[adizere]

The relayer algorithm for handling channel closing does not have an English specification in ICS 018 (at least in the master branch). Any idea where is the English high-level spec for this algorithm? I wanted to cross-check it with your TLA+ code.

[istoilkovska]

You're right, it's missing in the ICS018, which is why channel closing wasn't added to the relayer spec until now. I've reverse engineered the datagram creation from the channel closure handlers.

[milosevic]

This is different from ICS04. I guess the reason is that they don't have UNINIT state?Is this the condition used in the Go implementation?

[istoilkovska]

Both the ICS004 and the Go implementation checks if the channel end can be found in the store, i.e. if it is non-null. In the TLA+ specification, each channel end is in UNINIT in the initial state of the system (c.f. Chain.tla and RelayerDefinitions.tla), hence a channel (also connection) end in state UNINIT denotes a null channel (connection) end.