Basic packet flow in TLA+ (informalsystems#248)

* 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]>
hu55a1n1 · Sep 30, 2020 · b2a4182 · b2a4182
1 parent 7acd7cf
commit b2a4182
Show file tree

Hide file tree

Showing 11 changed files with 510 additions and 78 deletions.
diff --git a/docs/spec/relayer/Chain.tla → docs/spec/relayer/tla/Chain.tla b/docs/spec/relayer/Chain.tla → docs/spec/relayer/tla/Chain.tla
@@ -1,7 +1,7 @@
 ---------------------------- MODULE Chain ----------------------------
 
 EXTENDS Integers, FiniteSets, RelayerDefinitions, 
-        ClientHandlers, ConnectionHandlers, ChannelHandlers
+        ClientHandlers, ConnectionHandlers, ChannelHandlers, PacketHandlers
 
 CONSTANTS MaxHeight, \* maximal chain height
           ChainID, \* chain identifier
@@ -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
+          packetLog, \* packet log
+          appPacketSeq \* packet sequence number from the application on the chain
 
-vars == <<chainStore, incomingDatagrams, history>>
+vars == <<chainStore, incomingDatagrams, incomingPacketDatagrams, history, packetLog, appPacketSeq>>
 Heights == 1..MaxHeight \* set of possible heights of the chains in the system          
 
 (***************************************************************************
@@ -78,12 +81,34 @@ ChannelUpdate(chainID, store, datagrams) ==
 
     chanCloseConfirmStore
 
+(***************************************************************************
+ Packet update operators
+ ***************************************************************************)
+\* Update the chain store of the chain with chainID and the packet log, 
+\* using the packet datagrams generated by the relayer
+\* (Handler operators defined in PacketHandlers.tla)    
+PacketUpdate(chainID, store, packetDatagrams, log) ==
+    \* if the sequence of packet datagrams is not empty
+    IF packetDatagrams /= AsSeqPacketDatagrams(<<>>)
+    THEN \* process the packet datagram at the head of the sequence
+         LET packetDatagram == AsPacketDatagram(Head(packetDatagrams)) IN
+         LET packet == packetDatagram.packet IN
+         \* get the new updated store and packet log entry
+         LET newStoreAndLog == 
+                IF packetDatagram.type = "PacketRecv"
+                THEN HandlePacketRecv(chainID, store, packetDatagram, log)
+                ELSE IF packetDatagram.type = "PacketAck"
+                     THEN HandlePacketAck(chainID, store, packetDatagram, log)
+                     ELSE [chainStore|-> store, packetLogEntry |-> log] IN
+         newStoreAndLog
+    ELSE [chainStore |-> store, packetLog |->log]
+
 (***************************************************************************
  Chain update operators
  ***************************************************************************)
 \* Update chainID with the received datagrams
-\* 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) == 
 
     \* ICS 002: Client updates
     LET clientUpdatedStore == LightClientUpdate(chainID, chainStore, datagrams) IN
@@ -94,15 +119,20 @@ UpdateChainStore(chainID, datagrams) ==
     \* ICS 003: Channel updates
     LET channelUpdatedStore == ChannelUpdate(chainID, connectionUpdatedStore, datagrams) IN
 
+    \* ICS 004: Packet transmission
+    LET packetUpdatedStoreAndLogEntry == PacketUpdate(chainID, channelUpdatedStore, packetDatagrams, log) IN
+    LET packetUpdatedStore == packetUpdatedStoreAndLogEntry.chainStore IN
 
     \* update height
     LET updatedChainStore == 
-        IF /\ chainStore /= channelUpdatedStore
+        IF /\ chainStore /= packetUpdatedStore
            /\ chainStore.height + 1 \in Heights 
-        THEN [channelUpdatedStore EXCEPT !.height = chainStore.height + 1]
-        ELSE channelUpdatedStore
+        THEN [packetUpdatedStore EXCEPT !.height = chainStore.height + 1]
+        ELSE packetUpdatedStore
     IN
