Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Basic packet flow in TLA+ #248

Merged
merged 8 commits into from
Sep 30, 2020
Merged

Basic packet flow in TLA+ #248

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
18203aa
send packet action added, relayer packet creation
istoilkovska Sep 15, 2020
2440e29
packet receive, ack
istoilkovska Sep 18, 2020
d2d07f0
packet ack
istoilkovska Sep 22, 2020
6f66413
readme updated
istoilkovska Sep 22, 2020
0b5b78e
Apply suggestions from code review
istoilkovska Sep 25, 2020
fc2dd62
addressed comments
istoilkovska Sep 28, 2020
3ee4b0e
applied review comments
istoilkovska Sep 30, 2020
7aead8a
moved files around
istoilkovska Sep 30, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
207 changes: 177 additions & 30 deletions docs/spec/relayer/Chain.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
---------------------------- MODULE Chain ----------------------------

EXTENDS Integers, FiniteSets, RelayerDefinitions,
ClientHandlers, ConnectionHandlers, ChannelHandlers
ClientHandlers, ConnectionHandlers, ChannelHandlers, PacketHandlers

CONSTANTS MaxHeight, \* maximal chain height
ChainID, \* chain identifier
Expand All @@ -10,9 +10,12 @@ CONSTANTS MaxHeight, \* maximal chain height

VARIABLES chainStore, \* chain store, containing client heights, a connection end, a channel end
incomingDatagrams, \* set of incoming datagrams
history \* history variable
incomingPacketDatagrams, \* sequence of incoming packet datagrams
history, \* history variable
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the purpose of history variable?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We use the history variable in the invariant we check with Apalache. The history variable is a record that stores flags about the state of the connection and channel ends. The flags are set once, when the state changes. The invariant checks that if a flag is set, the state of the connection or channel end does not go back to a previous state.

Example: a connection is open, and the flag history.connOpen is set to TRUE. The following invariant has to hold:

history.connOpen => /\ chainA.connectionEnd.state /= "UNINIT"
                    /\ chainA.connectionEnd.state /= "INIT"
                    /\ chainA.connectionEnd.state /= "TRYOPEN"

packetLog, \* packet log
appPacketSeq \* packet sequence number from the application on the chain

vars == <<chainStore, incomingDatagrams, history>>
vars == <<chainStore, incomingDatagrams, incomingPacketDatagrams, history, packetLog, appPacketSeq>>
Heights == 1..MaxHeight \* set of possible heights of the chains in the system

(***************************************************************************
Expand Down Expand Up @@ -78,12 +81,34 @@ ChannelUpdate(chainID, store, datagrams) ==

chanCloseConfirmStore

(***************************************************************************
Packet update operators
***************************************************************************)
\* Update the chain store of the chain with chainID and the packet log,
\* using the packet datagrams generated by the relayer
\* (Handler operators defined in PacketHandlers.tla)
PacketUpdate(chainID, store, packetDatagrams, log) ==
\* if the sequence of packet datagrams is not empty
IF packetDatagrams /= AsSeqPacketDatagrams(<<>>)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why the structure is not the same as with others, i.e., it contains HandlePacketRecv and HandlePacketAck that internally check for the datagram type?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is because the PacketUpdate operator computes the update to the chain store with a single packet datagram, taken from the sequence of packet datagrams, while the other *Update operators update the chain store with a set of datagrams, which is obtained by taking a subset of the incoming datagrams, containing datagrams of particular type.

THEN \* process the packet datagram at the head of the sequence
LET packetDatagram == AsPacketDatagram(Head(packetDatagrams)) IN
LET packet == packetDatagram.packet IN
\* get the new updated store and packet log entry
LET newStoreAndLog ==
IF packetDatagram.type = "PacketRecv"
THEN HandlePacketRecv(chainID, store, packetDatagram, log)
ELSE IF packetDatagram.type = "PacketAck"
THEN HandlePacketAck(chainID, store, packetDatagram, log)
ELSE [chainStore|-> store, packetLogEntry |-> log] IN
newStoreAndLog
ELSE [chainStore |-> store, packetLog |->log]

(***************************************************************************
Chain update operators
***************************************************************************)
\* Update chainID with the received datagrams
\* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels).
UpdateChainStore(chainID, datagrams) ==
\* Supports ICS2 (Clients), ICS3 (Connections), and ICS4 (Channels & Packets).
UpdateChainStoreAndPacketLog(chainID, datagrams, packetDatagrams, log) ==
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should have a sequence of datagrams for everything. We can get handshake datagrams interleaved with packet datagrams and the order matters. And then in the function we should process them in order.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I had the idea to transition to sequences of datagams completely. But doing so increases the state space that TLC enumerates. Will try to think about better handling, while still processing datagrams in order.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agree with Anca that orders matter. We can have either sequence or handle only single datagram at the time.


\* ICS 002: Client updates
LET clientUpdatedStore == LightClientUpdate(chainID, chainStore, datagrams) IN
Expand All @@ -94,15 +119,62 @@ UpdateChainStore(chainID, datagrams) ==
\* ICS 003: Channel updates
LET channelUpdatedStore == ChannelUpdate(chainID, connectionUpdatedStore, datagrams) IN

\* ICS 004: Packet transmission
LET packetUpdatedStoreAndLogEntry == PacketUpdate(chainID, channelUpdatedStore, packetDatagrams, log) IN
LET packetUpdatedStore == packetUpdatedStoreAndLogEntry.chainStore IN

\* update height
LET updatedChainStore ==
IF /\ chainStore /= channelUpdatedStore
IF /\ chainStore /= packetUpdatedStore
/\ chainStore.height + 1 \in Heights
THEN [channelUpdatedStore EXCEPT !.height = chainStore.height + 1]
ELSE channelUpdatedStore
THEN [packetUpdatedStore EXCEPT !.height = chainStore.height + 1]
ELSE packetUpdatedStore
IN
updatedChainStore

[chainStore |-> updatedChainStore,
packetLog |-> packetUpdatedStoreAndLogEntry.packetLog]

(***************************************************************************
Packet acknowledgement operators
***************************************************************************)

\* write acknowledgements to chain store
WriteAcknowledgement(chain, packet) ==
\* if the acknowledgement for the packet has not been written
IF packet \notin chain.packetAcknowledgements
THEN \* write the acknowledgement to the chain store and remove
\* the packet from the set of packets to acknowledge
LET packetAcknowledgement ==
AsPacketAcknowledgement(
[channelID |-> packet.dstChannelID,
sequence |-> packet.sequence,
acknowledgement |-> TRUE]) IN
[chain EXCEPT !.packetAcknowledgements =
chain.packetAcknowledgements
\union
{packetAcknowledgement},
!.packetsToAcknowledge =
Tail(chain.packetsToAcknowledge)]

\* remove the packet from the set of packets to acknowledge
ELSE [chain EXCEPT !.packetsToAcknowledge =
Tail(chain.packetsToAcknowledge)]

\* log acknowledgements to packet Log
LogAcknowledgement(chain, log, packet) ==
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not sure if we need to model event log as it is not necessarily, i.e., current ICS18 is not using it. It might be useful as part of MBT, but in the initial version I would prefer having the minimal set of functionalities needed.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can have it merged like this for now, I will experiment to see if by removing it we can obtain some model checking results.

\* if the acknowledgement for the packet has not been written
IF packet \notin chain.packetAcknowledgements
THEN \* append a "WriteAck" log entry to the log
LET packetLogEntry ==
AsPacketLogEntry(
[type |-> "WriteAck",
srcChainID |-> ChainID,
sequence |-> packet.sequence,
timeoutHeight |-> packet.timeoutHeight,
acknowledgement |-> TRUE]) IN
Append(log, packetLogEntry)
\* do not add anything to the log
ELSE log

