TLA+ for ICS20 -- ICF deliverable (#409)

* ICS 20 polish * escrow accounts in shared variable * renamed files * updated readme * properties * token transfer properties * added packet data field in packet commitment * final readme fixes
informalsystems · Nov 26, 2020 · 9963c4a · 9963c4a
1 parent d732aef
commit 9963c4a
Show file tree

Hide file tree

Showing 9 changed files with 921 additions and 532 deletions.
diff --git a/docs/spec/fungible-token-transfer/Bank.tla b/docs/spec/fungible-token-transfer/Bank.tla
@@ -8,13 +8,15 @@ SubtractCoins(accounts, accountID, amount) ==
 
 \* add coins to account
 AddCoins(accounts, accountID, amount) ==
+    LET newDomain == (DOMAIN accounts) \union {accountID} IN
+
     \* if an account with accountID exists
     IF accountID \in DOMAIN accounts
     \* add amount to account
     THEN [accounts EXCEPT ![accountID] = accounts[accountID] + amount]
     \* otherwise create a new account with balance equal to amount 
     \* and add it to the map
-    ELSE [accID \in DOMAIN accounts \union {accountID} |-> 
+    ELSE [accID \in newDomain |-> 
             IF accID = accountID
             THEN amount
             ELSE accounts[accID]   
@@ -76,14 +78,28 @@ BurnCoins(accounts, address, denomination, amount) ==
 
 
 \* Mint new coins of denomination to account with the given address
-\* TODO: when can an error happen here?
-MintCoins(accounts, address, denomination, amount) ==
+MintCoins(accounts, address, denomination, amount, maxBalance) ==
     LET accountID == <<address, denomination>> IN
-
-    AddCoins(accounts, accountID, amount)
+
+    \* if the new balance does not exceed maxBalance
+    IF \/ /\ accountID \notin DOMAIN accounts
+          /\ amount <= maxBalance 
+       \/ /\ accountID \in DOMAIN accounts
+          /\ accounts[accountID] + amount <= maxBalance
+    \* add coins to accountID   
+    THEN [
+            accounts |-> AddCoins(accounts, accountID, amount), 
+            error |-> FALSE
+         ]
+    \* otherwise report an error         
+    ELSE [
+            accounts |-> accounts,
+            error |-> TRUE
+         ]
+
 
 
 =============================================================================
 \* Modification History
-\* Last modified Thu Nov 05 19:47:41 CET 2020 by ilinastoilkovska
+\* Last modified Thu Nov 19 18:54:36 CET 2020 by ilinastoilkovska
 \* Created Thu Oct 28 19:49:56 CET 2020 by ilinastoilkovska
diff --git a/...ec/fungible-token-transfer/ICS20Chain.tla → docs/spec/fungible-token-transfer/Chain.tla b/...ec/fungible-token-transfer/ICS20Chain.tla → docs/spec/fungible-token-transfer/Chain.tla
@@ -1,7 +1,7 @@
------------------------------ MODULE ICS20Chain -----------------------------
+------------------------------- MODULE Chain -------------------------------
 
-EXTENDS Integers, FiniteSets, Sequences, ICS20Definitions, PacketHandlers, 
-        FungibleTokenTransferHandlers
+EXTENDS Integers, FiniteSets, Sequences, IBCTokenTransferDefinitions, 
+        ICS04PacketHandlers, ICS20FungibleTokenTransferHandlers
 
 CONSTANTS MaxHeight, \* maximal chain height
           MaxPacketSeq, \* maximal packet sequence number
@@ -14,45 +14,45 @@ VARIABLES chainStore, \* chain store, containing client heights, a connection en
           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
+          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, 
-          packetLog, accounts>>
+          packetLog, accounts, escrowAccounts>>
 Heights == 1..MaxHeight \* set of possible heights of the chains in the system 
 
 (***************************************************************************
  Token transfer operators
  ***************************************************************************)
-\* Create a packet: Abstract away from ports, and timestamp. 
+\* Create a packet: Abstract away from timestamp. 
 \* Assume timeoutHeight is MaxHeight + 1
 CreatePacket(packetData) ==
     AsPacket([
         sequence |-> appPacketSeq,
         timeoutHeight |-> MaxHeight + 1,
         data |-> packetData, 
         srcChannelID |-> GetChannelID(ChainID),
-        dstChannelID |-> GetChannelID(GetCounterpartyChainID(ChainID))
+        srcPortID |-> GetPortID(ChainID),
+        dstChannelID |-> GetCounterpartyChannelID(ChainID),
+        dstPortID |-> GetCounterpartyPortID(ChainID)
     ])
-
-\* update packet committments and escrow accounts in the chain store
-UpdatePacketCommitmentsAndEscrowAcounts(chain, packet, escrowAccounts) ==
-    \* write packet committment
-    LET writtenCommittmentStore == WritePacketCommitment(chain, packet) IN
-    \* update escrow accounts 
-    [writtenCommittmentStore EXCEPT !.escrowAccounts = escrowAccounts]
-
+
 
 \* Update the chain store and packet log with ICS20 packet datagrams 
 TokenTransferUpdate(chainID, packetDatagram, log) ==
     LET packet == packetDatagram.packet IN
     \* get the new updated store, packet log, and accounts
     LET tokenTransferUpdate == 
         IF packetDatagram.type = "PacketRecv"
-        THEN HandlePacketRecv(chainID, chainStore, packetDatagram, log, accounts)
+        THEN HandlePacketRecv(chainID, chainStore, packetDatagram, log, accounts, escrowAccounts, MaxBalance)
         ELSE IF packetDatagram.type = "PacketAck"
-             THEN HandlePacketAck(chainID, chainStore, packetDatagram, log, accounts)
-             ELSE [store |-> chainStore, log |-> log, accounts |-> accounts] IN
+             THEN HandlePacketAck(chainStore, packetDatagram, log, accounts, escrowAccounts, MaxBalance)
+             ELSE [store |-> chainStore, 
+                   log |-> log, 
+                   accounts |-> accounts, 
+                   escrowAccounts |-> escrowAccounts]
+    IN
 
     LET tokenTransferStore == tokenTransferUpdate.store IN
 
@@ -65,7 +65,8 @@ TokenTransferUpdate(chainID, packetDatagram, log) ==
 
     [store |-> updatedStore, 
      log |-> tokenTransferUpdate.log, 
-     accounts |-> tokenTransferUpdate.accounts]       
+     accounts |-> tokenTransferUpdate.accounts,
+     escrowAccounts |-> tokenTransferUpdate.escrowAccounts]       
 
 (***************************************************************************
  Chain actions
@@ -74,7 +75,8 @@ TokenTransferUpdate(chainID, packetDatagram, log) ==
 AdvanceChain ==
     /\ chainStore.height + 1 \in Heights
     /\ chainStore' = [chainStore EXCEPT !.height = chainStore.height + 1]
-    /\ UNCHANGED <<incomingPacketDatagrams, appPacketSeq, packetLog, accounts>>
+    /\ UNCHANGED <<incomingPacketDatagrams, appPacketSeq, packetLog>>
+    /\ UNCHANGED <<accounts, escrowAccounts>>
 
 \* handle the incoming packet datagrams
 HandlePacketDatagrams ==
@@ -84,6 +86,7 @@ HandlePacketDatagrams ==
         /\ chainStore' = tokenTransferUpdate.store 
         /\ packetLog' = tokenTransferUpdate.log
         /\ accounts' = tokenTransferUpdate.accounts
+        /\ escrowAccounts' = tokenTransferUpdate.escrowAccounts
         /\ incomingPacketDatagrams' = Tail(incomingPacketDatagrams)
         /\ UNCHANGED appPacketSeq
 
@@ -94,7 +97,7 @@ SendPacket ==
     \* Create packet data 
     /\ LET createOutgoingPacketOutcome == 
             CreateOutgoingPacketData(accounts, 
-                                     chainStore.escrowAccounts,
+                                     escrowAccounts,
                                      <<NativeDenomination>>,
                                      MaxBalance,
                                      ChainID,
@@ -106,8 +109,7 @@ SendPacket ==
         \/ /\ ~createOutgoingPacketOutcome.error
            /\ LET packet == CreatePacket(createOutgoingPacketOutcome.packetData) IN
                 \* update chain store with packet committment
-                /\ chainStore' = UpdatePacketCommitmentsAndEscrowAcounts(
-                                chainStore, packet, createOutgoingPacketOutcome.escrowAccounts)
+                /\ chainStore' = WritePacketCommitment(chainStore, packet)
                 \* log sent packet
                 /\ packetLog' = Append(packetLog, 
                                   AsPacketLogEntry(
@@ -119,6 +121,8 @@ SendPacket ==
                                   ))
                 \* update bank accounts 
                 /\ accounts' = createOutgoingPacketOutcome.accounts
+                \* update escrow accounts 
+                /\ escrowAccounts' = createOutgoingPacketOutcome.escrowAccounts
                 \* increase application packet sequence
                 /\ appPacketSeq' = appPacketSeq + 1
                 /\ UNCHANGED incomingPacketDatagrams
@@ -132,17 +136,17 @@ AcknowledgePacket ==
     /\ chainStore' = WriteAcknowledgement(chainStore, Head(chainStore.packetsToAcknowledge))
     \* log acknowledgement
     /\ packetLog' = LogAcknowledgement(ChainID, chainStore, packetLog, Head(chainStore.packetsToAcknowledge))
-    /\ UNCHANGED <<incomingPacketDatagrams, accounts>>
-    /\ UNCHANGED <<appPacketSeq>>
+    /\ UNCHANGED <<incomingPacketDatagrams, appPacketSeq>> 
+    /\ UNCHANGED <<accounts, escrowAccounts>>
 
 (***************************************************************************
  Specification
  ***************************************************************************)
 \* Initial state predicate
 \* Initially
-\*  - the chain store is initialized to some element of the set
-\*    ICS20InitChainStore(ChainID, NativeDenomination) 
-\*    (defined in ICS20Definitions.tla)
+\*  - the chain store is initialized to 
+\*    ICS20InitChainStore(ChainID, <<NativeDenomination>>) 
+\*    (defined in IBCTokenTransferDefinitions.tla)
 \*  - incomingPacketDatagrams is an empty sequence
 \*  - the appPacketSeq is set to 1
 Init == 
@@ -168,5 +172,5 @@ Fairness ==
 
 =============================================================================
 \* Modification History
-\* Last modified Fri Nov 06 20:27:05 CET 2020 by ilinastoilkovska
+\* Last modified Fri Nov 20 16:09:50 CET 2020 by ilinastoilkovska
 \* Created Mon Oct 17 13:01:03 CEST 2020 by ilinastoilkovska