Relayer TLA+: Support for running Apalache (#224)

* expriments with apalache * apalache file * Type annotations for Apalache * apalache type annotations * final apalache type annotations * removed PacketHandlers.tla and dependencies
informalsystems · Sep 15, 2020 · 4877ee9 · 4877ee9
1 parent 6f84d97
commit 4877ee9
Show file tree

Hide file tree

Showing 10 changed files with 929 additions and 360 deletions.
diff --git a/docs/spec/relayer/Chain.tla b/docs/spec/relayer/Chain.tla
@@ -1,15 +1,19 @@
 ---------------------------- MODULE Chain ----------------------------
 
-EXTENDS Naturals, FiniteSets, RelayerDefinitions, 
+EXTENDS Integers, FiniteSets, RelayerDefinitions, 
         ClientHandlers, ConnectionHandlers, ChannelHandlers
 
-CONSTANTS ChainID, \* chain identifier
-          Heights \* set of possible heights of the chains in the system 
+CONSTANTS MaxHeight, \* maximal chain height
+          ChainID, \* chain identifier
+          ChannelOrdering, \* indicate whether the channels are ordered or unordered  
+          MaxPacketSeq \* maximal packet sequence number
 
-VARIABLES chainStore,
-          incomingDatagrams
+VARIABLES chainStore, \* chain store, containing client heights, a connection end, a channel end 
+          incomingDatagrams, \* set of incoming datagrams
+          history \* history variable
 
-vars == <<chainStore, incomingDatagrams>>          
+vars == <<chainStore, incomingDatagrams, history>>
+Heights == 1..MaxHeight \* set of possible heights of the chains in the system          
 
 (***************************************************************************
  Client update operators
@@ -21,10 +25,10 @@ LightClientUpdate(chainID, store, datagrams) ==
     \* create clients
     LET clientCreatedStore == HandleCreateClient(chainID, store, datagrams) IN
     \* update clients
-    LET clientUpdatedStore == HandleUpdateClient(chainID, clientCreatedStore, datagrams) IN
+    LET clientUpdatedStore == HandleClientUpdate(chainID, clientCreatedStore, datagrams) IN
 
     clientUpdatedStore
-    
+
 (***************************************************************************
  Connection update operators
  ***************************************************************************)
@@ -34,36 +38,44 @@ LightClientUpdate(chainID, store, datagrams) ==
 ConnectionUpdate(chainID, store, datagrams) ==
     \* update the chain store with "ConnOpenInit" datagrams
     LET connOpenInitStore == HandleConnOpenInit(chainID, store, datagrams) IN
+
     \* update the chain store with "ConnOpenTry" datagrams
-    LET connOpenTryStore  == HandleConnOpenTry(chainID, connOpenInitStore, datagrams) IN
+    LET connOpenTryStore == HandleConnOpenTry(chainID, connOpenInitStore, datagrams) IN
+
     \* update the chain store with "ConnOpenAck" datagrams
     LET connOpenAckStore == HandleConnOpenAck(chainID, connOpenTryStore, datagrams) IN
+
     \* update the chain store with "ConnOpenConfirm" datagrams
     LET connOpenConfirmStore == HandleConnOpenConfirm(chainID, connOpenAckStore, datagrams) IN
 
+    \* output the updated chain store 
     connOpenConfirmStore
-
+    
 (***************************************************************************
  Channel update operators
  ***************************************************************************)
-\* Update the channels on chain with chainID, 
+\* Update the channel on chain with chainID, 
 \* using the channel datagrams generated by the relayer
 \* (Handler operators defined in ChannelHandlers.tla)
 ChannelUpdate(chainID, store, datagrams) ==
     \* update the chain store with "ChanOpenInit" datagrams
     LET chanOpenInitStore == HandleChanOpenInit(chainID, store, datagrams) IN
+
     \* update the chain store with "ChanOpenTry" datagrams
     LET chanOpenTryStore == HandleChanOpenTry(chainID, chanOpenInitStore, datagrams) IN
+
     \* update the chain store with "ChanOpenAck" datagrams
     LET chanOpenAckStore == HandleChanOpenAck(chainID, chanOpenTryStore, datagrams) IN
+
     \* update the chain store with "ChanOpenConfirm" datagrams
     LET chanOpenConfirmStore == HandleChanOpenConfirm(chainID, chanOpenAckStore, datagrams) IN
-    
+
     \* update the chain store with "ChanCloseInit" datagrams
     LET chanCloseInitStore == HandleChanCloseInit(chainID, chanOpenConfirmStore, datagrams) IN
+
     \* update the chain store with "ChanCloseConfirm" datagrams
     LET chanCloseConfirmStore == HandleChanCloseConfirm(chainID, chanCloseInitStore, datagrams) IN
-    
+
     chanCloseConfirmStore
 
 (***************************************************************************
@@ -72,21 +84,24 @@ ChannelUpdate(chainID, store, datagrams) ==
 \* Update chainID with the received datagrams
 \* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels).
 UpdateChainStore(chainID, datagrams) == 
+
     \* ICS 002: Client updates
-    LET lightClientsUpdatedStore == LightClientUpdate(chainID, chainStore, datagrams) IN 
+    LET clientUpdatedStore == LightClientUpdate(chainID, chainStore, datagrams) IN
+
     \* ICS 003: Connection updates
-    LET connectionsUpdatedStore == ConnectionUpdate(chainID, lightClientsUpdatedStore, datagrams) IN
-    \* ICS 004: Channel updates
-    LET channelsUpdatedStore == ChannelUpdate(chainID, connectionsUpdatedStore, datagrams) IN
-
+    LET connectionUpdatedStore == ConnectionUpdate(chainID, clientUpdatedStore, datagrams) IN
+
+    \* ICS 003: Channel updates
+    LET channelUpdatedStore == ChannelUpdate(chainID, connectionUpdatedStore, datagrams) IN
+
+
     \* update height
     LET updatedChainStore == 
-        IF /\ chainStore /= channelsUpdatedStore
+        IF /\ chainStore /= channelUpdatedStore
            /\ chainStore.height + 1 \in Heights 
-        THEN [channelsUpdatedStore EXCEPT !.height = chainStore.height + 1]
-        ELSE channelsUpdatedStore
+        THEN [channelUpdatedStore EXCEPT !.height = chainStore.height + 1]
+        ELSE channelUpdatedStore
     IN
-
     updatedChainStore
 
 (***************************************************************************
@@ -96,13 +111,29 @@ UpdateChainStore(chainID, datagrams) ==
 AdvanceChain ==
     /\ chainStore.height + 1 \in Heights
     /\ chainStore' = [chainStore EXCEPT !.height = chainStore.height + 1]
-    /\ UNCHANGED incomingDatagrams
+    /\ UNCHANGED <<incomingDatagrams, history>>
 
 \* Handle the datagrams and update the chain state        
 HandleIncomingDatagrams ==
-    /\ incomingDatagrams /= {} 
-    /\ chainStore' = UpdateChainStore(ChainID, incomingDatagrams)
-    /\ incomingDatagrams' = {}
+    /\ 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
 
 (***************************************************************************
  Specification
@@ -111,31 +142,35 @@ HandleIncomingDatagrams ==
 \* Initially
 \*  - each chain is initialized to InitChain (defined in RelayerDefinitions.tla)
 \*  - pendingDatagrams for each chain is empty
+\*  - the packetSeq is set to 1
 Init == 
-    /\ chainStore = InitChain 
-    /\ incomingDatagrams = {}
+    /\ chainStore = InitChainStore(ChannelOrdering)
+    /\ incomingDatagrams = AsSetDatagrams({})
+    /\ history = InitHistory
 
 \* Next state action
 \* The chain either
 \*  - advances its height
 \*  - receives datagrams and updates its state
+\*  - sends a packet (TODO)
 Next ==
-    \/ AdvanceChain
+    \/ AdvanceChain 
     \/ HandleIncomingDatagrams
     \/ UNCHANGED vars
-
+        
 Fairness ==
     /\ WF_vars(AdvanceChain)
-    /\ WF_vars(HandleIncomingDatagrams)
+    /\ WF_vars(HandleIncomingDatagrams)        
 
 (***************************************************************************
  Invariants
  ***************************************************************************)
 \* Type invariant   
-\* Chains and Datagrams are defined in RelayerDefinitions.tla        
+\* ChainStores and Datagrams are defined in RelayerDefinitions.tla        
 TypeOK ==    
-    /\ chainStore \in Chains
-    /\ incomingDatagrams \in SUBSET Datagrams(Heights)
+    /\ chainStore \in ChainStores(MaxHeight, ChannelOrdering, MaxPacketSeq)
+    /\ incomingDatagrams \in SUBSET Datagrams(MaxHeight, MaxPacketSeq)
+    /\ history \in Histories
 
 (***************************************************************************
  Properties
@@ -147,5 +182,5 @@ HeightDoesntDecrease ==
 
 =============================================================================
 \* Modification History
-\* Last modified Fri Jul 10 16:13:04 CEST 2020 by ilinastoilkovska
+\* Last modified Thu Sep 10 15:43:42 CEST 2020 by ilinastoilkovska
 \* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska