diff --git a/verification/spec/relayer/ChannelHandlers.tla b/verification/spec/relayer/ChannelHandlers.tla new file mode 100644 index 0000000000..c0ea6ffd41 --- /dev/null +++ b/verification/spec/relayer/ChannelHandlers.tla @@ -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 diff --git a/verification/spec/relayer/ClientHandlers.tla b/verification/spec/relayer/ClientHandlers.tla new file mode 100644 index 0000000000..9395283245 --- /dev/null +++ b/verification/spec/relayer/ClientHandlers.tla @@ -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 diff --git a/verification/spec/relayer/ConnectionHandlers.tla b/verification/spec/relayer/ConnectionHandlers.tla new file mode 100644 index 0000000000..6c4a6a546c --- /dev/null +++ b/verification/spec/relayer/ConnectionHandlers.tla @@ -0,0 +1,168 @@ +------------------------- 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/verification/spec/relayer/Environment.tla b/verification/spec/relayer/Environment.tla new file mode 100644 index 0000000000..da33e5c04a --- /dev/null +++ b/verification/spec/relayer/Environment.tla @@ -0,0 +1,350 @@ +---------------------------- 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/verification/spec/relayer/README.md b/verification/spec/relayer/README.md index 617edb9b2d..358a23a271 100644 --- a/verification/spec/relayer/README.md +++ b/verification/spec/relayer/README.md @@ -1,17 +1,26 @@ A TLA+ specification of the Relayer algorithm. -The specification has two modules: - - `relayer.tla` (the main module) - - `environment.tla` (the environment module) +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. Currently, the relayer and the environment can only handle ICS 002 Client datagrams. +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` as a module in the spec + - 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 invariants `Inv` (a conjunction of the invariants `TypeOK`, `CreateClientInv`, `ClientUpdateInv`) - - add the properties `CreateClientIsGenerated`, `Env!ClientCreated`, `Env!ClientUpdated`, `Env!HeightsDontDecrease` + - 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/verification/spec/relayer/Relayer.tla b/verification/spec/relayer/Relayer.tla new file mode 100644 index 0000000000..12c9df8f5e --- /dev/null +++ b/verification/spec/relayer/Relayer.tla @@ -0,0 +1,744 @@ +------------------------------ 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/verification/spec/relayer/environment.tla b/verification/spec/relayer/environment.tla deleted file mode 100644 index 2ebc89e410..0000000000 --- a/verification/spec/relayer/environment.tla +++ /dev/null @@ -1,343 +0,0 @@ ----------------------------- MODULE environment ---------------------------- - -EXTENDS Naturals, FiniteSets - -CONSTANTS MaxHeight \* maximal height of all the chains in the system - -VARIABLES chains, \* a function that assigns to each chainID a chain record - pendingDatagrams \* a function that assigns to each chainID a set of pending datagrams - -vars == <> - -ChainIDs == {"chainA", "chainB"} -ClientIDs == {"clA", "clB"} -Heights == 1..MaxHeight - -nullClientID == 0 -nullHeight == 0 - -Max(S) == CHOOSE x \in S: \A y \in S: y <= x - -(*** 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. - - - counterpartyClientHeight : an integer between nullHeight and MaxHeight - Stores the height of the client for the counterparty chain. -**************) -Chains == - [ - height : Heights \union {nullHeight}, - counterpartyClientHeight : Heights \union {nullHeight} - ] - -(*** Datagrams *** - A set of datagrams. -******************) -Datagrams == - [type : {"CreateClient"}, clientID : ClientIDs, height : Heights] - \union - [type : {"ClientUpdate"}, clientID : ClientIDs, height : Heights] - -(*************** -Chain helper operators -***************) -\* get the latest height of the chainID -GetLatestHeight(chainID) == - chains[chainID].height - -\* get the client height of the client for the counterparty chain -GetCounterpartyClientHeight(chainID) == - chains[chainID].counterpartyClientHeight - -\* 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 the counterparty of chainID -GetCounterpartyClientID(chainID) == - IF chainID = "chainA" THEN "clB" ELSE "clA" - -(*************** -Light client update operators -***************) - -\* Handle "CreateClient" datagrams -HandleCreateClient(chainID, chain, datagrams) == - \* get "CreateClient" datagrams - LET createClients == {dgr \in datagrams : dgr.type = "CreateClient"} IN - \* get heights in datagrams with correct counterparty clientID for chainID - LET createClientHeights == - {h \in Heights : \E dgr \in createClients : - /\ dgr.clientID = GetCounterpartyClientID(chainID) - /\ dgr.height = h} IN - - \* new chain record with clients created - LET clientsCreated == [ - height |-> chain.height, - counterpartyClientHeight |-> IF createClientHeights /= {} - THEN Max(createClientHeights) - ELSE chain.counterpartyClientHeight - ] IN - clientsCreated - -\* Handle "ClientUpdate" datagrams -HandleUpdateClient(chainID, chain, datagrams) == - \* get "ClientUpdate" datagrams - LET updateClients == {dgr \in datagrams : dgr.type = "ClientUpdate"} IN - \* get heights in datagrams with correct counterparty clientID for chainID - LET updateClientHeights == - {h \in Heights : \E dgr \in updateClients : - /\ dgr.clientID = GetCounterpartyClientID(chainID) - /\ dgr.height = h} IN - - \* new chain record with clients updated - LET clientsUpdated == [ - height |-> chain.height, - counterpartyClientHeight |-> IF updateClientHeights /= {} - THEN Max(updateClientHeights) - ELSE chain.counterpartyClientHeight - ] IN - - clientsUpdated - -\* Update the clients on chain with chainID, -\* using the client datagrams generated by the relayer -LightClientUpdate(chainID, chain, datagrams) == - \* create clients - LET clientsCreated == HandleCreateClient(chainID, chain, datagrams) IN - \* update clients - LET clientsUpdated == HandleUpdateClient(chainID, clientsCreated, datagrams) IN - - clientsUpdated - -(*************** -Connection update operators -***************) - -\* Handle "ConnOpenInit" datagrams -HandleConnOpenInit(chainID, chain, datagrams) == - \* TODO - chain - -\* Handle "ConnOpenTry" datagrams -HandleConnOpenTry(chainID, chain, datagrams) == - \* TODO - chain - -\* Handle "ConnOpenAck" datagrams -HandleConnOpenAck(chainID, chain, datagrams) == - \* TODO - chain - -\* Handle "ConnOpenConfirm" datagrams -HandleConnOpenConfirm(chainID, chain, datagrams) == - \* TODO - chain - -\* 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 connInit == HandleConnOpenInit(chainID, chain, datagrams) IN - \* update chain with "ConnOpenTry" datagrams - LET connTry == HandleConnOpenTry(chainID, connInit, datagrams) IN - \* update chain with "ConnOpenAck" datagrams - LET connAck == HandleConnOpenAck(chainID, connTry, datagrams) IN - \* update chain with "ConnOpenConfirm" datagrams - LET connConfirm == HandleConnOpenConfirm(chainID, connAck, datagrams) IN - - connConfirm - -(*************** -Channel update operators -***************) - -\* Handle "ChanOpenInit" datagrams -HandleChanOpenInit(chainID, chain, datagrams) == - \* TODO - chain - -\* Handle "ChanOpenTry" datagrams -HandleChanOpenTry(chainID, chain, datagrams) == - \* TODO - chain - -\* Handle "ChanOpenAck" datagrams -HandleChanOpenAck(chainID, chain, datagrams) == - \* TODO - chain - -\* Handle "ChanOpenConfirm" datagrams -HandleChanOpenConfirm(chainID, chain, datagrams) == - \* TODO - chain - -\* 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 chanInit == HandleChanOpenInit(chainID, chain, datagrams) IN - \* update chain with "ChanOpenTry" datagrams - LET chanTry == HandleChanOpenTry(chainID, chanInit, datagrams) IN - \* update chain with "ChanOpenAck" datagrams - LET chanAck == HandleChanOpenAck(chainID, chanTry, datagrams) IN - \* update chain with "ChanOpenConfirm" datagrams - LET chanConfirm == HandleChanOpenConfirm(chainID, chanAck, datagrams) IN - - chanConfirm - - - -(*************** -Chain update operators -***************) - -\* Update chainID with the received datagrams -\* Currently, only supporting ICS 002: Client updates -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 - - channelsUpdated - -(*************** -Chain actions -***************) - -\* Advance the height of the chain until MaxHeight is reached -AdvanceChain == - \E chainID \in ChainIDs : - /\ chains[chainID].height < MaxHeight - /\ chains' = [chains EXCEPT - ![chainID].height = chains[chainID].height + 1 - ] - /\ UNCHANGED pendingDatagrams - -\* Receive the datagrams and update the chain state -ReceiveDatagrams == - \E chainID \in ChainIDs : - /\ pendingDatagrams[chainID] /= {} - /\ chains' = [chains EXCEPT - ![chainID] = UpdateChain(chainID, pendingDatagrams[chainID]) - ] - - /\ pendingDatagrams' = [pendingDatagrams EXCEPT - ![chainID] = {} - ] -\* Initial value of the chain: -\* - height is initialized to 1 -\* - the counterparty light client is uninitialized -InitChain == - [height |-> 1, - counterpartyClientHeight |-> nullHeight] - -(*************** -Specification -***************) - -\* Initial state predicate -\* Initially -\* - each chain is initialized to InitChain -\* - pendingDatagrams for each chain is empty -Init == - /\ chains = [chainID \in ChainIDs |-> InitChain] - /\ pendingDatagrams = [chainID \in ChainIDs |-> {}] - -\* Next state action -\* One of the chains either -\* - advances its height -\* - receives datagrams and updates its state -Next == - \/ AdvanceChain - \/ ReceiveDatagrams - \/ UNCHANGED vars - -\* Fairness constraints -Fairness == - /\ WF_vars(AdvanceChain) - /\ WF_vars(ReceiveDatagrams) - -(************ -Invariants -************) - -\* Type invariant -TypeOK == - /\ chains \in [ChainIDs -> Chains] - /\ pendingDatagrams \in [ChainIDs -> SUBSET Datagrams] - -(************ -Helper operators used in properties -************) - -\* returns true if there is a "CreateClient" datagram -\* in the pending datagrams for chainID -IsCreateClientInPendingDatagrams(chainID) == - \E h \in Heights: - [type |-> "CreateClient", clientID |-> GetCounterpartyClientID(chainID), height |-> h] - \in pendingDatagrams[chainID] - -\* returns true if there is a "ClientUpdate" datagram -\* in the pending datagrams for chainID and height h -IsClientUpdateInPendingDatagrams(chainID, h) == - [type |-> "ClientUpdate", clientID |-> GetCounterpartyClientID(chainID), height |-> h] - \in pendingDatagrams[chainID] - - -\* returns true if the counterparty client is initialized on chainID -IsCounterpartyClientOnChain(chainID) == - chains[chainID].counterpartyClientHeight /= nullHeight - -\* returns true if the counterparty client height on chainID is greater or equal than height -CounterpartyClientHeightUpdated(chainID, height) == - chains[chainID].counterpartyClientHeight >= height - -(************ -Properties -************) - -\* it ALWAYS holds that, for every chainID: -\* - if -\* * there is a "CreateClient" datagram in pending datagrams of chainID -\* * a counterparty client does not exist on chainID -\* - then -\* * the counterparty client is EVENTUALLY created on chainID -ClientCreated == - [](\A chainID \in ChainIDs : - (/\ IsCreateClientInPendingDatagrams(chainID) - /\ ~IsCounterpartyClientOnChain(chainID)) - => (<>(IsCounterpartyClientOnChain(chainID)))) - -\* 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, h) - /\ GetCounterpartyClientHeight(chainID) < h) - => (<>(CounterpartyClientHeightUpdated(chainID, h)))) - -\* 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)) - -============================================================================= -\* Modification History -\* Last modified Wed Mar 25 17:34:23 CET 2020 by ilinastoilkovska -\* Created Fri Mar 13 19:48:22 CET 2020 by ilinastoilkovska diff --git a/verification/spec/relayer/relayer.tla b/verification/spec/relayer/relayer.tla deleted file mode 100644 index 145313c859..0000000000 --- a/verification/spec/relayer/relayer.tla +++ /dev/null @@ -1,274 +0,0 @@ ------------------------------- MODULE relayer ------------------------------ - -EXTENDS Naturals, FiniteSets - -CONSTANTS MaxHeight \* maximal height of all the chains in the system - -VARIABLES chains, \* a function that assigns to each chainID a chain record - pendingDatagrams, \* a function that assigns to each chainID a set of pending datagrams - relayerClientHeights, \* a function that assigns to each ClientID a height - turn - - -\* Instance of the environment, -\* that takes care of the chain logic -Env == INSTANCE environment - WITH chains <- chains, - pendingDatagrams <- pendingDatagrams, - MaxHeight <- MaxHeight - -vars == <> -envVars == <> - -ChainIDs == Env!ChainIDs -ClientIDs == Env!ClientIDs -Heights == Env!Heights -RelayerClientIDs == Env!ClientIDs - -nullClientID == 0 -nullHeight == 0 - - -(*** Datagrams *** - A set of datagrams. -******************) -Datagrams == Env!Datagrams - -(*************** -Chain helper operators -***************) -\* get the latest height of the chainID -GetLatestHeight(chainID) == Env!GetLatestHeight(chainID) - -\* get the client height of the client for the counterparty chain on chainID -GetCounterpartyClientHeight(chainID) == Env!GetCounterpartyClientHeight(chainID) - -\* get the client ID of the client for chainID -GetClientID(chainID) == Env!GetClientID(chainID) - -\* get the client ID of the client for the counterparty chain of chainID -GetCounterpartyClientID(chainID) == Env!GetCounterpartyClientID(chainID) - -(*************** -Client datagrams -****************) - -\* Compute client datagrams for clients on srcChainID for dstChainID -ClientDatagrams(srcChainID, dstChainID) == - LET dstChainHeight == GetLatestHeight(dstChainID) IN - LET dstClientHeight == GetCounterpartyClientHeight(srcChainID) IN - LET dstClientID == GetCounterpartyClientID(srcChainID) IN - - LET srcDatagrams == - IF dstClientHeight = nullHeight - THEN \* the dst client does not exist on the src chain - {[type |-> "CreateClient", - height |-> relayerClientHeights[dstClientID], - clientID |-> dstClientID]} - ELSE \* the dst client exists at the src chain - IF dstClientHeight < dstChainHeight - THEN \* the height of the dst client is smaller than the height of the dst chain - {[type |-> "ClientUpdate", - height |-> relayerClientHeights[dstClientID], - clientID |-> dstClientID]} - ELSE {} IN - - srcDatagrams - -(*************** -Connection datagrams -****************) - -ConnectionDatagrams(srcChainID, dstChainID) == - \* TODO - [src |-> {}, dst |-> {}] - -(*************** -Channel datagrams -****************) - -ChannelDatagrams(srcChainID, dstChainID) == - \* TODO - [src |-> {}, dst |-> {}] - -(**************** -Compute pending datagrams -****************) - -\* Currently, only supporting ICS 002: Client updates -\* TODO: Support the remaining datagrams -PendingDatagrams(srcChainID, dstChainID) == - \* ICS 002 : Clients - \* - Determine if light clients needs to be updated - LET clientDatagrams == [src |-> ClientDatagrams(srcChainID, dstChainID), - dst |-> ClientDatagrams(dstChainID, srcChainID)] IN - - \* ICS3 : Connections - \* - Determine if any connection handshakes are in progress - LET connectionDatagrams == ConnectionDatagrams(srcChainID, dstChainID) IN - - \* ICS4 : Channels & Packets - \* - Determine if any packets, acknowledgements, or timeouts need to be relayed - LET channelDatagrams == ChannelDatagrams(srcChainID, dstChainID) IN - - [src |-> clientDatagrams.src - \union - connectionDatagrams.src - \union - channelDatagrams.src, - dst |-> clientDatagrams.dst - \union - connectionDatagrams.dst - \union - channelDatagrams.dst] - - - -(*************** -Relayer actions -***************) - -\* Update the height of the relayer client for some chainID -UpdateRelayerClients == - \E chainID \in ChainIDs : - /\ relayerClientHeights[GetClientID(chainID)] < GetLatestHeight(chainID) - /\ relayerClientHeights' = [relayerClientHeights EXCEPT - ![GetClientID(chainID)] = GetLatestHeight(chainID) - ] - /\ UNCHANGED <> - -\* for two chains, srcChainID and dstChainID, -\* where srcChainID /= dstChainID, and where the -\* relayer clients for srcChainID and dstChainID -\* are initialized (i.e., their height is not nullHeight), -\* create the pending datagrams and update the -\* corresponding sets of pending datagrams -Relay == - \E srcChainID \in ChainIDs : - \E dstChainID \in ChainIDs : - /\ srcChainID /= dstChainID - /\ relayerClientHeights[GetClientID(srcChainID)] /= nullHeight - /\ relayerClientHeights[GetClientID(dstChainID)] /= nullHeight - /\ LET datagrams == PendingDatagrams(srcChainID, dstChainID) IN - /\ pendingDatagrams' = - [pendingDatagrams EXCEPT - ![srcChainID] = pendingDatagrams[srcChainID] \union datagrams.src, - ![dstChainID] = pendingDatagrams[dstChainID] \union datagrams.dst - ] - /\ UNCHANGED <> - -\* might create state explosion -FaultyRelay == - \E srcChainID \in ChainIDs : - \E dstChainID \in ChainIDs : - LET srcFaultyDatagrams == CHOOSE src \in SUBSET(Datagrams) : TRUE IN - LET dstFaultyDatagrams == CHOOSE dst \in SUBSET(Datagrams) : TRUE IN - /\ pendingDatagrams' = - [pendingDatagrams EXCEPT - ![srcChainID] = pendingDatagrams[srcChainID] \union srcFaultyDatagrams, - ![dstChainID] = pendingDatagrams[dstChainID] \union dstFaultyDatagrams - ] - /\ UNCHANGED <> - -(*************** -Component actions -***************) - -\* Relayer -\* The relayer either -\* - updates its clients, or -\* - relays datagrams between two chains, or -\* - does nothing -Relayer == - \/ UpdateRelayerClients - \/ Relay -\* \/ FaultyRelay - \/ UNCHANGED vars - -\* Environment -\* The environment takes the action Env!Next -\* and leaves the relayer variable unchanged -Environment == - /\ Env!Next - /\ UNCHANGED relayerClientHeights - -(*************** -Specification -***************) - -\* Initial state predicate -\* Initially -\* - it is either the relayer's or the environment's turn -\* - the relayer clients are uninitialized (i.e., their height -\* is nullHeight -\* - the environment is initialized, by Env!Init -Init == - /\ turn \in {"relayer", "environment"} - /\ relayerClientHeights = [clientID \in ClientIDs |-> 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 == - /\ WF_<>(UpdateRelayerClients) - /\ WF_<>(Relay) - /\ Env!Fairness - -\* Spec formula -Spec == Init /\ [][Next]_vars /\ Fairness - -(************ -Invariants -************) - -\* Type invariant -TypeOK == - /\ turn \in {"relayer", "environment"} - /\ relayerClientHeights \in [ClientIDs -> Heights \union {nullHeight}] - /\ Env!TypeOK - -\* CreateClientInv -\* if a "CreateClient" datagram is in pendingDatagrams for chainID, -\* then the clientID of the datagram is the counterparty clientID for chainID -CreateClientInv == - \A chainID \in ChainIDs : \A clID \in ClientIDs : \A h \in Heights : - [type |-> "CreateClient", clientID |-> clID, height |-> h] \in pendingDatagrams[chainID] - => clID = GetCounterpartyClientID(chainID) - -\* if a "ClientUpdate" datagram is in pendingDatagrams for chainID, -\* then the clientID of the datagram is the counterparty clientID for chainID -ClientUpdateInv == - \A chainID \in ChainIDs : \A clID \in ClientIDs : \A h \in Heights : - [type |-> "ClientUpdate", clientID |-> clID, height |-> h] \in pendingDatagrams[chainID] - => clID = GetCounterpartyClientID(chainID) - -\* "CreateClient" datagrams are created -CreateClientIsGenerated == - [](\A chainID \in ChainIDs : - GetCounterpartyClientHeight(chainID) = nullHeight - => <>(\E h \in Heights : - [type |-> "CreateClient", clientID |-> GetCounterpartyClientID(chainID), height |-> h] - \in pendingDatagrams[chainID])) - -\* Inv -\* A conjunction of all invariants -Inv == - /\ TypeOK - /\ CreateClientInv - /\ ClientUpdateInv - -============================================================================= -\* Modification History -\* Last modified Wed Mar 25 17:49:56 CET 2020 by ilinastoilkovska -\* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska