forked from cosmos/ibc-rs
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Relayer TLA+ refactoring (cosmos#117)
* relayer restructuring * refactoring the relayer * changed file structure * removing v2 * Added RelayerDefinitions.tla and addressed some comments * Update docs/spec/relayer/README.md Co-authored-by: Adi Seredinschi <[email protected]> * addressed comments * fixed fairness constraint Co-authored-by: Adi Seredinschi <[email protected]>
- Loading branch information
1 parent
e1b7894
commit 8e3716c
Showing
14 changed files
with
2,189 additions
and
663 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,172 @@ | ||
| -------------------------- MODULE ChannelHandlers -------------------------- | ||
|
|
||
| (*************************************************************************** | ||
| This module contains definitions of operators that are used to handle | ||
| channel datagrams | ||
| ***************************************************************************) | ||
|
|
||
| EXTENDS Naturals, FiniteSets | ||
|
|
||
| ChannelIDs == {"chanAtoB", "chanBtoA"} | ||
| nullChannelID == "none" | ||
|
|
||
| ChannelStates == {"UNINIT", "INIT", "TRYOPEN", "OPEN", "CLOSED"} | ||
| ChannelOrder == {"ORDERED", "UNORDERED"} | ||
|
|
||
| (*************************************************************************** | ||
| Channel helper operators | ||
| ***************************************************************************) | ||
|
|
||
| \* get the channel ID of the channel end at the connection end of chainID | ||
| GetChannelID(chainID) == | ||
| IF chainID = "chainA" | ||
| THEN "chanAtoB" | ||
| ELSE IF chainID = "chainB" | ||
| THEN "chanBtoA" | ||
| ELSE nullChannelID | ||
|
|
||
| \* get the channel ID of the channel end at chainID's counterparty chain | ||
| GetCounterpartyChannelID(chainID) == | ||
| IF chainID = "chainA" | ||
| THEN "chanBtoA" | ||
| ELSE IF chainID = "chainB" | ||
| THEN "chanAtoB" | ||
| ELSE nullChannelID | ||
|
|
||
| (*************************************************************************** | ||
| Channel datagram handlers | ||
| ***************************************************************************) | ||
|
|
||
| \* Handle "ChanOpenInit" datagrams | ||
| HandleChanOpenInit(chainID, chain, datagrams) == | ||
| \* get "ChanOpenInit" datagrams, with a valid channel ID | ||
| LET chanOpenInitDgrs == {dgr \in datagrams : | ||
| /\ dgr.type = "ChanOpenInit" | ||
| /\ dgr.channelID = GetChannelID(chainID)} IN | ||
|
|
||
| \* if there are valid "ChanOpenInit" datagrams and the connection is not "UNINIT", | ||
| \* create a new channel end and update the chain | ||
| IF chanOpenInitDgrs /= {} /\ chain.connectionEnd.state /= "UNINIT" | ||
| THEN LET chanOpenInitDgr == CHOOSE dgr \in chanOpenInitDgrs : TRUE IN | ||
| LET chanOpenInitChannelEnd == [ | ||
| state |-> "INIT", | ||
| channelID |-> chanOpenInitDgr.channelID, | ||
| counterpartyChannelID |-> chanOpenInitDgr.counterpartyChannelID | ||
| ] IN | ||
| LET chanOpenInitConnectionEnd == [ | ||
| chain.connectionEnd EXCEPT !.channelEnd = chanOpenInitChannelEnd | ||
| ] IN | ||
| LET chanOpenInitChain == [ | ||
| chain EXCEPT !.connectionEnd = chanOpenInitConnectionEnd | ||
| ] IN | ||
|
|
||
| \* TODO: check here if channel is already in INIT? | ||
| \* TODO: when handling packets later on, set nextSequenceRecv and nextSequenceSend to 1 | ||
| chanOpenInitChain | ||
| \* otherwise, do not update the chain | ||
| ELSE chain | ||
|
|
||
| \* Handle "ChanOpenTry" datagrams | ||
| HandleChanOpenTry(chainID, chain, datagrams) == | ||
| \* get "ChanOpenTry" datagrams, with a valid channel ID | ||
| LET chanOpenTryDgrs == {dgr \in datagrams : | ||
| /\ dgr.type = "ChanOpenTry" | ||
| /\ dgr.channelID = GetChannelID(chainID) | ||
| /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN | ||
|
|
||
| \* if there are valid "ChanOpenTry" datagrams and the connection is "OPEN", | ||
| \* update the channel end | ||
| IF chanOpenTryDgrs /= {} /\ chain.connectionEnd.state = "OPEN" | ||
| THEN LET chanOpenTryDgr == CHOOSE dgr \in chanOpenTryDgrs : TRUE IN | ||
| LET chanOpenTryChannelEnd == [ | ||
| state |-> "TRYOPEN", | ||
| channelID |-> chanOpenTryDgr.channelID, | ||
| counterpartyChannelID |-> chanOpenTryDgr.counterpartyChannelID | ||
| ] IN | ||
|
|
||
| IF \/ chain.connectionEnd.channelEnd.state = "UNINIT" | ||
| \/ /\ chain.connectionEnd.channelEnd.state = "INIT" | ||
| /\ chain.connectionEnd.channelEnd.counterpartyChannelID | ||
| = chanOpenTryChannelEnd.counterpartyChannelID | ||
| \* if the channel end on the chain is in "UNINIT" or it is in "INIT", | ||
| \* but the fields are the same as in the datagram, update the channel end | ||
| THEN LET chanOpenTryConnectionEnd == [ | ||
| chain.connectionEnd EXCEPT !.channelEnd = chanOpenTryChannelEnd | ||
| ] IN | ||
| LET chanOpenTryChain == [ | ||
| chain EXCEPT !.connectionEnd = chanOpenTryConnectionEnd | ||
| ] IN | ||
|
|
||
| chanOpenTryChain | ||
| \* otherwise, do not update the chain | ||
| ELSE chain | ||
| \* otherwise, do not update the chain | ||
| ELSE chain | ||
|
|
||
| \* Handle "ChanOpenAck" datagrams | ||
| HandleChanOpenAck(chainID, chain, datagrams) == | ||
| \* get "ChanOpenAck" datagrams, with a valid channel ID | ||
| LET chanOpenAckDgrs == {dgr \in datagrams : | ||
| /\ dgr.type = "ChanOpenAck" | ||
| /\ dgr.channelID = GetChannelID(chainID) | ||
| /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN | ||
|
|
||
| \* if there are valid "ChanOpenAck" datagrams, update the channel end | ||
| IF chanOpenAckDgrs /= {} /\ chain.connectionEnd.state = "OPEN" | ||
| THEN \* if the channel end on the chain is in "INIT" or it is in "TRYOPEN", | ||
| \* update the channel end | ||
| IF \/ chain.connectionEnd.channelEnd.state = "INIT" | ||
| \/ chain.connectionEnd.channelEnd.state = "TRYOPEN" | ||
| THEN LET chanOpenAckDgr == CHOOSE dgr \in chanOpenAckDgrs : TRUE IN | ||
| LET chanOpenAckChannelEnd == [ | ||
| chain.connectionEnd.channelEnd EXCEPT !.state = "OPEN", | ||
| !.channelID = chanOpenAckDgr.channelID | ||
| ] IN | ||
| LET chanOpenAckConnectionEnd == [ | ||
| chain.connectionEnd EXCEPT !.channelEnd = chanOpenAckChannelEnd | ||
| ] IN | ||
| LET chanOpenAckChain == [ | ||
| chain EXCEPT !.connectionEnd = chanOpenAckConnectionEnd | ||
| ] IN | ||
|
|
||
| chanOpenAckChain | ||
| \* otherwise, do not update the chain | ||
| ELSE chain | ||
| \* otherwise, do not update the chain | ||
| ELSE chain | ||
|
|
||
|
|
||
| \* Handle "ChanOpenConfirm" datagrams | ||
| HandleChanOpenConfirm(chainID, chain, datagrams) == | ||
| \* get "ChanOpenConfirm" datagrams, with a valid channel ID | ||
| LET chanOpenConfirmDgrs == {dgr \in datagrams : | ||
| /\ dgr.type = "ChanOpenConfirm" | ||
| /\ dgr.channelID = GetChannelID(chainID) | ||
| /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN | ||
|
|
||
| \* if there are valid "ChanOpenConfirm" datagrams, update the channel end | ||
| IF chanOpenConfirmDgrs /= {} /\ chain.connectionEnd.state = "OPEN" | ||
| THEN \* if the channel end on the chain is in "TRYOPEN", update the channel end | ||
| IF chain.connectionEnd.channelEnd.state = "TRYOPEN" | ||
| THEN LET chanOpenConfirmDgr == CHOOSE dgr \in chanOpenConfirmDgrs : TRUE IN | ||
| LET chanOpenConfirmChannelEnd == [ | ||
| chain.connectionEnd.channelEnd EXCEPT !.state = "OPEN", | ||
| !.channelID = chanOpenConfirmDgr.channelID | ||
| ] IN | ||
| LET chanOpenConfirmConnectionEnd == [ | ||
| chain.connectionEnd EXCEPT !.channelEnd = chanOpenConfirmChannelEnd | ||
| ] IN | ||
| LET chanOpenConfirmChain == [ | ||
| chain EXCEPT !.connectionEnd = chanOpenConfirmConnectionEnd | ||
| ] IN | ||
|
|
||
| chanOpenConfirmChain | ||
| \* otherwise, do not update the chain | ||
| ELSE chain | ||
| \* otherwise, do not update the chain | ||
| ELSE chain | ||
|
|
||
| ============================================================================= | ||
| \* Modification History | ||
| \* Last modified Fri May 22 17:19:49 CEST 2020 by ilinastoilkovska | ||
| \* Created Tue Apr 07 16:58:02 CEST 2020 by ilinastoilkovska |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,111 @@ | ||
| -------------------------- MODULE ClientHandlers --------------------------- | ||
|
|
||
| (*************************************************************************** | ||
| This module contains definitions of operators that are used to handle | ||
| client datagrams | ||
| ***************************************************************************) | ||
|
|
||
| EXTENDS Naturals, FiniteSets | ||
|
|
||
| CONSTANTS MaxHeight \* maximal height of all the chains in the system | ||
|
|
||
| ClientIDs == {"clA", "clB"} | ||
| nullClientID == "none" | ||
| nullHeight == 0 | ||
|
|
||
| Heights == 1..MaxHeight | ||
|
|
||
| Max(S) == CHOOSE x \in S: \A y \in S: y <= x | ||
|
|
||
| (*************************************************************************** | ||
| Client helper operators | ||
| ***************************************************************************) | ||
|
|
||
| \* get the ID of chainID's counterparty chain | ||
| GetCounterpartyChainID(chainID) == | ||
| IF chainID = "chainA" THEN "chainB" ELSE "chainA" | ||
|
|
||
| \* get the client ID of the client for chainID | ||
| GetClientID(chainID) == | ||
| IF chainID = "chainA" THEN "clA" ELSE "clB" | ||
|
|
||
| \* get the client ID of the client for chainID's counterparty chain | ||
| GetCounterpartyClientID(chainID) == | ||
| IF chainID = "chainA" THEN "clB" ELSE "clA" | ||
|
|
||
|
|
||
| (*************************************************************************** | ||
| Client datagram handlers | ||
| ***************************************************************************) | ||
|
|
||
| \* client heights: | ||
| \* good version: add all client heights from datagrams to counterpartyClientHeights | ||
| \* bad version: add only Max of client heights from datagrams to counterpartyClientHeights | ||
| \* if Max > Max(counterpartyClientHeights) | ||
|
|
||
| \* Handle "CreateClient" datagrams | ||
| HandleCreateClient(chainID, chain, datagrams) == | ||
| \* get "CreateClient" datagrams with valid clientID | ||
| LET createClientDgrs == {dgr \in datagrams : | ||
| /\ dgr.type = "CreateClient" | ||
| /\ dgr.clientID = GetCounterpartyClientID(chainID)} IN | ||
| \* get heights in datagrams with correct counterparty clientID for chainID | ||
| LET createClientHeights == {h \in Heights : \E dgr \in createClientDgrs : dgr.height = h} IN | ||
|
|
||
| \* new chain record with clients created | ||
| LET clientCreateChain == [ | ||
| height |-> chain.height, | ||
| counterpartyClientHeights |-> | ||
| \* if set of counterparty client heights is not empty | ||
| IF chain.counterpartyClientHeights /= {} | ||
| \* then discard CreateClient datagrams | ||
| THEN chain.counterpartyClientHeights | ||
| \* otherwise, if set of heights from datagrams is not empty | ||
| ELSE IF createClientHeights /= {} | ||
| \* then create counterparty client with height Max(createClientHeights) | ||
| THEN {Max(createClientHeights)} | ||
| \* otherwise, do not create client (as chain.counterpartyClientHeight = {}) | ||
| ELSE chain.counterpartyClientHeights, | ||
| connectionEnd |-> chain.connectionEnd | ||
| ] IN | ||
|
|
||
| clientCreateChain | ||
|
|
||
| \* Handle "ClientUpdate" datagrams | ||
| HandleUpdateClient(chainID, chain, datagrams) == | ||
| \* max client height of chain | ||
| LET maxClientHeight == IF chain.counterpartyClientHeights /= {} | ||
| THEN Max(chain.counterpartyClientHeights) | ||
| ELSE 0 IN | ||
| \* get "ClientUpdate" datagrams with valid clientID | ||
| LET updateClientDgrs == {dgr \in datagrams : | ||
| /\ dgr.type = "ClientUpdate" | ||
| /\ dgr.clientID = GetCounterpartyClientID(chainID) | ||
| /\ maxClientHeight < dgr.height} IN | ||
| \* get heights in datagrams with correct counterparty clientID for chainID | ||
| LET updateClientHeights == {h \in Heights : \E dgr \in updateClientDgrs : dgr.height = h} IN | ||
|
|
||
| \* new chain record with clients updated | ||
| LET clientUpdatedChain == [ | ||
| height |-> chain.height, | ||
| counterpartyClientHeights |-> | ||
| \* if set of counterparty client heights is empty | ||
| IF chain.counterpartyClientHeights = {} | ||
| \* then discard ClientUpdate datagrams | ||
| THEN chain.counterpartyClientHeights | ||
| \* otherwise, if set of heights from datagrams is not empty | ||
| ELSE IF updateClientHeights /= {} | ||
| \* then update counterparty client heights with updateClientHeights | ||
| THEN chain.counterpartyClientHeights \union updateClientHeights | ||
| \* otherwise, do not update client heights | ||
| ELSE chain.counterpartyClientHeights, | ||
| connectionEnd |-> chain.connectionEnd | ||
| ] IN | ||
|
|
||
| clientUpdatedChain | ||
|
|
||
|
|
||
| ============================================================================= | ||
| \* Modification History | ||
| \* Last modified Tue May 26 11:30:26 CEST 2020 by ilinastoilkovska | ||
| \* Created Tue Apr 07 16:42:47 CEST 2020 by ilinastoilkovska |
Oops, something went wrong.