From 5becdb64e345311eb4bfeec044e543fe70c95241 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Fri, 3 Apr 2020 16:43:54 +0200 Subject: [PATCH 1/7] added connection datagrams --- verification/spec/relayer/README.md | 11 +- verification/spec/relayer/environment.tla | 385 ++++++++++++++++------ verification/spec/relayer/relayer.tla | 351 +++++++++++++++----- 3 files changed, 557 insertions(+), 190 deletions(-) diff --git a/verification/spec/relayer/README.md b/verification/spec/relayer/README.md index 617edb9b2d..a48fd99e69 100644 --- a/verification/spec/relayer/README.md +++ b/verification/spec/relayer/README.md @@ -4,7 +4,10 @@ The specification has two modules: - `relayer.tla` (the main module) - `environment.tla` (the environment module) -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. +Currently, the relayer and the environment can only handle ICS 002 Client datagrams +and ICS 003 Connection datagrams. To import the specification in the TLA+ toolbox and run TLC: - add the spec `relayer.tla` in TLA+ toolbox @@ -12,6 +15,8 @@ To import the specification in the TLA+ toolbox and run TLC: - 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 invariants `Inv` (a conjunction of the invariants `TypeOK`, `CreateClientInv`, + `ClientUpdateInv`) + - add the properties `CreateClientIsGenerated`, `ClientCreated`, `ClientUpdateIsGenerated`, + `ClientUpdated`, `ConnOpenInitIsGenerated`, `ConnnectionOpened`, `HeightsDontDecrease` - run TLC on the model diff --git a/verification/spec/relayer/environment.tla b/verification/spec/relayer/environment.tla index 2ebc89e410..fcbae1c073 100644 --- a/verification/spec/relayer/environment.tla +++ b/verification/spec/relayer/environment.tla @@ -11,13 +11,48 @@ vars == <> ChainIDs == {"chainA", "chainB"} ClientIDs == {"clA", "clB"} +ConnectionIDs == {"connAtoB", "connBtoA"} Heights == 1..MaxHeight -nullClientID == 0 +nullClientID == "none" +nullConnectionID == "none" nullHeight == 0 +ConnectionStates == {"UNINIT", "INIT", "TRYOPEN", "OPEN"} + Max(S) == CHOOSE x \in S: \A y \in S: y <= x +(*** 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. + + - TODO: add channel +**************) +ConnectionEnds == + [ + state : ConnectionStates, + connectionID : ConnectionIDs \union {nullConnectionID}, + clientID : ClientIDs \union {nullClientID}, + counterpartyConnectionID : ConnectionIDs \union {nullConnectionID}, + counterpartyClientID : ClientIDs \union {nullClientID} + ] + (*** Chains *** A set of chain records. A chain record contains the following fields: @@ -27,11 +62,15 @@ Max(S) == CHOOSE x \in S: \A y \in S: y <= x - counterpartyClientHeight : an integer between nullHeight and MaxHeight Stores the height 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}, - counterpartyClientHeight : Heights \union {nullHeight} + counterpartyClientHeight : Heights \union {nullHeight}, + connectionEnd : ConnectionEnds ] (*** Datagrams *** @@ -40,18 +79,31 @@ Chains == Datagrams == [type : {"CreateClient"}, clientID : ClientIDs, height : Heights] \union - [type : {"ClientUpdate"}, clientID : ClientIDs, height : Heights] + [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] (*************** 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 + chains[chainID].height + +\* get the height of the client for chainID's counterparty chain GetCounterpartyClientHeight(chainID) == chains[chainID].counterpartyClientHeight + +\* get the chain identifier 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) == @@ -59,60 +111,106 @@ GetClientID(chainID) == \* get the client ID of the client for the counterparty of chainID GetCounterpartyClientID(chainID) == - IF chainID = "chainA" THEN "clB" ELSE "clA" + IF chainID = "chainA" THEN "clB" ELSE "clA" + +\* 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 + +\* 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 the counterparty of chainID +GetCounterpartyConnectionID(chainID) == + IF chainID = "chainA" + THEN "connBtoA" + ELSE IF chainID = "chainB" + THEN "connAtoB" + ELSE nullConnectionID + +\* 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 OPEN +IsConnectionOpen(chainID) == + chains[chainID].connectionEnd.state = "OPEN" + (*************** -Light client update operators +Client update operators ***************) \* Handle "CreateClient" datagrams HandleCreateClient(chainID, chain, datagrams) == - \* get "CreateClient" datagrams - LET createClients == {dgr \in datagrams : dgr.type = "CreateClient"} IN + \* 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 createClients : - /\ dgr.clientID = GetCounterpartyClientID(chainID) - /\ dgr.height = h} IN + LET createClientHeights == {h \in Heights : \E dgr \in createClientDgrs : dgr.height = h} IN \* new chain record with clients created - LET clientsCreated == [ + LET clientCreateChain == [ height |-> chain.height, counterpartyClientHeight |-> IF createClientHeights /= {} THEN Max(createClientHeights) - ELSE chain.counterpartyClientHeight + ELSE chain.counterpartyClientHeight, + connectionEnd |-> chain.connectionEnd ] IN - clientsCreated + + IF chain.counterpartyClientHeight = nullHeight + \* if the counterparty client height is null, create the client + THEN clientCreateChain + \* otherwise, do not update the chain + ELSE chain \* Handle "ClientUpdate" datagrams HandleUpdateClient(chainID, chain, datagrams) == - \* get "ClientUpdate" datagrams - LET updateClients == {dgr \in datagrams : dgr.type = "ClientUpdate"} IN + \* get "ClientUpdate" datagrams with valid clientID + LET updateClientDgrs == {dgr \in datagrams : + /\ dgr.type = "ClientUpdate" + /\ dgr.clientID = GetCounterpartyClientID(chainID)} 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 + LET updateClientHeights == {h \in Heights : \E dgr \in updateClientDgrs : dgr.height = h} IN \* new chain record with clients updated - LET clientsUpdated == [ + LET clientUpdatedChain == [ height |-> chain.height, counterpartyClientHeight |-> IF updateClientHeights /= {} THEN Max(updateClientHeights) - ELSE chain.counterpartyClientHeight + ELSE chain.counterpartyClientHeight, + connectionEnd |-> chain.connectionEnd ] IN - clientsUpdated + IF chain.counterpartyClientHeight < clientUpdatedChain.counterpartyClientHeight + \* if the current height of the counterparty client is smaller than the new height, update it + THEN clientUpdatedChain + \* otherwise, do not update the chain + ELSE chain \* 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 + LET clientCreatedChain == HandleCreateClient(chainID, chain, datagrams) IN \* update clients - LET clientsUpdated == HandleUpdateClient(chainID, clientsCreated, datagrams) IN + LET clientUpdatedChain == HandleUpdateClient(chainID, clientCreatedChain, datagrams) IN - clientsUpdated + clientUpdatedChain (*************** Connection update operators @@ -120,37 +218,155 @@ Connection update operators \* Handle "ConnOpenInit" datagrams HandleConnOpenInit(chainID, chain, datagrams) == - \* TODO - chain + \* get "ConnOpenInit" datagrams, with a valid connection ID + LET connOpenInitDgrs == {dgr \in datagrams : + /\ dgr.type = "ConnOpenInit" + /\ dgr.connectionID = GetConnectionID(chainID)} IN + + IF connOpenInitDgrs /= {} + \* if there are valid "ConnOpenInit" datagrams, create a new connection end and update the chain + 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 + ] IN + LET connOpenInitChain == [ + height |-> chain.height, + counterpartyClientHeight |-> chain.counterpartyClientHeight, + connectionEnd |-> connOpenInitConnectionEnd + ] IN + + \* TODO: check here if connection is already in INIT? + connOpenInitChain + \* otherwise, do not update the chain + ELSE chain +\* TODO height check \* Handle "ConnOpenTry" datagrams HandleConnOpenTry(chainID, chain, datagrams) == - \* TODO - chain - + \* 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 <= chain.counterpartyClientHeight} 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 + ] 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 == [ + height |-> chain.height, + counterpartyClientHeight |-> chain.counterpartyClientHeight, + connectionEnd |-> connOpenTryConnectionEnd + ] IN + + \* TODO: check here if connection is already in TRYOPEN? + connOpenTryChain + \* otherwise, do not update the chain + ELSE chain + \* otherwise, do not update the chain + ELSE chain + +\* TODO look at code for height check \* Handle "ConnOpenAck" datagrams HandleConnOpenAck(chainID, chain, datagrams) == - \* TODO - chain - + \* 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} 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 == [ + state |-> "OPEN", + connectionID |-> connOpenAckDgr.connectionID, + clientID |-> chain.connectionEnd.clientID, + counterpartyConnectionID |-> chain.connectionEnd.counterpartyConnectionID, + counterpartyClientID |-> chain.connectionEnd.counterpartyClientID + ] IN + LET connOpenAckChain == [ + height |-> chain.height, + counterpartyClientHeight |-> chain.counterpartyClientHeight, + connectionEnd |-> connOpenAckConnectionEnd + ] IN + + \* TODO: check here if connection is already in OPEN? + connOpenAckChain + \* otherwise, do not update the chain + ELSE chain + \* otherwise, do not update the chain + ELSE chain + +\* TODO look at code for height check \* Handle "ConnOpenConfirm" datagrams HandleConnOpenConfirm(chainID, chain, datagrams) == - \* TODO - chain + \* get "ConnOpenConfirm" datagrams, with a valid connection ID and valid height + LET connOpenConfirmDgrs == {dgr \in datagrams : + /\ dgr.type = "ConnOpenConfirm" + /\ dgr.connectionID = GetConnectionID(chainID)} 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 == [ + state |-> "OPEN", + connectionID |-> connOpenConfirmDgr.connectionID, + clientID |-> chain.connectionEnd.clientID, + counterpartyConnectionID |-> chain.connectionEnd.counterpartyConnectionID, + counterpartyClientID |-> chain.connectionEnd.counterpartyClientID + ] IN + LET connOpenConfirmChain == [ + height |-> chain.height, + counterpartyClientHeight |-> chain.counterpartyClientHeight, + connectionEnd |-> connOpenConfirmConnectionEnd + ] IN + + \* TODO: check here if connection is already in OPEN? + connOpenConfirmChain + \* otherwise, do not update the chain + ELSE chain + \* otherwise, do not update the chain + ELSE 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 + LET connOpenInitChain == HandleConnOpenInit(chainID, chain, datagrams) IN \* update chain with "ConnOpenTry" datagrams - LET connTry == HandleConnOpenTry(chainID, connInit, datagrams) IN + LET connOpenTryChain == HandleConnOpenTry(chainID, connOpenInitChain, datagrams) IN \* update chain with "ConnOpenAck" datagrams - LET connAck == HandleConnOpenAck(chainID, connTry, datagrams) IN + LET connOpenAckChain == HandleConnOpenAck(chainID, connOpenTryChain, datagrams) IN \* update chain with "ConnOpenConfirm" datagrams - LET connConfirm == HandleConnOpenConfirm(chainID, connAck, datagrams) IN + LET connOpenConfirmChain == HandleConnOpenConfirm(chainID, connOpenAckChain, datagrams) IN - connConfirm + connOpenConfirmChain (*************** Channel update operators @@ -233,12 +449,27 @@ ReceiveDatagrams == /\ pendingDatagrams' = [pendingDatagrams EXCEPT ![chainID] = {} ] + + +\* 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] + \* 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, - counterpartyClientHeight |-> nullHeight] + counterpartyClientHeight |-> nullHeight, + connectionEnd |-> InitConnectionEnd] (*************** Specification @@ -275,69 +506,7 @@ 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 +\* Last modified Fri Apr 03 16:36:29 CEST 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 index 145313c859..85c8c66a36 100644 --- a/verification/spec/relayer/relayer.tla +++ b/verification/spec/relayer/relayer.tla @@ -6,7 +6,7 @@ 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 + relayerChainHeights, \* a function that assigns to each ClientID a height turn @@ -17,16 +17,18 @@ Env == INSTANCE environment pendingDatagrams <- pendingDatagrams, MaxHeight <- MaxHeight -vars == <> +vars == <> envVars == <> ChainIDs == Env!ChainIDs ClientIDs == Env!ClientIDs +ConnectionIDs == Env!ConnectionIDs Heights == Env!Heights RelayerClientIDs == Env!ClientIDs -nullClientID == 0 -nullHeight == 0 +nullClientID == Env!nullClientID +nullConnectionID == Env!nullConnectionID +nullHeight == Env!nullHeight (*** Datagrams *** @@ -40,48 +42,155 @@ 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 +\* get the height of the client for chainID's counterparty chain GetCounterpartyClientHeight(chainID) == Env!GetCounterpartyClientHeight(chainID) +\* get the ID of the counterparty chain of chainID +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 the counterparty chain of chainID 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 height +CounterpartyClientHeightUpdated(chainID, height) == Env!CounterpartyClientHeightUpdated(chainID, height) + +\* get the connection ID of the connection end at chainID +GetConnectionID(chainID) == Env!GetConnectionID(chainID) + +\* get the connection ID of the connection end at the counterparty of chainID +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 OPEN +IsConnectionOpen(chainID) == Env!IsConnectionOpen(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 +\* Compute client datagrams for clients for srcChainID on dstChainID +\* 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 == GetCounterpartyClientHeight(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 - LET srcDatagrams == - IF dstClientHeight = nullHeight - THEN \* the dst client does not exist on the src chain + \* generate datagrams for dstChainID + LET dstDatagrams == + IF srcClientHeight = nullHeight + THEN \* the src client does not exist on dstChainID {[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 + 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 |-> relayerClientHeights[dstClientID], - clientID |-> dstClientID]} + height |-> srcChainHeight, + clientID |-> srcClientID]} ELSE {} IN - srcDatagrams + [datagrams|-> dstDatagrams, relayerUpdate |-> updatedRelayer] + +\* Get the client datagrams for clients on srcChainID and on dstChainID, +\* as well as the relayer update triggered by creating client datagrams +ClientDatagrams(srcChainID, dstChainID) == + \* get the client datagrams for dstChainID + \* and relayer update triggered by difference between the height of + \* srcChainID and the height that the relayer stores for srcChainID + LET dstLightClientUpdates == + LightClientUpdates(srcChainID, dstChainID, relayerChainHeights) IN + LET dstClientDatagrams == + dstLightClientUpdates.datagrams IN + LET dstRelayerUpdate == + dstLightClientUpdates.relayerUpdate IN + + \* get the client datagrams for srcChainID + \* and relayer update triggered by difference between the height of + \* dstChainID and the height that the relayer stores for dstChainID + LET srcLightClientUpdates == + LightClientUpdates(dstChainID, srcChainID, dstRelayerUpdate) IN + LET srcClientDatagrams == + srcLightClientUpdates.datagrams IN + LET srcRelayerUpdate == + srcLightClientUpdates.relayerUpdate IN + + [src |-> srcClientDatagrams, dst |-> dstClientDatagrams, relayerUpdate |-> srcRelayerUpdate] + (*************** Connection datagrams ****************) +\* Compute connection datagrams that are sent to dstChainID +ComputeConnectionDatagrams(srcChainID, dstChainID) == + LET srcEnd == GetConnectionEnd(srcChainID) IN + LET dstEnd == GetConnectionEnd(dstChainID) IN + + LET srcConnectionID == GetConnectionID(srcChainID) IN + LET dstConnectionID == GetConnectionID(dstChainID) IN + + LET srcHeight == GetLatestHeight(srcChainID) IN + LET srcConsensusHeight == GetCounterpartyClientHeight(srcChainID) IN + + IF dstEnd.state = "UNINIT" /\ srcEnd.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 srcEnd.state = "INIT" /\ \/ dstEnd.state = "UNINIT" + \/ dstEnd.state = "INIT" + THEN {[type |-> "ConnOpenTry", + desiredConnectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + clientID |-> srcEnd.counterpartyClientID, \* "clA" + counterpartyConnectionID |-> srcConnectionID, \* "connAtoB" + counterpartyClientID |-> srcEnd.clientID, \* "clB" + proofHeight |-> srcHeight, + consensusHeight |-> srcConsensusHeight]} + + ELSE IF srcEnd.state = "TRYOPEN" /\ \/ dstEnd.state = "INIT" + \/ dstEnd.state = "TRYOPEN" + THEN {[type |-> "ConnOpenAck", + connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + proofHeight |-> srcHeight, + consensusHeight |-> srcConsensusHeight]} + + ELSE IF srcEnd.state = "OPEN" /\ dstEnd.state = "TRYOPEN" + THEN {[type |-> "ConnOpenConfirm", + connectionID |-> dstEnd.connectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + proofHeight |-> srcHeight]} + ELSE {} + +\* Get the connection datagrams designated for srcChainID and dstChainID ConnectionDatagrams(srcChainID, dstChainID) == - \* TODO - [src |-> {}, dst |-> {}] + LET srcConnectionDatagrams == ComputeConnectionDatagrams(dstChainID, srcChainID) IN + LET dstConnectionDatagrams == ComputeConnectionDatagrams(srcChainID, dstChainID) IN + + [src |-> srcConnectionDatagrams, dst |-> dstConnectionDatagrams] (*************** Channel datagrams @@ -100,8 +209,7 @@ Compute pending 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 + LET clientDatagrams == ClientDatagrams(srcChainID, dstChainID) IN \* ICS3 : Connections \* - Determine if any connection handshakes are in progress @@ -111,16 +219,9 @@ PendingDatagrams(srcChainID, dstChainID) == \* - 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] + [src |-> clientDatagrams.src \union connectionDatagrams.src \union channelDatagrams.src, + dst |-> clientDatagrams.dst \union connectionDatagrams.dst \union channelDatagrams.dst, + relayerUpdate |-> clientDatagrams.relayerUpdate] @@ -131,9 +232,9 @@ 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) + /\ relayerChainHeights[chainID] < GetLatestHeight(chainID) + /\ relayerChainHeights' = [relayerChainHeights EXCEPT + ![chainID] = GetLatestHeight(chainID) ] /\ UNCHANGED <> @@ -147,29 +248,15 @@ 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 + /\ LET datagramsAndRelayerUpdate == PendingDatagrams(srcChainID, dstChainID) IN /\ pendingDatagrams' = [pendingDatagrams EXCEPT - ![srcChainID] = pendingDatagrams[srcChainID] \union datagrams.src, - ![dstChainID] = pendingDatagrams[dstChainID] \union datagrams.dst + ![srcChainID] = pendingDatagrams[srcChainID] \union datagramsAndRelayerUpdate.src, + ![dstChainID] = pendingDatagrams[dstChainID] \union datagramsAndRelayerUpdate.dst ] - /\ UNCHANGED <> + /\ relayerChainHeights' = datagramsAndRelayerUpdate.relayerUpdate + /\ UNCHANGED chains -\* 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 ***************) @@ -182,7 +269,6 @@ Component actions Relayer == \/ UpdateRelayerClients \/ Relay -\* \/ FaultyRelay \/ UNCHANGED vars \* Environment @@ -190,7 +276,7 @@ Relayer == \* and leaves the relayer variable unchanged Environment == /\ Env!Next - /\ UNCHANGED relayerClientHeights + /\ UNCHANGED relayerChainHeights (*************** Specification @@ -199,12 +285,12 @@ 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 relayer chain heights 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] + /\ relayerChainHeights = [chainID \in ChainIDs |-> nullHeight] /\ Env!Init \* Next state action @@ -221,13 +307,45 @@ Next == \* Fairness constraints Fairness == - /\ WF_<>(UpdateRelayerClients) - /\ WF_<>(Relay) + /\ WF_<>(UpdateRelayerClients) + /\ WF_<>(Relay) /\ Env!Fairness \* Spec formula Spec == Init /\ [][Next]_vars /\ Fairness +(************ +Helper operators used in properties +************) + +\* returns true if there is a "CreateClient" datagram +\* in the pending datagrams for chainID and height h +IsCreateClientInPendingDatagrams(chainID, clID, h) == + [type |-> "CreateClient", clientID |-> clID, height |-> h] + \in pendingDatagrams[chainID] + +\* returns true if there is a "ClientUpdate" datagram +\* in the pending datagrams for chainID and height h +IsClientUpdateInPendingDatagrams(chainID, clID, h) == + [type |-> "ClientUpdate", clientID |-> clID, height |-> h] + \in pendingDatagrams[chainID] + +\* returns true if a "ConnOpenInit" datagram for a connection +\* with counterpartyChainID is in pending datagrams of chainID +IsConnOpenInitInPendingDatagrams(chainID, counterpartyChainID) == + LET connectionID == GetConnectionID(chainID) IN + LET clientID == GetCounterpartyClientID(chainID) IN + LET counterpartyConnectionID == GetConnectionID(counterpartyChainID) IN + LET counterpartyClientID == GetCounterpartyClientID(counterpartyChainID) IN + + [type |-> "ConnOpenInit", + connectionID |-> connectionID, + clientID |-> clientID, + counterpartyConnectionID |-> counterpartyConnectionID, + counterpartyClientID |-> counterpartyClientID] \in pendingDatagrams[chainID] + + + (************ Invariants ************) @@ -235,40 +353,115 @@ Invariants \* Type invariant TypeOK == /\ turn \in {"relayer", "environment"} - /\ relayerClientHeights \in [ClientIDs -> Heights \union {nullHeight}] + /\ relayerChainHeights \in [ChainIDs -> 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) + \A chainID \in ChainIDs : \A clID \in ClientIDs : + ((\E h \in Heights : IsCreateClientInPendingDatagrams(chainID, clID, h)) + => (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] + IsClientUpdateInPendingDatagrams(chainID, clID, h) => 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 + /\ ClientUpdateInv + +(************ +Properties about client datagrams +************) + +\* 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 : + GetCounterpartyClientHeight(chainID) = nullHeight + => <>(\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 : + (/\ GetCounterpartyClientHeight(chainID) = h1 + /\ GetCounterpartyClientHeight(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) + /\ GetCounterpartyClientHeight(chainID) < h) + => (<>(CounterpartyClientHeightUpdated(chainID, h)))) + +(************ +Properties about connection datagrams +************) + +ConnOpenInitIsGenerated == + [](\A chainID \in ChainIDs : + (/\ IsConnectionUninit(chainID) + /\ IsConnectionUninit(GetCounterpartyChainID(chainID))) + => <>(IsConnOpenInitInPendingDatagrams(chainID, GetCounterpartyChainID(chainID)))) + +\* it ALWAYS holds that, for every cahinID, and every counterpartyChainID: +\* - if +\* * there is a "ConnOpenInit" message for the connection between +\* chainID and counterpartyChainID in pending datagrams of chainID +\* * the connection is not open +\* - then +\* * the connection is EVENTUALLY open +ConnectionOpened == + [](\A chainID \in ChainIDs : + IsConnOpenInitInPendingDatagrams(chainID, GetCounterpartyChainID(chainID)) + => (<>(/\ IsConnectionOpen(chainID) + /\ IsConnectionOpen(GetCounterpartyChainID(chainID))))) + +\* 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:49:56 CET 2020 by ilinastoilkovska +\* Last modified Fri Apr 03 16:39:06 CEST 2020 by ilinastoilkovska \* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska From ddf311f8777bcbb200f9979baf117420875d53f3 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Wed, 15 Apr 2020 16:27:00 +0200 Subject: [PATCH 2/7] relayer TLA spec: connection and channel handshake datagrams --- verification/spec/relayer/ChannelHandlers.tla | 172 ++++ verification/spec/relayer/ClientHandlers.tla | 94 +++ .../spec/relayer/ConnectionHandlers.tla | 168 ++++ verification/spec/relayer/Environment.tla | 334 ++++++++ verification/spec/relayer/README.md | 30 +- verification/spec/relayer/Relayer.tla | 769 ++++++++++++++++++ verification/spec/relayer/environment.tla | 512 ------------ verification/spec/relayer/relayer.tla | 467 ----------- 8 files changed, 1554 insertions(+), 992 deletions(-) create mode 100644 verification/spec/relayer/ChannelHandlers.tla create mode 100644 verification/spec/relayer/ClientHandlers.tla create mode 100644 verification/spec/relayer/ConnectionHandlers.tla create mode 100644 verification/spec/relayer/Environment.tla create mode 100644 verification/spec/relayer/Relayer.tla delete mode 100644 verification/spec/relayer/environment.tla delete mode 100644 verification/spec/relayer/relayer.tla diff --git a/verification/spec/relayer/ChannelHandlers.tla b/verification/spec/relayer/ChannelHandlers.tla new file mode 100644 index 0000000000..c3a8b9f6e7 --- /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 chanOpenInitDgrs /= {} /\ chain.connectionEnd.state /= "UNINIT" + \* if there are valid "ChanOpenInit" datagrams and the connection is not "UNINIT", + \* create a new channel end and update the chain + 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 <= chain.counterpartyClientHeight} IN + + IF chanOpenTryDgrs /= {} /\ chain.connectionEnd.state = "OPEN" + \* if there are valid "ChanOpenTry" datagrams and the connection is "OPEN", + \* update the channel end + 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 <= chain.counterpartyClientHeight} IN + + IF chanOpenAckDgrs /= {} /\ chain.connectionEnd.state = "OPEN" + \* if there are valid "ChanOpenAck" datagrams, update the channel end + THEN IF \/ chain.connectionEnd.channelEnd.state = "INIT" + \/ chain.connectionEnd.channelEnd.state = "TRYOPEN" + \* if the channel end on the chain is in "INIT" or it is in "TRYOPEN", + \* update the channel end + 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 <= chain.counterpartyClientHeight} IN + + IF chanOpenConfirmDgrs /= {} /\ chain.connectionEnd.state = "OPEN" + \* if there are valid "ChanOpenConfirm" datagrams, update the channel end + THEN IF chain.connectionEnd.channelEnd.state = "TRYOPEN" + \* if the channel end on the chain is in "TRYOPEN", update the channel end + 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 Wed Apr 15 16:18:59 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..741115121c --- /dev/null +++ b/verification/spec/relayer/ClientHandlers.tla @@ -0,0 +1,94 @@ +-------------------------- 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 + ***************************************************************************) + +\* 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, + counterpartyClientHeight |-> IF createClientHeights /= {} + THEN Max(createClientHeights) + ELSE chain.counterpartyClientHeight, + connectionEnd |-> chain.connectionEnd + ] IN + + IF chain.counterpartyClientHeight = nullHeight + \* if the counterparty client height is null, create the client + THEN clientCreateChain + \* otherwise, do not update the chain + ELSE chain + +\* Handle "ClientUpdate" datagrams +HandleUpdateClient(chainID, chain, datagrams) == + \* get "ClientUpdate" datagrams with valid clientID + LET updateClientDgrs == {dgr \in datagrams : + /\ dgr.type = "ClientUpdate" + /\ dgr.clientID = GetCounterpartyClientID(chainID)} 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, + counterpartyClientHeight |-> IF updateClientHeights /= {} + THEN Max(updateClientHeights) + ELSE chain.counterpartyClientHeight, + connectionEnd |-> chain.connectionEnd + ] IN + +\* IF chain.counterpartyClientHeight < clientUpdatedChain.counterpartyClientHeight + \* if the current height of the counterparty client is smaller than the new height, update it +\* THEN clientUpdatedChain + \* otherwise, do not update the chain +\* ELSE chain + clientUpdatedChain + + +============================================================================= +\* Modification History +\* Last modified Wed Apr 15 16:17:39 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..07ccdd673a --- /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 connOpenInitDgrs /= {} + \* if there are valid "ConnOpenInit" datagrams, create a new connection end and update the chain + \* TODO: check here if connection is already in INIT? + 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 <= chain.counterpartyClientHeight} 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} 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)} 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 Wed Apr 15 16:18:37 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..67fecf272b --- /dev/null +++ b/verification/spec/relayer/Environment.tla @@ -0,0 +1,334 @@ +---------------------------- 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 + pendingDatagrams \* a function that assigns a set of pending datagrams 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. + + - counterpartyClientHeight : an integer between nullHeight and MaxHeight + Stores the height 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}, + counterpartyClientHeight : Heights \union {nullHeight}, + 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 height of the client for chainID's counterparty chain +GetCounterpartyClientHeight(chainID) == + chains[chainID].counterpartyClientHeight + +\* 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 h +CounterpartyClientHeightUpdated(chainID, h) == + chains[chainID].counterpartyClientHeight >= h + +\* 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 +\* 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(chainID) == + /\ chains[chainID].height < MaxHeight + /\ chains' = [chains EXCEPT + ![chainID].height = chains[chainID].height + 1 + ] + /\ UNCHANGED pendingDatagrams + +\* Receive the datagrams and update the chain state +ReceiveDatagrams(chainID) == + /\ pendingDatagrams[chainID] /= {} + /\ chains' = [chains EXCEPT + ![chainID] = UpdateChain(chainID, pendingDatagrams[chainID]) + ] + /\ pendingDatagrams' = [pendingDatagrams 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, + counterpartyClientHeight |-> nullHeight, + 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] + /\ pendingDatagrams = [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) + \/ ReceiveDatagrams(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(ReceiveDatagrams(chainID)) + +(*************************************************************************** + Invariants + ***************************************************************************) +\* Type invariant +TypeOK == + /\ chains \in [ChainIDs -> Chains] + /\ pendingDatagrams \in [ChainIDs -> SUBSET Datagrams] + +============================================================================= +\* Modification History +\* Last modified Wed Apr 15 16:18:18 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 a48fd99e69..358a23a271 100644 --- a/verification/spec/relayer/README.md +++ b/verification/spec/relayer/README.md @@ -1,22 +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 -and ICS 003 Connection 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`, `ClientCreated`, `ClientUpdateIsGenerated`, - `ClientUpdated`, `ConnOpenInitIsGenerated`, `ConnnectionOpened`, `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..4bbe16e4d7 --- /dev/null +++ b/verification/spec/relayer/Relayer.tla @@ -0,0 +1,769 @@ +------------------------------ 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 + pendingDatagrams, \* a function that assigns a set of pending datagrams to each chainID + relayerChainHeights, \* a function that assigns a height to each chainID + turn + +vars == <> +envVars == <> + +\* Instance of the module Environment, which encodes the chain logic +Env == INSTANCE Environment + WITH chains <- chains, + pendingDatagrams <- pendingDatagrams, + 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 +GetCounterpartyClientHeight(chainID) == Env!GetCounterpartyClientHeight(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 == GetCounterpartyClientHeight(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] + +\* Get the client datagrams for clients on srcChainID and on dstChainID, +\* as well as the relayer update triggered by creating client datagrams +ClientDatagrams(srcChainID, dstChainID) == + \* get the client datagrams for dstChainID + \* and relayer update triggered by difference between the height of + \* srcChainID and the height that the relayer stores for srcChainID + LET dstLightClientUpdates == + LightClientUpdates(srcChainID, dstChainID, relayerChainHeights) IN + LET dstClientDatagrams == + dstLightClientUpdates.datagrams IN + LET dstRelayerUpdate == + dstLightClientUpdates.relayerUpdate IN + + \* get the client datagrams for srcChainID + \* and relayer update triggered by difference between the height of + \* dstChainID and the height that the relayer stores for dstChainID + LET srcLightClientUpdates == + LightClientUpdates(dstChainID, srcChainID, dstRelayerUpdate) IN + LET srcClientDatagrams == + srcLightClientUpdates.datagrams IN + LET srcRelayerUpdate == + srcLightClientUpdates.relayerUpdate IN + + [src |-> srcClientDatagrams, dst |-> dstClientDatagrams, relayerUpdate |-> srcRelayerUpdate] + +(*************************************************************************** + Connection datagrams + ***************************************************************************) +\* Compute connection datagrams designated for dstChainID. +\* These are used to update the connection end on dstChainID in the environment. +ComputeConnectionDatagrams(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 == GetCounterpartyClientHeight(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 {} + +\* Get the connection datagrams designated for srcChainID and dstChainID +ConnectionDatagrams(srcChainID, dstChainID) == + \* connection datagrams from dstChainID to srcChainID + LET srcConnectionDatagrams == ComputeConnectionDatagrams(dstChainID, srcChainID) IN + \* connection datagrams from srcChainID to dstChainID + LET dstConnectionDatagrams == ComputeConnectionDatagrams(srcChainID, dstChainID) IN + + [src |-> srcConnectionDatagrams, dst |-> dstConnectionDatagrams] + +(*************************************************************************** + Channel datagrams + ***************************************************************************) +\* Compute channel datagrams designated for dstChainID. +\* These are used to update the channel end on dstChainID in the environment. +ComputeChannelDatagrams(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 {} + + +\* Get the channel datagrams designated for srcChainID and dstChainID +ChannelDatagrams(srcChainID, dstChainID) == + \* channel datagrams from dstChainID to srcChainID + LET srcChannelDatagrams == ComputeChannelDatagrams(dstChainID, srcChainID) IN + \* channel datagrams from srcChainID to dstChainID + LET dstChannelDatagrams == ComputeChannelDatagrams(srcChainID, dstChainID) IN + + [src |-> srcChannelDatagrams, dst |-> dstChannelDatagrams] + +(*************************************************************************** + Compute pending datagrams + ***************************************************************************) +\* 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 == ClientDatagrams(srcChainID, dstChainID) 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 + + [src |-> clientDatagrams.src \union connectionDatagrams.src \union channelDatagrams.src, + dst |-> clientDatagrams.dst \union connectionDatagrams.dst \union channelDatagrams.dst, + relayerUpdate |-> clientDatagrams.relayerUpdate] + +(*************************************************************************** + Relayer actions + ***************************************************************************) +\* Update the height of the relayer client for some chainID +UpdateRelayerClients == + \E chainID \in ChainIDs : + /\ 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 == + \E srcChainID \in ChainIDs : + \E dstChainID \in ChainIDs : + /\ srcChainID /= dstChainID + /\ LET datagramsAndRelayerUpdate == PendingDatagrams(srcChainID, dstChainID) IN + /\ pendingDatagrams' = + [pendingDatagrams EXCEPT + ![srcChainID] = pendingDatagrams[srcChainID] \union datagramsAndRelayerUpdate.src, + ![dstChainID] = pendingDatagrams[dstChainID] \union datagramsAndRelayerUpdate.dst + ] + /\ relayerChainHeights' = datagramsAndRelayerUpdate.relayerUpdate + /\ UNCHANGED chains + +(*************************************************************************** + Component actions + ***************************************************************************) +\* Relayer +\* The relayer either +\* - updates its clients, or +\* - relays datagrams between two chains, or +\* - does nothing +Relayer == + \/ UpdateRelayerClients + \/ Relay + \/ 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 == + /\ WF_<>(UpdateRelayerClients) + /\ WF_<>(Relay) + /\ Env!Fairness + +\* Spec formula +Spec == Init /\ [][Next]_vars /\ Fairness + +(*************************************************************************** + Helper operators used in properties + ***************************************************************************) +\* returns true if there is a "CreateClient" datagram +\* in pending datagrams of chainID +IsCreateClientInPendingDatagrams(chainID, clID, h) == + [type |-> "CreateClient", clientID |-> clID, height |-> h] + \in pendingDatagrams[chainID] + +\* returns true if there is a "ClientUpdate" datagram +\* in pending datagrams of chainID +IsClientUpdateInPendingDatagrams(chainID, clID, h) == + [type |-> "ClientUpdate", clientID |-> clID, height |-> h] + \in pendingDatagrams[chainID] + +\* returns true if there is a "ConnOpenInit" datagram +\* in pending datagrams of chainID +IsConnOpenInitInPendingDatagrams( + chainID, clientID, counterpartyClientID, + connectionID, counterpartyConnectionID + ) == + + [type |-> "ConnOpenInit", + connectionID |-> connectionID, + clientID |-> clientID, + counterpartyConnectionID |-> counterpartyConnectionID, + counterpartyClientID |-> counterpartyClientID] \in pendingDatagrams[chainID] + +\* returns true if there is a "ConnOpenTry" datagram +\* in pending datagrams of 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 pendingDatagrams[chainID] + +\* returns true if there is a "ConnOpenAck" datagram +\* in pending datagrams of chainID +IsConnOpenAckInPendingDatagrams(chainID, connectionID) == + \E pHeight \in Heights : \E cHeight \in Heights : + [type |-> "ConnOpenAck", + connectionID |-> connectionID, + proofHeight |-> pHeight, + consensusHeight |-> cHeight] \in pendingDatagrams[chainID] + +\* returns true if there is a "ConnOpenConfirm" datagram +\* in pending datagrams of chainID +IsConnOpenConfirmInPendingDatagrams(chainID, connectionID) == + \E pHeight \in Heights : + [type |-> "ConnOpenConfirm", + connectionID |-> connectionID, + proofHeight |-> pHeight] \in pendingDatagrams[chainID] + +\* returns true if there is a "ChanOpenInit" datagram +\* in pending datagrams of chainID +IsChanOpenInitInPendingDatagrams(chainID, channelID, counterpartyChannelID) == + [type |-> "ChanOpenInit", + channelID |-> channelID, + counterpartyChannelID |-> counterpartyChannelID] \in pendingDatagrams[chainID] + +\* returns true if there is a "ChanOpenTry" datagram +\* in pending datagrams of chainID +IsChanOpenTryInPendingDatagrams(chainID, channelID, counterpartyChannelID) == + \E pHeight \in Heights : + [type |-> "ChanOpenTry", + channelID |-> channelID, + counterpartyChannelID |-> counterpartyChannelID, + proofHeight |-> pHeight] \in pendingDatagrams[chainID] + +\* returns true if there is a "ChanOpenAck" datagram +\* in pending datagrams of chainID +IsChanOpenAckInPendingDatagrams(chainID, channelID) == + \E pHeight \in Heights : + [type |-> "ChanOpenAck", + channelID |-> channelID, + proofHeight |-> pHeight] \in pendingDatagrams[chainID] + +\* returns true if there is a "ChanOpenConfirm" datagram +\* in pending datagrams of chainID +IsChanOpenConfirmInPendingDatagrams(chainID, channelID) == + \E pHeight \in Heights : + [type |-> "ChanOpenConfirm", + channelID |-> channelID, + proofHeight |-> pHeight] \in pendingDatagrams[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) + /\ GetCounterpartyClientHeight(chainID) = nullHeight)) + +\* 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) + /\ GetCounterpartyClientHeight(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 : + GetCounterpartyClientHeight(chainID) = nullHeight + => <>(\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 : + (/\ GetCounterpartyClientHeight(chainID) = h1 + /\ GetCounterpartyClientHeight(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) + /\ GetCounterpartyClientHeight(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 +\* * the relayer EVENTUALLY adds a "ConnOpenInit" datagram in pending datagrams of chainID +ConnOpenInitIsGenerated == + [](\A chainID \in ChainIDs : + (/\ IsConnectionUninit(chainID) + /\ IsConnectionUninit(GetCounterpartyChainID(chainID))) + => <>(IsConnOpenInitInPendingDatagrams( + chainID, GetCounterpartyClientID(chainID), GetClientID(chainID), + GetConnectionID(chainID), GetCounterpartyConnectionID(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) + /\ IsChannelUninit(GetCounterpartyChainID(chainID))) + => <>(IsChanOpenInitInPendingDatagrams(chainID, GetChannelID(chainID), GetCounterpartyChannelID(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 Wed Apr 15 16:25:56 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 fcbae1c073..0000000000 --- a/verification/spec/relayer/environment.tla +++ /dev/null @@ -1,512 +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"} -ConnectionIDs == {"connAtoB", "connBtoA"} -Heights == 1..MaxHeight - -nullClientID == "none" -nullConnectionID == "none" -nullHeight == 0 - -ConnectionStates == {"UNINIT", "INIT", "TRYOPEN", "OPEN"} - -Max(S) == CHOOSE x \in S: \A y \in S: y <= x - -(*** 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. - - - TODO: add channel -**************) -ConnectionEnds == - [ - state : ConnectionStates, - connectionID : ConnectionIDs \union {nullConnectionID}, - clientID : ClientIDs \union {nullClientID}, - counterpartyConnectionID : ConnectionIDs \union {nullConnectionID}, - counterpartyClientID : ClientIDs \union {nullClientID} - ] - -(*** 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. - - - connectionEnd : a connection end record - Stores data about the connection with the counterparty chain -**************) -Chains == - [ - height : Heights \union {nullHeight}, - counterpartyClientHeight : Heights \union {nullHeight}, - 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] - -(*************** -Chain helper operators -***************) -\* get the latest height of the chainID -GetLatestHeight(chainID) == - chains[chainID].height - -\* get the height of the client for chainID's counterparty chain -GetCounterpartyClientHeight(chainID) == - chains[chainID].counterpartyClientHeight - -\* get the chain identifier 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 the counterparty of chainID -GetCounterpartyClientID(chainID) == - IF chainID = "chainA" THEN "clB" ELSE "clA" - -\* 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 - -\* 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 the counterparty of chainID -GetCounterpartyConnectionID(chainID) == - IF chainID = "chainA" - THEN "connBtoA" - ELSE IF chainID = "chainB" - THEN "connAtoB" - ELSE nullConnectionID - -\* 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 OPEN -IsConnectionOpen(chainID) == - chains[chainID].connectionEnd.state = "OPEN" - - -(*************** -Client update operators -***************) - -\* 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, - counterpartyClientHeight |-> IF createClientHeights /= {} - THEN Max(createClientHeights) - ELSE chain.counterpartyClientHeight, - connectionEnd |-> chain.connectionEnd - ] IN - - IF chain.counterpartyClientHeight = nullHeight - \* if the counterparty client height is null, create the client - THEN clientCreateChain - \* otherwise, do not update the chain - ELSE chain - -\* Handle "ClientUpdate" datagrams -HandleUpdateClient(chainID, chain, datagrams) == - \* get "ClientUpdate" datagrams with valid clientID - LET updateClientDgrs == {dgr \in datagrams : - /\ dgr.type = "ClientUpdate" - /\ dgr.clientID = GetCounterpartyClientID(chainID)} 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, - counterpartyClientHeight |-> IF updateClientHeights /= {} - THEN Max(updateClientHeights) - ELSE chain.counterpartyClientHeight, - connectionEnd |-> chain.connectionEnd - ] IN - - IF chain.counterpartyClientHeight < clientUpdatedChain.counterpartyClientHeight - \* if the current height of the counterparty client is smaller than the new height, update it - THEN clientUpdatedChain - \* otherwise, do not update the chain - ELSE chain - -\* 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 -***************) - -\* 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 connOpenInitDgrs /= {} - \* if there are valid "ConnOpenInit" datagrams, create a new connection end and update the chain - 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 - ] IN - LET connOpenInitChain == [ - height |-> chain.height, - counterpartyClientHeight |-> chain.counterpartyClientHeight, - connectionEnd |-> connOpenInitConnectionEnd - ] IN - - \* TODO: check here if connection is already in INIT? - connOpenInitChain - \* otherwise, do not update the chain - ELSE chain - -\* TODO height check -\* 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 <= chain.counterpartyClientHeight} 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 - ] 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 == [ - height |-> chain.height, - counterpartyClientHeight |-> chain.counterpartyClientHeight, - connectionEnd |-> connOpenTryConnectionEnd - ] IN - - \* TODO: check here if connection is already in TRYOPEN? - connOpenTryChain - \* otherwise, do not update the chain - ELSE chain - \* otherwise, do not update the chain - ELSE chain - -\* TODO look at code for height check -\* 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} 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 == [ - state |-> "OPEN", - connectionID |-> connOpenAckDgr.connectionID, - clientID |-> chain.connectionEnd.clientID, - counterpartyConnectionID |-> chain.connectionEnd.counterpartyConnectionID, - counterpartyClientID |-> chain.connectionEnd.counterpartyClientID - ] IN - LET connOpenAckChain == [ - height |-> chain.height, - counterpartyClientHeight |-> chain.counterpartyClientHeight, - connectionEnd |-> connOpenAckConnectionEnd - ] IN - - \* TODO: check here if connection is already in OPEN? - connOpenAckChain - \* otherwise, do not update the chain - ELSE chain - \* otherwise, do not update the chain - ELSE chain - -\* TODO look at code for height check -\* 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)} 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 == [ - state |-> "OPEN", - connectionID |-> connOpenConfirmDgr.connectionID, - clientID |-> chain.connectionEnd.clientID, - counterpartyConnectionID |-> chain.connectionEnd.counterpartyConnectionID, - counterpartyClientID |-> chain.connectionEnd.counterpartyClientID - ] IN - LET connOpenConfirmChain == [ - height |-> chain.height, - counterpartyClientHeight |-> chain.counterpartyClientHeight, - connectionEnd |-> connOpenConfirmConnectionEnd - ] IN - - \* TODO: check here if connection is already in OPEN? - connOpenConfirmChain - \* otherwise, do not update the chain - ELSE chain - \* otherwise, do not update the chain - ELSE 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 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 -***************) - -\* 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 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] - -\* 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, - counterpartyClientHeight |-> nullHeight, - 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] - /\ 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] - -============================================================================= -\* Modification History -\* Last modified Fri Apr 03 16:36:29 CEST 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 85c8c66a36..0000000000 --- a/verification/spec/relayer/relayer.tla +++ /dev/null @@ -1,467 +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 - relayerChainHeights, \* 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 -ConnectionIDs == Env!ConnectionIDs -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 the chainID -GetLatestHeight(chainID) == Env!GetLatestHeight(chainID) - -\* get the height of the client for chainID's counterparty chain -GetCounterpartyClientHeight(chainID) == Env!GetCounterpartyClientHeight(chainID) - -\* get the ID of the counterparty chain of chainID -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 the counterparty chain of chainID -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 height -CounterpartyClientHeightUpdated(chainID, height) == Env!CounterpartyClientHeightUpdated(chainID, height) - -\* get the connection ID of the connection end at chainID -GetConnectionID(chainID) == Env!GetConnectionID(chainID) - -\* get the connection ID of the connection end at the counterparty of chainID -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 OPEN -IsConnectionOpen(chainID) == Env!IsConnectionOpen(chainID) - -(*************** -Client datagrams -****************) - -\* Compute client datagrams for clients for srcChainID on dstChainID -\* 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 == GetCounterpartyClientHeight(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] - -\* Get the client datagrams for clients on srcChainID and on dstChainID, -\* as well as the relayer update triggered by creating client datagrams -ClientDatagrams(srcChainID, dstChainID) == - \* get the client datagrams for dstChainID - \* and relayer update triggered by difference between the height of - \* srcChainID and the height that the relayer stores for srcChainID - LET dstLightClientUpdates == - LightClientUpdates(srcChainID, dstChainID, relayerChainHeights) IN - LET dstClientDatagrams == - dstLightClientUpdates.datagrams IN - LET dstRelayerUpdate == - dstLightClientUpdates.relayerUpdate IN - - \* get the client datagrams for srcChainID - \* and relayer update triggered by difference between the height of - \* dstChainID and the height that the relayer stores for dstChainID - LET srcLightClientUpdates == - LightClientUpdates(dstChainID, srcChainID, dstRelayerUpdate) IN - LET srcClientDatagrams == - srcLightClientUpdates.datagrams IN - LET srcRelayerUpdate == - srcLightClientUpdates.relayerUpdate IN - - [src |-> srcClientDatagrams, dst |-> dstClientDatagrams, relayerUpdate |-> srcRelayerUpdate] - - -(*************** -Connection datagrams -****************) - -\* Compute connection datagrams that are sent to dstChainID -ComputeConnectionDatagrams(srcChainID, dstChainID) == - LET srcEnd == GetConnectionEnd(srcChainID) IN - LET dstEnd == GetConnectionEnd(dstChainID) IN - - LET srcConnectionID == GetConnectionID(srcChainID) IN - LET dstConnectionID == GetConnectionID(dstChainID) IN - - LET srcHeight == GetLatestHeight(srcChainID) IN - LET srcConsensusHeight == GetCounterpartyClientHeight(srcChainID) IN - - IF dstEnd.state = "UNINIT" /\ srcEnd.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 srcEnd.state = "INIT" /\ \/ dstEnd.state = "UNINIT" - \/ dstEnd.state = "INIT" - THEN {[type |-> "ConnOpenTry", - desiredConnectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - clientID |-> srcEnd.counterpartyClientID, \* "clA" - counterpartyConnectionID |-> srcConnectionID, \* "connAtoB" - counterpartyClientID |-> srcEnd.clientID, \* "clB" - proofHeight |-> srcHeight, - consensusHeight |-> srcConsensusHeight]} - - ELSE IF srcEnd.state = "TRYOPEN" /\ \/ dstEnd.state = "INIT" - \/ dstEnd.state = "TRYOPEN" - THEN {[type |-> "ConnOpenAck", - connectionID |-> dstConnectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight, - consensusHeight |-> srcConsensusHeight]} - - ELSE IF srcEnd.state = "OPEN" /\ dstEnd.state = "TRYOPEN" - THEN {[type |-> "ConnOpenConfirm", - connectionID |-> dstEnd.connectionID, \* "connBtoA" (if srcChainID = "chainA", dstChainID = "chainB") - proofHeight |-> srcHeight]} - ELSE {} - -\* Get the connection datagrams designated for srcChainID and dstChainID -ConnectionDatagrams(srcChainID, dstChainID) == - LET srcConnectionDatagrams == ComputeConnectionDatagrams(dstChainID, srcChainID) IN - LET dstConnectionDatagrams == ComputeConnectionDatagrams(srcChainID, dstChainID) IN - - [src |-> srcConnectionDatagrams, dst |-> dstConnectionDatagrams] - -(*************** -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 == ClientDatagrams(srcChainID, dstChainID) 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, - relayerUpdate |-> clientDatagrams.relayerUpdate] - - - -(*************** -Relayer actions -***************) - -\* Update the height of the relayer client for some chainID -UpdateRelayerClients == - \E chainID \in ChainIDs : - /\ relayerChainHeights[chainID] < GetLatestHeight(chainID) - /\ relayerChainHeights' = [relayerChainHeights EXCEPT - ![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 - /\ LET datagramsAndRelayerUpdate == PendingDatagrams(srcChainID, dstChainID) IN - /\ pendingDatagrams' = - [pendingDatagrams EXCEPT - ![srcChainID] = pendingDatagrams[srcChainID] \union datagramsAndRelayerUpdate.src, - ![dstChainID] = pendingDatagrams[dstChainID] \union datagramsAndRelayerUpdate.dst - ] - /\ relayerChainHeights' = datagramsAndRelayerUpdate.relayerUpdate - /\ UNCHANGED chains - -(*************** -Component actions -***************) - -\* Relayer -\* The relayer either -\* - updates its clients, or -\* - relays datagrams between two chains, or -\* - does nothing -Relayer == - \/ UpdateRelayerClients - \/ Relay - \/ 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 == - /\ WF_<>(UpdateRelayerClients) - /\ WF_<>(Relay) - /\ Env!Fairness - -\* Spec formula -Spec == Init /\ [][Next]_vars /\ Fairness - -(************ -Helper operators used in properties -************) - -\* returns true if there is a "CreateClient" datagram -\* in the pending datagrams for chainID and height h -IsCreateClientInPendingDatagrams(chainID, clID, h) == - [type |-> "CreateClient", clientID |-> clID, height |-> h] - \in pendingDatagrams[chainID] - -\* returns true if there is a "ClientUpdate" datagram -\* in the pending datagrams for chainID and height h -IsClientUpdateInPendingDatagrams(chainID, clID, h) == - [type |-> "ClientUpdate", clientID |-> clID, height |-> h] - \in pendingDatagrams[chainID] - -\* returns true if a "ConnOpenInit" datagram for a connection -\* with counterpartyChainID is in pending datagrams of chainID -IsConnOpenInitInPendingDatagrams(chainID, counterpartyChainID) == - LET connectionID == GetConnectionID(chainID) IN - LET clientID == GetCounterpartyClientID(chainID) IN - LET counterpartyConnectionID == GetConnectionID(counterpartyChainID) IN - LET counterpartyClientID == GetCounterpartyClientID(counterpartyChainID) IN - - [type |-> "ConnOpenInit", - connectionID |-> connectionID, - clientID |-> clientID, - counterpartyConnectionID |-> counterpartyConnectionID, - counterpartyClientID |-> counterpartyClientID] \in pendingDatagrams[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 clientID of the datagram is the counterparty clientID for chainID -CreateClientInv == - \A chainID \in ChainIDs : \A clID \in ClientIDs : - ((\E h \in Heights : IsCreateClientInPendingDatagrams(chainID, clID, h)) - => (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 : - IsClientUpdateInPendingDatagrams(chainID, clID, h) - => clID = GetCounterpartyClientID(chainID) - -\* Inv -\* A conjunction of all invariants -Inv == - /\ TypeOK - /\ CreateClientInv - /\ ClientUpdateInv - -(************ -Properties about client datagrams -************) - -\* 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 : - GetCounterpartyClientHeight(chainID) = nullHeight - => <>(\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 : - (/\ GetCounterpartyClientHeight(chainID) = h1 - /\ GetCounterpartyClientHeight(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) - /\ GetCounterpartyClientHeight(chainID) < h) - => (<>(CounterpartyClientHeightUpdated(chainID, h)))) - -(************ -Properties about connection datagrams -************) - -ConnOpenInitIsGenerated == - [](\A chainID \in ChainIDs : - (/\ IsConnectionUninit(chainID) - /\ IsConnectionUninit(GetCounterpartyChainID(chainID))) - => <>(IsConnOpenInitInPendingDatagrams(chainID, GetCounterpartyChainID(chainID)))) - -\* it ALWAYS holds that, for every cahinID, and every counterpartyChainID: -\* - if -\* * there is a "ConnOpenInit" message for the connection between -\* chainID and counterpartyChainID in pending datagrams of chainID -\* * the connection is not open -\* - then -\* * the connection is EVENTUALLY open -ConnectionOpened == - [](\A chainID \in ChainIDs : - IsConnOpenInitInPendingDatagrams(chainID, GetCounterpartyChainID(chainID)) - => (<>(/\ IsConnectionOpen(chainID) - /\ IsConnectionOpen(GetCounterpartyChainID(chainID))))) - -\* 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 Fri Apr 03 16:39:06 CEST 2020 by ilinastoilkovska -\* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska From 68714453bbe1a8ed80a9a44deae027aac5df803b Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Tue, 19 May 2020 13:30:25 +0200 Subject: [PATCH 3/7] Refactored relayerwith Anca's comments --- verification/spec/relayer/ChannelHandlers.tla | 8 +- verification/spec/relayer/ClientHandlers.tla | 50 +++-- .../spec/relayer/ConnectionHandlers.tla | 11 +- verification/spec/relayer/Environment.tla | 36 ++-- verification/spec/relayer/Relayer.tla | 181 ++++++++---------- 5 files changed, 147 insertions(+), 139 deletions(-) diff --git a/verification/spec/relayer/ChannelHandlers.tla b/verification/spec/relayer/ChannelHandlers.tla index c3a8b9f6e7..012355c1ab 100644 --- a/verification/spec/relayer/ChannelHandlers.tla +++ b/verification/spec/relayer/ChannelHandlers.tla @@ -72,7 +72,7 @@ HandleChanOpenTry(chainID, chain, datagrams) == LET chanOpenTryDgrs == {dgr \in datagrams : /\ dgr.type = "ChanOpenTry" /\ dgr.channelID = GetChannelID(chainID) - /\ dgr.proofHeight <= chain.counterpartyClientHeight} IN + /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN IF chanOpenTryDgrs /= {} /\ chain.connectionEnd.state = "OPEN" \* if there are valid "ChanOpenTry" datagrams and the connection is "OPEN", @@ -109,7 +109,7 @@ HandleChanOpenAck(chainID, chain, datagrams) == LET chanOpenAckDgrs == {dgr \in datagrams : /\ dgr.type = "ChanOpenAck" /\ dgr.channelID = GetChannelID(chainID) - /\ dgr.proofHeight <= chain.counterpartyClientHeight} IN + /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN IF chanOpenAckDgrs /= {} /\ chain.connectionEnd.state = "OPEN" \* if there are valid "ChanOpenAck" datagrams, update the channel end @@ -142,7 +142,7 @@ HandleChanOpenConfirm(chainID, chain, datagrams) == LET chanOpenConfirmDgrs == {dgr \in datagrams : /\ dgr.type = "ChanOpenConfirm" /\ dgr.channelID = GetChannelID(chainID) - /\ dgr.proofHeight <= chain.counterpartyClientHeight} IN + /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN IF chanOpenConfirmDgrs /= {} /\ chain.connectionEnd.state = "OPEN" \* if there are valid "ChanOpenConfirm" datagrams, update the channel end @@ -168,5 +168,5 @@ HandleChanOpenConfirm(chainID, chain, datagrams) == ============================================================================= \* Modification History -\* Last modified Wed Apr 15 16:18:59 CEST 2020 by ilinastoilkovska +\* Last modified Thu May 14 16:29:29 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 index 741115121c..f9d1ea0501 100644 --- a/verification/spec/relayer/ClientHandlers.tla +++ b/verification/spec/relayer/ClientHandlers.tla @@ -38,6 +38,11 @@ GetCounterpartyClientID(chainID) == 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 @@ -50,18 +55,22 @@ HandleCreateClient(chainID, chain, datagrams) == \* new chain record with clients created LET clientCreateChain == [ height |-> chain.height, - counterpartyClientHeight |-> IF createClientHeights /= {} - THEN Max(createClientHeights) - ELSE chain.counterpartyClientHeight, + 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 - IF chain.counterpartyClientHeight = nullHeight - \* if the counterparty client height is null, create the client - THEN clientCreateChain - \* otherwise, do not update the chain - ELSE chain - + clientCreateChain + \* Handle "ClientUpdate" datagrams HandleUpdateClient(chainID, chain, datagrams) == \* get "ClientUpdate" datagrams with valid clientID @@ -74,21 +83,24 @@ HandleUpdateClient(chainID, chain, datagrams) == \* new chain record with clients updated LET clientUpdatedChain == [ height |-> chain.height, - counterpartyClientHeight |-> IF updateClientHeights /= {} - THEN Max(updateClientHeights) - ELSE chain.counterpartyClientHeight, + 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 height Max(createClientHeights) + THEN chain.counterpartyClientHeights \union {Max(updateClientHeights)} + \* otherwise, do not update client heights + ELSE chain.counterpartyClientHeights, connectionEnd |-> chain.connectionEnd ] IN - -\* IF chain.counterpartyClientHeight < clientUpdatedChain.counterpartyClientHeight - \* if the current height of the counterparty client is smaller than the new height, update it -\* THEN clientUpdatedChain - \* otherwise, do not update the chain -\* ELSE chain + clientUpdatedChain ============================================================================= \* Modification History -\* Last modified Wed Apr 15 16:17:39 CEST 2020 by ilinastoilkovska +\* Last modified Thu May 14 16:20:42 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 index 07ccdd673a..bf4a832e59 100644 --- a/verification/spec/relayer/ConnectionHandlers.tla +++ b/verification/spec/relayer/ConnectionHandlers.tla @@ -71,7 +71,8 @@ HandleConnOpenTry(chainID, chain, datagrams) == /\ dgr.type = "ConnOpenTry" /\ dgr.desiredConnectionID = GetConnectionID(chainID) /\ dgr.consensusHeight <= chain.height - /\ dgr.proofHeight <= chain.counterpartyClientHeight} IN + /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN + \* TODO: check dgr.proofHeight \in chain.counterpartyClientHeight IF connOpenTryDgrs /= {} \* if there are valid "ConnOpenTry" datagrams, update the connection end @@ -112,7 +113,8 @@ HandleConnOpenAck(chainID, chain, datagrams) == LET connOpenAckDgrs == {dgr \in datagrams : /\ dgr.type = "ConnOpenAck" /\ dgr.connectionID = GetConnectionID(chainID) - /\ dgr.consensusHeight <= chain.height} IN + /\ dgr.consensusHeight <= chain.height + /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN IF connOpenAckDgrs /= {} \* if there are valid "ConnOpenAck" datagrams, update the connection end @@ -141,7 +143,8 @@ 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)} IN + /\ dgr.connectionID = GetConnectionID(chainID) + /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN IF connOpenConfirmDgrs /= {} \* if there are valid "connOpenConfirmDgrs" datagrams, update the connection end @@ -164,5 +167,5 @@ HandleConnOpenConfirm(chainID, chain, datagrams) == ============================================================================= \* Modification History -\* Last modified Wed Apr 15 16:18:37 CEST 2020 by ilinastoilkovska +\* Last modified Thu May 14 16:29:33 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 index 67fecf272b..63d8cc04e1 100644 --- a/verification/spec/relayer/Environment.tla +++ b/verification/spec/relayer/Environment.tla @@ -76,8 +76,8 @@ ConnectionEnds == - 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. + - 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 @@ -85,7 +85,7 @@ ConnectionEnds == Chains == [ height : Heights \union {nullHeight}, - counterpartyClientHeight : Heights \union {nullHeight}, + counterpartyClientHeights : SUBSET(Heights), connectionEnd : ConnectionEnds ] @@ -125,17 +125,23 @@ Datagrams == GetLatestHeight(chainID) == chains[chainID].height -\* get the height of the client for chainID's counterparty chain -GetCounterpartyClientHeight(chainID) == - chains[chainID].counterpartyClientHeight +\* 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].counterpartyClientHeight /= nullHeight + chains[chainID].counterpartyClientHeights /= {} \* returns true if the counterparty client height on chainID is greater or equal than h CounterpartyClientHeightUpdated(chainID, h) == - chains[chainID].counterpartyClientHeight >= h + h \in chains[chainID].counterpartyClientHeights \* get the connection end at chainID GetConnectionEnd(chainID) == @@ -238,7 +244,15 @@ UpdateChain(chainID, datagrams) == \* ICS 004: Channel updates LET channelsUpdated == ChannelUpdate(chainID, connectionsUpdated, datagrams) IN - channelsUpdated + \* update height + LET updatedChain == + IF /\ chain /= channelsUpdated + /\ chain.height < MaxHeight + THEN [channelsUpdated EXCEPT !.height = chain.height + 1] + ELSE channelsUpdated + IN + + updatedChain (*************************************************************************** Chain actions @@ -290,7 +304,7 @@ InitConnectionEnd == \* - the connection end is initialized to InitConnectionEnd InitChain == [height |-> 1, - counterpartyClientHeight |-> nullHeight, + counterpartyClientHeights |-> {}, connectionEnd |-> InitConnectionEnd] (*************************************************************************** @@ -330,5 +344,5 @@ TypeOK == ============================================================================= \* Modification History -\* Last modified Wed Apr 15 16:18:18 CEST 2020 by ilinastoilkovska +\* Last modified Fri May 15 15:07:29 CEST 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 index 4bbe16e4d7..75882dda34 100644 --- a/verification/spec/relayer/Relayer.tla +++ b/verification/spec/relayer/Relayer.tla @@ -14,7 +14,8 @@ VARIABLES chains, \* a function that assigns a chain record to each chainID relayerChainHeights, \* a function that assigns a height to each chainID turn -vars == <> +vars == <> +specVars == <> envVars == <> \* Instance of the module Environment, which encodes the chain logic @@ -46,7 +47,10 @@ Datagrams == Env!Datagrams GetLatestHeight(chainID) == Env!GetLatestHeight(chainID) \* get the height of the client for chainID's counterparty chain -GetCounterpartyClientHeight(chainID) == Env!GetCounterpartyClientHeight(chainID) +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) @@ -114,7 +118,7 @@ IsChannelOpen(chainID) == Env!IsChannelOpen(chainID) \* the relayer stores for srcChainID LightClientUpdates(srcChainID, dstChainID, relayer) == LET srcChainHeight == GetLatestHeight(srcChainID) IN - LET srcClientHeight == GetCounterpartyClientHeight(dstChainID) IN + LET srcClientHeight == GetMaxCounterpartyClientHeight(dstChainID) IN LET srcClientID == GetClientID(srcChainID) IN \* check if the relayer chain height for srcChainID should be updated @@ -144,37 +148,12 @@ LightClientUpdates(srcChainID, dstChainID, relayer) == [datagrams|-> dstDatagrams, relayerUpdate |-> updatedRelayer] -\* Get the client datagrams for clients on srcChainID and on dstChainID, -\* as well as the relayer update triggered by creating client datagrams -ClientDatagrams(srcChainID, dstChainID) == - \* get the client datagrams for dstChainID - \* and relayer update triggered by difference between the height of - \* srcChainID and the height that the relayer stores for srcChainID - LET dstLightClientUpdates == - LightClientUpdates(srcChainID, dstChainID, relayerChainHeights) IN - LET dstClientDatagrams == - dstLightClientUpdates.datagrams IN - LET dstRelayerUpdate == - dstLightClientUpdates.relayerUpdate IN - - \* get the client datagrams for srcChainID - \* and relayer update triggered by difference between the height of - \* dstChainID and the height that the relayer stores for dstChainID - LET srcLightClientUpdates == - LightClientUpdates(dstChainID, srcChainID, dstRelayerUpdate) IN - LET srcClientDatagrams == - srcLightClientUpdates.datagrams IN - LET srcRelayerUpdate == - srcLightClientUpdates.relayerUpdate IN - - [src |-> srcClientDatagrams, dst |-> dstClientDatagrams, relayerUpdate |-> srcRelayerUpdate] - (*************************************************************************** Connection datagrams ***************************************************************************) \* Compute connection datagrams designated for dstChainID. \* These are used to update the connection end on dstChainID in the environment. -ComputeConnectionDatagrams(srcChainID, dstChainID) == +ConnectionDatagrams(srcChainID, dstChainID) == LET srcConnectionEnd == GetConnectionEnd(srcChainID) IN LET dstConnectionEnd == GetConnectionEnd(dstChainID) IN @@ -182,7 +161,7 @@ ComputeConnectionDatagrams(srcChainID, dstChainID) == LET dstConnectionID == GetConnectionID(dstChainID) IN LET srcHeight == GetLatestHeight(srcChainID) IN - LET srcConsensusHeight == GetCounterpartyClientHeight(srcChainID) IN + LET srcConsensusHeight == GetMaxCounterpartyClientHeight(srcChainID) IN IF dstConnectionEnd.state = "UNINIT" /\ srcConnectionEnd.state = "UNINIT" THEN {[type |-> "ConnOpenInit", @@ -214,21 +193,12 @@ ComputeConnectionDatagrams(srcChainID, dstChainID) == proofHeight |-> srcHeight]} ELSE {} -\* Get the connection datagrams designated for srcChainID and dstChainID -ConnectionDatagrams(srcChainID, dstChainID) == - \* connection datagrams from dstChainID to srcChainID - LET srcConnectionDatagrams == ComputeConnectionDatagrams(dstChainID, srcChainID) IN - \* connection datagrams from srcChainID to dstChainID - LET dstConnectionDatagrams == ComputeConnectionDatagrams(srcChainID, dstChainID) IN - - [src |-> srcConnectionDatagrams, dst |-> dstConnectionDatagrams] - (*************************************************************************** Channel datagrams ***************************************************************************) \* Compute channel datagrams designated for dstChainID. \* These are used to update the channel end on dstChainID in the environment. -ComputeChannelDatagrams(srcChainID, dstChainID) == +ChannelDatagrams(srcChainID, dstChainID) == LET srcChannelEnd == GetChannelEnd(srcChainID) IN LET dstChannelEnd == GetChannelEnd(dstChainID) IN @@ -261,18 +231,8 @@ ComputeChannelDatagrams(srcChainID, dstChainID) == proofHeight |-> srcHeight]} ELSE {} - -\* Get the channel datagrams designated for srcChainID and dstChainID -ChannelDatagrams(srcChainID, dstChainID) == - \* channel datagrams from dstChainID to srcChainID - LET srcChannelDatagrams == ComputeChannelDatagrams(dstChainID, srcChainID) IN - \* channel datagrams from srcChainID to dstChainID - LET dstChannelDatagrams == ComputeChannelDatagrams(srcChainID, dstChainID) IN - - [src |-> srcChannelDatagrams, dst |-> dstChannelDatagrams] - (*************************************************************************** - Compute pending datagrams + Compute pending datagrams (from srcChainID to dstChainID) ***************************************************************************) \* Currently supporting: \* - ICS 002: Client updates @@ -282,7 +242,7 @@ ChannelDatagrams(srcChainID, dstChainID) == PendingDatagrams(srcChainID, dstChainID) == \* ICS 002 : Clients \* - Determine if light clients needs to be updated - LET clientDatagrams == ClientDatagrams(srcChainID, dstChainID) IN + LET clientDatagrams == LightClientUpdates(srcChainID, dstChainID, relayerChainHeights) IN \* ICS3 : Connections \* - Determine if any connection handshakes are in progress @@ -296,16 +256,16 @@ PendingDatagrams(srcChainID, dstChainID) == \* - Determine if any packets, acknowledgements, or timeouts need to be relayed \* TODO - [src |-> clientDatagrams.src \union connectionDatagrams.src \union channelDatagrams.src, - dst |-> clientDatagrams.dst \union connectionDatagrams.dst \union channelDatagrams.dst, + [datagrams |-> clientDatagrams.datagrams \union + connectionDatagrams \union + channelDatagrams, relayerUpdate |-> clientDatagrams.relayerUpdate] (*************************************************************************** Relayer actions ***************************************************************************) \* Update the height of the relayer client for some chainID -UpdateRelayerClients == - \E chainID \in ChainIDs : +UpdateRelayerClients(chainID) == /\ relayerChainHeights[chainID] < GetLatestHeight(chainID) /\ relayerChainHeights' = [relayerChainHeights EXCEPT ![chainID] = GetLatestHeight(chainID) @@ -314,15 +274,15 @@ UpdateRelayerClients == \* for two chains, srcChainID and dstChainID, where srcChainID /= dstChainID, \* create the pending datagrams and update the corresponding sets of pending datagrams -Relay == - \E srcChainID \in ChainIDs : - \E dstChainID \in ChainIDs : +Relay(srcChainID, dstChainID) == + /\ srcChainID /= dstChainID /\ LET datagramsAndRelayerUpdate == PendingDatagrams(srcChainID, dstChainID) IN /\ pendingDatagrams' = [pendingDatagrams EXCEPT - ![srcChainID] = pendingDatagrams[srcChainID] \union datagramsAndRelayerUpdate.src, - ![dstChainID] = pendingDatagrams[dstChainID] \union datagramsAndRelayerUpdate.dst + ![dstChainID] = pendingDatagrams[dstChainID] + \union + datagramsAndRelayerUpdate.datagrams ] /\ relayerChainHeights' = datagramsAndRelayerUpdate.relayerUpdate /\ UNCHANGED chains @@ -336,8 +296,8 @@ Relay == \* - relays datagrams between two chains, or \* - does nothing Relayer == - \/ UpdateRelayerClients - \/ Relay + \/ \E chainID \in ChainIDs : UpdateRelayerClients(chainID) + \/ \E srcChainID \in ChainIDs : \E dstChainID \in ChainIDs : Relay(srcChainID, dstChainID) \/ UNCHANGED vars \* Environment @@ -375,8 +335,10 @@ Next == \* Fairness constraints Fairness == - /\ WF_<>(UpdateRelayerClients) - /\ WF_<>(Relay) + /\ \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 @@ -398,18 +360,32 @@ IsClientUpdateInPendingDatagrams(chainID, clID, h) == \in pendingDatagrams[chainID] \* returns true if there is a "ConnOpenInit" datagram -\* in pending datagrams of chainID +\* 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 pendingDatagrams[srcChainID] + +\* returns true if there is a "ConnOpenInit" datagram +\* in pending datagrams of chainID IsConnOpenInitInPendingDatagrams( chainID, clientID, counterpartyClientID, connectionID, counterpartyConnectionID - ) == - + ) == + [type |-> "ConnOpenInit", connectionID |-> connectionID, clientID |-> clientID, counterpartyConnectionID |-> counterpartyConnectionID, counterpartyClientID |-> counterpartyClientID] \in pendingDatagrams[chainID] - + \* returns true if there is a "ConnOpenTry" datagram \* in pending datagrams of chainID IsConnOpenTryInPendingDatagrams( @@ -442,7 +418,11 @@ IsConnOpenConfirmInPendingDatagrams(chainID, connectionID) == [type |-> "ConnOpenConfirm", connectionID |-> connectionID, proofHeight |-> pHeight] \in pendingDatagrams[chainID] - + +\*\* returns true if there is a "ConnOpenInit" datagram +\*\* for the channel between srcChainID and dstChainID +\*ChanOpenInitGenerated(srcChainID, GetCounterpartyChainID(chainID)) == + \* returns true if there is a "ChanOpenInit" datagram \* in pending datagrams of chainID IsChanOpenInitInPendingDatagrams(chainID, channelID, counterpartyChannelID) == @@ -492,7 +472,7 @@ CreateClientInv == \A chainID \in ChainIDs : \A clID \in ClientIDs : ((\E h \in Heights : IsCreateClientInPendingDatagrams(chainID, clID, h)) => (/\ clID = GetCounterpartyClientID(chainID) - /\ GetCounterpartyClientHeight(chainID) = nullHeight)) + /\ GetCounterpartyClientHeights(chainID) = {})) \* if a "ClientUpdate" datagram is in pendingDatagrams for chainID, \* then the datagram has the correct client ID @@ -501,7 +481,7 @@ ClientUpdateInv == \A chainID \in ChainIDs : \A clID \in ClientIDs : \A h \in Heights : IsClientUpdateInPendingDatagrams(chainID, clID, h) => (/\ clID = GetCounterpartyClientID(chainID) - /\ GetCounterpartyClientHeight(chainID) < h) + /\ GetMaxCounterpartyClientHeight(chainID) < h) \* ConnOpenInitInv \* if a "ConnOpenInit" datagram is in pendingDatagrams for chainID, @@ -512,10 +492,8 @@ 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 - ) + IsConnOpenInitInPendingDatagrams(chainID, clientID, counterpartyClientID, + connectionID, counterpartyConnectionID) => /\ clientID = GetCounterpartyClientID(chainID) /\ counterpartyClientID = GetClientID(chainID) /\ connectionID = GetConnectionID(chainID) @@ -638,7 +616,7 @@ Inv == \* * the relayer EVENTUALLY adds a "CreateClient" datagram in pending datagrams of chainID CreateClientIsGenerated == [](\A chainID \in ChainIDs : - GetCounterpartyClientHeight(chainID) = nullHeight + GetCounterpartyClientHeights(chainID) = {} => <>(\E h \in Heights : IsCreateClientInPendingDatagrams(chainID, GetCounterpartyClientID(chainID), h))) \* it ALWAYS holds that, for every chainID: @@ -661,8 +639,8 @@ ClientCreated == \* * the relayer EVENTUALLY adds a "ClientUpdate" datagram in pending datagrams of chainID ClientUpdateIsGenerated == [](\A chainID \in ChainIDs : \A h1 \in Heights : - (/\ GetCounterpartyClientHeight(chainID) = h1 - /\ GetCounterpartyClientHeight(chainID) < GetLatestHeight(GetCounterpartyChainID(chainID))) + (/\ GetMaxCounterpartyClientHeight(chainID) = h1 + /\ GetMaxCounterpartyClientHeight(chainID) < GetLatestHeight(GetCounterpartyChainID(chainID))) => <>(\E h2 \in Heights : /\ h1 <= h2 /\ IsClientUpdateInPendingDatagrams(chainID, GetCounterpartyClientID(chainID), h2))) @@ -677,7 +655,7 @@ ClientUpdateIsGenerated == ClientUpdated == [](\A chainID \in ChainIDs : \A h \in Heights : (/\ IsClientUpdateInPendingDatagrams(chainID, GetCounterpartyClientID(chainID), h) - /\ GetCounterpartyClientHeight(chainID) < h) + /\ GetMaxCounterpartyClientHeight(chainID) < h) => (<>(CounterpartyClientHeightUpdated(chainID, h)))) (*************************************************************************** @@ -687,16 +665,17 @@ ClientUpdated == \* - if \* * the connection on chainID is uninitialized and \* * the connection on chainID's counterparty is uninitialized -\* - then -\* * the relayer EVENTUALLY adds a "ConnOpenInit" datagram in pending datagrams of chainID +\* - 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) - /\ IsConnectionUninit(GetCounterpartyChainID(chainID))) - => <>(IsConnOpenInitInPendingDatagrams( - chainID, GetCounterpartyClientID(chainID), GetClientID(chainID), - GetConnectionID(chainID), GetCounterpartyConnectionID(chainID) - ))) + 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 @@ -705,13 +684,13 @@ ConnOpenInitIsGenerated == \* - then \* * the connection is EVENTUALLY open ConnectionOpened == - [](\A chainID \in ChainIDs : + [](\A chainID \in ChainIDs : IsConnOpenInitInPendingDatagrams( chainID, GetClientID(chainID), GetCounterpartyClientID(chainID), GetConnectionID(chainID), GetCounterpartyConnectionID(chainID) ) - => (<>(/\ IsConnectionOpen(chainID) - /\ IsConnectionOpen(GetCounterpartyChainID(chainID))))) + => <>(/\ IsConnectionOpen(chainID) + /\ IsConnectionOpen(GetCounterpartyChainID(chainID)))) (*************************************************************************** Properties about channel handshake @@ -724,9 +703,9 @@ ConnectionOpened == \* * the relayer EVENTUALLY adds a "ChanOpenInit" datagram in pending datagrams of chainID ChanOpenInitIsGenerated == [](\A chainID \in ChainIDs : - (/\ IsChannelUninit(chainID) - /\ IsChannelUninit(GetCounterpartyChainID(chainID))) - => <>(IsChanOpenInitInPendingDatagrams(chainID, GetChannelID(chainID), GetCounterpartyChannelID(chainID)))) + (IsChannelUninit(chainID) + => <>(\/ IsChanOpenInitInPendingDatagrams(chainID, GetChannelID(chainID), GetCounterpartyChannelID(chainID)) + \/ IsChannelInit(GetCounterpartyChainID(chainID))))) \* it ALWAYS holds that, for every cahinID, and every counterpartyChainID: \* - if @@ -753,17 +732,17 @@ HeightsDontDecrease == \* Prop \* A conjunction of all properties Prop == - /\ CreateClientIsGenerated - /\ ClientCreated - /\ ClientUpdateIsGenerated - /\ ClientUpdated + /\ CreateClientIsGenerated + /\ ClientCreated + /\ ClientUpdateIsGenerated + /\ ClientUpdated /\ ConnOpenInitIsGenerated - /\ ConnectionOpened + /\ ConnectionOpened /\ ChanOpenInitIsGenerated /\ ChannelOpened - /\ HeightsDontDecrease + /\ HeightsDontDecrease ============================================================================= \* Modification History -\* Last modified Wed Apr 15 16:25:56 CEST 2020 by ilinastoilkovska +\* Last modified Mon May 18 19:24:50 CEST 2020 by ilinastoilkovska \* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska From 9121195a880723ae44ee1db3169523a63bac5db0 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Wed, 20 May 2020 15:46:50 +0200 Subject: [PATCH 4/7] Update verification/spec/relayer/Environment.tla Co-authored-by: Adi Seredinschi --- verification/spec/relayer/Environment.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verification/spec/relayer/Environment.tla b/verification/spec/relayer/Environment.tla index 63d8cc04e1..33fe46ddab 100644 --- a/verification/spec/relayer/Environment.tla +++ b/verification/spec/relayer/Environment.tla @@ -234,7 +234,7 @@ ChannelUpdate(chainID, chain, datagrams) == Chain update operators ***************************************************************************) \* Update chainID with the received datagrams -\* Currently, only supporting ICS 002: Client updates +\* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels). UpdateChain(chainID, datagrams) == LET chain == chains[chainID] IN \* ICS 002: Client updates From f1124bb0380a3b7e394e6aed46262c257eb066e6 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Fri, 22 May 2020 17:20:48 +0200 Subject: [PATCH 5/7] Addressed Adi's and Zarko's comments --- verification/spec/relayer/ChannelHandlers.tla | 24 +++--- verification/spec/relayer/ClientHandlers.tla | 8 +- .../spec/relayer/ConnectionHandlers.tla | 7 +- verification/spec/relayer/Environment.tla | 19 +++-- verification/spec/relayer/Relayer.tla | 82 +++++++++---------- 5 files changed, 67 insertions(+), 73 deletions(-) diff --git a/verification/spec/relayer/ChannelHandlers.tla b/verification/spec/relayer/ChannelHandlers.tla index 012355c1ab..c0ea6ffd41 100644 --- a/verification/spec/relayer/ChannelHandlers.tla +++ b/verification/spec/relayer/ChannelHandlers.tla @@ -44,9 +44,9 @@ HandleChanOpenInit(chainID, chain, datagrams) == /\ dgr.type = "ChanOpenInit" /\ dgr.channelID = GetChannelID(chainID)} IN - IF chanOpenInitDgrs /= {} /\ chain.connectionEnd.state /= "UNINIT" \* 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", @@ -74,9 +74,9 @@ HandleChanOpenTry(chainID, chain, datagrams) == /\ dgr.channelID = GetChannelID(chainID) /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN - IF chanOpenTryDgrs /= {} /\ chain.connectionEnd.state = "OPEN" \* if there are valid "ChanOpenTry" datagrams and the connection is "OPEN", - \* update the channel end + \* update the channel end + IF chanOpenTryDgrs /= {} /\ chain.connectionEnd.state = "OPEN" THEN LET chanOpenTryDgr == CHOOSE dgr \in chanOpenTryDgrs : TRUE IN LET chanOpenTryChannelEnd == [ state |-> "TRYOPEN", @@ -111,12 +111,12 @@ HandleChanOpenAck(chainID, chain, datagrams) == /\ 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" - \* if there are valid "ChanOpenAck" datagrams, update the channel end - THEN IF \/ chain.connectionEnd.channelEnd.state = "INIT" + 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" - \* if the channel end on the chain is in "INIT" or it is in "TRYOPEN", - \* update the channel end THEN LET chanOpenAckDgr == CHOOSE dgr \in chanOpenAckDgrs : TRUE IN LET chanOpenAckChannelEnd == [ chain.connectionEnd.channelEnd EXCEPT !.state = "OPEN", @@ -144,10 +144,10 @@ HandleChanOpenConfirm(chainID, chain, datagrams) == /\ 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" - \* if there are valid "ChanOpenConfirm" datagrams, update the channel end - THEN IF chain.connectionEnd.channelEnd.state = "TRYOPEN" - \* if the channel end on the chain is in "TRYOPEN", update the channel end + 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", @@ -165,8 +165,8 @@ HandleChanOpenConfirm(chainID, chain, datagrams) == ELSE chain \* otherwise, do not update the chain ELSE chain - + ============================================================================= \* Modification History -\* Last modified Thu May 14 16:29:29 CEST 2020 by ilinastoilkovska +\* 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 index f9d1ea0501..c364545420 100644 --- a/verification/spec/relayer/ClientHandlers.tla +++ b/verification/spec/relayer/ClientHandlers.tla @@ -70,7 +70,7 @@ HandleCreateClient(chainID, chain, datagrams) == ] IN clientCreateChain - + \* Handle "ClientUpdate" datagrams HandleUpdateClient(chainID, chain, datagrams) == \* get "ClientUpdate" datagrams with valid clientID @@ -90,8 +90,8 @@ HandleUpdateClient(chainID, chain, datagrams) == THEN chain.counterpartyClientHeights \* otherwise, if set of heights from datagrams is not empty ELSE IF updateClientHeights /= {} - \* then update counterparty client heights with height Max(createClientHeights) - THEN chain.counterpartyClientHeights \union {Max(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 @@ -102,5 +102,5 @@ HandleUpdateClient(chainID, chain, datagrams) == ============================================================================= \* Modification History -\* Last modified Thu May 14 16:20:42 CEST 2020 by ilinastoilkovska +\* Last modified Fri May 22 17:19:54 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 index bf4a832e59..6c4a6a546c 100644 --- a/verification/spec/relayer/ConnectionHandlers.tla +++ b/verification/spec/relayer/ConnectionHandlers.tla @@ -43,9 +43,8 @@ HandleConnOpenInit(chainID, chain, datagrams) == /\ dgr.type = "ConnOpenInit" /\ dgr.connectionID = GetConnectionID(chainID)} IN - IF connOpenInitDgrs /= {} \* if there are valid "ConnOpenInit" datagrams, create a new connection end and update the chain - \* TODO: check here if connection is already in INIT? + IF connOpenInitDgrs /= {} /\ chain.connectionEnd.state = "UNINIT" THEN LET connOpenInitDgr == CHOOSE dgr \in connOpenInitDgrs : TRUE IN LET connOpenInitConnectionEnd == [ state |-> "INIT", @@ -72,7 +71,6 @@ HandleConnOpenTry(chainID, chain, datagrams) == /\ dgr.desiredConnectionID = GetConnectionID(chainID) /\ dgr.consensusHeight <= chain.height /\ dgr.proofHeight \in chain.counterpartyClientHeights} IN - \* TODO: check dgr.proofHeight \in chain.counterpartyClientHeight IF connOpenTryDgrs /= {} \* if there are valid "ConnOpenTry" datagrams, update the connection end @@ -137,7 +135,6 @@ HandleConnOpenAck(chainID, chain, datagrams) == \* 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 @@ -167,5 +164,5 @@ HandleConnOpenConfirm(chainID, chain, datagrams) == ============================================================================= \* Modification History -\* Last modified Thu May 14 16:29:33 CEST 2020 by ilinastoilkovska +\* 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 index 63d8cc04e1..bc1757f81d 100644 --- a/verification/spec/relayer/Environment.tla +++ b/verification/spec/relayer/Environment.tla @@ -10,9 +10,10 @@ EXTENDS Naturals, FiniteSets, ClientHandlers, ConnectionHandlers, ChannelHandlers VARIABLES chains, \* a function that assigns a chain record to each chainID - pendingDatagrams \* a function that assigns a set of pending datagrams to each chainID + incomingDatagrams \* a function that assigns a set of incoming datagrams + \* incoming from the relayer to each chainID -vars == <> +vars == <> ChainIDs == {"chainA", "chainB"} @@ -263,15 +264,15 @@ AdvanceChain(chainID) == /\ chains' = [chains EXCEPT ![chainID].height = chains[chainID].height + 1 ] - /\ UNCHANGED pendingDatagrams + /\ UNCHANGED incomingDatagrams \* Receive the datagrams and update the chain state ReceiveDatagrams(chainID) == - /\ pendingDatagrams[chainID] /= {} + /\ incomingDatagrams[chainID] /= {} /\ chains' = [chains EXCEPT - ![chainID] = UpdateChain(chainID, pendingDatagrams[chainID]) + ![chainID] = UpdateChain(chainID, incomingDatagrams[chainID]) ] - /\ pendingDatagrams' = [pendingDatagrams EXCEPT + /\ incomingDatagrams' = [incomingDatagrams EXCEPT ![chainID] = {} ] @@ -316,7 +317,7 @@ InitChain == \* - pendingDatagrams for each chain is empty Init == /\ chains = [chainID \in ChainIDs |-> InitChain] - /\ pendingDatagrams = [chainID \in ChainIDs |-> {}] + /\ incomingDatagrams = [chainID \in ChainIDs |-> {}] \* Next state action \* One of the chains either @@ -340,9 +341,9 @@ Fairness == \* Type invariant TypeOK == /\ chains \in [ChainIDs -> Chains] - /\ pendingDatagrams \in [ChainIDs -> SUBSET Datagrams] + /\ incomingDatagrams \in [ChainIDs -> SUBSET Datagrams] ============================================================================= \* Modification History -\* Last modified Fri May 15 15:07:29 CEST 2020 by ilinastoilkovska +\* Last modified Fri May 22 17:09:26 CEST 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 index 75882dda34..51c691caf2 100644 --- a/verification/spec/relayer/Relayer.tla +++ b/verification/spec/relayer/Relayer.tla @@ -10,18 +10,19 @@ 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 - pendingDatagrams, \* a function that assigns a set of pending datagrams 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 == <> +vars == <> +specVars == <> envVars == <> \* Instance of the module Environment, which encodes the chain logic Env == INSTANCE Environment WITH chains <- chains, - pendingDatagrams <- pendingDatagrams, + incomingDatagrams <- outgoingDatagrams, MaxHeight <- MaxHeight ChainIDs == Env!ChainIDs @@ -270,22 +271,21 @@ UpdateRelayerClients(chainID) == /\ relayerChainHeights' = [relayerChainHeights EXCEPT ![chainID] = GetLatestHeight(chainID) ] - /\ UNCHANGED <> + /\ 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) == - - /\ srcChainID /= dstChainID - /\ LET datagramsAndRelayerUpdate == PendingDatagrams(srcChainID, dstChainID) IN - /\ pendingDatagrams' = - [pendingDatagrams EXCEPT - ![dstChainID] = pendingDatagrams[dstChainID] - \union - datagramsAndRelayerUpdate.datagrams - ] - /\ relayerChainHeights' = datagramsAndRelayerUpdate.relayerUpdate - /\ UNCHANGED chains + LET datagramsAndRelayerUpdate == PendingDatagrams(srcChainID, dstChainID) IN + /\ srcChainID /= dstChainID + /\ outgoingDatagrams' = + [outgoingDatagrams EXCEPT + ![dstChainID] = outgoingDatagrams[dstChainID] + \union + datagramsAndRelayerUpdate.datagrams + ] + /\ relayerChainHeights' = datagramsAndRelayerUpdate.relayerUpdate + /\ UNCHANGED chains (*************************************************************************** Component actions @@ -348,16 +348,16 @@ Spec == Init /\ [][Next]_vars /\ Fairness Helper operators used in properties ***************************************************************************) \* returns true if there is a "CreateClient" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsCreateClientInPendingDatagrams(chainID, clID, h) == [type |-> "CreateClient", clientID |-> clID, height |-> h] - \in pendingDatagrams[chainID] + \in outgoingDatagrams[chainID] \* returns true if there is a "ClientUpdate" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsClientUpdateInPendingDatagrams(chainID, clID, h) == [type |-> "ClientUpdate", clientID |-> clID, height |-> h] - \in pendingDatagrams[chainID] + \in outgoingDatagrams[chainID] \* returns true if there is a "ConnOpenInit" datagram \* for the connection between srcChainID and dstChainID @@ -371,10 +371,10 @@ ConnOpenInitGenerated(srcChainID, dstChainID) == connectionID |-> srcConnectionID, clientID |-> srcClientID, counterpartyConnectionID |-> dstConnectionID, - counterpartyClientID |-> dstClientID] \in pendingDatagrams[srcChainID] + counterpartyClientID |-> dstClientID] \in outgoingDatagrams[srcChainID] \* returns true if there is a "ConnOpenInit" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsConnOpenInitInPendingDatagrams( chainID, clientID, counterpartyClientID, connectionID, counterpartyConnectionID @@ -384,10 +384,10 @@ IsConnOpenInitInPendingDatagrams( connectionID |-> connectionID, clientID |-> clientID, counterpartyConnectionID |-> counterpartyConnectionID, - counterpartyClientID |-> counterpartyClientID] \in pendingDatagrams[chainID] + counterpartyClientID |-> counterpartyClientID] \in outgoingDatagrams[chainID] \* returns true if there is a "ConnOpenTry" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsConnOpenTryInPendingDatagrams( chainID, clientID, counterpartyClientID, connectionID, counterpartyConnectionID @@ -400,60 +400,56 @@ IsConnOpenTryInPendingDatagrams( counterpartyConnectionID |-> counterpartyConnectionID, counterpartyClientID |-> counterpartyClientID, proofHeight |-> pHeight, - consensusHeight |-> cHeight] \in pendingDatagrams[chainID] + consensusHeight |-> cHeight] \in outgoingDatagrams[chainID] \* returns true if there is a "ConnOpenAck" datagram -\* in pending datagrams of chainID +\* 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 pendingDatagrams[chainID] + consensusHeight |-> cHeight] \in outgoingDatagrams[chainID] \* returns true if there is a "ConnOpenConfirm" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsConnOpenConfirmInPendingDatagrams(chainID, connectionID) == \E pHeight \in Heights : [type |-> "ConnOpenConfirm", connectionID |-> connectionID, - proofHeight |-> pHeight] \in pendingDatagrams[chainID] - -\*\* returns true if there is a "ConnOpenInit" datagram -\*\* for the channel between srcChainID and dstChainID -\*ChanOpenInitGenerated(srcChainID, GetCounterpartyChainID(chainID)) == + proofHeight |-> pHeight] \in outgoingDatagrams[chainID] \* returns true if there is a "ChanOpenInit" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsChanOpenInitInPendingDatagrams(chainID, channelID, counterpartyChannelID) == [type |-> "ChanOpenInit", channelID |-> channelID, - counterpartyChannelID |-> counterpartyChannelID] \in pendingDatagrams[chainID] + counterpartyChannelID |-> counterpartyChannelID] \in outgoingDatagrams[chainID] \* returns true if there is a "ChanOpenTry" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsChanOpenTryInPendingDatagrams(chainID, channelID, counterpartyChannelID) == \E pHeight \in Heights : [type |-> "ChanOpenTry", channelID |-> channelID, counterpartyChannelID |-> counterpartyChannelID, - proofHeight |-> pHeight] \in pendingDatagrams[chainID] + proofHeight |-> pHeight] \in outgoingDatagrams[chainID] \* returns true if there is a "ChanOpenAck" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsChanOpenAckInPendingDatagrams(chainID, channelID) == \E pHeight \in Heights : [type |-> "ChanOpenAck", channelID |-> channelID, - proofHeight |-> pHeight] \in pendingDatagrams[chainID] + proofHeight |-> pHeight] \in outgoingDatagrams[chainID] \* returns true if there is a "ChanOpenConfirm" datagram -\* in pending datagrams of chainID +\* in outgoing datagrams for chainID IsChanOpenConfirmInPendingDatagrams(chainID, channelID) == \E pHeight \in Heights : [type |-> "ChanOpenConfirm", channelID |-> channelID, - proofHeight |-> pHeight] \in pendingDatagrams[chainID] + proofHeight |-> pHeight] \in outgoingDatagrams[chainID] (*************************************************************************** Invariants @@ -741,8 +737,8 @@ Prop == /\ ChanOpenInitIsGenerated /\ ChannelOpened /\ HeightsDontDecrease - + ============================================================================= \* Modification History -\* Last modified Mon May 18 19:24:50 CEST 2020 by ilinastoilkovska +\* Last modified Fri May 22 17:20:08 CEST 2020 by ilinastoilkovska \* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska From cdffb6498603e2239c6c7c8d0b5403108a406eed Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Tue, 26 May 2020 11:57:06 +0200 Subject: [PATCH 6/7] fix in ClientHandlers --- verification/spec/relayer/ClientHandlers.tla | 11 ++++++++--- verification/spec/relayer/Relayer.tla | 18 +++++++++--------- 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/verification/spec/relayer/ClientHandlers.tla b/verification/spec/relayer/ClientHandlers.tla index c364545420..9395283245 100644 --- a/verification/spec/relayer/ClientHandlers.tla +++ b/verification/spec/relayer/ClientHandlers.tla @@ -72,11 +72,16 @@ HandleCreateClient(chainID, chain, datagrams) == clientCreateChain \* Handle "ClientUpdate" datagrams -HandleUpdateClient(chainID, chain, 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)} IN + /\ 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 @@ -102,5 +107,5 @@ HandleUpdateClient(chainID, chain, datagrams) == ============================================================================= \* Modification History -\* Last modified Fri May 22 17:19:54 CEST 2020 by ilinastoilkovska +\* 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/Relayer.tla b/verification/spec/relayer/Relayer.tla index 51c691caf2..2238a3048c 100644 --- a/verification/spec/relayer/Relayer.tla +++ b/verification/spec/relayer/Relayer.tla @@ -728,17 +728,17 @@ HeightsDontDecrease == \* Prop \* A conjunction of all properties Prop == - /\ CreateClientIsGenerated - /\ ClientCreated - /\ ClientUpdateIsGenerated +\* /\ CreateClientIsGenerated +\* /\ ClientCreated +\* /\ ClientUpdateIsGenerated /\ ClientUpdated - /\ ConnOpenInitIsGenerated - /\ ConnectionOpened - /\ ChanOpenInitIsGenerated - /\ ChannelOpened - /\ HeightsDontDecrease +\* /\ ConnOpenInitIsGenerated +\* /\ ConnectionOpened +\* /\ ChanOpenInitIsGenerated +\* /\ ChannelOpened +\* /\ HeightsDontDecrease ============================================================================= \* Modification History -\* Last modified Fri May 22 17:20:08 CEST 2020 by ilinastoilkovska +\* Last modified Tue May 26 11:30:45 CEST 2020 by ilinastoilkovska \* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska From a2e8dfd407a6ca9179295efb64b240fa6f81ccdf Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Tue, 26 May 2020 12:43:19 +0200 Subject: [PATCH 7/7] small fix --- verification/spec/relayer/Environment.tla | 11 ++++++----- verification/spec/relayer/Relayer.tla | 18 +++++++++--------- 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/verification/spec/relayer/Environment.tla b/verification/spec/relayer/Environment.tla index 5011a52ddc..da33e5c04a 100644 --- a/verification/spec/relayer/Environment.tla +++ b/verification/spec/relayer/Environment.tla @@ -267,7 +267,7 @@ AdvanceChain(chainID) == /\ UNCHANGED incomingDatagrams \* Receive the datagrams and update the chain state -ReceiveDatagrams(chainID) == +ReceiveIncomingDatagrams(chainID) == /\ incomingDatagrams[chainID] /= {} /\ chains' = [chains EXCEPT ![chainID] = UpdateChain(chainID, incomingDatagrams[chainID]) @@ -324,16 +324,17 @@ Init == \* - advances its height \* - receives datagrams and updates its state Next == - \E chainID \in ChainIDs : + \E chainID \in ChainIDs : \/ AdvanceChain(chainID) - \/ ReceiveDatagrams(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(ReceiveDatagrams(chainID)) + /\ \A chainID \in ChainIDs : WF_vars(ReceiveIncomingDatagrams(chainID)) (*************************************************************************** Invariants @@ -345,5 +346,5 @@ TypeOK == ============================================================================= \* Modification History -\* Last modified Fri May 22 17:09:26 CEST 2020 by ilinastoilkovska +\* 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/Relayer.tla b/verification/spec/relayer/Relayer.tla index 2238a3048c..12c9df8f5e 100644 --- a/verification/spec/relayer/Relayer.tla +++ b/verification/spec/relayer/Relayer.tla @@ -728,17 +728,17 @@ HeightsDontDecrease == \* Prop \* A conjunction of all properties Prop == -\* /\ CreateClientIsGenerated -\* /\ ClientCreated -\* /\ ClientUpdateIsGenerated + /\ CreateClientIsGenerated + /\ ClientCreated + /\ ClientUpdateIsGenerated /\ ClientUpdated -\* /\ ConnOpenInitIsGenerated -\* /\ ConnectionOpened -\* /\ ChanOpenInitIsGenerated -\* /\ ChannelOpened -\* /\ HeightsDontDecrease + /\ ConnOpenInitIsGenerated + /\ ConnectionOpened + /\ ChanOpenInitIsGenerated + /\ ChannelOpened + /\ HeightsDontDecrease ============================================================================= \* Modification History -\* Last modified Tue May 26 11:30:45 CEST 2020 by ilinastoilkovska +\* Last modified Tue May 26 12:13:36 CEST 2020 by ilinastoilkovska \* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska