From f6f1b1a2314e76890767852e36c4d798aa46fce7 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Wed, 16 Dec 2020 13:20:26 +0100 Subject: [PATCH 1/8] packet delay spec first draft --- docs/spec/tla/packet-delay/Chain.tla | 142 ++++++++ docs/spec/tla/packet-delay/IBCPacketDelay.tla | 280 +++++++++++++++ .../IBCPacketDelayDefinitions.tla | 186 ++++++++++ .../tla/packet-delay/ICS04PacketHandlers.tla | 330 ++++++++++++++++++ 4 files changed, 938 insertions(+) create mode 100644 docs/spec/tla/packet-delay/Chain.tla create mode 100644 docs/spec/tla/packet-delay/IBCPacketDelay.tla create mode 100644 docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla create mode 100644 docs/spec/tla/packet-delay/ICS04PacketHandlers.tla diff --git a/docs/spec/tla/packet-delay/Chain.tla b/docs/spec/tla/packet-delay/Chain.tla new file mode 100644 index 0000000000..ee04a75bcf --- /dev/null +++ b/docs/spec/tla/packet-delay/Chain.tla @@ -0,0 +1,142 @@ +------------------------------- MODULE Chain ------------------------------- + +EXTENDS Integers, FiniteSets, Sequences, ICS04PacketHandlers, IBCPacketDelayDefinitions + +CONSTANTS MaxHeight, \* maximal chain height + ChannelOrdering, \* indicate whether the channels are ordered or unordered + MaxPacketSeq, \* maximal packet sequence number + MaxDelay, \* maximal packet delay + ChainID \* a chain ID + +VARIABLES chainStore, \* chain store, containing client heights, a connection end, a channel end + incomingPacketDatagrams, \* sequence of incoming packet datagrams + appPacketSeq, \* packet sequence number from the application on the chain + packetLog, \* packet log + packetDatagramTimestamp \* history variable that tracks when packet datagrams were processed + +vars == <> +Heights == 1..MaxHeight \* set of possible heights of the chains in the system + +(*************************************************************************** + Packet update operators + ***************************************************************************) +\* Update the chain store and packet log with packet datagrams +PacketUpdate(chainID, packetDatagram, log) == + + LET packet == packetDatagram.packet IN + \* get the new updated store, packet log + LET packetUpdate == + IF packetDatagram.type = "PacketRecv" + THEN HandlePacketRecv(chainID, chainStore, packetDatagram, log, packetDatagramTimestamp) + ELSE IF packetDatagram.type = "PacketAck" + THEN HandlePacketAck(chainID, chainStore, packetDatagram, log, packetDatagramTimestamp) + ELSE [chainStore |-> chainStore, + packetLog |-> log, + datagramTimestamp |-> packetDatagramTimestamp] + IN + + LET packetUpdateStore == packetUpdate.chainStore IN + + \* update height and timestamp + LET updatedStore == + IF packetUpdateStore.height + 1 \in Heights + THEN [packetUpdateStore EXCEPT + !.height = packetUpdateStore.height + 1, + !.timestamp = packetUpdateStore.timestamp + 1] + ELSE [packetUpdateStore EXCEPT + !.timestamp = packetUpdateStore.timestamp + 1] + IN + + [chainStore |-> updatedStore, + packetLog |-> packetUpdate.packetLog, + datagramTimestamp |-> packetUpdate.datagramTimestamp] + +(*************************************************************************** + 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, + !.timestamp = chainStore.timestamp + 1] + /\ UNCHANGED <> + +\* handle the incoming packet datagrams +HandlePacketDatagrams == + \* enabled if incomingPacketDatagrams is not empty + /\ incomingPacketDatagrams /= <<>> + /\ LET packetUpdate == PacketUpdate(ChainID, Head(incomingPacketDatagrams), packetLog) IN + /\ chainStore' = packetUpdate.chainStore + /\ packetLog' = packetUpdate.packetLog + /\ incomingPacketDatagrams' = Tail(incomingPacketDatagrams) + /\ UNCHANGED appPacketSeq + +\* Send a packet +SendPacket == + \* enabled if appPacketSeq is not bigger than MaxPacketSeq + /\ appPacketSeq <= MaxPacketSeq + \* Create packet + /\ LET packet == [ + sequence |-> appPacketSeq, + timeoutHeight |-> MaxHeight + 1, + srcPortID |-> chainStore.channelEnd.portID, + srcChannelID |-> chainStore.channelEnd.channelID, + dstPortID |-> chainStore.channelEnd.counterpartyPortID, + dstChannelID |-> chainStore.channelEnd.counterpartyChannelID] IN + \* update chain store with packet committment + /\ chainStore' = WritePacketCommitment(chainStore, packet) + \* log sent packet + /\ packetLog' = Append(packetLog, + [type |-> "PacketSent", + srcChainID |-> ChainID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight] + ) + \* increase application packet sequence + /\ appPacketSeq' = appPacketSeq + 1 + /\ UNCHANGED incomingPacketDatagrams + + + +\* Acknowledge a packet +AcknowledgePacket == + /\ chainStore.packetsToAcknowledge /= <<>> + \* write acknowledgements to chain store + /\ chainStore' = WriteAcknowledgement(chainStore, Head(chainStore.packetsToAcknowledge)) + \* log acknowledgement + /\ packetLog' = LogAcknowledgement(ChainID, chainStore, packetLog, Head(chainStore.packetsToAcknowledge)) + /\ UNCHANGED <> + +(*************************************************************************** + Specification + ***************************************************************************) +\* Initial state predicate +\* Initially +\* - the chain store is initialized to +\* InitChainStore(ChainID, ChannelOrdering, MaxDelay) +\* (defined in IBCPacketDelayDefinitions.tla) +\* - incomingPacketDatagrams is an empty sequence +\* - the appPacketSeq is set to 1 +Init == + /\ chainStore = InitChainStore(ChainID, ChannelOrdering, MaxDelay) + /\ incomingPacketDatagrams = <<>> + /\ appPacketSeq = 1 + +\* Next state action +\* The chain either +\* - advances its height +\* - receives datagrams and updates its state +\* - sends a packet +\* - acknowledges a packet +Next == + \/ AdvanceChain + \/ HandlePacketDatagrams + \/ SendPacket + \/ AcknowledgePacket + \/ UNCHANGED vars + +============================================================================= +\* Modification History +\* Last modified Wed Dec 16 13:16:38 CET 2020 by ilinastoilkovska +\* Created Thu Dec 10 13:52:13 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelay.tla b/docs/spec/tla/packet-delay/IBCPacketDelay.tla new file mode 100644 index 0000000000..63bdf97415 --- /dev/null +++ b/docs/spec/tla/packet-delay/IBCPacketDelay.tla @@ -0,0 +1,280 @@ +--------------------------- MODULE IBCPacketDelay --------------------------- + +EXTENDS Integers, FiniteSets, Sequences, IBCPacketDelayDefinitions + +CONSTANTS MaxHeight, \* maximal height of all the chains in the system + ChannelOrdering, \* indicate whether the channels are ordered or unordered + MaxPacketSeq, \* maximal packet sequence number + MaxDelay \* maximal packet delay + +VARIABLES chainAstore, \* store of ChainA + chainBstore, \* store of ChainB + packetDatagramsChainA, \* sequence of packet datagrams incoming to ChainA + packetDatagramsChainB, \* sequence of packet datagrams incoming to ChainB + outgoingPacketDatagrams, \* packet datagrams created by the relayer but not submitted + packetLog, \* packet log + appPacketSeqChainA, \* packet sequence number from the application on ChainA + appPacketSeqChainB, \* packet sequence number from the application on ChainB + packetDatagramTimestamp \* history variable that tracks when packet datagrams were processed + +chainAvars == <> +chainBvars == <> +vars == <> +(*************************************************************************** + Instances of Chain + ***************************************************************************) + +\* We suppose there are two chains that communicate, ChainA and ChainB +\* ChainA -- Instance of Chain.tla +ChainA == INSTANCE Chain + WITH ChainID <- "chainA", + chainStore <- chainAstore, + incomingPacketDatagrams <- packetDatagramsChainA, + appPacketSeq <- appPacketSeqChainA + +\* ChainB -- Instance of Chain.tla +ChainB == INSTANCE Chain + WITH ChainID <- "chainB", + chainStore <- chainBstore, + incomingPacketDatagrams <- packetDatagramsChainB, + appPacketSeq <- appPacketSeqChainB + + + (*************************************************************************** + Environment operators + ***************************************************************************) + +\* get chain store by ID +GetChainByID(chainID) == + IF chainID = "chainA" + THEN chainAstore + ELSE chainBstore + +\* update the client height of the client for the counterparty chain of chainID +UpdateClientHeights(chainID) == + /\ \/ /\ chainID = "chainA" + /\ chainBstore.height \notin DOMAIN chainAstore.counterpartyClientHeights + /\ chainAstore' = [chainAstore EXCEPT + !.counterpartyClientHeights = + [h \in DOMAIN chainAstore.counterpartyClientHeights \union {chainBstore.height} |-> + IF h = chainBstore.height + THEN chainAstore.timestamp + ELSE chainAstore.counterpartyClientHeights[h]], + !.timestamp = chainAstore.timestamp + 1 + ] + /\ UNCHANGED chainBstore + \/ /\ chainID = "chainB" + /\ chainAstore.height \notin DOMAIN chainBstore.counterpartyClientHeights + /\ chainBstore' = [chainBstore EXCEPT + !.counterpartyClientHeights = + [h \in DOMAIN chainBstore.counterpartyClientHeights \union {chainAstore.height} |-> + IF h = chainAstore.height + THEN chainBstore.timestamp + ELSE chainBstore.counterpartyClientHeights[h]], + !.timestamp = chainBstore.timestamp + 1 + ] + /\ UNCHANGED chainAstore + \/ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> + + +\* Compute a packet datagram designated for dstChainID, based on the packetLogEntry +PacketDatagram(srcChainID, dstChainID, packetLogEntry) == + + LET srcChannelID == GetChannelID(srcChainID) IN \* "chanAtoB" (if srcChainID = "chainA") + LET dstChannelID == GetChannelID(dstChainID) IN \* "chanBtoA" (if dstChainID = "chainB") + + LET srcPortID == GetPortID(srcChainID) IN \* "portA" (if srcChainID = "chainA") + LET dstPortID == GetPortID(dstChainID) IN \* "portB" (if dstChainID = "chainB") + + LET srcHeight == GetLatestHeight(GetChainByID(srcChainID)) IN + + \* the source chain of the packet that is received by dstChainID is srcChainID + LET recvPacket(logEntry) == [sequence |-> logEntry.sequence, + timeoutHeight |-> logEntry.timeoutHeight, + srcChannelID |-> srcChannelID, + srcPortID |-> srcPortID, + dstChannelID |-> dstChannelID, + dstPortID |-> dstPortID] IN + + \* the source chain of the packet that is acknowledged by srcChainID is dstChainID + LET ackPacket(logEntry) == [sequence |-> logEntry.sequence, + timeoutHeight |-> logEntry.timeoutHeight, + srcChannelID |-> dstChannelID, + srcPortID |-> dstPortID, + dstChannelID |-> srcChannelID, + dstPortID |-> srcPortID] IN + + IF packetLogEntry.type = "PacketSent" + THEN [type |-> "PacketRecv", + packet |-> recvPacket(packetLogEntry), + proofHeight |-> srcHeight] + ELSE IF packetLogEntry.type = "WriteAck" + THEN [type |-> "PacketAck", + packet |-> ackPacket(packetLogEntry), + acknowledgement |-> packetLogEntry.acknowledgement, + proofHeight |-> srcHeight] + ELSE NullDatagram + +\* submit a packet datagram if a delay has passed +\* or install the appropriate height if it is missing +SubmitDatagramOrInstallClientHeight(chainID) == + LET packetDatagram == Head(outgoingPacketDatagrams[chainID]) IN + LET chain == GetChainByID(chainID) IN + + LET clientHeightTimestamp == + IF packetDatagram.proofHeight \in DOMAIN chain.counterpartyClientHeights + THEN chain.counterpartyClientHeights[packetDatagram.proofHeight] + ELSE 0 IN + + \* packetDatagram.proof height is installed on chain + IF clientHeightTimestamp /= 0 + \* the delay has passed + THEN IF clientHeightTimestamp + MaxDelay < chain.timestamp + \* submit the datagram to the corresponding chain + THEN LET datagramsChainA == IF chainID = "chainA" + THEN Append(packetDatagramsChainA, packetDatagram) + ELSE packetDatagramsChainA IN + LET datagramsChainB == IF chainID = "chainB" + THEN Append(packetDatagramsChainB, packetDatagram) + ELSE packetDatagramsChainB IN + LET outgoingDatagrams == [outgoingPacketDatagrams EXCEPT + ![chainID] = Tail(outgoingPacketDatagrams[chainID])] IN + + [datagramsChainA |-> datagramsChainA, + datagramsChainB |-> datagramsChainB, + outgoingDatagrams |-> outgoingDatagrams, + chainA |-> chainAstore, + chainB |-> chainBstore] + \* otherwise do not submit and do not install any new heights + ELSE [datagramsChainA |-> packetDatagramsChainA, + datagramsChainB |-> packetDatagramsChainB, + outgoingDatagrams |-> outgoingPacketDatagrams, + chainA |-> chainAstore, + chainB |-> chainBstore] + \* packetDatagram.proof height is not installed on chain, + \* install it + ELSE LET chainA == IF chainID = "chainA" + THEN [chainAstore EXCEPT + !.counterpartyClientHeights = + [h \in DOMAIN chainAstore.counterpartyClientHeights \union {packetDatagram.proofHeight} |-> + IF h = packetDatagram.proofHeight + THEN chainAstore.timestamp + ELSE chainAstore.counterpartyClientHeights[h]], + !.timestamp = chainAstore.timestamp + 1 + ] + ELSE chainAstore IN + LET chainB == IF chainID = "chainB" + THEN [chainBstore EXCEPT + !.counterpartyClientHeights = + [h \in DOMAIN chainBstore.counterpartyClientHeights \union {packetDatagram.proofHeight} |-> + IF h = packetDatagram.proofHeight + THEN chainBstore.timestamp + ELSE chainBstore.counterpartyClientHeights[h]], + !.timestamp = chainBstore.timestamp + 1 + ] + ELSE chainBstore IN + + [datagramsChainA |-> packetDatagramsChainA, + datagramsChainB |-> packetDatagramsChainB, + outgoingDatagrams |-> outgoingPacketDatagrams, + chainA |-> chainA, + chainB |-> chainB] + +(*************************************************************************** + Environment actions + ***************************************************************************) + \* update the client height of some chain + UpdateClients == + \E chainID \in ChainIDs : UpdateClientHeights(chainID) + +\* create datagrams depending on packet log +CreateDatagrams == + /\ packetLog /= <<>> + /\ LET packetLogEntry == Head(packetLog) IN + LET srcChainID == packetLogEntry.srcChainID IN + LET dstChainID == GetCounterpartyChainID(srcChainID) IN + LET packetDatagram == PacketDatagram(srcChainID, dstChainID, packetLogEntry) IN + /\ \/ /\ packetDatagram = NullDatagram + /\ UNCHANGED outgoingPacketDatagrams + \/ /\ packetDatagram /= NullDatagram + /\ outgoingPacketDatagrams' = + [chainID \in ChainIDs |-> + IF chainID = dstChainID + THEN Append(outgoingPacketDatagrams[chainID], packetDatagram) + ELSE outgoingPacketDatagrams[chainID] + ] + /\ packetLog' = Tail(packetLog) + /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* submit datagrams if delay has passed +SubmitDatagramsWithDelay == + \E chainID \in ChainIDs : + /\ outgoingPacketDatagrams[chainID] /= <<>> + /\ LET submitted == SubmitDatagramOrInstallClientHeight(chainID) IN + /\ packetDatagramsChainA' = submitted.datagramsChainA + /\ packetDatagramsChainB' = submitted.datagramsChainB + /\ outgoingPacketDatagrams' = submitted.outgoingDatagrams + /\ chainAstore' = submitted.chainA + /\ chainBstore' = submitted.chainB + /\ UNCHANGED <> + +(*************************************************************************** + Component actions + ***************************************************************************) + +\* ChainAction: either chain takes a step, leaving the other +\* variables unchange +ChainAction == + \/ /\ ChainA!Next + /\ UNCHANGED chainBvars + /\ UNCHANGED outgoingPacketDatagrams + \/ /\ ChainB!Next + /\ UNCHANGED chainAvars + /\ UNCHANGED outgoingPacketDatagrams + +\* EnvironmentAction: either +\* - create packet datagrams if packet log is not empty, or +\* - update counterparty clients, or +\* - submit datagrams after their delay has passed +EnvironmentAction == + \/ CreateDatagrams + \/ UpdateClients + \/ SubmitDatagramsWithDelay + +(*************************************************************************** + Specification + ***************************************************************************) + +\* Initial state predicate +Init == + /\ ChainA!Init + /\ ChainB!Init + /\ outgoingPacketDatagrams = [chainID \in ChainIDs |-> <<>>] + /\ packetLog = <<>> + +\* Next state action +Next == + \/ ChainAction + \/ EnvironmentAction + \/ UNCHANGED vars + +Spec == Init /\ [][Next]_vars + + +Inv == + \A chainID \in ChainIDs : + \A h \in DOMAIN GetChainByID(chainID).counterpartyClientHeights : + packetDatagramTimestamp[<>] > GetChainByID(chainID).counterpartyClientHeights[h] + MaxDelay + +============================================================================= +\* Modification History +\* Last modified Tue Dec 15 17:10:33 CET 2020 by ilinastoilkovska +\* Created Thu Dec 10 13:44:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla new file mode 100644 index 0000000000..9006a5a844 --- /dev/null +++ b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla @@ -0,0 +1,186 @@ +--------------------- MODULE IBCPacketDelayDefinitions --------------------- + +EXTENDS Integers, FiniteSets, Sequences + +(********************** Common operator definitions ***********************) +ChainIDs == {"chainA", "chainB"} +ChannelIDs == {"chanAtoB", "chanBtoA"} +PortIDs == {"portA", "portB"} +ChannelStates == {"UNINIT", "INIT", "TRYOPEN", "OPEN", "CLOSED"} + +nullHeight == 0 +nullChannelID == "none" +nullPortID == "none" +nullEscrowAddress == "none" + +Max(S) == CHOOSE x \in S: \A y \in S: y <= x + +(******* PacketCommitments, PacketReceipts, PacketAcknowledgements ********* + Sets of packet commitments, packet receipts, packet acknowledgements. + ***************************************************************************) +PacketCommitments(maxHeight, maxPacketSeq) == + [ + channelID : ChannelIDs, + portID : PortIDs, + sequence : 1..maxPacketSeq, + timeoutHeight : 1..maxHeight + ] + +PacketReceipts(maxPacketSeq) == + [ + channelID : ChannelIDs, + portID : PortIDs, + sequence : 1..maxPacketSeq + ] + +PacketAcknowledgements(maxPacketSeq) == + [ + channelID : ChannelIDs, + portID : PortIDs, + sequence : 1..maxPacketSeq, + acknowledgement : BOOLEAN + ] + +(********************************* Packets ********************************* + A set of packets. + ***************************************************************************) +Packets(maxHeight, maxPacketSeq) == + [ + sequence : 1..maxPacketSeq, + timeoutHeight : 1..maxHeight, + srcPortID : PortIDs, + srcChannelID : ChannelIDs, + dstPortID : PortIDs, + dstChannelID : ChannelIDs + ] + + +(******************************** Datagrams ******************************** + A set of datagrams. + We consider client and packet datagrams + ***************************************************************************) +Datagrams(maxHeight, maxPacketSeq, maxBalance, Denomination) == + [type : {"PacketRecv"}, + packet : Packets(maxHeight, maxPacketSeq), + proofHeight : 1..maxHeight] + \union + [type : {"PacketAck"}, + packet : Packets(maxHeight, maxPacketSeq), + acknowledgement : BOOLEAN, + proofHeight : 1..maxHeight] + +NullDatagram == + [type |-> "null"] + +(*************************************************************************** + Chain helper operators + ***************************************************************************) + +\* get the ID of chainID's counterparty chain +GetCounterpartyChainID(chainID) == + IF chainID = "chainA" THEN "chainB" ELSE "chainA" + +\* get the maximal height of the client for chainID's counterparty chain +GetMaxCounterpartyClientHeight(chain) == + IF DOMAIN chain.counterpartyClientHeights /= {} + THEN Max(DOMAIN chain.counterpartyClientHeights) + ELSE nullHeight + +\* get the channel ID of the channel end at 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 + +\* get the port ID at chainID +GetPortID(chainID) == + IF chainID = "chainA" + THEN "portA" + ELSE IF chainID = "chainB" + THEN "portB" + ELSE nullPortID + +\* get the port ID at chainID's counterparty chain +GetCounterpartyPortID(chainID) == + IF chainID = "chainA" + THEN "portB" + ELSE IF chainID = "chainB" + THEN "portA" + ELSE nullPortID + +\* get the latest height of chain +GetLatestHeight(chain) == + chain.height + +(*************************************************************************** + Initial values of a channel end, connection end, chain store + ***************************************************************************) +\* Initial value of an unordered channel end: +\* - state is "OPEN" (we assume channel handshake has successfully finished) +\* - order is "UNORDERED" +\* - portID, channelID, counterpartyPortID, counterpartyChannelID depend on ChainID +InitUnorderedChannelEnd(ChainID) == + [ + state |-> "OPEN", + order |-> "UNORDERED", + portID |-> GetPortID(ChainID), + channelID |-> GetChannelID(ChainID), + counterpartyPortID |-> GetCounterpartyPortID(ChainID), + counterpartyChannelID |-> GetCounterpartyChannelID(ChainID) + ] + +\* Initial value of an ordered channel end: +\* - state is "OPEN" (we assume channel handshake has successfully finished) +\* - order is "ORDERED" +\* - nextSendSeq, nextRcvSeq, nextAckSeq are set to 0 +\* - portID, channelID, counterpartyPortID, counterpartyChannelID depend on ChainID +InitOrderedChannelEnd(ChainID) == + [ + state |-> "OPEN", + order |-> "ORDERED", + nextSendSeq |-> 0, + nextRcvSeq |-> 0, + nextAckSeq |-> 0, + portID |-> GetPortID(ChainID), + channelID |-> GetChannelID(ChainID), + counterpartyPortID |-> GetCounterpartyPortID(ChainID), + counterpartyChannelID |-> GetCounterpartyChannelID(ChainID) + ] + +InitChannelEnd(ChainID, ChannelOrdering) == + IF ChannelOrdering = "ORDERED" + THEN InitOrderedChannelEnd(ChainID) + ELSE InitUnorderedChannelEnd(ChainID) + +\* Initial value of the chain store: +\* - height is initialized to 1 +\* - timestamp is initialized to 0 +\* - the counterparty client is created at timestamp 1 +\* - the channel end is initialized to InitConnectionEnd +InitChainStore(ChainID, ChannelOrdering, MaxDelay) == + [ + height |-> 1, + timestamp |-> 1, + counterpartyClientHeights |-> [h \in {1} |-> 1], + channelEnd |-> InitChannelEnd(ChainID, ChannelOrdering), + + packetCommitments |-> {}, + packetReceipts |-> {}, + packetAcknowledgements |-> {}, + packetsToAcknowledge |-> <<>> + ] + +============================================================================= +\* Modification History +\* Last modified Tue Dec 15 15:53:32 CET 2020 by ilinastoilkovska +\* Created Thu Dec 10 14:06:33 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla new file mode 100644 index 0000000000..605b8f9afa --- /dev/null +++ b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla @@ -0,0 +1,330 @@ +------------------------ MODULE ICS04PacketHandlers ------------------------ + +EXTENDS Integers, FiniteSets, Sequences, IBCPacketDelayDefinitions + +(*************************************************************************** + Packet datagram handlers + ***************************************************************************) + +\* Handle "PacketRecv" datagrams +HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == + \* get chainID's channel end + LET channelEnd == chain.channelEnd IN + \* get packet + LET packet == packetDatagram.packet IN + + IF \* if the channel end is open for packet transmission + /\ channelEnd.state = "OPEN" + \* if the packet has not passed the timeout height + /\ \/ packet.timeoutHeight = 0 + \/ chain.height < packet.timeoutHeight + \* if the "PacketRecv" datagram has valid port and channel IDs + /\ packet.srcPortID = channelEnd.counterpartyPortID + /\ packet.srcChannelID = channelEnd.counterpartyChannelID + /\ packet.dstPortID = channelEnd.portID + /\ packet.dstChannelID = channelEnd.channelID + \* if "PacketRecv" datagram can be verified + /\ packetDatagram.proofHeight \in DOMAIN chain.counterpartyClientHeights + THEN \* construct log entry for packet log + LET logEntry == [type |-> "PacketRecv", + srcChainID |-> chainID, + sequence |-> packet.sequence, + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + timeoutHeight |-> packet.timeoutHeight + ] IN + + \* if the channel is unordered and the packet has not been received + IF /\ channelEnd.order = "UNORDERED" + /\ [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence + ] \notin chain.packetReceipts + THEN LET newChainStore == [chain EXCEPT + \* record that the packet has been received + !.packetReceipts = + chain.packetReceipts + \union + {[channelID |-> packet.dstChannelID, + portID |-> packet.dstPortID, + 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, datagramTimestamp |-> datagramTimestamp] + ELSE [chainStore |-> chain, packetLog |-> log, datagramTimestamp |-> datagramTimestamp] + + +\* Handle "PacketAck" datagrams +HandlePacketAck(chainID, chain, packetDatagram, log, datagramTimestamp) == + \* get chainID's channel end + LET channelEnd == chain.channelEnd IN + \* get packet + LET packet == packetDatagram.packet IN + \* get packet committment that should be in chain store + LET packetCommitment == [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight] IN + + IF \* if the channel end is open for packet transmission + /\ channelEnd.state = "OPEN" + \* if the packet committment exists in the chain store + /\ packetCommitment \in chain.packetCommitments + \* if the "PacketRecv" datagram has valid port and channel IDs + /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID + /\ packet.dstPortID = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID + \* if the "PacketAck" datagram can be verified + /\ packetDatagram.proofHeight \in DOMAIN 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 + !.channelEnd.nextAckSeq = + channelEnd.nextAckSeq + 1, + !.packetCommitments = chain.packetCommitments \ {packetCommitment}] + \* if the channel is unordered, remove packet commitment + ELSE IF channelEnd.order = "UNORDERED" + THEN [chain EXCEPT + !.packetCommitments = chain.packetCommitments \ {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 channel end + LET channelEnd == chain.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"} + \* if the packet has valid port and channel IDs + /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID + /\ packet.dstPortID = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID + \* 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 {[portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight]}, + !.channelEnd = + [channelEnd EXCEPT !.nextSendSeq = channelEnd.nextSendSeq + 1], + !.timestamp = + chain.timestamp + 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 {[portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight]}, + !.timestamp = + chain.timestamp + 1 + ] + \* otherwise, do not update the chain store + ELSE chain + +\* write acknowledgements to chain store +WriteAcknowledgement(chain, packet) == + \* create a packet acknowledgement for this packet + LET packetAcknowledgement == + [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence, + acknowledgement |-> TRUE] IN + + \* if the acknowledgement for the packet has not been written + IF packetAcknowledgement \notin chain.packetAcknowledgements + THEN \* write the acknowledgement to the chain store and remove + \* the packet from the set of packets to acknowledge + [chain EXCEPT !.packetAcknowledgements = + chain.packetAcknowledgements + \union + {packetAcknowledgement}, + !.packetsToAcknowledge = + Tail(chain.packetsToAcknowledge), + !.timestamp = + chain.timestamp + 1] + + \* remove the packet from the sequence of packets to acknowledge + ELSE [chain EXCEPT !.packetsToAcknowledge = + Tail(chain.packetsToAcknowledge), + !.timestamp = + chain.timestamp + 1] + +\* 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 == + [type |-> "WriteAck", + srcChainID |-> chainID, + sequence |-> packet.sequence, + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + timeoutHeight |-> packet.timeoutHeight, + acknowledgement |-> TRUE] IN + Append(log, packetLogEntry) + \* do not add anything to the log + ELSE log + + +\* check if a packet timed out +TimeoutPacket(chain, counterpartyChain, packet, proofHeight) == + \* get connection end + LET connectionEnd == chain.connectionEnd IN + \* get channel end + LET channelEnd == connectionEnd.channelEnd IN + \* get counterparty channel end + LET counterpartyChannelEnd == counterpartyChain.channelEnd IN + + \* get packet committment that should be in chain store + LET packetCommitment == [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight] IN + \* get packet receipt that should be absent in counterparty chain store + LET packetReceipt == [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence] IN + + \* if channel end is open + IF /\ channelEnd.state = "OPEN" + \* srcChannelID and srcPortID match channel and port IDs + /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID + \* dstChannelID and dstPortID match counterparty channel and port IDs + /\ packet.dstPortID = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID + \* packet has timed out + /\ packet.timeoutHeight > 0 + /\ proofHeight >= packet.timeoutHeight + \* chain has sent the packet + /\ packetCommitment \in chain.packetCommitments + \* counterparty chain has not received the packet + /\ \/ /\ channelEnd.order = "ORDERED" + /\ counterpartyChannelEnd.nextRcvSeq <= packet.sequence + \/ /\ channelEnd.order = "UNORDERED" + /\ packetReceipt \notin counterpartyChain.packetReceipts + \* counterparty channel end has dstPortID and dstChannelID + /\ counterpartyChannelEnd.portID = packet.dstPortID + /\ counterpartyChannelEnd.channelID = packet.dstChannelID + \* close ordered channel and remove packet commitment + THEN LET updatedChannelEnd == [channelEnd EXCEPT + !.state = IF channelEnd.order = "ORDERED" + THEN "CLOSED" + ELSE channelEnd.state] IN + LET updatedConnectionEnd == [connectionEnd EXCEPT + !.channelEnd = updatedChannelEnd] IN + LET updatedChainStore == [chain EXCEPT + !.packetCommitments = + chain.packetCommitments \ {packetCommitment}, + !.connectionEnd = updatedConnectionEnd] IN + + updatedChainStore + + \* otherwise, do not update the chain store + ELSE chain + +\* check if a packet timed out on close +TimeoutOnClose(chain, counterpartyChain, packet, proofHeight) == + \* get connection end + LET connectionEnd == chain.connectionEnd IN + \* get channel end + LET channelEnd == connectionEnd.channelEnd IN + \* get counterparty channel end + LET counterpartyChannelEnd == counterpartyChain.connectionEnd.channelEnd IN + + \* get packet committment that should be in chain store + LET packetCommitment == [portID |-> packet.srcPortID, + channelID |-> packet.srcChannelID, + sequence |-> packet.sequence, + timeoutHeight |-> packet.timeoutHeight] IN + \* get packet receipt that should be absent in counterparty chain store + LET packetReceipt == [portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence] IN + + + \* if srcChannelID and srcPortID match channel and port IDs + IF /\ packet.srcPortID = channelEnd.portID + /\ packet.srcChannelID = channelEnd.channelID + \* if dstChannelID and dstPortID match counterparty channel and port IDs + /\ packet.dstPort = channelEnd.counterpartyPortID + /\ packet.dstChannelID = channelEnd.counterpartyChannelID + \* chain has sent the packet + /\ packetCommitment \in chain.packetCommitments + \* counterparty channel end is closed and its fields are as expected + /\ counterpartyChannelEnd.state = "CLOSED" + /\ counterpartyChannelEnd.portID = packet.dstPortID + /\ counterpartyChannelEnd.channelID = packet.dstChannelID + /\ counterpartyChannelEnd.counterpartyPortID = packet.srcPortID + /\ counterpartyChannelEnd.counterpartyChannelID = packet.srcChannelID + \* counterparty chain has not received the packet + /\ \/ /\ channelEnd.order = "ORDERED" + /\ counterpartyChannelEnd.nextRcvSeq <= packet.sequence + \/ /\ channelEnd.order = "UNORDERED" + /\ packetReceipt \notin counterpartyChain.packetReceipts + \* close ordered channel and remove packet commitment + THEN LET updatedChannelEnd == [channelEnd EXCEPT + !.state = IF channelEnd.order = "ORDERED" + THEN "CLOSED" + ELSE channelEnd.state] IN + LET updatedConnectionEnd == [connectionEnd EXCEPT + !.channelEnd = updatedChannelEnd] IN + LET updatedChainStore == [chain EXCEPT + !.packetCommitments = + chain.packetCommitments \ {packetCommitment}, + !.connectionEnd = updatedConnectionEnd] IN + + updatedChainStore + + \* otherwise, do not update the chain store + ELSE chain + +============================================================================= +\* Modification History +\* Last modified Wed Dec 16 13:17:08 CET 2020 by ilinastoilkovska +\* Created Thu Dec 10 15:12:41 CET 2020 by ilinastoilkovska From ba725b41a30d18be14f3fbcb57d3185f079bc243 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Fri, 22 Jan 2021 10:50:02 +0100 Subject: [PATCH 2/8] packet delay spec --- .../IBCTokenTransferDefinitions.tla | 4 +- .../spec/tla/ibc-core/ICS04PacketHandlers.tla | 4 +- docs/spec/tla/packet-delay/Chain.tla | 11 +++--- docs/spec/tla/packet-delay/IBCPacketDelay.tla | 21 ++++++++-- .../IBCPacketDelayDefinitions.tla | 4 +- .../tla/packet-delay/ICS04PacketHandlers.tla | 39 +++++++++++++++---- 6 files changed, 61 insertions(+), 22 deletions(-) diff --git a/docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla b/docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla index 80276bc019..d7e0eb50ca 100644 --- a/docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla +++ b/docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla @@ -284,7 +284,7 @@ Packets(maxHeight, maxPacketSeq, maxBalance, Denominations) == ChainStores(maxHeight, maxPacketSeq, maxBalance, Denomination) == [ height : 1..maxHeight, - clientHeight : 1..maxHeight, + counterpartyClientHeights : SUBSET (1..maxHeight), channelEnd : ChannelEnds, packetCommitments : SUBSET(PacketCommitments(maxHeight, maxPacketSeq, maxBalance, @@ -370,7 +370,7 @@ GetLatestHeight(chain) == AsInt(chain.height) (*************************************************************************** - Initial values of a channel end, chain store, accounts for ICS02 + Initial values of a channel end, chain store, accounts for ICS20 ***************************************************************************) \* Initial value of a channel end: \* - state is "OPEN" (we assume channel handshake has successfully finished) diff --git a/docs/spec/tla/ibc-core/ICS04PacketHandlers.tla b/docs/spec/tla/ibc-core/ICS04PacketHandlers.tla index 49040c1131..ede19f57bd 100644 --- a/docs/spec/tla/ibc-core/ICS04PacketHandlers.tla +++ b/docs/spec/tla/ibc-core/ICS04PacketHandlers.tla @@ -99,8 +99,8 @@ HandlePacketAck(chainID, chain, packetDatagram, log) == IF \* if the channel and connection ends are open for packet transmission /\ channelEnd.state = "OPEN" /\ connectionEnd.state = "OPEN" - \* if the packet committment exists in the chain store - /\ packetCommitment \in chain.packetCommittments + \* if the packet commitment exists in the chain store + /\ packetCommitment \in chain.packetCommitments \* if the "PacketRecv" datagram has valid port and channel IDs /\ packet.srcPortID = channelEnd.portID /\ packet.srcChannelID = channelEnd.channelID diff --git a/docs/spec/tla/packet-delay/Chain.tla b/docs/spec/tla/packet-delay/Chain.tla index ee04a75bcf..3e7bde632d 100644 --- a/docs/spec/tla/packet-delay/Chain.tla +++ b/docs/spec/tla/packet-delay/Chain.tla @@ -14,7 +14,7 @@ VARIABLES chainStore, \* chain store, containing client heights, a connection en packetLog, \* packet log packetDatagramTimestamp \* history variable that tracks when packet datagrams were processed -vars == <> +vars == <> Heights == 1..MaxHeight \* set of possible heights of the chains in the system (*************************************************************************** @@ -60,7 +60,7 @@ AdvanceChain == /\ chainStore' = [chainStore EXCEPT !.height = chainStore.height + 1, !.timestamp = chainStore.timestamp + 1] - /\ UNCHANGED <> + /\ UNCHANGED <> \* handle the incoming packet datagrams HandlePacketDatagrams == @@ -70,6 +70,7 @@ HandlePacketDatagrams == /\ chainStore' = packetUpdate.chainStore /\ packetLog' = packetUpdate.packetLog /\ incomingPacketDatagrams' = Tail(incomingPacketDatagrams) + /\ packetDatagramTimestamp' = packetUpdate.datagramTimestamp /\ UNCHANGED appPacketSeq \* Send a packet @@ -95,7 +96,7 @@ SendPacket == ) \* increase application packet sequence /\ appPacketSeq' = appPacketSeq + 1 - /\ UNCHANGED incomingPacketDatagrams + /\ UNCHANGED <> @@ -106,7 +107,7 @@ AcknowledgePacket == /\ chainStore' = WriteAcknowledgement(chainStore, Head(chainStore.packetsToAcknowledge)) \* log acknowledgement /\ packetLog' = LogAcknowledgement(ChainID, chainStore, packetLog, Head(chainStore.packetsToAcknowledge)) - /\ UNCHANGED <> + /\ UNCHANGED <> (*************************************************************************** Specification @@ -138,5 +139,5 @@ Next == ============================================================================= \* Modification History -\* Last modified Wed Dec 16 13:16:38 CET 2020 by ilinastoilkovska +\* Last modified Wed Dec 16 13:36:59 CET 2020 by ilinastoilkovska \* Created Thu Dec 10 13:52:13 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelay.tla b/docs/spec/tla/packet-delay/IBCPacketDelay.tla index 63bdf97415..195a2d740d 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelay.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelay.tla @@ -259,6 +259,7 @@ Init == /\ ChainB!Init /\ outgoingPacketDatagrams = [chainID \in ChainIDs |-> <<>>] /\ packetLog = <<>> + /\ packetDatagramTimestamp = [x \in {} |-> 0] \* Next state action Next == @@ -268,13 +269,25 @@ Next == Spec == Init /\ [][Next]_vars +(*************************************************************************** + Invariants + ***************************************************************************) -Inv == +\* each packet datagam is processed at time t (stored in packetDatagramTimestamp), +\* such that t > ht + delay, where +\* ht is the time when the client height is installed +PacketDatagramsDelay == \A chainID \in ChainIDs : - \A h \in DOMAIN GetChainByID(chainID).counterpartyClientHeights : - packetDatagramTimestamp[<>] > GetChainByID(chainID).counterpartyClientHeights[h] + MaxDelay + \A h \in DOMAIN GetChainByID(chainID).counterpartyClientHeights : + <> \in DOMAIN packetDatagramTimestamp + => + packetDatagramTimestamp[<>] > GetChainByID(chainID).counterpartyClientHeights[h] + MaxDelay + +\* a conjnction of all invariants +Inv == + /\ PacketDatagramsDelay ============================================================================= \* Modification History -\* Last modified Tue Dec 15 17:10:33 CET 2020 by ilinastoilkovska +\* Last modified Wed Dec 16 17:41:19 CET 2020 by ilinastoilkovska \* Created Thu Dec 10 13:44:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla index 9006a5a844..c9923bfee8 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla @@ -171,7 +171,7 @@ InitChainStore(ChainID, ChannelOrdering, MaxDelay) == [ height |-> 1, timestamp |-> 1, - counterpartyClientHeights |-> [h \in {1} |-> 1], + counterpartyClientHeights |-> [h \in {} |-> 0], channelEnd |-> InitChannelEnd(ChainID, ChannelOrdering), packetCommitments |-> {}, @@ -182,5 +182,5 @@ InitChainStore(ChainID, ChannelOrdering, MaxDelay) == ============================================================================= \* Modification History -\* Last modified Tue Dec 15 15:53:32 CET 2020 by ilinastoilkovska +\* Last modified Wed Dec 16 17:40:36 CET 2020 by ilinastoilkovska \* Created Thu Dec 10 14:06:33 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla index 605b8f9afa..4be3f5e16d 100644 --- a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla +++ b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla @@ -50,8 +50,16 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == sequence |-> packet.sequence]}, \* add packet to the set of packets for which an acknowledgement should be written !.packetsToAcknowledge = Append(chain.packetsToAcknowledge, packet)] IN + \* record the timestamp in the history variable + LET newDatagramTimestamp == + [tID \in (DOMAIN datagramTimestamp \union {<>}) |-> + IF tID = <> + THEN chain.timestamp + ELSE datagramTimestamp[tID]] IN - [chainStore |-> newChainStore, packetLog |-> Append(log, logEntry)] + [chainStore |-> newChainStore, + packetLog |-> Append(log, logEntry), + datagramTimestamp |-> newDatagramTimestamp] ELSE \* if the channel is ordered and the packet sequence is nextRcvSeq IF /\ channelEnd.order = "ORDERED" @@ -62,8 +70,16 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == 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)] + \* record the timestamp in the history variable + LET newDatagramTimestamp == + [tID \in (DOMAIN datagramTimestamp \union {<>}) |-> + IF tID = <> + THEN chain.timestamp + ELSE datagramTimestamp[tID]] IN + + [chainStore |-> newChainStore, + packetLog |-> Append(log, logEntry), + datagramTimestamp |-> newDatagramTimestamp] \* otherwise, do not update the chain store and the log @@ -109,11 +125,20 @@ HandlePacketAck(chainID, chain, packetDatagram, log, datagramTimestamp) == !.packetCommitments = chain.packetCommitments \ {packetCommitment}] \* otherwise, do not update the chain store ELSE chain IN + + \* record the timestamp in the history variable + LET newDatagramTimestamp == + [tID \in (DOMAIN datagramTimestamp \union {<>}) |-> + IF tID = <> + THEN chain.timestamp + ELSE datagramTimestamp[tID]] IN + + [chainStore |-> newChainStore, + packetLog |-> log, + datagramTimestamp |-> newDatagramTimestamp] - [chainStore |-> newChainStore, packetLog |-> log] - \* otherwise, do not update the chain store and the log - ELSE [chainStore |-> chain, packetLog |-> log] + ELSE [chainStore |-> chain, packetLog |-> log, datagramTimestamp |-> datagramTimestamp] \* write packet committments to chain store @@ -326,5 +351,5 @@ TimeoutOnClose(chain, counterpartyChain, packet, proofHeight) == ============================================================================= \* Modification History -\* Last modified Wed Dec 16 13:17:08 CET 2020 by ilinastoilkovska +\* Last modified Wed Dec 16 13:28:05 CET 2020 by ilinastoilkovska \* Created Thu Dec 10 15:12:41 CET 2020 by ilinastoilkovska From a4596201ecd20c088ddbebf9dcbfc1e00e992e19 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Fri, 22 Jan 2021 10:52:10 +0100 Subject: [PATCH 3/8] small fix in packet handlers --- docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla b/docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla index 0b69901358..2aa0e6c600 100644 --- a/docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla +++ b/docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla @@ -97,6 +97,7 @@ HandlePacketAck(chain, packetDatagram, log, accounts, escrowAccounts, maxBalance LET packetCommitment == AsPacketCommitment( [portID |-> packet.srcPortID, channelID |-> packet.srcChannelID, + data |-> packet.data, sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight]) IN @@ -321,5 +322,5 @@ TimeoutOnClose(chain, counterpartyChain, accounts, escrowAccounts, ============================================================================= \* Modification History -\* Last modified Tue Dec 01 16:59:04 CET 2020 by ilinastoilkovska +\* Last modified Fri Jan 15 15:26:01 CET 2021 by ilinastoilkovska \* Created Thu Oct 19 18:29:58 CET 2020 by ilinastoilkovska From b8ddea1997933d0df1ca6dbaaaab37c192960791 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Thu, 15 Apr 2021 16:32:46 +0200 Subject: [PATCH 4/8] added type annotations in packet delay spec --- docs/spec/tla/packet-delay/Chain.tla | 25 ++-- docs/spec/tla/packet-delay/IBCPacketDelay.tla | 102 ++++++++++----- .../IBCPacketDelayDefinitions.tla | 111 ++++++++++++++-- .../tla/packet-delay/ICS04PacketHandlers.tla | 122 +++++++++++------- docs/spec/tla/packet-delay/README.md | 14 ++ 5 files changed, 268 insertions(+), 106 deletions(-) create mode 100644 docs/spec/tla/packet-delay/README.md diff --git a/docs/spec/tla/packet-delay/Chain.tla b/docs/spec/tla/packet-delay/Chain.tla index 3e7bde632d..9624f35158 100644 --- a/docs/spec/tla/packet-delay/Chain.tla +++ b/docs/spec/tla/packet-delay/Chain.tla @@ -2,17 +2,19 @@ EXTENDS Integers, FiniteSets, Sequences, ICS04PacketHandlers, IBCPacketDelayDefinitions -CONSTANTS MaxHeight, \* maximal chain height - ChannelOrdering, \* indicate whether the channels are ordered or unordered - MaxPacketSeq, \* maximal packet sequence number - MaxDelay, \* maximal packet delay - ChainID \* a chain ID +CONSTANTS + MaxHeight, \* maximal chain height + ChannelOrdering, \* indicate whether the channels are ordered or unordered + MaxPacketSeq, \* maximal packet sequence number + MaxDelay, \* maximal packet delay + ChainID \* a chain ID -VARIABLES chainStore, \* chain store, containing client heights, a connection end, a channel end - incomingPacketDatagrams, \* sequence of incoming packet datagrams - appPacketSeq, \* packet sequence number from the application on the chain - packetLog, \* packet log - packetDatagramTimestamp \* history variable that tracks when packet datagrams were processed +VARIABLES + chainStore, \* chain store, containing client heights and a channel end + incomingPacketDatagrams, \* sequence of incoming packet datagrams + appPacketSeq, \* packet sequence number from the application on the chain + packetLog, \* packet log + packetDatagramTimestamp \* history variable that tracks when packet datagrams were processed vars == <> Heights == 1..MaxHeight \* set of possible heights of the chains in the system @@ -21,6 +23,9 @@ Heights == 1..MaxHeight \* set of possible heights of the chains in the system Packet update operators ***************************************************************************) \* Update the chain store and packet log with packet datagrams +(* @type: (Str, DATAGRAM, Seq(LOGENTRY)) => + [chainStore: CHAINSTORE, packetLog: Seq(LOGENTRY), datagramTimestamp: <> -> Int]; +*) PacketUpdate(chainID, packetDatagram, log) == LET packet == packetDatagram.packet IN diff --git a/docs/spec/tla/packet-delay/IBCPacketDelay.tla b/docs/spec/tla/packet-delay/IBCPacketDelay.tla index 195a2d740d..9d7848a036 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelay.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelay.tla @@ -1,21 +1,42 @@ --------------------------- MODULE IBCPacketDelay --------------------------- +(*************************************************************************** + A TLA+ specification of the IBC packet transmission with packet delays. + Packet delays ensure that packet-related data should be accepted only + after some delay has passed since the corresponding header is installed. +***************************************************************************) + EXTENDS Integers, FiniteSets, Sequences, IBCPacketDelayDefinitions -CONSTANTS MaxHeight, \* maximal height of all the chains in the system - ChannelOrdering, \* indicate whether the channels are ordered or unordered - MaxPacketSeq, \* maximal packet sequence number - MaxDelay \* maximal packet delay +CONSTANTS + \* @type: Int; + MaxHeight, \* maximal height of all the chains in the system + \* @type: Str; + ChannelOrdering, \* indicate whether the channels are ordered or unordered + \* @type: Int; + MaxPacketSeq, \* maximal packet sequence number + \* @type: Int; + MaxDelay \* maximal packet delay -VARIABLES chainAstore, \* store of ChainA - chainBstore, \* store of ChainB - packetDatagramsChainA, \* sequence of packet datagrams incoming to ChainA - packetDatagramsChainB, \* sequence of packet datagrams incoming to ChainB - outgoingPacketDatagrams, \* packet datagrams created by the relayer but not submitted - packetLog, \* packet log - appPacketSeqChainA, \* packet sequence number from the application on ChainA - appPacketSeqChainB, \* packet sequence number from the application on ChainB - packetDatagramTimestamp \* history variable that tracks when packet datagrams were processed +VARIABLES + \* @type: CHAINSTORE; + chainAstore, \* store of ChainA + \* @type: CHAINSTORE; + chainBstore, \* store of ChainB + \* @type: Seq(DATAGRAM); + packetDatagramsChainA, \* sequence of packet datagrams incoming to ChainA + \* @type: Seq(DATAGRAM); + packetDatagramsChainB, \* sequence of packet datagrams incoming to ChainB + \* @type: Str -> Seq(DATAGRAM); + outgoingPacketDatagrams, \* packet datagrams created by the relayer but not submitted + \* @type: Seq(LOGENTRY); + packetLog, \* packet log + \* @type: Int; + appPacketSeqChainA, \* packet sequence number from the application on ChainA + \* @type: Int; + appPacketSeqChainB, \* packet sequence number from the application on ChainB + \* @type: <> -> Int; + packetDatagramTimestamp \* history variable that tracks when packet datagrams were processed chainAvars == <> chainBvars == <> @@ -24,6 +45,7 @@ vars == <> + (*************************************************************************** Instances of Chain ***************************************************************************) @@ -84,6 +106,7 @@ UpdateClientHeights(chainID) == \* Compute a packet datagram designated for dstChainID, based on the packetLogEntry +\* @type: (Str, Str, LOGENTRY) => DATAGRAM; PacketDatagram(srcChainID, dstChainID, packetLogEntry) == LET srcChannelID == GetChannelID(srcChainID) IN \* "chanAtoB" (if srcChainID = "chainA") @@ -95,30 +118,38 @@ PacketDatagram(srcChainID, dstChainID, packetLogEntry) == LET srcHeight == GetLatestHeight(GetChainByID(srcChainID)) IN \* the source chain of the packet that is received by dstChainID is srcChainID - LET recvPacket(logEntry) == [sequence |-> logEntry.sequence, - timeoutHeight |-> logEntry.timeoutHeight, - srcChannelID |-> srcChannelID, - srcPortID |-> srcPortID, - dstChannelID |-> dstChannelID, - dstPortID |-> dstPortID] IN + LET recvPacket == [ + sequence |-> packetLogEntry.sequence, + timeoutHeight |-> packetLogEntry.timeoutHeight, + srcChannelID |-> srcChannelID, + srcPortID |-> srcPortID, + dstChannelID |-> dstChannelID, + dstPortID |-> dstPortID + ] IN \* the source chain of the packet that is acknowledged by srcChainID is dstChainID - LET ackPacket(logEntry) == [sequence |-> logEntry.sequence, - timeoutHeight |-> logEntry.timeoutHeight, - srcChannelID |-> dstChannelID, - srcPortID |-> dstPortID, - dstChannelID |-> srcChannelID, - dstPortID |-> srcPortID] IN + LET ackPacket == [ + sequence |-> packetLogEntry.sequence, + timeoutHeight |-> packetLogEntry.timeoutHeight, + srcChannelID |-> dstChannelID, + srcPortID |-> dstPortID, + dstChannelID |-> srcChannelID, + dstPortID |-> srcPortID + ] IN IF packetLogEntry.type = "PacketSent" - THEN [type |-> "PacketRecv", - packet |-> recvPacket(packetLogEntry), - proofHeight |-> srcHeight] + THEN [ + type |-> "PacketRecv", + packet |-> recvPacket, + proofHeight |-> srcHeight + ] ELSE IF packetLogEntry.type = "WriteAck" - THEN [type |-> "PacketAck", - packet |-> ackPacket(packetLogEntry), - acknowledgement |-> packetLogEntry.acknowledgement, - proofHeight |-> srcHeight] + THEN [ + type |-> "PacketAck", + packet |-> ackPacket, + acknowledgement |-> packetLogEntry.acknowledgement, + proofHeight |-> srcHeight + ] ELSE NullDatagram \* submit a packet datagram if a delay has passed @@ -127,6 +158,10 @@ SubmitDatagramOrInstallClientHeight(chainID) == LET packetDatagram == Head(outgoingPacketDatagrams[chainID]) IN LET chain == GetChainByID(chainID) IN + \* if the proof height of the packet datagram is installed on the chain, + \* then clientHeightTimestamp is the timestamp, denoting the time when this + \* height was installed on the chain; + \* otherwise it is 0, denoting that this height is not installed on the chain LET clientHeightTimestamp == IF packetDatagram.proofHeight \in DOMAIN chain.counterpartyClientHeights THEN chain.counterpartyClientHeights[packetDatagram.proofHeight] @@ -151,7 +186,8 @@ SubmitDatagramOrInstallClientHeight(chainID) == outgoingDatagrams |-> outgoingDatagrams, chainA |-> chainAstore, chainB |-> chainBstore] - \* otherwise do not submit and do not install any new heights + \* the client height is installed, but the delay has not passed + \* do not submit and do not install any new heights ELSE [datagramsChainA |-> packetDatagramsChainA, datagramsChainB |-> packetDatagramsChainB, outgoingDatagrams |-> outgoingPacketDatagrams, diff --git a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla index c9923bfee8..3e35ded606 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla @@ -2,6 +2,83 @@ EXTENDS Integers, FiniteSets, Sequences +(************************ TYPE ALIASES FOR SNOWCAT *************************) +(* @typeAlias: CHAN = + [ + state: Str, + order: Str, + portID: Str, + channelID: Str, + counterpartyPortID: Str, + counterpartyChannelID: Str, + nextSendSeq: Int, + nextRcvSeq: Int, + nextAckSeq: Int + ]; +*) +(* @typeAlias: PACKET = + [ + sequence: Int, + timeoutHeight: Int, + srcPortID: Str, + srcChannelID: Str, + dstPortID: Str, + dstChannelID: Str + ]; +*) +(* @typeAlias: PACKETCOMM = + [ + portID: Str, + channelID: Str, + sequence: Int, + timeoutHeight: Int + ]; +*) +(* @typeAlias: PACKETREC = + [ + portID: Str, + channelID: Str, + sequence: Int + ]; +*) +(* @typeAlias: PACKETACK = + [ + portID: Str, + channelID: Str, + sequence: Int, + acknowledgement: Bool + ]; +*) +(* @typeAlias: CHAINSTORE = + [ + height: Int, + timestamp: Int, + counterpartyClientHeights: Int -> Int, + channelEnd: CHAN, + packetCommitments: Set(PACKETCOMM), + packetsToAcknowledge: Seq(PACKET), + packetReceipts: Set(PACKETREC), + packetAcknowledgements: Set(PACKETACK) + ]; +*) +(* @typeAlias: DATAGRAM = + [ + type: Str, + packet: PACKET, + proofHeight: Int, + acknowledgement: Bool + ]; +*) +(* @typeAlias: LOGENTRY = + [ + type: Str, + srcChainID: Str, + sequence: Int, + timeoutHeight: Int, + acknowledgement: Bool + ]; +*) + (********************** Common operator definitions ***********************) ChainIDs == {"chainA", "chainB"} ChannelIDs == {"chanAtoB", "chanBtoA"} @@ -15,9 +92,8 @@ nullEscrowAddress == "none" Max(S) == CHOOSE x \in S: \A y \in S: y <= x -(******* PacketCommitments, PacketReceipts, PacketAcknowledgements ********* - Sets of packet commitments, packet receipts, packet acknowledgements. - ***************************************************************************) +(******* PacketCommitments, PacketReceipts, PacketAcknowledgements *********) +\* Set of packet commitments PacketCommitments(maxHeight, maxPacketSeq) == [ channelID : ChannelIDs, @@ -25,7 +101,8 @@ PacketCommitments(maxHeight, maxPacketSeq) == sequence : 1..maxPacketSeq, timeoutHeight : 1..maxHeight ] - + +\* Set of packet receipts PacketReceipts(maxPacketSeq) == [ channelID : ChannelIDs, @@ -33,6 +110,7 @@ PacketReceipts(maxPacketSeq) == sequence : 1..maxPacketSeq ] +\* Set of packet acknowledgements PacketAcknowledgements(maxPacketSeq) == [ channelID : ChannelIDs, @@ -41,9 +119,8 @@ PacketAcknowledgements(maxPacketSeq) == acknowledgement : BOOLEAN ] -(********************************* Packets ********************************* - A set of packets. - ***************************************************************************) +(********************************* Packets *********************************) +\* Set of packets Packets(maxHeight, maxPacketSeq) == [ sequence : 1..maxPacketSeq, @@ -55,10 +132,8 @@ Packets(maxHeight, maxPacketSeq) == ] -(******************************** Datagrams ******************************** - A set of datagrams. - We consider client and packet datagrams - ***************************************************************************) +(******************************** Datagrams ********************************) +\* Set of datagrams (we consider only packet datagrams) Datagrams(maxHeight, maxPacketSeq, maxBalance, Denomination) == [type : {"PacketRecv"}, packet : Packets(maxHeight, maxPacketSeq), @@ -69,6 +144,7 @@ Datagrams(maxHeight, maxPacketSeq, maxBalance, Denomination) == acknowledgement : BOOLEAN, proofHeight : 1..maxHeight] +\* Null datagram NullDatagram == [type |-> "null"] @@ -81,6 +157,7 @@ GetCounterpartyChainID(chainID) == IF chainID = "chainA" THEN "chainB" ELSE "chainA" \* get the maximal height of the client for chainID's counterparty chain +\* @type: (CHAINSTORE) => Int; GetMaxCounterpartyClientHeight(chain) == IF DOMAIN chain.counterpartyClientHeights /= {} THEN Max(DOMAIN chain.counterpartyClientHeights) @@ -119,6 +196,7 @@ GetCounterpartyPortID(chainID) == ELSE nullPortID \* get the latest height of chain +\* @type: (CHAINSTORE) => Int; GetLatestHeight(chain) == chain.height @@ -157,6 +235,7 @@ InitOrderedChannelEnd(ChainID) == counterpartyChannelID |-> GetCounterpartyChannelID(ChainID) ] +\* Initial value of a channel end, based on the channel ordering InitChannelEnd(ChainID, ChannelOrdering) == IF ChannelOrdering = "ORDERED" THEN InitOrderedChannelEnd(ChainID) @@ -164,9 +243,11 @@ InitChannelEnd(ChainID, ChannelOrdering) == \* Initial value of the chain store: \* - height is initialized to 1 -\* - timestamp is initialized to 0 -\* - the counterparty client is created at timestamp 1 -\* - the channel end is initialized to InitConnectionEnd +\* - timestamp is initialized to 1 +\* - there are no installed client heights +\* - the channel end is initialized to InitChannelEnd +\* - the packet committments, receipts, acknowledgements, and packets +\* to acknowledge are empty InitChainStore(ChainID, ChannelOrdering, MaxDelay) == [ height |-> 1, @@ -179,6 +260,8 @@ InitChainStore(ChainID, ChannelOrdering, MaxDelay) == packetAcknowledgements |-> {}, packetsToAcknowledge |-> <<>> ] + +\* add ChainStore, ChannelEnds, write type invariant ============================================================================= \* Modification History diff --git a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla index 4be3f5e16d..4e4c379d80 100644 --- a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla +++ b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla @@ -7,6 +7,9 @@ EXTENDS Integers, FiniteSets, Sequences, IBCPacketDelayDefinitions ***************************************************************************) \* Handle "PacketRecv" datagrams +(* @type: (Str, CHAINSTORE, DATAGRAM, Seq(LOGENTRY), <> -> Int) => + [chainStore: CHAINSTORE, packetLog: Seq(LOGENTRY), datagramTimestamp: <> -> Int]; +*) HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == \* get chainID's channel end LET channelEnd == chain.channelEnd IN @@ -26,48 +29,56 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == \* if "PacketRecv" datagram can be verified /\ packetDatagram.proofHeight \in DOMAIN chain.counterpartyClientHeights THEN \* construct log entry for packet log - LET logEntry == [type |-> "PacketRecv", - srcChainID |-> chainID, - sequence |-> packet.sequence, - portID |-> packet.dstPortID, - channelID |-> packet.dstChannelID, - timeoutHeight |-> packet.timeoutHeight - ] IN + LET logEntry == [ + type |-> "PacketRecv", + srcChainID |-> chainID, + sequence |-> packet.sequence, + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + timeoutHeight |-> packet.timeoutHeight + ] IN \* if the channel is unordered and the packet has not been received IF /\ channelEnd.order = "UNORDERED" - /\ [portID |-> packet.dstPortID, - channelID |-> packet.dstChannelID, - sequence |-> packet.sequence + /\ [ + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence ] \notin chain.packetReceipts THEN LET newChainStore == [chain EXCEPT \* record that the packet has been received !.packetReceipts = chain.packetReceipts \union - {[channelID |-> packet.dstChannelID, - portID |-> packet.dstPortID, - sequence |-> packet.sequence]}, + {[ + channelID |-> packet.dstChannelID, + portID |-> packet.dstPortID, + sequence |-> packet.sequence + ]}, \* add packet to the set of packets for which an acknowledgement should be written !.packetsToAcknowledge = Append(chain.packetsToAcknowledge, packet)] IN \* record the timestamp in the history variable LET newDatagramTimestamp == - [tID \in (DOMAIN datagramTimestamp \union {<>}) |-> - IF tID = <> - THEN chain.timestamp - ELSE datagramTimestamp[tID]] IN + [ + tID \in (DOMAIN datagramTimestamp \union {<>}) |-> + IF tID = <> + THEN chain.timestamp + ELSE datagramTimestamp[tID] + ] IN - [chainStore |-> newChainStore, - packetLog |-> Append(log, logEntry), - datagramTimestamp |-> newDatagramTimestamp] + [ + chainStore |-> newChainStore, + packetLog |-> Append(log, logEntry), + datagramTimestamp |-> newDatagramTimestamp + ] 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, + !.channelEnd.nextRcvSeq = + channelEnd.nextRcvSeq + 1, \* add packet to the set of packets for which an acknowledgement should be written !.packetsToAcknowledge = Append(chain.packetsToAcknowledge, packet)] IN \* record the timestamp in the history variable @@ -77,9 +88,11 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == THEN chain.timestamp ELSE datagramTimestamp[tID]] IN - [chainStore |-> newChainStore, - packetLog |-> Append(log, logEntry), - datagramTimestamp |-> newDatagramTimestamp] + [ + chainStore |-> newChainStore, + packetLog |-> Append(log, logEntry), + datagramTimestamp |-> newDatagramTimestamp + ] \* otherwise, do not update the chain store and the log @@ -88,6 +101,9 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == \* Handle "PacketAck" datagrams +(* @type: (Str, CHAINSTORE, DATAGRAM, Seq(LOGENTRY), <> -> Int) => + [chainStore: CHAINSTORE, packetLog: Seq(LOGENTRY), datagramTimestamp: <> -> Int]; +*) HandlePacketAck(chainID, chain, packetDatagram, log, datagramTimestamp) == \* get chainID's channel end LET channelEnd == chain.channelEnd IN @@ -133,15 +149,18 @@ HandlePacketAck(chainID, chain, packetDatagram, log, datagramTimestamp) == THEN chain.timestamp ELSE datagramTimestamp[tID]] IN - [chainStore |-> newChainStore, - packetLog |-> log, - datagramTimestamp |-> newDatagramTimestamp] + [ + chainStore |-> newChainStore, + packetLog |-> log, + datagramTimestamp |-> newDatagramTimestamp + ] \* otherwise, do not update the chain store and the log ELSE [chainStore |-> chain, packetLog |-> log, datagramTimestamp |-> datagramTimestamp] \* write packet committments to chain store +\* @type: (CHAINSTORE, PACKET) => CHAINSTORE; WritePacketCommitment(chain, packet) == \* get channel end LET channelEnd == chain.channelEnd IN @@ -191,13 +210,15 @@ WritePacketCommitment(chain, packet) == ELSE chain \* write acknowledgements to chain store +\* @type: (CHAINSTORE, PACKET) => CHAINSTORE; WriteAcknowledgement(chain, packet) == \* create a packet acknowledgement for this packet - LET packetAcknowledgement == - [portID |-> packet.dstPortID, - channelID |-> packet.dstChannelID, - sequence |-> packet.sequence, - acknowledgement |-> TRUE] IN + LET packetAcknowledgement == [ + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence, + acknowledgement |-> TRUE + ] IN \* if the acknowledgement for the packet has not been written IF packetAcknowledgement \notin chain.packetAcknowledgements @@ -219,9 +240,18 @@ WriteAcknowledgement(chain, packet) == chain.timestamp + 1] \* log acknowledgements to packet Log +\* @type: (Str, CHAINSTORE, Seq(LOGENTRY), PACKET) => Seq(LOGENTRY); LogAcknowledgement(chainID, chain, log, packet) == + \* create a packet acknowledgement for this packet + LET packetAcknowledgement == [ + portID |-> packet.dstPortID, + channelID |-> packet.dstChannelID, + sequence |-> packet.sequence, + acknowledgement |-> TRUE + ] IN + \* if the acknowledgement for the packet has not been written - IF packet \notin chain.packetAcknowledgements + IF packetAcknowledgement \notin chain.packetAcknowledgements THEN \* append a "WriteAck" log entry to the log LET packetLogEntry == [type |-> "WriteAck", @@ -237,11 +267,10 @@ LogAcknowledgement(chainID, chain, log, packet) == \* check if a packet timed out +\* @type: (CHAINSTORE, CHAINSTORE, PACKET, Int) => CHAINSTORE; TimeoutPacket(chain, counterpartyChain, packet, proofHeight) == - \* get connection end - LET connectionEnd == chain.connectionEnd IN \* get channel end - LET channelEnd == connectionEnd.channelEnd IN + LET channelEnd == chain.channelEnd IN \* get counterparty channel end LET counterpartyChannelEnd == counterpartyChain.channelEnd IN @@ -281,12 +310,10 @@ TimeoutPacket(chain, counterpartyChain, packet, proofHeight) == !.state = IF channelEnd.order = "ORDERED" THEN "CLOSED" ELSE channelEnd.state] IN - LET updatedConnectionEnd == [connectionEnd EXCEPT - !.channelEnd = updatedChannelEnd] IN LET updatedChainStore == [chain EXCEPT + !.channelEnd = updatedChannelEnd, !.packetCommitments = - chain.packetCommitments \ {packetCommitment}, - !.connectionEnd = updatedConnectionEnd] IN + chain.packetCommitments \ {packetCommitment}] IN updatedChainStore @@ -294,13 +321,12 @@ TimeoutPacket(chain, counterpartyChain, packet, proofHeight) == ELSE chain \* check if a packet timed out on close +\* @type: (CHAINSTORE, CHAINSTORE, PACKET, Int) => CHAINSTORE; TimeoutOnClose(chain, counterpartyChain, packet, proofHeight) == - \* get connection end - LET connectionEnd == chain.connectionEnd IN \* get channel end - LET channelEnd == connectionEnd.channelEnd IN + LET channelEnd == chain.channelEnd IN \* get counterparty channel end - LET counterpartyChannelEnd == counterpartyChain.connectionEnd.channelEnd IN + LET counterpartyChannelEnd == counterpartyChain.channelEnd IN \* get packet committment that should be in chain store LET packetCommitment == [portID |-> packet.srcPortID, @@ -337,12 +363,10 @@ TimeoutOnClose(chain, counterpartyChain, packet, proofHeight) == !.state = IF channelEnd.order = "ORDERED" THEN "CLOSED" ELSE channelEnd.state] IN - LET updatedConnectionEnd == [connectionEnd EXCEPT - !.channelEnd = updatedChannelEnd] IN LET updatedChainStore == [chain EXCEPT + !.channelEnd = updatedChannelEnd, !.packetCommitments = - chain.packetCommitments \ {packetCommitment}, - !.connectionEnd = updatedConnectionEnd] IN + chain.packetCommitments \ {packetCommitment}] IN updatedChainStore diff --git a/docs/spec/tla/packet-delay/README.md b/docs/spec/tla/packet-delay/README.md new file mode 100644 index 0000000000..fbc8c25c53 --- /dev/null +++ b/docs/spec/tla/packet-delay/README.md @@ -0,0 +1,14 @@ +# TLA+ Specification of IBC Packet Transmission with Packet Delay (deprecated) + +This document describes the TLA+ specification of an IBC packet transmission with +packet delays. +IBC packet transmission with packet delays ensures that +packet-related data should be accepted only after some delay has passed since the corresponding header is installed. +This allows a correct relayer to intervene if the header is from a fork and shutdown the IBC handler, preventing damage at the application level. + +This TLA+ specification was used during the [design process](https://github.com/cosmos/cosmos-sdk/pull/7884) of the IBC connection-specified delay, where packet delay was a time duration. +Later, this design was augmented by adding a second delay parameter, in +terms of number of blocks; called [hybrid packet delay](https://github.com/cosmos/ibc/issues/539). + +## The Model of the Protocol + From 12d3026752176f99ae6b5a1ca4bd0e716e368852 Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Thu, 15 Apr 2021 18:55:01 +0200 Subject: [PATCH 5/8] type invariant --- docs/spec/tla/packet-delay/Chain.tla | 18 +- docs/spec/tla/packet-delay/IBCPacketDelay.tla | 36 ++-- .../IBCPacketDelayDefinitions.tla | 171 ++++++++++++++++-- .../tla/packet-delay/ICS04PacketHandlers.tla | 2 +- 4 files changed, 185 insertions(+), 42 deletions(-) diff --git a/docs/spec/tla/packet-delay/Chain.tla b/docs/spec/tla/packet-delay/Chain.tla index 9624f35158..c2734c466f 100644 --- a/docs/spec/tla/packet-delay/Chain.tla +++ b/docs/spec/tla/packet-delay/Chain.tla @@ -85,7 +85,7 @@ SendPacket == \* Create packet /\ LET packet == [ sequence |-> appPacketSeq, - timeoutHeight |-> MaxHeight + 1, + timeoutHeight |-> MaxHeight, srcPortID |-> chainStore.channelEnd.portID, srcChannelID |-> chainStore.channelEnd.channelID, dstPortID |-> chainStore.channelEnd.counterpartyPortID, @@ -125,7 +125,7 @@ AcknowledgePacket == \* - incomingPacketDatagrams is an empty sequence \* - the appPacketSeq is set to 1 Init == - /\ chainStore = InitChainStore(ChainID, ChannelOrdering, MaxDelay) + /\ chainStore = InitChainStore(ChainID, Heights, ChannelOrdering, MaxDelay) /\ incomingPacketDatagrams = <<>> /\ appPacketSeq = 1 @@ -140,9 +140,19 @@ Next == \/ HandlePacketDatagrams \/ SendPacket \/ AcknowledgePacket - \/ UNCHANGED vars + \/ UNCHANGED vars + +(*************************************************************************** + Invariants + ***************************************************************************) + +\* type invariant +TypeOK == + /\ chainStore \in ChainStores(Heights, ChannelOrdering, MaxPacketSeq) + /\ incomingPacketDatagrams \in Seq(Datagrams(Heights, MaxPacketSeq)) + /\ appPacketSeq \in Int ============================================================================= \* Modification History -\* Last modified Wed Dec 16 13:36:59 CET 2020 by ilinastoilkovska +\* Last modified Thu Apr 15 18:50:29 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 13:52:13 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelay.tla b/docs/spec/tla/packet-delay/IBCPacketDelay.tla index 9d7848a036..ecb9abd887 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelay.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelay.tla @@ -162,10 +162,7 @@ SubmitDatagramOrInstallClientHeight(chainID) == \* then clientHeightTimestamp is the timestamp, denoting the time when this \* height was installed on the chain; \* otherwise it is 0, denoting that this height is not installed on the chain - LET clientHeightTimestamp == - IF packetDatagram.proofHeight \in DOMAIN chain.counterpartyClientHeights - THEN chain.counterpartyClientHeights[packetDatagram.proofHeight] - ELSE 0 IN + LET clientHeightTimestamp == chain.counterpartyClientHeights[packetDatagram.proofHeight] IN \* packetDatagram.proof height is installed on chain IF clientHeightTimestamp /= 0 @@ -193,25 +190,20 @@ SubmitDatagramOrInstallClientHeight(chainID) == outgoingDatagrams |-> outgoingPacketDatagrams, chainA |-> chainAstore, chainB |-> chainBstore] - \* packetDatagram.proof height is not installed on chain, - \* install it + \* packetDatagram.proof height is not installed on chain, install it ELSE LET chainA == IF chainID = "chainA" THEN [chainAstore EXCEPT !.counterpartyClientHeights = - [h \in DOMAIN chainAstore.counterpartyClientHeights \union {packetDatagram.proofHeight} |-> - IF h = packetDatagram.proofHeight - THEN chainAstore.timestamp - ELSE chainAstore.counterpartyClientHeights[h]], + [chainAstore.counterpartyClientHeights EXCEPT + ![packetDatagram.proofHeight] = chainAstore.timestamp], !.timestamp = chainAstore.timestamp + 1 ] ELSE chainAstore IN LET chainB == IF chainID = "chainB" THEN [chainBstore EXCEPT !.counterpartyClientHeights = - [h \in DOMAIN chainBstore.counterpartyClientHeights \union {packetDatagram.proofHeight} |-> - IF h = packetDatagram.proofHeight - THEN chainBstore.timestamp - ELSE chainBstore.counterpartyClientHeights[h]], + [chainAstore.counterpartyClientHeights EXCEPT + ![packetDatagram.proofHeight] = chainBstore.timestamp], !.timestamp = chainBstore.timestamp + 1 ] ELSE chainBstore IN @@ -309,15 +301,21 @@ Spec == Init /\ [][Next]_vars Invariants ***************************************************************************) +\* type invariant +TypeOK == + /\ ChainA!TypeOK + /\ ChainB!TypeOK + \* each packet datagam is processed at time t (stored in packetDatagramTimestamp), -\* such that t > ht + delay, where +\* such that t >= ht + delay, where \* ht is the time when the client height is installed PacketDatagramsDelay == \A chainID \in ChainIDs : - \A h \in DOMAIN GetChainByID(chainID).counterpartyClientHeights : - <> \in DOMAIN packetDatagramTimestamp + \A h \in 1..MaxHeight : + /\ GetChainByID(chainID).counterpartyClientHeights[h] /= 0 + /\ <> \in DOMAIN packetDatagramTimestamp => - packetDatagramTimestamp[<>] > GetChainByID(chainID).counterpartyClientHeights[h] + MaxDelay + packetDatagramTimestamp[<>] >= GetChainByID(chainID).counterpartyClientHeights[h] + MaxDelay \* a conjnction of all invariants Inv == @@ -325,5 +323,5 @@ Inv == ============================================================================= \* Modification History -\* Last modified Wed Dec 16 17:41:19 CET 2020 by ilinastoilkovska +\* Last modified Thu Apr 15 18:53:41 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 13:44:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla index 3e35ded606..357a6d1bd3 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla @@ -83,7 +83,7 @@ EXTENDS Integers, FiniteSets, Sequences ChainIDs == {"chainA", "chainB"} ChannelIDs == {"chanAtoB", "chanBtoA"} PortIDs == {"portA", "portB"} -ChannelStates == {"UNINIT", "INIT", "TRYOPEN", "OPEN", "CLOSED"} +ChannelStates == {"OPEN", "CLOSED"} nullHeight == 0 nullChannelID == "none" @@ -92,14 +92,74 @@ nullEscrowAddress == "none" Max(S) == CHOOSE x \in S: \A y \in S: y <= x +(******************************* 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. We assume that channel + handshake has successfully finished, that is, the state is either + "OPEN" or "CLOSED" + + - order -- a string + Stores whether the channel end is ordered or unordered. It has one + of the following values: "UNORDERED", "ORDERED". + + * ordered channels have three additional packet sequence fields: + nextSendSeq -- stores the sequence number of the next packet that + is going to be sent, + nextRcvSeq -- stores the sequence number of the next packet that + is going to be received, + nextAckSeq -- stores the sequence number of the next packet that + is going to be acknowledged. + + - portID -- a port identifier + Stores the port identifier of this channel end. + + - channelID -- a channel identifier + Stores the channel identifier of this channel end. + + - counterpartyPortID -- a port identifier + Stores the port identifier of the counterparty channel end. + + - counterpartyChannelID -- a channel identifier + Stores the channel identifier of the counterparty channel end. + + Note: we omit channel versions and connection hops. + ***************************************************************************) +ChannelEnds(channelOrdering, maxPacketSeq) == + IF channelOrdering = "UNORDERED" + THEN \* set of unordered channels + [ + state : ChannelStates, + order : {"UNORDERED"}, + portID : PortIDs \union {nullPortID}, + channelID : ChannelIDs \union {nullChannelID}, + counterpartyPortID : PortIDs \union {nullPortID}, + counterpartyChannelID : ChannelIDs \union {nullChannelID} + ] + ELSE \* set of ordered channels + [ + state : ChannelStates, + order : {"ORDERED"}, + nextSendSeq : 0..maxPacketSeq, + nextRcvSeq : 0..maxPacketSeq, + nextAckSeq : 0..maxPacketSeq, + portID : PortIDs \union {nullPortID}, + channelID : ChannelIDs \union {nullChannelID}, + counterpartyPortID : PortIDs \union {nullPortID}, + counterpartyChannelID : ChannelIDs \union {nullChannelID} + ] + + (******* PacketCommitments, PacketReceipts, PacketAcknowledgements *********) \* Set of packet commitments -PacketCommitments(maxHeight, maxPacketSeq) == +PacketCommitments(Heights, maxPacketSeq) == [ channelID : ChannelIDs, portID : PortIDs, sequence : 1..maxPacketSeq, - timeoutHeight : 1..maxHeight + timeoutHeight : Heights ] \* Set of packet receipts @@ -121,32 +181,106 @@ PacketAcknowledgements(maxPacketSeq) == (********************************* Packets *********************************) \* Set of packets -Packets(maxHeight, maxPacketSeq) == +Packets(Heights, maxPacketSeq) == [ sequence : 1..maxPacketSeq, - timeoutHeight : 1..maxHeight, + timeoutHeight : Heights, srcPortID : PortIDs, srcChannelID : ChannelIDs, dstPortID : PortIDs, dstChannelID : ChannelIDs ] - + +(******************************** ChainStores ****************************** + A set of chain store records. + 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. + + - connectionEnd : a connection end record + Stores data about the connection with the counterparty chain. + + - packetCommitments : a set of packet commitments + A packet commitment is added to this set when a chain sends a packet + to the counterparty. + + - packetReceipts : a set of packet receipts + A packet receipt is added to this set when a chain received a packet + from the counterparty chain. + + - packetsToAcknowledge : a sequence of packets + A packet is added to this sequence when a chain receives it and is used + later for the receiver chain to write an acknowledgement for the packet. + + - packetAcknowledgements : a set of packet acknowledgements + A packet acknowledgement is added to this set when a chain writes an + acknowledgement for a packet it received from the counterparty. + + A chain store is the combination of the provable and private stores. + ***************************************************************************) +ChainStores(Heights, channelOrdering, maxPacketSeq) == + [ + height : Heights, + timestamp : Int, + counterpartyClientHeights : [Heights -> Int], + channelEnd : ChannelEnds(channelOrdering, maxPacketSeq), + packetCommitments : SUBSET(PacketCommitments(Heights, maxPacketSeq)), + packetReceipts : SUBSET(PacketReceipts(maxPacketSeq)), + packetsToAcknowledge : Seq(Packets(Heights, maxPacketSeq)), + packetAcknowledgements : SUBSET(PacketAcknowledgements(maxPacketSeq)) + ] (******************************** Datagrams ********************************) \* Set of datagrams (we consider only packet datagrams) -Datagrams(maxHeight, maxPacketSeq, maxBalance, Denomination) == - [type : {"PacketRecv"}, - packet : Packets(maxHeight, maxPacketSeq), - proofHeight : 1..maxHeight] - \union - [type : {"PacketAck"}, - packet : Packets(maxHeight, maxPacketSeq), - acknowledgement : BOOLEAN, - proofHeight : 1..maxHeight] +Datagrams(Heights, maxPacketSeq) == + [ + type : {"PacketRecv"}, + packet : Packets(Heights, maxPacketSeq), + proofHeight : Heights + ] \union [ + type : {"PacketAck"}, + packet : Packets(Heights, maxPacketSeq), + acknowledgement : BOOLEAN, + proofHeight : Heights + ] \* Null datagram NullDatagram == [type |-> "null"] + +(**************************** PacketLogEntries *****************************) +\* Set of packet log entries +PacketLogEntries(Heights, maxPacketSeq) == + [ + type : {"PacketSent"}, + srcChainID : ChainIDs, + sequence : 1..maxPacketSeq, + timeoutHeight : Heights + ] \union [ + type : {"PacketRecv"}, + srcChainID : ChainIDs, + sequence : 1..maxPacketSeq, + portID : PortIDs, + channelID : ChannelIDs, + timeoutHeight : Heights + ] \union [ + type : {"WriteAck"}, + srcChainID : ChainIDs, + sequence : 1..maxPacketSeq, + portID : PortIDs, + channelID : ChannelIDs, + timeoutHeight : Heights, + acknowledgement : BOOLEAN + ] + +\* Null packet log entry +NullPacketLogEntry == + [type |-> "null"] + (*************************************************************************** Chain helper operators @@ -248,11 +382,11 @@ InitChannelEnd(ChainID, ChannelOrdering) == \* - the channel end is initialized to InitChannelEnd \* - the packet committments, receipts, acknowledgements, and packets \* to acknowledge are empty -InitChainStore(ChainID, ChannelOrdering, MaxDelay) == +InitChainStore(ChainID, Heights, ChannelOrdering, MaxDelay) == [ height |-> 1, timestamp |-> 1, - counterpartyClientHeights |-> [h \in {} |-> 0], + counterpartyClientHeights |-> [h \in Heights |-> 0], channelEnd |-> InitChannelEnd(ChainID, ChannelOrdering), packetCommitments |-> {}, @@ -265,5 +399,6 @@ InitChainStore(ChainID, ChannelOrdering, MaxDelay) == ============================================================================= \* Modification History -\* Last modified Wed Dec 16 17:40:36 CET 2020 by ilinastoilkovska +\* Last modified Thu Apr 15 18:50:37 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 14:06:33 CET 2020 by ilinastoilkovska + \ No newline at end of file diff --git a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla index 4e4c379d80..bc25e1c16a 100644 --- a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla +++ b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla @@ -375,5 +375,5 @@ TimeoutOnClose(chain, counterpartyChain, packet, proofHeight) == ============================================================================= \* Modification History -\* Last modified Wed Dec 16 13:28:05 CET 2020 by ilinastoilkovska +\* Last modified Thu Apr 15 18:54:38 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 15:12:41 CET 2020 by ilinastoilkovska From 5a0de357726e75dc9479d6da5387d334cdb3cddd Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Fri, 16 Apr 2021 12:39:27 +0200 Subject: [PATCH 6/8] readme and fixes in packet handlers --- docs/spec/tla/packet-delay/Chain.tla | 7 +- docs/spec/tla/packet-delay/IBCPacketDelay.tla | 32 +++--- .../IBCPacketDelayDefinitions.tla | 4 +- .../tla/packet-delay/ICS04PacketHandlers.tla | 54 +++++---- .../tla/packet-delay/MC_IBCPacketDelay.tla | 30 +++++ docs/spec/tla/packet-delay/README.md | 107 ++++++++++++++++++ 6 files changed, 188 insertions(+), 46 deletions(-) create mode 100644 docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla diff --git a/docs/spec/tla/packet-delay/Chain.tla b/docs/spec/tla/packet-delay/Chain.tla index c2734c466f..98d8ef2356 100644 --- a/docs/spec/tla/packet-delay/Chain.tla +++ b/docs/spec/tla/packet-delay/Chain.tla @@ -32,9 +32,9 @@ PacketUpdate(chainID, packetDatagram, log) == \* get the new updated store, packet log LET packetUpdate == IF packetDatagram.type = "PacketRecv" - THEN HandlePacketRecv(chainID, chainStore, packetDatagram, log, packetDatagramTimestamp) + THEN HandlePacketRecv(chainID, chainStore, packetDatagram, MaxDelay, log, packetDatagramTimestamp) ELSE IF packetDatagram.type = "PacketAck" - THEN HandlePacketAck(chainID, chainStore, packetDatagram, log, packetDatagramTimestamp) + THEN HandlePacketAck(chainID, chainStore, packetDatagram, MaxDelay, log, packetDatagramTimestamp) ELSE [chainStore |-> chainStore, packetLog |-> log, datagramTimestamp |-> packetDatagramTimestamp] @@ -151,8 +151,9 @@ TypeOK == /\ chainStore \in ChainStores(Heights, ChannelOrdering, MaxPacketSeq) /\ incomingPacketDatagrams \in Seq(Datagrams(Heights, MaxPacketSeq)) /\ appPacketSeq \in Int + /\ packetLog \in Seq(PacketLogEntries(Heights, MaxPacketSeq)) ============================================================================= \* Modification History -\* Last modified Thu Apr 15 18:50:29 CEST 2021 by ilinastoilkovska +\* Last modified Fri Apr 16 11:49:19 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 13:52:13 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelay.tla b/docs/spec/tla/packet-delay/IBCPacketDelay.tla index ecb9abd887..28f002ec5a 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelay.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelay.tla @@ -45,6 +45,8 @@ vars == <> + +Heights == 1..MaxHeight (*************************************************************************** Instances of Chain @@ -79,24 +81,18 @@ GetChainByID(chainID) == \* update the client height of the client for the counterparty chain of chainID UpdateClientHeights(chainID) == /\ \/ /\ chainID = "chainA" - /\ chainBstore.height \notin DOMAIN chainAstore.counterpartyClientHeights + /\ chainAstore.counterpartyClientHeights[chainBstore.height] = 0 /\ chainAstore' = [chainAstore EXCEPT - !.counterpartyClientHeights = - [h \in DOMAIN chainAstore.counterpartyClientHeights \union {chainBstore.height} |-> - IF h = chainBstore.height - THEN chainAstore.timestamp - ELSE chainAstore.counterpartyClientHeights[h]], + !.counterpartyClientHeights = [chainAstore.counterpartyClientHeights EXCEPT + ![chainBstore.height] = chainAstore.timestamp], !.timestamp = chainAstore.timestamp + 1 ] /\ UNCHANGED chainBstore \/ /\ chainID = "chainB" - /\ chainAstore.height \notin DOMAIN chainBstore.counterpartyClientHeights + /\ chainBstore.counterpartyClientHeights[chainAstore.height] = 0 /\ chainBstore' = [chainBstore EXCEPT - !.counterpartyClientHeights = - [h \in DOMAIN chainBstore.counterpartyClientHeights \union {chainAstore.height} |-> - IF h = chainAstore.height - THEN chainBstore.timestamp - ELSE chainBstore.counterpartyClientHeights[h]], + !.counterpartyClientHeights = [chainBstore.counterpartyClientHeights EXCEPT + ![chainAstore.height] = chainBstore.timestamp], !.timestamp = chainBstore.timestamp + 1 ] /\ UNCHANGED chainAstore @@ -202,7 +198,7 @@ SubmitDatagramOrInstallClientHeight(chainID) == LET chainB == IF chainID = "chainB" THEN [chainBstore EXCEPT !.counterpartyClientHeights = - [chainAstore.counterpartyClientHeights EXCEPT + [chainBstore.counterpartyClientHeights EXCEPT ![packetDatagram.proofHeight] = chainBstore.timestamp], !.timestamp = chainBstore.timestamp + 1 ] @@ -287,7 +283,7 @@ Init == /\ ChainB!Init /\ outgoingPacketDatagrams = [chainID \in ChainIDs |-> <<>>] /\ packetLog = <<>> - /\ packetDatagramTimestamp = [x \in {} |-> 0] + /\ packetDatagramTimestamp = [<> \in ChainIDs \X Heights |-> 0] \* Next state action Next == @@ -305,15 +301,17 @@ Spec == Init /\ [][Next]_vars TypeOK == /\ ChainA!TypeOK /\ ChainB!TypeOK + /\ outgoingPacketDatagrams \in [ChainIDs -> Seq(Datagrams(Heights, MaxPacketSeq))] + /\ packetDatagramTimestamp \in [ChainIDs \X Heights -> Int] \* each packet datagam is processed at time t (stored in packetDatagramTimestamp), \* such that t >= ht + delay, where \* ht is the time when the client height is installed PacketDatagramsDelay == \A chainID \in ChainIDs : - \A h \in 1..MaxHeight : + \A h \in Heights : /\ GetChainByID(chainID).counterpartyClientHeights[h] /= 0 - /\ <> \in DOMAIN packetDatagramTimestamp + /\ packetDatagramTimestamp[<>] /= 0 => packetDatagramTimestamp[<>] >= GetChainByID(chainID).counterpartyClientHeights[h] + MaxDelay @@ -323,5 +321,5 @@ Inv == ============================================================================= \* Modification History -\* Last modified Thu Apr 15 18:53:41 CEST 2021 by ilinastoilkovska +\* Last modified Fri Apr 16 11:24:33 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 13:44:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla index 357a6d1bd3..8d02d8773d 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla @@ -394,11 +394,9 @@ InitChainStore(ChainID, Heights, ChannelOrdering, MaxDelay) == packetAcknowledgements |-> {}, packetsToAcknowledge |-> <<>> ] - -\* add ChainStore, ChannelEnds, write type invariant ============================================================================= \* Modification History -\* Last modified Thu Apr 15 18:50:37 CEST 2021 by ilinastoilkovska +\* Last modified Fri Apr 16 10:39:11 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 14:06:33 CET 2020 by ilinastoilkovska \ No newline at end of file diff --git a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla index bc25e1c16a..5667c31a82 100644 --- a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla +++ b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla @@ -10,12 +10,18 @@ EXTENDS Integers, FiniteSets, Sequences, IBCPacketDelayDefinitions (* @type: (Str, CHAINSTORE, DATAGRAM, Seq(LOGENTRY), <> -> Int) => [chainStore: CHAINSTORE, packetLog: Seq(LOGENTRY), datagramTimestamp: <> -> Int]; *) -HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == +HandlePacketRecv(chainID, chain, packetDatagram, delay, log, datagramTimestamp) == \* get chainID's channel end LET channelEnd == chain.channelEnd IN \* get packet LET packet == packetDatagram.packet IN + \* if the proof height of the packet datagram is installed on the chain, + \* then clientHeightTimestamp is the timestamp, denoting the time when this + \* height was installed on the chain; + \* otherwise it is 0, denoting that this height is not installed on the chain + LET clientHeightTimestamp == chain.counterpartyClientHeights[packetDatagram.proofHeight] IN + IF \* if the channel end is open for packet transmission /\ channelEnd.state = "OPEN" \* if the packet has not passed the timeout height @@ -26,8 +32,10 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == /\ packet.srcChannelID = channelEnd.counterpartyChannelID /\ packet.dstPortID = channelEnd.portID /\ packet.dstChannelID = channelEnd.channelID - \* if "PacketRecv" datagram can be verified - /\ packetDatagram.proofHeight \in DOMAIN chain.counterpartyClientHeights + \* if "PacketRecv" datagram can be verified (i.e., proofHeight is installed) + /\ clientHeightTimestamp /= 0 + \* the "PacketRecv" datagram was received after packet delay + /\ clientHeightTimestamp + delay < chain.timestamp THEN \* construct log entry for packet log LET logEntry == [ type |-> "PacketRecv", @@ -58,12 +66,8 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == \* add packet to the set of packets for which an acknowledgement should be written !.packetsToAcknowledge = Append(chain.packetsToAcknowledge, packet)] IN \* record the timestamp in the history variable - LET newDatagramTimestamp == - [ - tID \in (DOMAIN datagramTimestamp \union {<>}) |-> - IF tID = <> - THEN chain.timestamp - ELSE datagramTimestamp[tID] + LET newDatagramTimestamp == [datagramTimestamp EXCEPT + ![<>] = chain.timestamp ] IN [ @@ -82,11 +86,9 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == \* add packet to the set of packets for which an acknowledgement should be written !.packetsToAcknowledge = Append(chain.packetsToAcknowledge, packet)] IN \* record the timestamp in the history variable - LET newDatagramTimestamp == - [tID \in (DOMAIN datagramTimestamp \union {<>}) |-> - IF tID = <> - THEN chain.timestamp - ELSE datagramTimestamp[tID]] IN + LET newDatagramTimestamp == [datagramTimestamp EXCEPT + ![<>] = chain.timestamp + ] IN [ chainStore |-> newChainStore, @@ -104,7 +106,7 @@ HandlePacketRecv(chainID, chain, packetDatagram, log, datagramTimestamp) == (* @type: (Str, CHAINSTORE, DATAGRAM, Seq(LOGENTRY), <> -> Int) => [chainStore: CHAINSTORE, packetLog: Seq(LOGENTRY), datagramTimestamp: <> -> Int]; *) -HandlePacketAck(chainID, chain, packetDatagram, log, datagramTimestamp) == +HandlePacketAck(chainID, chain, packetDatagram, delay, log, datagramTimestamp) == \* get chainID's channel end LET channelEnd == chain.channelEnd IN \* get packet @@ -115,6 +117,12 @@ HandlePacketAck(chainID, chain, packetDatagram, log, datagramTimestamp) == sequence |-> packet.sequence, timeoutHeight |-> packet.timeoutHeight] IN + \* if the proof height of the packet datagram is installed on the chain, + \* then clientHeightTimestamp is the timestamp, denoting the time when this + \* height was installed on the chain; + \* otherwise it is 0, denoting that this height is not installed on the chain + LET clientHeightTimestamp == chain.counterpartyClientHeights[packetDatagram.proofHeight] IN + IF \* if the channel end is open for packet transmission /\ channelEnd.state = "OPEN" \* if the packet committment exists in the chain store @@ -124,8 +132,10 @@ HandlePacketAck(chainID, chain, packetDatagram, log, datagramTimestamp) == /\ packet.srcChannelID = channelEnd.channelID /\ packet.dstPortID = channelEnd.counterpartyPortID /\ packet.dstChannelID = channelEnd.counterpartyChannelID - \* if the "PacketAck" datagram can be verified - /\ packetDatagram.proofHeight \in DOMAIN chain.counterpartyClientHeights + \* if "PacketAck" datagram can be verified (i.e., proofHeight is installed) + /\ clientHeightTimestamp /= 0 + \* the "PacketAck" datagram was received after packet delay + /\ clientHeightTimestamp + delay < chain.timestamp THEN \* if the channel is ordered and the packet sequence is nextAckSeq LET newChainStore == IF /\ channelEnd.order = "ORDERED" @@ -143,11 +153,9 @@ HandlePacketAck(chainID, chain, packetDatagram, log, datagramTimestamp) == ELSE chain IN \* record the timestamp in the history variable - LET newDatagramTimestamp == - [tID \in (DOMAIN datagramTimestamp \union {<>}) |-> - IF tID = <> - THEN chain.timestamp - ELSE datagramTimestamp[tID]] IN + LET newDatagramTimestamp == [datagramTimestamp EXCEPT + ![<>] = chain.timestamp + ] IN [ chainStore |-> newChainStore, @@ -375,5 +383,5 @@ TimeoutOnClose(chain, counterpartyChain, packet, proofHeight) == ============================================================================= \* Modification History -\* Last modified Thu Apr 15 18:54:38 CEST 2021 by ilinastoilkovska +\* Last modified Fri Apr 16 11:52:20 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 15:12:41 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla b/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla new file mode 100644 index 0000000000..1411f647c7 --- /dev/null +++ b/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla @@ -0,0 +1,30 @@ +-------------------------- MODULE MC_IBCPacketDelay ------------------------- + +MaxHeight == 3 +ChannelOrdering == "UNORDERED" +MaxPacketSeq == 1 +MaxDelay == 1 + +VARIABLES + \* @type: CHAINSTORE; + chainAstore, \* store of ChainA + \* @type: CHAINSTORE; + chainBstore, \* store of ChainB + \* @type: Seq(DATAGRAM); + packetDatagramsChainA, \* sequence of packet datagrams incoming to ChainA + \* @type: Seq(DATAGRAM); + packetDatagramsChainB, \* sequence of packet datagrams incoming to ChainB + \* @type: Str -> Seq(DATAGRAM); + outgoingPacketDatagrams, \* packet datagrams created by the relayer but not submitted + \* @type: Seq(LOGENTRY); + packetLog, \* packet log + \* @type: Int; + appPacketSeqChainA, \* packet sequence number from the application on ChainA + \* @type: Int; + appPacketSeqChainB, \* packet sequence number from the application on ChainB + \* @type: <> -> Int; + packetDatagramTimestamp \* history variable that tracks when packet datagrams were processed + +INSTANCE IBCPacketDelay + +============================================================================= diff --git a/docs/spec/tla/packet-delay/README.md b/docs/spec/tla/packet-delay/README.md index fbc8c25c53..b01cdc44c0 100644 --- a/docs/spec/tla/packet-delay/README.md +++ b/docs/spec/tla/packet-delay/README.md @@ -12,3 +12,110 @@ terms of number of blocks; called [hybrid packet delay](https://github.com/cosmo ## The Model of the Protocol +We model a system where packet datagrams are both **submitted** by a +relayer and **handled** by a chain after a delay period has passed. +The system contains the following modules: +- [IBCPacketDelay.tla](IBCPacketDelay.tla), the main module, which +instantiates two chains and models the behavior of a correct relayer +as the environment where the two chains operate; +- [Chain.tla](Chain.tla), which models the behavior of a chain; +- [IBCPacketDelayDefinitions.tla](IBCPacketDelayDefinitions.tla), which contains definitions of operators that are shared between the + different modules; +- [ICS04PacketHandlers.tla](ICS04PacketHandlers.tla), which contains definitions of operators that specify packet transmission and packet datagram handling. + +### Timestamps + +To be able to enforce packet datagram submission and handling after a given delay, +we introduce a `timestamp` field in the chain store. +This `timestamp` is initially 1, and is incremented when a chain takes a step, that is, when it advances its height, or when it processes datagrams. + +Further, we need to keep track of the time when a counterparty client height +is installed on a chain. +That is, instead of keeping track of a set of counterparty client heights, in the +chain store, we store for each client height +the timestamp at which it was installed. +A counterparty client height whose timestamp is 0 has +not yet been installed on the chain. + + +### Relayer + +In this specification, the relayer is a part of the environment in which the two chains operate. +We define three actions that the environment (i.e., the relayer) can take: +- `UpdateClients`, which updates the counterparty client +heights of some chain. This action abstracts the +transmission of client datagrams. +- `CreateDatagrams`, which creates datagrams depending +on the packet log. This action scans the packet log and +adds the created packet datagram to the outgoing packet +datagram queue of the appropriate chain. +- `SubmitDatagramsWithDelay`, which submits datagrams if +delay has passed. This action scans the outgoing packet datagram queue +of a given chain, and +checks if the `proofHeight` of the datagram is a +client height that is installed on the chain. +The following cases are possible: + - if `proofHeight` is installed, then check if a `MaxDelay` period + has passed between the timestamp when the client height was + installed and the current `timestamp`, stored in the chain store. If + this is the case -- submit the datagram to the incoming packet + datagram queue of the chain; otherwise -- do nothing. + - if `proofHeight` is not installed, then install the it. + +### Packet handlers + +On the packet handling side, the chain also checks if the incoming +`PacketRecv` or `PacketAck` datagram has a valid `proofHeight` field. +This means that the `proofHeight` of the datagram should be installed on the +chain, and there should be `MaxDelay` period between the timestamp when the `proofHeight` was +installed and the current `timestamp` of the chain. + +### History variable + +We define a history variable, called `packetDatagramTimestamp`, where we store +for each `chainID` and each `proofHeight`, the timestamp of the chain `chainID` when a datagram with this `proofHeight` was processed. +We use this history variable in the invariant `PacketDatagramsDelay`, +described below. + + +## Invariants + +The module [IBCPacketDelay.tla](IBCPacketDelay.tla) defines the following invariants: +- `TypeOK`, the type invariant, +- `PacketDatagramsDelay`, which ensures that each packet +datagram is processed after a delay period. + +## Using the Model + +### Constants + +The module `IBCPacketDelay.tla` is parameterized by the constants: + - `MaxHeight`, a natural number denoting the maximal height of the chains, + - `ChannelOrdering`, a string denoting whether the channels are ordered or unordered, + - `MaxPacketSeq`, a natural number denoting the maximal packet sequence number + - `MaxDelay`, a natural number denoting the maximal packet delay + +### 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 `IBCPacketDelay.tla` + - create a model + - assign a value to the constants (example values can be found in `IBCPacketDelay.cfg`) + - 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 `IBCPacketDelay.tla` using the constants defined +in `IBCPacketDelay.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. + + From 6c92b34851ffbf4b4288efa0fe1cda560be4c2ce Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Mon, 19 Apr 2021 15:48:29 +0200 Subject: [PATCH 7/8] cfg file --- docs/spec/tla/packet-delay/Chain.tla | 4 +- docs/spec/tla/packet-delay/IBCPacketDelay.cfg | 12 +++ docs/spec/tla/packet-delay/IBCPacketDelay.tla | 15 +++- .../IBCPacketDelayDefinitions.tla | 21 ++++- .../tla/packet-delay/ICS04PacketHandlers.tla | 6 +- .../tla/packet-delay/MC_IBCPacketDelay.tla | 76 +++++++++++++++++++ 6 files changed, 123 insertions(+), 11 deletions(-) create mode 100644 docs/spec/tla/packet-delay/IBCPacketDelay.cfg diff --git a/docs/spec/tla/packet-delay/Chain.tla b/docs/spec/tla/packet-delay/Chain.tla index 98d8ef2356..c21ad200d0 100644 --- a/docs/spec/tla/packet-delay/Chain.tla +++ b/docs/spec/tla/packet-delay/Chain.tla @@ -128,7 +128,7 @@ Init == /\ chainStore = InitChainStore(ChainID, Heights, ChannelOrdering, MaxDelay) /\ incomingPacketDatagrams = <<>> /\ appPacketSeq = 1 - + \* Next state action \* The chain either \* - advances its height @@ -155,5 +155,5 @@ TypeOK == ============================================================================= \* Modification History -\* Last modified Fri Apr 16 11:49:19 CEST 2021 by ilinastoilkovska +\* Last modified Mon Apr 19 15:44:24 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 13:52:13 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelay.cfg b/docs/spec/tla/packet-delay/IBCPacketDelay.cfg new file mode 100644 index 0000000000..6b6fab9bd3 --- /dev/null +++ b/docs/spec/tla/packet-delay/IBCPacketDelay.cfg @@ -0,0 +1,12 @@ +CONSTANTS + MaxHeight = 3 + ChannelOrdering = "UNORDERED" + MaxPacketSeq = 1 + MaxDelay = 1 + +INIT Init +NEXT Next + +INVARIANTS + TypeOK + Inv \ No newline at end of file diff --git a/docs/spec/tla/packet-delay/IBCPacketDelay.tla b/docs/spec/tla/packet-delay/IBCPacketDelay.tla index 28f002ec5a..c52903bb35 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelay.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelay.tla @@ -65,14 +65,14 @@ ChainB == INSTANCE Chain WITH ChainID <- "chainB", chainStore <- chainBstore, incomingPacketDatagrams <- packetDatagramsChainB, - appPacketSeq <- appPacketSeqChainB - + appPacketSeq <- appPacketSeqChainB (*************************************************************************** Environment operators ***************************************************************************) \* get chain store by ID +\* @type: (Str) => CHAINSTORE; GetChainByID(chainID) == IF chainID = "chainA" THEN chainAstore @@ -150,6 +150,13 @@ PacketDatagram(srcChainID, dstChainID, packetLogEntry) == \* submit a packet datagram if a delay has passed \* or install the appropriate height if it is missing +(* @type: (Str) => +[ + datagramsChainA: Seq(DATAGRAM), datagramsChainB: Seq(DATAGRAM), + outgoingDatagrams: Str -> Seq(DATAGRAM), + chainA: CHAINSTORE, chainB: CHAINSTORE +]; +*) SubmitDatagramOrInstallClientHeight(chainID) == LET packetDatagram == Head(outgoingPacketDatagrams[chainID]) IN LET chain == GetChainByID(chainID) IN @@ -315,11 +322,11 @@ PacketDatagramsDelay == => packetDatagramTimestamp[<>] >= GetChainByID(chainID).counterpartyClientHeights[h] + MaxDelay -\* a conjnction of all invariants +\* a conjunction of all invariants Inv == /\ PacketDatagramsDelay ============================================================================= \* Modification History -\* Last modified Fri Apr 16 11:24:33 CEST 2021 by ilinastoilkovska +\* Last modified Mon Apr 19 15:43:40 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 13:44:21 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla index 8d02d8773d..cad0aee7ea 100644 --- a/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla +++ b/docs/spec/tla/packet-delay/IBCPacketDelayDefinitions.tla @@ -127,6 +127,7 @@ Max(S) == CHOOSE x \in S: \A y \in S: y <= x Note: we omit channel versions and connection hops. ***************************************************************************) +\* @type: (Str, Int) => Set(CHAN); ChannelEnds(channelOrdering, maxPacketSeq) == IF channelOrdering = "UNORDERED" THEN \* set of unordered channels @@ -154,6 +155,7 @@ ChannelEnds(channelOrdering, maxPacketSeq) == (******* PacketCommitments, PacketReceipts, PacketAcknowledgements *********) \* Set of packet commitments +\* @type: (Set(Int), Int) => Set(PACKETCOMM); PacketCommitments(Heights, maxPacketSeq) == [ channelID : ChannelIDs, @@ -163,6 +165,7 @@ PacketCommitments(Heights, maxPacketSeq) == ] \* Set of packet receipts +\* @type: (Int) => Set(PACKETREC); PacketReceipts(maxPacketSeq) == [ channelID : ChannelIDs, @@ -171,6 +174,7 @@ PacketReceipts(maxPacketSeq) == ] \* Set of packet acknowledgements +\* @type: (Int) => Set(PACKETACK); PacketAcknowledgements(maxPacketSeq) == [ channelID : ChannelIDs, @@ -181,6 +185,7 @@ PacketAcknowledgements(maxPacketSeq) == (********************************* Packets *********************************) \* Set of packets +\* @type: (Set(Int), Int) => Set(PACKET); Packets(Heights, maxPacketSeq) == [ sequence : 1..maxPacketSeq, @@ -222,6 +227,7 @@ Packets(Heights, maxPacketSeq) == A chain store is the combination of the provable and private stores. ***************************************************************************) +\* @type: (Set(Int), Str, Int) => Set(CHAINSTORE); ChainStores(Heights, channelOrdering, maxPacketSeq) == [ height : Heights, @@ -236,6 +242,7 @@ ChainStores(Heights, channelOrdering, maxPacketSeq) == (******************************** Datagrams ********************************) \* Set of datagrams (we consider only packet datagrams) +\* @type: (Set(Int), Int) => Set(DATAGRAM); Datagrams(Heights, maxPacketSeq) == [ type : {"PacketRecv"}, @@ -254,6 +261,7 @@ NullDatagram == (**************************** PacketLogEntries *****************************) \* Set of packet log entries +\* @type: (Set(Int), Int) => Set(LOGENTRY); PacketLogEntries(Heights, maxPacketSeq) == [ type : {"PacketSent"}, @@ -287,6 +295,7 @@ NullPacketLogEntry == ***************************************************************************) \* get the ID of chainID's counterparty chain +\* @type: (Str) => Str; GetCounterpartyChainID(chainID) == IF chainID = "chainA" THEN "chainB" ELSE "chainA" @@ -298,6 +307,7 @@ GetMaxCounterpartyClientHeight(chain) == ELSE nullHeight \* get the channel ID of the channel end at chainID +\* @type: (Str) => Str; GetChannelID(chainID) == IF chainID = "chainA" THEN "chanAtoB" @@ -306,6 +316,7 @@ GetChannelID(chainID) == ELSE nullChannelID \* get the channel ID of the channel end at chainID's counterparty chain +\* @type: (Str) => Str; GetCounterpartyChannelID(chainID) == IF chainID = "chainA" THEN "chanBtoA" @@ -314,6 +325,7 @@ GetCounterpartyChannelID(chainID) == ELSE nullChannelID \* get the port ID at chainID +\* @type: (Str) => Str; GetPortID(chainID) == IF chainID = "chainA" THEN "portA" @@ -322,6 +334,7 @@ GetPortID(chainID) == ELSE nullPortID \* get the port ID at chainID's counterparty chain +\* @type: (Str) => Str; GetCounterpartyPortID(chainID) == IF chainID = "chainA" THEN "portB" @@ -341,6 +354,7 @@ GetLatestHeight(chain) == \* - state is "OPEN" (we assume channel handshake has successfully finished) \* - order is "UNORDERED" \* - portID, channelID, counterpartyPortID, counterpartyChannelID depend on ChainID +\* @type: (Str) => CHAN; InitUnorderedChannelEnd(ChainID) == [ state |-> "OPEN", @@ -356,6 +370,7 @@ InitUnorderedChannelEnd(ChainID) == \* - order is "ORDERED" \* - nextSendSeq, nextRcvSeq, nextAckSeq are set to 0 \* - portID, channelID, counterpartyPortID, counterpartyChannelID depend on ChainID +\* @type: (Str) => CHAN; InitOrderedChannelEnd(ChainID) == [ state |-> "OPEN", @@ -367,9 +382,10 @@ InitOrderedChannelEnd(ChainID) == channelID |-> GetChannelID(ChainID), counterpartyPortID |-> GetCounterpartyPortID(ChainID), counterpartyChannelID |-> GetCounterpartyChannelID(ChainID) - ] + ] \* Initial value of a channel end, based on the channel ordering +\* @type: (Str, Str) => CHAN; InitChannelEnd(ChainID, ChannelOrdering) == IF ChannelOrdering = "ORDERED" THEN InitOrderedChannelEnd(ChainID) @@ -382,6 +398,7 @@ InitChannelEnd(ChainID, ChannelOrdering) == \* - the channel end is initialized to InitChannelEnd \* - the packet committments, receipts, acknowledgements, and packets \* to acknowledge are empty +\* @type: (Str, Set(Int), Str, Int) => CHAINSTORE; InitChainStore(ChainID, Heights, ChannelOrdering, MaxDelay) == [ height |-> 1, @@ -397,6 +414,6 @@ InitChainStore(ChainID, Heights, ChannelOrdering, MaxDelay) == ============================================================================= \* Modification History -\* Last modified Fri Apr 16 10:39:11 CEST 2021 by ilinastoilkovska +\* Last modified Mon Apr 19 15:46:15 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 14:06:33 CET 2020 by ilinastoilkovska \ No newline at end of file diff --git a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla index 5667c31a82..22a3b359be 100644 --- a/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla +++ b/docs/spec/tla/packet-delay/ICS04PacketHandlers.tla @@ -7,7 +7,7 @@ EXTENDS Integers, FiniteSets, Sequences, IBCPacketDelayDefinitions ***************************************************************************) \* Handle "PacketRecv" datagrams -(* @type: (Str, CHAINSTORE, DATAGRAM, Seq(LOGENTRY), <> -> Int) => +(* @type: (Str, CHAINSTORE, DATAGRAM, Int, Seq(LOGENTRY), <> -> Int) => [chainStore: CHAINSTORE, packetLog: Seq(LOGENTRY), datagramTimestamp: <> -> Int]; *) HandlePacketRecv(chainID, chain, packetDatagram, delay, log, datagramTimestamp) == @@ -103,7 +103,7 @@ HandlePacketRecv(chainID, chain, packetDatagram, delay, log, datagramTimestamp) \* Handle "PacketAck" datagrams -(* @type: (Str, CHAINSTORE, DATAGRAM, Seq(LOGENTRY), <> -> Int) => +(* @type: (Str, CHAINSTORE, DATAGRAM, Int, Seq(LOGENTRY), <> -> Int) => [chainStore: CHAINSTORE, packetLog: Seq(LOGENTRY), datagramTimestamp: <> -> Int]; *) HandlePacketAck(chainID, chain, packetDatagram, delay, log, datagramTimestamp) == @@ -383,5 +383,5 @@ TimeoutOnClose(chain, counterpartyChain, packet, proofHeight) == ============================================================================= \* Modification History -\* Last modified Fri Apr 16 11:52:20 CEST 2021 by ilinastoilkovska +\* Last modified Mon Apr 19 15:46:42 CEST 2021 by ilinastoilkovska \* Created Thu Dec 10 15:12:41 CET 2020 by ilinastoilkovska diff --git a/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla b/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla index 1411f647c7..895426203c 100644 --- a/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla +++ b/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla @@ -1,21 +1,97 @@ -------------------------- MODULE MC_IBCPacketDelay ------------------------- MaxHeight == 3 +\* @type: Str; ChannelOrdering == "UNORDERED" MaxPacketSeq == 1 MaxDelay == 1 VARIABLES + (* @typeAlias: CHAN = + [ + state: Str, + order: Str, + portID: Str, + channelID: Str, + counterpartyPortID: Str, + counterpartyChannelID: Str, + nextSendSeq: Int, + nextRcvSeq: Int, + nextAckSeq: Int + ]; + *) + (* @typeAlias: PACKET = + [ + sequence: Int, + timeoutHeight: Int, + srcPortID: Str, + srcChannelID: Str, + dstPortID: Str, + dstChannelID: Str + ]; + *) + (* @typeAlias: PACKETCOMM = + [ + portID: Str, + channelID: Str, + sequence: Int, + timeoutHeight: Int + ]; + *) + (* @typeAlias: PACKETREC = + [ + portID: Str, + channelID: Str, + sequence: Int + ]; + *) + (* @typeAlias: PACKETACK = + [ + portID: Str, + channelID: Str, + sequence: Int, + acknowledgement: Bool + ]; + *) + (* @typeAlias: CHAINSTORE = + [ + height: Int, + timestamp: Int, + counterpartyClientHeights: Int -> Int, + channelEnd: CHAN, + packetCommitments: Set(PACKETCOMM), + packetsToAcknowledge: Seq(PACKET), + packetReceipts: Set(PACKETREC), + packetAcknowledgements: Set(PACKETACK) + ]; + *) \* @type: CHAINSTORE; chainAstore, \* store of ChainA \* @type: CHAINSTORE; chainBstore, \* store of ChainB + (* @typeAlias: DATAGRAM = + [ + type: Str, + packet: PACKET, + proofHeight: Int, + acknowledgement: Bool + ]; + *) \* @type: Seq(DATAGRAM); packetDatagramsChainA, \* sequence of packet datagrams incoming to ChainA \* @type: Seq(DATAGRAM); packetDatagramsChainB, \* sequence of packet datagrams incoming to ChainB \* @type: Str -> Seq(DATAGRAM); outgoingPacketDatagrams, \* packet datagrams created by the relayer but not submitted + (* @typeAlias: LOGENTRY = + [ + type: Str, + srcChainID: Str, + sequence: Int, + timeoutHeight: Int, + acknowledgement: Bool + ]; + *) \* @type: Seq(LOGENTRY); packetLog, \* packet log \* @type: Int; From cd3ff098b2fae0d7e3e0790a88c4df911f12368a Mon Sep 17 00:00:00 2001 From: istoilkovska Date: Tue, 20 Apr 2021 16:11:46 +0200 Subject: [PATCH 8/8] annotations in MC file --- .../tla/packet-delay/MC_IBCPacketDelay.tla | 76 ------------------- 1 file changed, 76 deletions(-) diff --git a/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla b/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla index 895426203c..1411f647c7 100644 --- a/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla +++ b/docs/spec/tla/packet-delay/MC_IBCPacketDelay.tla @@ -1,97 +1,21 @@ -------------------------- MODULE MC_IBCPacketDelay ------------------------- MaxHeight == 3 -\* @type: Str; ChannelOrdering == "UNORDERED" MaxPacketSeq == 1 MaxDelay == 1 VARIABLES - (* @typeAlias: CHAN = - [ - state: Str, - order: Str, - portID: Str, - channelID: Str, - counterpartyPortID: Str, - counterpartyChannelID: Str, - nextSendSeq: Int, - nextRcvSeq: Int, - nextAckSeq: Int - ]; - *) - (* @typeAlias: PACKET = - [ - sequence: Int, - timeoutHeight: Int, - srcPortID: Str, - srcChannelID: Str, - dstPortID: Str, - dstChannelID: Str - ]; - *) - (* @typeAlias: PACKETCOMM = - [ - portID: Str, - channelID: Str, - sequence: Int, - timeoutHeight: Int - ]; - *) - (* @typeAlias: PACKETREC = - [ - portID: Str, - channelID: Str, - sequence: Int - ]; - *) - (* @typeAlias: PACKETACK = - [ - portID: Str, - channelID: Str, - sequence: Int, - acknowledgement: Bool - ]; - *) - (* @typeAlias: CHAINSTORE = - [ - height: Int, - timestamp: Int, - counterpartyClientHeights: Int -> Int, - channelEnd: CHAN, - packetCommitments: Set(PACKETCOMM), - packetsToAcknowledge: Seq(PACKET), - packetReceipts: Set(PACKETREC), - packetAcknowledgements: Set(PACKETACK) - ]; - *) \* @type: CHAINSTORE; chainAstore, \* store of ChainA \* @type: CHAINSTORE; chainBstore, \* store of ChainB - (* @typeAlias: DATAGRAM = - [ - type: Str, - packet: PACKET, - proofHeight: Int, - acknowledgement: Bool - ]; - *) \* @type: Seq(DATAGRAM); packetDatagramsChainA, \* sequence of packet datagrams incoming to ChainA \* @type: Seq(DATAGRAM); packetDatagramsChainB, \* sequence of packet datagrams incoming to ChainB \* @type: Str -> Seq(DATAGRAM); outgoingPacketDatagrams, \* packet datagrams created by the relayer but not submitted - (* @typeAlias: LOGENTRY = - [ - type: Str, - srcChainID: Str, - sequence: Int, - timeoutHeight: Int, - acknowledgement: Bool - ]; - *) \* @type: Seq(LOGENTRY); packetLog, \* packet log \* @type: Int;