Skip to content

Commit

Permalink
A modular TLA+ spec of ICS02 (containing type annotations for Snowcat) (
Browse files Browse the repository at this point in the history 
informalsystems#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
  • Loading branch information
istoilkovska authored Apr 15, 2021
1 parent c7d049f commit 09f5116
Show file tree
Hide file tree
Showing 8 changed files with 747 additions and 0 deletions.
137 changes: 137 additions & 0 deletions docs/spec/tla/client/Chain.tla
View file
Original file line number Diff line number Diff line change
@@ -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 == <<chainStore, incomingDatagrams, history>>
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 <<incomingDatagrams, history>>

\* 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
97 changes: 97 additions & 0 deletions docs/spec/tla/client/ICS02ClientHandlers.tla
View file
Original file line number Diff line number Diff line change
@@ -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
120 changes: 120 additions & 0 deletions docs/spec/tla/client/ICS02Definitions.tla
View file
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit 09f5116

Please sign in to comment.