-    updatedChainStore
+
+    [chainStore |-> updatedChainStore, 
+     packetLog |-> packetUpdatedStoreAndLogEntry.packetLog]
 
 (***************************************************************************
  Chain actions
@@ -111,29 +141,68 @@ UpdateChainStore(chainID, datagrams) ==
 AdvanceChain ==
     /\ chainStore.height + 1 \in Heights
     /\ chainStore' = [chainStore EXCEPT !.height = chainStore.height + 1]
-    /\ UNCHANGED <<incomingDatagrams, history>>
+    /\ UNCHANGED <<incomingDatagrams, incomingPacketDatagrams, history>>
+    /\ UNCHANGED <<packetLog, appPacketSeq>>
+
+\* Send a packet
+SendPacket ==   
+    \* enabled if appPacketSeq is not bigger than MaxPacketSeq 
+    /\ appPacketSeq <= MaxPacketSeq
+    \* Create a packet: Abstract away from packet data, ports, and timestamp. 
+    \* Assume timeoutHeight is MaxHeight + 1
+    /\ LET packet == AsPacket([
+        sequence |-> appPacketSeq,
+        timeoutHeight |-> MaxHeight + 1,
+        srcChannelID |-> GetChannelID(ChainID),
+        dstChannelID |-> GetChannelID(GetCounterpartyChainID(ChainID))]) IN
+        \* update chain store with packet committment
+        /\ chainStore' = WritePacketCommitment(chainStore, packet)
+        \* log sent packet
+        /\ packetLog' = Append(packetLog, AsPacketLogEntry(
+                                               [type |-> "PacketSend", 
+                                                srcChainID |-> ChainID,  
+                                                sequence |-> packet.sequence ,
+                                                timeoutHeight |-> packet.timeoutHeight]))
+        \* increase application packet sequence
+        /\ appPacketSeq' = appPacketSeq + 1
+        /\ UNCHANGED <<incomingDatagrams, incomingPacketDatagrams, history>>
+
+\* write a packet acknowledgement on the packet log and chain store
+AcknowledgePacket ==
+    /\ chainStore.packetsToAcknowledge /= AsSeqPacket(<<>>)
+    /\ chainStore' = WriteAcknowledgement(chainStore, Head(chainStore.packetsToAcknowledge))
+    /\ packetLog' = LogAcknowledgement(ChainID, chainStore, packetLog, Head(chainStore.packetsToAcknowledge))
+    /\ UNCHANGED <<incomingDatagrams, incomingPacketDatagrams, history>>
+    /\ UNCHANGED appPacketSeq
 
 \* Handle the datagrams and update the chain state        
 HandleIncomingDatagrams ==