(***************************************************************************
Chain actions
Expand All @@ -111,29 +183,98 @@ UpdateChainStore(chainID, datagrams) ==
AdvanceChain ==
/\ chainStore.height + 1 \in Heights
/\ chainStore' = [chainStore EXCEPT !.height = chainStore.height + 1]
/\ UNCHANGED <<incomingDatagrams, history>>
/\ UNCHANGED <<incomingDatagrams, incomingPacketDatagrams, history>>
/\ UNCHANGED <<packetLog, appPacketSeq>>

\* Send a packet
SendPacket ==
\* Create a packet
\* Abstract away from packet data, ports, and timestamp.
\* Assume timeoutHeight is MaxHeight + 1
LET packet == AsPacket([
sequence |-> appPacketSeq,
timeoutHeight |-> MaxHeight + 1,
srcChannelID |-> GetChannelID(ChainID),
dstChannelID |-> GetChannelID(GetCounterpartyChainID(ChainID))
]) IN
LET connectionEnd == chainStore.connectionEnd IN
LET channelEnd == chainStore.connectionEnd.channelEnd IN
LET latestClientHeight == GetMaxCounterpartyClientHeight(chainStore) IN
\* channel end is neither null nor closed
/\ channelEnd.state \notin {"UNINIT", "CLOSED"}
\* connection end is initialized
/\ connectionEnd.state /= "UNINIT"
\* timeout height has not passed
/\ \/ packet.timeoutHeight = 0
\/ latestClientHeight < packet.timeoutHeight
/\ \* if the channel is ordered, check if packetSeq is nextSentSeq,
\* add a packet committment in the chain store, and increase nextSentSeq
\/ /\ channelEnd.order = "ORDERED"
/\ packet.sequence = channelEnd.nextSentSeq
istoilkovska marked this conversation as resolved.
Show resolved Hide resolved
/\ packet.sequence <= MaxPacketSeq
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a model constraint, not the handler one; ideally they should not be mixed and model constraint can be a precondition at the higher level.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've refactored this action a bit.

/\ chainStore' = [chainStore EXCEPT
!.packetCommitments =
chainStore.packetCommitments \union {[channelID |-> packet.srcChannelID,
sequence |-> packet.sequence,
timeoutHeight |-> packet.timeoutHeight]},
!.connectionEnd.channelEnd.nextSentSeq = channelEnd.nextSentSeq + 1
]
\* if the channel is unordered,
\* add a packet committment in the chain store
\/ /\ channelEnd.order = "UNORDERED"
/\ chainStore' = [chainStore EXCEPT
!.packetCommitments =
chainStore.packetCommitments \union {[channelID |-> packet.srcChannelID,
sequence |-> packet.sequence,
timeoutHeight |-> packet.timeoutHeight]}
]

\* log sent packet
/\ packetLog' = Append(packetLog, AsPacketLogEntry(
[type |-> "PacketSend",
srcChainID |-> ChainID,
sequence |-> packet.sequence ,
timeoutHeight |-> packet.timeoutHeight]))
\* increase application packet sequence
/\ appPacketSeq' = appPacketSeq + 1
/\ UNCHANGED <<incomingDatagrams, incomingPacketDatagrams, history>>

\* write a packet acknowledgement on the packet log and chain store
AcknowledgePacket ==
/\ chainStore.packetsToAcknowledge /= AsSeqPacket(<<>>)
/\ chainStore' = WriteAcknowledgement(chainStore, Head(chainStore.packetsToAcknowledge))
/\ packetLog' = LogAcknowledgement(chainStore, packetLog, Head(chainStore.packetsToAcknowledge))
/\ UNCHANGED <<incomingDatagrams, incomingPacketDatagrams, history>>
/\ UNCHANGED appPacketSeq

