Added type annotations for Snowcat in IBCCore and IBCTokenTransfer TL…

…A+ specs (informalsystems#820) * annotations for snowcat * README modified * ICS20 snowcat type annotations * comments and README * added MC files * fix in README
Kukoomomo · Apr 15, 2021 · c7d049f · c7d049f
1 parent 7a23de2
commit c7d049f
Show file tree

Hide file tree

Showing 19 changed files with 1,198 additions and 1,011 deletions.
diff --git a/docs/spec/tla/fungible-token-transfer/Bank.tla b/docs/spec/tla/fungible-token-transfer/Bank.tla
@@ -1,12 +1,19 @@
 -------------------------------- MODULE Bank --------------------------------
 
+(***************************************************************************
+ This module contains definitions of operators that model the behavior of 
+ the bank module.
+ ***************************************************************************)
+
 EXTENDS Integers, FiniteSets
 
 \* subtract coins from account
+\* @type: (ACCOUNT -> Int, ACCOUNT, Int) => ACCOUNT -> Int;
 SubtractCoins(accounts, accountID, amount) ==
     [accounts EXCEPT ![accountID] = accounts[accountID] - amount]
 
 \* add coins to account
+\* @type: (ACCOUNT -> Int, ACCOUNT, Int) => ACCOUNT -> Int;
 AddCoins(accounts, accountID, amount) ==
     LET newDomain == (DOMAIN accounts) \union {accountID} IN
 
@@ -29,6 +36,9 @@ AddCoins(accounts, accountID, amount) ==
 \*        to account balances
 \*      - receiverAccounts is a map from receiver addresses and denominations 
 \*        to account balances
+(* @type: (ACCOUNT -> Int, Str, ACCOUNT -> Int, Str, Seq(Str), Int) => 
+            [senderAccounts: ACCOUNT -> Int, receiverAccounts: ACCOUNT -> Int, error: Bool];
+*)
 TransferCoins(senderAccounts, senderAddr, 
               receiverAccounts, receiverAddr, 
               denomination, amount) ==
@@ -58,6 +68,7 @@ TransferCoins(senderAccounts, senderAddr,
 \* denomination  
 \*      - accounts is a map from addresses and denominations 
 \*        to account balances
+\* @type: (ACCOUNT -> Int, Str, Seq(Str), Int) => [accounts: ACCOUNT -> Int, error: Bool];
 BurnCoins(accounts, address, denomination, amount) ==
     LET accountID == <<address, denomination>> IN
     LET balance == accounts[accountID] IN
@@ -78,6 +89,7 @@ BurnCoins(accounts, address, denomination, amount) ==
 
 
 \* Mint new coins of denomination to account with the given address
+\* @type: (ACCOUNT -> Int, Str, Seq(Str), Int, Int) => [accounts: ACCOUNT -> Int, error: Bool];
 MintCoins(accounts, address, denomination, amount, maxBalance) ==
     LET accountID == <<address, denomination>> IN
 
@@ -97,9 +109,7 @@ MintCoins(accounts, address, denomination, amount, maxBalance) ==
             error |-> TRUE
          ]
 
-
-
 =============================================================================
 \* Modification History
-\* Last modified Thu Nov 19 18:54:36 CET 2020 by ilinastoilkovska
+\* Last modified Wed Apr 14 14:50:41 CEST 2021 by ilinastoilkovska
 \* Created Thu Oct 28 19:49:56 CET 2020 by ilinastoilkovska
diff --git a/docs/spec/tla/fungible-token-transfer/Chain.tla b/docs/spec/tla/fungible-token-transfer/Chain.tla
@@ -1,21 +1,34 @@
 ------------------------------- MODULE Chain -------------------------------
 
+(***************************************************************************
+ This module models the behavior of a chain running the IBC Token Transfer 
+ Protocol.
+ 
+ The chain state is represented by a chain store, which is a snapshot of the
+ provable and private stores, to the extent necessary for ICS20. Additionally, 
+ a chain has a dedicated datagram container for packet datagrams (given by a 
+ queue of datagrams that models the order in which the datagrams were submitted 
+ by some relayer).
+***************************************************************************)
+
 EXTENDS Integers, FiniteSets, Sequences, IBCTokenTransferDefinitions, 
         ICS04PacketHandlers, ICS20FungibleTokenTransferHandlers
 
-CONSTANTS MaxHeight, \* maximal chain height
-          MaxPacketSeq, \* maximal packet sequence number
-          MaxBalance, \* maximal account balance
-          ChainID, \* a chain ID
-          NativeDenomination \* native denomination of tokens at ChainID 
+CONSTANTS 
+    MaxHeight, \* maximal chain height
+    MaxPacketSeq, \* maximal packet sequence number
+    MaxBalance, \* maximal account balance
+    ChainID, \* a chain ID
+    NativeDenomination \* native denomination of tokens at ChainID 
 
 
-VARIABLES chainStore, \* chain store, containing client heights, a connection end, a channel end 
-          incomingPacketDatagrams, \* sequence of incoming packet datagrams
-          appPacketSeq, \* packet sequence number from the application on the chain
-          packetLog, \* packet log
-          accounts, \* a map from chainIDs and denominations to account balances
-          escrowAccounts \* a map from channelIDs and denominations to escrow account balances
+VARIABLES 
+    chainStore, \* chain store, containing client heights, a channel end 
+    incomingPacketDatagrams, \* sequence of incoming packet datagrams
+    appPacketSeq, \* packet sequence number from the application on the chain
+    packetLog, \* packet log
+    accounts, \* a map from chainIDs and denominations to account balances
+    escrowAccounts \* a map from channelIDs and denominations to escrow account balances
 
 
 vars == <<chainStore, incomingPacketDatagrams, appPacketSeq, 
@@ -29,18 +42,19 @@ Heights == 1..MaxHeight \* set of possible heights of the chains in the system
 \* Assume timeoutHeight is MaxHeight
 CreatePacket(packetData) ==
     LET channelEnd == chainStore.channelEnd IN
-    AsPacket([
+    [
         sequence |-> appPacketSeq,
         timeoutHeight |-> MaxHeight,
         data |-> packetData, 
         srcPortID |-> channelEnd.portID,
         srcChannelID |-> channelEnd.channelID,
         dstPortID |-> channelEnd.counterpartyPortID,
         dstChannelID |-> channelEnd.counterpartyChannelID
-    ])
+    ]
 
 
 \* Update the chain store and packet log with ICS20 packet datagrams 
+\* @type: (Str, DATAGRAM, Seq(LOGENTRY)) => [store: CHAINSTORE, log: Seq(LOGENTRY), accounts: ACCOUNT -> Int, escrowAccounts: ACCOUNT -> Int];
 TokenTransferUpdate(chainID, packetDatagram, log) ==
     LET packet == packetDatagram.packet IN
     \* get the new updated store, packet log, and accounts
@@ -82,7 +96,7 @@ AdvanceChain ==
 \* handle the incoming packet datagrams
 HandlePacketDatagrams ==
     \* enabled if incomingPacketDatagrams is not empty
-    /\ incomingPacketDatagrams /= AsSeqDatagrams(<<>>)
+    /\ incomingPacketDatagrams /= <<>>
     /\ LET tokenTransferUpdate == TokenTransferUpdate(ChainID, Head(incomingPacketDatagrams), packetLog) IN 
         /\ chainStore' = tokenTransferUpdate.store 
         /\ packetLog' = tokenTransferUpdate.log
@@ -115,14 +129,13 @@ SendPacket ==
                 \* update chain store with packet committment
                 /\ chainStore' = updatedChainStore
                 \* log sent packet
-                /\ packetLog' = Append(packetLog, 
-                                  AsPacketLogEntry(
-                                    [type |-> "PacketSent", 
-                                     srcChainID |-> ChainID,  
-                                     sequence |-> packet.sequence,
-                                     timeoutHeight |-> packet.timeoutHeight,
-                                     data |-> packet.data]
-                                  ))
+                /\ packetLog' = Append(packetLog, [
+                                                    type |-> "PacketSent", 
+                                                    srcChainID |-> ChainID,  
+                                                    sequence |-> packet.sequence,
+                                                    timeoutHeight |-> packet.timeoutHeight,
+                                                    data |-> packet.data
+                                                  ])
                 \* update bank accounts 
                 /\ accounts' = createOutgoingPacketOutcome.accounts
                 \* update escrow accounts 
