Basic packet flow in TLA+ #248

istoilkovska · 2020-09-22T12:42:27Z

Closes: #124

Description

Added support for handling the basic packet flow in the Relayer TLA+ specification. Currently, the spec handles sending, receiving, and acknowledgements of packets.

The following basic packet flow is assumed:

ChainA sends a packet by writing a sent packet log entry to the packet log and writing a packet commitment
A relayer reads the packet log, picks the sent packet log entry, and creates PacketRecv datagram for ChainB
ChainB processes the PacketRecv datagram, and adds the received packet to its set of packets that should be acknowledged (asynchronous acknowledgements)
ChainB writes the acknowledgement by writing a log entry to the packet log
A relayer reads the packet log, picks the write ack log entry, and creates PacketAck datagram for ChainA
ChainA processes the PacketAck datagram by deleting the packet commitment of the original sent packet

The packets and packet logs are sequences, rather than sets. This is to ensure that there is order in sending, receiving, and acknowledgements of packets.

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

ancazamfir

Very nice spec! I have a few comments after the first pass. Struggling with TLC, one relayer and minimal config, it still runs after almost 1hr.

docs/spec/relayer/PacketHandlers.tla

ancazamfir · 2020-09-25T11:34:24Z

docs/spec/relayer/Chain.tla

-\* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels).
-UpdateChainStore(chainID, datagrams) == 
+\* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels & Packets).
+UpdateChainStoreAndPacketLog(chainID, datagrams, packetDatagrams, log) == 


I think we should have a sequence of datagrams for everything. We can get handshake datagrams interleaved with packet datagrams and the order matters. And then in the function we should process them in order.

Yes, I had the idea to transition to sequences of datagams completely. But doing so increases the state space that TLC enumerates. Will try to think about better handling, while still processing datagrams in order.

Agree with Anca that orders matter. We can have either sequence or handle only single datagram at the time.

docs/spec/relayer/Relayer.tla

docs/spec/relayer/Chain.tla

Co-authored-by: Anca Zamfir <[email protected]>

codecov-commenter · 2020-09-28T12:22:05Z

Codecov Report

Merging #248 into master will increase coverage by 20.4%.
The diff coverage is 55.2%.

@@            Coverage Diff            @@
##           master    #248      +/-   ##
=========================================
+ Coverage    13.6%   34.1%   +20.4%     
=========================================
  Files          69     106      +37     
  Lines        3752    7112    +3360     
  Branches     1374    2579    +1205     
=========================================
+ Hits          513    2430    +1917     
- Misses       2618    4318    +1700     
+ Partials      621     364     -257

Impacted Files	Coverage Δ
modules/src/events.rs	`0.0% <ø> (ø)`
modules/src/ics02_client/events.rs	`0.0% <ø> (ø)`
modules/src/ics02_client/raw.rs	`0.0% <0.0%> (ø)`
modules/src/ics03_connection/error.rs	`16.6% <0.0%> (-16.7%)`	⬇️
...ules/src/ics03_connection/handler/conn_open_ack.rs	`87.5% <ø> (ø)`
.../src/ics03_connection/handler/conn_open_confirm.rs	`87.5% <ø> (ø)`
modules/src/ics04_channel/error.rs	`75.0% <ø> (+50.0%)`	⬆️
modules/src/ics04_channel/packet.rs	`0.0% <0.0%> (ø)`
modules/src/ics07_tendermint/client_def.rs	`0.0% <0.0%> (ø)`
modules/src/ics07_tendermint/consensus_state.rs	`18.5% <0.0%> (-14.9%)`	⬇️
... and 165 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 4877ee9...fc2dd62. Read the comment docs.

milosevic · 2020-09-29T11:18:31Z

docs/spec/relayer/Chain.tla

@@ -10,9 +10,12 @@ CONSTANTS MaxHeight, \* maximal chain height

 VARIABLES chainStore, \* chain store, containing client heights, a connection end, a channel end 
          incomingDatagrams, \* set of incoming datagrams
-          history \* history variable
+          incomingPacketDatagrams, \* sequence of incoming packet datagrams
+          history, \* history variable


What is the purpose of history variable?

We use the history variable in the invariant we check with Apalache. The history variable is a record that stores flags about the state of the connection and channel ends. The flags are set once, when the state changes. The invariant checks that if a flag is set, the state of the connection or channel end does not go back to a previous state.

Example: a connection is open, and the flag history.connOpen is set to TRUE. The following invariant has to hold:

history.connOpen => /\ chainA.connectionEnd.state /= "UNINIT" /\ chainA.connectionEnd.state /= "INIT" /\ chainA.connectionEnd.state /= "TRYOPEN"

milosevic · 2020-09-29T11:47:07Z

docs/spec/relayer/Chain.tla

+\* (Handler operators defined in PacketHandlers.tla)    
+PacketUpdate(chainID, store, packetDatagrams, log) ==
+    \* if the sequence of packet datagrams is not empty
+    IF packetDatagrams /= AsSeqPacketDatagrams(<<>>)


Why the structure is not the same as with others, i.e., it contains HandlePacketRecv and HandlePacketAck that internally check for the datagram type?

It is because the PacketUpdate operator computes the update to the chain store with a single packet datagram, taken from the sequence of packet datagrams, while the other *Update operators update the chain store with a set of datagrams, which is obtained by taking a subset of the incoming datagrams, containing datagrams of particular type.

milosevic · 2020-09-29T12:50:46Z

docs/spec/relayer/Chain.tla

+                            Tail(chain.packetsToAcknowledge)] 
+
+\* log acknowledgements to packet Log
+LogAcknowledgement(chain, log, packet) ==


