-
Notifications
You must be signed in to change notification settings - Fork 323
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
Connection Handshake (ICS3) L2 TLA+ spec #58
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.
Added some comments. I think we should discuss at this point.
***************************************************************************) | ||
ConnectionEnds == | ||
[ | ||
connectionID : ConnectionIDs \union {Null}, |
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.
Is there a need having Null here as connectionEnd is never initialised with null fields? The same for clientIDs.
(*** | ||
* Initial value for a connection end. | ||
**) | ||
ConnectionEndInitValue == |
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 probably not needed.
(*** | ||
* Initial values for a connection. | ||
**) | ||
ConnectionInitValue == |
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 same here.
CHModuleInitValue == | ||
[chainHeight |-> 1, | ||
connectionState |-> "UNINT", | ||
connection |-> ConnectionInitValue ] |
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 just define NilConnection as operator and that should be initial value of the connection field.
connection : Connections] | ||
|
||
NextEnv == | ||
\/ OnConnInitMsg |
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 can probably simplify this with inMsg' \in ConnectionHandshakeMessages.
*****************************************************************************) | ||
|
||
Init == | ||
turn = "env" \* Initially, the environment takes a turn. |
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.
turn = "env" \* Initially, the environment takes a turn. | |
/\ turn = "env" \* Initially, the environment takes a turn. |
verification/spec/connection-handshake/ConnectionHandshakeModule.tla
Outdated
Show resolved
Hide resolved
verification/spec/connection-handshake/ConnectionHandshakeModule.tla
Outdated
Show resolved
Hide resolved
verification/spec/connection-handshake/ConnectionHandshakeModule.tla
Outdated
Show resolved
Hide resolved
verification/spec/connection-handshake/ConnectionHandshakeModule.tla
Outdated
Show resolved
Hide resolved
verification/spec/connection-handshake/ConnectionHandshakeModule.tla
Outdated
Show resolved
Hide resolved
verification/spec/connection-handshake/ConnectionHandshakeModule.tla
Outdated
Show resolved
Hide resolved
verification/spec/connection-handshake/ConnectionHandshakeModule.tla
Outdated
Show resolved
Hide resolved
verification/spec/connection-handshake/ConnectionHandshakeModule.tla
Outdated
Show resolved
Hide resolved
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.
Great work!It turns out that modelling connection handshake with underlying mechanisms turns out not to be simple task. I would suggest to try to address comments and to merge this PR. Then we could consider as a follow up work to think about integration with relayer spec which would allow us to simplify some stuff in this spec that are posing us problems. In my view, all proof related business will be moved outside protocol spec and we can at the protocol level assume that we only receive messages that have passed light client related proof checks. Protocol will also not need to care about height business as it will be managed outside the protocols (by chain abstraction). Hopefully this will make a bit easier expressing what are the conditions in which we expect protocol to terminate and also it would allow us to point out the problems in the current design and help us verify potential protocol improvements.
…tion_handshake_tla Connection Handshake (ICS3) L2 TLA+ spec
WIP for : #4
Rendered version here: ch.tla.
For contributor use:
docs/
) and code commentsFiles changed
in the Github PR explorer