@@ -135,7 +148,7 @@ SendPacket ==
 
 \* Acknowledge a packet
 AcknowledgePacket ==
-    /\ chainStore.packetsToAcknowledge /= AsSeqPacketsToAck(<<>>)
+    /\ chainStore.packetsToAcknowledge /= <<>>
     \* write acknowledgements to chain store
     /\ chainStore' = WriteAcknowledgement(chainStore, Head(chainStore.packetsToAcknowledge))
     \* log acknowledgement
@@ -155,8 +168,8 @@ AcknowledgePacket ==
 \*  - the appPacketSeq is set to 1
 Init == 
     /\ chainStore = ICS20InitChainStore(ChainID)
-    /\ incomingPacketDatagrams = AsSeqDatagrams(<<>>)
-    /\ appPacketSeq = AsInt(1)
+    /\ incomingPacketDatagrams = <<>>
+    /\ appPacketSeq = 1
 
 \* Next state action
 \* The chain either
@@ -180,11 +193,11 @@ Fairness ==
 \* Type invariant   
 \* ChainStores, Datagrams, PacketLogEntries are defined in IBCTokenTransferDefinitions.tla        
 TypeOK ==    
-    /\ chainStore \in ChainStores(Heights, MaxPacketSeq, MaxBalance, NativeDenomination)
+    /\ chainStore \in ChainStores(Heights, MaxPacketSeq, MaxBalance, {NativeDenomination})
     /\ appPacketSeq \in 1..(MaxPacketSeq + 1)
 
 
 =============================================================================
 \* Modification History
-\* Last modified Mon Feb 01 19:31:22 CET 2021 by ilinastoilkovska
+\* Last modified Wed Apr 14 15:33:11 CEST 2021 by ilinastoilkovska
 \* Created Mon Oct 17 13:01:03 CEST 2020 by ilinastoilkovska