\* Handle the datagrams and update the chain state
HandleIncomingDatagrams ==
/\ incomingDatagrams /= AsSetDatagrams({})
/\ chainStore' = UpdateChainStore(ChainID, AsSetDatagrams(incomingDatagrams))
/\ incomingDatagrams' = AsSetDatagrams({})
/\ history' = CASE chainStore'.connectionEnd.state = "INIT"
-> [history EXCEPT !.connInit = TRUE]
[] chainStore'.connectionEnd.state = "TRYOPEN"
-> [history EXCEPT !.connTryOpen = TRUE]
[] chainStore'.connectionEnd.state = "OPEN"
-> [history EXCEPT !.connOpen = TRUE]
[] chainStore'.connectionEnd.channelEnd.state = "INIT"
-> [history EXCEPT !.chanInit = TRUE]
[] chainStore'.connectionEnd.channelEnd.state = "TRYOPEN"
-> [history EXCEPT !.chanTryOpen = TRUE]
[] chainStore'.connectionEnd.channelEnd.state = "OPEN"
-> [history EXCEPT !.chanOpen = TRUE]
[] chainStore'.connectionEnd.channelEnd.state = "CLOSED"
-> [history EXCEPT !.chanClosed = TRUE]
[] OTHER
-> history
/\ \/ incomingDatagrams /= AsSetDatagrams({})
\/ incomingPacketDatagrams /= AsSeqPacketDatagrams(<<>>)
/\ LET updatedChainStoreAndPacketLog == UpdateChainStoreAndPacketLog(ChainID, incomingDatagrams, incomingPacketDatagrams, packetLog) IN
/\ chainStore' = updatedChainStoreAndPacketLog.chainStore
/\ packetLog' = updatedChainStoreAndPacketLog.packetLog
/\ incomingDatagrams' = AsSetDatagrams({})
/\ incomingPacketDatagrams' = IF incomingPacketDatagrams /= AsSeqPacketDatagrams(<<>>)
THEN Tail(incomingPacketDatagrams)
ELSE incomingPacketDatagrams
/\ history' = CASE chainStore'.connectionEnd.state = "INIT"
-> [history EXCEPT !.connInit = TRUE]
[] chainStore'.connectionEnd.state = "TRYOPEN"
-> [history EXCEPT !.connTryOpen = TRUE]
[] chainStore'.connectionEnd.state = "OPEN"
-> [history EXCEPT !.connOpen = TRUE]
[] chainStore'.connectionEnd.channelEnd.state = "INIT"
-> [history EXCEPT !.chanInit = TRUE]
[] chainStore'.connectionEnd.channelEnd.state = "TRYOPEN"
-> [history EXCEPT !.chanTryOpen = TRUE]
[] chainStore'.connectionEnd.channelEnd.state = "OPEN"
-> [history EXCEPT !.chanOpen = TRUE]
[] chainStore'.connectionEnd.channelEnd.state = "CLOSED"
-> [history EXCEPT !.chanClosed = TRUE]
[] OTHER
-> history
/\ UNCHANGED appPacketSeq

(***************************************************************************
Specification
Expand All @@ -146,7 +287,9 @@ HandleIncomingDatagrams ==
Init ==
/\ chainStore = InitChainStore(ChannelOrdering)
/\ incomingDatagrams = AsSetDatagrams({})
/\ incomingPacketDatagrams = AsSeqDatagrams(<<>>)
/\ history = InitHistory
/\ appPacketSeq = AsInt(1)

\* Next state action
\* The chain either
Expand All @@ -156,6 +299,8 @@ Init ==
Next ==
\/ AdvanceChain
\/ HandleIncomingDatagrams
\/ SendPacket
istoilkovska marked this conversation as resolved.
Show resolved Hide resolved
\/ AcknowledgePacket
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we add timeout handling here? Then it seems complete.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, what about channel closing? Is it also triggered "externally"?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

channel closing is triggered by the application so yes the trigger is "external"

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We currently have a flag for each chain that triggers channel closing, which is non-deterministically set by the environment. When we add timeouts we would have channel closing that is triggered by a timeout.

\/ UNCHANGED vars

Fairness ==
Expand All @@ -171,6 +316,8 @@ TypeOK ==
/\ chainStore \in ChainStores(MaxHeight, ChannelOrdering, MaxPacketSeq)
/\ incomingDatagrams \in SUBSET Datagrams(MaxHeight, MaxPacketSeq)
/\ history \in Histories
/\ appPacketSeq \in 1..MaxPacketSeq
/\ packetLog \in SUBSET Packets(MaxHeight, MaxPacketSeq)

(***************************************************************************
Properties
Expand All @@ -182,5 +329,5 @@ HeightDoesntDecrease ==

=============================================================================
\* Modification History
\* Last modified Thu Sep 10 15:43:42 CEST 2020 by ilinastoilkovska
\* Last modified Tue Sep 22 13:43:43 CEST 2020 by ilinastoilkovska
\* Created Fri Jun 05 16:56:21 CET 2020 by ilinastoilkovska
Loading