From b2a4182d6645c172568936164ab3be6e28982564 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Wed, 30 Sep 2020 14:31:40 +0200 Subject: [PATCH] Basic packet flow in TLA+ (#248) * send packet action added, relayer packet creation * packet receive, ack * packet ack * readme updated * Apply suggestions from code review Co-authored-by: Anca Zamfir * addressed comments * applied review comments * moved files around Co-authored-by: Anca Zamfir --- docs/spec/relayer/{ => tla}/Chain.tla | 138 +++++++++--- .../relayer/{ => tla}/ChannelHandlers.tla | 0 .../spec/relayer/{ => tla}/ClientHandlers.tla | 0 .../relayer/{ => tla}/ConnectionHandlers.tla | 0 .../relayer/{ => tla}/ICS18Environment.cfg | 0 .../relayer/{ => tla}/ICS18Environment.tla | 45 +++- .../{ => tla}/ICS18Environment_apalache.tla | 0 docs/spec/relayer/tla/PacketHandlers.tla | 203 ++++++++++++++++++ docs/spec/relayer/{ => tla}/README.md | 7 +- docs/spec/relayer/{ => tla}/Relayer.tla | 84 ++++++-- .../relayer/{ => tla}/RelayerDefinitions.tla | 111 ++++++++-- 11 files changed, 510 insertions(+), 78 deletions(-) rename docs/spec/relayer/{ => tla}/Chain.tla (51%) rename docs/spec/relayer/{ => tla}/ChannelHandlers.tla (100%) rename docs/spec/relayer/{ => tla}/ClientHandlers.tla (100%) rename docs/spec/relayer/{ => tla}/ConnectionHandlers.tla (100%) rename docs/spec/relayer/{ => tla}/ICS18Environment.cfg (100%) rename docs/spec/relayer/{ => tla}/ICS18Environment.tla (89%) rename docs/spec/relayer/{ => tla}/ICS18Environment_apalache.tla (100%) create mode 100644 docs/spec/relayer/tla/PacketHandlers.tla rename docs/spec/relayer/{ => tla}/README.md (93%) rename docs/spec/relayer/{ => tla}/Relayer.tla (81%) rename docs/spec/relayer/{ => tla}/RelayerDefinitions.tla (89%) diff --git a/docs/spec/relayer/Chain.tla b/docs/spec/relayer/tla/Chain.tla similarity index 51% rename from docs/spec/relayer/Chain.tla rename to docs/spec/relayer/tla/Chain.tla index 960cc9f104..39ca4a3f60 100644 --- a/docs/spec/relayer/Chain.tla +++ b/docs/spec/relayer/tla/Chain.tla @@ -1,7 +1,7 @@ ---------------------------- MODULE Chain ---------------------------- EXTENDS Integers, FiniteSets, RelayerDefinitions, - ClientHandlers, ConnectionHandlers, ChannelHandlers + ClientHandlers, ConnectionHandlers, ChannelHandlers, PacketHandlers CONSTANTS MaxHeight, \* maximal chain height ChainID, \* chain identifier @@ -10,9 +10,12 @@ CONSTANTS MaxHeight, \* maximal chain height VARIABLES chainStore, \* chain store, containing client heights, a connection end, a channel end incomingDatagrams, \* set of incoming datagrams - history \* history variable + incomingPacketDatagrams, \* sequence of incoming packet datagrams + history, \* history variable + packetLog, \* packet log + appPacketSeq \* packet sequence number from the application on the chain -vars == <> +vars == <> Heights == 1..MaxHeight \* set of possible heights of the chains in the system (*************************************************************************** @@ -78,12 +81,34 @@ ChannelUpdate(chainID, store, datagrams) == chanCloseConfirmStore +(*************************************************************************** + Packet update operators + ***************************************************************************) +\* Update the chain store of the chain with chainID and the packet log, +\* using the packet datagrams generated by the relayer +\* (Handler operators defined in PacketHandlers.tla) +PacketUpdate(chainID, store, packetDatagrams, log) == + \* if the sequence of packet datagrams is not empty + IF packetDatagrams /= AsSeqPacketDatagrams(<<>>) + THEN \* process the packet datagram at the head of the sequence + LET packetDatagram == AsPacketDatagram(Head(packetDatagrams)) IN + LET packet == packetDatagram.packet IN + \* get the new updated store and packet log entry + LET newStoreAndLog == + IF packetDatagram.type = "PacketRecv" + THEN HandlePacketRecv(chainID, store, packetDatagram, log) + ELSE IF packetDatagram.type = "PacketAck" + THEN HandlePacketAck(chainID, store, packetDatagram, log) + ELSE [chainStore|-> store, packetLogEntry |-> log] IN + newStoreAndLog + ELSE [chainStore |-> store, packetLog |->log] + (*************************************************************************** Chain update operators ***************************************************************************) \* Update chainID with the received datagrams -\* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels). -UpdateChainStore(chainID, datagrams) == +\* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels & Packets). +UpdateChainStoreAndPacketLog(chainID, datagrams, packetDatagrams, log) == \* ICS 002: Client updates LET clientUpdatedStore == LightClientUpdate(chainID, chainStore, datagrams) IN @@ -94,15 +119,20 @@ UpdateChainStore(chainID, datagrams) == \* ICS 003: Channel updates LET channelUpdatedStore == ChannelUpdate(chainID, connectionUpdatedStore, datagrams) IN + \* ICS 004: Packet transmission + LET packetUpdatedStoreAndLogEntry == PacketUpdate(chainID, channelUpdatedStore, packetDatagrams, log) IN + LET packetUpdatedStore == packetUpdatedStoreAndLogEntry.chainStore IN \* update height LET updatedChainStore == - IF /\ chainStore /= channelUpdatedStore + IF /\ chainStore /= packetUpdatedStore /\ chainStore.height + 1 \in Heights - THEN [channelUpdatedStore EXCEPT !.height = chainStore.height + 1] - ELSE channelUpdatedStore + THEN [packetUpdatedStore EXCEPT !.height = chainStore.height + 1] + ELSE packetUpdatedStore IN - updatedChainStore + + [chainStore |-> updatedChainStore, + packetLog |-> packetUpdatedStoreAndLogEntry.packetLog] (*************************************************************************** Chain actions @@ -111,29 +141,68 @@ UpdateChainStore(chainID, datagrams) == AdvanceChain == /\ chainStore.height + 1 \in Heights /\ chainStore' = [chainStore EXCEPT !.height = chainStore.height + 1] - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Send a packet +SendPacket == + \* enabled if appPacketSeq is not bigger than MaxPacketSeq + /\ appPacketSeq <= MaxPacketSeq + \* Create a packet: Abstract away from packet data, ports, and timestamp. + \* Assume timeoutHeight is MaxHeight + 1 + /\ LET packet == AsPacket([ + sequence |-> appPacketSeq, + timeoutHeight |-> MaxHeight + 1, + srcChannelID |-> GetChannelID(ChainID), + dstChannelID |-> GetChannelID(GetCounterpartyChainID(ChainID))]) IN + \* update chain store with packet committment + /\ chainStore' = WritePacketCommitment(chainStore, packet) + \* log sent packet + /\ packetLog' = Append(packetLog, AsPacketLogEntry( + [type |-> "PacketSend", + srcChainID |-> ChainID, + sequence |-> packet.sequence , + timeoutHeight |-> packet.timeoutHeight])) + \* increase application packet sequence + /\ appPacketSeq' = appPacketSeq + 1 + /\ UNCHANGED <> + +\* write a packet acknowledgement on the packet log and chain store +AcknowledgePacket == + /\ chainStore.packetsToAcknowledge /= AsSeqPacket(<<>>) + /\ chainStore' = WriteAcknowledgement(chainStore, Head(chainStore.packetsToAcknowledge)) + /\ packetLog' = LogAcknowledgement(ChainID, chainStore, packetLog, Head(chainStore.packetsToAcknowledge)) + /\ UNCHANGED <> + /\ UNCHANGED appPacketSeq \* Handle the datagrams and update the chain state HandleIncomingDatagrams == - /\ incomingDatagrams /= AsSetDatagrams({}) - /\ chainStore' = UpdateChainStore(ChainID, AsSetDatagrams(incomingDatagrams)) - /\ incomingDatagrams' = AsSetDatagrams({}) - /\ history' = CASE chainStore'.connectionEnd.state = "INIT" - -> [history EXCEPT !.connInit = TRUE] - [] chainStore'.connectionEnd.state = "TRYOPEN" - -> [history EXCEPT !.connTryOpen = TRUE] - [] chainStore'.connectionEnd.state = "OPEN" - -> [history EXCEPT !.connOpen = TRUE] - [] chainStore'.connectionEnd.channelEnd.state = "INIT" - -> [history EXCEPT !.chanInit = TRUE] - [] chainStore'.connectionEnd.channelEnd.state = "TRYOPEN" - -> [history EXCEPT !.chanTryOpen = TRUE] - [] chainStore'.connectionEnd.channelEnd.state = "OPEN" - -> [history EXCEPT !.chanOpen = TRUE] - [] chainStore'.connectionEnd.channelEnd.state = "CLOSED" - -> [history EXCEPT !.chanClosed = TRUE] - [] OTHER - -> history + /\ \/ incomingDatagrams /= AsSetDatagrams({}) + \/ incomingPacketDatagrams /= AsSeqPacketDatagrams(<<>>) + /\ LET updatedChainStoreAndPacketLog == UpdateChainStoreAndPacketLog(ChainID, incomingDatagrams, incomingPacketDatagrams, packetLog) IN + /\ chainStore' = updatedChainStoreAndPacketLog.chainStore + /\ packetLog' = updatedChainStoreAndPacketLog.packetLog + /\ incomingDatagrams' = AsSetDatagrams({}) + /\ incomingPacketDatagrams' = IF incomingPacketDatagrams /= AsSeqPacketDatagrams(<<>>) + THEN Tail(incomingPacketDatagrams) + ELSE incomingPacketDatagrams + /\ history' = CASE chainStore'.connectionEnd.state = "INIT" + -> [history EXCEPT !.connInit = TRUE] + [] chainStore'.connectionEnd.state = "TRYOPEN" + -> [history EXCEPT !.connTryOpen = TRUE] + [] chainStore'.connectionEnd.state = "OPEN" + -> [history EXCEPT !.connOpen = TRUE] + [] chainStore'.connectionEnd.channelEnd.state = "INIT" + -> [history EXCEPT !.chanInit = TRUE] + [] chainStore'.connectionEnd.channelEnd.state = "TRYOPEN" + -> [history EXCEPT !.chanTryOpen = TRUE] + [] chainStore'.connectionEnd.channelEnd.state = "OPEN" + -> [history EXCEPT !.chanOpen = TRUE] + [] chainStore'.connectionEnd.channelEnd.state = "CLOSED" + -> [history EXCEPT !.chanClosed = TRUE] + [] OTHER + -> history + /\ UNCHANGED appPacketSeq (*************************************************************************** Specification @@ -146,16 +215,21 @@ HandleIncomingDatagrams == Init == /\ chainStore = InitChainStore(ChannelOrdering) /\ incomingDatagrams = AsSetDatagrams({}) + /\ incomingPacketDatagrams = AsSeqDatagrams(<<>>) /\ history = InitHistory + /\ appPacketSeq = AsInt(1) \* Next state action \* The chain either \* - advances its height \* - receives datagrams and updates its state -\* - sends a packet (TODO) +\* - sends a packet if the appPacketSeq is not bigger than MaxPacketSeq +\* - acknowledges a packet Next == \/ AdvanceChain \/ HandleIncomingDatagrams + \/ SendPacket + \/ AcknowledgePacket \/ UNCHANGED vars Fairness == @@ -171,6 +245,8 @@ TypeOK == /\ chainStore \in ChainStores(MaxHeight, ChannelOrdering, MaxPacketSeq) /\ incomingDatagrams \in SUBSET Datagrams(MaxHeight, MaxPacketSeq) /\ history \in Histories + /\ appPacketSeq \in 1..MaxPacketSeq + /\ packetLog \in SUBSET Packets(MaxHeight, MaxPacketSeq) (*************************************************************************** Properties @@ -182,5 +258,5 @@ HeightDoesntDecrease == ============================================================================= \* Modification History -\* Last modified Thu Sep 10 15:43:42 CEST 2020 by ilinastoilkovska +\* Last modified Wed Sep 30 13:47:16 CEST 2020 by ilinastoilkovska \* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/ChannelHandlers.tla b/docs/spec/relayer/tla/ChannelHandlers.tla similarity index 100% rename from docs/spec/relayer/ChannelHandlers.tla rename to docs/spec/relayer/tla/ChannelHandlers.tla diff --git a/docs/spec/relayer/ClientHandlers.tla b/docs/spec/relayer/tla/ClientHandlers.tla similarity index 100% rename from docs/spec/relayer/ClientHandlers.tla rename to docs/spec/relayer/tla/ClientHandlers.tla diff --git a/docs/spec/relayer/ConnectionHandlers.tla b/docs/spec/relayer/tla/ConnectionHandlers.tla similarity index 100% rename from docs/spec/relayer/ConnectionHandlers.tla rename to docs/spec/relayer/tla/ConnectionHandlers.tla diff --git a/docs/spec/relayer/ICS18Environment.cfg b/docs/spec/relayer/tla/ICS18Environment.cfg similarity index 100% rename from docs/spec/relayer/ICS18Environment.cfg rename to docs/spec/relayer/tla/ICS18Environment.cfg diff --git a/docs/spec/relayer/ICS18Environment.tla b/docs/spec/relayer/tla/ICS18Environment.tla similarity index 89% rename from docs/spec/relayer/ICS18Environment.tla rename to docs/spec/relayer/tla/ICS18Environment.tla index 57ada5ae8d..da2f3d84dd 100644 --- a/docs/spec/relayer/ICS18Environment.tla +++ b/docs/spec/relayer/tla/ICS18Environment.tla @@ -1,6 +1,6 @@ -------------------------- MODULE ICS18Environment -------------------------- -EXTENDS Integers, FiniteSets, RelayerDefinitions +EXTENDS Integers, FiniteSets, Sequences, RelayerDefinitions CONSTANTS MaxHeight, \* maximal height of all the chains in the system MaxPacketSeq, \* maximal packet sequence number (will be used later) @@ -16,24 +16,34 @@ VARIABLES chainAstore, \* store of ChainA chainBstore, \* store of ChainB incomingDatagramsChainA, \* set of datagrams incoming to ChainA incomingDatagramsChainB, \* set of datagrams incoming to ChainB + incomingPacketDatagramsChainA, \* sequence of packet datagrams incoming to ChainA + incomingPacketDatagramsChainB, \* sequence of packet datagrams incoming to ChainB relayer1Heights, \* the client heights of Relayer1 relayer2Heights, \* the client heights of Relayer2 outgoingDatagrams, \* sets of datagrams outgoing of the relayers + outgoingPacketDatagrams, \* sequences of packet datagrams outgoing of the relayers closeChannelA, \* flag that triggers closing of the channel end at ChainA closeChannelB, \* flag that triggers closing of the channel end at ChainB historyChainA, \* history variables for ChainA - historyChainB \* history variables for ChainB + historyChainB, \* history variables for ChainB + packetLog, \* a set of packets sent by both chains + appPacketSeqChainA, \* packet sequence number from the application on ChainA + appPacketSeqChainB \* packet sequence number from the application on ChainA vars == <> + historyChainA, historyChainB, + packetLog, + appPacketSeqChainA, appPacketSeqChainB>> -chainAvars == <> -chainBvars == <> -relayerVars == <> +chainAvars == <> +chainBvars == <> +relayerVars == <> Heights == 1..MaxHeight \* set of possible heights of the chains in the system @@ -62,14 +72,18 @@ ChainA == INSTANCE Chain WITH ChainID <- "chainA", chainStore <- chainAstore, incomingDatagrams <- incomingDatagramsChainA, - history <- historyChainA + incomingPacketDatagrams <- incomingPacketDatagramsChainA, + history <- historyChainA, + appPacketSeq <- appPacketSeqChainA \* ChainB -- Instance of Chain.tla ChainB == INSTANCE Chain WITH ChainID <- "chainB", chainStore <- chainBstore, incomingDatagrams <- incomingDatagramsChainB, - history <- historyChainB + incomingPacketDatagrams <- incomingPacketDatagramsChainB, + history <- historyChainB, + appPacketSeq <- appPacketSeqChainB (*************************************************************************** Component actions @@ -109,9 +123,17 @@ SubmitDatagrams == /\ incomingDatagramsChainA' = AsSetDatagrams(incomingDatagramsChainA \union outgoingDatagrams["chainA"]) /\ incomingDatagramsChainB' = AsSetDatagrams(incomingDatagramsChainB \union outgoingDatagrams["chainB"]) /\ outgoingDatagrams' = [chainID \in ChainIDs |-> AsSetDatagrams({})] + /\ incomingPacketDatagramsChainA' = AsSeqPacketDatagrams(incomingPacketDatagramsChainA + \o + outgoingPacketDatagrams["chainA"]) + /\ incomingPacketDatagramsChainB' = AsSeqPacketDatagrams(incomingPacketDatagramsChainB + \o + outgoingPacketDatagrams["chainB"]) + /\ outgoingPacketDatagrams' = [chainID \in ChainIDs |-> AsSeqPacketDatagrams(<<>>)] /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED <> + /\ UNCHANGED <> \* Non-deterministically set channel closing flags CloseChannels == @@ -121,12 +143,16 @@ CloseChannels == /\ UNCHANGED <> /\ UNCHANGED closeChannelB /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> \/ /\ closeChannelB = FALSE /\ closeChannelB' \in BOOLEAN /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED closeChannelA /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> \* Faulty relayer action FaultyRelayer == @@ -150,6 +176,7 @@ Init == /\ Relayer2!Init /\ closeChannelA = FALSE /\ closeChannelB = FALSE + /\ packetLog = AsPacketLog(<<>>) \* Next state action Next == @@ -539,5 +566,5 @@ ICS18Delivery == ============================================================================= \* Modification History -\* Last modified Thu Sep 10 15:41:47 CEST 2020 by ilinastoilkovska +\* Last modified Fri Sep 18 18:56:16 CEST 2020 by ilinastoilkovska \* Created Fri Jun 05 16:48:22 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/ICS18Environment_apalache.tla b/docs/spec/relayer/tla/ICS18Environment_apalache.tla similarity index 100% rename from docs/spec/relayer/ICS18Environment_apalache.tla rename to docs/spec/relayer/tla/ICS18Environment_apalache.tla diff --git a/docs/spec/relayer/tla/PacketHandlers.tla b/docs/spec/relayer/tla/PacketHandlers.tla new file mode 100644 index 0000000000..32680d9437 --- /dev/null +++ b/docs/spec/relayer/tla/PacketHandlers.tla @@ -0,0 +1,203 @@ +--------------------------- MODULE PacketHandlers --------------------------- + +(*************************************************************************** + This module contains definitions of operators that are used to handle + packet datagrams + ***************************************************************************) + +EXTENDS Integers, FiniteSets, RelayerDefinitions + +(*************************************************************************** + Packet datagram handlers + ***************************************************************************) + +\* Handle "PacketRecv" datagrams +HandlePacketRecv(chainID, chain, packetDatagram, log) == + \* get chainID's connection end + LET connectionEnd == chain.connectionEnd IN + \* get chainID's channel end + LET channelEnd == chain.connectionEnd.channelEnd IN + \* get packet + LET packet == packetDatagram.packet IN + + IF \* if the channel and connection ends are open for packet transmission + /\ channelEnd.state /= "UNINIT" + /\ channelEnd.state = "OPEN" + /\ connectionEnd.state /= "UNINIT" + /\ connectionEnd.state = "OPEN" + \* if the packet has not passed the timeout height + /\ \/ packet.timeoutHeight = 0 + \/ chain.height < packet.timeoutHeight + \* if the "PacketRecv" datagram can be verified + /\ packetDatagram.srcChannelID = channelEnd.channelID + /\ packetDatagram.dstChannelID = channelEnd.counterpartyChannelID + /\ packetDatagram.proofHeight \in chain.counterpartyClientHeights + THEN \* construct log entry for packet log + LET logEntry == AsPacketLogEntry( + [type |-> "PacketRecv", + srcChainID |-> chainID, + sequence |-> packet.sequence, + channelID |-> packet.dstChannelID, + timeoutHeight |-> packet.timeoutHeight + ]) IN + + \* if the channel is unordered and the packet has not been received + IF /\ channelEnd.order = "UNORDERED" + /\ <> \notin chain.packetReceipt + THEN LET newChainStore == [chain EXCEPT + \* record that the packet has been received + !.packetReceipts = chain.packetReceipts + \union + {AsPacketReceipt( + [channelID |-> packet.dstChannelID, + sequence |-> packet.sequence])}, + \* add packet to the set of packets for which an acknowledgement should be written + !.packetsToAcknowledge = Append(chain.packetsToAcknowledge, packet)] IN + + [chainStore |-> newChainStore, packetLog |-> Append(log, logEntry)] + + ELSE \* if the channel is ordered and the packet sequence is nextRcvSeq + IF /\ channelEnd.order = "ORDERED" + /\ packet.sequence = channelEnd.nextRcvSeq + THEN LET newChainStore == [chain EXCEPT + \* increase the nextRcvSeq + !.connectionEnd.channelEnd.nextRcvSeq = + chain.connectionEnd.channelEnd.nextRcvSeq + 1, + \* add packet to the set of packets for which an acknowledgement should be written + !.packetsToAcknowledge = Append(chain.packetsToAcknowledge, packet)] IN + + [chainStore |-> newChainStore, packetLog |-> Append(log, logEntry)] + + + \* otherwise, do not update the chain store and the log + ELSE [chainStore |-> chain, packetLog |-> log] + ELSE [chainStore |-> chain, packetLog |-> log] + + +\* Handle "PacketAck" datagrams +HandlePacketAck(chainID, chain, packetDatagram, log) == + \* get chainID's connection end + LET connectionEnd == chain.connectionEnd IN + \* get chainID's channel end + LET channelEnd == chain.connectionEnd.channelEnd IN + \* get packet + LET packet == packetDatagram.packet IN + \* get packet committment that should be in chain store + LET packetCommitment == AsPacketCommitment( + [channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeihgt |-> packet.timeoutHeight]) IN + + IF \* if the channel and connection ends are open for packet transmission + /\ channelEnd.state /= "UNINIT" + /\ channelEnd.state = "OPEN" + /\ connectionEnd.state /= "UNINIT" + /\ connectionEnd.state = "OPEN" + \* if the packet committment exists in the chain store + /\ packetCommitment \in chain.packetCommittments + \* if the "PacketAck" datagram can be verified + /\ packetDatagram.srcChannelID = GetChannelID(chainID) + /\ packetDatagram.dstChannelID = GetCounterpartyChannelID(chainID) + /\ packetDatagram.proofHeight \in chain.counterpartyClientHeights + THEN \* if the channel is ordered and the packet sequence is nextAckSeq + LET newChainStore == + IF /\ channelEnd.order = "ORDERED" + /\ packet.sequence = channelEnd.nextAckSeq + THEN \* increase the nextAckSeq and remove packet commitment + [chain EXCEPT + !.connectionEnd.channelEnd.nextAckSeq = + chain.connectionEnd.channelEnd.nextAckSeq + 1, + !.packetCommitment = chain.packetCommitment \ {packetCommitment}] + \* otherwise, do not update the chain store + ELSE chain IN + + + [chainStore |-> newChainStore, packetLog |-> log] + \* otherwise, do not update the chain store and the log + ELSE [chainStore |-> chain, packetLog |-> log] + + +\* write packet committments to chain store +WritePacketCommitment(chain, packet) == + \* get connection end + LET connectionEnd == chain.connectionEnd IN + \* get channel end + LET channelEnd == connectionEnd.channelEnd IN + \* get latest counterparty client height + LET latestClientHeight == GetMaxCounterpartyClientHeight(chain) IN + + IF \* channel end is neither null nor closed + /\ channelEnd.state \notin {"UNINIT", "CLOSED"} + \* connection end is initialized + /\ connectionEnd.state /= "UNINIT" + \* timeout height has not passed + /\ \/ packet.timeoutHeight = 0 + \/ latestClientHeight < packet.timeoutHeight + THEN IF \* if the channel is ordered, check if packetSeq is nextSendSeq, + \* add a packet committment in the chain store, and increase nextSendSeq + /\ channelEnd.order = "ORDERED" + /\ packet.sequence = channelEnd.nextSendSeq + THEN [chain EXCEPT + !.packetCommitments = + chain.packetCommitments \union {[channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight]}, + !.connectionEnd.channelEnd.nextSendSeq = channelEnd.nextSendSeq + 1 + ] + \* otherwise, do not update the chain store + ELSE chain + ELSE IF \* if the channel is unordered, + \* add a packet committment in the chain store + /\ channelEnd.order = "UNORDERED" + THEN [chain EXCEPT + !.packetCommitments = + chain.packetCommitments \union {[channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight]} + ] + \* otherwise, do not update the chain store + ELSE chain + +\* write acknowledgements to chain store +WriteAcknowledgement(chain, packet) == + \* if the acknowledgement for the packet has not been written + IF packet \notin chain.packetAcknowledgements + THEN \* write the acknowledgement to the chain store and remove + \* the packet from the set of packets to acknowledge + LET packetAcknowledgement == + AsPacketAcknowledgement( + [channelID |-> packet.dstChannelID, + sequence |-> packet.sequence, + acknowledgement |-> TRUE]) IN + [chain EXCEPT !.packetAcknowledgements = + chain.packetAcknowledgements + \union + {packetAcknowledgement}, + !.packetsToAcknowledge = + Tail(chain.packetsToAcknowledge)] + + \* remove the packet from the set of packets to acknowledge + ELSE [chain EXCEPT !.packetsToAcknowledge = + Tail(chain.packetsToAcknowledge)] + +\* log acknowledgements to packet Log +LogAcknowledgement(chainID, chain, log, packet) == + \* if the acknowledgement for the packet has not been written + IF packet \notin chain.packetAcknowledgements + THEN \* append a "WriteAck" log entry to the log + LET packetLogEntry == + AsPacketLogEntry( + [type |-> "WriteAck", + srcChainID |-> chainID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight, + acknowledgement |-> TRUE]) IN + Append(log, packetLogEntry) + \* do not add anything to the log + ELSE log + + +============================================================================= +\* Modification History +\* Last modified Wed Sep 30 13:48:09 CEST 2020 by ilinastoilkovska +\* Created Wed Jul 29 14:30:04 CEST 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/README.md b/docs/spec/relayer/tla/README.md similarity index 93% rename from docs/spec/relayer/README.md rename to docs/spec/relayer/tla/README.md index 610c03c699..156cda0b36 100644 --- a/docs/spec/relayer/README.md +++ b/docs/spec/relayer/tla/README.md @@ -11,6 +11,7 @@ The specification has seven modules: - `ClientHandlers.tla` - `ConnectionHandlers.tla` - `ChannelHandlers.tla` + - `PacketHandlers.tla` - `RelayerDefinitions.tla` The module `ICS18Environment.tla` creates instances of `Relayer.tla` and @@ -21,8 +22,9 @@ The module `ICS18Environment.tla` creates instances of `Relayer.tla` and The module `Relayer.tla` contains the specification of the relayer algorithm. The module `Chain.tla` captures the chain logic. It extends the modules `ClientHandlers.tla`, -`ConnectionHandlers.tla`, and `ChannelHandlers.tla`, which contain definition of -operators that handle client, connection handshake, and channel handshake +`ConnectionHandlers.tla`, `ChannelHandlers.tla`, and +`PacketHandlers.tla`, which contain definition of +operators that handle client, connection handshake, channel handshake, and packet datagrams, respectively. The module `RelayerDefinitions.tla` contains definition of operators that are used across all the modules. @@ -34,6 +36,7 @@ The module `ICS18Environment.tla` is parameterized by the constants: - `ConnectionDatagramsRelayer_i`, for `i in {1, 2}`, a Boolean flag defining if `Relayer_i` creates connection datagrams, - `ChannelDatagramsRelayer_i`, for `i in {1, 2}`, a Boolean flag defining if `Relayer_i` creates channel datagrams, - `MaxHeight`, a natural number denoting the maximal height of the chains, + - `MaxPacketSeq`, a natural number denoting the maximal packet sequence number, - `ChannelOrdering`, a string indicating whether the channels are ordered or unordered ## Properties diff --git a/docs/spec/relayer/Relayer.tla b/docs/spec/relayer/tla/Relayer.tla similarity index 81% rename from docs/spec/relayer/Relayer.tla rename to docs/spec/relayer/tla/Relayer.tla index c32c8037d5..578e6f2989 100644 --- a/docs/spec/relayer/Relayer.tla +++ b/docs/spec/relayer/tla/Relayer.tla @@ -5,7 +5,7 @@ process running a relayer algorithm ***************************************************************************) -EXTENDS Integers, FiniteSets, RelayerDefinitions +EXTENDS Integers, FiniteSets, Sequences, RelayerDefinitions CONSTANTS GenerateClientDatagrams, \* toggle generation of client datagrams GenerateConnectionDatagrams, \* toggle generation of connection datagrams @@ -21,12 +21,14 @@ CONSTANTS MaxHeight, \* set of possible heights of the chains in the system VARIABLES chainAstore, \* store of ChainA chainBstore, \* store of ChainB outgoingDatagrams, \* a function that assigns a set of pending datagrams - \* outgoing from the relayer to each chainID + \* outgoing from the relayer to each chainID + outgoingPacketDatagrams, \* a dedicated datagrams channel for packet datagrams relayerHeights, \* a function that assigns a height to each chainID closeChannelA, \* flag that triggers closing of the channel end at ChainA - closeChannelB \* flag that triggers closing of the channel end at ChainB + closeChannelB, \* flag that triggers closing of the channel end at ChainB + packetLog \* packet log -vars == <> +vars == <> Heights == 1..MaxHeight \* set of possible heights of the chains in the system GetChainByID(chainID) == @@ -46,7 +48,7 @@ GetCloseChannelFlag(chainID) == \* These are used to update the client for srcChainID on dstChainID. \* Some client updates might trigger an update of the height that \* the relayer stores for srcChainID -LightClientUpdates(srcChainID, dstChainID, relayer) == +ClientDatagrams(srcChainID, dstChainID, relayer) == LET srcChain == GetChainByID(srcChainID) IN LET dstChain == GetChainByID(dstChainID) IN LET srcChainHeight == GetLatestHeight(srcChain) IN @@ -55,7 +57,6 @@ LightClientUpdates(srcChainID, dstChainID, relayer) == LET emptySetDatagrams == AsSetDatagrams({}) IN - \* check if the relayer chain height for srcChainID should be updated LET srcRelayerChainHeight == IF relayer[srcChainID] < srcChainHeight @@ -233,19 +234,45 @@ ChannelDatagrams(srcChainID, dstChainID) == dstDatagrams (*************************************************************************** - Compute datagrams (from srcChainID to dstChainID) + Packet datagrams + ***************************************************************************) +\* Compute a packet datagram designated for dstChainID, based on the packetLogEntry +PacketDatagram(srcChainID, dstChainID, packetLogEntry) == + + LET srcChannelID == GetChannelID(srcChainID) IN \* "chanAtoB" (if srcChainID = "chainA", dstChainID = "chainB") + LET dstChannelID == GetChannelID(dstChainID) IN \* "chanBtoA" (if srcChainID = "chainA", dstChainID = "chainB") + + LET srcHeight == GetLatestHeight(GetChainByID(srcChainID)) IN + + LET packetData(logEntry) == AsPacket([sequence |-> logEntry.sequence, + timeoutHeight |-> logEntry.timeoutHeight, + srcChannelID |-> srcChannelID, + dstChannelID |-> dstChannelID]) IN + + IF packetLogEntry.type = "PacketSent" + THEN AsDatagram([type |-> "PacketRecv", + packet |-> packetData(packetLogEntry), + proofHeight |-> srcHeight]) + ELSE IF packetLogEntry.type = "WriteAck" + THEN AsDatagram([type |-> "PacketAck", + packet |-> packetData(packetLogEntry), + acknowledgement |-> packetLogEntry.acknowledgement, + proofHeight |-> srcHeight]) + ELSE NullDatagram + +(*************************************************************************** + Compute client, connection, channel datagrams (from srcChainID to dstChainID) ***************************************************************************) \* Currently supporting: \* - ICS 002: Client updates \* - ICS 003: Connection handshake \* - ICS 004: Channel handshake -\* - ICS 004: Packet transmission ComputeDatagrams(srcChainID, dstChainID) == \* ICS 002 : Clients \* - Determine if light clients needs to be updated LET clientDatagrams == IF GenerateClientDatagrams - THEN LightClientUpdates(srcChainID, dstChainID, relayerHeights) + THEN ClientDatagrams(srcChainID, dstChainID, relayerHeights) ELSE [datagrams |-> AsSetDatagrams({}), relayerUpdate |-> relayerHeights] IN \* ICS3 : Connections @@ -261,8 +288,7 @@ ComputeDatagrams(srcChainID, dstChainID) == IF GenerateChannelDatagrams THEN ChannelDatagrams(srcChainID, dstChainID) ELSE AsSetDatagrams({}) IN - - + [datagrams |-> clientDatagrams.datagrams \union connectionDatagrams \union channelDatagrams, @@ -279,6 +305,7 @@ UpdateRelayerClients(chainID) == ![chainID] = GetLatestHeight(GetChainByID(chainID)) ] /\ UNCHANGED <> + /\ UNCHANGED <> \* for two chains, srcChainID and dstChainID, where srcChainID /= dstChainID, \* create the pending datagrams and update the corresponding sets of pending datagrams @@ -293,12 +320,38 @@ Relay(srcChainID, dstChainID) == ] /\ relayerHeights' = datagramsAndRelayerUpdate.relayerUpdate /\ UNCHANGED <> + /\ UNCHANGED <> + +\* given an entry from the packet log, create a packet datagram and +\* append it to the outgoing packet datagram queue for dstChainID +RelayPacketDatagram(packetLogEntry) == + LET srcChainID == packetLogEntry.srcChainID IN + LET dstChainID == GetCounterpartyChainID(srcChainID) IN + + LET packetDatagram == PacketDatagram(srcChainID, dstChainID, packetLogEntry) IN + + IF packetDatagram /= NullDatagram + THEN [outgoingPacketDatagrams EXCEPT + ![dstChainID] = Append(outgoingPacketDatagrams[dstChainID], + AsPacketDatagram(packetDatagram))] + ELSE outgoingPacketDatagrams +\* update the relayer client heights UpdateRelayer == \E chainID \in ChainIDs : UpdateRelayerClients(chainID) +\* create client, connection, channel datagrams CreateDatagrams == - \E srcChainID \in ChainIDs : \E dstChainID \in ChainIDs : Relay(srcChainID, dstChainID) + \E srcChainID \in ChainIDs : \E dstChainID \in ChainIDs : Relay(srcChainID, dstChainID) + +\* scan packet log and create packet datagrams +ScanPacketLog == + /\ packetLog /= AsPacketLog(<<>>) + /\ outgoingPacketDatagrams' = RelayPacketDatagram(AsPacketLogEntry(Head(packetLog))) + /\ packetLog' = Tail(packetLog) + /\ UNCHANGED <> + /\ UNCHANGED <> + (*************************************************************************** Specification @@ -309,15 +362,18 @@ CreateDatagrams == Init == /\ relayerHeights = [chainID \in ChainIDs |-> AsInt(nullHeight)] /\ outgoingDatagrams = [chainID \in ChainIDs |-> AsSetDatagrams({})] + /\ outgoingPacketDatagrams = [chainID \in ChainIDs |-> AsSeqPacketDatagrams(<<>>)] \* Next state action \* The relayer either: \* - updates its clients, or -\* - relays datagrams between two chains, or +\* - creates datagrams, +\* - scans the packet log and creates packet datagrams, or \* - does nothing Next == \/ UpdateRelayer \/ CreateDatagrams + \/ ScanPacketLog \/ UNCHANGED vars \* Fairness constraints @@ -337,5 +393,5 @@ TypeOK == ============================================================================= \* Modification History -\* Last modified Wed Sep 09 16:22:49 CEST 2020 by ilinastoilkovska +\* Last modified Fri Sep 18 17:26:08 CEST 2020 by ilinastoilkovska \* Created Fri Mar 06 09:23:12 CET 2020 by ilinastoilkovska diff --git a/docs/spec/relayer/RelayerDefinitions.tla b/docs/spec/relayer/tla/RelayerDefinitions.tla similarity index 89% rename from docs/spec/relayer/RelayerDefinitions.tla rename to docs/spec/relayer/tla/RelayerDefinitions.tla index 2226ac48a5..5f84cb55de 100644 --- a/docs/spec/relayer/RelayerDefinitions.tla +++ b/docs/spec/relayer/tla/RelayerDefinitions.tla @@ -5,7 +5,7 @@ different modules ***************************************************************************) -EXTENDS Integers, FiniteSets +EXTENDS Integers, FiniteSets, Sequences (********************* TYPE ANNOTATIONS FOR APALACHE ***********************) \* operator for type annotations @@ -53,6 +53,21 @@ PacketCommitmentType == sequence |-> Int, timeoutHeight |-> Int ] + +\* packet receipt type +PacketReceiptType == + [ + channelID |-> STRING, + sequence |-> Int + ] + +\* packet acknowledgement type +PacketAcknowledgementType == + [ + channelID |-> STRING, + sequence |-> Int, + acknowledgement |-> BOOLEAN + ] \* packet type PacketType == @@ -80,7 +95,10 @@ ChainStoreType == height |-> Int, counterpartyClientHeights |-> {Int}, connectionEnd |-> ConnectionEndType, - packetCommitment |-> {PacketCommitmentType} + packetCommitments |-> {PacketCommitmentType}, + packetsToAcknowledge |-> Seq(PacketType), + packetReceipts |-> {PacketReceiptType}, + packetAcknowledgements |-> {PacketAcknowledgementType} ] \* history variable type @@ -152,28 +170,52 @@ DatagramType == AsID(ID) == ID <: STRING AsInt(n) == n <: Int +AsSetInt(S) == S <: {Int} AsString(s) == s <: STRING + AsChannelEnd(channelEnd) == channelEnd <: ChannelEndType AsSetChannelEnd(CE) == CE <: {ChannelEndType} + AsConnectionEnd(connectionEnd) == connectionEnd <: ConnectionEndType + AsChainStore(chainStore) == chainStore <: ChainStoreType + AsHistory(history) == history <: HistoryType + AsDatagram(dgr) == dgr <: DatagramType + AsClientDatagram(dgr) == dgr <: ClientDatagramType AsSetClientDatagrams(Dgrs) == Dgrs <: {ClientDatagramType} + AsConnectionDatagram(dgr) == dgr <: ConnectionDatagramType AsSetConnectionDatagrams(Dgrs) == Dgrs <: {ConnectionDatagramType} + AsChannelDatagram(dgr) == dgr <: ChannelDatagramType AsSetChannelDatagrams(Dgrs) == Dgrs <: {ChannelDatagramType} + AsPacketDatagram(dgr) == dgr <: PacketDatagramType AsSetPacketDatagrams(Dgrs) == Dgrs <: {PacketDatagramType} +AsSeqPacketDatagrams(Dgrs) == Dgrs <: Seq(PacketDatagramType) + AsSetDatagrams(Dgrs) == Dgrs <: {DatagramType} -AsSetInt(S) == S <: {Int} +AsSeqDatagrams(Dgrs) == Dgrs <: Seq(DatagramType) + AsPacket(packet) == packet <: PacketType AsSetPacket(P) == P <: {PacketType} -AsSetPacketCommitment(P) == P <: {PacketCommitmentType} +AsSeqPacket(P) == P <: Seq(PacketType) + +AsPacketCommitment(pc) == pc <: PacketCommitmentType +AsSetPacketCommitment(PC) == PC <: {PacketCommitmentType} + +AsPacketReceipt(pr) == pr <: PacketReceiptType +AsSetPacketReceipt(PR) == PR <: {PacketReceiptType} + +AsPacketAcknowledgement(pa) == pa <: PacketAcknowledgementType +AsSetPacketAcknowledgement(PA) == PA <: {PacketAcknowledgementType} + AsPacketLogEntry(logEntry) == logEntry <: PacketLogEntryType -AsPacketLog(packetLog) == packetLog <: {PacketLogEntryType} +AsPacketLog(packetLog) == packetLog <: Seq(PacketLogEntryType) + (********************** Common operator definitions ***********************) ChainIDs == {"chainA", "chainB"} @@ -240,15 +282,28 @@ ChannelEnds(channelOrdering, maxPacketSeq) == ] <: {ChannelEndType} -(**************************** PacketCommitments **************************** - A set of packet commitments. +(******* PacketCommitments, PacketReceipts, PacketAcknowledgements ********* + Sets of packet commitments, packet receipts, packet acknowledgements. ***************************************************************************) - PacketCommitments(maxHeight, maxPacketSeq) == +PacketCommitments(maxHeight, maxPacketSeq) == [ channelID : ChannelIDs, sequence : 1..maxPacketSeq, timeoutHeight : 1..maxHeight ] <: {PacketCommitmentType} + +PacketReceipts(maxPacketSeq) == + [ + channelID : ChannelIDs, + sequence : 1..maxPacketSeq + ] <: {PacketReceiptType} + +PacketAcknowledgements(maxPacketSeq) == + [ + channelID : ChannelIDs, + sequence : 1..maxPacketSeq, + acknowledgement : BOOLEAN + ] <: {PacketAcknowledgementType} (***************************** ConnectionEnds ***************************** A set of connection end records. @@ -282,6 +337,17 @@ ConnectionEnds(channelOrdering, maxPacketSeq) == counterpartyClientID : ClientIDs \union {nullClientID}, channelEnd : ChannelEnds(channelOrdering, maxPacketSeq) ] <: {ConnectionEndType} + +(********************************* Packets ********************************* + A set of packets. + ***************************************************************************) +Packets(maxHeight, maxPacketSeq) == + [ + sequence : 1..maxPacketSeq, + timeoutHeight : 1..maxHeight, + srcChannelID : ChannelIDs, + dstChannelID : ChannelIDs + ] <: {PacketType} (******************************** ChainStores ****************************** A set of chain records. @@ -301,20 +367,12 @@ ChainStores(maxHeight, channelOrdering, maxPacketSeq) == height : 1..maxHeight, counterpartyClientHeights : SUBSET(1..maxHeight), connectionEnd : ConnectionEnds(channelOrdering, maxPacketSeq), - packetCommitment : SUBSET(PacketCommitments(maxHeight, maxPacketSeq)) + packetCommitments : SUBSET(PacketCommitments(maxHeight, maxPacketSeq)), + packetReceipts : SUBSET(PacketReceipts(maxPacketSeq)), + packetsToAcknowledge : Seq(Packets(maxHeight, maxPacketSeq)), + packetAcknowledgements : SUBSET(PacketAcknowledgements(maxPacketSeq)) ] <: {ChainStoreType} -(********************************* Packets ********************************* - A set of packets. - ***************************************************************************) -Packets(maxHeight, maxPacketSeq) == - [ - sequence : 1..maxPacketSeq, - timeoutHeight : 1..maxHeight, - srcChannelID : ChannelIDs, - dstChannelID : ChannelIDs - ] <: {PacketType} - (******************************** Datagrams ******************************** A set of datagrams. ***************************************************************************) @@ -352,6 +410,12 @@ Datagrams(maxHeight, maxPacketSeq) == \union [type : {"PacketAck"}, packet : Packets(maxHeight, maxPacketSeq), acknowledgement : BOOLEAN, proofHeight : 1..maxHeight] <: {DatagramType} + +NullDatagram == + [type |-> "null"] <: DatagramType + +NullPacketLogEntry == + [type |-> "null"] <: PacketLogEntryType Histories == [ @@ -420,7 +484,10 @@ InitChainStore(channelOrdering) == [height |-> 1, counterpartyClientHeights |-> AsSetInt({}), connectionEnd |-> InitConnectionEnd(channelOrdering), - packetCommitment |-> AsSetPacketCommitment({})] <: ChainStoreType + packetCommitments |-> AsSetPacketCommitment({}), + packetReceipts |-> AsSetPacketReceipt({}), + packetsToAcknowledge |-> AsSeqPacket(<<>>), + packetAcknowledgements |-> AsSetPacketAcknowledgement({})] <: ChainStoreType \* Initial value of history flags @@ -559,5 +626,5 @@ IsChannelClosed(chain) == ============================================================================= \* Modification History -\* Last modified Thu Sep 10 15:42:52 CEST 2020 by ilinastoilkovska +\* Last modified Wed Sep 30 13:32:32 CEST 2020 by ilinastoilkovska \* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska \ No newline at end of file