From 73679c6af87a21f515e1a138946afea864ef43e3 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Fri, 10 Jul 2020 16:39:07 +0200 Subject: [PATCH] removed relayer-old and added support for channel closing handshake --- docs/spec/relayer-old/ChannelHandlers.tla | 172 ----- docs/spec/relayer-old/ClientHandlers.tla | 111 --- docs/spec/relayer-old/ConnectionHandlers.tla | 168 ----- docs/spec/relayer-old/Environment.tla | 350 --------- docs/spec/relayer-old/README.md | 26 - docs/spec/relayer-old/Relayer.tla | 744 ------------------- docs/spec/relayer/Chain.tla | 9 +- docs/spec/relayer/ChannelHandlers.tla | 59 +- docs/spec/relayer/ClientHandlers.tla | 4 +- docs/spec/relayer/ICS18Environment.tla | 86 ++- docs/spec/relayer/Relayer.tla | 29 +- docs/spec/relayer/RelayerDefinitions.tla | 11 +- 12 files changed, 169 insertions(+), 1600 deletions(-) delete mode 100644 docs/spec/relayer-old/ChannelHandlers.tla delete mode 100644 docs/spec/relayer-old/ClientHandlers.tla delete mode 100644 docs/spec/relayer-old/ConnectionHandlers.tla delete mode 100644 docs/spec/relayer-old/Environment.tla delete mode 100644 docs/spec/relayer-old/README.md delete mode 100644 docs/spec/relayer-old/Relayer.tla diff --git a/docs/spec/relayer-old/ChannelHandlers.tla b/docs/spec/relayer-old/ChannelHandlers.tla deleted file mode 100644 index c0ea6ffd41..0000000000 --- a/docs/spec/relayer-old/ChannelHandlers.tla +++ /dev/null @@ -1,172 +0,0 @@ --------------------------- 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 diff --git a/docs/spec/relayer-old/ClientHandlers.tla b/docs/spec/relayer-old/ClientHandlers.tla deleted file mode 100644 index 9395283245..0000000000 --- a/docs/spec/relayer-old/ClientHandlers.tla +++ /dev/null @@ -1,111 +0,0 @@ --------------------------- 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 diff --git a/docs/spec/relayer-old/ConnectionHandlers.tla b/docs/spec/relayer-old/ConnectionHandlers.tla deleted file mode 100644 index 6c4a6a546c..0000000000 --- a/docs/spec/relayer-old/ConnectionHandlers.tla +++ /dev/null @@ -1,168 +0,0 @@ -------------------------- MODULE ConnectionHandlers ------------------------- - -(*************************************************************************** - This module contains definitions of operators that are used to handle - connection datagrams - ***************************************************************************) - -EXTENDS Naturals, FiniteSets - -ConnectionIDs == {"connAtoB", "connBtoA"} -nullConnectionID == "none" - -ConnectionStates == {"UNINIT", "INIT", "TRYOPEN", "OPEN"} - -(*************************************************************************** - Connection helper operators - ***************************************************************************) - -\* get the connection ID of the connection end at chainID -GetConnectionID(chainID) == - IF chainID = "chainA" - THEN "connAtoB" - ELSE IF chainID = "chainB" - THEN "connBtoA" - ELSE nullConnectionID - -\* get the connection ID of the connection end at chainID's counterparty chain -GetCounterpartyConnectionID(chainID) == - IF chainID = "chainA" - THEN "connBtoA" - ELSE IF chainID = "chainB" - THEN "connAtoB" - ELSE nullConnectionID - -(*************************************************************************** - Connection datagram handlers - ***************************************************************************) - -\* Handle "ConnOpenInit" datagrams -HandleConnOpenInit(chainID, chain, datagrams) == - \* get "ConnOpenInit" datagrams, with a valid connection ID - LET connOpenInitDgrs == {dgr \in datagrams : - /\ dgr.type = "ConnOpenInit" - /\ dgr.connectionID = GetConnectionID(chainID)} IN - - \* if there are valid "ConnOpenInit" datagrams, create a new connection end and update the chain - IF connOpenInitDgrs /= {} /\ chain.connectionEnd.state = "UNINIT" - THEN LET connOpenInitDgr == CHOOSE dgr \in connOpenInitDgrs : TRUE IN - LET connOpenInitConnectionEnd == [ - state |-> "INIT", - connectionID |-> connOpenInitDgr.connectionID, - clientID |-> connOpenInitDgr.clientID, - counterpartyConnectionID |-> connOpenInitDgr.counterpartyConnectionID, - counterpartyClientID |-> connOpenInitDgr.counterpartyClientID, - channelEnd |-> chain.connectionEnd.channelEnd - ] IN - LET connOpenInitChain == [ - chain EXCEPT !.connectionEnd = connOpenInitConnectionEnd - ] IN - - connOpenInitChain - \* otherwise, do not update the chain - ELSE chain - - -\* Handle "ConnOpenTry" datagrams -HandleConnOpenTry(chainID, chain, datagrams) == - \* get "ConnOpenTry" datagrams, with a valid connection ID and valid height - LET connOpenTryDgrs == {dgr \in datagrams : - /\ dgr.type = "ConnOpenTry" - /\ dgr.desiredConnectionID = GetConnectionID(chainID) - /\ dgr.consensusHeight <= chain.height - /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN - - IF connOpenTryDgrs /= {} - \* if there are valid "ConnOpenTry" datagrams, update the connection end - THEN LET connOpenTryDgr == CHOOSE dgr \in connOpenTryDgrs : TRUE IN - LET connOpenTryConnectionEnd == [ - state |-> "TRYOPEN", - connectionID |-> connOpenTryDgr.desiredConnectionID, - clientID |-> connOpenTryDgr.clientID, - counterpartyConnectionID |-> connOpenTryDgr.counterpartyConnectionID, - counterpartyClientID |-> connOpenTryDgr.counterpartyClientID, - channelEnd |-> chain.connectionEnd.channelEnd - ] IN - - IF \/ chain.connectionEnd.state = "UNINIT" - \/ /\ chain.connectionEnd.state = "INIT" - /\ chain.connectionEnd.counterpartyConnectionID - = connOpenTryConnectionEnd.counterpartyConnectionID - /\ chain.connectionEnd.clientID - = connOpenTryConnectionEnd.clientID - /\ chain.connectionEnd.counterpartyClientID - = connOpenTryConnectionEnd.counterpartyClientID - \* if the connection end on the chain is in "UNINIT" or it is in "INIT", - \* but the fields are the same as in the datagram, update the connection end - THEN LET connOpenTryChain == [ - chain EXCEPT !.connectionEnd = connOpenTryConnectionEnd - ] IN - - connOpenTryChain - \* otherwise, do not update the chain - ELSE chain - \* otherwise, do not update the chain - ELSE chain - - -\* Handle "ConnOpenAck" datagrams -HandleConnOpenAck(chainID, chain, datagrams) == - \* get "ConnOpenAck" datagrams, with a valid connection ID and valid height - LET connOpenAckDgrs == {dgr \in datagrams : - /\ dgr.type = "ConnOpenAck" - /\ dgr.connectionID = GetConnectionID(chainID) - /\ dgr.consensusHeight <= chain.height - /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN - - IF connOpenAckDgrs /= {} - \* if there are valid "ConnOpenAck" datagrams, update the connection end - THEN IF \/ chain.connectionEnd.state = "INIT" - \/ chain.connectionEnd.state = "TRYOPEN" - \* if the connection end on the chain is in "INIT" or it is in "TRYOPEN", - \* update the connection end - THEN LET connOpenAckDgr == CHOOSE dgr \in connOpenAckDgrs : TRUE IN - LET connOpenAckConnectionEnd == [ - chain.connectionEnd EXCEPT !.state = "OPEN", - !.connectionID = connOpenAckDgr.connectionID - ] IN - LET connOpenAckChain == [ - chain EXCEPT !.connectionEnd = connOpenAckConnectionEnd - ] IN - - connOpenAckChain - \* otherwise, do not update the chain - ELSE chain - \* otherwise, do not update the chain - ELSE chain - -\* Handle "ConnOpenConfirm" datagrams -HandleConnOpenConfirm(chainID, chain, datagrams) == - \* get "ConnOpenConfirm" datagrams, with a valid connection ID and valid height - LET connOpenConfirmDgrs == {dgr \in datagrams : - /\ dgr.type = "ConnOpenConfirm" - /\ dgr.connectionID = GetConnectionID(chainID) - /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN - - IF connOpenConfirmDgrs /= {} - \* if there are valid "connOpenConfirmDgrs" datagrams, update the connection end - THEN IF chain.connectionEnd.state = "TRYOPEN" - \* if the connection end on the chain is in "TRYOPEN", update the connection end - THEN LET connOpenConfirmDgr == CHOOSE dgr \in connOpenConfirmDgrs : TRUE IN - LET connOpenConfirmConnectionEnd == [ - chain.connectionEnd EXCEPT !.state = "OPEN", - !.connectionID = connOpenConfirmDgr.connectionID - ] IN - LET connOpenConfirmChain == [ - chain EXCEPT !.connectionEnd = connOpenConfirmConnectionEnd - ] IN - - connOpenConfirmChain - \* otherwise, do not update the chain - ELSE chain - \* otherwise, do not update the chain - ELSE chain - -============================================================================= -\* Modification History -\* Last modified Fri May 22 17:20:00 CEST 2020 by ilinastoilkovska -\* Created Tue Apr 07 16:09:26 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/relayer-old/Environment.tla b/docs/spec/relayer-old/Environment.tla deleted file mode 100644 index da33e5c04a..0000000000 --- a/docs/spec/relayer-old/Environment.tla +++ /dev/null @@ -1,350 +0,0 @@ ----------------------------- MODULE Environment ---------------------------- - -(*************************************************************************** - This module captures the chain logic. It extends the modules ClientHandlers, - ConnectionHandlers, and ChannelHandlers, which contain definitions of - operators that handle the client, connection, and channel datagrams, - respectively. - ***************************************************************************) - -EXTENDS Naturals, FiniteSets, ClientHandlers, ConnectionHandlers, ChannelHandlers - -VARIABLES chains, \* a function that assigns a chain record to each chainID - incomingDatagrams \* a function that assigns a set of incoming datagrams - \* incoming from the relayer to each chainID - -vars == <> - -ChainIDs == {"chainA", "chainB"} - -(******************************* ChannelEnds ******************************* - A set of channel end records. - A channel end record contains the following fields: - - - state -- a string - Stores the current state of this channel end. It has one of the - following values: "UNINIT", "INIT", "TRYOPEN", "OPEN", "CLOSED". - - - channelID -- a channel identifier - Stores the channel identifier of this channel end. - - - counterpartyChannelID -- a channel identifier - Stores the channel identifier of the counterparty channel end. - - (** ignoring channel ordering for now **) - ***************************************************************************) -ChannelEnds == - [ - state : ChannelStates, - channelID : ChannelIDs \union {nullChannelID}, - counterpartyChannelID : ChannelIDs \union {nullChannelID} - ] - -(***************************** ConnectionEnds ***************************** - A set of connection end records. - A connection end record contains the following fields: - - - state -- a string - Stores the current state of this connection end. It has one of the - following values: "UNINIT", "INIT", "TRYOPEN", "OPEN". - - - connectionID -- a connection identifier - Stores the connection identifier of this connection end. - - - counterpartyConnectionID -- a connection identifier - Stores the connection identifier of the counterparty connection end. - - - clientID -- a client identifier - Stores the client identifier associated with this connection end. - - - counterpartyClientID -- a client identifier - Stores the counterparty client identifier associated with this connection end. - ***************************************************************************) -ConnectionEnds == - [ - state : ConnectionStates, - connectionID : ConnectionIDs \union {nullConnectionID}, - clientID : ClientIDs \union {nullClientID}, - counterpartyConnectionID : ConnectionIDs \union {nullConnectionID}, - counterpartyClientID : ClientIDs \union {nullClientID}, - channelEnd : ChannelEnds - ] - -(********************************** Chains ********************************* - A set of chain records. - A chain record contains the following fields: - - - height : an integer between nullHeight and MaxHeight. - Stores the current height of the chain. - - - counterpartyClientHeights : a set of integers between 1 and MaxHeight - Stores the heights of the client for the counterparty chain. - - - connectionEnd : a connection end record - Stores data about the connection with the counterparty chain - ***************************************************************************) -Chains == - [ - height : Heights \union {nullHeight}, - counterpartyClientHeights : SUBSET(Heights), - connectionEnd : ConnectionEnds - ] - -(******************************** Datagrams ******************************** - A set of datagrams. - ***************************************************************************) -Datagrams == - [type : {"CreateClient"}, clientID : ClientIDs, height : Heights] - \union - [type : {"ClientUpdate"}, clientID : ClientIDs, height : Heights] - \union - [type : {"ConnOpenInit"}, connectionID : ConnectionIDs, clientID : ClientIDs, - counterpartyConnectionID : ConnectionIDs, counterpartyClientID : ClientIDs] - \union - [type : {"ConnOpenTry"}, desiredConnectionID : ConnectionIDs, - counterpartyConnectionID : ConnectionIDs, counterpartyClientID : ClientIDs, - clientID : ClientIDs, proofHeight : Heights, consensusHeight : Heights] - \union - [type : {"ConnOpenAck"}, connectionID : ConnectionIDs, proofHeight : Heights, - consensusHeight : Heights ] - \union - [type : {"ConnOpenConfirm"}, connectionID : ConnectionIDs, proofHeight : Heights] - \union - [type : {"ChanOpenInit"}, channelID : ChannelIDs, counterpartyChannelID : ChannelIDs] - \union - [type : {"ChanOpenTry"}, channelID : ChannelIDs, counterpartyChannelID : ChannelIDs, - proofHeight : Heights] - \union - [type : {"ChanOpenAck"}, channelID : ChannelIDs, proofHeight : Heights] - \union - [type : {"ChanOpenConfirm"}, channelID : ChannelIDs, proofHeight : Heights] - -(*************************************************************************** - Chain helper operators - ***************************************************************************) -\* get the latest height of chainID -GetLatestHeight(chainID) == - chains[chainID].height - -\* get the maximal height of the client for chainID's counterparty chain -GetMaxCounterpartyClientHeight(chainID) == - IF chains[chainID].counterpartyClientHeights /= {} - THEN Max(chains[chainID].counterpartyClientHeights) - ELSE nullHeight - -\* get the set of heights of the client for chainID's counterparty chain -GetCounterpartyClientHeights(chainID) == - chains[chainID].counterpartyClientHeights - -\* returns true if the counterparty client is initialized on chainID -IsCounterpartyClientOnChain(chainID) == - chains[chainID].counterpartyClientHeights /= {} - -\* returns true if the counterparty client height on chainID is greater or equal than h -CounterpartyClientHeightUpdated(chainID, h) == - h \in chains[chainID].counterpartyClientHeights - -\* get the connection end at chainID -GetConnectionEnd(chainID) == - chains[chainID].connectionEnd - -\* returns true if the connection end on chainID is UNINIT -IsConnectionUninit(chainID) == - chains[chainID].connectionEnd.state = "UNINIT" - -\* returns true if the connection end on chainID is INIT -IsConnectionInit(chainID) == - chains[chainID].connectionEnd.state = "INIT" - -\* returns true if the connection end on chainID is TRYOPEN -IsConnectionTryopen(chainID) == - chains[chainID].connectionEnd.state = "TRYOPEN" - -\* returns true if the connection end on chainID is OPEN -IsConnectionOpen(chainID) == - chains[chainID].connectionEnd.state = "OPEN" - -\* get the channel end at the connection end of chainID -GetChannelEnd(chainID) == - chains[chainID].connectionEnd.channelEnd - -\* returns true if the channel end on chainID is UNINIT -IsChannelUninit(chainID) == - chains[chainID].connectionEnd.channelEnd.state = "UNINIT" - -\* returns true if the channel end on chainID is INIT -IsChannelInit(chainID) == - chains[chainID].connectionEnd.channelEnd.state = "INIT" - -\* returns true if the channel end on chainID is TRYOPEN -IsChannelTryopen(chainID) == - chains[chainID].connectionEnd.channelEnd.state = "TRYOPEN" - -\* returns true if the channel end on chainID is OPEN -IsChannelOpen(chainID) == - chains[chainID].connectionEnd.channelEnd.state = "OPEN" - -(*************************************************************************** - Client update operators - ***************************************************************************) -\* Update the clients on chain with chainID, -\* using the client datagrams generated by the relayer -LightClientUpdate(chainID, chain, datagrams) == - \* create clients - LET clientCreatedChain == HandleCreateClient(chainID, chain, datagrams) IN - \* update clients - LET clientUpdatedChain == HandleUpdateClient(chainID, clientCreatedChain, datagrams) IN - - clientUpdatedChain - -(*************************************************************************** - Connection update operators - ***************************************************************************) -\* Update the connections on chain with chainID, -\* using the connection datagrams generated by the relayer -ConnectionUpdate(chainID, chain, datagrams) == - \* update chain with "ConnOpenInit" datagrams - LET connOpenInitChain == HandleConnOpenInit(chainID, chain, datagrams) IN - \* update chain with "ConnOpenTry" datagrams - LET connOpenTryChain == HandleConnOpenTry(chainID, connOpenInitChain, datagrams) IN - \* update chain with "ConnOpenAck" datagrams - LET connOpenAckChain == HandleConnOpenAck(chainID, connOpenTryChain, datagrams) IN - \* update chain with "ConnOpenConfirm" datagrams - LET connOpenConfirmChain == HandleConnOpenConfirm(chainID, connOpenAckChain, datagrams) IN - - connOpenConfirmChain - -(*************************************************************************** - Channel update operators - ***************************************************************************) -\* Update the channels on chain with chainID, -\* using the channel datagrams generated by the relayer -ChannelUpdate(chainID, chain, datagrams) == - \* update chain with "ChanOpenInit" datagrams - LET chanOpenInitChain == HandleChanOpenInit(chainID, chain, datagrams) IN - \* update chain with "ChanOpenTry" datagrams - LET chanOpenTryChain == HandleChanOpenTry(chainID, chanOpenInitChain, datagrams) IN - \* update chain with "ChanOpenAck" datagrams - LET chanOpenAckChain == HandleChanOpenAck(chainID, chanOpenTryChain, datagrams) IN - \* update chain with "ChanOpenConfirm" datagrams - LET chanOpenConfirmChain == HandleChanOpenConfirm(chainID, chanOpenAckChain, datagrams) IN - - chanOpenConfirmChain - -(*************************************************************************** - Chain update operators - ***************************************************************************) -\* Update chainID with the received datagrams -\* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels). -UpdateChain(chainID, datagrams) == - LET chain == chains[chainID] IN - \* ICS 002: Client updates - LET lightClientsUpdated == LightClientUpdate(chainID, chain, datagrams) IN - \* ICS 003: Connection updates - LET connectionsUpdated == ConnectionUpdate(chainID, lightClientsUpdated, datagrams) IN - \* ICS 004: Channel updates - LET channelsUpdated == ChannelUpdate(chainID, connectionsUpdated, datagrams) IN - - \* update height - LET updatedChain == - IF /\ chain /= channelsUpdated - /\ chain.height < MaxHeight - THEN [channelsUpdated EXCEPT !.height = chain.height + 1] - ELSE channelsUpdated - IN - - updatedChain - -(*************************************************************************** - Chain actions - ***************************************************************************) -\* Advance the height of the chain until MaxHeight is reached -AdvanceChain(chainID) == - /\ chains[chainID].height < MaxHeight - /\ chains' = [chains EXCEPT - ![chainID].height = chains[chainID].height + 1 - ] - /\ UNCHANGED incomingDatagrams - -\* Receive the datagrams and update the chain state -ReceiveIncomingDatagrams(chainID) == - /\ incomingDatagrams[chainID] /= {} - /\ chains' = [chains EXCEPT - ![chainID] = UpdateChain(chainID, incomingDatagrams[chainID]) - ] - /\ incomingDatagrams' = [incomingDatagrams EXCEPT - ![chainID] = {} - ] - -(*************************************************************************** - Initial values of a channel end, connection end, chain - ***************************************************************************) -\* Initial value of a channel end: -\* - state is "UNINIT" -\* - channelID, counterpartyChannelID are uninitialized -InitChannelEnd == - [state |-> "UNINIT", - channelID |-> nullChannelID, - counterpartyChannelID |-> nullChannelID] - -\* Initial value of a connection end: -\* - state is "UNINIT" -\* - connectionID, counterpartyConnectionID are uninitialized -\* - clientID, counterpartyClientID are uninitialized -InitConnectionEnd == - [state |-> "UNINIT", - connectionID |-> nullConnectionID, - clientID |-> nullClientID, - counterpartyConnectionID |-> nullConnectionID, - counterpartyClientID |-> nullClientID, - channelEnd |-> InitChannelEnd] - -\* Initial value of the chain: -\* - height is initialized to 1 -\* - the counterparty light client is uninitialized -\* - the connection end is initialized to InitConnectionEnd -InitChain == - [height |-> 1, - counterpartyClientHeights |-> {}, - connectionEnd |-> InitConnectionEnd] - -(*************************************************************************** - Specification - ***************************************************************************) -\* Initial state predicate -\* Initially -\* - each chain is initialized to InitChain -\* - pendingDatagrams for each chain is empty -Init == - /\ chains = [chainID \in ChainIDs |-> InitChain] - /\ incomingDatagrams = [chainID \in ChainIDs |-> {}] - -\* Next state action -\* One of the chains either -\* - advances its height -\* - receives datagrams and updates its state -Next == - \E chainID \in ChainIDs : - \/ AdvanceChain(chainID) - \/ ReceiveIncomingDatagrams(chainID) - \/ UNCHANGED vars - - -\* Fairness constraints -Fairness == - \* ensure all chains take steps - /\ \A chainID \in ChainIDs : WF_vars(AdvanceChain(chainID)) - /\ \A chainID \in ChainIDs : WF_vars(ReceiveIncomingDatagrams(chainID)) - -(*************************************************************************** - Invariants - ***************************************************************************) -\* Type invariant -TypeOK == - /\ chains \in [ChainIDs -> Chains] - /\ incomingDatagrams \in [ChainIDs -> SUBSET Datagrams] - -============================================================================= -\* Modification History -\* Last modified Tue May 26 12:38:40 CEST 2020 by ilinastoilkovska -\* Created Fri Mar 13 19:48:22 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer-old/README.md b/docs/spec/relayer-old/README.md deleted file mode 100644 index 358a23a271..0000000000 --- a/docs/spec/relayer-old/README.md +++ /dev/null @@ -1,26 +0,0 @@ -A TLA+ specification of the Relayer algorithm. - -The specification has five modules: - - `Relayer.tla` (the main module) - - `Environment.tla` - - `ClientHandlers.tla` - - `ConnectionHandlers.tla` - - `ChannelHandlers.tla` - -The module `Relayer.tla` contains the specification of the relayer algorithm. -It instantiates the module `Environment.tla`, which takes care of the chain logic. -The module `Environment.tla` extends the modules `ClientHandlers.tla`, -`ConnectionHandlers.tla`, and `ChannelHandlers.tla`, which contain definition of -operators that handle client, connection handshake, and channel handshake -datagrams, respectively. - -To import the specification in the TLA+ toolbox and run TLC: - - add the spec `Relayer.tla` in TLA+ toolbox - - add `Environment.tla`, `ClientHandlers.tla`, `ConnectionHandlers.tla`, and - `ChannelHandlers.tla` as modules in the spec - - create a model - - assign a value to the constant `MaxHeight` - - choose "Temporal formula" as the behavior spec, and use the formula `Spec` - - add the invariant `Inv` (a conjunction of all the defined invariants) - - add the property `Prop` (a conjunction of all the defined properties) - - run TLC on the model diff --git a/docs/spec/relayer-old/Relayer.tla b/docs/spec/relayer-old/Relayer.tla deleted file mode 100644 index 12c9df8f5e..0000000000 --- a/docs/spec/relayer-old/Relayer.tla +++ /dev/null @@ -1,744 +0,0 @@ ------------------------------- MODULE Relayer ------------------------------ - -(*************************************************************************** - This module contains the specification of the relayer algorithm. - It instantiates the module Environment, which takes care of the chain logic. - ***************************************************************************) - -EXTENDS Naturals, FiniteSets - -CONSTANTS MaxHeight \* maximal height of all the chains in the system - -VARIABLES chains, \* a function that assigns a chain record to each chainID - outgoingDatagrams, \* a function that assigns a set of pending datagrams - \* outgoing from the relayer to each chainID - relayerChainHeights, \* a function that assigns a height to each chainID - turn - -vars == <> -specVars == <> -envVars == <> - -\* Instance of the module Environment, which encodes the chain logic -Env == INSTANCE Environment - WITH chains <- chains, - incomingDatagrams <- outgoingDatagrams, - MaxHeight <- MaxHeight - -ChainIDs == Env!ChainIDs -ClientIDs == Env!ClientIDs -ConnectionIDs == Env!ConnectionIDs -ChannelIDs == Env!ChannelIDs -Heights == Env!Heights -RelayerClientIDs == Env!ClientIDs - -nullClientID == Env!nullClientID -nullConnectionID == Env!nullConnectionID -nullHeight == Env!nullHeight - -(******************************** Datagrams ******************************** - A set of datagrams. - ***************************************************************************) -Datagrams == Env!Datagrams - -(*************************************************************************** - Chain helper operators - ***************************************************************************) -\* get the latest height of chainID -GetLatestHeight(chainID) == Env!GetLatestHeight(chainID) - -\* get the height of the client for chainID's counterparty chain -GetMaxCounterpartyClientHeight(chainID) == Env!GetMaxCounterpartyClientHeight(chainID) - -\* get the set of heights of the client for chainID's counterparty chain -GetCounterpartyClientHeights(chainID) == Env!GetCounterpartyClientHeights(chainID) - -\* get the ID of chainID's counterparty chain -GetCounterpartyChainID(chainID) == Env!GetCounterpartyChainID(chainID) - -\* get the client ID of the client for chainID -GetClientID(chainID) == Env!GetClientID(chainID) - -\* get the client ID of the client for chainID's counterparty chain -GetCounterpartyClientID(chainID) == Env!GetCounterpartyClientID(chainID) - -\* returns true if the counterparty client is initialized on chainID -IsCounterpartyClientOnChain(chainID) == Env!IsCounterpartyClientOnChain(chainID) - -\* returns true if the counterparty client height on chainID is greater or equal than h -CounterpartyClientHeightUpdated(chainID, h) == Env!CounterpartyClientHeightUpdated(chainID, h) - -\* get the connection ID of the connection end at chainID -GetConnectionID(chainID) == Env!GetConnectionID(chainID) - -\* get the connection ID of the connection end at chainID's counterparty chain -GetCounterpartyConnectionID(chainID) == Env!GetCounterpartyConnectionID(chainID) - -\* get the connection end at chainID -GetConnectionEnd(chainID) == Env!GetConnectionEnd(chainID) - -\* returns true if the connection end on chainID is UNINIT -IsConnectionUninit(chainID) == Env!IsConnectionUninit(chainID) - -\* returns true if the connection end on chainID is INIT -IsConnectionInit(chainID) == Env!IsConnectionInit(chainID) - -\* returns true if the connection end on chainID is TRYOPEN -IsConnectionTryopen(chainID) == Env!IsConnectionTryopen(chainID) - -\* returns true if the connection end on chainID is OPEN -IsConnectionOpen(chainID) == Env!IsConnectionOpen(chainID) - -\* get the channel ID of the channel end at the connection end of chainID -GetChannelID(chainID) == Env!GetChannelID(chainID) - -\* get the channel ID of the channel end at chainID's counterparty chain -GetCounterpartyChannelID(chainID) == Env!GetCounterpartyChannelID(chainID) - -\* get the channel end at the connection end of chainID -GetChannelEnd(chainID) == Env!GetChannelEnd(chainID) - -\* returns true if the channel end on chainID is UNINIT -IsChannelUninit(chainID) == Env!IsChannelUninit(chainID) - -\* returns true if the channel end on chainID is INIT -IsChannelInit(chainID) == Env!IsChannelInit(chainID) - -\* returns true if the channel end on chainID is TRYOPEN -IsChannelTryopen(chainID) == Env!IsChannelTryopen(chainID) - -\* returns true if the channel end on chainID is OPEN -IsChannelOpen(chainID) == Env!IsChannelOpen(chainID) - -(*************************************************************************** - Client datagrams - ***************************************************************************) -\* Compute client datagrams designated for dstChainID. -\* These are used to update the client for srcChainID on dstChainID in the environment. -\* Some client updates might trigger an update of the height that -\* the relayer stores for srcChainID -LightClientUpdates(srcChainID, dstChainID, relayer) == - LET srcChainHeight == GetLatestHeight(srcChainID) IN - LET srcClientHeight == GetMaxCounterpartyClientHeight(dstChainID) IN - LET srcClientID == GetClientID(srcChainID) IN - - \* check if the relayer chain height for srcChainID should be updated - LET srcRelayerChainHeight == - IF relayer[srcChainID] < srcChainHeight - THEN srcChainHeight - ELSE relayer[srcChainID] IN - - \* create an updated relayer - LET updatedRelayer == - [relayer EXCEPT ![srcChainID] = srcRelayerChainHeight] IN - - \* generate datagrams for dstChainID - LET dstDatagrams == - IF srcClientHeight = nullHeight - THEN \* the src client does not exist on dstChainID - {[type |-> "CreateClient", - height |-> srcChainHeight, - clientID |-> srcClientID]} - ELSE \* the src client exists on dstChainID - IF srcClientHeight < srcChainHeight - THEN \* the height of the src client on dstChainID is smaller than the height of the src chain - {[type |-> "ClientUpdate", - height |-> srcChainHeight, - clientID |-> srcClientID]} - ELSE {} IN - - [datagrams|-> dstDatagrams, relayerUpdate |-> updatedRelayer] - -(*************************************************************************** - Connection datagrams - ***************************************************************************) -\* Compute connection datagrams designated for dstChainID. -\* These are used to update the connection end on dstChainID in the environment. -ConnectionDatagrams(srcChainID, dstChainID) == - LET srcConnectionEnd == GetConnectionEnd(srcChainID) IN - LET dstConnectionEnd == GetConnectionEnd(dstChainID) IN - - LET srcConnectionID == GetConnectionID(srcChainID) IN - LET dstConnectionID == GetConnectionID(dstChainID) IN - - LET srcHeight == GetLatestHeight(srcChainID) IN - LET srcConsensusHeight == GetMaxCounterpartyClientHeight(srcChainID) IN - - IF dstConnectionEnd.state = "UNINIT" /\ srcConnectionEnd.state = "UNINIT" THEN - {[type |-> "ConnOpenInit", - connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - clientID |-> GetCounterpartyClientID(dstChainID), \* "clA" - counterpartyConnectionID |-> srcConnectionID, \* "connAtoB" - counterpartyClientID |-> GetCounterpartyClientID(srcChainID)]} \* "clB" - - ELSE IF srcConnectionEnd.state = "INIT" /\ \/ dstConnectionEnd.state = "UNINIT" - \/ dstConnectionEnd.state = "INIT" THEN - {[type |-> "ConnOpenTry", - desiredConnectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - clientID |-> srcConnectionEnd.counterpartyClientID, \* "clA" - counterpartyConnectionID |-> srcConnectionID, \* "connAtoB" - counterpartyClientID |-> srcConnectionEnd.clientID, \* "clB" - proofHeight |-> srcHeight, - consensusHeight |-> srcConsensusHeight]} - - ELSE IF srcConnectionEnd.state = "TRYOPEN" /\ \/ dstConnectionEnd.state = "INIT" - \/ dstConnectionEnd.state = "TRYOPEN" THEN - {[type |-> "ConnOpenAck", - connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight, - consensusHeight |-> srcConsensusHeight]} - - ELSE IF srcConnectionEnd.state = "OPEN" /\ dstConnectionEnd.state = "TRYOPEN" THEN - {[type |-> "ConnOpenConfirm", - connectionID |-> dstConnectionEnd.connectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight]} - ELSE {} - -(*************************************************************************** - Channel datagrams - ***************************************************************************) -\* Compute channel datagrams designated for dstChainID. -\* These are used to update the channel end on dstChainID in the environment. -ChannelDatagrams(srcChainID, dstChainID) == - LET srcChannelEnd == GetChannelEnd(srcChainID) IN - LET dstChannelEnd == GetChannelEnd(dstChainID) IN - - LET srcChannelID == GetChannelID(srcChainID) IN - LET dstChannelID == GetChannelID(dstChainID) IN - - LET srcHeight == GetLatestHeight(srcChainID) IN - - IF dstChannelEnd.state = "UNINIT" /\ srcChannelEnd.state = "UNINIT" THEN - {[type |-> "ChanOpenInit", - channelID |-> dstChannelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - counterpartyChannelID |-> srcChannelID]} \* "chanAtoB" - - ELSE IF srcChannelEnd.state = "INIT" /\ \/ dstChannelEnd.state = "UNINIT" - \/ dstChannelEnd.state = "INIT" THEN - {[type |-> "ChanOpenTry", - channelID |-> dstChannelID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - counterpartyChannelID |-> srcChannelID, \* "chanAtoB" - proofHeight |-> srcHeight]} - - ELSE IF srcChannelEnd.state = "TRYOPEN" /\ \/ dstChannelEnd.state = "INIT" - \/ dstChannelEnd.state = "TRYOPEN" THEN - {[type |-> "ChanOpenAck", - channelID |-> dstChannelID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight]} - - ELSE IF srcChannelEnd.state = "OPEN" /\ dstChannelEnd.state = "TRYOPEN" THEN - {[type |-> "ChanOpenConfirm", - channelID |-> dstChannelEnd.channelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight]} - ELSE {} - -(*************************************************************************** - Compute pending datagrams (from srcChainID to dstChainID) - ***************************************************************************) -\* Currently supporting: -\* - ICS 002: Client updates -\* - ICS 003: Connection handshake -\* - ICS 004: Channel handshake -\* TODO: Support the remaining datagrams -PendingDatagrams(srcChainID, dstChainID) == - \* ICS 002 : Clients - \* - Determine if light clients needs to be updated - LET clientDatagrams == LightClientUpdates(srcChainID, dstChainID, relayerChainHeights) IN - - \* ICS3 : Connections - \* - Determine if any connection handshakes are in progress - LET connectionDatagrams == ConnectionDatagrams(srcChainID, dstChainID) IN - - \* ICS4 : Channels & Packets - \* - Determine if any channel handshakes are in progress - LET channelDatagrams == ChannelDatagrams(srcChainID, dstChainID) IN - - \* ICS4 : Channels & Packets - \* - Determine if any packets, acknowledgements, or timeouts need to be relayed - \* TODO - - [datagrams |-> clientDatagrams.datagrams \union - connectionDatagrams \union - channelDatagrams, - relayerUpdate |-> clientDatagrams.relayerUpdate] - -(*************************************************************************** - Relayer actions - ***************************************************************************) -\* Update the height of the relayer client for some chainID -UpdateRelayerClients(chainID) == - /\ relayerChainHeights[chainID] < GetLatestHeight(chainID) - /\ relayerChainHeights' = [relayerChainHeights EXCEPT - ![chainID] = GetLatestHeight(chainID) - ] - /\ UNCHANGED <> - -\* for two chains, srcChainID and dstChainID, where srcChainID /= dstChainID, -\* create the pending datagrams and update the corresponding sets of pending datagrams -Relay(srcChainID, dstChainID) == - LET datagramsAndRelayerUpdate == PendingDatagrams(srcChainID, dstChainID) IN - /\ srcChainID /= dstChainID - /\ outgoingDatagrams' = - [outgoingDatagrams EXCEPT - ![dstChainID] = outgoingDatagrams[dstChainID] - \union - datagramsAndRelayerUpdate.datagrams - ] - /\ relayerChainHeights' = datagramsAndRelayerUpdate.relayerUpdate - /\ UNCHANGED chains - -(*************************************************************************** - Component actions - ***************************************************************************) -\* Relayer -\* The relayer either -\* - updates its clients, or -\* - relays datagrams between two chains, or -\* - does nothing -Relayer == - \/ \E chainID \in ChainIDs : UpdateRelayerClients(chainID) - \/ \E srcChainID \in ChainIDs : \E dstChainID \in ChainIDs : Relay(srcChainID, dstChainID) - \/ UNCHANGED vars - -\* Environment -\* The environment takes the action Env!Next -\* and leaves the relayer variable unchanged -Environment == - /\ Env!Next - /\ UNCHANGED relayerChainHeights - -(*************************************************************************** - Specification - ***************************************************************************) -\* Initial state predicate -\* Initially -\* - it is either the relayer's or the environment's turn -\* - the relayer chain heights are uninitialized -\* (i.e., their height is nullHeight) -\* - the environment is initialized, by Env!Init -Init == - /\ turn \in {"relayer", "environment"} - /\ relayerChainHeights = [chainID \in ChainIDs |-> nullHeight] - /\ Env!Init - -\* Next state action -\* The system consists of two components: relayer and environment. -\* In the system, the relayer and environment -\* take alternate steps -Next == - \/ /\ turn = "relayer" - /\ Relayer - /\ turn' = "environment" - \/ /\ turn = "environment" - /\ Environment - /\ turn' = "relayer" - -\* Fairness constraints -Fairness == - /\ \A chainID \in ChainIDs : - WF_specVars(UpdateRelayerClients(chainID)) - /\ \A srcChainID \in ChainIDs : \A dstChainID \in ChainIDs : - WF_specVars(Relay(srcChainID, dstChainID)) - /\ Env!Fairness - -\* Spec formula -Spec == Init /\ [][Next]_vars /\ Fairness - -(*************************************************************************** - Helper operators used in properties - ***************************************************************************) -\* returns true if there is a "CreateClient" datagram -\* in outgoing datagrams for chainID -IsCreateClientInPendingDatagrams(chainID, clID, h) == - [type |-> "CreateClient", clientID |-> clID, height |-> h] - \in outgoingDatagrams[chainID] - -\* returns true if there is a "ClientUpdate" datagram -\* in outgoing datagrams for chainID -IsClientUpdateInPendingDatagrams(chainID, clID, h) == - [type |-> "ClientUpdate", clientID |-> clID, height |-> h] - \in outgoingDatagrams[chainID] - -\* returns true if there is a "ConnOpenInit" datagram -\* for the connection between srcChainID and dstChainID -ConnOpenInitGenerated(srcChainID, dstChainID) == - LET srcClientID == GetClientID(dstChainID) IN - LET dstClientID == GetClientID(srcChainID) IN - LET srcConnectionID == GetConnectionID(srcChainID) IN - LET dstConnectionID == GetConnectionID(dstChainID) IN - - [type |-> "ConnOpenInit", - connectionID |-> srcConnectionID, - clientID |-> srcClientID, - counterpartyConnectionID |-> dstConnectionID, - counterpartyClientID |-> dstClientID] \in outgoingDatagrams[srcChainID] - -\* returns true if there is a "ConnOpenInit" datagram -\* in outgoing datagrams for chainID -IsConnOpenInitInPendingDatagrams( - chainID, clientID, counterpartyClientID, - connectionID, counterpartyConnectionID - ) == - - [type |-> "ConnOpenInit", - connectionID |-> connectionID, - clientID |-> clientID, - counterpartyConnectionID |-> counterpartyConnectionID, - counterpartyClientID |-> counterpartyClientID] \in outgoingDatagrams[chainID] - -\* returns true if there is a "ConnOpenTry" datagram -\* in outgoing datagrams for chainID -IsConnOpenTryInPendingDatagrams( - chainID, clientID, counterpartyClientID, - connectionID, counterpartyConnectionID - ) == - - \E pHeight \in Heights : \E cHeight \in Heights : - [type |-> "ConnOpenTry", - desiredConnectionID |-> connectionID, - clientID |-> clientID, - counterpartyConnectionID |-> counterpartyConnectionID, - counterpartyClientID |-> counterpartyClientID, - proofHeight |-> pHeight, - consensusHeight |-> cHeight] \in outgoingDatagrams[chainID] - -\* returns true if there is a "ConnOpenAck" datagram -\* in outgoing datagrams for chainID -IsConnOpenAckInPendingDatagrams(chainID, connectionID) == - \E pHeight \in Heights : \E cHeight \in Heights : - [type |-> "ConnOpenAck", - connectionID |-> connectionID, - proofHeight |-> pHeight, - consensusHeight |-> cHeight] \in outgoingDatagrams[chainID] - -\* returns true if there is a "ConnOpenConfirm" datagram -\* in outgoing datagrams for chainID -IsConnOpenConfirmInPendingDatagrams(chainID, connectionID) == - \E pHeight \in Heights : - [type |-> "ConnOpenConfirm", - connectionID |-> connectionID, - proofHeight |-> pHeight] \in outgoingDatagrams[chainID] - -\* returns true if there is a "ChanOpenInit" datagram -\* in outgoing datagrams for chainID -IsChanOpenInitInPendingDatagrams(chainID, channelID, counterpartyChannelID) == - [type |-> "ChanOpenInit", - channelID |-> channelID, - counterpartyChannelID |-> counterpartyChannelID] \in outgoingDatagrams[chainID] - -\* returns true if there is a "ChanOpenTry" datagram -\* in outgoing datagrams for chainID -IsChanOpenTryInPendingDatagrams(chainID, channelID, counterpartyChannelID) == - \E pHeight \in Heights : - [type |-> "ChanOpenTry", - channelID |-> channelID, - counterpartyChannelID |-> counterpartyChannelID, - proofHeight |-> pHeight] \in outgoingDatagrams[chainID] - -\* returns true if there is a "ChanOpenAck" datagram -\* in outgoing datagrams for chainID -IsChanOpenAckInPendingDatagrams(chainID, channelID) == - \E pHeight \in Heights : - [type |-> "ChanOpenAck", - channelID |-> channelID, - proofHeight |-> pHeight] \in outgoingDatagrams[chainID] - -\* returns true if there is a "ChanOpenConfirm" datagram -\* in outgoing datagrams for chainID -IsChanOpenConfirmInPendingDatagrams(chainID, channelID) == - \E pHeight \in Heights : - [type |-> "ChanOpenConfirm", - channelID |-> channelID, - proofHeight |-> pHeight] \in outgoingDatagrams[chainID] - -(*************************************************************************** - Invariants - ***************************************************************************) -\* Type invariant -TypeOK == - /\ turn \in {"relayer", "environment"} - /\ relayerChainHeights \in [ChainIDs -> Heights \union {nullHeight}] - /\ Env!TypeOK - -\* CreateClientInv -\* if a "CreateClient" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct client ID -\* and the client that should be created does not exist (has null height) -CreateClientInv == - \A chainID \in ChainIDs : \A clID \in ClientIDs : - ((\E h \in Heights : IsCreateClientInPendingDatagrams(chainID, clID, h)) - => (/\ clID = GetCounterpartyClientID(chainID) - /\ GetCounterpartyClientHeights(chainID) = {})) - -\* if a "ClientUpdate" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct client ID -\* and the client that should be updated has height less than the one in the datagram -ClientUpdateInv == - \A chainID \in ChainIDs : \A clID \in ClientIDs : \A h \in Heights : - IsClientUpdateInPendingDatagrams(chainID, clID, h) - => (/\ clID = GetCounterpartyClientID(chainID) - /\ GetMaxCounterpartyClientHeight(chainID) < h) - -\* ConnOpenInitInv -\* if a "ConnOpenInit" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct client ID, counterparty clientID, -\* connection ID, counterparty connection ID -\* and the connection that should be in INIT is currently in UNINIT -ConnOpenInitInv == - \A chainID \in ChainIDs : - \A clientID \in ClientIDs : \A counterpartyClientID \in ClientIDs : - \A connectionID \in ConnectionIDs : \A counterpartyConnectionID \in ConnectionIDs : - IsConnOpenInitInPendingDatagrams(chainID, clientID, counterpartyClientID, - connectionID, counterpartyConnectionID) - => /\ clientID = GetCounterpartyClientID(chainID) - /\ counterpartyClientID = GetClientID(chainID) - /\ connectionID = GetConnectionID(chainID) - /\ counterpartyConnectionID = GetCounterpartyConnectionID(chainID) - /\ IsConnectionUninit(chainID) - - -\* ConnOpenTryInv -\* if a "ConnOpenTry" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct client ID, counterparty clientID, -\* connection ID, counterparty connection ID, proof height, consensus height -\* and the connection that should be in TRYOPEN is currently either UNINIT or INIT -ConnOpenTryInv == - \A chainID \in ChainIDs : - \A clientID \in ClientIDs : \A counterpartyClientID \in ClientIDs : - \A connectionID \in ConnectionIDs : \A counterpartyConnectionID \in ConnectionIDs : - IsConnOpenTryInPendingDatagrams( - chainID, clientID, counterpartyClientID, - connectionID, counterpartyConnectionID - ) - => /\ clientID = GetCounterpartyClientID(chainID) - /\ counterpartyClientID = GetClientID(chainID) - /\ connectionID = GetConnectionID(chainID) - /\ counterpartyConnectionID = GetCounterpartyConnectionID(chainID) - /\ \/ IsConnectionUninit(chainID) - \/ IsConnectionInit(chainID) - -\* ConnOpenAckInv -\* if a "ConnOpenAck" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct connection ID, proof height, consensus height -\* and the connection that should be in OPEN is currently either INIT or TRYOPEN -ConnOpenAckInv == - \A chainID \in ChainIDs : \A connectionID \in ConnectionIDs : - IsConnOpenAckInPendingDatagrams(chainID, connectionID) - => /\ connectionID = GetConnectionID(chainID) - /\ \/ IsConnectionInit(chainID) - \/ IsConnectionTryopen(chainID) - -\* ConnOpenConfirmInv -\* if a "ConnOpenConfirm" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct client ID, counterparty clientID, -\* connection ID, counterparty connection ID, proof height -\* and the connection that should be in OPEN is currently TRYOPEN -ConnOpenConfirmInv == - \A chainID \in ChainIDs : \A connectionID \in ConnectionIDs : - IsConnOpenConfirmInPendingDatagrams(chainID, connectionID) - => /\ connectionID = GetConnectionID(chainID) - /\ IsConnectionTryopen(chainID) - -\* ChanOpenInitInv -\* if a "ChanOpenInit" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct client ID, counterparty clientID, -\* connection ID, counterparty connection ID -\* and the connection that should be in INIT is currently in UNINIT -ChanOpenInitInv == - \A chainID \in ChainIDs : - \A channelID \in ChannelIDs : \A counterpartyChannelID \in ChannelIDs : - IsChanOpenInitInPendingDatagrams(chainID, channelID, counterpartyChannelID) - => /\ channelID = GetChannelID(chainID) - /\ counterpartyChannelID = GetCounterpartyChannelID(chainID) - /\ IsChannelUninit(chainID) - - -\* ChanOpenTryInv -\* if a "ChanOpenTry" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct client ID, counterparty clientID, -\* connection ID, counterparty connection ID, proof height, consensus height -\* and the connection that should be in TRYOPEN is currently either UNINIT or INIT -ChanOpenTryInv == - \A chainID \in ChainIDs : - \A channelID \in ChannelIDs : \A counterpartyChannelID \in ChannelIDs : - IsChanOpenTryInPendingDatagrams(chainID, channelID, counterpartyChannelID) - => /\ channelID = GetChannelID(chainID) - /\ counterpartyChannelID = GetCounterpartyChannelID(chainID) - /\ \/ IsChannelUninit(chainID) - \/ IsChannelInit(chainID) - -\* ChanOpenAckInv -\* if a "ChanOpenAck" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct connection ID, proof height, consensus height -\* and the connection that should be in OPEN is currently either INIT or TRYOPEN -ChanOpenAckInv == - \A chainID \in ChainIDs : \A channelID \in ChannelIDs : - IsChanOpenAckInPendingDatagrams(chainID, channelID) - => /\ \/ IsChannelInit(chainID) - \/ IsChannelTryopen(chainID) - -\* ChanOpenConfirmInv -\* if a "ChanOpenConfirm" datagram is in pendingDatagrams for chainID, -\* then the datagram has the correct client ID, counterparty clientID, -\* connection ID, counterparty connection ID, proof height -\* and the connection that should be in OPEN is currently TRYOPEN -ChanOpenConfirmInv == - \A chainID \in ChainIDs : \A channelID \in ChannelIDs : - IsChanOpenConfirmInPendingDatagrams(chainID, channelID) - => /\ IsChannelTryopen(chainID) - -\* Inv -\* A conjunction of all invariants -Inv == - /\ TypeOK - /\ CreateClientInv - /\ ClientUpdateInv - /\ ConnOpenInitInv - /\ ConnOpenTryInv - /\ ConnOpenAckInv - /\ ConnOpenConfirmInv - /\ ChanOpenInitInv - /\ ChanOpenTryInv - /\ ChanOpenAckInv - /\ ChanOpenConfirmInv - -(*************************************************************************** - Properties about client updates - ***************************************************************************) -\* it ALWAYS holds that, for every chainID: -\* - if -\* * the counterparty client is not initialized -\* - then -\* * the relayer EVENTUALLY adds a "CreateClient" datagram in pending datagrams of chainID -CreateClientIsGenerated == - [](\A chainID \in ChainIDs : - GetCounterpartyClientHeights(chainID) = {} - => <>(\E h \in Heights : IsCreateClientInPendingDatagrams(chainID, GetCounterpartyClientID(chainID), h))) - -\* it ALWAYS holds that, for every chainID: -\* - if -\* * there is a "CreateClient" datagram in pending datagrams of chainID for some height h -\* * a counterparty client does not exist on chainID -\* - then -\* * the counterparty client is EVENTUALLY created on chainID -ClientCreated == - [](\A chainID \in ChainIDs : - (/\ \E h \in Heights : IsCreateClientInPendingDatagrams(chainID, GetCounterpartyClientID(chainID), h) - /\ ~IsCounterpartyClientOnChain(chainID)) - => (<>(IsCounterpartyClientOnChain(chainID)))) - -\* it ALWAYS holds that, for every chainID: -\* - if -\* * the counterparty client on chainID has height smaller -\* than the height of chainID's counterparty chain -\* - then -\* * the relayer EVENTUALLY adds a "ClientUpdate" datagram in pending datagrams of chainID -ClientUpdateIsGenerated == - [](\A chainID \in ChainIDs : \A h1 \in Heights : - (/\ GetMaxCounterpartyClientHeight(chainID) = h1 - /\ GetMaxCounterpartyClientHeight(chainID) < GetLatestHeight(GetCounterpartyChainID(chainID))) - => <>(\E h2 \in Heights : - /\ h1 <= h2 - /\ IsClientUpdateInPendingDatagrams(chainID, GetCounterpartyClientID(chainID), h2))) - -\* it ALWAYS holds that, for every chainID: -\* - if -\* * there is a "ClientUpdate" datagram in pending datagrams of chainID -\* for height h -\* * the counterparty client height is smaller than h -\* - then -\* * the counterparty client height is EVENTUALLY udpated to at least h -ClientUpdated == - [](\A chainID \in ChainIDs : \A h \in Heights : - (/\ IsClientUpdateInPendingDatagrams(chainID, GetCounterpartyClientID(chainID), h) - /\ GetMaxCounterpartyClientHeight(chainID) < h) - => (<>(CounterpartyClientHeightUpdated(chainID, h)))) - -(*************************************************************************** - Properties about connection handshake - ***************************************************************************) -\* it ALWAYS holds that, for every chainID: -\* - if -\* * the connection on chainID is uninitialized and -\* * the connection on chainID's counterparty is uninitialized -\* - then EVENTUALLY either -\* * there is a "ConnOpenInit" datagram in pending datagrams of chainID -\* * or the state of the counterparty connection is "INIT" -ConnOpenInitIsGenerated == - [](\A chainID \in ChainIDs : - IsConnectionUninit(chainID) - => <>(\/ IsConnOpenInitInPendingDatagrams( - chainID, GetCounterpartyClientID(chainID), GetClientID(chainID), - GetConnectionID(chainID), GetCounterpartyConnectionID(chainID) - ) - \/ IsConnectionInit(GetCounterpartyChainID(chainID)))) - -\* it ALWAYS holds that, for every cahinID, and every counterpartyChainID: -\* - if -\* * there is a "ConnOpenInit" datagram in pending datagrams of chainID -\* * the connection is not open -\* - then -\* * the connection is EVENTUALLY open -ConnectionOpened == - [](\A chainID \in ChainIDs : - IsConnOpenInitInPendingDatagrams( - chainID, GetClientID(chainID), GetCounterpartyClientID(chainID), - GetConnectionID(chainID), GetCounterpartyConnectionID(chainID) - ) - => <>(/\ IsConnectionOpen(chainID) - /\ IsConnectionOpen(GetCounterpartyChainID(chainID)))) - -(*************************************************************************** - Properties about channel handshake - ***************************************************************************) -\* it ALWAYS holds that, for every chainID: -\* - if -\* * the chain on chainID is uninitialized and -\* * the chain on chainID's counterparty is uninitialized -\* - then -\* * the relayer EVENTUALLY adds a "ChanOpenInit" datagram in pending datagrams of chainID -ChanOpenInitIsGenerated == - [](\A chainID \in ChainIDs : - (IsChannelUninit(chainID) - => <>(\/ IsChanOpenInitInPendingDatagrams(chainID, GetChannelID(chainID), GetCounterpartyChannelID(chainID)) - \/ IsChannelInit(GetCounterpartyChainID(chainID))))) - -\* it ALWAYS holds that, for every cahinID, and every counterpartyChainID: -\* - if -\* * there is a "ChanOpenInit" datagram in pending datagrams of chainID -\* - then -\* * the channel is EVENTUALLY open -ChannelOpened == - [](\A chainID \in ChainIDs : - IsChanOpenInitInPendingDatagrams(chainID, GetChannelID(chainID), GetCounterpartyChannelID(chainID)) - => <>(/\ IsChannelOpen(chainID) - /\ IsChannelOpen(GetCounterpartyChainID(chainID)))) - - -(*************************************************************************** - Properties about the environment - ***************************************************************************) -\* for every chainID, it is always the case that the height of the chain -\* does not decrease -HeightsDontDecrease == - [](\A chainID \in ChainIDs : \A h \in Heights : - (chains[chainID].height = h) - => <>(chains[chainID].height >= h)) - -\* Prop -\* A conjunction of all properties -Prop == - /\ CreateClientIsGenerated - /\ ClientCreated - /\ ClientUpdateIsGenerated - /\ ClientUpdated - /\ ConnOpenInitIsGenerated - /\ ConnectionOpened - /\ ChanOpenInitIsGenerated - /\ ChannelOpened - /\ HeightsDontDecrease - -============================================================================= -\* Modification History -\* Last modified Tue May 26 12:13:36 CEST 2020 by ilinastoilkovska -\* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/Chain.tla b/docs/spec/relayer/Chain.tla index 9a4d89d0aa..4cd65a41ea 100644 --- a/docs/spec/relayer/Chain.tla +++ b/docs/spec/relayer/Chain.tla @@ -59,7 +59,12 @@ ChannelUpdate(chainID, store, datagrams) == \* update the chain store with "ChanOpenConfirm" datagrams LET chanOpenConfirmStore == HandleChanOpenConfirm(chainID, chanOpenAckStore, datagrams) IN - chanOpenConfirmStore + \* 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 (*************************************************************************** Chain update operators @@ -142,5 +147,5 @@ HeightDoesntDecrease == ============================================================================= \* Modification History -\* Last modified Thu Jul 02 16:10:33 CEST 2020 by ilinastoilkovska +\* Last modified Fri Jul 10 16:13:04 CEST 2020 by ilinastoilkovska \* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/ChannelHandlers.tla b/docs/spec/relayer/ChannelHandlers.tla index 03a526adb8..0fa2313761 100644 --- a/docs/spec/relayer/ChannelHandlers.tla +++ b/docs/spec/relayer/ChannelHandlers.tla @@ -140,7 +140,64 @@ HandleChanOpenConfirm(chainID, chain, datagrams) == \* otherwise, do not update the chain ELSE chain +\* Handle "ChanCloseInit" datagrams +HandleChanCloseInit(chainID, chain, datagrams) == + \* get "ChanCloseInit" datagrams, with a valid channel ID + LET chanCloseInitDgrs == {dgr \in datagrams : + /\ dgr.type = "ChanCloseInit" + /\ dgr.channelID = GetChannelID(chainID)} IN + + \* if there are valid "ChanCloseInit" datagrams + IF /\ chanCloseInitDgrs /= {} + \* and the channel end is neither UNINIT nor CLOSED + /\ chain.connectionEnd.channelEnd.state \notin {"UNINIT", "CLOSED"} + \* and the connection end is OPEN + /\ chain.connectionEnd.state = "OPEN" + THEN \* then close the channel end + LET chanCloseInitChannelEnd == [ + chain.connectionEnd.channelEnd EXCEPT !.state = "CLOSED" + ] IN + LET chanCloseInitConnectionEnd == [ + chain.connectionEnd EXCEPT !.channelEnd = chanCloseInitChannelEnd + ] IN + LET chanCloseInitChain == [ + chain EXCEPT !.connectionEnd = chanCloseInitConnectionEnd + ] IN + + chanCloseInitChain + \* otherwise, do not update the chain + ELSE chain + +\* Handle "ChanCloseConfirm" datagrams +HandleChanCloseConfirm(chainID, chain, datagrams) == + \* get "ChanCloseConfirm" datagrams, with a valid channel ID + LET chanCloseConfirmDgrs == {dgr \in datagrams : + /\ dgr.type = "ChanCloseConfirm" + /\ dgr.channelID = GetChannelID(chainID) + /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN + + \* if there are valid "ChanCloseConfirm" datagrams + IF /\ chanCloseConfirmDgrs /= {} + \* and the channel end is neither UNINIT nor CLOSED + /\ chain.connectionEnd.channelEnd.state \notin {"UNINIT", "CLOSED"} + \* and the connection end is OPEN + /\ chain.connectionEnd.state = "OPEN" + THEN \* then close the channel end + LET chanCloseInitChannelEnd == [ + chain.connectionEnd.channelEnd EXCEPT !.state = "CLOSED" + ] IN + LET chanCloseInitConnectionEnd == [ + chain.connectionEnd EXCEPT !.channelEnd = chanCloseInitChannelEnd + ] IN + LET chanCloseInitChain == [ + chain EXCEPT !.connectionEnd = chanCloseInitConnectionEnd + ] IN + + chanCloseInitChain + \* otherwise, do not update the chain + ELSE chain + ============================================================================= \* Modification History -\* Last modified Mon Jul 06 15:43:14 CEST 2020 by ilinastoilkovska +\* Last modified Thu Jul 09 09:13:10 CEST 2020 by ilinastoilkovska \* Created Tue Apr 07 16:58:02 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/ClientHandlers.tla b/docs/spec/relayer/ClientHandlers.tla index 33ca3078b9..bdce3785d0 100644 --- a/docs/spec/relayer/ClientHandlers.tla +++ b/docs/spec/relayer/ClientHandlers.tla @@ -31,7 +31,7 @@ HandleCreateClient(chainID, chain, datagrams) == counterpartyClientHeights |-> \* if the set of counterparty client heights is not empty and \* if the set of heights from datagrams is empty - IF chain.counterpartyClientHeights /= {} /\ createClientHeights = {} + IF chain.counterpartyClientHeights /= {} \/ createClientHeights = {} \* then discard CreateClient datagrams THEN chain.counterpartyClientHeights \* otherwise, create counterparty client with height Max(createClientHeights) @@ -77,5 +77,5 @@ HandleUpdateClient(chainID, chain, datagrams) == ============================================================================= \* Modification History -\* Last modified Mon Jul 06 15:37:30 CEST 2020 by ilinastoilkovska +\* Last modified Thu Jul 09 13:12:01 CEST 2020 by ilinastoilkovska \* Created Tue Apr 07 16:42:47 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/ICS18Environment.tla b/docs/spec/relayer/ICS18Environment.tla index f15218dcfe..dc9bbfabe1 100644 --- a/docs/spec/relayer/ICS18Environment.tla +++ b/docs/spec/relayer/ICS18Environment.tla @@ -16,12 +16,15 @@ VARIABLES chainAstore, \* store of ChainA incomingDatagramsChainB, \* set of datagrams incoming to ChainB relayer1Heights, \* the client heights of Relayer1 relayer2Heights, \* the client heights of Relayer2 - outgoingDatagrams \* sets of datagrams outgoing of the relayers + outgoingDatagrams, \* sets of datagrams outgoing of the relayers + closeChannelA, \* flag that triggers closing of the channel end at ChainA + closeChannelB \* flag that triggers closing of the channel end at ChainB vars == <> + outgoingDatagrams, + closeChannelA, closeChannelB>> chainAvars == <> chainBvars == <> relayerVars == <> @@ -38,9 +41,6 @@ Relayer1 == INSTANCE Relayer WITH GenerateClientDatagrams <- ClientDatagramsRelayer1, GenerateConnectionDatagrams <- ConnectionDatagramsRelayer1, GenerateChannelDatagrams <- ChannelDatagramsRelayer1, - Heights <- Heights, - chainAstore <- chainAstore, - chainBstore <- chainBstore, relayerHeights <- relayer1Heights \* Relayer2 -- Instance of Relayer.tla @@ -48,23 +48,18 @@ Relayer2 == INSTANCE Relayer WITH GenerateClientDatagrams <- ClientDatagramsRelayer2, GenerateConnectionDatagrams <- ConnectionDatagramsRelayer2, GenerateChannelDatagrams <- ChannelDatagramsRelayer2, - Heights <- Heights, - chainAstore <- chainAstore, - chainBstore <- chainBstore, relayerHeights <- relayer2Heights \* We suppose there are two chains that communicate, ChainA and ChainB \* ChainA -- Instance of Chain.tla ChainA == INSTANCE Chain WITH ChainID <- "chainA", - Heights <- Heights, chainStore <- chainAstore, incomingDatagrams <- incomingDatagramsChainA \* ChainB -- Instance of Chain.tla ChainB == INSTANCE Chain WITH ChainID <- "chainB", - Heights <- Heights, chainStore <- chainBstore, incomingDatagrams <- incomingDatagramsChainB @@ -79,10 +74,12 @@ RelayerAction == /\ UNCHANGED chainAvars /\ UNCHANGED chainBvars /\ UNCHANGED relayer2Heights + /\ UNCHANGED <> \/ /\ Relayer2!Next /\ UNCHANGED chainAvars /\ UNCHANGED chainBvars /\ UNCHANGED relayer1Heights + /\ UNCHANGED <> \* ChainAction: either chain takes a step, leaving the other \* variables unchanged @@ -90,9 +87,11 @@ ChainAction == \/ /\ ChainA!Next /\ UNCHANGED chainBvars /\ UNCHANGED relayerVars + /\ UNCHANGED <> \/ /\ ChainB!Next /\ UNCHANGED chainAvars /\ UNCHANGED relayerVars + /\ UNCHANGED <> (*************************************************************************** ICS18Environment actions @@ -103,6 +102,20 @@ SubmitDatagrams == /\ incomingDatagramsChainB' = incomingDatagramsChainB \cup outgoingDatagrams["chainB"] /\ outgoingDatagrams' = [chainID \in ChainIDs |-> {}] /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Non-deterministically set channel closing flags +CloseChannels == + \/ /\ closeChannelA = FALSE + /\ closeChannelA' \in BOOLEAN + /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED closeChannelB + \/ /\ closeChannelB = FALSE + /\ closeChannelB' \in BOOLEAN + /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED closeChannelA \* Faulty relayer action FaultyRelayer == @@ -111,6 +124,7 @@ FaultyRelayer == EnvironmentAction == \/ SubmitDatagrams + \/ CloseChannels \* TODO: Uncomment once FaultyRelayer is specified \* \/ FaultyRelayer @@ -123,6 +137,8 @@ Init == /\ ChainB!Init /\ Relayer1!Init /\ Relayer2!Init + /\ closeChannelA = FALSE + /\ closeChannelB = FALSE \* Next state action Next == @@ -139,6 +155,8 @@ Fairness == /\ ChainB!Fairness /\ Relayer1!Fairness /\ Relayer2!Fairness + /\ <>[]closeChannelA + /\ <>[]closeChannelB \* Specification formula Spec == Init /\ [][Next]_vars /\ Fairness @@ -202,6 +220,14 @@ IsChanOpenInitInOutgoingDatagrams(chainID) == [type |-> "ChanOpenInit", channelID |-> chanID, counterpartyChannelID |-> counterpartyChanID] \in outgoingDatagrams[chainID] + +\* returns true if there is a "ChanCloseInit" datagram +\* in outgoing datagrams for chainID +IsChanCloseInitInOutgoingDatagrams(chainID) == + LET chanID == GetChannelID(chainID) IN + [type |-> "ChanCloseInit", + channelID |-> chanID] \in outgoingDatagrams[chainID] + ---------------------------------------------------------------------------- (*************************************************************************** @@ -294,7 +320,20 @@ ChannelOpenSafety == /\ IsChannelOpen(GetChainByID(chainID)) => [](/\ ~IsChannelUninit(GetChainByID(chainID)) /\ ~IsChannelInit(GetChainByID(chainID)) - /\ ~IsChannelTryOpen(GetChainByID(chainID)))) + /\ ~IsChannelTryOpen(GetChainByID(chainID)))) + +\* it ALWAYS holds that, for every chainID +\* - if +\* * the channel end is in CLOSED +\* - then +\* * it NEVER goes to UNINIT, INIT, TRYOPEN, or OPEN +ChannelCloseSafety == + [](\A chainID \in ChainIDs: + /\ IsChannelClosed(GetChainByID(chainID)) + => [](/\ ~IsChannelUninit(GetChainByID(chainID)) + /\ ~IsChannelInit(GetChainByID(chainID)) + /\ ~IsChannelTryOpen(GetChainByID(chainID)) + /\ ~IsChannelOpen(GetChainByID(chainID)))) (*************************************************************************** Safety [ICS18Safety]: @@ -314,7 +353,8 @@ ICS18Safety == /\ (ChannelDatagramsRelayer1 \/ ChannelDatagramsRelayer2) => /\ ChannelInitSafety /\ ChannelTryOpenSafety - /\ ChannelOpenSafety + /\ ChannelOpenSafety + /\ ChannelCloseSafety (*************************************************************************** Liveness: Eventual delivery of client datagrams @@ -349,7 +389,7 @@ ClientUpdateDelivery == \* * EVENTUALLY a ConnOpenInit is sent to chainID \* - then \* * EVENTUALLY the connections at chainID and its counterparty are open - ConnOpenInitDelivery == +ConnOpenInitDelivery == [](\A chainID \in ChainIDs : (<>IsConnOpenInitInOutgoingDatagrams(chainID) => <>(/\ IsConnectionOpen(GetChainByID(chainID)) @@ -358,16 +398,27 @@ ClientUpdateDelivery == (*************************************************************************** Liveness: Eventual delivery of channel datagrams ***************************************************************************) - \* it ALWAYS holds that, for every chainID +\* it ALWAYS holds that, for every chainID \* - if \* * EVENTUALLY a ChanOpenInit is sent to chainID \* - then \* * EVENTUALLY the channels at chainID and its counterparty are open - ChanOpenInitDelivery == +ChanOpenInitDelivery == [](\A chainID \in ChainIDs : (<>IsChanOpenInitInOutgoingDatagrams(chainID) => <>(/\ IsChannelOpen(GetChainByID(chainID)) /\ IsChannelOpen(GetChainByID(GetCounterpartyChainID(chainID)))))) + +\* it ALWAYS holds that, for every chainID +\* - if +\* * EVENTUALLY a ChanCloseInit is sent to chainID +\* - then +\* * EVENTUALLY the channels at chainID and its counterparty are closed +ChanCloseInitDelivery == + [](\A chainID \in ChainIDs : + (<>IsChanCloseInitInOutgoingDatagrams(chainID) + => <>(/\ IsChannelClosed(GetChainByID(chainID)) + /\ IsChannelClosed(GetChainByID(GetCounterpartyChainID(chainID)))))) (*************************************************************************** Liveness [ICS18Delivery]: @@ -389,9 +440,10 @@ ICS18Delivery == => ConnOpenInitDelivery \* at least one relayer creates channel datagrams /\ (ChannelDatagramsRelayer1 \/ ChannelDatagramsRelayer2) - => ChanOpenInitDelivery + => /\ ChanOpenInitDelivery + /\ ChanCloseInitDelivery ============================================================================= \* Modification History -\* Last modified Tue Jul 07 13:13:08 CEST 2020 by ilinastoilkovska +\* Last modified Fri Jul 10 16:07:25 CEST 2020 by ilinastoilkovska \* Created Fri Jun 05 16:48:22 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/Relayer.tla b/docs/spec/relayer/Relayer.tla index 8f4a085c10..041abe829e 100644 --- a/docs/spec/relayer/Relayer.tla +++ b/docs/spec/relayer/Relayer.tla @@ -21,7 +21,9 @@ VARIABLES chainAstore, \* store of ChainA chainBstore, \* store of ChainB outgoingDatagrams, \* a function that assigns a set of pending datagrams \* outgoing from the relayer to each chainID - relayerHeights \* a function that assigns a height to each chainID + relayerHeights, \* a function that assigns a height to each chainID + closeChannelA, \* flag that triggers closing of the channel end at ChainA + closeChannelB \* flag that triggers closing of the channel end at ChainB vars == <> @@ -29,6 +31,11 @@ GetChainByID(chainID) == IF chainID = "chainA" THEN chainAstore ELSE chainBstore + +GetCloseChannelFlag(chainID) == + IF chainID = "chainA" + THEN closeChannelA + ELSE closeChannelB (*************************************************************************** Client datagrams @@ -136,6 +143,8 @@ ChannelDatagrams(srcChainID, dstChainID) == LET srcHeight == GetLatestHeight(srcChain) IN + LET dstCloseChannel == GetCloseChannelFlag(dstChainID) IN + IF dstChannelEnd.state = "UNINIT" /\ srcChannelEnd.state = "UNINIT" THEN {[type |-> "ChanOpenInit", channelID |-> dstChannelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") @@ -144,22 +153,32 @@ ChannelDatagrams(srcChainID, dstChainID) == ELSE IF srcChannelEnd.state = "INIT" /\ \/ dstChannelEnd.state = "UNINIT" \/ dstChannelEnd.state = "INIT" THEN {[type |-> "ChanOpenTry", - channelID |-> dstChannelID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + channelID |-> dstChannelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") counterpartyChannelID |-> srcChannelID, \* "chanAtoB" proofHeight |-> srcHeight]} ELSE IF srcChannelEnd.state = "TRYOPEN" /\ \/ dstChannelEnd.state = "INIT" \/ dstChannelEnd.state = "TRYOPEN" THEN {[type |-> "ChanOpenAck", - channelID |-> dstChannelID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + channelID |-> dstChannelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") proofHeight |-> srcHeight]} ELSE IF srcChannelEnd.state = "OPEN" /\ dstChannelEnd.state = "TRYOPEN" THEN {[type |-> "ChanOpenConfirm", channelID |-> dstChannelEnd.channelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") proofHeight |-> srcHeight]} - ELSE {} + ELSE IF dstChannelEnd.state = "OPEN" /\ GetCloseChannelFlag(dstChannelID) THEN + {[type |-> "ChanCloseInit", + channelID |-> dstChannelEnd.channelID]} \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + + ELSE IF srcChannelEnd.state = "CLOSED" /\ dstChannelEnd.state /= "CLOSED" THEN + {[type |-> "ChanCloseConfirm", + channelID |-> dstChannelEnd.channelID, \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + proofHeight |-> srcHeight]} + + ELSE {} + (*************************************************************************** Compute datagrams (from srcChainID to dstChainID) ***************************************************************************) @@ -268,5 +287,5 @@ TypeOK == ============================================================================= \* Modification History -\* Last modified Mon Jul 06 15:55:07 CEST 2020 by ilinastoilkovska +\* Last modified Thu Jul 09 15:51:13 CEST 2020 by ilinastoilkovska \* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/RelayerDefinitions.tla b/docs/spec/relayer/RelayerDefinitions.tla index ce9c566b49..c178ce560d 100644 --- a/docs/spec/relayer/RelayerDefinitions.tla +++ b/docs/spec/relayer/RelayerDefinitions.tla @@ -125,6 +125,10 @@ Datagrams(Heights) == [type : {"ChanOpenAck"}, channelID : ChannelIDs, proofHeight : Heights] \union [type : {"ChanOpenConfirm"}, channelID : ChannelIDs, proofHeight : Heights] + \union + [type : {"ChanCloseInit"}, channelID : ChannelIDs] + \union + [type : {"ChanCloseConfirm"}, channelID : ChannelIDs, proofHeight : Heights] (*************************************************************************** Initial values of a channel end, connection end, chain @@ -274,9 +278,12 @@ IsChannelTryOpen(chain) == \* returns true if the channel end on chainID is OPEN IsChannelOpen(chain) == chain.connectionEnd.channelEnd.state = "OPEN" - + +\* returns true if the channel end on chainID is CLOSED +IsChannelClosed(chain) == + chain.connectionEnd.channelEnd.state = "CLOSED" ============================================================================= \* Modification History -\* Last modified Mon Jul 06 16:19:06 CEST 2020 by ilinastoilkovska +\* Last modified Fri Jul 10 16:04:18 CEST 2020 by ilinastoilkovska \* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska \ No newline at end of file