I am not sure if we need to model event log as it is not necessarily, i.e., current ICS18 is not using it. It might be useful as part of MBT, but in the initial version I would prefer having the minimal set of functionalities needed.

We can have it merged like this for now, I will experiment to see if by removing it we can obtain some model checking results.

milosevic · 2020-09-29T12:56:26Z

docs/spec/relayer/Chain.tla

+       \* add a packet committment in the chain store, and increase nextSendSeq
+       \/ /\ channelEnd.order = "ORDERED"
+          /\ packet.sequence = channelEnd.nextSendSeq
+          /\ packet.sequence <= MaxPacketSeq


This is a model constraint, not the handler one; ideally they should not be mixed and model constraint can be a precondition at the higher level.

I've refactored this action a bit.

docs/spec/relayer/Chain.tla

milosevic · 2020-09-29T14:34:11Z

docs/spec/relayer/Chain.tla

@@ -156,6 +299,8 @@ Init ==
 Next ==
    \/ AdvanceChain 
    \/ HandleIncomingDatagrams
+    \/ SendPacket
+    \/ AcknowledgePacket


Should we add timeout handling here? Then it seems complete.

Also, what about channel closing? Is it also triggered "externally"?

channel closing is triggered by the application so yes the trigger is "external"

We currently have a flag for each chain that triggers channel closing, which is non-deterministically set by the environment. When we add timeouts we would have channel closing that is triggered by a timeout.

docs/spec/relayer/PacketHandlers.tla

milosevic · 2020-09-29T15:19:54Z

docs/spec/relayer/PacketHandlers.tla

+\* Handle "PacketRecv" datagrams
+HandlePacketRecv(chainID, chain, packetDatagram, log) ==
+    \* get chainID's connection end
+    LET connectionEnd == chain.connectionEnd IN


I am wondering if we are missing important aspect here as we don't use chain and connection id from packetDatagram to fetch local connection and channel end.

We can check in lines 32-33

/\ packetDatagram.srcChannelID = channelEnd.channelID /\ packetDatagram.dstChannelID = channelEnd.counterpartyChannelID

where channelEnd is defined like in line 17. This should filter out packet datagrams that do not have the correct channelIDs.

milosevic

LGTM. There are few comments that could be addressed and few more general concerns that we can address later.

ancazamfir

Looks good! Thanks Ilina!

* send packet action added, relayer packet creation * packet receive, ack * packet ack * readme updated * Apply suggestions from code review Co-authored-by: Anca Zamfir <[email protected]> * addressed comments * applied review comments * moved files around Co-authored-by: Anca Zamfir <[email protected]>

istoilkovska added 4 commits September 15, 2020 16:53

send packet action added, relayer packet creation

18203aa

packet receive, ack

2440e29

packet ack

d2d07f0

readme updated

6f66413

istoilkovska added I: spec Internal: related to IBC specifications I: logic Internal: related to the relaying logic labels Sep 22, 2020

istoilkovska added this to the v0.0.4 milestone Sep 22, 2020

istoilkovska requested review from milosevic and ancazamfir September 22, 2020 12:42

istoilkovska requested a review from romac as a code owner September 22, 2020 12:42

istoilkovska self-assigned this Sep 22, 2020

istoilkovska removed this from the v0.0.4 milestone Sep 22, 2020

istoilkovska removed I: logic Internal: related to the relaying logic I: spec Internal: related to IBC specifications labels Sep 22, 2020

ancazamfir reviewed Sep 25, 2020

View reviewed changes

istoilkovska and others added 2 commits September 25, 2020 17:19

Apply suggestions from code review

0b5b78e

Co-authored-by: Anca Zamfir <[email protected]>

addressed comments

fc2dd62

milosevic reviewed Sep 29, 2020

View reviewed changes

docs/spec/relayer/Chain.tla Show resolved Hide resolved

milosevic reviewed Sep 29, 2020

View reviewed changes

docs/spec/relayer/PacketHandlers.tla Outdated Show resolved Hide resolved

milosevic reviewed Sep 29, 2020

View reviewed changes

milosevic approved these changes Sep 30, 2020

View reviewed changes

istoilkovska added 2 commits September 30, 2020 13:53

applied review comments

3ee4b0e

moved files around

7aead8a

ancazamfir approved these changes Sep 30, 2020

View reviewed changes

ancazamfir merged commit 10b8a69 into master Sep 30, 2020

ancazamfir deleted the ilina/packets_tla branch September 30, 2020 12:31

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Basic packet flow in TLA+ #248

Basic packet flow in TLA+ #248

istoilkovska commented Sep 22, 2020

ancazamfir left a comment

ancazamfir Sep 25, 2020

istoilkovska Sep 25, 2020

milosevic Sep 29, 2020

codecov-commenter commented Sep 28, 2020

milosevic Sep 29, 2020

istoilkovska Sep 30, 2020

milosevic Sep 29, 2020

istoilkovska Sep 30, 2020

milosevic Sep 29, 2020

istoilkovska Sep 30, 2020

milosevic Sep 29, 2020

istoilkovska Sep 30, 2020

milosevic Sep 29, 2020

milosevic Sep 29, 2020

ancazamfir Sep 30, 2020

istoilkovska Sep 30, 2020

milosevic Sep 29, 2020

istoilkovska Sep 30, 2020

milosevic left a comment

ancazamfir left a comment

Basic packet flow in TLA+ #248

Basic packet flow in TLA+ #248

Conversation

istoilkovska commented Sep 22, 2020

Description

ancazamfir left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

codecov-commenter commented Sep 28, 2020

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

milosevic left a comment

Choose a reason for hiding this comment

ancazamfir left a comment

Choose a reason for hiding this comment