-
Notifications
You must be signed in to change notification settings - Fork 326
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.
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
Relayer TLA+ specification, connection and channel handshake datagrams #55
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks amazing, though I am a bit surprised by the whopping complexity. The sharing of variables across files (pendingDatagrams) makes it hard to follow. However, this problem is exacerbated on my side since I'm still getting comfortable with TLA+.
|
/\ dgr.type = "ChanOpenInit" | ||
/\ dgr.channelID = GetChannelID(chainID)} IN | ||
|
||
IF chanOpenInitDgrs /= {} /\ chain.connectionEnd.state /= "UNINIT" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should it be chain.connectionEnd.channelEnd.state
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this check is for the state of the underlying connection, to make sure it is initiated.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Exactly, there's a line in the ICS04 handlers stating abortTransactionUnless(connection !== null)
or abortTransactionUnless(connection.state === OPEN)
.
\* connection datagrams from dstChainID to srcChainID | ||
LET srcConnectionDatagrams == ComputeConnectionDatagrams(dstChainID, srcChainID) IN | ||
\* connection datagrams from srcChainID to dstChainID | ||
LET dstConnectionDatagrams == ComputeConnectionDatagrams(srcChainID, dstChainID) IN |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If I am not wrong ConnOpenInit
will be created for both source and destination chain in case dstConnectionEnd.state = "UNINIT" /\ srcConnectionEnd.state = "UNINIT"
? We want non-deterministically to send it only to one of the chain.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is fixed now, we are only sending in one direction, i.e., from srcChainID
to dstChainID
LET clientUpdatedChain == [ | ||
height |-> chain.height, | ||
counterpartyClientHeight |-> IF updateClientHeights /= {} | ||
THEN Max(updateClientHeights) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should store all installed heights, not just the maximum height.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Indeed, installing only the maximum height violates liveness.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Amazing work! Few comments that should probably be addressed in a separate PR:
- Chain height (environment) should be increased before datagrams are processed.
- Protocols should manage its state, not chain. For example, connectionEnd should not be part of the chain, but connection handshake protocol.
- It might be useful to be able to have minimal relayer spec (with a very simple protocol on top) so we can check if relayer satisfies high level properties (for example eventual message delivery)
- We should always have at least two correct relayer processes and adversarial relayers (probably sufficient to model as adversary network)
- We probably want to be more precise with respect to management of ids. Ids are owned by the chains and then relayer need to pick right id and to try to create the corresponding client.
- We probably want to model configuration based relayer, i.e., similar functionality should be modelled using constants
- I am not sure if counterpartyClientHeight is the best name for this concept. We probably want to emphasise that it is light client state, but we probably only need height as part of it to model important mechanisms.
- I am not sure if
UpdateRelayerClients
should be atomic action. I think this should
be part of the relay functionality.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The spec look great!! Thanks Ilina!
/\ dgr.type = "ChanOpenInit" | ||
/\ dgr.channelID = GetChannelID(chainID)} IN | ||
|
||
IF chanOpenInitDgrs /= {} /\ chain.connectionEnd.state /= "UNINIT" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this check is for the state of the underlying connection, to make sure it is initiated.
Co-authored-by: Adi Seredinschi <adi@informal.systems>
Description
WIP for #5
Updated Relayer TLA+ specification, that in addition to client update datagrams, now handles connection and channel handshake datagrams.
The whole specification now contains five modules:
Relayer.tla
(the main module)Environment.tla
ClientHandlers.tla
ConnectionHandlers.tla
ChannelHandlers.tla
The module
Relayer.tla
contains the specification of the relayer algorithm.It instantiates the module
Environment.tla
, which takes care of the chain logic.The module
Environment.tla
extends the modulesClientHandlers.tla
,ConnectionHandlers.tla
, andChannelHandlers.tla
, which contain definition ofoperators that handle client, connection handshake, and channel handshake
datagrams, respectively.
The
README.md
file contains instructions about how to load the specification inthe TLA+ Toolbox and check the specified invariants and properties with TLC.
For contributor use:
docs/
) and code commentsFiles changed
in the Github PR explorer