-    /\ incomingDatagrams /= AsSetDatagrams({}) 
-    /\ chainStore' = UpdateChainStore(ChainID, AsSetDatagrams(incomingDatagrams))
-    /\ incomingDatagrams' = AsSetDatagrams({})
-    /\ history' = CASE chainStore'.connectionEnd.state = "INIT" 
-                                -> [history EXCEPT !.connInit = TRUE]
-                        [] chainStore'.connectionEnd.state = "TRYOPEN"
-                                -> [history EXCEPT !.connTryOpen = TRUE] 
-                        [] chainStore'.connectionEnd.state = "OPEN"
-                                -> [history EXCEPT !.connOpen = TRUE] 
-                        [] chainStore'.connectionEnd.channelEnd.state = "INIT"
-                                -> [history EXCEPT !.chanInit = TRUE]
-                        [] chainStore'.connectionEnd.channelEnd.state = "TRYOPEN"
-                                -> [history EXCEPT !.chanTryOpen = TRUE]
-                        [] chainStore'.connectionEnd.channelEnd.state = "OPEN"
-                                -> [history EXCEPT !.chanOpen = TRUE]
-                        [] chainStore'.connectionEnd.channelEnd.state = "CLOSED"
-                                -> [history EXCEPT !.chanClosed = TRUE] 
-                        [] OTHER 
-                                -> history
+    /\ \/ incomingDatagrams /= AsSetDatagrams({})
+       \/ incomingPacketDatagrams /= AsSeqPacketDatagrams(<<>>) 
+    /\ LET updatedChainStoreAndPacketLog == UpdateChainStoreAndPacketLog(ChainID, incomingDatagrams, incomingPacketDatagrams, packetLog) IN
+        /\ chainStore' = updatedChainStoreAndPacketLog.chainStore
+        /\ packetLog' = updatedChainStoreAndPacketLog.packetLog 
+        /\ incomingDatagrams' = AsSetDatagrams({})
+        /\ incomingPacketDatagrams' = IF incomingPacketDatagrams /= AsSeqPacketDatagrams(<<>>)
+                                      THEN Tail(incomingPacketDatagrams)
+                                      ELSE incomingPacketDatagrams
+        /\ history' = CASE chainStore'.connectionEnd.state = "INIT" 
+                                    -> [history EXCEPT !.connInit = TRUE]
+                            [] chainStore'.connectionEnd.state = "TRYOPEN"
+                                    -> [history EXCEPT !.connTryOpen = TRUE] 
+                            [] chainStore'.connectionEnd.state = "OPEN"
+                                    -> [history EXCEPT !.connOpen = TRUE] 
+                            [] chainStore'.connectionEnd.channelEnd.state = "INIT"
+                                    -> [history EXCEPT !.chanInit = TRUE]
+                            [] chainStore'.connectionEnd.channelEnd.state = "TRYOPEN"
+                                    -> [history EXCEPT !.chanTryOpen = TRUE]
+                            [] chainStore'.connectionEnd.channelEnd.state = "OPEN"
+                                    -> [history EXCEPT !.chanOpen = TRUE]
+                            [] chainStore'.connectionEnd.channelEnd.state = "CLOSED"
+                                    -> [history EXCEPT !.chanClosed = TRUE] 
+                            [] OTHER 
+                                    -> history
+        /\ UNCHANGED appPacketSeq
 
 (***************************************************************************
  Specification
@@ -146,16 +215,21 @@ HandleIncomingDatagrams ==
 Init == 
     /\ chainStore = InitChainStore(ChannelOrdering)
     /\ incomingDatagrams = AsSetDatagrams({})
+    /\ incomingPacketDatagrams = AsSeqDatagrams(<<>>)
     /\ history = InitHistory
+    /\ appPacketSeq = AsInt(1)
 
 \* Next state action
 \* The chain either
 \*  - advances its height
 \*  - receives datagrams and updates its state
-\*  - sends a packet (TODO)
+\*  - sends a packet if the appPacketSeq is not bigger than MaxPacketSeq
+\*  - acknowledges a packet
 Next ==
     \/ AdvanceChain 
     \/ HandleIncomingDatagrams
+    \/ SendPacket
+    \/ AcknowledgePacket
     \/ UNCHANGED vars
 
 Fairness ==
@@ -171,6 +245,8 @@ TypeOK ==
     /\ chainStore \in ChainStores(MaxHeight, ChannelOrdering, MaxPacketSeq)
     /\ incomingDatagrams \in SUBSET Datagrams(MaxHeight, MaxPacketSeq)
     /\ history \in Histories
+    /\ appPacketSeq \in 1..MaxPacketSeq
+    /\ packetLog \in SUBSET Packets(MaxHeight, MaxPacketSeq)
 
 (***************************************************************************
  Properties
@@ -182,5 +258,5 @@ HeightDoesntDecrease ==
 
 =============================================================================
 \* Modification History
-\* Last modified Thu Sep 10 15:43:42 CEST 2020 by ilinastoilkovska
+\* Last modified Wed Sep 30 13:47:16 CEST 2020 by ilinastoilkovska
 \* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska
diff --git a/docs/spec/relayer/ChannelHandlers.tla → docs/spec/relayer/tla/ChannelHandlers.tla b/docs/spec/relayer/ChannelHandlers.tla → docs/spec/relayer/tla/ChannelHandlers.tla
diff --git a/docs/spec/relayer/ClientHandlers.tla → docs/spec/relayer/tla/ClientHandlers.tla b/docs/spec/relayer/ClientHandlers.tla → docs/spec/relayer/tla/ClientHandlers.tla
diff --git a/docs/spec/relayer/ConnectionHandlers.tla → docs/spec/relayer/tla/ConnectionHandlers.tla b/docs/spec/relayer/ConnectionHandlers.tla → docs/spec/relayer/tla/ConnectionHandlers.tla
diff --git a/docs/spec/relayer/ICS18Environment.cfg → docs/spec/relayer/tla/ICS18Environment.cfg b/docs/spec/relayer/ICS18Environment.cfg → docs/spec/relayer/tla/ICS18Environment.cfg
diff --git a/docs/spec/relayer/ICS18Environment.tla → docs/spec/relayer/tla/ICS18Environment.tla b/docs/spec/relayer/ICS18Environment.tla → docs/spec/relayer/tla/ICS18Environment.tla
@@ -1,6 +1,6 @@
 -------------------------- MODULE ICS18Environment --------------------------
 
-EXTENDS Integers, FiniteSets, RelayerDefinitions
+EXTENDS Integers, FiniteSets, Sequences, RelayerDefinitions
 
 CONSTANTS MaxHeight, \* maximal height of all the chains in the system
           MaxPacketSeq, \* maximal packet sequence number (will be used later)
@@ -16,24 +16,34 @@ VARIABLES chainAstore, \* store of ChainA
           chainBstore, \* store of ChainB
           incomingDatagramsChainA, \* set of datagrams incoming to ChainA
           incomingDatagramsChainB, \* set of datagrams incoming to ChainB
+          incomingPacketDatagramsChainA, \* sequence of packet datagrams incoming to ChainA
+          incomingPacketDatagramsChainB, \* sequence of packet datagrams incoming to ChainB
           relayer1Heights, \* the client heights of Relayer1
           relayer2Heights, \* the client heights of Relayer2
           outgoingDatagrams, \* sets of datagrams outgoing of the relayers
+          outgoingPacketDatagrams, \* sequences of packet datagrams outgoing of the relayers
           closeChannelA, \* flag that triggers closing of the channel end at ChainA
           closeChannelB, \* flag that triggers closing of the channel end at ChainB
           historyChainA, \* history variables for ChainA
-          historyChainB \* history variables for ChainB
+          historyChainB, \* history variables for ChainB
+          packetLog, \* a set of packets sent by both chains
+          appPacketSeqChainA, \* packet sequence number from the application on ChainA
+          appPacketSeqChainB \* packet sequence number from the application on ChainA
 
 vars == <<chainAstore, chainBstore, 
           incomingDatagramsChainA, incomingDatagramsChainB,
+          incomingPacketDatagramsChainA, incomingPacketDatagramsChainB,
           relayer1Heights, relayer2Heights,
           outgoingDatagrams,
+          outgoingPacketDatagrams,
           closeChannelA, closeChannelB, 
-          historyChainA, historyChainB>>
+          historyChainA, historyChainB,
+          packetLog,
+          appPacketSeqChainA, appPacketSeqChainB>>
 
-chainAvars == <<chainAstore, incomingDatagramsChainA, historyChainA>>
-chainBvars == <<chainBstore, incomingDatagramsChainB, historyChainB>>
-relayerVars == <<relayer1Heights, relayer2Heights, outgoingDatagrams>>
+chainAvars == <<chainAstore, incomingDatagramsChainA, incomingPacketDatagramsChainA, historyChainA, appPacketSeqChainA>>
+chainBvars == <<chainBstore, incomingDatagramsChainB, incomingPacketDatagramsChainB, historyChainB, appPacketSeqChainB>>
+relayerVars == <<relayer1Heights, relayer2Heights, outgoingDatagrams, outgoingPacketDatagrams>>
 Heights == 1..MaxHeight \* set of possible heights of the chains in the system                      
 
 
@@ -62,14 +72,18 @@ ChainA == INSTANCE Chain
           WITH ChainID <- "chainA",
                chainStore <- chainAstore,
                incomingDatagrams <- incomingDatagramsChainA,
-               history <- historyChainA
+               incomingPacketDatagrams <- incomingPacketDatagramsChainA,
+               history <- historyChainA,
+               appPacketSeq <- appPacketSeqChainA
 
 \* ChainB -- Instance of Chain.tla 
 ChainB == INSTANCE Chain
           WITH ChainID <- "chainB",
                chainStore <- chainBstore,
                incomingDatagrams <- incomingDatagramsChainB,
-               history <- historyChainB
+               incomingPacketDatagrams <- incomingPacketDatagramsChainB,
+               history <- historyChainB,
+               appPacketSeq <- appPacketSeqChainB
 
 (***************************************************************************
  Component actions
@@ -109,9 +123,17 @@ SubmitDatagrams ==
     /\ incomingDatagramsChainA' = AsSetDatagrams(incomingDatagramsChainA \union outgoingDatagrams["chainA"])
     /\ incomingDatagramsChainB' = AsSetDatagrams(incomingDatagramsChainB \union outgoingDatagrams["chainB"])
     /\ outgoingDatagrams' = [chainID \in ChainIDs |-> AsSetDatagrams({})]
+    /\ incomingPacketDatagramsChainA' = AsSeqPacketDatagrams(incomingPacketDatagramsChainA 
+                                                             \o
+                                                             outgoingPacketDatagrams["chainA"]) 
+    /\ incomingPacketDatagramsChainB' = AsSeqPacketDatagrams(incomingPacketDatagramsChainB
+                                                             \o
+                                                             outgoingPacketDatagrams["chainB"])
+    /\ outgoingPacketDatagrams' = [chainID \in ChainIDs |-> AsSeqPacketDatagrams(<<>>)]                                                          
     /\ UNCHANGED <<chainAstore, chainBstore, relayer1Heights, relayer2Heights>>
     /\ UNCHANGED <<closeChannelA, closeChannelB>>
     /\ UNCHANGED <<historyChainA, historyChainB>>
+    /\ UNCHANGED <<packetLog, appPacketSeqChainA, appPacketSeqChainB>>
 
 \* Non-deterministically set channel closing flags
 CloseChannels ==
@@ -121,12 +143,16 @@ CloseChannels ==
        /\ UNCHANGED <<incomingDatagramsChainA, incomingDatagramsChainB, outgoingDatagrams>>
        /\ UNCHANGED closeChannelB
        /\ UNCHANGED <<historyChainA, historyChainB>>
+       /\ UNCHANGED <<packetLog, appPacketSeqChainA, appPacketSeqChainB>>
+       /\ UNCHANGED <<incomingPacketDatagramsChainA, incomingPacketDatagramsChainB, outgoingPacketDatagrams>>
     \/ /\ closeChannelB = FALSE
        /\ closeChannelB' \in BOOLEAN
        /\ UNCHANGED <<chainAstore, chainBstore, relayer1Heights, relayer2Heights>>
        /\ UNCHANGED <<incomingDatagramsChainA, incomingDatagramsChainB, outgoingDatagrams>>
        /\ UNCHANGED closeChannelA
        /\ UNCHANGED <<historyChainA, historyChainB>>
+       /\ UNCHANGED <<packetLog, appPacketSeqChainA, appPacketSeqChainB>>
+       /\ UNCHANGED <<incomingPacketDatagramsChainA, incomingPacketDatagramsChainB, outgoingPacketDatagrams>>
 
 \* Faulty relayer action
 FaultyRelayer ==
@@ -150,6 +176,7 @@ Init ==
     /\ Relayer2!Init
     /\ closeChannelA = FALSE
     /\ closeChannelB = FALSE
+    /\ packetLog = AsPacketLog(<<>>)
 
 \* Next state action
 Next ==
@@ -539,5 +566,5 @@ ICS18Delivery ==
 
 =============================================================================
 \* Modification History
-\* Last modified Thu Sep 10 15:41:47 CEST 2020 by ilinastoilkovska
+\* Last modified Fri Sep 18 18:56:16 CEST 2020 by ilinastoilkovska
 \* Created Fri Jun 05 16:48:22 CET 2020 by ilinastoilkovska
diff --git a/...pec/relayer/ICS18Environment_apalache.tla → ...relayer/tla/ICS18Environment_apalache.tla b/...pec/relayer/ICS18Environment_apalache.tla → ...relayer/tla/ICS18Environment_apalache.tla