From 09f51165dbb022a1dee6c9c58f42871560fafb69 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Thu, 15 Apr 2021 13:36:33 +0200 Subject: [PATCH] A modular TLA+ spec of ICS02 (containing type annotations for Snowcat) (#825) * IBC client protocol * client specs, work with apalache * small fix * map of clients in chain store * type annotations * type annotation empty set * client update history tracking * fixed type annotations and single chain instantiation * client spec in tla directory * type annotations and comments * modified MC files * type invariants and README --- docs/spec/tla/client/Chain.tla | 137 ++++++++++++++ docs/spec/tla/client/ICS02ClientHandlers.tla | 97 ++++++++++ docs/spec/tla/client/ICS02Definitions.tla | 120 +++++++++++++ .../client/ICS02SingleChainEnvironment.tla | 107 +++++++++++ .../tla/client/ICS02TwoChainsEnvironment.tla | 167 ++++++++++++++++++ docs/spec/tla/client/MC_SingleChain.tla | 17 ++ docs/spec/tla/client/MC_TwoChains.tla | 22 +++ docs/spec/tla/client/README.md | 80 +++++++++ 8 files changed, 747 insertions(+) create mode 100644 docs/spec/tla/client/Chain.tla create mode 100644 docs/spec/tla/client/ICS02ClientHandlers.tla create mode 100644 docs/spec/tla/client/ICS02Definitions.tla create mode 100644 docs/spec/tla/client/ICS02SingleChainEnvironment.tla create mode 100644 docs/spec/tla/client/ICS02TwoChainsEnvironment.tla create mode 100644 docs/spec/tla/client/MC_SingleChain.tla create mode 100644 docs/spec/tla/client/MC_TwoChains.tla create mode 100644 docs/spec/tla/client/README.md diff --git a/docs/spec/tla/client/Chain.tla b/docs/spec/tla/client/Chain.tla new file mode 100644 index 0000000000..765c9b2450 --- /dev/null +++ b/docs/spec/tla/client/Chain.tla @@ -0,0 +1,137 @@ +----------------------------- MODULE Chain ------------------------------ + +(*************************************************************************** + This module models the behavior of a chain running the IBC Core Client + Protocol. +****************************************************************************) + +EXTENDS Integers, FiniteSets, ICS02ClientHandlers, ICS02Definitions + +CONSTANTS + MaxHeight, \* maximal chain height + ChainID, \* chain identifier + NrClients, \* number of clients that will be created on the chain + ClientIDs \* a set of counterparty client IDs + +VARIABLES + chainStore, \* chain store, containing a client state for each client + incomingDatagrams, \* set of incoming datagrams + history \* history variable + +vars == <> +Heights == 1..MaxHeight \* set of possible heights of the chains in the system + +\* @type: (CHAINSTORE, Str) => Int; +GetClientNr(store, clientID) == + IF \E clientNr \in DOMAIN chainStore.clientStates : + store.clientStates[clientNr].clientID = clientID + THEN CHOOSE clientNr \in DOMAIN store.clientStates : + store.clientStates[clientNr].clientID = clientID + ELSE 0 + +(*************************************************************************** + Client update operators + ***************************************************************************) +\* Update the clients on chain with chainID, +\* using the client datagrams generated by the relayer +\* (Handler operators defined in ClientHandlers.tla) +LightClientUpdate(chainID, store, clientID, datagrams) == + \* create client + LET clientCreatedStore == HandleCreateClient(store, clientID, datagrams) IN + \* update client + LET clientUpdatedStore == HandleClientUpdate(clientCreatedStore, clientID, datagrams, MaxHeight) IN + + clientUpdatedStore + +(*************************************************************************** + Chain actions + ***************************************************************************) +\* Advance the height of the chain until MaxHeight is reached +AdvanceChain == + /\ chainStore.height + 1 \in Heights + /\ chainStore' = [chainStore EXCEPT !.height = chainStore.height + 1] + /\ UNCHANGED <> + +\* Handle the datagrams and update the chain state +HandleIncomingDatagrams == + /\ incomingDatagrams /= {} + /\ \E clientID \in ClientIDs : + /\ chainStore' = LightClientUpdate(ChainID, chainStore, clientID, incomingDatagrams) + /\ history' = [history EXCEPT ![clientID] = + LET clientNr == GetClientNr(chainStore', clientID) IN + IF /\ clientNr /= 0 + /\ ~history[clientID].created + /\ chainStore.clientStates[clientNr].clientID = nullClientID + /\ chainStore'.clientStates[clientNr].clientID /= nullClientID + THEN [created |-> TRUE, updated |-> history[clientID].updated] + ELSE IF /\ clientNr /= 0 + /\ history[clientID].created + /\ chainStore.clientStates[clientNr].heights /= chainStore'.clientStates[clientNr].heights + /\ chainStore.clientStates[clientNr].heights \subseteq chainStore'.clientStates[clientNr].heights + THEN [created |-> history[clientID].created, updated |-> TRUE] + ELSE history[clientID] + ] + /\ incomingDatagrams' = {dgr \in incomingDatagrams : dgr.clientID /= clientID} + +(*************************************************************************** + Specification + ***************************************************************************) +\* Initial state predicate +\* Initially +\* - each chain is initialized to InitChain (defined in RelayerDefinitions.tla) +\* - pendingDatagrams for each chain is empty +\* - the packetSeq is set to 1 +Init == + /\ chainStore = ICS02InitChainStore(NrClients, ClientIDs) + /\ incomingDatagrams = {} + +\* Next state action +\* The chain either +\* - advances its height +\* - receives datagrams and updates its state +\* - sends a packet if the appPacketSeq is not bigger than MaxPacketSeq +\* - acknowledges a packet +Next == + \/ AdvanceChain + \/ HandleIncomingDatagrams + \/ UNCHANGED vars + +Fairness == + /\ WF_vars(AdvanceChain) + /\ WF_vars(HandleIncomingDatagrams) + +(*************************************************************************** + Invariants + ***************************************************************************) +\* Type invariant +\* ChainStores and Datagrams are defined in RelayerDefinitions.tla +TypeOK == + /\ chainStore \in ChainStores(NrClients, ClientIDs, MaxHeight) + /\ incomingDatagrams \in SUBSET Datagrams(ClientIDs, MaxHeight) + +\* two clients with the same ID cannot be created +CreatedClientsHaveDifferentIDs == + (\A clientNr \in 1..NrClients : + chainStore.clientStates[clientNr].clientID /= nullClientID) + => (\A clientNr1 \in 1..NrClients : \A clientNr2 \in 1..NrClients : + clientNr1 /= clientNr2 + => chainStore.clientStates[clientNr1].clientID /= + chainStore.clientStates[clientNr2].clientID) + +\* only created clients can be updated +UpdatedClientsAreCreated == + \A clID \in ClientIDs : + history[clID].updated => history[clID].created + +(*************************************************************************** + Properties + ***************************************************************************) +\* it ALWAYS holds that the height of the chain does not EVENTUALLY decrease +HeightDoesntDecrease == + [](\A h \in Heights : chainStore.height = h + => <>(chainStore.height >= h)) + +============================================================================= +\* Modification History +\* Last modified Thu Apr 15 12:17:59 CEST 2021 by ilinastoilkovska +\* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/client/ICS02ClientHandlers.tla b/docs/spec/tla/client/ICS02ClientHandlers.tla new file mode 100644 index 0000000000..2e31ed2df5 --- /dev/null +++ b/docs/spec/tla/client/ICS02ClientHandlers.tla @@ -0,0 +1,97 @@ +----------------------- MODULE ICS02ClientHandlers ------------------------- + +(*************************************************************************** + This module contains definitions of operators that are used to handle + client create and update datagrams. + ***************************************************************************) + +EXTENDS Integers, FiniteSets, ICS02Definitions + +(*************************************************************************** + Client datagram handlers + ***************************************************************************) + +\* Handle "CreateClient" datagrams +\* @type: (CHAINSTORE, Str, Set(DATAGRAM)) => CHAINSTORE; +HandleCreateClient(chain, clientID, datagrams) == + \* get "CreateClient" datagrams with valid clientID + LET createClientDgrs == {dgr \in datagrams : + /\ dgr.type = "CreateClient" + /\ dgr.clientID = clientID} IN + \* get heights in datagrams with correct counterparty clientID for chainID + LET createClientHeights == {dgr.height : dgr \in createClientDgrs} IN + \* get next available client number where a client can be created + LET nextClientNr == + IF /\ \A clientNr \in DOMAIN chain.clientStates : + chain.clientStates[clientNr].clientID /= clientID + /\ \E clientNr \in DOMAIN chain.clientStates : + chain.clientStates[clientNr].clientID = nullClientID + THEN CHOOSE clientNr \in DOMAIN chain.clientStates : + \/ /\ clientNr = 1 + /\ chain.clientStates[clientNr].clientID = nullClientID + \/ /\ clientNr - 1 \in DOMAIN chain.clientStates + /\ chain.clientStates[clientNr - 1].clientID /= nullClientID + /\ chain.clientStates[clientNr].clientID = nullClientID + ELSE 0 IN + + \* new chain record with client created + LET clientCreateChain == + IF nextClientNr \in DOMAIN chain.clientStates + THEN [chain EXCEPT !.clientStates = + [chain.clientStates EXCEPT ![nextClientNr] = + \* if the slot at nextClientNr is an empty slot + IF /\ chain.clientStates[nextClientNr].clientID = nullClientID + \* if the set of heights from datagrams is not empty + /\ createClientHeights /= {} + \* then create a client with clientID at the slot nextClientNr + THEN [clientID |-> clientID, + heights |-> {Max(createClientHeights)}] + \* otherwise, discard CreateClient datagrams + ELSE chain.clientStates[nextClientNr] + ]] + ELSE chain IN + + clientCreateChain + +\* Handle "ClientUpdate" datagrams +\* @type: (CHAINSTORE, Str, Set(DATAGRAM), Int) => CHAINSTORE; +HandleClientUpdate(chain, clientID, datagrams, MaxHeight) == + \* get the client number of the client with clientID + LET clientNr == IF \E clientNr \in DOMAIN chain.clientStates : + chain.clientStates[clientNr].clientID = clientID + THEN CHOOSE clientNr \in DOMAIN chain.clientStates : + chain.clientStates[clientNr].clientID = clientID + ELSE 0 IN + \* max client height of client ID + LET maxClientHeight == IF clientNr /= 0 + THEN Max(chain.clientStates[clientNr].heights) + ELSE MaxHeight IN + \* get "ClientUpdate" datagrams with valid clientID + LET updateClientDgrs == {dgr \in datagrams : + /\ dgr.type = "ClientUpdate" + /\ dgr.clientID = clientID + /\ maxClientHeight < dgr.height} IN + \* get heights in datagrams with correct counterparty clientID for chainID + LET updateClientHeights == {dgr.height : dgr \in updateClientDgrs} IN + + \* new chain record with client updated + LET clientUpdatedChain == + IF clientNr \in DOMAIN chain.clientStates + THEN [chain EXCEPT !.clientStates = + [chain.clientStates EXCEPT ![clientNr] = + \* if clientNr is a valid client number + IF /\ clientNr \in DOMAIN chain.clientStates + \* if the slot at clientNr holds a client with clientID + /\ chain.clientStates[clientNr].clientID = clientID + THEN [chain.clientStates[clientNr] EXCEPT !.heights = + chain.clientStates[clientNr].heights \union updateClientHeights] + ELSE chain.clientStates[clientNr] + ]] + ELSE chain IN + + clientUpdatedChain + +============================================================================= +\* Modification History +\* Last modified Wed Apr 14 18:46:39 CEST 2021 by ilinastoilkovska +\* Created Tue Apr 07 16:42:47 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/tla/client/ICS02Definitions.tla b/docs/spec/tla/client/ICS02Definitions.tla new file mode 100644 index 0000000000..d7b367166a --- /dev/null +++ b/docs/spec/tla/client/ICS02Definitions.tla @@ -0,0 +1,120 @@ +-------------------------- MODULE ICS02Definitions -------------------------- + +(*************************************************************************** + This module contains definitions of operators that are shared between the + different modules, and which are relevant for ICS02. + ***************************************************************************) + +EXTENDS Integers, FiniteSets, Sequences + +(************************ TYPE ALIASES FOR SNOWCAT *************************) +(* @typeAlias: CLIENTSTATE = + [ + clientID: Str, + heights: Set(Int) + ]; +*) +(* @typeAlias: CHAINSTORE = + [ + height: Int, + clientStates: Int -> CLIENTSTATE + ]; +*) +(* @typeAlias: DATAGRAM = + [ + type: Str, + clientID: Str, + height: Int + ]; +*) + +(********************** Common operator definitions ***********************) +ChainIDs == {"chainA", "chainB"} + +nullHeight == 0 +nullClientID == "none" + +Max(S) == CHOOSE x \in S: \A y \in S: y <= x + +BoundedSeq(S, bound) == UNION {[1..n -> S] : n \in 1..bound} + +SetHeights(h1, h2) == {h \in 1..10 : h1 <= h /\ h <= h2} + +(****************************** ClientStates ******************************* + A client state is a set of heights + ***************************************************************************) +ClientStates(ClientIDs, maxHeight) == + [ + clientID : ClientIDs, + heights : SUBSET(1..maxHeight) + ] + +NullClientState == + [ + clientID |-> nullClientID, + heights |-> {} + ] + +(******************************** ChainStores ****************************** + A set of chain store records, with fields relevant for ICS02. + A chain store record contains the following fields: + + - height : an integer between nullHeight and MaxHeight. + Stores the current height of the chain. + + - counterpartyClientHeights : a set of integers between 1 and MaxHeight + Stores the heights of the client for the counterparty chain. + + ***************************************************************************) +ChainStores(NrClients, ClientIDs, maxHeight) == + [ + height : 1..maxHeight, + clientStates : [1..NrClients -> ClientStates(ClientIDs, maxHeight) \union {NullClientState}] + ] + +(******************************** Datagrams ********************************) +\* Set of datagrams +Datagrams(ClientIDs, maxHeight) == + [type : {"CreateClient"}, clientID : ClientIDs, height : 1..maxHeight] + \union + [type : {"ClientUpdate"}, clientID : ClientIDs, height : 1..maxHeight] + +\* Set of client datagrams for a specific set ClientIDs of client IDs. +ClientDatagrams(ClientIDs, Heights) == + [type : {"CreateClient"}, clientID : ClientIDs, height : Heights] + \union + [type : {"ClientUpdate"}, clientID : ClientIDs, height : Heights] + +\* Null datagram +NullDatagram == + [type |-> "null"] + +(*************************************************************************** + Initial value of a chain store for ICS02 + ***************************************************************************) +\* Initial value of the chain store for ICS02: +\* - height is initialized to 1 +\* - the counterparty clients are uninitialized +ICS02InitChainStore(NrClients, ClientIDs) == + [ + height |-> 1, + clientStates |-> [clientNr \in 1..NrClients |-> NullClientState] + ] + +(*************************************************************************** + Client helper operators + ***************************************************************************) + +\* get the ID of chainID's counterparty chain +GetCounterpartyChainID(chainID) == + IF chainID = "chainA" THEN "chainB" ELSE "chainA" + +\* get the latest height of chainID +\* @type: (CHAINSTORE) => Int; +GetLatestHeight(chain) == + chain.height + +========================================================================= +\* Modification History +\* Last modified Thu Apr 15 12:17:55 CEST 2021 by ilinastoilkovska +\* Created Tue Oct 06 16:26:25 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/tla/client/ICS02SingleChainEnvironment.tla b/docs/spec/tla/client/ICS02SingleChainEnvironment.tla new file mode 100644 index 0000000000..41a58038ee --- /dev/null +++ b/docs/spec/tla/client/ICS02SingleChainEnvironment.tla @@ -0,0 +1,107 @@ +-------------------- MODULE ICS02SingleChainEnvironment -------------------- + +(*************************************************************************** + A TLA+ specification of the IBC client protocol (ICS02). This module models + a system consisting of one chain that can create multiple clients, and which + operates in an environment that overapproximates the behavior of a correct + relayer. + ***************************************************************************) + +EXTENDS Integers, FiniteSets, Sequences, ICS02Definitions + +CONSTANTS + \* @type: Int; + MaxHeight, \* maximal height of all the chains in the system + \* @type: Int; + NrClientsChainA, \* number of clients that will be created on the chain + \* @type: Set(Str); + ClientIDsChainA \* a set of counterparty client IDs for the chain + +ASSUME MaxHeight < 10 + +VARIABLES + \* @type: CHAINSTORE; + chainAstore, \* store of ChainA + \* @type: Set(DATAGRAM); + datagramsChainA, \* set of datagrams incoming to ChainA + \* @type: Str -> [created: Bool, updated: Bool]; + history \* history variable + +vars == <> + +(*************************************************************************** + Instances of ICS02Chain + ***************************************************************************) + +\* We suppose there is a single chain, ChainA +\* ChainA -- Instance of Chain.tla +ChainA == INSTANCE Chain + WITH ChainID <- "chainA", + NrClients <- NrClientsChainA, + ClientIDs <- ClientIDsChainA, + chainStore <- chainAstore, + incomingDatagrams <- datagramsChainA + +(*************************************************************************** + ICS02Environment actions + ***************************************************************************) + +\* non-deterministically create datagrams +CreateDatagrams == + \* pick a sequence from the set of client datagrams non-deterministically + /\ datagramsChainA' \in + SUBSET ClientDatagrams( + ClientIDsChainA, + SetHeights(1, MaxHeight) + ) + + /\ UNCHANGED <> + + +(*************************************************************************** + Component actions + ***************************************************************************) + +\* ChainAction: the chain takes a step +ChainAction == + ChainA!Next + +\* EnvironmentAction: non-deterministically create datagrams +EnvironmentAction == + CreateDatagrams + +(*************************************************************************** + Specification + ***************************************************************************) +\* Initial state predicate +Init == + /\ ChainA!Init + /\ history = [clientID \in ClientIDsChainA |-> [created |-> FALSE, updated |-> FALSE]] + +\* Next state action +Next == + \/ ChainAction + \/ EnvironmentAction + \/ UNCHANGED vars + +\* Specification formula +Spec == Init /\ [][Next]_vars + +(*************************************************************************** + Invariants + ***************************************************************************) + +\* type invariant +TypeOK == + /\ ChainA!TypeOK + /\ history \in [ClientIDsChainA -> [created : BOOLEAN, updated : BOOLEAN]] + +\* conjunction of invariants +ICS02SingleChainInv == + /\ ChainA!CreatedClientsHaveDifferentIDs + /\ ChainA!UpdatedClientsAreCreated + +============================================================================= +\* Modification History +\* Last modified Thu Apr 15 12:16:46 CEST 2021 by ilinastoilkovska +\* Created Fri Oct 02 12:57:19 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/tla/client/ICS02TwoChainsEnvironment.tla b/docs/spec/tla/client/ICS02TwoChainsEnvironment.tla new file mode 100644 index 0000000000..f8ed9f67b1 --- /dev/null +++ b/docs/spec/tla/client/ICS02TwoChainsEnvironment.tla @@ -0,0 +1,167 @@ +---------------------- MODULE ICS02TwoChainsEnvironment ---------------------- + +(*************************************************************************** + A TLA+ specification of the IBC client protocol (ICS02). This module models + a system consisting of two chain that can create multiple clients, and which + operate in an environment that overapproximates the behavior of a correct + relayer. + ***************************************************************************) + +EXTENDS Integers, FiniteSets, Sequences, ICS02Definitions + +CONSTANTS + \* @type: Int; + MaxHeight, \* maximal height of all the chains in the system + \* @type: Int; + NrClientsChainA, \* number of clients that will be created on ChainA + \* @type: Int; + NrClientsChainB, \* number of clients that will be created on ChainB + \* @type: Set(Str); + ClientIDsChainA, \* a set of counterparty client IDs for ChainA + \* @type: Set(Str); + ClientIDsChainB \* a set of counterparty client IDs for ChainB + +ASSUME MaxHeight < 10 +ASSUME ClientIDsChainA \intersect ClientIDsChainB = {} + +VARIABLES + \* @type: CHAINSTORE; + chainAstore, \* store of ChainA + \* @type: CHAINSTORE; + chainBstore, \* store of ChainB + \* @type: Set(DATAGRAM); + datagramsChainA, \* set of datagrams incoming to ChainA + \* @type: Set(DATAGRAM); + datagramsChainB, \* set of datagrams incoming to ChainB + \* @type: Str -> [created: Bool, updated: Bool]; + history \* history variable + +chainAvars == <> +chainBvars == <> +vars == <> + +(*************************************************************************** + Instances of ICS02Chain + ***************************************************************************) + +\* We suppose there are two chains that communicate, ChainA and ChainB +\* ChainA -- Instance of Chain.tla +ChainA == INSTANCE Chain + WITH ChainID <- "chainA", + NrClients <- NrClientsChainA, + ClientIDs <- ClientIDsChainA, + chainStore <- chainAstore, + incomingDatagrams <- datagramsChainA + +\* ChainB -- Instance of Chain.tla +ChainB == INSTANCE Chain + WITH ChainID <- "chainB", + NrClients <- NrClientsChainB, + ClientIDs <- ClientIDsChainB, + chainStore <- chainBstore, + incomingDatagrams <- datagramsChainB + +GetChainByID(chainID) == + IF chainID = "chainA" + THEN chainAstore + ELSE chainBstore + +GetNrClientsByID(chainID) == + IF chainID = "chainA" + THEN NrClientsChainA + ELSE NrClientsChainB + + +(*************************************************************************** + ICS02Environment actions + ***************************************************************************) + +\* non-deterministically create datagrams +CreateDatagrams == + \* pick a sequence from the set of client datagrams non-deterministically + \* for each chain + /\ datagramsChainA = {} + /\ datagramsChainB = {} + /\ datagramsChainA' \in + SUBSET ClientDatagrams( + ClientIDsChainA, + SetHeights(1, GetLatestHeight(GetChainByID("chainB"))) + ) + /\ datagramsChainB' \in + SUBSET ClientDatagrams( + ClientIDsChainB, + SetHeights(1, GetLatestHeight(GetChainByID("chainA"))) + ) + + /\ UNCHANGED <> + /\ UNCHANGED history + + +(*************************************************************************** + Component actions + ***************************************************************************) + +\* ChainAction: either chain takes a step, leaving the other +\* variables unchanged +ChainAction == + \/ /\ ChainA!Next + /\ UNCHANGED chainBvars + \/ /\ ChainB!Next + /\ UNCHANGED chainAvars + +\* EnvironmentAction: non-deterministically create datagrams +EnvironmentAction == + CreateDatagrams + +(*************************************************************************** + Specification + ***************************************************************************) +\* Initial state predicate +Init == + /\ ChainA!Init + /\ ChainB!Init + /\ history = [clientID \in (ClientIDsChainA \union ClientIDsChainB) |-> + [created |-> FALSE, updated |-> FALSE]] + +\* Next state action +Next == + \/ ChainAction + \/ EnvironmentAction + \/ UNCHANGED vars + +\* Specification formula +Spec == Init /\ [][Next]_vars + +(*************************************************************************** +Invariants + ***************************************************************************) + +\* type invariant +TypeOK == + /\ ChainA!TypeOK + /\ ChainB!TypeOK + /\ history \in [ClientIDsChainA -> [created : BOOLEAN, updated : BOOLEAN]] + +\* the maximum client height is less than or equal to the current height of +\* the counterparty chain +ClientHeightsAreBelowCounterpartyHeight == + \A chainID \in ChainIDs : + \A clientNr \in 1..GetNrClientsByID(chainID) : + (GetChainByID(chainID).clientStates[clientNr].heights /= {} + => (Max(GetChainByID(chainID).clientStates[clientNr].heights) + <= GetLatestHeight(GetChainByID(GetCounterpartyChainID(chainID))))) + +\* conjunction of invariants +ICS02TwoChainsInv == + /\ ChainA!CreatedClientsHaveDifferentIDs + /\ ChainA!UpdatedClientsAreCreated + /\ ChainB!CreatedClientsHaveDifferentIDs + /\ ChainB!UpdatedClientsAreCreated + /\ ClientHeightsAreBelowCounterpartyHeight + +============================================================================= +\* Modification History +\* Last modified Wed Apr 14 19:08:27 CEST 2021 by ilinastoilkovska +\* Created Fri Oct 02 12:57:19 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/tla/client/MC_SingleChain.tla b/docs/spec/tla/client/MC_SingleChain.tla new file mode 100644 index 0000000000..68dd22c294 --- /dev/null +++ b/docs/spec/tla/client/MC_SingleChain.tla @@ -0,0 +1,17 @@ +--------------------------- MODULE MC_SingleChain --------------------------- + +MaxHeight == 4 +NrClientsChainA == 2 +ClientIDsChainA == {"B1", "B2"} + +VARIABLES + \* @type: CHAINSTORE; + chainAstore, \* store of ChainA + \* @type: Set(DATAGRAM); + datagramsChainA, \* set of datagrams incoming to ChainA + \* @type: Str -> [created: Bool, updated: Bool]; + history \* history variable + +INSTANCE ICS02SingleChainEnvironment + +============================================================================= diff --git a/docs/spec/tla/client/MC_TwoChains.tla b/docs/spec/tla/client/MC_TwoChains.tla new file mode 100644 index 0000000000..7bbf436552 --- /dev/null +++ b/docs/spec/tla/client/MC_TwoChains.tla @@ -0,0 +1,22 @@ +---------------------------- MODULE MC_TwoChains ---------------------------- + +MaxHeight == 4 +NrClientsChainA == 2 +NrClientsChainB == 2 +ClientIDsChainA == {"B1", "B2"} +ClientIDsChainB == {"A1", "A2"} + +VARIABLES + \* @type: CHAINSTORE; + chainAstore, \* store of ChainA + \* @type: CHAINSTORE; + chainBstore, \* store of ChainB + \* @type: Set(DATAGRAM); + datagramsChainA, \* set of datagrams incoming to ChainA + \* @type: Set(DATAGRAM); + datagramsChainB, \* set of datagrams incoming to ChainB + \* @type: Str -> [created: Bool, updated: Bool]; + history \* history variable + +INSTANCE ICS02TwoChainsEnvironment +============================================================================= \ No newline at end of file diff --git a/docs/spec/tla/client/README.md b/docs/spec/tla/client/README.md new file mode 100644 index 0000000000..fbfbbbbece --- /dev/null +++ b/docs/spec/tla/client/README.md @@ -0,0 +1,80 @@ +# TLA+ specification of the IBC Core Client Protocol + +This document describes the TLA+ models of the core logic of the English specification +[ICS02](https://github.com/cosmos/ibc/tree/5877197dc03e844542cb8628dd52674a37ca6ff9/spec/ics-002-client-semantics). +We start by discussing [the model of the +protocol](#the-model-of-the-protocol). +Then, we discuss the [invariants](#invariants) that we formalize, and finally, we +discuss how to [use the model](#using-the-model). + +## The Model of the Protocol + +We present models two of two different systems, which are used to check +different invariants: +1. The first system, specified in [ICS02SingleChainEnvironment.tla](ICS02SingleChainEnvironment.tla), consists of a single chain that can +create multiple clients. +The chain operates in an environment that overapproximates the +behavior of a correct relayer. +2. The second system, specified in [ICS02TwoChainsEnvironment.tla](ICS02TwoChainsEnvironment.tla), consists of two chain that can +create multiple clients. +The relayer is again overapproximated using an environment. + +Both systems extend the following modules: +- [Chain.tla](Chain.tla), which models the behavior of a chain running the IBC Core Client Protocol. +- [ICS02ClientHandlers.tla](ICS02ClientHandlers.tla), which contains definitions of +operators that are used to handle client creation and client update events. +- [ICS02Definitions.tla](ICS02Definitions.tla), which contains definitions of operators that are shared between the + different modules, and which are relevant for ICS02. + +## Invariants + +The module [Chain.tla](Chain.tla) defines the following invariants: +- `TypeOK`, the type invariant, +- `CreatedClientsHaveDifferentIDs`, which ensures that two clients two clients with the same ID cannot be created, +- `UpdatedClientsAreCreated`, which ensures that only created clients can be updated. + +These invariants are checked for a system of single chain in [ICS02SingleChainEnvironment.tla](ICS02SingleChainEnvironment.tla), and for a system of two chains in [ICS02TwoChainsEnvironment.tla](ICS02TwoChainsEnvironment.tla). +Additionally, [ICS02SingleChainEnvironment](ICS02TwoChainsEnvironment.tla) checks the invariant: +- `ClientHeightsAreBelowCounterpartyHeight`, which ensures that the maximum client +height is less than or equal to the current height of the counterparty chain. + + +## Using the Model + +### Constants + +The modules `ICS02SingleChainEnvironment.tla` and `ICS02TwoChainsEnvironment.tla` +are parameterized by the constants: + - `MaxHeight`, a natural number denoting the maximal height of the chains, + - `NrClientsChainA`, a number of clients that will be created on ChainA + - `NrClientsChainB`, a number of clients that will be created on ChainB + - `ClientIDsChainA`, a set of counterparty client IDs for ChainA + - `ClientIDsChainB`, a set of counterparty client IDs for ChainB + +We assume that the sets `ClientIDsChainA` and `ClientIDsChainB` contain distinct +client IDs. + + +### Importing the specification into TLA+ toolbox + +To import the specification in the TLA+ toolbox and run TLC: + - add a new spec in TLA+ toolbox with the root-module file `ICS02SingleChainEnvironment.tla` (or `ICS02TwoChainsEnvironment.tla`) + - create a model + - assign a value to the constants (example values can be found in `ICS02SingleChainEnvironment.cfg` (or `ICS02TwoChainsEnvironment.tla`)) + - choose "Temporal formula" as the behavior spec, and use the formula `Spec` + - choose invariants/properties that should be checked + - run TLC on the model + +#### Basic checks with TLC + +We ran TLC on `ICS02SingleChainEnvironment.tla` using the constants defined +in `ICS02SingleChainEnvironment.cfg`. +We were able to check the invariants described above within seconds. + +#### Apalache + +The specification contains type annotations for the +model checker [Apalache](https://github.com/informalsystems/apalache). +The specification passes the type check using the type checker [Snowcat](https://apalache.informal.systems/docs/apalache/typechecker-snowcat.html) +integrated in Apalache. +