ICS3 connection versioning / model checking in TLA+ #211
Conversation
…rs into ilina/ics3_versions
|
|
||
| __Context__. | ||
| The original issue triggering this discussion is here: [cosmos/ics/#459](https://github.com/cosmos/ics/issues/459). | ||
| Briefly, version negotiation in the ICS3 handshake can interfere in various ways, breaking either the safety or liveness of this protocol. |
There was a problem hiding this comment.
The current liveness issues are expected as the two parties do not agree on a version. Not sure if and how these should be reported. If there would be liveness issue due to protocol bugs (e.g. the two parties do not agree even if there is one common version) the format here would be fine.
There was a problem hiding this comment.
When it comes to liveness, this can suffer in two cases:
- due to empty version intersection, case (a),
- due to mode
onTryNonDet, case (c)
The current liveness issues are expected as the two parties do not agree on a version. Not sure if and how these should be reported.
So this concerns case (a). My initial thought was to classify this as a hidden assumption, which we disclose here. We thus provide a clear reason to make this assumption explicit in the ICS.
If there would be liveness issue due to protocol bugs (e.g. the two parties do not agree even if there is one common version) the format here would be fine.
I agree this is not a bug and rather it's a case of underspecification, but I would say the format here is good for this in fact.
|
Latest version of disclosure log rendered here: |
) * connection handshake with versions, non-deterministic choice of version * added different version picking modes * added comments explaining version picking * connection spec fix * bug in Environment.tla * added overwrite mode * overwrite mode fixes * Update README.md * cleanup in connection handshake spec * fix in sending Ack message * Typos; cleaner Concurrency; added Utils; * Added a WIP marker for the disclosure log * Traces; WIP for ACK cases * Disclosure log ready for review * Added summary table cf. Anca's suggestion. Co-authored-by: istoilkovska <anili100@gmail.com>
Discussion ground for our work to close informalsystems/ibc-rs#117.
Will also close informalsystems/ibc-rs#116.
Description
For contributor use:
docs/) and code commentsFiles changedin the Github PR explorer