Skip to content

Commit 53f97f6

Browse files
adizereadizere
committed
Merge branch 'master' into adi/158_local
2 parents 68771b6 + 9963c4a commit 53f97f6

28 files changed

+1043
-638
lines changed

‎CHANGELOG.md

-2
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ Special thanks to external contributors for this release: @CharlyCst ([#347]).
66

77
### FEATURES
88

9-
- Update Tokio to version 0.3 ([#402])
109
- Update to tendermint-rs version `0.17-RC3` ([#403])
1110
- [changelog] Added "unreleased" section in `CHANGELOG.MD` to help streamline releases ([#274])
1211
- [relayer] Integrate relayer spike into relayer crate ([#335])
@@ -48,7 +47,6 @@ Special thanks to external contributors for this release: @CharlyCst ([#347]).
4847
[#373]: https://github.com/informalsystems/ibc-rs/issues/373
4948
[#374]: https://github.com/informalsystems/ibc-rs/issues/374
5049
[#389]: https://github.com/informalsystems/ibc-rs/issues/389
51-
[#402]: https://github.com/informalsystems/ibc-rs/issues/402
5250
[#403]: https://github.com/informalsystems/ibc-rs/issues/403
5351
[proto-compiler]: https://github.com/informalsystems/ibc-rs/tree/master/proto-compiler
5452

‎Cargo.toml

-15
Original file line numberDiff line numberDiff line change
@@ -10,18 +10,3 @@ members = [
1010
exclude = [
1111
"proto-compiler"
1212
]
13-
14-
[patch.crates-io]
15-
tendermint = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/prost-dev" }
16-
tendermint-rpc = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/prost-dev" }
17-
tendermint-proto = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/prost-dev" }
18-
tendermint-light-client = { git = "https://github.com/informalsystems/tendermint-rs", branch = "romac/prost-dev" }
19-
20-
bytes = { git = "https://github.com/tokio-rs/bytes", tag = "v0.6.0" }
21-
22-
tonic = { git = "https://github.com/romac/tonic", branch = "romac/hyper-0.14-dev" }
23-
24-
prost = { git = "https://github.com/danburkert/prost", branch = "master" }
25-
prost-types = { git = "https://github.com/danburkert/prost", branch = "master" }
26-
prost-build = { git = "https://github.com/danburkert/prost", branch = "master" }
27-
prost-derive = { git = "https://github.com/danburkert/prost", branch = "master" }

‎docs/spec/fungible-token-transfer/Bank.tla

+22-6
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,15 @@ SubtractCoins(accounts, accountID, amount) ==
88

99
\* add coins to account
1010
AddCoins(accounts, accountID, amount) ==
11+
LET newDomain == (DOMAIN accounts) \union {accountID} IN
12+
1113
\* if an account with accountID exists
1214
IF accountID \in DOMAIN accounts
1315
\* add amount to account
1416
THEN [accounts EXCEPT ![accountID] = accounts[accountID] + amount]
1517
\* otherwise create a new account with balance equal to amount
1618
\* and add it to the map
17-
ELSE [accID \in DOMAIN accounts \union {accountID} |->
19+
ELSE [accID \in newDomain |->
1820
IF accID = accountID
1921
THEN amount
2022
ELSE accounts[accID]
@@ -76,14 +78,28 @@ BurnCoins(accounts, address, denomination, amount) ==
7678

7779

7880
\* Mint new coins of denomination to account with the given address
79-
\* TODO: when can an error happen here?
80-
MintCoins(accounts, address, denomination, amount) ==
81+
MintCoins(accounts, address, denomination, amount, maxBalance) ==
8182
LET accountID == <<address, denomination>> IN
82-
83-
AddCoins(accounts, accountID, amount)
83+
84+
\* if the new balance does not exceed maxBalance
85+
IF \/ /\ accountID \notin DOMAIN accounts
86+
/\ amount <= maxBalance
87+
\/ /\ accountID \in DOMAIN accounts
88+
/\ accounts[accountID] + amount <= maxBalance
89+
\* add coins to accountID
90+
THEN [
91+
accounts |-> AddCoins(accounts, accountID, amount),
92+
error |-> FALSE
93+
]
94+
\* otherwise report an error
95+
ELSE [
96+
accounts |-> accounts,
97+
error |-> TRUE
98+
]
99+
84100

85101

86102
=============================================================================
87103
\* Modification History
88-
\* Last modified Thu Nov 05 19:47:41 CET 2020 by ilinastoilkovska
104+
\* Last modified Thu Nov 19 18:54:36 CET 2020 by ilinastoilkovska
89105
\* Created Thu Oct 28 19:49:56 CET 2020 by ilinastoilkovska

‎docs/spec/fungible-token-transfer/ICS20Chain.tla renamed to ‎docs/spec/fungible-token-transfer/Chain.tla

+33-29
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
----------------------------- MODULE ICS20Chain -----------------------------
1+
------------------------------- MODULE Chain -------------------------------
22

3-
EXTENDS Integers, FiniteSets, Sequences, ICS20Definitions, PacketHandlers,
4-
FungibleTokenTransferHandlers
3+
EXTENDS Integers, FiniteSets, Sequences, IBCTokenTransferDefinitions,
4+
ICS04PacketHandlers, ICS20FungibleTokenTransferHandlers
55

66
CONSTANTS MaxHeight, \* maximal chain height
77
MaxPacketSeq, \* maximal packet sequence number
@@ -14,45 +14,45 @@ VARIABLES chainStore, \* chain store, containing client heights, a connection en
1414
incomingPacketDatagrams, \* sequence of incoming packet datagrams
1515
appPacketSeq, \* packet sequence number from the application on the chain
1616
packetLog, \* packet log
17-
accounts \* a map from chainIDs and denominations to account balances
17+
accounts, \* a map from chainIDs and denominations to account balances
18+
escrowAccounts \* a map from channelIDs and denominations to escrow account balances
1819

1920

2021
vars == <<chainStore, incomingPacketDatagrams, appPacketSeq,
21-
packetLog, accounts>>
22+
packetLog, accounts, escrowAccounts>>
2223
Heights == 1..MaxHeight \* set of possible heights of the chains in the system
2324

2425
(***************************************************************************
2526
Token transfer operators
2627
***************************************************************************)
27-
\* Create a packet: Abstract away from ports, and timestamp.
28+
\* Create a packet: Abstract away from timestamp.
2829
\* Assume timeoutHeight is MaxHeight + 1
2930
CreatePacket(packetData) ==
3031
AsPacket([
3132
sequence |-> appPacketSeq,
3233
timeoutHeight |-> MaxHeight + 1,
3334
data |-> packetData,
3435
srcChannelID |-> GetChannelID(ChainID),
35-
dstChannelID |-> GetChannelID(GetCounterpartyChainID(ChainID))
36+
srcPortID |-> GetPortID(ChainID),
37+
dstChannelID |-> GetCounterpartyChannelID(ChainID),
38+
dstPortID |-> GetCounterpartyPortID(ChainID)
3639
])
37-
38-
\* update packet committments and escrow accounts in the chain store
39-
UpdatePacketCommitmentsAndEscrowAcounts(chain, packet, escrowAccounts) ==
40-
\* write packet committment
41-
LET writtenCommittmentStore == WritePacketCommitment(chain, packet) IN
42-
\* update escrow accounts
43-
[writtenCommittmentStore EXCEPT !.escrowAccounts = escrowAccounts]
44-
40+
4541

4642
\* Update the chain store and packet log with ICS20 packet datagrams
4743
TokenTransferUpdate(chainID, packetDatagram, log) ==
4844
LET packet == packetDatagram.packet IN
4945
\* get the new updated store, packet log, and accounts
5046
LET tokenTransferUpdate ==
5147
IF packetDatagram.type = "PacketRecv"
52-
THEN HandlePacketRecv(chainID, chainStore, packetDatagram, log, accounts)
48+
THEN HandlePacketRecv(chainID, chainStore, packetDatagram, log, accounts, escrowAccounts, MaxBalance)
5349
ELSE IF packetDatagram.type = "PacketAck"
54-
THEN HandlePacketAck(chainID, chainStore, packetDatagram, log, accounts)
55-
ELSE [store |-> chainStore, log |-> log, accounts |-> accounts] IN
50+
THEN HandlePacketAck(chainStore, packetDatagram, log, accounts, escrowAccounts, MaxBalance)
51+
ELSE [store |-> chainStore,
52+
log |-> log,
53+
accounts |-> accounts,
54+
escrowAccounts |-> escrowAccounts]
55+
IN
5656

5757
LET tokenTransferStore == tokenTransferUpdate.store IN
5858

@@ -65,7 +65,8 @@ TokenTransferUpdate(chainID, packetDatagram, log) ==
6565

6666
[store |-> updatedStore,
6767
log |-> tokenTransferUpdate.log,
68-
accounts |-> tokenTransferUpdate.accounts]
68+
accounts |-> tokenTransferUpdate.accounts,
69+
escrowAccounts |-> tokenTransferUpdate.escrowAccounts]
6970

7071
(***************************************************************************
7172
Chain actions
@@ -74,7 +75,8 @@ TokenTransferUpdate(chainID, packetDatagram, log) ==
7475
AdvanceChain ==
7576
/\ chainStore.height + 1 \in Heights
7677
/\ chainStore' = [chainStore EXCEPT !.height = chainStore.height + 1]
77-
/\ UNCHANGED <<incomingPacketDatagrams, appPacketSeq, packetLog, accounts>>
78+
/\ UNCHANGED <<incomingPacketDatagrams, appPacketSeq, packetLog>>
79+
/\ UNCHANGED <<accounts, escrowAccounts>>
7880

7981
\* handle the incoming packet datagrams
8082
HandlePacketDatagrams ==
@@ -84,6 +86,7 @@ HandlePacketDatagrams ==
8486
/\ chainStore' = tokenTransferUpdate.store
8587
/\ packetLog' = tokenTransferUpdate.log
8688
/\ accounts' = tokenTransferUpdate.accounts
89+
/\ escrowAccounts' = tokenTransferUpdate.escrowAccounts
8790
/\ incomingPacketDatagrams' = Tail(incomingPacketDatagrams)
8891
/\ UNCHANGED appPacketSeq
8992

@@ -94,7 +97,7 @@ SendPacket ==
9497
\* Create packet data
9598
/\ LET createOutgoingPacketOutcome ==
9699
CreateOutgoingPacketData(accounts,
97-
chainStore.escrowAccounts,
100+
escrowAccounts,
98101
<<NativeDenomination>>,
99102
MaxBalance,
100103
ChainID,
@@ -106,8 +109,7 @@ SendPacket ==
106109
\/ /\ ~createOutgoingPacketOutcome.error
107110
/\ LET packet == CreatePacket(createOutgoingPacketOutcome.packetData) IN
108111
\* update chain store with packet committment
109-
/\ chainStore' = UpdatePacketCommitmentsAndEscrowAcounts(
110-
chainStore, packet, createOutgoingPacketOutcome.escrowAccounts)
112+
/\ chainStore' = WritePacketCommitment(chainStore, packet)
111113
\* log sent packet
112114
/\ packetLog' = Append(packetLog,
113115
AsPacketLogEntry(
@@ -119,6 +121,8 @@ SendPacket ==
119121
))
120122
\* update bank accounts
121123
/\ accounts' = createOutgoingPacketOutcome.accounts
124+
\* update escrow accounts
125+
/\ escrowAccounts' = createOutgoingPacketOutcome.escrowAccounts
122126
\* increase application packet sequence
123127
/\ appPacketSeq' = appPacketSeq + 1
124128
/\ UNCHANGED incomingPacketDatagrams
@@ -132,17 +136,17 @@ AcknowledgePacket ==
132136
/\ chainStore' = WriteAcknowledgement(chainStore, Head(chainStore.packetsToAcknowledge))
133137
\* log acknowledgement
134138
/\ packetLog' = LogAcknowledgement(ChainID, chainStore, packetLog, Head(chainStore.packetsToAcknowledge))
135-
/\ UNCHANGED <<incomingPacketDatagrams, accounts>>
136-
/\ UNCHANGED <<appPacketSeq>>
139+
/\ UNCHANGED <<incomingPacketDatagrams, appPacketSeq>>
140+
/\ UNCHANGED <<accounts, escrowAccounts>>
137141

138142
(***************************************************************************
139143
Specification
140144
***************************************************************************)
141145
\* Initial state predicate
142146
\* Initially
143-
\* - the chain store is initialized to some element of the set
144-
\* ICS20InitChainStore(ChainID, NativeDenomination)
145-
\* (defined in ICS20Definitions.tla)
147+
\* - the chain store is initialized to
148+
\* ICS20InitChainStore(ChainID, <<NativeDenomination>>)
149+
\* (defined in IBCTokenTransferDefinitions.tla)
146150
\* - incomingPacketDatagrams is an empty sequence
147151
\* - the appPacketSeq is set to 1
148152
Init ==
@@ -168,5 +172,5 @@ Fairness ==
168172

169173
=============================================================================
170174
\* Modification History
171-
\* Last modified Fri Nov 06 20:27:05 CET 2020 by ilinastoilkovska
175+
\* Last modified Fri Nov 20 16:09:50 CET 2020 by ilinastoilkovska
172176
\* Created Mon Oct 17 13:01:03 CEST 2020 by ilinastoilkovska

0 commit comments

Comments
 (0)